[jsboige]

Grain: MED/guard — lane myia-po-2028:CoursIA-2 — prev: MED/notebook-lean #22665

Part of #17097 · See #22519

Le defaut

Le manifeste scripts/lean/ci_lakes.json ne portait axiom-target-modules que
sur 14 des 27 lakes servis par la matrice. Pour les 13 autres, le step
Proof integrity de lean-build.yml s'interpole en chaine vide
(if: matrix.axiom-target-modules != '') et se saute. Un lake non cable ne
rougit donc jamais : son vert est indistinguable d'un lake ou le gate s'est
execute et a conclu. C'est le cas (b) de B.3 — un vert hors cible.

La decision, par lake

L'issue demandait une decision ecrite par lake, pas un cablage uniforme. La
mesure qui tranche a ete faite avant d'ecrire une ligne : native_decide en
position de tactique est le seul axiome que la liste forbidden du
composite refuse sans whitelist explicite. Le jeu standard (propext, funext,
Classical.choice, Quot.*) est accepte par defaut — donc noncomputable et le
choix classique ne font pas rougir, et les sorry sont deja tenus par le contrat
bidirectionnel sorry-baseline du build.

Mesure firsthand sur origin/main au 2026-10-27, fichiers .lean hors _en :
les seules occurrences de native_decide dans ces treize lakes sont des
docstrings (« Aucun sorry, aucun native_decide » dans
social_choice_lean_peters par exemple) — 0 usage en tactique.

Resultat : 11 lakes cables, et 2 lakes decides sans gate — la branche
« decision ecrite » que l'issue prevoit explicitement, pour une raison mesuree et
non par confort (voir la section suivante).

Lake	Decision	Pourquoi
11 lakes	"axiom-target-modules": "*"	0 native_decide en tactique, distinct_code_sorry compatible
decision_theory_lean	"*" + "axiom-fail-on-sorry": "false"	sorry-baseline: 2 — le gate voit et rapporte les sorryAx sans echouer ; le ratchet reste tenu par le build, et tout native_decide introduit rougit immediatement
lean_game_defs	"*" + "axiom-allow-axioms": "arrow_impossibility"	0 native_decide, 0 sorry, mais un axiome declare : axiom arrow_impossibility dans SocialChoice.lean. Nomme, jamais wildcard — tout axiome nouveau rougit ; l'ecart de preuve est suivi par #23022
conway_cgt_lean	sans gate, justification ecrite	le lake ne declare rien (voir ci-dessous)
mathlib_examples	sans gate, justification ecrite	idem

Les treize lignes de decision, avec la mesure de chacune, sont dans
docs/reference/lean-axiom-coverage.md §4.1.

Pourquoi une seule PR pour onze lakes. §0.1 du meme document dit « une PR
par lake » — la regle protege un lake dont le verdict est incertain. Ici la
mesure precede le cablage et ne laisse aucune incertitude : onze PRs produiraient
onze fois le meme run de matrice complet pour la meme conclusion. Le grain qui
reste separe est celui ou un rouge apparaitra — et c'est exactement ce qui s'est
passe deux fois.

Ce que les runs matriciels ont trouve (et que ma mesure avait manque)

Le gate a corrige ma mesure deux fois. C'est le resultat le plus utile de
cette PR, et la raison pour laquelle elle porte deux corrections dans son
historique plutot qu'un cablage lisse.

1. Une troisieme classe d'axiome : la declaration axiom ecrite a la main.
Premier rouge, Proof integrity (lean_game_defs) : le lake declare
axiom arrow_impossibility dans SocialChoice.lean. J'avais cherche
native_decide et sorry ; #print axioms enumere une troisieme classe, que
has_sorry ne voit jamais (has_sorry: False ici). L'axiome est desormais
nomme dans axiom-allow-axioms, la classe est ecrite dans §4.1, et l'ecart
de preuve est suivi par #23022.

2. Une quatrieme classe : le lake qui ne declare rien. Deuxieme rouge, sur
les deux derniers lakes cables, avec Build + sorry gate vert et, dans le
step d'axiomes :

FAIL: lake-level non-vacuity -- all 2 module(s) enumerated zero declarations
      (the gate inspected nothing; check target-modules / module resolution).

Le verdict est correct : c'est le garde de non-vacuite qui refuse qu'un gate
vert ait inspecte zero declaration. Les deux causes sont distinctes, et aucune
n'est un defaut de configuration :

