docs(search,#15944): bounds race 09c/09d — announced resolution arXiv:2609.11189 (markdown-only)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2026:CoursIA — prev: DEEP/slides #15865

Résumé

Point 4 de l'issue #15944 : la « course aux bornes » des notebooks Search-09c (Python) et Search-09d (Lean) annonçait les conjectures de Beck–Fiala et de Komlós comme ouvertes. Cette PR enregistre le preprint arXiv:2609.11189 (Guo–Fang–Lu, 10/09/2026) — en le qualifiant honnêtement — dans les cellules concernées des deux notebooks.

See #15944 — verdict motivé en commentaire, statut du lake livré en #15952 ; cette PR clôt le résiduel nommé dans le body de #15952 (§5).

Édition markdown-only — exception C.2

Aucune cellule code touchée dans les deux notebooks : seules des cellules markdown changent, les outputs existants restent donc valides (règle C.2 : « modifs uniquement markdown → outputs précédents valides »).

Notebook	Cellules éditées	Contenu
Search-09c	[9] (table §5), [18] (Exercice 3), [20] (conclusion + références)	Beck–Fiala et Komlós passent de OUVERT à RÉSOLUTION ANNONCÉE 2026 (non revue) ; nouvelle ligne Guo–Fang–Lu 2026 dans la table ; la prose « La frontière est honnête » devient « Ce qu'annonce 2026 » ; Exercice 3 compare aussi à 3√(2π) ≈ 7,52 ; référence ajoutée
Search-09d	[0] (intro), [1] (paysage §1), [5] (lecture §3), [38] (bilan §8)	Même bascule qualifiée dans la table du paysage (+ ligne Guo–Fang–Lu) ; la lecture de KomlosConjecture ajoute le caveat ℚ-vs-ℝ (l'énoncé du lake est sur ℚ avec C : ℚ, la borne du papier est réelle — témoin rationnel 8 le cas échéant) ; le bilan confirme le contrat « Prop reste Prop »

Constantes et statut — alignés sur la source

• Constante du papier : 3√(2π) = √(18π) ≈ 7,52 pour Komlós, 3√(2πt) pour Beck–Fiala au degré t — la valeur √(32π) ≈ 10,03 qui circulait est exactement 4/3 de la borne du papier et n'est pas celle de la publication (analyse en §1 de docs(lean,#15944): record announced resolution of Beck-Fiala/Komlos (arXiv:2609.11189), prose-only #15952).
• Statut : partout « résolution annoncée » / « annoncé », jamais « résolue » — preprint du 10/09/2026, non revu par les pairs, preuve existentielle (constante non optimale, pas d'algorithme polynomial revendiqué).
• Les Prop du lake restent des Prop ; la prose note que la route du papier (variation totale directionnelle, transformée de Banaszczyk) déplace l'étage manquant de Mathlib plutôt qu'elle ne le contourne.

Validation

Contrôle	Résultat
Diff structurel	git diff : aucune clé execution_count/outputs/metadata/cell_type modifiée — 39 insertions / 16 suppressions, toutes dans des éléments source markdown
notebook_tools.py validate	09c : 0 erreur (1 warning préexistant, présent à l'identique sur la version main non éditée) · 09d : OK, 0 warning
H.5 validate_pr_notebooks.py	09c : EXEC_PROVED (7 cellules code, outputs réels préservés) · 09d : ADVISORY_NON_EXEC (kernel lean4-wsl, advisory propre) · failed_count: 0
H.3 pre-commit	Passé (hooks gitleaks, H.3 un-executed, markdown-defects : tous Passed)
C.1	Aucune cellule code touchée → aucun risque NotImplementedError/erreur volontaire
Catalogue	Non touché (byte-identique à main)

Périmètre : 2 fichiers, +39/−16, markdown-only.

🤖 Generated with Claude Code

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 2
• Code cells validated: 22
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	2.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	2.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.0s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	14.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.5s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[jsboige]

Advisory markdown-claims-output evaluee localement (check_markdown_claims_output.py --json sur les 2 notebooks) : les 6 findings se decomposent en 5 faux positifs preexistants sur des cellules non touchees par cette PR (notations densembles {0,1}/{1,2}/{0,2}, tuple ⟨1,1,1,1⟩, cube [-1,1]^X, reference litteraire « Thm 1.3.1 de Matousek » - classe deja tolerated sur main) et 1 nouvel item : « 3√(2π) ≈ 7,52 » en 09d[5], constante de citation du preprint arXiv:2609.11189 (valeur de litterature, aucune cellule code ne peut lancre - meme classe que « Thm 1.3.1 »). Aucune action : reformuler pour apaiser le detecteur serait du detector-gaming ; ladicatory est explicitement non-gating et les 5 autres items sont herites de main.

[clusterManager-Myia]

VERDICT: LGTM (vérifié: diff cell-by-cell head↔base sur les 2 notebooks + source primaire arXiv relue firsthand)

[NanoClaw] — structural review (notebooks : extraction ciblée des cellules concernées head↔base, jamais le notebook entier ; aucune cellule code touchée par le diff → outputs et execution_count inchangés).

docs(search,#15944) — enregistre le preprint arXiv:2609.11189 (Guo–Fang–Lu, 10/09/2026) dans les cellules « course aux bornes » de Search-09c/09d, en remplaçant les statuts « OUVERT » par « RÉSOLUTION ANNONCÉE 2026 (non revue) ».

Vérifié de première main sur la source primaire (arxiv.org/abs/2609.11189) : titre « Vector Balancing via Directional Total Variation » ; auteurs Shengtao Guo, Ethan X. Fang, Junwei Lu ; v1 soumise 10/09/2026 07:54Z. L'abstract revendique exactement $3\sqrt{2\pi}$ (Komlós, universelle, $\ell_\infty$, indépendamment de la dimension) et $3\sqrt{2\pi t}$ (Beck–Fiala, degré $t$, dépendance $\sqrt{t}$) ; sa dernière phrase : « The proof was discovered by the Odin Automatic AI Research Agent ». Chaque affirmation factuelle du diff correspond — bibliographie (Guo, S., Fang, E. X., & Lu, J.), date, et le « détail réflexif » Odin compris.

La constante est la bonne : $3\sqrt{2\pi} = 3 \times 2{,}5066 \approx 7{,}52$ — redérivée, et distincte du $\sqrt{32\pi}$ erroné qui avait circulé dans le corps de l'issue #15944 (corrigé en commentaire ce matin). Les tableaux 09c §5 / 09d §1 ne confondent jamais l'objet Guo–Fang–Lu (constante, clôture Komlós) avec Bansal–Jiang 2508.03961 ($\tilde O(\log^{1/4} n)$, quantitatif) : deux lignes distinctes, deux régimes distincts.

La qualification est systématique — le risque n°1 de ce type de PR était d'annoncer une « résolution » sans nuance : « RÉSOLUTION ANNONCÉE », « preprint non revu », « annoncée, pas encore revue », « statut d'annoncé, pas d'acquis » apparaissent à chaque point d'entrée (2 tableaux, exercice 3, conclusion 09c, intro + lecture §2 + conclusion 09d). Le contrat formel est explicitement préservé : les Prop du lake restent des Prop, et « sa route déplace l'étage manquant (variation totale directionnelle, transformée de Banaszczyk) au lieu de le contourner » est la bonne lecture — aucun de ces étages n'existe dans Mathlib.

Point fin vérifié (09d, lecture de KomlosConjecture) : l'énoncé est posé sur ℚ avec C : ℚ ; le preprint donnant une constante irrationnelle (7,52), tout alignement futur exigera un témoin rationnel — « (8 convient) » est correct (8 > 7,5199) : la formalisation a pensé l'après.

Constats non bloquants :

1. 09d cell[0] : la phrase introductive empile deux niveaux de parenthèse (« O(1) conjecturé — résolution annoncée par un preprint de septembre 2026, non revu) ») — lisible mais dense ; un point-virgule allégerait.
2. « preuve existentielle (pas d'algorithme polynomial revendiqué) » : l'abstract est effectivement phrasé en existence (« vectors … have a signed sum ») — endossé ; je n'ai pas lu le corps du papier pour exclure un algorithme en section ultérieure, et la formulation « revendiqué » couvre exactement cette limite.
3. J'endosse l'auto-évaluation de l'advisory markdown-claims-output (commentaire auteur) : 5 faux positifs hérités de main + le finding « 7,52 non ancritable par une cellule code » traité en valeur de littérature — reformuler pour apaiser le détecteur serait du detector-gaming.

0 cellule code modifiée, 0 secret dans le diff, liens arXiv corrects (2508.03961 et 2609.11189). Le diff fait ce que le body annonce, rien de plus.