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 (H1 Baker + Product-Bound + H2 Bařina) et k > 1322 (fermé uniquement par l'hypothèse supposée H3, avec H2). Sous H2, H3 équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque) : seul le cas k ≤ 1322 est démontré sans circularité (erratum du 2 octobre 2026, voir le changelog et la page Papers). sdw_from_cf est un corollaire en aval, pas une étape de la preuve.

The main theorem no_nontrivial_cycle_phase59 splits into two sub-branches: k ≤ 1322 (H1 Baker + Product-Bound + H2 Barina) and k > 1322 (closed only by the assumed hypothesis H3, with H2). Under H2, H3 is equivalent to the conclusion itself (in Lean, k is any return time): only the case k ≤ 1322 is proved without circularity (erratum of 2 October 2026, see the changelog and the Papers page). sdw_from_cf is a downstream corollary, not a step of the proof.

§ I — Vue d'ensemble

§ I — Overview

Architecture macroscopique

Macroscopic architecture

flowchart TB
    A["H1 BakerSeparation
(parameter — working hypothesis)"] --> PB["Phase56 cycle_min_bound_nat
n ≤ (k^7+k)/3"]
    S["Phase52 nSeq_step_mul"] --> PB
    PB --> C["Phase58 no_cycle_k_le_1322"]
    A2["H2 BarinaVerification
(parameter — n < 2^71)"] --> C
    A2 --> F["Phase59 no_cycle_k_gt_1322"]
    A3["H3 DerivedLargeKBound
(ASSUMED parameter:
k > 1322 → n < 2^71)"] --> F
    C --> G["no_nontrivial_cycle_phase59
(Main theorem)"]
    F --> G
    G -.-> E["sdw_from_cf (corollary)"]

    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

H1, H2, H3 sont des paramètres des théorèmes, pas des axiomes Lean. Les vérifications arithmétiques cf_gap_8 … cf_gap_13 ne sont utilisées par aucun théorème de cette chaîne (voir § IV). no_nontrivial_cycle_final (Phase58) est une variante dont la 3e hypothèse est ProductBoundThreshold (k ≤ 982) : c'est elle qu'énonce le PDF Zenodo.

H1, H2, H3 are parameters of the theorems, not Lean axioms. The arithmetic checks cf_gap_8 … cf_gap_13 are used by no theorem of this chain (see § IV). no_nontrivial_cycle_final (Phase58) is a variant whose 3rd hypothesis is ProductBoundThreshold (k ≤ 982): it is the one stated in the Zenodo PDF.

§ 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 : Product-Bound (H1) + Barina (H2)

Small cycles: Product-Bound (H1) + Barina (H2)

Pour $k \leq 1322$, l'hypothèse H1 BakerSeparation (paramètre ; forme effective $(2^s - 3^k) \cdot k^6 \geq 3^k$ — hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme — voir mea culpa #28) donne, sous réserve qu'elle tienne, une borne effective sur $|\Lambda_{S,k}|$. La chaîne Product-Bound $(k^7 + k)/3 < 2^{71}$ implique $n_{\min} < 2^{71}$, ce qui est exclu par H2 BarinaVerification.

For $k \leq 1322$, hypothesis H1 BakerSeparation (parameter; effective form $(2^s - 3^k) \cdot k^6 \geq 3^k$ — working hypothesis, stronger in this form than published effective bounds — see mea culpa #28) gives, under the assumption that it holds, an effective bound on $|\Lambda_{S,k}|$. The Product-Bound chain $(k^7 + k)/3 < 2^{71}$ implies $n_{\min} < 2^{71}$, which is excluded by H2 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 — conséquence de no_cycle_k_le_1322 : $k \geq 92$, sous H1, H2 (nommée par analogie avec le $m \geq 92$ de Hercher 2023, quantité distincte)

    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 — consequence of no_cycle_k_le_1322: $k \geq 92$, under H1, H2 (named by analogy with Hercher 2023's $m \geq 92$, a distinct quantity)

  

§ IV — Sous-branche k > 1322

§ IV — Sub-branch k > 1322

Grands cycles : l'hypothèse supposée H3

Large cycles: the assumed hypothesis H3

Pour $k > 1322$, aucun argument n'est formalisé : le cas est fermé par no_cycle_k_gt_1322, qui ne prend que H2 (barina) et H3 (cf). H3 est supposée, non dérivée ; sous H2, elle équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque). Le dépôt contient aussi six vérifications arithmétiques aux convergents $p_n/q_n$ de $\log_2 3$, faites par native_decide (axiomes Lean.ofReduceBool, Lean.trustCompiler). Elles ne sont utilisées par aucun théorème de la chaîne principale, ne couvrent que $k$ de 665 à 10 590 736 (une plage finie), et le passage de ces fenêtres à H3 n'est pas formalisé (le fichier Phase63 prévu pour cela n'est qu'un squelette). Elles ne démontrent donc pas H3 :

For $k > 1322$, no argument is formalized: the case is closed by no_cycle_k_gt_1322, which takes only H2 (barina) and H3 (cf). H3 is assumed, not derived; under H2 it is equivalent to the conclusion itself (in Lean, k is any return time). The repository also contains six arithmetic checks at the convergents $p_n/q_n$ of $\log_2 3$, done by native_decide (axioms Lean.ofReduceBool, Lean.trustCompiler). They are used by no theorem of the main chain, cover only $k$ from 665 to 10,590,736 (a finite range), and the step from these windows to H3 is not formalized (the Phase63 file intended for it is only a skeleton). They therefore do not prove H3:

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`

sdw_from_cf est un corollaire en aval : à partir des trois hypothèses H1, H2, H3, il établit ProductBoundThreshold (k ≤ 982), vrai par vacuité puisque, sous ces hypothèses, aucun cycle n'existe.

sdw_from_cf is a downstream corollary: from the three hypotheses H1, H2, H3 it establishes ProductBoundThreshold (k ≤ 982), vacuously true since, under these hypotheses, no cycle exists.

→ 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 de Lean 4.27.0, avant la correction du bug de noyau lean4#14576 ; le fichier de steiner_cycle_eq fait partie des 35 fichiers revérifiés sous Lean 4.34.0 les 20 et 21 octobre 2026, celui de no_nontrivial_cycle_phase59 non) à gauche, l'énoncé mathématique informel (lisible) à droite.

For each pivotal theorem, the Lean code (checked by the Lean 4.27.0 kernel, before the fix of kernel bug lean4#14576; the file of steiner_cycle_eq is one of the 35 files re-checked on Lean 4.34.0 on 20–21 October 2026, that of no_nontrivial_cycle_phase59 is not) 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
  have h := steiner_eq n k
  rwa [hcyc.2.2.2] at h

Énoncé mathématique Mathematical statement

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

Steiner identity. Let $(n, k)$ be a hypothetical Collatz cycle starting at $n$, with $k$ odd terms. 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 theorem

Lean 4

theorem no_nontrivial_cycle_phase59
    (baker : BakerSeparation) (barina : BarinaVerification)
    (cf : DerivedLargeKBound)
    (n k : ℕ) (hcyc : IsOddCycle n k) : False := by
  by_cases hk : k ≤ 1322
  · exact no_cycle_k_le_1322 baker barina n k hcyc hk
  · push_neg at hk
    exact no_cycle_k_gt_1322 barina cf n k hcyc hk

Énoncé mathématique Mathematical statement

Théorème principal (Merle 2026). Sous les trois hypothèses H1 BakerSeparation, H2 BarinaVerification et H3 DerivedLargeKBound (paramètres du théorème) :

Main theorem (Merle 2026). Under the three hypotheses H1 BakerSeparation, H2 BarinaVerification and H3 DerivedLargeKBound (parameters of the theorem):

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

(IsOddCycle n k impose $n > 1$.) La preuve se décompose en deux sous-branches : $k \leq 1322$ (H1 + H2, via le Product-Bound) et $k > 1322$ (H3 + H2). Erratum (2 octobre 2026) : H3 est supposée, non dérivée ; sous H2 elle équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque). Seul « aucun cycle non trivial avec $k \leq 1322$, sous H1 et H2 » est démontré sans circularité.

(IsOddCycle n k requires $n > 1$.) The proof splits in two sub-branches: $k \leq 1322$ (H1 + H2, via the Product-Bound) and $k > 1322$ (H3 + H2). Erratum (2 October 2026): H3 is assumed, not derived; under H2 it is equivalent to the conclusion itself (in Lean, k is any return time). Only "no non-trivial cycle with $k \leq 1322$, under H1 and H2" is proved without circularity.

§ VI — Verrou structurel

§ VI — Structural lock

Pourquoi la voie Product-Bound ne ferme pas les grands cycles

Why the Product-Bound route does not close large cycles

Le Product-Bound $n \leq (k^7+k)/3$ passe sous $2^{71}$ seulement jusqu'à $k = 1322$. L'énoncé δ8 ci-dessous explique pourquoi cette voie ne peut pas, à elle seule, fermer la fenêtre des grands cycles. C'est un énoncé sur une méthode de preuve : il ne remplace pas H3 et n'exclut aucun cycle.

The Product-Bound $n \leq (k^7+k)/3$ stays below $2^{71}$ only up to $k = 1322$. The δ8 statement below explains why this route cannot, on its own, close the window of large cycles. It is a statement about a proof method: it does not replace H3 and excludes no cycle.

δ8 (Product-Bound impossibility)

Pour fermer la fenêtre actuelle, la chaîne Product-Bound aurait besoin d'une minoration $K \ln 2 - k \ln 3 > k^{-c}$ avec un exposant de forme linéaire $c \approx 0{,}96$ (soit une mesure d'irrationalité $\mu = c + 1 \approx 1{,}96$). Or le théorème de Dirichlet impose $c \geq 1$ ($\mu \geq 2$) : cette voie est fermée, quelle que soit la constante, avec une marge d'environ 0,04 sur l'exposant. C'est un énoncé sur une méthode de preuve : il n'exclut aucun cycle et n'est pas formalisé en Lean.

To close the current window, the Product-Bound chain would need a lower bound $K \ln 2 - k \ln 3 > k^{-c}$ with a linear-form exponent $c \approx 0.96$ (i.e. an irrationality measure $\mu = c + 1 \approx 1.96$). Dirichlet's theorem forces $c \geq 1$ ($\mu \geq 2$): this route is closed, whatever the constant, by a margin of about 0.04 in the exponent. This is a statement about a proof method: it excludes no cycle and is not formalized in Lean.

Source : registre commun, entrée L-A9 (LEDGER.md ; convention corrigée en août 2026). L'énoncé du PDF Zenodo et de paper/v2/05-obstruction-I-product-bound-impossibility.md mélange les deux conventions. La conclusion rejoint une remarque de Halbeisen et Hungerbühler (Acta Arith. 78 (1997), §5, p. 238) : des estimations valables pour les cycles rationnels ne suffisent pas, seules, à exclure les cycles entiers. L'esquisse de preuve du Lemme 5.1 du PDF est retirée (erratum de la version Zenodo v4, item 7).

Source: shared ledger, entry L-A9 (LEDGER.md; convention corrected in August 2026). The statement in the Zenodo PDF and in paper/v2/05-obstruction-I-product-bound-impossibility.md mixes the two conventions. The conclusion amounts to a remark of Halbeisen and Hungerbühler (Acta Arith. 78 (1997), §5, p. 238): estimates valid for rational cycles cannot on their own exclude integer cycles. The proof sketch of Lemma 5.1 in the PDF is withdrawn (erratum of the Zenodo v4 version, item 7).

§ 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
# (toolchain imposée par le script : Lean 4.27.0)

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
# (toolchain required by the script: Lean 4.27.0)

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

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