Cartographie scientifique · Pré-publication

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

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 (LMN95), 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["Baker LMN95
borne effective"]
    BARINA["Barina 2025
n < 2^71"]
    HERCHER["Hercher 2023
m ≤ 91"]
    JAR["★ JAR
no_nontrivial_cycle_phase59
kernel-checked Lean 4"]

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

    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

→ 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

Vingt-huit 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.

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

§ VI

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

§ VII

É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).

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 (25 mea culpa publics)
Direction multi-cerveau (NEW · NEW2 · OLD · Red Team)

JAR Springer submission (28-page paper, Zenodo DOI)
Architect of PROTOCOLE ARES v2 (25 public mea culpa)
Multi-brain coordination (NEW · NEW2 · OLD · Red Team)

ORCID GitHub Email

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

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