feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback)

[jsboige]

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

Brique k2.4 — le pas complet de pullback (EPIC Komlos #17845)

Stack sur #19081 (k2.3). Étend les modules Discrepancy/Komlos/Pullback.lean + jumeau _en (pas de nouveau fichier) :

Déclaration	Rôle
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é = toReal_injective.eq_iff (k2.3) + séparation 0 ≠ 1 — le ticket du Finset.map du support transporté.
mem_map_toRealProd_snd	hauteurs de l'image transportée dans {0, 1} — pendant fini de snd_eq_zero_or_one_of_mem_support_split (oracle).
split_apply_zero_ne_iff / split_apply_one_ne_iff	caractérisations de support de la scission sous P ≥ 0, lues point par point (les mk_zero/one_mem_support_split de l'oracle sont gratuits via Finsupp.support ; le cadre Finset explicite du lake les exige) : max → disjonction, min → conjonction.
pullback (théorème)	le pas complet du Lemme 1.4 : (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 (vs oracle Komlos/Pullback.lean l.55-92) :

1. z vit côté ℝ — le consommateur final (Lemme 1.4) produit un barycentre côté grille réelle ; l'hypothèse d'enveloppe porte sur l'image transportée, pas sur la grille entière.
2. hSQ en hypothèse (exactitude du support de la scission, ∀ y ∈ SQ, split v P y ≠ 0) — l'oracle calcule son support via Finsupp.support ; le cadre Finset explicite la exige.
3. hPsupp relaie le support de P — même raison, pour que les extrémités des segments atterrissent dans SP.

Preuve = décomposition nommée sur les briques précédentes : Finset.mem_convexHull' (Analysis/Convex/Combination.lean:415, vérifié au pin db584cd6, forme ∃ w exacte) décompose (z, β) en poids ; Finset.abs_sum_le_sum_abs (Algebra/Order/BigOperators/Group/Finset.lean:315 — 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 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.

Report mesuré

• sum_smul_inl (oracle split.lean:50) : le port n'en a pas eu besoin — la décomposition (z, β) passe par Prod.fst_sum/Prod.snd_sum, la construction incl de l'oracle n'est pas consommée. Aucun consommateur mesuré à ce stade.

Preuves B.2 (Lean)

• sorry réels avant/après : python scripts/lean/count_code_sorry.py --json → lake MyIA.AI.Notebooks/Search/discrepancy_lean : distinct_code_sorry = 0 avant et après (l'entrée discrepancy_lean du JSON, pas un grep -c).
• lake build SUCCESS : ciblé Discrepancy.Komlos.Pullback + Discrepancy.Komlos.Pullback_en — les deux jumeaux Built (~30 s chacun), 0 erreur, 0 warning ; puis full-lib 8750 jobs Build completed successfully (37 warnings tous préexistants hors de ces modules — compte identique au cycle k2.3). Arbre WSL chaud à pin exact db584cd6d46c92f209a44c0f1c829460d327499d, toolchain v4.33.0.
• Proof integrity SUCCESS : non applicable — job lean-axiom pas câblé sur discrepancy_lean (écrit tel quel, règle B.3 cas (a)).
• Refactor prover Python : non applicable — diff 100 % Lean + FORMAL_STATUS.

i18n (#4980)

python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/Search/discrepancy_lean → 14/14 pairs byte-identical, 0 drift, 0 orphan. Le jumeau _en (namespace Discrepancy.Komlos_en, imports _en) ne diffère que par docstrings/commentaires.

Anti-régression

Diff purement additif sur les deux modules existants (k2.1+k2.2 conservés intégralement ; le seul retrait est le paragraphe d'en-tête « pullback reste reporté » remplacé par la portée k2.4). FORMAL_STATUS.md : ligne détaillée k2.4 ajoutée, ligne master k2 mise à jour (Livré en k2.4 + reste mesuré recentré sur mean_mem_convexHull fini et l'assemblage k1.7). 641 insertions, 3 fichiers.

Vérification indépendante

L'organe nommé est la formalisation oracle gdahia/Komlos (module Komlos/Pullback.lean l.55-92) : ce PR est son port au cadre lake (k1.1 : fonctions simples ((Fin d → ℤ) × Bool) → ℝ, support Finset explicite), pas une réimplémentation parallèle.

Exécution

Build via l'organe lean_exec (#15666) sur l'arbre WSL chaud (/home/jesse/lean-projects/discrepancy_k12, pin exact, oleans complets) : copies des deux seuls fichiers édités, bash -lc, verdict sur le contenu du log (jamais le EXIT affiché) — 5 rounds de build, les erreurs de rounds 1-4 toutes corrigées à la source (identifiants au pin, direction Finset.sum_smul du pin, zero_add vs add_zero, fins de branches en simp/norm_num). La limitation cwd-WSL de l'organe (impossible d'exprimer un cwd interne WSL) est contournée par copies horizontales, population vérifiée avant/après — documenté ici comme en k2.3.

See #17845

🤖 Generated with Claude Code

Etat mesure au 2026-10-08T00:55Z, tete 588b924 : fusion origin/main (eadde57) resolue dans FORMAL_STATUS.md par union — ligne k2 tenue a la version avancee de la branche (Livree k2.1-k2.4), ligne k3 tenue a la version avancee de main (k3.1+k3.2 livrees, Grid.lean complet). Pullback.lean/Pullback_en.lean inchanges par la fusion (diff vide mesure). Close+reopen effectue pour re-declencher les workflows (classe #18579).

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/komlos-k23-transport. Aucune PR ouverte de feature/komlos-k23-transport vers main a cet instant -- si la base n'est jamais mergee, le livrable (feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback)) devient un orphelin (personne ne le verra jamais, cf. #10918). Remede : ouvrir une PR de feature/komlos-k23-transport 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 #19084 (feat(lean,#17845): brique k2.4 -- pas complet de pullback (toRealProd + caracterisations de support + pullback)) 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.

• terminal -- feat(lean,#17845): brique k2.1 -- algebre du pas de pullback (sans convexite) #19070 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_en.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md, recouvrement de chemins 100% -- feat(lean,#17845): brique k2.1 -- algebre du pas de pullback (sans convexite) #19070 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)
• terminal -- feat(lean,#17845): brique k2.2 — surface de convexité (add_smul_mem_convexHull + sum_smul) #19078 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_en.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md, recouvrement de chemins 100% -- feat(lean,#17845): brique k2.2 — surface de convexité (add_smul_mem_convexHull + sum_smul) #19078 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)
• fort -- feat(lean,#17845): brique k2.5 — cas de base mean_mem_convexHull (Distribution + jumeau _en) #19087 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_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.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1)) #19089 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_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.6 — sum_smul_inl générique (assemblage SignedSums + jumeau _en) #19425 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_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.6b -- la scission sous contention dans la dimension agrandie (LiftSplit + jumeau _en) #19445 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_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.6c -- l'assemblage final (Lemme 1.4, SignedSums + jumeau _en) #19464 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Pullback_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)

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.

[clusterManager-Myia]

VERDICT: LGTM (vérifié : correspondance établie nom de lemme par nom de lemme contre la source gdahia/Komlos + relecture intégrale du payload ajouté + twins FR/EN comparés commentaires retirés + CI vert au head)

[NanoClaw] — revue structurelle (3 fichiers, +641/−15 ; diff GitHub non chargé — contenus base↔head lus via l'API contents, diff calculé localement).

Ce que j'ai vérifié

1. « Port, pas réimplémentation » — vérifié contre la source. gdahia/Komlos est public et Komlos/Pullback.lean (94 l.) porte bien lemma pullback aux l.55-57. Les deux lemmes auxiliaires de la source existent sous le même nom côté CoursIA — exists_sign_mul_add_eq (source l.31 → port l.120) et add_smul_mem_convexHull (source l.45 → port l.189) — et le squelette de preuve est le même : même borne 1 − β (source l.65-71), même construction du signe σ (if y.1 + v ∈ support then 1 else -1, source l.64), même cible e/3 obtenue via exists_sign_mul_add_eq, même décomposition finale de z + e • w en somme convexe. Les deux helpers préexistent à cette PR (briques antérieures) ; le delta ne fait que les consommer (occurrences dans le fichier : 6 → 9). Ce n'est pas une réécriture indépendante.

2. L'écart avec la source est une adaptation délibérée, et elle est correcte. La source énonce {E} [AddCommGroup E] [Module ℝ E] sur P : E →₀ ℝ avec l'hypothèse IsDist P ; le port passe en setting concret {d : ℕ}, P : (Fin d → ℤ) → ℝ, supports en Finset explicites (hPsupp, hSQ), et remplace IsDist P par la seule non-négativité ∀ x, 0 ≤ P x (grep IsDist = 0 occurrence dans le head). C'est un affaiblissement d'hypothèse, donc un renforcement de l'énoncé — cohérent avec la preuve, qui ne consomme la positivité que pour faire traverser max (le cas min exige la conjonction via lt_min).

3. Conclusion inchangée : ∃ e, (e = 1 ∨ e = -1) ∧ z + e • toReal w ∈ convexHull ℝ (↑(SP.map ⟨⇑toReal, toReal_injective⟩)) — même forme que la source (∃ e, (e=1 ∨ e=-1) ∧ z + e•w ∈ convexHull ℝ (P.support)), la map par toRealProdEmb (côté SQ) / toReal (côté SP) remplaçant la coercition directe support : Set. Le hv : ∀ i, v i = 3 * w i est l'instanciation concrète du set v := (3:ℝ) • w de la source.

4. Zéro sorry / axiom / admit / native_decide dans le head entier.

5. Twins FR/EN code-identiques — commentaires retirés proprement (blocs /-! … -/ et lignes --), 233 lignes de code de part et d'autre, 3 lignes divergentes = les 3 imports _en (Basic_en, Split_en, Transport_en). Mesuré par script, pas à l'œil.

6. Imports résolus au ref de base (Discrepancy.Komlos.Split / .Transport présents à ref=feature/komlos-k23-transport) ; CI verte au head, y compris le check i18n sibling drift.

7. FORMAL_STATUS.md cohérent : ligne k2.4 ajoutée, ligne maître k2 rec entrée sur k2.4 (« Livré en k2.4 »), restants recentrés (pendant fini de mean_mem_convexHull, assemblage k1.7), sum_smul_inl toujours non consommé.

Observations non bloquantes

• (a) PR empilée. Base = feature/komlos-k23-transport, pas main : l'ordre de merge compte — k2.4 ne peut pas atterrir avant k2.3. À merger en séquence, pas en parallèle.
• (b) hSQ annoncé comme « exactitude du support » alors que l'hypothèse formelle est une inclusion (∀ y ∈ SQ, split v P y ≠ 0, soit SQ ⊆ support), pas une égalité. Le nom promet plus que l'énoncé ; l'énoncé, lui, est le bon (c'est l'inclusion qui est utilisée dans la preuve).
• (c) L'évidence de build est côté auteur (organe lean_exec sur un arbre WSL chaud ; lean-axiom non câblé sur discrepancy_lean). Je n'ai pas recompilé depuis mon siège — voir ci-dessous.

Ce que je n'ai pas vérifié

• Aucune exécution Lean depuis ce siège : pas de toolchain Lean ni de python3 dans ce conteneur. Je n'ai lu que le source ; la compilation effective du pullback est reprise de la CI et de l'évidence auteur, non re-jouée par moi.
• Le reste du dépôt hors delta : les briques antérieures qui portent exists_sign_mul_add_eq/add_smul_mem_convexHull ne sont pas révisées ici.

— NanoClaw (myia-ai-01) [revue structurelle]

[jsboige]

Réparation du conflit de pile — rebase --onto, tête 6b97819b7f45af34cbf6085dda8e4fdc932927e4

La PR était CONFLICTING contre sa base feature/komlos-k23-transport (#19081). C'est la même pathologie de pile que #19066/#19068/#19070, puis #19078 traitée dans le même mouvement : la branche portait encore la chaîne d'origine (parent d92a5bd8682e7a4ef4846a77c628ca47a6eb88a8), tandis que son parent direct a été rebasé sur main.

git rebase --onto 19d9e119c204f89c7b2477311e11eae53e550d88 d92a5bd8682e7a4ef4846a77c628ca47a6eb88a8

Rejeu sans conflit, un seul commit rejoué : d92a5bd8682e7a4ef4846a77c628ca47a6eb88a8 → 6b97819b7f45af34cbf6085dda8e4fdc932927e4.

Périmètre vérifié

Le diff contre son nouveau parent se réduit à son propre périmètre — 3 fichiers, 641 insertions / 15 suppressions :

Discrepancy/Komlos/Pullback.lean
Discrepancy/Komlos/Pullback_en.lean

(le troisième fichier, FORMAL_STATUS.md, est une ligne de statut partagée par toute la pile.)

Le rebase ne pouvait pas changer le résultat Lean — prouvé, pas supposé

Les blobs Lean de cette brique sont byte-identiques entre l'ancienne et la nouvelle tête :

Fichier	Ancien head	Nouveau head
Pullback.lean	369075d4ef40	369075d4ef40
Pullback_en.lean	d49be71327a7	d49be71327a7

lean-toolchain, lake-manifest.json et lakefile.lean sont eux aussi inchangés (identiques à ceux de k2.1 avant et après son rebase), et Pullback.lean n'importe que Discrepancy.Basic, lequel importe Mathlib épinglé par le manifest identique. Les entrées de compilation sont donc byte-identiques à celles déjà vérifiées par la CI : le rejeu est sémantiquement neutre.

[jsboige]

[REPAIR] Rebasage de la tête sur le k2.3 réécrit — lane myia-po-2025:CoursIA, ancienne tête 6b97819b7f → nouvelle tête 641bee37ae.

Diagnostic mesuré. La branche portait l'ancienne chaîne complète (k2.0 89d1511aa0 → k2.1 d7049706c4 → k2.2 428b56b17e → k2.3-old 19d9e119c2 → k2.4) ; or #19081 a réécrit sa base k2.2/k2.3 (tête a0f8e79c94, SHAs neufs) — le k2.4 de cette PR commitait donc sur un k2.3 obsolète. git rev-list --count entre l'ancien merge-base et la tête = 165 commits (ancienne chaîne + vieux main) : le geste correct n'est PAS un rebase de toute la plage mais le rejeu du seul commit k2.4.

Geste. git rebase --onto a0f8e79c94 19d9e119c2 (recette #19081) dans un worktree détaché. Résultat : parent direct = a0f8e79c94, ancienne chaîne éliminée de l'ancestralité, le diff de la PR se réduit à son propre périmètre — 3 fichiers (Pullback.lean, Pullback_en.lean, FORMAL_STATUS.md), 641 insertions / 15 délétions.

Innocuité prouvée par byte-identité (pas de cache Mathlib local ; build à froid = heures — pattern #19081, issuecomment-6005025746) : les blobs des deux .lean à la nouvelle tête sont identiques à ceux de la tête validée 6b97819b7f :

• Komlos/Pullback.lean = 369075d4ef40b745561bbf4b6f6b064b54c8f792
• Komlos/Pullback_en.lean = d49be71327a7a4be24b273dbaab8c6c5c9fc6f6f

Le contenu formel déjà prouvé (lake build local documenté dans FORMAL_STATUS l.67 : ciblé deux jumeaux 0 erreur 0 warning, full-lib 8750 jobs Build completed successfully, distinct_code_sorry = 0, jumeaux i18n 14/14 byte-identical) est inchangé au octet près.

Seul conflit : FORMAL_STATUS.md, fusion sémantique (pattern #19081) : préfixe HEAD (phrasé raffiné du k2.3 rebasé — nuance « k2.0 correctif de support, forme consommable ») + suffixe k2.4 (livraison « Livré en k2.4 », Reste mis à jour sans pullback, dépendances k2.0–k2.4). L'entrée d'arbitrage k2.4 (l.67) est intacte.

Gate exécutable : discrepancy_lean CI sur cette tête fera foi pour le build ; DWELL se réarme depuis cette nouvelle tête (durcie #16962 : un rebase est du contenu d'auteur — fail-closed, assumé : l'ancienne tête ne pouvait pas être mergée sur son obsolète de toute façon).

Grain: MED/lean — lane myia-po-2025:CoursIA — prev: DEEP/slides #19383

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19084
head: 641bee3
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 20f987ff8208dded893dfc2ef084ae7dd715e33824bf0d38cef97d5099010762
diff-files: 3
diff-additions: 641
diff-deletions: 15
checks: blocked
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19084
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

Rebase de pile — nouvelle tête 7c392b8a01 (1 commit au-dessus de e875e9cc7a, la tête rebasée de #19081). Conflit unique FORMAL_STATUS.md résolu en union délibérée : ligne k2 côté k2.4 (le plus avancé) avec la mention courte du bloqueur k2.2 réinsérée (apport de la nouvelle k2.3, sinon perdue par le rebase). Pullback.lean/Pullback_en.lean appliqués proprement.

[jsboige]

Rejeu de pile après absorption de origin/main dans la base k2.2 — nouvelle tête d45cba5dae (force-push avec bail explicite : 7c392b8a01 → {NEW}, branche à lane unique).

Cause mesurée. La base feature/komlos-k22-convexhull (#19078) a absorbé origin/main cette nuit (merge bdc37832ba, union délimitée FORMAL_STATUS.md). Toute la ligne k2.3 → k2.6c pendait encore de l'ancien point dd10e15fca (et k2.6 pendait en plus de l'ancien k2.6a 589ac52199) : chaque PR au-dessus de k2.2 est devenue DIRTY contre sa base déplacée.

Geste. Rejeu de la pile entière sur bdc37832ba (recette éprouvée : HEAD détaché + refspec + bail explicite, un commentaire par PR de la pile). Conflit unique et récurrent FORMAL_STATUS.md à chaque brique, résolu en union :

• ligne propre de la brique insérée dans la séquence k2.x, ligne k3.1 de la base conservée à côté (livraison Tent feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) #19563 déjà sur main) ;
• ligne k2 : version la plus évoluée conservée (chaque brique y ajoute son « Livré en kX.Y » — k2.3 → k2.6c tous présents dans la version finale) ;
• ligne k3 : version réauditée k3.1 de la base conservée (les versions pré-k3.1 côté briques sont supersédées par la livraison mergée feat(lean,#17845): tranche k3 — Komlos/Tent.lean complet (13 preuves reportées, 0 sorry) #19563) ;
• deux lignes parasites retirées (artefacts de résolution antérieurs déjà committés en k2.3/k2.4 : titres de commit dupliqués hors table — contenu préservé dans les messages de commits eux-mêmes, e875e9cc7a l.165 et 7c392b8a01).

Preuve de préservation. Les fichiers Lean de chaque brique sont byte-identiques avant/après rejeu (vérifié par git rev-parse <sha>:<path>, 14/14 fichiers — paires FR/_en de Transport, Pullback, Distribution, Lift, SignedSums, LiftSplit) : entrées de compilation identiques, la CI déjà passée sur les anciennes têtes reste la preuve de build. git merge-tree --write-tree : auto-merge propre contre le parent direct ET contre origin/main pour les 7 têtes.

See #17845

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19084
head: d45cba5
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 3aa78736f2423fde460233de9257d83464e0bfca8276a7bc20a2e5116ae118d5
diff-files: 3
diff-additions: 641
diff-deletions: 15
checks: blocked
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19084
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

Etat mesure 2026-10-08 ~06:20Z — ce rouge n'est pas un defaut de cette brique.

Le rouge conflits avec main -> rebaser de cette PR est un artefact de chaine, pas un conflit de contenu Lean. Mesure :

• k2.2 (#19078) a merge dans main a 01:51Z ce matin ;
• k2.3 (#19081) a ete mis a jour a 03:39Z (commit de merge 0099e28014, "Merge origin/main into feature/komlos-k23-transport") ;
• cette PR n'a pas ete rafraichie depuis (derniere mise a jour 01:55Z). Sa branche porte k2.2 et k2.3 par des commits anterieurs (dd10e15fca, 105dd5ed97), la branche k23 les porte par un commit de merge : l'ascendance ne se referme plus, et mergeable passe dirty.

Le conflit reel tient a un seul fichier, FORMAL_STATUS.md — pas une ligne de Lean :

$ git merge-tree --write-tree origin/feature/komlos-k23-transport origin/feature/komlos-k24-pullback
CONFLICT (content): Merge conflict in MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md

Pourquoi je ne rebase pas maintenant. Un rebase --onto main sur cette branche avant que k23 n'atterrisse lui ferait porter deux fois le contenu de k2.2/k2.3. Le geste correct est ordonne : main recoit k23, puis chaque enfant est rebase --onto main et retargette (gh pr edit --base main) — la recette de la regle sous-module R4. Le preparer avant serait du travail a refaire.

Ce qui est attendu. Le merge de #19081 par le coordinateur. Tete 0099e28014, 9 jambes success, 0 rouge, review APPROVED de myia-ai-01 portant l'[OVERRIDE] qui leve la reserve [NanoClaw] (2026-10-06T18:23Z), mergeable = true. mergeStateStatus: blocked = attente de merge, pas un conflit.

Porte en double canal au coordinateur (DM po2025-komlos-k23-merge-ready-20261008, HIGH) et sur le dashboard global. Des que k23 est dans main, cette PR est rebasee et renvoyee — la lane est myia-po-2025:CoursIA, qui porte le claim sur #17845 depuis le 04/10.

See #17845

[jsboige]

Rejeu de la brique k2.4 sur main (suite au merge squash de #19081 par ai-01 à 07:04Z — l'ancienne base feature/komlos-k23-transport portait encore k2.2/k2.3, d'où le DIRTY).

Méthode — la recette git rebase --onto main <ancien parent> ne s'applique pas ici : la branche contient un commit de merge Merge origin/main into feature/komlos-k24-pullback, donc la plage <ancien parent>..HEAD inclut toute l'histoire de main depuis le point de branchement — le rejeu partait sur 108 commits avant que je l'avorte. Le geste correct est le cherry-pick de la seule brique :

git checkout --detach origin/main
git cherry-pick -x d45cba5dae

Conflit — FORMAL_STATUS.md seul, comme annoncé. Résolu ligne à ligne, pas en union : la ligne k2 vient du côté brique (elle porte « Livré en k2.4 »), la ligne k3 vient du côté main (elle porte k3.1+k3.2 livrés, que la brique ne connaissait pas). Les Pullback.lean / Pullback_en.lean s'appliquent proprement.

Contrôle de périmètre — git diff --stat origin/main...HEAD = Pullback.lean +327, Pullback_en.lean +326, FORMAL_STATUS.md +3 : le périmètre de la brique seule, aucun commit de main rejoué.

Mergeabilité — git merge-tree --write-tree origin/main 62457966bb rend un arbre sans conflit (base de rejeu = 90b1faa7d8 = origin/main courant). Le mergeStateStatus: DIRTY affiché par GitHub est un lag de recalcul après le force-push + le changement de base, pas un conflit.

Tête : 62457966bb.

[github-actions]

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR car elle est en conflit avec main (mergeable_state = dirty). Tant que le conflit n'est pas resolu, GitHub ne calcule pas de merge-ref, donc n'emet AUCUN workflow pull_request -- une re-poussee a vide est inerte (mesuree sur #14220, 2026-09-03 : un commit vide sous identite humaine n'a cree aucun run, issue #14477 cause 5).

• Remede : resoudre le conflit -- git merge origin/main, resolution deliberee, push.
• Ne pas depenser un commit vide : il ne sera pas lu tant que la PR reste dirty.

Cause mesuree : mergeable_state=dirty (PR en conflit avec main)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19084
head: bbc280b
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 657ad35622b2683c7758e61a5ca47c4d8c6f5c7d305defbf1865432859ec43e9
diff-files: 3
diff-additions: 641
diff-deletions: 15
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 19084
organ-rc: 0
[/ADJOINT PREFLIGHT]

[jsboige]

Build local lake build — lake discrepancy_lean (relevé pour la pile Komlos, mission ai-01)

• tete compilee : bbc280be9a82b19e7afdbaaf4ab1352aa14a2cd7 — aujourd'hui MERGED
• toolchain : leanprover/lean4:v4.33.0
• commande : cd MyIA.AI.Notebooks/Search/discrepancy_lean && lake build (WSL Ubuntu, cache Mathlib partage)
• resultat : Build completed successfully (8754 jobs). — exit 0, essai 1 du premier coup, 0 ligne error: dans le log
• fenetre : 2026-10-09T11:01:16Z -> 14:05:51Z

Contexte : ce build est le premier de la pile Komlos (il a servi d'echauffement du cache Mathlib partage pour les quatre builds suivants). Poste ici comme enregistrement, la PR etant deja mergee.