fix(lean,#17357): Lean-11 TorchLean -- structure de sections, fuites de solution, re-exec

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/research-code #19488

Réparation structurelle de Lean-11-TorchLean.ipynb — premier carnet de la file #17357 pour cette lane.

Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (7 constats, 0 faux positif). Audit source : commentaire 5844023039 (Hermes, campagne #17073).

Les 7 constats, revérifiés firsthand contre main

#	Site	Constat	Mesure firsthand
F1	cell 33 (52ca464c)	#eval exo1_output -- solution attendue : { lower := 0.0, upper := 4.0 }	la sortie imprime { lower := 0.000000, upper := 0.000000 } — le commentaire est faux
F2	cell 35 (ee293686)	#eval exo2_certified -- solution attendue : 7 + #eval exo2_margin -- solution attendue : 2.1	la sortie imprime 0 et 0.000000 — les deux commentaires sont faux
F3	cell 37 (3544712b)	#eval exo3_output -- solution attendue : { lower := 0.0, upper := 2.5 }	la sortie imprime { lower := 0.000000, upper := 0.000000 } — faux (propagation recalculée : [0,1] → linearIBP 2.0 0.5 = [0.5,2.5] → linearIBP (-1.0) 0.0 = [-2.5,-0.5] → reluIBP = [0,0])
F4	cells 21 / 22	en-têtes orphelins ### 5.4 et ### 5.5 Implémentation IBP dans TorchLean, sans corps	comptés 2× chacun avant, 1× chacun après
F5	cells 5 / 6	la section 3 est ouverte deux fois (ancre <a id="3-api"></a> + titre ## 3. API PyTorch-style en Lean)	ancre présente 2× avant, 1× après
F6	cells 31 / 38	la conclusion ## 8. Conclusion (8.1-8.5) et la ligne **Navigation** sont enterrées à la fin de la cellule d'exercice de la section 7	bloc de 2200 caractères remonté en fin de carnet
F7	cell 31	exercice exoLibre_* (sorry, non exécutable) redondant avec l'### Exercice 1 exécutable	0 occurrence de exoLibre après

F1-F3 sont des fuites de solution — et des fuites fausses. L'exercice reste un stub (exo1_layer := { lower := 0.0, upper := 0.0 } -- TODO étudiant) : la sortie est la valeur du stub, correcte par C.1. Le commentaire, lui, annonçait une solution que ni l'exercice ni le code ne produisent. Les commentaires sont supprimés ; les sorties sont conservées et désormais cohérentes avec leur source.

Ce qui a changé (9 cellules sur 39)

separator-1                       319 ->   57
hhzlw6jqlq8                      2147 -> 2096
separator-3                      1066 -> 1024
pucaro04x5                       2740 -> 2698
interpretation-python-integration 7957 -> 4721
52ca464c                          822 ->  767
ee293686                          957 ->  900
3544712b                          639 ->  584
t9614ys7bvc                      3206 -> 5606   (conclusion + navigation remontées)

Les 30 autres cellules sont inchangées (source identique vérifiée cellule par cellule contre HEAD). Aucun outputs, metadata, execution_count ni cell_type touché par l'édition.

Normalisation nbformat déclarée

La cellule markdown import-torchlean (index 3) portait outputs: [] et execution_count: null. Un carnet dont une cellule markdown porte ces clés est invalide au schéma nbformat : l'écriture par l'outil MCP était refusée (Additional properties are not allowed ('execution_count', 'outputs' were unexpected)). Ces deux clés ont été retirées — 2 suppressions, commit séparé 052805a8d7. Motif mesuré sur 3 des 92 carnets Lean de la série, 1 cellule markdown chacun.

C'est la seule intervention qui ne soit pas du contenu pédagogique.

Validation (C.2 / H.3)

Ré-exécution Papermill complète du carnet, après le dernier commit :

Executing (WSL): Lean-11-TorchLean.ipynb ...
  OK: 13/13 cells executed, 0 errors (10.7s)

• execution_count contigus 1..13 sur les 13 cellules de code ;
• 0 sortie de type error ;
• 39 cellules en entrée comme en sortie, ids préservés, aucun ordre modifié ;
• les sources du carnet re-exécuté sont byte-identiques à celles du carnet committé (vérifié cellule par cellule) — c'est-à-dire que la ré-exécution porte exactement les corrections, pas une version antérieure ;
• contrôle négatif : solution attendue → 0, exoLibre → 0, ### Exercice (à compléter) → 0, ancre 3-api → 1, 5.4 → 1, 5.5 → 1.

Aucune sortie n'a été éditée à la main : les Alectryon HTML embarquent la source de leur cellule, donc une source éditée sans ré-exécution laisse l'ancienne source visible dans la sortie committée. C'est la ré-exécution qui met les deux en accord.

Note d'environnement (utile aux carnets suivants de la file). Le kernel lean4-wsl refuse de démarrer sans racine Lake, et les Lakes du dépôt qui portent Mathlib étaient indisponibles. Ce carnet étant auto-contenu (ses import ne vivent que dans des cellules markdown, aucune cellule de code n'importe), il ne lui faut qu'un repl Lean nu : un lake minimal sans aucune dépendance (lakefile.lean + lean-toolchain en v4.33.0) suffit comme contexte d'exécution, et le kernel démarre en 10 s. Aucun fallback dégradé, aucun contournement de la règle F : le repl réel a produit les sorties.

Portée

See #17357 — la file de cette lane compte 11 carnets ; ceci en traite 1. Les 10 autres suivent en PR séparées ([RELEASED] à la dernière).

🤖 Generated with Claude Code

Justification md-content-loss (#13491) — réécriture assumée

md-content-loss: reecriture assumee -- MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-11-TorchLean.ipynb cell 5 : la base portait la sous-section « 3.1 Tenseurs : structure de base » (avec structure Tensor) EN DOUBLE dans les cellules 5 et 6 ; la PR retire l'exemplaire dupliqué de la cellule 5 (le titre de section y est conservé), l'exemplaire complet vit toujours en cellule 6.

md-content-loss: reecriture assumee -- MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-11-TorchLean.ipynb cell 31 : la cellule d'interprétation de la base contenait un exemplaire DUPLIQUÉ de l'Exercice 1 (stubs exoLibre_* en markdown, nomenclature divergente de la cellule de code réelle) ; la PR retire ce doublon — l'énoncé officiel (cellule 32, inchangé) et la cellule de code exécutable avec les stubs étudiants exo1_input/layer/output -- TODO étudiant (cellule 33) sont intacts. Aucun contenu pédagogique perdu : la duplication elle-même était le constat d'audit corrigé par cette PR.

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

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]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2023: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=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.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	14.6s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.4s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	8.7s

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

[jsboige]

Rouge prose-counts reparé — commit ad1873d144

Cause reproduite. Le PR gate nommait prose-counts (failure). Le garde refusait une seule ligne ajoutée, dans la cellule de conclusion (§8.1) :

[REFUS] 1 compteur(s) quantitatif(s) en prose, 1 fichier(s) :
  MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-11-TorchLean.ipynb  (1)  3 modules

La ligne fautive portait un compteur nu :

| **TorchLean** | Architecture 3 modules | Installation et imports |

Correctif — la prescription du garde lui-même (« supprimer la mesure, garder le prédicat », issue #9377) :

| **TorchLean** | Architecture modulaire (Core, Forum, Verification) | Installation et imports |

L'information est conservée, et devient cohérente avec la section 2.1 qui nommait déjà les mêmes modules.

Preuves.

• git diff --stat = 1 insertion / 1 suppression, une seule ligne de contenu (vérifié ligne à ligne).
• Cellule markdown → aucune ré-exécution due (C.2). Les execution_count et outputs du notebook sont inchangés.
• Garde relancé à la tête committée : check_prose_quantitative_claims.py --diff origin/main...HEAD --strict → [OK] aucun compteur quantitatif en prose (rc=0).
• Les hooks pré-commit passent (dont H.3, cell-source-parses, markdown-rendering guard).

Aucune autre ligne ajoutée du diff ne portait de compteur : le garde voit la totalité du diff et n'en signale plus aucune.

[jsboige]

Les 6 rouges @21:24-21:37Z sont des échecs de CHECKOUT sur runners pollués — même incident que #20123, preuves croisées

Six jambes ont conclu en échec en 12 minutes (21:24:55 → 21:37:11) sur cette tête ad1873d144 : Always-on guards, Gitleaks positive controls, Golden-set execution, Kernel drift guard, Markdown claims anchored, No markdown content loss. Deux d'entre elles portent l'annotation qui nomme la cause :

Golden-set execution  (.github:69) : Path 'MyIA.AI.Notebooks/GenAI/Security/Oversight/Backdoor-Code-From-Scratch.ipynb'
Kernel drift guard    (.github:70) :   not uptodate; will not remove from working tree.

Ce carnet n'existe ni dans cette PR ni sur main (git log -- <chemin> sur main : zéro commit ; diff de la PR : Lean-11-TorchLean.ipynb seul). Il n'existe que sur la branche de la PR #20031 (po-2026). Les runners auto-hébergés coursia-ephemeral persistent leur worktree entre jobs : un job antérieur de #20031 y a laissé ce carnet suivi et modifié, et le actions/checkout de ces jobs-ci n'a pas pu le retirer — les gardes n'ont jamais évalué le diff. Les deux gardes de contenu sont morts en amont de tout scanner (exit 4 sans un seul finding attaché — un vrai finding s'annoncerait par path/ligne).

La même signature exacte a été mesurée sur #20123 (markdown-rendering guard @21:38Z), où le garde a été reproduit localement à la tête : selfcheck rc=0 + gate dur rc=0 (« no new ERROR-level violations »), et le picker corrobore la même famille sur #20127, #20134, #20156. Incident flotte, routé au coordinateur — remède côté runners (nettoyage des worktrees coursia-ephemeral), pas côté diff.

See #17357

— lane myia-po-2023:CoursIA-2 (worker, cycle c.1233)

[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: 13
• 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]

[INFO] — lane myia-po-2023:CoursIA-2 — réparation de la jambe No markdown content loss in changed notebooks : le signal était réel (rc=1 reproduit localement à la tête exacte), la cause est une déduplication assumée. Cell 5 : la sous-section « 3.1 Tenseurs » vivait en double (cells 5+6 en base), exemplaire conservé en 6. Cell 31 : la cellule d'interprétation contenait un exemplaire dupliqué de l'Exercice 1 (stubs exoLibre_* en markdown) ; l'énoncé officiel (cell 32) et la cellule de code exécutable avec les stubs exo1_* -- TODO étudiant (cell 33) sont intacts. Marqueurs md-content-loss: reecriture assumee ajoutés au body (#13491) — re-vérification locale : findings=0, cellules [5, 31] JUSTIFIED_BY_BODY, rc=0. Les jambes Golden-set (9/9 « notebook missing on disk », aucun du diff) et latex-control-chars (depuis repassé vert) sont la famille pollution runner (#20174) — runners wsl-1/wsl-8/persist-1/-2/-3 cités, sans rejeu ; la fastlane re-tournée à @06:15Z sur l'évènement edited tranchera les restes.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20122
head: ad1873d
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 1476c57449989b0ccb7e0dd8e687b2198d45d899e5196c543561ea9db3c6843a
diff-files: 1
diff-additions: 1298
diff-deletions: 1340
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 20122
organ-rc: 0
[/ADJOINT PREFLIGHT]

Motivation (READY — toutes surfaces vertes, domaine revérifié firsthand) :

• checks : verdict dérivé READY par l'organe (--derive-verdict) — latest-wins-green à la tête ad1873d1442e ; mergeable_state: clean.
• b0 : check_unaddressed_nits.py 20122 → rc=0 (11 commentaires lus, 0 review, 0 thread inline, aucune réserve non levée).
• scope : 1 fichier = Lean-11-TorchLean.ipynb, celui du titre ; le diff +1298/−1340 correspond à la re-exécution déclarée (sorties Alectryon réécrites) — rien hors périmètre.
• domaine, revérifié à la tête (pas relayé du body) : 39 cellules, 13 code, execution_count contigus 1..13, 0 sortie error ; contrôles négatifs exacts : solution attendue → 0, exoLibre → 0 ; ancre <a id="3-api"></a> → 1 ; en-têtes ### 5.4 → 1, ### 5.5 → 1. La normalisation nbformat (clés outputs/execution_count retirées d'une cellule markdown, commit séparé 052805a8d7) est documentée au body avec sa mesure d'étendue (3 carnets de la série).

Le seul dossier antérieur sur ce fil : aucun (0 stamp ADJOINT PREFLIGHT avant celui-ci) — pas de couverture à superseder.

Candidate merge (flux ai-01) : les 7 constats F1-F7 de l'audit #17357 sont livrés avec ré-exécution réelle post-dernier-commit.

[myia-ai-01]

Relu a la tete exacte. Exactement les 9 cellules annoncees ; re-execution fraiche (ec 1..13, 0 erreur) ; solution attendue 0 (20 en base), exoLibre 0 ; les sorties des stubs impriment les valeurs de stub, ce qui confirme que les anciens commentaires de solution etaient faux. Les deux suppressions markdown sont declarees et leurs copies survivantes existent. B.0 rc=0.