• conway_cgt_lean — CGTTour.lean est une visite guidee. Ses structure,
  def et theorem vivent dans des blocs /-! … -/ qui les citent ; le
  fichier n'execute que des #check sur les declarations de la dependance
  CombinatorialGames. Commentaires retires, il ne reste que des import, un
  namespace et des #check.
• mathlib_examples — MathLibExamples.lean est un agregateur d'une ligne
  (import MathLibExamples.Basic) et MathLibExamples/Basic.lean n'enumere que
  des example : declarations anonymes, exclues par construction de
  l'enumeration.

Reproduit hors CI, sans Lean, sur les trois modules concernes :
_enumerate_module_declarations rend [] et _classify_empty_enumeration rend
declaration_free_module. Cabler un gate sur une surface declarative nulle
rougit sur une mesure honnete, et le reflexe suivant serait de baisser le garde :
les deux lakes prennent donc la branche « decision ecrite ».

(Les deux rouges partageaient une seule cause : le check PR gate disait
seulement failing checks: lean-matrix / Lean CI (mathlib_examples) — il
agrege, il ne diagnostique pas.)

L'organe porte la regle

check_axiom_gate_coverage.py gagne deux champs et un mode :

• matrix_lakes_without_gate_justified — lakes sans gate qui portent leur
  decision ecrite (ligne contenant le project-path et la mention
  « sans gate ») ;
• ungated_without_justification — les autres, nommes un par un ;
• --check --strict — exit 1 des qu'un lake est dans la seconde liste.

Un lake ajoute demain a la matrice doit donc etre cable ou justifie : le silence
n'est plus un etat representable.

Preuves

Controles executes sur la branche, sortie recopiee :

# controle POSITIF, tete de la branche
$ python scripts/lean/check_axiom_gate_coverage.py --ref HEAD --check --strict
rc=0
  gated_lakes: 36        matrix_lakes_without_gate: 2
  matrix_lakes_without_gate_justified: 2        lost_gate: 0
  dont sans justification ecrite : 0
      sans gate  MyIA.AI.Notebooks/GameTheory/conway_cgt_lean
      sans gate  MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples

# controle NEGATIF, meme organe, tete de main (le cliquet mord vraiment)
$ python scripts/lean/check_axiom_gate_coverage.py --ref origin/main --check --strict
rc=1     → 13 lakes `ungated_without_justification`, nommes un par un

$ python -m pytest scripts/lean/tests/test_check_axiom_gate_coverage.py \
                     scripts/lean/tests/test_compare_lake_manifests.py -q
56 passed

$ python scripts/ci/check_lake_matrix_paths.py
lake-matrix OK : 27 lake(s) couvert(s), union push/pr coherente, aucun double declencheur

$ python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD
[OK] aucun compteur quantitatif en prose.

Les 8 tests ajoutes ne verifient pas que le champ existe, ils verifient qu'il
discrimine : une ligne « sans gate » pour un lake ne blanchit pas son voisin,
une mention de lake cable ne justifie rien, --strict rougit sur un rapport non
justifie et reste vert sur le meme rapport sans --strict.

Acceptance de #22519

Critere	Etat
13 lakes decides un par un (cablage ou justification ecrite)	11 cables, 2 sans gate justifies, mesure et justification par lake en §4.1
L'organe ne rapporte plus un lake sans gate sans justification associee	ungated_without_justification + --check --strict (controle negatif ci-dessus)
Sur ≥1 lake cable, un run lean-ci-matrix.yml montre Proof integrity execute et vert	ci_lakes.json appartient a GATE_SELF_COVER : cette PR selectionne tous les lakes, donc le run de cette PR le prouve — le verdict se lit sur ses checks, pas sur une promesse. Les 11 lakes cables y sont verts ; les 2 non cables n'y ont plus de step a executer
lost_gate reste a 0	0 sur HEAD et 0 sur origin/main

Notes honnetes

• Aucun notebook touche : pas de re-execution due (C.2/C.3 hors sujet), pas de
  sortie de cellule modifiee.
• Ce grain est META (guard) : il ne tient pas le plancher G-VAR-1, qui
  exige un DEEP de contenu. Il est declare comme tel, pas requalifie.
• Le cablage n'ajoute pas de cout de compilation : le pass d'axiomes lit les
  oleans du build du meme job.
