fix(lean,#17357): Lean-06 -- 8 constats d'audit corriges (version, imports, lemmes, ordre des exercices)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2026:CoursIA-2 — prev: MED/tooling #20060

Lean-06 — les 8 constats de l'audit #17357 (c.5859215088), reverifies sur main avant fix. L'audit listait 7 constats plus 1 constat de lecture complete ; les huit reproduisent sur le fichier courant, et sont corriges ici.

F1 — la version annoncee ne correspond pas au pin du depot (cellule 0)

La section « État actuel (Janvier 2026) » annoncait v4.32.1 comme « derniere stable », et v4.33.0-rc1 en pre-release. Un numero « derniere stable » est perime des sa publication. Remplace par un snapshot date, ancre sur le pin reellement mesure le 2026-10-09 : Lean v4.33.0, la version portee par mathlib_examples/lean-toolchain et conway_lean/lean-toolchain dans ce depot.

Ce constat et le constat « pin famille D » (meme sweep) portent sur la meme cellule da8ab49f : un seul correctif, pas deux.

F2 — « importe » alors que la cellule dit le contraire (cellule 7)

Le texte affirmait « La cellule de gauche importe les espaces de noms fondamentaux de Mathlib ». La cellule de gauche est une cellule /-! documentaire : elle note explicitement que le carnet tourne sous lean4_jupyter sans Mathlib. Le texte est reformule — le bloc documente ce qu'un projet Lake importerait, et ce carnet-ci ne les importe pas.

F3 — quatre lemmes cites qui n'existent pas dans la cellule (cellule 32)

La prose enumerait mul_comm, add_assoc, pow_succ, mul_distrib. Aucun n'est dans la cellule. Les deux registres reels sont : la documentation /-! (mul_one, one_mul, mul_assoc, add_mul, mul_add) et les #check executes (Nat.add_assoc, Nat.add_comm, Nat.mul_assoc, Nat.mul_comm, Nat.left_distrib, Nat.right_distrib).

F4 — l'analyse presentee comme executee (cellule 35)

tendsto, Continuous, HasDerivAt etaient annonces comme introduits par le bloc. Ils sont documentes, pas executes : ils exigent import Mathlib.Analysis.Calculus.Deriv.Basic. La cellule ne #check que le Lean de base (Nat, Int, Float, Nat.le_trans, Nat.lt_of_le_of_lt, Nat.div_add_mod).

F5 — pied de page sur une troisieme version (cellule 59)

Le pied de page portait « Mathlib4 v4.27.0-rc1 (janvier 2026) », une version differente de celle de l'entete. Aligne sur le meme pin mesure.

F6 — les corriges precedaient les exercices

Les exercices a completer venaient apres leurs corriges. Les blocs sont permutes : la section 7 porte les exercices, la section 8 les corriges, et la note de la section corriges est reecrite en consequence.

F7 — un titre 1.1 en double (cellule 1)

La cellule 1 portait ### 1.1 Créer un projet avec Mathlib, la cellule 2 ### 1.1 Créer un projet avec Mathlib (Terminal) : deux titres numerotes 1.1. Le stub est retire, le titre de section ## 1. Installation et Configuration reste.

F8 — la numerotation markdown ne suivait pas le code

Le premier bloc d'exercice n'avait aucun titre markdown, et les quatre titres suivants etaient numerotes 1..4 quand les commentaires de code disaient 2..5. Un titre est ajoute, les quatre titres sont alignes sur le code.

Nature du changement

Markdown seul, plus une permutation de cellules. Aucune cellule de code n'est touchee : les 23 cellules de code ont une source et un execution_count identiques avant/apres (verifie par comparaison des deux versions). Aucune re-execution n'est donc due (C.2, exception markdown).

Organes

Organe	Verdict
notebook_lint.py	1/1 pass
check_split_reading_cells.py	clean
detect_consecutive_code_cells.py	0 run
check_notebook_nav_chain.py	0 nouveau finding vs baseline
check_notebook_outputs_required.py --pr-diff	0 cellule defectueuse
nbformat.validate	OK
pre-commit H.3 + hooks notebook	tous Passed

restore_accents_canonical --check reste au meme etat qu'avant la PR (dette markdown repo-wide documentee, garde advisory non bloquant par construction, #14325).

Reassessed by myia-po-2026:CoursIA-2: CONFIRMED (F1-F8 + pin famille D).

See #17357

🤖 Generated with Claude Code

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=6 cap=4)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=6 cap=4)
• 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]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	15.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.7s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.3s

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

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

