Frontier Closure and a Proposed Computer-Assisted Proof of the Collatz Conjecture via the Five-Lemma Quotient Admission Framework — Proof Package

This repository contains the complete proof package for a proposed computer-assisted proof of the Collatz Conjecture via the Five-Lemma Quotient Admission Framework, comprising Lemmas A–E. The proposed proof remains conditional on the computational and verification conditions RC1–RC4 stated in the paper. Proof package The package includes: the main paper and companion proof documents a plain-English explainer proof-chain documentation, including Documents 93 and 100–127 a Lean 4 proof skeleton 33 core Python audit scripts finite-state-machine closure certificates entry and refinement certificates the merged pinned residue guard SHA-256 manifests archived logs and exact tool copies Lean 4 formalisation Build results: 3,331 build jobs zero build errors no Collatz-specific axioms foundational dependencies only: propext Classical.choice Quot.sound The Lean project is a formal skeleton and axiom ledger. It is not presented as a complete machine-checked proof of the Collatz Conjecture. Computational certificates The proof package includes: 5,666 coarse M674 finite-state-machine states all 5,666 states independently certified closed zero open states zero nondeterministic states zero nonclosed rows entry certificates for refinement rounds 1–4 delta-12, delta-16 and zero-zero refinement artefacts a merged pinned residue guard containing 5,537,661 rows zero open pinned-residue cases The audit scripts cover: finite-state-machine closure exact seam verification proof-gate auditing constructor and admission checks root-tube lineage Mersenne corridor closure D-layer verification pinned-descent verification certificate replay and consistency checks Version 2.1 validation update Version 2.1 adds a CSV-independent synthetic quotient-layer stress certificate for the door-collapse mechanism at the deliberately hostile power depth: d = 2^4096 This is a 1234-digit quotient depth. The verifier generates the synthetic post-ramp quotient layer directly from: x0 ≡ 2 × 3^(d−1) × w − 1 (mod 2^P) The calculation does not depend on the original q-frontier CSV files. The certified run checked every odd w satisfying: 1 ≤ w ≤ 2^20 Results: 524,288 states checked 524,288 states closed zero failures maximum tail length: 2,056 accelerated steps maximum B: 4,113 minimum precision remaining: 28,655 bits positive full-bit affine margin reached in every tested state Independent replay verification A separate replay check examined: 300 independently replayed states all 50 emitted top-stress rows zero mismatches With 4,096 bits of precision and a 320-step bound, two states remained unresolved rather than being reported as closed. After increasing the limits to 32,768 precision bits and 4,096 accelerated steps, both states and the complete tested layer closed. Version 2.1 files The added validation package contains: POWER_JUMP_COLLAPSE_HORIZON_NOTE_d2pow4096.md D2POW4096_INDEPENDENT_RECHECK.md power_jump_2pow4096_outputs.zip SHA256SUMS_V2_1_ADDENDUM.txt The output archive includes: result JSON failures CSV top-stress CSV replay results collapse-horizon certificate claim ledger checksum information exact tool copies used for the run Interpretation The Version 2.1 certificate establishes the following finite computational statement: For d = 2^4096 and every odd w ≤ 2^20, the synthetic post-ramp quotient state reaches positive full-bit affine margin within 4,096 accelerated steps using 32,768 bits of 2-adic precision. The result validates the door-collapse mechanism for the complete tested 20-bit odd quotient layer at an extreme power depth. It strengthens the computational verification package without relying on the earlier q-frontier CSV files. It does not change the paper’s stated conditional status under RC1–RC4. Proof status The proposed proof concludes that every positive integer trajectory under the Collatz map eventually reaches 1, subject to RC1–RC4. The package is presented as: a proposed computer-assisted proof finite and independently auditable conditional on the authenticity and correctness of the supplied certificates, constructors, audit scripts and upstream proof artefacts not an unconditional classical proof See PAPER_COLLATZ_FRONTIER_CLOSURE_V2.pdf for the complete theorem statement, Five-Lemma framework, computational conditions, proof chain and reviewer checklist. Author Dennis Knightknighty101@gmail.com