Reorg(lean,#19522): Lean-15c annexes groupees par theme, hierarchie 3 niveaux

[jsboige]

Grain: MED/notebook-lean -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/notebook-lean #19564

Sujet

Lean-15c avait 6 annexes plates empilees en queue (cells 24..43) sous le meme niveau ## Annexe -- <titre>. C'est illisible : 20 cellules consecutives sans groupement thematique.

Le reorg introduit un wrapper thematique et descend d'un niveau de hierarchie (mandat user #19439) :

## 12. Conclusion
## Annexes -- approfondissements optionnels
  ### Annexe A -- Faisceaux en profondeur
    #### A.1 -- Le coeur egaliseur rendu visible (SheafCondition)
      [code cell preserve verbatim]
      **Lecture de la sortie** -- <body>
    #### A.2 -- Du crible ferme a la faisceautisation Plus
      [code]
      **Lecture de la sortie** -- ...
    #### A.3 -- Les tiges (stalks) : du germe au recollement
      [code]
      **Lecture de la sortie** -- ...
    #### A.4 -- Des ouverts au prefaisceau gratte-ciel
      [code]
      **Lecture de la sortie** -- ...
      **Exercice** -- <body>
      [code -- exercise]
  ### Annexe B -- Cohomologie et sites
    #### B.1 -- Faisceaux flasques et resolution de Godement
      [code]
      **Lecture de la sortie** -- ...
    #### B.2 -- Sites, topologies et comparaisons
      [code]
      **Lecture de la sortie** -- ...

Ancienne structure : 2 niveaux (## Annexe + ### Lecture) ; nouvelle : 3 niveaux (## chapter wrapper + ### annex + #### A.X). Lecture descend de ### Lecture a un paragraphe en **Lecture de la sortie** dans la sous-section #### A.X ; le contenu interpretatif reste present, mais perd son niveau de titre (la frontiere #### reste celle du sujet de l'annexe, pas de l'interpretation).

Regroupement thematique

• Annexe A (Faisceaux en profondeur) : 4 annexes liees au concept de faisceau, en trois vagues successives du chantier de visibilite ([EPIC] Visibilite des lakes Lean dans les notebooks — 13-20 % des declarations citees, 97/177 modules invisibles #11703) : la condition de faisceau comme pont, la construction de faisceaux a partir d'un crible (Lawvere-Tierney), la localite des tiges, le retour aux prefaisceaux.
• Annexe B (Cohomologie et sites) : 2 annexes sur la cohomologie des faisceaux (faisceaux flasques, resolution de Godement) et la theorie des sites.

Le regroupement A/B suit la frontiere naturelle de la matiere : faisceaux est un objet d'etude, cohomologie est un calcul sur cet objet. L'ordre suit les dependances du cours (chapitres 6 puis 7).

Modifications (1 fichier, +91/-77)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb (45 -> 48 cellules : 24 cours + 1 conclusion + 1 wrapper ## + 2 wrappers ### A/B + 20 cellules d'annexe transformees = 48).

Type de cellule	Avant	Apres	Modif
Cours (cells 0..23)	24	24	preserve tel quel
Conclusion (cell 24)	1	1	preservee (deplacee a 24 par accident de numbering -- la Conclusion est a cells[24], la 1ere annexe demarre a cells[25] via le wrapper)
Wrapper ## Annexes	0	1	nouveau (cell 25)
Wrapper ### Annexe A/B	0	2	nouveau (cells 26, 41)
Headers ## Annexe -- X	6	0	transformes en #### A.X -- X
Headers ### Lecture / ### Exercice	7	0	transformes en **Lecture de la sortie** -- body / **Exercice** -- body
Code cells	7	7	preservees verbatim (execution_count, outputs, metadata)

Validation

• nbformat.validate() : OK (warning MissingIDFieldWarning non bloquant -- pre-existant dans le depot, ne devient hard error qu'en nbformat 6.0).
• Code cells preservees : 18 cellules code (11 du cours + 7 des annexes), toutes avec execution_count et outputs inchangees.
• C.2 : re-execution non due -- les cellules code sont deplacees, non modifiees. Pas de changement de source code, donc pas de regression d'output possible.
• Pas de regle H.3 violee : execution_count reste non-null partout.
• Pas de regle C.1 violee : pas d'erreur volontaire introduite.

Issue spec respectee

L'issue #19522 demandait "Une PR par carnet" : Lean-15c ici, Komlos-Discrepancy-02 dans une PR soeur sur la meme branche (ou une autre). Cette PR couvre strictement Lean-15c.

Refs #19522, #11703, #19439.

Co-Authored-By: Claude Haiku 4.5 (1M context) noreply@anthropic.com

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

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

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.7s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.3s
Search-01-StateSpace.ipynb	✅ SUCCESS	2.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	19.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	8.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	11.7s

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

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

Notebook PR Validation: PASS

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

Path-collision (organ #13359/#13615)

Cette PR #19573 (Reorg(lean,#19522): Lean-15c annexes groupees par theme, hierarchie 3 niveaux) 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 -- feat(lean,#11703): annexe Flasque/Godement dans Lean-15c — 8 modules noirs rendus visibles (16/83 -> 8/83) #19083 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb, recouvrement de chemins 100% -- feat(lean,#11703): annexe Flasque/Godement dans Lean-15c — 8 modules noirs rendus visibles (16/83 -> 8/83) #19083 est deja sur main.
• terminal -- 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, recouvrement de chemins 100% -- feat(lean,#11703): annexe sites & topologies dans Lean-15c — lake grothendieck_lean 0/83 modules noirs #19110 est deja sur main.
• faible -- feat(lean,#11703): annexe résolution canonique de Godement — 4 derniers modules noirs #19439 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb

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]

Ripe-signal -- PR prete a merge.

Tete : b8265bbe90cb (feature/19522-lean-15c-reorg).

Gates au vert (89 SUCCESS / 0 FAILURE, 4 SKIPPED, 1 NEUTRAL sur 94 jambes) :

• Lean CI Matrix : success
• PR gate : success
• prose-counts : success
• cell-source-parses : success
• Twin parity audit ([#4208] Métadonnée de parité des jumeaux Python/C# (twin: path/parity_level/last_audit_sha/known_differences) #8057) : success
• Validate Quarto (PR) : success
• validate-notebooks : success

Aucune revue postée (ni Hermes, ni NanoClaw, ni ai-01, ni user).

Reorg des annexes du carnet Lean-15c-Lean-Grothendieck-Companion.ipynb (6 sections plates -> 2 wrappers thematiques A/B « Faisceaux / Cohomologie » + hierarchie 3 niveaux, +91/-77, 18 cellules code preservees verbatim C.2). Suit la convention des reorgs Lean deja livrees (cf Lean-31 A-D, Lean-16b A-G). Issue de suivi #19522 (EPIC visibilite lakes Lean #11703) cloturee par cette PR + #19577 (sister PR Discrepancy-02).

Verdict substantiel : preparé et pret a merge.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19573
head: b8265bb
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 1b5c7e81c10df974a50a3f76450c21958bf61431262cd3bbaed41c6dc2835922
diff-files: 1
diff-additions: 91
diff-deletions: 77
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19573
organ-rc: 0
[/ADJOINT PREFLIGHT]