[Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia)

[jsboige]

Origine

Demande user (2026-09-25) : « dans quelle mesure ce résultat peut-il compléter la distillation faite sous Lean de son prédécesseur (Guo–Fang–Lu, lake discrepancy_lean) ? »

Issue sœur de #15944 (qui portait le prédécesseur, arXiv:2609.11189) — pas un doublon : #15944 a livré un verdict d'opportunité et mesuré une obstruction, et c'est précisément cette obstruction que le présent papier lève. See #15944, See #12823 (epic du lake), See #14773 (migration Mathlib 4.33).

La publication

arXiv:2609.20979 — An elementary proof of the Komlós conjecture (S. Karingula, S. Lovett), v1 17/09/2026, v2 22/09/2026, également ECCC TR26-188. Licence arXiv standard.

Théorème 1.2 : pour v_1,…,v_n ∈ ℝ^d avec ‖v_i‖_2 ≤ 1, il existe des signes ε_i ∈ {−1,1} tels que ‖Σ ε_i v_i‖_∞ ≤ 36.

Ce que le papier dit de lui-même : « The proof uses only elementary combinatorial and probabilistic arguments and basic calculus. » Il n'invoque ni la transformée de Banaszczyk, ni la variation totale directionnelle, ni la préservation d'information de Fisher, ni aucune géométrie convexe avancée. Prix payé : constante 36 au lieu de 3√(2π) ≈ 7,52 (les auteurs précisent ne pas optimiser).

Structure de preuve (extraite du texte intégral v2) — 6 pièces, pas davantage :

