no_nontrivial_cycle_phase59 · kernel-checked Lean 4 · Mathlib v4.27

Cartographie scientifique · Pré-publication

Une enquête sur les cycles non triviaux conjecturés de la suite de Collatz, formalisée en Lean 4.

Aussi connue en France sous le nom de Conjecture de Syracuse (« suite de Syracuse », « algorithme de Syracuse », « problème 3n+1 »). Also known as the Syracuse problem, the 3n+1 problem, the Kakutani problem, the Hasse algorithm, or the Ulam conjecture.

Trente-cinq pistes mathématiques, trois axiomes piliers, une famille d'hypothèses ouvertes — organisées autour d'une obstruction diophantienne unique : l'inégalité de verrou reliant le nombre d'étapes impaires au nombre d'étapes paires d'un cycle hypothétique.

Résultat principal — preprint 28 p. (DOI Zenodo)

Théorème conditionnel : aucun cycle Collatz non-trivial — modulo 3 axiomes externes documentés

⚠ Théorème CONDITIONNEL⚠ CONDITIONAL theorem — modulo 3 hypothèses externes documentées : BakerSeparation (conjecture de travail, Baker 1966 / Matveev 2000 effectif), BarinaVerification (n<2⁷¹, vérification computationnelle reproductible Barina 2025), DerivedLargeKBound (dérivation projet, k>1322 ⇒ n<2⁷¹, n'est pas un théorème publié — cf. HYPOTHESES.md §5). Ne prouve PAS la conjecture Collatz. — modulo 3 documented external hypotheses: BakerSeparation (working conjecture, Baker 1966 / Matveev 2000 effective), BarinaVerification (n<2⁷¹, reproducible computational verification, Barina 2025), DerivedLargeKBound (project-derived hypothesis, k>1322 ⇒ n<2⁷¹, not a published theorem — see HYPOTHESES.md §5). Does NOT prove the Collatz conjecture.

Le théorème principal no_nontrivial_cycle_phase59 est kernel-checked en Lean 4 (Mathlib v4.27), avec 3 axiomes Lean kernel (propext, Classical.choice, Quot.sound) et 3 hypothèses externes documentées : BakerSeparation (conjecture de travail, renforcement non démontré des bornes Rhin 1987 / Wu 2003 / Salikhov 2007 publiées — voir #28 + δ10 + δ11), BarinaVerification (n < 2⁷¹, vérification computationnelle reproductible, Barina 2025), DerivedLargeKBound (dérivation projet, k > 1322 ⇒ n < 2⁷¹ ; combine BakerSeparation + gaps fractions continues log₂3 + Product Bound + BarinaVerification ; n'est pas un théorème publié — cf. HYPOTHESES.md §5 ; Hercher 2023 sur les m-cycles porte sur une quantité différente (m = minima locaux, ≠ k = pas impairs) et n'est pas la source de DerivedLargeKBound).

Contribution scientifique : pas la non-existence inconditionnelle (cf. δ8 lemma, irréalisable avec les outils 2026), mais la cartographie rigoureuse des obstructions structurelles qui rend la conditionnalité nécessaire, pas arbitraire. Sept théorèmes centraux, ~30 fichiers Lean, paper 28 pages, reproductible via reproduce.sh EXIT 0.

→ Lire le paper (PDF, 28 p.) → DOI Zenodo → Architecture de la preuve

2,4·10⁻⁹

Borne inf. |Λ|

Salikhov 2007 inconditionnel

k ≥ 2·10²⁰

Requis pour cycle

Hercher 2023 conditional Baker

δ₈ = 8

Lemme du verrou

Product-Bound Impossibility

35+

Pistes étudiées

Région I + II + III

Λ_{S,k}

Le verrou Λ_{S,k}

Quatorze des quinze paradigmes mathématiques investigués retombent sur la même obstruction diophantienne :

$$\Lambda_{S,k} = S \log 2 - k \log 3$$

graph LR
    P1["Tao 2019 ergodique"] -->|"Haar 0 ≠ ∅"| LAMBDA
    P2["Kolmogorov-Chaitin"] -->|"K=O(log k)"| LAMBDA
    P3["Fourier Sturmien"] -->|"slope log_2 3"| LAMBDA
    P4["Padé / Wu / Salikhov"] -->|"plafond μ ≥ 5.117"| LAMBDA
    P5["Marcovecchio 2025"] -->|"μ_2 algébriques"| LAMBDA
    P6["Tropical (oracle)"] -->|"décroissance fine"| LAMBDA
    P7["Schémas + Faltings"] -->|"hauteurs ⇔ ABC"| LAMBDA
    P8["Néron-Tate"] -->|"ABC effective"| LAMBDA
    P9["Tresses / Nœuds"] -->|"insensible 2/3-adique"| LAMBDA
    P10["Logique modèle"] -->|"Cobham 2 bases"| LAMBDA
    P11["Skolem-Mahler-Lech"] -->|"non-LRS"| LAMBDA
    P12["Anashin 2-adique"] -->|"ergodicité ℤ_2"| LAMBDA
    P13["Krasikov-Lagarias"] -->|"densité aveugle"| LAMBDA
    P14["Holomorphic LSW"] -->|"log|ρ| = -Λ"| LAMBDA
    P15["Inv. statistiques"] -->|"autocorr. Christoffel"| LAMBDA

    LAMBDA["Λ_{S,k}
VERROU"]
    BAKER["BakerSeparation
(conjecture de travail)
renforcement non démontré
de Rhin/Wu/Salikhov"]
    BARINA["Barina 2025
n < 2^71"]
    DERIVED["DerivedLargeKBound
dérivation projet
k > 1322 → n < 2^71"]
    MAIN["★ Main result
no_nontrivial_cycle_phase59
kernel-checked Lean 4"]

    DELTA8["δ8 (Phase58)
Product-Bound
impossibility"]
    DELTA8P["δ8' (Phase58 §5.2)
Baker+CF lower
not upper"]
    DELTA10["δ10 (Phase64)
Barina-Replacement
impossibility · kernel-1"]
    DELTA11["δ11 (Phase65)
Salikhov-Insufficient
conditional · kernel-3 + 3 ad-hoc"]

    LAMBDA -->|"axiome 1"| BAKER
    BAKER -->|"BakerSeparation"| MAIN
    BARINA -->|"BarinaVerification"| MAIN
    DERIVED -->|"3e hypothèse externe"| MAIN

    DELTA8 -.->|"justifie"| DERIVED
    DELTA8P -.->|"justifie"| DERIVED
    DELTA10 -.->|"justifie"| BARINA
    DELTA11 -.->|"justifie (CONDITIONNEL)"| BAKER

    style LAMBDA fill:#c8a86a,color:#0e0f13,stroke:#fff,stroke-width:2px
    style BAKER fill:#6a9b7a,color:#0e0f13
    style BARINA fill:#6a9b7a,color:#0e0f13
    style DERIVED fill:#6a9b7a,color:#0e0f13
    style MAIN fill:#f3d99c,color:#0e0f13,stroke:#c8a86a,stroke-width:3px
    style DELTA8 fill:#3a4a5a,color:#e0e6f0,stroke:#6366f1,stroke-width:1px
    style DELTA8P fill:#3a4a5a,color:#e0e6f0,stroke:#6366f1,stroke-width:1px
    style DELTA10 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px
    style DELTA11 fill:#3a4a5a,color:#e0e6f0,stroke:#fb923c,stroke-width:2px,stroke-dasharray:5

→ Le théorème principal no_nontrivial_cycle_phase59 est l'unique nœud de fermeture conditionnelle. Les 14 paradigmes convergent vers le verrou Λ ; seules les 3 hypothèses externes (BakerSeparation, BarinaVerification, DerivedLargeKBound) — et non les paradigmes — alimentent le théorème final.

§ I

Catalogue des voies d'attaque

Catalogue exhaustif des approches mathématiques pour la non-existence des cycles non triviaux Collatz. Cliquez sur une ligne pour voir les détails. Transparence éditoriale : 21 entrées sur 36 (≈58 %) sont en statut stub — notes exploratoires en attente de sourçage formel ; le champ status_meta du JSON les marque explicitement (cf. assets/data/pistes.json).

ID	Nom	Région	Statut	4-test	Lean	Source

§ III

Trois hypothèses sur la sortie

Évolution des probabilités estimées au fil des cycles d'investigation (Cycle 0 → Cycle 2). La hausse de C reflète la convergence cumulative des paradigmes vers Λ_{S,k}.

Combinaison Baker+CF+Khinchin

Baker+CF+Khinchin combination

Probabilité finale : <5% — bloquée par le δ8 lemma (paper §5 obstruction-I).

Final probability: <5% — blocked by the δ8 lemma (paper §5 obstruction-I).

Combinaison HORS-δ8 (holonomy)

δ8-FREE combination (holonomy)

Probabilité finale : 8-12% — voie Calegari-Dimitrov-Tang 2025, hors cadre Baker+CF.

Final probability: 8-12% — Calegari-Dimitrov-Tang 2025 route, outside the Baker+CF framework.

Téléportation hors domaine

Out-of-domain teleportation

Probabilité finale : 5-10% — 9 sur 11 culs-de-sac dans la Région II.

Final probability: 5-10% — 9 of 11 dead-ends in Region II.

Riemann-class (sortie inaccessible 2026)

Riemann-class (exit unreachable in 2026)

Probabilité finale : 75-80% — dominante après convergence δ8 + Cobham + 14 paradigmes.

Final probability: 75-80% — dominant after δ8 + Cobham + 14 paradigms convergence.

Le δ8 lemma — impossibilité structurelle

The δ8 lemma — structural impossibility

Lemma δ8 (Product-Bound Impossibility) — Soit $\xi \in \mathbb{R} \setminus \mathbb{Q}$ avec mesure d'irrationalité effective $\mu(\xi) \leq c$. Supposons un cycle Collatz $(n,k)$ avec borne Product-Bound $m \leq (k^{c+1}+k)/3$. Alors aucune borne uniforme algébrique $F(k) < 2^{71}$ ne peut être obtenue via cette dérivation pour tout $k \in \mathbb{N}$.

Lemma δ8 (Product-Bound Impossibility) — Let $\xi \in \mathbb{R} \setminus \mathbb{Q}$ have effective irrationality measure $\mu(\xi) \leq c$. Suppose a Collatz cycle $(n,k)$ with Product-Bound $m \leq (k^{c+1}+k)/3$. Then no uniform algebraic bound $F(k) < 2^{71}$ can be obtained via this derivation for every $k \in \mathbb{N}$.

Lemme R72 (Lean 4)

Lemma R72 (Lean 4)

Identité Steiner factorisée — pierre angulaire de l'arsenal.

Factored Steiner identity — cornerstone of the arsenal.

Lean · compiled/-- R72 NEW — identité Steiner factorisée :
    n · (2^S - 3^k) = corrSum n k.
    Universel : pour tout cycle `IsOddCycle n k`. -/
theorem cycle_n_mul_D_s_eq_corrSum
    (n k : ℕ) (hcyc : IsOddCycle n k) :
    n * ((2 : ℕ) ^ (aSumSeq n k) - 3 ^ k) = corrSum n k := by
  have h_steiner_nat : n * 2 ^ (aSumSeq n k) = 3 ^ k * n + corrSum n k :=
    steiner_cycle_eq n k hcyc
  have h_pow_gt : 2 ^ (aSumSeq n k) > 3 ^ k :=
    cycle_pow2_gt_pow3_universal n k hcyc
  have h_n_D_distrib : n * ((2 : ℕ) ^ (aSumSeq n k) - 3 ^ k) =
                       n * 2 ^ (aSumSeq n k) - n * 3 ^ k := by
    rw [Nat.mul_sub_left_distrib]
  rw [h_n_D_distrib, h_steiner_nat]
  have h_comm : 3 ^ k * n = n * 3 ^ k := by ring
  omega

Lemme R92 (Lean 4)

Lemma R92 (Lean 4)

Premier certificat fini case-by-case dérivé de l'arsenal lacunaire.

First finite case-by-case certificate derived from the lacunary arsenal.

Lean · compiled/-- R92 NEW — Showcase : pour cycle k=2 avec aSeq[0] ≡ 1 mod 3
    et aSeq[1] ≡ 1 mod 3, on a 7 ∤ D_s. -/
theorem cycle_k_2_parity_1_1_p_7_no_dvd_D_s
    (n : ℕ) (hcyc : IsOddCycle n 2)
    (h_s_0 : aSeq n 0 % 3 = 1)
    (h_s_1 : aSeq n 1 % 3 = 1) :
    ¬ (7 : ℕ) ∣ ((2 : ℕ) ^ (aSumSeq n 2) - 3 ^ 2) := by
  apply cycle_lacunary_nonzero_implies_p_nmid_D_s n 2 7 hcyc
  rw [orderOf_2_ZMod_7, orderOf_3_ZMod_7]
  have h_aS_0 : aSumSeq n 0 = 0 := by unfold aSumSeq aSum; simp
  have h_aS_1 : aSumSeq n 1 = aSeq n 0 := aSumSeq_one_eq n
  rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero]
  simp only [zero_add]
  rw [h_aS_0, h_aS_1]
  decide

§ IV

Tests REQ-MATH-NNN exécutés

Chaque assertion mathématique est validée par script dans le sandbox tests_math/, conformément au PROTOCOLE ARES (Règle 1 : zéro calcul mental).

§ V

Vingt-huit mea culpa publics

La discipline antifragile demande que chaque erreur détectée soit documentée publiquement avec sévérité 0-10 et règle extraite. Sans cela, le pattern multi-cerveau humain-IA répète indéfiniment les mêmes hallucinations. Aperçu de 16 mea culpa parmi les 32 documentés au total ; archive complète dans le repo GitHub _handoff_mailbox/.

§ VI

État des travaux

Snapshot d'activité du projet, traçable sur GitHub. Registre complet (Research Ledger) →

Cette section documente l'état du projet et sa traçabilité ; elle ne constitue pas une revendication d'acceptation ou de preuve finale. This section documents project status and traceability; it is not a claim of acceptance or final proof.

Dernier jalon validé

δ11 — Salikhov-Insufficient-for-3732 (CONDITIONNEL)

VALIDATED 2026-05-08

Closure conditionnelle E.1 Salikhov 2007. Lean 4 / Mathlib v4.27 kernel-checked. kernel-3 + 3 axiomes ad-hoc transparents. Score G3 6/6 cross-val ~37/37 + 0 réserve. 4 mea culpa publics #29-32. Conditional closure of approach E.1 Salikhov 2007. Lean 4 / Mathlib v4.27 kernel-checked. kernel-3 + 3 transparent ad-hoc axioms. G3 6/6 cross-val score ~37/37 + 0 reservation. 4 public mea culpa #29-32.

→ Voir tag v0.7.3-delta11See tag v0.7.3-delta11

Statut paper

Preprint — Zenodo (v1.1, 28 p.)

PREPRINT 2026-04-27

"On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4". DOI Zenodo permanent. Première soumission éditoriale 2026-04-27 rejetée 2026-05-13 ; repositionnement éditorial en cours, voir changelog et research ledger. "On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4". Permanent Zenodo DOI. Initial editorial submission 2026-04-27 rejected 2026-05-13; editorial repositioning in progress, see changelog and research ledger.

→ DOI Zenodo

Dernière vérification Lean

lake build Delta11Salikhov PASS (Mathlib v4.27)

VALIDATED 2026-05-08

2039 jobs / ~11s / 0 warning post-Phase 6-bis polish (−82% vs ~67s pré-polish). 0 sorry, 0 admit. Profil axiomes kernel-3 + 3 ad-hoc transparents. 2039 jobs / ~11s / 0 warning post-Phase 6-bis polish (−82% vs ~67s pre-polish). 0 sorry, 0 admit. Axiom profile kernel-3 + 3 transparent ad-hoc.

→ Delta11Salikhov.lean

Dernier audit résolu

Mea culpa #29 #30 #31 #32 (5-IA cross-validation catch)

RESOLVED 2026-05-08

Cycle δ11 closure E.1 — cross-modèle a payé son prix DEUX FOIS : ChatGPT catché DOI Wu&Wang erroné (#31), Gemini catché axiome non-positivement-restreint (#32). Score G3 6/6 cross-val ~37/37 + 0 réserve. δ11 E.1 closure cycle — cross-model paid its price TWICE: ChatGPT caught wrong Wu&Wang DOI (#31), Gemini caught non-positively-restricted axiom (#32). G3 6/6 cross-val score ~37/37 + 0 reservation.

→ Voir tag v0.7.3-delta11See tag v0.7.3-delta11

Études en cours

2 études actives 2 active studies

IN PROGRESS 2026-05-08

Eliahou-Steiner formalisation · Knight 2026 lecture critique. (Désaxiomatisation Baker E.1 Salikhov : fermée conditionnellement par δ11 le 2026-05-08, voir tag v0.7.3-delta11.) Eliahou-Steiner formalization · Knight 2026 critical reading. (Baker desaxiomatisation E.1 Salikhov: conditionally closed by δ11 on 2026-05-08, see tag v0.7.3-delta11.)

→ Voir étudesSee studies

§ VII

Communauté Collatz

Ressources et collaborations existantes autour de la conjecture de Collatz (vérifiées 2026-04-29).

ccchallenge.org

The Collatz Conjecture Challenge

Formalisation de la littérature Collatz, paper par paper. 358 papers à formaliser, forum GitHub Discussions + Discord communautaire.

Formalization of the Collatz literature, paper by paper. 358 papers to formalize, GitHub Discussions forum + community Discord.

→ ccchallenge.org

Terry Tao

What's new — blog

Blog WordPress de Terence Tao. Post 2019 fondateur : « Almost all Collatz orbits attain almost bounded values ».

Terence Tao's WordPress blog. Foundational 2019 post: "Almost all Collatz orbits attain almost bounded values".

→ terrytao.wordpress.com

Lagarias

The Ultimate Challenge — AMS 2010

Bibliographie annotée 1963-2009 par Jeffrey C. Lagarias (Univ. Michigan), curateur informel de la littérature Collatz.

Annotated 1963-2009 bibliography by Jeffrey C. Lagarias (Univ. Michigan), informal curator of the Collatz literature.

→ AMS Lagarias 3x+1 overview

tcosmo

coreli — Collatz Research Library

Bibliothèque Python (Jupyter) pour expérimentation et test d'hypothèses sur le processus de Collatz.

Python (Jupyter) library for experimentation and hypothesis testing on the Collatz process.

→ github.com/tcosmo/coreli

Quanta

Mathematician Proves Huge Result

Article de vulgarisation sur les avancées Tao 2019. Décembre 2019, Erica Klarreich.

Popular-science article on the Tao 2019 advances. December 2019, Erica Klarreich.

→ Quanta Magazine

Wikipedia

Collatz conjecture

Article complet, bibliographie, historique. Disponible en français et anglais.

Complete article, bibliography, history. Available in French and English.

→ Wikipedia

§ VIII

Équipe

Ce projet est conduit par un chercheur indépendant en collaboration avec des systèmes d'IA, sous protocole de vérification rigoureux (PROTOCOLE ARES v2).

Investigateur principal

Principal Investigator

Eric Merle

Chercheur indépendant · France

Independent researcher · France

Conception et coordination scientifique du projet. Auteur du PROTOCOLE ARES v2, méthodologie de vérification anti-hallucination pour la recherche mathématique humain-IA. Travaille en architecture multi-agents (Claude Opus + ChatGPT) sous discipline antifragile : chaque erreur détectée devient une règle opérationnelle publique.

Project design and scientific coordination. Author of PROTOCOLE ARES v2, an anti-hallucination verification methodology for human-AI mathematical research. Works under a multi-agent architecture (Claude Opus + ChatGPT) with antifragile discipline: every detected error becomes a public operational rule.

Preprint 28 p. (DOI Zenodo 10.5281/zenodo.19790406)
Architecte du PROTOCOLE ARES v2 (28 mea culpa publics)
Direction multi-cerveau (NEW · NEW2 · OLD · Red Team)

28-page preprint (Zenodo DOI 10.5281/zenodo.19790406)
Architect of PROTOCOLE ARES v2 (28 public mea culpa)
Multi-brain coordination (NEW · NEW2 · OLD · Red Team)

ORCID GitHub Email

Agents de recherche IA

AI Research Agents

Claude Opus (Anthropic)

Architecture multi-cerveau asynchrone. Quatre sous-agents (NEW, NEW2, OLD, Red Team) communiquant via mailbox horodaté. Discipline antifragile : chaque erreur détectée est documentée publiquement pour produire des règles opérationnelles applicables.

Asynchronous multi-brain architecture. Four sub-agents (NEW, NEW2, OLD, Red Team) communicating via timestamped mailbox. Antifragile discipline: every detected error is documented publicly to produce applicable operational rules.

NEW — direction de recherche
NEW2 — spécialiste Lean
OLD — intuition mathématique
Red Team — audit adversarial

NEW — research direction
NEW2 — Lean specialist
OLD — mathematical intuition
Red Team — adversarial audit

Oracle stratégique

Strategic Oracle

ChatGPT 5.5 (OpenAI)

Validation indépendante. Consultations structurées sur les questions stratégiques : méta-prompts à rôles multiples, recherche de contre-exemples, auto-vérification falsifiable. Application de la Two-Key Rule — aucun résultat n'est validé par l'instance qui l'a généré.

Independent validation. Structured consultations on strategic questions: multi-role meta-prompts, counter-example search, falsifiable self-verification. Two-Key Rule applied — no result is validated by the instance that produced it.

Validation croisée des paradigmes
Bibliographie tagée [VÉRIFIÉ]/[INCERTAIN]
Document de synthèse régénéré

Cross-validation of paradigms
Bibliography tagged [VERIFIED]/[UNCERTAIN]
Regenerated synthesis document

Méthodologie

Methodology

Cette cartographie résulte d'un protocole de recherche humain-IA encadré par le PROTOCOLE ARES v2 (Audit, Rigueur, Évaluation, Sécurité). Toutes les affirmations mathématiques sont vérifiées par script (sandbox tests_math/), toutes les références sont vérifiées contre references.bib avant citation, et chaque erreur détectée est documentée publiquement.

This cartography results from a human-AI research protocol governed by PROTOCOLE ARES v2 (Audit, Rigor, Evaluation, Security). Every mathematical claim is verified by script (sandbox tests_math/), every reference is verified against references.bib before citation, and every detected error is documented publicly.

Inspirations méthodologiques : Polymath Project (Tao, Gowers), Lean community (Mathlib), formalisation collaborative (ccchallenge.org).

Methodological inspirations: Polymath Project (Tao, Gowers), Lean community (Mathlib), collaborative formalization (ccchallenge.org).