Discrepancy-02 — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)

Deuxième marche de la sous-série Discrepancy/ (issue #17816, arbitrage Search #17802) — compagnon formel de Search-09c

Le lake discrepancy_lean formalise la discrépance combinatoire : colorer en ±1 les éléments d’un système d’ensembles de degré ≤ k en minimisant la pire somme colorée ‖Ax‖∞. Search-09c a exploré ce territoire en Python numérique — tirages aléatoires, arrondi flottant de Beck–Fiala, oracle exact CP-SAT. Ce compagnon exécute la couche formelle : les énoncés exacts du lake, intégrés au noyau Lean 4.

La cible centrale est le module Discrepancy/Komlos.lean — invisible d’aucun notebook avant celui-ci — qui porte la frontière SOTA du sujet : la conjecture de Komlós (matrices à colonnes unitaires, O(1) conjecturé — résolution annoncée par un preprint de septembre 2026, non revu) et les formes du papier Bansal–Jiang 2025 (arXiv:2508.03961), premières à dépasser Banaszczyk.

Trois « discrépances », une désambiguïsation : la Limited Discrepancy Search de Search-03c est une heuristique de parcours d’arbre (Harvey & Ginsberg) — aucun rapport avec les sommes signées mesurées ici ; Search-09c et ce compagnon traitent le même objet mathématique, l’un numériquement, l’autre formellement.

Contrat de validation du kernel : lean4-wsl émet tous ses messages — y compris les erreurs de compilation Lean — en display_data de sévérité info, jamais en output_type=error. Un passage sain se vérifie donc par l’absence de marque ❌ et de toute sévérité error dans les raw outputs (détail : wsl-kernels-detail.md).

Comment lire ce notebook : chaque section suit le même mouvement — le cadre (les énoncés du lake tels que #check les rend), une exécution chiffrée (#eval sur des témoins décidés), puis une lecture mathématique qui interprète les nombres. Les conjectures vivent en Prop nommées — jamais en théorèmes tronqués : c’est l’honnêteté documentée du lake (voir FORMAL_STATUS.md).

1. Le paysage : prouvé, conjecturé, et la formalisation honnête

La théorie de la discrépance se lit comme une course aux bornes, chaque ligne gagnant un facteur logarithmique sur la précédente :

Résultat	Régime	Borne	Statut
Beck–Fiala (classique)	degré `≤ k`	`disc ≤ 2k − 1`	théorème (prouvé)
Beck–Fiala (conjecture)	degré `≤ k`	`O(√k)`	résolution annoncée 2026 (non revue)
Banaszczyk (1998)	colonnes unitaires	`O(√(log n))`	théorème
Bansal–Jiang (2025)	`k ≥ (log n)²`	`O(√k)`	théorème (papier)
Bansal–Jiang (2025)	colonnes unitaires	`Õ(log^(1/4) n)`	théorème (papier)
Komlós	colonnes unitaires	`O(1)` ; annoncé `< 3√(2π) ≈ 7,52`	résolution annoncée 2026 (non revue)
Guo–Fang–Lu (2026)	degré `≤ k` et colonnes unitaires	`< 3√(2πt)` et `< 3√(2π)`	annoncé (preprint non revu)

La formalisation doit dire la vérité sur ce qu’elle sait : les preuves de Bansal–Jiang exigent un étage absent de Mathlib (SDP et dualité, indépendance spectrale affine, mouvement brownien discret guidé, concentration matricielle). Le lake choisit donc d’énoncer les conjectures comme des Prop nommées — des énoncés exacts, citables, vérifiables de type — dont les preuves attendront l’étage amont. Aucun sorry maquillé en théorème : la frontière est déclarée frontière. Le preprint de septembre 2026 qui annonce la résolution des deux conjectures (arXiv:2609.11189, non revu) ne change pas ce contrat : sa route — variation totale directionnelle, transformée de Banaszczyk — déplace l’obstruction au lieu de la contourner, et cet étage n’existe pas davantage dans Mathlib.

Chargeons le lake dans le noyau.

import Discrepancy.Komlos
-- La machinerie prouvee du lake, interrogee en section 6 :
import Discrepancy.Kernel
import Discrepancy.Partial
import Discrepancy.Progress
import Discrepancy.BeckFiala
import Discrepancy.ErdosSpencer

import Discrepancy.Komlos

-- La machinerie prouvee du lake, interrogee en section 6 :

import Discrepancy.Kernel

import Discrepancy.Partial

import Discrepancy.Progress

import Discrepancy.BeckFiala

import Discrepancy.ErdosSpencer

--% env 0

Raw input

{"cmd": "import Discrepancy.Komlos\n-- La machinerie prouvee du lake, interrogee en section 6 :\nimport Discrepancy.Kernel\nimport Discrepancy.Partial\nimport Discrepancy.Progress\nimport Discrepancy.BeckFiala\nimport Discrepancy.ErdosSpencer"}

Raw output

{"env": 0}

L’import résout Discrepancy.Komlos — et par lui Discrepancy.Basic, puis Mathlib tout entier : le chargement du noyau prend quelques minutes, c’est le prix d’un socle formel complet. Une fois chargé, chaque définition du lake vit dans l’environnement sous son nom qualifié — Discrepancy. en préfixe de namespace.

-- Le moteur verifie l'existence et les types des declarations du module noir
#check Discrepancy.KomlosConjecture
#check Discrepancy.BansalJiangLargeDegree
#check Discrepancy.KomlosBansalJiangWeak

-- ... et des fondations de Basic, citees par les enonces
#check Discrepancy.IsColoring
#check Discrepancy.discrepancy
#check Discrepancy.maxDegree
#check Discrepancy.BeckFialaConjecture
#check Discrepancy.BeckFialaClassic

-- Le moteur verifie l'existence et les types des declarations du module noir

#check Discrepancy.KomlosConjecture Discrepancy.KomlosConjecture : Prop

#check Discrepancy.BansalJiangLargeDegree Discrepancy.BansalJiangLargeDegree : Prop

#check Discrepancy.KomlosBansalJiangWeak Discrepancy.KomlosBansalJiangWeak : Prop

-- ... et des fondations de Basic, citees par les enonces

#check Discrepancy.IsColoring Discrepancy.IsColoring.{u_1} {α : Type u_1} (c : α → ℤ) : Prop

#check Discrepancy.discrepancy Discrepancy.discrepancy.{u_1} {α : Type u_1} [DecidableEq α] (F : Finset (Finset α)) (c : α → ℤ) : ℕ

#check Discrepancy.maxDegree Discrepancy.maxDegree.{u_1} {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : ℕ

#check Discrepancy.BeckFialaConjecture Discrepancy.BeckFialaConjecture : Prop

#check Discrepancy.BeckFialaClassic Discrepancy.BeckFialaClassic : Prop

--% env 1

Raw input

{"cmd": "-- Le moteur verifie l'existence et les types des declarations du module noir\n#check Discrepancy.KomlosConjecture\n#check Discrepancy.BansalJiangLargeDegree\n#check Discrepancy.KomlosBansalJiangWeak\n\n-- ... et des fondations de Basic, citees par les enonces\n#check Discrepancy.IsColoring\n#check Discrepancy.discrepancy\n#check Discrepancy.maxDegree\n#check Discrepancy.BeckFialaConjecture\n#check Discrepancy.BeckFialaClassic", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data": "Discrepancy.KomlosConjecture : Prop"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data": "Discrepancy.BansalJiangLargeDegree : Prop"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data": "Discrepancy.KomlosBansalJiangWeak : Prop"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data": "Discrepancy.IsColoring.{u_1} {α : Type u_1} (c : α → ℤ) : Prop"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "Discrepancy.discrepancy.{u_1} {α : Type u_1} [DecidableEq α] (F : Finset (Finset α)) (c : α → ℤ) : ℕ"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "Discrepancy.maxDegree.{u_1} {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : ℕ"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "Discrepancy.BeckFialaConjecture : Prop"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data": "Discrepancy.BeckFialaClassic : Prop"}],
 "env": 1}

Lecture du résultat — trois signatures, trois régimes : universelle, grand degré, polylog

Chaque #check rend la signature complète — l’énoncé mathématique entier, pas son nom. Trois lectures structurent le paysage :

KomlosConjecture commence par ∃ C : ℚ, ∀ (m n : ℕ) (A : Matrix …) : il existe une constante universelle — indépendante de la matrice, de ses dimensions, de tout — C telle que toute matrice à colonnes unitaires admette une coloration ±1 bornant chaque somme de ligne par C. L’hypothèse ∀ j, ∑ i, A i j * A i j = 1 est la condition unitaire : chaque colonne est un vecteur de norme 1. C’est l’énoncé de Komlós, ouvert depuis les années 1970 — Banaszczyk n’en a que O(√(log n)). Un preprint de septembre 2026 (arXiv:2609.11189, non revu) annonce la constante universelle 3√(2π) ≈ 7,52 — sur ℝ ; l’énoncé ci-dessus reste une Prop, posé sur ℚ avec C : ℚ : tout alignement futur devra choisir un témoin rationnel explicite (8 convient).
BansalJiangLargeDegree change de régime : ∃ C : ℕ, ∀ n k (F : Finset (Finset (Fin n))), avec deux hypothèses — degré maxDegree F ≤ k et (Nat.log 2 n)² ≤ k — pour la même conclusion O(√k) que la conjecture de Beck–Fiala. Le papier prouve que la conjecture vaut dès que le degré domine le carré du logarithme.
KomlosBansalJiangWeak est la même conclusion que Komlós avec la borne affaiblie C * ((Nat.log 2 n : ℚ)²) — un exposant polylog conservateur (2 au lieu du 1/4 du papier) : l’énoncé reste impliqué par le théorème du papier, donc vrai dès que le papier l’est, sans prétendre aux exposants exacts du Õ.

Les sommes sont écrites à la main (∑ i, A i j * c j) plutôt qu’avec Matrix.mulVec — choix du lake pour que la colonne-ligne reste lisible comme une somme de produits, au plus près du papier.

2. Le vocabulaire opérationnel, sur un système concret

Avant les conjectures, les définitions que tout le monde partage. Un système est une famille finie de parties ; une coloration c envoie chaque élément sur ±1 ; la discrépance du système sous c est la pire somme colorée en valeur absolue. Prenons trois ensembles sur Fin 3 : {0,1}, {1,2}, {0,2} — chaque élément appartient à exactement deux ensembles (degré 2).

-- Un systeme concret sur Fin 3 : deux paires partageant l'element 1
def p1 : Finset (Fin 3) := {0, 1}
def p2 : Finset (Fin 3) := {1, 2}

def F2 : Finset (Finset (Fin 3)) := {p1, p2}

def cBon : Fin 3 → ℤ := ![1, -1, 1]
def cMauvais : Fin 3 → ℤ := ![1, 1, 1]

-- La discrepance : pire somme coloree en valeur absolue (un Nat via natAbs)
#eval Discrepancy.discrepancy F2 cBon        -- sommes : {0,1}→1-1=0, {1,2}→-1+1=0
#eval Discrepancy.discrepancy F2 cMauvais    -- sommes : 2, 2

-- Le degre maximal : l'element 1 appartient aux deux ensembles
#eval Discrepancy.maxDegree F2

-- Un systeme concret sur Fin 3 : deux paires partageant l'element 1

def p1 : Finset (Fin 3) := {0, 1}

def p2 : Finset (Fin 3) := {1, 2}

def F2 : Finset (Finset (Fin 3)) := {p1, p2}

def cBon : Fin 3 → ℤ := ![1, -1, 1]

def cMauvais : Fin 3 → ℤ := ![1, 1, 1]

-- La discrepance : pire somme coloree en valeur absolue (un Nat via natAbs)

#eval Discrepancy.discrepancy F2 cBon        -- sommes : {0,1}→1-1=0, {1,2}→-1+1=0 0

#eval Discrepancy.discrepancy F2 cMauvais    -- sommes : 2, 2 2

-- Le degre maximal : l'element 1 appartient aux deux ensembles

#eval Discrepancy.maxDegree F2 2

--% env 2

Raw input

{"cmd": "-- Un systeme concret sur Fin 3 : deux paires partageant l'element 1\ndef p1 : Finset (Fin 3) := {0, 1}\ndef p2 : Finset (Fin 3) := {1, 2}\n\ndef F2 : Finset (Finset (Fin 3)) := {p1, p2}\n\ndef cBon : Fin 3 \u2192 \u2124 := ![1, -1, 1]\ndef cMauvais : Fin 3 \u2192 \u2124 := ![1, 1, 1]\n\n-- La discrepance : pire somme coloree en valeur absolue (un Nat via natAbs)\n#eval Discrepancy.discrepancy F2 cBon        -- sommes : {0,1}\u21921-1=0, {1,2}\u2192-1+1=0\n#eval Discrepancy.discrepancy F2 cMauvais    -- sommes : 2, 2\n\n-- Le degre maximal : l'element 1 appartient aux deux ensembles\n#eval Discrepancy.maxDegree F2", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "0"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 5},
   "data": "2"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 5},
   "data": "2"}],
 "env": 2}

