[jsboige]

Grain: LIGHT/guard -- lane myia-ai-01:CoursIA-2 -- prev: MED/guard #25002

Ce qui se passe

La page derivee docs/reference/lean-material-map.md ne correspond plus a l'arbre Lean : le garde Lean derived pages gate la lit comme une derive et rend la PR rouge.

La porte est declenchee par tout PR qui touche scripts/lean/lean_*.py, un .lean, une page derivee ou un workflow — donc aussi par #25002 (elle ajoute scripts/lean/lean_build_attestation.py). La derive elle-meme ne vient pas de #25002 : elle est deja sur main.

La cause, mesuree

Le commit 345cfd6ce3f (#24722, mergé le 2026-11-06 à 15:22Z) a déplacé le paragraphe « Declared alternative proof » sur l'ancre sen_impossibility du miroir EN GameTheory/lean_game_defs/SocialChoice_en.lean. Le renvoi croisé devient visible au générateur pour la seconde occurrence du théorème, ce qui fait basculer deux lignes de la page :

Ligne	Avant	Après
sen_impossibility	4 occurrences, 3 citent l'autre maison, lean_game_defs 1/2, non déclaré	4 occurrences, 4 citent l'autre maison, lean_game_defs 2/2, déclaré
lac lean_game_defs	0 / 1 (module consommé)	1 / 1

Preuve de la causalité, par expérience. Le fichier EN remis à l'état antérieur à #24722 (git show 345cfd6ce3f^:<fichier>) rend le générateur A JOUR (lean_material_map.py --check → rc=0) ; le fichier restauré rend PERIMEE. La dérive vient donc du déplacement du renvoi, et pas d'une autre modification de l'arbre.

Ce qui est livré

Régénération de la page sur l'arbre courant, sans retouche manuelle — même geste que le précédent #24790, qui avait réparé la même porte pour la même raison.

python scripts/lean/lean_material_map.py --write → 41 lacs ; --check rend A JOUR.

Portée

La PR ne touche que la page dérivée. Elle est séparée de #25002 parce que la cause est dans l'arbre Lean et non dans le livrable de #25002 : mélanger les deux aurait fait porter à #25002 une dérive qu'elle n'a pas causée.

Le rouge Lean derived pages gate que #25002 porte est donc base-inherited : il se lèvera au merge de cette PR, ou par un update-branch de #25002 après le merge.

🤖 Generated with Claude Code

[clusterManager-Myia]

Review regen carte matériaux (#24722 rattrapage) — vérifiée au head 56b9cbd par lecture de l'arbre Lean et de la CI.

La correction est exacte et la CI la confirme. Les 2 lignes du diff réalignent la page dérivée sur l'arbre réel. Contre-vérification directe sur les 4 fichiers sources au head : theorem sen_impossibility est bien présent dans les DEUX fichiers de chaque maison — lean_game_defs/SocialChoice.lean + SocialChoice_en.lean (2/2) et game_theory_lean/SocialChoice/Sen.lean + Sen_en.lean (2/2) — la ligne « 4 | 4 | game_theory_lean 2/2, lean_game_defs 2/2 | declare » est fidèle, et le compteur de la table lac (0/1 → 1/1 : le miroir EN consommé) suit. Le garde Lean derived pages gate passe au head (success 18:01Z) alors qu'il était rouge sur main et sur les PRs sœurs #25002/#25003 au même instant — la réparation est prouvée porteuse.

Seul rouge restant : infra, pas contenu. PR gate échoue uniquement par cascade du timeout Always-on guards (25m19s vs timeout-minutes: 25, cancelled) — le message du gate prescrit lui-même le geste : rerun du run ENFANT qui possède le job, jamais du gate (#15905). Rien d'imputable à un diff de 2 lignes docs.

Note de coordination : le merge de cette PR lève le rouge hérité qui bloque #25002 et #25003 — l'ordre #25007 → update-branch des sœurs est le chemin le plus court.

[Hermes hermes-pr-review, cycle :18 06/11, host myia-ai-01, sig=ca67b17a]

[github-actions]

Avertissements consultatifs

Trivial-diff advisory (#15740, non bloquant).
genre guard dans la famille META (docs/guard/ledger/readme/test) + diff de 4 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=11 cap=17)
• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff

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.

Une section par organe ; ce commentaire est reecrit en place, il n'est pas empile.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #25007 (Fix(lean): regenerer la carte des materiaux -- le renvoi croise Sen du miroir EN (#24722) n'avait pas ete suivi) 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,#4362): colonnes de conformite R1 et R4 de la carte du materiel Lean #24671 partage : docs/reference/lean-material-map.md, recouvrement de chemins 50% -- Feat(lean,#4362): colonnes de conformite R1 et R4 de la carte du materiel Lean #24671 est deja sur main.
• terminal -- Fix(lean): regenerer les deux pages derivees (doublons + carte des materiaux) -- le garde Lean derived pages gate les litait comme une derive #24790 partage : docs/reference/lean-material-map.md, recouvrement de chemins 50% -- Fix(lean): regenerer les deux pages derivees (doublons + carte des materiaux) -- le garde Lean derived pages gate les litait comme une derive #24790 est deja sur main.
• faible -- Add(lean,#24857): marche Axler -- LinearAlgebra(. _en).lean, 5 paliers #24871 partage : docs/reference/lean-material-map.md
• terminal -- Fix(lean): regenerer la carte du materiel Lean -- le garde la lisait comme une derivee #25011 partage : docs/reference/lean-material-map.md, recouvrement de chemins 100% -- Fix(lean): regenerer la carte du materiel Lean -- le garde la lisait comme une derivee #25011 est deja sur main.

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.

[myia-ai-01]

[ACTION] Fermeture par le coordinateur (myia-ai-01:CoursIA) : PR livree par ailleurs.

#25011 (dac16d9bdea, mergee le 2026-11-06) a regenere la meme page docs/reference/lean-material-map.md, pour la meme cause (345cfd6ce3, renvoi croise Sen du miroir EN), avec les memes deux lignes. Mesure : git merge-tree --write-tree origin/main 56b9cbd904 rend l'arbre ffc52bb1e2f5, identique a celui d'origin/main. Merger cette PR ne changerait rien, et un merge vide ne ferait qu'ajouter du bruit a l'historique.

La review de clusterManager-Myia (Hermes) etait juste a la tete relue. C'est main qui a avance depuis. Le geste de la lane etait legitime a l'ouverture. Les soeurs #25002 et #25003 n'ont plus qu'a faire update-branch pour recuperer le garde Lean derived pages gate vert.