feat(lean,#2159): Partie 61 SitesComparison — foncteurs continus et lemme de comparaison (SGA 4 III.1.6)

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: MED/guard #12881

Périmètre : 5 fichiers — Grothendieck/SitesComparison.lean (neuf FR, 158 lignes), Grothendieck/SitesComparison_en.lean (neuf EN, 147), Grothendieck.lean (imports umbrella + 2 entrées de substance FR/EN), README.md, README.en.md (ligne table 61 + compteurs réconciliés + ligne 59 EN rétro-comblée).

Summary

Partie 61 de l'hommage Grothendieck (#2159) : foncteurs continus et lemme de comparaison — le pont préfaisceau→faisceau, dernier chaînon niveau faisceaux non couvert par le lake (grep IsContinuous|sheafPushforward sur les 58 modules : 0 occurrence, mesuré firsthand avant écriture).

Cible tirée de Mathlib.CategoryTheory.Sites.Continuous (v4.32.1), non exploitée par le lake :

• sheafPushforwardContinuous_comp_sheafToPresheaf : le carré commute — pushforward continu puis oubli des faisceaux = précomposition par F.op (via Functor.sheafPushforwardContinuousCompSheafToPresheafIso).
• sheafPushforwardContinuous_id : pushforward continu le long de l'identité = identité.
• sheafPushforwardContinuous_comp : les pushforwards continus composent (contravariance en les foncteurs) — miroir faisceau de pullback_pullback (Partie 6).
• adjunction_sheafPushforwardContinuous : le lemme de comparaison (SGA 4 III.1.6) — si F ⊣ G avec F, G continus, les pushforwards continus sur les catégories de faisceaux sont adjoints. Les adjonctions descendent aux faisceaux sans sheafification explicite. Généralisation sites-arbitraires de pullbackPushforwardAdjunction (DirectImage.lean, niveau schémas).

Ré-groundtruth de l'Epic livré au passage (commentaire #2159 (comment)) : la cible nommée « encore ouverte : pullback_imap » du body était stale — livrée par #9762/#9818, duals #11820/#11917 ; le lake est à 58 leaf FR + 58 EN, 0 sorry réel.

Conformité discipline Lean (B)

1. Comptage sorry réel : avant = 0, après = 0 (python scripts/lean/count_code_sorry.py --json sur le lake : distinct_code_sorry: 0 ; naive_sorry: 104 = prose bilingue, l'écart 104/0 est la raison pour laquelle l'instrument est le script).
2. lake build Grothendieck SUCCESS, WSL local, worktree frais : Build completed successfully (2919 jobs) — log intégral des modules neufs : Built Grothendieck.SitesComparison (82s) / Built Grothendieck.SitesComparison_en (81s) (lake build Grothendieck.SitesComparison Grothendieck.SitesComparison_en, exit 0). Quatre itérations de compilation ont été nécessaires (def-vs-theorem sur Iso/Adjunction, ordre d'arguments (E := A), qualification Functor.whiskeringLeft) — la tête finale est celle qui build.
3. Proof integrity : câblage lean-grothendieck.yml (reusable lean-axiom.yml, target-modules: "*", fail-on-sorry: true) — atteint le module par clôture d'imports (module importé par l'umbrella Grothendieck.lean). 3 bridges sont des def (Iso/Adjunction sont des structures data-carrying, pas des Prop) : aucun axiome ajouté, miroir exact des defs Mathlib pontées.
4. Refactor prover : N/A — aucun script prover touché.

Ce diff

• 2 modules neufs (FR + sibling EN, pattern i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : namespace Grothendieck ↔ Grothendieck_en, énoncés/preuves byte-identiques, docstrings seules à différer).
• Root aggregator : 2 imports + 2 entrées de substance (FR + EN).
• READMEs : ligne table Partie 61 (les deux), toolchain corrigé v4.32.0→v4.32.1 (stale vs lean-toolchain réel), compteurs 58 leaf + 58 siblings (SheafCohomology/ sous-dossier inclus, mesuré find), ligne 59 EN rétro-comblée (le miroir EN accusait un retard d'une ligne — drift §E corrigé au passage).

Conformité

• L898 : aucune autre PR ouverte sur SitesComparison* (seule feat(lean,#2159): Partie 60 — dictionnaire Grothendieck <-> Lawvere-Tierney (frontière Partie 59 fermée) #12718, lane-mêmes fichiers différents — TopologyDictionary).
• Anti-régression : 0 preuve existante touchée (2 fichiers neufs + aggregator/README seuls).
• Catalogue byte-identique. 0 notebook, 0 secret, 0 emoji.

See #2159 (sous-grain de l'umbrella, cf ré-groundtruth)

Test plan

• lake build Grothendieck SUCCESS — Build completed successfully (2919 jobs) (WSL local, head d727bc6)
• lake build Grothendieck.SitesComparison Grothendieck.SitesComparison_en — modules neufs Built (82s/81s), exit 0
• Comptage sorry réel avant/après : 0/0 (count_code_sorry.py, champ distinct_code_sorry)
• Sibling checker : check_i18n_siblings.py SitesComparison_en.lean → 1/1 pairs byte-identical | 0 drift | 0 orphan | 0 unbuilt (re-vérifié APRÈS les 4 itérations de compilation)
• CI lean-grothendieck + proof-integrity verts sur la tête (file CI saturée — attendu)

🤖 Generated with Claude Code

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