Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -507,11 +507,12 @@
"|---|---|---|---|\n",
"| Borne inférieure (Erdős–Spencer, méthode probabiliste) | $\\ge \\Omega(\\sqrt{k})$ sur certains systèmes | **PROUVÉ** | Section 3 (le hasard mesure le plancher) |\n",
"| Beck–Fiala (1981) | $\\le 2k - 1$ | **PROUVÉ** (arrondi flottant) | Section 4 (implémenté et mesuré) |\n",
"| Conjecture de Beck–Fiala | $O(\\sqrt{k})$ | **OUVERT** en général | — |\n",
"| Conjecture de Beck–Fiala | $O(\\sqrt{k})$ | **RÉSOLUTION ANNONCÉE 2026** — $< 3\\sqrt{2\\pi t}$, preprint non revu | — |\n",
"| Banaszczyk (1998) | $O(\\sqrt{k \\log n})$ | **PROUVÉ** (mesure gaussienne de corps convexes) | — |\n",
"| Spencer, « six deviations suffice » (1986) | $O(\\sqrt{n})$ pour $m = n$ | **PROUVÉ** (entropie partielle) | Exercice 2 |\n",
"| **Bansal–Jiang 2025** ([arXiv:2508.03961](https://arxiv.org/abs/2508.03961)) | $O(\\sqrt{k})$ dès $k \\ge \\log^2 n$ ; $\\tilde O(\\sqrt{k} + \\sqrt{\\log n})$ en dessous | **PROUVÉ** — **résout la conjecture pour $k \\ge \\log^2 n$** | — |\n",
"| Komlós (colonnes unitaires) | conjecture $O(1)$ ; Banaszczyk $O(\\sqrt{\\log n})$ ; **2025 : $\\tilde O(\\log^{1/4} n)$** | **OUVERT** à $O(1)$ | Exercice 3 |\n",
"| Komlós (colonnes unitaires) | conjecture $O(1)$ ; Banaszczyk $O(\\sqrt{\\log n})$ ; 2025 : $\\tilde O(\\log^{1/4} n)$ ; **2026 : $< 3\\sqrt{2\\pi} \\approx 7{,}52$ annoncé** | **RÉSOLUTION ANNONCÉE 2026** (non revue) | Exercice 3 |\n",
"| **Guo–Fang–Lu 2026** ([arXiv:2609.11189](https://arxiv.org/abs/2609.11189)) | $\\ell_\\infty < 3\\sqrt{2\\pi}$ (Komlós, universelle) ; $< 3\\sqrt{2\\pi t}$ (Beck–Fiala, degré $t$) | **RÉSOLUTION ANNONCÉE** — preprint du 10/09/2026, **non revu par les pairs** | — |\n",
"\n",
"**Ce qu'apporte 2025.** Tout dans Bansal–Jiang est **algorithmique** (polynomial) : une\n",
"relaxation **SDP** suivie d'un **arrondi par mouvement brownien discret guidé**. La nouveauté\n",
Expand All @@ -522,10 +523,17 @@
"qui relie ce notebook au reste du parcours ; les ponts (funnel PyMC, double-Q des\n",
"métaheuristiques, anti-fantôme ICT) sont rassemblés en section 7.\n",
"\n",
"La frontière est honnête : en dessous de $k \\ge \\log^2 n$ et pour la conjecture Komlós\n",
"$O(1)$, le problème reste ouvert ; l'étage amont (mesure gaussienne, dualité SDP, concentration\n",
"matricielle) n'est pas formalisé dans Mathlib — c'est la raison d'être du jumeau formel\n",
"[`discrepancy_lean/`](discrepancy_lean/) (livrable B de l'issue #12823)."
"**Ce qu'annonce 2026.** Le preprint [arXiv:2609.11189](https://arxiv.org/abs/2609.11189) (Guo–Fang–Lu,\n",
"10/09/2026) annonce une somme signée de norme $\\ell_\\infty < 3\\sqrt{2\\pi} \\approx 7{,}52$\n",
"pour Komlós — indépendamment de la dimension — et $< 3\\sqrt{2\\pi t}$ pour Beck–Fiala au\n",
"degré $t$ : la dépendance en $\\sqrt{t}$ que la conjecture prédit. Statut d'**annoncé**, pas\n",
"d'acquis : le papier a quelques jours et **n'est pas revu par les pairs**, et la preuve est\n",
"**existentielle** (constante non optimale, pas d'algorithme polynomial revendiqué). Détail\n",
"réflexif pour une série d'IA : l'abstract crédite la découverte à un *« Automatic AI Research\n",
"Agent »* (Odin). Côté formel, la route annoncée (variation totale directionnelle, transformée de\n",
"Banaszczyk) **déplace** l'étage manquant plutôt qu'elle ne le contourne — rien n'en existe dans\n",
"Mathlib, et le jumeau formel [`discrepancy_lean/`](discrepancy_lean/) garde ses conjectures en\n",
"`Prop` nommées jusqu'à l'écho communautaire (livrable B de l'issue #12823)."
]
},
{
Expand Down Expand Up @@ -820,8 +828,9 @@
"(la discrépance mesure toujours $\\|Ax\\|_\\infty$). Générez $n$ vecteurs unitaires aléatoires\n",
"dans $\\mathbb{R}^m$ ($m = 8$, $n = 40$), mesurez le meilleur coloriage aléatoire et l'arrondi\n",
"Beck–Fiala *adapté* (le degré n'a plus de sens : que prendre comme seuil d'activité ?).\n",
"Comparez à $\\sqrt{\\log n}$ (Banaszczyk) et $\\log^{1/4} n$ (Bansal–Jiang 2025) : quelles\n",
"échelles observez-vous ?"
"Comparez à $\\sqrt{\\log n}$ (Banaszczyk), à $\\log^{1/4} n$ (Bansal–Jiang 2025) et à la\n",
"constante universelle annoncée $3\\sqrt{2\\pi} \\approx 7{,}52$ (Guo–Fang–Lu 2026, preprint non\n",
"revu) : quelles échelles observez-vous ?"
]
},
{
Expand Down Expand Up @@ -875,16 +884,20 @@
"produit $\\Theta(\\sqrt{k})$ et aucune méthode ne peut espérer $o(\\sqrt{k})$ — la conjecture de\n",
"Beck–Fiala est serrée. **L'algorithme** : l'arrondi flottant fige les variables une à une dans\n",
"des directions qui ne dérangent aucune ligne active — une garantie déterministe $2k-1$, mesurée\n",
"ici très en deçà de sa borne. **La frontière 2025** : Bansal–Jiang closent la conjecture pour\n",
"ici très en deçà de sa borne. **La frontière** : Bansal–Jiang (2025) closent la conjecture pour\n",
"$k \\ge \\log^2 n$ par un découplage spectral affine qui empêche les dérives de conspirer — le\n",
"même geste anti-conspiracy que le double-Q et l'anti-fantôme d'ICT rencontrent ailleurs dans\n",
"ce parcours.\n",
"ce parcours — et un preprint de septembre 2026 (Guo–Fang–Lu, arXiv:2609.11189) annonce la\n",
"résolution générale à constante universelle $3\\sqrt{2\\pi}$ : **annoncée**, pas encore revue —\n",
"le jumeau formel garde ses `Prop` en attendant l'écho communautaire.\n",
"\n",
"**Références.** Beck, J., & Fiala, T. (1981). « Integer-making theorems ». *Discrete Applied\n",
"Mathematics* 3(1). — Matoušek, J. (2002). *Lectures on Discrete Geometry*, Ch. 1 (Thm 1.3.1).\n",
"— Spencer, J. (1986). « Ten Lectures on the Probabilistic Method ». — Banaszczyk, W. (1998).\n",
"« Balancing vectors and Gaussian chaos ». — Bansal, N., & Jiang, H. (2025).\n",
"[arXiv:2508.03961](https://arxiv.org/abs/2508.03961).\n",
"[arXiv:2508.03961](https://arxiv.org/abs/2508.03961). — Guo, S., Fang, E. X., & Lu, J. (2026).\n",
"« Vector Balancing via Directional Total Variation », [arXiv:2609.11189](https://arxiv.org/abs/2609.11189)\n",
"(preprint, résolution annoncée non revue).\n",
"\n",
"Voir [Search-03c (LDS)](../Part1-Foundations/Search-03c-LimitedDiscrepancySearch.ipynb) pour la désambiguïsation,\n",
"le [README de la Partie 1](README.md) pour la suite, et [`discrepancy_lean/`](discrepancy_lean/)\n",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
"\n",
"La cible centrale est le module `Discrepancy/Komlos.lean` — invisible d'aucun notebook avant\n",
"celui-ci — qui porte la frontière SOTA du sujet : la **conjecture de Komlós** (matrices à colonnes\n",
"unitaires, `O(1)` conjecturé, ouverte) et les formes du papier **Bansal–Jiang 2025**\n",
"unitaires, `O(1)` conjecturé — résolution **annoncée** par un preprint de septembre 2026, non revu) et les formes du papier **Bansal–Jiang 2025**\n",
"([arXiv:2508.03961](https://arxiv.org/abs/2508.03961)), premières à dépasser Banaszczyk.\n",
"\n",
"**Trois « discrépances », une désambiguïsation** : la *Limited Discrepancy Search* de\n",
Expand Down Expand Up @@ -68,17 +68,22 @@
"| Résultat | Régime | Borne | Statut |\n",
"|---|---|---|---|\n",
"| Beck–Fiala (classique) | degré `≤ k` | `disc ≤ 2k − 1` | **théorème** (prouvé) |\n",
"| Beck–Fiala (conjecture) | degré `≤ k` | `O(√k)` | conjecture ouverte |\n",
"| Beck–Fiala (conjecture) | degré `≤ k` | `O(√k)` | résolution **annoncée** 2026 (non revue) |\n",
"| Banaszczyk (1998) | colonnes unitaires | `O(√(log n))` | théorème |\n",
"| **Bansal–Jiang (2025)** | `k ≥ (log n)²` | `O(√k)` | théorème (papier) |\n",
"| **Bansal–Jiang (2025)** | colonnes unitaires | `Õ(log^(1/4) n)` | théorème (papier) |\n",
"| **Komlós** | colonnes unitaires | `O(1)` | **conjecture ouverte** |\n",
"| **Komlós** | colonnes unitaires | `O(1)` ; **annoncé `< 3√(2π) ≈ 7,52`** | résolution **annoncée** 2026 (non revue) |\n",
"| **Guo–Fang–Lu (2026)** | degré `≤ k` et colonnes unitaires | `< 3√(2πt)` et `< 3√(2π)` | **annoncé** (preprint non revu) |\n",
"\n",
"La formalisation doit dire la vérité sur ce qu'elle sait : les preuves de Bansal–Jiang exigent un\n",
"étage absent de Mathlib (SDP et dualité, indépendance spectrale affine, mouvement brownien discret\n",
"guidé, concentration matricielle). Le lake choisit donc d'énoncer les conjectures comme des\n",
"**`Prop` nommées** — des énoncés exacts, citables, vérifiables de type — dont les preuves\n",
"attendront l'étage amont. Aucun `sorry` maquillé en théorème : la frontière est déclarée frontière.\n",
"Le preprint de septembre 2026 qui annonce la résolution des deux conjectures ([arXiv:2609.11189](https://arxiv.org/abs/2609.11189),\n",
"non revu) ne change pas ce contrat : sa route — variation totale directionnelle, transformée de\n",
"Banaszczyk — **déplace** l'obstruction au lieu de la contourner, et cet étage n'existe pas\n",
"davantage dans Mathlib.\n",
"\n",
"Chargeons le lake dans le noyau."
]
Expand Down Expand Up @@ -381,7 +386,10 @@
" que toute matrice à colonnes unitaires admette une coloration `±1` bornant chaque somme de ligne\n",
" par `C`. L'hypothèse `∀ j, ∑ i, A i j * A i j = 1` est la condition *unitaire* : chaque colonne\n",
" est un vecteur de norme 1. C'est l'énoncé de Komlós, ouvert depuis les années 1970 — Banaszczyk\n",
" n'en a que `O(√(log n))`.\n",
" n'en a que `O(√(log n))`. Un preprint de septembre 2026 (arXiv:2609.11189, non revu) annonce\n",
" la constante universelle `3√(2π) ≈ 7,52` — sur `ℝ` ; l'énoncé ci-dessus reste une `Prop`, posé\n",
" sur `ℚ` avec `C : ℚ` : tout alignement futur devra choisir un témoin rationnel explicite\n",
" (`8` convient).\n",
"- **`BansalJiangLargeDegree`** change de régime : `∃ C : ℕ, ∀ n k (F : Finset (Finset (Fin n)))`,\n",
" avec **deux hypothèses** — degré `maxDegree F ≤ k` *et* `(Nat.log 2 n)² ≤ k` — pour la même\n",
" conclusion `O(√k)` que la conjecture de Beck–Fiala. Le papier prouve que la conjecture vaut dès\n",
Expand Down Expand Up @@ -2487,7 +2495,9 @@
" vie d'heuristique de parcours — sans rapport ;\n",
"- le lake [discrepancy_lean](../discrepancy_lean/README.md) garde ses conjectures en `Prop` nommée :\n",
" quand l'étage SDP existera en Mathlib, la preuve remplacera la déclaration sans changer\n",
" l'énoncé — et ce notebook montrera le basculement."
" l'énoncé — et ce notebook montrera le basculement. L'annonce de septembre 2026 (résolution à\n",
" constante universelle, preprint non revu) ne change pas ce contrat : sa route exige un autre\n",
" étage absent de Mathlib, et les `Prop` attendent toujours une preuve formelle."
]
}
],
Expand Down
Loading