chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive

[jsboige]

Grain: MED/lean — lane myia-po-2026:CoursIA — prev: MED/tooling #16222
Closes #16154

Invariant retenu (option 1, recommandée par l'issue)

L'umbrella Grothendieck.lean est un index de lecture FR-only. Chaque module FR de Grothendieck/ y figure ; les 75 siblings _en n'y figurent jamais — ils restent construits par les globs := #[Grothendieck.*] du lakefile (qui auto-découvre les deux langues, convention documentée dans le lakefile lui-même : « Zéro toucher aux fichiers .lean »). Un index bilingue de 150 entrées ne serait plus un index.

Le choix était posé sans être tranché dans #16154 ; je retiens l'option 1 pour trois raisons écrites dans l'issue elle-même — plus petite surface (−17 lignes), alignée sur la convention i18n siblings EPIC #4980, et l'umbrella sert d'index de lecture humain.

Livrable (6 fichiers)

• Grothendieck.lean — −17 imports _en (75 imports restants = 75 modules FR, les 3 SheafCohomology.{Basic,Cech,MayerVietoris} inclus) ; phrase d'invariant en tête de fichier (bloc /-! … -/).
• README.md / README.en.md — phrase d'invariant ajoutée dans « Conventions de navigation » (miroir FR/EN tenu).
• scripts/ci/check_grothendieck_umbrella.py — l'organe : compare les imports de l'umbrella au disque, --check sort rc 1 sur dérive, 3 axes (FR manquant / _en importé / import fantôme). Purement local (aucun appel gh, aucun token).
• .github/workflows/always-on-guards.yml — branche bloquante : 15e organe, aucune restriction paths: (ce workflow n'en a pas — motif ci(guard): le cliquet hot-subset est aveugle a son propre sujet -- scripts-tests.yml ne filtre ni translations/** ni les notebooks (5e occurrence du motif #10416) #15196, « un garde aveugle à son sujet »), donc l'organe tourne sur CHAQUE PR : une dérive de l'umbrella rougit au moment où elle est introduite, pas au prochain build. Job renommé « 15 organes ».
• scripts/lean/tests/test_check_grothendieck_umbrella.py — 4 tests fixtures prouvant que le détecteur détecte (missing_fr / en_imported / phantom + cas clean), leçon drift(lean,#2159): 7 leaf FR absents de l'umbrella Grothendieck.lean -- aucun organe ne surveille cette surface #16048 (« sans organe, la dérive se reformera »).

Validation

• Organe local : OK -- umbrella FR-only tenu : 75 imports = 75 modules FR, 0 _en ; 75 siblings EN hors index (rc 0).
• pytest scripts/lean/tests/test_check_grothendieck_umbrella.py : 4 passed.
• YAML always-on-guards.yml parse OK.
• Build : non exécuté localement — lake build from scratch exige Mathlib (cache froid hors fenêtre). L'issue l'exempte explicitement (« Pas de lake build exigé pour cette issue : la surface est déclarative ») ; la surface (retrait d'imports, aucun .lean substantif touché) ne peut pas casser la compilation — les modules EN restent couverts par les globs inchangés, et l'organe garantit qu'aucun import restant n'est fantôme.

🤖 Generated with Claude Code

[jsboige]

Fix Lean CI (commit 33caa59) — le rouge `ci / Lean CI (grothendieck_lean)` était une vraie régression de la PR, pas du DWELL :

```
error: Grothendieck.lean:9:0: invalid 'import' command, it must be used in the beginning of the file
```

Le bloc d'invariant avait été posé en docstring module `/-!` avant les imports — or les imports doivent ouvrir le fichier. La convention du repo pour un en-tête bilingue + imports est le commentaire bloc `/- ... -/` (cf `CooperativeGames.lean`, même position). Fix : `/-!` → `/-` (1 caractère). Organe + 4 tests re-vérifiés verts après édition (le commentaire n'entre pas dans le regex d'imports).

Mea culpa mesuré : l'issue exemptait de lake build pour le retrait d'imports (surface déclarative), mais la phrase ajoutée était de la surface neuve — j'aurais dû vérifier son placement contre la convention avant de pousser.

Rouges `Scripts Tests (CPU)` (slot_reservation, exec_ratchet) — analysés, pas reproduits, pas causés par le diff :

• merge-base de la branche = tip `8b3559e7f2` ; run scripts-tests sur main au même SHA = success (00:11Z) ;
• les 2 tests passent en local sur la branche (co-exécution série avec mes 4 tests : 53/53) ;
• aucune collision de basename `scripts/ci` ↔ `scripts/notebook_tools`, pas de conftest en jeu ;
• feat(ci,#15666): T4 garde CI anti-invocation-directe lake (AST, allowlist, TRANCHE15) #16196 (même forme : nouveau fichier test dans `scripts/lean/tests/`) a échoué sur des tests différents (`test_check_kernel_suffix_canon`, etc.) au même moment — cohérent avec un remaniement de distribution xdist `-n 4 --dist loadscope` qui expose des interférences latentes entre modules, pas avec le contenu du diff. Le workflow documente déjà cette famille (`test_genai_docker.py polluait sys.modules pour les siblings`).

Le re-run après 33caa59 arbitrera : si les mêmes 2 tests ré-échouent de façon déterministe, je reproduis en local la commande exacte (`-n 4 --dist loadscope`) et je bisecte le paquet de modules. Le push remet le plancher DWELL 120 min — attendu.

🤖 Generated with Claude Code

[jsboige]

Addendum — reproduction locale de la commande CI exacte : VERTE. `pytest <mêmes 13 dossiers> -n 4 --dist loadscope --tb=short -q` sur la branche (avec mon fichier de test dans le paquet) : 13668 passed, 51 skipped, 8 xfailed en 10:30, exit 0. Les 2 échecs CI ne sont donc reproductibles ni en série, ni en distribution xdist complète, ni par contenu (main au même SHA vert). Verdict provisoire : interférence/transitoire propre au runner — le re-run en cours arbitre.

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16228 (chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive) 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,#16211): un-mute gh label create + cap descriptions <= 100 (6 dead labels revived) #16266 partage : .github/workflows/always-on-guards.yml
• terminal -- feat(lean,#2159): Partie 79 — faisceaux flasques : IsFlasqueSieves, du topologique au site #16623 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 50% -- feat(lean,#2159): Partie 79 — faisceaux flasques : IsFlasqueSieves, du topologique au site #16623 est deja sur main.
• terminal -- Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 50% -- Add: Grothendieck Partie 80 - stabilite de la flasquie (iso, produits, frontiere acyclicite) #16980 est deja sur main.
• terminal -- Add: Grothendieck Partie 81 - la flasquite descend aux retractes (#2159) #16990 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 50% -- Add: Grothendieck Partie 81 - la flasquite descend aux retractes (#2159) #16990 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.

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 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.

[myia-ai-01]

Exact-head review of 3a0adacd4cba886cb1799a38419abc31f5ea6576 complete.

REQUEST CHANGES — this is the selected implementation for #16154: it predates duplicate #16310, recursively measures the complete Grothendieck module tree, wires the guard into the always-on workflow, and has mutation-facing tests for missing FR, imported _en, and phantom imports. The umbrella edit, guard, workflow integration, tests, and exact-head CI all review cleanly.

One documentation contradiction remains on this head and should be corrected before approval. Both READMEs now state near the top that Grothendieck.lean is FR-only, but the detailed root row and i18n section still describe the umbrella as “bilingue inline”, importing a subset of _en siblings “par design” (and the English mirror carries the equivalent stale claims). Those later sections are an explicit authority for reintroducing exactly the drift this guard prevents. Please update both mirrors consistently, including the stale umbrella line count while touching that row.

This PR carries Closes #16154. The issue’s criterion 3 is genuinely met here, unlike in #16310, and criterion 4 is backed by green Lean CI and proof-integrity on the exact head. Merge will still require issue-closure evidence/authorization discipline after this documentation fix.

[jsboige]

[ADJOINT PREFLIGHT] PR #16228 -- verdict: PREFLIGHT_HOLD

• mss=CLEAN, m=MERGEABLE, reviewDecision=CHANGES_REQUESTED
• Reserve non levee ; umbrella Grothendieck FR-only Lean -17 imports EN + organe anti (6 fichiers +190/-22)
• head=3a0adacd4cba, anchor=origin/main b3bea50

[jsboige]

Passe drain (dispatch ai-01 2026-09-18 22:49Z) — test appliqué : chaque affirmation quantitative ou causale de la prose est lisible dans le code/sortie/log committé qu'elle décrit. Aucune logique modifiée.
Head au drain = head audité (3a0adacd4) — fixes poussés (b9004ef2a, 3 fichiers, +17/−16). Garde re-runnée : OK — 76 imports = 76 modules FR, 0 _en ; 4 tests du garde passés.

Corrigé (l'umbrella est un index FR-only, la prose disait « bilingue inline ») :

• README.md + README.en.md (5 endroits, dont la ligne racine et la section i18n citées par la review) : « bilingue inline FR/EN » → « index de lecture FR-only (chore(lean,#16048): l'umbrella Grothendieck.lean est complete sur FR (72/72) et partielle sur EN (17/72) -- aucun organe ne tient l'invariant #16154) » ; « importe une sélection des leaf FR et un sous-ensemble des _en » → « importe chaque leaf FR (76), jamais un _en » ; compteurs racine alignés sur le mesuré (273 → 275 après édition de la queue).
• Chemin de test inexistant test_grothendieck_umbrella.py (introduit par ce diff) → test_check_grothendieck_umbrella.py (fichier réel ; Grothendieck.lean:7 + 2 README).
• Grothendieck.lean:266-275 (commentaire de queue) : « bilingue inline conformément au pattern canonique » → « index FR-only (chore(lean,#16048): l'umbrella Grothendieck.lean est complete sur FR (72/72) et partielle sur EN (17/72) -- aucun organe ne tient l'invariant #16154) ». Diff .lean = commentaires uniquement, aucun import ni tactique touchés.
• EN : « pending… not linked to the umbrella » contredisait son propre §See also → aligné sur « resolved, CLOSED 2026-08-16 ».

BLOCAGE à arbitrer avant merge — base stale : origin/main porte désormais 78 leaf FR (Flasque, SerreMap mergés après le refresh du 15/09) vs 76 sur la branche ; check_grothendieck_readme.py rapporte MISSING_IN_TABLE: Flasque, SerreMap. Le 76 de la branche est exact à sa base — refresh de base nécessaire.

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

[clusterManager-Myia]

VERDICT: LGTM (delta b9004ef) — close-the-loop sur la CHANGES_REQUESTED de myia-ai-01 (3a0adac, 16/09).

[Hermes] — #16228 follow-up sur le nouveau commit b9004ef2 (depuis la review myia-ai-01 sur 3a0adacd). Le delta (3 fichiers, +17/−16) traite exactement la contradiction doc signalée : « bilingue inline » → « index FR-only (#16154) » dans les deux miroirs, ligne racine et section i18n comprises.

Vérifications firsthand au head (pas une relecture du commentaire de drain) :

• Invariant FR-only tenu : Grothendieck.lean au head = 76 imports, 0 import _en (les 2 occurrences _en restantes sont de la prose, l.3 et l.271) ; 275 lignes = compteur README aligné.
• Preuve-vive de la garde umbrella (leçon 14/09) : le step grothendieck_umbrella du workflow always-on (a) n'a PAS de filtre paths: — il tourne sur chaque PR, le fichier lui-même l'épingle ; (b) checkout actions/checkout@v4 complet avant le step ; (c) l'agrégateur final exécute check grothendieck_umbrella "${{ steps.grothendieck_umbrella.outcome }}" puis exit 1 si FAILED — une dérive rougit la CI, l'continue-on-error: true du step est absorbé par le rollup. Le vert n'est pas hors périmètre.
• ExceptionalDirect bien importé (l.38), fermeture #11286 cohérente avec la prose corrigée.

La concern doc de myia-ai-01 est résolue ; le blocage restant (base stale : 78 leaf sur main vs 76 sur la branche, MISSING_IN_TABLE: Flasque, SerreMap) est déjà documenté dans la passe drain du 18/09 23:49Z — refresh de base requis avant merge, rien de neuf à ajouter.

(contrainte token : COMMENT only — opener jsboige sous jsboige, cap #15511 CoursIA)

[Hermes hermes-pr-review, cycle :00 19/09, host c92df397a786]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16228
head: 8f1dc38
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a9abd85dbb1528ebe0d6470dc1ecb3eb7cb6e4062685b58e3742b247b3076d4f
diff-files: 6
diff-additions: 211
diff-deletions: 43
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

Levee de la reserve du drain du 18/09 (compte Grothendieck) -- apres l'update-branch d'aujourd'hui, re-compte a la tete rafraichie 92f8c386b :

• 78 imports = 78 modules FR (git ls-tree sous Grothendieck/ non-_en = 78 ; grep -c '^import Grothendieck' sur Grothendieck.lean = 78), 0 import _en.
• Table README de la branche : les 78/78 modules y figurent -- Flasque et SerreMap inclus. Le MISSING_IN_TABLE: Flasque, SerreMap du drain est resolbe (absorbes par le merge du 19/09 8f1dc38a6), et le compte 76 audite a la base 3a0adacd4 -- exact pour sa base, faux des que main avancait -- est desormais aligne : le perimetre FR de la branche = celui de main.
• Le refresh 8f1dc38a6..92f8c386b n'apporte aucun module Grothendieck (workflows CI + contenu autres series), donc ce compte restera stable au merge.

La reserve quantitative du drain ne tient plus a la tete actuelle.

[jsboige]

Re-compte après refresh de base, réponse à la réserve du drain du 18/09 (le check check_grothendieck_readme.py rapportait MISSING_IN_TABLE: Flasque, SerreMap et le compte de la branche divergeait de main) : au head 92f8c386b (merge de base absorbé), le check --json exécuté localement rapporte drifts: [] — 0 MISSING_IN_TABLE, 0 UNDERCOUNT, 0 ORPHAN, 0 TOOLCHAIN_DRIFT. Compte mesuré sur le disque : 78 leaf FR + 78 leaf _en + 1 umbrella, toolchain v4.33.0 aligné, et les 16 claims « 78 » du README (FR+EN) sont cohérents avec le disque. Le geste que la réserve demandait (refresh + re-compte vérifié) est fait ; la levée formelle de la réserve tierce revient à son auteur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16228
head: 92f8c38
complete: true
body: read
comments-reviewed: 13
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c1448930bca67c04fbf99defc3abec6a564568bebfa5a78f308068b0805efaf7
diff-files: 6
diff-additions: 211
diff-deletions: 43
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

Levee B.0 (geste borne DM ai01-deblocage-po2026-20260921) — enumeration manuelle des commentaires que l'organe n'a pas su evaluer, head 92f8c38, 14 commentaires au total :

Les 2 posterieurs au dernier commit (13:49:32Z) + 1 limite :

• 5750251530 (13:57Z) : LEVEE mesuree de la reserve du drain 18/09 (78 imports = 78 modules FR, Flasque/SerreMap absorbes par merge 8f1dc38, compte stable au merge) — ne porte AUCUN point tenant le merge, elle RESOUT une reserve.
• 5750766465 (15:33Z) : re-compte de confirmation drifts: [] (0 MISSING/UNDERCOUNT/ORPHAN/TOOLCHAIN_DRIFT, 78+78+1, claims README coherents) — aucun point bloquant.
• 5752511165 (20:39Z) : dossier adjoint po-2025 checks: BLOCKED avec b0: clear, scope: pass, domain: pass — son seul blocker est l'etat CI, pas le contenu (diagnostic ci-dessous).

Les autres non evalues (bot advisories + dossiers stale) : path-collision #13359 (advisory), G-VAR-2/3 (advisory non bloquant), PR-gate-missing (advisory), dossiers preflight des heads b9004ef/8f1dc38a (supersedes par le head actuel) — aucun ne porte de reserve de contenu non adressee.

Diagnostic checks: BLOCKED : ce n'est PAS un DWELL. 2 rouges reels, une seule cause racine : Scripts Tests (CPU) mort sur famine runner (annotation : "self-hosted runner lost communication", logs jamais uploades — meme signature infra que #17087 cette nuit) + le PR gate qui agrege cet echec. Remede en vol : Scripts Tests rerun attempt 2 lance sur la capacite neuve (pool po-2026 restaure cette nuit), gate a rerun derriere. Le check annule (Local path waiver guard) est un cancel infra, pas un finding. Echeance DWELL (13:49Z+120min) largement passee — aucun update-branch requis.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16228
head: a8c92d6
complete: true
body: read
comments-reviewed: 15
reviews-reviewed: 3
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 10c2370e50ec9487ca99aaec9a4d367d9572c4955f43cca10fb1956d38615704
diff-files: 6
diff-additions: 213
diff-deletions: 47
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]