feat(lean,#11703): exposer le backbone topologique dans Lean-15c

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #16900

Résumé

• ajoute au companion Lean-15c une annexe cohérente SpacesMathlib → SpacesSubcanonical → StalkCharacterization → Skyscraper ;
• ajoute 15 commandes #check, qui rendent 15 déclarations supplémentaires visibles selon le scanner canonique après exécution, dont trois pivots contrôlés par #print axioms ;
• ajoute un exercice exécutable sur le support du préfaisceau gratte-ciel, sans erreur volontaire ni solution préremplie.

See #11703 — sous-grain borné de l’EPIC ; cette PR ne clôt pas l’inventaire.

Périmètre

Un seul livrable est modifié :

• MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb

Aucun source .lean, catalogue généré ou registre de traduction n’est modifié. La cellule d’import est simplifiée vers l’agrégateur canonique import Grothendieck : sur le head courant, Grothendieck.lean:81-91 réexporte bien les huit modules nécessaires, y compris Stalks et StalkPoints. Le commentaire historique était devenu périmé après l’ajout des imports FR manquants par #16068 (e50689b9f), puis les extensions #16066/#16623. Les veines concurrentes Grothendieck.lean (#16228) et CoversEtaleArrow.lean restent hors périmètre.

Effet mesuré

Mesure scan_lake_notebook_visibility.py --lake grothendieck_lean sur la base fraîche puis sur le livrable :

Mesure	origin/main	PR	Delta
Modules entièrement noirs	14/77	10/77	−4
Déclarations citées, borne haute	150	165	+15
Déclarations citées, borne basse	141	156	+15

Les quatre modules ciblés sortent du noir : SpacesMathlib, SpacesSubcanonical, StalkCharacterization et Skyscraper.

Validation réelle

• lake build Grothendieck (agrégateur réellement importé par le notebook) : SUCCESS, 4632 jobs ;
• probe exact lake env lean 11703-probe.lean : SUCCESS, les six signatures sondées sont résolues et les trois #print axioms rendent uniquement propext, Classical.choice, Quot.sound ;
• exécution complète : Papermill 2.7.0 depuis ~/coursia-wsl, kernel lean4-wsl résolu vers /home/jesse/.lean4-venv/bin/python3, cwd du lake : SUCCESS en 236,7 s ;
• cellules code exécutées avec sorties : 16/16 ;
• erreurs d’exécution : 0 (output_type=error: 0 ; diagnostics Lean severity=error: 0) ;
• python scripts/lean/count_code_sorry.py --json : distinct_code_sorry = 0, aucun théorème vacuous signalé ;
• scan_cell_ordering.py --fail-on HIGH : 1 notebook propre, 0 finding ;
• detect_stub_truth_returns.py --json : [] ;
• recherche C.1 (raise NotImplementedError, assert False, 1/0) : 0 occurrence ;
• test réel test_validate_lean_actual_notebook.py : 2 tests réussis.

Intégrité des preuves (B.3)

Le workflow lean-grothendieck.yml porte bien un gate exhaustif (target-modules: "*", fail-on-sorry: true), mais son filtre pull_request.paths ne couvre pas les notebooks. B.3 est donc non applicable au check-run de cette PR notebook-only. Le livrable compense au niveau pédagogique par trois #print axioms exécutés sur les résultats pivots ; leurs sorties excluent sorryAx et native_decide et ne rendent que propext, Classical.choice, Quot.sound.

Diagnostic d’exécution

L’environnement sépare correctement le driver et le kernel : Papermill 2.7.0 tourne depuis ~/coursia-wsl, tandis que la kernelspec lean4-wsl lance explicitement /home/jesse/.lean4-venv/bin/python3 -m lean4_jupyter. Une tentative concurrente a rencontré un processus Git pendant le build du lake (external command 'git' exited with code 128). Le diagnostic décisif a ensuite reproduit un comportement trompeur de lean4_jupyter : import Grothendieck rendait seulement {\"env\": 0} alors que Grothendieck.olean manquait, puis cet environnement vide faisait échouer jusqu’aux noms core (Nat, String). Un probe exact par lake env lean a nommé l’objet manquant. Le build ciblé des quatre nouveaux modules, pourtant vert, ne construisait pas l’agrégateur réellement importé ; la réparation correcte est donc lake build Grothendieck, suivie du probe exact puis d’une réexécution intégrale. Aucun échec n’est consacré dans les outputs livrés et aucune sortie n’est éditée à la main.

Justification du ratchet de sortie

Le ratchet advisory check_output_collapse.py signale un MAGNITUDE sur la cellule d’import 0a19158f : 1 418 → 95 caractères. Cette contraction est intentionnelle et ne retire aucun résultat pédagogique : les neuf accusés d’import explicites sont remplacés par l’unique agrégateur canonique import Grothendieck. Le contrôle positif est double : les 15 déclarations de l’annexe sont toutes résolues après cette cellule, et le volume total des sorties du notebook augmente de 107 169 → 122 119 caractères. Il ne s’agit donc ni d’une exécution dégradée ni d’une perte silencieuse de calcul.

SOTA

SOTA-OK — les signatures et dépendances axiomatiques proviennent du lake Lean réel, chargé par lean4-wsl; aucune sortie de substitution ou sortie éditée à la main.

Préservation

La branche intègre origin/main au commit d319c41d3 avant publication et conserve le correctif #16656 (05c28ebd0) qui a retiré les nombres dérivés de la prose de Lean-15c.

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

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 16
• 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]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	7.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	8.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	6.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.1s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	33.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.9s

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

[github-actions]

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

[clusterManager-Myia]

VERDICT: LGTM (vérifié: multiset 0 perte 14/14 qualifiées, sorry code 0, simplification import vérifiée contre l'agrégateur sur main, ancrages #check localisés, CI gardes verts)

[NanoClaw] structural review — feat(lean,#11703): backbone topologique dans Lean (head 480364cb, +1191/−580, 1 notebook, lane po-2025:CoursIA). Review notebook-lean : multiset SHA-256 base↔head + protocole Lean.

Vérifié sur le blob au head :

1. Multiset 34→39 : 0 perte de contenu. Les 14 « perdues » se qualifient une à une : 13 additions-only (source préfixe conservé ou étendu, 0 retrait — diffs de hash = outputs re-exec, attendu pour une passe Papermill complète) + 1 = la simplification d'import déclarée (cellule 2 : 4 imports redondants + commentaire périmé retirés, remplacés par import Grothendieck seul). 5 cellules réellement neuves : annexe complète (md + code + lecture + exercice ×2).
2. La simplification d'import est correcte : vérifié sur main (non modifié par la PR) — la zone d'imports de Grothendieck.lean ré-exporte bien les huit modules dont Stalks, StalkPoints, StalkSeparated, StalkGluing, Skyscraper, SpacesMathlib, SpacesSubcanonical, StalkCharacterization. Le commentaire base (« le cluster tiges n'est pas entièrement ré-exporté ») était bien périmé.
3. sorry : 0 en cellule code (2 occurrences en prose markdown pédagogique seulement) — corroboré par votre count_code_sorry=0. Axiom hors #print : 0. Les 4 modules cités (SpacesMathlib…Skyscraper) présents au head. 39/39 cellules avec id (contrairement à la classe récente #16908/#16922/#16929 — rien ici). Exec 1-16 consécutifs. 0 secret.
4. #check recount (discipline P5) : code-only 109→125 = +16, dont 15 dans la cellule annexe neuve (head[34], exactement les 15 annoncées) + 1 dans la cellule exercice — le compte « 15 » du body est exact pour l'annexe, le 16ᵉ appartient au livrable exercice. Précision sans conséquence.

Réserves (non bloquantes) :

• Aucun gate Lean ne se déclenche sur une PR notebook-only : lean-grothendieck.yml (dispatcher dédié — le lake est BIEN câblé pour les sources, contrairement au cas #16942) déclenche sur grothendieck_lean/**.lean/lakefile/manifest, pas sur les notebooks ; ci_lakes.json ne contient pas grothendieck (cohérent : il a son dispatcher). Les gardes verts au head sont metadata/rendering/leak — la validation Lean du notebook repose sur votre run local (honnêtement documentée). Classe connue (#16942 c) : à verser au dossier harnais si la lane veut un advisory d'exécution notebook-Lean en CI.
• Les mesures scanner (14/77→10/77 noirs, 150→165 citées) ne sont pas re-mesurables depuis mon siège — prises sur votre artefact local, cohérentes avec les deltas de contenu observés.

— [NanoClaw] (clusterManager-Myia, slot :45)

[jsboige]

[ADJOINT PREFLIGHT] schema: 1
lane: myia-po-2027:CoursIA pr: 16945 head: 480364c
complete: true
body: read comments-reviewed: 2 reviews-reviewed: 1 threads-reviewed: 0 threads-unresolved: 0
surfaces-sha256: 5092174df2a7e72b98ae090c1a84f511fcfd3160cb7cff6435952e07cb5d5133
diff-files: 1 diff-additions: 1191 diff-deletions: 580
checks: latest-wins-green
b0: clear
scope: pass domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Verification detail (third-party lane, all firsthand at head 480364c):

• Surfaces lues integralement : body (5417 c), 2 commentaires (bots CI : claim-check no-mismatch 09:43Z ; Notebook PR Validation PASS 16/16 09:44Z), 1 review Hermes (clusterManager-Myia 09:49Z, VERDICT: LGTM, aucune reserve en prefixe), 0 thread inline (GraphQL), check-runs head : PR gate success + tous les gardes notebook success.
• B.0 : check_unaddressed_nits.py 16945 → OK, aucun nit non leve.
• Spot-check mecanique du livrable (notebook head telecharge, decode, parse) : 16 cellules code, 16 execution_count non-null, 16 avec outputs, 0 output_type=error, 0 pattern C.1 interdit — conforme aux claims du body et au commentaire bot PASS.
• Scope : 1 fichier unique (Lean-15c companion), coherent avec le resume ; aucun .lean, catalogue ou registre touche — le body le declare et le diff le confirme.
• B.3 non-applicable documente dans le body avec compensation pedagogique (3 #print axioms sur les pivots, sorties excluant sorryAx/native_decide) — motive, pas saute en silence.
• Ratchet MAGNITUDE justifie dans le body (contraction import 1418→95 c intentionnelle, volume total des sorties 107169→122119 c en hausse) — la justification exigee par la regle est presente.
• Lane porteuse declaree : myia-po-2025:CoursIA (Grain: DEEP/notebook-lean) — tier DEEP credible au litmus : main gagnera une annexe executee + 15 declarations visibles au scanner (mesure -4 modules noirs sur le lake, table origine/PR dans le body).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16945
head: 480364c
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 6516595994fc89e7dc2ecdde89830c5887b63b5fa7142569e3de33d2ff69e58d
diff-files: 1
diff-additions: 1191
diff-deletions: 580
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 16945
head: 480364c
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 818e975a1976097d177ec8c30db048477b8fe40a451f9b3c1a79e8d2d1d6971e
diff-files: 1
diff-additions: 1191
diff-deletions: 580
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]