Lecture du résultat — le témoin `F2` sur `Fin 3` : discrépance nulle, degré 2

La coloration alternée ⟨1, −1, 1⟩ produit les sommes 0 et 0 — la discrépance est nulle : chaque ensemble contient un +1 et un −1, parfaitement équilibrés. La coloration constante, elle, cumule : sommes 2 et 2, discrépance 2. La définition rend cela visible dans son code même : discrepancy F c = (F.image fun S => (S.sum c).natAbs).sup id — on prend la somme colorée de chaque partie (S.sum c), sa valeur absolue (natAbs, d’où le type ℕ), puis le suprémum sur la famille (sup id : la pire partie). Et maxDegree F2 = 2 : le degré d’un élément est le cardinal des ensembles qui le contiennent (degree F x = (F.filter fun S => x ∈ S).card), et l’élément 1 appartient aux deux.

Ce système illustre déjà la tension du sujet : avec k = 2, Beck–Fiala classique promet disc ≤ 2·2 − 1 = 3 pour toute coloration existante correcte — et le système admet mieux (0). La conjecture de Beck–Fiala (ligne O(√k) du tableau) porte sur l’optimum ; la marge entre 3, √2 et ce que le pire système force vraiment, c’est exactement l’écart que Bansal–Jiang 2025 a commencé à refermer.

3. Komlós en acte — I : des colonnes unitaires pythagoriciennes

La conjecture de Komlós vit dans le monde des matrices à colonnes unitaires : chaque colonne j vérifie ∑ i, A i j * A i j = 1 — un vecteur de norme euclidienne 1. Le plus petit exemple rationnel non trivial est pythagoricien : (3/5, 4/5), car (3/5)² + (4/5)² = 9/25 + 16/25 = 1. Construisons une matrice 2×2 dont les deux colonnes sont unitaires — puis laissons le noyau vérifier la condition, au lieu de la croire sur parole.

-- Matrice 2x2 a colonnes unitaires : (3/5, 4/5) et (4/5, 3/5), pythagoriciennes
def A2 : Matrix (Fin 2) (Fin 2) ℚ := !![(3/5 : ℚ), (4/5 : ℚ);
                                        (4/5 : ℚ), (3/5 : ℚ)]

-- Le noyau verifie la condition unitaire de Komlos, colonne par colonne
#eval (∀ j, ∑ i, A2 i j * A2 i j = 1)

-- Matrice 2x2 a colonnes unitaires : (3/5, 4/5) et (4/5, 3/5), pythagoriciennes

def A2 : Matrix (Fin 2) (Fin 2) ℚ := !![(3/5 : ℚ), (4/5 : ℚ);

                                        (4/5 : ℚ), (3/5 : ℚ)]

-- Le noyau verifie la condition unitaire de Komlos, colonne par colonne

#eval (∀ j, ∑ i, A2 i j * A2 i j = 1) true

