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

Changelog

Changelog

Historique des principales évolutions du projet : paper, arsenal Lean, site web et mea culpa publics. Versioning sémantique. Les entrées anciennes sont conservées telles quelles ; la v0.9.0 corrige plusieurs de leurs affirmations. → Atom feed

History of the main project changes: paper, Lean arsenal, website and public mea culpa. Semantic versioning. Older entries are kept as they were; v0.9.0 corrects several of their claims. → Atom feed

v0.10.20 Les résultats en tête : accueil, archives du printemps 2026, menu et page PapersResults first: home page, spring 2026 archive, menu and Papers page

  • Bannière de l'accueil : plus compacte (titre plus petit, moins de vide) et sur toute la largeur de l'écran (elle s'arrêtait à 1100 px) ; son texte ne change pas. Le premier écran montre le dernier jalon, l'avertissement « Ce site ne prouve pas la conjecture de Collatz. » et le lien vers l'erratum, au bureau (1440×900), sur un portable (1366×657) et sur un téléphone (390×664).
  • Temps de lecture : il n'est plus dans la bannière mais à la fin de l'en-tête de la page ; ses libellés et ses nombres suivent la langue affichée (« 4 930 mots », « 4,930 words »), et il compte le texte de la langue affichée au chargement de la page (blocs repliés compris).
  • Chapeau de l'accueil : il décrit l'état actuel (formalisations en Lean 4 de trois travaux classiques, note d'errata, catalogue de trente-six pistes, preprint d'avril 2026 avec son erratum).
  • Nouvelle section « Résultats », juste sous l'en-tête : quatre cartes (Steiner 1978 sans hypothèse, Lagarias 1990, Halbeisen–Hungerbühler 1997, note d'errata), chacune avec une phrase reprise des pages du site et un lien « Pour auditer » vers le README du dossier (release v1.5) ou vers le DOI ; rappel que rien de nouveau n'est revendiqué sur les cycles et que ce site ne prouve pas la conjecture.
  • Nouvelle section « Archives du printemps 2026 » (§ II) : le verrou Λ et son diagramme, les hypothèses A, A′, B et C et les tests REQ-MATH y sont déplacés tels quels, chacun dans un bloc repliable daté d'avril 2026 ; les mea culpa y sont déplacés tels quels, non repliés. Un lien vers une ancre de ces blocs, ou une entrée du sommaire latéral, les ouvre ; le diagramme et le graphique sont redessinés à l'ouverture. Liens vers les pages de la même époque (lemmes, preuve, explorateur Λ).
  • Numérotation de l'accueil : § I catalogue, § II archives (§ III à § V à l'intérieur, inchangés), § VI communauté, § VII équipe (le § II manquait).
  • Menu (toutes les pages) : neuf entrées, Accueil, Résultats, Papers, Preprint, Pistes, Registre, Pour tous, Cycles, Archives 2026 ; les pages Lemmes, Preuve et Λ restent en ligne, liées depuis les archives.
  • Accueil, encadré du preprint : « Ce que le projet apporte » devient « Ce que le projet apportait en avril 2026 ».
  • Page Papers : titre « Formalisations publiées, preprint d'avril 2026 et travaux en cours » ; nouveau § I « Formalisations publiées », où les cartes Steiner 1978, Lagarias 1990 et Halbeisen–Hungerbühler 1997 sont déplacées telles quelles, chacune avec une ligne « Pour auditer » ; la carte Lagarias 1990 cite, en anglais, la liste de ce que vérifie le noyau selon le README du dossier ; le preprint devient le § II, les travaux en cours le § III, dont l'introduction renvoie à la note d'errata des cartes du § I ; chapeau complété ; titre de page, Open Graph et Twitter « Papers ».
  • Carte « Dernier audit » de l'accueil : relecture adverse des changements de cette version ; l'audit précédent (v0.10.19) est rappelé.
  • Palette de recherche : les résumés de l'accueil et de Papers suivent la nouvelle présentation.
  • Cache des navigateurs : paramètre de version de main.js mis à jour sur toutes les pages.
  • Les entrées ci-dessous restent telles quelles.
  • Home page banner: more compact (smaller title, less empty space) and across the full width of the screen (it stopped at 1100 px); its text does not change. The first screen shows the latest milestone, the warning "This site does not prove the Collatz conjecture." and the link to the erratum, on a desktop (1440×900), a laptop (1366×657) and a phone (390×664).
  • Reading time: no longer in the banner but at the end of the page header; its labels and numbers follow the displayed language ("4 930 mots", "4,930 words"), and it counts the text in the language displayed when the page loads (collapsed blocks included).
  • Home page lede: it describes the current state (Lean 4 formalisations of three classical works, errata note, catalogue of thirty-six leads, April 2026 preprint with its erratum).
  • New "Results" section, just below the header: four cards (Steiner 1978 without hypothesis, Lagarias 1990, Halbeisen–Hungerbühler 1997, errata note), each with one sentence taken from the site's pages and a "To audit" link to the folder's README (release v1.5) or to the DOI; a reminder that nothing new is claimed about cycles and that this site does not prove the conjecture.
  • New "Spring 2026 archive" section (§ II): the Λ lock and its diagram, hypotheses A, A′, B and C and the REQ-MATH tests are moved there as they were, each in a collapsible block dated April 2026; the mea culpa are moved there as they were, not collapsed. A link to an anchor in these blocks, or an entry of the side table of contents, opens them; the diagram and the chart are redrawn when opened. Links to the pages of the same period (lemmas, proof, Λ explorer).
  • Home page numbering: § I catalogue, § II archive (§ III to § V inside, unchanged), § VI community, § VII team (§ II was missing).
  • Menu (all pages): nine entries, Home, Results, Papers, Preprint, Approaches, Ledger, For everyone, Cycles, 2026 archive; the Lemmas, Proof and Λ pages stay online, linked from the archive.
  • Home page, preprint box: "What the project contributes" becomes "What the project contributed in April 2026".
  • Papers page: title "Published formalisations, the April 2026 preprint and work in progress"; new § I "Published formalisations", where the Steiner 1978, Lagarias 1990 and Halbeisen–Hungerbühler 1997 cards are moved as they were, each with a "To audit" line; the Lagarias 1990 card quotes the list of what the kernel checks according to the folder's README; the preprint becomes § II, work in progress § III, whose introduction points to the errata note of the § I cards; lede completed; page, Open Graph and Twitter title "Papers".
  • "Latest audit" card of the home page: adversarial review of the changes of this version; the previous audit (v0.10.19) is recalled.
  • Search palette: the summaries of the home page and of Papers follow the new presentation.
  • Browser cache: version parameter of main.js updated on every page.
  • The entries below are kept as they were.

