Preprint (DOI Zenodo, 2026-04-27)
Preprint (Zenodo DOI, 2026-04-27)
Un seul paper a été déposé à ce jour : le théorème principal no_nontrivial_cycle_phase59 et son cadre conditionnel à trois axiomes documentés. Le DOI Zenodo et les sources sont publics. Première soumission éditoriale (2026-04-27) rejetée 2026-05-13 ; repositionnement éditorial en cours (voir changelog).
Only one paper has been deposited to date: the main theorem no_nontrivial_cycle_phase59 and its three-axiom conditional framework. The Zenodo DOI and sources are public. Initial editorial submission (2026-04-27) rejected 2026-05-13; editorial repositioning in progress (see changelog).
Paper 1 — Preprint (v1.1, 28 p.)
Paper 1 — Preprint (v1.1, 28 p.)
On the non-existence of non-trivial Collatz/Syracuse cycles: a conditional formal proof in Lean 4 with documented structural obstructions
28 pages. Preuve formelle conditionnelle modulo trois axiomes externes (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Profil d'axiomes minimal (3 axiomes Lean kernel : propext, Classical.choice, Quot.sound).
Architecture en 7 théorèmes centraux + auxiliaires, kernel-checked, reproductible via reproduce.sh.
28 pages. Conditional formal proof modulo three external axioms (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Minimal axiom profile (3 Lean kernel axioms: propext, Classical.choice, Quot.sound).
Architecture: 7 central theorems + auxiliaries, kernel-checked, reproducible via reproduce.sh.
Contribution principale : pas la non-existence inconditionnelle (irréalisable dans le cadre des outils 2026), mais la cartographie rigoureuse des obstructions structurelles qui rend la conditionnalité nécessaire, pas arbitraire.
Main contribution: not unconditional non-existence (unattainable with 2026 tools), but the rigorous mapping of structural obstructions that makes the conditionality necessary, not arbitrary.
Statut : PREPRINT — v1.1 déposée 2026-04-27 sur Zenodo ; première soumission éditoriale rejetée 2026-05-13, repositionnement en cours
Théorème Lean : no_nontrivial_cycle_phase59 (Phase59ContinuedFractions.lean:236)
DOI : 10.5281/zenodo.19790406
PDF : collatz-conditional-proof.pdf
Sources : paper/v2/
Status: PREPRINT — v1.1 deposited 2026-04-27 on Zenodo; initial editorial submission rejected 2026-05-13, repositioning in progress
Lean theorem: no_nontrivial_cycle_phase59 (Phase59ContinuedFractions.lean:236)
DOI: 10.5281/zenodo.19790406
PDF: collatz-conditional-proof.pdf
Sources: paper/v2/
Profil d'axiomes du résultat principal
Axiom profile of the main result
Le théorème no_nontrivial_cycle_phase59 repose sur un profil d'axiomes minimal et explicite. Aucun sorryAx dans la chaîne critique.
The theorem no_nontrivial_cycle_phase59 rests on a minimal, explicit axiom profile. No sorryAx in the critical chain.
| Catégorie | Identifiant Lean | Énoncé | Source |
|---|---|---|---|
| Axiomes Lean kernel (universels — toutes preuves Mathlib) | |||
| Kernel | propext |
Extensionnalité propositionnelle | Lean core |
| Kernel | Classical.choice |
Axiome du choix | Lean core |
| Kernel | Quot.sound |
Soundness des quotients | Lean core |
| Hypothèses externes documentées (les 3 conditions) | |||
| Externe 1 | BakerSeparation |
$(2^S - 3^k) \cdot k^6 \geq 3^k$ (conjecture de travail — renforcement non démontré des bornes Rhin/Wu/Salikhov publiées, voir mea culpa #28) | Motivé par : Rhin 1987, Simons-de Weger 2005, Wu 2003 |
| Externe 2 | BarinaVerification |
Tous $n < 2^{71}$ atteignent 1 | Barina 2025, J. Supercomp. 81, 810 |
| Externe 3 | DerivedLargeKBound |
Pour tout cycle avec $k > 1322$, $n < 2^{71}$ (dérivation projet ; combine Baker + CF + Product Bound + Barina) | Dérivation projet — cf. HYPOTHESES.md §5 + paper §4. Pas Hercher 2023 (m-cycles, quantité distincte). |
| Category | Lean identifier | Statement | Source |
|---|---|---|---|
| Lean kernel axioms (universal — every Mathlib proof) | |||
| Kernel | propext |
Propositional extensionality | Lean core |
| Kernel | Classical.choice |
Axiom of choice | Lean core |
| Kernel | Quot.sound |
Quotient soundness | Lean core |
| Documented external hypotheses (the 3 conditions) | |||
| External 1 | BakerSeparation |
$(2^S - 3^k) \cdot k^6 \geq 3^k$ (working conjecture — undemonstrated strengthening of published Rhin/Wu/Salikhov bounds, see mea culpa #28) | Motivated by: Rhin 1987, Simons-de Weger 2005, Wu 2003 |
| External 2 | BarinaVerification |
All $n < 2^{71}$ reach 1 | Barina 2025, J. Supercomp. 81, 810 |
| External 3 | DerivedLargeKBound |
For any cycle with $k > 1322$, $n < 2^{71}$ (project-derived; combines Baker + CF + Product Bound + Barina) | Project derivation — see HYPOTHESES.md §5 + paper §4. Not Hercher 2023 (m-cycles, distinct quantity). |
Lecture : si les trois conditions externes sont admises (deux hypothèses Diophantiennes + une vérification computationnelle Barina), alors la non-existence des cycles non-triviaux Collatz est prouvée formellement dans Lean 4, kernel-checked. Les axiomes kernel sont ceux que toute preuve Mathlib utilise — ils ne sont pas spécifiques à ce projet.
Reading: if the three external conditions are admitted (two Diophantine hypotheses + one computational Barina verification), then the non-existence of non-trivial Collatz/Syracuse cycles is formally proven in Lean 4, kernel-checked. The kernel axioms are those used by every Mathlib proof — they are not specific to this project.
Quelques pistes d'écriture explorées
A few writing leads being explored
Cette section liste des travaux d'écriture en cours ou idées à explorer, sans engagement de soumission ni de calendrier. Aucune conférence ni revue n'est ciblée publiquement. Tant qu'un texte n'est pas soumis ou accepté, il reste à l'état de brouillon privé.
This section lists writing work in progress or ideas being explored, without any submission commitment or schedule. No conference or journal is publicly targeted. Until a text is submitted or accepted, it remains a private draft.
δ10 — Barina-Replacement Impossibility (Phase 64)
δ10 — Barina-Replacement Impossibility (Phase 64)
Lemme cartographique fini : aucune borne diophantienne publiée (Salikhov 2007 / Wu 2003 / Rhin 1987 / Simons-de Weger 2005) ne peut remplacer BarinaVerification dans no_nontrivial_cycle_phase59. 0 sorry, axiom profile [propext] (kernel-1 minimal). Three-Key validated (OLD3 + NEW4 + ChatGPT 5.5) — validation interne multi-IA, non peer review (cf. FAQ Q11). Trilogie d'impossibilité Baker+CF+Khinchin maintenant complète : δ8 + δ8' + δ10. → Voir branche study/delta10
Cartographic finite catalogue lemma: no published Diophantine bound (Salikhov 2007 / Wu 2003 / Rhin 1987 / Simons-de Weger 2005) can replace BarinaVerification in no_nontrivial_cycle_phase59. 0 sorry, axiom profile [propext] (kernel-1 minimal). Three-Key validated (OLD3 + NEW4 + ChatGPT 5.5) — internal multi-AI validation, not peer review (see FAQ Q11). Baker+CF+Khinchin impossibility trilogy now complete: δ8 + δ8' + δ10. → See study/delta10 branch
Pattern multi-cerveau antifragile humain-IA
Antifragile human-AI multi-brain pattern
Documentation du pattern méthodologique : multi-instances IA asynchrones, mailbox horodaté, Two/Three-Key Rule, mea culpa publics avec règle extraite. ~28 mea culpa sur le périmètre Collatz à ce jour.
Documentation of the methodological pattern: asynchronous AI multi-instances, time-stamped mailbox, Two/Three-Key Rule, public mea culpa with extracted rules. ~28 mea culpa on the Collatz perimeter to date.
Décomposition Eliahou-Steiner en Lean 4
Eliahou-Steiner block decomposition in Lean 4
Library Lean 4 réutilisable pour les minima locaux, l'amplification de blocs, et le splitting par moyenne géométrique R73 / R76b. État : ~1300 lignes prototypes, à consolider.
Reusable Lean 4 library for local minima, block amplification, and R73 / R76b geometric-mean splitting. Status: ~1300 prototype lines, to consolidate.
δ11 Salikhov-Insufficient-for-3732 — impossibilité granulaire conditionnelle
δ11 Salikhov-Insufficient-for-3732 — conditional granular impossibility
Lemme cartographique conditionnel Lean 4 / Mathlib v4.27 (dernière version stable ; rétro-compat v4.26 non couverte par design — Phase 65, kernel-3 + 3 axiomes ad-hoc transparents) prouvant que Salikhov 2007 ($\mu \leq 5.125$, DOI 10.1134/S1064562407060361) SEUL est insuffisant pour fermer la sous-branche $k \in [3694, 3732]$, contrairement à Wu 2003 ($c = 5.117$, $k_{\max} = 3732$, DOI 10.1090/S0025-5718-02-01442-4). Wu & Wang 2014 ($\mu \leq 5.1163051$, J. Number Theory 142, 264-273, DOI 10.1016/j.jnt.2014.03.007) raffine Salikhov sans changer qualitativement le verdict δ11. Le théorème est CONDITIONNEL sous 3 axiomes ad-hoc transparents : C_Salikhov : ℝ, 0 < C_Salikhov (convention diophantienne effective, explicitée Phase 5e suite catch Gemini ARES shadow) et C_Salikhov < 10^{-30} — pas une dérivation directe du paper Salikhov 2007 ; cohérent avec littérature diophantienne effective (Baker, Mignotte). Cf. mea culpa #29 / #30 / #31 / #32. Phase 6-bis polish (commit 0ec9889) : refactor imports (build −82% : ~67s → ~11s, 2039 jobs) + range narratif explicit + Mathlib v4.27 pin assumé. Le gap résiduel ($k \in [3733, 1.375 \cdot 10^{11}]$) reste conditionnel sur BakerSeparation. Branche study/E1-salikhov-2007-impossibility.
Conditional cartographic Lean 4 / Mathlib v4.27 lemma (latest stable version; v4.26 retro-compatibility not covered by design — Phase 65, kernel-3 + 3 transparent ad-hoc axioms) proving that Salikhov 2007 ($\mu \leq 5.125$, DOI 10.1134/S1064562407060361) alone is insufficient to close the sub-branch $k \in [3694, 3732]$, unlike Wu 2003 ($c = 5.117$, $k_{\max} = 3732$, DOI 10.1090/S0025-5718-02-01442-4). Wu & Wang 2014 ($\mu \leq 5.1163051$, J. Number Theory 142, 264-273, DOI 10.1016/j.jnt.2014.03.007) refines Salikhov without qualitatively changing the δ11 verdict. The theorem is CONDITIONAL under 3 transparent ad-hoc axioms: C_Salikhov : ℝ, 0 < C_Salikhov (effective Diophantine convention, made explicit in Phase 5e following Gemini ARES shadow catch) and C_Salikhov < 10^{-30} — not a direct derivation from Salikhov 2007 paper ; consistent with effective Diophantine literature (Baker, Mignotte). See mea culpa #29 / #30 / #31 / #32. Phase 6-bis polish (commit 0ec9889): imports refactor (build −82%: ~67s → ~11s, 2039 jobs) + explicit narrative range + assumed Mathlib v4.27 pin. The residual gap ($k \in [3733, 1.375 \cdot 10^{11}]$) remains conditional on BakerSeparation. Branch study/E1-salikhov-2007-impossibility.
Knight 2026 — high cycles
Knight 2026 — high cycles
Lecture du paper Knight 2026 (Discrete Math 349(3), 114812). La preuve 2-adique courte de la Section 5 (élimination d'un cycle de Christoffel par paire $(k, x)$) pourrait constituer un excellent lemme auxiliaire en Lean 4, sans fermer le gap résiduel global.
Reading the Knight 2026 paper (Discrete Math 349(3), 114812). The short 2-adic proof of Section 5 (eliminating one Christoffel cycle per $(k, x)$ pair) could make an excellent auxiliary lemma in Lean 4, without closing the residual gap globally.
Aucun de ces travaux n'a de date ferme ni de venue ciblée. Si vous êtes intéressé par une collaboration ou une relecture, ouvrez une discussion GitHub.
None of these works have a firm date or targeted venue. If you are interested in collaboration or review, open a GitHub discussion.
Discussion communautaire
Community discussion
Discussions, questions, et propositions sur GitHub Discussions.
Discussions, questions, and proposals on GitHub Discussions.
→ Ouvrir / participer aux discussions → Open / join discussions