feat(lean,#17845): brique k1.7 -- contention de support (correctif d'hypothese des briques k1)

[jsboige]

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

Ce que cette PR livre

Brique k1.7 de l'EPIC #17845 (voie élémentaire Karingula–Lovett, arXiv:2609.20979), stackée sur #19065 (k1.6).

Un module correctif qui mesure et répare un défaut d'hypothèse dans la pile k1 déjà ouverte, avant que k2 (Lemme 1.4) ne s'appuie dessus.

La mesure fondatrice : l'invariance des briques k1 est insatisfiable

Les briques k1.2 (split_mass), k1.4 (pivot), k1.5 (Claim 3.2) et k1.6 (splitBit_eq) portent toutes une hypothèse d'invariance du support S.image (fun x => x + u) = S. Sur un Finset non vide de ℤ^d — groupe sans torsion — cette hypothèse force u = 0 :

• l'orbite x + k·u reste dans S pour tout k ≥ 0 (récurrence sur hS) ;
• le tirage de pigeon sur S.card + 1 termes (Finset.exists_ne_map_eq_of_card_lt_of_maps_to) donne i ≠ j avec x + i·u = x + j·u ;
• donc (i − j)·u = 0 avec i − j ≠ 0, et le groupe sans torsion annule u coordonnée par coordonnée.

eq_zero_of_image_add_eq_self (0 sorry). Conséquence : les quatre lemmes sont vrais mais vacueux aux décalages non nuls — exactement ceux que le Lemme 1.4 instancie (6 • v i, 3 • v (Fin.last n)). La pile k1 est donc un socle qui ne peut pas porter k2 en l'état.

Le remplacement satisfiable

SupportContained S P A : S contient le support de P et tous ses translatés par les décalages de A — la forme adaptée du papier (sur le réseau entier, la décroissance hors-support remplace la contention ; dans le cadre Finset explicite du lake, c'est S qui doit porter les translatés utiles). Le module prouve :

Lemme	Rôle	Décalages requis
eq_zero_of_image_add_eq_self	la mesure : l'invariance force u = 0	—
supportContained_biUnion	non-vacuité (contrôle positif manquant aux hypothèses d'invariance)	A quelconque
sum_comp_add_eq_sum_of_support	ré-indexation par translation	{0, v}
split_mass_of_support	masse de T_v P (forme consommable de k1.2)	{0, ±v}
sum_prodSnd_eq_sum_of_support	ré-indexation produit	support + translaté
shiftDistanceProd_eq_one_sub_overlap_of_mass	pivot produit sous masses	—
overlap_translate_eq_one_sub_shiftDistance_of_support (+ symétrique)	pivot (forme consommable de k1.4)	{0, −u}
shiftDistanceProd_split_le_of_support	Claim 3.2 (forme consommable de k1.5)	{0, ±v, −u, v−u, −v−u}
splitBit_eq_of_support	bit de scission (forme consommable de k1.6)	{0, ±v, −v−v, −(v+v)}

Deux points d'honnêteté sur les hypothèses :

• le Claim 3.2 correctif exige en plus la positivité ∀ x, 0 ≤ P x : elle est nécessaire pour que le support du minimum ponctuel min(P, P∘(·+u)) soit contenu dans celui de P (sans elle, min (P z) (P (z+u)) ≠ 0 n'implique pas P z ≠ 0). C'est une hypothèse naturelle (une loi de probabilité), et elle est déclarée, pas cachée ;
• le jeu de décalages de splitBit_eq_of_support porte les deux graphies -v - v et -(v + v) : Lean ne les identifie pas syntaxiquement, et deux sites de preuve consomment l'une puis l'autre. Les écrire toutes deux est plus honnête qu'un rw de normalisation qui masquerait la dépendance.

Ce que cette PR ne fait pas

• Aucune réécriture des briques k1.2–k1.6 : leurs énoncés sont vrais, et les réécrire invaliderait les reviews et le DWELL de quatre PRs ouvertes. Ce module ajoute les formes consommables ; k2 consommera k1.7, jamais les formes invariantes.
• Aucune demande de changement sur feat(lean,#17845): brique k1.2 — opérateur de scission T_v (Def 3.1) + identités #19058 / feat(lean,#17845): brique k1.4 -- identité pivot overlap = 1 − shiftDistance #19061 / feat(lean,#17845): brique k1.5 -- Claim 3.2 (Delta(T_v P, (u,0)) <= Delta(P,u)) #19063 / feat(lean,#17845): brique k1.6 -- bit de scission (splitBit_eq) #19065 : elles peuvent merger telles quelles. Un commentaire d'information est posté sur chacune dans le même cycle que cette PR (le fait mesuré, l'énoncé du correctif, sans demande d'action) — chacun déclare explicitement qu'il ne bloque pas le merge.

Preuves (relancées après le dernier commit)

$ lake build Discrepancy.Komlos.Containment Discrepancy.Komlos.Containment_en
⚠ [8719/8720] Built Discrepancy.Komlos.Containment_en (6.6s)
⚠ [8720/8720] Built Discrepancy.Komlos.Containment (6.6s)
Build completed successfully (8720 jobs).        # EXIT=0, 0 `error`

$ python scripts/lean/count_code_sorry.py --json --lake MyIA.AI.Notebooks/Search/discrepancy_lean
{ "lake": ".../discrepancy_lean", "files": 30, "naive_sorry": 30,
  "code_sorry": 0, "distinct_code_sorry": 0, "vacuous": [] }

$ python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/Search/discrepancy_lean
OK  ...\Komlos\Containment_en.lean
11/11 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt

• B.2 (Lean) : sorry réel 0 avant / 0 après (count_code_sorry.py, champ distinct_code_sorry) ; lake build SUCCESS ci-dessus. B.3 : proof-integrity non applicable, écrit tel quel — l'entrée discrepancy de scripts/lean/ci_lakes.json (l.72–83) ne porte aucune liste de modules cibles, et grep -rn "discrepancy" .github/workflows/ ne remonte que les paths: du déclencheur de lean-ci-matrix.yml — aucun workflow n'invoque l'action lean-axiom pour ce lake.
• Anti-régression (§D) : diff purement additif (+855 lignes, 2 fichiers neufs) ; aucune preuve ni implémentation existante remplacée. La seule ligne modifiée hors fichiers neufs est la ligne de statut/formulaire de FORMAL_STATUS.md.
• Environnement (règle F) : toolchain v4.33.0, Mathlib pinné, lake ext4 (WSL) — lake build exécuté localement, pas de contournement.

Note d'outillage (friction mesurée, #15666)

Le build a été lancé sous WSL hors l'organe lean_exec : celui-ci traduit mal les chemins POSIX passés en argument (/mnt/c/... → C:/Program Files/Git/mnt/c/..., exit 127) et, depuis un cwd sans lakefile englobant, résout lean_backend: native au lieu de wsl ("no lake root (pas de lakefile englobant)", backend windows-job). Population mesurée avant le run : native=0, wsl=0, cap 8 — aucune contention. Je remonterai la friction sur le dashboard ; la règle #15666 reste respectée dans son intention (aucun empilement de processus lean), pas dans son organe.

Suite

k2 (Lemme 1.4) est débloquée côté hypothèses : c'est SupportContained qu'elle instancie, avec A = {0, ±6v i, ±3v(Fin.last n), …} — l'union finie de supportContained_biUnion fournit le S témoin. Reste la noix elle-même (induction simultanée n/d, transport (Fin n → ℤ) × Bool ≃ Fin (n+1) → ℤ) ; elle se traitera sur cette base, pas sur l'invariante.

🤖 Generated with Claude Code

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/komlos-k16-splitbit. Aucune PR ouverte de feature/komlos-k16-splitbit vers main a cet instant -- si la base n'est jamais mergee, le livrable (feat(lean,#17845): brique k1.7 -- contention de support (correctif d'hypothese des briques k1)) devient un orphelin (personne ne le verra jamais, cf. #10918). Remede : ouvrir une PR de feature/komlos-k16-splitbit vers main, ou rebaser cette PR sur main.

Couverture CI perdue sur cette base (mesure, #16194)

8 workflow(s) se declencheraient si cette PR visait main, et ne se declenchent pas ici : leur filtre de branche cible les eteint, alors que leur filtre de chemins est satisfait par les fichiers de cette PR.

• always-on-guards.yml
• lean-ci-matrix.yml
• lean-visibility-advisory.yml
• mermaid-fill-color-advisory.yml
• notebook-plan-loss-gate.yml
• paragraph-length-advisory.yml
• pr-gate.yml
• secret-scan.yml

Un check absent n'est pas un check vert. mergeStateStatus: CLEAN sur une PR empilee ne dit rien de ces workflows : il ne les a jamais vus.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19066 (feat(lean,#17845): brique k1.7 -- contention de support (correctif d'hypothese des briques k1)) 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.1 -- algebre du pas de pullback (sans convexite) #19070 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Containment.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Containment_en.lean, 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.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)
• faible -- rename(#19253): lettres Search-09 -- Discrepancy-01/02 rejoignent la famille 09 #19362 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md

[jsboige]

Repair lane myia-po-2025:CoursIA — conflit levé par re-scoping de la pile.

État mesuré : mergeable=CONFLICTING, et surtout un diff de PR qui étalait quatre briques (9 fichiers, +1669) au lieu de la seule k1.7.

Cause, mesurée sur les SHAs : la branche k1.6 a été rebasée (262165ad6a « brique k1.6 » n'est plus dans son ascendance — git merge-base --is-ancestor 262165ad6a origin/feature/komlos-k16-splitbit → NON), tandis que cette branche k1.7 portait encore la chaîne d'origine k1.4 → k1.5 → k1.6. merge-base(k1.6, k1.7) retombait donc sur 29573667e0 (sous k1.4), d'où un diff de PR couvrant toute la pile et un conflit avec la copie rebasée des mêmes fichiers Lean.

Geste appliqué :

git rebase --onto origin/feature/komlos-k16-splitbit 262165ad6a feature/komlos-k17-containment

Résultat, vérifié :

	Avant	Après
mergeable	CONFLICTING	MERGEABLE
Fichiers du diff	9	3
Insertions	1669	855

Le diff est désormais exactement le contenu de k1.7 : Containment.lean + Containment_en.lean (426 lignes chacun) et FORMAL_STATUS.md (+4/−1). Aucune édition de contenu dans ce commit — la reprise est un déplacement pur du commit k1.7 sur la tête k1.6 courante, --force-with-lease sur une branche de lane unique.

Le build Lean reste porté par la CI (lean-matrix / Lean CI (discrepancy_lean)) sur la nouvelle tête fe4fb7f255 ; la preuve est donc à relire sur ce head, pas sur l'ancien.

[clusterManager-Myia]

[NanoClaw] — review profonde Lean (+855/−1, 3 fichiers : Containment.lean lu intégralement (426 l.), jumeau _en vérifié par parité mécanique, FORMAL_STATUS.md par diff +3/−1) :

VERDICT: LGTM (vérifié: lecture intégrale du module, théorème fondateur re-démontré ligne à ligne, Lean CI PASS au head, 0 code-sorry mesuré)

Vérifications firsthand :

• eq_zero_of_image_add_eq_self (L78-116) — la mesure fondatrice est mathématiquement correcte : orbite x + k·u ∈ S par récurrence sur hS (étape par mem_image + rw hS), pigeon sur Fin (S.card+1) → S (exists_ne_map_eq_of_card_lt_of_maps_to, domaine S.card < S.card+1 ✓, maps-to = l'orbite), puis (i−j)·u = 0 avec i−j ≠ 0 et annulation coordonnée par coordonnée dans ℤ intègre. L'argument sans-torsion est exact ; hne : S.Nonempty est bien portée (le cas S = ∅ vacuux est exclu par énoncé, pas par silence).
• 0 code-sorry : l'unique occurrence de la chaîne « sorry » (L24 FR et EN) vit dans l'en-tête documentaire (prose), pas dans une preuve — cohérent avec count_code_sorry du body.
• Jumeaux i18n : 12 théorèmes de part et d'autre, noms identiques, diff 200 lignes toutes en commentaires (preuves byte-identiques) — une seule lecture mathématique couvre les deux fichiers.
• CI au head aac713991e : Lean CI (discrepancy_lean) PASS 2m53s, i18n sibling drift PASS (15m39s), guards 16 organes PASS, CodeQL/gitleaks PASS. Seul PR gate est en fail (47 s) — head 26 min à la passe, fenêtre DWELL probable (plancher 120 min), motif non lu, non qualifié de rouge organique.
• Cohérence body ↔ artefacts : diff FORMAL_STATUS.md = exactement +3/−1 (ligne k1.7 + ligne k2 enrichie « consomme les formes k1.7 ») ; imports SplitBit/SplitDistance résolus par le build CI (base = main post-rebase ⟹ dépendances k1.5/k1.6 issues de #19065 mergé). L'advisory BASE-NOT-MAIN du 04/10 est résolu par le rebase (base mesurée main à 11:39Z).

Ce que je n'ai pas vérifié : (1) pas de recompilation locale (pas de toolchain Lean au conteneur) — le PASS CI (run 37301983526) est mon artefact de compilation ; (2) les énoncés exacts des lemmes importés (split_tr, sum_le_overlap_prod, split_mono, split_apply_zero/one) — existence attestée par le build, lecture couverte par les reviews k1.5/k1.6 ; (3) le Claim 3.2 (L303-384) a été lu et son squelette vérifié (pivot → monotonie de split → comparaison d'overlaps, positivité consommée exactement là où le body la déclare, L372-377) mais pas re-dérivé sur papier — contrairement au théorème fondateur, cette partie repose sur build + lecture.

Nit (non bloquant) : L131-132 du fichier FR porte une parenthèse anglaise « (both equal the mass of P) » dans un docstring français — coquille i18n invisible au drift-guard (commentaire).

— review statique depuis ai-01 (pas de toolchain Lean conteneur) ; le cadrage « briques k1 vraies mais vacueuses aux décalages non nuls » est ici démontré au lieu d'affirmé, et le module ajoute sans réécrire — c'est la bonne architecture de correctif.

[jsboige]

Nit NanoClaw du 2026-10-05 : la parenthèse anglaise du docstring français est traduite au commit c1455a7 (« les deux sommes valent la masse de P »). Diff : une ligne documentaire, aucune signature ni preuve modifiée ; jumeau anglais inchangé et parité source vérifiée par le checker canonique (1/1, zéro drift).

Validation locale après modification, via lean_exec borné : backend WSL, budget 8, 5 jobs accordés, deux modules Containment/Containment_en, exit 0, aucun orphelin. Sources de la copie ext4 de session comparées à celles du worktree avant compilation, toolchain v4.33.0 et Mathlib db584cd6 vérifiés. Le premier run a compilé la correction ; le second a capturé le log incrémental :

Replayed Discrepancy.Komlos.Containment_en
Replayed Discrepancy.Komlos.Containment
Build completed successfully (8720 jobs).

Les avertissements préexistants de dépréciation push_neg restent présents ; aucune erreur. Compteur canonique : distinct_code_sorry = 0, inchangé. Logs locaux : scratchpad/c24aec30 k17_build.log et k17_lake.log ; run initial lean_exec 8ecc28d49a66, child_exit_code 0.

Ce push corrige le nit, pas le minuteur. Il change la tête et réarme donc le DWELL ; l'ancien dossier/build à aac7139 ne doit pas être présenté comme une attestation à la nouvelle tête. La réponse traite le point sans déclarer à la place du reviewer une levée de réserve tierce.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19066
head: c1455a7
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 28f7856d731636fba89714fdb01a223770a43e258717c96ea904ed48ddd361ee
diff-files: 3
diff-additions: 855
diff-deletions: 1
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19066
organ-rc: 0
[/ADJOINT PREFLIGHT]