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 (PostJAR) 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 (PostJAR) 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 dépendent uniquement des trois axiomes fondamentaux du noyau Lean. Aucun sorryAx dans la chaîne critique.

The central theorems rely only on the three fundamental axioms of the Lean kernel. 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

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 (LMN95)
BarinaVerification (n < 2^71)
DerivedLargeKBound (Hercher)

§ 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 JAR. ● Axiomes externes (Baker, Barina, Hercher) · ● 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 = JAR main result. ● External axioms (Baker, Barina, Hercher) · ● 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 — PostJAR

Arsenal R34-R96 (PostJAR)

Extensions développées après la soumission JAR. Trois familles principales :

Extensions developed after the JAR submission. 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