fix(lean,#9768): KNOTS-03 -- prose exercice 2 realignee sur la baseline CI reelle (9 -> 8)

[jsboige]

Grain: MED/notebook-python — lane myia-po-2025:CoursIA — prev: DEEP/notebook-dotnet #20268

Correctif du finding n°1 de la tranche d'audit Phase 0 famille SymbolicAI/Lean (9e famille, EPIC #9768) : la prose de l'exercice 2 de KNOTS-03 restait ancrée sur une baseline CI périmée (9) alors que la baseline réelle est 8 depuis #19107 (verifyMoves_sound prouvée, sorry-baseline: "9" → "8" dans lean-knot.yml ligne 170).

Changements (cellules 37 et 38 uniquement)

• md cell[37] : « Le CI gate sur 9 sorries réels (lean-knot.yml sorry-baseline: "9", post-feat(lean,#18611): scaffold ReidemeisterCombinatorial -- MoveSequence + movesConnects + verifyMoves (squelette d'organe) #18615) » → « 8 sorries réels (lean-knot.yml sorry-baseline: "8", post-Fix(lean,#2874): verifyMoves_sound prouvee — sorry 9 -> 8 distinct sur knot_lean #19107) » ; l'indice remplace « comparé à la constante 9 » par « constante 8 ».
• code cell[38] (exercice, stub) : BASELINE = 9 → BASELINE = 8, consigne « confrontez le compte réel à la baseline CI (8) » ; stub C.1 conforme (pass, aucune erreur volontaire).

Un étudiant qui faisait l'exercice correctement trouvait 8, le comparait à 9 comme la consigne l'exigeait, et concluait à une régression qui n'existe pas.

Diagnostic dérive (C.4)

• Cause : changement de valeur de référence en amont non propagé à la prose — la baseline CI est passée de 9 à 8 le 04/10 (Fix(lean,#2874): verifyMoves_sound prouvee — sorry 9 -> 8 distinct sur knot_lean #19107), la re-exécution du 09/10 (fix(lean,#19480): errors="replace" sur le probe subprocess de KNOTS-03 + re-exec C.2 #19872) a rafraîchi les outputs (qui mesurent bien 8) sans réaligner la prose de l'exercice ni sa constante. Apparenté (d) régression dépendance (dépendance à une valeur de config externe au notebook) ; ni (a) env/kernel, ni (b) claim fabriquée d'origine (le 9 était exact avant Fix(lean,#2874): verifyMoves_sound prouvee — sorry 9 -> 8 distinct sur knot_lean #19107), ni (c) moteur, ni (e) stochasticité.
• Verdict : CAUSE_FIXED — la valeur ré-alignée (8) est doublement ancrée : lean-knot.yml ligne 170 (sorry-baseline: "8") et les outputs re-exécutés de ce PR (TOTAL sorry réel = 8 : Lidman 2 + Reidemeister 2 + Slice 4).

Preuve d'exécution réelle (C.2, D.1-D.3)

• Re-exécution complète via MCP jupyter-papermill (kernel python3, cwd = dossier du notebook) : 14/14 cellules, 0 échec, execution_count 1-14 partout, outputs committés.
• Grep erreurs volontaires : aucune (raise NotImplementedError / assert False / 1/0 absents ; le stub de l'exercice est BASELINE = 8 + pass).
• Comparaison systématique old vs new : les sources ne diffèrent que sur les cellules [37, 38] ; aucune cellule # Solution / # Exemple résolu touchée.
• La re-exécution a aussi rafraîchi les sorties des cellules [2, 11, 18, 21, 30, 33], qui mesurent l'état du lake knot_lean : elles avaient dérivé depuis fix(lean,#19480): errors="replace" sur le probe subprocess de KNOTS-03 + re-exec C.2 #19872 car le lake a avancé (feat(lean,#18397): tranche 3 -- extraction arcPartition vers Knots/ArcPartition.lean (sibling EN) #19284 : extraction ArcPartition.lean → 15 modules FR, nouvelles déclarations dans ReidemeisterMoves/Combinatorial, paires i18n 15/15 → 16/16 byte-identical). Aucune sortie ne se réduit (ratchet output-collapse : croissance uniquement) ; l'invariant de l'exercice — total sorry réel = 8 — est inchangé d'un bout à l'autre.

Non couvert

Finding n°2 de la tranche (Lean-16j, contradiction qualitative « pas de Classical.choice » vs output depends on axioms: [propext, Classical.choice, Quot.sound]) : laissé à une passe de prose sur la série, non bloquant — voir rapport d'audit c.6098508609 sur #9768.

See #9768 — l'EPIC n'est pas résolue par cette PR seule (correctif du finding n°1 de la 9e famille uniquement).

🤖 Generated with Claude Code

[github-actions]

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

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

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

prev: genre mot-clé fermant (#10093) — LEVÉ (2026-10-10T17:12:17Z).

aucun genre mots-clé fermant dans le body ni les commits ; prev: accepté(s) : #20268

Run vert du garde : ce commentaire bloquant est obsolète. Réécrit en place (#15372) plutôt que laissé affiché faux — le marqueur reste porté pour le prochain upsert. Historique : runs Always-on guards de la PR.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20276 (fix(lean,#9768): KNOTS-03 -- prose exercice 2 realignee sur la baseline CI reelle (9 -> 8)) 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 -- fix(lean,#19480): errors="replace" sur le probe subprocess de KNOTS-03 + re-exec C.2 #19872 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb, recouvrement de chemins 100% -- fix(lean,#19480): errors="replace" sur le probe subprocess de KNOTS-03 + re-exec C.2 #19872 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]

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.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.2s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	15.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.8s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.7s

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 14
• 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-2027:CoursIA
pr: 20276
head: 06704b0
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 775c15a7e80553b1e176714309af9afc9ff12e2c20db4333bdad3489849eadd9
diff-files: 1
diff-additions: 348
diff-deletions: 287
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20276
organ-rc: 0
[/ADJOINT PREFLIGHT]

[myia-ai-01]

Approbation a la tete 06704b0. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.

• Preuve du claim central : present: C.4 diagnostic CAUSE_FIXED with double anchor (lean-knot.yml l.170 sorry-baseline '8' post-#19107 + re-executed outputs TOTAL sorry reel = 8: Lidman 2 + Reidemeister 2 + Slice 4); no # Solution cell touched
• Execution : KNOTS-03 (14 code cells): ec 1-14, 0 errors; changed code cell 38 is the exercise stub (ec=13, no output — same as on main by design); sources differ from main only on cells 37/38; re-exec refreshed lake-state outputs of cells 2,11,18,21,30,33 (growth only per body)
• Aucune violation C.1, aucun recit d'activite ajoute.

La baseline 8 est confirmee sur main (lean-knot.yml l.170, sorry-baseline: "8").