fix(notebook,#17357): Lean-15 -- 4 constats markdown + 3 faux positifs mesures

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2027:CoursIA-2 — prev: MED/notebook-lean #20163

Contexte

Suite de la file Lean dispatchée par ai-01 sur #17357 (partition Hermes). Carnet
Lean-15-Grothendieck-Tribute.ipynb, ses 7 constats revérifiés sur main avant
toute correction, selon audit-reassessment.md.

Audit source : c.5842457576.

Livraison initiale markdown-only (4 insertions / 4 suppressions, 0 cellule de code),
puis commit de suivi 9c24c9bd6cfa qui livre le résiduel F2/F3 côté code — d'où
ré-exécution complète 12/12 cellules de code, exec_count 1..12, 0 erreur (C.2).
Diff total actuel : 361 insertions / 599 suppressions sur 3 fichiers (l'écart vient des
sorties recalées par la ré-exécution et des blocs metadata.papermill retirés — ratchet
BLOCK_REMOVED, 0 régression).

Constats CONFIRMÉS et corrigés (4)

F1 — « les trois exercices suivants » alors qu'il y en a quatre

La cellule 4c39dc61 (§ 8) annonce trois exercices. La section en porte quatre :
les exercices 1-3 y sont décrits, et ### Exercice 4 : le lemme de Yoneda (e2d7f8a6)
suit dans la même section. « trois » → « quatre ».

F2 — l'indice de l'exercice 4 donne un identifiant faux

La cellule e2d7f8a6 écrit : « Le lemme lui-même vit dans CategoryTheory.Yoneda.yonedaLemma ».

Mesure sur le source Mathlib du lake :

Ce que le carnet disait	Ce que le dépôt porte
CategoryTheory.Yoneda.yonedaLemma	def yonedaLemma : yonedaPairing C ≅ yonedaEvaluation C, ligne 837 de Mathlib/CategoryTheory/Yoneda.lean

Le namespace Yoneda se ferme ligne 177 : la déclaration de la ligne 837 est hors de
ce namespace, et le nom réel est CategoryTheory.yonedaLemma. Le carnet se contredisait
d'ailleurs lui-même — l'interp de la section 1 (lean13-interp-functor) donnait, elle, le
nom correct. L'indice est corrigé, avec le fichier et le namespace nommés.

F3 — « affichent » une signature que l'extrait affiché ne porte pas

L'interp lean13-interp-morphisms affirmait : « Les trois predicats Lean affichent une
signature uniforme ». La cellule ancrée lean13-check-morphisms exécute
display_lean_module('MathlibMap', highlight=[8, 9, 10]) — et les lignes 8-10 du module
sont, dans la sortie committée, du texte de commentaire (de Grothendieck. Chaque #check vérifie…), pas des signatures. Le module affiché ne contient ni Etale, ni
Smooth, ni IsSeparated.

Le verbe est corrigé (« Mathlib déclare ces trois prédicats… ») : la phrase n'affirme plus
que l'écran les montre. Le highlight est réparé côté module en commit de suivi
(9c24c9bd6cfa) : MathlibMap.lean porte désormais les trois #check des propriétés
locales (lignes 100-102, imports Morphisms.Etale/Smooth/Separated ajoutés) et le
highlight de lean13-check-morphisms pointe sur ces lignes réelles — le rendu montre
les >>> sur les #check. Compilation mesurée : lake env lean Grothendieck/MathlibMap.lean
rc=0, toutes les signatures existantes intactes ; sibling EN byte-identique sur les
statements (check_i18n_siblings OK 1/1).

F6 — des « stubs » qui n'en sont pas

La cellule 4c39dc61 annonçait des exercices « suivant la convention C.1 (stub sans
raise NotImplementedError) ». Mesure sur les 4 cellules d'exercice (6e9d167b,
3091aa4c, 550858c3, 8aac9b8d) : aucun stub, aucun TODO, aucun sorry. Chacune
fournit un snippet complet exécuté par run_lean, suivi d'un print("Lecture : …") qui
donne déjà l'interprétation — l'apprenant n'a rien à compléter.

La phrase est réécrite pour dire ce que les cellules sont : des explorations guidées
complètes. La convention C.1 reste satisfaite au sens fort (aucune erreur volontaire), mais
la qualification « stub » était fausse. Convertir ces cellules en vrais stubs reste une
décision pédagogique distincte, nommée en fin de PR (résiduel 3).

Constats FALSE POSITIVE (3, mesurés, aucune modification)

F4 — CategoryTheory.yonedaLemma est un nom Mathlib valide

L'audit classe en stale-claim la phrase « Dans Mathlib, il s'enonce
CategoryTheory.yonedaLemma », au motif que l'identifiant a 0 occurrence dans la sortie
ancrée. Mais la phrase est un énoncé sur Mathlib, pas sur la sortie affichée — et il est
exact : def yonedaLemma existe (Yoneda.lean, l.837, namespace CategoryTheory).
Confondre « absent de l'écran » et « faux » est précisément le faux positif que
audit-reassessment.md demande d'écarter.

F5 — les quatre topologies sont bien dans le même fichier

L'audit écrit que atomic a 0 occurrence et que « le 4e item de la liste annoncée n'existe
pas ». Le carnet affirme que Mathlib fournit ces topologies dans le même fichier —
mesure :

Topologie	Mathlib/CategoryTheory/Sites/Grothendieck.lean
trivial	def trivial — ligne 240
discrete	def discrete — ligne 254
dense	def dense — ligne 376
atomic	def atomic (hro : RightOreCondition C) — ligne 408

Les quatre vivent dans le même fichier, comme le carnet l'écrit. L'énoncé est exact.

F7 — un prérequis déclaré n'est pas un énoncé faux

Le constat difficulty-jump reproche à la cellule lean13-intro-bio de déclarer « notions
de base de théorie des catégories » comme prérequis sans que la série amont les construise.
La mesure de l'audit est exacte ; mais la cellule déclare ce prérequis — c'est la
fonction d'une section « Prérequis » — et n'affirme nulle part que la série le couvre.
Aucun énoncé faux n'est identifiable : le constat déplace un jugement pédagogique
(la marche est haute) dans la classe stale-claim, où il n'est pas confirmable.

Verdict

Reassessed by myia-po-2027:CoursIA-2: CONFIRMED (F1, F2, F3, F6) ; FALSE POSITIVE (F4, F5, F7).

4 constats traités, 3 faux positifs mesurés sur ce carnet — 0 constat non traité.
Les résiduels F2/F3 côté code, d'abord reportés (environnement Lean en réparation), ont
été livrés en commit de suivi 9c24c9bd6cfa avec ré-exécution complète.

Résiduel — F2/F3 livrés en commit de suivi (9c24c9bd6cfa)

1. F3 côté module — LIVRÉ : MathlibMap.lean porte les #check des propriétés
   locales (lignes 100-102) et le highlight de lean13-check-morphisms pointe sur ces
   lignes au lieu de l'en-tête de commentaire.
2. F2 côté code — LIVRÉ : #check CategoryTheory.yonedaLemma ajouté au snippet de
   8aac9b8d — la signature résout dans la sortie committée.
3. F6 — OUVERT (décision pédagogique) : convertir ces explorations guidées en vrais
   stubs reste une décision distincte, hors du périmètre de ce correctif d'audit.

Ré-exécution complète 12/12 cellules de code, exec_count 1..12, 0 erreur ; blocs
metadata.papermill retirés avant commit (ratchet : BLOCK_REMOVED, 0 régression).

See #17357 — livraison partielle, l'issue reste ouverte.

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359) — résolue

