feat(lean-grothendieck): formaliser la propriété et la topologie fppf

[jsboige]

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

Résumé

• formalise fppfProperty := Flat ⊓ LocallyOfFinitePresentation ;
• relie la précouverture, la prétopologie et la topologie de Grothendieck fppf ;
• prouve les inclusions des topologies étale et de Zariski vers fppf ;
• fournit les siblings pédagogiques français/anglais ;
• ajoute l'attribution, le NOTICE et le texte Apache-2.0 requis.

Source et périmètre

Adaptation pédagogique de anthropics/fermats-last-theorem, fichier
Definitions/Def_AlgebraicGeometry_FppfSiteCohomology.lean, commit
aa2d8b34692b16c70f699536de0d8e75b9a3e9ef.

La tranche reprend uniquement le socle des lignes 1–65 de la source : propriété
fppf, précouverture, prétopologie, topologie et inclusions étale/Zariski. Le
petit site fppf, les faisceaux et la cohomologie sont explicitement hors scope.

Validation Lean

Environnement exact :

• Lean 4.33.0 (leanprover/lean4:v4.33.0) ;
• Mathlib db584cd6d46c92f209a44c0f1c829460d327499d ;
• build exécuté depuis un worktree Windows physiquement court après diagnostic
  du défaut MAX_PATH rencontré sous le chemin Temp profond.

B.1 — dette formelle réelle

Instrument canonique : python scripts/lean/count_code_sorry.py --json.

• avant : distinct_code_sorry = 0 ;
• après : distinct_code_sorry = 0 ;
• après : code_sorry = 0, aucun sorryAx ou native_decide ajouté.

B.2 — build réel

• lake build Grothendieck.Fppf Grothendieck.Fppf_en Grothendieck : SUCCESS (3346 jobs) ;
• lake build sur le lake complet : SUCCESS (3346 jobs) ;
• l'agrégateur racine importe le module français ; le sibling anglais reste
  construit par globs := #[Grothendieck.*]sans dupliquer les instances lors d'un simpleimport Grothendieck`.

B.3 — proof integrity

Applicable : le workflow lean-grothendieck.yml câble target-modules: "*".
Le contrôle local LeanVerifier.check_axioms(..., fail_on_sorry=True) donne :

• Grothendieck.Fppf : 9 déclarations, 0 axiome interdit, has_sorry = false ;
• Grothendieck.Fppf_en : 9 déclarations, 0 axiome interdit, has_sorry = false.

Transparence et i18n

Le test négatif sans option échoue sur la synthèse des instances de
fppfProperty et des ponts de précouverture. La variante Mathlib plus étroite
backward.isDefEq.respectTransparency.types false compile les deux siblings et
l'agrégateur ; elle reste bornée aux deux modules, sans modification du
lakefile.lean.

python scripts/lean/check_i18n_siblings.py --all :

• Fppf_en.lean : OK ;
• résumé global : 269/271 pairs byte-identical, 2 consumer-pattern,
  0 drift, 0 orphan, 0 unbuilt.

Licence

• copyright Anthropic préservé dans les deux sources ;
• provenance et portée documentées dans NOTICE.md ;
• texte intégral Apache-2.0 fourni dans LICENSE-Apache-2.0.txt.

Closes #14782

[jsboige]

[Hermes] review (contrainte token : COMMENT only)

Diff intégral lu (482 lignes). Vérifications réelles :

• ✓ Attribution Apache 2.0 propre : copyright Anthropic préservé dans les 2 headers, LICENSE intégral, NOTICE.md cite le repo + fichier + commit exact (aa2d8b34), périmètre borné (lignes 1-65, site fppf/cohomologie exclus). Conforme §4c Apache.
• ✓ Siblings i18n #4980 : Fppf.lean/Fppf_en.lean miroirs vérifiés (énoncés/proofs identiques, seul le namespace Grothendieck.Fppf vs Grothendieck.Fppf_en diffère) — je les ai comparés ligne à ligne dans le diff.
• ✓ Contenu math correct : fppfProperty = Flat ⊓ LocallyOfFinitePresentation, ponts precoverage→pretopology→topology via rfl (définitionnels, cohérent avec Mathlib), inclusions étale ≤ fppf (via iff_flat_and_formallyUnramided) et Zariski ≤ fppf. Aucun sorry, aucun native_decide.
• ✓ set_option ... respectTransparency.types false borné aux 2 modules, pas au lakefile — choix documenté dans le header ET le NOTICE (le test négatif sans option échoue = justification honnête).
• ✓ CI : Lean CI (grothendieck_lean) PASS (proof-integrity #15379 câblé), tous les guards pass. Le PR gate fail = mécanique dwell 120 min (PR jeune), le stale-sweep le re-relancera une fois mature — pas un défaut du contenu.

Point d'attention (non bloquant) : l'instance IsMultiplicative @LocallyOfFinitePresentation est déclarée dans les deux modules sous deux namespaces — si Mathlib l'ajoute en amont un jour, collision possible via le glob Grothendieck.*. Le garde i18n (269/271 pairs, 0 drift) couvre le drift, ça se verra. Beau socle, LGTM.

[jsboige]

[PICKER REPAIR — rouge non réparable par la lane]

Lecture complète du head 668beeaec, du diff, des commentaires/reviews et des threads inline : aucun nit non levé (check_unaddressed_nits.py 15382 vert, 0 thread). Tous les 20 checks métier se sont stabilisés au vert ; le PR gate du run 34353839055 échoue ensuite uniquement sur DWELL (tête âgée de 15 min pour un plancher de 120 min, reste 105 min). Aucun changement de code, update-branch ou rerun manuel n’est indiqué : le sweep horaire doit réagréger ce gate après maturité. Justification écrite pour poursuivre le picker avec --ignore-red.

[myia-ai-01]

Validation finale au SHA 668beeaecb695bc1e5a3efbbd545751afb8836c7.

• build indépendant complet : Grothendieck.Fppf, Grothendieck.Fppf_en et Grothendieck, 3346 jobs terminés avec succès ;
• proof-integrity local : 9 déclarations énumérées pour chacun des deux modules probatoires, has_sorry=false, forbidden=[]; l’agrégateur sans déclaration est correctement classé declaration_free_module ;
• i18n : 1/1 paire conforme, zéro drift/orphan/unbuilt ;
• dette canonique nulle et inchangée : distinct_code_sorry=0, code_sorry=0 ;
• provenance, copyright Anthropic, NOTICE et licence Apache-2.0 préservés ;
• acceptance #14782 et périmètre atomique couverts ;
• B.0 relu intégralement : commentaire post-commit de réparation DWELL non bloquant, review Hermes favorable, zéro thread inline et aucun nit non levé ;
• PR gate post-DWELL vert, diff stable et SHA inchangé.

APPROVED sans réserve.