--% env 3

Raw input

{"cmd": "-- Matrice 2x2 a colonnes unitaires : (3/5, 4/5) et (4/5, 3/5), pythagoriciennes\ndef A2 : Matrix (Fin 2) (Fin 2) \u211a := !![(3/5 : \u211a), (4/5 : \u211a);\n                                        (4/5 : \u211a), (3/5 : \u211a)]\n\n-- Le noyau verifie la condition unitaire de Komlos, colonne par colonne\n#eval (\u2200 j, \u2211 i, A2 i j * A2 i j = 1)", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "true"}],
 "env": 3}

Lecture du résultat — la condition unitaire de `A2`, décidée par le noyau

true — le noyau a évalué les deux sommes 9/25 + 16/25 et conclut l’égalité à 1. C’est la condition d’hypothèse de KomlosConjecture (∀ j, ∑ i, A i j * A i j = 1), décidée sur le témoin plutôt qu’assertée. La question de Komlós devient concrète : pour cette matrice, existe-t-il une coloration c ∈ {±1}² telle que les deux sommes de ligne ½·(3c₀ + 4c₁) et ½·(4c₀ + 3c₁) restent petites ? Énumérons — il n’y a que 2² = 4 colorations possibles.

-- Les 4 colorations possibles de Fin 2, et la somme de chaque ligne sous chacune
def colorings2 : List (Fin 2 → ℤ) := [![1, 1], ![1, -1], ![-1, 1], ![-1, -1]]

def lineSum (A : Matrix (Fin 2) (Fin 2) ℚ) (c : Fin 2 → ℤ) (i : Fin 2) : ℚ :=
  ∑ j, A i j * (c j : ℚ)

-- Pour chaque coloriage : les deux sommes de ligne (ligne 0, ligne 1)
#eval colorings2.map fun c => (lineSum A2 c 0, lineSum A2 c 1)

-- Les 4 colorations possibles de Fin 2, et la somme de chaque ligne sous chacune

def colorings2 : List (Fin 2 → ℤ) := [![1, 1], ![1, -1], ![-1, 1], ![-1, -1]]

def lineSum (A : Matrix (Fin 2) (Fin 2) ℚ) (c : Fin 2 → ℤ) (i : Fin 2) : ℚ :=

  ∑ j, A i j * (c j : ℚ)

-- Pour chaque coloriage : les deux sommes de ligne (ligne 0, ligne 1)

#eval colorings2.map fun c => (lineSum A2 c 0, lineSum A2 c 1) [(7 / 5, 7 / 5), (-1 / 5, 1 / 5), (1 / 5, -1 / 5), (-7 / 5, -7 / 5)]

--% env 4

Raw input

{"cmd": "-- Les 4 colorations possibles de Fin 2, et la somme de chaque ligne sous chacune\ndef colorings2 : List (Fin 2 \u2192 \u2124) := [![1, 1], ![1, -1], ![-1, 1], ![-1, -1]]\n\ndef lineSum (A : Matrix (Fin 2) (Fin 2) \u211a) (c : Fin 2 \u2192 \u2124) (i : Fin 2) : \u211a :=\n  \u2211 j, A i j * (c j : \u211a)\n\n-- Pour chaque coloriage : les deux sommes de ligne (ligne 0, ligne 1)\n#eval colorings2.map fun c => (lineSum A2 c 0, lineSum A2 c 1)", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data":
   "[(7 / 5, 7 / 5), (-1 / 5, 1 / 5), (1 / 5, -1 / 5), (-7 / 5, -7 / 5)]"}],
 "env": 4}

Lecture du résultat — les quatre colorations de `A2` : l’opposition divise la pire somme par sept

`c`	ligne 0 = `(3c₀ + 4c₁)/5`	ligne 1 = `(4c₀ + 3c₁)/5`	pire
`(1, 1)`	`7/5`	`7/5`	1.4
`(1, −1)`	`−1/5`	`1/5`	0.2
`(−1, 1)`	`1/5`	`−1/5`	0.2
`(−1, −1)`	`−7/5`	`−7/5`	1.4

La coloration qui oppose les deux colonnes équilibre presque parfaitement les lignes : la pire somme tombe à 1/5, sept fois moins que la pire coloration. C’est tout le geste de la discrépance : le choix des signes compense les colonnes entre elles. Le noyau peut aller au bout — chercher le minimum de la pire somme sur les quatre colorations.

-- La pire somme (en valeur absolue) d'une coloration, puis le minimum sur toutes
def absQ (x : ℚ) : ℚ := if x < 0 then -x else x

def maxLineAbs (A : Matrix (Fin 2) (Fin 2) ℚ) (c : Fin 2 → ℤ) : ℚ :=
  max (absQ (lineSum A c 0)) (absQ (lineSum A c 1))

-- Minimum et maximum d'une liste de rationnels (le cas vide, jamais atteint ici, vaut 0)
def minList : List ℚ → ℚ
  | [] => 0
  | [x] => x
  | x :: t => min x (minList t)

def maxList : List ℚ → ℚ
  | [] => 0
  | [x] => x
  | x :: t => max x (maxList t)

#eval minList (colorings2.map (maxLineAbs A2))

-- La pire somme (en valeur absolue) d'une coloration, puis le minimum sur toutes

def absQ (x : ℚ) : ℚ := if x < 0 then -x else x

def maxLineAbs (A : Matrix (Fin 2) (Fin 2) ℚ) (c : Fin 2 → ℤ) : ℚ :=

  max (absQ (lineSum A c 0)) (absQ (lineSum A c 1))

-- Minimum et maximum d'une liste de rationnels (le cas vide, jamais atteint ici, vaut 0)

def minList : List ℚ → ℚ

  | [] => 0

  | [x] => x

  | x :: t => min x (minList t)

def maxList : List ℚ → ℚ

  | [] => 0

  | [x] => x

  | x :: t => max x (maxList t)

#eval minList (colorings2.map (maxLineAbs A2)) 1 / 5

--% env 5

Raw input

{"cmd": "-- La pire somme (en valeur absolue) d'une coloration, puis le minimum sur toutes\ndef absQ (x : \u211a) : \u211a := if x < 0 then -x else x\n\ndef maxLineAbs (A : Matrix (Fin 2) (Fin 2) \u211a) (c : Fin 2 \u2192 \u2124) : \u211a :=\n  max (absQ (lineSum A c 0)) (absQ (lineSum A c 1))\n\n-- Minimum et maximum d'une liste de rationnels (le cas vide, jamais atteint ici, vaut 0)\ndef minList : List \u211a \u2192 \u211a\n  | [] => 0\n  | [x] => x\n  | x :: t => min x (minList t)\n\ndef maxList : List \u211a \u2192 \u211a\n  | [] => 0\n  | [x] => x\n  | x :: t => max x (maxList t)\n\n#eval minList (colorings2.map (maxLineAbs A2))", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 18, "column": 0},
   "endPos": {"line": 18, "column": 5},
   "data": "1 / 5"}],
 "env": 5}

Lecture du résultat — la discrépance optimale de `A2` vaut `1/5`, et les trois bornes s’y confondent

1/5 — la discrépance optimale de A2 (au sens de Komlós : le min du max des sommes de ligne sur les colorations ±1) vaut exactement 1/5, calculée par énumération exhaustive dans le noyau. Recommençons la lecture des conjectures avec ce nombre en main :

la conjecture de Komlós promet une constante universelle C avec 1/5 ≤ C — trivial sur ce témoin, mais l’énoncé exige la même C pour toutes les matrices, de toutes tailles ;
la forme affaiblie KomlosBansalJiangWeak borne par C · (log₂ n)² — ici n = 2, log₂ 2 = 1, donc la borne est C · 1 = C : sur ce témoin, la forme faible ne coûte rien ;
Banaszczyk donnerait O(√(log 2)) = O(1) : sur n = 2, toutes les bornes se confondent. Pour séparer les conjectures, il faut regarder n croître.

4. Komlós en acte — II : `n = 4` et la croissance mesurée contre le polylog

