[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #14007

Summary

• Continue la saga sheaf de grothendieck_lean (Epic [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159 « nouveaux theoremes ») avec un module jumele FR/EN (Partie 64) qui pousse l'invariance de la condition de faisceau produit-equaliseur jusqu'a la forme equaliseur elle-meme (la Partie 63 l'a reliee a Presieve.IsSheaf; la Partie 7 a montre son invariance pour IsSheaf; personne n'a encore enonce l'invariance dans la forme equaliseur).
• Deux theoremes nouveaux (ni Mathlib ni la Partie 63 ne les enoncent sous cette forme) :
  • equalizer_sheaf_condition_iff_of_nat_equiv — la condition equaliseur (forme cribles, Equalizer.Sieve.w) est preservee dans les deux sens par une equivalence naturelle composant par composant. Version « forme equaliseur » de isSheaf_iff_of_nat_equiv (Partie 7).
  • equalizer_arrows_iff_sieve_generate — la condition equaliseur (forme arrows, Equalizer.Presieve.Arrows.w) equivaut a celle (forme cribles, Equalizer.Sieve.w) sur le crible Sieve.generate (ofArrows X π) engendre. Pont operationnel entre les deux formes.
• Preuves axiom-propres : rw / exact sur les lemmes Mathlib (Equalizer.Sieve.equalizer_sheaf_condition, Equalizer.Presieve.Arrows.sheaf_condition, Presieve.isSheafFor_iff_generate) et les theoremes deja mergees des Parties 63/7.

Changes

• Grothendieck/SheafConditionInvariance.lean (FR) — nouveau module, namespace Grothendieck.
• Grothendieck/SheafConditionInvariance_en.lean (EN) — sibling byte-identique hors docstrings, namespace Grothendieck_en (convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980).
• Grothendieck.lean (agregateur) — +2 imports (SheafConditionInvariance, SheafConditionInvariance_en).

Review Checklist

• 1. Scope — PR = 1 sujet (2 theoremes de la saga sheaf); fichiers confines a grothendieck_lean (3 fichiers, +211/−0).
• 2. Post-fix validation — lake build Grothendieck SUCCESS (2927 jobs, local, re-lance apres le dernier commit, sans aucun « URL has changed »); count_code_sorry.py --json → distinct_code_sorry = 0.
• 3. Pedagogical coherence — N/A (pas d'exercices notebook; module de preuve enrichissant coherentement la Partie 63, meme ordre logique equaliseur → invariance → genération).
• 4. Real execution — N/A (pas de notebook ni slides; build Lean verifie, exec_reel = lake build).
• 5. Regression check — git status propre (3 fichiers); les seuls symboles touches sont des lemmes Mathlib/Partie63-7 reutilises (pas modifies); aucun autre module grothendieck ne reference les deux nouveaux noms.

Anti-regression

• No sorry : count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean --json → distinct_code_sorry = 0 (avant comme apres; la Partie 64 est une pure addition). Note : grep -c sorry sur les fichiers touches sur-compte (114 naifs = les marqueurs « tous les sorrys elimines » dans les docstrings, contre 0 code sorry) — l'instrument de reference est count_code_sorry.py.
• Aucune suppression : 211 insertions, 0 deletion. Aucun code metier retire.
• Axiomes : preuves par rw/exact sur lemmes deja vettes (Mathlib + Parties 63/7 mergees) — pas de native_decide, pas de sorryAx, pas d'usage explicite de Classical.choice. Job CI proof-integrity (lean-grothendieck.yml → lean-axiom.yml, target-modules: "*", fail-on-sorry: true) couvre le module FR; le sibling _en est exclu par defaut (coherence lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889). Verification locale faite; le job CI confirmera sur la tete de la PR.

Notebook-specific

• N/A — aucun fichier .ipynb touche.

---

See #2159 (tranche de l'EPIC « nouveaux theoremes »), parent #1646.

[jsboige]

[Hermes] — #14053 feat(lean): grothendieck Partie 64 — invariance de la condition de faisceau égaliseur

Verdict: COMMENT (LGTM sous réserve de build non-local) — lecture DEEP.

Vérification réalisée (repo monté au head SHA cbabb11) :

• Axiome-propreté : scan des deux modules → aucun sorry de code, aucun sorryAx, aucun native_decide, aucun Classical.choice, aucun axiom. Les seuls matchs sorry sont dans des docstrings commençant par -- (« Tous les sorrys éliminés à la création » / « All sorrys eliminated at creation ») — le body prévient explicitement de ce faux positif grep -c sorry.
• Deux théorèmes présents : equalizer_sheaf_condition_iff_of_nat_equiv (l.77) et equalizer_arrows_iff_sieve_generate (l.100).
• Preuves : chaînes rw [← ...] + exact sur lemmes Mathlib/Parties 63/7. Théorème 1 se réduit à isSheaf_iff_of_nat_equiv (transport IsSheaf→forme égaliseur correct) ; théorème 2 passe par Arrows.sheaf_condition + Sieve.equalizer_sheaf_condition + isSheafFor_iff_generate (pont arrows↔sieve correct). Aucune déclaration de preuve vide.
• Sibling EN : diff normalisé (namespace Grothendieck_en→Grothendieck + strip docstrings) → le code de théorème est byte-identique entre FR et EN ; seuls les bloc-comments d'en-tête (docstrings FR↔EN) diffèrent. Convention i18n #4980 respectée.
• Agrégateur : Grothendieck.lean +2 imports confirmé dans le diff.

Limite honnête : lake build Grothendieck n'a pas pu être relancé ici (aucun outil Lean monté sur cette machine). La claim du body « 2927 jobs SUCCESS » repose sur le build local déclaré, corroborée mais non re-vérifiée de bout en bout. La structure des preuves (rw/exact sur lemmes mergeés) rend l'échec improbable, mais si le CI proof-integrity échoue sur la tête de PR, c'est la seule zone non couverte par cette review.

Aucun credential dans le diff (fichiers Lean purs). La PR est une pure addition (+211/−0) sans retrait de logique.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #14053 (feat(lean): grothendieck Partie 64 — invariance de la condition de faisceau egaliseur) 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): grothendieck Partie 65 — caracterisation de la condition de faisceau egaliseur #14056 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159)