Guardat en:
| Autor principal: | |
|---|---|
| Format: | Recurso digital |
| Idioma: | |
| Publicat: |
Zenodo
2026
|
| Accés en línia: | https://doi.org/10.5281/zenodo.20073716 |
| Etiquetes: |
Afegir etiqueta
Sense etiquetes, Sigues el primer a etiquetar aquest registre!
|
Taula de continguts:
- <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Initial release of the Lean 4 proofs for "Minimal Topologies of Forward-Local Failure in AI Systems: The Hamiltonian Microscope."</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">This release contains two standalone Lean 4 proof files covering the principal formal results of the paper, organized into two groups:</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Constraint-System Instantiation</p> <ul class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-disc flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">252_hamiltonian_constraint_system.lean</code> — Path-Game Is a Constraint System (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PathGame.toConstraintSystem</code>): defines the abstract <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PathGame</code> structure with partial-path states, vertex moves, Hamiltonian-path completions, and the two <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">ConstraintSystem</code> axioms (coherence and monotonicity); provides the constructor establishing the formal connection. As a consequence, the four Sudoku-Microscope structural theorems — local-global separation, catastrophic-commitment foreclosure, forced-gate safety, and bucket sufficiency — apply to path-games by inheritance. The 4×4 instance (start = r1c1, finish = r1c4, exactly 8 valid Hamiltonian paths) is one concrete instantiation; the framework covers any Hamiltonian-path problem.</li> </ul> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Layer 2 Signature Formalization</p> <ul class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-disc flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">253_layer2_signature.lean</code> — Layer 2 Silent-Commit Signature (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">layer2Signature</code>): defines the silent-commit signature as a formal predicate — a catastrophic commit satisfies the signature iff it occurs at a multi-candidate cell AND the committed tuple lacks positive admissibility evidence. Provider-agnostic well-definedness (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">layer2_provider_agnostic</code>): the predicate depends only on the evidence record and the local-validity structure of the state, not on which model produced the trajectory. Paper 8's novel formal concept — the 195/195 cross-provider replication is the empirical finding that all observed catastrophic commits satisfy this signature; the Lean file formalizes the signature itself as a provider-agnostic structural predicate.</li> </ul> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">The two files together build on the abstract <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">ConstraintSystem</code> framework developed in Sudoku-Microscope (Paper 7). File 252 instantiates that framework for Hamiltonian path-games, making the four Sudoku-Microscope structural theorems available by inheritance. File 253 adds the Layer 2 silent-commit signature formalization — the novel formal content specific to this paper's cross-provider pilot. The 4×4 Hamiltonian instance is the empirically tested domain; the framework covers any Hamiltonian-path problem on any graph.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">All files compile against current Mathlib.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Companion paper: <a class="underline underline underline-offset-2 decoration-1 decoration-current/40 hover:decoration-current focus:decoration-current" href="https://doi.org/10.5281/zenodo.20278073">10.5281/zenodo.20278073</a></p>