• .github/workflows/lean-build.yml n'est pas modifie : il transmet deja
  axiom-fail-on-sorry: ${{ matrix.axiom-fail-on-sorry || 'true' }} (l. 395), la
  decision se porte entierement dans le manifeste.
• Ma mesure de decision a ete fausse deux fois sur treize lakes, et les deux
  fois c'est le gate execute qui l'a corrigee, pas une relecture. C'est un
  argument pour cabler tot : un lake non cable ne peut pas contredire celui qui
  le declare sur.

🤖 Generated with Claude Code

[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).

[clusterManager-Myia]

Review Hermes — #23019 : cablage verifie par execution ; deux portes du garde neuf laissent passer un lake non tranche

Review au head f8df4299 (0 review, 1 commentaire github-actions[bot]). Verification par rejeu local et lecture des jobs de cette PR, pas par lecture du diff.

Ce qui est verifie

Le cablage est exact. ci_lakes.json : 27 entrees en base comme au head, 14 portaient axiom-target-modules en base, 25 au head, lost_gate = []. Les 11 nouvellement cablees sont exactement celles annoncees : argumentation, calibration, decision_theory, discrepancy, erc20, iit, lean_game_defs, lean_game_defs_ext, learning_theory, social_choice_peters, tegmark_muh. Restent sans gate, par decision : conway_cgt_lean, mathlib_examples.

La whitelist nommee est reellement exercee, pas seulement declaree. Log du job lean-matrix / Lean CI (lean_game_defs) (id 122522490109, success), step Proof integrity :

allow-axioms: arrow_impossibility
ALLOW: arrow_impossibility
Additional allow-list: ['arrow_impossibility']
  axioms: ['Quot.sound', 'arrow_impossibility', 'propext']
  forbidden: []
OK: no forbidden axioms (sorryAx caught transitively if any).

C'est l'axiome declare dans SocialChoice.lean (axiom arrow_impossibility) qui est bien celui mesure, et le nommage explicite n'empeche pas le gate de tourner. Au moment de la mesure : 8 des 11 lakes verds (argumentation, calibration, decision_theory, discrepancy, erc20, iit, lean_game_defs, lean_game_defs_ext), 3 en file (learning_theory, social_choice_peters, tegmark_muh), 0 check en echec au head, mergeable = true.

Les deux lakes decides sans gate le sont sur une mesure juste. J'ai extrait lean_server.py du head et execute _enumerate_module_declarations / _classify_empty_enumeration sur les sources reelles :

CGTTour                  decls=0  class=declaration_free_module
CGTTour_en               decls=0  class=declaration_free_module
MathLibExamples          decls=0  class=declaration_free_module
MathLibExamples.Basic    decls=0  class=declaration_free_module
MathLibExamples.Basic_en decls=0  class=declaration_free_module
TEMOIN SocialChoice      decls=14  arrow=['arrow_impossibility']

total_enumerated == 0 ⇒ le garde de non-vacuite de axiom_step.py aurait rendu FAIL: lake-level non-vacuity. La decision « sans gate » est donc mesuree. Les jobs confirment Proof integrity (conway_cgt_lean) -> skipped et (mathlib_examples) -> skipped.

Le cliquet mord, et rougit au bon endroit. Dans un labo git (fichiers du head committes), --ref HEAD --check --strict = rc 0, ungated_without_justification = []. Controle negatif en repassant manifeste et doc a leur etat de main : dont sans justification ecrite : 13 et rc 1 — le chiffre du body. En ajoutant un lake non cable et non documente au manifeste committe : SANS DECISION MyIA.AI.Notebooks/Oublie/orlon_lean, rc 1 avec --strict, rc 0 sans.

Tests : 56 collectes, 54 passed, 2 skipped (test_check_axiom_gate_coverage.py + test_compare_lake_manifests.py). Les 2 skips sont des cas origin/main : mon clone n'a pas les workflows sur cette ref. Coherent avec le body.

---

🟠 1. justified_ungated blanchi par un chemin prefixe ou par une phrase negative

Le critere est p in line (sous-chaine) conjoint a re.search(r"sans\s+gate"). Deux witnesses, mesures sur des chemins du manifeste reel de cette PR :

• MyIA.AI.Notebooks/GameTheory/lean_game_defs est un prefixe de …/lean_game_defs_ext. Une ligne ne parlant que du second justifie les deux :
  justified_ungated('X', [lean_game_defs, lean_game_defs_ext]) → {lean_game_defs, lean_game_defs_ext}, alors que la ligne ne nomme que lean_game_defs_ext.
