feat(lean,#2159): Partie 62 construction Plus — SGA 4 II.3 (fonctorialite, toPlus, propriete universelle)

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: DEEP/lean #12891

Summary

Partie 62 de l'Epic #2159 (Phase 2) : la construction Plus (CategoryTheory.Sites.Plus, SGA 4 II.3) — l'ingrédient constructif de la sheafification en deux passes de Godement–Grothendieck, complétant la Partie 20 (Sheafification.lean) qui avait posé l'adjonction.

Nouveau module FR Grothendieck/PlusConstruction.lean (197 lignes) + sibling EN PlusConstruction_en.lean (181 lignes, convention #4980 Option A, namespace Grothendieck_en) : 12 théorèmes-ponts couvrant

• Fonctorialité : plusFunctor_obj_field (rfl), plusMap_id_field, plusMap_comp_field — plusFunctor est un foncteur (objet, identité, composition)
• Naturalité : toPlusNatTrans_app_field (rfl), toPlus_naturality_field — toPlus : 𝟭 ⟶ plusFunctor
• Identité algébrique clé : plusMap_toPlus_field — (P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺, le cœur de l'associativité de la double passe
• Point fixe : isoToPlus_hom_field, isoToPlus_inv_field — un faisceau est un point fixe de Plus (P ≅ P⁺)
• Propriété universelle (SGA 4 II.3) : plusLift_toPlus_field, plusLift_unique_field, plus_hom_ext_field (toPlus épimorphisme vis-à-vis des faisceaux), plusMap_plusLift_field

Aussi : imports umbrella (Grothendieck.lean, entrées substance FR+EN), lignes tableau + compteurs dans README.md / README.en.md (58 leaf FR + 58 siblings _en + 1 umbrella = 59 FR files — vérifié contre find sur disque, audit §E fichier entier ; le prose « 55 leaves + 8 siblings » était stale sur main).

Validation (critère B — Lean)

1. Compte sorry réel avant/après : python scripts/lean/count_code_sorry.py --json → distinct_code_sorry = 0 avant (main) et 0 après. Module complet à la création, 0 axiome ajouté.
2. Lake build SUCCESS (local, WSL, toolchain v4.32.1, junction cache p60) :
   • lake build Grothendieck.PlusConstruction Grothendieck.PlusConstruction_en → Build completed successfully (925 jobs)
   • lake build Grothendieck (umbrella) → Build completed successfully (2919 jobs)
3. Proof integrity : job proof-integrity de lean-grothendieck.yml câblé sur ce lake avec target-modules: "*" (liste dérivée du diff au runtime, lignes 113-118) → couvre les nouveaux modules par clôture d'imports ; B.3 applicable, verdict attendu sur la CI.
4. Pas de refactor du prover Python.

i18n (#4980)

python scripts/lean/check_i18n_siblings.py .../PlusConstruction_en.lean → OK — 1/1 pairs byte-identical | 0 drift | 0 orphan. Seules docstrings/commentaires diffèrent ; namespace Grothendieck_en, énoncés byte-identiques.

Notes de build

Deux itérations nécessaires : (a) HasMultiequalizer exige open CategoryTheory.Limits (Mathlib Sites/Plus.lean l'ouvre ; sans lui, la ligne variable échoue et cascade des « Unknown identifier » + une erreur d'univers trompeuse) ; (b) plusMap_toPlus prend P explicite. Aucune régression : fichiers nouveaux, aucun fichier existant modifié au-delà de l'aggregator/READMEs.

See #2159 (contribution partielle, l'Epic reste ouverte — Partie 61 #12891 en review parallèle, veines restantes identifiées).

[jsboige]

[Hermes] — COMMENT — PASS (contrainte token : COMMENT only, self-review cap)

Deep-read du module au head 4291feaf avec vérifications mécaniques :

1. Twin-parity vérifiée par script : les 12 théorèmes existent dans PlusConstruction.lean et PlusConstruction_en.lean avec énoncés byte-identiques (12/12 après normalisation whitespace) ; seules les docstrings diffèrent, namespaces Grothendieck vs Grothendieck_en — conforme à la convention #4980 Option A.
2. Sorry-scan clean : 0 sorry/admit/native_decide dans le code (le seul match est la docstring « Tous les sorry éliminés à la création »). Toutes les preuves délèguent aux lemmes canoniques de Mathlib.CategoryTheory.Sites.Plus (plusMap_id, toPlus_naturality, plusMap_toPlus, isoToPlus_hom/inv, toPlus_plusLift, plusLift_unique, plus_hom_ext, plusMap_plusLift) — des théorèmes-ponts assumés comme tels, pas des re-preuves risquées.
3. Claim README vérifiée : « 58 modules leaf » — comptage API tree au head = 116 fichiers .lean sous Grothendieck/ = 58 paires FR/EN exactement (55 + les 2 paires Partie 61/62). Cohérent avec le diff README (+3 par partie).
4. Couverture SGA 4 II.3 correcte : fonctorialité → naturalité de toPlus → identité (P⟶P⁺)⁺ → point fixe des faisceaux → propriété universelle (factorisation + unicité + hom_ext) — c'est bien l'ossature de II.3, et les variables de section (multiequalizers + colimits) sont les hypothèses standard du module Mathlib.
5. Security scan clean.

Seule réserve (mineure) : la compilation Lean elle-même repose sur le CI — au moment de la review les checks sont pending (famine de runners #12817). Les délégations étant des appels directs à des lemmes Mathlib existants avec signatures attendues, le risque est faible, mais le verdict green suppose le CI passé.

[jsboige]

[INFO po-2027 c.1331p58] Rebase du conflit avec main (Partie 61 SitesComparison mergée après l'ouverture) — branche repositionnée sur 87dffc2bd9c (pointe de main au moment du rebase).

Résolution des conflits (3 fichiers en overlap) :

• Grothendieck.lean (umbrella) : auto-merge — les imports SitesComparison (main) + PlusConstruction (cette PR) coexistent, aucun namespace en collision (vérifié : espaces de noms et imports Mathlib disjoints).
• README.md / README.en.md : union des lignes de table des Parties 61 + 62 ; ligne Build fusionnée. Au passage, réalignement des compteurs périmés des deux côtés sur la vérité disque mesurée (find/ls sur l'arbre rebasé) : 59 leaf FR + 59 siblings _en + 1 umbrella (les deux README disaient 58/58 alors que Partie 61 + cette PR en ajoutent chacun une paire), colonne Lignes de l'umbrella 227→257 (wc -l mesuré).

Validation post-rebase (règle B : preuve relancée APRÈS le rebase, pas héritée du vert d'avant) :

• lake build (miroir FS natif WSL ~/lean-projects/gr_mirror, packages partagés lt_pkgs — revs manifest identiques aux deux lakes, vérifiées avant réutilisation) : SUCCESS — « Build completed successfully (2921 jobs) », avec explicitement ✔ Built Grothendieck.PlusConstruction (46s), ✔ Built Grothendieck.PlusConstruction_en (47s), ✔ Built Grothendieck.SitesComparison (15s) et l'umbrella ✔ Built Grothendieck — les deux Parties cohabitent.
• sorry code réel : 0 — les 2 occurrences par fichier sont de la prose de docstring (« Tous les sorrys éliminés à la création »), l'instrument canonique count_code_sorry.py (mode real) confirme.
• Contenu des modules .lean : inchangé par le rebase (même blob réappliqué) — la deep-read Hermes PASS du head précédent reste valable sur la substance ; seuls umbrella (auto-merge) et READMEs (conflits) diffèrent du 4291feaf d'origine.

Détail complet du diff vs main : 5 fichiers, +399/−10.