Enrich(notebook,#17978): Lean-15d references Serre100, Langlands, Geo-02 + Sheydvasser

[jsboige]

feat(notebook,#17978): Lean-15d references Serre100, Langlands, Geo-02 + Sheydvasser

Grain: MED/notebook-python -- lane myia-po-2023:CoursIA-2 -- prev: LIGHT/ripe-signal #19078 (c.1052)

Contexte

Dispatch ai-01 c.1053 (msg-20261005T073515-kz3yar, HIGH) : « Lean-15d ne reference que Lean-15. Il faut y ajouter Serre100, Langlands et la greffe Sheydvasser/Geo-02 (#17888, #17912), re-executer, puis proposer le fil narratif dans l'issue. »

Périmètre

Un seul fichier modifié, markdown only sur 3 cellules (c00, c14, c17) :

• c00 (intro) : table « Le depot porte deja trois carnets » étendue à 6 carnets (+ Serre100/01..15, + Langlands/01..02, + Geometry/02-From-Equation-To-Proof) + phrase pivot qui annonce les 5 sources d'inspiration des figures 1-7.
• c14 (lecture fig 4 — faisceaux) : référence à Serre100/03-cohomologie-cech-espaces-finis -- la condition de recollement sur espaces finis, où la cohomologie $\check{H}^1$ de Čech code la même condition de cocycle en algèbre. La figure Python est le cas continu de ce que le Čech discrét code.
• c17 (lecture fig 5 — Yoneda) : référence à Serre100/04-lemme-yoneda-categories-finies -- le lemme de Yoneda sur les catégories finies, qui rend l'énumération des transformations naturelles algorithmique.

Préservation C.2 (modifs markdown only)

14/14 cellules code conservent leur execution_count et outputs (la table « Le depot porte deja... » → 6 carnets n'est pas une cellule code). Carnet exécuté OK par papermill 11s/36 cellules (sanity check post-edit). C.2 exception modifs markdown only respectée.

Fil narratif proposé pour #17978

Le corpus Grothendieck du dépôt se lit comme une spirale à 6 entrées, où chaque carnet regarde le même objet sous un angle différent :

Carnet	Angle d'attaque	Ce qu'il rend visible
Lean-15 (Tribute)	Catalogue des modules	L'inventaire : 8 modules, 177 visibles, 13-20 % cités
Lean-15b	Exercices	L'atelier : manipuler les notions à la main
Lean-15c (Companion)	Preuves natives	La formalisation : ce qui tient en lake build
Serre100/01..15	Arithmétique	L'ancrage : les mêmes structures naissent des corps finis
Langlands/01..02	Correspondance	L'horizon : la conjecture qui unifie le tout
Geometry/02	Preuve	Le geste : l'échec et le contre-exemple lus par Sheydvasser
Lean-15d (ce carnet)	Figures	L'intuition : ce que les mots et le code ne montrent pas

Lean-15d a vocation à être la carne de visite de la spirale : un lecteur qui ouvre Lean-15d et parcourt les 7 figures doit pouvoir, en 30 minutes, savoir où aller ensuite dans le corpus. Les références ajoutées rendent ce geste possible — sans elles, Lean-15d était une île.

Tests / validation

• ✅ python -m papermill exécution bout-en-bout 11s, 36/36 cellules, 0 erreur
• ✅ H.3 pre-commit execution_count is None + outputs=[] = passed
• ✅ C.4 grounded : aucune valeur chiffrée ajoutée dans le markdown
• ✅ C.5 valeurs quantitatives : pas de chiffre en prose (uniquement liens)
• ✅ C.7 ancres code[N] : aucune référence numérique ajoutée (seulement des liens vers d'autres notebooks)
• ✅ Source-collapse ratchet : insertions > 0, deletions = 4 (les -Aucun des trois → -Aucun des six)

Acceptance

• 3 ajouts markdown (c00, c14, c17)
• Aucune cellule code touchée
• Outputs pré-existants préservés
• C.2 exception modifs markdown only respectée
• Fil narratif rédigé (proposé en commentaire sur Cadrage: rendre comestible et visible le travail Grothendieck du depot (narration + visuels + gradation) #17978)

🤖 Generated with Claude Code

See #17978 #17756 #17888 #17912 #1453

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

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.3s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s
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)

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

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19281
head: d1ed282
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: fc9d44fdaefbe0b7253b59fef5ee03c24a9b0993a48bf4152a0aeab2a0dd2e4c
diff-files: 1
diff-additions: 13
diff-deletions: 4
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 19281
organ-rc: 0
[/ADJOINT PREFLIGHT]

note: MED/notebook Lean-15d references Serre100, Langlands, Geo-02, Sheyd, lane porteuse po-2023-2 (a confirmer). 1 fichier 13 lignes, aucun interdit. PR gate SUCCESS (DWELL expire 12:07Z echu), B.0 rc=0 OK, scope pass, domain not-applicable. MED -> merge_ready eligible selon tag.