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 — paper soumis JAR Springer

Aucun cycle Collatz non-trivial — modulo trois conditions explicites

Le théorème principal no_nontrivial_cycle_phase59 est kernel-checked en Lean 4 (Mathlib v4.27), avec un profil d'axiomes minimal (3 axiomes Lean kernel : propext, Classical.choice, Quot.sound) et trois hypothèses externes documentées : BakerSeparation (séparation effective sur |S log 2 − k log 3|, motivée par les bornes Baker-type Rhin 1987 / Simons-de Weger 2005 / Wu 2003 — l'exposant utilisé dans notre formalisation Lean est plus strict que les bornes publiées et constitue donc une hypothèse explicite, pas un théorème dérivé), BarinaVerification (n < 2⁷¹), DerivedLargeKBound (Hercher 2023, m ≤ 91).

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
borne effective
(plus stricte que publié)"]
    BARINA["Barina 2025
n < 2^71"]
    HERCHER["Hercher 2023
m ≤ 91"]
    JAR["★ JAR
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"]

    LAMBDA -->|"axiome 1"| BAKER
    BAKER -->|"BakerSeparation"| JAR
    BARINA -->|"BarinaVerification"| JAR
    HERCHER -->|"DerivedLargeKBound"| JAR

    DELTA8 -.->|"justifie"| HERCHER
    DELTA8P -.->|"justifie"| HERCHER
    DELTA10 -.->|"justifie"| BARINA

    style LAMBDA fill:#c8a86a,color:#0e0f13,stroke:#fff,stroke-width:2px
    style BAKER fill:#6a9b7a,color:#0e0f13
    style BARINA fill:#6a9b7a,color:#0e0f13
    style HERCHER fill:#6a9b7a,color:#0e0f13
    style JAR 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

→ Le théorème JAR 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 (Baker, Barina, Hercher) — 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 12 mea culpa parmi les 28 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é

δ10 — Barina-Replacement Impossibility

VALIDATED 2026-04-30

Lemme cartographique fini. Lean 4 kernel-checked, axiom profile [propext] only, 0 sorry. Cartographic finite catalogue lemma. Lean 4 kernel-checked, axiom profile [propext] only, 0 sorry.

→ Voir brancheSee branch

Statut paper

JAR Springer — Submitted

SUBMITTED 2026-04-27

"On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4". DOI Zenodo. Under review. "On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4". Zenodo DOI. Under review.

→ DOI Zenodo

Dernière vérification Lean

reproduce.sh EXIT 0

VALIDATED 2026-04-30

25 théorèmes probés (7 central + 3 aux + 15 M3). 0 sorryAx. Toolchain Lean 4.27.0. 25 theorems probed (7 central + 3 aux + 15 M3). 0 sorryAx. Lean 4.27.0 toolchain.

→ reproduce.sh

Dernier audit résolu

FIND-016 — BakerSeparation k^6

RESOLVED 2026-04-30

AI-assisted Three-Key audit. Doc-comment Lean transparency note. Mea culpa #28 publié. AI-assisted Three-Key audit. Lean transparency note. Public mea culpa #28.

→ Voir auditSee audit

Études en cours

3 études actives 3 active studies

IN PROGRESS 2026-04-30

Eliahou-Steiner formalisation · Désaxiomatisation Baker (Salikhov/Wu) · Knight 2026 lecture critique. Eliahou-Steiner formalization · Baker desaxiomatisation (Salikhov/Wu) · Knight 2026 critical reading.

→ 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.

Soumission JAR Springer (paper 28 p., DOI Zenodo)
Architecte du PROTOCOLE ARES v2 (28 mea culpa publics)
Direction multi-cerveau (NEW · NEW2 · OLD · Red Team)

JAR Springer submission (28-page paper, Zenodo DOI)
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).