Prenons n = 4 colonnes unitaires orthogonales : les quatre motifs de signes (++++), (++--), (+-+-), (+--+) de Hadamard, chacun normalisé par 1/2 — car (±1/2)² × 4 = 1, chaque colonne est unitaire. Le carré du logarithme passe de 1 à (log₂ 4)² = 4 : si la pire somme mesurée croît nettement moins vite, la conjecture O(1) garde toute sa plausibilité sur ce petit terrain. L’énumération reste exhaustive : 2⁴ = 16 colorations.

-- Matrice 4x4 : colonnes de Hadamard normalisees 1/2 (chacune unitaire)
def A4 : Matrix (Fin 4) (Fin 4) ℚ := !![ 1/2,  1/2,  1/2,  1/2;
                                         1/2,  1/2, -1/2, -1/2;
                                         1/2, -1/2,  1/2, -1/2;
                                         1/2, -1/2, -1/2,  1/2]

-- Le noyau verifie l'universalite de la condition unitaire sur les 4 colonnes
#eval (∀ j, ∑ i, A4 i j * A4 i j = 1)

-- Les 16 colorations de Fin 4, par comprehension monadique
def colorings4 : List (Fin 4 → ℤ) := do
  let a ← [1, -1]
  let b ← [1, -1]
  let c ← [1, -1]
  let d ← [1, -1]
  return ![a, b, c, d]

-- Pire somme de ligne (valeur absolue) d'une coloration, par balayage des 4 lignes
def maxLineAbs4 (c : Fin 4 → ℤ) : ℚ :=
  (List.finRange 4).foldl (fun acc i => max acc (absQ (∑ j, A4 i j * (c j : ℚ)))) 0

-- Le duo demande : minimum et maximum de la pire somme sur les 16 colorations
#eval (minList (colorings4.map maxLineAbs4), maxList (colorings4.map maxLineAbs4))

-- Matrice 4x4 : colonnes de Hadamard normalisees 1/2 (chacune unitaire)

def A4 : Matrix (Fin 4) (Fin 4) ℚ := !![ 1/2,  1/2,  1/2,  1/2;

                                         1/2,  1/2, -1/2, -1/2;

                                         1/2, -1/2,  1/2, -1/2;

                                         1/2, -1/2, -1/2,  1/2]

-- Le noyau verifie l'universalite de la condition unitaire sur les 4 colonnes

#eval (∀ j, ∑ i, A4 i j * A4 i j = 1) true

-- Les 16 colorations de Fin 4, par comprehension monadique

def colorings4 : List (Fin 4 → ℤ) := do

  let a ← [1, -1]

  let b ← [1, -1]

  let c ← [1, -1]

  let d ← [1, -1]

  return ![a, b, c, d]

-- Pire somme de ligne (valeur absolue) d'une coloration, par balayage des 4 lignes

def maxLineAbs4 (c : Fin 4 → ℤ) : ℚ :=

  (List.finRange 4).foldl (fun acc i => max acc (absQ (∑ j, A4 i j * (c j : ℚ)))) 0

-- Le duo demande : minimum et maximum de la pire somme sur les 16 colorations

#eval (minList (colorings4.map maxLineAbs4), maxList (colorings4.map maxLineAbs4)) (1, 2)

--% env 6

Raw input

{"cmd": "-- Matrice 4x4 : colonnes de Hadamard normalisees 1/2 (chacune unitaire)\ndef A4 : Matrix (Fin 4) (Fin 4) \u211a := !![ 1/2,  1/2,  1/2,  1/2;\n                                         1/2,  1/2, -1/2, -1/2;\n                                         1/2, -1/2,  1/2, -1/2;\n                                         1/2, -1/2, -1/2,  1/2]\n\n-- Le noyau verifie l'universalite de la condition unitaire sur les 4 colonnes\n#eval (\u2200 j, \u2211 i, A4 i j * A4 i j = 1)\n\n-- Les 16 colorations de Fin 4, par comprehension monadique\ndef colorings4 : List (Fin 4 \u2192 \u2124) := do\n  let a \u2190 [1, -1]\n  let b \u2190 [1, -1]\n  let c \u2190 [1, -1]\n  let d \u2190 [1, -1]\n  return ![a, b, c, d]\n\n-- Pire somme de ligne (valeur absolue) d'une coloration, par balayage des 4 lignes\ndef maxLineAbs4 (c : Fin 4 \u2192 \u2124) : \u211a :=\n  (List.finRange 4).foldl (fun acc i => max acc (absQ (\u2211 j, A4 i j * (c j : \u211a)))) 0\n\n-- Le duo demande : minimum et maximum de la pire somme sur les 16 colorations\n#eval (minList (colorings4.map maxLineAbs4), maxList (colorings4.map maxLineAbs4))", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data": "true"},
  {"severity": "info",
   "pos": {"line": 23, "column": 0},
   "endPos": {"line": 23, "column": 5},
   "data": "(1, 2)"}],
 "env": 6}

Lecture du résultat — `A4` (Hadamard) : la pire somme va de 1 à 2, et le duo de témoins

(1, 2) — sur les seize colorations, la pire somme de ligne va de 1 (atteint par exemple par ⟨1, −1, −1, −1⟩ et ses symétriques, qui répartissent les ±1 contre les motifs de Hadamard) à 2 (les colorations alignées, ⟨1,1,1,1⟩ charge la ligne 0 à ½·4 = 2). Notons qu’aucune coloration n’atteint 0 : la matrice de Hadamard est inversible, donc Hc = 0 forcerait c = 0 — impossible avec des ±1. Récapitulons le duo de témoins :

Témoin	`n`	`(log₂ n)²`	disc. optimale mesurée
`A2` (pythagoricien)	2	1	`1/5`
`A4` (Hadamard `1/2`)	4	4	`1`

La borne polylog de la forme faible a été multipliée par 4 quand la discrépance mesurée l’a été par 5 — sur deux points, aucune asymptotique ne se lit ; ces témoins sont des panneaux indicateurs, pas des preuves. Mais ils rendent la question de Komlós tactile : la conjecture exige que la dernière colonne finisse par plafonner en n, contre l’intuition que plus de colonnes offrent plus de compensations. C’est précisément ce que le papier Bansal–Jiang approach : Õ(log^(1/4) n) — presque plat.

5. Ce que le lake prouve déjà : les théorèmes P0

Le lake n’est pas que des conjectures : ses fondations portent trois théorèmes élémentaires prouvés — discrepancy_empty (le système vide a disc 0), discrepancy_singleton_empty (une famille réduite à l’ensemble vide), degree_le_card (le degré d’un élément est borné par le cardinal des ensembles). Leurs énoncés sont courts, et le premier se vérifie numériquement à la demande.

-- Les trois theoremes P0 du lake
#check @Discrepancy.discrepancy_empty
#check @Discrepancy.discrepancy_singleton_empty
#check @Discrepancy.degree_le_card

-- Le premier, execute sur un temoin : le systeme vide a discrepance 0, quelle que soit la couleur
#eval Discrepancy.discrepancy (∅ : Finset (Finset (Fin 3))) cBon

-- Les trois theoremes P0 du lake

#check @Discrepancy.discrepancy_empty @Discrepancy.discrepancy_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ), Discrepancy.discrepancy ∅ c = 0

#check @Discrepancy.discrepancy_singleton_empty @Discrepancy.discrepancy_singleton_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ),
  Discrepancy.discrepancy {∅} c = 0

#check @Discrepancy.degree_le_card @Discrepancy.degree_le_card : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α)) (x : α),
  Discrepancy.degree F x ≤ F.card

-- Le premier, execute sur un temoin : le systeme vide a discrepance 0, quelle que soit la couleur

#eval Discrepancy.discrepancy (∅ : Finset (Finset (Fin 3))) cBon 0

--% env 7

Raw input

