feat(lean,#17845): brique k1.3 — opérateur overlap + identités de base (stack sur #19058)

[jsboige]

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

Stack — merger #19058 (k1.2) AVANT celle-ci. La branche est basée sur feature/komlos-k12-split : le diff affiché ci-dessus inclut la tranche k1.2 tant que #19058 est ouverte ; le delta propre à cette PR est le seul commit ced1306f7d (2 nouveaux modules + ligne FORMAL_STATUS k1.3). Après le merge de #19058, GitHub retire automatiquement la tranche k1.2 du diff.

Objet

Brique k1.3 de l'EPIC Komlos (#17845) : opérateur de recouvrement overlap — la masse commune de deux fonctions pondérées, quantité que la preuve élémentaire de Karingula–Lovett (arXiv:2609.20979) fait passer de P à sa translate puis contrôle à travers la scission split (k1.2). Module jumeau FR/EN Discrepancy/Komlos/Overlap.lean + Overlap_en.lean (convention i18n #4980).

Contenu

• overlap P Q S = ∑_{x∈S} min (P x) (Q x) — le Komlos.overlap P Q = mass (P ⊓ Q) de Dahia (gdahia/Komlos, Apache-2.0, copyright conservé en header) transposé au cadre Finset explicite du lake : l'infimum de Finsupp devient le min ponctuel, le support devient un argument.
• Identités closes : overlap_comm, overlap_self (= la masse), overlap_nonneg, overlap_mono, overlap_le_sum_left/right (domination par chaque masse), sum_le_overlap (mass_le_overlap chez Dahia — toute masse partagée est majorée), min_eq_half_add_sub_abs (min a b = ½ (a + b − |a − b|)).
• Reporté à k1.4 : l'identité pivot overlap P (P ∘ (· + u)) = 1 − Δ(P, u) sous masse 1 et invariance du support (exige sum_translate_image de k1.2 — d'où la stack — et la convention forward de ShiftDistance) ; overlap_tr ; Claim 3.2 (Δ(T_v P, (u,0)) ≤ Δ(P,u)) ; split_tr.
• Aucune dépendance sur ShiftDistance ou Split dans les imports (Discrepancy.Basic seul) : la brique se situe en amont de l'identité pivot ; c'est le découpage FORMAL_STATUS (conflit de lignes adjacentes évité par la stack, d'où le choix de baser sur k1.2).

Preuves (B Lean)

1. lake build EXIT=0 : les deux modules Discrepancy.Komlos.Overlap + Discrepancy.Komlos.Overlap_en built — « Build completed successfully (8708 jobs) », 0 error, 0 warning — via l'organe lean_exec (Lean: organe canonique d'exécution avec budgets machine-wide et confinement des processus #15666), env ext4 WSL (toolchain v4.33.0, Mathlib pin db584cd6), au premier essai.
2. Comptage sorry : count_code_sorry.py --json --lake MyIA.AI.Notebooks/Search/discrepancy_lean → distinct_code_sorry 0 → 0 (lake à 22 fichiers, aucun sorry introduit).
3. B.3 proof integrity : non applicable — le job lean-axiom n'est pas câblé sur ce lake (cas [Lean][CI] Critere B.3 « Proof integrity (axiom check) » : outillage existant non cable en CI + 2 defauts bloquants #8677, vérifié sur feat(lean,#17845): brique k1.2 — opérateur de scission T_v (Def 3.1) + identités #19058 : grep -ln 'lean-axiom' .github/workflows/*.yml liste 13 lakes, discrepancy_lean absent). CI couvrante : lean-ci-matrix.yml.
4. i18n : check_i18n_siblings.py → 7/7 pairs OK (dont la nouvelle paire Overlap), 0 drift, 0 orphan, byte-identiques hors docstrings.

Diagnostic dérive

N/A — nouveau module Lean (*.lean), pas de notebook.

See #17845 — brique k1.3 ; l'EPIC reste ouverte (k1.4 : identité pivot + Claim 3.2 ; k2 : Lemma 1.4).

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19060 (feat(lean,#17845): brique k1.3 — opérateur overlap + identités de base (stack sur #19058)) 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 k1.5 -- Claim 3.2 (Delta(T_v P, (u,0)) <= Delta(P,u)) #19063 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 k1.6 -- bit de scission (splitBit_eq) #19065 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 k1.7 -- contention de support (correctif d'hypothese des briques k1) #19066 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.0 -- moments de la scission (mean_split) #19068 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.1 -- algebre du pas de pullback (sans convexite) #19070 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.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)

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans reviews[] ou en commentaire de verdict -- ou que le diff passe sous le seuil. Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

[jsboige]

Conflit résolu — rebase de la pile Komlos (changement de tête : ced1306f7d → 5a6c67d84a)

Cause : le squash-merge de #19058 (k1.2, 31dd647be7 sur main) a laissé la branche porter les DEUX étages (a36e6f0438 k1.2 + ced1306f7d k1.3) — après retarget base=main, GitHub voyait k1.2 en double → mergeable: CONFLICTING (conflit fantôme d'absorption, cf submodule-maintenance R4 / pattern stack-squash).

Fix : git rebase --onto origin/main a36e6f0438 feature/komlos-k13-overlap — rejoue k1.3 seul sur main. Preuves :

• diff vs main : 3 fichiers, +268 (Overlap.lean, Overlap_en.lean, FORMAL_STATUS.md) — k1.3 scope pur, les Split.lean retombés dans le périmètre k1.2 déjà mergé ;
• git diff ced1306f7d 5a6c67d84a -- Search/discrepancy_lean/ : vide (répertoire Komlos byte-identique ancien/nouveau tip — aucune perte de contenu) ;
• git merge-tree --write-tree origin/main HEAD : pas de conflit ;
• commit rejoué : même message, même auteur, même trailer, +268/3 fichiers.

Conséquences pour le dossier : la tête a changé — tout dossier [ADJOINT PREFLIGHT] doit être écrit sur 5a6c67d84a. Le push de contenu ré-arme le plancher DWELL (élude ~18:20Z). La lane enchaînera le même geste sur chaque étage au fur et à mesure des merges de la pile (les 11 branches filles portent toutes les commits absorbés de leurs prédécesseurs).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA-2
pr: 19060
head: 5a6c67d
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 4d33555cee56566bcf6bbd0e40d88686bcf9e1e599484cba82ba256d3c0628d4
diff-files: 3
diff-additions: 268
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Notes pour la lecture coordinator (reponses nominatives au dispatch c1406) :

• Question Modules: (lean-axiom) : verifie firsthand sur le checkout -- discrepancy_lean est ABSENT des 13 workflows cablant lean-axiom (lean-axiom.yml, lean-ci-matrix.yml, etc., aucun n'a d'entree discrepancy). La verification Modules: est donc SANS OBJET pour ce lake : le claim B.3 « non applicable » du body (cas [Lean][CI] Critere B.3 « Proof integrity (axiom check) » : outillage existant non cable en CI + 2 defauts bloquants #8677, meme verification faite sur feat(lean,#17845): brique k1.2 — opérateur de scission T_v (Def 3.1) + identités #19058) est exact. La CI couvrante est lean-ci-matrix.yml : lean-matrix / Lean CI (discrepancy_lean): success @16:21:56Z a la tete rebasee -- corrobore le lake build 8708 jobs EXIT=0 du body.
• Post-rebase propre : la pile Komlos a ete rebasee apres le merge de feat(lean,#17845): brique k1.2 — opérateur de scission T_v (Def 3.1) + identités #19058 (commentaire lane 16:22:17Z : ced1306f7d -> 5a6c67d84a, conflit sur lignes FORMAL_STATUS documente). Le diff ne porte PLUS que la tranche k1.3 : 3 fichiers (Overlap.lean + Overlap_en.lean + FORMAL_STATUS.md) +268/-0 -- la tranche k1.2 est bien retiree du diff post-merge.
• B.0 rc=0, 27 jambes / 27 noms sans rouge latest-wins, PR gate success @18:24:19Z, mergeStateStatus CLEAN. Sorry 0->0 atteste (count_code_sorry, 22 fichiers). i18n 7/7 paires (nouvelle paire Overlap), check i18n sibling drift vert.
• Aucune review (label REVIEW-COVERAGE 12:17Z) -- ce dossier + la review ai-01 y pourvoient. Elle porte la pile k1.4-k2.6a : merger liberera le retarget des etages superieurs.

— dossier myia-po-2027:CoursIA-2, dispatch ai-01 c1406 (lot n°2).