diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit.lean new file mode 100644 index 0000000000..ea88f58a8a --- /dev/null +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit.lean @@ -0,0 +1,221 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +Adapté à `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` (toolchain +v4.34.0, cadre `Finsupp` sur `E →₀ ℝ`). Ce module n'a **pas de contrepartie +oracle nom pour nom** : chez l'oracle, l'hypothèse d'induction s'applique à +la distribution scindée dans `E × ℝ` sans aucune précondition de support — +le `Finsupp` transporte son support gratuitement (`Finsupp.embDomain`) ; +c'est le cadre `Finset` explicite du lake qui doit payer ce transport, et +ce paiement est précisément l'objet de cette brique. + +**Portée de ce commit** (brique k2.6b, `lake build SUCCESS` requis, 0 +`sorry`) — la scission sous contention, lue dans la dimension agrandie +`Fin (d+1) → ℤ` : + +- `pushUp_split_ne_zero` — lecture du support de la poussée : toute masse + de `pushUp (split w P)` vit sur l'image de `liftUp` et provient d'une + masse de `P` à distance `± w` de sa base (l'auxiliaire que consomme le + transfert de contenance) ; +- `supportContained_pushUp_split` — **le transfert de contenance à + travers la scission** : si `S` contient le support de `P` et ses + translatés par `A`, et `A` est stable par `± w`, alors l'image liftée + `(S ×ˢ univ).map liftUpEmb` contient le support de `pushUp (split w P)` + et ses translatés par les décalages embarqués `Fin.snoc · 0` de `A` ; +- `coordMoment_pushUp_split_of_support` — **la conservation du moment de + base sous contenance, au niveau lifté** : le moment coordonné de la + scission-poussée, lu en coordonnée héritée `i.castSucc`, est le moment + de `P` en `i` — la composition du pont `coordMoment_pushUp_castSucc` + (k2.6a) avec `prodMoment_split_of_support` (k2.0) ; +- `coordMoment_pushUp_split_last` — la composante de hauteur : le moment + de la scission-poussée en dernière coordonnée est le bit de scission + (`coordMoment_pushUp_last` (k2.6a) × `heightMoment_split` (k2.0)) ; +- `supportContained_pushUp_split_three` — la forme `{0, snoc u 0, + −snoc u 0}` que le cran suivant de l'induction consomme : instance du + transfert par monotonie (`SupportContained.mono`), les trois décalages + étant les images `snoc · 0` de `0`, `u`, `−u`. + +**Consommateur mesuré** : l'induction du Lemme 1.4 (brique k2.6c, oracle +`Komlos/SignedSums.lean` l.44-55) applique son hypothèse d'induction à +`split (3 • v_last) P` dans l'espace agrandi — chez nous, à `pushUp +(split w P)` dans `Fin (d+1) → ℤ`. Les préconditions de support et les +ré-écritures de barycentre que cet appel exige sont exactement les cinq +énoncés ci-dessus : la contenance pour instancier l'hypothèse +(`supportContained_pushUp_split_three`), les moments pour réécrire le +point qu'elle produit (`coordMoment_pushUp_split_of_support` et +`_last`, le miroir lake du `rw [mean_split, …] at hmem` de l.54). + +**Différé** : l'induction elle-même (`SignedSums.lean` nom pour nom, +k2.6c). L'état détaillé vit dans `FORMAL_STATUS.md`. +-/ + +import Discrepancy.Komlos.Containment +import Discrepancy.Komlos.Lift +import Discrepancy.Komlos.MeanSplit +import Discrepancy.Komlos.Split + +/-! +# La scission sous contention, dans la dimension agrandie (k2.6b) + +Chez l'oracle, le pas de l'induction du Lemme 1.4 est gratuit côté +support : `split v P` est un `Finsupp` sur `E × ℝ`, dont le support se +transporte par `Finsupp.embDomain` sans précondition. Dans le cadre +`Finset` explicite du lake, le même pas doit **prouver** que le support +de la scission-poussée `pushUp (split w P)` est contenu — et le restera +au cran suivant de l'induction — dans l'image liftée du support de +départ. + +Ce module paie ce double coût en une brique : le **transfert de +contention** (le support scindé-poussé obéit à la contention transportée +par `snoc · 0`) et la **conservation des moments sous contenance** au +niveau lifté (les deux composantes de `mean_split_of_support` k2.0 lues +à travers les ponts de k2.6a). +-/ + +namespace Discrepancy.Komlos + +/-- **Toute masse de la scission-poussée provient d'une masse de `P` à +distance `± w`** : si `pushUp (split w P) z ≠ 0`, alors `z` est sur +l'image de `liftUp` — `z = liftUp (x, b)` — et l'un de `P (x + w)`, +`P (x − w)` est non nul. La moitié vient de `pushUp_eq_zero` (hors +image, la poussée est nulle), l'autre des formes `max`/`min` de `split` +(une moitié non nulle force l'un des deux arguments non nul). + +C'est l'auxiliaire de support que consomme le transfert de contenance +`supportContained_pushUp_split` : il ramène toute question de support +sur la poussée à une question de support sur `P`. -/ +lemma pushUp_split_ne_zero {d : ℕ} (w : Fin d → ℤ) {P : (Fin d → ℤ) → ℝ} + {z : Fin (d + 1) → ℤ} (hz : pushUp (split w P) z ≠ 0) : + ∃ (x : Fin d → ℤ) (b : Bool), z = liftUp (x, b) ∧ + (P (x + w) ≠ 0 ∨ P (x - w) ≠ 0) := by + by_cases hex : ∃ y : (Fin d → ℤ) × Bool, liftUp y = z + · obtain ⟨⟨x, b⟩, rfl⟩ := hex + rw [pushUp_apply] at hz + refine ⟨x, b, rfl, ?_⟩ + cases b with + | false => + rw [split_apply_zero] at hz + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [max_eq_right h] at hz + exact Or.inr (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [max_eq_left h] at hz + exact Or.inl (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + | true => + rw [split_apply_one] at hz + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [min_eq_left h] at hz + exact Or.inl (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [min_eq_right h] at hz + exact Or.inr (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [pushUp_eq_zero _ (fun y hy => hex ⟨y, hy⟩)] at hz + exact absurd rfl hz + +/-- **Transfert de contenance à travers la scission** : si `S` contient +le support de `P` et ses translatés par `A`, et si `A` est stable par +`± w`, alors l'image liftée `(S ×ˢ univ).map liftUpEmb` contient le +support de la scission-poussée `pushUp (split w P)` et ses translatés +par les décalages embarqués `Fin.snoc · 0` de `A`. + +C'est la précondition de support que le pas de l'induction (k2.6c) doit +établir pour appliquer l'hypothèse d'induction à la dimension `d + 1` : +chez l'oracle (`Komlos/SignedSums.lean` l.44-53), le `Finsupp` paie ce +transport gratuitement (`Finsupp.embDomain`) ; le cadre `Finset` du lake +le paie ici. La stabilité de `A` par `± w` est le prix exact de la +scission : un point de masse `P (x ± w) ≠ 0` déplacé de `a` atterrit en +`x + a`, atteint depuis `x ± w` par le décalage `a ∓ w ∈ A`. -/ +theorem supportContained_pushUp_split {d : ℕ} (w : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S A : Finset (Fin d → ℤ)} + (hS : SupportContained S P A) + (hA : ∀ a ∈ A, a + w ∈ A ∧ a - w ∈ A) : + SupportContained ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) + (pushUp (split w P)) (A.image (fun a => Fin.snoc a 0)) := by + intro z hz t ht + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp ht + obtain ⟨x, b, rfl, hPw⟩ := pushUp_split_ne_zero w hz + rw [liftUp_add_snoc] + show liftUp (x + a, b) ∈ (S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb + refine Finset.mem_map.mpr ⟨(x + a, b), ?_, liftUpEmb_apply _⟩ + refine Finset.mem_product.mpr ⟨?_, Finset.mem_univ _⟩ + rcases hPw with h | h + · have hxw := hS (x + w) h (a - w) (hA a ha).2 + have hxa : (x + w) + (a - w) = x + a := by + funext j; simp only [Pi.add_apply, Pi.sub_apply]; ring + rw [← hxa]; exact hxw + · have hxw := hS (x - w) h (a + w) (hA a ha).1 + have hxa : (x - w) + (a + w) = x + a := by + funext j; simp only [Pi.add_apply, Pi.sub_apply]; ring + rw [← hxa]; exact hxw + +/-- **Conservation du moment de base sous contenance, au niveau lifté** : +le moment coordonné de la scission-poussée, lu en coordonnée héritée +`i.castSucc`, est le moment de `P` en `i` — sous la même contention +`SupportContained S P {0, w, −w}` que `prodMoment_split_of_support` +(k2.0). C'est la composition du pont de moment `coordMoment_pushUp_castSucc` +(k2.6a, inconditionnel) avec l'identité de conservation de k2.0 : le +barycentre de base traverse la scission **puis** le pont de niveau sans +changement. + +Consommateur mesuré : le `rw [mean_split, sum_smul_inl, …] at hmem` du +pas de l'induction (`Komlos/SignedSums.lean` l.54), composante spatiale. -/ +theorem coordMoment_pushUp_split_of_support {d : ℕ} (w : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S : Finset (Fin d → ℤ)} + (hS : SupportContained S P ({0, w, -w} : Finset (Fin d → ℤ))) + (i : Fin d) : + coordMoment (pushUp (split w P)) + ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) i.castSucc + = coordMoment P S i := by + rw [coordMoment_pushUp_castSucc, prodMoment_split_of_support w hS i] + +/-- **Le moment de hauteur de la scission-poussée, au niveau lifté** : +lu en dernière coordonnée, il est le bit de scission `splitBit w P S` — +la composante de hauteur de `mean_split_of_support` (k2.0) à travers le +pont `coordMoment_pushUp_last` (k2.6a). Aucune contention n'est +requise : le moment de hauteur se lit tranche par tranche +(`heightMoment_split`, k2.0). + +Consommateur mesuré : le `rw [mean_split, …] at hmem` du pas de +l'induction (`Komlos/SignedSums.lean` l.54), composante de hauteur. -/ +theorem coordMoment_pushUp_split_last {d : ℕ} (w : Fin d → ℤ) + (P : (Fin d → ℤ) → ℝ) (S : Finset (Fin d → ℤ)) : + coordMoment (pushUp (split w P)) + ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) (Fin.last d) + = splitBit w P S := by + rw [coordMoment_pushUp_last, heightMoment_split] + +/-- **La contenance du cran suivant, sous la forme exacte que +l'induction consomme** : si `A` contient `0`, `u` et `−u` et est stable +par `± w`, la scission-poussée obéit à la contention `{0, snoc u 0, +−snoc u 0}` sur l'image liftée. C'est l'instance par monotonie +(`SupportContained.mono`) du transfert générique, les trois décalages +étant les images `snoc · 0` de `0` (`snoc 0 0 = 0`), `u` et `−u` +(`−snoc u 0 = snoc (−u) 0`). + +Le cran suivant de l'induction (k2.6c) scinde `pushUp (split w P)` dans +la direction `u` embarquée à hauteur nulle — les formes `_of_support` de +k2.0 (appliquées à la dimension `d + 1`) exigent exactement cette +contention à trois décalages. -/ +theorem supportContained_pushUp_split_three {d : ℕ} (w u : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S A : Finset (Fin d → ℤ)} + (hS : SupportContained S P A) + (hA : ∀ a ∈ A, a + w ∈ A ∧ a - w ∈ A) + (h0 : (0 : Fin d → ℤ) ∈ A) (hu : u ∈ A) (hu' : -u ∈ A) : + SupportContained ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) + (pushUp (split w P)) + ({0, Fin.snoc u 0, -(Fin.snoc u 0)} : Finset (Fin (d + 1) → ℤ)) := by + refine (supportContained_pushUp_split w hS hA).mono ?_ + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht + rcases ht with rfl | rfl | rfl + · refine Finset.mem_image.mpr ⟨0, h0, ?_⟩ + funext j + induction j using Fin.lastCases <;> simp + · exact Finset.mem_image.mpr ⟨u, hu, rfl⟩ + · refine Finset.mem_image.mpr ⟨-u, hu', ?_⟩ + funext j + induction j using Fin.lastCases <;> simp [Pi.neg_apply] + +end Discrepancy.Komlos diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit_en.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit_en.lean new file mode 100644 index 0000000000..0143f1ea6b --- /dev/null +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/LiftSplit_en.lean @@ -0,0 +1,222 @@ +/- +Copyright (c) 2026 Gabriel Dahia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Dahia +Adapted for `discrepancy_lean` (issue #17845, Karingula–Lovett distillation +arXiv:2609.20979): toolchain v4.33.0, Mathlib `db584cd6`, i18n convention #4980. + +The original Dahia source lives in the `gdahia/Komlos` repository (toolchain +v4.34.0, `Finsupp` framework over `E →₀ ℝ`). This module has **no +name-for-name oracle counterpart**: at the oracle, the induction hypothesis +applies to the split distribution in `E × ℝ` with no support precondition +whatsoever — the `Finsupp` transports its support for free +(`Finsupp.embDomain`); it is the lake's explicit `Finset` framework that +must pay for this transport, and that payment is precisely the subject of +this brick. + +**Scope of this commit** (brick k2.6b, `lake build SUCCESS` required, 0 +`sorry`) — the split under containment, read in the grown dimension +`Fin (d+1) → ℤ`: + +- `pushUp_split_ne_zero` — reading the pushed support: any mass of + `pushUp (split w P)` lives on the image of `liftUp` and originates + from a mass of `P` at distance `± w` from its base (the auxiliary + consumed by the containment transfer); +- `supportContained_pushUp_split` — **the containment transfer across + the split**: if `S` contains the support of `P` and its translates by + `A`, and `A` is stable under `± w`, then the lifted image + `(S ×ˢ univ).map liftUpEmb` contains the support of `pushUp (split w P)` + and its translates by the embedded shifts `Fin.snoc · 0` of `A`; +- `coordMoment_pushUp_split_of_support` — **conservation of the base + moment under containment, at the lifted level**: the coordinate moment + of the split-push, read on an inherited coordinate `i.castSucc`, is + the moment of `P` at `i` — the composition of the bridge + `coordMoment_pushUp_castSucc` (k2.6a) with `prodMoment_split_of_support` + (k2.0); +- `coordMoment_pushUp_split_last` — the height component: the moment of + the split-push on the last coordinate is the split bit + (`coordMoment_pushUp_last` (k2.6a) × `heightMoment_split` (k2.0)); +- `supportContained_pushUp_split_three` — the `{0, snoc u 0, −snoc u 0}` + form consumed by the next induction step: an instance of the transfer + by monotonicity (`SupportContained.mono`), the three shifts being the + `snoc · 0` images of `0`, `u`, `−u`. + +**Measured consumer**: the Lemma 1.4 induction (brick k2.6c, oracle +`Komlos/SignedSums.lean` l.44-55) applies its induction hypothesis to +`split (3 • v_last) P` in the grown space — on our side, to `pushUp +(split w P)` in `Fin (d+1) → ℤ`. The support preconditions and the +barycenter rewrites this call requires are exactly the five statements +above: containment to instantiate the hypothesis +(`supportContained_pushUp_split_three`), moments to rewrite the point it +produces (`coordMoment_pushUp_split_of_support` and `_last`, the lake +mirror of l.54's `rw [mean_split, …] at hmem`). + +**Deferred**: the induction itself (`SignedSums.lean` name for name, +k2.6c). The detailed state lives in `FORMAL_STATUS.md`. +-/ + +import Discrepancy.Komlos.Containment_en +import Discrepancy.Komlos.Lift_en +import Discrepancy.Komlos.MeanSplit_en +import Discrepancy.Komlos.Split_en + +/-! +# The split under containment, in the grown dimension (k2.6b) + +At the oracle, the induction step of Lemma 1.4 is free on the support +side: `split v P` is a `Finsupp` over `E × ℝ`, whose support is +transported by `Finsupp.embDomain` with no precondition. In the lake's +explicit `Finset` framework, the same step must **prove** that the +support of the split-push `pushUp (split w P)` is contained — and will +remain so at the next induction step — in the lifted image of the +starting support. + +This module pays that double cost in one brick: the **containment +transfer** (the split-pushed support obeys the containment transported +by `snoc · 0`) and the **conservation of moments under containment** at +the lifted level (the two components of `mean_split_of_support` k2.0 +read through the k2.6a bridges). +-/ + +namespace Discrepancy.Komlos_en + +/-- **Any mass of the split-push originates from a mass of `P` at +distance `± w`**: if `pushUp (split w P) z ≠ 0`, then `z` is on the +image of `liftUp` — `z = liftUp (x, b)` — and one of `P (x + w)`, +`P (x − w)` is nonzero. Half comes from `pushUp_eq_zero` (off the +image, the push is zero), the other half from the `max`/`min` shapes of +`split` (a nonzero half forces one of the two arguments nonzero). + +This is the support auxiliary consumed by the containment transfer +`supportContained_pushUp_split`: it reduces any support question on the +push to a support question on `P`. -/ +lemma pushUp_split_ne_zero {d : ℕ} (w : Fin d → ℤ) {P : (Fin d → ℤ) → ℝ} + {z : Fin (d + 1) → ℤ} (hz : pushUp (split w P) z ≠ 0) : + ∃ (x : Fin d → ℤ) (b : Bool), z = liftUp (x, b) ∧ + (P (x + w) ≠ 0 ∨ P (x - w) ≠ 0) := by + by_cases hex : ∃ y : (Fin d → ℤ) × Bool, liftUp y = z + · obtain ⟨⟨x, b⟩, rfl⟩ := hex + rw [pushUp_apply] at hz + refine ⟨x, b, rfl, ?_⟩ + cases b with + | false => + rw [split_apply_zero] at hz + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [max_eq_right h] at hz + exact Or.inr (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [max_eq_left h] at hz + exact Or.inl (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + | true => + rw [split_apply_one] at hz + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [min_eq_left h] at hz + exact Or.inl (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [min_eq_right h] at hz + exact Or.inr (by intro h0; rw [h0, mul_zero] at hz; exact hz rfl) + · rw [pushUp_eq_zero _ (fun y hy => hex ⟨y, hy⟩)] at hz + exact absurd rfl hz + +/-- **Containment transfer across the split**: if `S` contains the +support of `P` and its translates by `A`, and `A` is stable under +`± w`, then the lifted image `(S ×ˢ univ).map liftUpEmb` contains the +support of the split-push `pushUp (split w P)` and its translates by +the embedded shifts `Fin.snoc · 0` of `A`. + +This is the support precondition the induction step (k2.6c) must +establish to apply the induction hypothesis at dimension `d + 1`: at +the oracle (`Komlos/SignedSums.lean` l.44-53), the `Finsupp` pays this +transport for free (`Finsupp.embDomain`); the lake's `Finset` framework +pays it here. The stability of `A` under `± w` is the exact price of +the split: a mass point `P (x ± w) ≠ 0` moved by `a` lands at `x + a`, +reached from `x ± w` through the shift `a ∓ w ∈ A`. -/ +theorem supportContained_pushUp_split {d : ℕ} (w : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S A : Finset (Fin d → ℤ)} + (hS : SupportContained S P A) + (hA : ∀ a ∈ A, a + w ∈ A ∧ a - w ∈ A) : + SupportContained ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) + (pushUp (split w P)) (A.image (fun a => Fin.snoc a 0)) := by + intro z hz t ht + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp ht + obtain ⟨x, b, rfl, hPw⟩ := pushUp_split_ne_zero w hz + rw [liftUp_add_snoc] + show liftUp (x + a, b) ∈ (S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb + refine Finset.mem_map.mpr ⟨(x + a, b), ?_, liftUpEmb_apply _⟩ + refine Finset.mem_product.mpr ⟨?_, Finset.mem_univ _⟩ + rcases hPw with h | h + · have hxw := hS (x + w) h (a - w) (hA a ha).2 + have hxa : (x + w) + (a - w) = x + a := by + funext j; simp only [Pi.add_apply, Pi.sub_apply]; ring + rw [← hxa]; exact hxw + · have hxw := hS (x - w) h (a + w) (hA a ha).1 + have hxa : (x - w) + (a + w) = x + a := by + funext j; simp only [Pi.add_apply, Pi.sub_apply]; ring + rw [← hxa]; exact hxw + +/-- **Conservation of the base moment under containment, at the lifted +level**: the coordinate moment of the split-push, read on an inherited +coordinate `i.castSucc`, is the moment of `P` at `i` — under the same +containment `SupportContained S P {0, w, −w}` as +`prodMoment_split_of_support` (k2.0). This is the composition of the +moment bridge `coordMoment_pushUp_castSucc` (k2.6a, unconditional) with +the k2.0 conservation identity: the base barycenter crosses the split +**and then** the level bridge unchanged. + +Measured consumer: the `rw [mean_split, sum_smul_inl, …] at hmem` of +the induction step (`Komlos/SignedSums.lean` l.54), spatial component. -/ +theorem coordMoment_pushUp_split_of_support {d : ℕ} (w : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S : Finset (Fin d → ℤ)} + (hS : SupportContained S P ({0, w, -w} : Finset (Fin d → ℤ))) + (i : Fin d) : + coordMoment (pushUp (split w P)) + ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) i.castSucc + = coordMoment P S i := by + rw [coordMoment_pushUp_castSucc, prodMoment_split_of_support w hS i] + +/-- **The height moment of the split-push, at the lifted level**: read +on the last coordinate, it is the split bit `splitBit w P S` — the +height component of `mean_split_of_support` (k2.0) through the bridge +`coordMoment_pushUp_last` (k2.6a). No containment is required: the +height moment is read slice by slice (`heightMoment_split`, k2.0). + +Measured consumer: the `rw [mean_split, …] at hmem` of the induction +step (`Komlos/SignedSums.lean` l.54), height component. -/ +theorem coordMoment_pushUp_split_last {d : ℕ} (w : Fin d → ℤ) + (P : (Fin d → ℤ) → ℝ) (S : Finset (Fin d → ℤ)) : + coordMoment (pushUp (split w P)) + ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) (Fin.last d) + = splitBit w P S := by + rw [coordMoment_pushUp_last, heightMoment_split] + +/-- **The next step's containment, in the exact form the induction +consumes**: if `A` contains `0`, `u` and `−u` and is stable under +`± w`, the split-push obeys the containment `{0, snoc u 0, −snoc u 0}` +on the lifted image. This is the instance by monotonicity +(`SupportContained.mono`) of the generic transfer, the three shifts +being the `snoc · 0` images of `0` (`snoc 0 0 = 0`), `u` and `−u` +(`−snoc u 0 = snoc (−u) 0`). + +The next induction step (k2.6c) splits `pushUp (split w P)` in the +direction `u` embedded at height zero — the `_of_support` forms of +k2.0 (applied at dimension `d + 1`) require exactly this three-shift +containment. -/ +theorem supportContained_pushUp_split_three {d : ℕ} (w u : Fin d → ℤ) + {P : (Fin d → ℤ) → ℝ} {S A : Finset (Fin d → ℤ)} + (hS : SupportContained S P A) + (hA : ∀ a ∈ A, a + w ∈ A ∧ a - w ∈ A) + (h0 : (0 : Fin d → ℤ) ∈ A) (hu : u ∈ A) (hu' : -u ∈ A) : + SupportContained ((S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb) + (pushUp (split w P)) + ({0, Fin.snoc u 0, -(Fin.snoc u 0)} : Finset (Fin (d + 1) → ℤ)) := by + refine (supportContained_pushUp_split w hS hA).mono ?_ + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht + rcases ht with rfl | rfl | rfl + · refine Finset.mem_image.mpr ⟨0, h0, ?_⟩ + funext j + induction j using Fin.lastCases <;> simp + · exact Finset.mem_image.mpr ⟨u, hu, rfl⟩ + · refine Finset.mem_image.mpr ⟨-u, hu', ?_⟩ + funext j + induction j using Fin.lastCases <;> simp [Pi.neg_apply] + +end Discrepancy.Komlos_en diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums.lean index 24265be21a..cd9b4fe7d8 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums.lean +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums.lean @@ -8,13 +8,23 @@ 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/SignedSums.lean`, toolchain v4.34.0, cadre `Finsupp` sur `E →₀ ℝ`). L'assemblage final — l'itération `induction n with` du Lemme 1.4 — s'y lit -l.37-58. Ce module du lake ouvre la distillation : la première brique -`sum_smul_inl` y est livrée générique, la carte de consommation des organes -est mesurée en tête de module, la décision de cadre (option (c), -arbitrée en k2.6a) y est consignée. +l.37-58. Ce module du lake porte la distillation entière : la première brique +`sum_smul_inl` y est livrée générique (k2.6, la carte de consommation des +organes mesurée en tête de module, la décision de cadre — option (c) — +arbitrée en k2.6a), puis l'assemblage final lui-même (k2.6c) : le carré réel +`snocReal`, le transport d'enveloppe `mem_convexHull_map_snocReal`, la porte +inductive à deux ensembles `exists_colouring_aux` (fermeture `S` + support +exact `E` — le prix `Finset` du support canonique du `Finsupp` de l'oracle) +et l'énoncé public `exists_isColouring_mean_add_sum_mem_convexHull`. -/ import Discrepancy.Basic +import Discrepancy.Komlos.Containment +import Discrepancy.Komlos.Distribution +import Discrepancy.Komlos.Lift +import Discrepancy.Komlos.LiftSplit +import Discrepancy.Komlos.Pullback +import Discrepancy.Komlos.Split /-! # Sommes signées — assemblage du Lemme 1.4 (brique k2.6) @@ -64,4 +74,484 @@ lemma sum_smul_inl {n : ℕ} {E : Type*} [AddCommGroup E] [Module ℝ E] (∑ i, ε i • (v i, (0 : ℝ))) = (∑ i, ε i • v i, (0 : ℝ)) := by refine Prod.ext ?_ ?_ <;> simp [Prod.smul_mk, Prod.fst_sum, Prod.snd_sum] +/-! ### Brique k2.6c : l'assemblage final — l'induction du Lemme 1.4 -/ + +/-- **L'isomorphisme `snoc` côté réel** : `(Fin d → ℝ) × ℝ → (Fin (d+1) → ℝ)`, +`(z, t) ↦ snoc z t`. C'est la forme réelle du pont de niveau : le carré +`toReal ∘ liftUp = snoc ∘ toRealProd` (cf `toReal_liftUp`, k2.6a) dit que +transporter le support poussé dans la dimension agrandie revient à +`snoc`-er le support produit transporté — et c'est par là que la conclusion +d'induction à la dimension `d+1` nourrit le `pullback` de k2.4, énoncé dans +`(Fin d → ℝ) × ℝ`. -/ +def snocReal {d : ℕ} : ((Fin d → ℝ) × ℝ) → (Fin (d + 1) → ℝ) := + fun p => Fin.snoc p.1 p.2 + +lemma snocReal_apply_castSucc {d : ℕ} (p : (Fin d → ℝ) × ℝ) (j : Fin d) : + snocReal p j.castSucc = p.1 j := by simp [snocReal] + +lemma snocReal_apply_last {d : ℕ} (p : (Fin d → ℝ) × ℝ) : + snocReal p (Fin.last d) = p.2 := by simp [snocReal] + +/-- **Le carré réel** : `snocReal (toRealProd y) = toReal (liftUp y)` — +la lecture combinée de `toReal_liftUp` (k2.6a) et de la définition +`toRealProd` (k2.4). C'est la seule équation qui manque au transport des +enveloppes entre les deux lectures de la dimension agrandie. -/ +lemma snocReal_toRealProd {d : ℕ} (y : (Fin d → ℤ) × Bool) : + snocReal (toRealProd y) = toReal (liftUp y) := by + rw [toReal_liftUp] + funext j + simp [snocReal, toRealProd] + +lemma snocReal_injective {d : ℕ} : Function.Injective (snocReal (d := d)) := by + rintro ⟨z₁, t₁⟩ ⟨z₂, t₂⟩ h + have h1 : z₁ = z₂ := by + funext j + have := congrFun h j.castSucc + simpa [snocReal] using this + have h2 : t₁ = t₂ := by + have := congrFun h (Fin.last d) + simpa [snocReal] using this + exact Prod.ext h1 h2 + +/-- La version `Finset.Embedding` de `snocReal`, pour les `Finset.map` des +supports transportés. -/ +def snocRealEmb {d : ℕ} : ((Fin d → ℝ) × ℝ) ↪ (Fin (d + 1) → ℝ) := + ⟨snocReal, snocReal_injective⟩ + +lemma snocRealEmb_apply {d : ℕ} (p : (Fin d → ℝ) × ℝ) : snocRealEmb p = snocReal p := rfl + +/-- `snocReal` comme application `ℝ`-linéaire. C'est la structure qui +transporte les enveloppes convexes : `LinearMap.image_convexHull` identifie +l'enveloppe de l'image à l'image de l'enveloppe, et l'injectivité restitue +le point — le lemme de transport ci-dessous en découle immédiatement. -/ +def snocLM {d : ℕ} : ((Fin d → ℝ) × ℝ) →ₗ[ℝ] (Fin (d + 1) → ℝ) where + toFun p := snocReal p + map_add' p q := by + funext j + induction j using Fin.lastCases with + | last => simp [snocReal, Fin.snoc_last, Pi.add_apply] + | cast i => simp [snocReal, Fin.snoc_castSucc, Pi.add_apply] + map_smul' c p := by + funext j + induction j using Fin.lastCases with + | last => simp [snocReal, Fin.snoc_last, Pi.smul_apply, smul_eq_mul] + | cast i => simp [snocReal, Fin.snoc_castSucc, Pi.smul_apply, smul_eq_mul] + +/-- **Transport d'enveloppe à travers `snoc`** : appartenir à l'enveloppe +d'un ensemble fini `snoc`-é, c'est appartenir à l'enveloppe de l'ensemble +source. + +C'est l'organe qui referme le carré de diagramme pour l'assemblage k2.6c : +l'hypothèse d'induction conclut dans `Fin (d+1) → ℝ` (enveloppe du support +poussé transporté), le `pullback` de k2.4 consomme `(Fin d → ℝ) × ℝ` +(enveloppe du support produit transporté) — la correspondance est exactement +ce transport. Preuve : `snocReal` est linéaire (`snocLM`) et injective, et +`LinearMap.image_convexHull` commute l'enveloppe et l'image. -/ +lemma mem_convexHull_map_snocReal {d : ℕ} {E : Finset ((Fin d → ℝ) × ℝ)} + {p : (Fin d → ℝ) × ℝ} : + snocReal p ∈ convexHull ℝ + (↑(E.map snocRealEmb) : Set ((Fin (d + 1) → ℝ))) ↔ + p ∈ convexHull ℝ (↑E : Set ((Fin d → ℝ) × ℝ)) := by + have hset : (↑(E.map snocRealEmb) : Set ((Fin (d + 1) → ℝ))) + = (⇑snocLM) '' (↑E : Set ((Fin d → ℝ) × ℝ)) := by + rw [Finset.coe_map] + rfl + rw [hset, ← LinearMap.image_convexHull] + constructor + · rintro ⟨q, hq, hfq⟩ + rwa [snocReal_injective hfq] at hq + · exact fun h => ⟨p, h, rfl⟩ + +/-! ### La porte inductive : deux ensembles, `S` la fermeture et `E` le support -/ + +/-- **Lemme 1.4 (Karingula–Lovett), forme lake — la porte inductive**. + +Chez l'oracle (`gdahia/Komlos`, `SignedSums.lean` l.37-58), l'induction vit +sur les `Finsupp` : le support exact est canonique à chaque niveau, et la +conclusion d'hypothèse d'induction se consomme telle quelle par `pullback`. +Le cadre `Finset` explicite du lake doit payer ce transport : la contenance +`SupportContained` (k1.7) exige un support **fermé par décalages de `A`** +(les points de masse déplacés y atterrissent), tandis que le `pullback` +(k2.4) exige une enveloppe portée par le **support exact** de la scission +(`hSQ : ∀ y ∈ SQ, split v P y ≠ 0`). Ces deux rôles sont incompatibles sur +un seul `Finset` : la porte en porte donc deux — `S` (fermeture : masse, +moments, contenance) et `E` (support exact : enveloppe de la conclusion, +`E ⊆ S`). + +Au niveau suivant, `S'` est l'image liftée du produit plein (la contenance +y est transférée par `supportContained_pushUp_split`, k2.6b) et `E'` le +support exact poussé (`SQ.map liftUpEmb`, `SQ` le filtre des scissions non +nulles). Le pont entre les deux lectures est le carré +`snocReal ∘ toRealProd = toReal ∘ liftUp` plus le transport d'enveloppe +`mem_convexHull_map_snocReal` (ci-dessus). -/ +theorem exists_colouring_aux (n : ℕ) : + ∀ (d : ℕ) (S E : Finset (Fin d → ℤ)) (P : (Fin d → ℤ) → ℝ), + (∀ x, 0 ≤ P x) → (∑ x ∈ S, P x = 1) → + (∀ x, P x ≠ 0 → x ∈ E) → E ⊆ S → + ∀ A : Finset (Fin d → ℤ), 0 ∈ A → SupportContained S P A → + ∀ v : Fin n → (Fin d → ℤ), + (∀ i, v i ∈ A ∧ -v i ∈ A) → + (∀ a ∈ A, ∀ i, a + 3 • v i ∈ A ∧ a - 3 • v i ∈ A) → + (∀ i, shiftDistance S P (6 • v i) ≤ 3⁻¹) → + ∃ ε : Fin n → ℤ, (∀ i, ε i = 1 ∨ ε i = -1) ∧ + (fun j => coordMoment P S j + ∑ i, (ε i : ℝ) * (v i j : ℝ)) ∈ + convexHull ℝ + ↑(E.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ))) := by + induction n with + | zero => + intro d S E P hP0 hmass hE hES A hA0 hC v hAv hAstab hv + have hzero : ∀ x ∈ S, x ∉ E → P x = 0 := by + intro x _ hx + by_contra hp + exact hx (hE x hp) + have hmassE : ∑ x ∈ E, P x = 1 := by + rw [← hmass] + exact Finset.sum_subset hES hzero + have hmean := mean_mem_convexHull hP0 hmassE + refine ⟨fun _ => 1, fun i => i.elim0, ?_⟩ + have hfun : (fun j => coordMoment P S j + + ∑ i : Fin 0, ((fun _ => 1 : Fin 0 → ℤ) i : ℝ) * (v i j : ℝ)) + = (fun j => coordMoment P E j) := by + funext j + have hvan : ∀ x ∈ S, x ∉ E → P x * (x j : ℝ) = 0 := by + intro x _ hxE + by_contra hp + exact hxE (hE x (fun h0 => hp (by rw [h0]; ring))) + simp only [coordMoment] + rw [Finset.sum_subset hES hvan] + simp + rw [hfun] + exact hmean + | succ n ih => + intro d S E P hP0 hmass hE hES A hA0 hC v hAv hAstab hv + classical + -- Le vecteur de scission + set w : Fin d → ℤ := 3 • v (Fin.last n) with hw + -- Appartenances à A (chaînes de stabilité depuis 0) + have hm0 : (0 : Fin d → ℤ) ∈ A := hA0 + have hmw : 3 • v (Fin.last n) ∈ A := by + simpa using (hAstab 0 hA0 (Fin.last n)).1 + have hmnw : -(3 • v (Fin.last n)) ∈ A := by + simpa using (hAstab 0 hA0 (Fin.last n)).2 + have hmn3 : ∀ i : Fin (n + 1), -(3 • v i) ∈ A := by + intro i + simpa using (hAstab 0 hA0 i).2 + have mono3 : SupportContained S P ({0, w, -w} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw) + -- Les données de niveau d + 1 + set SQ : Finset ((Fin d → ℤ) × Bool) := + (S ×ˢ (Finset.univ : Finset Bool)).filter (fun y => split w P y ≠ 0) + with hSQ + set S' : Finset (Fin (d + 1) → ℤ) := + (S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb with hS' + set E' : Finset (Fin (d + 1) → ℤ) := SQ.map liftUpEmb with hE' + set A' : Finset (Fin (d + 1) → ℤ) := + A.image (fun a => Fin.snoc a 0) with hA' + -- Petites équations de snoc + have hadd_snoc : ∀ x y : Fin d → ℤ, + (Fin.snoc x 0 : Fin (d + 1) → ℤ) + Fin.snoc y 0 + = Fin.snoc (x + y) 0 := by + intro x y + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + have hsub_snoc : ∀ x y : Fin d → ℤ, + (Fin.snoc x 0 : Fin (d + 1) → ℤ) - Fin.snoc y 0 + = Fin.snoc (x - y) 0 := by + intro x y + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + have hneg_snoc : ∀ x : Fin d → ℤ, + -(Fin.snoc x 0 : Fin (d + 1) → ℤ) = Fin.snoc (-x) 0 := by + intro x + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + -- Les vecteurs embarqués se lisent comme des snoc à hauteur nulle + have hv'snoc : ∀ i : Fin n, + (liftUp (v i.castSucc, false) : Fin (d + 1) → ℤ) + = Fin.snoc (v i.castSucc) 0 := fun _ => rfl + -- Les arguments du niveau suivant + have hP0' : ∀ z, 0 ≤ pushUp (split w P) z := + fun z => pushUp_nonneg (split_nonneg hP0 w) z + have hmass' : ∑ z ∈ S', pushUp (split w P) z = 1 := by + rw [hS', pushUp_mass, split_mass_of_support w mono3] + exact hmass + have hsupp' : ∀ z, pushUp (split w P) z ≠ 0 → z ∈ E' := by + intro z hz + by_cases hy : ∃ y : (Fin d → ℤ) × Bool, liftUp y = z + · obtain ⟨y, rfl⟩ := hy + have hy' : split w P y ≠ 0 := by + rw [← pushUp_apply (split w P) y] + exact hz + -- l'antécédent vit dans S ×ˢ univ + have hy1 : y.1 ∈ S := by + obtain ⟨x, b⟩ := y + have hne : P (x + w) ≠ 0 ∨ P (x - w) ≠ 0 := by + cases b with + | false => + rw [split_apply_zero] at hy' + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [max_eq_right h] at hy' + exact Or.inr (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + · rw [max_eq_left h] at hy' + exact Or.inl (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + | true => + rw [split_apply_one] at hy' + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [min_eq_left h] at hy' + exact Or.inl (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + · rw [min_eq_right h] at hy' + exact Or.inr (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + rcases hne with h | h + · have hx := hC (x + w) h (-w) hmnw + simpa using hx + · have hx := hC (x - w) h w hmw + simpa using hx + refine Finset.mem_map.2 ⟨y, Finset.mem_filter.2 ⟨?_, hy'⟩, rfl⟩ + exact Finset.mem_product.2 ⟨hy1, Finset.mem_univ _⟩ + · exact absurd (pushUp_eq_zero (split w P) + (fun y hy' => hy ⟨y, hy'⟩)) hz + have hES' : E' ⊆ S' := by + intro z hz + obtain ⟨y, hy, rfl⟩ := Finset.mem_map.1 hz + exact Finset.mem_map.2 ⟨y, Finset.filter_subset _ _ hy, rfl⟩ + have hA0' : 0 ∈ A' := Finset.mem_image.2 ⟨0, hA0, by + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp⟩ + have hC' : SupportContained S' (pushUp (split w P)) A' := + supportContained_pushUp_split w hC + (fun a ha => ⟨(hAstab a ha (Fin.last n)).1, (hAstab a ha (Fin.last n)).2⟩) + have hAv' : ∀ i : Fin n, + liftUp (v i.castSucc, false) ∈ A' ∧ -liftUp (v i.castSucc, false) ∈ A' := by + intro i + constructor + · refine Finset.mem_image.2 ⟨v i.castSucc, (hAv i.castSucc).1, ?_⟩ + rw [hv'snoc i] + · refine Finset.mem_image.2 ⟨-v i.castSucc, (hAv i.castSucc).2, ?_⟩ + rw [hv'snoc i, hneg_snoc] + have hAstab' : ∀ a ∈ A', ∀ i : Fin n, + a + 3 • liftUp (v i.castSucc, false) ∈ A' + ∧ a - 3 • liftUp (v i.castSucc, false) ∈ A' := by + intro a' ha' i + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.1 ha' + rw [hA'] + have h1 : 3 • liftUp (v i.castSucc, false) + = Fin.snoc (3 • v i.castSucc) 0 := by + funext j + induction j using Fin.lastCases with + | last => simp [liftUp] + | cast k => simp [liftUp, Pi.smul_apply] + constructor + · refine Finset.mem_image.2 ⟨a + 3 • v i.castSucc, + (hAstab a ha i.castSucc).1, ?_⟩ + rw [h1, hadd_snoc] + · refine Finset.mem_image.2 ⟨a - 3 • v i.castSucc, + (hAstab a ha i.castSucc).2, ?_⟩ + rw [h1, hsub_snoc] + have hv' : ∀ i : Fin n, + shiftDistance S' (pushUp (split w P)) (6 • liftUp (v i.castSucc, false)) + ≤ 3⁻¹ := by + intro i + have h6 : 6 • liftUp (v i.castSucc, false) + = Fin.snoc (6 • v i.castSucc) 0 := by + funext j + induction j using Fin.lastCases with + | last => simp [liftUp] + | cast k => simp [liftUp, Pi.smul_apply] + -- la contention à six décalages + have hmn6 : -(3 • v i.castSucc) - 3 • v i.castSucc ∈ A := + (hAstab _ (hmn3 i.castSucc) i.castSucc).2 + have hwu : 3 • v (Fin.last n) - 3 • v i.castSucc ∈ A := + (hAstab _ hmw i.castSucc).2 + have hnwu : -(3 • v (Fin.last n)) - 3 • v i.castSucc ∈ A := + (hAstab _ hmnw i.castSucc).2 + have hid1 : (-(3 • v i.castSucc) - 3 • v i.castSucc : Fin d → ℤ) + = -(6 • v i.castSucc) := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, Pi.neg_apply] + ring + have hid2 : 3 • v (Fin.last n) - 3 • v i.castSucc - 3 • v i.castSucc + = w - 6 • v i.castSucc := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, hw] + ring + have hid3 : -(3 • v (Fin.last n)) - 3 • v i.castSucc - 3 • v i.castSucc + = -w - 6 • v i.castSucc := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, Pi.neg_apply, hw] + ring + have h6set : SupportContained S P + ({0, w, -w, -(6 • v i.castSucc), w - 6 • v i.castSucc, + -w - 6 • v i.castSucc} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl | rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw + · rw [← hid1] + exact hmn6 + · rw [← hid2] + exact (hAstab _ hwu i.castSucc).2 + · rw [← hid3] + exact (hAstab _ hnwu i.castSucc).2) + rw [h6, hS', shiftDistance_pushUp] + exact (shiftDistanceProd_split_le_of_support w (6 • v i.castSucc) + hP0 hmass h6set).trans (hv i.castSucc) + obtain ⟨ε', hε', hmem'⟩ := ih (d + 1) S' E' (pushUp (split w P)) + hP0' hmass' hsupp' hES' A' hA0' hC' + (fun i => liftUp (v i.castSucc, false)) hAv' hAstab' hv' + -- Le point de niveau d + 1, lu coordonnée par coordonnée + set z : Fin d → ℝ := fun k => + coordMoment P S k + ∑ i : Fin n, (ε' i : ℝ) * (v i.castSucc k : ℝ) + with hz + set β : ℝ := splitBit w P S with hb + have hpt : (fun j => coordMoment (pushUp (split w P)) S' j + + ∑ i : Fin n, (ε' i : ℝ) * ((liftUp (v i.castSucc, false)) j : ℝ)) + = Fin.snoc z β := by + funext j + induction j using Fin.lastCases with + | last => + show coordMoment (pushUp (split w P)) S' (Fin.last d) + + ∑ i : Fin n, (ε' i : ℝ) + * ((liftUp (v i.castSucc, false)) (Fin.last d) : ℝ) + = (Fin.snoc z β : Fin (d + 1) → ℝ) (Fin.last d) + rw [hS', coordMoment_pushUp_split_last w P S, hb] + simp + | cast k => + show coordMoment (pushUp (split w P)) S' k.castSucc + + ∑ i : Fin n, (ε' i : ℝ) + * ((liftUp (v i.castSucc, false)) k.castSucc : ℝ) + = (Fin.snoc z β : Fin (d + 1) → ℝ) k.castSucc + rw [hS', coordMoment_pushUp_split_of_support w mono3 k, hz] + simp + have hmem2 : (fun j => coordMoment (pushUp (split w P)) S' j + + ∑ i : Fin n, (ε' i : ℝ) * ((liftUp (v i.castSucc, false)) j : ℝ)) + ∈ convexHull ℝ + ↑(E'.map (⟨⇑toReal, toReal_injective⟩ : + (Fin (d + 1) → ℤ) ↪ (Fin (d + 1) → ℝ))) := hmem' + rw [hpt] at hmem2 + -- le carré : le support poussé transporté est l'image snocReal + have hmapE : E'.map + (⟨⇑toReal, toReal_injective⟩ : (Fin (d + 1) → ℤ) ↪ (Fin (d + 1) → ℝ)) + = (SQ.map toRealProdEmb).map snocRealEmb := by + apply Finset.ext + intro t + simp only [Finset.mem_map] + constructor + · rintro ⟨q, hq, rfl⟩ + obtain ⟨y, hy, rfl⟩ := Finset.mem_map.1 hq + exact ⟨toRealProd y, ⟨y, hy, rfl⟩, snocReal_toRealProd y⟩ + · rintro ⟨r, hr, rfl⟩ + obtain ⟨y, hy, rfl⟩ := hr + exact ⟨liftUp y, Finset.mem_map.2 ⟨y, hy, rfl⟩, + (snocReal_toRealProd y).symm⟩ + rw [hmapE] at hmem2 + have h1 : Fin.snoc z β = snocReal (z, β) := rfl + rw [h1] at hmem2 + obtain hmempb := (mem_convexHull_map_snocReal + (E := SQ.map toRealProdEmb) (p := (z, β))).mp hmem2 + -- la clé de hauteur : splitBit ≥ 1/3 + have hw2 : w + w = 6 • v (Fin.last n) := by + funext j + simp only [Pi.add_apply, Pi.smul_apply, hw] + ring + have hidww : -(w + w) = -w - w := by + funext j + simp only [Pi.add_apply, Pi.neg_apply, Pi.sub_apply, hw] + ring + have hP5 : SupportContained S P + ({0, w, -w, -w - w, -(w + w)} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw + · exact (hAstab _ hmnw (Fin.last n)).2 + · rw [hidww] + exact (hAstab _ hmnw (Fin.last n)).2) + have hβ : 3⁻¹ ≤ β := by + rw [hb, splitBit_eq_of_support w hP0 hmass hP5, hw2] + linarith [hv (Fin.last n)] + -- le rappel : z + e • toReal (v dernier) ∈ enveloppe du support de P + obtain ⟨e, he, hfin⟩ := pullback (v := w) (w := v (Fin.last n)) hP0 hE + (fun i => by rw [hw]; simp) + (fun y hy => (Finset.mem_filter.1 hy).2) + hβ hmempb + -- l'assemblage final + have hēe : ((if e = 1 then 1 else -1 : ℤ) : ℝ) = e := by + rcases he with h | h + · rw [if_pos h, h] + norm_num + · rw [if_neg (by rw [h]; norm_num), h] + norm_num + refine ⟨Fin.snoc ε' (if e = 1 then 1 else -1), ?_, ?_⟩ + · intro i + induction i using Fin.lastCases with + | last => + simp only [Fin.snoc_last] + rcases he with h | h + · exact Or.inl (by rw [if_pos h]) + · exact Or.inr (by rw [if_neg (by rw [h]; norm_num)]) + | cast j => simpa using hε' j + · have hfe : (fun j => coordMoment P S j + + ∑ i : Fin (n + 1), + ((Fin.snoc ε' (if e = 1 then 1 else -1) : Fin (n + 1) → ℤ) i : ℝ) + * (v i j : ℝ)) + = z + e • toReal (v (Fin.last n)) := by + funext j + rw [Fin.sum_univ_castSucc, Fin.snoc_last, hēe] + simp only [Fin.snoc_castSucc, Pi.add_apply, Pi.smul_apply, toReal_apply, hz] + ring + rw [hfe] + exact hfin + +/-- **Lemme 1.4 (Karingula–Lovett) — énoncé public** : si chaque `v i` +d'un ensemble `A` contenant `0` et stable par `± 3 • v j` a une distance de +décalage `≤ 1/3` pour `6 • v i`, il existe une coloration `ε` telle que le +barycentre de `P` augmenté des sommes signées appartienne à l'enveloppe +convexe du support transporté de `P`. + +La forme porte (`exists_colouring_aux`) conclut sur le support exact `E` ; +l'énoncé public le consomme avec `E := S.filter (P · ≠ 0)` et remonte à +l'enveloppe de `S` par monotonie — c'est la lecture lake de l'oracle +`gdahia/Komlos` (`SignedSums.lean` l.32-36), où le `Finsupp` porte son +support canonique. -/ +theorem exists_isColouring_mean_add_sum_mem_convexHull (n d : ℕ) + (S : Finset (Fin d → ℤ)) (P : (Fin d → ℤ) → ℝ) (hP0 : ∀ x, 0 ≤ P x) + (hmass : ∑ x ∈ S, P x = 1) (hPsupp : ∀ x, P x ≠ 0 → x ∈ S) + (A : Finset (Fin d → ℤ)) (hA0 : 0 ∈ A) (hC : SupportContained S P A) + (v : Fin n → (Fin d → ℤ)) (hAv : ∀ i, v i ∈ A ∧ -v i ∈ A) + (hAstab : ∀ a ∈ A, ∀ i, a + 3 • v i ∈ A ∧ a - 3 • v i ∈ A) + (hv : ∀ i, shiftDistance S P (6 • v i) ≤ 3⁻¹) : + ∃ ε : Fin n → ℤ, (∀ i, ε i = 1 ∨ ε i = -1) ∧ + (fun j => coordMoment P S j + ∑ i, (ε i : ℝ) * (v i j : ℝ)) ∈ + convexHull ℝ + ↑(S.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ))) := by + obtain ⟨ε, hε, hmem⟩ := exists_colouring_aux n d S (S.filter (fun x => P x ≠ 0)) P + hP0 hmass (fun x hx => Finset.mem_filter.2 ⟨hPsupp x hx, hx⟩) + (Finset.filter_subset _ _) A hA0 hC v hAv hAstab hv + refine ⟨ε, hε, ?_⟩ + have hsub : (S.filter (fun x => P x ≠ 0)).map + (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ)) + ⊆ S.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ)) := + Finset.map_subset_map.mpr (Finset.filter_subset _ _) + exact convexHull_mono (Finset.coe_subset.2 hsub) hmem + end Discrepancy.Komlos diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums_en.lean b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums_en.lean index 63069e76d2..3e5f26610f 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums_en.lean +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/SignedSums_en.lean @@ -8,13 +8,24 @@ arXiv:2609.20979): toolchain v4.33.0, Mathlib `db584cd6`, i18n convention #4980. The original Dahia source lives in the `gdahia/Komlos` repository (module `Komlos/SignedSums.lean`, toolchain v4.34.0, `Finsupp` framework over `E →₀ ℝ`). The final assembly — the `induction n with` iteration of -Lemma 1.4 — reads there at l.37-58. This lake module opens the -distillation: the first brick `sum_smul_inl` ships here in generic form, -the consumption map of the organs is measured at the top of the module, -and the framework decision (option (c), arbitrated in k2.6a) is recorded. +Lemma 1.4 — reads there at l.37-58. This lake module carries the whole +distillation: the first brick `sum_smul_inl` ships here in generic form +(k2.6, the consumption map of the organs measured at the top of the module, +the framework decision — option (c) — arbitrated in k2.6a), then the final +assembly itself (k2.6c): the real square `snocReal`, the hull transport +`mem_convexHull_map_snocReal`, the two-set inductive gate +`exists_colouring_aux` (closure `S` + exact support `E` — the `Finset` +price of the oracle's canonical `Finsupp` support) and the public statement +`exists_isColouring_mean_add_sum_mem_convexHull`. -/ import Discrepancy.Basic_en +import Discrepancy.Komlos.Containment_en +import Discrepancy.Komlos.Distribution_en +import Discrepancy.Komlos.Lift_en +import Discrepancy.Komlos.LiftSplit_en +import Discrepancy.Komlos.Pullback_en +import Discrepancy.Komlos.Split_en /-! # Signed sums — assembly of Lemma 1.4 (brick k2.6) @@ -65,4 +76,484 @@ lemma sum_smul_inl {n : ℕ} {E : Type*} [AddCommGroup E] [Module ℝ E] (∑ i, ε i • (v i, (0 : ℝ))) = (∑ i, ε i • v i, (0 : ℝ)) := by refine Prod.ext ?_ ?_ <;> simp [Prod.smul_mk, Prod.fst_sum, Prod.snd_sum] +/-! ### Brick k2.6c: the final assembly — the Lemma 1.4 induction -/ + +/-- **The real-side `snoc` isomorphism**: `(Fin d → ℝ) × ℝ → (Fin (d+1) → ℝ)`, +`(z, t) ↦ snoc z t`. It is the real form of the level bridge: the square +`toReal ∘ liftUp = snoc ∘ toRealProd` (cf `toReal_liftUp`, k2.6a) says that +transporting the pushed support into the grown dimension amounts to +`snoc`-ing the transported product support — and that is how the induction +conclusion at dimension `d+1` feeds the k2.4 `pullback`, stated in +`(Fin d → ℝ) × ℝ`. -/ +def snocReal {d : ℕ} : ((Fin d → ℝ) × ℝ) → (Fin (d + 1) → ℝ) := + fun p => Fin.snoc p.1 p.2 + +lemma snocReal_apply_castSucc {d : ℕ} (p : (Fin d → ℝ) × ℝ) (j : Fin d) : + snocReal p j.castSucc = p.1 j := by simp [snocReal] + +lemma snocReal_apply_last {d : ℕ} (p : (Fin d → ℝ) × ℝ) : + snocReal p (Fin.last d) = p.2 := by simp [snocReal] + +/-- **The real square**: `snocReal (toRealProd y) = toReal (liftUp y)` — +the combined reading of `toReal_liftUp` (k2.6a) and of the definition +`toRealProd` (k2.4). It is the only equation missing from the hull +transport between the two readings of the grown dimension. -/ +lemma snocReal_toRealProd {d : ℕ} (y : (Fin d → ℤ) × Bool) : + snocReal (toRealProd y) = toReal (liftUp y) := by + rw [toReal_liftUp] + funext j + simp [snocReal, toRealProd] + +lemma snocReal_injective {d : ℕ} : Function.Injective (snocReal (d := d)) := by + rintro ⟨z₁, t₁⟩ ⟨z₂, t₂⟩ h + have h1 : z₁ = z₂ := by + funext j + have := congrFun h j.castSucc + simpa [snocReal] using this + have h2 : t₁ = t₂ := by + have := congrFun h (Fin.last d) + simpa [snocReal] using this + exact Prod.ext h1 h2 + +/-- The `Finset.Embedding` version of `snocReal`, for the `Finset.map`s of +the transported supports. -/ +def snocRealEmb {d : ℕ} : ((Fin d → ℝ) × ℝ) ↪ (Fin (d + 1) → ℝ) := + ⟨snocReal, snocReal_injective⟩ + +lemma snocRealEmb_apply {d : ℕ} (p : (Fin d → ℝ) × ℝ) : snocRealEmb p = snocReal p := rfl + +/-- `snocReal` as an `ℝ`-linear map. This is the structure that transports +convex hulls: `LinearMap.image_convexHull` identifies the hull of the image +with the image of the hull, and injectivity restores the point — the +transport lemma below follows immediately. -/ +def snocLM {d : ℕ} : ((Fin d → ℝ) × ℝ) →ₗ[ℝ] (Fin (d + 1) → ℝ) where + toFun p := snocReal p + map_add' p q := by + funext j + induction j using Fin.lastCases with + | last => simp [snocReal, Fin.snoc_last, Pi.add_apply] + | cast i => simp [snocReal, Fin.snoc_castSucc, Pi.add_apply] + map_smul' c p := by + funext j + induction j using Fin.lastCases with + | last => simp [snocReal, Fin.snoc_last, Pi.smul_apply, smul_eq_mul] + | cast i => simp [snocReal, Fin.snoc_castSucc, Pi.smul_apply, smul_eq_mul] + +/-- **Hull transport through `snoc`**: belonging to the hull of a +`snoc`-ed finite set is belonging to the hull of the source set. + +This is the organ that closes the diagram square for the k2.6c assembly: +the induction hypothesis concludes in `Fin (d+1) → ℝ` (hull of the +transported pushed support), the k2.4 `pullback` consumes +`(Fin d → ℝ) × ℝ` (hull of the transported product support) — the +correspondence is exactly this transport. Proof: `snocReal` is linear +(`snocLM`) and injective, and `LinearMap.image_convexHull` commutes the +hull and the image. -/ +lemma mem_convexHull_map_snocReal {d : ℕ} {E : Finset ((Fin d → ℝ) × ℝ)} + {p : (Fin d → ℝ) × ℝ} : + snocReal p ∈ convexHull ℝ + (↑(E.map snocRealEmb) : Set ((Fin (d + 1) → ℝ))) ↔ + p ∈ convexHull ℝ (↑E : Set ((Fin d → ℝ) × ℝ)) := by + have hset : (↑(E.map snocRealEmb) : Set ((Fin (d + 1) → ℝ))) + = (⇑snocLM) '' (↑E : Set ((Fin d → ℝ) × ℝ)) := by + rw [Finset.coe_map] + rfl + rw [hset, ← LinearMap.image_convexHull] + constructor + · rintro ⟨q, hq, hfq⟩ + rwa [snocReal_injective hfq] at hq + · exact fun h => ⟨p, h, rfl⟩ + +/-! ### The inductive gate: two sets, `S` the closure and `E` the support -/ + +/-- **Lemma 1.4 (Karingula–Lovett), lake form — the inductive gate**. + +At the oracle (`gdahia/Komlos`, `SignedSums.lean` l.37-58), the induction +lives on `Finsupp`s: the exact support is canonical at every level, and the +induction-hypothesis conclusion is consumed as-is by `pullback`. The lake's +explicit `Finset` framework must pay for that transport: the containment +`SupportContained` (k1.7) demands a support **closed under shifts of `A`** +(the displaced mass points land there), whereas the `pullback` (k2.4) +demands a hull carried by the **exact support** of the split +(`hSQ : ∀ y ∈ SQ, split v P y ≠ 0`). Those two roles are incompatible on a +single `Finset`: the gate therefore carries two — `S` (closure: mass, +moments, containment) and `E` (exact support: hull of the conclusion, +`E ⊆ S`). + +At the next level, `S'` is the lifted image of the full product (containment +is transferred there by `supportContained_pushUp_split`, k2.6b) and `E'` the +pushed exact support (`SQ.map liftUpEmb`, `SQ` the filter of non-zero +splits). The bridge between the two readings is the square +`snocReal ∘ toRealProd = toReal ∘ liftUp` plus the hull transport +`mem_convexHull_map_snocReal` (above). -/ +theorem exists_colouring_aux (n : ℕ) : + ∀ (d : ℕ) (S E : Finset (Fin d → ℤ)) (P : (Fin d → ℤ) → ℝ), + (∀ x, 0 ≤ P x) → (∑ x ∈ S, P x = 1) → + (∀ x, P x ≠ 0 → x ∈ E) → E ⊆ S → + ∀ A : Finset (Fin d → ℤ), 0 ∈ A → SupportContained S P A → + ∀ v : Fin n → (Fin d → ℤ), + (∀ i, v i ∈ A ∧ -v i ∈ A) → + (∀ a ∈ A, ∀ i, a + 3 • v i ∈ A ∧ a - 3 • v i ∈ A) → + (∀ i, shiftDistance S P (6 • v i) ≤ 3⁻¹) → + ∃ ε : Fin n → ℤ, (∀ i, ε i = 1 ∨ ε i = -1) ∧ + (fun j => coordMoment P S j + ∑ i, (ε i : ℝ) * (v i j : ℝ)) ∈ + convexHull ℝ + ↑(E.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ))) := by + induction n with + | zero => + intro d S E P hP0 hmass hE hES A hA0 hC v hAv hAstab hv + have hzero : ∀ x ∈ S, x ∉ E → P x = 0 := by + intro x _ hx + by_contra hp + exact hx (hE x hp) + have hmassE : ∑ x ∈ E, P x = 1 := by + rw [← hmass] + exact Finset.sum_subset hES hzero + have hmean := mean_mem_convexHull hP0 hmassE + refine ⟨fun _ => 1, fun i => i.elim0, ?_⟩ + have hfun : (fun j => coordMoment P S j + + ∑ i : Fin 0, ((fun _ => 1 : Fin 0 → ℤ) i : ℝ) * (v i j : ℝ)) + = (fun j => coordMoment P E j) := by + funext j + have hvan : ∀ x ∈ S, x ∉ E → P x * (x j : ℝ) = 0 := by + intro x _ hxE + by_contra hp + exact hxE (hE x (fun h0 => hp (by rw [h0]; ring))) + simp only [coordMoment] + rw [Finset.sum_subset hES hvan] + simp + rw [hfun] + exact hmean + | succ n ih => + intro d S E P hP0 hmass hE hES A hA0 hC v hAv hAstab hv + classical + -- The splitting vector + set w : Fin d → ℤ := 3 • v (Fin.last n) with hw + -- Memberships in A (stability chains from 0) + have hm0 : (0 : Fin d → ℤ) ∈ A := hA0 + have hmw : 3 • v (Fin.last n) ∈ A := by + simpa using (hAstab 0 hA0 (Fin.last n)).1 + have hmnw : -(3 • v (Fin.last n)) ∈ A := by + simpa using (hAstab 0 hA0 (Fin.last n)).2 + have hmn3 : ∀ i : Fin (n + 1), -(3 • v i) ∈ A := by + intro i + simpa using (hAstab 0 hA0 i).2 + have mono3 : SupportContained S P ({0, w, -w} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw) + -- The level-(d + 1) data + set SQ : Finset ((Fin d → ℤ) × Bool) := + (S ×ˢ (Finset.univ : Finset Bool)).filter (fun y => split w P y ≠ 0) + with hSQ + set S' : Finset (Fin (d + 1) → ℤ) := + (S ×ˢ (Finset.univ : Finset Bool)).map liftUpEmb with hS' + set E' : Finset (Fin (d + 1) → ℤ) := SQ.map liftUpEmb with hE' + set A' : Finset (Fin (d + 1) → ℤ) := + A.image (fun a => Fin.snoc a 0) with hA' + -- Small snoc equations + have hadd_snoc : ∀ x y : Fin d → ℤ, + (Fin.snoc x 0 : Fin (d + 1) → ℤ) + Fin.snoc y 0 + = Fin.snoc (x + y) 0 := by + intro x y + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + have hsub_snoc : ∀ x y : Fin d → ℤ, + (Fin.snoc x 0 : Fin (d + 1) → ℤ) - Fin.snoc y 0 + = Fin.snoc (x - y) 0 := by + intro x y + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + have hneg_snoc : ∀ x : Fin d → ℤ, + -(Fin.snoc x 0 : Fin (d + 1) → ℤ) = Fin.snoc (-x) 0 := by + intro x + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp + -- The embedded vectors read as snoc's at zero height + have hv'snoc : ∀ i : Fin n, + (liftUp (v i.castSucc, false) : Fin (d + 1) → ℤ) + = Fin.snoc (v i.castSucc) 0 := fun _ => rfl + -- The arguments of the next level + have hP0' : ∀ z, 0 ≤ pushUp (split w P) z := + fun z => pushUp_nonneg (split_nonneg hP0 w) z + have hmass' : ∑ z ∈ S', pushUp (split w P) z = 1 := by + rw [hS', pushUp_mass, split_mass_of_support w mono3] + exact hmass + have hsupp' : ∀ z, pushUp (split w P) z ≠ 0 → z ∈ E' := by + intro z hz + by_cases hy : ∃ y : (Fin d → ℤ) × Bool, liftUp y = z + · obtain ⟨y, rfl⟩ := hy + have hy' : split w P y ≠ 0 := by + rw [← pushUp_apply (split w P) y] + exact hz + -- the antecedent lives in S ×ˢ univ + have hy1 : y.1 ∈ S := by + obtain ⟨x, b⟩ := y + have hne : P (x + w) ≠ 0 ∨ P (x - w) ≠ 0 := by + cases b with + | false => + rw [split_apply_zero] at hy' + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [max_eq_right h] at hy' + exact Or.inr (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + · rw [max_eq_left h] at hy' + exact Or.inl (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + | true => + rw [split_apply_one] at hy' + rcases le_total (P (x + w)) (P (x - w)) with h | h + · rw [min_eq_left h] at hy' + exact Or.inl (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + · rw [min_eq_right h] at hy' + exact Or.inr (by intro h0; rw [h0, mul_zero] at hy'; exact hy' rfl) + rcases hne with h | h + · have hx := hC (x + w) h (-w) hmnw + simpa using hx + · have hx := hC (x - w) h w hmw + simpa using hx + refine Finset.mem_map.2 ⟨y, Finset.mem_filter.2 ⟨?_, hy'⟩, rfl⟩ + exact Finset.mem_product.2 ⟨hy1, Finset.mem_univ _⟩ + · exact absurd (pushUp_eq_zero (split w P) + (fun y hy' => hy ⟨y, hy'⟩)) hz + have hES' : E' ⊆ S' := by + intro z hz + obtain ⟨y, hy, rfl⟩ := Finset.mem_map.1 hz + exact Finset.mem_map.2 ⟨y, Finset.filter_subset _ _ hy, rfl⟩ + have hA0' : 0 ∈ A' := Finset.mem_image.2 ⟨0, hA0, by + funext j + induction j using Fin.lastCases with + | last => simp + | cast i => simp⟩ + have hC' : SupportContained S' (pushUp (split w P)) A' := + supportContained_pushUp_split w hC + (fun a ha => ⟨(hAstab a ha (Fin.last n)).1, (hAstab a ha (Fin.last n)).2⟩) + have hAv' : ∀ i : Fin n, + liftUp (v i.castSucc, false) ∈ A' ∧ -liftUp (v i.castSucc, false) ∈ A' := by + intro i + constructor + · refine Finset.mem_image.2 ⟨v i.castSucc, (hAv i.castSucc).1, ?_⟩ + rw [hv'snoc i] + · refine Finset.mem_image.2 ⟨-v i.castSucc, (hAv i.castSucc).2, ?_⟩ + rw [hv'snoc i, hneg_snoc] + have hAstab' : ∀ a ∈ A', ∀ i : Fin n, + a + 3 • liftUp (v i.castSucc, false) ∈ A' + ∧ a - 3 • liftUp (v i.castSucc, false) ∈ A' := by + intro a' ha' i + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.1 ha' + rw [hA'] + have h1 : 3 • liftUp (v i.castSucc, false) + = Fin.snoc (3 • v i.castSucc) 0 := by + funext j + induction j using Fin.lastCases with + | last => simp [liftUp] + | cast k => simp [liftUp, Pi.smul_apply] + constructor + · refine Finset.mem_image.2 ⟨a + 3 • v i.castSucc, + (hAstab a ha i.castSucc).1, ?_⟩ + rw [h1, hadd_snoc] + · refine Finset.mem_image.2 ⟨a - 3 • v i.castSucc, + (hAstab a ha i.castSucc).2, ?_⟩ + rw [h1, hsub_snoc] + have hv' : ∀ i : Fin n, + shiftDistance S' (pushUp (split w P)) (6 • liftUp (v i.castSucc, false)) + ≤ 3⁻¹ := by + intro i + have h6 : 6 • liftUp (v i.castSucc, false) + = Fin.snoc (6 • v i.castSucc) 0 := by + funext j + induction j using Fin.lastCases with + | last => simp [liftUp] + | cast k => simp [liftUp, Pi.smul_apply] + -- the six-shift contention + have hmn6 : -(3 • v i.castSucc) - 3 • v i.castSucc ∈ A := + (hAstab _ (hmn3 i.castSucc) i.castSucc).2 + have hwu : 3 • v (Fin.last n) - 3 • v i.castSucc ∈ A := + (hAstab _ hmw i.castSucc).2 + have hnwu : -(3 • v (Fin.last n)) - 3 • v i.castSucc ∈ A := + (hAstab _ hmnw i.castSucc).2 + have hid1 : (-(3 • v i.castSucc) - 3 • v i.castSucc : Fin d → ℤ) + = -(6 • v i.castSucc) := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, Pi.neg_apply] + ring + have hid2 : 3 • v (Fin.last n) - 3 • v i.castSucc - 3 • v i.castSucc + = w - 6 • v i.castSucc := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, hw] + ring + have hid3 : -(3 • v (Fin.last n)) - 3 • v i.castSucc - 3 • v i.castSucc + = -w - 6 • v i.castSucc := by + funext j + simp only [Pi.sub_apply, Pi.smul_apply, Pi.neg_apply, hw] + ring + have h6set : SupportContained S P + ({0, w, -w, -(6 • v i.castSucc), w - 6 • v i.castSucc, + -w - 6 • v i.castSucc} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl | rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw + · rw [← hid1] + exact hmn6 + · rw [← hid2] + exact (hAstab _ hwu i.castSucc).2 + · rw [← hid3] + exact (hAstab _ hnwu i.castSucc).2) + rw [h6, hS', shiftDistance_pushUp] + exact (shiftDistanceProd_split_le_of_support w (6 • v i.castSucc) + hP0 hmass h6set).trans (hv i.castSucc) + obtain ⟨ε', hε', hmem'⟩ := ih (d + 1) S' E' (pushUp (split w P)) + hP0' hmass' hsupp' hES' A' hA0' hC' + (fun i => liftUp (v i.castSucc, false)) hAv' hAstab' hv' + -- The level-(d + 1) point, read coordinate by coordinate + set z : Fin d → ℝ := fun k => + coordMoment P S k + ∑ i : Fin n, (ε' i : ℝ) * (v i.castSucc k : ℝ) + with hz + set β : ℝ := splitBit w P S with hb + have hpt : (fun j => coordMoment (pushUp (split w P)) S' j + + ∑ i : Fin n, (ε' i : ℝ) * ((liftUp (v i.castSucc, false)) j : ℝ)) + = Fin.snoc z β := by + funext j + induction j using Fin.lastCases with + | last => + show coordMoment (pushUp (split w P)) S' (Fin.last d) + + ∑ i : Fin n, (ε' i : ℝ) + * ((liftUp (v i.castSucc, false)) (Fin.last d) : ℝ) + = (Fin.snoc z β : Fin (d + 1) → ℝ) (Fin.last d) + rw [hS', coordMoment_pushUp_split_last w P S, hb] + simp + | cast k => + show coordMoment (pushUp (split w P)) S' k.castSucc + + ∑ i : Fin n, (ε' i : ℝ) + * ((liftUp (v i.castSucc, false)) k.castSucc : ℝ) + = (Fin.snoc z β : Fin (d + 1) → ℝ) k.castSucc + rw [hS', coordMoment_pushUp_split_of_support w mono3 k, hz] + simp + have hmem2 : (fun j => coordMoment (pushUp (split w P)) S' j + + ∑ i : Fin n, (ε' i : ℝ) * ((liftUp (v i.castSucc, false)) j : ℝ)) + ∈ convexHull ℝ + ↑(E'.map (⟨⇑toReal, toReal_injective⟩ : + (Fin (d + 1) → ℤ) ↪ (Fin (d + 1) → ℝ))) := hmem' + rw [hpt] at hmem2 + -- the square: the transported pushed support is the snocReal image + have hmapE : E'.map + (⟨⇑toReal, toReal_injective⟩ : (Fin (d + 1) → ℤ) ↪ (Fin (d + 1) → ℝ)) + = (SQ.map toRealProdEmb).map snocRealEmb := by + apply Finset.ext + intro t + simp only [Finset.mem_map] + constructor + · rintro ⟨q, hq, rfl⟩ + obtain ⟨y, hy, rfl⟩ := Finset.mem_map.1 hq + exact ⟨toRealProd y, ⟨y, hy, rfl⟩, snocReal_toRealProd y⟩ + · rintro ⟨r, hr, rfl⟩ + obtain ⟨y, hy, rfl⟩ := hr + exact ⟨liftUp y, Finset.mem_map.2 ⟨y, hy, rfl⟩, + (snocReal_toRealProd y).symm⟩ + rw [hmapE] at hmem2 + have h1 : Fin.snoc z β = snocReal (z, β) := rfl + rw [h1] at hmem2 + obtain hmempb := (mem_convexHull_map_snocReal + (E := SQ.map toRealProdEmb) (p := (z, β))).mp hmem2 + -- the height key: splitBit ≥ 1/3 + have hw2 : w + w = 6 • v (Fin.last n) := by + funext j + simp only [Pi.add_apply, Pi.smul_apply, hw] + ring + have hidww : -(w + w) = -w - w := by + funext j + simp only [Pi.add_apply, Pi.neg_apply, Pi.sub_apply, hw] + ring + have hP5 : SupportContained S P + ({0, w, -w, -w - w, -(w + w)} : Finset (Fin d → ℤ)) := + hC.mono (by + intro t ht + simp only [Finset.mem_insert, Finset.mem_singleton] at ht ⊢ + rcases ht with rfl | rfl | rfl | rfl | rfl + · exact hm0 + · exact hmw + · exact hmnw + · exact (hAstab _ hmnw (Fin.last n)).2 + · rw [hidww] + exact (hAstab _ hmnw (Fin.last n)).2) + have hβ : 3⁻¹ ≤ β := by + rw [hb, splitBit_eq_of_support w hP0 hmass hP5, hw2] + linarith [hv (Fin.last n)] + -- the recall: z + e • toReal (v last) ∈ hull of the support of P + obtain ⟨e, he, hfin⟩ := pullback (v := w) (w := v (Fin.last n)) hP0 hE + (fun i => by rw [hw]; simp) + (fun y hy => (Finset.mem_filter.1 hy).2) + hβ hmempb + -- the final assembly + have hēe : ((if e = 1 then 1 else -1 : ℤ) : ℝ) = e := by + rcases he with h | h + · rw [if_pos h, h] + norm_num + · rw [if_neg (by rw [h]; norm_num), h] + norm_num + refine ⟨Fin.snoc ε' (if e = 1 then 1 else -1), ?_, ?_⟩ + · intro i + induction i using Fin.lastCases with + | last => + simp only [Fin.snoc_last] + rcases he with h | h + · exact Or.inl (by rw [if_pos h]) + · exact Or.inr (by rw [if_neg (by rw [h]; norm_num)]) + | cast j => simpa using hε' j + · have hfe : (fun j => coordMoment P S j + + ∑ i : Fin (n + 1), + ((Fin.snoc ε' (if e = 1 then 1 else -1) : Fin (n + 1) → ℤ) i : ℝ) + * (v i j : ℝ)) + = z + e • toReal (v (Fin.last n)) := by + funext j + rw [Fin.sum_univ_castSucc, Fin.snoc_last, hēe] + simp only [Fin.snoc_castSucc, Pi.add_apply, Pi.smul_apply, toReal_apply, hz] + ring + rw [hfe] + exact hfin + +/-- **Lemma 1.4 (Karingula–Lovett) — public statement**: if every `v i` +of a set `A` containing `0` and stable under `± 3 • v j` has shift distance +`≤ 1/3` for `6 • v i`, then there exists a coloring `ε` such that the +barycenter of `P` augmented by the signed sums belongs to the convex hull +of the transported support of `P`. + +The gate form (`exists_colouring_aux`) concludes on the exact support `E`; +the public statement consumes it with `E := S.filter (P · ≠ 0)` and climbs +back to the hull of `S` by monotonicity — this is the lake reading of the +oracle `gdahia/Komlos` (`SignedSums.lean` l.32-36), where the `Finsupp` +carries its canonical support. -/ +theorem exists_isColouring_mean_add_sum_mem_convexHull (n d : ℕ) + (S : Finset (Fin d → ℤ)) (P : (Fin d → ℤ) → ℝ) (hP0 : ∀ x, 0 ≤ P x) + (hmass : ∑ x ∈ S, P x = 1) (hPsupp : ∀ x, P x ≠ 0 → x ∈ S) + (A : Finset (Fin d → ℤ)) (hA0 : 0 ∈ A) (hC : SupportContained S P A) + (v : Fin n → (Fin d → ℤ)) (hAv : ∀ i, v i ∈ A ∧ -v i ∈ A) + (hAstab : ∀ a ∈ A, ∀ i, a + 3 • v i ∈ A ∧ a - 3 • v i ∈ A) + (hv : ∀ i, shiftDistance S P (6 • v i) ≤ 3⁻¹) : + ∃ ε : Fin n → ℤ, (∀ i, ε i = 1 ∨ ε i = -1) ∧ + (fun j => coordMoment P S j + ∑ i, (ε i : ℝ) * (v i j : ℝ)) ∈ + convexHull ℝ + ↑(S.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ))) := by + obtain ⟨ε, hε, hmem⟩ := exists_colouring_aux n d S (S.filter (fun x => P x ≠ 0)) P + hP0 hmass (fun x hx => Finset.mem_filter.2 ⟨hPsupp x hx, hx⟩) + (Finset.filter_subset _ _) A hA0 hC v hAv hAstab hv + refine ⟨ε, hε, ?_⟩ + have hsub : (S.filter (fun x => P x ≠ 0)).map + (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ)) + ⊆ S.map (⟨⇑toReal, toReal_injective⟩ : (Fin d → ℤ) ↪ (Fin d → ℝ)) := + Finset.map_subset_map.mpr (Finset.filter_subset _ _) + exact convexHull_mono (Finset.coe_subset.2 hsub) hmem + end Discrepancy.Komlos_en diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md index 7a4530630b..a5c2aeb14e 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md @@ -67,7 +67,9 @@ boutes `k1..k5` ci-dessous ; issue de suivi : #17845. | **k2.4** | `Discrepancy.Komlos.pullback` : **le pas complet du pullback** — le théorème que k2.1 (algèbre), k2.2 (convexité) et k2.3 (transport) ont préparé, porté de `Komlos/Pullback.lean` l.55-92. Briques closes : `toRealProd` + `toRealProd_injective` + `toRealProdEmb` (l'embedding **produit** `(Fin d → ℤ) × Bool → (Fin d → ℝ) × ℝ` — la hauteur `Bool` du lake devient la coordonnée réelle `β` de l'oracle, `false ↦ 0` / `true ↦ 1` ; injectivité par `toReal_injective.eq_iff` + séparation `0 ≠ 1` — le ticket du `Finset.map` du support transporté), `mem_map_toRealProd_snd` (hauteurs de l'image dans `{0, 1}` — le pendant fini de `snd_eq_zero_or_one_of_mem_support_split`), `split_apply_zero_ne_iff` / `split_apply_one_ne_iff` (les **caractérisations de support** de la scission sous `P ≥ 0`, lecture point-par-point des `mk_zero/one_mem_support_split` de l'oracle — le `max` exige la disjonction, le `min` la conjonction) et **le théorème `pullback`** : `(z, β)` dans l'enveloppe du support transporté de `split v P`, `v = 3·w` coordonnée par coordonnée, `β ≥ 1/3` ⇒ un signe `e ∈ {±1}` ramène `z + e • toReal w` dans l'enveloppe du support transporté de `P`. **Trois écarts de cadre arbitrés** : (a) `z` vit côté `ℝ` (le consommateur final Lemme 1.4 produit un barycentre côté grille réelle, d'où l'hypothèse dans l'image transportée) ; (b) `hSQ` exactitude du support de la scission en **hypothèse** (l'oracle la calcule via `Finsupp.support` ; le cadre `Finset` explicite la exige) ; (c) `hPsupp` relaie le support de `P`. Preuve décomposée sur les ingrédients k2.1-k2.3 : `Finset.mem_convexHull'` (`Analysis.Convex/Combination.lean:415` — vérifié au pin, forme `∃ w` exacte) décompose `(z, β)` en poids ; `Finset.abs_sum_le_sum_abs` (`Algebra/Order/BigOperators/Group/Finset.lean:315` — **dans le namespace `Finset`** au pin, l'identifiant nu n'existe pas) borne la part des poids hauteur 0 ; `exists_sign_mul_add_eq` (k2.1) produit `e` et `c` ; chaque point revient dans l'enveloppe par `add_smul_mem_convexHull` (k2.2, tranches hautes) ou l'appartenance directe d'une extrémité via `toReal_mem_map_iff` (k2.3, tranches basses) ; `sum_smul_mem_convexHull` (k2.2) referme. `sum_smul_inl` (`split.lean:50`) **reporté** : le port n'en a pas eu besoin (la décomposition `(z, β)` passe par `Prod.fst_sum`/`Prod.snd_sum` ; aucun consommateur mesuré). Module FR + jumeau `_en`, étendus (pas de nouveau fichier). 0 `sorry`. | brique k2 (pas complet) | **PROUVÉ** (k2.4, 10-04, `lake build` local — ciblé deux jumeaux 0 erreur **0 warning** (~30 s chacun), puis full-lib `8750 jobs` *Build completed successfully* ; `distinct_code_sorry = 0` ; jumeaux i18n `14/14 byte-identical` — voir PR) | ce PR (stack sur #19081) | | **k2.5** | `Discrepancy.Komlos.mean_mem_convexHull` : **le cas de base `n = 0` de l'assemblage** — porté de `Komlos/Distribution.lean` l.105, module de l'oracle repris **nom pour nom** (nouveau `Distribution.lean` + jumeau `_en` ; le glob `.submodules` du lakefile le découvre — `Komlos.lean` n'est pas un agrégateur, aucun enregistrement). Énoncé : le barycentre — lu coordonnée par coordonnée, `fun i => coordMoment P S i` (k2.0) — d'une distribution positive (`hP`) de masse 1 (`hmass`) sur `S` appartient à l'enveloppe convexe du support **transporté** `S.map ⟨toReal, toReal_injective⟩` — la même forme exacte que la conclusion de `pullback` (k2.4), que la base `n = 0` de l'assemblage consommera (`SignedSums.lean` l.42). **La clé du port** : chez l'oracle le one-liner (`Finset.mem_convexHull'.2 ⟨S, …⟩`) tient parce que les poids demandés sont le `Finsupp` lui-même, **nul hors support par construction** ; le cadre `Finset` explicite du lake exigeait de construire ce poids sur la grille réelle — et c'est **déjà l'organe `push` de k2.3** (`push toReal P` sur `Function.extend`, nul hors image par construction, équivalent du `Finsupp.embDomain` de l'oracle) : aucun poids à inventer, la preuve redevient le one-liner oracle avec ses trois composantes lisant les organes k2.3 — `push_apply` (positivité des poids transportés, chaque point du support transporté relisant `P` à son unique antécédent), `push_mass` (masse conservée, le `mass_push` de l'oracle), `coordMoment_toReal` (le point produit, le `mean_push` de l'oracle — le barycente affirmé dans l'enveloppe est exactement celui que les moments k2.0 calculent). **Trois écarts de cadre arbitrés** (même famille que k2.4) : (a) le `mean` se lit coordonnée par coordonnée (`Fin d → ℤ` n'est pas un `ℝ`-module, bloqueur mesuré en k2.2) ; (b) `IsDist` devient deux hypothèses `hP`/`hmass` (la structure `Finsupp` portait ces faits par construction) ; (c) le support de l'énoncé est `S` transporté exact, pas un `s ⊇ support` arbitraire. **Reportés avec raison mesurée** : l'infrastructure sup/inf du module oracle (`mass_sup_add_mass_inf`, `mean_sup_add_mean_inf`, `support_inf_subset`, `support_sup_subset`) — aucun consommateur dans notre cadre (la préservation de masse à la scission est `split_mass` k1.2, consommée en hypothèse chaînée) ; et **`sum_smul_inl` (`split.lean:50`) acquiert un consommateur mesuré** par la lecture k1.7 du pas (`SignedSums.lean` l.53 : `rw [mean_split, sum_smul_inl, Prod.mk_add_mk, add_zero] at hmem`) — livré avec k2.6 où sa forme exacte se fixe. 0 `sorry`. | brique k2 (cas de base) | **PROUVÉ** (k2.5, 10-04, `lake build` local — ciblé deux jumeaux 0 erreur **0 warning** (31 s chacun, SUCCESS au premier round) ; `distinct_code_sorry = 0` ; jumeaux i18n `15/15 byte-identical` — voir PR) | ce PR (stack sur #19084) | | **k2.6a** | `Discrepancy.Komlos.liftUp` : **le pont de niveau — premier préalable mécanique de l'assemblage k2.6**. Ce module n'a **pas de contrepartie oracle**, et cette absence est le fait technique que la brique documente : le Lemme 1.4 de l'oracle est quantifié sur `E` **variable** (`induction n with`, `SignedSums.lean` l.37), son hypothèse d'induction s'applique donc dans l'espace grandi `E × ℝ` (l.52) sans rien construire ; la base du lake `Fin d → ℤ` est **fixe**, et aucun organe k1.x/k2.x ne s'applique à une distribution sur un type réellement différent. **Design-gate arbitré et consigné dans le header du module** : (a) généralisation abstraite `X × Bool` et (b) espace produit itéré `(Fin d → ℤ) × (Fin n → Bool)` **rejetées** — toutes deux une seconde formalisation de la chaîne entière ; **(c) retenue : l'espace qui grandit est `Fin (d + k) → ℤ`**, réalisé par `liftUp : ((Fin d → ℤ) × Bool) → (Fin (d+1) → ℤ)` (partie spatiale par `Fin.snoc`, hauteur `Bool` comme l'entier `{0,1}` à la dernière coordonnée — la contrepartie discrète du `incl b : E ↪ E × ℝ` de l'oracle, `Split.lean` l.31), le miroir d'induction étant `induction n generalizing d` : chaque brique du lake étant générique en `d`, elles s'appliquent **telles quelles à la dimension suivante**. **Livré** : `liftUp` + `liftUp_injective` + `liftUpEmb`/`liftUpEmb_apply` (le pont syntaxique que les rewrites sur les images `Finset.map` exigent — mesuré au round 1 : `rw` ne voit pas `liftUpEmb y` comme `liftUp ?y`) ; `liftUp_add_snoc` (les translations de hauteur nulle commutent avec l'embedding — l'équation qui fait marcher le pont de distance) ; `pushUp` — la poussée le long de `liftUp` sur le **même pattern `Function.extend` que l'organe `push` de k2.3** (et non cet organe : celui-ci est typé sur un morphisme additif, le côté produit n'a pas d'opposé), avec sa lecture `apply`/`eq_zero`/`nonneg`/`mass` ; les **deux ponts de moment** (`coordMoment_pushUp_castSucc` = `prodMoment`, `coordMoment_pushUp_last` = `heightMoment` — les deux composantes de `mean_split` k2.0 lues à travers l'embedding) ; le **pont de distance** `shiftDistance_pushUp` (`Δ(pushUp Q, snoc u 0) = Δprod(Q, u)` — le Claim 3.2 de k1.5 s'applique à la dimension agrandie sans perte) ; l'**exactitude du support** dans les deux sens (`pushUp_ne_zero_of_mem` / `pushUp_mem_map_of_ne_zero`) ; `sum_smul_snoc` — **la forme lake du `sum_smul_inl` de l'oracle dont k2.5 annonçait le consommateur mesuré** (`Split.lean` l.50-53, consommé à `SignedSums.lean` l.54 : une somme pondérée de vecteurs embarqués à hauteur nulle reste à hauteur nulle) ; et `toReal_liftUp` (commutation `toReal ∘ liftUp = snoc ∘ (toReal × hauteur)` — le carré avec `toRealProd` k2.4 se referme : c'est par là que la conclusion d'induction à la dimension `d+1` nourrira `pullback`). **Reportés avec consommateur mesuré** : la conservation des moments sous contenance (`prodMoment_split_of_support`) et le transfert de contenance à travers la scission (k2.6b) ; l'induction elle-même, `SignedSums.lean` nom pour nom (k2.6c). **Trois classes d'erreur mesurées aux rounds 1-2** (consignées pour les portages suivants) : `rfl` échoue sur les lemmes de lecture de `Fin.snoc` au pin (version Tuple hétérogène via `dite`+cast, `Tuple/Basic.lean` l.515 — remplacé par `simp [liftUp]` sur `Fin.snoc_castSucc` l.526 / `Fin.snoc_last` l.539) ; `rw` est syntaxique et exige le pont `liftUpEmb_apply` sur les images `Finset.map` ; `cases` sur un terme non-variable (`y.2`) ne substitue pas dans le but — déstructurer la paire d'abord. Module FR + jumeau `_en` (header et docstring de module en français côté FR, convention du lake — advisory HALF-DONE de l'organe i18n levé). 0 `sorry`. | brique k2 (assemblage) | **PROUVÉ** (k2.6a, 10-04, `lake build` local — ciblé deux jumeaux 0 erreur **0 warning** (28 s chacun, SUCCESS au 3ᵉ round : 6 classes d'erreur des rounds 1-2 diagnostiquées contre le source Mathlib du pin) ; full-lib **8754 jobs** *Build completed successfully*, **37 warnings — identique à k2.5**, 0 sur les modules nouveaux ; `distinct_code_sorry = 0` (lake discrepancy) ; jumeaux i18n byte-identical — voir PR) | ce PR (stack sur #19087) | -| **k2.6** | `Discrepancy.Komlos.sum_smul_inl` : **première brique de l'assemblage** — nouveau module `Komlos/SignedSums.lean` (+ jumeau `_en`), repris nom pour nom de l'oracle. Livré : `sum_smul_inl` **générique** (`{E : Type*} [AddCommGroup E] [Module ℝ E]`, `∑ i, ε i • (v i, 0) = (∑ i, ε i • v i, 0)` par `Prod.ext` + `Prod.smul_mk`/`fst_sum`/`snd_sum` — les trois noms **vérifiés au pin** : `smul_mk` en `GroupWithZero/Action/Prod.lean`, `fst_sum`/`snd_sum` versions additives de `fst_prod`/`snd_prod` en `BigOperators/Pi.lean` l.155, toolkit identique à `Convex/Combination.lean` l.460) — l'assistant que l'oracle invoque au pas de l'induction (`SignedSums.lean` l.53 : `rw [mean_split, sum_smul_inl, Prod.mk_add_mk, add_zero] at hmem`) pour distribuer une somme de couples sur la première composante. **Carte de généricité (mesurée, en tête du module)** : l'induction de l'oracle ré-instancie ses organes à chaque niveau sur un ambiant croissant `E → E × ℝ → …` ; les organes k2.0–k2.5 de ce lake sont **monomorphes** (`Fin d → ℤ`, hauteur `Bool`) — split, mean_split_of_support, shiftDist_split_le, splitBit_eq, pullback, mean_mem_convexHull. Déjà génériques dans le lake : `segment_repr`, `add_smul_mem_convexHull`, `sum_smul_mem_convexHull` (Pullback.lean l.150/189/213). `sum_smul_inl` était **absent** — livré générique ici, consommable à tout niveau. **Voie β (ping-pong deux espaces) close par la mesure** : le pas oracle écrit simultanément dans `E` (les `v i`) et `ℝ` (les hauteurs) au même niveau d'itération, pas en alternance. **Décision de cadre arbitrée en k2.6a** (option (c) : l'espace qui grandit est réalisé `Fin (d + k) → ℤ` par `liftUp`, la voie α est écartée — cf ligne k2.6a) ; `sum_smul_inl` se positionne comme l'organe générique ℝ-modulaire **complémentaire de `sum_smul_snoc`** (k2.6a, forme lake côté grille), consommable côté transport/hull. 0 `sorry`. | brique k2 (assemblage, 1/…) | **PROUVÉ** (k2.6 brique 1, 10-06, `lake build` local ciblé deux jumeaux EXIT=0, `distinct_code_sorry = 0`, jumeaux i18n byte-identical — voir PR) | ce PR (stack sur #19089) | +| **k2.6** | `Discrepancy.Komlos.sum_smul_inl` : **première brique de l'assemblage** — nouveau module `Komlos/SignedSums.lean` (+ jumeau `_en`), repris nom pour nom de l'oracle. Livré : `sum_smul_inl` **générique** (`{E : Type*} [AddCommGroup E] [Module ℝ E]`, `∑ i, ε i • (v i, 0) = (∑ i, ε i • v i, 0)` par `Prod.ext` + `Prod.smul_mk`/`fst_sum`/`snd_sum` — les trois noms **vérifiés au pin** : `smul_mk` en `GroupWithZero/Action/Prod.lean`, `fst_sum`/`snd_sum` versions additives de `fst_prod`/`snd_prod` en `BigOperators/Pi.lean` l.155, toolkit identique à `Convex/Combination.lean` l.460) — l'assistant que l'oracle invoque au pas de l'induction (`SignedSums.lean` l.53 : `rw [mean_split, sum_smul_inl, Prod.mk_add_mk, add_zero] at hmem`) pour distribuer une somme de couples sur la première composante. **Carte de généricité (mesurée, en tête du module)** : l'induction de l'oracle ré-instancie ses organes à chaque niveau sur un ambiant croissant `E → E × ℝ → …` ; les organes k2.0–k2.5 de ce lake sont **monomorphes** (`Fin d → ℤ`, hauteur `Bool`) — split, mean_split_of_support, shiftDist_split_le, splitBit_eq, pullback, mean_mem_convexHull. Déjà génériques dans le lake : `segment_repr`, `add_smul_mem_convexHull`, `sum_smul_mem_convexHull` (Pullback.lean l.150/189/213). `sum_smul_inl` était **absent** — livré générique ici, consommable à tout niveau. **Voie β (ping-pong deux espaces) close par la mesure** : le pas oracle écrit simultanément dans `E` (les `v i`) et `ℝ` (les hauteurs) au même niveau d'itération, pas en alternance. **Décision de cadre arbitrée en k2.6a** (option (c) : l'espace qui grandit est réalisé `Fin (d + k) → ℤ` par `liftUp`, la voie α est écartée — cf ligne k2.6a) ; `sum_smul_inl` se positionne comme l'organe générique ℝ-modulaire **complémentaire de `sum_smul_snoc`** (k2.6a, forme lake côté grille), consommable côté transport/hull. 0 `sorry`. | brique k2 (assemblage, 1/…) | **PROUVÉ** (k2.6 brique 1, 10-06, `lake build` local ciblé deux jumeaux EXIT=0, `distinct_code_sorry = 0`, jumeaux i18n byte-identical — voir PR) | #19425 (stack sur #19089) | +| **k2.6b** | `Discrepancy.Komlos.supportContained_pushUp_split` : **la scission sous contention, lue dans la dimension agrandie** — nouveau module `Komlos/LiftSplit.lean` (+ jumeau `_en`), **sans contrepartie oracle** : chez l'oracle le `Finsupp` transporte son support gratuitement (`Finsupp.embDomain`), c'est le cadre `Finset` explicite du lake qui doit payer ce transport — et ce paiement est l'objet de la brique. **Livré** : `pushUp_split_ne_zero` (toute masse de `pushUp (split w P)` vit sur l'image de `liftUp` et provient d'une masse de `P` à distance `± w` — `pushUp_eq_zero` × formes `max`/`min` de `split` par `le_total`/`max_eq_left`/`min_eq_left`) ; `supportContained_pushUp_split` (**le transfert de contenance à travers la scission** : `SupportContained S P A` + stabilité de `A` par `± w` ⟹ la scission-poussée obéit à la contention sur l'image liftée `(S ×ˢ univ).map liftUpEmb`, pour les décalages embarqués `Fin.snoc · 0` de `A` — la précondition de support que le pas de l'induction doit établir pour appliquer l'hypothèse à la dimension `d+1`) ; `coordMoment_pushUp_split_of_support` + `coordMoment_pushUp_split_last` (**la conservation des moments sous contenance, au niveau lifté** : les deux composantes de `mean_split_of_support` k2.0 composées avec les ponts de moment k2.6a — le miroir lake du `rw [mean_split, …] at hmem` de `SignedSums.lean` l.54, composantes spatiale `i.castSucc` et hauteur `Fin.last`) ; `supportContained_pushUp_split_three` (la forme `{0, snoc u 0, −snoc u 0}` exacte que le cran suivant consomme, instance du transfert par `SupportContained.mono` — `snoc 0 0 = 0`, `−snoc u 0 = snoc (−u) 0`). **La stabilité de `A` par `± w` est le prix exact de la scission** : un point de masse `P (x ± w) ≠ 0` déplacé de `a` atterrit en `x + a`, atteint depuis `x ± w` par le décalage `a ∓ w ∈ A`. **Consommateur mesuré** : k2.6c — l'induction elle-même (`SignedSums.lean` l.44-55). 0 `sorry`. | brique k2 (assemblage, 2/…) | **PROUVÉ** (k2.6b, 10-06, `lake build` local ciblé deux jumeaux EXIT=0, `distinct_code_sorry = 0`, jumeaux i18n byte-identical — voir PR) | ce PR (stack sur #19425) | +| **k2.6c** | `Discrepancy.Komlos.exists_isColouring_mean_add_sum_mem_convexHull` : **l'assemblage final — l'induction du Lemme 1.4** (`Komlos/SignedSums.lean` l.37-58, nom pour nom). **Décision d'architecture (mesurée)** : le `Finsupp` de l'oracle porte son support exact gratuitement à chaque niveau ; le cadre `Finset` du lake ne peut pas — la contenance `SupportContained` (k1.7) exige un support **fermé par décalages de `A`**, le `pullback` (k2.4) exige une enveloppe sur le **support exact** (`hSQ`), et ces deux rôles sont incompatibles sur un seul `Finset` (un point de masse déplacé par `a ∈ A` peut atterrir sur masse nulle, hors support exact). **Livré** : `snocReal` + `snocLM` + `snocReal_injective` (l'isomorphisme `snoc` côté réel `(Fin d → ℝ) × ℝ → (Fin (d+1) → ℝ)`, structure linéaire et injectivité) ; `snocReal_toRealProd` (le carré réel `snocReal ∘ toRealProd = toReal ∘ liftUp`) ; `mem_convexHull_map_snocReal` (le transport d'enveloppe à travers `snoc`, par `LinearMap.image_convexHull` — l'organe Mathlib remplace une double décomposition à réindexation de poids) ; **`exists_colouring_aux`** — la porte inductive à **deux ensembles** : `S` (fermeture : masse, moments, contenance) et `E` (support exact : enveloppe de la conclusion, `E ⊆ S`) ; au niveau suivant `S' = (S ×ˢ univ).map liftUpEmb` (contenance par `supportContained_pushUp_split` k2.6b), `E' = SQ.map liftUpEmb` (`SQ` le filtre des scissions non nulles) ; et **`exists_isColouring_mean_add_sum_mem_convexHull`** — l'énoncé public (`E := S.filter (P · ≠ 0)`, remontée par `convexHull_mono` + `Finset.map_subset_map`). **La chaîne du pas** (mirror l.44-58) : scission en `w = 3 • v_last` ; `hmass'` par `pushUp_mass` + `split_mass_of_support` ; `hC'` par k2.6b ; `hv'` par `shiftDistance_pushUp` (k2.6a) + Claim 3.2 (k1.7, contention à six décalages atteinte en 1-3 crans de `hAstab`) ; point IH lu comme `snocReal (z, β)` (moments par `coordMoment_pushUp_split_of_support`/`_last`) ; transport par le carré + `mem_convexHull_map_snocReal` ; `hβ : 3⁻¹ ≤ splitBit` par `splitBit_eq_of_support` + `linarith` ; clôture `pullback` (k2.4, implicites nommés `v := w`, `w := v_last`) ; coloration `Fin.snoc ε' ē`. **Le k2 est clos** (l'assemblage l.37-58 est le lemme entier). 0 `sorry`. | brique k2 (assemblage, 3/3 — **clôture du k2**) | **PROUVÉ** (k2.6c, 10-06, `lake build` local ciblé deux jumeaux EXIT=0, `distinct_code_sorry = 0`, jumeaux i18n byte-identical — voir PR) | ce PR (stack sur #19445) | | **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`) | | **k3.2** | `Discrepancy.Komlos.gridF` (`Komlos/Grid.lean` + jumeau `_en`) : **le poids normalisé unidimensionnel et sa borne `L²` de translation — port complet du `Komlos/Grid.lean` de l'oracle** (la voie k3 de l'oracle est désormais complète). Briques closes : `gridM` (demi-largeur `6·N`), `gridZ` (constante de normalisation = `∑ tent²`), `gridF` (`tent (gridM N) j / √(gridZ N)`), `cast_gridM`, `gridZ_eq` (**`gridZ N = 144·N³ + 2·N`**), `gridZ_pos`, `gridF_nonneg`, `support_gridF_subset`, `finsum_gridF_sq` (**masse totale `1`**), `sum_gridF_sub_sq`/`sum_gridF_sq` (formes `Finset` consommables), **résultat porteur `sum_gridF_sub_sq_le`** : distance `L²` au carré entre `gridF N` et son translaté par `m` ≤ `m²/(12·N²)` — l'analogue discret du Lemme 4.1, entrée directe de la discrétisation k4 (Lemme 1.5). Adaptations mesurées : le `positivity` de l'oracle sur `gridZ_pos` échoue au pin (stricte positivité dépend de `hN : 0 < N`) → cast + `linarith` ; le `linarith` final de `gridZ_eq` échoue sur le produit non-linéaire → normalisation `ring` explicite avant `linarith` ; `support_tent_subset` de ce lake étant typé `Set.Icc` (l'oracle : `Finset.Icc`), `support_gridF_subset` est prouvé directement (`Finset.mem_coe` + composite `le_abs_self`) ; l'API `finsum` (**existe au pin**, à la racine — sondée) permet le port quasi verbatim des énoncés de masse. **Correctif i18n embarqué** : `Tent_en.lean` passait en `namespace Discrepancy.Komlos` (seul `_en` du lake non suffixé — défaut #17918) ; il repasse en `Discrepancy.Komlos_en`, condition de l'import propre `Grid_en → Tent_en`. 0 `sorry`. | brique k3 (poids normalisé + L²) | **PROUVÉ** (k3.2, 10-06, `lake build` local EXIT=0 sur les trois cibles — 8710 jobs : `Grid`, `Grid_en`, `Tent_en` recompilé ; `distinct_code_sorry = 0`, jumeaux i18n `2/2 byte-identical` — voir PR) | ce PR (stack sur #19563) | | 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). | — | @@ -167,7 +169,7 @@ branche, jamais `main`. Issue de suivi : #17845. | **k1.7** | Correctif d'hypothèse **avant** k2 : l'invariance du support des briques k1 est insatisfiable aux décalages non nuls (mesuré, `eq_zero_of_image_add_eq_self`) → formes consommables sous **contention** `SupportContained` | fini | k1 | | **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`). **Livré en k2.2** : la **machinerie de convexité** — `convexHull` passe de 0 à sa première occurrence ; `add_smul_mem_convexHull` (verbatim) + `sum_smul_mem_convexHull` (l'étape de clôture `Convex.sum_mem`). **Livré en k2.3** : le **transport de dimension** (`Komlos/Transport.lean` : `toReal` + `push` + `push_mass` + les deux ponts que la conclusion lit sur le support transporté — barycentre `coordMoment_toReal`, appartenance `toReal_mem_map_iff` ; `shiftDist_push` et `tvDist_push` reportés avec raison mesurée, cf ligne k2.3) qui, dans une base concrète `Fin d → ℤ`, remplace la généralité de `E` — **le bloqueur mesuré en k2.2 est levé** (Fin d → ℤ n’est pas un ℝ-module ; l’oracle énonce pullback sur E →₀ ℝ — le transport plonge la grille dans Fin d → ℝ où convexHull ℝ parle). **Livré en k2.4** : **le pas complet** (`pullback`, `Komlos/Pullback.lean` l.55-92 — `toRealProd` + les caractérisations de support + le théorème `pullback` lui-même, porté sur `Finset.mem_convexHull'` du pin ; trois écarts de cadre arbitrés, cf ligne k2.4). **Livré en k2.5** : **le cas de base** (`mean_mem_convexHull`, `Komlos/Distribution.lean` l.105, module repris nom pour nom — nouveau `Distribution.lean` + jumeau `_en` ; le one-liner oracle tient tel quel sur l'organe `push` de k2.3, les trois composantes lisant `push_apply`/`push_mass`/`coordMoment_toReal`, cf ligne k2.5). **Livré en k2.6a** : **le pont de niveau** (`Lift.lean` + jumeau `_en`, sans contrepartie oracle — l'espace qui grandit est réalisé `Fin (d + k) → ℤ` par l'embedding `liftUp`, design-gate arbitré option (c) consigné dans le header du module ; `pushUp` sur le pattern `Function.extend` de k2.3, les ponts de moment / de distance / de support, et `sum_smul_snoc` — **la forme lake du `sum_smul_inl` dont k2.5 annonçait le consommateur mesuré**, désormais livrée, cf ligne k2.6a). **Livré en k2.6 (brique 1)** : `sum_smul_inl` **générique** (module `Komlos/SignedSums.lean` + jumeau `_en`, repris nom pour nom — la carte de généricité des organes y est mesurée, la voie β close par la mesure, la décision de cadre consignée ouverte). **Reste à ce lake, mesuré** : **k2.6b** (la conservation des moments sous contenance `prodMoment_split_of_support` + le transfert de contenance à travers la scission) puis **k2.6c** — la lecture k1.7 du pas elle-même (`SignedSums.lean` l.37-58 nom pour nom : l'itération `induction n generalizing d` qui consomme `mean_mem_convexHull` en base (l.42), `mean_split` + `sum_smul_snoc` au pas (l.53-54) et `pullback` en clôture). | fini + induction | k1, k1.7, k2.0–k2.6 | +| **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`). **Livré en k2.2** : la **machinerie de convexité** — `convexHull` passe de 0 à sa première occurrence ; `add_smul_mem_convexHull` (verbatim) + `sum_smul_mem_convexHull` (l'étape de clôture `Convex.sum_mem`). **Livré en k2.3** : le **transport de dimension** (`Komlos/Transport.lean` : `toReal` + `push` + `push_mass` + les deux ponts que la conclusion lit sur le support transporté — barycentre `coordMoment_toReal`, appartenance `toReal_mem_map_iff` ; `shiftDist_push` et `tvDist_push` reportés avec raison mesurée, cf ligne k2.3) qui, dans une base concrète `Fin d → ℤ`, remplace la généralité de `E` — **le bloqueur mesuré en k2.2 est levé** (Fin d → ℤ n’est pas un ℝ-module ; l’oracle énonce pullback sur E →₀ ℝ — le transport plonge la grille dans Fin d → ℝ où convexHull ℝ parle). **Livré en k2.4** : **le pas complet** (`pullback`, `Komlos/Pullback.lean` l.55-92 — `toRealProd` + les caractérisations de support + le théorème `pullback` lui-même, porté sur `Finset.mem_convexHull'` du pin ; trois écarts de cadre arbitrés, cf ligne k2.4). **Livré en k2.5** : **le cas de base** (`mean_mem_convexHull`, `Komlos/Distribution.lean` l.105, module repris nom pour nom — nouveau `Distribution.lean` + jumeau `_en` ; le one-liner oracle tient tel quel sur l'organe `push` de k2.3, les trois composantes lisant `push_apply`/`push_mass`/`coordMoment_toReal`, cf ligne k2.5). **Livré en k2.6a** : **le pont de niveau** (`Lift.lean` + jumeau `_en`, sans contrepartie oracle — l'espace qui grandit est réalisé `Fin (d + k) → ℤ` par l'embedding `liftUp`, design-gate arbitré option (c) consigné dans le header du module ; `pushUp` sur le pattern `Function.extend` de k2.3, les ponts de moment / de distance / de support, et `sum_smul_snoc` — **la forme lake du `sum_smul_inl` dont k2.5 annonçait le consommateur mesuré**, désormais livrée, cf ligne k2.6a). **Livré en k2.6 (brique 1)** : `sum_smul_inl` **générique** (module `Komlos/SignedSums.lean` + jumeau `_en`, repris nom pour nom — la carte de généricité des organes y est mesurée, la voie β close par la mesure, la décision de cadre arbitrée en k2.6a). **Livré en k2.6b** : la scission sous contention dans la dimension agrandie (module `Komlos/LiftSplit.lean` + jumeau `_en` — le **transfert de contenance** `supportContained_pushUp_split` + la **conservation des moments liftée** `coordMoment_pushUp_split_of_support`/`_last` : la précondition de support et les ré-écritures de barycentre que le pas exige pour appliquer l'hypothèse d'induction à `pushUp (split w P)` dans `Fin (d+1) → ℤ`, cf ligne k2.6b). **Livré en k2.6c** : **l'assemblage final lui-même** (`SignedSums.lean` l.37-58 nom pour nom — l'itération `induction n` qui consomme `mean_mem_convexHull` en base (l.42), la scission de niveau et les moments k2.6b au pas, `pullback` en clôture (l.55) : la porte inductive à deux ensembles `S`/`E`, le carré réel `snocReal` et le transport d'enveloppe `mem_convexHull_map_snocReal`, cf ligne k2.6c). **Le k2 est clos** — les sept crans k2.0 → k2.6c sont livrés. | fini + induction | k1, k1.7, k2.0–k2.6c | | **k3** | Lemme 4.1 — densité-tente. **Réauditée contre l'oracle au pin (k3.1)** : la voie Dahia est **totalement discrète** — 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` est sans objet. **LIVRÉE EN INTÉGRALITÉ** : k3.1 (`Tent.lean` complet, lignes k3.1/k3.2) puis k3.2 (`Grid.lean` complet — `gridF` normalisé, `gridZ_eq : gridZ N = 144·N³ + 2·N`, masse `1`, **`sum_gridF_sub_sq_le` : distance `L²` de translation ≤ m²/(12·N²)**, l'analogue discret du Lemme 4.1). **Reste** : k4 (Lemme 1.5, discrétisation). | fini (oracle discret, complet) | k3.1, k3.2 | | **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`/`Search-09e` (ligne « course aux bornes » du 22/09/2026) | assemblage | k2, k4 |