La collision de chemins signalée sur #20164 n'existe plus au passage du 2026-10-10T02:53Z : aucune autre PR ouverte ne partage désormais de chemin de fichier avec elle. Note laissée en place de l'avertissement (retraction non destructive).

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	11.6s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	9.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	18.0s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.7s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.3s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Grain tag obligatoire (#10045, bloquant).

unknown.

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

[github-actions]

<mot-clé fermant> #N où N est une PR -- bloquant (#10101).

unknown

GitHub interprète close/closes/closed/fix/fixes/fixed/resolve/resolves/resolved #N comme un ordre de fermeture automatique dès que le texte atterrit dans le message de squash -- et fermer une PR par mot-clé n'est jamais intentionnel (une PR se merge ou se ferme explicitement, elle ne se « résout » pas). C'est exactement l'incident mesuré dans #10101 : un commit affirmant avoir fermé une PR « sans la merger ».

Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Closes #<issue> est intentionnel (catalog-pr-hygiene HARD 4) et passe silencieusement ; seul un #N qui résout en PR déclenche ce gate.

Pour passer ce gate :

• retirez le mot-clé fermant devant le numéro, ou
• écrivez le numéro SANS le # (un nombre nu n'est pas un auto-close).

[github-actions]

G-VAR-3 : deux grains LIGHT du meme genre consecutifs -- bloquant (#11170).

unknown

Referentiel du verdict (#15739) -- ce verdict a ete calcule contre : predecesseur #? (?, source ?), sequence de merges arretee au n/a. Un merge posterieur de la meme lane peut l'avoir invalide -- recalculer avec :

python scripts/ci/variation_adjacency_guard.py --pr-number 20164

variation-protocol.md §2 bannit absolument deux grains du meme GENRE LIGHT consecutifs pour une lane (genres : guard, ledger, docs, readme, test). Le remede n'est pas de retaguer le meme travail avec un autre genre (c'est le gaming que §1 ferme) : il faut piocher un grain d'un genre different pour la prochaine PR.

Pour passer ce gate, remplacez la prev: par un grain precedent d'un genre different (ou changez le genre du grain courant pour un genre de substance differente) :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<genre-different> #<PR>

[github-actions]

Collision de lane sur une reference fermante (#10223).

unknown

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

• la lane detenrice relache son claim ([RELEASED] lane <machine:workspace> sur l'issue concernee), ou
• le coordinateur ecrit un arbitrage ([OVERRIDE] lane <cette lane> -- c'est la trace qui rend l'override mecaniquement traçable, guard: brancher le claim-locus en CI — un gate qui compare le Grain: lane d'une PR au [CLAIMED] de l'issue qu'elle ferme #10223 Tache 2), ou
• le claim atteint 48 h de peremption (le protocole re-arbitre les claims d'une lane inactive).

Voir #10223 et lane-claim-protocol.md.

[github-actions]

Artefact de resultats au-dela de la barre de 512 Ko -- bloquant (#15890).

unknown

Pour passer ce gate :

• commiter l'agrege falsifiable (biais signes, p-values DM par configuration, preuves de folds) dans scripts/results/, et
• deposer les series completes hors depot (GDrive, comme la bibliotheque), en citant le chemin dans le body de la PR.

Politique complete : .claude/rules/results-artifact-policy.md (grandfathering : les artefacts deja sur main restent, aucune reecriture d'historique).

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[jsboige]

Residuel Lean-15 livre -- tete 9c24c9bd6cfa.

Volet 1 — MathlibMap.lean porte les proprietes locales des morphismes (constat F3 de la revue) :

• 3 imports ajoutes (Mathlib.AlgebraicGeometry.Morphisms.Etale/Smooth/Separated) + nouvelle section « Geometrie algebrique : proprietes locales des morphismes » avant « Ce que Mathlib n'a PAS ENCORE » -- lignes 100-102 :

#check @AlgebraicGeometry.Etale         -- morphisme etale
#check @AlgebraicGeometry.Smooth        -- morphisme lisse
#check @AlgebraicGeometry.IsSeparated   -- morphisme separe

• Compilation mesuree : lake env lean Grothendieck/MathlibMap.lean (WSL, cache Mathlib repare au pin db584cd6d4) -- rc=0, les trois signatures resolvent (@Etale, @Smooth, @IsSeparated : {X Y : Scheme} → (X ⟶ Y) → Prop) et toutes les signatures existantes du module restent intactes (topologies, IsSheaf, Presieve.IsSeparated, Scheme, Spec, Gamma, forgetToTop, forgetToLocallyRingedSpace).
• Sibling EN MathlibMap_en.lean : meme section, docstrings EN, statements byte-identiques -- organe check_i18n_siblings.py : OK 1/1, exit 0.
• Cellule lean13-check-morphisms : display_lean_module('MathlibMap', highlight=[100, 101, 102]) -- le rendu commite montre les marqueurs >>> sur les lignes reelles des trois #check (mesure dans la sortie de la cellule).

Volet 2 — #check CategoryTheory.yonedaLemma (constat F2) : ajoute dans la cellule 8aac9b8d (snippet run_lean). La sortie commitee montre la signature complete :

CategoryTheory.yonedaLemma.{v₁, u₁} (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : ...

Volet 3 -- decision F6 (stubs) : les explorations guidees restent des explorations. Les convertir en stubs serait une regression de contenu (CLAUDE.md section D : ne pas remplacer une implementation existante par un stub) -- ces cellules demontrent un moteur, elles ne sont pas des exercices a trous.

Re-execution complete : 12/12 cellules code, execution_count 1..12, 0 erreur, aucun texte d'erreur dans les sorties. Sources modifiees : exactement les 2 cellules visees (lean13-check-morphisms, 8aac9b8d) ; sorties rafraichies sur les 5 cellules dependantes.

Ratchet papermill : blocs herites (nb-level + 31 cell-level) retires avant commit -- organe local : BLOCK_REMOVED, 0 regression.

Diff : 3 fichiers, +357/-595 (le solde negatif = les blocs papermill retires, pas une perte de contenu).

See #17357

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2027:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-09) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=3 cap=2)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=0 genre=3 cap=2)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 12
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[jsboige]

Markdown claims anchored to previous output (#11435 advisory) — famille #20174, pollution cross-PR à l'échelle. Runner myia-po-2024-linux-persist-2. Aucun rejeu.

La jambe (advisory) échoue à la tête 9c24c9bd6cfa, step Run unit tests, exit 4 — et l'annotation nomme 10 fichiers étrangers à cette PR :

Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-2-Data&Features-Python.ipynb' not uptodate; will not remove from working tree.
Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-2-Data&Features.ipynb'      not uptodate; will not remove from working tree.
Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-3-Entrainement-Python.ipynb' …
Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-3-Entrainement&AutoML.ipynb' …
Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-4-Evaluation-Python.ipynb'  …
Path 'MyIA.AI.Notebooks/ML/ML.Net/ML-4-Evaluation.ipynb'         … (×10 au total)

Cette PR touche MathlibMap.lean (+ sibling) et les carnets Lean-15 — aucun fichier ML.Net. Ce sont des résidus d'un job précédent sur le même slot (série ML/ML.Net), laissés modifiés dans le work dir épinglé ; l'opération git de la jambe refuse de les retirer et le job meurt avant de produire un verdict. Même signature que l'addendum posé sur #20203 aujourd'hui (cid 6093861599, QC-Py-43 de #20212 sur persist-4) — la pollution cross-PR n'est donc pas un incident isolé mais un mode récurrent du défaut : le work dir épinglé porte à la fois des fichiers absents ET des fichiers étrangers sales, selon l'historique des jobs qu'il a servis.

Aucun rejeu (arbitrage ai-01 sur #20174, 02:28Z) : un rejeu retombe sur le même slot. Purge = po-2024.

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA-2
pr: 20164
head: 9c24c9b
complete: true
body: read
comments-reviewed: 16
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: d83bd48c6428db8f39d1ab469a6d1ffb98d4b1b9c9f3139160acf1995391f3be
diff-files: 3
diff-additions: 361
diff-deletions: 599
checks: latest-wins-green
b0: clear
scope: fail
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20164
organ-rc: 3
[/ADJOINT PREFLIGHT]

Lecture tierce a la tete 9c24c9b. Le FOND est meilleur que le body, mais le body est PERIME sur ses declarations centrales — mesure cellule par cellule contre origin/main :

• le body ecrit « Markdown uniquement : 3 cellules modifiees, 0 cellule de code touchee », « execution_count et outputs identiques », et nomme en RESIDUEL REPORTE les fixes F3 (highlight module) et F2 (#check yonedaLemma) ;
• la TETE porte l'inverse : 2 cellules code changees (lean13-check-morphisms : highlight 8-10 -> 100-102 pointant sur les nouveaux #check Etale/Smooth/IsSeparated ajoutes au module ; 8aac9b8d : #check CategoryTheory.yonedaLemma ajoute au snippet) et 5 cellules avec sorties regenerees (exec 2/3/5/8/12 conserves, sorties reelles — la sortie de 8aac9b8d montre la signature complete de CategoryTheory.yonedaLemma, preuve d'un vrai run Lean) ;
• les fichiers .lean (+12/+12 miroir FR/EN) sont des AJOUTS purs (imports + section #check) — aucune regression ;
• les corrections markdown F1/F2/F3/F6 annoncees sont bien la (« quatre », identifiant corrige, verbe corrige, « explorations guidees »).

Le travail est donc PLUS avance que declare : les residuels dits « reportes » sont faits, avec la re-execution que le body disait impossible. Mais un body qui affirme « 0 cellule code touchee » devant un diff qui en touche deux avec sorties regenerees est une declaration C.2 inversee : un reviewer fidele au body mergerait un autre diff que celui qu'il a lu.

Geste lane, leger : rafraichir le body aux valeurs de la tete (le correctif C.2 est DECLARE dans l'autre sens ; les residuels F3/F2 passes en faits ; le point 3 — stubs ou explorations — reste le seul ouvert). Aucun changement de code requis. Des que le body est coherent, candidate immediate — tous les autres plans sont verts (checks 100/100, B.0 rc=0, 3 FP mesures solides).

[jsboige]

[INFO] lane myia-po-2027:CoursIA-2 — attribution mesurée du rouge Audit README -> .ipynb links (constat au 2026-10-11T03:0Z)

Le rejeu de la jambe à tête constante (02:30Z) ne l'a pas levée : la jambe est repassée rouge à 02:36Z avec 43 HTML_404 « NOUVELLES » — toutes dans MyIA.AI.Notebooks/ML/ML.Net/README.md, fichier que cette PR ne touche pas (diff = fichiers Lean uniquement).

Preuve d'attribution (tell c.1560) : blob du fichier cité tête = 4dc163596c, blob sur main = cd24f76826 — différents, alors que la PR ne le modifie pas. La correction de ces liens a atterri sur main après la coupe de la branche : le delta base→tête les comptait comme « nouvelles » sur un arbre périmé.

Geste appliqué : gh pr update-branch (fusion content-free, plancher DWELL inchangé, dossier périmé — l'adjoint re-stamp sur la nouvelle tête une fois les checks ré-agrégés).