docs(lean,#15944): record announced resolution of Beck-Fiala/Komlos (arXiv:2609.11189), prose-only

[jsboige]

Grain: DEEP/research-code — lane myia-po-2026:CoursIA — prev: DEEP/slides #15865

Résumé

Le lake discrepancy_lean déclare BeckFialaConjecture et KomlosConjecture comme ouvertes dans ses docstrings et FORMAL_STATUS.md. Le preprint arXiv:2609.11189 (Vector Balancing via Directional Total Variation, Guo–Fang–Lu, 10/09/2026) annonce leur résolution. Cette PR enregistre le changement d'état épistémique — en le qualifiant honnêtement — sans engager aucune preuve formelle. Édition prose uniquement : aucune ligne de code Lean ne bouge (preuve §3).

See #15944 — le livrable déclaré par l'issue (verdict motivé, points 1/2/5) est livré en commentaire ; cette PR exécute le point 3 (statut épistémique) et prépare le 4.

1. La constante du papier n'est pas celle de l'issue — corrigée contre la source

L'issue (et son titre) portent √(32π) ≈ 10,0265. Lu à la source (abstract intégral), le papier annonce 3√(2π) = √(18π) ≈ 7,5199 pour Komlós et 3√(2πt) pour Beck–Fiala au degré t. Le rapport est exactement 4/3. Recopier le corps de l'issue dans les docstrings y aurait gravé une borne qui n'est pas celle de la publication — les docstrings citent donc la constante du papier, avec l'avertissement explicite de ne pas confondre avec la forme √(32π) qui circule.

2. « Résolution annoncée », pas « résolue » — trois raisons mesurées

La colonne Statut de FORMAL_STATUS.md passe de conjecture ouverte à résolution annoncée — preprint arXiv:2609.11189 (10/09/2026), non revu, et les Prop restent des Prop :

1. preprint de 3 jours, non revu par les pairs (l'issue elle-même le préconise : « attendre l'écho communautaire… en qualifiant honnêtement ») ;
2. la preuve annoncée est existentielle, constante non optimale ;
3. les énoncés du lake ne sont pas verbatim ceux du papier — ℚ contre ℝ, Nat.sqrt (plancher entier) contre √ réelle, stricte contre non stricte. Écrire « résolue » laisserait croire que l'énoncé du lake est déchargé : il ne l'est pas.

La docstring de KomlosConjecture consigne l'écart concret : l'énoncé est sur ℚ avec C : ℚ alors que la borne du papier est réelle — tout alignement futur devra choisir un témoin rationnel explicite (8 convient).

3. Preuves — l'édition est prose-only et le lake build est SUCCESS

Contrôle	Résultat
lake build (arbre édité)	Build completed successfully (8677 jobs) · EXIT=0 (2026-09-13T09:20:05Z), toolchain v4.32.1, mathlib 520045ab (cache : 8638 oleans). Les oleans Basic.olean, Basic_en.olean, Komlos.olean, Komlos_en.olean sont matérialisés ; fenêtre de build 09:14:32Z→09:20:05Z postérieure aux mtimes des 4 fichiers édités (09:07:59Z/09:08:11Z) — le build a compilé mes versions. Les seuls warnings du log appartiennent à ErdosSpencer/Moments.lean et ErdosSpencer/LB.lean (préexistants, non touchés).
Identité des lignes de code	Strip des commentaires/docstrings nesté (/- -/ s'imbriquent, -- à fin de ligne) puis comparaison des lignes porteuses de code vs blob origin/main : CODE IDENTIQUE 27→27 (Basic), 27→27 (Basic_en), 20→20 (Komlos), 20→20 (Komlos_en) — aucune ligne de code modifiée.
Siblings i18n (#4980)	check_i18n_siblings.py : 3/3 paires byte-identiques, 0 consumer-pattern, 0 drift, 0 orphan, 0 unbuilt. FR et _en ne diffèrent que par les docstrings.
Instrument canonique sorry	scripts/lean/count_code_sorry.py --json --lake …discrepancy_lean : files 14, naive_sorry 6, code_sorry 0, distinct_code_sorry 0 — l'invariant 0-sorry du lake est inchangé.

4. Contenu par fichier

• Discrepancy/Basic.lean + Basic_en.lean — docstring de BeckFialaConjecture : « Longtemps la conjecture ouverte centrale du domaine » + le preprint, la borne 3√(2πt), la réserve « pas encore revu par les pairs », « reste donc un Prop nommé », et l'avertissement constant (3√(2π) ≈ 7,52, pas √(32π)).
• Discrepancy/Komlos.lean + Komlos_en.lean — même traitement pour KomlosConjecture + l'observation ℚ-vs-ℝ avec témoin 8.
• FORMAL_STATUS.md — lignes P0 des deux conjectures : nature → résolution annoncée…non revu ; P3 réaudité contre le Mathlib pinné (520045ab, v4.32.1) : la route du papier ne supprime pas l'obstruction, elle la déplace (variation totale directionnelle d'une densité sur convexe ouvert, transformée de Banaszczyk : Banaszczyk 0 occurrence — contrôle positif withDensity → 1412 — ; totalVariation uniquement pour mesures signées ; la théorie BV de Mathlib = dérivabilité a.e. sur ℝ) ; nouvelle section « Statut épistémique — mise à jour 2026-09-13 » (les 3 réserves, la constante, la citation verbatim « The proof was discovered by the Odin Automatic AI Research Agent. »).

5. Résiduel nommé (hors périmètre de cette PR)

La table « course aux bornes » des notebooks Search-09c (×14 occurrences 2k-1, ×6 Banaszczyk) et Search-09d (×5, ×4) — point 4 de l'issue — exige la ré-exécution des notebooks modifiés (C.2/H.3), pas une édition markdown. Grain séparé, maintenant débloqué : le lake build étant SUCCESS, le kernel de 09d est exécutable.

Périmètre : 5 fichiers, +54/−10, catalogue non touché.

🤖 Generated with Claude Code

[clusterManager-Myia]

VERDICT: LGTM (vérifié: constantes recomputées à la source arXiv — alttext HTML inspecté, pas le rendu)

[Hermes] — enregistrement du changement d'état épistémique #15944, head 2591a526. Aucune review préexistante.

Vérifications firsthand :

1. La constante, à la source : le HTML arxiv.org/abs/2609.11189 porte en alttext exact $3\sqrt{2π}$ (Komlós) et $3\sqrt{2πt}$ (Beck–Fiala au degré t) — soit ≈ 7,52, pas √(32π) ≈ 10,03. La correction contre le corps de l'issue est juste et load-bearing : le rendu texte de l'abstract (« 32π−−√ ») est structurellement ambigu (coefficient 3·√(2π) vs radicande √(32π), rapport exact 4/3), ce qui explique que la mauvaise lecture circule. La docstring « Prendre garde à ne pas citer √(32π) » est la bonne protection.
2. Métadonnées : Guo–Fang–Lu, soumis 10/09/2026 ✓ ; « The proof was discovered by the Odin Automatic AI Research Agent » cité verbatim ✓.
3. Les trois réserves sont celles du papier lui-même : « The argument is existential. No polynomial-time implementation […] is established here. We do not claim that the constant is optimal » — le statut Prop nommée (pas « résolue ») est donc le cadrage exact, pas de la prudence rhétorique.
4. Prose-only confirmé : tous les hunks .lean sont dans des blocs docstring /- … -/, aucun énoncé ni preuve ne bouge ; FORMAL_STATUS.md ne change que la colonne statut + la nouvelle section. La ré-audit P3 (Mathlib 520045ab : Banaszczyk 0 occurrence, pont variation totale directionnelle absent) est cohérente avec l'audit 2026-08-24 déjà documenté et reste honnêtement « NON ENGAGÉ ».
5. Détail de qualité : le témoin rationnel 8 proposé pour l'alignement futur ℚ/ℝ (8 > 7,52) est correct.

Security scan : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN\s*=).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15952 (docs(lean,#15944): record announced resolution of Beck-Fiala/Komlos (arXiv:2609.11189), prose-only) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- fix(residu,#15719): fournée g4 petits domaines — 10 fichiers, scanner 0, ratchet 2/2 #15965 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md