v0.10.19 Fond et erratum : corrections de l'audit du 28 octobre 2026Substance and erratum: corrections from the audit of 28 October 2026

  • Page « Pour tous » : l'erratum y est dit en entier. La 3e hypothèse, avec la 2e, ne contient pas seulement la réponse « pour les très grandes boucles » : à elles deux, elles excluent toute autre boucle, petite ou grande (dans le fichier Lean, une boucle parcourue plusieurs fois compte comme une boucle plus longue) ; le théorème tourne en rond (quatre passages corrigés ; l'erratum y est dit « précisé le 20 octobre » ; pied de page daté).
  • Page « Cycles » : la vérification exhaustive est bornée (boucles d'au plus 10 termes impairs, registre commun, entrée L-A3) ; « quatre boucles connues » au lieu de « réellement quatre boucles » (aussi dans le titre de la figure 2, les méta-descriptions et les données structurées) ; la « conspiration » des chiffres en base 2 et 3 est dite lecture heuristique ; les faits chiffrés ont été vérifiés des deux côtés par du code Python (et non par un noyau Lean d'un côté) ; le théorème conditionnel d'avril y est présenté avec son erratum, sans revendication d'apport ; pied de page daté.
  • Méta-descriptions, Open Graph, Twitter et données structurées (accueil, Papers) : H1 est dite hypothèse de travail, pas un théorème publié (BakerSeparation) et H2 la vérification de Bařina ; la revérification de no_cycle_k_le_1322 sous Lean 4.34.0 est mentionnée.
  • Chapeau de l'accueil : « organisées autour d'une obstruction diophantienne unique » devient « l'approche principale bute sur une obstruction diophantienne ».
  • Diagramme des paradigmes et décompte des « 14 paradigmes » : sont en pointillé, cadre et flèche, comme « Schémas + Faltings » (piste K, retirée), les pistes pour lesquelles le catalogue, tranché du 22 au 27/10/2026, n'a trouvé aucune source publiée (C pour sa partie Fourier, I.1, J, R pour ses autocorrélations, et W), sans mot nouveau dans le diagramme ; la légende dit « diagramme d'avril 2026, conservé pour mémoire », que toutes ses flèches vers le verrou Λ sont des hypothèses de travail d'avril 2026 et non des résultats, et renvoie aux fiches du catalogue, en particulier celles de F et de Z, qui ne confirment pas non plus le retour au verrou ; le paragraphe du verrou et la note de la carte C ne disent plus que le décompte est « en revue ».
  • Carte « Dernier audit » de l'accueil : elle porte sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (v0.10.18) est rappelé.
  • Données structurées du registre (40 événements) et du changelog (dernière version).
  • Titre de l'accueil : « cycles non triviaux hypothétiques » (et non « conjecturés ») et « avec des formalisations en Lean 4 ».
  • Lien vers le PDF d'avril : son libellé dit qu'il s'agit du preprint d'avril 2026, sans l'erratum.
  • FAQ : versions de Lean et de Mathlib (4.27.0 pour le preprint d'avril, 4.34.0 pour les formalisations d'octobre et la revérification de no_cycle_k_le_1322) ; pied de page daté.
  • Papers : le PDF et le README énoncent la variante no_nontrivial_cycle_final (3e hypothèse ProductBoundThreshold), le site suit no_nontrivial_cycle_phase59 ; les deux sont circulaires ; « 0 sorry dans les preuves » pour Lagarias 1990 et Halbeisen–Hungerbühler 1997, comme pour Steiner 1978 ; titre exact du preprint (aussi dans les méta-descriptions de Papers, les données structurées et la carte « Statut paper » de l'accueil).
  • Lemme R92 (accueil et catalogue des lemmes) : la preuve se termine par decide, vérifié par le noyau, et non native_decide ; l'extrait de l'accueil reprend la ligne simp only qui manquait.
  • Registre de recherche : un événement daté reconnaît que des événements antérieurs ont été réécrits sans date le 02/10/2026 et le 20/10/2026 (textes d'origine dans l'historique git, commits fde2ffb et d94cde6) et précise l'erratum ; ces événements ne sont pas réécrits à nouveau. Un second événement daté consigne la release v1.5 du dépôt Lean (documentation et licence, DOI 10.5281/zenodo.23728612) et les liens ccchallenge n° 14, 15 et 16, qui pointent désormais vers elle ; la section « Liens publics » cite la v1.5.
  • MAINTAINERS.md : section « Continuité » à jour (version v4 du dépôt Zenodo avec son erratum ; dépôt des formalisations d'articles classiques).
  • Barre du haut : de 769 à 1919 px de large, le menu passe sur une deuxième ligne au lieu de pousser hors de l'écran les boutons « Citer », thème, langue et impression.
  • Cache des navigateurs : paramètres de version de main.js, main.css, research-ledger.js, research-ledger.json et lemmes.json mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • "For everyone" page: the erratum is stated in full. Together with the 2nd, the 3rd hypothesis does not only contain the answer "for very large loops": together they exclude every other loop, small or large (in the Lean file, a loop gone round several times counts as a longer loop); the theorem is circular (four passages corrected; the erratum is said to be "made precise on 20 October" there; dated footer).
  • "Cycles" page: the exhaustive check is bounded (loops with at most 10 odd terms, shared ledger, entry L-A3); "four known loops" instead of "really does have four loops" (also in the title of figure 2, the meta descriptions and the structured data); the "conspiracy" of base-2 and base-3 digits is called a heuristic reading; the numerical facts were checked on both sides by Python code (not by a Lean kernel on one side); the April conditional theorem is presented with its erratum, with no claim of contribution; dated footer.
  • Meta descriptions, Open Graph, Twitter and structured data (home page, Papers): H1 is called a working hypothesis, not a published theorem (BakerSeparation), and H2 Barina's verification; the re-check of no_cycle_k_le_1322 on Lean 4.34.0 is mentioned.
  • Home page lede: "organized around a single diophantine obstruction" becomes "the main approach runs into a Diophantine obstruction".
  • Paradigm diagram and count of "14 paradigms": dashed, frame and arrow, like "Schemes + Faltings" (lead K, withdrawn), are the leads for which the catalogue, settled from 22 to 27 October 2026, found no published source (C for its Fourier part, I.1, J, R for its autocorrelations, and W), with no new word in the diagram; the caption says "April 2026 diagram, kept for the record", that all its arrows to the Λ lock are working hypotheses of April 2026, not results, and points to the entries of the catalogue, in particular those of F and Z, which do not confirm the return to the lock either; the paragraph on the lock and the note of card C no longer say that the count is "being reviewed".
  • "Latest audit" card of the home page: it refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (v0.10.18) is recalled.
  • Structured data of the ledger (40 events) and of the changelog (latest version).
  • Home page title: "hypothetical non-trivial cycles" (not "conjectural") and "with formalisations in Lean 4".
  • Link to the April PDF: its label says it is the April 2026 preprint, without the erratum.
  • FAQ: Lean and Mathlib versions (4.27.0 for the April preprint, 4.34.0 for the October formalisations and the re-check of no_cycle_k_le_1322); dated footer.
  • Papers: the PDF and the README state the variant no_nontrivial_cycle_final (3rd hypothesis ProductBoundThreshold), the site follows no_nontrivial_cycle_phase59; both are circular; "0 sorry in the proofs" for Lagarias 1990 and Halbeisen–Hungerbühler 1997, as for Steiner 1978; exact title of the preprint (also in the meta descriptions of Papers, the structured data and the "Paper status" card of the home page).
  • Lemma R92 (home page and lemma catalogue): the proof ends with decide, checked by the kernel, not native_decide; the home-page excerpt restores the missing simp only line.
  • Research ledger: a dated event acknowledges that earlier events were rewritten without a date on 2026-10-02 and 2026-10-20 (original texts in the git history, commits fde2ffb and d94cde6) and clarifies the erratum; those events are not rewritten again. A second dated event records release v1.5 of the Lean repository (documentation and license, DOI 10.5281/zenodo.23728612) and the ccchallenge links nos. 14, 15 and 16, which now point to it; the "Public links" section cites v1.5.
  • MAINTAINERS.md: "Continuity" section updated (version v4 of the Zenodo record with its erratum; repository of the formalisations of classical papers).
  • Top bar: from 769 to 1919 px wide, the menu moves to a second row instead of pushing the "Cite", theme, language and print buttons off the screen.
  • Browser cache: version parameters of main.js, main.css, research-ledger.js, research-ledger.json and lemmes.json updated.
  • The entries below are kept as they were.

v0.10.18 Accueil : le travail récent en tête ; le preprint et son erratum juste aprèsHome page: recent work first; the preprint and its erratum just after

  • Bannière de l'accueil : le dernier jalon du registre, Steiner 1978 en Lean sans l'hypothèse H_Rhin (dossier logs23/, release v1.4, 28/10/2026), avec ses limites, au lieu du théorème conditionnel du preprint d'avril 2026 et de son erratum, qui restent sur l'accueil juste après « État des travaux ».
  • Avertissement en tête de page : sous le surtitre, avant le titre, une courte mention dit que ce site ne prouve pas la conjecture de Collatz et que le preprint d'avril 2026 a un erratum du 2 octobre 2026 (lien), avec ce qui est démontré, dans les mots de l'erratum : aucun cycle non trivial avec k ≤ 1322, sous les hypothèses H1 et H2. L'avertissement et le mot « erratum » sont ainsi dans le premier écran en 1440 × 900 et dans une émulation de téléphone de 375 × 812 (tailles mesurées).
  • « État des travaux » : la section est déplacée juste sous le titre de la page ; son bandeau « § VI » devient « Travail récent », puisqu'elle précède désormais le § I ; son introduction renvoie à l'erratum du preprint. Ses cinq cartes ne changent pas, sauf « Dernier audit ».
  • Nouvelle section « Le preprint d'avril 2026 et son erratum du 2 octobre » : elle reprend, déplacés tels quels, l'encadré d'erratum (texte inchangé, ancre #erratum conservée), le résultat principal du preprint et les chiffres clés ; son intertitre et le titre du résultat principal apparaissent désormais dans le sommaire de la page.
  • Bannière, hauteur : à partir de 769 px de large, sa hauteur n'est plus fixe (elle garde la même hauteur minimale), pour que rien n'y soit rogné, ni sur tablette ni sur très grand écran (style de la page d'accueil, à l'écran seulement ; l'impression n'est pas modifiée).
  • Ancre #erratum : marge de défilement, pour que la barre du haut, qui reste affichée, ne cache plus la première ligne de l'encadré quand on y arrive par un lien.
  • Méta-descriptions (moteurs de recherche, Open Graph, Twitter) : elles commencent par l'état actuel (formalisations en Lean 4 de travaux classiques, dont Steiner 1978 sans H_Rhin, et « ce site ne prouve pas la conjecture ») ; le texte sur le preprint et son erratum suit, inchangé.
  • Données structurées (JSON-LD) : le site (nœud WebSite) reçoit une description qui commence par l'état actuel ; la description et le résumé du preprint ne changent pas.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.17, 2026-10-28) y est rappelé.
  • Cache des navigateurs : paramètre de version de main.js mis à jour (il sert aussi aux données du catalogue).
  • Les entrées ci-dessous restent telles quelles.
  • Home page banner: the latest milestone of the ledger, Steiner 1978 in Lean without the hypothesis H_Rhin (folder logs23/, release v1.4, 2026-10-28), with its limits, instead of the conditional theorem of the April 2026 preprint and its erratum, which stay on the home page just after "Research status".
  • Warning at the top of the page: under the eyebrow, before the title, a short notice says that this site does not prove the Collatz conjecture and that the April 2026 preprint has an erratum of 2 October 2026 (link), with what is proved, in the words of the erratum: no non-trivial cycle with k ≤ 1322, under hypotheses H1 and H2. The warning and the word "erratum" are thus on the first screen at 1440 × 900 and in a 375 × 812 phone emulation (measured sizes).
  • "Research status": the section is moved just below the page title; its "§ VI" eyebrow becomes "Recent work", since it now comes before § I; its introduction points to the erratum of the preprint. Its five cards do not change, except "Latest audit".
  • New section "The April 2026 preprint and its erratum of 2 October": it holds, moved as they were, the erratum box (text unchanged, anchor #erratum kept), the main result of the preprint and the key figures; its heading and the title of the main result now appear in the page's table of contents.
  • Banner, height: from 769 px wide, its height is no longer fixed (it keeps the same minimum height), so that nothing in it is cut, on tablets or on very wide screens (home-page style, on screen only; printing is not changed).
  • Anchor #erratum: scroll margin, so that the top bar, which stays visible, no longer hides the first line of the box when one arrives through a link.
  • Meta descriptions (search engines, Open Graph, Twitter): they start with the current state (Lean 4 formalisations of classical work, including Steiner 1978 without H_Rhin, and "this site does not prove the conjecture"); the text on the preprint and its erratum follows, unchanged.
  • Structured data (JSON-LD): the site (WebSite node) gets a description that starts with the current state; the description and abstract of the preprint do not change.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.17, 2026-10-28) is recalled.
  • Browser cache: version parameter of main.js updated (it is also used for the catalogue data).
  • The entries below are kept as they were.

v0.10.17 Steiner 1978 sans l'hypothèse H_Rhin ; pointeurs Zenodo ; correction de la piste P7Steiner 1978 without the hypothesis H_Rhin; Zenodo pointers; correction of lead P7

  • Registre de recherche (frise) : un jalon ajouté, le 28/10/2026 : le dossier logs23/ du dépôt Lean (release v1.4, DOI 10.5281/zenodo.23720217) démontre le théorème de Steiner 1978 sans l'hypothèse H_Rhin, par une minoration bien plus faible qui suffit (étape du 27/10, état final : commit 137c9be) ; H_Rhin lui-même n'est pas démontré, et aucune nouveauté n'est revendiquée. Compteurs : 38 événements au lieu de 37, dont 27 jalons au lieu de 26 ; données structurées (JSON-LD) et date de la page mises à jour.
  • Carte « Dernier jalon » de l'accueil : Steiner 1978 sans H_Rhin (28/10/2026) au lieu des 21 pistes « stub », qui deviennent le jalon précédent.
  • Carte « Dernière vérification Lean » de l'accueil : la vérification de logs23/ (14 énoncés, check.sh relancé le 28/10/2026 depuis un clone neuf) au lieu de celle de steiner1978/ (12 énoncés, dont 6 sous H_Rhin), rappelée ; archive Zenodo v1.4 au lieu de v1.2.
  • Page Histoire, entrée d'octobre : une phrase ajoutée (le 28/10, logs23/ et la release v1.4) ; sources : v0.10.0 à v0.10.7 et v0.10.10 à v0.10.17.
  • Page Papers, carte « Steiner 1978 en Lean 4 » : mise à jour datée du 28/10/2026 (sans H_Rhin dans logs23/, avec ses limites) ; lien vers logs23/ ; archive Zenodo v1.4 au lieu de v1.2 (toutes versions : DOI de concept).
  • Page Registre, liens publics : Steiner 1978 démontré sous H_Rhin, puis sans cette hypothèse dans logs23/ (v1.4) ; l'archive du dépôt Lean pointe désormais vers le DOI de concept, qui mène à la dernière version (v1.4 : 10.5281/zenodo.23720217), au lieu de la v1.2. Les entrées datées (changelog, flux, événements du 21 et du 27/10) gardent le DOI de leur version.
  • Correction (28/10/2026) de la piste P7 (Bayer–David 2025) : la fiche disait « Précédent méthodologique Lean Diophantine » ; c'est inexact : l'article (ITP 2025, DOI 10.4230/LIPIcs.ITP.2025.3) et sa formalisation (Archive of Formal Proofs, « Universal Pairs for Diophantine Equations ») sont en Isabelle/HOL et portent sur le dixième problème de Hilbert. Texte et référence corrigés ; statut inchangé.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.16, 2026-10-27) y est rappelé.
  • Cache des navigateurs : paramètres de version de main.js (il sert aussi aux données du catalogue), de research-ledger.js et de research-ledger.json (page Registre) mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • Research ledger (timeline): one milestone added, on 2026-10-28: the logs23/ folder of the Lean repository (release v1.4, DOI 10.5281/zenodo.23720217) proves Steiner's 1978 theorem without the hypothesis H_Rhin, through a much weaker lower bound that suffices (step of 2026-10-27, final state: commit 137c9be); H_Rhin itself is not proved, and no novelty is claimed. Counters: 38 events instead of 37, 27 of them milestones instead of 26; structured data (JSON-LD) and date of the page updated.
  • "Latest milestone" card of the home page: Steiner 1978 without H_Rhin (2026-10-28) instead of the 21 "stub" leads, which become the previous milestone.
  • "Last Lean verification" card of the home page: the check of logs23/ (14 statements, check.sh run on 2026-10-28 from a fresh clone) instead of that of steiner1978/ (12 statements, 6 of them under H_Rhin), which is recalled; Zenodo archive v1.4 instead of v1.2.
  • History page, October entry: one sentence added (on 28 October, logs23/ and release v1.4); sources: v0.10.0 to v0.10.7 and v0.10.10 to v0.10.17.
  • Papers page, "Steiner 1978 in Lean 4" card: dated update of 2026-10-28 (without H_Rhin in logs23/, with its limits); link to logs23/; Zenodo archive v1.4 instead of v1.2 (all versions: concept DOI).
  • Ledger page, public links: Steiner 1978 proved under H_Rhin, and then without that hypothesis in logs23/ (v1.4); the archive of the Lean repository now points to the concept DOI, which leads to the latest version (v1.4: 10.5281/zenodo.23720217), instead of v1.2. Dated entries (changelog, feed, events of 21 and 27 October) keep the DOI of their version.
  • Correction (2026-10-28) of lead P7 (Bayer–David 2025): the entry said "Lean Diophantine methodological precedent"; this is inaccurate: the paper (ITP 2025, DOI 10.4230/LIPIcs.ITP.2025.3) and its formalisation (Archive of Formal Proofs, "Universal Pairs for Diophantine Equations") are in Isabelle/HOL and concern Hilbert's tenth problem. Text and reference corrected; status unchanged.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.16, 2026-10-27) is recalled.
  • Browser cache: version parameters of main.js (also used for the catalogue data), of research-ledger.js and of research-ledger.json (Ledger page) updated.
  • The entries below are kept as they were.

v0.10.16 Frise et synthèse : registre, Histoire et accueil mis à jourTimeline and summary: ledger, History and home page updated

  • Registre de recherche (frise) : trois événements ajoutés : le 21/10/2026 au soir, la formalisation de Steiner 1978 comparée à l'article original, lu après la release v1.2 sur une copie numérisée (rien ne change dans les fichiers Lean) ; le 27/10/2026, la release v1.3 du dépôt Lean (DOI 10.5281/zenodo.23686224 ; documentation seulement, fichiers Lean inchangés), qui consigne le retrait, daté du 21/10, de l'affirmation selon laquelle l'article n'avait pas pu être consulté ; le 27/10/2026, un jalon : les 21 pistes « stub » du catalogue tranchées (v0.10.11 à v0.10.15), avec les corrections publiées en chemin (nom de la piste F, pistes K et C, mea culpa #23, piste L, ancien texte de X, ancienne note de Z).
  • Compteurs du registre : 37 événements au lieu de 34, dont 26 jalons au lieu de 25 ; répartitions par type, statut, portée et statut épistémique recomptées ; données structurées (JSON-LD) et date de la page mises à jour. Les compteurs du § I (preprint, phases Lean, findings, mea culpa, études ouvertes) sont inchangés.
  • Page Histoire, entrée d'octobre : deux phrases ajoutées (la release v1.3, documentation et métadonnées seulement ; les 21 pistes « stub » tranchées du 22 au 27/10) ; sources : v0.10.0 à v0.10.7 et v0.10.10 à v0.10.16.
  • Carte « Dernier jalon » de l'accueil : les 21 pistes « stub » tranchées (27/10/2026) au lieu de Steiner 1978, qui devient le jalon précédent.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.15, 2026-10-27) y est rappelé.
  • Carte « Dernière vérification Lean » : vérifiée et laissée telle quelle, la v1.3 ne modifiant aucun fichier Lean.
  • Cache des navigateurs : paramètres de version de main.js (il sert aussi aux données du catalogue), de research-ledger.js et de research-ledger.json (page Registre) mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • Research ledger (timeline): three events added: on the evening of 2026-10-21, the Steiner 1978 formalisation compared with the original paper, read after release v1.2 in a scanned copy (nothing in the Lean files changes); on 2026-10-27, release v1.3 of the Lean repository (DOI 10.5281/zenodo.23686224; documentation only, Lean files unchanged), which records the withdrawal, dated 21 October, of the statement that the paper "could not be accessed"; on 2026-10-27, a milestone: the 21 "stub" leads of the catalogue settled (v0.10.11 to v0.10.15), with the corrections published along the way (name of lead F, leads K and C, mea culpa #23, lead L, former text of X, former note of Z).
  • Ledger counters: 37 events instead of 34, 26 of them milestones instead of 25; breakdowns by type, status, scope and epistemic status recounted; structured data (JSON-LD) and date of the page updated. The counters of § I (preprint, Lean phases, findings, mea culpa, open studies) are unchanged.
  • History page, October entry: two sentences added (release v1.3, documentation and metadata only; the 21 "stub" leads settled from 22 to 27 October); sources: v0.10.0 to v0.10.7 and v0.10.10 to v0.10.16.
  • "Latest milestone" card of the home page: the 21 "stub" leads settled (2026-10-27) instead of Steiner 1978, which becomes the previous milestone.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.15, 2026-10-27) is recalled.
  • "Last Lean verification" card: checked and left as it was, since v1.3 changes no Lean file.
  • Browser cache: version parameters of main.js (also used for the catalogue data), of research-ledger.js and of research-ledger.json (Ledger page) updated.
  • The entries below are kept as they were.

v0.10.15 Catalogue : dernière piste « stub » tranchée ; test REQ-MATH-007 retiré ; bibliothèque prototype archivéeCatalogue: last "stub" lead settled; test REQ-MATH-007 withdrawn; prototype library archived

  • Piste Z (dynamique holomorphe, Letherman–Schleicher–Wood 1999) : cul-de-sac, désormais sourcé, et ancienne note corrigée : dans les fonctions entières de Letherman, Schleicher et Wood, les entiers sont des points critiques, si bien qu'un cycle d'entiers y est superattractif (multiplicateur nul) ; la formule de l'ancienne note (« log|ρ| = -Λ avec convention Lagarias — encode Baker ») vaut pour une autre fonction, l'interpolation étudiée par Chamberland (1996), où le multiplicateur redonne la forme linéaire S log 2 − k log 3 de l'approche principale.
  • Diagramme du verrou : l'étiquette « log|ρ| = -Λ » de la flèche « Holomorphic LSW » est retirée : elle ne vaut pas pour les fonctions de Letherman, Schleicher et Wood (voir la piste Z).
  • Catalogue des pistes : plus aucune piste n'est marquée stub ; les vingt et une qui l'étaient ont été tranchées les 22 et 27/10/2026 (v0.10.11 à v0.10.15).
  • Compteurs : la carte « pistes cataloguées » de l'accueil indique « plus aucune note à sourcer » au lieu d'une, et l'introduction du catalogue cite les vingt et une pistes tranchées.
  • Test REQ-MATH-007 (lemmes ChatGPT en Lean) : retiré au lieu de « avertissement » : son fichier (branche arsenal-postjar, Lean 4.27.0) n'a pas changé depuis le 29/04/2026, nous ne lui connaissons aucune recompilation sous Lean 4.34, et aucun fichier publié ne l'importe (les deux lemmes de ce fichier dont dépend le théorème CGS-7, drop_forces_s_ge_two et one_step_strict_increase_if_s_eq_one, en ont été recopiés dans CGS7Dependencies.lean).
  • Carte « Bibliothèque prototype : minima locaux et blocs » de la page Papers : archivée au lieu de « à consolider ou à archiver » : elle ne sert à aucune des formalisations prévues par le labo, et nous ne lui connaissons aucune revérification sous Lean 4.34 ; la mise en garde sur l'axiome hercher_m_le_91_axiom est conservée. L'introduction de la section cite désormais les cartes archivées. Ses deux fichiers sont marqués « archivé » dans la liste de l'arsenal de la page Lemmes. Le dépôt de code n'est pas modifié.
  • Retouches de la v0.10.14 : mea culpa #23 : l'article de Rozier est daté « en ligne en 2025 », le résumé de la règle retrouve sa fin d'avril (« ou via DOI/zbMATH/MR »), et la leçon est dite « précisée » au lieu de « élargie » ; piste Y : « les bibliographies annotées de Lagarias » au lieu de « la bibliographie annotée » (les exposants 0,841 et 0,809 viennent de deux bibliographies), et « la notice zbMATH de leur article ».
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.14, 2026-10-27) y est rappelé.
  • Cache des navigateurs : paramètres de version de main.js (il sert aussi aux données du catalogue) et de lemmes.json (page Lemmes) mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • Lead Z (holomorphic dynamics, Letherman–Schleicher–Wood 1999): dead end, now sourced, and former note corrected: in the entire functions of Letherman, Schleicher and Wood, the integers are critical points, so that an integer cycle is superattracting there (multiplier zero); the formula of the former note ("log|ρ| = -Λ with Lagarias convention — encodes Baker") applies to another function, the interpolation studied by Chamberland (1996), where the multiplier gives back the linear form S log 2 − k log 3 of the main approach.
  • Lock diagram: the label "log|ρ| = -Λ" of the "Holomorphic LSW" arrow is removed: it does not hold for the functions of Letherman, Schleicher and Wood (see lead Z).
  • Catalogue of leads: no lead is marked stub any more; the twenty-one that were have been settled on 2026-10-22 and 2026-10-27 (v0.10.11 to v0.10.15).
  • Counters: the "catalogued approaches" card of the home page reads "no stub notes left" instead of one, and the introduction of the catalogue cites the twenty-one settled leads.
  • Test REQ-MATH-007 (ChatGPT lemmas in Lean): withdrawn instead of "warning": its file (arsenal-postjar branch, Lean 4.27.0) has not changed since 2026-04-29, we know of no recompilation of it under Lean 4.34, and no published file imports it (the two lemmas of this file on which the CGS-7 theorem depends, drop_forces_s_ge_two and one_step_strict_increase_if_s_eq_one, were copied from it into CGS7Dependencies.lean).
  • "Prototype library: local minima and blocks" card of the Papers page: archived instead of "to consolidate or archive": it serves none of the formalisations planned by the lab, and we know of no re-check of it under Lean 4.34; the warning about the axiom hercher_m_le_91_axiom is kept. The introduction of the section now mentions archived cards. Its two files are marked "archived" in the arsenal list of the Lemmas page. The code repository is not modified.
  • Touch-ups of v0.10.14: mea culpa #23: Rozier's paper is dated "online in 2025", the summary of the rule gets back its April ending ("or via DOI/zbMATH/MR"), and the lesson is said to be "made more precise" instead of "widened"; lead Y: "Lagarias's annotated bibliographies" instead of "annotated bibliography" (the exponents 0.841 and 0.809 come from two bibliographies), and "the zbMATH review of their paper".
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.14, 2026-10-27) is recalled.
  • Browser cache: version parameters of main.js (also used for the catalogue data) and of lemmes.json (Lemmas page) updated.
  • The entries below are kept as they were.

