feat(lean,#17845): tranche k3.2 — Komlos/Grid.lean, poids normalisé gridF + borne L² (0 sorry)

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/lean #19563

Tranche k3.2 du lake discrepancy_lean : Komlos/Grid.lean — le poids normalisé gridF et sa borne L² (stack sur #19563)

See #17845 (EPIC distillation Karingula–Lovett). Avec k3.1 (Tent.lean, #19563), la voie k3 de l'oracle est complète : le poids normalisé unidimensionnel et sa borne L² de translation — l'analogue discret du Lemme 4.1, entrée directe de la discrétisation k4 (Lemme 1.5).

Ce que la tranche livre

Port complet du Komlos/Grid.lean de l'oracle (12 briques) : gridM (demi-largeur 6·N), gridZ (constante de normalisation), 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), et le résultat porteur sum_gridF_sub_sq_le : distance L² au carré entre gridF N et son translaté par m ≤ m²/(12·N²).

Adaptations v4.34 → pin (détail en note de fin de fichier)

• Syntaxe de modules v4.34 (module / public import / @[expose]) retirée.
• gridZ_pos : le positivity de l'oracle échoue au pin — la stricte positivité de 144·N³ + 2·N dépend de hN : 0 < N, invisible pour positivity (sondé) → cast explicite + pow_nonneg + linarith.
• gridZ_eq : le linarith final de l'oracle échoue sur le produit non-linéaire 6·N·(2·(6·N)²+1) → normalisation explicite have e : … := by ring avant linarith.
• support_gridF_subset : le support_tent_subset de ce lake est typé Set.Icc (l'oracle : Finset.Icc) — preuve directe by_contra + Finset.mem_coe/mem_Icc, composite le_abs_self + abs_neg pour chaque borne (omega ne splitte pas |j| sur ℤ).
• L'API finsum existe au pin (finsum_eq_sum_of_support_subset, finsum_comp_equiv, à la racine — sondé par lake env lean) : les énoncés de masse sont portés quasi verbatim.
• Correctif i18n embarqué : Tent_en.lean passait en namespace Discrepancy.Komlos (seul jumeau _en du lake non suffixé — défaut hérité de feat(discrepancy,#17845): port Komlos.Tent from Dahia (buildable core) #17918, mesuré : les 9 autres _en sont en Discrepancy.Komlos_en) ; il repasse en Discrepancy.Komlos_en, condition de l'import propre Grid_en → Tent_en. Corps de preuve inchangé (byte-identique), recompilé vert.

Preuves de validation

1. sorry réel avant/après : python scripts/lean/count_code_sorry.py --json → lake discrepancy : distinct_code_sorry 0 → 0 (tranche additive).
2. lake build SUCCESS local (WSL, pin v4.33.0 / db584cd6, oleans Mathlib pré-construits) :

✔ [8708/8710] Built Discrepancy.Komlos.Grid (28s)
✔ [8709/8710] Built Discrepancy.Komlos.Tent_en (28s)
✔ [8710/8710] Built Discrepancy.Komlos.Grid_en (3.8s)
Build completed successfully (8710 jobs).

3. Proof integrity (B.3) : non applicable — job lean-axiom non câblé sur ce lake (aucune clé axiom-target-modules pour discrepancy dans scripts/lean/ci_lakes.json, cas (a) du §B.3).
4. Jumeaux i18n (i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) : python scripts/lean/check_i18n_siblings.py <4 fichiers> → 2/2 pairs byte-identical | 0 drift | 0 orphan (rc=0) — la paire Tent re-vérifiée après le correctif de namespace.
5. FORMAL_STATUS.md : ligne k3.2 + ligne de planification k3 passée à « LIVRÉE EN INTÉGRALITÉ ».

Scope du diff

• Discrepancy/Komlos/Grid.lean (FR) + Discrepancy/Komlos/Grid_en.lean (EN) : nouveaux, miroirs.
• Discrepancy/Komlos/Tent_en.lean : correctif de namespace uniquement (2 lignes), corps byte-identique.
• FORMAL_STATUS.md : ligne k3.2 + planification k3.

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19569 (feat(lean,#17845): tranche k3.2 — Komlos/Grid.lean, poids normalisé gridF + borne L² (0 sorry)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• fort -- feat(lean,#17845): brique k2.2 — surface de convexité (add_smul_mem_convexHull + sum_smul) #19078 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.3 -- transport de dimension (toReal + push + ponts barycentre/appartenance) #19081 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback) #19084 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.5 — cas de base mean_mem_convexHull (Distribution + jumeau _en) #19087 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1)) #19089 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.6 — sum_smul_inl générique (assemblage SignedSums + jumeau _en) #19425 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.6b -- la scission sous contention dans la dimension agrandie (LiftSplit + jumeau _en) #19445 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• fort -- feat(lean,#17845): brique k2.6c -- l'assemblage final (Lemme 1.4, SignedSums + jumeau _en) #19464 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)
• terminal -- feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) #19563 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Tent_en.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md, recouvrement de chemins 50% -- feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) #19563 est deja sur main. (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845) (issues communes : [Veille→Distillation] arXiv 2609.20979 (Karingula-Lovett) — preuve ELEMENTAIRE de Komlos, constante 36 : supprime l'obstruction P3 mesuree de #15944 (variation totale directionnelle) et une formalisation Lean 4 tierce existe deja (Dahia) #17845)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

Rejeu sur origin/main — nouvelle tête dff66a4d82 (force-push avec bail explicite : ad9f44d12d → dff66a4d82, branche à lane unique).

Cause mesurée. La branche portait le commit k3 (Tent) absorbé depuis par main via #19563 (Tent.lean byte-identique branche/main, vérifié git rev-parse) + la brique k3.2 (Grid). Le commit absorbé la rendait CONFLICTING contre main.

Geste. git rebase --onto origin/main 39aa4360e8 : rejoue uniquement la brique k3.2 (Grid) sur main ; le commit Tent absorbé tombe de la pile (contenu déjà sur main). Rejeu sans conflit (1/1).

Preuve de préservation. Grid.lean, Grid_en.lean, Tent_en.lean byte-identiques avant/après (blobs git rev-parse identiques) — la CI passée sur l'ancienne tête reste la preuve de build. Périmètre vs main inchangé : 4 fichiers (paire Grid + Tent_en.lean + FORMAL_STATUS.md).

See #17845

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 19569
head: dff66a4
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 36b98068fe374ff9493ad0b5e2f0c6502ac244d8189832cbe8ae6dd2283e5dd5
diff-files: 4
diff-additions: 330
diff-deletions: 3
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19569
organ-rc: 0
[/ADJOINT PREFLIGHT]

Dossier tiers emis par myia-po-2027:CoursIA, lane qui ne porte pas cette PR (porteuse : myia-po-2025:CoursIA). Lecture des quatre actes, aucun champ mecanique derive a la main (le bloc ci-dessus est rendu par --emit ; seuls complete, body, checks, b0, scope, domain sont des lectures).

Actes de lecture.

• complete — les 4 surfaces lues integralement : body, 2 commentaires, 0 review, 0 thread inline.
• body — le body annonce 4 fichiers ; le diff en porte exactement 4 (Grid.lean +162, Grid_en.lean +164, Tent_en.lean +2/-2, FORMAL_STATUS.md +2/-1). Rien hors perimetre annonce.
• checks — fold latest-wins a la source (commits/dff66a4d82/check-runs, dernier started_at par nom) : PR gate, lean-matrix / Lean CI (discrepancy_lean), i18n sibling drift, parity gate, Always-on guards — tous success. Aucun rouge residuel.
• b0 — python scripts/check_unaddressed_nits.py 19569 rend OK, aucun nit non leve. L'unique commentaire non evalue est l'explication de rebase de l'auteur (jsboige, 2026-10-07T05:07:05Z) : une declaration d'auteur, pas une reserve. L'advisory PR-PATH-COLLISION du bot (2026-10-06T19:11:57Z) est anterieur au rebase --onto origin/main et son verdict terminal visait le commit Tent absorbe, retire de la pile par ce rebase ; l'organe le declare lui-meme non bloquant.
• scope — pass : 4 fichiers, tous dans MyIA.AI.Notebooks/Search/discrepancy_lean/, coherents avec la tranche k3.2 annoncee. Le correctif de namespace Tent_en.lean (2 lignes, Discrepancy.Komlos -> Discrepancy.Komlos_en) est une modification distincte de la livraison de feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) #19563, pas une redondance.
• domain — pass (Lean). Criteres B.2 : distinct_code_sorry 0 -> 0 (aucun sorry dans les lignes ajoutees, verifie sur le patch) ; build prouve par la jambe CI lean-matrix / Lean CI (discrepancy_lean) verte a cette tete ; B.3 declaree « non applicable » avec son motif (§B.3 cas (a) : job lean-axiom non cable sur ce lake) ; jumeaux i18n verifies par la jambe i18n sibling drift verte.