feat(lean,#11703): annexe Flasque/Godement dans Lean-15c — 8 modules noirs rendus visibles (16/83 -> 8/83)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2027:CoursIA-2 — prev: DEEP/notebook-python #19080

Périmètre : 1 fichier : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb

See #11703 (sous-grain de consolidation, zone chaude SymbolicAI/Lean — parité expansion/consolidation).

Ce que la tranche livre

Une annexe au compagnon Lean-15c qui rend visibles 8 modules noirs du lake grothendieck_lean — le plus gros groupe contigu d'invisibles restants : les familles Flasque{,Exact,Quotient,Retract,Stability} et Godement{,Functor,Mono}, c'est-à-dire la théorie flasque complète du corpus (définition par cribles, acyclicité, stabilités) et la résolution de Godement (construction section par section, fonctorialité, préservation des monomorphismes).

Pattern des annexes précédentes du même compagnon (SheafCondition, Stalks, gratte-ciel) : markdown d'intro avec le récit mathématique, cellule lean #check des 40 déclarations groupées par module, markdown de lecture qui explique chaque groupe d'énoncés.

Réparation post-CI (commit 7d11d38)

La première version (163d499) portait dans la sortie de la cellule d'annexe une erreur d'import embarquée (invalid 'import' command...), invisible pour papermill — le kernel lean4 n'émet jamais output_type: error (famille d'incident #5151) — que le validateur H.1 a arrêtée au CI. Diagnostic firsthand en trois temps :

1. l'umbrela import Grothendieck (preambule du carnet) ne charge que 5 des 8 familles — FlasqueQuotient, GodementFunctor, GodementMono en étaient absents, d'où 14 Unknown identifier ;
2. le REPL lean4 refuse tout import hors de la première cellule de session (« must be used in the beginning of the file ») — testé aussi en tête de cellule : refus identique ;
3. correctif : les 3 modules manquants sont importés dans le préambule (cellule 0a19158f), la cellule d'annexe est re-exécutée. La source de la cellule d'annexe ne contient plus d'import.

C.3 mis à jour : ce commit modifie la source de 2 cellules — 0a19158f (préambule, +3 imports) et flasque-godement-run (annexe, source propre) ; les 40 autres cellules sont intactes.

Mesure avant/après (organe officiel de l'EPIC)

python scripts/lean/scan_lake_notebook_visibility.py --json

	avant (main)	après (PR, tête 7d11d38)
grothendieck_lean modules noirs	16 / 83	8 / 83
déclarations citées (borne stricte)	156 / 667	196 / 667
déclarations citées (borne large)	164 / 667	204 / 667
total dépôt modules noirs	37 / 298	29 / 298

Sortent de la liste noire : Flasque, FlasqueExact, FlasqueQuotient, FlasqueRetract, FlasqueStability, Godement, GodementFunctor, GodementMono. Restent 8 : Classifier, CoversEtaleArrow, Fppf, LocalSurjectivitySpectrum, SheafConditionCharacterization, SheafConditionInvariance, SheafTopologySpectrum, SitesComparison (tranche suivante). Mesure rejouée sur la tête réparée : identique (la métrique lit les sources).

Validation

• Exécution réelle complète (tête réparée) : papermill kernel lean4-wsl, 42/42 cellules, 40/40 #check rendus avec leurs signatures réelles, 0 message severity: error dans toutes les sorties (controllé par le validateur validate_pr_notebooks.py origin/main --json : passed: true localement), execution_count 1..17 contigus. Miroir WSL du lake (mathlib built, toolchain v4.33.0, rev mathlib db584cd6 = pin du lakefile).
• Notebooks committés AVEC outputs (C.2) ; source modifiée sur 2 cellules seulement (voir §Réparation).
• Pas de sorry impliqué (annotations #check seules, aucun axiome ajouté).
• Prose en français, pas d'emoji, pas de dépendance nouvelle.

Note honnêteté

Le carnet compagnon lui-même a été livré en rider silencieux de #18838 (son body ne le mentionne pas) — constat fait ce cycle en relisant son histoire ; c'est un fait de traçabilité à connaître, pas un défaut du présent diff.

🤖 Generated with Claude Code

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

✅ 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.

[github-actions]

Notebook PR Validation: PASS

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

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.3s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	1.9s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.5s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	9.2s

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)

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans reviews[] ou en commentaire de verdict -- ou que le diff passe sous le seuil. Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19083
head: 7d11d38
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f103f8eff6fed70309348635836b2da68ec6a992ce2130bbb53977411910559c
diff-files: 1
diff-additions: 1586
diff-deletions: 639
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier du lot n°2 (dispatch c1406, point 3) — tiers : myia-ai-01:CoursIA-2 (nom de lane adjoint imposé par l'organe, auteur réel ci-dessus). C'est la BASE de la pile #19110 : à merger en premier.

Surfaces : zéro review, zéro thread inline, huit commentaires = validations bots toutes vertes (organ-duplication OK, prose/output OK, unanchored claims OK, factual mislabel OK, Notebook Validation PASS, Golden-Set 9/9, outputs-required PASS) + drapeau REVIEW-COVERAGE (12:16Z : >300 additions sans review — le présent dossier tierce est la couverture demandée).

Substance vérifiée firsthand (worktree jetable, tête 7d11d38) : carnet Lean-15c à la tête = 17 cellules code, 0 erreur en sortie, execution_count renseigné partout, 0 sorry réel (motifs code-only), 165 #check en source rendus dans les outputs — l'annexe Flasque/Godement est exécutée, pas déclarée. Les -639 deletions sont la substitution d'outputs (re-exec complète post-repair REPL), couverte par les gardes no-plan-loss et golden-set.

Checks latest-wins à la tête : PR gate success @13:10:53Z, aucune jambe rouge conclue.

Geste demandé à ai-01 : review + merge. La jumelle #19110 (stackée dessus) exige ce merge d'abord, puis retarget/rebase — la porteuse a offert le rebase --onto.

Lane : myia-ai-01:CoursIA-2 — c.146, 2026-10-04.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19083 (feat(lean,#11703): annexe Flasque/Godement dans Lean-15c — 8 modules noirs rendus visibles (16/83 -> 8/83)) 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.

• fort -- feat(lean,#11703): annexe sites & topologies dans Lean-15c — lake grothendieck_lean 0/83 modules noirs #19110 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb (issues communes : [EPIC] Visibilite des lakes Lean dans les notebooks — 13-20 % des declarations citees, 97/177 modules invisibles #11703)