{"cmd": "-- Les trois theoremes P0 du lake\n#check @Discrepancy.discrepancy_empty\n#check @Discrepancy.discrepancy_singleton_empty\n#check @Discrepancy.degree_le_card\n\n-- Le premier, execute sur un temoin : le systeme vide a discrepance 0, quelle que soit la couleur\n#eval Discrepancy.discrepancy (\u2205 : Finset (Finset (Fin 3))) cBon", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@Discrepancy.discrepancy_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ), Discrepancy.discrepancy ∅ c = 0"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@Discrepancy.discrepancy_singleton_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ),\n  Discrepancy.discrepancy {∅} c = 0"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Discrepancy.degree_le_card : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α)) (x : α),\n  Discrepancy.degree F x ≤ F.card"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "0"}],
 "env": 7}

Lecture du résultat — les théorèmes du socle : la discrépance du vide est nulle, et c’est prouvé

0 — et le théorème dit que c’est invitable : discrepancy ∅ c = 0 pour toute coloration c, parce que le supremum d’une famille vide d’entiers est le bottom (Finset.sup sur ∅). La preuve du lake tient en un simp [discrepancy]. On pourrait croire l’évidence dispensable ; formalisée, elle devient le socle vérifié sur lequel les énoncés plus ambitieux s’appuient — et le garde-fou contre une définition de discrepancy qui se comporterait mal sur les cas dégénérés. C’est la hiérarchie honnête du lake : des théorèmes petits et prouvés, des conjectures grandes et nommées, aucun flou entre les deux.

6. La machinerie prouvée : Beck–Fiala (b1–b4) et Erdős–Spencer (p1a–p4)

Les sections précédentes interrogeaient les fondations (P0, section 5) et les conjectures (Komlós, Bansal–Jiang, section 1). Le lake porte aussi deux résultats prouvés de bout en bout, assemblés boute par boute (voir FORMAL_STATUS.md) — et jusqu’ici aucune de leurs déclarations n’était citée par le moindre notebook du corpus : c’était le plus grand trou de visibilité de l’EPIC #11703 (6 modules noirs sur 8 au rejeu du 2026-09-02).

Beck–Fiala classique (disc ≤ 2k − 1) : la « noix » du lake, prouvée en quatre boutes — b1 le double comptage dimensionnel (Kernel.lean), b2 l’invariant de coloration partielle (Partial.lean), b3 le progrès d’une phase (Progress.lean), b4 la terminaison et l’assemblage (BeckFiala.lean).
Erdős–Spencer inférieur (√k/14 explicite) : la borne inférieure par méthode probabiliste (ErdosSpencer.lean, assemblage p1a–p4) — pour k ≤ n, il existe une famille de degré ≤ k qu’aucune coloration ne discipline à mieux que √k/14.

-- Section 6 : les quatre boutes de la preuve Beck-Fiala, interrogees nativement.
-- b1 : s'il reste plus de flottants que d'elements, une direction du noyau meurt
#check @Discrepancy.card_dangerous_lt_card_floating
#check @Discrepancy.exists_dangerous_kernel_vec
-- b2 : une ligne figee preserve sa somme initiale a 2k-1 pres
#check @Discrepancy.frozen_line_sum_le
-- b3 : chaque phase avance jusqu'au premier contact avec le bord du cube
#check @Discrepancy.exists_step_hits_boundary
-- b4 : l'assemblage -- le theoreme classique, disc <= 2k - 1
#check @Discrepancy.beck_fiala_classic
-- Le certificat : de quoi la preuve depend-elle, exactement ?
#print axioms Discrepancy.beck_fiala_classic

-- Section 6 : les quatre boutes de la preuve Beck-Fiala, interrogees nativement.

-- b1 : s'il reste plus de flottants que d'elements, une direction du noyau meurt

#check @Discrepancy.card_dangerous_lt_card_floating @Discrepancy.card_dangerous_lt_card_floating : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α))
  (X : Finset α) (k : ℕ), X.Nonempty → (∀ x ∈ X, Discrepancy.degree F x ≤ k) → {S ∈ F | k < (S ∩ X).card}.card < X.card

#check @Discrepancy.exists_dangerous_kernel_vec @Discrepancy.exists_dangerous_kernel_vec : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α))
  (X : Finset α) (k : ℕ),
  X.Nonempty →
    (∀ x ∈ X, Discrepancy.degree F x ≤ k) →
      ∃ v, (∃ x ∈ X, v x ≠ 0) ∧ ∀ S ∈ {S ∈ F | k < (S ∩ X).card}, ∑ x ∈ X, (if x ∈ S then 1 else 0) * v x = 0

-- b2 : une ligne figee preserve sa somme initiale a 2k-1 pres

#check @Discrepancy.frozen_line_sum_le @Discrepancy.frozen_line_sum_le : ∀ {α : Type u_1} [DecidableEq α] (c₀ : α → ℚ) (c : α → ℤ) (Y S : Finset α) (k : ℕ),
  Y ⊆ S →
    Y.card ≤ k →
      Discrepancy.IsColoring c →
        (∀ x ∈ Y, |c₀ x| < 1) → ∑ x ∈ S, c₀ x = 0 → (∀ x ∈ S, x ∉ Y → ↑(c x) = c₀ x) → (∑ x ∈ S, c x).natAbs ≤ 2 * k - 1

-- b3 : chaque phase avance jusqu'au premier contact avec le bord du cube

#check @Discrepancy.exists_step_hits_boundary @Discrepancy.exists_step_hits_boundary : ∀ {α : Type u_1} [DecidableEq α] (c₀ v : α → ℚ) (X : Finset α),
  X.Nonempty →
    (∀ x ∈ X, |c₀ x| < 1) →
      (∃ x₀ ∈ X, v x₀ ≠ 0) → ∃ t, 0 < t ∧ (∀ x ∈ X, |c₀ x + t * v x| ≤ 1) ∧ ∃ x₁ ∈ X, |c₀ x₁ + t * v x₁| = 1

-- b4 : l'assemblage -- le theoreme classique, disc <= 2k - 1

#check @Discrepancy.beck_fiala_classic Discrepancy.beck_fiala_classic : Discrepancy.BeckFialaClassic

-- Le certificat : de quoi la preuve depend-elle, exactement ?

#print axioms Discrepancy.beck_fiala_classic 'Discrepancy.beck_fiala_classic' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 8

Raw input

{"cmd": "-- Section 6 : les quatre boutes de la preuve Beck-Fiala, interrogees nativement.\n-- b1 : s'il reste plus de flottants que d'elements, une direction du noyau meurt\n#check @Discrepancy.card_dangerous_lt_card_floating\n#check @Discrepancy.exists_dangerous_kernel_vec\n-- b2 : une ligne figee preserve sa somme initiale a 2k-1 pres\n#check @Discrepancy.frozen_line_sum_le\n-- b3 : chaque phase avance jusqu'au premier contact avec le bord du cube\n#check @Discrepancy.exists_step_hits_boundary\n-- b4 : l'assemblage -- le theoreme classique, disc <= 2k - 1\n#check @Discrepancy.beck_fiala_classic\n-- Le certificat : de quoi la preuve depend-elle, exactement ?\n#print axioms Discrepancy.beck_fiala_classic", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@Discrepancy.card_dangerous_lt_card_floating : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α))\n  (X : Finset α) (k : ℕ), X.Nonempty → (∀ x ∈ X, Discrepancy.degree F x ≤ k) → {S ∈ F | k < (S ∩ X).card}.card < X.card"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Discrepancy.exists_dangerous_kernel_vec : ∀ {α : Type u_1} [inst : DecidableEq α] (F : Finset (Finset α))\n  (X : Finset α) (k : ℕ),\n  X.Nonempty →\n    (∀ x ∈ X, Discrepancy.degree F x ≤ k) →\n      ∃ v, (∃ x ∈ X, v x ≠ 0) ∧ ∀ S ∈ {S ∈ F | k < (S ∩ X).card}, ∑ x ∈ X, (if x ∈ S then 1 else 0) * v x = 0"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@Discrepancy.frozen_line_sum_le : ∀ {α : Type u_1} [DecidableEq α] (c₀ : α → ℚ) (c : α → ℤ) (Y S : Finset α) (k : ℕ),\n  Y ⊆ S →\n    Y.card ≤ k →\n      Discrepancy.IsColoring c →\n        (∀ x ∈ Y, |c₀ x| < 1) → ∑ x ∈ S, c₀ x = 0 → (∀ x ∈ S, x ∉ Y → ↑(c x) = c₀ x) → (∑ x ∈ S, c x).natAbs ≤ 2 * k - 1"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@Discrepancy.exists_step_hits_boundary : ∀ {α : Type u_1} [DecidableEq α] (c₀ v : α → ℚ) (X : Finset α),\n  X.Nonempty →\n    (∀ x ∈ X, |c₀ x| < 1) →\n      (∃ x₀ ∈ X, v x₀ ≠ 0) → ∃ t, 0 < t ∧ (∀ x ∈ X, |c₀ x + t * v x| ≤ 1) ∧ ∃ x₁ ∈ X, |c₀ x₁ + t * v x₁| = 1"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "Discrepancy.beck_fiala_classic : Discrepancy.BeckFialaClassic"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "'Discrepancy.beck_fiala_classic' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 8}

