restore(lean,#17066): lean15b — restauration « Lecture des 18 vérifications » (mot pour mot, +13/-0)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #17213

Résumé

Restauration de la cellule markdown ### Lecture des 18 vérifications : l'index est vivant, pas déclaré (id c34d70af, 1104 chars), supprimée à tort par la passe de densification #17040 : réinsertion mot pour mot depuis la base d412b5a13c79, à sa position d'origine — entre la cellule code « Comptage systematique des #check » (idx 26) et « ## 8. Exemples guidés ».

Pourquoi cette cellule : elle lit la sortie de la cellule de comptage (liste des 18 #check du MathlibMap vendu) — sortie devenue orpheline sur origin/main (aucune cellule ne la lisait). Son apport est distinct de la cellule conservée « Interpretation : ce que Mathlib a » (qui lit l'affichage du module) : ordonnancement de la liste (socle catégories → cribles → topologies extrémales → faisceaux → schémas), argument « index vivant, pas déclaré » (chaque entrée vérifiée par compilation — valeur canari de non-régression).

Contexte de la mission (routage po-2024)

Mission « auto-attestation refusée » routée depuis #17110. Vérifié firsthand :

• la cellule est absente de origin/main (0 occurrence, sortie de la cellule 26 orpheline) ;
• la branche fix(lean,#17066): Lean-6 Mathlib Essentials — réparer la dégradation #16862 REPAIR-7/8 (sauts de ligne doublés, accents) #17110 ne porte pas la restauration : son diff est Lean-6-Mathlib-Essentials.ipynb uniquement (+681/−599), déjà porté par docs(notebooks,#16638): reaccent Lean-6 Mathlib Essentials.ipynb #16862 (constat Hermes po-2026, re-vérifié po-2024 via pulls/17110/files) ;
• merger fix(lean,#17066): Lean-6 Mathlib Essentials — réparer la dégradation #16862 REPAIR-7/8 (sauts de ligne doublés, accents) #17110 tel quel laisserait l'analyse absente de main. Le sort de fix(lean,#17066): Lean-6 Mathlib Essentials — réparer la dégradation #16862 REPAIR-7/8 (sauts de ligne doublés, accents) #17110 (rebasage/fermeture) revient à sa lane et au coordinateur — cette PR livre la mission annoncée.

Preuves (mesurées sur cette branche)

Vérification	Résultat
Diff	+13/−0, 1 fichier — insertion pure
Cellules code	18 avant = 18 après, byte-identiques (source, outputs, execution_count, metadata, ids)
Cellules md	22 → 23
detect_notebook_plan_loss --base d412b5a13c79 --check	rc=0, 0 finding, md base=23 head=23, headings 33=33
detect_md_content_loss --base d412b5a13c79 --check	rc=0, 0 finding, normalized_chars 18574 = base
Headings dupliqués (h3+)	0
Re-exécution	Non due — aucune cellule code touchée (C.3 : scope markdown-only)

Claim posé sur #17066 (c.5760925410, scoped paths: sur le notebook).

See #17066
See #17110

🤖 Generated with Claude Code

[github-actions]

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

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.7s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.2s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.1s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	18.5s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s

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

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

Path-collision (organ #13359/#13615)

Cette PR #17214 (restore(lean,#17066): lean15b — restauration « Lecture des 18 vérifications » (mot pour mot, +13/-0)) 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(density,#17040): redressement paquet P17 - Lean/Planners #17052 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb, recouvrement de chemins 50% -- fix(density,#17040): redressement paquet P17 - Lean/Planners #17052 est deja sur main.

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]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 17214
head: 22b27af
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: bf71a514d2b2d239ea218f20655cb3c3de4ae9ee016fe4cb5ce5b19983df0037
diff-files: 1
diff-additions: 13
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier Secrétaire cat. 2 mini-cost cycle 3, exact-head 22b27af, +13/-0, 1 fichier(s).
Mesures firsthand 2026-09-22T01:2xZ.
SHA gate live N/A....

— secrétaire myia-po-2026:CoursIA-3