v0.10.14 Catalogue : cinq autres pistes « stub » tranchées ; mea culpa #23 corrigéCatalogue: five more "stub" leads settled; mea culpa #23 corrected

  • Catalogue des pistes : cinq autres pistes marquées stub, toutes de la Région II, sont tranchées, chacune avec sa source ou sa raison : cinq culs-de-sac, dont quatre sourcés (Q.bis, V, X, Y) et un sans source propre, dont la raison est sourcée (W).
  • Piste Q.bis (parityGraph à rebours) : classée cul-de-sac en l'état au lieu de « Inconnue », sourcé : l'étude à rebours existe (ensembles de prédécesseurs : Wirsching, 1996 ; minoration de leur taille pour tout entier non multiple de 3 : Krasikov et Lagarias, 2003) ; elle s'appliquerait aux éléments d'un éventuel cycle non trivial, dont aucun n'est multiple de 3, mais dit seulement que leurs ensembles de prédécesseurs seraient grands, non qu'un tel cycle n'existe pas.
  • Piste V (FRACTRAN / Conway 1972) : cul-de-sac, désormais sourcé : l'indécidabilité montrée par Conway (1972) et le langage FRACTRAN qu'il en a tiré (1987) portent sur des familles d'applications de type Collatz généralisées, pas sur l'application 3x+1 ni sur ses cycles.
  • Piste W (Anashin 2-adique) : cul-de-sac, sans source propre : nous n'avons trouvé aucun travail d'Anashin sur 3x+1 (zbMATH et arXiv), et la référence notée en avril 2026 pour cette piste est un article sans rapport ; la raison est sourcée, la même que pour la piste P (Lagarias 1985, remarque suivant le théorème K : ce théorème n'implique rien sur les entiers, ensemble de mesure nulle dans les entiers 2-adiques).
  • Piste X (Tao 2022) : cul-de-sac, désormais sourcé ; même article que la piste B : son théorème vaut pour presque tout entier (densité logarithmique), ce qui ne peut pas exclure un cycle, ensemble fini ; l'ancien texte de la fiche (« Tao exclut explicitement cycles dans son paper ») est remplacé par ce que dit l'article (remarque 1.4 et § 5).
  • Piste Y (Krasikov–Lagarias 2003) : cul-de-sac, désormais sourcé : le résultat minore le nombre π_a(x) d'entiers n ≤ x dont l'orbite atteint a, pour tout a non multiple de 3 (π_a(x) > x^0,841 pour x assez grand) ; il s'appliquerait aux éléments d'un cycle non trivial, mais n'exclut pas un tel cycle.
  • Mea culpa #23 (« 3 références inventées ») : correction datée ajoutée, le mea culpa restant en place : vérifiées à la source, deux des trois références existent (O. Rozier, arXiv:2306.15284, 2023 ; J. Berstel et M. Mignotte, Bull. Soc. Math. France 104 (1976), 175-184) ; la troisième (« Bell-Burris-Hanrot-Sands 2013 ») reste introuvable (zbMATH et arXiv).
  • Piste L (Néron-Tate / abc) : nom et référence corrigés : « Rozier-Terracol 2026 » et Rozier-Terracol, Discrete Math. 349(10), 115167 (un autre article, dont le résumé ne mentionne pas abc) deviennent « Rozier 2023 » et Rozier, Experimental Math. 35 (2026), 325-334; arXiv:2306.15284 ; son texte est inchangé.
  • Filtre « Inconnues » du catalogue : retiré, plus aucune piste n'ayant ce statut (Q.bis était la dernière).
  • Compteurs : 1 note à sourcer sur 36 (≈3 %) au lieu de 6 (≈17 %), dans la carte « pistes cataloguées » de l'accueil et dans l'introduction du catalogue, qui cite désormais les vingt pistes tranchées.
  • Carte B des hypothèses : « 16 sur 16 culs-de-sac dans la Région II » au lieu de 15 (la piste Q.bis) ; son estimation est inchangée.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.13, 2026-10-27) y est rappelé.
  • Cache des navigateurs : paramètre de version de main.js mis à jour (il sert aussi aux données du catalogue).
  • Les entrées ci-dessous restent telles quelles.
  • Catalogue of leads: five more leads marked stub, all in Region II, are settled, each with its source or its reason: five dead ends, four of them sourced (Q.bis, V, X, Y) and one with no source of its own, whose reason is sourced (W).
  • Lead Q.bis (backward parityGraph): classified as a dead end as things stand instead of "Unexplored", sourced: the backward study exists (predecessor sets: Wirsching, 1996; lower bound on their size for every integer not divisible by 3: Krasikov and Lagarias, 2003); it would apply to the elements of a possible non-trivial cycle, none of which is a multiple of 3, but only says that their predecessor sets would be large, not that such a cycle does not exist.
  • Lead V (FRACTRAN / Conway 1972): dead end, now sourced: the undecidability shown by Conway (1972) and the FRACTRAN language he drew from it (1987) concern families of generalised Collatz-type maps, not the 3x+1 map nor its cycles.
  • Lead W (Anashin 2-adic): dead end, with no source of its own: we found no work by Anashin on 3x+1 (zbMATH and arXiv), and the reference noted in April 2026 for this lead is an unrelated paper; the reason is sourced, the same as for lead P (Lagarias 1985, remark following Theorem K: that theorem implies nothing about the integers, a set of measure zero in the 2-adic integers).
  • Lead X (Tao 2022): dead end, now sourced; same paper as lead B: its theorem holds for almost all integers (logarithmic density), which cannot exclude a cycle, a finite set; the former text of the entry ("Tao explicitly excludes cycles in his paper") is replaced by what the paper says (Remark 1.4 and § 5).
  • Lead Y (Krasikov–Lagarias 2003): dead end, now sourced: the result bounds from below the number π_a(x) of integers n ≤ x whose orbit reaches a, for every a not divisible by 3 (π_a(x) > x^0.841 for sufficiently large x); it would apply to the elements of a non-trivial cycle, but does not exclude such a cycle.
  • Mea culpa #23 ("3 fabricated references"): dated correction added, the mea culpa staying in place: checked at the source, two of the three references exist (O. Rozier, arXiv:2306.15284, 2023; J. Berstel and M. Mignotte, Bull. Soc. Math. France 104 (1976), 175-184); the third ("Bell-Burris-Hanrot-Sands 2013") remains untraceable (zbMATH and arXiv).
  • Lead L (Néron-Tate / abc): name and reference corrected: "Rozier-Terracol 2026" and Rozier-Terracol, Discrete Math. 349(10), 115167 (another paper, whose abstract does not mention abc) become "Rozier 2023" and Rozier, Experimental Math. 35 (2026), 325-334; arXiv:2306.15284; its text is unchanged.
  • "Unexplored" filter of the catalogue: removed, as no lead has this status any more (Q.bis was the last one).
  • Counters: 1 note to be sourced out of 36 (≈3 %) instead of 6 (≈17 %), in the "catalogued approaches" card of the home page and in the introduction of the catalogue, which now cites the twenty settled leads.
  • Card B of the hypotheses: "16 of 16 dead-ends in Region II" instead of 15 (lead Q.bis); its estimate is unchanged.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.13, 2026-10-27) is recalled.
  • Browser cache: version parameter of main.js updated (it is also used for the catalogue data).
  • The entries below are kept as they were.

