docs(analyse,#17357): retirer la preuve Lean 4 verbatim du stub mul_comm (ANALYSE-02-Tao)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-lean #20105

See #17357 — cinquième carnet de la file dispatchée (DM ai-01 13:29Z, tableau c.6081858350). Carnet : ANALYSE-02-Tao-Lean-Python.ipynb (ex Lean-19-Analysis-I-Tao-Workflow.ipynb, rang 2 de l'audit c.5851352755).

Reassessed by myia-po-2025:CoursIA: CONFIRMED (F1) — revérifié firsthand sur main à la tête 19303c100d avant tout fix, conformément au protocole audit-reassessment.

Re-vérification

• F1 CONFIRMÉ (solution-leak, cellule 17 82528214, exec 8) — l'énoncé §6.2 (« Implementer Nat.mul_comm from scratch… Prouver mul_comm a b = mul b a par double induction ») demande à l'apprenant de construire la preuve ; le stub la livrait mot pour mot en commentaires — les deux inductions imbriquées, simp [Nat.succ_mul, Nat.mul_succ] et rw [Nat.mul_succ, ih, Nat.add_comm, ih_b]. Il ne restait qu'à recopier, l'effort visé était neutralisé.
  Contraste vérifié : les stubs des exercices 1 (cellule 15) et 3 (cellule 19) ne donnent que méthode et sources (commandes git log --follow, liste des trois formalisations à comparer), jamais la réponse. Le défaut est donc confiné à la cellule 17 — une cause, un constat.

Le fix

• Cellule 17 — le bloc # En Lean 4 natif : (9 lignes : le theorem … := by et tout son script de tactiques) est retiré. Le plan d'étapes déjà présent est conservé tel quel — 1. add_comm, 2. add_assoc, 3. mul_comm par double induction en réutilisant les deux lemmes — et la ligne TODO est reformulée : « construire la preuve soi-même, puis la confronter à celle du lac », là où elle invitait à « voir la preuve de Tao » (c'est-à-dire à la recopier). Aucun ajout au-delà : l'énoncé, la docstring et les trois print sont inchangés.

Vérifications

• C.2 (cellule code modifiée → ré-exécution) : la cellule 17 est une cellule code (ses commentaires portent le stub), donc la ré-exécution est due. Rejeu complet notebook_tools.py execute --kernel python3 → SUCCESS, 9/9 cellules execution_count 1-9 avec sorties, 0 erreur.
• Sorties fidèles, aucun churn : les 9 cellules ont une sortie byte-identique à la base, mesuré cellule par cellule avant/après. La sortie authentique de la cellule 12 (empreinte axiomatique réelle via lake env lean en WSL : [propext, sorryAx, Classical.choice, Quot.sound]) est reproduite à l'identique — commande également rejouée à la main en WSL avant le rejeu complet (21 s, sortie identique).
• Kernel : check_kernel_drift.py origin/main --explain → OK: 0 kernel-drift regression (kernelspec.name python3 inchangé ; language_info 3.13.15 → 3.13.14, écart de patch toléré).
• Split-reading ratchet (--base-ref origin/main) : 1 carnet modifié, 0 en régression (paires 0 → 0). Mode --base : clean.
• Dette d'accents (detect_accent_stripping.py) : 68 → 68 — les mots ajoutés sont écrits sous leur forme accentuée canonique, aucune forme dé-accentuée nouvelle.
• H.3 : hooks pre-commit tous verts (dont la normalisation scrub-papermill-paths, seule retouche admise sur les métadonnées papermill).
• Diff : 1 fichier, 122+/122− — la cellule 17 (source) et les horodatages metadata.papermill du rejeu ; 21 cellules avant/après, aucune cellule ajoutée ni retirée.

Suite de la file : Lean-12-Sensitivity (F1, c.5845586784) puis Lean-16f-Conway (F2-F3, c.5845151605), après merge de #19665. [RELEASED] viendra sur la dernière PR de la file.

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	7.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	8.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	6.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.7s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	28.6s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	21.0s

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

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

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20109 (docs(analyse,#17357): retirer la preuve Lean 4 verbatim du stub mul_comm (ANALYSE-02-Tao)) 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(17357): ANALYSE-02-Tao -- retirer la fuite de solution F1 (script mul_comm de l'exercice 2) #20144 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb, recouvrement de chemins 100% -- fix(17357): ANALYSE-02-Tao -- retirer la fuite de solution F1 (script mul_comm de l'exercice 2) #20144 est deja sur main. (issues communes : [Audit #17073] Série Lean — partition Hermes #17357) (issues communes : [Audit #17073] Série Lean — partition Hermes #17357)

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.

[jsboige]

MESURE — le verdict du gate est anterieur a ses propres enfants

La jambe PR gate de cette PR est en failure (check-run 114018636451, demarree 2026-10-09T22:07:05Z, conclue 2026-10-09T22:07:18Z). Son annotation nomme : check-navlinks (cancelled, 10m09s) et markdown-rendering guard (cancelled, 11m22s), toutes deux au timeout declare de 10 min.

Relevé au fold check_run_state.py sur la tete courante : aucune jambe pendante, et les rouges actuels ne sont pas ceux que le gate a nommes --

jambe rouge maintenant	etat	demarree
check-navlinks	failure	2026-10-09T23:48:42Z

Les enfants rouges ont donc demarre apres la conclusion du gate. Sous famine, le gate rend son verdict pendant que ses constituants attendent encore un runner : son failure porte sur l'etat de la file, pas sur cette PR.

Aucun geste de lane pris, par decision mesuree. L'annotation du gate prescrit de rejouer le run enfant, jamais le gate (#15905) -- mais ici ce rejeu ne s'appuie sur rien : la jambe nommee a deja une execution fraiche, qui a echoue a 23:48:42Z — rejouer reproduirait ce qui vient d'etre mesure. Rejouer ajouterait de la file dans une famine, pour un verdict qui bouge tout seul a chaque slot obtenu.

Portee : je constate l'etat de la tete a l'instant du releve ; je n'ai pas lu les logs de ces jambes et ne me prononce donc pas sur leur cause.

[jsboige]

[CLOSED-as-delivered] — fermeture par la lane porteuse myia-po-2025:CoursIA, sur mesure firsthand du 2026-10-10.

L'objet unique de cette PR est livre sur main par #20144 (merge d10f1e7a5f, lot c2140 du 10/10) : « Fix: ANALYSE-02-Tao exercice 2 -- retirer le script de preuve mul_comm du stub (fuite de solution, #17357 F1) ».

Comparaison des deux blocs de source au stub lemma_mul_comm (seule difference de source entre ma tete 3a663ebfc5 et origin/main ; le reste du diff est de la metadonnee papermill) :

• cette PR : # TODO étudiant : construire la preuve soi-même, puis la confronter a celle du lac (même théorème, deux écritures à comparer). + les 3 indices + pass ;
• main (fix(17357): ANALYSE-02-Tao -- retirer la fuite de solution F1 (script mul_comm de l'exercice 2) #20144) : # TODO étudiant : voir la preuve de Tao dans Section_2_3.lean. + les mêmes 3 indices + # Le script final n'est pas donné ici : c'est l'objet de l'exercice. Construire la double induction d'après les indices ci-dessus, puis confronter votre preuve à Section_2_3.lean du lac source après coup. + pass.

Les deux retirent la preuve verbatim du stub (fuite de solution) et pointent l'etudiant vers le lac ; la version de main est plus explicite sur le geste attendu. Aucune substance propre de cette PR ne manque sur main — rebaser ne produirait qu'un remplacement de formulation sans valeur, en ecrasant la metadonnee d'execution fraiche de #20144.

Voir #17357 (F1) pour le suivi de campagne. Aucun autre fichier dans le perimetre.

— lane myia-po-2025:CoursIA