Lecture du résultat — la colonne vertébrale de Beck–Fiala et son certificat d’axiomes

Les quatre #check tracent la colonne vertébrale de l’algorithme : tant qu’une ligne garde plus de k éléments flottants, le noyau dimensionnel (b1) fournit une direction qui préserve exactement les sommes des lignes dangereuses ; la phase (b3) avance le long de cette direction jusqu’au premier contact avec le bord du cube [-1,1]^X et fige au moins un nouveau flottant en ±1 ; l’invariant (b2) garantit qu’une ligne figée ne dérive jamais de plus de 2k − 1. Le nombre de flottants décroît strictement à chaque phase, donc la boucle termine et l’arrondi final produit la coloration (b4). Le #print axioms rend le certificat ci-dessus : la preuve repose sur les trois axiomes standard de Mathlib (propext, Classical.choice, Quot.sound) — aucun sorry, aucun native_decide : beck_fiala_classic est un théorème au sens plein, pas un énoncé espéré.

-- La borne inferieure d'Erdos-Spencer, a constante explicite (assemblage p1a-p4) :
-- pour 1 <= k <= n il existe une famille de degre <= k telle que TOUTE coloration
-- garde une ligne a somme >= sqrt(k)/14
#check @Discrepancy.erdos_spencer_lb_explicit
#print axioms Discrepancy.erdos_spencer_lb_explicit
-- La forme optimiste sqrt(k)/2 reste une Prop OUVERTE -- jamais pretendue prouvee :
#check Discrepancy.ErdosSpencerLB

-- La borne inferieure d'Erdos-Spencer, a constante explicite (assemblage p1a-p4) :

-- pour 1 <= k <= n il existe une famille de degre <= k telle que TOUTE coloration

-- garde une ligne a somme >= sqrt(k)/14

#check @Discrepancy.erdos_spencer_lb_explicit Discrepancy.erdos_spencer_lb_explicit : ∀ (n k : ℕ),
  1 ≤ k →
    k ≤ n →
      ∃ F,
        Discrepancy.maxDegree F ≤ k ∧
          ∀ (C : Fin n → ℤ), Discrepancy.IsColoring C → k.sqrt ≤ 14 * Discrepancy.discrepancy F C

#print axioms Discrepancy.erdos_spencer_lb_explicit 'Discrepancy.erdos_spencer_lb_explicit' depends on axioms: [propext, Classical.choice, Quot.sound]

-- La forme optimiste sqrt(k)/2 reste une Prop OUVERTE -- jamais pretendue prouvee :

#check Discrepancy.ErdosSpencerLB Discrepancy.ErdosSpencerLB : Prop

--% env 9

Raw input

{"cmd": "-- La borne inferieure d'Erdos-Spencer, a constante explicite (assemblage p1a-p4) :\n-- pour 1 <= k <= n il existe une famille de degre <= k telle que TOUTE coloration\n-- garde une ligne a somme >= sqrt(k)/14\n#check @Discrepancy.erdos_spencer_lb_explicit\n#print axioms Discrepancy.erdos_spencer_lb_explicit\n-- La forme optimiste sqrt(k)/2 reste une Prop OUVERTE -- jamais pretendue prouvee :\n#check Discrepancy.ErdosSpencerLB", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Discrepancy.erdos_spencer_lb_explicit : ∀ (n k : ℕ),\n  1 ≤ k →\n    k ≤ n →\n      ∃ F,\n        Discrepancy.maxDegree F ≤ k ∧\n          ∀ (C : Fin n → ℤ), Discrepancy.IsColoring C → k.sqrt ≤ 14 * Discrepancy.discrepancy F C"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "'Discrepancy.erdos_spencer_lb_explicit' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data": "Discrepancy.ErdosSpencerLB : Prop"}],
 "env": 9}

Lecture du résultat — `erdos_spencer_lb_explicit` : le second sommet, et la constante 14 assumée

erdos_spencer_lb_explicit est le second sommet prouvé : moments de la somme de Rademacher, Paley–Zygmund, union bound sur les 2^n colorations — la méthode probabiliste construit une famille de degré ≤ k qu’aucune coloration ne discipline à mieux que √k/14. La constante 14 n’est pas celle de l’énoncé optimal (√k/2) : l’écart est documenté dans le statut du module (Paley–Zygmund force ≥ 12t tirages par bloc quand le contrôle de degré n’en autorise que k), et le lake ne le masque pas — ErdosSpencerLB, la forme √k/2, reste une Prop ouverte, chargée ici comme conjecture. C’est la même hiérarchie honnête que celle de la section 1 : petits théorèmes prouvés, grandes conjectures nommées, aucun flou entre les deux — et le même certificat d’axiomes que Beck–Fiala.

7. Exercices

Trois preuves à compléter. Les indices sont dans les commentaires ; les #check en fin de cellule servent d’ancres d’exécution — la cellule reste une commande Lean valide même non complétée.

Exercice 1 — le système vide, à la main

Prouvez sur Fin 3 ce que discrepancy_empty dit en général : toute coloration du système vide a discrépance nulle. Indice : Finset.sup sur une famille vide rend ⊥ ; simp [Discrepancy.discrepancy] déplie la définition, et Finset.image_empty + Finset.sup_empty terminent.

-- Exercice 1 : le systeme vide a discrepance 0
-- TODO etudiant
-- example (c : Fin 3 → ℤ) :
--     Discrepancy.discrepancy (∅ : Finset (Finset (Fin 3))) c = 0 := by
--   sorry

-- ancre d'execution (cellule valide meme non completee) :
#check @Discrepancy.discrepancy_empty

-- Exercice 1 : le systeme vide a discrepance 0

-- TODO etudiant

-- example (c : Fin 3 → ℤ) :

--     Discrepancy.discrepancy (∅ : Finset (Finset (Fin 3))) c = 0 := by

--   sorry

-- ancre d'execution (cellule valide meme non completee) :

#check @Discrepancy.discrepancy_empty @Discrepancy.discrepancy_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ), Discrepancy.discrepancy ∅ c = 0

--% env 10

Raw input

{"cmd": "-- Exercice 1 : le systeme vide a discrepance 0\n-- TODO etudiant\n-- example (c : Fin 3 \u2192 \u2124) :\n--     Discrepancy.discrepancy (\u2205 : Finset (Finset (Fin 3))) c = 0 := by\n--   sorry\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check @Discrepancy.discrepancy_empty", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@Discrepancy.discrepancy_empty : ∀ {α : Type u_1} [inst : DecidableEq α] (c : α → ℤ), Discrepancy.discrepancy ∅ c = 0"}],
 "env": 10}

Exercice 2 — la colonne pythagoricienne est unitaire

L’hypothèse de Komlós pour la matrice A2 repose sur (3/5)² + (4/5)² = 1. Prouvez-le — puis, plus fort, prouvez la version générique sur les deux colonnes de A2 (indice : Fin.sum_univ_two réduit la somme, puis norm_num ferme l’arithmétique rationnelle).