v0.10.13 Catalogue : cinq autres pistes « stub » tranchéesCatalogue: five more "stub" leads settled

  • Catalogue des pistes : cinq autres pistes marquées stub, toutes de la Région II, sont tranchées, chacune avec sa source ou sa raison : cinq culs-de-sac, dont quatre sourcés (N, O, P, Q) et un sans source publiée, fondé sur une exploration du labo d'avril 2026 (I.1).
  • Piste I.1 (tresses / nœuds) : cul-de-sac, sans source publiée : aucune source trouvée ; l'exploration du labo du 29/04/2026 notait « Pas d'encodage canonique cycle Collatz ↦ objet topologique », et concluait que les invariants topologiques sont « insensibles à valuations 2/3-adiques ».
  • Piste N (topos arithmétique, IUT de Mochizuki) : classée cul-de-sac en l'état au lieu de « Inconnue » : la preuve de la conjecture abc par la théorie inter-universelle de Teichmüller est contestée (notice zbMATH de sa première partie, signée par P. Scholze), et le seul lien publié entre abc et 3x+1 que nous ayons trouvé (Rozier, 2025) ne porte pas sur les cycles.
  • Piste O (théorie de la complexité) : classée cul-de-sac en l'état au lieu de « Inconnue » : les résultats d'indécidabilité que nous avons trouvés (Conway 1972 ; Kurtz et Simon 2007) portent sur des applications de Collatz généralisées, pas sur l'application 3x+1 ; nous n'avons trouvé aucune source qui relie ses cycles à une réduction de type Cook–Levin.
  • Piste P (mécanique statistique, Sinai 2003) : classée cul-de-sac au lieu de « Inconnue », sourcé : Sinai (2003) donne des énoncés statistiques, et Lagarias (1985, théorème K, d'après Matthews et Watts) note que le mélange de T sur les entiers 2-adiques n'implique rien sur les entiers, de mesure nulle.
  • Piste Q (parityGraph forward) : cul-de-sac, désormais sourcé : la matrice d'adjacence du graphe de 3x+1 a été étudiée (Alves et al. 2005 ; Cardon et Tuckfield 2011), et ces formulations sont équivalentes à la question des cycles, sans la trancher ; sur toute partie finie stable par l'application, le spectre ne fait que redire les cycles (vérifié par nous).
  • Compteurs : 6 notes à sourcer sur 36 (≈17 %) au lieu de 11 (≈31 %), dans la carte « pistes cataloguées » de l'accueil et dans l'introduction du catalogue, qui cite désormais les quinze pistes tranchées.
  • Carte B des hypothèses : « 15 sur 16 culs-de-sac dans la Région II » au lieu de 12 (les pistes N, O et P) ; son estimation est inchangée.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.12, 2026-10-22) y est rappelé.
  • Cache des navigateurs : paramètre de version de main.js mis à jour (il sert aussi aux données du catalogue).
  • Les entrées ci-dessous restent telles quelles.
  • Catalogue of leads: five more leads marked stub, all in Region II, are settled, each with its source or its reason: five dead ends, four of them sourced (N, O, P, Q) and one with no published source, based on an exploration by the lab in April 2026 (I.1).
  • Lead I.1 (braids / knots): dead end, with no published source: none found; the lab's exploration of 2026-04-29 had found no canonical encoding of a cycle as a topological object, and concluded that topological invariants are insensitive to 2-adic and 3-adic valuations.
  • Lead N (arithmetic topos, Mochizuki's IUT): classified as a dead end as things stand instead of "Unexplored": the proof of the abc conjecture by inter-universal Teichmüller theory is disputed (zbMATH review of its first part, signed by P. Scholze), and the only published link between abc and 3x+1 that we found (Rozier, 2025) does not concern cycles.
  • Lead O (complexity theory): classified as a dead end as things stand instead of "Unexplored": the undecidability results that we found (Conway 1972; Kurtz and Simon 2007) concern generalised Collatz maps, not the 3x+1 map; we found no source linking its cycles to a Cook–Levin-type reduction.
  • Lead P (statistical mechanics, Sinai 2003): classified as a dead end instead of "Unexplored", sourced: Sinai (2003) gives statistical statements, and Lagarias (1985, Theorem K, after Matthews and Watts) notes that the mixing of T on the 2-adic integers implies nothing about the integers, a set of measure zero.
  • Lead Q (forward parityGraph): dead end, now sourced: the adjacency matrix of the 3x+1 graph has been studied (Alves et al. 2005; Cardon and Tuckfield 2011), and these formulations are equivalent to the cycle question without settling it; on any finite subset stable under the map, the spectrum only restates the cycles (checked by us).
  • Counters: 6 notes to be sourced out of 36 (≈17 %) instead of 11 (≈31 %), in the "catalogued approaches" card of the home page and in the introduction of the catalogue, which now cites the fifteen settled leads.
  • Card B of the hypotheses: "15 of 16 dead-ends in Region II" instead of 12 (leads N, O and P); its estimate is unchanged.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.12, 2026-10-22) is recalled.
  • Browser cache: version parameter of main.js updated (it is also used for the catalogue data).
  • The entries below are kept as they were.

