Λ Cycles Conditionnels de Collatz Collatz / Syracuse Conditional Cycles
Historique versionné
Versioned history

Changelog

Changelog

Historique transparent de toutes les évolutions du projet : paper, arsenal Lean, site web, cycles Red Team, et mea culpa publics. Versioning sémantique. → Atom feed

Transparent history of all project evolutions: paper, Lean arsenal, website, Red Team cycles, and public mea culpa. Semantic versioning. → Atom feed

v0.8.0 Page Cycles + collaboration ouverte avec B. MacindoeCycles page + open collaboration with B. Macindoe

  • Nouvelle page /cycles/ — « Deux tours, quatre ports » : récit en images des boucles réelles de Collatz (1, −1, −5, −17), du cadeau de Gersonides (1342, De numeris harmonicis) et de l'asymétrie de Benford. Page compagnon du gateway interactif de Benjamin Macindoe (cross-link mutuel).
  • Collaboration à deux clés avec B. Macindoe (preprint Reduced coordinates, v2 + miroir 3-adique) : résultat commun L-A1 (récurrence de transport) certifié Lean 4 kernel-3, référencé sur la page Papers.
  • Lien « Cycles » ajouté à la navigation des 12 pages ; sitemap et flux Atom mis à jour.
  • New page /cycles/ — "Two towers, four harbours": a picture-led account of the real Collatz loops (1, −1, −5, −17), Gersonides' gift (1342, De numeris harmonicis) and Benford's asymmetry. Companion to Benjamin Macindoe's interactive gateway (mutual cross-link).
  • Two-key collaboration with B. Macindoe (preprint Reduced coordinates, v2 + 3-adic mirror): joint result L-A1 (transport recurrence) certified in Lean 4 kernel-3, referenced on the Papers page.
  • "Cycles" link added to all 12 page navs; sitemap and Atom feed updated.

v0.7.4 JAR rejection — repositionnement éditorialJAR rejection — editorial repositioning

  • Notification de rejet — Journal of Automated Reasoning : la soumission du 2026-04-27 (v1.1, 28 pages, kernel-checked Lean 4) a été rejetée le 2026-05-13. Aucune modification des artefacts formels : le théorème conditionnel no_nontrivial_cycle_phase59 et le profil d'axiomes minimal (kernel-3 + 3 hypothèses externes documentées) restent inchangés et reproductibles via reproduce.sh EXIT 0.
  • Site repositionné en mode preprint : le DOI Zenodo permanent 10.5281/zenodo.19790406 reste la référence canonique. Toutes les affirmations actives « submitted to JAR » / « en review » de l'index, /papers/, /pour-tous/, /syracuse/, /histoire/, /research-ledger/, /faq/, OG image, modale Citer, et meta descriptions ont été neutralisées en mention preprint Zenodo neutre. Le badge ★ JAR du tableau des pistes est renommé en ★ Main (status jar → main dans pistes.json, classe CSS .badge.jar → .badge.main).
  • Discipline anti-promotionnelle FIND-015 réaffirmée : aucune nouvelle cible journal n'est annoncée publiquement à ce stade. Les entrées historiques (v0.3.0 soumission, v0.5.0 mise en valeur résultat) sont préservées pour traçabilité — elles décrivent des faits datés vrais et ne sont pas réécrites. Une nouvelle entrée paper-jar-rejected est ajoutée au research-ledger en complément historique (supersedes ↔ superseded_by).
  • Code paths préservés : la branche Git arsenal-postjar, le répertoire Lean ProjetCollatz/PostJAR/, et tous les permaliens GitHub blob/raw restent inchangés. Ces noms désignent des conventions de code (« travail postérieur au dépôt v1.1 ») qui restent factuellement correctes indépendamment du verdict éditorial.
  • Rejection notification — Journal of Automated Reasoning: the 2026-04-27 submission (v1.1, 28 pages, kernel-checked Lean 4) was rejected on 2026-05-13. No modification of formal artefacts: the conditional theorem no_nontrivial_cycle_phase59 and the minimal axiom profile (kernel-3 + 3 documented external hypotheses) remain unchanged and reproducible via reproduce.sh EXIT 0.
  • Site repositioned in preprint mode: the permanent Zenodo DOI 10.5281/zenodo.19790406 remains the canonical reference. All active "submitted to JAR" / "under review" claims across index, /papers/, /pour-tous/, /syracuse/, /histoire/, /research-ledger/, /faq/, OG image, Cite modal, and meta descriptions have been neutralized to a Zenodo-preprint mention. The ★ JAR badge of the approaches table is renamed ★ Main (status jar → main in pistes.json, CSS class .badge.jar → .badge.main).
  • FIND-015 anti-promotional discipline reaffirmed: no new target journal is publicly announced at this stage. Historical entries (v0.3.0 submission, v0.5.0 main result featured) are preserved for traceability — they describe dated factual events and are not rewritten. A new paper-jar-rejected event is added to the research ledger as historical complement (supersedes ↔ superseded_by).
  • Code paths preserved: the Git branch arsenal-postjar, the Lean directory ProjetCollatz/PostJAR/, and all GitHub blob/raw permalinks remain unchanged. These names denote code conventions ("work after the v1.1 deposit") that remain factually correct regardless of editorial verdict.