-- Exercice 2 : la colonne (3/5, 4/5) est unitaire
-- TODO etudiant
-- example : (3 : ℚ) / 5 * (3 / 5) + 4 / 5 * (4 / 5) = 1 := by
--   sorry

-- ancre d'execution (cellule valide meme non completee) :
#check Discrepancy.KomlosConjecture

-- Exercice 2 : la colonne (3/5, 4/5) est unitaire

-- TODO etudiant

-- example : (3 : ℚ) / 5 * (3 / 5) + 4 / 5 * (4 / 5) = 1 := by

--   sorry

-- ancre d'execution (cellule valide meme non completee) :

#check Discrepancy.KomlosConjecture Discrepancy.KomlosConjecture : Prop

--% env 11

Raw input

{"cmd": "-- Exercice 2 : la colonne (3/5, 4/5) est unitaire\n-- TODO etudiant\n-- example : (3 : \u211a) / 5 * (3 / 5) + 4 / 5 * (4 / 5) = 1 := by\n--   sorry\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check Discrepancy.KomlosConjecture", "env": 10}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data": "Discrepancy.KomlosConjecture : Prop"}],
 "env": 11}

Exercice 3 — la conjecture implique sa forme faible sur `n = 2`

Montrez que KomlosConjecture spécialise sa conclusion à n = 2 sans perte : la borne C · (log₂ 2)² se réduit à C · 1 = C. Indice : obtain ⟨C, hC⟩ := h expose la constante universelle ; appliquez hC avec n := 2 ; Nat.log 2 2 = 1 se ferme par decide ou norm_num, et mul_one termine.

-- Exercice 3 : KomlosConjecture specialisee a n = 2
-- TODO etudiant
-- example (h : Discrepancy.KomlosConjecture) :
--     ∃ C : ℚ, ∀ (m : ℕ) (A : Matrix (Fin m) (Fin 2) ℚ),
--       (∀ j, ∑ i, A i j * A i j = 1) →
--         ∃ c : Fin 2 → ℚ,
--           (∀ j, c j = 1 ∨ c j = -1) ∧ ∀ i, |∑ j, A i j * c j| ≤ C := by
--   sorry

-- ancre d'execution (cellule valide meme non completee) :
#check Discrepancy.KomlosBansalJiangWeak

-- Exercice 3 : KomlosConjecture specialisee a n = 2

-- TODO etudiant

-- example (h : Discrepancy.KomlosConjecture) :

--     ∃ C : ℚ, ∀ (m : ℕ) (A : Matrix (Fin m) (Fin 2) ℚ),

--       (∀ j, ∑ i, A i j * A i j = 1) →

--         ∃ c : Fin 2 → ℚ,

--           (∀ j, c j = 1 ∨ c j = -1) ∧ ∀ i, |∑ j, A i j * c j| ≤ C := by

--   sorry

-- ancre d'execution (cellule valide meme non completee) :

#check Discrepancy.KomlosBansalJiangWeak Discrepancy.KomlosBansalJiangWeak : Prop

--% env 12

Raw input

{"cmd": "-- Exercice 3 : KomlosConjecture specialisee a n = 2\n-- TODO etudiant\n-- example (h : Discrepancy.KomlosConjecture) :\n--     \u2203 C : \u211a, \u2200 (m : \u2115) (A : Matrix (Fin m) (Fin 2) \u211a),\n--       (\u2200 j, \u2211 i, A i j * A i j = 1) \u2192\n--         \u2203 c : Fin 2 \u2192 \u211a,\n--           (\u2200 j, c j = 1 \u2228 c j = -1) \u2227 \u2200 i, |\u2211 j, A i j * c j| \u2264 C := by\n--   sorry\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check Discrepancy.KomlosBansalJiangWeak", "env": 11}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data": "Discrepancy.KomlosBansalJiangWeak : Prop"}],
 "env": 12}