v0.10.12 Catalogue : cinq autres pistes « stub » tranchéesCatalogue: five more "stub" leads settled

  • Catalogue des pistes : cinq autres pistes marquées stub sont tranchées, chacune avec sa source ou sa raison : trois culs-de-sac sourcés (H, H.1 pour son volet MSO / Büchi–Bruyère, H.2), un cul-de-sac sans source propre (R), une piste retirée, dont la réouverture n'a pas été précisée (M) ; et deux corrections de la v0.10.11 (C, K).
  • Piste M (BHV, Bilu–Hanrot–Voutier) : retirée : une application, en avril 2026, avait été formulée puis reconnue tautologique (mea culpa n° 11 : par l'identité R72, elle revenait à supposer qu'aucun cycle non trivial n'existe) ; les « applications spécifiques » de la réouverture qui a suivi n'ont pas été précisées, et nous n'avons trouvé aucune source qui relie ce théorème aux cycles ; dans le tableau, « Partielle » devient « Cul-de-sac », avec « retirée (réouverture non précisée) » dans son nom, et la colonne 4-test passe de « 3/4 » à « — » ; la référence de l'article est ajoutée.
  • Piste R (invariants statistiques) : cul-de-sac, sans source propre pour les autocorrélations (les moments se ramènent à la proportion de termes impairs, déjà étudiée) ; sa raison est sourcée, et c'est la même que pour la piste C : ces invariants ne dépendent que du mot de parité, et tout mot qui contient un 1 et vérifie 2^S > 3^k est celui d'un cycle rationnel positif (Halbeisen et Hungerbühler, Acta Arith. 78 (1997), Lemme 2 et §5).
  • Piste H (logique modèle-théorique) : cul-de-sac, désormais sourcé : Cobham (1969) ; Villemaire (1992), ⟨ℕ, +, V₂, V₃⟩ indécidable ; et deux prépublications de 2026 (arXiv:2601.12772, arXiv:2602.06066), selon lesquelles l'itération de 3x+1 n'est pas définissable dans l'arithmétique de Büchi en base 2, ni l'accessibilité en base 3.
  • Piste H.1 (MSO / Skolem–Bruyère) : classée cul-de-sac au lieu de « Inconnue », avec les sources de H qui la concernent (Villemaire 1992 et les deux prépublications de 2026) et Bruyère, Hansel, Michaux et Villemaire (1994) ; en avril 2026, elle avait été abordée sous la piste H.
  • Piste H.2 (Skolem–Mahler–Lech / Derksen) : cul-de-sac, désormais sourcé (Lech 1953, Derksen 2007) : ces théorèmes portent sur les suites récurrentes linéaires ; l'application 3x+1 n'est pas linéaire, et l'orbite d'un cycle est une récurrence linéaire triviale.
  • Correction (22/10/2026) des pistes K et C de la v0.10.11 : la fiche K de la v0.10.11 disait que la note d'avril n'avait jamais été rédigée (ni reliée à une courbe ou à un schéma) ; c'est inexact : un compte rendu interne non publié du 28/04/2026 (2026-04-28-2105-from-NEW3-to-NEW-Q6-schema-arithmetique.md) en contient une analyse (le cycle vu comme un schéma arithmétique, le théorème de Faltings sous condition de genre ≥ 2, genre non calculé, aucune source reliant les cycles à ce cadre). La fiche le dit désormais, avec des citations exactes ; l'issue (retirée, non sourcée) est inchangée, pour les raisons qu'elle donne. La fiche C dit désormais que le volet « Fourier discret » n'a, dans ce que nous avons relu, aucune source publiée (les comptes rendus d'avril 2026 le ramènent à Λ_{S,k}, le plus souvent via le volet sturmien, par des renvois internes).
  • Compteurs : 11 notes à sourcer sur 36 (≈31 %) au lieu de 16 (≈44 %), dans la carte « pistes cataloguées » de l'accueil et dans l'introduction du catalogue, qui cite désormais les dix pistes tranchées.
  • Carte B des hypothèses : « 12 sur 16 culs-de-sac dans la Région II » au lieu de 11 (la piste H.1) ; son estimation est inchangée.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.11, 2026-10-22) y est rappelé.
  • Cache des navigateurs : paramètre de version de main.js mis à jour (il sert aussi aux données du catalogue).
  • Les entrées ci-dessous restent telles quelles ; les fiches C et K de l'entrée v0.10.11 sont corrigées par la puce « Correction » ci-dessus.
  • Catalogue of leads: five more leads marked stub are settled, each with its source or its reason: three sourced dead ends (H, H.1 for its MSO / Büchi–Bruyère part, H.2), one dead end with no source of its own (R), one lead withdrawn, whose reopening was not specified (M); and two corrections to v0.10.11 (C, K).
  • Lead M (BHV, Bilu–Hanrot–Voutier): withdrawn: an application, in April 2026, had been formulated and then found to be tautological (mea culpa #11: by the identity R72, it amounted to assuming that no non-trivial cycle exists); the "specific applications" of the reopening that followed were not specified, and we found no source linking this theorem to cycles; in the table, "Partial" becomes "Dead end", with "withdrawn (reopening not specified)" in its name, and the 4-test column goes from "3/4" to "—"; the reference of the paper is added.
  • Lead R (statistical invariants): dead end, with no source of its own for the autocorrelations (the moments reduce to the proportion of odd terms, already studied); its reason is sourced, and it is the same as for lead C: these invariants depend only on the parity word, and every word that contains a 1 and satisfies 2^S > 3^k is that of a positive rational cycle (Halbeisen and Hungerbühler, Acta Arith. 78 (1997), Lemma 2 and §5).
  • Lead H (model-theoretic logic): dead end, now sourced: Cobham (1969); Villemaire (1992), ⟨ℕ, +, V₂, V₃⟩ undecidable; and two 2026 preprints (arXiv:2601.12772, arXiv:2602.06066), according to which the iteration of 3x+1 is not definable in Büchi arithmetic in base 2, nor reachability in base 3.
  • Lead H.1 (MSO / Skolem–Bruyère): classified as a dead end instead of "Unexplored", with the sources of H that concern it (Villemaire 1992 and the two 2026 preprints) and Bruyère, Hansel, Michaux and Villemaire (1994); in April 2026, it had been addressed under lead H.
  • Lead H.2 (Skolem–Mahler–Lech / Derksen): dead end, now sourced (Lech 1953, Derksen 2007): these theorems are about linear recurrence sequences; the 3x+1 map is not linear, and the orbit of a cycle is a trivial linear recurrence.
  • Correction (2026-10-22) of leads K and C of v0.10.11: the entry for K in v0.10.11 said that the April note had never been written up (nor linked to a curve or a scheme); this is inaccurate: an unpublished internal report of 2026-04-28 (2026-04-28-2105-from-NEW3-to-NEW-Q6-schema-arithmetique.md) contains an analysis of it (the cycle viewed as an arithmetic scheme, Faltings's theorem under a genus ≥ 2 condition, genus not computed, no source linking cycles to this framework). The entry now says so; the outcome (withdrawn, unsourced) is unchanged, for the reasons it gives. The entry for C now says that the "discrete Fourier" part has, in what we have re-read, no published source (the April 2026 reports reduce it to Λ_{S,k}, mostly via the Sturmian part, through internal references).
  • Counters: 11 notes to be sourced out of 36 (≈31 %) instead of 16 (≈44 %), in the "catalogued approaches" card of the home page and in the introduction of the catalogue, which now cites the ten settled leads.
  • Card B of the hypotheses: "12 of 16 dead-ends in Region II" instead of 11 (lead H.1); its estimate is unchanged.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.11, 2026-10-22) is recalled.
  • Browser cache: version parameter of main.js updated (it is also used for the catalogue data).
  • The entries below are kept as they were; the entries for C and K in the v0.10.11 entry are corrected by the "Correction" bullet above.

v0.10.11 Catalogue : cinq pistes « stub » tranchéesCatalogue: five "stub" leads settled

  • Catalogue des pistes : les cinq premières pistes marquées stub (notes non sourcées) sont tranchées, chacune avec sa source ou sa raison : trois culs-de-sac sourcés (C, E.4, F), un cul-de-sac sans source publiée (J), une piste retirée faute de source (K).
  • Piste C (Fourier discret / Sturmien) : cul-de-sac, désormais sourcé. Fernández et Ibáñez (arXiv:2607.24844, prépublication de 2026) relient mots de Christoffel et cycles par des estimations de taille ; Halbeisen et Hungerbühler (Acta Arith. 78 (1997), Lemme 2 et §5) notent que de telles estimations, valables pour les cycles rationnels, ne suffisent pas, seules, à exclure les cycles entiers. Le volet « Fourier discret », jamais rédigé, est retiré ; le nom de la piste le signale.
  • Piste E.4 (Zudilin 2007) : source ajoutée (J. Théor. Nombres Bordeaux 19 (2007), DOI 10.5802/jtnb.588) ; classée cul-de-sac au lieu de « partielle » : sa borne porte sur ‖(3/2)^k‖ et, par cette voie, ne donne pas plus que 2^(k−1) pour 2^S − 3^k, loin de ce que demande H1.
  • Piste F : renommée « Marcovecchio 2014 (non-quadraticité de log 2) ». Nous n'avons trouvé aucun article de 2025 ; le seul texte de l'auteur daté de 2025 est le dépôt sur arXiv d'un article paru en 2014 (Int. J. Number Theory 10, DOI 10.1142/S1793042114500584), désormais cité. Cul-de-sac : ses mesures portent sur l'approximation d'un logarithme comme log 2, pas sur la forme S ln 2 − k ln 3. Dans le diagramme du verrou, le nœud devient « Marcovecchio 2014 ».
  • Piste J (tropical, suggestion d'un assistant IA) : classée cul-de-sac au lieu de « partielle », sans source publiée (aucune trouvée) : la tropicalisation de l'équation des cycles, vérifiée par le labo le 26/09/2026, est satisfaite d'office et redonne la congruence de départ.
  • Piste K (schémas arithmétiques + Faltings) : retirée, non sourcée : jamais formulée ni rédigée, aucune source trouvée ; dans le tableau, « Partielle » devient « Cul-de-sac », avec « retirée (non sourcée) » dans son nom, et la colonne 4-test passe de « 1/4 » à « — ». Dans le diagramme du verrou, son nœud et sa flèche passent en pointillé ; le nœud porte la date du retrait (« ✗ 2026-10-22 ») et la flèche perd son étiquette « hauteurs ⇔ ABC ».
  • Compteurs : 16 notes à sourcer sur 36 (≈44 %) au lieu de 21 (≈58 %), dans la carte « pistes cataloguées » de l'accueil et dans l'introduction du catalogue, qui cite aussi les cinq pistes tranchées.
  • Verrou Λ : la phrase d'introduction date d'avril 2026 le décompte « quatorze des quinze paradigmes » et le dit en revue ; la légende du diagramme ne donne plus de nombre (« les paradigmes du diagramme », liste d'avril 2026, en revue) ; toutes deux signalent le retrait de « Schémas + Faltings ». La carte C des hypothèses porte la même mention ; son estimation est inchangée.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.10, 2026-10-21) y est rappelé.
  • Cache des navigateurs : paramètre de version de main.js mis à jour (il sert aussi aux données du catalogue).
  • Les entrées ci-dessous restent telles quelles.
  • Catalogue of leads: the first five leads marked stub (unsourced notes) are settled, each with its source or its reason: three sourced dead ends (C, E.4, F), one dead end with no published source (J), one lead withdrawn for lack of a source (K).
  • Lead C (discrete Fourier / Sturmian): dead end, now sourced. Fernández and Ibáñez (arXiv:2607.24844, 2026 preprint) link Christoffel words and cycles through size estimates; Halbeisen and Hungerbühler (Acta Arith. 78 (1997), Lemma 2 and §5) note that such estimates, valid for rational cycles, cannot on their own exclude integer cycles. The "discrete Fourier" part, never written up, is withdrawn; the name of the lead says so.
  • Lead E.4 (Zudilin 2007): source added (J. Théor. Nombres Bordeaux 19 (2007), DOI 10.5802/jtnb.588); classified as a dead end instead of "partial": its bound concerns ‖(3/2)^k‖ and, this way, gives no more than 2^(k−1) for 2^S − 3^k, far from what H1 requires.
  • Lead F: renamed "Marcovecchio 2014 (non-quadraticity of log 2)". We found no paper from 2025; the author's only text dated 2025 is the arXiv deposit of a paper published in 2014 (Int. J. Number Theory 10, DOI 10.1142/S1793042114500584), now cited. Dead end: its measures concern the approximation of a logarithm such as log 2, not the form S ln 2 − k ln 3. In the lock diagram, the node becomes "Marcovecchio 2014".
  • Lead J (tropical, suggested by an AI assistant): classified as a dead end instead of "partial", with no published source (none found): the tropicalisation of the cycle equation, checked by the lab on 2026-09-26, is satisfied for free and gives back the starting congruence.
  • Lead K (arithmetic schemes + Faltings): withdrawn, unsourced: never formulated nor written up, no source found; in the table, "Partial" becomes "Dead end", with "withdrawn (unsourced)" in its name, and the 4-test column goes from "1/4" to "—". In the lock diagram, its node and its arrow are now dashed; the node carries the date of the withdrawal ("✗ 2026-10-22") and the arrow loses its label ("hauteurs ⇔ ABC").
  • Counters: 16 notes to be sourced out of 36 (≈44 %) instead of 21 (≈58 %), in the "catalogued approaches" card of the home page and in the introduction of the catalogue, which also cites the five settled leads.
  • Λ lock: the introductory sentence dates the count "fourteen of the fifteen paradigms" to April 2026 and says that it is under review; the caption of the diagram no longer gives a number ("the paradigms of the diagram", April 2026 list, under review); both mention the withdrawal of "Schemes + Faltings". Card C of the hypotheses carries the same mention; its estimate is unchanged.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.10, 2026-10-21) is recalled.
  • Browser cache: version parameter of main.js updated (it is also used for the catalogue data).
  • The entries below are kept as they were.

v0.10.10 Steiner 1978 en Lean 4Steiner 1978 in Lean 4

  • Steiner 1978 en Lean 4 (release v1.2, archive Zenodo DOI 10.5281/zenodo.23541611) : formalisation d'un théorème classique de 1978 ; le seul circuit sur les entiers positifs qui soit un cycle de l'application 3x+1 est {1, 2}, démontré ici sous une hypothèse nommée (la borne de Rhin, H_Rhin, jamais un axiome) et sans aucune hypothèse pour au plus 20 000 termes impairs. La formalisation n'apporte rien de nouveau sur les cycles de Collatz. Les énoncés et la preuve ont été écrits sans l'article original (Congr. Numer. 20, 1978) : ils sont reconstruits à partir de Steiner 1981, de la bibliographie annotée de Lagarias et de Simons–de Weger 2005 (lu dans sa version 1.44 de 2010). Après la release v1.2, le 21/10/2026, l'article a été lu sur une copie numérisée et comparé aux énoncés : rien ne change dans les fichiers Lean. 12 énoncés figés, tous prouvés ; axiomes standard seuls ; 0 sorry dans les preuves, 0 native_decide. La borne pour 20 000 termes impairs est bien plus faible que celles qui s'appuient sur une vérification informatique de la conjecture. Proposé sur ccchallenge (« Ready to be audited »).
  • Page Papers : nouvelle carte « Steiner 1978 en Lean 4 », sur le modèle des cartes Halbeisen–Hungerbühler 1997 et Lagarias 1990, avec la réserve que les énoncés et la preuve ont été écrits sans l'article original, lu ensuite et comparé aux énoncés.
  • Carte « Dernier jalon » de l'accueil : elle porte désormais sur Steiner 1978, avec la réserve ; le jalon précédent (la note d'errata, le même jour, avec son DOI) y est rappelé.
  • Carte « Dernière vérification Lean » de l'accueil : elle porte désormais sur les 12 énoncés de Steiner 1978, avec la réserve ; la vérification précédente (revérification de no_cycle_k_le_1322) y est rappelée.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des changements de la v0.10.9, 2026-10-21) y est rappelé.
  • Histoire : l'entrée d'octobre 2026 cite aussi Steiner 1978, avec l'hypothèse nommée H_Rhin, la réserve et son DOI ; son renvoi au changelog devient « v0.10.0 à v0.10.7 et v0.10.10 ».
  • Registre de recherche : un événement daté du 2026-10-21 (publication de la release v1.2), avec la réserve ; 34 événements, dont 25 jalons ; compteurs et données structurées mis à jour. La ligne « Dépôt Lean » de la page du registre cite désormais « les formalisations de Halbeisen–Hungerbühler 1997 et de Lagarias 1990, et celle d'un théorème de Steiner 1978, démontré sous l'hypothèse nommée H_Rhin, jamais un axiome, et reconstruit à partir de comptes rendus publiés, sans l'article original, lu ensuite et comparé aux énoncés », ainsi que l'archive v1.2.
  • Cache des navigateurs : paramètre de version de main.js, de research-ledger.js et des données mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • Steiner 1978 in Lean 4 (release v1.2, Zenodo archive DOI 10.5281/zenodo.23541611): formalisation of a classical theorem from 1978; the only circuit on the positive integers that is a cycle of the 3x+1 map is {1, 2}, here proved under a named hypothesis (Rhin's bound, H_Rhin, never an axiom) and without any hypothesis for at most 20,000 odd terms. The formalisation proves nothing new about Collatz cycles. The statements and the proof were written without the original paper (Congr. Numer. 20, 1978): they are reconstructed from Steiner 1981, Lagarias's annotated bibliography and Simons–de Weger 2005 (read in their version 1.44 of 2010). After release v1.2, on 2026-10-21, the paper was read in a scanned copy and compared with the statements: nothing in the Lean files changes. 12 frozen statements, all proved; standard axioms only; 0 sorry in the proofs, 0 native_decide. The bound for 20,000 odd terms is far weaker than those that rely on a computer verification of the conjecture. Submitted to ccchallenge ("Ready to be audited").
  • Papers page: new card "Steiner 1978 in Lean 4", on the model of the Halbeisen–Hungerbühler 1997 and Lagarias 1990 cards, with the reservation that the statements and the proof were written without the original paper, which was read afterwards and compared with the statements.
  • "Latest milestone" card of the home page: it now refers to Steiner 1978, with the reservation; the previous milestone (the errata note, the same day, with its DOI) is recalled.
  • "Last Lean verification" card of the home page: it now refers to the 12 statements of Steiner 1978, with the reservation; the previous check (re-check of no_cycle_k_le_1322) is recalled.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the changes of v0.10.9, 2026-10-21) is recalled.
  • History: the October 2026 entry also cites Steiner 1978, with the named hypothesis H_Rhin, the reservation and its DOI; its pointer to the changelog becomes "v0.10.0 to v0.10.7 and v0.10.10".
  • Research ledger: one event dated 2026-10-21 (publication of release v1.2), with the reservation; 34 events, of which 25 milestones; counters and structured data updated. The "Lean repository" line of the ledger page now cites "the formalisations of Halbeisen–Hungerbühler 1997 and Lagarias 1990, and that of a theorem of Steiner 1978, proved under the named hypothesis H_Rhin, never an axiom, and reconstructed from published accounts without the original paper, which was read afterwards and compared with the statements", as well as the v1.2 archive.
  • Browser cache: version parameter of main.js, of research-ledger.js and of the data updated.
  • The entries below are kept as they were.

v0.10.9 Revérification de no_cycle_k_le_1322, note d'errataRe-check of no_cycle_k_le_1322, errata note

  • Revérification sous Lean 4.34.0. Les 20 et 21 octobre 2026, les 35 fichiers Lean de la release v1.0 qui forment la clôture des imports de Phase58PorteDeuxFinal.lean (qui contient no_cycle_k_le_1322) ont été revérifiés sous Lean 4.34.0, qui contient la correction de lean4#14576 : ils compilent, et no_cycle_k_le_1322 ne dépend que de propext, Classical.choice et Quot.sound. Phase59 à Phase63 et PhaseVIII, donc no_nontrivial_cycle_phase59, n'ont pas été revérifiés. Détails et limites : recheck-v4.34-2026-10-20. Mis à jour : accueil (bandeau, encadré de l'erratum, résultat principal, carte « Dernière vérification Lean », données structurées), Papers (carte du preprint, dont l'encadré de l'erratum et la lecture du résultat ; elle dit aussi lesquels des sept théorèmes centraux sont revérifiés), Lemmes (introduction, qui le dit aussi ; descriptions de la page ; fiches de no_nontrivial_cycle_phase59 et de no_cycle_k_le_1322), Preuve (descriptions de la page, texte de la vue côte à côte), Histoire, registre (compteur des phases Lean), graphe des dépendances, piste ★ Main et image de partage (régénérée depuis sa source). Restent non revérifiés, entre autres : no_nontrivial_cycle_phase59, no_cycle_k_gt_1322, sdw_from_cf, δ10, δ11 et CGS-7.
  • Note d'errata sur Halbeisen–Hungerbühler 1997 et Lagarias 1990 (Zenodo, 21/10/2026, DOI 10.5281/zenodo.23535498) : 9 et 21 points, chacun vérifié par un théorème Lean ou par un script. Aucun n'invalide un théorème que nous avons formalisé. La liste n'est pas exhaustive. Les deux lignes fausses du tableau 3.1 de Lagarias (k = 35 et k = 73) étaient déjà corrigées dans l'OEIS (A102280, A102284 ; G. H. Morley, 2013). Ajoutée aux cartes HH 1997 et Lagarias 1990 de la page Papers ; elle devient la carte « Dernier jalon » de l'accueil.
  • Page Papers : l'introduction précise qu'un seul article de recherche a été déposé et mentionne la note technique d'errata ; l'introduction de la section « Quelques pistes d'écriture explorées » signale cette note comme exception.
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de cette version ; l'audit précédent (relecture adverse des sept fermetures de la v0.10.8, 2026-10-21) y est rappelé.
  • Registre de recherche : deux événements datés du 2026-10-21 (la revérification et la note d'errata), alors qu'aucun événement ne portait cette date ; 33 événements, dont 24 jalons ; compteurs et données structurées mis à jour.
  • Page du registre : les libellés des cinq compteurs s'affichaient en français et en anglais à la fois ; la règle .stat-label[hidden] n'en affiche plus qu'une langue.
  • Cache des navigateurs : paramètre de version de main.js, de research-ledger.js et de dependency-graph.js, des données et de l'image de partage (og-image.png) mis à jour.
  • Les entrées ci-dessous restent telles quelles.
  • Re-check on Lean 4.34.0. On 20–21 October 2026, the 35 Lean files of release v1.0 that make up the import closure of Phase58PorteDeuxFinal.lean (which contains no_cycle_k_le_1322) were re-checked on Lean 4.34.0, which includes the fix of lean4#14576: they compile, and no_cycle_k_le_1322 depends only on propext, Classical.choice and Quot.sound. Phase59–63 and PhaseVIII, hence no_nontrivial_cycle_phase59, were not re-checked. Details and limits: recheck-v4.34-2026-10-20. Updated: home page (banner, erratum box, main result, "Last Lean verification" card, structured data), Papers (preprint card, including the erratum box and the reading of the result; it also says which of the seven central theorems are re-checked), Lemmes (introduction, which says it too; page descriptions; entries of no_nontrivial_cycle_phase59 and no_cycle_k_le_1322), Proof (page descriptions, text of the side-by-side view), History, research ledger (Lean phases counter), dependency graph, lead ★ Main and sharing image (regenerated from its source). Still not re-checked, among others: no_nontrivial_cycle_phase59, no_cycle_k_gt_1322, sdw_from_cf, δ10, δ11 and CGS-7.
  • Errata note on Halbeisen–Hungerbühler 1997 and Lagarias 1990 (Zenodo, 2026-10-21, DOI 10.5281/zenodo.23535498): 9 and 21 points, each checked by a Lean theorem or by a script. None of them invalidates a theorem that we formalised. The list is not exhaustive. The two wrong rows of Lagarias's Table 3.1 (k = 35 and k = 73) were already corrected in the OEIS (A102280, A102284; G. H. Morley, 2013). Added to the HH 1997 and Lagarias 1990 cards of the Papers page; it becomes the "Latest milestone" card of the home page.
  • Papers page: the introduction says that only one research paper has been deposited and mentions the technical errata note; the introduction of the section "A few writing leads being explored" notes this note as an exception.
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the changes of this version; the previous audit (adversarial review of the seven closures of v0.10.8, 2026-10-21) is recalled.
  • Research ledger: two events dated 2026-10-21 (the re-check and the errata note), whereas no event had that date; 33 events, of which 24 milestones; counters and structured data updated.
  • Ledger page: the labels of the five counters were shown in French and in English at once; the rule .stat-label[hidden] now shows one language only.
  • Browser cache: version parameter of the scripts main.js, research-ledger.js and dependency-graph.js, of the data and of the sharing image (og-image.png) updated.
  • The entries below are kept as they were.

v0.10.8 Fermeture de sept points ouvertsSeven open items closed

  • Tests REQ-MATH-003 et REQ-MATH-004 : les seuils tirés de Salikhov 2007 et de Wu & Wang 2014 sont retirés (erratum de la version Zenodo v4, item 3) ; REQ-MATH-004 est retiré, REQ-MATH-003 porte un avertissement.
  • δ10 retiré (cartographie dépassée) : profils revus contre les sources disponibles (deux faux, un non vérifiable) ; ses conditions (1) et (3) portent sur le remplacement de BakerSeparation, qui n'est pas nécessaire pour le résultat k ≤ 1322 : Hercher 2023, avec la vérification de Bařina, l'implique déjà (erratum, item 4). Mis à jour : carte Papers, registre, pistes δ10 et A, hypothèses H1 et H2, test REQ-MATH-012 (retiré), diagramme, mea culpa #28.
  • « Trilogie d'impossibilité » retirée : voir la ligne de correction ci-dessous.
  • Décomposition Eliahou-Steiner : étude close ; elle ne contenait aucun énoncé d'Eliahou ; la borne d'Eliahou reprise par Halbeisen et Hungerbühler (Théorème 2) est démontrée dans hh1997/. La carte Papers devient « Bibliothèque prototype : minima locaux et blocs » ; son axiome hercher_m_le_91_axiom inverse l'énoncé de Hercher 2023 et n'est utilisé par aucun théorème.
  • Remplacement partiel de l'hypothèse de Baker (Salikhov/Wu) : étude close, cul-de-sac (erratum, items 3 et 4) ; piste E.2 classée cul-de-sac ; page Lemmes (PadeBound.lean) mise à jour.
  • Knight 2026 : lecture close (publication vérifiée ; formalisation d'un tiers « Being formalised » sur ccchallenge) ; piste P9 classée cul-de-sac.
  • Calegari–Dimitrov–Tang 2025 : lecture close, sur le seul résumé ; cul-de-sac en l'état (piste P6). Carte A′ de l'accueil : l'estimation d'avril 2026 (8-12 %) est inchangée, avec une note datée ; note datée aussi sur la frise Histoire.
  • Carte B de l'accueil : « 9 sur 11 » corrigé en « 11 sur 16 culs-de-sac dans la Région II » (chiffre tiré de pistes.json ; l'estimation 5-10 % est inchangée).
  • Carte « Dernier audit » de l'accueil : elle porte désormais sur la relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des sept fermetures de cette version, contre les sources disponibles ; l'audit précédent (relecture adverse de l'erratum, 2026-10-20) y est rappelé.
  • Page Papers, section « Quelques pistes d'écriture explorées » : l'introduction précise que les cartes closes ou retirées restent affichées pour mémoire, chacune avec son statut ; la note finale porte sur les travaux encore ouverts.
  • Registre de recherche : les quatre études ouvertes en avril 2026 sont closes et visibles parmi les jalons ; compteurs mis à jour.
  • L'entrée v0.6.0 est corrigée : la « trilogie d'impossibilité » est retirée ; δ8 et δ8′ reformulent une remarque de Halbeisen et Hungerbühler (Acta Arith. 78 (1997), §5, p. 238), et l'esquisse de preuve du Lemme 5.1 du PDF est retirée (erratum de la version Zenodo v4, item 7) ; δ10 est retiré (cartographie dépassée) : il ne montre pas qu'aucune borne publiée ne remplace la vérification de Bařina.
  • Les entrées ci-dessous restent telles quelles.
  • Tests REQ-MATH-003 and REQ-MATH-004: the thresholds derived from Salikhov 2007 and Wu & Wang 2014 are withdrawn (erratum of the Zenodo v4 version, item 3); REQ-MATH-004 is withdrawn, REQ-MATH-003 carries a warning.
  • δ10 withdrawn (outdated cartography): profiles reviewed against the available sources (two wrong, one cannot be checked); its conditions (1) and (3) concern replacing BakerSeparation, which the k ≤ 1322 result does not need: Hercher 2023 with Bařina's verification already implies it (erratum, item 4). Updated: Papers card, ledger, leads δ10 and A, hypotheses H1 and H2, test REQ-MATH-012 (withdrawn), diagram, mea culpa #28.
  • "Impossibility trilogy" withdrawn: see the correction line below.
  • Eliahou-Steiner decomposition: study closed; it contained no statement of Eliahou's; Eliahou's bound as restated by Halbeisen and Hungerbühler (Theorem 2) is proved in hh1997/. The Papers card becomes "Prototype library: local minima and blocks"; its axiom hercher_m_le_91_axiom reverses Hercher's 2023 statement and is used by no theorem.
  • Partial replacement of the Baker hypothesis (Salikhov/Wu): study closed, dead end (erratum, items 3 and 4); lead E.2 classified as a dead end; Lemmes page (PadeBound.lean) updated.
  • Knight 2026: reading closed (publication checked; third-party formalisation "Being formalised" on ccchallenge); lead P9 classified as a dead end.
  • Calegari–Dimitrov–Tang 2025: reading closed, on the abstract only; dead end as things stand (lead P6). Card A′ of the home page: the April 2026 estimate (8-12%) is unchanged, with a dated note; dated note also on the History timeline.
  • Card B of the home page: "9 of 11" corrected to "11 of 16 dead-ends in Region II" (figure from pistes.json; the 5-10% estimate is unchanged).
  • "Latest audit" card of the home page: it now refers to the internal adversarial review, AI-assisted (not peer review), of the seven closures of this version, against the available sources; the previous audit (adversarial review of the erratum, 2026-10-20) is recalled.
  • Papers page, section "A few writing leads being explored": the introduction states that closed or withdrawn cards are kept for the record, each with its status; the closing note concerns the works still open.
  • Research ledger: the four studies opened in April 2026 are closed and shown among the milestones; counters updated.
  • The v0.6.0 entry is corrected: the "impossibility trilogy" is withdrawn; δ8 and δ8′ restate a remark of Halbeisen and Hungerbühler (Acta Arith. 78 (1997), §5, p. 238), and the proof sketch of Lemma 5.1 of the PDF is withdrawn (erratum of the Zenodo v4 version, item 7); δ10 is withdrawn (outdated cartography): it does not show that no published bound replaces Bařina's verification.
  • The entries below are kept as they were.

v0.10.7 Lagarias 1990 en Lean 4Lagarias 1990 in Lean 4

  • Formalisation d'un classique : J. C. Lagarias, « The set of rational cycles for the 3x+1 problem », Acta Arithmetica 56 (1990), 33-53, en Lean 4.34.0 (Mathlib v4.34.0). Ce n'est pas un résultat nouveau. 60 énoncés, tous prouvés, 0 sorry, 0 native_decide, axiomes standard seuls ; deux théorèmes sous hypothèses nommées (théorème des nombres premiers, Baker–Fel'dman). Dossier lagarias1990/ (e39566c) ; release v1.1, archive Zenodo DOI 10.5281/zenodo.23514572 ; proposé sur ccchallenge.
  • Pages : nouvelle carte sur Papers ; accueil (« Dernier jalon », « Dernière vérification Lean ») ; registre de recherche (nouvel événement) ; Histoire (octobre 2026).
  • Formalisation of a classic: J. C. Lagarias, "The set of rational cycles for the 3x+1 problem", Acta Arithmetica 56 (1990), 33-53, in Lean 4.34.0 (Mathlib v4.34.0). This is not a new result. 60 statements, all proved, 0 sorry, 0 native_decide, standard axioms only; two theorems under named hypotheses (prime number theorem, Baker–Fel'dman). Folder lagarias1990/ (e39566c); release v1.1, Zenodo archive DOI 10.5281/zenodo.23514572; submitted to ccchallenge.
  • Pages: new card on Papers; home page ("Latest milestone", "Last Lean verification"); research ledger (new event); History (October 2026).

v0.10.6 δ11 retiréδ11 withdrawn

  • δ11 retiré (décision du 20 octobre 2026) : le lemme delta11_salikhov_insufficient (Phase 65, k ∈ [3694, 3732], étiquette v0.7.3-delta11) reposait sur la transposition au problème, qui porte sur log₂ 3, de la mesure d'irrationalité de ln 3 de Salikhov 2007, et sur un axiome ad hoc (C_Salikhov < 10^-30) non tiré de l'article. La borne de Salikhov n'étant établie qu'au-delà de hauteurs non explicites, aucun seuil explicite (k ≤ 3693, k ≤ 3732) n'en découle : erratum de la version Zenodo v4, item 3. Note de retrait sur la branche d'étude ; le code reste consultable pour l'historique, mais ne doit plus être cité comme un résultat.
  • Pages : statut « retiré », avec la raison et le lien, sur Papers (carte δ11), Histoire (mai 2026), l'accueil (diagramme, filtre des pistes), dans le catalogue des pistes (E.1, et E.2 qui repose sur la même transposition) et dans le registre de recherche (événement du 08/05 passé à « Retiré », nouvel événement du 20/10). Rien n'est effacé. δ10 n'est pas concerné.
  • Cache des navigateurs : paramètre de version des scripts main.js, research-ledger.js et dependency-graph.js mis à jour, pour que les changements depuis le 2 octobre s'affichent sans vider le cache.
  • Les entrées ci-dessous restent telles quelles ; celles qui présentent δ11 (v0.7.3 et suivantes) sont corrigées par cette ligne.
  • δ11 withdrawn (decision of 20 October 2026): the lemma delta11_salikhov_insufficient (Phase 65, k ∈ [3694, 3732], tag v0.7.3-delta11) rested on the transposition to the problem, which involves log₂ 3, of Salikhov's 2007 irrationality measure of ln 3, and on an ad hoc axiom (C_Salikhov < 10^-30) not taken from the paper. Since Salikhov's bound holds only beyond unspecified heights, no explicit threshold (k ≤ 3693, k ≤ 3732) follows from it: erratum of the Zenodo v4 version, item 3. Withdrawal note on the study branch; the code remains available for the record but must no longer be cited as a result.
  • Pages: status "withdrawn", with the reason and the link, on Papers (δ11 card), History (May 2026), the home page (diagram, approaches filter), in the approaches catalogue (E.1, and E.2, which rests on the same transposition) and in the research ledger (event of 2026-05-08 set to "Withdrawn", new event of 2026-10-20). Nothing is erased. δ10 is not affected.
  • Browser cache: version parameter of the scripts main.js, research-ledger.js and dependency-graph.js updated, so that the changes made since 2 October show without clearing the cache.
  • The entries below are kept as they were; those presenting δ11 (v0.7.3 onwards) are corrected by this line.

v0.10.5 Relecture de toutes les pages : derniers restesAll pages reviewed: remaining fixes

  • FAQ et graphe des dépendances : l'item 1 de l'erratum v4 n'y était pas passé (« équivaut à la conclusion pour k > 1322 »). Même formulation qu'ailleurs : la conclusion elle-même, car en Lean k est un temps de retour quelconque.
  • Papers : « 3 versions » devient « 4 versions » (la v4 du 20/10/2026 conserve le PDF de 39 p. et ajoute ERRATUM.pdf, 2 p.).
  • Registre de recherche : liens vers la v4 du preprint (10.5281/zenodo.23496480), le dépôt Lean et son archive logicielle (10.5281/zenodo.23498096) ; compteur du preprint mis à jour.
  • Retouches : « μ(ln 3) < 5,117 » (Wu & Wang 2014) dans la frise Histoire ; le nœud δ8 du diagramme de l'accueil renvoie à la remarque de Halbeisen–Hungerbühler 1997 (§5).
  • FAQ and dependency graph: item 1 of the v4 erratum had not reached them ("equivalent to the conclusion for k > 1322"). Same wording as elsewhere: the conclusion itself, since in Lean k is any return time.
  • Papers: "3 versions" becomes "4 versions" (v4 of 2026-10-20 keeps the 39-page PDF and adds ERRATUM.pdf, 2 pp.).
  • Research ledger: links to version v4 of the preprint (10.5281/zenodo.23496480), the Lean repository and its software archive (10.5281/zenodo.23498096); preprint counter updated.
  • Small fixes: "μ(ln 3) < 5.117" (Wu & Wang 2014) in the History timeline; the δ8 node of the home diagram points to the remark of Halbeisen–Hungerbühler 1997 (§5).

v0.10.4 Frise et cartes à jour (19-20 octobre 2026)Timeline and cards up to date (19-20 October 2026)

  • Registre de recherche : cinq événements ajoutés (formalisation de Halbeisen–Hungerbühler 1997 ; PR #8 fusionnée ; crédits d'antériorité ; version v4 du preprint avec erratum ; archive logicielle Zenodo), statistiques recalculées. Il s'arrêtait au 2 octobre.
  • Accueil : la carte « Dernier jalon » montre la version v4 avec erratum ; la carte du preprint indique 4 versions (avril–octobre 2026) ; la carte « Dernier audit » montre la relecture adverse de l'erratum (interne, assistée par IA, pas une évaluation par les pairs).
  • Histoire : deux étapes ajoutées à la frise, juillet 2026 (collaboration avec B. Macindoe) et octobre 2026 (Halbeisen–Hungerbühler 1997 en Lean ; version v4 avec erratum).
  • Research ledger: five events added (formalisation of Halbeisen–Hungerbühler 1997; PR #8 merged; prior-literature credits; version v4 of the preprint with erratum; Zenodo software archive), statistics recomputed. It stopped on 2 October.
  • Home page: the "Latest milestone" card shows version v4 with the erratum; the preprint card says 4 versions (April–October 2026); the "Latest audit" card shows the adversarial review of the erratum (internal, AI-assisted, not peer review).
  • History: two steps added to the timeline, July 2026 (collaboration with B. Macindoe) and October 2026 (Halbeisen–Hungerbühler 1997 in Lean; version v4 with erratum).

v0.10.3 Archive Zenodo de la formalisation HH 1997Zenodo archive of the HH 1997 formalisation

  • Archive Zenodo (logiciel) : le dépôt Lean qui contient la formalisation de Halbeisen–Hungerbühler 1997 (dossier hh1997/) est archivé sur Zenodo, release v1.0 : DOI 10.5281/zenodo.23498096 (DOI de concept 10.5281/zenodo.23498095, toutes versions). Lien ajouté sur la page Papers et sur l'accueil.
  • Zenodo archive (software): the Lean repository that contains the formalisation of Halbeisen–Hungerbühler 1997 (folder hh1997/) is archived on Zenodo, release v1.0: DOI 10.5281/zenodo.23498096 (concept DOI 10.5281/zenodo.23498095, all versions). Link added on the Papers page and on the home page.

v0.10.2 Alignement sur la version Zenodo v4 (erratum)Aligned with the Zenodo v4 version (erratum)

  • Zenodo : la version v4 du preprint (20/10/2026, DOI 10.5281/zenodo.23496480) conserve le PDF du 27 avril 2026 et ajoute un erratum de 2 pages. Les phrases « le PDF porte encore l'ancien énoncé » sont remplacées sur toutes les pages.
  • Erratum, item 1 : la formule « sous H2, H3 équivaut à la conclusion pour k > 1322 » (v0.9.0 à v0.10.1) était trop faible. En Lean, k est un temps de retour quelconque, et tout multiple d'un temps de retour en est un (cycle_nSeq_multiples). Sous H2, H3 exclut donc à elle seule tout cycle non trivial, comme ProductBoundThreshold, l'hypothèse du PDF : les deux équivalent à la conclusion. Ce qui est démontré sans circularité ne change pas : aucun cycle non trivial avec k ≤ 1322, sous H1 et H2.
  • Cohérence avec l'erratum v4 : les seuils k ≤ 3693 et k ≤ 3732 sont retirés (item 3) ; pour δ8, la conclusion rejoint une remarque de Halbeisen–Hungerbühler 1997 (§5, p. 238), et l'esquisse de preuve du Lemme 5.1 du PDF est retirée (item 7).
  • Inchangé : la mention « non revérifié depuis » du théorème principal (Lean 4.27.0) ; le bloc sur la collaboration.
  • Les entrées ci-dessous restent telles quelles ; celles de v0.9.0 à v0.10.1 sont corrigées par la deuxième ligne ci-dessus.
  • Zenodo: version v4 of the preprint (2026-10-20, DOI 10.5281/zenodo.23496480) keeps the PDF of 27 April 2026 and adds a 2-page erratum. The sentences "the PDF still carries the old statement" are replaced on every page.
  • Erratum, item 1: the wording "under H2, H3 is equivalent to the conclusion for k > 1322" (v0.9.0 to v0.10.1) was too weak. In Lean, k is any return time, and every multiple of a return time is again one (cycle_nSeq_multiples). Under H2, H3 therefore excludes every non-trivial cycle on its own, as does ProductBoundThreshold, the hypothesis of the PDF: both are equivalent to the conclusion. What is proved without circularity is unchanged: no non-trivial cycle with k ≤ 1322, under H1 and H2.
  • Consistency with the v4 erratum: the thresholds k ≤ 3693 and k ≤ 3732 are withdrawn (item 3); for δ8, the conclusion amounts to a remark of Halbeisen–Hungerbühler 1997 (§5, p. 238), and the proof sketch of Lemma 5.1 in the PDF is withdrawn (item 7).
  • Unchanged: the statement that the main theorem (Lean 4.27.0) has not been re-checked since; the collaboration block.
  • The entries below are kept as they were; those of v0.9.0 to v0.10.1 are corrected by the second line above.

v0.10.1 Corrections : crédit de L-A1, état de la collaborationCorrections: credit for L-A1, state of the collaboration

  • Crédit de L-A1 : l'entrée v0.8.0 ci-dessous présente la récurrence de transport L-A1 comme un « résultat commun » de la collaboration avec B. Macindoe. Ce n'était pas un résultat nouveau : c'est le Lemme 9, éq. (13)-(15), de Halbeisen–Hungerbühler 1997 et le Théorème 1 de Seifert 1988. Ce qui reste à nous : la vérification en Lean. La correction du registre commun est proposée à B. Macindoe (round 20, pull request #10, en cours de revue).
  • Collaboration : compte des pull requests mis à jour sur la page Papers et sur l'accueil (huit fusionnées, la dernière le 19 octobre 2026 ; deux en cours de revue).
  • Dépôt Lean : crédits d'antériorité ajoutés au README (L-A1, L-A4, L-A5, L-A7, L-A8 : section « Prior literature », 7221e7a) ; aucun fichier Lean modifié.
  • Les entrées ci-dessous restent telles quelles ; celle de v0.8.0 est corrigée par la première ligne ci-dessus.
  • Credit for L-A1: the v0.8.0 entry below presents the transport recurrence L-A1 as a "joint result" of the collaboration with B. Macindoe. It was not a new result: it is Lemma 9, eq. (13)-(15), of Halbeisen–Hungerbühler 1997 and Theorem 1 of Seifert 1988. What remains ours: the Lean check. The correction of the shared ledger is proposed to B. Macindoe (round 20, pull request #10, under review).
  • Collaboration: pull-request count updated on the Papers page and on the home page (eight merged, the last on 19 October 2026; two under review).
  • Lean repository: prior-literature credits added to the README (L-A1, L-A4, L-A5, L-A7, L-A8: "Prior literature" section, 7221e7a); no Lean file changed.
  • The entries below are kept as they were; the v0.8.0 entry is corrected by the first line above.

v0.10.0 Halbeisen–Hungerbühler 1997 en Lean 4Halbeisen–Hungerbühler 1997 in Lean 4

  • Formalisation d'un classique : L. Halbeisen et N. Hungerbühler, « Optimal bounds for the length of rational Collatz cycles », Acta Arithmetica 78 (1997), 227-239, en Lean 4.34.0 (Mathlib v4.34.0). Ce n'est pas un résultat nouveau. Tout ce que l'article démontre est vérifié par le noyau, ainsi que la vérification finie de l'exemple du §4.4 (faite en partie, dans l'article, par un calcul approché). 70 énoncés figés avant leur preuve, 0 sorry, 0 native_decide, axiomes standard seuls. Non démontrée : la borne 1/2 de la Remarque 1, que l'article ne démontre pas. Dossier hh1997/ (36d5136) : code, commande de vérification, correspondance ligne à ligne avec l'article, coquilles relevées.
  • Pages : nouvelle carte sur la page Papers ; carte « Dernière vérification Lean » de l'accueil mise à jour.
  • Inchangé : l'erratum du 2 octobre 2026 ; le théorème principal, vérifié sous Lean 4.27.0 et non revérifié depuis.
  • Formalisation of a classic: L. Halbeisen and N. Hungerbühler, "Optimal bounds for the length of rational Collatz cycles", Acta Arithmetica 78 (1997), 227-239, in Lean 4.34.0 (Mathlib v4.34.0). This is not a new result. Everything the paper proves is checked by the kernel, together with the finite verification behind the example of §4.4 (done partly numerically in the paper). 70 statements frozen before their proofs, 0 sorry, 0 native_decide, standard axioms only. Not proved: the 1/2 bound of Remark 1, which the paper does not prove. Folder hh1997/ (36d5136): code, verification command, line-by-line comparison with the paper, typos found.
  • Pages: new card on the Papers page; the home page "Last Lean verification" card updated.
  • Unchanged: the erratum of 2 October 2026; the main theorem, checked on Lean 4.27.0 and not re-checked since.

v0.9.0 Erratum de l'énoncé principal + corrections factuellesErratum to the main statement + factual corrections

  • Erratum (bandeau de l'accueil) : la troisième hypothèse, H3 (DerivedLargeKBound), est supposée, non dérivée ; sous H2, elle équivaut à l'absence de cycle avec k > 1322 (k = nombre de termes impairs du cycle). Seul « aucun cycle non trivial avec k ≤ 1322, sous H1 et H2 » (no_cycle_k_le_1322) est démontré sans circularité. Les versions précédentes présentaient H3 comme une « dérivation projet » : c'était faux. Le PDF déposé sur Zenodo n'est pas encore corrigé (il énonce le théorème avec ProductBoundThreshold, qui pose le même problème).
  • Noyau Lean : mention du bug de noyau lean4#14576 (corrigé en Lean v4.32.2, 28/07/2026). Le théorème principal a été vérifié sous Lean 4.27.0, avant ce correctif, et n'a pas été revérifié depuis. Les six fichiers de la pile commune avec B. Macindoe ont été revérifiés sous Lean 4.34.0 le 23/09/2026 (artefact 9934df4).
  • Corrections factuelles : Christian Hercher (et non « Christoph »), Journal of Integer Sequences 26 (2023), Article 23.3.5 : aucun m-cycle non trivial avec m ≤ 91 ; Salikhov 2007 = mesure d'irrationalité de ln 3, δ11 en réexamen ; la valeur 5,117 est celle de Wu & Wang 2014, pas de Wu 2003 ; chiffres clés sans source retirés de l'accueil ; énoncé de δ8 dans une seule convention ; vraie signature de no_nontrivial_cycle_phase59 et diagramme de la preuve corrigé ; « HYPOTHESES.md §5 » → section H3 ; Gersonide 1342/43 ; « à 100 % » retiré ; statut du papier (soumission au JAR rejetée le 13/05/2026, pas de nouvelle soumission) et compteurs (36 pistes, mea culpa numérotés jusqu'au #32).
  • Autres corrections : licence du paper et du code Lean = CC BY 4.0 (et non MIT) ; page Histoire : théorème de Tao (2019) en densité logarithmique, Crandall 1978 ; titre exact de l'article de Tao (Histoire, FAQ, Syracuse) ; auteur de l'article de Quanta Magazine sur Tao (Kevin Hartnett) ; référence de Knight (Discrete Mathematics 349(3), 2026) ; badge « build vérifié » retiré (il affichait la date d'un ancien commit).
  • DOI : DOI de concept 10.5281/zenodo.19790405 (toutes versions) pour citer le preprint ; v3 du preprint de B. Macindoe (10.5281/zenodo.21730505).
  • Collaboration : lien vers le dépôt public commun one-obstruction-three-faces ; pull requests #6 et #7 (rounds 16 et 17) fusionnées le 02/10/2026 ; B. Macindoe dans la section Équipe, dont les descriptions d'organisation interne sont retirées.
  • Registre de recherche : cinq événements ajoutés (collaboration, revérification Lean 4.34.0, fusion des PR #6 et #7, audit du site, erratum) ; δ11 passe au statut « En cours » (en réexamen) ; statistiques recalculées.
  • Dossier docs/ (notes internes de développement) retiré du site ; image de partage (réseaux sociaux) refaite avec l'énoncé corrigé ; pieds de page en v0.9.0.
  • Les versions v0.7.5 et v0.7.5b (13/05/2026, rectifications sur DerivedLargeKBound) n'avaient pas d'entrée dans ce changelog. Elles remplaçaient la présentation de H3 comme théorème publié de Hercher par « dérivation projet » ; cette présentation est à son tour corrigée par l'erratum (H3 est supposée).
  • Les entrées ci-dessous sont conservées telles quelles. Plusieurs de leurs affirmations sont corrigées par cette version : « 3 hypothèses externes documentées » (H3 est supposée : voir l'erratum) ; « kernel-checked » sans version de Lean ; « 28 pages » ; « trilogie d'impossibilité » (δ8 n'est pas formalisé en Lean ; δ10 porte sur un catalogue fini de quatre sources, pas sur toutes les bornes publiées) ; chiffres attribués à Wu 2003 (k_max = 3732) ; en v0.8.0, Gersonide « 1342 » (1342/43 selon les sources) et le lien Cycles « ajouté à la navigation des 12 pages » (il manquait sur Papers et Pour tous : ajouté en v0.9.0).
  • Erratum (home page banner): the third hypothesis, H3 (DerivedLargeKBound), is assumed, not derived; under H2 it is equivalent to the absence of cycles with k > 1322 (k = number of odd terms of the cycle). Only "no non-trivial cycle with k ≤ 1322, under H1 and H2" (no_cycle_k_le_1322) is proved without circularity. Earlier versions presented H3 as a "project derivation": that was wrong. The PDF deposited on Zenodo is not yet corrected (it states the theorem with ProductBoundThreshold, which has the same problem).
  • Lean kernel: kernel bug lean4#14576 is now mentioned (fixed in Lean v4.32.2, 28 July 2026). The main theorem was checked on Lean 4.27.0, before that fix, and has not been re-checked since. The six files of the stack shared with B. Macindoe were re-checked on Lean 4.34.0 on 23 September 2026 (artifact 9934df4).
  • Factual corrections: Christian Hercher (not "Christoph"), Journal of Integer Sequences 26 (2023), Article 23.3.5: no non-trivial m-cycle with m ≤ 91; Salikhov 2007 = irrationality measure of ln 3, δ11 under re-examination; the value 5.117 is that of Wu & Wang 2014, not Wu 2003; unsourced key figures removed from the home page; δ8 stated in a single convention; true signature of no_nontrivial_cycle_phase59 and corrected proof diagram; "HYPOTHESES.md §5" → section H3; Gersonides 1342/43; "100 %" removed; paper status (JAR submission rejected on 2026-05-13, no new submission) and counters (36 approaches, mea culpa numbered up to #32).
  • Other corrections: license of the paper and the Lean code = CC BY 4.0 (not MIT); History page: Tao's theorem (2019) in logarithmic density, Crandall 1978; exact title of Tao's paper (History, FAQ, Syracuse); author of the Quanta Magazine article on Tao (Kevin Hartnett); Knight reference (Discrete Mathematics 349(3), 2026); "build verified" badge removed (it showed the date of an old commit).
  • DOI: concept DOI 10.5281/zenodo.19790405 (all versions) to cite the preprint; v3 of B. Macindoe's preprint (10.5281/zenodo.21730505).
  • Collaboration: link to the shared public repository one-obstruction-three-faces; pull requests #6 and #7 (rounds 16 and 17) merged on 2026-10-02; B. Macindoe in the Team section, from which descriptions of internal organisation are removed.
  • Research ledger: five events added (collaboration, Lean 4.34.0 re-check, merge of PRs #6 and #7, site audit, erratum); δ11 moved to status "In progress" (under re-examination); statistics recomputed.
  • docs/ folder (internal development notes) removed from the site; social sharing image redone with the corrected statement; footers at v0.9.0.
  • Versions v0.7.5 and v0.7.5b (2026-05-13, rectifications on DerivedLargeKBound) had no entry in this changelog. They replaced the presentation of H3 as Hercher's published theorem with "project derivation"; that presentation is in turn corrected by the erratum (H3 is assumed).
  • The entries below are kept as they were. Several of their claims are corrected by this version: "3 documented external hypotheses" (H3 is assumed: see the erratum); "kernel-checked" without a Lean version; "28 pages"; "impossibility trilogy" (δ8 is not formalized in Lean; δ10 covers a finite catalogue of four sources, not all published bounds); figures attributed to Wu 2003 (k_max = 3732); in v0.8.0, Gersonides "1342" (1342/43 depending on the source) and the Cycles link "added to all 12 page navs" (it was missing on Papers and For everyone: added in v0.9.0).

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 = ∑_{t<k} s_t ≥ k + N. Décomposition en 2 lemmes : cgs7_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 = ∑_{t<k} s_t ≥ k + N. Two-lemma decomposition: cgs7_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