v1.0 — Machine-Checked Principal Results

Initial release of the Lean 4 proofs for "Minimal Topologies of Forward-Local Failure in AI Systems: The Hamiltonian Microscope."

This release contains two standalone Lean 4 proof files covering the principal formal results of the paper, organized into two groups:

Constraint-System Instantiation

• 252_hamiltonian_constraint_system.lean — Hamiltonian path-game as ConstraintSystem instance (PathGame.toConstraintSystem). Defines an abstract PathGame structure with partial-path states, vertex moves, Hamiltonian-path completions, and the coherence and monotonicity axioms. Constructs the ConstraintSystem instance, thereby inheriting all four Sudoku-Microscope theorems (local-global separation, catastrophic-commitment foreclosure, forced-gate safety, bucket sufficiency) without redundant proof.

Layer 2 Signature Formalization

• 253_layer2_signature.lean — Layer 2 silent-commit signature definition and structural lemmas. Formalizes: the signature predicate (layer2Signature — commit at multi-candidate cell without positive admissibility evidence); the positive-evidence criterion (hasPositiveEvidence, catalog ID 254); the signature locality lemma (layer2_signature_local, ID 262 — signature is local to the failing commit, not global to the run); the indeterminate-not-evidence rider (indeterminate_not_evidence, ID 263); and the emission-without-affirmation rider (emission_without_affirmation_not_evidence, ID 283 — emitting a tool call is not sufficient for verification). Provider-agnostic by construction: the predicate depends only on evidence structure, not on which model produced the trajectory.

The proofs are formulated over the abstract ConstraintSystem framework from the Sudoku-Microscope repo. The 4×4 Hamiltonian grid path-game (start = r1c1, finish = r1c4, 8 valid paths A–H) is one concrete instance; the framework covers any Hamiltonian-path problem on any graph.

All files compile against current Mathlib.

Companion paper: 10.5281/zenodo.20278073