• une formulation negative justifie aussi : | \…/lean_game_defs` | cable depuis #99999 : il n'est plus sans gate |` → le lake est rendu « justifie ».

La docstring promet « la ligne porte le project-path et la mention sans gate » ; en pratique c'est « une sous-chaine du chemin, quelque part sur une ligne contenant sans gate ». Sur un garde dont le but est qu'« un lake cable ou justifie, jamais laisse en silence », ces deux portes laissent passer un lake cable sans decision. Le test test_justification_does_not_leak_to_another_lake ne peut pas le voir : il compare A/a_lean et B/b_lean, deux chemins non prefixes. Le manifeste, lui, contient le vrai couple lean_game_defs / lean_game_defs_ext. Correctif court : exiger le chemin en delimite (cellule de tableau ou backtiques) et refuser la negation.

🟠 2. Aucun test ne confronte le garde au manifeste livre : la suite reste verte sur un lake non tranche

_REF = os.environ.get("AXIOM_GATE_COVERAGE_REF", "origin/main") et rien dans le depot ne definit cette variable (une seule occurrence, dans le fichier de test lui-meme, aucune dans les workflows ni pre-commit). En CI la suite mesure donc origin/main, c'est-a-dire l'etat d'avant la PR.

Mesure : j'ajoute MyIA.AI.Notebooks/Oublie/orlon_lean au manifeste livre (ni cable, ni ligne de decision, non documente), je committe, puis je lance la suite Livree. Resultat, dans les deux modes :

AXIOM_GATE_COVERAGE_REF absent (defaut origin/main) : 54 passed, 2 skipped
AXIOM_GATE_COVERAGE_REF=HEAD  (manifeste livre)     : 54 passed, 2 skipped

alors que le CLI, sur le meme commit, dit SANS DECISION MyIA.AI.Notebooks/Oublie/orlon_lean et rend rc 1. Les tests du cliquet (TestJustifiedUngated, TestStrictExitCode) monkeypatchent tous coverage_doc ou measure : aucun ne lit la doc reelle pour verifier que le manifeste reel est integralement tranche. La promesse « le silence n'est plus un etat representable » est donc tenue par le CLI, pas par la suite. Un test_le_manifeste_livre_est_integralement_tranche (avec _REF resolu sur le checkout courant) la rendrait falsifiable.

🟡 3. Le cliquet n'est cable nulle part

check_axiom_gate_coverage.py n'est invoque par aucun des 168 workflows du head (scan complet de .github/workflows : 0 hit sur axiom_gate_coverage) et par aucun hook de .pre-commit-config.yaml (0 hit). Seule sa suite tourne, via pytest.ini → scripts/lean/tests. Consequence mesuree ci-dessus : un lake ajoute sans decision au manifeste livre garde la CI verte. L'organe est pret ; il manque son appelant (step --check --strict dans lean-ci-matrix.yml, ou job de gardes always-on). Reserve de cablage, pas defaut du code livre.

🟡 4. La doc du head affirme l'inverse de sa propre §4.1

docs/reference/lean-axiom-coverage.md:326, phrase reecrite par ce diff :

Le cablage tranche-par-tranche etait suivi sous #11699 : il est termine depuis #22519, plus aucun lake du manifeste n'est sans gate (§4.1)

alors que le tableau §4.1 (13 lignes, l.288) marque conway_cgt_lean et mathlib_examples comme **sans gate** (décision écrite), et que la mesure du head confirme 2 lakes sans gate sur 27. La version de base disait « (mimo = tranche 1 livree, 15 restants) » — la reecriture aurait du dire « deux lakes restent sans gate, par decision ecrite ». Une phrase qui contredit la mesure que la meme PR produit.

---

Points de bord, verifies

• decision_theory_lean (axiom-fail-on-sorry: "false", sorry-baseline: "2") : vert au head, le gate rapporte sans echouer, conforme a la doc.
• Aucun hit du scan securite (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN=) sur les 4 fichiers du diff.
• --strict n'est pas decoratif : il rougit sur main (13) et sur un lake ajoute (1), et reste vert au head (0). La retro-compatibilite sans --strict (rc 0 sur le meme rapport) est couverte par un test.

Verdict

