feat(lean,#17845): brique k1.3 — opérateur overlap + identités de base (stack sur #19058)

MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Overlap.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2026 Gabriel Dahia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Dahia
+Adapted to `discrepancy_lean` (issue #17845, Karingula–Lovett distillation
+arXiv:2609.20979) : toolchain v4.33.0, Mathlib `db584cd6`, convention i18n #4980.
+
+Le source Dahia original vit dans le dépôt `gdahia/Komlos` (module
+`Komlos/ShiftDistance.lean`, toolchain v4.34.0, cadre `Finsupp` sur `E →₀ ℝ`,
+`overlap P Q = mass (P ⊓ Q)` avec `tvDist` et `shiftDist` dans le même
+module). L'adaptation ci-dessous suit la convention du lake établie par la
+brique k1.1 (`ShiftDistance.lean`) : cadre **Finset explicite**
+`P : (Fin d → ℤ) → ℝ` avec support `S` passé en argument — l'infimum de
+Finsupp devient le `min` ponctuel, le support devient un argument explicite,
+sans `Finsupp` ni ordre pointillé.
+
+**Portée de ce commit** (brique k1.3, `lake build SUCCESS` requis, 0
+`sorry`) :
+
+Briques closes : `overlap` (opérateur de recouvrement), `overlap_comm`,
+`overlap_self` (le recouvrement d'une fonction avec elle-même est sa masse),
+`overlap_nonneg`, `overlap_mono`, `overlap_le_sum_left`, `overlap_le_sum_right`
+(le recouvrement est dominé par chaque masse), `sum_le_overlap` (toute
+fonction sous-minorée par les deux arguments est dominée par le
+recouvrement — `mass_le_overlap` chez Dahia), `min_eq_half_add_sub_abs`
+(l'identité ponctuelle `min a b = ½ (a + b − |a − b|)` — la brique locale de
+l'identité pivot).
+
+**Reporté à k1.4** : l'identité pivot `overlap P (P ∘ (· + u)) = 1 − Δ(P, u)`
+sous masse 1 et invariance du support par `u` (exige la ré-indexation
+`sum_translate_image` de k1.2 et la convention forward de `ShiftDistance`) ;
+`overlap_tr` (invariance du recouvrement par translation commune, même
+chemin) ; Claim 3.2 (`Δ(T_v P, (u, 0)) ≤ Δ(P, u)`) et `split_tr` (suivent
+l'identité pivot). L'état détaillé vit dans `FORMAL_STATUS.md`.
+-/
+
+import Discrepancy.Basic
+
+/-!
+# Opérateur de recouvrement `overlap` (Karingula–Lovett)
+
+`Discrepancy.Komlos.overlap P Q S` est la somme des minima ponctuels
+`min (P x) (Q x)` sur le support fini explicite `S` : la **masse commune**
+de `P` et `Q`. Pour deux distributions de probabilité, le recouvrement
+vaut `1 − tvDist` (identité pivot reportée à k1.4) — c'est la quantité que
+la preuve élémentaire de Komlós fait passer de `P` à sa translate, puis
+contrôle à travers la scission `split` (k1.2).
+
+Cette brique ne suppose que `Discrepancy.Basic` (aucune dépendance sur
+`ShiftDistance` ou `Split` : elle se situe en amont de l'identité pivot).
+Le pin Mathlib `db584cd6` est dans la cohorte fleet v4.32.1
+(mutualisation #4363) ; l'écart avec la toolchain locale v4.33.0 est pris
+en charge par `lake build`.
+-/
+
+namespace Discrepancy.Komlos
+
+/-- Opérateur de recouvrement : la somme des minima ponctuels sur le
+support explicite `S`. C'est le `Komlos.overlap P Q = mass (P ⊓ Q)` de
+Dahia transposé au cadre Finset du lake — la masse commune de `P` et `Q`,
+sans `Finsupp` artificiel. -/
+noncomputable def overlap {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) : ℝ := ∑ x ∈ S, min (P x) (Q x)
+
+/-- Symétrie du recouvrement : `min` est commutatif terme à terme. -/
+lemma overlap_comm {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S = overlap Q P S := by
+  unfold overlap
+  exact Finset.sum_congr rfl (fun x _ => min_comm (P x) (Q x))
+
+/-- Le recouvrement d'une fonction avec elle-même est sa masse sur `S`. -/
+lemma overlap_self {d : ℕ} (P : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P P S = ∑ x ∈ S, P x := by
+  unfold overlap
+  exact Finset.sum_congr rfl (fun x _ => min_self (P x))
+
+/-- Positivité : le recouvrement de deux fonctions positives sur `S` est
+positif. -/
+lemma overlap_nonneg {d : ℕ} {P Q : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hP : ∀ x ∈ S, 0 ≤ P x) (hQ : ∀ x ∈ S, 0 ≤ Q x) :
+    0 ≤ overlap P Q S := by
+  unfold overlap
+  exact Finset.sum_nonneg (fun x hx => le_min (hP x hx) (hQ x hx))
+
+/-- Monotonie en les deux arguments : le recouvrement transporte l'ordre
+ponctuel. -/
+lemma overlap_mono {d : ℕ} {P P' Q Q' : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hP : ∀ x ∈ S, P x ≤ P' x) (hQ : ∀ x ∈ S, Q x ≤ Q' x) :
+    overlap P Q S ≤ overlap P' Q' S := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x hx => min_le_min (hP x hx) (hQ x hx))
+
+/-- Le recouvrement est dominé par chaque masse. -/
+lemma overlap_le_sum_left {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S ≤ ∑ x ∈ S, P x := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x _ => min_le_left (P x) (Q x))
+
+/-- Variante symétrique : le recouvrement est dominé par la seconde
+masse. -/
+lemma overlap_le_sum_right {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S ≤ ∑ x ∈ S, Q x := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x _ => min_le_right (P x) (Q x))
+
+/-- Toute fonction sous-minorée par les deux arguments est dominée par le
+recouvrement (`mass_le_overlap` chez Dahia) : la masse commune majore
+toute masse partagée. C'est le sens qui servira à k1.4 pour minorer le
+recouvrement par la masse conservée par la scission. -/
+lemma sum_le_overlap {d : ℕ} {R P Q : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hRP : ∀ x ∈ S, R x ≤ P x) (hRQ : ∀ x ∈ S, R x ≤ Q x) :
+    ∑ x ∈ S, R x ≤ overlap P Q S := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x hx => le_min (hRP x hx) (hRQ x hx))
+
+/-- Identité ponctuelle du minimum : `min a b = ½ (a + b − |a − b|)` — la
+brique locale de l'identité pivot `overlap = 1 − tvDist` (k1.4) : sommée
+terme à terme, elle relie recouvrement et distance de translation. -/
+lemma min_eq_half_add_sub_abs (a b : ℝ) :
+    min a b = (1 / 2 : ℝ) * (a + b - |a - b|) := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, abs_of_nonpos (by linarith)]
+    ring
+  · rw [min_eq_right h, abs_of_nonneg (by linarith)]
+    ring
+
+end Discrepancy.Komlos

MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Overlap_en.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Gabriel Dahia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Dahia
+Adapted to `discrepancy_lean` (issue #17845, Karingula–Lovett distillation
+arXiv:2609.20979) : toolchain v4.33.0, Mathlib `db584cd6`, convention i18n #4980.
+
+The original Dahia source lives in `gdahia/Komlos` (module
+`Komlos/ShiftDistance.lean`, toolchain v4.34.0, `Finsupp` framework over
+`E →₀ ℝ`, `overlap P Q = mass (P ⊓ Q)` with `tvDist` and `shiftDist` in the
+same module). The adaptation below follows the lake convention established
+by brick k1.1 (`ShiftDistance.lean`) : **explicit Finset** framework
+`P : (Fin d → ℤ) → ℝ` with the support `S` passed as an argument — the
+Finsupp infimum becomes the pointwise `min`, the support becomes an explicit
+argument, without `Finsupp` or dotted order.
+
+**Scope of this commit** (brick k1.3, `lake build SUCCESS` required, 0
+`sorry`) :
+
+Bricks closed : `overlap` (overlap operator), `overlap_comm`, `overlap_self`
+(the overlap of a function with itself is its mass), `overlap_nonneg`,
+`overlap_mono`, `overlap_le_sum_left`, `overlap_le_sum_right` (the overlap
+is dominated by each mass), `sum_le_overlap` (any function bounded above by
+both arguments is dominated by the overlap — `mass_le_overlap` in Dahia),
+`min_eq_half_add_sub_abs` (the pointwise identity
+`min a b = ½ (a + b − |a − b|)` — the local brick of the pivot identity).
+
+**Postponed to k1.4** : the pivot identity
+`overlap P (P ∘ (· + u)) = 1 − Δ(P, u)` under mass 1 and invariance of the
+support by `u` (requires the re-indexing `sum_translate_image` from k1.2 and
+the forward convention of `ShiftDistance`) ; `overlap_tr` (invariance of
+the overlap under a common translation, same path) ; Claim 3.2
+(`Δ(T_v P, (u, 0)) ≤ Δ(P, u)`) and `split_tr` (both follow the pivot
+identity). The detailed state lives in `FORMAL_STATUS.md`.
+-/
+
+import Discrepancy.Basic
+
+/-!
+# Overlap operator `overlap` (Karingula–Lovett)
+
+`Discrepancy.Komlos_en.overlap P Q S` is the sum of the pointwise minima
+`min (P x) (Q x)` over the explicit finite support `S` : the **common
+mass** of `P` and `Q`. For two probability distributions the overlap
+equals `1 − tvDist` (pivot identity postponed to k1.4) — it is the
+quantity that the elementary proof of Komlós carries from `P` to its
+translate, then controls through the splitting `split` (k1.2).
+
+This brick only assumes `Discrepancy.Basic` (no dependency on
+`ShiftDistance` or `Split` : it sits upstream of the pivot identity).
+The Mathlib pin `db584cd6` is in the fleet cohort v4.32.1
+(mutualisation #4363) ; the gap with the local toolchain v4.33.0 is
+handled by `lake build`.
+-/
+
+namespace Discrepancy.Komlos_en
+
+/-- Overlap operator : the sum of pointwise minima over the explicit
+support `S`. This is Dahia's `Komlos.overlap P Q = mass (P ⊓ Q)`
+transposed to the Finset framework of the lake — the common mass of `P`
+and `Q`, without artificial `Finsupp`. -/
+noncomputable def overlap {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) : ℝ := ∑ x ∈ S, min (P x) (Q x)
+
+/-- Symmetry of the overlap : `min` is commutative termwise. -/
+lemma overlap_comm {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S = overlap Q P S := by
+  unfold overlap
+  exact Finset.sum_congr rfl (fun x _ => min_comm (P x) (Q x))
+
+/-- The overlap of a function with itself is its mass over `S`. -/
+lemma overlap_self {d : ℕ} (P : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P P S = ∑ x ∈ S, P x := by
+  unfold overlap
+  exact Finset.sum_congr rfl (fun x _ => min_self (P x))
+
+/-- Nonnegativity : the overlap of two nonnegative functions over `S` is
+nonnegative. -/
+lemma overlap_nonneg {d : ℕ} {P Q : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hP : ∀ x ∈ S, 0 ≤ P x) (hQ : ∀ x ∈ S, 0 ≤ Q x) :
+    0 ≤ overlap P Q S := by
+  unfold overlap
+  exact Finset.sum_nonneg (fun x hx => le_min (hP x hx) (hQ x hx))
+
+/-- Monotonicity in both arguments : the overlap transports the pointwise
+order. -/
+lemma overlap_mono {d : ℕ} {P P' Q Q' : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hP : ∀ x ∈ S, P x ≤ P' x) (hQ : ∀ x ∈ S, Q x ≤ Q' x) :
+    overlap P Q S ≤ overlap P' Q' S := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x hx => min_le_min (hP x hx) (hQ x hx))
+
+/-- The overlap is dominated by each mass. -/
+lemma overlap_le_sum_left {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S ≤ ∑ x ∈ S, P x := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x _ => min_le_left (P x) (Q x))
+
+/-- Symmetric variant : the overlap is dominated by the second mass. -/
+lemma overlap_le_sum_right {d : ℕ} (P Q : (Fin d → ℤ) → ℝ)
+    (S : Finset (Fin d → ℤ)) :
+    overlap P Q S ≤ ∑ x ∈ S, Q x := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x _ => min_le_right (P x) (Q x))
+
+/-- Any function bounded above by both arguments is dominated by the
+overlap (`mass_le_overlap` in Dahia) : the common mass majorates any
+shared mass. This is the direction k1.4 will use to lower-bound the
+overlap by the mass preserved through splitting. -/
+lemma sum_le_overlap {d : ℕ} {R P Q : (Fin d → ℤ) → ℝ}
+    {S : Finset (Fin d → ℤ)}
+    (hRP : ∀ x ∈ S, R x ≤ P x) (hRQ : ∀ x ∈ S, R x ≤ Q x) :
+    ∑ x ∈ S, R x ≤ overlap P Q S := by
+  unfold overlap
+  exact Finset.sum_le_sum (fun x hx => le_min (hRP x hx) (hRQ x hx))
+
+/-- Pointwise identity for the minimum : `min a b = ½ (a + b − |a − b|)` —
+the local brick of the pivot identity `overlap = 1 − tvDist` (k1.4) :
+summed termwise, it connects the overlap and the translation distance. -/
+lemma min_eq_half_add_sub_abs (a b : ℝ) :
+    min a b = (1 / 2 : ℝ) * (a + b - |a - b|) := by
+  rcases le_total a b with h | h
+  · rw [min_eq_left h, abs_of_nonpos (by linarith)]
+    ring
+  · rw [min_eq_right h, abs_of_nonneg (by linarith)]
+    ring
+
+end Discrepancy.Komlos_en

MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md

@@ -54,6 +54,7 @@ boutes `k1..k5` ci-dessous ; issue de suivi : #17845.
 | p4 (contrôle du degré + assemblage) | `rademacherSum_eq_two_sub` (identité Z = 2·(somme des coords vraies) − somme totale, pont alea signé ↔ sommes d'ensembles), `blockOf`/`drawSet`/`pairFamily` (bloc de t = k/12 points via `Fin.castLEEmb`, tirage → coordonnées vraies, FAMILLE APPARIÉE (drawSet, bloc \\ drawSet)), `blockOf_sum`/`drawSet_sum`/`drawSet_subset`, `drawSet_mem`/`compDraw_mem`, `degree_pairFamily_le` (degré ≤ m par injection vers `Finset.range m` : chaque paire est disjointe donc un point apparaît au plus une fois par tirage), et le THÉORÈME FINAL `erdos_spencer_lb_explicit` : ∀ n k ≥ 1, k ≤ n → ∃ F, maxDegree F ≤ k ∧ ∀ C coloration, Nat.sqrt k ≤ 14 * discrepancy F C — petit k < 12 singletons, gros k = 12 tirages par bloc de k/12 points, triangulaire \|Z\| ≤ \|x\| + \|x−s\| ≤ 2·disc, k ≤ 23t ≤ 184·disc² | brique P2 | **PROUVÉ** (p4, 08-26, axiomes [propext, Classical.choice, Quot.sound]) | **P2 EST ASSEMBLÉ** à constante explicite √k/14 ; la forme optimiste √k/2 (`ErdosSpencerLB`) reste une `Prop` OUVERTE (obstruction structurelle : Paley–Zygmund force m ≥ 12t tirages, degré force m ≤ k — documenté dans le statut du module) |
 | **k1.1** | `Discrepancy.Komlos.shiftDistance` (Def 1.3, Karingula–Lovett) : Δ(P, u) = ½ · Σ_x \|P(x + u) − P(x)\| (convention **forward**, pas backward). Identités closes : `shiftDistance_zero` (u=0 ⇒ Δ=0), `shiftDistance_nonneg` (Δ ≥ 0). **Reporté à k1.2** : `shiftDistance_symm` (exige invariance du support `S = S.image (· + u)`), `shiftDistance_eq_zero_of_zero` (réécriture `(1/2)*0 = 0` après `Finset.sum_eq_zero_iff_of_nonneg` subtile), `shiftDistance_le_one` (typeclass `(0 : ℝ) ≤ (1/2 : ℝ)` non résolu en Lean 4 v4.33.0 sans `Mathlib` étendu). 3 briques livrées au lieu de 6 initialement visées, 0 `sorry`. | brique k1 (tranche 1/2) | **PROUVÉ** (k1.1, 09-30, Lean CI PASS run 36791564415) | branche `feature/17845-k2-lemme-1-4` (PR #18630) |
 | **k1.2** | `Discrepancy.Komlos.split` (Def 3.1, Karingula–Lovett) : opérateur de scission `T_v` sur `(ℤ^d) × Bool` — tranche `false` = ½·max{P(x+v), P(x−v)}, tranche `true` = ½·min (cadre Finset du lake, hauteur `Bool` ; Dahia : `Finsupp`, hauteur `E × ℝ`). Identités closes : `split_apply_zero`, `split_apply_one`, `split_nonneg`, `sum_invariance_image` (ré-indexation générique `Σ P(f x) = Σ P(x)` sous invariance `S.image f = S` pour `f` injective — la brique de télescopage identifiée manquante à `shiftDistance_symm` ; cas additif `sum_translate_image` pour k1.3), `split_mass` (préservation de la masse `Σ_{S×{0,1}} T_vP = Σ_S P` sous invariance `±v`), `split_mono` (monotonie ponctuelle). **Reporté à k1.3** : Claim 3.2 (`Δ(T_vP, (u,0)) ≤ Δ(P,u)`) via l'identité `Δ = 1 − overlap` (l'opérateur `overlap` n'est pas encore distillé) ; `split_tr` (commutation scission ∘ translation, même dépendance) ; les trois identités `shiftDistance_*` restent reportées (elles vivent dans `ShiftDistance.lean`). 0 `sorry`. | brique k1 (tranche 2/2) | **PROUVÉ** (k1.2, 10-04, `lake build` local EXIT=0 — voir PR) | ce PR |
+| **k1.3** | `Discrepancy.Komlos.overlap` : opérateur de recouvrement `overlap P Q S = ∑_{x∈S} min (P x) (Q x)` — la masse commune (Dahia : `mass (P ⊓ Q)` sur `E →₀ ℝ`, module commun avec `tvDist`/`shiftDist`). Identités closes : `overlap_comm`, `overlap_self` (= masse), `overlap_nonneg`, `overlap_mono`, `overlap_le_sum_left/right`, `sum_le_overlap` (`mass_le_overlap` chez Dahia), `min_eq_half_add_sub_abs` (`min a b = ½(a+b−|a−b|)` — brique de l'identité pivot). **Reporté à k1.4** : identité pivot `overlap P (P∘(·+u)) = 1 − Δ(P,u)` (exige `sum_translate_image` k1.2 + convention forward de `ShiftDistance`) ; `overlap_tr` ; Claim 3.2 (`Δ(T_vP,(u,0)) ≤ Δ(P,u)`) ; `split_tr`. 0 `sorry`. | brique k1 (amont pivot) | **PROUVÉ** (k1.3, 10-04, `lake build` local EXIT=0 — voir PR) | ce PR (stack sur #19058) |
 | P3 | Banaszczyk 1998 / formes fortes des papiers 2025 **et 2026** | aspiration | **NON ENGAGÉ** — exige SDP + dualité, indépendance spectrale affine, brownien discret guidé, concentration matricielle : **aucun de cet étage n'existe dans Mathlib** (vérifié 2026-08-24). **Réaudité 2026-09-13** contre le Mathlib pinné (`520045ab`, v4.32.1) : le contournement proposé par arXiv:2609.11189 ne supprime pas l'obstruction, il la **déplace** — sa route exige la *variation totale directionnelle* d'une densité sur convexe ouvert et la *transformée de Banaszczyk* préservée sous translation, deux notions **absentes du même Mathlib** (`Banaszczyk` : 0 occurrence ; `totalVariation` n'existe que pour les mesures signées ; la théorie BV de Mathlib concerne la dérivabilité a.e. des fonctions de `ℝ`). Ce que ce papier rapproche, ce sont les *socles* : gaussiennes (`Probability/Distributions/Gaussian/*`) et `ConvexBody` (`Analysis/Convex/Body.lean`) sont présents ; le **pont** manque. Documenté, jamais promis. **Réaudité 2026-09-25** : la voie **élémentaire** de Karingula–Lovett (arXiv:2609.20979, constante `36`) **supprime** cet étage au lieu de le déplacer — sa mécanique est discrète (distance de décalage `Δ`, opérateur de scission `T_v`, induction sur `n` et `d`) à une seule exception, l'estimation de la densité-tente, qui se fait par FTC sur segments + Cauchy–Schwarz `L²` et **non** par de la théorie BV. Balayage des prérequis sur le checkout Mathlib local (`v4.32.0`) : famille **`norm_image_sub_le` présente** (dont `Analysis/Calculus/IntervalIntegral/DistLEIntegral.lean`), `totalVariation` toujours cantonné aux mesures vectorielles (`VectorMeasure/Decomposition/*`) — mais le papier n'en a plus besoin. Réserve de portée : ce balayage porte sur un checkout **voisin** (`v4.32.0`), pas sur le pin du lake (`520045ab`) — à re-vérifier avant la première boute `.lean`. Une formalisation Lean 4 tierce de cette preuve existe déjà (mise à jour du 2026-09-25 ci-dessous). | — |
 | probe-15944 (réduction, cas régulier) | `komlos_oracle_imp_beck_fiala_regular` (`Komlos.lean` + sibling `_en`) : tout oracle de Komlós **réel** (colonnes unitaires, sommes de lignes `≤ C` en valeur absolue) implique `disc ≤ 2⌈C⌉₊ · Nat.sqrt k` pour toute famille **régulière** (chaque élément dans exactement `k` parties). Scaling uniforme `1/√k` licite car tous degrés égaux ; conversion `ℝ → ℕ` par `√k ≤ Nat.sqrt k + 1`. | brique P3 (pont) | **PROUVÉ** (2026-09-17) | Première brique du pont vers l'oracle du preprint 2026 : avec `C = 3√(2π)` (borne annoncée arXiv:2609.11189, non revue), les familles de degré exactement `t` admettent `disc ≤ 16√t` — **conditionnellement** au preprint. Cas général bloqué par deux obstructions mesurées : degrés hétérogènes (le scaling par colonne `1/√(deg j)` rend la somme colorée pondérée non factorisable — la réduction connue exige la coloration partielle itérée) et l'énoncé `ℚ` de `KomlosConjecture` (scaling irrationnel ; la forme réelle est le pont naturel). |