v0.7.3 δ11 Salikhov-Insufficient-for-3732 (CONDITIONNEL) — architecture 5-IA cross-validationδ11 Salikhov-Insufficient-for-3732 (CONDITIONAL) — 5-AI cross-validation architecture

  • δ11 — Salikhov-Insufficient-for-3732 (Lean 4 / Mathlib v4.27) : nouveau lemme formel sur la sous-branche k ∈ [3694, 3732] de la piste E.1 Salikhov 2007 (μ ≤ 5.125). Théorème delta11_salikhov_insufficient kernel-checked, lake build PASS sur Mac M1 (post-Phase 6-bis polish : 2039 jobs, ~11s, 0 warning ; gain de −82% vs ~67s pré-polish suite refactor imports), 0 sorry, 0 admit. Branche study/E1-salikhov-2007-impossibility (4 commits : 16884f1 + fa4ad47 + 3ca2f34 + 0ec9889), paper JAR (main) intouché, push origin verrouillé tant que GF8 n'est pas levé.
  • Profil épistémique CONDITIONNEL transparent : [propext, Classical.choice, Quot.sound, C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound] — kernel-3 standard + 3 axiomes ad-hoc explicitement déclarés. axiom C_Salikhov : ℝ (existence de la constante effective Salikhov, non-publiée explicitement) + axiom C_Salikhov_pos : 0 < C_Salikhov (convention diophantienne effective implicite Salikhov 2007, explicitée Phase 5e suite catch Gemini ARES shadow ; sans cela, théorème vacuously-true pour C ≤ 0) + axiom c_salikhov_upper_bound : C_Salikhov < (10:ℝ)^(-30:ℤ) (borne supérieure conservatrice cohérente avec la littérature diophantienne effective Baker / Mignotte ; PAS extraite du paper Salikhov 2007). Le théorème δ11 prouve une insuffisance numérique de la borne ad-hoc retenue, pas une propriété directement publiée par Salikhov 2007.
  • Architecture 5-IA cross-validation : Session A (Claude Code Opus 4.7) + Session D (Claude Opus 4.7 CLI mailbox indépendante) + Gemini Pro 3.1 + ChatGPT 5.5 thinking + Claude.ai web Opus 4.7. Anti-corrélation 3 niveaux : sub-agents internal Session D (3 prompts différenciés) + cross-modèle Opus vs ChatGPT/Gemini + cross-Claude pur Opus CLI vs Opus web. Le cross-modèle a payé son prix DEUX FOIS : (1) ChatGPT G3 RT shadow a flagué un DOI Wu & Wang 2014 erroné dans la version initiale du PROVENANCE (mea culpa #31), invisible aux 4 instances Claude ; (2) Gemini G3 ARES shadow Deep Research a flagué axiom C_Salikhov : ℝ non positivement restreint (théorème vacuously-true pour C ≤ 0, mea culpa #32), invisible aux 5 IAs précédentes y compris ChatGPT.
  • Trois protocoles d'audit G3 indépendants 6/6 cross-validation : RED TEAM épistémique 12/12 PASS + 0 réserve, NASA failure modes 14/15 PASS + 0 WARN (N14 multi-Mathlib transformé en décision design assumée Phase 6-bis), ARES adversarial 10/10 PASS + 0 réserve (A2 imports résolu Phase 6-bis, A9 transformé en décision design). Score consolidé post-Phase 6-bis : ~37/37 PASS direct + 0/37 réserve résiduelle + 0/37 KO. Six fichiers d'audit publiés dans collatz-lab-audit/findings/ (3 primary Session D + 3 shadow ChatGPT / Claude.ai web / Gemini Deep Research).
  • Lineage formel des bornes d'irrationalité de log 3 documenté dans le doc-comment Lean (Phase 5a fix Session D) : Rhin 1987 (μ ≤ 8.616) → Wu 2003 (Math. Comp. 72(242), DOI 10.1090/S0025-5718-02-01442-4, online 2002 / print 2003) → Salikhov 2007 (Doklady Math. 76(3), DOI 10.1134/S1064562407060361) → Wu & Wang 2014 (J. Number Theory 142, DOI 10.1016/j.jnt.2014.03.007, raffinement μ ≤ 5.1163051). Tous les DOIs vérifiés indépendamment via CrossRef API 2026-05-08.
  • Quatre mea culpa publics : #29 /papers/ présentait Salikhov 2007 et Wu 2003 comme équivalents pour k ≤ 3732 alors que Wu 2003 est strictement plus fort sur cette sous-branche (k_max=3732 vs Salikhov k_max=3693) ; #30 Wu & Wang 2014 (μ ≤ 5.116) absent du registre pistes.json initial alors que c'est le raffinement le plus récent ; #31 DOI Wu & Wang 2014 initialement erroné (.004 = Anglès-Pellarin) dans PROVENANCE_DELTA11.md, corrigé .007 après audit cross-modèle ChatGPT (CrossRef API confirmation indépendante) ; #32 axiom C_Salikhov : ℝ initialement non positivement restreint dans Delta11Salikhov.lean, théorème vacuously-true pour C ≤ 0 (catch Gemini Pro 3.1 ARES shadow Deep Research), corrigé Phase 5e par ajout de axiom C_Salikhov_pos : 0 < C_Salikhov (convention diophantienne explicitée).
  • Méthode Lean (Phase 64 algébrique vs numérique) : décomposition en deux lemmes reduction_step1a (algébrique, isolation de la signature pure) + reduction_step1b (numérique, calc-chain via puissance entière 10000-binding pour éviter norm_num sur rpow rationnel). Direction monotonie confirmée upper-bound sur k (binding k ≤ 10000 purement instrumental ; conclusion mathématique sur intervalle strict [3694, 3732]). Erreur initiale chunk 2 (binding lower) catchée par ChatGPT cross-modèle, corrigée Session D.
  • Phase 6-bis polish (commit 0ec9889) — 3 actions atomiques pour score G3 nominal pur ~37/37 + 0 réserve : (1) A2 résolu : refactor import Mathlib global → 7 imports spécifiques (Pow.Real + Positivity + NormNum + Ring + Linarith + GCongr + Phase60IrrationalityLog23), build passé de 7886 jobs / ~67s à 2039 jobs / ~11s (−82%) ; (2) RT2 résolu : doc-comment explicite « range mécanique = range narratif, aucune extrapolation cachée » au-dessus du théorème principal ; (3) N14 + A9 transformés en décisions design assumées : pin Mathlib v4.27 (dernière version stable) explicite, rétro-compat v4.26 non garantie par design (décision Eric chat 2026-05-08T11:40 « on restera sur Mathlib dernière version »).
  • Disclosure : ce théorème est CONDITIONNEL sous trois axiomes ad-hoc transparents et validé strictement sur Mathlib v4.27 (rétro-compat v4.26 non couverte par design). C'est une maquette formelle conditionnelle, pas une extraction certifiée du paper original Salikhov 2007. La piste E.1 reste donc partiellement fermée, pas démontrée inconditionnellement. Voir le disclaimer GF7 complet dans le header du fichier Delta11Salikhov.lean.
  • δ11 — Salikhov-Insufficient-for-3732 (Lean 4 / Mathlib v4.27): new formal lemma on sub-branch k ∈ [3694, 3732] of approach E.1 Salikhov 2007 (μ ≤ 5.125). Theorem delta11_salikhov_insufficient kernel-checked, lake build PASS on Mac M1 (post-Phase 6-bis polish: 2039 jobs, ~11s, 0 warning; −82% gain vs ~67s pre-polish following imports refactor), 0 sorry, 0 admit. Branch study/E1-salikhov-2007-impossibility (4 commits: 16884f1 + fa4ad47 + 3ca2f34 + 0ec9889), JAR paper (main) untouched, push origin locked until GF8 is lifted.
  • CONDITIONAL transparent epistemic profile: [propext, Classical.choice, Quot.sound, C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound] — standard kernel-3 + 3 explicitly declared ad-hoc axioms. axiom C_Salikhov : ℝ (existence of Salikhov's effective constant, not explicitly published) + axiom C_Salikhov_pos : 0 < C_Salikhov (effective Diophantine convention implicit in Salikhov 2007, made explicit in Phase 5e following Gemini ARES shadow catch ; without it, theorem vacuously-true for C ≤ 0) + axiom c_salikhov_upper_bound : C_Salikhov < (10:ℝ)^(-30:ℤ) (conservative upper bound consistent with effective Diophantine literature Baker / Mignotte; NOT extracted from Salikhov 2007 paper). The δ11 theorem proves a numerical insufficiency of the chosen ad-hoc bound, not a property directly published by Salikhov 2007.
  • 5-AI cross-validation architecture: Session A (Claude Code Opus 4.7) + Session D (Claude Opus 4.7 CLI independent mailbox) + Gemini Pro 3.1 + ChatGPT 5.5 thinking + Claude.ai web Opus 4.7. 3-tier anti-correlation: Session D internal sub-agents (3 differentiated prompts) + cross-model Opus vs ChatGPT/Gemini + pure cross-Claude Opus CLI vs Opus web. Cross-model paid its price TWICE: (1) ChatGPT G3 RT shadow flagged a wrong Wu & Wang 2014 DOI in the initial PROVENANCE (mea culpa #31), invisible to all 4 Claude instances; (2) Gemini G3 ARES shadow Deep Research flagged axiom C_Salikhov : ℝ non positively restricted (theorem vacuously-true for C ≤ 0, mea culpa #32), invisible to all 5 previous AIs including ChatGPT.
  • Three independent G3 audit protocols 6/6 cross-validation: epistemic RED TEAM 12/12 PASS + 0 reservation, NASA failure modes 14/15 PASS + 0 WARN (N14 multi-Mathlib transformed into design choice in Phase 6-bis), ARES adversarial 10/10 PASS + 0 reservation (A2 imports resolved in Phase 6-bis, A9 transformed into design choice). Consolidated score post-Phase 6-bis: ~37/37 direct PASS + 0/37 residual reservation + 0/37 KO. Six audit files published in collatz-lab-audit/findings/ (3 primary Session D + 3 shadow ChatGPT / Claude.ai web / Gemini Deep Research).
  • Formal lineage of log 3 irrationality bounds documented in Lean doc-comment (Phase 5a Session D fix): Rhin 1987 (μ ≤ 8.616) → Wu 2003 (Math. Comp. 72(242), DOI 10.1090/S0025-5718-02-01442-4, online 2002 / print 2003) → Salikhov 2007 (Doklady Math. 76(3), DOI 10.1134/S1064562407060361) → Wu & Wang 2014 (J. Number Theory 142, DOI 10.1016/j.jnt.2014.03.007, refinement μ ≤ 5.1163051). All DOIs independently verified via CrossRef API 2026-05-08.
  • Four public mea culpa: #29 /papers/ presented Salikhov 2007 and Wu 2003 as equivalent for k ≤ 3732 while Wu 2003 is strictly stronger on this sub-branch (k_max=3732 vs Salikhov k_max=3693); #30 Wu & Wang 2014 (μ ≤ 5.116) missing from the initial pistes.json registry whereas it is the most recent refinement; #31 Wu & Wang 2014 DOI initially wrong (.004 = Anglès-Pellarin) in PROVENANCE_DELTA11.md, corrected to .007 after cross-model ChatGPT audit (CrossRef API independent confirmation); #32 axiom C_Salikhov : ℝ initially not positively restricted in Delta11Salikhov.lean, theorem vacuously-true for C ≤ 0 (caught by Gemini Pro 3.1 ARES shadow Deep Research), fixed in Phase 5e by adding axiom C_Salikhov_pos : 0 < C_Salikhov (Diophantine convention made explicit).
  • Lean methodology (Phase 64 algebraic vs numerical): decomposition into two lemmas reduction_step1a (algebraic, isolation of pure signature) + reduction_step1b (numerical, calc-chain via integer power 10000-binding to avoid norm_num on rational rpow). Monotonicity direction confirmed upper-bound on k (k ≤ 10000 binding purely instrumental ; mathematical conclusion stays on strict interval [3694, 3732]). Initial chunk 2 error (lower-bound binding) caught by ChatGPT cross-model, fixed by Session D.
  • Phase 6-bis polish (commit 0ec9889) — 3 atomic actions for nominal pure G3 score ~37/37 + 0 reservation: (1) A2 resolved: refactor import Mathlib global → 7 specific imports (Pow.Real + Positivity + NormNum + Ring + Linarith + GCongr + Phase60IrrationalityLog23), build went from 7886 jobs / ~67s to 2039 jobs / ~11s (−82%); (2) RT2 resolved: explicit doc-comment "mechanical range = narrative range, no hidden extrapolation" above the main theorem; (3) N14 + A9 transformed into assumed design choices: explicit Mathlib v4.27 pin (latest stable version), v4.26 retro-compatibility not guaranteed by design (Eric chat decision 2026-05-08T11:40 "we'll stay on the latest Mathlib version").
  • Disclosure: this theorem is CONDITIONAL under three transparent ad-hoc axioms and validated strictly on Mathlib v4.27 (v4.26 retro-compatibility not covered by design). It is a conditional formal mock-up, not a certified extraction from the original Salikhov 2007 paper. Approach E.1 thus remains partially closed, not unconditionally proven. See full GF7 disclaimer in the header of Delta11Salikhov.lean.

v0.7.0 CGS-7 finalisé — audit indépendant 4 IA + lake build PASSCGS-7 finalized — independent 4-AI audit + lake build PASS

  • CGS-7 — sum_s_ge_length_plus_num_nonincrease : théorème Lean 4 / Mathlib v4.27 démontré formellement. lake build TestsMath PASS (7888 jobs, 31s sur Mac M1), 0 sorry, profil axiomes [propext, Classical.choice, Quot.sound] (kernel-3 standard). Branche study/cgs-7-instantiation dérivée d'arsenal-postjar, paper JAR (main) intouché.
  • Énoncé final (reformulation 4 IA convergente) : pour cycle Collatz hypothétique avec x_t > 1, s_t ≥ 1, x_{t+1} = (3·x_t+1)/2^{s_t}, soit N = #{t < k | x_{t+1} ≤ x_t}. Alors S = ∑_{tcgs7_algebraic_pure (algébrique pur) + cgs7_dynamic_transfer (transfert dynamique via drop_forces_s_ge_two).
  • Audit indépendant 4 IA convergent : Session A (Claude Opus 4.7) + Session B (Claude Opus 4.7 indépendante) + Gemini Pro 3.1 + ChatGPT (thinking étendu/Instant). Convergence 4/4 sur faille esquisse NEW3 originale (polarité inversée drop_forces_s_ge_two + ambiguïté sémantique D = #{s_t≥2} algébrique vs descentes dynamiques) → reformulation collective + démonstration validée.
  • Test négatif Red Team exécutable : #check_failure dans section RedTeamNegativeTest bloque au build toute tentative de polarité inversée. Garde-fou anti-régression actif (Lean affiche "info: Application type mismatch" sur la version inversée).
  • Audits 3 protocoles : RED TEAM 12/12 PASS, NASA 14/15 PASS + 1 note v4.28, ARES 8/10 PASS direct + 2 notes optimisation. Vérification anti-hallucination cross-vérifiée ligne à ligne (CGS7Dependencies = ChatGPTLemmas_test strict modulo patches Mathlib v4.27 documentés).
  • Pivot Option C-bis : démonstration via instanciation locale (décomposition 1 + indicatrice sur Finset) plutôt que via le lemme abstrait abstract_decomposition_totalVal_ge_totalLen_plus_blocks (l. 234) — choix validé 4/4 IA pour minimiser la surface de dépendance.
  • Disclosure : ce théorème est CONDITIONNEL — il vaut sous l'hypothèse qu'un cycle Collatz non trivial existe. C'est un lemme de la chaîne no_nontrivial_cycle_phase59 du paper JAR, pas un résultat autonome.
  • CGS-7 — sum_s_ge_length_plus_num_nonincrease: Lean 4 / Mathlib v4.27 theorem formally proved. lake build TestsMath PASS (7888 jobs, 31s on Mac M1), 0 sorry, axiom profile [propext, Classical.choice, Quot.sound] (kernel-3 standard). Branch study/cgs-7-instantiation derived from arsenal-postjar, JAR paper (main) untouched.
  • Final statement (4-AI convergent reformulation): for hypothetical Collatz cycle with x_t > 1, s_t ≥ 1, x_{t+1} = (3·x_t+1)/2^{s_t}, let N = #{t < k | x_{t+1} ≤ x_t}. Then S = ∑_{tcgs7_algebraic_pure (pure algebraic) + cgs7_dynamic_transfer (dynamic transfer via drop_forces_s_ge_two).
  • Independent 4-AI audit: Session A (Claude Opus 4.7) + Session B (Claude Opus 4.7 independent) + Gemini Pro 3.1 + ChatGPT (extended thinking/Instant). 4/4 convergence on original NEW3 sketch flaw (inverted polarity in drop_forces_s_ge_two + semantic ambiguity D = #{s_t≥2} algebraic vs dynamic descents) → collective reformulation + validated proof.
  • Executable negative Red Team test: #check_failure in RedTeamNegativeTest section blocks at build any attempt at inverted polarity. Active anti-regression safeguard (Lean displays "info: Application type mismatch" on inverted version).
  • 3-protocol audits: RED TEAM 12/12 PASS, NASA 14/15 PASS + 1 v4.28 note, ARES 8/10 direct PASS + 2 optimization notes. Anti-hallucination cross-verified line-by-line (CGS7Dependencies = ChatGPTLemmas_test strict modulo documented Mathlib v4.27 patches).
  • Option C-bis pivot: proof via local instantiation (1 + indicator Finset decomposition) rather than via the abstract lemma abstract_decomposition_totalVal_ge_totalLen_plus_blocks (l. 234) — choice validated 4/4 to minimize dependency surface.
  • Disclosure: this theorem is CONDITIONAL — it holds under the hypothesis that a non-trivial Collatz cycle exists. It is a lemma in the no_nontrivial_cycle_phase59 chain of the JAR paper, not a standalone result.

v0.6.0 δ10 cartographique + Research Ledger + trilogie d'impossibilitéδ10 cartographic + Research Ledger + impossibility trilogy

  • FIND-016 audit clos : BakerSeparation k^6 plus strict que littérature publiée → doc-comment Lean transparency note ajoutée. Mea culpa #28 publié. Three-Key validated. Branche audit/find-016-transparency-doc-comment, tag audit-find016-2026-04-30.
  • δ10 — Barina-Replacement Impossibility Lemma (Phase 64) : nouveau théorème Lean 4, 296 lignes, kernel-checked, 0 sorry, axiom profile [propext] only (kernel-1 minimal). Catalogue audit fini : aucune borne diophantienne publiée (Salikhov 2007 / Wu 2003 / Rhin 1987 / Simons-de Weger 2005) ne peut remplacer BarinaVerification. Branche study/delta10-barina-replacement-impossibility, tag study-delta10-2026-04-30.
  • Trilogie d'impossibilité Baker+CF+Khinchin complète : δ8 (Phase58 §5) + δ8' (Phase58 §5.2) + δ10 (Phase64). Chaque hypothèse externe du paper JAR est maintenant adossée à une preuve d'impossibilité formelle. Profil épistémique strictement décroissant : kernel-3 → kernel-3 → kernel-1.
  • Research Ledger public à /research-ledger/ : 6 sections (status snapshot / milestones / audits & corrections / ongoing studies / full ledger / external references), filtrable, FR/EN bilingue, schema enrichi (claim_scope + verification_method + evidence_level + epistemic_status + last_verified_at). Tag site-research-ledger-2026-04-30.
  • Cross-links site : section accueil "§ VI État des travaux" (5 cartes), Mermaid diagram étendu avec trilogie, JSON-LD abstract mentionne δ10 + trilogie, mea culpa #28 lien vers δ10, /papers/ carte δ10 "★ Validé Lean 4 kernel-checked".
  • Méthodologie tri-IA : 7 Three-Key validations ChatGPT 5.5 thinking extended (Q5/Q9/Q11/Q12/Q13/Q14/Q15) via Chrome MCP, 2 cycles Two-Key OLD3↔NEW4 (FIND-016 4 phases + δ10 7 phases L1-L7), branche main INTACTE 7h+ (red line préservée). Validation multi-IA interne anti-hallucination, non peer review (cf. FAQ Q11).
  • Disclosure anti-promotionnelle (Q15) : cette release documente la traçabilité ; les revendications scientifiques restent limitées au paper et aux artefacts Lean formels.
  • FIND-016 audit closed: BakerSeparation k^6 stronger than published bounds → Lean transparency note added to doc-comment. Public mea culpa #28. Three-Key validated. Branch audit/find-016-transparency-doc-comment, tag audit-find016-2026-04-30.
  • δ10 — Barina-Replacement Impossibility Lemma (Phase 64): new Lean 4 theorem, 296 lines, kernel-checked, 0 sorry, axiom profile [propext] only (kernel-1 minimal). Cartographic finite catalogue: no published Diophantine bound (Salikhov 2007 / Wu 2003 / Rhin 1987 / Simons-de Weger 2005) can replace BarinaVerification. Branch study/delta10-barina-replacement-impossibility, tag study-delta10-2026-04-30.
  • Baker+CF+Khinchin impossibility trilogy complete: δ8 (Phase58 §5) + δ8' (Phase58 §5.2) + δ10 (Phase64). Each external hypothesis of the JAR paper is now backed by a formal impossibility lemma. Strictly decreasing epistemic profile: kernel-3 → kernel-3 → kernel-1.
  • Research Ledger public at /research-ledger/: 6 sections (status snapshot / milestones / audits & corrections / ongoing studies / full ledger / external references), filterable, FR/EN bilingual, enriched schema (claim_scope + verification_method + evidence_level + epistemic_status + last_verified_at). Tag site-research-ledger-2026-04-30.
  • Site cross-links: home page enriched with "§ VI Research status" snapshot (5 cards), Mermaid diagram extended with trilogy, JSON-LD abstract mentions δ10 + trilogy, mea culpa #28 links to δ10, /papers/ has δ10 "★ Validated Lean 4 kernel-checked" card.
  • Tri-AI methodology: 7 Three-Key ChatGPT 5.5 thinking extended validations (Q5/Q9/Q11/Q12/Q13/Q14/Q15) via Chrome MCP, 2 cycles Two-Key OLD3↔NEW4 cross-check (FIND-016 4 phases + δ10 7 phases L1-L7), branch main INTACTE 7h+ (red line preserved). Internal multi-AI anti-hallucination validation, not peer review (see FAQ Q11).
  • Anti-promotional disclosure (Q15): this release documents traceability; scientific claims remain limited to the paper and formal Lean artefacts.

v0.5.1 Site web haut de gammeHigh-end website

  • Localisation EN-canonique : anglais par défaut (sauf navigator fr-*), bouton FR/EN sur 4 pages
  • Graphe de dépendances D3 force-directed interactif sur /lemmes/
  • Palette de recherche universelle (⌘K / Ctrl+K / /) sur pistes, théorèmes, lemmes, cf_gaps
  • Widget de citation 5 formats (BibTeX, APA 7, Chicago 17, RIS, plain) avec copy-to-clipboard
  • Mode clair/sombre avec prefers-color-scheme + toggle persisté localStorage
  • Scroll progress bar dorée en haut de chaque page
  • SEO complet : sitemap.xml, robots.txt, JSON-LD ScholarlyArticle, hreflang, Open Graph 1200×630, Twitter Cards, favicons SVG/PNG
  • Atom feed pour les updates : /feed.xml
  • Page changelog (cette page)
  • EN-canonical localization: English by default (except navigator fr-*), FR/EN button on all 4 pages
  • Interactive D3 force-directed dependency graph on /lemmes/
  • Universal search palette (⌘K / Ctrl+K / /) across approaches, theorems, lemmas, cf_gaps
  • 5-format citation widget (BibTeX, APA 7, Chicago 17, RIS, plain) with copy-to-clipboard
  • Light/dark theme toggle with prefers-color-scheme auto-detect, persisted in localStorage
  • Golden scroll progress bar at the top of every page
  • Complete SEO: sitemap.xml, robots.txt, JSON-LD ScholarlyArticle, hreflang, Open Graph 1200×630, Twitter Cards, favicons
  • Atom feed for updates: /feed.xml
  • Changelog page (this page)

v0.5.0 Mise en valeur résultat principal JARJAR main result featured

  • Encart "Résultat principal" sur la page d'accueil avec PDF, DOI, lien Lean
  • Ligne ★ JAR épinglée en tête du tableau des pistes (toujours visible)
  • Diagramme Mermaid Λ enrichi avec le nœud central JAR + 3 conditions externes
  • Tableau profil d'axiomes sur /papers/ (3 kernel + 3 externes)
  • Routing ghURL() : main vs arsenal-postjar pour fichiers Lean
  • 15/15 URLs dynamiques HTTP 200 OK
  • "Main result" highlight box on homepage with PDF, DOI, Lean link
  • ★ JAR pinned row at the top of the approaches table (always visible)
  • Λ Mermaid diagram enriched with central JAR node + 3 external conditions
  • Axiom profile table on /papers/ (3 kernel + 3 external)
  • ghURL() routing: main vs arsenal-postjar for Lean files
  • 15/15 dynamic URLs HTTP 200 OK

v0.4.0 Cycles 4 et 5 - patches Mathlib v4.27 + Knight 2026Cycles 4 and 5 - Mathlib v4.27 patches + Knight 2026

  • Cycle 4 (CGS-7) : 6 lemmes ChatGPT diagnostiqués et patchés pour Mathlib v4.27
  • Cycle 5 (Knight 2026) : Section 5 inconditionnelle (preuve 2-adique 5 lignes), Section 3 Baker-dépendant
  • Mea culpa #24 (Salikhov 2007 ≠ 2008) + #25 (Bost-Charles 2022 inventé) documentés
  • Filtre 4-test consolidé (R72 / Steiner-Eliahou / Lagarias / anti-Λ)
  • Cycle 4 (CGS-7): 6 ChatGPT lemmas diagnosed and patched for Mathlib v4.27
  • Cycle 5 (Knight 2026): Section 5 unconditional (5-line 2-adic proof), Section 3 Baker-dependent
  • Mea culpa #24 (Salikhov 2007 not 2008) + #25 (Bost-Charles 2022 fabricated) documented
  • 4-test filter consolidated (R72 / Steiner-Eliahou / Lagarias / anti-Λ)

v0.3.0 Soumission JAR Springer v1.1JAR Springer submission v1.1

  • Paper de 28 pages soumis au Journal of Automated Reasoning
  • Théorème no_nontrivial_cycle_phase59 kernel-checked Lean 4 + Mathlib v4.27
  • Profil minimal : 3 axiomes kernel + 3 hypothèses externes documentées
  • DOI Zenodo 10.5281/zenodo.19790406
  • reproduce.sh EXIT 0 sur clone propre, runtime ~3-5 min Mac M1 Pro
  • 28-page paper submitted to Journal of Automated Reasoning
  • Theorem no_nontrivial_cycle_phase59 kernel-checked in Lean 4 + Mathlib v4.27
  • Minimal profile: 3 kernel axioms + 3 documented external hypotheses
  • Zenodo DOI 10.5281/zenodo.19790406
  • reproduce.sh EXIT 0 on clean clone, runtime ~3-5 min on Mac M1 Pro

v0.2.0 Arsenal R34-R96 PostJARPostJAR R34-R96 arsenal

  • 72 théorèmes auxiliaires développés post-JAR
  • 5 clusters : Steiner foundations, corrSum divisibility, modular universal, lacunary periodization, block decomposition
  • Branche dédiée arsenal-postjar sur GitHub
  • 72 auxiliary theorems developed post-JAR
  • 5 clusters: Steiner foundations, corrSum divisibility, modular universal, lacunary periodization, block decomposition
  • Dedicated branch arsenal-postjar on GitHub

Discussion sur les versions

Version discussion

Annonces et discussions de releases sur GitHub.

Release announcements and discussions on GitHub.

→ Voir les annonces sur GitHub → View announcements on GitHub