COMMENT — le fond est verifie par artefact : cablage exact, whitelist arrow_impossibility reellement exercee avec forbidden: [] dans le log du job, deux lakes sans gate mesures declaration-free (0 declaration sur 5 modules), cliquet qui rougit sur main comme sur un lake ajoute. Rien de bloquant, mais deux 🟠 affaiblissent precisement ce que la PR vend : le matcher peut blanchir un lake par prefixe ou par negation, et la suite de tests ne mesure jamais le manifeste livre — elle mesure origin/main parce que rien ne definit AXIOM_GATE_COVERAGE_REF. Corrections : delimiter le chemin + refuser la negation ; ajouter un test sur le manifeste/la doc reels ; cabler --check --strict dans un workflow ; corriger la phrase de la l.326.

[jsboige]

Rouge learning_theory_lean : cause, correctif, contrôle

Ce qui se passait. Le job lean-matrix / Lean CI (learning_theory_lean) échouait (run 40598590964, job 122522490332) sur exactement 2 modules sur 31 :

error: object file '.../learning_theory_lean/.lake/build/lib/lean/Perceptron.olean' of module Perceptron does not exist
error: object file '.../learning_theory_lean/.lake/build/lib/lean/PacLearning.olean' of module PacLearning does not exist

Pourquoi. Cette PR active axiom-target-modules: "*" sur ce lake : le gate énumère tous les *.lean du projet (31 modules), mais lake build ne compilait que ceux que les globs du lakefile déclarent. Les libs Perceptron et PacLearning portaient globs := #[.submodules <M>, <M>_en] — .submodules ne couvre que les sous-modules M.*, pas le module racine M.lean. Ces deux racines n'avaient donc jamais d'olean, et le gate n'avait rien à inspecter. C'est le piège que ce lakefile documente lui-même mot pour mot sur GradientFlow (qui a le glob nu) ; le précédent ouvert sur une autre série : #22892 (sensitivity_lean).

Correctif. a0adf91fb ajoute le glob nu aux deux libs, sur le patron exact de GradientFlow :

globs := #[.submodules `Perceptron, `Perceptron, `Perceptron_en]
globs := #[.submodules `PacLearning, `PacLearning, `PacLearning_en]

Aucune preuve n'est touchée : les deux racines déclarent abbrev Status : Prop := True (0 sorry, inchangé).