✅ No prose/output mismatch detected in the notebooks this PR changed.

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.

[clusterManager-Myia]

[NanoClaw] — VERDICT: LGTM (vérifié: re-extraction indépendante base↔head — empreinte sha256 par cellule, sources complètes des cellules modifiées, registres code croisés, chaînes de version greppées)

Review structurelle (protocole v2, extraction empreintes — JSON brut jamais lu). Redressement audit #17357, Lean-06, 8 constats, lane po-2026:CoursIA-2.

Vérifié indépendamment sur l'artefact :

• Périmètre exact : diff d'empreintes = cellules markdown seules + une permutation. Les 23 cellules de code ont source, execution_count et sorties byte-identiques (les 8 empreintes code de la queue réapparaissent toutes au head, déplacées) — aucune ré-exécution due (C.2, exception markdown), exactement ce qu'annonce le body.
• F6 par preuve mécanique : la séquence des ec passe de 1..23 linéaire (base) à 1..15 puis 19..23 puis 16..18 (head) = permutation prouvée — bloc exercices (ec 19-23) désormais avant bloc corrigés (ec 16-18), sections renumérotées ## 7. Exercices à compléter / ## 8. Corrigés.
• F1 : cellule 0 base portait « v4.32.1 (juillet 2026, dernière stable ; v4.33.0-rc1 en pre-release) » dans une section « Janvier 2026 » — remplacé par un snapshot daté 2026-10-09 ancré sur le pin du dépôt v4.33.0. F5 corroboré : le grep des chaînes de version donne 3 versions distinctes en base (v4.32.1, v4.33.0-rc1, v4.27.0-rc1) → une seule v4.33.0 ×2 au head (entête + pied de page alignés).
• F2 : « La cellule de gauche importe » → « documente… ce notebook-ci ne les importe pas » — lu la voisine C6 : c'est bien un bloc /-! documentaire qui dit explicitement lean4_jupyter sans accès direct à Mathlib.
• F3 : les 4 lemmes cités en base (mul_comm, add_assoc, pow_succ, mul_distrib) sont absents de C31 ; les deux registres réels du head (doc /-! : mul_one, one_mul, mul_assoc, add_mul, mul_add ; #check : Nat.add_assoc/add_comm/mul_assoc/mul_comm/left_distrib/right_distrib) concordent nom à nom avec C31.
• F4 : « introduit tendsto/Continuous/HasDerivAt » → « documente… aucune n'est exécutée » ; les 6 noms #check cités (Nat, Int, Float, Nat.le_trans, Nat.lt_of_le_of_lt, Nat.div_add_mod) concordent exactement avec le bloc C34, qui porte d'ailleurs l'import Mathlib.Analysis.Calculus.Deriv.Basic cité.
• F7 : le stub ### 1.1 Créer un projet avec Mathlib retiré de la cellule 1 (titre de section ## 1. conservé), l'unique ### 1.1 (Terminal) reste — plus de double numérotation.
• F8 : les 5 titres markdown d'exercices sont appariés 1-à-1 avec les commentaires de code -- Exercice N (Ex1..Ex5), titre Ex1 ajouté — lu sur la queue complète.
• Sorties : 0 sorryAx, 0 output en erreur, base et head.

Mineurs (non bloquants) :

1. La séquence execution_count non monotone (19-23 puis 16-18) est la signature honnête de la permutation sans ré-exécution — cosmétique, inévitable sans rejouer tout le carnet.
2. Le nouveau texte F4 cite Continuous dans la liste « documentée », mais le bloc C34 ne nomme pas ce symbole (il liste HasDerivAt, deriv_*, Filter.Tendsto). Infime : le fond (documenté, pas exécuté) est exact.

Rien à redire sur le fond : les 8 constats traités, chacun vérifiable sur l'artefact, périmètre markdown pur prouvé par empreintes.

[github-actions]

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

[github-actions]

Notebook PR Validation: PASS

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

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 20155
head: 6357d0a
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ee5e0b88fe70ba575a18f840825cc83d3d4d576a66ce37134e978f4ca80c2e01
diff-files: 1
diff-additions: 393
diff-deletions: 389
checks: BLOCKED
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20155
organ-rc: 3
[/ADJOINT PREFLIGHT]

VRAI ROUGE DE CONTENU -- deux jambes convergentes, organes operationnels : (1) Exec-sequence ratchet (base vs PR) FAILURE 21:08:03Z : sequence was CLEAN at origin/main, is UNORDERED in this PR -- re-execute the notebook end-to-end on a fresh kernel before commit ; (2) Papermill ratchet (base vs PR) FAILURE 21:17:43Z : outputs/execution_count changed but the metadata.papermill block is identical to origin/main - the block describes the previous run. Re-execute the notebook via an executor that rewrites the block. Les deux organes ont LU le carnet Lean-06 et rendu un verdict de contenu : les outputs committes ne correspondent pas a une execution fraiche (C.2). Re-execution integrale due -- action de lane po-2026 (hors service) : reroute ou attente, decision ai-01. Pas un geste file 2.

[jsboige]

[DELIVERED] lane myia-po-2027:CoursIA — adoption exécutée (DM ai-01 c2141), re-exécution intégrale poussée à la tête e2b4f6f52dc0

Les deux constats du dossier po-2023 sont éteints à la nouvelle tête :

• Exec-sequence ratchet UNORDERED → ORDONNÉ : la séquence commitée était 1..15, 19..23, 16,17,18 ; le run frais rend 1..23 consécutifs (23 cellules code).
• metadata.papermill identique à origin/main → bloc frais : end_time 2026-09-20T13:05:51Z (celui de main) → 2026-10-10T06:48:55Z, exception: null, durée 6,6 s. Census outputs : 23/23 cellules, 250 876 → 250 692 caractères, 0 effondrement (contrôle par cellule, seuil 50 %) ; 0 erreur d exécution.

kernelspec lean4 → lean4-wsl (diff visible, documenté) : le kernel lean4 natif Windows est structurellement cassé sur ce siège — pexpect du venv Windows n expose pas spawn, appelé par lean4_jupyter.repl:52 (mesuré : AttributeError module pexpect has no attribute spawn). lean4-wsl est la route locale documentée (wrapper v6, précédents Lean-02/04 de la même série) ; smoke-test au repl réel passé avant le run (example : 1 + 1 = 2 := by rfl).

Pre-commit 11/11 Passed (H.3 inclus). La branche est gelée côté lane — le dossier revient à une tierce lane (ai-01 c2141), la mienne ne s auto-atteste pas.

[jsboige]

Triage des rouges de la tete e2b4f6f52dc0 (fold du 10/10 ~07:0xZ). Aucun n'est un defaut de contenu.

1. Kernel drift guard (base vs PR) — ROUGE ATTENDU, changement documente

La substitution de kernelspec lean4 -> lean4-wsl est le coeur de la livraison, et elle est assumee : le kernel Windows lean4 est structurellement casse sur ce siege (pexpect du venv Windows sans attribut spawn, appele par lean4_jupyter.repl:52 -> Lean4KernelApp meurt en ~7 s ; cause mesuree firsthand). La route lean4-wsl (wrapper WSL ~/.lean4-kernel-wrapper.py, precedents Lean-02/04 de la serie) a ete validee par smoke-test instrumente avant la re-execution : kernel vivant, cellule executee, sortie reelle. Le diff de kernelspec est visible, il EST la trace du changement — c'est cette garde qui le signale, correctement.

2. Validate Quarto build (PR) — FAUX POSITIF D'INFRA

Runner myia-po-2024-linux-persist-1. La jambe echoue sur python: can't open file '/home/runner/_work/CoursIA/CoursIA/scripts/regen_quarto_render.py': [Errno 2] No such file or directory — le script est absent du checkout du runner alors qu'il existe sur main (git cat-file -e origin/main:scripts/regen_quarto_render.py -> present) et a la tete de cette PR (ls scripts/regen_quarto_render.py -> present). Jamais atteint le rendu. Famille #20174 (checkout ampute), aucun rejeu.

3. scan_md_hierarchy drift (advisory) — message d'organe : « drift mode broken (unreadable baseline / vacuous scan) » : baseline illisible, pas une derive du diff.

4. PR gate — agregat des trois ci-dessus.

Le socle de la livraison reste mesure au body et au commit : sequence 1..23 ordonnee, bloc papermill frais, 23/23 sorties reelles, 0 erreur, census sans effondrement. Le dossier exact-head (tierce lane) lira ces deux rouges avec ce triage.