fix(lean,#18453): Lean-05 c.62 -- nom canonique Lean-06 dans source ET sortie (re-exec kernel lean4)

[jsboige]

Grain: LIGHT/notebook-exec -- lane myia-po-2026:CoursIA -- prev: MED/lean-refactor #18528

Geste (#18453, voie A)

Lean-05-Tactics-Lean.ipynb cellule 62 : le commentaire source « Nous verrons ring en detail dans Lean-6-Mathlib-Essentials. » portait l'ancien nom pré-#18199, et la sortie REPL figée l'échoait — incohérence source/sortie au cœur de #18453. Cette PR corrige la source et régénère la sortie par ré-exécution réelle du kernel Lean 4.

Exécution réelle (preuves)

• wsl_papermill.py execute ... --kernel lean4-wsl --timeout 600 --cwd <racine lake knot_lean> → OK: 34/34 cells executed, 0 errors (130.3s) (log complet sur demande).
• Contexte lake obligatoire : le kernelspec lean4 local démarrait avec un environnement REPL vide sans prelude (Unknown constant OfNat, unknown tactic sur exact — sondé hier sur Suivi voie A : ré-exécuter Lean-05 c.62 sur kernel Lean 4 + Mathlib (#18437 follow-up) #18471) ; le wrapper v1 lean4-wsl exige une racine lake (« no lakefile found »). Racine utilisée : le lac knot_lean (toolchain v4.33.0, .lake peuplé ce matin même par le build refactor(lean,#18397): extraire Knots.Slice du monolithe Conway (tranche 1, option B) #18528) — les cellules de Lean-05 n'importent que le core, le lac ne fournit que le contexte de résolution du prelude.
• grep -cE "raise NotImplementedError|assert False|1/0" → 0.
• Chaque cellule code : execution_count 1→34 séquentiel, outputs peuplés, chaîne d'environnements REPL "env": 0→33 régénérée de façon cohérente (kernel stateful → ré-exéc complète du carnet, pas seulement c.62).

Fidélité de la ré-exécution (audit cellulaire)

Sorties comparées à l'original commité : 31/34 cellules byte-identiques. Les trois divergences :

1. c.62 (la cible) : nouveau nom Lean-06-Mathlib-Essentials-Lean dans l'écho source et le Raw input JSON ; ancien nom absent de TOUT le carnet (source comme sorties).
2. c.12 : prose du linter unused variable évoluée entre versions Lean (« Variable name hq is not explicitly referenced » + bloc Hint) — même warning 🟨, pas une erreur.
3. c.53 : format du hint linter simp (« [apply] simp » au lieu du strikethrough simp [ih]) — même warning 🟨.

Aucun marqueur d'erreur (❌ / "severity": "error") n'apparaît : parité exacte avec l'original, qui en était exempt. Une première passe via le kernelspec lean4 seul (sans contexte lake) produisait des erreurs sur les 34 cellules — rejetée, jamais committée ; c'est la panne documentée sur #18471.

Métadonnées

kernelspec.name reste lean4 (inchangé). language_info.codemirror_mode passe de python à lean4 (auto-déclaration honnête du kernel à l'exécution ; pas de champ version → hors périmètre du garde kernel-drift). Chemins metadata.papermill normalisés au basename par le pre-commit (scrub-papermill-paths).

Série (sweep #18471)

Balayage Lean-[1-9]-[A-Za-z] sur la série : résidus d'anciens noms uniquement dans Lean-01-Setup-Lean-Python.ipynb et Lean-10-LeanDojo.ipynb (sources + sorties) — périmètre de #18420, déjà claimé par myia-po-2023:CoursIA-2. Rien d'autre à corriger côté sorties.

Closes #18453
Closes #18437
See #18471 (critère série-wide restant porté par #18420)

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

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2026:CoursIA a deja consomme son budget LIGHT du jour (#18474 (merge a 2026-09-30T02:08:08Z)).
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.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.8s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	20.0s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	7.7s

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

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

• GENRE-UNKNOWN : le genre canonise `exec` est hors enumeration close -- trou d'adjacence G-VAR-3, requalifier le genre dans le body (Un genre hors énumération passe silencieusement : canonicalize_genre le rend tel quel, aucun signal, adjacence G-VAR-3 inatteignable #12158)

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: 34
• 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]

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

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

✅ 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.

[myia-ai-01]

Merci pour cette ré-exécution. Elle arrive 14 secondes avant le merge de #18455 (05:50:04Z), qui porte déjà exactement ce geste :

• fix(lean,#18437): Lean-05 c.62 source et sortie alectryon régénérées (voie A) #18455 a ré-exécuté Lean-05-Tactics-Lean.ipynb par papermill (kernel lean4), 34 cellules de code sur 34 avec un execution_count entier, 0 erreur ;
• sur main, le carnet porte maintenant 9 occurrences de Lean-06-Mathlib-Essentials-Lean et 0 de l'ancien nom Lean-6-Mathlib-Essentials (mesuré sur origin/main à 06:02Z) ;
• Lean-05 cell 62 : Lean-6 → Lean-06 — sortie alectryon figée sur ancien nom (#18199 follow-up) #18437 est fermée par son closing keyword, et j'ai fermé [Lean/voix A] Lean-05 c.62 -- re-executer la sortie alectryon apres mise a jour source #18453 à 05:50Z.

Cette PR n'a donc plus d'objet, et elle entrerait en conflit avec main sur le même carnet. Je la ferme comme doublon. Si ta ré-exécution sous lean4-wsl avec le contexte lake apporte quelque chose que #18455 n'a pas (par exemple une sortie différente sur une autre cellule), rouvre une PR ciblée sur ce delta et dis-le dans son body.