Авторский контракт композиции «Poincare conjecture» Arxo

ru · unofficial · sha256:95dd47621987ab15147ec3c265e7a895c99e400993939ab9314acc550baa38f8

Авторский контракт композиции «Poincare conjecture» Arxo, версия 0.1.0. Пакет связывает записи разных владельцев (cmi.poincare, hamilton.ricci_flow_program, perelman.entropy_2002, perelman.surgery_2003, perelman.finite_extinction_2003) через общий словарь arxo.three_manifolds/arxo.math_claims, не создавая собственных фактов взамен чужих. poincare_conjecture_established(c) -- НОВОЕ институциональное отношение композиции, вычисляемое ТОЛЬКО когда established_by_source верно ОДНОВРЕМЕННО для ВСЕХ ЧЕТЫРЁХ оснований: hamilton.ricci_flow_program::HamiltonRicciFlowProgramClaim, perelman.entropy_2002::PerelmanEntropyClaim, perelman.surgery_2003::PerelmanSurgeryClaim и perelman.finite_extinction_2003::PerelmanFiniteExtinctionClaim. Отсутствие любого ОДНОГО из четырёх -- задание намеренно не удаляет established_by_source ни одного из них (все четыре установлены каждым своим доктринальным пакетом безусловно), поэтому граничный сценарий "недостающего основания" тестируется отдельным сценарием со специально урезанным миром (без одного из четырёх доктринальных пакетов), а не попыткой снять established_by_source внутри полного мира. homeomorphic_to_sphere(m) -- применение ПРИНЯТОЙ теоремы к предъявленному конкретному многообразию: когда poincare_conjecture_established держится и m удовлетворяет гипотезе (dimension=3, closed, is_simply_connected), заключение выводится ДЛЯ ЭТОГО m -- НЕ постулируется словарём arxo.three_manifolds напрямую (см. его package.law). proof_assistant_verified(c) -- институциональное отношение, ОБЪЯВЛЕННОЕ здесь и НИКОГДА не устанавливаемое ни одним правилом всего набора: наличие статей Перельмана и их established_by_source НЕ означает, что Arxo (или какой-либо proof assistant) повторно проверил доказательство -- признанное математическое доказательство (established_by_source через source_proves трёх статей Перельмана и работы Гамильтона), его источниковая формализация (claim и Proof в этом наборе) и фактическая проверка proof assistant -- ТРИ РАЗНЫХ факта, и набор формализует только первые два.

Ссылаются нормы: CollectEstablishedResult, CollectPoincareFormulation, PoincareConjectureEstablished, PoincareTheoremAppliesToManifold, established_results_summary, grounding_result_presented, poincare_conjecture_established, poincare_formulation_from, proof_assistant_verified