docs(notebooks,#16638): reaccent Lean-2 Dependent Types (filtre print C.2)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16961-open

Résumé

Sub-grain #16638 : réaccent Lean-2-Dependent-Types.ipynb (vocabulaire théorique des types). 36 cells touchées, +47/-47 mirror strict.

Intégrité C.2

Vérif	Résultat
Cells totales	59 = 59 ✓
Cells code	29 = 29 ✓
Cells avec outputs modifiés	0 ✓
Mirror diff stat	+47 / -47 ✓

Top sub-grain #16638 (cumul top 13)

Rang	Notebook	Subs	PR	Cycle
1	Lean-10 LeanDojo	494	#16943	c.1299
2	Lean-9 SK Multi-Agents	452	#16948	c.1301
3	Lean-5 Tactics	346	#16955	c.1305
4	Lean-6 Mathlib Essentials	345	#16862	c.1294
5	Lean-16b Conway	407	#16868	c.1296
6	Lean-3 Propositions	264	#16951	c.1302
7	Lean-4 Quantifiers	245	#16956	c.1306
8	Lean-8 Agentic Proving	221	#16953	c.1304
9	Lean-7 LLM Integration	217	#16952	c.1303
10	Lean-13 Kochen-Specker	143	#16961	c.1307
11	Lean-12 Sensitivity	147	#16947	c.1300
12	Lean-2 Dependent Types	83	cette PR	c.1308
13	Lean-1-Setup	31	#16837	c.1289

Total cumulé top 13 = 3395 substitutions.

🤖 Generated with Claude Code

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

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	6.0s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	6.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	8.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	8.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.6s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	55.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.4s

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: 29
• 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]

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

[jsboige]

[ADJOINT PREFLIGHT] schema: 1
lane: myia-po-2027:CoursIA pr: 16964 head: 4f0c0e4392d4a58aa0d2e4529403e2dab5f5b04e
complete: true
body: read comments-reviewed: 4 reviews-reviewed: 0 threads-reviewed: 0 threads-unresolved: 0
surfaces-sha256: 12cf63b4cfcae7b449e560352849fb22a2862186107220fd0baf791e6cf90bc2
diff-files: 1 diff-additions: 47 diff-deletions: 47
checks: latest-wins-green
b0: clear
scope: pass domain: pass
verdict: READY (0 review Hermes au head — dossier mecanique complet)
[/ADJOINT PREFLIGHT]

Verification detail (third-party lane — porteuse myia-po-2024:CoursIA-2 ; all firsthand at head) :

• Surfaces : body (filtre print C.2, campagne reaccent Rollout deaccent repo-wide : piloter les tranches par serie (~946 notebooks candidats) #16638), 4 commentaires bots CI PASS, 0 review, 0 thread. B.0 : OK. Grain tag present (MED/notebook-lean — lane myia-po-2024:CoursIA-2).
• Verification decisive reaccent (base vs head, multiset par cellule) : 0 cellule ajoutee/supprimee ; 12 markdown reaccentuees ; 14 cellules code modifiees = commentaires Lean -- UNIQUEMENT (21 lignes diff, toutes prefixees --) — la sortie Lean ne depend pas des commentaires. Outputs byte-identiques base↔head sur les 29 cellules code : coherent et legitime, aucune re-exec due (C.2 respecte : rien d'affiche n'a change).
• Spot-check mecanique : ratchets output-failure/collapse/flood, H.4, validation CI tous verts au head (fail:0, 0 en vol). Additions==deletions (47/47) coherent avec reaccent ligne-a-ligne.

[jsboige]

[ERRATUM] dossier precedent — champ head: errone. Le head exact de cette PR au moment du dossier est 31abe89da6789bfcf09cc532066cc94fd92cd9e1 (le SHA imprime dans le dossier precedent est invalide). Toutes les mesures du dossier (multiset base↔head, classification des lignes diff, verification outputs) ont ete prises sur le ref refs/remotes/pr/16964 = 31abe89da6789bfcf09cc532066cc94fd92cd9e1 — les conclusions tiennent, seul le champ head imprime etait fautif. Verdict inchange.

— myia-po-2027:CoursIA

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16964
head: 31abe89
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8f1682932aa398893b345c12f01984f8b9b9f066a33f6b8b968e86f755e8de33
diff-files: 1
diff-additions: 47
diff-deletions: 47
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]