Architecture · Phase 12 → Phase 63

Chaîne de preuve formelle

Formal proof chain

Le théorème principal no_nontrivial_cycle_phase59 se décompose en deux sous-branches : k ≤ 1322 (Barina + Product-Bound) et k > 1322 (continued fractions de $\log_2 3$). La transition s'opère par sdw_from_cf, le lemme conditionnel clé qui dérive la borne Simons-de Weger des fractions continues.

The main theorem no_nontrivial_cycle_phase59 splits into two sub-branches: k ≤ 1322 (Barina + Product-Bound) and k > 1322 (continued fractions of $\log_2 3$). The transition is handled by sdw_from_cf, the key conditional lemma that derives the Simons-de Weger bound from continued fractions.

§ I — Vue d'ensemble

§ I — Overview

Architecture macroscopique

Macroscopic architecture

flowchart TB
    A["Axiom BakerSeparation
(LMN95 1995)"] --> B["Phase52SteinerEquation
steiner_cycle_eq"]
    A2["Axiom BarinaVerification
(n < 2^71)"] --> C["Phase58PorteDeuxFinal
no_cycle_k_le_1322"]
    A3["Axiom DerivedLargeKBound
(Hercher m ≤ 91)"] --> C

    B --> C
    B --> D["Phase59ContinuedFractions
cf_gap_8 ... cf_gap_13
(native_decide)"]

    D --> E["Phase59
sdw_from_cf"]
    E --> F["Phase59
no_cycle_k_gt_1322"]

    C --> G["no_nontrivial_cycle_phase59
(Main theorem)"]
    F --> G

    G --> H["Alias variants:
no_nontrivial_cycle_final
no_nontrivial_cycle_derived
no_nontrivial_cycle_full"]

    style A fill:#9080a8,color:#0e0f13
    style A2 fill:#9080a8,color:#0e0f13
    style A3 fill:#9080a8,color:#0e0f13
    style G fill:#c8a86a,color:#0e0f13,stroke:#fff,stroke-width:2px
    style H fill:#6a9b7a,color:#0e0f13

§ II — Phase 52

Identité de Steiner

Steiner identity

Pour tout cycle Collatz hypothétique IsOddCycle n k, l'identité fondamentale s'écrit :

For any hypothetical Collatz cycle IsOddCycle n k, the fundamental identity reads:

$$n \cdot 2^S = 3^k \cdot n + \mathrm{corrSum}\,n\,k$$

Cette identité est universelle (pas de Baker requise). Elle est prouvée dans Phase52SteinerEquation.lean par steiner_cycle_eq.

This identity is universal (no Baker required). It is proven in Phase52SteinerEquation.lean by steiner_cycle_eq.

→ Voir Phase52SteinerEquation.lean → View Phase52SteinerEquation.lean

§ III — Sous-branche k ≤ 1322

§ III — Sub-branch k ≤ 1322

Petits cycles : Barina + Product-Bound

Small cycles: Barina + Product-Bound

Pour $k \leq 1322$, Baker LMN95 (sous forme axiome) donne $|\Lambda_{S,k}| > C/k^7$ effective. La chaîne Product-Bound $(k^7 + k)/3 < 2^{71}$ implique $n_\min < 2^{71}$, ce qui est exclu par BarinaVerification.

For $k \leq 1322$, Baker LMN95 (as an axiom) gives effective $|\Lambda_{S,k}| > C/k^7$. The Product-Bound chain $(k^7 + k)/3 < 2^{71}$ implies $n_\min < 2^{71}$, which is excluded by BarinaVerification.

    Théorèmes clés (Phase58PorteDeuxFinal)
    Key theorems (Phase58PorteDeuxFinal)
    product_bound_fits_barina_1322 — vérification numérique $(1322^7+1322)/3 < 2^{71}$
k1322_bound_implies_n_bound — implication $k \leq 1322 \Rightarrow n < 2^{71}$
no_cycle_k_le_1322 — résultat final pour cette sous-branche
hercher_from_baker_barina — dérivation Hercher m ≤ 91 conditional

    product_bound_fits_barina_1322 — numerical verification $(1322^7+1322)/3 < 2^{71}$
k1322_bound_implies_n_bound — implication $k \leq 1322 \Rightarrow n < 2^{71}$
no_cycle_k_le_1322 — final result for this sub-branch
hercher_from_baker_barina — conditional Hercher m ≤ 91 derivation

  

§ IV — Sous-branche k > 1322

§ IV — Sub-branch k > 1322

Grands cycles : continued fractions

Large cycles: continued fractions

Pour $k > 1322$, l'argument classique (Lagarias 1985, Simons-de Weger 2005) utilise les convergents $p_n/q_n$ de $\log_2 3$. Six fenêtres arithmétiques sont vérifiées par native_decide :

For $k > 1322$, the classical argument (Lagarias 1985, Simons-de Weger 2005) uses the convergents $p_n/q_n$ of $\log_2 3$. Six arithmetic windows are verified via native_decide:

Fenêtre	Convergent (p_n, q_n)	Inégalité prouvée
Window	Convergent (p_n, q_n)	Proven inequality
W8	`(1054, 665)`	`cf_gap_8` : $2 \cdot 2^{1055} \geq 3 \cdot 3^{665}$
W9	`(24727, 15601)`	`cf_gap_9`
W10	`(50508, 31867)`	`cf_gap_10`
W11	`(125743, 79335)`	`cf_gap_11`
W12	`(176251, 111202)`	`cf_gap_12`
W13	`(301994, 190537)`	`cf_gap_13`

Le lemme conditionnel sdw_from_cf dérive la borne Simons-de Weger des fractions continues, et no_cycle_k_gt_1322 conclut.

The conditional lemma sdw_from_cf derives the Simons-de Weger bound from continued fractions, and no_cycle_k_gt_1322 closes the argument.

→ Voir Phase59ContinuedFractions.lean → View Phase59ContinuedFractions.lean

§ V — Lean ↔ Mathématiques

§ V — Lean ↔ Mathematics

Vue côte-à-côte : code Lean et énoncé informel

Side-by-side view: Lean code and informal statement

Pour chaque théorème pivot, le code Lean (vérifié par le noyau) à gauche, l'énoncé mathématique informel (lisible) à droite.

For each pivotal theorem, the Lean code (kernel-verified) on the left, the informal mathematical statement (readable) on the right.

steiner_cycle_eq — Phase52 universal identity

Lean 4

theorem steiner_cycle_eq
    (n k : ℕ) (hcyc : IsOddCycle n k) :
    n * 2 ^ (aSumSeq n k) = 3 ^ k * n + corrSum n k := by
  -- preuve par récurrence sur la longueur k du cycle
  -- Mathlib v4.27, kernel-checked, 0 sorry

Énoncé mathématique Mathematical statement

Identité de Steiner. Soit un cycle Collatz $(n, k)$ hypothétique de longueur $k$, avec $n$ minimum. Alors :

Steiner identity. Let $(n, k)$ be a hypothetical Collatz cycle of length $k$, with $n$ minimum. Then:

$$n \cdot 2^S = 3^k \cdot n + \mathrm{corrSum}(n, k)$$

où $S = \sum_{i} a_i$ est la somme des valuations 2-adiques le long du cycle.

where $S = \sum_{i} a_i$ is the sum of 2-adic valuations along the cycle.

no_nontrivial_cycle_phase59 — ★ Main JAR theorem

Lean 4

theorem no_nontrivial_cycle_phase59 :
    ∀ (n k : ℕ), n > 1 → ¬ IsOddCycle n k := by
  intro n k hn
  by_contra hcyc
  -- (1) k ≤ 1322 → no_cycle_k_le_1322 (Barina + Product-Bound)
  -- (2) k > 1322 → no_cycle_k_gt_1322 (continued fractions + Baker)
  rcases Nat.lt_or_ge k 1323 with hk | hk
  · exact no_cycle_k_le_1322 hcyc hk
  · exact no_cycle_k_gt_1322 hcyc hk

Énoncé mathématique Mathematical statement

Théorème principal (Merle 2026). Sous les trois hypothèses externes BakerSeparation, BarinaVerification, et DerivedLargeKBound :

Main theorem (Merle 2026). Under the three external hypotheses BakerSeparation, BarinaVerification, and DerivedLargeKBound:

$$\forall\, n > 1,\ \forall\, k \in \mathbb{N},\ \neg\, \mathrm{IsOddCycle}(n, k)$$

i.e. il n'existe aucun cycle Collatz non-trivial. La preuve se décompose en deux sous-branches selon que $k \leq 1322$ (Barina) ou $k > 1322$ (continued fractions de $\log_2 3$).

i.e. there exists no non-trivial Collatz cycle. The proof splits in two sub-branches depending on whether $k \leq 1322$ (Barina) or $k > 1322$ (continued fractions of $\log_2 3$).

§ VI — Verrou structurel

§ VI — Structural lock

Pourquoi les 3 axiomes sont nécessaires

Why the 3 axioms are necessary

Le δ8 lemma (paper §5 obstruction-I) prouve structurellement qu'aucune dérivation de la forme Baker + continued fractions + Khinchin ne peut produire de borne uniforme algébrique $F(k) < 2^{71}$ pour tout $k$. La conditionnalité sur Baker n'est donc pas un placeholder, mais une obstruction prouvée.

The δ8 lemma (paper §5 obstruction-I) structurally proves that no derivation of the form Baker + continued fractions + Khinchin can produce a uniform algebraic bound $F(k) < 2^{71}$ for every $k$. The conditionality on Baker is therefore not a placeholder, but a proven obstruction.

Lemma δ8 (Product-Bound Impossibility)

Soit $\xi \in \mathbb{R} \setminus \mathbb{Q}$ avec mesure d'irrationalité effective $\mu(\xi) \leq c$. Alors aucune borne uniforme algébrique $F(k) < 2^{71}$ ne peut être obtenue via la chaîne Product-Bound pour tout $k \in \mathbb{N}$.

Let $\xi \in \mathbb{R} \setminus \mathbb{Q}$ with effective irrationality measure $\mu(\xi) \leq c$. Then no uniform algebraic bound $F(k) < 2^{71}$ can be obtained via the Product-Bound chain for every $k \in \mathbb{N}$.

Source : paper/v2/05-obstruction-I-product-bound-impossibility.md

Source: paper/v2/05-obstruction-I-product-bound-impossibility.md

§ VII — Reproductibilité

§ VII — Reproducibility

Vérifier la chaîne complète

Verify the complete chain

git clone https://github.com/ericmerle3789/collatz-conditional-cycles.git
cd collatz-conditional-cycles
./reproduce.sh
# EXIT 0 = build green, axioms match expected_axioms.md, 0 sorry detected

git clone https://github.com/ericmerle3789/collatz-conditional-cycles.git
cd collatz-conditional-cycles
./reproduce.sh
# EXIT 0 = build green, axioms match expected_axioms.md, 0 sorry detected

→ Voir le catalogue détaillé des lemmes
→ Repo GitHub complet
→ DOI Zenodo 10.5281/zenodo.19790406

→ See the detailed lemma catalog
→ Full GitHub repo
→ Zenodo DOI 10.5281/zenodo.19790406