Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Recurso digital |
| Sprache: | |
| Veröffentlicht: |
Zenodo
2026
|
| Online-Zugang: | https://doi.org/10.5281/zenodo.18224541 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
Inhaltsangabe:
- <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>