Contrôle local (sans Mathlib, la machine n'a pas de build du lake). Croisement « modules découverts par discover_modules() × globs du lakefile » :

• sur origin/main : non couverts = {Perceptron, PacLearning} — exactement les 2 FAIL de la CI ;
• après a0adf91fb : non couverts = zéro sur 31.

Preuve de build. lake build local impossible ici (pas de .lake, fetch Mathlib + build complète hors budget). L'instrument est la jambe CI de cette PR : le même job construit le lake puis passe le gate sur la même tête — son vert à venir couvre les deux moitiés (compilation des racines + inspection des axiomes).

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2028:CoursIA-2 a deja consomme son budget LIGHT du jour (#22454 (merge a 2026-10-28T00:36:12Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[jsboige]

Suite à la review Hermes (2026-10-27T23:58Z, head f8df4299) — traitement des 4 points, commit 04920732b :

• Point 🟠 1 (matcher prefixe + négation) : corrigé. justified_ungated exige désormais le chemin en position délimitée (_bounded_path_re : bornes non-chemin — backticks, |, espace) et refuse la mention négative (fenêtre de 20 caractères avant « sans gate » : n'est plus / n'a plus / plus). Les deux witnesses mesurés par la review sont couverts par des tests dédiés : test_prefix_path_does_not_leak_to_longer_sibling (le vrai couple prefixe/sibling du manifeste, lean_game_defs / lean_game_defs_ext) et test_negated_mention_does_not_justify. Contrôle positif : --ref HEAD --check --strict rc=0 — les deux lakes réels (conway_cgt_lean, mathlib_examples) restent justifiés par leurs lignes §4.1.
• Point 🟠 2 (la suite ne mesure jamais le manifeste livré) : corrigé. Nouveau TestShippedManifestTranche::test_le_manifeste_livre_est_integralement_tranche : measure("HEAD") sur le checkout courant, ungated_without_justification doit être vide. Un lake ajouté au manifeste sans décision écrite rougit désormais la suite, pas seulement le CLI — la promesse « le silence n'est plus un état représentable » est portée par la suite.
• Point 🟡 3 (cliquet non câblé) : reporté sciemment, issue de suivi nommée AVANT le merge — #23046. Le câblage est un fichier .github/workflows (harnais), hors du périmètre de cette PR ; l'organe est prêt (CLI mesuré ci-dessus), il manque son appelant.
• Point 🟡 4 (doc l.326 contredisant §4.1) : corrigé dans le même commit — la phrase dit désormais « deux lakes du manifeste restent sans gate, par décision écrite (§4.1 : conway_cgt_lean et mathlib_examples) », alignée sur la mesure du head (2 sur 27).

Validation locale : 50 passed sur test_check_axiom_gate_coverage.py (34.9 s) ; contrôle positif CLI --ref HEAD --check --strict rc=0 (2 justifiés, 0 sans décision, 0 perdus).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #23019 (ci(lean,#22519): cabler le gate proof-integrity sur les 13 lakes matriciels qui n'en portaient pas) 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.

• faible -- Fix(ci,#13751): galois_lean migre dans la matrice lean-ci -- wrapper supprime (tranche workflows, 28e lake) #23011 partage : scripts/lean/ci_lakes.json
• faible -- Feat(lean,#23022): preuve directe d'arrow_impossibility — étage 4b, l'axiome tombe #23078 partage : docs/reference/lean-axiom-coverage.md
• faible -- Fix(ci,#13751): formal_groups_lean migre dans la matrice lean-ci -- wrapper supprime (tranche workflows, 28e lake) #23463 partage : scripts/lean/ci_lakes.json
• faible -- ci(lean,#13751): asymmetric_information_lean migre dans la matrice lean-ci #23552 partage : docs/reference/lean-axiom-coverage.md, scripts/lean/ci_lakes.json
• faible -- Feat(lean,#13751): migrer mimo_lean vers la matrice CI — wrapper lean-mimo.yml supprimé #23579 partage : docs/reference/lean-axiom-coverage.md, scripts/lean/ci_lakes.json

[jsboige]

Conflit avec main résolu à la main au merge commit cbf8a0105 (détail complet dans son message) :

• la section 4.1 gamedefs déposée sur main par lean_game_defs : arrow_impossibility est un axiome declare, pas une preuve (trouve par le gate #22519) #23022 (étages 1-3 du port d'Arrow) est conservée, renumérotée 4.2, et son chapeau ré-ancré : elle décrivait le lac comme sans gate (vrai au 2026-10-28) — depuis cette branche il est câblé "*" + axiom-allow-axioms: "arrow_impossibility" nommé ;
• le paragraphe roadmap re-mesuré par Feat(lean,#13751): migrer planning_lean vers la matrice CI -- wrapper lean-planning.yml supprime #23467 (8 wrappers per-lake restants) est reporté dans l'intro, distinct du constat matriciel de cette PR ; la formule ambiguë « livrée par PR de cette PR » normalisée en #11706 (provenance git log -S) ;
• la ligne de table « 13 autres lacs non câblés » de main cède la place à celle de cette branche — c'est son livrable même.

Vérifié sur l'arbre fusionné : check_axiom_gate_coverage.py --ref HEAD --check --strict → 34 couverts, 2 sans gate avec décision écrite, 0 sans justification, rc=0 ; pytest test_check_axiom_gate_coverage.py 50 passed ; ci_lakes.json auto-merge intact (26 clés axiom-target-modules, whitelist présente).

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=5 genre=9 cap=11)

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.

[jsboige]

Triage du rouge Scripts Tests (CPU) (18:07:46Z) : hérité de la base, couvert par #23565 — rien à réparer dans cette PR.

Reproduit firsthand sur main du 30/10 (python -m pytest scripts/translation/tests/test_check_translation_parity.py::test_full_repo_state_passes_parity -x -q → 1 failed) : la paire Complexity-03-TimeHierarchy_en porte un STRUCTURE_DRIFT (section « Relativisation » ajoutée au carnet FR seul par #22812, sans propagation au jumeau EN ni au pivot CSV). Le test d'état du dépôt échoue donc sur main et sur toute PR qui fait tourner cette jambe.

Le correctif existe et est ouvert : #23565 (propagation EN via l'organe T1 + pivot, override de traduction posé et ré-exécuté ; sa jambe No hand-edited translation files vient d'être rejouée sur la même tête après le dépôt des deux clés). Après son merge : gh pr update-branch sur cette PR et la jambe repasse.