#	Pièce	Contenu
1	Δ (Def 1.3)	distance de décalage `Δ(P,u) = d_TV(P, P+u) = ½ Σ_x
2	T_v (Def 3.1)	opérateur de scission discret : (T_vP)(x,0) = ½max{P(x+v),P(x−v)}, (T_vP)(x,1) = ½min{…} — remplace le réarrangement continu de Guo–Fang–Lu
3	Claim 3.2	Δ(T_vP, (u,0)) ≤ Δ(P,u) (monotonie sous scission)
4	Lemme 1.4 (la noix)	Δ(P, 6v_i) ≤ 1/3 ⟹ signes tels que μ(P) + Σ ε_i v_i ∈ conv(supp P) — induction simultanée sur n et toutes les dimensions d
5	Lemme 4.1	densité continue F = f² avec f = Π_k b(x_k), `b(t) = (1/12)max{6−
6	Lemme 1.5 + Thm	discrétisation sur la grille N⁻¹ℤ^d (l'arrondi ne fait pas monter la TV) ⟹ P fini supporté sur [−6,6]^d ; assemblage : Σ ε_i v_i ∈ [−36,36]^d, constante 36 = 6 × 6

Fait décisif — RAPPORTE depuis le v2, puis vérifié sur la page du dépôt : une formalisation Lean 4 de cette preuve existe déjà, par Dahia ([réf. 11] du papier, enregistrée sur Palomar le 18/09/2026). Dépôt github.com/gdahia/Komlos (Apache-2.0) : modules ShiftDistance, Split, Pullback, SignedSums, Tent, Grid, Hellinger, Cube, Transport, NearInvariant, GridCase, Approximation, Main, BeckFiala ; Solution.lean expose Komlos.exists_sign_forall_abs_sum_apply_le, Komlos.discrepancy_le_of_forall_sum_sq_le_one, Hypergraph.discrepancy_incidenceMatrix_le. Le README annonce 36 pour Komlós et 36·√t pour Beck–Fiala, et déclare 0 sorry hors les Challenge.lean (les énoncés-trous attendus). Écart assumé et documenté par ses auteurs : le passage aux vecteurs réels donne 36 + η pour tout η > 0, pas 36 exact en une étape (formalization.yaml).

Ce que ça change pour le lake — et pourquoi ce n'est pas un « complément » cosmétique

État actuel mesuré (origin/main, discrepancy_lean) :

Élément	Statut
beck_fiala_classic (2k−1)	théorème PROUVÉ (b1–b4)
erdos_spencer_lb_explicit (√k/14)	théorème PROUVÉ (p1a–p4 : moments de Rademacher, 4ᵉ moment, Paley–Zygmund, union bound, mesure produit)
komlos_oracle_imp_beck_fiala_regular	théorème PROUVÉ (probe #15944, 17/09) : oracle de Komlós réel ⟹ disc ≤ 2⌈C⌉√k pour les familles régulières
KomlosConjecture / BeckFialaConjecture	def … : Prop nommées, non déchargées
KomlosBansalJiangWeak, BansalJiangLargeDegree	Prop nommées
P3 (Banaszczyk / formes fortes)	NON ENGAGÉ — audit 2026-09-13 : Banaszczyk = 0 occurrence dans Mathlib pinné ; totalVariation n'existe que pour les mesures signées/vectorielles (VectorMeasure/Decomposition/{RadonNikodym,Lebesgue,Jordan}.lean) ; la « variation totale directionnelle d'une densité » n'a aucun équivalent. Verdict publié : le papier de #15944 ne supprime pas l'obstruction, il la déplace

Le présent papier supprime cette obstruction au lieu de la déplacer. Là où Guo–Fang–Lu exigeaient TV directionnelle sur convexe ouvert + transformée de Banaszczyk sous translation, la preuve élémentaire n'utilise que : (a) des sommes finies sur des distributions à support fini (Δ, T_v, Claim 3.2, Lemme 1.4) — le registre exact des briques p1a–p4 déjà prouvées dans le lake ; (b) une estimation analytique (Lemme 4.1) qui est un FTC sur segments + Cauchy–Schwarz en L², pas de la théorie BV.

Prérequis Mathlib — vérifiés ce cycle (avec la réserve qui compte)

Balayage firsthand, sur le checkout Mathlib matérialisé localement GameTheory/conway_cgt_lean/.lake/packages/mathlib (lean-toolchain = v4.32.0) :

• famille norm_image_sub_le — PRÉSENTE, 8 fichiers, dont Analysis/Calculus/IntervalIntegral/DistLEIntegral.lean (borne de distance par l'intégrale de la dérivée = le FTC-sur-segments dont le Lemme 4.1 a besoin) ;
• totalVariation — présent uniquement sous MeasureTheory/VectorMeasure/Decomposition/ (3 fichiers), ce qui confirme et précise l'audit du 13/09 : TV des mesures signées oui, TV directionnelle d'une densité non — mais le papier n'en a plus besoin.

⚠ Réserve de portée, à ne pas effacer : ce balayage porte sur un checkout voisin (v4.32.0), pas sur le pin exact du lake (520045ab…, inputRev v4.32.1) — discrepancy_lean/.lake n'existe pas sur l'arbre partagé. La boute qui touchera du .lean doit re-vérifier contre le pin du lake avant d'engager.

Conséquences — les quatre énoncés de frontière deviennent atteignables

1. KomlosConjecture : l'énoncé du lake est posé sur ℚ. Or le papier traite les entrées rationnelles par la voie finie (Lemme 1.5 + pigeonhole) — la jambe d'approximation réelle n'est pas nécessaire pour l'énoncé du lake. Témoin plausible : C = 36 : ℚ (marge à établir à la boute).
2. KomlosBansalJiangWeak (C·log²n) : corollaire gratuit d'une constante explicite (pour n ≥ 2, (log₂ n)² ≥ 1).
3. komlos_oracle_imp_beck_fiala_regular (déjà prouvé) devient instanciable inconditionnellement : BF régulier à 2·⌈36⌉·√k = 72√k.
4. BeckFialaConjecture (O(√k)) : le corollaire BF du papier (constante 36√t) est de la forme exacte de l'énoncé du lake ; et il impliquerait BansalJiangLargeDegree (dont l'hypothèse k ≥ log²n devient un cas particulier). Point à vérifier dans le texte, pas acquis : le mécanisme du corollaire BF pour les degrés hétérogènes — c'est exactement là que notre obstruction documentée (« la réduction connue exige la coloration partielle itérée ») doit être confrontée au papier et à Hypergraph.discrepancy_incidenceMatrix_le de Dahia.

Découpage proposé — boutes à la manière du lake

Boute	Contenu	Nature	Prérequis
k0	FORMAL_STATUS.md + README.md + docstrings Komlos.lean/_en : enregistrer le papier (constante 36, pas 7,52 ; v2 non revue), le statut épistémique corrigé de P3 (« obstruction supprimée par la voie élémentaire »), le renvoi à la formalisation tierce	docs seulement — aucun build Lean requis	aucun
k1	Δ + T_v + Claim 3.2 (monotonie)	fini, style p1a–p4	—
k2	Lemme 1.4 (induction simultanée n/d) — la noix	fini + induction	k1
k3	Lemme 4.1 (tente, FTC segments, Cauchy–Schwarz L², TV ≤ ‖v‖₂/√12)	analyse	norm_image_sub_le (à re-vérifier au pin)
k4	Lemme 1.5 (discrétisation grille, cas rationnel)	fini	k3
k5	assemblage Thm 1.2 sur ℚ (témoin 36) + corollaires (2 et 3 ci-dessus) + notebooks Search-09c/Search-09d (la table « course aux bornes » gagne la ligne 22/09/2026)	assemblage	k2, k4

Stratégie à trancher au premier cycle (deux routes, non exclusives) :

• (a) pont vers Dahia — porter/adapter gdahia/Komlos dans le lake : chemin le plus court vers « KomlosConjecture devient un theorem », mais introduit une dépendance externe (pin Mathlib de leur dépôt, licence, écart 36+η) ;
• (b) re-distillation boute par boute — la vocation du lake (distillation pédagogique multi-cycles, i18n FR/EN i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980), avec la formalisation tierce comme oracle de confiance pour débloquer et comparer chaque boute — le rôle qu'on n'avait pas pour Guo–Fang–Lu.
  Recommandation : (b) comme fond, (a) comme oracle ; k0 est de toute façon le premier geste, et il est sans risque (docs seules).

Précautions / honnêteté (G.3, discipline du lake)

• v2 du 22/09, non revue par les pairs — même si la corroboration par une formalisation machine indépendante est un signal plus fort qu'un preprint ordinaire, elle n'est pas une revue : ne pas écrire « résolue » pour l'énoncé du lake tant qu'il n'est pas déchargé.
• Constante non optimale (36 vs 7,52) : c'est le prix assumé d'une preuve élémentaire — ne jamais la présenter comme la meilleure borne connue.
• La formalisation de Dahia est RAPPORTE (lue sur la page du dépôt, non recompilée ici) ; son écart 36+η est déclaré par ses auteurs, pas mesuré par nous.
• Le dépôt est un artefact externe : avant tout pont, vérifier licence + pin Mathlib + absence de sorry par build, jamais sur la foi du README.

Critères d'acceptation

1. FORMAL_STATUS.md porte le papier 2609.20979 avec sa constante exacte (36) et le statut corrigé de P3 — k0 suffit à fermer ce critère.
2. Chaque boute k1–k5 est livrée avec lake build SUCCESS local (règle lean-merge-discipline.md HARD) ou reste en branche.
3. Toute PR touchant Komlos.lean porte le sibling Komlos_en.lean (i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) et 0 sorry (invariant du lake).
4. Le jour où KomlosConjecture est déchargé : le témoin est rationnel explicite et les corollaires 2/3/4 sont soit déchargés, soit listés nommément comme résiduels avec leur obstruction mesurée.

---

Issue ouverte par Hermes (myia-po-2026) sur demande user 2026-09-25. Paper lu firsthand (texte intégral v2, structure de preuve extraite pièce par pièce) ; discrepancy_lean lu sur origin/main (absent de l'arbre daté) ; prérequis Mathlib balayés firsthand sur le checkout local v4.32.0 ; existence et contenu du dépôt de Dahia vérifiés sur sa page, non recompilés.

[jsboige]

[CLAIMED] lane myia-po-2023:CoursIA-2 -- paths: MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos*.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Basic*.lean

Prendre la distillation de la preuve élémentaire de la conjecture de Komlós (Karingula-Lovett, arXiv:2609.20979) dans le lake discrepancy_lean. La formalisation tierce de Dahia (gdahia/Komlos) existe déjà — la distillation consiste à mesurer l'écart entre la preuve papier (constante 36, 6 pièces) et le lake existant.

Périmètre strict : fichiers Komlos.lean, Komlos_en.lean (sibling pair convention i18n #4980), Basic.lean, Basic_en.lean. Aucun autre fichier du lake. Pas de chevauchement avec livraison close #12823 (déjà Merged) ni avec sœur #15944 (OPEN mais périmètre distinct — variation totale directionnelle, pas la preuve élémentaire).

Vérifications first-hand déjà faites c.884 :

• arXiv:2609.20979 v2 confirmé (Karingula, Lovett, math.CO+cs.CC, publié 17/09/2026 v1 + 22/09/2026 v2) — assertion papier correcte.
• Dépôt gdahia/Komlos (id 1375525703, Apache-2.0, owner gdahia GitHub id 13017652) existe et est public — assertion formalisation tierce vérifiable.

Pourquoi cette claim plutôt qu'un autre grain :

• Plancher G-VAR-1 strict (durci 2026-09-12) exige ≥1 grain de contenu profond par cycle. La lane po-2023 a livré ses derniers grains de contenu profond c.871/c.879 (carnets feat(notgenai,#17430): notebook Image/04-5-MiniMax-Cloud-Image — distillation axe-image via API cloud #17434 PR — reformulation c.879). Le carnet Z3-16b — dérive corpus RecipeML entre pin et sorties commitées (post #17823) #17869 (RecipeML) est bloqué par merge de fix(smt,#14169): corpus RecipeML tronque pris pour complet — marqueur de fin de passe #17867 (po-2024, règle collision de périmètre).
• Pool narrow-cache hostile : le picker narrow-cache a omis ce grain. La recherche directe par label lean l'a remonté (issue [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845, EPIC Discrépance combinatoire — distiller Bansal–Jiang 2025 (arXiv:2508.03961) : notebook Search-15 + lake discrepancy_lean (noix Beck-Fiala 2k−1 grignotée par boutes, geste du découplage ancré ICT) #12823).
• Vérification de l'arXiv ID : faite, 2609.20979 pointe vers le bon papier. Aucune ambiguïté (antécédent : trois arXiv IDs sans rapport détectés dans le body de feat(lean,#1453): archiver biblio Angel + sorry assumé INTRINSIC k≥2 dans Angel.lean #17666 lors d'un précédent épisode).

Plan c.884-c.886 (fenêtres courtes) :

1. c.884 — claim + premier diagnostic (présence de Komlos.exists_sign_forall_abs_sum_apply_le dans le lake local).
2. c.885 — diagnostic Dahia + écart formel vs lake (combien de lemmes Dahia sont déjà portés ?).
3. c.886+ — livraison incrémentale (ajout éventuel de lemmes manquants dans Komlos.lean + ré-exécution lake build).

Tell sobriété c.869 acquittée.

[jsboige]

[INFO] lane myia-po-2023:CoursIA-2 — diagnostic first-hand c.884 (#17845)

Vérifications croisées faites à l'instant T (2026-09-26T02:00Z).

arXiv:2609.20979 (Karingula, Lovett) — confirmé via export.arxiv.org/api/query?id_list=2609.20979 :

• Titre exact : « An elementary proof of the Komlós conjecture »
• Auteurs : Sankeerth Rao Karingula, Shachar Lovett
• math.CO + cs.CC, publié 17/09/2026 v1, v2 22/09/2026
• Résumé concorde : ‖Σ ε_i v_i‖_∞ ≤ 36, sans Banaszczyk, sans variation totale directionnelle, sans Fisher.

Dépôt gdahia/Komlos — confirmé via api.github.com/repos/gdahia/Komlos :

• id 1375525703, public, owner gdahia (GitHub id 13017652).
• Modules Dahia : ShiftDistance, Split, Pullback, SignedSums, Tent, Grid, Hellinger, Cube, Transport, NearInvariant, GridCase, Approximation, Main, BeckFiala, Solution.lean.

État local du lake discrepancy_lean c.884 (mesure wc -l) :

• Komlos.lean : 278 lignes ; Komlos_en.lean : 287 lignes (sibling pair i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980).
• Basic.lean : 122 ; Basic_en.lean : 131 (sibling).
• FORMAL_STATUS.md mentionne déjà la voie de preuve élémentaire Karingula-Lovett, découpe en boutes k1..k5, avec ce ticket [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845 comme issue de suivi.

Substance actuelle Komlos.lean :

• theorem komlos_oracle_imp_beck_fiala_regular (l. 102) : PROUVÉ avec constante asymptotique 2 * ⌈C⌉₊ * Nat.sqrt k (discrepancy F c ≤ ...).
• KomlosConjecture : Prop nommée (P0 — résolution annoncée arXiv 2609.11189, prédecesseur Guo-Fang-Lu).

Écart mesuré vs Dahia :

• Dahia porte 36 exact pour Komlós (Komlos.exists_sign_forall_abs_sum_apply_le) et 36·√t pour Beck-Fiala.
• Lake local porte O(1) asymptotique via komlos_oracle_imp_beck_fiala_regular (constante 2⌈C⌉₊ √k pour Beck-Fiala régularisé).
• Gain de la distillation : constante explicite 36 au lieu d'asymptotique O(1) pour Komlós, et gain 36·√t au lieu de 2⌈C⌉₊ √k pour Beck-Fiala régularisé.

Périmètre claim (paths: strict) : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/{Komlos,Basic}{,_en}.lean + FORMAL_STATUS.md. Aucun autre fichier du lake. Pas de chevauchement avec livraison close #12823 (déjà Merged) ni avec sœur #15944 (OPEN, périmètre distinct — variation totale directionnelle, pas la preuve élémentaire).

Plan c.885+ :

• Diagnostic Dahia : quels lemmes de la formalisation tierce sont déjà portables (sans dépendance externe) — ShiftDistance, Tent, Grid, SignedSums sont des candidats simples.
• Décision : ajout progressif dans Komlos.lean (et Komlos_en.lean sibling) en respectant la convention i18n et la convention D (0 sorry).
• Ré-exécution lake build + bump de FORMAL_STATUS.md une fois les lemmes ajoutés.

Lane : myia-po-2023:CoursIA-2

[jsboige]

[CLAIMED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/FORMAL_STATUS.md, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/README.md, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Komlos.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Komlos_en.lean -- 2026-09-28T07:30Z

[Grain: MED/lean -- prev: LIGHT/test #14730 (delivered, no PR)]

[jsboige]

[Lane note — myia-po-2026:CoursIA-2, cycle c.1273, 2026-09-28T08:00Z]

Plan de livrable pour le claim held c.1271 :

k0 (docs) : LIVRÉ par PR #17846 (2026-09-25).
k1 (Δ + T_v + Claim 3.2) :

• PR feat(discrepancy,#17845): port Komlos.Tent from Dahia (buildable core) #17918 (2026-09-27) a importé Komlos/Tent.lean (Lem. 4.1 partie analyse).
• Reste à livrer : Def 1.3 (Δ = TV décalage), Def 3.1 (T_v split), Claim 3.2 (monotonie sous scission).
• Style p1a-p4 (registre fini, décharges par lemmes intermédiaires depuis les theorems déjà prouvés dans le lake).
  k2 (Lemme 1.4, induction simultanée n et d) : pas démarré.
  k3 (Lem. 4.1, FTC segments, Cauchy-Schwarz L^2) : partiellement livré via Tent.lean (constante √12).
  k4 (Lem. 1.5, discrétisation grille) : pas démarré.
  k5 (assemblage Thm 1.2 + corollaires 2/3 + notebooks Search-09c/09d) : pas démarré.

Contraintes opérationnelles :

• Lean v4.32.1 NON-BUILDABLE localement sur cette machine (cf MEMORY operating state). Donc aucun test local possible des preuves ; CI ferait le build.
• Strategie de port : re-distillation pédagogique (route b), pas pont direct depuis gdahia/Komlos (route a = introduit dependance externe, écart declare 36+η).
• i18n : sibling Komlos_en.lean (convention i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 ratifié) à produire en parallèle.
• Souring Dahia reste comme oracle de confiance, pas comme base de code.

Pas de cycle de livraison c.1273 (fenêtre courte, k1 demande > 25 min de code Lean + preuves). Reprise c.1274 ou plus tard selon priorite dashboard.

Lane po-2026:CoursIA-2 rend la main.

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory//discrepancy_lean//.lean, MyIA.AI.Notebooks/GameTheory/**/Komlos.lean -- 2026-09-30T21:00Z