From 39aa4360e83a55fec3597b387d4972d7fc8ef7eb Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 6 Oct 2026 20:49:05 +0200 Subject: [PATCH] feat(lean,#17845): tranche k3 -- Komlos/Tent.lean complet (13 preuves reportees, 0 sorry) Port integral du Tent.lean de l'oracle (gdahia/Komlos) au pin v4.33.0/db584cd6 : sum_tent, sum_tent_sq, abs_tent_sub_le, step, abs_step_le_one, step_eq_zero, sum_step_sq_le, tent_sub_tent_eq_sum_step, sum_tent_sub_sq_le_nat/_le (borne L2 discrete du Lemme 4.1), support_tent_subset, Icc_neg_add_one, sum_Icc_comp_tent_add_one. lake build SUCCESS sur les deux jumeaux, i18n byte-identical, distinct_code_sorry 0 -> 0 (additif). Ligne FORMAL_STATUS k3.1 + reaudit k3 : la voie oracle est totalement discrete (Grid.lean ensuite). Co-Authored-By: Claude Sonnet 5.5 --- .../Discrepancy/Komlos/Tent.lean | 273 +++++++++++++--- .../Discrepancy/Komlos/Tent_en.lean | 304 ++++++++++++++---- .../Search/discrepancy_lean/FORMAL_STATUS.md | 3 +- 3 files changed, 469 insertions(+), 111 deletions(-) diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent.lean index 95675348a3..f76c59b54d 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent.lean +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent.lean @@ -13,42 +13,41 @@ Mathlib v4.34.0). L'adaptation ci-dessous vise v4.33.0 / Mathlib `db584cd6` : - les preuves qui dépendent de lemmes absents en v4.33.0 sont réécrites avec les équivalents stables. -**Portée de ce commit** (brique minimale compilable, `lake build SUCCESS` -requis pour passer la gate du module racine — convention anti-régression -D, 0 `sorry`) : +**Portée de ce commit** (tranche k3 complète du fichier `Tent.lean` de +l'oracle — `lake build SUCCESS` requis pour passer la gate du module racine — +convention anti-régression D, 0 `sorry`) : Briques closes : `tent`, `tent_nonneg`, `tent_neg`, `tent_zero`, -`tent_eq_zero`, `tent_of_abs_le`, `tent_add_one`, `card_Icc_neg`. +`tent_eq_zero`, `tent_of_abs_le`, `support_tent_subset`, `tent_add_one`, +`card_Icc_neg`, `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one`, `sum_tent`, +`sum_tent_sq`, `abs_tent_sub_le`, `step`, `abs_step_le_one`, `step_eq_zero`, +`sum_step_sq_le`, `tent_sub_tent_eq_sum_step`, `sum_tent_sub_sq_le_nat`, +`sum_tent_sub_sq_le`. -**Reporté à c.886+** (livraison progressive, preuve par preuve, jamais -`sorry`) : `support_tent_subset`, `Icc_neg_add_one`, -`sum_Icc_comp_tent_add_one`, `sum_tent`, `sum_tent_sq`, -`abs_tent_sub_le`, `step`, `abs_step_le_one`, `step_eq_zero`, -`sum_step_sq_le`, `tent_sub_tent_eq_sum_step`, -`sum_tent_sub_sq_le_nat`, `sum_tent_sub_sq_le`. +Le fichier porte désormais **l'intégralité** du `Komlos/Tent.lean` de Dahia : +les 13 preuves reportées en c.885 sont livrées ici, chacune adaptée du +`grind` v4.34 vers des tactiques disponibles au pin v4.33.0 / `db584cd6` +(détail par preuve dans la note d'adaptation en fin de fichier). L'état détaillé vit dans `FORMAL_STATUS.md` (« Distillation -Karingula–Lovett, briques k1..k5 »). La livraison c.885 est une **graine -structurelle** : la tente est dans le namespace, son support est -caractérisé, et les sommes closes sont identifiées comme prochaine -cible d'induction. +Karingula–Lovett, briques k1..k5 »). -/ import Discrepancy.Basic /-! -# La fonction « tente » discrète (noyau compilable) +# La fonction « tente » discrète `Discrepancy.Komlos.tent M j = max (M - |j|) 0` est la tente de demi-largeur `M` sur `ℤ`. Son carré, après normalisation, donne les poids unidimensionnels utilisés par la grille `Komlos.Grid` dans la distillation Karingula–Lovett (arXiv:2609.20979, sœur de #15944, EPIC #12823). -Ce fichier établit **dans ce commit** la définition et les propriétés de -support / symétrie (9 briques closes). Les sommes closes (`sum_tent`, -`sum_tent_sq`) et les bornes Lipschitz / `L²` sont livrées en c.886+ : -voir la note d'adaptation en fin de fichier et la section correspondante -de `FORMAL_STATUS.md`. +Ce fichier calcule `∑ j, tent M j ^ 2` et prouve +`∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * M * m ^ 2` — la borne `L²` +discrète qui porte le Lemme 4.1 (l'estimation de densité-tente par +Cauchy–Schwarz). Cette dernière s'obtient en exprimant un décalage comme +somme de différences de pas puis en appliquant Cauchy–Schwarz. -/ namespace Discrepancy.Komlos @@ -77,12 +76,16 @@ lemma tent_of_abs_le {M : ℕ} {j : ℤ} (h : |j| ≤ (M : ℤ)) : rw [tent, max_eq_left_iff, sub_nonneg] exact_mod_cast h --- Le support de la tente est inclus dans `[-M, M]`. **Rapporté à --- c.886+** : la preuve directe demande un fold de `Int.abs` dont les noms --- varient entre v4.33.0 et v4.34.0. La version `tent_eq_zero` suffit pour --- les sommes closes : le lemme est documenté pour complétude mais pas --- démontré dans ce commit. --- TODO c.886+ : support_tent_subset avec fold propre de Int.abs. +/-- Le support de la tente est inclus dans `[-M, M]`. -/ +lemma support_tent_subset (M : ℕ) : + Function.support (tent M) ⊆ Set.Icc (-(M : ℤ)) (M : ℤ) := by + intro j hj + by_contra h + simp only [Set.mem_Icc, not_and_or, not_le] at h + rcases h with hj' | hj' + · exact hj (tent_eq_zero + ((by omega : (M : ℤ) ≤ -j).trans ((le_abs_self (-j : ℤ)).trans_eq (abs_neg j)))) + · exact hj (tent_eq_zero ((by omega : (M : ℤ) ≤ j).trans (le_abs_self j))) /-- `tent_add_one` (lemme technique pour l'induction) : sur le support `[-M, M]`, la tente de demi-largeur `M + 1` est la tente de demi-largeur `M` @@ -98,28 +101,202 @@ lemma card_Icc_neg (M : ℕ) : #(Icc (-(M : ℤ)) M) = 2 * M + 1 := by rw [Int.card_Icc] omega -/-! ## Note d'adaptation (livraison progressive) - -**Statut c.885** : 9 briques closes (`tent`, `tent_nonneg`, `tent_neg`, -`tent_zero`, `tent_eq_zero`, `tent_of_abs_le`, `support_tent_subset`, -`tent_add_one`, `card_Icc_neg`). Le module build (`lake build -Discrepancy.Komlos.Tent` SUCCESS), 0 `sorry` en code. - -**Action c.886+** : ajouter `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one`, -`sum_tent`, `sum_tent_sq` (sommes closes), `abs_tent_sub_le`, `step`, -`abs_step_le_one`, `step_eq_zero`, `sum_step_sq_le`, -`tent_sub_tent_eq_sum_step`, `sum_tent_sub_sq_le_nat`, -`sum_tent_sub_sq_le` — preuve par preuve, chacune passe `lake build -SUCCESS` avant commit. L'état détaillé vit dans `FORMAL_STATUS.md` -(« Distillation Karingula–Lovett »). - -**Portage Dahia → v4.33.0** : Dahia exploite intensivement `grind` -(introduit en v4.34.0) pour les preuves de disjonction ensembliste -(`sum_insert (by grind)`) et les tactiques d'arithmétique linéaire -imprécises. Sans `grind`, la voie est : (a) prouver les disjonctions -explicitement via `omega` après unfolding `Icc`, ou (b) réécrire en -termes de `Finset.range` qui ne souffre pas du même problème. C'est -l'objet de c.886+. +/-- `Icc (-(M+1)) (M+1)` est `Icc (-M) M` plus les deux extrémités. -/ +lemma Icc_neg_add_one (M : ℕ) : + Icc (-((M + 1 : ℕ) : ℤ)) ((M + 1 : ℕ) : ℤ) + = insert (-((M + 1 : ℕ) : ℤ)) (insert ((M + 1 : ℕ) : ℤ) (Icc (-(M : ℤ)) (M : ℤ))) := by + ext j + simp only [mem_Icc, mem_insert] + omega + +/-- Passer de la demi-largeur `M` à `M + 1` relève la tente de `1` sur +`[-M, M]` et ajoute deux points de valeur nulle. -/ +lemma sum_Icc_comp_tent_add_one (M : ℕ) (f : ℝ → ℝ) (hf : f 0 = 0) : + ∑ j ∈ Icc (-((M + 1 : ℕ) : ℤ)) ((M + 1 : ℕ) : ℤ), f (tent (M + 1) j) + = ∑ j ∈ Icc (-(M : ℤ)) (M : ℤ), f (tent M j + 1) := by + have h1 : (-((M + 1 : ℕ) : ℤ)) ∉ insert ((M + 1 : ℕ) : ℤ) (Icc (-(M : ℤ)) (M : ℤ)) := by + intro h + rcases mem_insert.1 h with h' | h' + · omega + · simp only [mem_Icc] at h' + omega + have h2 : ((M + 1 : ℕ) : ℤ) ∉ Icc (-(M : ℤ)) (M : ℤ) := by + intro h + simp only [mem_Icc] at h + omega + have e1 : tent (M + 1) (-((M + 1 : ℕ) : ℤ)) = 0 := + tent_eq_zero (by rw [abs_neg]; exact le_abs_self _) + have e2 : tent (M + 1) ((M + 1 : ℕ) : ℤ) = 0 := tent_eq_zero (le_abs_self _) + rw [Icc_neg_add_one, sum_insert h1, sum_insert h2, e1, e2, hf] + simp only [zero_add] + refine sum_congr rfl ?_ + intro j hj + simp only [mem_Icc] at hj + rw [tent_add_one (abs_le.2 ⟨hj.1, hj.2⟩)] + +/-- Somme close : la tente sur son support somme à `M ^ 2`. -/ +lemma sum_tent (M : ℕ) : ∑ j ∈ Icc (-(M : ℤ)) M, tent M j = (M : ℝ) ^ 2 := by + induction M with + | zero => simp + | succ M ih => + have h := sum_Icc_comp_tent_add_one M id (rfl : (id : ℝ → ℝ) 0 = 0) + simp only [id] at h + rw [h] + simp only [sum_add_distrib, ih, sum_const, card_Icc_neg, nsmul_eq_mul] + push_cast + ring + +/-- Somme close : la somme des carrés de la tente vaut `M * (2 * M ^ 2 + 1) / 3` +(écrite ici multipliée par `3` pour rester sans division). -/ +lemma sum_tent_sq (M : ℕ) : + (∑ j ∈ Icc (-(M : ℤ)) M, tent M j ^ 2) * 3 = (M : ℝ) * (2 * (M : ℝ) ^ 2 + 1) := by + induction M with + | zero => norm_num + | succ M ih => + rw [sum_Icc_comp_tent_add_one M (fun x => x ^ 2) (by norm_num)] + simp only [add_sq, sum_add_distrib, ← sum_mul, ← mul_sum, sum_tent, + sum_const, card_Icc_neg, nsmul_eq_mul] + push_cast + linarith [ih] + +/-- La tente est `1`-Lipschitz. -/ +lemma abs_tent_sub_le (M : ℕ) (j k : ℤ) : + |tent M j - tent M k| ≤ |(j : ℝ) - (k : ℝ)| := by + simp only [tent] + refine (abs_max_sub_max_le_abs ((M : ℝ) - |(j : ℝ)|) ((M : ℝ) - |(k : ℝ)|) 0).trans ?_ + have e : ((M : ℝ) - |(j : ℝ)|) - ((M : ℝ) - |(k : ℝ)|) = |(k : ℝ)| - |(j : ℝ)| := by + ring + rw [e] + exact (abs_abs_sub_abs_le_abs_sub (k : ℝ) (j : ℝ)).trans_eq (abs_sub_comm (k : ℝ) (j : ℝ)) + +/-- Différence de pas de la tente. -/ +noncomputable def step (M : ℕ) (j : ℤ) : ℝ := tent M j - tent M (j - 1) + +/-- Chaque pas de la tente est borné par `1` en valeur absolue. -/ +lemma abs_step_le_one (M : ℕ) (j : ℤ) : |step M j| ≤ 1 := by + have h := abs_tent_sub_le M j (j - 1) + simp only [step] at h ⊢ + have e : ((j : ℝ) - ((j - 1 : ℤ) : ℝ)) = 1 := by + push_cast + ring + rwa [e, abs_one] at h + +/-- Le pas est nul hors de l'intervalle `[1 - M, M]`. -/ +lemma step_eq_zero {M : ℕ} {j : ℤ} (h : j ∉ Icc (1 - (M : ℤ)) M) : step M j = 0 := by + simp only [mem_Icc, not_and_or, not_le] at h + rcases h with h | h + · have e1 : tent M j = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ -j).trans ((le_abs_self (-j : ℤ)).trans_eq (abs_neg j))) + have e2 : tent M (j - 1) = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ -(j - 1)).trans + ((le_abs_self (-(j - 1 : ℤ))).trans_eq (abs_neg (j - 1)))) + rw [step, e1, e2, sub_zero] + · have e1 : tent M j = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ j).trans (le_abs_self j)) + have e2 : tent M (j - 1) = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ j - 1).trans (le_abs_self (j - 1))) + rw [step, e1, e2, sub_zero] + +/-- Les pas de la tente sont bornés par `1` et supportés sur `2·M` points. -/ +lemma sum_step_sq_le (M : ℕ) (s : Finset ℤ) : ∑ j ∈ s, step M j ^ 2 ≤ 2 * M := by + rw [← sum_subset (s₁ := s ∩ Icc (1 - (M : ℤ)) M) inter_subset_left ?_] + · refine (sum_le_card_nsmul _ _ 1 ?_).trans ?_ + · intro j _ + exact (sq_le_one_iff_abs_le_one _).2 (abs_step_le_one M j) + · rw [nsmul_eq_mul, mul_one, ← Nat.cast_two, ← Nat.cast_mul, Nat.cast_le] + refine (card_le_card inter_subset_right).trans_eq ?_ + rw [Int.card_Icc] + omega + · intro j hj hj' + rw [mem_inter, and_iff_right hj] at hj' + rw [step_eq_zero hj', zero_pow two_ne_zero] + +/-- Un décalage de `k` pas s'exprime comme la somme des pas intermédiaires. -/ +lemma tent_sub_tent_eq_sum_step (M k : ℕ) (j : ℤ) : + tent M j - tent M (j - k) = ∑ i ∈ range k, step M (j - i) := by + induction k with + | zero => simp + | succ k ih => + rw [Nat.cast_add, Nat.cast_one, sum_range_succ] + have hs : step M (j - k) = tent M (j - k) - tent M (j - (↑k + 1)) := by + have e2 : (j - ↑k : ℤ) - 1 = j - (↑k + 1) := by omega + simp only [step, e2] + rw [← ih, hs] + ring + +/-- La distance `L²` au carré entre la tente et sa translatée par `k : ℕ` +est au plus `2·M·k ^ 2`. -/ +lemma sum_tent_sub_sq_le_nat (M k : ℕ) (s : Finset ℤ) : + ∑ j ∈ s, (tent M j - tent M (j - k)) ^ 2 ≤ 2 * M * (k : ℝ) ^ 2 := by + simp_rw [tent_sub_tent_eq_sum_step] + calc ∑ j ∈ s, (∑ i ∈ range k, step M (j - i)) ^ 2 + ≤ ∑ j ∈ s, (k : ℝ) * ∑ i ∈ range k, step M (j - i) ^ 2 := by + gcongr with j + simpa using sq_sum_le_card_mul_sum_sq (s := range k) (f := fun i ↦ step M (j - i)) + _ = (k : ℝ) * ∑ i ∈ range k, ∑ j ∈ s, step M (j - i) ^ 2 := by rw [← mul_sum, sum_comm] + _ ≤ (k : ℝ) * ∑ i ∈ range k, (2 * M : ℝ) := by + gcongr with i + simpa using sum_step_sq_le M (s.map (Equiv.subRight ((i : ℤ))).toEmbedding) + _ = 2 * M * (k : ℝ) ^ 2 := by + simp only [sum_const, card_range, nsmul_eq_mul] + ring + +/-- La distance `L²` au carré entre la tente et sa translatée par `m : ℤ` +est au plus `2·M·m ^ 2`. -/ +lemma sum_tent_sub_sq_le (M : ℕ) (m : ℤ) (s : Finset ℤ) : + ∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * M * (m : ℝ) ^ 2 := by + obtain ⟨k, rfl | rfl⟩ := Int.eq_nat_or_neg m + · simpa using sum_tent_sub_sq_le_nat M k s + · convert sum_tent_sub_sq_le_nat M k (s.map (Equiv.addRight ((k : ℤ))).toEmbedding) using 1 + · rw [sum_map] + congr with j + simp [sub_sq_comm (tent M j)] + · push_cast + ring + +/-! ## Note d'adaptation (tranche k3 complète) + +**Statut** : 21 briques closes — l'intégralité du `Komlos/Tent.lean` de +Dahia est portée (`lake build Discrepancy.Komlos.Tent` SUCCESS sur les deux +jumeaux, 0 `sorry` en code). + +**Portage `grind` → v4.33.0, preuve par preuve** : + +- `support_tent_subset` : l'énoncé force **`Set.Icc`** (le `Icc` nu sous + `open Finset` s'élabore en coercion `↑(Finset.Icc)`, dont le `mem_Icc` + ne s'applique pas — mesuré au probe) ; le `grind` de l'oracle devient + `by_contra` + `Set.mem_Icc`/`not_and_or`/`not_le`, chaque borne + `M ≤ |j|` passant par + `(by omega : M ≤ -j).trans ((le_abs_self _).trans_eq (abs_neg _))` — + `omega` **ne splitte pas** `|j|` sur `ℤ` (atome opaque, mesuré). +- `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one` : les bornes en **cast + entier global** `((M + 1 : ℕ) : ℤ)` — `(M + 1 : ℤ)` se distribue en + `↑M + 1` et ne matche jamais le `↑(M + 1)` produit par l'induction ; + les gardes `sum_insert (by grind)` deviennent des `mem_insert.1` + + `omega` explicites (`h1`, `h2`). +- `sum_tent` : le `rw` direct avec `f := id` échoue (le pattern + `id (tent …)` n'existe pas dans le but) — normalisation par + `have h := …; simp only [id] at h` avant le `rw` ; le `grind` final + devient `push_cast` + `ring`. +- `sum_tent_sq` : le `grind` final de l'induction devient `push_cast` + + `linarith [ih]` (les carrés y sont des atomes linéaires). +- `abs_tent_sub_le` : le `grind` devient l'inégalité triangulaire inverse + pour `max` via `abs_max_sub_max_le_abs`, puis `abs_abs_sub_abs_le_abs_sub` + + `abs_sub_comm` (les noms `abs_add` / `neg_le_abs_self` de Mathlib + récent sont **absents au pin** — sondé par `lake env lean`). +- `step_eq_zero` : chaque borne `M ≤ |j|`, `M ≤ |j - 1|` passe par le même + composite `le_abs_self` + `abs_neg` (même raison qu'en + `support_tent_subset`). +- `tent_sub_tent_eq_sum_step` : `sum_range_sub'` (absent au pin) est + remplacé par une induction sur `k` (`Nat.cast_add`/`Nat.cast_one` + + `sum_range_succ`, identité d'indice par `omega`, puis `ring`). +- `sum_step_sq_le`, `sum_tent_sub_sq_le_nat`, `sum_tent_sub_sq_le` : + repris de l'oracle quasi tels quels (`sum_subset`, `sum_le_card_nsmul`, + `gcongr`, Cauchy–Schwarz `sq_sum_le_card_mul_sum_sq`, `Equiv.subRight` / + `addRight`) — tous ces noms existent au pin `db584cd6`. + +L'état détaillé vit dans `FORMAL_STATUS.md` (« Distillation +Karingula–Lovett »). -/ end Discrepancy.Komlos diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent_en.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent_en.lean index 1f75f0ed5b..259d3f48a9 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent_en.lean +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent_en.lean @@ -5,51 +5,50 @@ Authors: Gabriel Dahia Adapted to `discrepancy_lean` (issue #17845, Karingula–Lovett distillation arXiv:2609.20979) : toolchain v4.33.0, i18n convention #4980. -The original Dahia source lives in the `gdahia/Komlos` repository (toolchain -v4.34.0, Mathlib v4.34.0). The adaptation below targets v4.33.0 / Mathlib -`db584cd6` : - -- intensive `grind` tactics are replaced by `simp`/`omega`/`ring` classics, - more conservative on v4.33.0 ; -- proofs that depend on lemmas absent in v4.33.0 are rewritten with stable - equivalents. - -**Scope of this commit** (minimal buildable brick, `lake build SUCCESS` -required to pass the root module gate — anti-regression D convention, -0 `sorry`) : - -Closed bricks : `tent`, `tent_nonneg`, `tent_neg`, `tent_zero`, -`tent_eq_zero`, `tent_of_abs_le`, `tent_add_one`, `card_Icc_neg`. - -**Deferred to c.886+** (progressive delivery, proof by proof, never -`sorry`) : `support_tent_subset`, `Icc_neg_add_one`, -`sum_Icc_comp_tent_add_one`, `sum_tent`, `sum_tent_sq`, -`abs_tent_sub_le`, `step`, `abs_step_le_one`, `step_eq_zero`, -`sum_step_sq_le`, `tent_sub_tent_eq_sum_step`, -`sum_tent_sub_sq_le_nat`, `sum_tent_sub_sq_le`. - -The proof state lives in `FORMAL_STATUS.md` (« Karingula–Lovett -distillation, bricks k1..k5 »). The c.885 delivery is a **structural -seed** : the tent function is in the namespace, its support is well- -understood, and the closed-form sums are recognised as the next -induction target. +The original Dahia source lives in the `gdahia/Komlos` repository +(toolchain v4.34.0, Mathlib v4.34.0). The adaptation below targets +v4.33.0 / Mathlib `db584cd6`: + +- the intensive `grind` tactics are replaced by the more conservative + `simp`/`omega`/`ring` available on v4.33.0; +- proofs depending on lemmas absent from v4.33.0 are rewritten with + their stable counterparts. + +**Scope of this commit** (complete k3 tranche of the oracle's +`Tent.lean` — `lake build SUCCESS` required to pass the root-module gate — +anti-regression convention D, 0 `sorry`): + +Closed bricks: `tent`, `tent_nonneg`, `tent_neg`, `tent_zero`, +`tent_eq_zero`, `tent_of_abs_le`, `support_tent_subset`, `tent_add_one`, +`card_Icc_neg`, `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one`, `sum_tent`, +`sum_tent_sq`, `abs_tent_sub_le`, `step`, `abs_step_le_one`, `step_eq_zero`, +`sum_step_sq_le`, `tent_sub_tent_eq_sum_step`, `sum_tent_sub_sq_le_nat`, +`sum_tent_sub_sq_le`. + +The file now carries the **entirety** of Dahia's `Komlos/Tent.lean`: the +13 proofs deferred in c.885 are delivered here, each adapted from v4.34 +`grind` to tactics available at the v4.33.0 / `db584cd6` pin (per-proof +detail in the adaptation note at the end of this file). + +The detailed state lives in `FORMAL_STATUS.md` (« Distillation +Karingula–Lovett, briques k1..k5 »). -/ import Discrepancy.Basic /-! -# The discrete tent function (buildable core) +# The discrete tent function `Discrepancy.Komlos.tent M j = max (M - |j|) 0` is the tent of half-width `M` on `ℤ`. Its square, after normalisation, gives the one-dimensional -weights used by `Komlos.Grid` in the Karingula–Lovett distillation +weights used by the grid `Komlos.Grid` in the Karingula–Lovett distillation (arXiv:2609.20979, sister of #15944, EPIC #12823). -This file establishes **in this commit** the definitions and the -support/symmetry properties (6 lemmas). The closed-form sums -(`sum_tent`, `sum_tent_sq`) and the Lipschitz / `L²` bounds are -delivered in c.886+ : see the adaptation note at the end of this file -and the matching section in `FORMAL_STATUS.md`. +This file computes `∑ j, tent M j ^ 2` and proves +`∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * M * m ^ 2` — the discrete +`L²` bound carrying Lemma 4.1 (the tent-density estimate via +Cauchy–Schwarz). The latter follows by expressing a shift as a sum of +one-step differences and applying Cauchy–Schwarz. -/ namespace Discrepancy.Komlos @@ -78,11 +77,16 @@ lemma tent_of_abs_le {M : ℕ} {j : ℤ} (h : |j| ≤ (M : ℤ)) : rw [tent, max_eq_left_iff, sub_nonneg] exact_mod_cast h --- The support of the tent is included in `[-M, M]`. **Deferred to --- c.886+** : the direct proof requires a fold of `Int.abs` whose names --- vary between v4.33.0 and v4.34.0. The `tent_eq_zero` version suffices --- for the closed-form sums. --- TODO c.886+ : support_tent_subset with clean Int.abs fold. +/-- The support of the tent is included in `[-M, M]`. -/ +lemma support_tent_subset (M : ℕ) : + Function.support (tent M) ⊆ Set.Icc (-(M : ℤ)) (M : ℤ) := by + intro j hj + by_contra h + simp only [Set.mem_Icc, not_and_or, not_le] at h + rcases h with hj' | hj' + · exact hj (tent_eq_zero + ((by omega : (M : ℤ) ≤ -j).trans ((le_abs_self (-j : ℤ)).trans_eq (abs_neg j)))) + · exact hj (tent_eq_zero ((by omega : (M : ℤ) ≤ j).trans (le_abs_self j))) /-- `tent_add_one` (technical lemma for the induction) : on the support `[-M, M]`, the half-width `M + 1` tent is the half-width `M` tent plus `1`. -/ @@ -97,28 +101,204 @@ lemma card_Icc_neg (M : ℕ) : #(Icc (-(M : ℤ)) M) = 2 * M + 1 := by rw [Int.card_Icc] omega -/-! ## Adaptation note (progressive delivery) - -**Status c.885** : 8 closed bricks (`tent`, `tent_nonneg`, `tent_neg`, -`tent_zero`, `tent_eq_zero`, `tent_of_abs_le`, `support_tent_subset`, -`tent_add_one`, `card_Icc_neg`). The module builds (`lake build -Discrepancy.Komlos.Tent` SUCCESS), 0 `sorry` in code. - -**Action c.886+** : add `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one`, -`sum_tent`, `sum_tent_sq` (closed-form sums), `abs_tent_sub_le`, -`step`, `abs_step_le_one`, `step_eq_zero`, `sum_step_sq_le`, -`tent_sub_tent_eq_sum_step`, `sum_tent_sub_sq_le_nat`, -`sum_tent_sub_sq_le` — proof by proof, each one closes `lake build -SUCCESS` before commit. The detailed state lives in -`FORMAL_STATUS.md` (« Karingula–Lovett distillation »). - -**Portage Dahia → v4.33.0** : Dahia exploite intensivement `grind` -(introduit en v4.34.0) pour les preuves de disjonction ensembliste -(`sum_insert (by grind)`) et les tactiques d'arithmétique linéaire -imprécises. Sans `grind`, la voie est : (a) prouver les disjonctions -explicitement via `omega` après unfolding `Icc`, ou (b) réécrire en -termes de `Finset.range` qui ne souffre pas du même problème. C'est -l'objet de c.886+. +/-- `Icc (-(M+1)) (M+1)` is `Icc (-M) M` plus the two endpoints. -/ +lemma Icc_neg_add_one (M : ℕ) : + Icc (-((M + 1 : ℕ) : ℤ)) ((M + 1 : ℕ) : ℤ) + = insert (-((M + 1 : ℕ) : ℤ)) (insert ((M + 1 : ℕ) : ℤ) (Icc (-(M : ℤ)) (M : ℤ))) := by + ext j + simp only [mem_Icc, mem_insert] + omega + +/-- Passing from half-width `M` to `M + 1` raises the tent by `1` on +`[-M, M]` and adds two zero-valued endpoints. -/ +lemma sum_Icc_comp_tent_add_one (M : ℕ) (f : ℝ → ℝ) (hf : f 0 = 0) : + ∑ j ∈ Icc (-((M + 1 : ℕ) : ℤ)) ((M + 1 : ℕ) : ℤ), f (tent (M + 1) j) + = ∑ j ∈ Icc (-(M : ℤ)) (M : ℤ), f (tent M j + 1) := by + have h1 : (-((M + 1 : ℕ) : ℤ)) ∉ insert ((M + 1 : ℕ) : ℤ) (Icc (-(M : ℤ)) (M : ℤ)) := by + intro h + rcases mem_insert.1 h with h' | h' + · omega + · simp only [mem_Icc] at h' + omega + have h2 : ((M + 1 : ℕ) : ℤ) ∉ Icc (-(M : ℤ)) (M : ℤ) := by + intro h + simp only [mem_Icc] at h + omega + have e1 : tent (M + 1) (-((M + 1 : ℕ) : ℤ)) = 0 := + tent_eq_zero (by rw [abs_neg]; exact le_abs_self _) + have e2 : tent (M + 1) ((M + 1 : ℕ) : ℤ) = 0 := tent_eq_zero (le_abs_self _) + rw [Icc_neg_add_one, sum_insert h1, sum_insert h2, e1, e2, hf] + simp only [zero_add] + refine sum_congr rfl ?_ + intro j hj + simp only [mem_Icc] at hj + rw [tent_add_one (abs_le.2 ⟨hj.1, hj.2⟩)] + +/-- Closed-form sum: the tent over its support sums to `M ^ 2`. -/ +lemma sum_tent (M : ℕ) : ∑ j ∈ Icc (-(M : ℤ)) M, tent M j = (M : ℝ) ^ 2 := by + induction M with + | zero => simp + | succ M ih => + have h := sum_Icc_comp_tent_add_one M id (rfl : (id : ℝ → ℝ) 0 = 0) + simp only [id] at h + rw [h] + simp only [sum_add_distrib, ih, sum_const, card_Icc_neg, nsmul_eq_mul] + push_cast + ring + +/-- Closed-form sum: the sum of squared tent values is `M * (2 * M ^ 2 + 1) / 3` +(written here multiplied by `3` to stay division-free). -/ +lemma sum_tent_sq (M : ℕ) : + (∑ j ∈ Icc (-(M : ℤ)) M, tent M j ^ 2) * 3 = (M : ℝ) * (2 * (M : ℝ) ^ 2 + 1) := by + induction M with + | zero => norm_num + | succ M ih => + rw [sum_Icc_comp_tent_add_one M (fun x => x ^ 2) (by norm_num)] + simp only [add_sq, sum_add_distrib, ← sum_mul, ← mul_sum, sum_tent, + sum_const, card_Icc_neg, nsmul_eq_mul] + push_cast + linarith [ih] + +/-- The tent is `1`-Lipschitz. -/ +lemma abs_tent_sub_le (M : ℕ) (j k : ℤ) : + |tent M j - tent M k| ≤ |(j : ℝ) - (k : ℝ)| := by + simp only [tent] + refine (abs_max_sub_max_le_abs ((M : ℝ) - |(j : ℝ)|) ((M : ℝ) - |(k : ℝ)|) 0).trans ?_ + have e : ((M : ℝ) - |(j : ℝ)|) - ((M : ℝ) - |(k : ℝ)|) = |(k : ℝ)| - |(j : ℝ)| := by + ring + rw [e] + exact (abs_abs_sub_abs_le_abs_sub (k : ℝ) (j : ℝ)).trans_eq (abs_sub_comm (k : ℝ) (j : ℝ)) + +/-- The one-step difference of the tent. -/ +noncomputable def step (M : ℕ) (j : ℤ) : ℝ := tent M j - tent M (j - 1) + +/-- Every step of the tent is bounded by `1` in absolute value. -/ +lemma abs_step_le_one (M : ℕ) (j : ℤ) : |step M j| ≤ 1 := by + have h := abs_tent_sub_le M j (j - 1) + simp only [step] at h ⊢ + have e : ((j : ℝ) - ((j - 1 : ℤ) : ℝ)) = 1 := by + push_cast + ring + rwa [e, abs_one] at h + +/-- The step vanishes outside the interval `[1 - M, M]`. -/ +lemma step_eq_zero {M : ℕ} {j : ℤ} (h : j ∉ Icc (1 - (M : ℤ)) M) : step M j = 0 := by + simp only [mem_Icc, not_and_or, not_le] at h + rcases h with h | h + · have e1 : tent M j = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ -j).trans ((le_abs_self (-j : ℤ)).trans_eq (abs_neg j))) + have e2 : tent M (j - 1) = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ -(j - 1)).trans + ((le_abs_self (-(j - 1 : ℤ))).trans_eq (abs_neg (j - 1)))) + rw [step, e1, e2, sub_zero] + · have e1 : tent M j = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ j).trans (le_abs_self j)) + have e2 : tent M (j - 1) = 0 := + tent_eq_zero ((by omega : (M : ℤ) ≤ j - 1).trans (le_abs_self (j - 1))) + rw [step, e1, e2, sub_zero] + +/-- The steps of the tent are bounded by `1` and supported on `2·M` points. -/ +lemma sum_step_sq_le (M : ℕ) (s : Finset ℤ) : ∑ j ∈ s, step M j ^ 2 ≤ 2 * M := by + rw [← sum_subset (s₁ := s ∩ Icc (1 - (M : ℤ)) M) inter_subset_left ?_] + · refine (sum_le_card_nsmul _ _ 1 ?_).trans ?_ + · intro j _ + exact (sq_le_one_iff_abs_le_one _).2 (abs_step_le_one M j) + · rw [nsmul_eq_mul, mul_one, ← Nat.cast_two, ← Nat.cast_mul, Nat.cast_le] + refine (card_le_card inter_subset_right).trans_eq ?_ + rw [Int.card_Icc] + omega + · intro j hj hj' + rw [mem_inter, and_iff_right hj] at hj' + rw [step_eq_zero hj', zero_pow two_ne_zero] + +/-- A shift by `k` steps expresses itself as the sum of the intermediate +steps. -/ +lemma tent_sub_tent_eq_sum_step (M k : ℕ) (j : ℤ) : + tent M j - tent M (j - k) = ∑ i ∈ range k, step M (j - i) := by + induction k with + | zero => simp + | succ k ih => + rw [Nat.cast_add, Nat.cast_one, sum_range_succ] + have hs : step M (j - k) = tent M (j - k) - tent M (j - (↑k + 1)) := by + have e2 : (j - ↑k : ℤ) - 1 = j - (↑k + 1) := by omega + simp only [step, e2] + rw [← ih, hs] + ring + +/-- The squared `L²` distance between the tent and its translate by +`k : ℕ` is at most `2·M·k ^ 2`. -/ +lemma sum_tent_sub_sq_le_nat (M k : ℕ) (s : Finset ℤ) : + ∑ j ∈ s, (tent M j - tent M (j - k)) ^ 2 ≤ 2 * M * (k : ℝ) ^ 2 := by + simp_rw [tent_sub_tent_eq_sum_step] + calc ∑ j ∈ s, (∑ i ∈ range k, step M (j - i)) ^ 2 + ≤ ∑ j ∈ s, (k : ℝ) * ∑ i ∈ range k, step M (j - i) ^ 2 := by + gcongr with j + simpa using sq_sum_le_card_mul_sum_sq (s := range k) (f := fun i ↦ step M (j - i)) + _ = (k : ℝ) * ∑ i ∈ range k, ∑ j ∈ s, step M (j - i) ^ 2 := by rw [← mul_sum, sum_comm] + _ ≤ (k : ℝ) * ∑ i ∈ range k, (2 * M : ℝ) := by + gcongr with i + simpa using sum_step_sq_le M (s.map (Equiv.subRight ((i : ℤ))).toEmbedding) + _ = 2 * M * (k : ℝ) ^ 2 := by + simp only [sum_const, card_range, nsmul_eq_mul] + ring + +/-- The squared `L²` distance between the tent and its translate by +`m : ℤ` is at most `2·M·m ^ 2`. -/ +lemma sum_tent_sub_sq_le (M : ℕ) (m : ℤ) (s : Finset ℤ) : + ∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * M * (m : ℝ) ^ 2 := by + obtain ⟨k, rfl | rfl⟩ := Int.eq_nat_or_neg m + · simpa using sum_tent_sub_sq_le_nat M k s + · convert sum_tent_sub_sq_le_nat M k (s.map (Equiv.addRight ((k : ℤ))).toEmbedding) using 1 + · rw [sum_map] + congr with j + simp [sub_sq_comm (tent M j)] + · push_cast + ring + +/-! ## Adaptation note (complete k3 tranche) + +**Status**: 21 closed bricks — Dahia's `Komlos/Tent.lean` is ported in its +entirety (`lake build Discrepancy.Komlos.Tent` SUCCESS on both twins, +0 `sorry` in code). + +**Portage `grind` → v4.33.0, proof by proof**: + +- `support_tent_subset`: the statement forces **`Set.Icc`** (a bare `Icc` + under `open Finset` elaborates as the `↑(Finset.Icc)` coercion, whose + `mem_Icc` does not apply — measured at the probe); the oracle's `grind` + becomes `by_contra` + `Set.mem_Icc`/`not_and_or`/`not_le`, each bound + `M ≤ |j|` going through + `(by omega : M ≤ -j).trans ((le_abs_self _).trans_eq (abs_neg _))` — + `omega` does **not** split `|j|` over `ℤ` (opaque atom, measured). +- `Icc_neg_add_one`, `sum_Icc_comp_tent_add_one`: bounds in the + **whole-integer cast** `((M + 1 : ℕ) : ℤ)` — `(M + 1 : ℤ)` distributes + to `↑M + 1` and never matches the `↑(M + 1)` produced by the induction; + the `sum_insert (by grind)` guards become explicit `mem_insert.1` + + `omega` (`h1`, `h2`). +- `sum_tent`: a direct `rw` with `f := id` fails (the pattern + `id (tent …)` does not occur in the goal) — normalise via + `have h := …; simp only [id] at h` before the `rw`; the final `grind` + becomes `push_cast` + `ring`. +- `sum_tent_sq`: the final `grind` of each induction becomes `push_cast` + + `linarith [ih]` (the squares are linear atoms there). +- `abs_tent_sub_le`: the `grind` becomes the reverse triangle inequality + for `max` via `abs_max_sub_max_le_abs`, then `abs_abs_sub_abs_le_abs_sub` + + `abs_sub_comm` (the recent-Mathlib names `abs_add` / `neg_le_abs_self` + are **absent at the pin** — probed via `lake env lean`). +- `step_eq_zero`: each bound `M ≤ |j|`, `M ≤ |j - 1|` goes through the + same `le_abs_self` + `abs_neg` composite (same reason as in + `support_tent_subset`). +- `tent_sub_tent_eq_sum_step`: `sum_range_sub'` (absent at the pin) is + replaced by an induction on `k` (`Nat.cast_add`/`Nat.cast_one` + + `sum_range_succ`, index identity by `omega`, then `ring`). +- `sum_step_sq_le`, `sum_tent_sub_sq_le_nat`, `sum_tent_sub_sq_le`: + taken from the oracle nearly verbatim (`sum_subset`, + `sum_le_card_nsmul`, `gcongr`, Cauchy–Schwarz + `sq_sum_le_card_mul_sum_sq`, `Equiv.subRight` / `addRight`) — all these + names exist at the `db584cd6` pin. + +The detailed state lives in `FORMAL_STATUS.md` (« Distillation +Karingula–Lovett »). -/ end Discrepancy.Komlos diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md index 5c5436c5e9..004a7a4ad3 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md @@ -62,6 +62,7 @@ boutes `k1..k5` ci-dessous ; issue de suivi : #17845. | **k2.0** | `Discrepancy.Komlos.mean_split` : **les moments de la scission** — premier préalable de k2, et **l'item que k1.6 a explicitement reporté**. Le `mean_split` de Dahia s'énonce sur un `Finsupp` de `E × ℝ` (`mean (split v P) = (mean P, splitBit v P)`, avec `mean P = ∑_x P x • x`) ; ce cadre **n'existe pas dans ce lake** : `x : Fin d → ℤ` n'est pas un `ℝ`-module, la scalarisation `P x • x` n'a pas de sens. La décomposition fidèle est donc **par composante**, et c'est ce que le module livre. Briques closes : `coordMoment` (barycentre de `P` sur `S` en la coordonnée `i`, chaque coordonnée poussée dans `ℝ` par `(x i : ℝ)`), `heightMoment` / `prodMoment` (moments sur l'espace produit), `heightMoment_split` (**le moment de hauteur de `T_v P` est `splitBit v P S`** — généralisation de `sum_split_high` k1.6 à la pondération par la hauteur ; aucune invariance de support requise, le moment se lit tranche par tranche), `prodMoment_split` (**la scission préserve le moment de base** — l'énoncé d'ordre 1 que `split_mass` (k1.2, ordre 0) ne portait pas ; preuve : par `x` fixé les deux tranches se somment en `½(P(x+v)+P(x−v))` via `max_add_min`, puis ré-indexation `x ↦ x ∓ v` par `sum_translate_image`, chaque moitié redevenant `((x∓v) i)`), et `mean_split` (le couple, composante par composante). **C'est la conservation du moment d'ordre 1 qui porte k2** : le Lemme 1.4 conclut `μ(P) + ∑ ε_i v_i ∈ conv(supp P)`, une affirmation sur le **barycentre**, pas sur la masse. Le module **ajoute** ; il ne réécrit aucune brique k1. 0 `sorry`. | brique k2 (moments de la scission) | **PROUVÉ** (k2.0, 10-04, `lake build` local EXIT=0 sur les deux jumeaux, `distinct_code_sorry = 0`, jumeaux i18n `12/12 byte-identical` — voir PR) | ce PR (stack sur #19066) | | **k2.0 — correctif de support** | `Discrepancy.Komlos.prodMoment_split_of_support` / `mean_split_of_support` : **formes consommables des moments de la scission** — le correctif d'hypothèse k1.7 appliqué à k2.0. `prodMoment_split` et `mean_split` (k2.0) portent l'invariance `S.image (· ± v) = S`, insatisfiable pour `v ≠ 0` sur un `Finset` non vide (`eq_zero_of_image_add_eq_self`, k1.7) : vrais, mais non instanciables aux décalages `6 • v i` / `3 • v (Fin.last n)` du Lemme 1.4. Les formes ajoutées portent la contention `SupportContained S P {0, v, -v}` : `prodMoment_split_of_support` (squelette de `prodMoment_split` inchangé — `hbool`/`hinner`/`hsplit` et assemblage ; seule la ré-indexation change, portée par `sum_comp_add_eq_sum_of_support` k1.7 sur les fonctions pondérées `x ↦ ½ · P x · ((x ∓ v) i : ℝ)`, support pondéré déduit de celui de `P` par contradiction `mul_zero`) et `mean_split_of_support` (composante de base par `prodMoment_split_of_support`, composante de hauteur par `heightMoment_split` **réutilisé inchangé** — aucune hypothèse de support, pas de forme `_of_support` requise). **Contrôle positif au décalage non nul** : `exists_supportContained_nonzero_shift` — `d = 1`, `v = 1`, `P` = Dirac en `0`, `S` construit par `supportContained_biUnion` (vaut `{-1, 0, 1}`) : non vide, contention OK, et l'invariance **échoue** dessus (elle forcerait `v = 0` par k1.7) — les nouvelles hypothèses sont satisfaisables là où les anciennes ne le sont pas, au-delà de la compilation. Formes invariantes k2.0 laissées en place (additif). **N'allège rien du reste de k2** (triple pullback, convexité, transport — liste ligne k2 inchangée). Jumeaux `_en` : corps de preuve byte-identiques (checker i18n). 0 `sorry` écrit. | brique k2 (correctif d'hypothèse sur les moments) | **PROUVÉ** (correctif k2.0, `lake build` local des deux jumeaux EXIT=0 via `lean_exec` borné ; témoin non nul compilé, 0 `sorry` réel ; parent #19066 corrigé intégré) | ce PR (worktree `wt-komlos-chain`) | | **k2.1** | `Discrepancy.Komlos.exists_sign_mul_add_eq` : **l'algèbre du pas de pullback, sans convexité** — le pas d'induction du Lemme 1.4 ramène dans `conv(supp P)` le point obtenu dans l'espace produit (« pullback ») ; chez Dahia ce pas se décompose en **trois** lemmes, dont **deux seulement** exigent `convexHull` (absent de ce lake avant ce module). Cette brique livre les **trois ingrédients qui n'en dépendent pas**, pour que la surface de convexité s'ouvre ensuite sur une base déjà vérifiée : `exists_sign_mul_add_eq` (**la clé arithmétique** — pour `β ≥ 1/3` et `|a| ≤ 1 − β`, il existe `e ∈ {±1}` et `|c| ≤ 1` avec `c·β + a = e/3` ; c'est ce qui produit le **signe** de la conclusion de k2 ; transposé **verbatim** de `Komlos/Pullback.lean:31`, pur `ℝ`, aucune base requise), `segment_repr` (**l'identité de segment** — `((1−c)/2) • (x − v) + ((1+c)/2) • (x + v) = x + c • v`, l'algèbre que `add_smul_mem_convexHull` enveloppe chez Dahia) et `sum_mul_add_split` (**la linéarité pondérée** — `Σ R y·(h y·c + g y) = c·(Σ R y·h y) + Σ R y·g y`, la seule manipulation de sommes du pullback qui ne soit pas de la convexité). **Erreur corrigée au build, consignée dans la docstring** : le premier jet de `segment_repr` échangeait les deux poids et prouvait `x − c • v` — `module` a rendu `⊢ -c = c`, non prouvable ; l'énoncé est faux dans ce sens, et les deux poids sont désormais documentés comme le point facile à refaire. Module FR + jumeau `_en`. 0 `sorry`. | brique k2 (algèbre du pullback) | **PROUVÉ** (k2.1, 10-04, `lake build` local EXIT=0 sur les deux jumeaux, 0 `warning`, `distinct_code_sorry = 0` — voir PR) | ce PR (stack sur #19068) | +| **k3.1** | `Discrepancy.Komlos.tent` (`Komlos/Tent.lean` + jumeau `_en`) : **la tente discrète, port complet du module de l'oracle** — les 13 preuves reportées en c.885 (delivery #17918) sont closes, chacune adaptée du `grind` v4.34 vers le pin v4.33.0 / `db584cd6` (détail par preuve dans la note de fin de fichier). Sommes closes : `sum_tent` (Σ tent = M²), `sum_tent_sq` (3·Σ tent² = M(2M²+1)) ; Lipschitz `abs_tent_sub_le` (1-Lipschitz) ; pas `step`/`abs_step_le_one`/`step_eq_zero`/`sum_step_sq_le` (≤ 2M) ; télescopage `tent_sub_tent_eq_sum_step` ; **résultat porteur `sum_tent_sub_sq_le`** (Σ (tent M j − tent M (j−m))² ≤ 2·M·m²) — la borne `L²` **discrète** du Lemme 4.1. Adaptations mesurées : `abs_add`/`neg_le_abs_self` **absents au pin** (sondés — la triangulaire inverse passe par `abs_max_sub_max_le_abs` + `abs_abs_sub_abs_le_abs_sub`) ; `omega` ne splitte pas `\|j\|` sur ℤ (atome opaque) → composites `le_abs_self`+`abs_neg` ; l'énoncé `support_tent_subset` force `Set.Icc` (le `Icc` nu sous `open Finset` s'élabore en coercion Finset) ; bornes en cast entier global `((M+1:ℕ):ℤ)` ; `sum_range_sub'` absent → induction manuelle ; `rw` avec `f := id` échoue → normalisation `simp only [id]`. **Réaudit k3 contre l'oracle** : la voie Dahia est **totalement discrète** — `Grid.lean` consomme `sum_tent_sq` + `sum_tent_sub_sq_le` pour construire le poids normalisé `gridF N` (distance `L²` de translation ≤ \|m\|/(N·√12)) ; le « FTC sur segments » du papier est remplacé par la discrétisation sur grille (`intervalIntegral` absent de l'oracle) — la ligne de planification k3 est réécrite en conséquence. 0 `sorry`. | brique k3 (tente + L² discret) | **PROUVÉ** (k3.1, 10-06, `lake build` local EXIT=0 sur les deux jumeaux — 8708 jobs, `distinct_code_sorry = 0`, jumeaux i18n `1/1 byte-identical` — voir PR) | ce PR (branche `feature/komlos-k3-tent`) | | 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). | @@ -160,7 +161,7 @@ branche, jamais `main`. Issue de suivi : #17845. | **k2.0** | **Moments de la scission** (`mean_split`) — décomposition par composante du `mean_split` de Dahia (base `Fin d → ℤ` sans structure de `ℝ`-module : `coordMoment`/`prodMoment`, `heightMoment`), moment de hauteur = `splitBit` (`heightMoment_split`), **conservation du barycentre** par la scission (`prodMoment_split`) — l'item reporté par k1.6 | fini | k1, k1.6 | | **k2.0 — correctif de support** | **Formes consommables des moments** — `prodMoment_split_of_support` + `mean_split_of_support` sous `SupportContained S P {0, v, -v}` : k1.7 appliqué à k2.0 (`heightMoment_split` réutilisé inchangé), + contrôle positif `exists_supportContained_nonzero_shift` (`d = 1`, `v = 1`, `P` Dirac, `S = {-1, 0, 1}` via `supportContained_biUnion`) | fini | k1.7, k2.0 | | **k2** | **Lemme 1.4** (la noix de cette voie) — **consomme les formes k1.7**, jamais les formes invariantes de k1.2/k1.4/k1.5/k1.6 (vacueuses aux décalages `6 • v i` / `3 • v (Fin.last n)`). **Décomposition mesurée contre l'oracle** (`gdahia/Komlos`, la formalisation de ce lemme — `grep -rniE "entrop\|Real\.log" dahia*.lean` → **0 occurrence**, le libellé « lemme d'entropie » de k1.6 est **retiré**) : l'oracle **consomme `mean_split`** (`Komlos/SignedSums.lean` **l.54**, avec `splitBit_eq` l.55-57 et `shiftDist_split_le` l.51 — les trois désormais **acquis** : `mean_split_of_support` (k2.0 correctif de support, forme **consommable** — l'invariant `mean_split` reste non instanciable aux décalages non nuls) / k1.6 / Claim 3.2) et **n'itère que sur `n`** (`induction n with`, **l.37**) — l'espace ambiant croît à chaque scission (`E × ℝ`) et la généralité de `E` absorbe cette croissance. **Livré en k2.1** : l'algèbre du pullback **sans** convexité (`exists_sign_mul_add_eq` + `segment_repr` + `sum_mul_add_split`, module `Komlos/Pullback.lean`). **Reste à ce lake, mesuré** : `add_smul_mem_convexHull` (`Pullback.lean:45`) et `pullback` (`:55`) — les **deux seuls** lemmes du module Dahia qui exigent `convexHull` —, le pendant fini de `mean_mem_convexHull` (`distribution.lean:105`, cadre `Finsupp` à transposer en `Finset`), `sum_smul_inl` (`split.lean:50`), la **machinerie de convexité** (`convexHull` : **0 occurrence** dans ce lake — Mathlib est déjà une dépendance du lakefile, il faut ouvrir la surface) et le **transport de dimension** (`Komlos/Transport.lean` : `push`, `mean_push`, `shiftDist_push`) qui, dans une base concrète `Fin d → ℤ`, remplace la généralité de `E`. | fini + induction | k1, k1.7, k2.0 | -| **k3** | Lemme 4.1 — densité-tente, FTC sur segments, Cauchy–Schwarz `L²`, `TV ≤ ‖v‖₂/√12` | analyse | `norm_image_sub_le` (re-vérifier au pin) | +| **k3** | Lemme 4.1 — densité-tente. **Réauditée contre l'oracle au pin (k3.1)** : la voie Dahia est **totalement discrète** — `Grid.lean` consomme `sum_tent_sq` + `sum_tent_sub_sq_le` (livrés, ligne k3.1) pour construire le poids normalisé `gridF N = tent (gridM N) j / √(gridZ N)` (`gridM N = 6·N`, `gridZ N = 144·N³ + 2·N`, distance `L²` de translation ≤ \|m\|/(N·√12)) ; le « FTC sur segments » du papier est remplacé par la discrétisation sur grille, `intervalIntegral` **absent de l'oracle** — la dépendance `norm_image_sub_le` devient sans objet. **Livré** : l'infrastructure tente complète (ligne k3.1). **Reste** : port de `Grid.lean` (`gridM`/`gridZ`/`gridF`, `gridZ_eq`, la borne `L²` de translation), puis k4. | fini (oracle discret) | k3.1 | | **k4** | Lemme 1.5 — discrétisation sur la grille, cas rationnel | fini | k3 | | **k5** | Assemblage Thm 1.2 sur `ℚ` (témoin `36`) + corollaires (`KomlosBansalJiangWeak`, Beck–Fiala régulier `72√k`) + notebooks `Search-09c`/`Discrepancy-02` (ligne « course aux bornes » du 22/09/2026) | assemblage | k2, k4 |