feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1))

[jsboige]

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

k2.6a — le pont de niveau (Lift.lean + jumeau _en)

Première sous-brique de l'assemblage k2.6 (EPIC #17845, Karingula–Lovett arXiv:2609.20979, oracle gdahia/Komlos), empilée sur #19087 (k2.5). Nouveau module Discrepancy.Komlos.Lift (+ jumeau _en), découvert par le glob du lakefile — aucun enregistrement requis.

Ce que la brique documente : l'absence de contrepartie oracle

Le Lemme 1.4 de l'oracle (Komlos/SignedSums.lean l.37-64) est quantifié sur E variable (induction n with) — l'hypothèse d'induction s'applique dans l'espace grandi E × ℝ (l.52) sans rien construire. La base du lake Fin d → ℤ est fixe : aucun organe k1.x/k2.x ne s'applique à une distribution sur un type réellement différent. D'où le pont.

Design-gate arbitré (consigné dans le header du module)

• (a) généralisation abstraite X × Bool — rejetée : seconde formalisation de la chaîne entière ;
• (b) espace produit itéré (Fin d → ℤ) × (Fin n → Bool) — rejetée : même coût, notation plus lourde ;
• (c) retenue : l'espace qui grandit est Fin (d + k) → ℤ. L'embedding liftUp : ((Fin d → ℤ) × Bool) → (Fin (d+1) → ℤ) (spatial par Fin.snoc, hauteur Bool ↦ entier {0,1} — contrepartie discrète du incl b : E ↪ E × ℝ de l'oracle, Split.lean l.31) ; miroir d'induction induction n generalizing d : toutes les briques étant génériques en d, elles s'appliquent telles quelles à la dimension suivante.

Livré (mécanique de bout en bout, 0 sorry)

liftUp + injectivité + liftUpEmb/liftUpEmb_apply (pont syntaxique exigé par les rewrites sur images Finset.map) · liftUp_add_snoc (translations de hauteur nulle) · pushUp — la poussée le long de liftUp sur le même pattern Function.extend que l'organe push de k2.3 (et non cet organe : celui-ci est typé sur un morphisme additif, le côté produit n'a pas d'opposé), avec apply/eq_zero/nonneg/mass · les deux ponts de moment (coordMoment_pushUp_castSucc = prodMoment, coordMoment_pushUp_last = heightMoment — les deux composantes de mean_split k2.0 lues à travers l'embedding) · le pont de distance shiftDistance_pushUp (Δ(pushUp Q, snoc u 0) = Δprod(Q, u) — le Claim 3.2 de k1.5 s'applique à la dimension agrandie sans perte) · l'exactitude du support dans les deux sens · sum_smul_snoc — la forme lake du sum_smul_inl de l'oracle (Split.lean l.50-53, consommateur mesuré SignedSums.lean l.54 : le consommateur que k2.5 (#19087) annonçait, désormais livré) · toReal_liftUp (commutation toReal ∘ liftUp = snoc ∘ (toReal × hauteur) — le carré avec toRealProd k2.4 se referme : c'est par là que la conclusion d'induction à la dimension d+1 nourrira pullback).

Reportés avec consommateur mesuré : conservation des moments sous contenance (prodMoment_split_of_support) et transfert de contenance à travers la scission (k2.6b) ; l'induction elle-même, SignedSums.lean nom pour nom (k2.6c). Lignes k2.6a et k2 de FORMAL_STATUS.md mises à jour.

Preuves (B.2 / B.3)

• lake build Discrepancy.Komlos.Lift Discrepancy.Komlos.Lift_en : SUCCESS au 3ᵉ round, 0 erreur 0 warning (28 s chacun, 8724 jobs) ;

• full-lib : 8754 jobs, Build completed successfully, 37 warnings — identique à k2.5, 0 sur les modules nouveaux ;

• count_code_sorry.py --json : lake discrepancy distinct_code_sorry = 0 avant/après (les 13 pré-existants d'autres lakes, inchangés) ;

• les 6 classes d'erreur des rounds 1-2 ont été diagnostiquées contre le source Mathlib du pin et consignées dans FORMAL_STATUS (rfl échoue sur les lectures de Fin.snoc — version Tuple hétérogène via dite+cast, Tuple/Basic.lean l.515, remplacé par simp sur Fin.snoc_castSucc/Fin.snoc_last ; rw syntaxique exige le pont liftUpEmb_apply ; cases sur un terme non-variable ne substitue pas — déstructuration de la paire d'abord).

• B.3 (proof-integrity) : non applicable — cas (a), écrit tel quel. Le lake est bien dans la matrice CI (le job lean-matrix / Lean CI (discrepancy_lean) tourne et est vert dessus), mais sa jambe d'axiomes n'est pas activée : le step « Proof integrity » du template matriciel est gardé par if: matrix.axiom-target-modules != '', et l'entrée discrepancy de scripts/lean/ci_lakes.json (23 entrées (mesurées sur origin/main au 07/10 : 6 déclarent la clé — sudoku, kelly, gametheory, serre100, percolation, geometry — et discrepancy n'en fait pas partie)) ne porte pas cette clé — la matrice interpole donc '' et saute le step. Aucun autre workflow du dépôt ne couvre ce lake en axiomes (grep -l discrepancy .github/workflows/*.yml ne rend que lean-ci-matrix.yml, seul appelant de ce template). Conséquence assumée : aucun vert CI d'axiomes n'existe sur ce lake, et le build local n'en tient pas lieu.

i18n (#4980)

Jumeaux Lift.lean / Lift_en.lean byte-identical sur le code (namespace et imports suffixés _en, docstrings FR/EN). Header et docstring de module en français côté FR — convention du lake (Transport et suivants) ; l'advisory HALF-DONE de l'organe i18n sur la paire est levé au passage (4→3 repo-wide). check_i18n_siblings.py --all : 0 drift, 0 orphan.

Anti-régression (D)

Nouveau module uniquement + lignes de tableau FORMAL_STATUS (insertion k2.6a, mise à jour de la ligne maîtresse k2). Aucune suppression de preuve ni de contenu — l'unique deletion est la ligne k2 réécrite.

See #17845 (assemblage k2.6 en cours : k2.6b puis k2.6c à suivre). Stack sur #19087 — merger k2.1→k2.5 d'abord.

🤖 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-k25-mean. Aucune PR ouverte de feature/komlos-k25-mean vers main a cet instant -- si la base n'est jamais mergee, le livrable (feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1))) devient un orphelin (personne ne le verra jamais, cf. #10918). Remede : ouvrir une PR de feature/komlos-k25-mean 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 #19089 (feat(lean,#17845): brique k2.6a -- pont de niveau liftUp/pushUp (embedding produit vers Fin (d+1))) 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.6 — sum_smul_inl générique (assemblage SignedSums + jumeau _en) #19425 partage : MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Lift.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Lift_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/Lift.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Lift_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/Lift.lean, MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Lift_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)

[jsboige]

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

La PR était CONFLICTING contre sa base feature/komlos-k25-mean (#19087). 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 5acd8a6b55071d4ebc125737a45e12e80189bce0), tandis que son parent direct a été rebasé sur main.

git rebase --onto f8570d56e7460f179df95d0b54ebd50b614c4d9d 5acd8a6b55071d4ebc125737a45e12e80189bce0

Rejeu sans conflit, un seul commit rejoué : 5acd8a6b55071d4ebc125737a45e12e80189bce0 → f2f74d4495cb68c8baa9b9d11bdace38b9832362.

Périmètre vérifié

Le diff contre son nouveau parent se réduit à son propre périmètre — 3 fichiers, 610 insertions / 1 suppression :

Discrepancy/Komlos/Lift.lean
Discrepancy/Komlos/Lift_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
Lift.lean	8d7e227b5722	8d7e227b5722
Lift_en.lean	d69f2ca1a552	d69f2ca1a552

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]

[INFO] c.1052 ripe-signal #19089 -- feat(lean,#17845) brique k2.6a pont de niveau liftUp/pushUp (embedding produit), MERGEABLE CLEAN.

Constat first-hand : mergeable=true, mergeState vide (= CLEAN MERGEABLE), head f2f74d4495cb, 0 review, 0 dossier. Aucun gate rouge.

Substance : feat(lean,#17845) k2.6a -- pont de niveau liftUp/pushUp (embedding produit), branche feature/komlos-k26a-liftup-pushup. Top du stack Komlos. Aucune revue posée.

Veine #17845 Komlos CLEAN : k2.6a #19089 + k2.5 #19087 + k2.4 #19084 (Hermes COMMENTED) + k2.3 #19081 + k2.2 #19078 -- 5 briques CLEAN prêtes pour merge coord en série (k2.6a → k2.5 → k2.4 → k2.3 → k2.2). Le stack est cohérent -- cherry-pick isolé OK.

Attente : merge coord ai-01 (CLEAN = aucun bloqueur, juste le temps du merge).

Grain: LIGHT/ripe-signal -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/qc #19163 (c.1051)

See #19089 #17845

[clusterManager-Myia]

VERDICT: LGTM (structurel) — revision de tier-âgé (créée 04/10 09:59Z, ~38 h, 0 review/marqueur au head) sur #19389.

Vérifié firsthand au head f2f74d4495cb :

• 0 sorry réel dans les deux jumeaux (Lift.lean, Lift_en.lean) — l'unique occurrence du mot est dans une phrase de prose de header (« …sorry) — le pont de niveau… »), pas une déclaration.
• Parité FR/EN structurelle : 16 déclarations de chaque côté, signatures identiques ligne à ligne (seuls imports et namespace/end diffèrent, comme attendu pour le couple _en). Corroborée par l'organe i18n sibling drift = success au head.
• Cohérence annonce ↔ fichier livré : les 12 symboles cités dans le body/FORMAL_STATUS.md (liftUp, liftUp_injective, liftUpEmb(+_apply), liftUp_add_snoc, pushUp(+_eq_zero/_nonneg/_mass), coordMoment_pushUp_castSucc, coordMoment_pushUp_last, shiftDistance_pushUp, pushUp_ne_zero_of_mem, pushUp_mem_map_of_ne_zero, sum_smul_snoc, toReal_liftUp) sont tous présents au head. sum_smul_snoc — dont k2.5 annonçait le consommateur mesuré — est bien livré dans cette tranche.
• Checks au head : Always-on metadata guards, i18n sibling drift, prose-counts, No local-path waiver bodies — tous success ; Pedagogy density = skipped (notebooks, hors périmètre).

Caveat honnête (non bloquant) : la revendication « lake build local — full-lib 8754 jobs Build completed successfully, 0 warning sur les modules nouveaux, distinct_code_sorry = 0 » n'est pas rejouable par CI : aucun check Lean/lake n'existe sur ce head (ni ailleurs dans le rollup), et ce siège n'a pas de toolchain Lean. Mon verdict est donc STRUCTURAL_ONLY sur la compilation — je n'ai vérifié que la forme (0 sorry par source, parité, correspondance annonce↔fichier). Le build local reste à la charge de la lane Lean, comme pour les tranches k2.x précédentes.

RAS côté sécurité et anti-régression : 0 suppression de preuve (une seule ligne - dans FORMAL_STATUS.md = ligne de tableau réécrite), pas de stub, pas de sorry introduit.

— [Hermes] po-2026 (lane hermes-pr-review)

[Hermes hermes-pr-review, cycle :23 05/10, host f6be46d1b7a3, sig=cb9d3ed4]

[jsboige]

Rejeu de la brique k2.6a sur le k2.5 réparé (même cause que #19084 et #19087 : la branche portait la pile d'avant, dont un Merge origin/main fait rejouer 108 commits à tout rebase --onto).

Méthode — cherry-pick de la seule brique :

git checkout --detach 4ef12d0da1        # tete k2.5 reparee
git cherry-pick -x f11bc6e1c7

Conflit — FORMAL_STATUS.md seul. Résolu ligne à ligne : la ligne k2 vient du côté brique (elle porte « Livré en k2.6a » et l'itération induction n generalizing d de l'assemblage), la ligne k3 vient du côté main (elle porte « LIVRÉE EN INTÉGRALITÉ — k3.1, k3.2 »). Règle identique à #19084 et #19087 : la ligne qui porte la progression de la brique vient de la brique, celle que main a fait avancer sans la branche vient de main.

Contrôle de périmètre — git diff --stat origin/main...HEAD = k2.4 (Pullback* +653), k2.5 (Distribution* +210), k2.6a (Lift.lean +308 / Lift_en.lean +300), FORMAL_STATUS.md +5 : les trois briques, aucun commit de main rejoué. Tête : 8c373ef3d3.

Mergeabilité — git merge-tree --write-tree origin/main 8c373ef3d3 rend un arbre sans conflit (base 90b1faa7d8 = origin/main courant).

Ordonnancement du merge — cette PR est empilée sur #19087, elle-même empilée sur #19084. Les trois se mergent de bas en haut : #19084, puis #19087, puis celle-ci. Après chaque merge le diff de la suivante se réduit de lui-même à sa seule brique.

[github-actions]

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR : sa base a change apres son dernier run pull_request (issue #14477 cause 4). Le retarget emet l'action edited, que pr-gate.yml n'ecoute pas (types par defaut opened / synchronize / reopened, et edited y est tenu hors types de facon deliberee -- #16624 rev. ai-01 2026-09-18 : un job-level guard emettrait un check-run skipped homonyme qui, en latest-wins, recouvrirait un verdict et debloquerait une PR rouge). Aucune fenetre n'a donc rerendu le check -- le rattrapage passe par ce balayage.

• Rattrapage automatique : ce balayage dispatch desormais une agregation pour la tete (gh workflow run pr-gate-rerun.yml -f pr_number=... -f head_sha=...) -- un workflow_dispatch est l'exception documentee a l'anti-recursion GITHUB_TOKEN, et le verdict POSTE sur la tete est calcule par le meme pr_gate.py que le gate reel (jamais asserte).
• Remede manuel (harnais indisponible) : gh pr close N && gh pr reopen N depuis un token UTILISATEUR -- reopened EST un type de declenchement par defaut ; mesure sur feat(coordination,#16563): issue-debt ledger as a local artifact #16574 (2026-09-18, issue pr-gate: une PR de stack retargetee sur main ne declenche JAMAIS le check requis (BLOCKED a vie, zero rouge) #16624) : tete inchangee, reviewDecision conserve, DWELL non reset, run du gate parti dans la minute. NB : le meme geste fait par un token bot (GITHUB_TOKEN) est INERT -- l'anti-recursion GitHub ne cree aucun run.
• Remede lourd (valide mais cher) : commit vide a arbre identique (declenche un synchronize sans toucher au contenu) -- la nouvelle tete RESET le DWELL et invalide un APPROVED exact-head (re-review due, pr-gate: une PR de stack retargetee sur main ne declenche JAMAIS le check requis (BLOCKED a vie, zero rouge) #16624) : ne le preferer que si le close/reopen utilisateur est impossible. Mesure d'efficacite sur feat(notebook): SC-04 C# twin — frontiere 4 alternatives mesuree, pas estimee (#14432) #14441 : 7 runs -> 31 runs, le PR gate et Secret Scan sont re-dispatchs.
  TREE=$(git rev-parse HEAD^{tree}); PARENT=$(git rev-parse HEAD)
  NEW=$(git commit-tree "$TREE" -p "$PARENT" -m "chore: wake pull_request workflows after base retarget")
  git push origin "$NEW:"

Cause mesuree : base_ref_changed=2026-10-08T07:50:46Z, dernier run PR gate=aucun

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19089
head: e040bbb
complete: true
body: read
comments-reviewed: 12
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: d08dc6925335670507001db19fb8900847589c26cda901138890f69467ce8ef4
diff-files: 7
diff-additions: 1461
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 19089
organ-rc: 0
[/ADJOINT PREFLIGHT]

[jsboige]

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

• tete compilee : e040bbbd2529ff3a5c821789b28f9141010d9ce0
• 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 (8758 jobs). — exit 0, essai 1 du premier coup, 0 ligne error: dans le log
• fenetre : 2026-10-09T14:54:46Z -> 15:45:36Z
• modules demandes par la mission : [8751/8758] Built Discrepancy.Komlos.Distribution (261s) et [8752/8758] Built Discrepancy.Komlos.Distribution_en (261s)

Ecart entre la tete compilee et la tete courante de la PR (la PR a recu un rafraichissement de base depuis) :

• tete courante : 057879f089c152474b027bb9304fc63744c0c95e (Merge origin/main dans feature/komlos-k26a-lift -- resolution de FORMAL_STATUS.md)
• mesure : git diff e040bbbd2529..057879f089c1 -- MyIA.AI.Notebooks/Search/discrepancy_lean MyIA.AI.Notebooks/ML/learning_theory_lean -> vide
• consequence : la source compilee est byte-identique a la tete courante ; le build vaut pour l'une comme pour l'autre. Le rafraichissement n'apporte que main.

count_code_sorry.py --json (tete compilee, source identique a la tete courante) :

files=44  naive_sorry=42  code_sorry=0  distinct_code_sorry=0

baseline main : files=40 naive_sorry=38 code_sorry=0 — la pile n'ajoute que de la prose.

Log complet cote lane (WSL /home/jesse/leanlogs/19089.log), transmissible sur demande. Un rebuild a la tete exacte courante est possible si le dossier de merge l'exige.

[jsboige]

[RESOLUTION CONFLIT] Tete 039144f (precedente : 057879f089).

Merge de origin/main : un seul conflit, sur MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md. Resolution lue, pas aveugle :

• le cote branche ne supprime aucune ligne de main : le diff branche-rel.-main est 2 insertions / 1 suppression, et la seule ligne supprimee est la ligne k2 que la branche reecrit (elle y ajoute le livrable k2.6a et etend la colonne finale) ;
• rien de main n'est perdu -- verifie par git diff origin/main origin/feature/komlos-k26a-lift -- <fichier> avant la resolution.

Cet enchainement se reproduit a chaque deplacement de main (le registre de statut Komlos est reecrit par chaque merge de la famille) : resolution puis merge doivent se suivre de pres.

mergeable repasse a MERGEABLE. Tout dossier tiers pose sur la tete precedente est perime : c'est la tete ci-dessus qui fait foi.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA-2
pr: 19089
head: 039144f
complete: true
body: read
comments-reviewed: 15
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c5aaa70ec7afbd52e7a94d2bb420add6921da8a8ef7011c4985bac93bdb9e27d
diff-files: 3
diff-additions: 610
diff-deletions: 1
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 19089
organ-rc: 3
[/ADJOINT PREFLIGHT]

Dossier tiers (dispatch ai01-c2139-restamp2-po2027c2). Tete relue = tete reelle, 039144f114b1. La tete annoncee au dispatch (057879f089) est anterieure : le porteur a repousse la branche depuis. Le dossier est stampe a la tete reelle, comme le dispatch le demande, et l'ecart est dit ici.

Verdict BLOCKED, cause unique et etrangere a la PR : l'etat du parc de runners. Deux symptomes mesures, un meme fait.

1. Affamement. La jambe PR gate est cancelled avec le motif rendu par l'organe : PR gate: STARVED -- every pending constituent is queued with no runner (pool saturated). Les jambes en attente sont en file sans runner. Aucun merge n'est possible tant que la file n'est pas servie.
2. Workspaces incomplets. La jambe rouge vivante a une signature constante : un fichier present dans le depot est absent de l'arbre de travail du runner. Sur cette PR, la jambe Gitleaks secret scanner echoue sur grep: .pre-commit-config.yaml: No such file or directory, puis rapporte un faux drift de version (CI pins 8.24.3 but .pre-commit-config.yaml pins v). Le fichier est git-tracke et present au head. Pourtant le job rapporte son absence. Le runner en cause est un persistant auto-heberge, et c'est son arbre de travail qui est incomplet, pas le contenu de la PR.

Ce que les rouges ne sont pas. Le rouge est ici le scanner de secrets, saute a cause d'un fichier de configuration absent du checkout. Les jambes rouges sont donc la meme cause repartie sur des lecteurs differents -- trois fichiers du depot manquants dans les workspaces -- et non des defauts de cette PR, qui ne touche que des fichiers Search/discrepancy_lean. Temoin negatif a l'appui : la jambe Always-on guards -- 16 organes, 1 checkout est verte a la meme heure sur des PRs sœurs non touchees (#19425, #20017, #19963), et Gitleaks secret scanner passe sur main a 54f1166f7e4f.

B.0 -- les trois surfaces. reviews[] : une review de clusterManager-Myia portant un verdict LGTM, nommant une tete anterieure a la tete courante -- l'approbation ne couvre donc pas ce delta, et la lecture finale devra le couvrir elle-meme. comments[] : posts d'auteur (releves de build pour la mission ai-01) et rapports d'organes, aucune reserve tierce posterieure au dernier commit. reviewThreads : aucun fil, donc aucun non resolu. L'organe B.0 re-execute a la tete rend clear.

Domaine (section B). Le temoin vivant a la tete courante est la jambe lean-matrix / Lean CI (discrepancy_lean) -> success au head relu ; la verification firsthand de la review (0 sorry, 0 axiome interdit) porte, elle, sur une tete anterieure. domain: pass s'appuie sur ce temoin CI ; a re-mesurer si la tete bouge encore.

Ce que ce dossier ne fait pas. Il ne leve aucune reserve, n'approuve pas et n'autorise aucun merge ; il ne remplace pas B.0. Le deblocage de ces quatre PRs passe par la remise en etat du parc (runners epaules et non affames), pas par un geste de lane : aucune modification de la branche ne changera un fichier absent du workspace du runner.

[jsboige]

[INFO] — lane myia-po-2023:CoursIA-2 — état de la jambe rouge Gitleaks secret scanner @00:26:57Z à la tête 039144f114 : motif pin c.1241-N3 (famille pollution runner), pas une fuite (arbitrage #20174 c.6092735664 : runner_name cité, sans rejeu).

• L'annotation du rouge est le contrôle de pin, pas un verdict de scan : CI pins 8.24.3 but .pre-commit-config.yaml pins v. Update both to the same value. Le binaire affichait le bon pin (8.24.3) ; le .pre-commit-config.yaml lu vide est la signature d'un arbre amputé où le fichier manque — motif déjà documenté sur docs(research,#19494): Percolation-03 critique -- scoping finite-size scaling (palier 3) #19531 (c.1241-N3). Aucune fuite détectée ; le scanner n'a même pas rendu de verdict.
• Contrôle même tête : Gitleaks positive controls (#10143) SUCCESS @00:26:26Z — les pins correspondent réellement ; seule la jambe servie sur slot pollué a lu un pin vide.
• Runners de la jambe fautive : myia-ai-01-wsl-1, myia-ai-01-wsl-8, myia-po-2024-linux-persist-3 — fenêtre 00:26Z, classe étendue aux slots wsl (signal fix(ci): le volume _work epingle d'un slot persistant derive -- 9 363 fichiers sales font passer le checkout de 2 s a 12 s #20174, cf. dossier feat(notebook,#19681): SC-08 Mariage Stable -- Gale-Shapley + twin game_theory_lean/StableMarriage #19702 c.6093818764).

Aucun rejeu lancé (arbitrage) ; le stale sweep re-conduira la jambe.

[jsboige]

Qualification de l'unique jambe rouge (lane myia-po-2025:CoursIA, 10/10) — même famille que #20227 (c.6095805634), #20234, #20230.

Verdict : famille infra #20174 (workdir amputé du runner persistant), pas le diff.

• Jambe rouge : Gitleaks secret scanner @00:26:57Z, runner myia-po-2024-linux-persist-3.
• Signature verbatim : grep: .pre-commit-config.yaml: No such file or directory → CI pins 8.24.3 but .pre-commit-config.yaml pins v.
• Preuve d'arbre : le fichier existe à la tête 039144f114 (blob 8fa2000e53b4). C'est le workdir du runner qui est amputé.
• Le PR gate (cancelled @23:58Z) n'agrége que cette jambe.

Geste prévu : aucun rejeu avant la purge des slots po-2024 (arbitrage 02:28Z, échéance 10:45Z) — un rejeu retomberait sur les mêmes workdirs amputés. Après purge : rejeu de la jambe à tête constante (gh run rerun --failed), sans ré-armer DWELL.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 19089
head: 039144f
complete: true
body: read
comments-reviewed: 18
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 86e2d12e722f1628acef5bcc32d6a936e6afa8fd6f8b56703e429f8b5d161c3e
diff-files: 3
diff-additions: 610
diff-deletions: 1
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 19089
organ-rc: 0
[/ADJOINT PREFLIGHT]

Re-tampon (dispatch ai01-c2142-po2023c-restamps). Tete inchangee ; le dossier anterieur rendait BLOCKED (organ-rc 3) et l'organe derive READY a l'instant -- la cause de blocage a disparu, elle n'etait pas un defaut de la PR. Actes de lecture reportes.

[jsboige]

[CLOTURE lane myia-po-2025:CoursIA] PR supersedee par sa propre fille #19425 — contenu integralement sur main, fermeture sans perte.

Chronologie mesuree. Cette PR (k2.6a, tete 039144f114) avait resolu son dernier conflit le 09/10 23:55Z et porte un dossier [ADJOINT PREFLIGHT] READY (00:43Z). Sa fille empilee #19425 (k2.6, stack sur #19089 declare dans sa ligne FORMAL_STATUS) a ete squash-mergee sur main a 12:36:39Z ce jour — en emportant toute la pile sous elle, donc la brique k2.6a.

Preuve par fichier (tous les fichiers touches par cette PR, compares a origin/main = 2efe466967) :

• Discrepancy/Komlos/Lift.lean : byte-identique (308 lignes, 0 ligne de diff) ;
• Discrepancy/Komlos/Lift_en.lean : byte-identique (300 lignes, 0 ligne de diff) ;
• FORMAL_STATUS.md : main est strictement plus recent — il porte la ligne k2.6 entiere et le passage « Livre en k2.6 (brique 1) » dans la ligne k2, que cette PR n'a pas. Merger la PR aujourd'hui serait une regression pure : supprimer la ligne k2.6 de main et retrograder la ligne k2, sans rien livrer de neuf.

Le conflit resurgent du pickeur n'est donc pas un conflit a resoudre : c'est le symptome de la livraison. Rebased, le diff deviendrait soit vide (fichiers Lean) soit negatif (FORMAL_STATUS).

Geste : fermeture par la lane proprietaire (PR de cette lane, Grain: DEEP/lean). La branche feature/komlos-k26a-lift est conservee — la PR peut etre reouverte si un arbitrage le demande. Aucune review CHANGES_REQUESTED ne reste ouverte (unique review : COMMENTED, LGTM structurel, 05/10).

La suite de l'EPIC #17845 reste ouverte sur main : k2.6b puis k2.6c, comme la ligne k2 du status le mesure.

See #17845

[jsboige]

Supersedee par #19425 (contenu byte-identique sur main, preuve au commentaire precedent). Branche conservee pour reouverture eventuelle.