Авторский контракт словаря математических утверждений Arxo

ru · unofficial · sha256:80e96ac5f6464d4b8ab405452a0a67c731fefd05a48911ac2893b928096708d2

Авторский контракт словаря математических утверждений Arxo, версия 0.1.0. Claim обозначает опознаваемое математическое утверждение (формулировку), не привязанное к конкретному источнику. Source обозначает библиографический или институциональный источник — публикацию, автора, организацию. Proof обозначает доказательство claim; само доказательство остаётся у источника, контракт лишь удостоверяет его существование там. Evidence обозначает вычислительное или проверочное свидетельство о claim. Scope обозначает область применимости claim или evidence. source_asserts(src, c) — источник утверждает claim: эмпирический факт о содержании источника, не о его истинности. source_proves(src, p, c) — источник обладает доказательством p claim c; доказательство не переносится в корпус и не проверяется повторно. conditional_on(c, hyp) — источник утверждает c при условии hyp: связывает условное следствие с его посылкой. assumed_in_scenario(hyp) — hyp принят как допущение именно этого сценария; факт дела, а не общее утверждение пакета. source_reports_open(src, c, asof) и source_reports_solved(src, c, asof) — раздельные датированные сообщения источника о статусе claim; несовпадающие сообщения разных источников не сливаются в одно. source_verified(src, c, ev) — источник сообщает о выполненной им проверке; факт о содержании публикации, не о том, что проверка воспроизведена здесь. computation_reproduced(ev) — институциональный факт, produced только правилом, которое действительно выполнило или проверило вычисление в этом корпусе; из source_verified он не выводится. has_scope(c, s) и evidence_has_scope(ev, s) — claim или evidence заявлены в границах области применимости s. established_by_source(c) выводится только из source_proves: источник опубликовал доказательство. established_under_assumption(c) выводится только из conditional_on и assumed_in_scenario данного сценария: снятие допущения снимает и вывод. Ни verified_by_system, ни computation_reproduced не участвуют в выводе established_*: конечная проверка не доказывает общее утверждение, а её локальное воспроизведение не заменяет доказательство. Отсутствие established_*(c) в ответе — NEITHER движка, не значение «c ложно» и не суждение об открытости c во всей математике; статус «открыта» берётся только из source_reports_open с его датой снимка.

Ссылаются нормы: Claim, ConsequenceUnderAssumption, ConsequenceUnderEstablishedPremise, EstablishedBySourceProof, Evidence, Proof, Scope, Source, assumed_in_scenario, computation_reproduced, conditional_on, depends_on_rh_directly, depends_on_rh_transitively, established_by_source, established_under_assumption, evidence_has_scope, has_scope, source_asserts, source_proves, source_reports_open, source_reports_solved, source_verified