Spremljeno u:
| Glavni autor: | |
|---|---|
| Format: | Recurso digital |
| Jezik: | |
| Izdano: |
Zenodo
2026
|
| Teme: | |
| Online pristup: | https://doi.org/10.5281/zenodo.19790406 |
| Oznake: |
Dodaj oznaku
Bez oznaka, Budi prvi tko označuje ovaj zapis!
|
Sadržaj:
- <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>