fix(17357): ANALYSE-02-Tao -- retirer la fuite de solution F1 (script mul_comm de l'exercice 2)

[jsboige]

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

Objet

ANALYSE-02-Tao-Lean-Python.ipynb — retrait de la fuite de solution F1 de l'audit #17357 (re-assessment protocole).

Reassessed by myia-po-2025:CoursIA: CONFIRMED (F1 — solution-leak)

Re-assessment (firsthand, contre main)

• Constat F1 : la cellule 82528214 (Code 6.2 — Exercice 2 « preuve de mul_comm from scratch ») contenait en commentaire le script Lean complet de la double induction (theorem mul_comm … induction a … rw [Nat.mul_succ, ih, Nat.add_comm, ih_b]) — soit la réponse de l'exercice livrée avec l'énoncé, en contradiction avec la vocation « TODO étudiant » de la cellule. Vérifié par lecture directe de la cellule sur main (audit [Audit #17073] Série Lean — partition Hermes #17357, constat F1).
• Classification : CONFIRMED pedagogy — fuite réelle, pas un faux positif de scanner.

Correctif

• Le bloc verbatim est remplacé par trois lignes non-fuyantes : le script final n'est pas donné (c'est l'objet de l'exercice), construire la double induction d'après les indices, puis confronter sa preuve à Section_2_3.lean du lac source après coup.
• Conservé : le # TODO étudiant, les indices 1-3 (add_comm → add_assoc → mul_comm), le pass # stub pedagogique (regle C.1), les trois print de sortie.
• Portée : seule la source de la cellule 82528214 change ; les 12 cellules markdown sont byte-identiques ; aucun autre code cell modifié (vérifié par diff programmatique base↔head).

Validation (C.2)

• Re-exécution complète via notebook_tools.py execute --kernel python3 : SUCCESS (36 s, y compris la cellule Code 5.2 qui invoque le lac teorth/analysis sous WSL).
• 9/9 cellules code : execution_count 1-9, toutes avec outputs, 0 erreur ; la sortie #print axioms (sorryAx, intermediate_value) est intacte.
• Sortie de la cellule modifiée inchangée (les 3 print ne dépendent pas du bloc retiré).
• Chemins metadata.papermill normalisés au basename (tolérance admise n°1).
• Hooks pre-commit : tous PASS (gitleaks, H.3, source-parses, scrub papermill).

Forme c1640 (PR mono-carnet, justifiée)

La directive c1640 demande des PR groupées par série (3-6 carnets). Sur la file #17357 de cette lane, les deux autres carnets actionnables sont gated : Lean-12-Sensitivity (F1) et Lean-16f-Conway (F2-F3) attendent le merge de #19665. ANALYSE-02-Tao est donc le seul carnet actionnable de la file à cet instant — une PR mono-carnet est la forme correcte ; les deux gated formeront une PR groupée dès que #19665 sera mergé.

See #17357

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

⚠️ 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.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	6.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	8.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	8.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	6.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	5.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	49.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	4.9s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	23.1s

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

[github-actions]

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20144 (fix(17357): ANALYSE-02-Tao -- retirer la fuite de solution F1 (script mul_comm de l'exercice 2)) 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.

• fort -- docs(analyse,#17357): retirer la preuve Lean 4 verbatim du stub mul_comm (ANALYSE-02-Tao) #20109 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb (issues communes : [Audit #17073] Série Lean — partition Hermes #17357)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 9
• 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-ai-01:CoursIA-2
pr: 20144
head: e15159a
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: bb707733fea4d7cdc941ca6519a92a00986a38ff191fa0da7dc49206e9eed613
diff-files: 1
diff-additions: 122
diff-deletions: 119
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 20144
organ-rc: 0
[/ADJOINT PREFLIGHT]

Lecture tierce complete (body, 8 commentaires, 0 review, 0 thread, diff integral a la tete exacte).

• checks : 95 jambes / 95 noms, latest-wins-green au head e15159ad22, aucun rouge residuel. PR gate vert a 23:21:03Z.
• b0 : check_unaddressed_nits.py 20144 -> rc=0, aucun nit non leve ; aucune review, aucun thread inline.
• scope : 1 fichier — SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb, +122/-119. See #17357 sans cloture. La forme mono-carnet est justifiee dans le body (les deux autres carnets de la file sont gated sur fix(lean,#18329): re-exécution Lean-12/16f sous python3-lean 3.13.16 — Lean-13 retiré (suivi #20065) #19665).
• domain : MED/notebook-python. Re-execution revendiquee (9/9 cellules, execution_count 1-9, 0 erreur) ; le retrait de la fuite de solution F1 est documente Reassessed by myia-po-2025:CoursIA: CONFIRMED avec le constat, la classification et ce qui est conserve (# TODO, indices, stub C.1). Normalisation metadata.papermill au basename = tolerance admise n°1.