Catalogue Lean 4 · Mathlib v4.27.0

Catalogue des théorèmes Lean

Lean theorem catalog

Sept théorèmes centraux (le théorème principal no_nontrivial_cycle_phase59, ses deux sous-branches, le corollaire sdw_from_cf et trois variantes) sont contrôlés par reproduce.sh sur la branche main : vérifiés par le noyau de Lean 4.27.0 (Mathlib v4.27.0), avant la correction du bug de noyau lean4#14576 (Lean v4.32.2, 28/07/2026). Quatre d'entre eux, no_cycle_k_le_1322, no_nontrivial_cycle_final, no_nontrivial_cycle_derived et no_nontrivial_cycle_full, ont été revérifiés sous Lean 4.34.0, qui contient la correction de lean4#14576, les 20 et 21 octobre 2026 ; ils ne dépendent que de propext, Classical.choice et Quot.sound. Les trois autres, no_nontrivial_cycle_phase59, no_cycle_k_gt_1322 et sdw_from_cf, n'ont pas été revérifiés (détails et limites : recheck-v4.34-2026-10-20). L'arsenal R34-R96 (extensions post-preprint, branche arsenal-postjar) étend le transport modulaire et la décomposition par blocs ; ce sont des prototypes, dont certains énoncés sont encore laissés en sorry.

Seven central theorems (the main theorem no_nontrivial_cycle_phase59, its two sub-branches, the corollary sdw_from_cf and three variants) are checked by reproduce.sh on the main branch: checked by the Lean 4.27.0 kernel (Mathlib v4.27.0), before the fix of kernel bug lean4#14576 (Lean v4.32.2, 28 July 2026). Four of them, no_cycle_k_le_1322, no_nontrivial_cycle_final, no_nontrivial_cycle_derived and no_nontrivial_cycle_full, were re-checked on Lean 4.34.0, which includes the fix of lean4#14576, on 20–21 October 2026; they depend only on propext, Classical.choice and Quot.sound. The other three, no_nontrivial_cycle_phase59, no_cycle_k_gt_1322 and sdw_from_cf, were not re-checked (details and limits: recheck-v4.34-2026-10-20). The R34-R96 arsenal (post-preprint extensions, arsenal-postjar branch) extends modular transport and block decomposition; these are prototypes, some of whose statements are still left as sorry.

§ 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 H1-H3, qui sont des paramètres des théorèmes, pas des axiomes Lean (H1 BakerSeparation : hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme, voir mea culpa #28 ; H2 BarinaVerification : traduction d'un résultat de calcul publié, Bařina 2025, n<2⁷¹ ; H3 DerivedLargeKBound, k>1322 ⇒ n<2⁷¹ : hypothèse supposée, non dérivée ; équivaut sous H2 à la conclusion elle-même (en Lean, k est un temps de retour quelconque) — cf. HYPOTHESES.md, section H3, qui la présente comme une dérivation : c'est corrigé par l'erratum du 02/10/2026). Selon la référence expected_axioms.md (Lean 4.27.0), 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) the 3 hypotheses H1-H3, which are parameters of the theorems, not Lean axioms (H1 BakerSeparation: working hypothesis, stronger in this form than published effective bounds, see mea culpa #28; H2 BarinaVerification: encoding of a published computational result, Barina 2025, n<2⁷¹; H3 DerivedLargeKBound, k>1322 ⇒ n<2⁷¹: assumed hypothesis, not derived; under H2 equivalent to the conclusion itself (in Lean, k is any return time) — see HYPOTHESES.md, section H3, which presents it as a derivation: corrected by the erratum of 2 Oct 2026). According to the reference expected_axioms.md (Lean 4.27.0), 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, hors de la chaîne du théorème principal.

Used by the arithmetic cf_gap_*, outside the chain of the main theorem.

Hypothèses H1-H3 (paramètres)

Hypotheses H1-H3 (parameters)

3 hypothèses (pas des axiomes Lean)

3 hypotheses (not Lean axioms)

H1 BakerSeparation (hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme ; voir mea culpa #28)(working hypothesis, stronger in this form than published effective bounds; see mea culpa #28)
H2 BarinaVerification (traduction d'un résultat de calcul publié : Bařina 2025, n < 2^71)(encoding of a published computational result: Barina 2025, n < 2^71)
H3 DerivedLargeKBound (k>1322 ⇒ n<2^71 : hypothèse supposée, non dérivée ; équivaut sous H2 à la conclusion elle-même (en Lean, k est un temps de retour quelconque))(k>1322 ⇒ n<2^71: assumed hypothesis, not derived; under H2 equivalent to the conclusion itself (in Lean, k is any return time))

§ 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 H1-H3 (paramètres ; H3 supposée) · ● Axiomes Lean kernel · ● Lemmes auxiliaires · ● Théorèmes centraux. Lignes pleines = dépendances logiques, pointillés courts = axiomes kernel. Les variantes (autres hypothèses, pas de simples alias) ne sont pas reliées au résultat principal.

Interactive graph of the proof architecture. Drag to reposition nodes, scroll to zoom. Golden star = main result. ● Hypotheses H1-H3 (parameters; H3 assumed) · ● Lean kernel axioms · ● Auxiliary lemmas · ● Central theorems. Solid lines = logical dependencies, short dashes = kernel axioms. The variants (other hypotheses, not mere aliases) are not connected to the main result.

§ 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. Ce sont des vérifications isolées : aucun théorème de la chaîne principale ne les utilise, et elles ne démontrent pas H3.

Theorems cf_gap_8 to cf_gap_13 compute arithmetic inequalities at the convergents of $\log_2 3$, validated by native_decide. These are isolated checks: no theorem of the main chain uses them, and they do not prove H3.

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 du projet : identité de Steiner, positivité de $D_s$, transport modulaire, périodisation lacunaire.

Auxiliary theorems of the project: 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 (avril 2026), sur la branche arsenal-postjar. Ce sont des prototypes : certains fichiers (par exemple PadeBound.lean, CycleArithmetic.lean) contiennent encore des énoncés laissés en sorry. Trois familles principales :

Extensions developed after the preprint deposit (April 2026), on the arsenal-postjar branch. These are prototypes: some files (e.g. PadeBound.lean, CycleArithmetic.lean) still contain statements left as sorry. Three main families:

§ VII — Reproductibilité

§ VII — Reproducibility

Vérifier la preuve localement

Verify the proof locally

La chaîne principale (branche main) est reproductible depuis un clone propre via reproduce.sh, sous Lean 4.27.0 (toolchain imposée par le script). Le script vérifie : compilation propre, profil d'axiomes attendu, absence de sorryAx.

The main chain (main branch) is reproducible from a clean clone via reproduce.sh, on Lean 4.27.0 (toolchain required by the script). 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