Annexe — ErdosSpencer/Moments : la machinerie des moments (#11703)

Le scan de visibilite (scan_lake_notebook_visibility.py) comptait ErdosSpencer/Moments.lean comme le dernier module noir du lake discrepancy_lean : 38 declarations citees nulle part. C’est pourtant la jambe probabiliste de la borne d’Erdos-Spencer — la ou la machinerie Komlos_execute plus haut borne la discrepance d’une colonne unitaire, les moments de la somme de Rademacher controlent la queue de la distribution des colorations :

rademacherSum c S — la somme signee ∑ i, c i * boolSign (S i) d’une coloration S vue comme tirage de signes ;
expect_rademacherSum_eq_zero et expect_rademacherSum_sq — les moments d’ordre 1 et 2 : esperance nulle, variance egale a la somme des carres des coefficients ;
expect_rademacher_fourth_moment puis ..._of_isColoring — le moment d’ordre 4, le coeur technique : les termes croises s’annulent par parite de boolSign ;
prob_tail_ge_of_isColoring — la borne de queue qui convertit le 4e moment en controle probabiliste (Cauchy-Schwarz pondere via weighted_cauchy).

L’import vit seul dans sa cellule : le REPL lean4 ne commit reellement l’environnement que si la commande ne contient que des imports (convention du kernel, cf la cellule d’import d’ouverture).

import Discrepancy.ErdosSpencer.Moments

import Discrepancy.ErdosSpencer.Moments

--% env 0

Raw input

{"cmd": "import Discrepancy.ErdosSpencer.Moments\n"}

Raw output

{"env": 0}

-- Moments (ErdosSpencer) : la machinerie des moments du lake, module noir restant (#11703)
#check @Discrepancy.rademacherSum
#check @Discrepancy.expect_rademacherSum_eq_zero
#check @Discrepancy.expect_rademacherSum_sq
#check @Discrepancy.expect_rademacher_fourth_moment
#check @Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring
#check @Discrepancy.prob_tail_ge_of_isColoring

-- Integrite : la machinerie ne depend que des axiomes standards
#print axioms Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring
#print axioms Discrepancy.prob_tail_ge_of_isColoring

-- Moments (ErdosSpencer) : la machinerie des moments du lake, module noir restant (#11703)

#check @Discrepancy.rademacherSum @Discrepancy.rademacherSum : {n : ℕ} → (Fin n → ℤ) → (Fin n → Bool) → ℝ

#check @Discrepancy.expect_rademacherSum_eq_zero @Discrepancy.expect_rademacherSum_eq_zero : ∀ {n : ℕ} (c : Fin n → ℤ),
  PacLearning.sampleExpect Discrepancy.fairCoin (Discrepancy.rademacherSum c) = 0

#check @Discrepancy.expect_rademacherSum_sq @Discrepancy.expect_rademacherSum_sq : ∀ {n : ℕ} (c : Fin n → ℤ),
  (PacLearning.sampleExpect Discrepancy.fairCoin fun S => Discrepancy.rademacherSum c S ^ 2) = ∑ i, ↑(c i) ^ 2

#check @Discrepancy.expect_rademacher_fourth_moment @Discrepancy.expect_rademacher_fourth_moment : ∀ {n : ℕ} (a : Fin n → ℝ),
  (PacLearning.sampleExpect Discrepancy.fairCoin fun S => (∑ i, a i * Discrepancy.boolSign (S i)) ^ 4) =
    3 * ((∑ i, a i * a i) * ∑ i, a i * a i) - 2 * ∑ i, a i * a i * (a i * a i)

#check @Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring @Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring : ∀ {n : ℕ} (c : Fin n → ℤ),
  Discrepancy.IsColoring c →
    (PacLearning.sampleExpect Discrepancy.fairCoin fun S => Discrepancy.rademacherSum c S ^ 4) = 3 * ↑n ^ 2 - 2 * ↑n

#check @Discrepancy.prob_tail_ge_of_isColoring @Discrepancy.prob_tail_ge_of_isColoring : ∀ {n : ℕ} (c : Fin n → ℤ),
  Discrepancy.IsColoring c →
    1 ≤ n →
      (Discrepancy.probEvt fun S => ↑n / 2 ≤ Discrepancy.rademacherSum c S * Discrepancy.rademacherSum c S) ≥ 1 / 12

-- Integrite : la machinerie ne depend que des axiomes standards

#print axioms Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring 'Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

#print axioms Discrepancy.prob_tail_ge_of_isColoring 'Discrepancy.prob_tail_ge_of_isColoring' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "-- Moments (ErdosSpencer) : la machinerie des moments du lake, module noir restant (#11703)\n#check @Discrepancy.rademacherSum\n#check @Discrepancy.expect_rademacherSum_eq_zero\n#check @Discrepancy.expect_rademacherSum_sq\n#check @Discrepancy.expect_rademacher_fourth_moment\n#check @Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring\n#check @Discrepancy.prob_tail_ge_of_isColoring\n\n-- Integrite : la machinerie ne depend que des axiomes standards\n#print axioms Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring\n#print axioms Discrepancy.prob_tail_ge_of_isColoring\n", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@Discrepancy.rademacherSum : {n : ℕ} → (Fin n → ℤ) → (Fin n → Bool) → ℝ"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "@Discrepancy.expect_rademacherSum_eq_zero : ∀ {n : ℕ} (c : Fin n → ℤ),\n  PacLearning.sampleExpect Discrepancy.fairCoin (Discrepancy.rademacherSum c) = 0"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "@Discrepancy.expect_rademacherSum_sq : ∀ {n : ℕ} (c : Fin n → ℤ),\n  (PacLearning.sampleExpect Discrepancy.fairCoin fun S => Discrepancy.rademacherSum c S ^ 2) = ∑ i, ↑(c i) ^ 2"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@Discrepancy.expect_rademacher_fourth_moment : ∀ {n : ℕ} (a : Fin n → ℝ),\n  (PacLearning.sampleExpect Discrepancy.fairCoin fun S => (∑ i, a i * Discrepancy.boolSign (S i)) ^ 4) =\n    3 * ((∑ i, a i * a i) * ∑ i, a i * a i) - 2 * ∑ i, a i * a i * (a i * a i)"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "@Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring : ∀ {n : ℕ} (c : Fin n → ℤ),\n  Discrepancy.IsColoring c →\n    (PacLearning.sampleExpect Discrepancy.fairCoin fun S => Discrepancy.rademacherSum c S ^ 4) = 3 * ↑n ^ 2 - 2 * ↑n"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "@Discrepancy.prob_tail_ge_of_isColoring : ∀ {n : ℕ} (c : Fin n → ℤ),\n  Discrepancy.IsColoring c →\n    1 ≤ n →\n      (Discrepancy.probEvt fun S => ↑n / 2 ≤ Discrepancy.rademacherSum c S * Discrepancy.rademacherSum c S) ≥ 1 / 12"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data":
   "'Discrepancy.expect_rademacherSum_fourth_moment_of_isColoring' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 6},
   "data":
   "'Discrepancy.prob_tail_ge_of_isColoring' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 1}

Lecture de la sortie — le triptyque des moments, et un lake sans module noir

Les six #check affichent les signatures completes. Le triptyque des moments se lit comme un escalier : moment 1 nul (pas de biais), moment 2 = energie (variance), moment 4 = le terme qui discrimine — son controle sous IsColoring c est ce qui rend la queue de rademacherSum c · assez fine pour l’argument Erdos-Spencer. Les deux #print axioms repondent [propext, Classical.choice, Quot.sound] — les axiomes standards de Lean, aucun sorryAx : la machinerie probabiliste est prouvee au meme titre que le reste du lake.

Avec ce module expose, le lake discrepancy_lean n’a plus aucun module noir : les deux jambees de la borne — Komlos deterministe, Erdos-Spencer probabiliste — sont desormais lisibles depuis ce compagnon.

8. Ce que ce compagnon a rendu visible

Avant ce notebook, le module Discrepancy/Komlos.lean était noir : aucune de ses trois déclarations — KomlosConjecture, BansalJiangLargeDegree, KomlosBansalJiangWeak — n’était citée par le moindre notebook du corpus (mesure scan_lake_notebook_visibility.py). Puis la section 6 a ouvert la moitié restante du lake : Kernel, Partial, Progress, BeckFiala (b1–b4) et ErdosSpencer (p1a–p4) — dont les deux sommets prouvés, beck_fiala_classic et erdos_spencer_lb_explicit, désormais chargés avec leur certificat d’axiomes.

Ce compagnon l’exécute : les trois Prop rendues avec leurs signatures complètes, la condition unitaire décidée sur des témoins pythagoriciens et hadamardiens, la discrépance optimale calculée par énumération exhaustive dans le noyau (1/5 puis 1), les théorèmes P0 relus avec leur témoin, et la machinerie prouvée interrogée boute par boute. Relié au corpus :

Search-09c mesure les mêmes objets en numérique (numpy, arrondi Beck–Fiala, oracle CP-SAT) — la discrépance exacte qu’il approche par solver, ce compagnon l’énumère in-kernel sur des petits témoins, et sa borne 2k − 1 est maintenant le théorème exécuté de la section 6 ;
Search-03c rappelle que « discrepancy » a aussi une vie d’heuristique de parcours — sans rapport ;
le lake discrepancy_lean garde ses conjectures en Prop nommée : quand l’étage SDP existera en Mathlib, la preuve remplacera la déclaration sans changer l’énoncé — et ce notebook montrera le basculement. L’annonce de septembre 2026 (résolution à constante universelle, preprint non revu) ne change pas ce contrat : sa route exige un autre étage absent de Mathlib, et les Prop attendent toujours une preuve formelle.

Retour au sommet

1. Le paysage : prouvé, conjecturé, et la formalisation honnête

Lecture du résultat — trois signatures, trois régimes : universelle, grand degré, polylog

2. Le vocabulaire opérationnel, sur un système concret

Lecture du résultat — le témoin F2 sur Fin 3 : discrépance nulle, degré 2

3. Komlós en acte — I : des colonnes unitaires pythagoriciennes

Lecture du résultat — la condition unitaire de A2, décidée par le noyau

Lecture du résultat — les quatre colorations de A2 : l’opposition divise la pire somme par sept

Lecture du résultat — la discrépance optimale de A2 vaut 1/5, et les trois bornes s’y confondent

4. Komlós en acte — II : n = 4 et la croissance mesurée contre le polylog

Lecture du résultat — A4 (Hadamard) : la pire somme va de 1 à 2, et le duo de témoins

5. Ce que le lake prouve déjà : les théorèmes P0

Lecture du résultat — les théorèmes du socle : la discrépance du vide est nulle, et c’est prouvé

6. La machinerie prouvée : Beck–Fiala (b1–b4) et Erdős–Spencer (p1a–p4)

Lecture du résultat — la colonne vertébrale de Beck–Fiala et son certificat d’axiomes

Lecture du résultat — erdos_spencer_lb_explicit : le second sommet, et la constante 14 assumée

7. Exercices

Exercice 1 — le système vide, à la main

Exercice 2 — la colonne pythagoricienne est unitaire

Exercice 3 — la conjecture implique sa forme faible sur n = 2

Annexe — ErdosSpencer/Moments : la machinerie des moments (#11703)

Lecture de la sortie — le triptyque des moments, et un lake sans module noir

8. Ce que ce compagnon a rendu visible

Lecture du résultat — le témoin `F2` sur `Fin 3` : discrépance nulle, degré 2

Lecture du résultat — la condition unitaire de `A2`, décidée par le noyau

Lecture du résultat — les quatre colorations de `A2` : l’opposition divise la pire somme par sept

Lecture du résultat — la discrépance optimale de `A2` vaut `1/5`, et les trois bornes s’y confondent

4. Komlós en acte — II : `n = 4` et la croissance mesurée contre le polylog

Lecture du résultat — `A4` (Hadamard) : la pire somme va de 1 à 2, et le duo de témoins

Lecture du résultat — `erdos_spencer_lb_explicit` : le second sommet, et la constante 14 assumée

Exercice 3 — la conjecture implique sa forme faible sur `n = 2`