On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions
Fuente:
Zenodo
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Recurso digital |
| Publicado: |
Zenodo
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866902312002256896 |
|---|---|
| author | Merle, Eric |
| author_facet | Merle, Eric |
| contents | <p>We address the no-non-trivial-cycle disjunct of the Collatz conjecture. The central result, formalized in Lean 4 with Mathlib v4.27.0, is a conditional non-existence theorem declared parametrically with three structural hypotheses: BakerSeparation (after Baker 1966), BarinaVerification (after the 2025 computational verification that every positive integer below 2^71 reaches 1), and ProductBoundThreshold, a project-derived cycle-complexity bound made fully explicit in the paper. The Lean formalization is machine-verified with kernel-3 axiom profile, no user axioms and no sorry, and is reproducible via reproduce.sh against an explicit expected_axioms.md baseline.</p> <p>We complement the theorem with two impossibility lemmas (delta-8, delta-8') showing that no uniform algebraic refinement of the Product Bound derivation can eliminate the third hypothesis within the Baker + continued-fraction framework; a literature mapping (delta-9) documenting the absence of any peer-reviewed deterministic upper bound on cycle length in the 1977-2026 results we surveyed; and an alternative disjunctive framing (delta-7) that connects the conditional theorem to Hercher's 2023 lower bound.</p> <p>Source code repository: https://github.com/ericmerle3789/collatz-conditional-cycles (branch main, release v1.0). License: Creative Commons Attribution 4.0 International (CC BY 4.0).</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_19790406 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions Merle, Eric Collatz conjecture 3x+1 problem Collatz cycles linear forms in logarithms Baker's theorem continued fractions irrationality measure formal verification Lean 4 Mathlib <p>We address the no-non-trivial-cycle disjunct of the Collatz conjecture. The central result, formalized in Lean 4 with Mathlib v4.27.0, is a conditional non-existence theorem declared parametrically with three structural hypotheses: BakerSeparation (after Baker 1966), BarinaVerification (after the 2025 computational verification that every positive integer below 2^71 reaches 1), and ProductBoundThreshold, a project-derived cycle-complexity bound made fully explicit in the paper. The Lean formalization is machine-verified with kernel-3 axiom profile, no user axioms and no sorry, and is reproducible via reproduce.sh against an explicit expected_axioms.md baseline.</p> <p>We complement the theorem with two impossibility lemmas (delta-8, delta-8') showing that no uniform algebraic refinement of the Product Bound derivation can eliminate the third hypothesis within the Baker + continued-fraction framework; a literature mapping (delta-9) documenting the absence of any peer-reviewed deterministic upper bound on cycle length in the 1977-2026 results we surveyed; and an alternative disjunctive framing (delta-7) that connects the conditional theorem to Hercher's 2023 lower bound.</p> <p>Source code repository: https://github.com/ericmerle3789/collatz-conditional-cycles (branch main, release v1.0). License: Creative Commons Attribution 4.0 International (CC BY 4.0).</p> |
| title | On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions |
| topic | Collatz conjecture 3x+1 problem Collatz cycles linear forms in logarithms Baker's theorem continued fractions irrationality measure formal verification Lean 4 Mathlib |
| url | https://doi.org/10.5281/zenodo.19790406 |