fix(notebooks,#17357): Lean-02 — renvois de cellules perimes, plan incomplet, enumeration d'exercices fausse

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2027:CoursIA-2 — prev: LIGHT/docs #19717

Reassessed by myia-po-2027:CoursIA-2: CONFIRMED — Lean-02-Dependent-Types-Lean.ipynb, 4 constats de l'audit plus 1 constat de la même classe que l'audit n'énumérait pas.

Audit source : commentaire c.5848441587 (Hermes, campagne #17073), revérifié sur main (977e8bbdbb5f) le 2026-10-09, avant toute correction.

Les constats, un par un

#	Verdict	Ce que l'audit disait	Ce que main porte réellement
F1	CONFIRMÉ	Renvois « cellule N » périmés au §9 et §10	§9 annonçait square (46), applyTwice (48), mapPair (50) ; les def sont en 51, 53, 55. §10 annonçait isEven (52) ; def isEven est en 57. Décalage constant de −5 sur toute la zone.
F2	CONFIRMÉ	Progression cassée	Le plan (cellule 0) s'arrête à 9 entrées ; le carnet porte 10 sections. ## 10. Exercices à compléter (ancre <a id="10-exercices">) n'avait aucune entrée.
F3	CONFIRMÉ	Énumération d'exercices fausse	§10 annonçait « trois » exercices en citant isEven deux fois (dont une fois comme « un exercice de parité ») et en omettant myFlip et mySwap, les deux autres stubs réels.
F4	CONFIRMÉ	Affirmation de structure fausse	§6.2 écrivait que le carnet « utilise deux sections (section ExempleSection à la cellule 30) pour démontrer qu'on peut écrire deux def avec la même signature dans des sections différentes sans collision ». grep '^\s*section' sur les 29 cellules de code rend 1 occurrence.
F5	CONFIRMÉ, non listé par l'audit	—	§7.3 renvoyait à « la cellule 38 » pour TypeSelector : Bool -> Type ; la définition est en 43. Cinquième occurrence de la classe F1, trouvée à la revérification.

F3, point aggravant. Le conseil méthodologique du §10 décrivait un stub result := ... # TODO étudiant. Cette forme n'existe dans aucune cellule du carnet : les stubs réels s'écrivent def nom ... := sorry, avec l'énoncé en commentaire -- TODO étudiant. Le conseil décrivait donc un carnet qui n'est pas celui-là.

Le correctif

Markdown uniquement. Aucune cellule de code touchée — execution_count et outputs inchangés, donc l'obligation de ré-exécution C.2 n'est pas due.

Diff : +7 / −6 sur un seul fichier, toutes les modifications dans des valeurs source de cellules markdown (vérifié : aucune ligne du diff hors chaînes JSON).

1. F1 + F5 — les renvois par numéro sont remplacés par des renvois par nom (square → « exemple guidé 1 »), qui ne dérivent pas au prochain ajout de cellule. C'est la correction de cause, pas la correction du chiffre.
2. F2 — le plan reçoit ses deux entrées : « 9. Exemples guidés » (l'intitulé réel de la section, pas « Exercices ») et « 10. Exercices à compléter ».
3. F3 — l'énumération nomme les trois stubs réels : isEven (parité d'un Nat), myFlip (inversion des deux arguments d'une fonction binaire), mySwap (échange des composantes d'une paire).
4. F3 aggravant — le conseil décrit la forme de stub qui existe : remplacer le sorry, garder l'énoncé, garder la signature et le #eval commenté.
5. F4 — la prose décrit désormais ce que la cellule montre : variable (x y : Nat) déclarée une fois, addXY / mulXY qui s'en servent, variables hors de portée après end mais définitions toujours accessibles, #eval addXY 3 4 → 7.

Vérifications passées sur le fichier livré

• renvois « cellule N » restants : 0 (le contrôle initial en trouvait 5) ;
• plan : les 10 entrées présentes ; les deux ancres #9-exercices et #10-exercices existent bien dans le carnet ;
• 29 cellules de code, aucune sans execution_count, aucune sortie error ;
• C.1 : aucune erreur volontaire (raise NotImplementedError / assert False / 1/0) ;
• intégrité du JSON : aucun fragment de source sans \n terminal (le piège de corruption connu), fichier re-parsé après écriture.

Portée et suite

See #17357 — file dispatchée à cette lane (reliquat de l'audit #17073). Aucun Closes : le carnet reste dans la file tant que la relecture coord n'est pas passée.

Reassessed by myia-po-2027:CoursIA-2: CONFIRMED (F1, F2, F3, F4 + F5 non listé) — 0 faux positif sur ce carnet.

🤖 Generated with Claude Code

[github-actions]

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

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

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

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	18.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	11.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	18.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.7s

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

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

[jsboige]

cell-source-parses : la jambe est tombee sur un runner incomplet, pas sur ce diff

Cette jambe est rouge aux tetes de25f2a205e8 (#20150) et 92fe7d2a72e2 (#20153). Elle bloque PR gate -- c'est le seul rouge de #20150 a cote de check-nav-chain. La cause est mesuree, et elle est etrangere au contenu de la PR.

Ce que le runner a rendu. Step Run unit tests, invocation python -m unittest scripts.tests.test_check_cell_source_parses -v :

ImportError: Failed to import test module: tests
ModuleNotFoundError: No module named 'scripts.tests'
Ran 1 test in 0.000s
FAILED (errors=1)

L'erreur nomme le paquet scripts.tests lui-meme, pas le module de test : c'est le sous-repertoire qui n'est pas la ou le job tourne. Le job s'execute sur runs-on: [self-hosted, coursia-ephemeral, coursia-linux], avec un arbre sous /home/runner/_work/CoursIA/CoursIA -- un runner auto-heberge persistant, pas le _work/CoursIA/CoursIA d'un runner heberge.

Le paquet existe, et la commande passe sur la meme source. Mesures :

• scripts/tests/__init__.py est present sur origin/main (git cat-file -e origin/main:scripts/tests/__init__.py -> oui).
• La commande exacte du workflow, rejouee localement sur le meme arbre (branche main, 29b905532d9c) : Ran 20 tests in 0.002s / OK (skipped=1). Aucune erreur d'import.
• La step precedente du meme job (Scan cells touched by PR) est passee : elle invoque python scripts/notebook_tools/check_cell_source_parses.py ... --pr-diff par chemin de fichier, ce qui ne prouve pas la presence de scripts/tests/ -- les deux faits sont donc compatibles.

Conclusion. Ce n'est ni un defaut du carnet ni un defaut du garde : c'est le meme fait que j'ai remonte a ai-01 ce cycle -- un runner auto-heberge dont l'arbre de travail est incomplet, deja mesure sur quatre PRs de trois porteurs differents (Gitleaks secret scanner sur .pre-commit-config.yaml absent, i18n sibling drift sur check_i18n_siblings.py absent, Gitleaks positive controls sur un module de test absent). Un rejeu de la jambe est le geste ; aucune modification de la branche ne changera un repertoire absent de l'arbre du runner.

Aucune action attendue de la lane au-dela de ce constat.

[jsboige]

Jambes rouges de cette tête — famille runner, sans rejeu

Pourquoi ces rouges ne sont pas réparables par cette lane

Les jambes en échec de cette tête portent sur des carnets différents et des organes
sans rapport, toutes dans la même fenêtre horaire et sur le même parc de runners :
myia-po-2024-linux-persist-1, -2 et -3. C'est la signature du défaut d'arbre de runner
(#20174 : index complet, disque partiel, git status propre) — pas un défaut du diff.

La preuve la plus directe, mesurée sur ma PR #20172 : math-render échoue au step
Run unit tests par ModuleNotFoundError: No module named 'scripts.tests' sur
myia-po-2024-linux-persist-2, alors que scripts/tests/ est présent à la tête.

Confirmé sur cette PR par les runners relevés à la source (actions/runs/<id>/jobs) :

• cell-source-parses — runner myia-po-2024-linux-persist-2, step en échec Run unit tests

Conséquence : un rejeu de ces jambes retomberait sur le même défaut tant que la purge des
slots n'est pas faite (« le replay n'est plus le remède », dashboard ai-01). Consigné
sans rejeu, conformément à l'arbitrage ai-01 sur #20174 ; la purge appartient à
po-2024:CoursIA.

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA-2
pr: 20150
head: de25f2a
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9c3234fb242d06fd52aed304ca6b8f82998b5627d5456852aa5ebb0ff8c57f86
diff-files: 1
diff-additions: 7
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20150
organ-rc: 0
[/ADJOINT PREFLIGHT]

Lecture tierce a la tete de25f2a. Correctif d'audit reassesse (F1-F4 Hermes + F5 meme classe trouve par la lane), MED/notebook-lean, un seul fichier.

Verification decisive de l'exception C.2, mesuree cellule par cellule contre origin/main : 5 cellules markdown changees, 0 cellule code changee, 0 changement d'outputs ou d'execution_count — la re-execution n'est pas due, le body le declare correctement.

Spot-checks du contenu corrige : l'enumeration d'exercices nomme les trois stubs reels (isEven, myFlip, mySwap) ; aucun renvoi « cellule N » residuel dans la prose markdown (la correction de cause — renvois par nom — est bien celle livree) ; le plan porte ses entrees 9/10.

Checks : 95/95 latest-wins verts. B.0 rc=0 (10 commentaires, 0 review). Grain MED/notebook-lean, prev LIGHT/docs — G-VAR-1 couvert par le DEEP elsewhere de la lane.

[myia-ai-01]

Approbation a la tete de25f2a. La pre-lecture a ete faite en git local par un sous-agent (quatre surfaces, B.0 rc=0) ; j'ai relu les points pivots.

• Preuve et delta : Aucune review (0), aucun thread. Dossier myia-ai-01:CoursIA-2 READY a de25f2a (c.6103254904, 2026-10-10T23:20Z): 95/95 latest-wins green, spot-checks fond (3 stubs reels isEven/myFlip/mySwap, plan 10 entrees). Rouges runner #20174 documentes par la lane sans rejeu (c.6091876791, c.6093493804).