Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Recurso digital |
| Lenguaje: | |
| Publicado: |
Zenodo
2026
|
| Acceso en línea: | https://doi.org/10.5281/zenodo.18224541 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866901166639546368 |
|---|---|
| author | adityabagchi2002-boop |
| author_facet | adityabagchi2002-boop |
| contents | <p>This release contains the complete, axiom-free Lean 4 source code validating the results presented in the manuscript "Finite-State Deterministic Validation of the Collatz Conjecture"</p> <p>Verification Status:</p> <p>Engine: Lean 4 (Mathlib)</p> <p>Axiom Check: Passed (Standard Foundations Only; No custom axiom or sorry commands used).</p> <p>CI Status: Passing (Green Badge).</p> <p>Scope of Formalization: This repository formally verifies the two central pillars of the proof:</p> <p>The Perturbation Model (Theorem 1): Validates the structural impossibility of non-trivial integer cycles by proving the mutual exclusivity of the algebraic cycle condition and the 3-adic valuation constraints.</p> <p>The Modular Loop Framework (Theorem 2): Validates the impossibility of divergent trajectories. It formally proves that any "escape path" (aperiodic divergence) requires the core integer to satisfy an infinite system of strictly nested congruences, leading to a direct arithmetic contradiction.</p> <p>Contents:</p> <p>CollatzLEAN_FINAL.lean: The primary source file containing all definitions, lemmas, and theorems.</p> <p>README.md: Documentation on how to reproduce the build and run the axiom check command (#print axioms).</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18224541 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE: Finite-State Deterministic Validation of Collatz Conjecture (Formally Validated) adityabagchi2002-boop <p>This release contains the complete, axiom-free Lean 4 source code validating the results presented in the manuscript "Finite-State Deterministic Validation of the Collatz Conjecture"</p> <p>Verification Status:</p> <p>Engine: Lean 4 (Mathlib)</p> <p>Axiom Check: Passed (Standard Foundations Only; No custom axiom or sorry commands used).</p> <p>CI Status: Passing (Green Badge).</p> <p>Scope of Formalization: This repository formally verifies the two central pillars of the proof:</p> <p>The Perturbation Model (Theorem 1): Validates the structural impossibility of non-trivial integer cycles by proving the mutual exclusivity of the algebraic cycle condition and the 3-adic valuation constraints.</p> <p>The Modular Loop Framework (Theorem 2): Validates the impossibility of divergent trajectories. It formally proves that any "escape path" (aperiodic divergence) requires the core integer to satisfy an infinite system of strictly nested congruences, leading to a direct arithmetic contradiction.</p> <p>Contents:</p> <p>CollatzLEAN_FINAL.lean: The primary source file containing all definitions, lemmas, and theorems.</p> <p>README.md: Documentation on how to reproduce the build and run the axiom check command (#print axioms).</p> |
| title | adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE: Finite-State Deterministic Validation of Collatz Conjecture (Formally Validated) |
| url | https://doi.org/10.5281/zenodo.18224541 |