feat(lean,#2159): Partie 76 -- le faisceau est exactement le prefaisceau separe qui recolle by jsboige · Pull Request #16047 · jsboige/CoursIA

jsboige · 2026-09-13T22:39:09Z

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

Ce que cette PR ajoute

Le capstone de la veine des tiges ouverte par les Parties 72-75. Les Parties 74 et 75 avaient établi les deux moitiés séparément ; celle-ci les assemble en l'équivalence qui les fonde :

TopCat.Presheaf.IsSheaf F  ↔  GermSeparated T F  ∧  GermGluing T F

Sens	Contenu
⇒	reprend 74 (`eq_of_germ_eq_of_isSheaf`, la séparation) et 75 (`existsUnique_section_of_isLocallyRepresentable`, le recollement)
⇐	*le seul endroit du lake où la condition de faisceau est dérivée* plutôt que consommée** — voir ci-dessous

La Partie 75 avait besoin de IsSheaf comme hypothèse ; cette PR le produit. On construit la famille de germes lue sur les représentants locaux d'une famille couvrante compatible, on l'injecte dans le recollement fourni par l'hypothèse, et la séparation fait le reste — elle donne à la fois que la section obtenue restreint à chaque représentant, et qu'elle est l'unique à le faire. Aucune des deux hypothèses n'est superflue : la séparation est l'unicité, le recollement fournit l'existence.

Références : Mac Lane–Moerdijk [MM92] II.6, Stacks 00AK.

Le pont côté Mathlib est Presheaf.isSheaf_of_isSheafUniqueGluing_types (consommé dans Mathlib/Topology/Sheaves/LocalPredicate.lean:246).

Périmètre effectif — 5 fichiers

Énumération explicite, telle que gh pr view 16047 --json files la rend (l'organe perimeter la confronte à toute assertion du body, #11268) :

#	Fichier	Rôle
1	`Grothendieck/StalkCharacterization.lean` (152 l.)	le module FR neuf — le livrable
2	`Grothendieck/StalkCharacterization_en.lean` (149 l.)	son jumeau `_en` (convention EPIC #4980)
3	`grothendieck_lean/Grothendieck.lean` (+2/−0)	umbrella — ajout des imports
4	`grothendieck_lean/README.md` (+10/−9)	table + compteurs FR
5	`grothendieck_lean/README.en.md` (+9/−8)	table + compteurs EN

Aucun fichier .github/workflows/** touché, aucun mouvement de baseline ni de seuil.

Validation (§B)

B.1 — compte de sorry réel (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) : 0 avant → 0 après, inchangé. naive_sorry 135 → 136 (la seule occurrence ajoutée est la mention en prose « Aucun sorry introduit » du header bilingue, que le mode real de la CI strip — c'est exactement la classe que le passage prose-header → real du 2026-07-12 existe pour absorber).

B.2 — lake build local SUCCESS (WSL, leanprover/lean4:v4.33.0, Mathlib db584cd6) :

✔ [3351/3352] Built Grothendieck (17s)
Build completed successfully (3352 jobs).

Le build est fait dans le sandbox WSL ~/groth-build, pas sur DrvFs : Mathlib y est chaud (lake exe cache get), et les modules neufs compilent isolément (Built Grothendieck.StalkCharacterization, Built Grothendieck.StalkCharacterization_en) avant le build d'ensemble. Ci-joint les sorties.

B.3 — proof-integrity : CÂBLÉ ET COUVRANT (ce n'est pas le cas « non applicable »). lean-grothendieck.yml appelle lean-axiom.yml avec target-modules: "*" — la liste est dérivée au runtime du contenu du lake (#10889), donc le module neuf est dans la cible par construction et le caveat « vert hors-cible » (#8782) ne s'applique pas. allow-axioms: "", fail-on-sorry: true.

i18n — python scripts/lean/check_i18n_siblings.py <lake> : StalkCharacterization_en.lean OK, 0 drift / 0 orphan. Contrôle indépendant : après strip des docstrings et commentaires, les corps de code sont identiques ligne à ligne (67 lignes) ; la seule divergence est la ligne de fermeture de namespace, qui est la divergence prescrite par la convention.

Note honnête — le compteur README

scripts/lean/check_grothendieck_readme.py lit git ls-tree -r origin/main (l.141), pas HEAD. Lancé sur cette branche il remonte donc ORPHAN_IN_TABLE: StalkCharacterization ×2 : le README (75) est en avance sur origin/main (74), ce qui est la définition d'une branche de feature non mergée. Réconciliation mesurée après merge : table FR 75 = table EN 75 = claims 75 = disque 75. Le compteur n'est pas câblé en CI (grep -rln check_grothendieck_readme .github/ vide), donc il ne bloque rien ; il est signalé ici pour qu'un reviewer ne lise pas ce rouge comme un défaut.

Observation hors scope (signalée, non corrigée ici)

L'umbrella Grothendieck.lean importe explicitement 83 modules, mais 7 leaf FR présents sur disque n'y figurent pas :

LocalSurjectivitySpectrum, Spaces, SpacesMathlib, SpacesSubcanonical, StalkPoints (P73), StalkSeparated (P74), Stalks (P72)

Le globs du lakefile les compile quand même, donc c'est une dérive de l'index umbrella, pas du build : lake build Grothendieck est vert. Elle préexiste à cette PR et n'est pas de son sujet — elle part en issue #16048, avec une question ouverte au coordinateur (étendre check_grothendieck_readme.py à une classe MISSING_FROM_UMBRELLA, sans quoi la dérive se reformera).

Correction d'une affirmation antérieure de ce body. Une première rédaction annonçait « quatre modules, dont StalkGluing_en », à partir d'une lecture partielle (les seules lignes 55-83 du fichier). Vérification faite par ensemble complet (comm sur les 74 leaf FR et les 74 jumeaux _en du disque vs les 83 imports) : les deux chiffres étaient faux, et l'inclusion de StalkGluing_en dans la liste l'était aussi. Le sous-ensemble _en n'est pas une dérive : 59 des 74 jumeaux sont absents de l'umbrella, ce que le README de ce lake documente explicitement par design (« l'umbrella n'importe pas tous les _en, par design »). Seuls les leaf FR font l'objet de l'observation. Le compte net est 7, pas 4.

See #2159.

🤖 Generated with Claude Code

…eau separe qui recolle Capstone de la veine des tiges (Parties 72-75). Les Parties 74 et 75 avaient etabli les deux moities separement ; cette partie les assemble en l'equivalence qui les fonde : IsSheaf F <-> <separation par les germes> /\ <recollement des familles localement representables> Le sens direct reprend 74 (`eq_of_germ_eq_of_isSheaf`) et 75 (`existsUnique_section_of_isLocallyRepresentable`). Le sens reciproque est le seul endroit du lake ou la condition de faisceau est DERIVEE plutot que consommee : la famille de germes lue sur les representants locaux d'une famille couvrante compatible est localement representable, le recollement fourni par l'hypothese en produit une section, et la separation donne a la fois qu'elle restreint a chaque representant et qu'elle est l'unique a le faire. Aucune des deux hypotheses n'est superflue. Nouveau module Grothendieck/StalkCharacterization.lean + jumeau _en (EPIC #4980), imports umbrella, README FR/EN resynchronises (comptes 74 -> 75). Mesures : lake build Grothendieck SUCCESS local (3352 jobs, WSL, v4.33.0) ; distinct_code_sorry = 0 inchange sur le lake. See #2159. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

github-actions · 2026-09-13T22:42:41Z

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2027:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-13) :

GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=2 cap=1)
NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

github-actions · 2026-09-13T23:24:45Z

Path-collision (organ #13359/#13615)

Cette PR #16047 (feat(lean,#2159): Partie 76 -- le faisceau est exactement le prefaisceau separe qui recolle) 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): recoller les familles de germes localement représentables #15601 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md, recouvrement de chemins 60% -- feat(lean): recoller les familles de germes localement représentables #15601 est deja sur main. (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159) (issues communes : [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159)
faible -- fix(notebook-lean,#15719): réparer les tables SymbolicAI sans altérer les notebooks #15958 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.en.md, MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/README.md
faible -- fix(lean,#16048): Grothendieck.lean umbrella -- ajouter 7 imports FR manquants #16068 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck.lean

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 · 2026-09-13T23:36:27Z

[INFO] rouge-non-reparable-lane -- justification ecrite (cycle c.1141, lane myia-po-2027:CoursIA)

Le PR gate de cette PR n'est pas un defaut de substance. Mesure firsthand de l'annotation (gh run view --job 103811147247 --log) :

[pr-gate] waiting on 0 check(s):
[pr-gate] settled: 28 check(s) green
[pr-gate] DWELL -- tete du 2026-09-13T22:37:50Z, 47 min -- plancher 120 min,
          reste 73 min, leve au premier balayage suivant 2026-09-14T00:37:50Z

0 check en attente, 28 checks verts : la jambe rouge est purement l'age de la tete (plancher DWELL de 120 min). Le gate l'ecrit lui-meme : « aucun geste manuel n'est requis » — le balayage horaire (pr-gate-stale-sweep.yml, cron 7 * * * *) re-agrege la jambe des que le plancher est ecoule.

Aucun geste de lane : un rerun de gate re-rend FAILURE sur DWELL tant que le plancher court, et un push le re-armerait pour 120 min de plus. Cette PR est la base de la pile du lake (#16066 est empilee dessus) — la pousser maintenant retarderait aussi l'enfant.

Voir #2159 (epic du lake) · lane myia-po-2027:CoursIA

…manquants Le bloc d'imports umbrella omettait 7 leaf FR presents sur disque : LocalSurjectivitySpectrum (Partie 67), Spaces (68), SpacesMathlib (70), SpacesSubcanonical (71), Stalks (72), StalkPoints (73), StalkSeparated (74). Le globs du lakefile.compile tous les modules par defaut, donc lake build Grothendieck reste vert : c'est une derive d'INDEX de lecture, pas de build. Mesure pre/post : - HEAD main : 74 FR disque, 83 imports umbrella, 7 FR manquants - Cette PR : 74 FR disque, 90 imports umbrella, 0 FR manquants Insertions par ordre alphabetique dans leurs sections du bloc import. Le suivi d'un organe MISSING_FROM_UMBRELLA pour scripts/lean/ check_grothendieck_readme.py reste ouvert (defer ai-01, cf issue #16048 "question ouverte") -- sujet propre, pas absorbe en rider. EPIC #2159 ; voir PR #16047 (Partie 75 StalkGluing, declencheur de la derive) et #15474 (nettoyage precedent du drift README, surface soeur).

…manquants (#16068) * fix(lean,#16048): Grothendieck.lean umbrella -- ajouter 7 imports FR manquants Le bloc d'imports umbrella omettait 7 leaf FR presents sur disque : LocalSurjectivitySpectrum (Partie 67), Spaces (68), SpacesMathlib (70), SpacesSubcanonical (71), Stalks (72), StalkPoints (73), StalkSeparated (74). Le globs du lakefile.compile tous les modules par defaut, donc lake build Grothendieck reste vert : c'est une derive d'INDEX de lecture, pas de build. Mesure pre/post : - HEAD main : 74 FR disque, 83 imports umbrella, 7 FR manquants - Cette PR : 74 FR disque, 90 imports umbrella, 0 FR manquants Insertions par ordre alphabetique dans leurs sections du bloc import. Le suivi d'un organe MISSING_FROM_UMBRELLA pour scripts/lean/ check_grothendieck_readme.py reste ouvert (defer ai-01, cf issue #16048 "question ouverte") -- sujet propre, pas absorbe en rider. EPIC #2159 ; voir PR #16047 (Partie 75 StalkGluing, declencheur de la derive) et #15474 (nettoyage precedent du drift README, surface soeur). * Fix: Grothendieck.lean umbrella — réordonner Spaces* après SieveOps Suite à revue Hermès CONCERNS (cycle :39, 2026-09-13 23:41Z) qui constatait que les 3 imports `Spaces*` insérés par cette PR étaient placés avant `SieveLattice` / `SieveOps`, créant une inversion alphabétique introduite par cette PR (la 4ᵉ du bloc FR, qui passe de 3 à 4 au head d7723b4). Fix : déplacer `import Grothendieck.Spaces`, `import Grothendieck.SpacesMathlib`, `import Grothendieck.SpacesSubcanonical` après `SieveOps`, restaurant l'ordre alphabétique revendiqué par le body PR. Le bloc FR passe de 4 à 3 inversions (les 3 pré-existantes ExceptionalTriple/Equivalences, PlusConstruction/MonoidalCategories, Sheafification/SheafTopologySpectrum). Contenu sémantique inchangé : aucun module ajouté ni retiré, aucun sorry, aucune ligne de preuve touchée. La surface reste purement déclarative (+3/-3 net, +0 import). Anti-régression : `lake build Grothendieck` reste vert (le `globs` du lakefile `#[`Grothendieck.*]` compile tous les modules indépendamment de l'ordre umbrella — cf body PR §Pourquoi cette dérive existait). L'umbrella est un index de lecture humain, pas un fichier de build. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * Fix: Grothendieck.lean umbrella -- deplacer Spaces* apres Sites* (4e inversion maintenue par repair c.1145) Geste exact ai-01 DM msg-20260914T041309-826ofx (c.1150) : Le repair precedent (commit 9989535, c.1145) avait deplace les 3 imports Spaces* apres SieveOps (lignes 75-77), ce qui retablissait l'ordre alphabetique dans la fenetre 71-77 (Sie* < Spa*) -- mais l'inversion n'avait pas disparu : elle avait avance d'une ligne. Le defaut etait au bord de la fenetre verifiee : L78 SitePoints < L75-77 Spa*, soit 4e inversion du bloc FR (la 4e etait juste deplacee, pas levee). Le geste exact = deplacer les lignes 75-77 APRES la ligne 80 (SitesComparison_en). Ordre resultant : SieveGenerate, SieveLattice, SieveOps, SitePoints, SitesComparison, SitesComparison_en, Spaces, SpacesMathlib, SpacesSubcanonical, StalkGluing, ... Verification : SieveOps < SitePoints (e<t) ; SitePoints < SitesComparison (P<s) ; SitesComparison < Spaces (i<p) ; SpacesSubcanonical < StalkGluing (p<t). Zero inversion dans la zone. Mesure post-fix (script Python sur le fichier) : - Imports FR : 74 (inchange vs main 67 + 7 nouveaux) - Inversions FR : 3 = etat main (ratchet neutre) - Les 3 inversions residuelles sont preexistantes et inchangees : ExceptionalTriple/Equivalences, PlusConstruction/MonoidalCategories, Sheafification/SheafTopologySpectrum. Le commentaire de repair precedent ("repasse de 4 a 3") etait faux a la mesure : le repair c.1145 n'avait pas leve la 4e inversion, il l'avait juste deplacee. Ce push la leve effectivement et le chiffre "3" devient vrai. Tell c.1102 ★★★★★ anti-stonewall x54e : geste effectif (code change re-mesure = 3), pas declaration verbale. Tell NEW c.564 ★★★ fondateur : la levee formelle exige une re-revue tierce Hermes OU une approbation tierce avec phrase affirmative. ai-01 tiers DM : "des que le deplacement est pousse, je re-mesure moi-meme et je leve". Tell NEW c.566 ★★★★ fondateur : git push reset DWELL mecaniquement. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Co-authored-by: myia-po-2027 <po-2027@coursia.lan>

Mathlib calcule les deux tiges du gratte-ciel separement, mais ne pose nulle part la notion de support d'un prefaisceau ni le calcul du sien. Cette partie les ajoute et assemble ce que la reunion des deux isomorphismes signifie : support (skyscraper p_0 A) = closure {p_0} Le sens direct transporte IsTerminal A vers la tige par l'iso de specialisation : une tige terminale force A terminal, ce qui contredit l'hypothese. Le sens reciproque transporte l'iso de non-specialisation vers l'objet terminal. Aucun des deux isomorphismes n'est superflu, et l'hypothese IsEmpty (IsTerminal A) est nommee, pas implicite : sans elle, un gratte-ciel de valeur terminale a un support vide alors que closure {p_0} est non vide. Corollaires : support = {p_0} pour p_0 ferme (le nom du faisceau est justifie), et la dichotomie des tiges point par point. Deux frictions du Mathlib de ce lake, mesurees et documentees dans le module : le niveau d'univers des morphismes de C est contraint a celui des points de X (section "We need to restrict universe level" de Skyscraper.lean), et IsTerminal y est un TYPE et non une Prop -- d'ou IsEmpty (IsTerminal _) la ou on attendrait non (IsTerminal _). Nouveau module Grothendieck/Skyscraper.lean + jumeau _en (EPIC #4980), imports umbrella, README FR/EN resynchronises (comptes 75 -> 76). Empile sur #16047 (Partie 76, encore ouverte) : la Partie 77 presuppose la 76. Mesures : lake build Grothendieck SUCCESS local (3357 jobs, WSL, v4.33.0) ; count_code_sorry distinct_code_sorry = 0 inchange ; check_i18n_siblings OK ; comptes disque 76 leaf FR + 76 leaf _en + 1 umbrella = 154 fichiers .lean. See #2159. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…écutée in-kernel Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #16047 Tranche 3 de #15700 : le 3e fichier du périmètre, le notebook compagnon natif des deux modules livrés par #16167. Empilée sur cette branche, dont elle importe Conway.CHSHQuantum. Contenu — 26 cellules dont 8 de code, exécutées par un kernel Lean 4 réel (lean4-wsl-conway, --cd vers le lake conway_lean au pin leanprover/lean4:v4.32.1) : - navigation vers Lean-13 (contextualité) et Lean-16f (libre arbitre) ; - tableau comparatif déterministe / randomisé / quantique, chaque ligne portant le statut de sa preuve — « prouvé dans ce lake » vs « importé de Mathlib » ; - 3 exemples guidés compilés : #check de la signature exacte de tsirelson_bound, #print axioms des 5 déclarations ([propext, Classical.choice, Quot.sound], aucun sorryAx), #eval de la frontière classique (score 2 atteint, mélange équilibré -> 0) ; - un contrôle positif de kernel (#eval 2+2 -> 4) : les imports du REPL sont paresseux, un kernel retombé sur le lake-stub répond muet (#11874) ; - 3 exercices bornés, stubs à corps trivial, aucun raise/assert False (C.1) ; - une section de limites nommées : saturation de 2*sqrt(2) non établie, aucune construction de Pauli, pas de borne en norme d'opérateur. Le kernelspec déclaré est lean4-wsl-conway et non lean4-wsl comme le nomme le body de l'issue : mesuré, lean4-wsl lancé depuis MyIA.AI.Notebooks/SymbolicAI/Lean (qui n'est pas un lake) retombe sur le stub et ne résout ni Conway ni Mathlib. Raisonnement complet et mesures au body de PR. Les deux organes de validation de ces notebooks sont par ailleurs aveugles au rouge Lean — signalé séparément en #16176, non traité ici. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

…son (tranche 3, empilée sur #16167) (#16177) * feat(lean,#15700): notebook natif Lean-13b — la borne de Tsirelson exécutée in-kernel Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #16047 Tranche 3 de #15700 : le 3e fichier du périmètre, le notebook compagnon natif des deux modules livrés par #16167. Empilée sur cette branche, dont elle importe Conway.CHSHQuantum. Contenu — 26 cellules dont 8 de code, exécutées par un kernel Lean 4 réel (lean4-wsl-conway, --cd vers le lake conway_lean au pin leanprover/lean4:v4.32.1) : - navigation vers Lean-13 (contextualité) et Lean-16f (libre arbitre) ; - tableau comparatif déterministe / randomisé / quantique, chaque ligne portant le statut de sa preuve — « prouvé dans ce lake » vs « importé de Mathlib » ; - 3 exemples guidés compilés : #check de la signature exacte de tsirelson_bound, #print axioms des 5 déclarations ([propext, Classical.choice, Quot.sound], aucun sorryAx), #eval de la frontière classique (score 2 atteint, mélange équilibré -> 0) ; - un contrôle positif de kernel (#eval 2+2 -> 4) : les imports du REPL sont paresseux, un kernel retombé sur le lake-stub répond muet (#11874) ; - 3 exercices bornés, stubs à corps trivial, aucun raise/assert False (C.1) ; - une section de limites nommées : saturation de 2*sqrt(2) non établie, aucune construction de Pauli, pas de borne en norme d'opérateur. Le kernelspec déclaré est lean4-wsl-conway et non lean4-wsl comme le nomme le body de l'issue : mesuré, lean4-wsl lancé depuis MyIA.AI.Notebooks/SymbolicAI/Lean (qui n'est pas un lake) retombe sur le stub et ne résout ni Conway ni Mathlib. Raisonnement complet et mesures au body de PR. Les deux organes de validation de ces notebooks sont par ailleurs aveugles au rouge Lean — signalé séparément en #16176, non traité ici. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(#16177): reparations markdown du preflight adjoint — pipes de tableau, formulation hypotheses, comptes Trois points de la review 5200122665 (exact-head d760cce), tous markdown-only (exception C.2, aucune re-execution due) : 1. Tableau d'intro : les pipes des inline-code `|score|` et `|expectedScore|` sont echappes en \| — GitHub les parsing comme delimiteurs de colonnes et rendait la table en un seul paragraphe. 2. Section 4 : « doit etre celle de Mathlib, sans elargissement ni restriction » remplacee par la formulation honnete alignee sur la base reparee (#16167) : reprise dont le sens « aucune hypothese retiree » est epingle par l'elaboration, le sens « aucune hypothese ajoutee » n'etant garde par aucun instrument (renvoi section 7). 3. Comptes : « huit classes » -> « sept » (Ring, PartialOrder, StarRing, StarOrderedRing, Algebra R, IsOrderedModule R, StarModule R ; IsCHSHTuple est un argument propositionnel, pas une 8e classe) dans le notebook et le README ; « six cellules de code » -> « huit » (execution_count 1..8) en conclusion. Sorties byte-identiques : seules 4 lignes source markdown du notebook et 1 ligne README changent. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

…ges (#16066) * feat(lean,#2159): Partie 77 -- le faisceau gratte-ciel, support et tiges Mathlib calcule les deux tiges du gratte-ciel separement, mais ne pose nulle part la notion de support d'un prefaisceau ni le calcul du sien. Cette partie les ajoute et assemble ce que la reunion des deux isomorphismes signifie : support (skyscraper p_0 A) = closure {p_0} Le sens direct transporte IsTerminal A vers la tige par l'iso de specialisation : une tige terminale force A terminal, ce qui contredit l'hypothese. Le sens reciproque transporte l'iso de non-specialisation vers l'objet terminal. Aucun des deux isomorphismes n'est superflu, et l'hypothese IsEmpty (IsTerminal A) est nommee, pas implicite : sans elle, un gratte-ciel de valeur terminale a un support vide alors que closure {p_0} est non vide. Corollaires : support = {p_0} pour p_0 ferme (le nom du faisceau est justifie), et la dichotomie des tiges point par point. Deux frictions du Mathlib de ce lake, mesurees et documentees dans le module : le niveau d'univers des morphismes de C est contraint a celui des points de X (section "We need to restrict universe level" de Skyscraper.lean), et IsTerminal y est un TYPE et non une Prop -- d'ou IsEmpty (IsTerminal _) la ou on attendrait non (IsTerminal _). Nouveau module Grothendieck/Skyscraper.lean + jumeau _en (EPIC #4980), imports umbrella, README FR/EN resynchronises (comptes 75 -> 76). Empile sur #16047 (Partie 76, encore ouverte) : la Partie 77 presuppose la 76. Mesures : lake build Grothendieck SUCCESS local (3357 jobs, WSL, v4.33.0) ; count_code_sorry distinct_code_sorry = 0 inchange ; check_i18n_siblings OK ; comptes disque 76 leaf FR + 76 leaf _en + 1 umbrella = 154 fichiers .lean. See #2159. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#2159): le mot « support » est gagne par stalk_dichotomy, pas pose dessus Finding A — le module demontre la necessite de `IsEmpty (IsTerminal A)` puis l'abandonnait dans la prose de ses freres. Trois docstrings portaient l'etiquette « sur le support » / « hors du support » pour des enonces qui ne supposent pas `hA` et ne parlent que de `closure {p0}` ; sans `hA`, `y in closure {p0}` ne dit rien du support (contre-exemple : valeur terminale, support vide, adherence non vide). Reparation retenue : (a) celle qui achete quelque chose. `stalk_dichotomy` prend desormais `hA` et conclut sur `support (skyscraper p0 A)`, par `rw [support_skyscraper p0 A hA]` — les branches disent alors litteralement « dans le support » / « hors du support », et « forme en tout point » devient vrai. Les deux docstrings de tige sont retitreese sur l'adherence, avec la mention explicite que les deux notions ne coincident que sous `hA`. Le mot « en moyenne » disparait. Aucun appelant externe de `stalk_dichotomy` (grep sur tout le depot) : le durcissement de signature ne casse rien. README FR+EN : colonne compte de lignes 161 -> 175. `lake build Grothendieck.Skyscraper Grothendieck.Skyscraper_en` — RC=0. Parite i18n : 43 lignes de code de chaque cote, 2 divergences (namespaces). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

… StalkCharacterization (#18665) The README table listed StalkCharacterization.lean at Partie 78 (ligne 189) but PR #16047 ships StalkCharacterization as Partie 76, while SerreMap (which already occupies Partie 78 at ligne 191) is the canonical Partie 78 per PR #16374. This created a numerical collision (Partie 78 listed twice). Tell c.11900 ★★ strict: confirmed first-hand via `gh pr list --state merged --search 2159` (Parties sequence as merged): Partie 76 = PR #16047 StalkCharacterization, Partie 78 = PR #16374 SerreMap. Fix: change Partie 78 to 76 on the StalkCharacterization row, preserving the StalkCharacterization content (the actual subject of the row). Trous 47-51, 55 remain: these are intentional numbering gaps in the Phase 5 shipment sequence (Phase 5 went 36 -> 46 -> 52, skipping 47-51; Partie 55 is split into 55a/55b/55c and not a single entry). Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

github-actions Bot added the lean-visibility-drift La PR ajoute des declarations lake non citees par AUCUN notebook (borne large) (#11703) label Sep 13, 2026

jsboige mentioned this pull request Sep 13, 2026

drift(lean,#2159): 7 leaf FR absents de l'umbrella Grothendieck.lean -- aucun organe ne surveille cette surface #16048

Closed

github-actions Bot mentioned this pull request Sep 13, 2026

fix(notebook-lean,#15719): réparer les tables SymbolicAI sans altérer les notebooks #15958

Merged

jsboige mentioned this pull request Sep 14, 2026

coord(po-2026:CoursIA): 82 PRs ouvertes, 14 groupes de collision intra-lane — survivants nommes, mesures #14214

Open

myia-ai-01 merged commit 0a005de into main Sep 14, 2026
32 of 37 checks passed

github-actions Bot mentioned this pull request Sep 15, 2026

chore(lean,#16154): umbrella Grothendieck FR-only — -17 imports EN + organe anti-derive #16228

Merged

github-actions Bot mentioned this pull request Sep 16, 2026

lean(#16334): SerreMap/SerreMap_en - miroir Serre de MathlibMap (grain 9) #16374

Merged

jsboige mentioned this pull request Oct 1, 2026

fix(grothendieck_lean,#2159): resync README table Partie 78 -> 76 for StalkCharacterization #18665

Merged

5 of 6 tasks

Navigation Menu

Repository navigation

feat(lean,#2159): Partie 76 -- le faisceau est exactement le prefaisceau separe qui recolle - #16047

feat(lean,#2159): Partie 76 -- le faisceau est exactement le prefaisceau separe qui recolle#16047
myia-ai-01 merged 1 commit into
mainfrom
lean/2159-p76-stalk-characterization

jsboige commented Sep 13, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026 •

edited

Loading

Uh oh!

jsboige commented Sep 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jsboige commented Sep 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Ce que cette PR ajoute

Périmètre effectif — 5 fichiers

Validation (§B)

Note honnête — le compteur README

Observation hors scope (signalée, non corrigée ici)

Uh oh!

github-actions Bot commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Path-collision (organ #13359/#13615)

Uh oh!

jsboige commented Sep 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jsboige commented Sep 13, 2026 •

edited

Loading

github-actions Bot commented Sep 13, 2026 •

edited

Loading