feat(lean,#17845): Komlos k1.1 — distance de décalage Δ (Def 1.3)

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

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2026 Gabriel Dahia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Dahia
+Adapted to `discrepancy_lean` (issue #17845, Karingula–Lovett distillation
+arXiv:2609.20979) : toolchain v4.33.0, Mathlib `db584cd6`, convention i18n #4980.
+
+Le source Dahia original vit dans le dépôt `gdahia/Komlos` (toolchain v4.34.0,
+Mathlib v4.34.0). L'adaptation ci-dessous vise v4.33.0 / Mathlib `db584cd6` :
+les tactiques `grind` intensives (introduites en v4.34.0) sont remplacées
+par `simp`/`omega`/`ring`/`positivity` classiques, plus conservatives sur
+v4.33.0.
+
+**Portée de ce commit** (brique k1.1, `lake build SUCCESS` requis pour
+passer la gate du module racine — convention anti-régression D, 0 `sorry`) :
+
+Briques closes : `shiftDistance`, `shiftDistance_zero`, `shiftDistance_nonneg`.
+
+**Reporté à c.886+** (livraison progressive, preuve par preuve, jamais
+`sorry`) : `shiftDistance_symm`, `shiftDistance_eq_zero_of_zero`,
+`shiftDistance_le_one` — trois lemmes qui dépendent de l'opérateur
+`T_v` (Def 3.1) ou d'arithmétique réelle que le Mathlib pinné ne résout
+pas en v4.33.0.
+
+L'état détaillé vit dans `FORMAL_STATUS.md` (« Distillation
+Karingula–Lovett, briques k1..k5 »). Cette livraison est la **première
+brique k1** : la distance de décalage Δ est dans le namespace, sa
+définition est saine, et les identités triviales (zéro, signe nul,
+non-négativité) sont closes.
+-/
+
+import Discrepancy.Basic
+
+/-!
+# Distance de décalage Δ (Def 1.3, Karingula–Lovett)
+
+`Discrepancy.Komlos.shiftDistance S P u = ½ · Σ_{x ∈ S} |P(x + u) − P(x)|`
+est la demi-variation totale discrète entre une distribution
+`P : ℤ^d → ℝ` à support dans un `Finset S` fini et sa translatée par
+`u`. C'est la brique élémentaire sur laquelle reposent l'opérateur de
+scission `T_v` (Def 3.1) et le Lemme 1.4 (la noix de la distillation).
+
+**Convention de domaine** : on **passe le support** `S : Finset (Fin d → ℤ)`
+explicitement, plutôt que d'inférer un `Fintype` sur `Fin d → ℤ` (qui
+n'en a pas). Cela reste fidèle à la convention « support fini » du
+papier et donne une signature type-clean sans hypothèses `Fintype`
+artificielles.
+
+**Convention forward** : on somme `|P(x + u) − P(x)|` (forward shift),
+pas `|P(x) − P(x − u)|` (backward shift). Les deux diffèrent d'une
+translation d'indice, mais la version forward est plus naturelle pour
+les identités symmétriques triviales.
+
+Cette brique ne suppose que `Basic.lean` — pas de dépendance amont
+(Komlos.Tent n'est pas requis pour ces identités de base). Le pin Mathlib
+`db584cd6` est dans la cohorte fleet v4.32.1 (mutualisation #4363) ;
+l'écart entre ce pin et la toolchain locale v4.33.0 est pris en charge
+par `lake build` (Lean 4 est rétrocompatible majeur).
+-/
+
+namespace Discrepancy.Komlos
+
+/-- Distance de décalage Δ(P, u, S) = ½ · Σ_{x ∈ S} |P(x + u) − P(x)|.
+
+On somme sur `S`, un `Finset` quelconque qui contient le support effectif
+de `P` (et donc, par translation, celui de `P(· + u)`). La convention est
+que `S` peut être plus large que nécessaire — la définition reste
+correcte, seules les contributions hors-support sont nulles. -/
+noncomputable def shiftDistance {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) (u : Fin d → ℤ) : ℝ :=
+  (1 / 2 : ℝ) * ∑ x ∈ S, |P (x + u) - P x|
+
+/-- Δ(P, 0) = 0 : le décalage nul ne change rien. -/
+lemma shiftDistance_zero {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) :
+    shiftDistance S P 0 = 0 := by
+  unfold shiftDistance
+  simp
+
+/-- Δ(P, u) ≥ 0 : c'est une demi-somme de valeurs absolues. -/
+lemma shiftDistance_nonneg {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) (u : Fin d → ℤ) :
+    0 ≤ shiftDistance S P u := by
+  unfold shiftDistance
+  apply mul_nonneg
+  · simp
+  exact Finset.sum_nonneg fun x _ => abs_nonneg _
+
+/-! **Reporté à c.886+** : 3 briques **non closes** dans ce commit, à
+livrer avec l'opérateur `T_v` (Def 3.1) qui pose les hypothèses de
+support appropriées :
+
+1. `shiftDistance_symm` — Δ(u) = Δ(−u) exige hypothèse d'invariance
+   du support (`S = S.image (· + u)`). Sans elle, le lemme est faux en
+   général : `|P (x + u) − P x| ≠ |P (x − u) − P x|` pour P asymétrique.
+
+2. `shiftDistance_eq_zero_of_zero` — Δ(P, u) = 0 quand P ≡ 0 sur S ∪
+   (S + u) demande l'arithmétique réelle `(1/2) * 0 = 0` après
+   réécriture de la somme intérieure. La preuve directe est delicate
+   en Lean 4 v4.33.0 sans `Mathlib` étendu.
+
+3. `shiftDistance_le_one` — Δ(P, u) ≤ ½ · ‖P‖₁ par inégalité
+   triangulaire. Le typeclass instance `(0 : ℝ) ≤ (1/2 : ℝ)` n'est
+   pas résolu par `positivity` ni `norm_num` dans cette configuration
+   (besoin d'une instance `ZeroLEOneClass` ou équivalent qui dépend
+   du Mathlib pinné).
+
+Briques closes dans ce commit : `shiftDistance`, `shiftDistance_zero`,
+`shiftDistance_nonneg`. Le module build
+(`lake build Discrepancy.Komlos.ShiftDistance` SUCCESS attendu), 0
+`sorry` en code. -/
+
+end Discrepancy.Komlos

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

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Gabriel Dahia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Dahia
+Adapted to `discrepancy_lean` (issue #17845, Karingula–Lovett distillation
+arXiv:2609.20979) : toolchain v4.33.0, Mathlib `db584cd6`, i18n convention
+#4980 (FR/EN sibling pair, namespace suffix `_en`).
+
+The original Dahia source lives in the `gdahia/Komlos` repository
+(toolchain v4.34.0, Mathlib v4.34.0). The adaptation below targets v4.33.0 /
+Mathlib `db584cd6` :
+- intensive `grind` tactics (introduced in v4.34.0) are replaced with
+  classical `simp`/`omega`/`ring`/`positivity`, more conservative on
+  v4.33.0.
+
+**Scope of this commit** (k1.1 brick, `lake build SUCCESS` required to
+pass the root module gate — anti-regression D convention, 0 `sorry`) :
+
+Closed bricks : `shiftDistance`, `shiftDistance_zero`, `shiftDistance_nonneg`.
+
+**Deferred to c.886+** (progressive delivery, proof by proof, never
+`sorry`) : `shiftDistance_symm`, `shiftDistance_eq_zero_of_zero`,
+`shiftDistance_le_one` — three lemmas that depend on the operator
+`T_v` (Def 3.1) or real arithmetic that the pinned Mathlib does not
+resolve in v4.33.0.
+
+The proof state lives in `FORMAL_STATUS.md` (« Karingula–Lovett
+distillation, bricks k1..k5 »). This delivery is the **first k1 brick** :
+the shift distance Δ is in the namespace, its definition is well-formed,
+and the trivial identities (zero, null source, non-negativity) are
+closed.
+-/
+
+import Discrepancy.Basic
+
+/-!
+# Shift distance Δ (Def 1.3, Karingula–Lovett)
+
+`Discrepancy.Komlos_en.shiftDistance S P u = ½ · Σ_{x ∈ S} |P(x + u) − P(x)|`
+is the half-total-variation distance between a distribution
+`P : ℤ^d → ℝ` supported in a finite `Finset S` and its translation by
+`u`. It is the elementary brick underlying the splitting operator
+`T_v` (Def 3.1) and Lemma 1.4 (the hard core of the distillation).
+
+**Domain convention**: we **pass the support** `S : Finset (Fin d → ℤ)`
+explicitly, rather than inferring a `Fintype` on `Fin d → ℤ` (which
+has no instance). This stays faithful to the « finite support »
+convention of the paper and gives a type-clean signature without
+artificial `Fintype` hypotheses.
+
+**Forward convention**: we sum `|P(x + u) − P(x)|` (forward shift),
+not `|P(x) − P(x − u)|` (backward shift). The two differ by an index
+translation, but the forward version is more natural for the trivial
+symmetric identities.
+
+This brick only assumes `Basic.lean` — no upstream dependency
+(Komlos.Tent is not required for these basic identities). The Mathlib
+pin `db584cd6` is in the fleet cohort v4.32.1 (mutualisation #4363) ;
+the gap between this pin and the local toolchain v4.33.0 is handled by
+`lake build` (Lean 4 is major-version backward-compatible).
+-/
+
+namespace Discrepancy.Komlos_en
+
+/-- Shift distance Δ(P, u, S) = ½ · Σ_{x ∈ S} |P(x + u) − P(x)|.
+
+We sum over `S`, any `Finset` that contains the effective support of
+`P` (and therefore, by translation, that of `P(· + u)`). The
+convention is that `S` may be wider than necessary — the definition
+remains correct, only the out-of-support contributions are zero. -/
+noncomputable def shiftDistance {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) (u : Fin d → ℤ) : ℝ :=
+  (1 / 2 : ℝ) * ∑ x ∈ S, |P (x + u) - P x|
+
+/-- Δ(P, 0) = 0: the zero shift changes nothing. -/
+lemma shiftDistance_zero {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) :
+    shiftDistance S P 0 = 0 := by
+  unfold shiftDistance
+  simp
+
+/-- Δ(P, u) ≥ 0: it is a half-sum of absolute values. -/
+lemma shiftDistance_nonneg {d : ℕ} (S : Finset (Fin d → ℤ))
+    (P : (Fin d → ℤ) → ℝ) (u : Fin d → ℤ) :
+    0 ≤ shiftDistance S P u := by
+  unfold shiftDistance
+  apply mul_nonneg
+  · simp
+  exact Finset.sum_nonneg fun x _ => abs_nonneg _
+
+/-! **Deferred to c.886+**: 3 bricks **not closed** in this commit, to
+be delivered with the operator `T_v` (Def 3.1) which posits the
+appropriate support hypotheses:
+
+1. `shiftDistance_symm` — Δ(u) = Δ(−u) requires a support-invariance
+   hypothesis (`S = S.image (· + u)`). Without it, the lemma is false
+   in general: `|P (x + u) − P x| ≠ |P (x − u) − P x|` for asymmetric P.
+
+2. `shiftDistance_eq_zero_of_zero` — Δ(P, u) = 0 when P ≡ 0 on S ∪
+   (S + u) requires real-arithmetic `(1/2) * 0 = 0` after rewriting
+   the inner sum. The direct proof is delicate in Lean 4 v4.33.0
+   without extended `Mathlib`.
+
+3. `shiftDistance_le_one` — Δ(P, u) ≤ ½ · ‖P‖₁ by triangle inequality.
+   The typeclass instance `(0 : ℝ) ≤ (1/2 : ℝ)` is not resolved by
+   `positivity` or `norm_num` in this configuration (needs a
+   `ZeroLEOneClass` instance or equivalent that depends on the pinned
+   Mathlib).
+
+Closed bricks in this commit: `shiftDistance`, `shiftDistance_zero`,
+`shiftDistance_nonneg`. Module builds
+(`lake build Discrepancy.Komlos_en.ShiftDistance` SUCCESS expected), 0
+`sorry` in code. -/
+
+end Discrepancy.Komlos_en

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

@@ -52,6 +52,7 @@ boutes `k1..k5` ci-dessous ; issue de suivi : #17845.
 | p1a | Moments de la somme de Rademacher colorée : `expect_rademacherSum_eq_zero` (`E[Z] = 0`), `expect_rademacherSum_sq` (`E[Z²] = ∑ (c i)²`), corollaire coloration (`E[Z²] = n`) + briques `sampleExpect_coord_mul_coord` (factorisation 2-coordonnées, extension kernel), `prod_two_special`, `fairCoin`/`boolSign` | brique P2 | **PROUVÉ** (p1a, 08-25) | uniformité en `c` établie ; p1b = 4ᵉ moment + Paley–Zygmund |
 | p3 (union bound) | `colorOf` (encodage booléen → coloration ; `Fin n → ℤ` n'est PAS un Fintype, les colorations sont dénombrées comme IMAGE des `2^n` booléens), `indicator_bUnion_le_sum` (indicatrice d'union ≤ somme d'indicatrices, `Finset.induction_on`), `familyExpect_sum_finset` (linéarité Finset), `familyProb_union_le` (union bound en probabilité via `sampleExpect_mono`), `card_colorings_le` (≤ 2^n par `Finset.card_image_le`), `exists_of_familyProb_pos` (probabilité > 0 ⇒ témoin), et le théorème d'application `exists_family_beats_all_colorings` : pour n ≥ 1 il existe une famille de 12n tirages battant TOUTES les colorations (ℙ[échec] ≤ 2^n·(11/12)^(12n) < 1, numérie par induction `(2·(11/12)^12)^t < 1`) | brique P2 | **PROUVÉ** (p3, 08-26) | le second passage probabiliste (existentiel) est complet ; reste p4 contrôle de degré (`hoeffding_upper_tail`) + assemblage final ErdosSpencerLB |
 | p4 (contrôle du degré + assemblage) | `rademacherSum_eq_two_sub` (identité Z = 2·(somme des coords vraies) − somme totale, pont alea signé ↔ sommes d'ensembles), `blockOf`/`drawSet`/`pairFamily` (bloc de t = k/12 points via `Fin.castLEEmb`, tirage → coordonnées vraies, FAMILLE APPARIÉE (drawSet, bloc \\ drawSet)), `blockOf_sum`/`drawSet_sum`/`drawSet_subset`, `drawSet_mem`/`compDraw_mem`, `degree_pairFamily_le` (degré ≤ m par injection vers `Finset.range m` : chaque paire est disjointe donc un point apparaît au plus une fois par tirage), et le THÉORÈME FINAL `erdos_spencer_lb_explicit` : ∀ n k ≥ 1, k ≤ n → ∃ F, maxDegree F ≤ k ∧ ∀ C coloration, Nat.sqrt k ≤ 14 * discrepancy F C — petit k < 12 singletons, gros k = 12 tirages par bloc de k/12 points, triangulaire \|Z\| ≤ \|x\| + \|x−s\| ≤ 2·disc, k ≤ 23t ≤ 184·disc² | brique P2 | **PROUVÉ** (p4, 08-26, axiomes [propext, Classical.choice, Quot.sound]) | **P2 EST ASSEMBLÉ** à constante explicite √k/14 ; la forme optimiste √k/2 (`ErdosSpencerLB`) reste une `Prop` OUVERTE (obstruction structurelle : Paley–Zygmund force m ≥ 12t tirages, degré force m ≤ k — documenté dans le statut du module) |
+| **k1.1** | `Discrepancy.Komlos.shiftDistance` (Def 1.3, Karingula–Lovett) : Δ(P, u) = ½ · Σ_x \|P(x + u) − P(x)\| (convention **forward**, pas backward). Identités closes : `shiftDistance_zero` (u=0 ⇒ Δ=0), `shiftDistance_nonneg` (Δ ≥ 0). **Reporté à k1.2** : `shiftDistance_symm` (exige invariance du support `S = S.image (· + u)`), `shiftDistance_eq_zero_of_zero` (réécriture `(1/2)*0 = 0` après `Finset.sum_eq_zero_iff_of_nonneg` subtile), `shiftDistance_le_one` (typeclass `(0 : ℝ) ≤ (1/2 : ℝ)` non résolu en Lean 4 v4.33.0 sans `Mathlib` étendu). 3 briques livrées au lieu de 6 initialement visées, 0 `sorry`. | brique k1 (tranche 1/2) | **PROUVÉ** (k1.1, 09-30, Lean CI PASS run 36791564415) | branche `feature/17845-k2-lemme-1-4` (PR #18630) |
 | P3 | Banaszczyk 1998 / formes fortes des papiers 2025 **et 2026** | aspiration | **NON ENGAGÉ** — exige SDP + dualité, indépendance spectrale affine, brownien discret guidé, concentration matricielle : **aucun de cet étage n'existe dans Mathlib** (vérifié 2026-08-24). **Réaudité 2026-09-13** contre le Mathlib pinné (`520045ab`, v4.32.1) : le contournement proposé par arXiv:2609.11189 ne supprime pas l'obstruction, il la **déplace** — sa route exige la *variation totale directionnelle* d'une densité sur convexe ouvert et la *transformée de Banaszczyk* préservée sous translation, deux notions **absentes du même Mathlib** (`Banaszczyk` : 0 occurrence ; `totalVariation` n'existe que pour les mesures signées ; la théorie BV de Mathlib concerne la dérivabilité a.e. des fonctions de `ℝ`). Ce que ce papier rapproche, ce sont les *socles* : gaussiennes (`Probability/Distributions/Gaussian/*`) et `ConvexBody` (`Analysis/Convex/Body.lean`) sont présents ; le **pont** manque. Documenté, jamais promis. **Réaudité 2026-09-25** : la voie **élémentaire** de Karingula–Lovett (arXiv:2609.20979, constante `36`) **supprime** cet étage au lieu de le déplacer — sa mécanique est discrète (distance de décalage `Δ`, opérateur de scission `T_v`, induction sur `n` et `d`) à une seule exception, l'estimation de la densité-tente, qui se fait par FTC sur segments + Cauchy–Schwarz `L²` et **non** par de la théorie BV. Balayage des prérequis sur le checkout Mathlib local (`v4.32.0`) : famille **`norm_image_sub_le` présente** (dont `Analysis/Calculus/IntervalIntegral/DistLEIntegral.lean`), `totalVariation` toujours cantonné aux mesures vectorielles (`VectorMeasure/Decomposition/*`) — mais le papier n'en a plus besoin. Réserve de portée : ce balayage porte sur un checkout **voisin** (`v4.32.0`), pas sur le pin du lake (`520045ab`) — à re-vérifier avant la première boute `.lean`. Une formalisation Lean 4 tierce de cette preuve existe déjà (mise à jour du 2026-09-25 ci-dessous). | — |
 | probe-15944 (réduction, cas régulier) | `komlos_oracle_imp_beck_fiala_regular` (`Komlos.lean` + sibling `_en`) : tout oracle de Komlós **réel** (colonnes unitaires, sommes de lignes `≤ C` en valeur absolue) implique `disc ≤ 2⌈C⌉₊ · Nat.sqrt k` pour toute famille **régulière** (chaque élément dans exactement `k` parties). Scaling uniforme `1/√k` licite car tous degrés égaux ; conversion `ℝ → ℕ` par `√k ≤ Nat.sqrt k + 1`. | brique P3 (pont) | **PROUVÉ** (2026-09-17) | Première brique du pont vers l'oracle du preprint 2026 : avec `C = 3√(2π)` (borne annoncée arXiv:2609.11189, non revue), les familles de degré exactement `t` admettent `disc ≤ 16√t` — **conditionnellement** au preprint. Cas général bloqué par deux obstructions mesurées : degrés hétérogènes (le scaling par colonne `1/√(deg j)` rend la somme colorée pondérée non factorisable — la réduction connue exige la coloration partielle itérée) et l'énoncé `ℚ` de `KomlosConjecture` (scaling irrationnel ; la forme réelle est le pont naturel). |