fix(lean,#16581): companion Lean-22 — cellule 14 compte 78 modules reels (siblings _en exclus), sortie re-executee

[jsboige]

Grain: MED/notebook-python — lane myia-po-2024:CoursIA — prev: DEEP/lean #16911

Summary

Dernière surface de la réconciliation triple de #16581 : la sortie de la cellule 14 du companion Lean-22 comptait les fichiers (rglob('*.lean') → 150, siblings _en inclus) là où le README du lake et la prose comptent les modules réels (78 leaf FR, siblings exclus). Les deux autres surfaces étaient déjà réconciliées sur main — prose retirée par #16656 (issue #16642), README réaligné à 78 par une PR tierce (checker check_grothendieck_readme.py : drifts: [] sur le head de cette branche).

Changement

• Cellule 14 du notebook : gro_modules exclut désormais les stems *_en (convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 — un sibling par module double tout compte de fichiers) ; libellé explicite « modules reels (siblings i18n _en exclus) ». La sortie affiche 78 — aligné sur le README du lake (78 leaf FR + 78 _en + 1 umbrella) et une liste sans doublons (Adjunction, Basic, … au lieu de Adjunction, Adjunction_en, …).

Validation

• Re-exécution réelle de la cellule modifiée (kernel python3 via nbclient, cwd = dossier du notebook, dans le worktree de la branche) : sortie committée = sortie kernel, execution_count réel, 0 erreur. Aucune autre cellule n'est modifiée — leurs outputs restent ceux de l'exécution feat(lean,#11703): annexe du companion Lean-22 — complétion adique et ramification inférieure #16256.
• python scripts/lean/check_grothendieck_readme.py --json sur le head : drifts: [] (surface README intacte, disk 78 FR + 78 EN + 1 umbrella).
• Acceptance 2 de Lean-22 companion : compte de modules grothendieck_lean triple (prose 34 / run 150 / README 75+1) — reconciliation requise #16581 vérifiée : grep des comptes numériques de modules (\d+ modules?, leaf) sur les companions Lean-15-Grothendieck-Tribute, Lean-15b, Lean-15c — aucun compte de modules galois ; seul le Lean-22 portait un compte dérivé.
• C.1 : aucune erreur volontaire ; cellule exécutée proprement de bout en bout.

Notes

• Constat de périmètre : ma lecture initiale venait d'un clone local en retard (le checker y rendait un BLOCKING périmé « 2 modules absents de la table » — état d'un main antérieur). Sur origin/main frais, drifts: [] : ce PR ne porte que la surface restante, la sortie de cellule.
• Le compte « 78 » reste sensible à l'arrivée de nouveaux modules — mais il est dérivé du disque à l'exécution (rglob), pas d'un chiffre en dur : il ne peut plus dériver silencieusement.

Closes #16581

🤖 Generated with Claude Code

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

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]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 16
• 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)

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=4 cap=3)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=4 cap=3)
• 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 outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.3s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	8.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	6.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	54.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.9s

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16923 (fix(lean,#16581): companion Lean-22 — cellule 14 compte 78 modules reels (siblings _en exclus), sortie re-executee) 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,#11703): annexe du companion Lean-22 — complétion adique et ramification inférieure #16256 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb, recouvrement de chemins 100% -- feat(lean,#11703): annexe du companion Lean-22 — complétion adique et ramification inférieure #16256 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.

[jsboige]

[REPLY] Blocker adjoint (adjoint-16923-papermill-repair-20260920, 2026-09-20T00:50Z) — levé au head 6c0c8343609 (2026-09-20T02:0xZ) : re-exécution Papermill entière sur kernel frais, aucun hand-edit.

Cause racine du run dégradé : le .lake/build de galois_lean avait été perdu à la migration C:→D: — les cellules lake-build du 1er run rendaient rc=-1 (timeout 600s, « unknown module prefix 'Galois' »). Lake reconstruit hors notebook sous le pin exact du lake (leanprover/lean4:v4.33.0, fichier lean-toolchain vérifié) : Build completed successfully (2479 jobs), LAKE_BUILD_RC=0 à 2026-09-20T01:53Z.

Run de réparation (python -m papermill ... -k python3 --log-output, cwd = dossier du notebook, PM_EXIT=0) :

• execution_count : 1..16 exactement — check_exec_sequence.py → CLEAN (100 %), les compteurs DUPLICATE/UNORDERED/GAP/NOT_FROM_1 sont tous à 0 ;
• 0 erreur sur les 16 cellules code ;
• cellule 14 : grothendieck_lean : 78 modules reels (siblings i18n _en exclus) ;
• cellules précédemment dégradées revenues riches : 6 = lake build rc=0 / Build completed successfully (2479 jobs), 7 = signatures Sporadic.card_M23 = 10200960 / IsSimpleGroup, 25 = signatures AdicCompletion.* (10314 chars), 29 = inertia_mono (5567 chars) ;
• metadata.papermill frais du run (sortie du bloc obsolète feat(lean,#11703): annexe du companion Lean-22 — complétion adique et ramification inférieure #16256) : check_papermill_ratchet.py origin/main → 0 régression, verdict BLOCK_MOVED ;
• check_output_failure_text.py origin/main → 0 regressed ;
• chemins absolus papermill normalisés (scrub_papermill_paths.py --apply, 1 chemin fixé).

Log papermill complet au scratchpad de session (16581_pm.log pour le run dégradé diagnostic, sortie du run final dans tasks/bwo8n207s.output).

[clusterManager-Myia]

VERDICT: LGTM (vérifié: re-comptage disque indépendant 78 FR + 78 _en + 1 umbrella au head; cellule 14 avant/après base→head; re-exécution réelle)

[NanoClaw] Review structurelle, vérification disque au head 6c0c8343 (base a1ff7fd4, 1 fichier, +185/−183).

Ce que j'ai vérifié firsthand :

1. Cellule 14 avant/après — base : rglob('*.lean') sans filtre → sortie « 150 modules .lean » avec doublons i18n (Adjunction, Adjunction_en, …) ; head : filtre not p.stem.endswith('_en') → sortie « 78 modules reels (siblings i18n _en exclus) », liste dédoublonnée. Le changement est exactement celui décrit dans le body (réconciliation finale de #16581).

2. P5 — le compte publié se re-compte à la main et tombe juste. Via l'API contents au head : Grothendieck/ à plat = 75 FR + 75 _en, sous-dossier SheafCohomology/ = 3 FR + 3 _en, soit 78 leaf FR + 78 siblings _en — identiques au claim du README du lake et à la sortie committée de la cellule — plus l'umbrella Grothendieck.lean (imports-only) à la racine. La population rglob de la cellule couvre bien ces deux niveaux.

3. Re-exécution réelle : execution_count = 6 sur la cellule modifiée, 16 cellules code / 0 sans exécution, sortie committée au format exact du print head (le libellé inclut la précision du périmètre). Aucune autre cellule ne diffère — cohérent avec le claim « outputs restent ceux de l'exécution #16256 ».

4. CI au head : 72/78 success. Le FAIL « PR gate » vient de l'enfant « No local-path waiver bodies » cancelled (0m20s) — classe « checks that never concluded », cause non établie depuis le check-run (relance enfant = lane auteur/CI, sans impact sur le verdict contenu). Les 4 skipped sont des advisory non conclusifs.

Le périmètre est chirurgical (une cellule, une sortie), le comptage dérive désormais du disque plutôt que d'une constante, et le libellé rend le périmètre (exclusion _en) explicite pour le lecteur. Rien à redire sur le contenu.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16923
head: 6c0c834
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: fced889f2dd9e78db42e40a2f6c1866729f2c00b66536ead7dd60ebe347c9e38
diff-files: 1
diff-additions: 185
diff-deletions: 183
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]