Catalogue Lean 4 · Mathlib v4.27.0

Théorèmes formellement vérifiés

Formally verified theorems

Sept théorèmes centraux constituent la chaîne de preuve de no_nontrivial_cycle_phase59, plus l'arsenal R34-R96 (extensions post-preprint) qui étend le transport modulaire et la décomposition par blocs. Tous sont kernel-checked et passent reproduce.sh EXIT 0.

Seven central theorems form the proof chain of no_nontrivial_cycle_phase59, plus the R34-R96 arsenal (post-preprint extensions) that extends modular transport and block decomposition. All are kernel-checked and pass reproduce.sh EXIT 0.

§ I

Profil d'axiomes

Axiom profile

Les théorèmes centraux reposent sur deux types d'hypothèses distincts : (1) les axiomes du noyau Lean (3, standards : propext, Classical.choice, Quot.sound) ; (2) les 3 hypothèses externes documentées (1 conjecture de travail : BakerSeparation, Baker 1966 / Matveev 2000 effectif ; 1 vérification computationnelle reproductible : BarinaVerification n<2⁷¹, Barina 2025 ; 1 dérivation projet : DerivedLargeKBound, k>1322 ⇒ n<2⁷¹, combine Baker + fractions continues + Product Bound + Barina, n'est pas un théorème publié — cf. HYPOTHESES.md §5). Aucun sorryAx dans la chaîne critique.

The central theorems rely on two distinct types of hypotheses: (1) Lean kernel axioms (3, standard: propext, Classical.choice, Quot.sound); (2) 3 documented external hypotheses (1 working conjecture: BakerSeparation, Baker 1966 / Matveev 2000 effective; 1 reproducible computational verification: BarinaVerification n<2⁷¹, Barina 2025; 1 project-derived hypothesis: DerivedLargeKBound, k>1322 ⇒ n<2⁷¹, combines Baker + continued fractions + Product Bound + Barina, not a published theorem — see HYPOTHESES.md §5). No sorryAx in the critical chain.

Axiomes (S) — Kernel Lean standard

Axioms (S) — Standard Lean kernel

3 axiomes universels

3 universal axioms

propext
Classical.choice
Quot.sound

Axiomes (N) — native_decide

Axioms (N) — native_decide

2 axiomes computationnels

2 computational axioms

Lean.ofReduceBool
Lean.trustCompiler

Utilisés par les cf_gap_* arithmétiques.

Used by the arithmetic cf_gap_*.

Hypothèses externes

External hypotheses

3 axiomes documentés

3 documented axioms

BakerSeparation (conjecture de travail — renforcement non démontré des bornes Rhin 1987 / Wu 2003 / Salikhov 2007 publiées ; voir #28 + lemme δ10)(working hypothesis / conjecture — undemonstrated strengthening of published Rhin 1987 / Wu 2003 / Salikhov 2007 bounds; see #28 + δ10 lemma)
BarinaVerification (n < 2^71)
DerivedLargeKBound (dérivation projet : k>1322 ⇒ n<2^71, n'est pas un théorème publié)(project-derived: k>1322 ⇒ n<2^71, not a published theorem)

§ II — Théorèmes centraux

§ II — Central theorems

Chaîne de preuve principale

Main proof chain

§ III — Graphe de dépendances

§ III — Dependency graph

Architecture interactive (D3 force-directed)

Interactive architecture (D3 force-directed)

Graphe interactif de l'architecture de la preuve. Drag pour déplacer les nœuds, scroll pour zoomer. Étoile dorée = résultat principal. ● Hypothèses externes (BakerSeparation, BarinaVerification, DerivedLargeKBound) · ● Axiomes Lean kernel · ● Lemmes auxiliaires · ● Théorèmes centraux. Lignes pleines = dépendances logiques, pointillés courts = axiomes kernel, pointillés longs dorés = alias.

Interactive graph of the proof architecture. Drag to reposition nodes, scroll to zoom. Golden star = main result. ● External hypotheses (BakerSeparation, BarinaVerification, DerivedLargeKBound) · ● Lean kernel axioms · ● Auxiliary lemmas · ● Central theorems. Solid lines = logical dependencies, short dashes = kernel axioms, long golden dashes = aliases.

§ IV — CF Windows

Continued fractions arithmetic gaps

Les théorèmes cf_gap_8 à cf_gap_13 calculent les inégalités arithmétiques aux convergents de $\log_2 3$, validées par native_decide.

Theorems cf_gap_8 to cf_gap_13 compute arithmetic inequalities at the convergents of $\log_2 3$, validated by native_decide.

Window	Convergent (p, q)	Théorème	Tactique
Window	Convergent (p, q)	Theorem	Tactic

§ V — Auxiliaires

§ V — Auxiliaries

Lemmes de l'arsenal

Arsenal lemmas

Théorèmes auxiliaires qui constituent les briques de la preuve principale : identité de Steiner, positivité de $D_s$, transport modulaire, périodisation lacunaire.

Auxiliary theorems that form the building blocks of the main proof: Steiner identity, positivity of $D_s$, modular transport, lacunary periodization.

§ VI — Extensions post-preprint

Arsenal R34-R96 (extensions post-preprint)

Extensions développées après le dépôt du preprint v1.1 (2026-04-27). Trois familles principales :

Extensions developed after the v1.1 preprint deposit (2026-04-27). Three main families:

§ VII — Reproductibilité

§ VII — Reproducibility

Vérifier la preuve localement

Verify the proof locally

Tout est reproductible depuis un clone propre via reproduce.sh. Le script vérifie : compilation propre, profil d'axiomes attendu, absence de sorryAx.

Everything is reproducible from a clean clone via reproduce.sh. The script checks: clean compilation, expected axiom profile, no sorryAx.

Procédure

Procedure

git clone https://github.com/ericmerle3789/collatz-conditional-cycles.git
cd collatz-conditional-cycles
./reproduce.sh

# EXIT 0 = build green + axioms match + 0 sorry detected
# Runtime Mac M1 Pro 16 GB : ~3-5 min avec cache, ~10s incrémental

git clone https://github.com/ericmerle3789/collatz-conditional-cycles.git
cd collatz-conditional-cycles
./reproduce.sh

# EXIT 0 = build green + axioms match + 0 sorry detected
# Runtime Mac M1 Pro 16 GB: ~3-5 min cached, ~10s incremental

→ Voir reproduce.sh sur GitHub
→ Voir expected_axioms.md (matrice d'axiomes attendus)

→ View reproduce.sh on GitHub
→ View expected_axioms.md (expected axiom matrix)

Discussion communautaire

Community discussion

Discussions techniques sur les théorèmes Lean et l'arsenal Diophantien.

Technical discussions on the Lean theorems and Diophantine arsenal.

→ Ouvrir / participer aux discussions → Open / join discussions