fix(lean,#16642): remove derived quantitative counts from Lean companion notebook prose

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb

@@ -29,7 +29,7 @@
     "  l'interpréteur Python pour valider empiriquement la conjecture.\n",
     "- **Lean-12b** (ce notebook) va plus loin : on **compile** réellement la preuve\n",
     "  Huang 2019 dans le lake `sensitivity_lean`, on interroge le compilateur via\n",
-    "  `#check` et `#print axioms`, et on vérifie **0 sorry**. C'est l'approche\n",
+    "  `#check` et `#print axioms`, et on vérifie **l'absence de sorry**. C'est l'approche\n",
     "  **formelle** : la conjecture est *prouvée*, pas seulement vérifiée sur cas.\n",
     "\n",
     "**Pourquoi les deux approches ensemble ?** La première motive (pourquoi se soucier de\n",
@@ -59,7 +59,7 @@
    "source": [
     "## 1. Import du lake `Sensitivity`\n",
     "\n",
-    "Le lake exporte 4 modules. L'import natif déclenche la résolution de la chaîne\n",
+    "Le lake exporte ses modules. L'import natif déclenche la résolution de la chaîne\n",
     "Mathlib (via la jonction locale).\n",
     "\n",
     "**Comment Lean 4 résout l'import** : `import Sensitivity` déclenche la lecture du\n",
@@ -332,7 +332,7 @@
     "### Preuve sans `sorry` — `#print axioms`\n",
     "\n",
     "Le théorème phare ne dépend que des 3 axiomes standards de Lean (pas de\n",
-    "`sorryAx`), ce qui prouve que la preuve est **complète** (0 sorry).\n",
+    "`sorryAx`), ce qui prouve que la preuve est **complète** (sans sorry).\n",
     "\n",
     "**Trois axiomes standards de Lean 4** :\n",
     "1. `propext` : l'extensionnalité des propositions — si $p \\leftrightarrow q$ et\n",
@@ -1552,7 +1552,7 @@
    "source": [
     "## Conclusion\n",
     "\n",
-    "Ce companion **natif** exhibe la preuve formelle 0-sorry de Huang 2019 dans le\n",
+    "Ce companion **natif** exhibe la preuve formelle sans-sorry de Huang 2019 dans le\n",
     "kernel Lean lui-même : `#check` et `#print axioms` rendent les signatures et les\n",
     "axiomes réels produits par le compilateur, sans intermédiaire Python. La\n",
     "sensitivity conjecture est **résolue formellement**.\n",
@@ -1566,7 +1566,7 @@
     "**Enseignements** :\n",
     "1. **`#check` et `#print axioms` sont les outils de certification**. Sans eux,\n",
     "   on est réduit à un acte de foi sur les preuves. Avec eux, on a une garantie\n",
-    "   syntaxique ET une garantie de complétude (0 `sorry`).\n",
+    "   syntaxique ET une garantie de complétude (sans `sorry`).\n",
     "2. **L'architecture stratifiée** (vocabulaire → lemme → théorème → portée) est\n",
     "   universelle en Lean 4. Lean-12 (Sensitivity), Lean-12b (Sensitivity\n",
     "   formelle), Lean-14 (Finiteness), Lean-16 (Conway Free Will) la reproduisent.\n",

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb

@@ -20,7 +20,7 @@
     "\n",
     "**Kernel** : Python 3 (Mathlib excerpts shown via `subprocess` -> WSL `lean`)\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "> *On peut tout faire pourvu qu'on prenne le temps de comprendre les choses.* -- A. Grothendieck"
    ]
@@ -62,7 +62,7 @@
     "\n",
     "**Note technique sur l'exécution**\n",
     "\n",
-    "Ce notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec verification sorry = 0. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n",
+    "Ce notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec verification de l'absence de sorry. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n",
     "\n",
     "Pour les exercices interactifs, `run_lean(snippet)` ecrit un snippet temporaire et l'execute dans l'environnement Lake du projet, ce qui donne acces a tout Mathlib."
    ]
@@ -117,7 +117,7 @@
     "\n",
     "Cette patiente est l'oppose du **coup de force**. Le present notebook pretend modestement illustrer la semence -- non la recolte.\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n"
    ]
   },
@@ -1784,8 +1784,8 @@
     "\n",
     "Le sous-projet `MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/` (workspace Lake avec `lakefile.lean`) accompagne cet hommage. Le projet a evolue depuis sa creation :\n",
     "\n",
-    "- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + 9 fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n",
-    "- **0 sorry** comme terme de preuve.\n",
+    "- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n",
+    "- **Aucun sorry** comme terme de preuve.\n",
     "- Les modules originaux couverts pedagogiquement dans ce notebook : `CategoryAndSites`, `SchemesTour`, `ZariskiSite`, `MathlibMap`, `Calibration`, `SieveLattice`. Les modules supplémentaires (SheafBasics, SieveOps, CoverageGen, CanonicalProps, SieveGenerate, DenseTopology, Sheafification, LeftExact, Subcanonical, SitePoints, SheafHom, ConstantSheaf, Conservative, SheafCohomology/Basic, MayerVietorisSquare, SheafCohomology/MayerVietoris, SheafCohomology/Cech + Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) approfondissent la théorie des faisceaux, des sites et de la cohomologie, ainsi que les fondamentaux catégoriels.\n",
     "\n",
     "Lie a l'Epic #1646 (Grothendieck Lean side-track).\n",
@@ -1810,7 +1810,7 @@
     "4. **Faisceaux et recollement**. Dans `Mathlib.Topology.Sheaves.Sheaf`, identifier la condition de recollement qu'un `Presheaf` doit satisfaire pour etre un `Sheaf`. Que dit-elle intuitivement ?\n",
     "5. **Pretopologie / topologie**. Dans `BigZariski.lean`, lire la preuve de `zariskiTopology_eq`. Combien de lignes ? Quelle tactique principale ?\n",
     "\n",
-    "---\n",
+    "***\n",
     "\n",
     "**Navigation** : [<< Lean-14 Finiteness-Derivatives](Lean-14-Finiteness-Derivatives.ipynb) | [Lean-16b Conway Tribute >>](Lean-16b-Conway-Game-of-Life-Lean.ipynb) | [Index](README.md)"
    ]

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb

@@ -32,7 +32,7 @@
     "\n",
     "1. Naviguer dans le projet Lake `grothendieck_lean/` et comprendre sa structure de modules.\n",
     "2. Lire les sources Lean des modules pedagogiques (parmi ceux du projet) et identifier les constructions cles (cribles, topologies, schemas, site de Zariski).\n",
-    "3. Analyser les 4 micro-preuves de Calibration (P1-P4) et comprendre les tactiques utilisees.\n",
+    "3. Analyser les micro-preuves de Calibration (P1-P4) et comprendre les tactiques utilisees.\n",
     "4. Interpreter les identites de pullback dans le treillis des cribles.\n",
     "5. Utiliser la carte MathlibMap comme index de reference des structures grothendieckiennes disponibles.\n",
     "6. Explorer interactivement les definitions via des snippets Lean executes en WSL.\n",
@@ -272,25 +272,25 @@
    "source": [
     "## 1. Le projet Lake `grothendieck_lean/`\n",
     "\n",
-    "Le projet `grothendieck_lean/` est un **workspace Lake** dedie a l'exploration pedagogique du langage mathematique de Grothendieck dans Mathlib 4. Il contient des modules sous le namespace `Grothendieck`. Cet atelier en catalogue une selection (modules pedagogiques detailles + modules avances couvrant faisceaux, cohomologie et Cech) ; les 9 autres (Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) sont des fondamentaux categoriels non traites ici.\n",
+    "Le projet `grothendieck_lean/` est un **workspace Lake** dedie a l'exploration pedagogique du langage mathematique de Grothendieck dans Mathlib 4. Il contient des modules sous le namespace `Grothendieck`. Cet atelier en catalogue une selection (modules pedagogiques detailles + modules avances couvrant faisceaux, cohomologie et Cech) ; les autres (Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) sont des fondamentaux categoriels non traites ici.\n",
     "\n",
     "### Architecture du projet\n",
     "\n",
     "```\n",
     "grothendieck_lean/\n",
     "  lakefile.lean          -- dépendance mathlib4\n",
     "  lean-toolchain         -- leanprover/lean4:v4.31.0-rc1\n",
-    "  Grothendieck.lean      -- module racine (importe les 32 sous-modules)\n",
+    "  Grothendieck.lean      -- module racine (importe les sous-modules)\n",
     "  Grothendieck/\n",
     "    CategoryAndSites.lean  -- Part 1: Cribles, topologies, 3 axiomes\n",
     "    SchemesTour.lean       -- Part 2: Scheme, Spec, Gamma\n",
     "    ZariskiSite.lean       -- Part 3: Pretopologie de Zariski, bridge theorem\n",
     "    MathlibMap.lean        -- Part 4: #check living index\n",
-    "    Calibration.lean       -- Part 5: 4 micro-preuves P1-P4\n",
+    "    Calibration.lean       -- Part 5: micro-preuves P1-P4\n",
     "    SieveLattice.lean      -- Part 6: Identites de pullback\n",
     "```\n",
     "\n",
-    "**Convention** : tous les modules utilisent le namespace `Grothendieck` et 0 sorry en code de production."
+    "**Convention** : tous les modules utilisent le namespace `Grothendieck` et aucun sorry en code de production."
    ]
   },
   {
@@ -462,13 +462,13 @@
     "|--------|--------|---------------|\n",
     "| Modules | -- | pedagogiques + avances (faisceaux, cohomologie, Cech + fondamentaux categoriels) |\n",
     "| Lignes totales | -- | Projet pedagogique etendu (modules namespace Grothendieck, originaux FR) |\n",
-    "| sorry | 0 | Toutes les preuves sont completes |\n",
+    "| sorry | aucun | Toutes les preuves sont completes |\n",
     "| Toolchain | v4.31.0-rc1 | Version recente de Lean 4 |\n",
     "\n",
     "**Points cles** :\n",
-    "1. Le module racine `Grothendieck.lean` importe les 32 sous-modules. Un `lake build Grothendieck` compile tout.\n",
+    "1. Le module racine `Grothendieck.lean` importe les sous-modules. Un `lake build Grothendieck` compile tout.\n",
     "2. Chaque module est autonome (imports Mathlib directs, pas de dependances inter-modules autres que via Mathlib).\n",
-    "3. Les 4 micro-preuves de `Calibration.lean` sont les seules preuves non triviales ; le reste est des `#check` et des `example`/`theorem` a une ligne."
+    "3. Les micro-preuves de `Calibration.lean` sont les seules preuves non triviales ; le reste est des `#check` et des `example`/`theorem` a une ligne."
    ]
   },
   {
@@ -1560,9 +1560,9 @@
     "tags": []
    },
    "source": [
-    "## 5. Calibration : les 4 micro-preuves (P1-P4)\n",
+    "## 5. Calibration : les micro-preuves (P1-P4)\n",
     "\n",
-    "Le module `Calibration` est le coeur **preuve** du projet. Il contient 4 theoremes qui exercice des stratégies de preuve différentes :\n",
+    "Le module `Calibration` est le coeur **preuve** du projet. Il contient des theoremes qui exercent des stratégies de preuve différentes :\n",
     "\n",
     "| Preuve | Stratégie | Enonce |\n",
     "|--------|----------|--------|\n",
@@ -1746,7 +1746,7 @@
     "```\n",
     "Stratégie : un lemme general de Mathlib qui dit que la topologie ⊥ rend tout prefaisceau faisceau. Le prover doit identifier ce lemme.\n",
     "\n",
-    "> **Note** : ces 4 preuves sont les cibles de calibration pour le harness de preuve automatique (Epic #1453). Elles servent de \"tests unitaires\" pour verifier que le prover sait utiliser différentes stratégies."
+    "> **Note** : ces preuves sont les cibles de calibration pour le harness de preuve automatique (Epic #1453). Elles servent de \"tests unitaires\" pour verifier que le prover sait utiliser différentes stratégies."
    ]
   },
   {
@@ -2439,7 +2439,7 @@
    "source": [
     "### Lecture des 18 vérifications : l'index est vivant, pas déclaré\n",
     "\n",
-    "La sortie énumère les 18 `#check` que `MathlibMap.lean` fait passer au noyau — 18 noms effectivement présents dans le Mathlib vendu au moment du build. Lisez la structure de la liste : les entrées 1-2 (`yoneda`, `coyoneda`) attestent le socle de théorie des catégories ; 3-10 balayent la hiérarchie cribles puis topologies de Grothendieck (`trivial`, `discrete`, `dense` — les trois topologies extrémales du cours) ; 11-13 les faisceaux (`IsSheaf`, `IsSeparated`, `TopCat.Sheaf`) ; 14-18 le monde des schémas (`Scheme`, `Spec`, `Γ` le foncteur des sections globales, et les deux foncteurs d'oubli vers `TopCat` et `LocallyRingedSpace`). Ce qui fait la valeur de cet index : chaque entrée a été **vérifiée par compilation**, pas copiée d'une documentation — si une future version de Mathlib renomme `Scheme.Γ`, le `#check` correspondant passera au rouge et signalera la divergence immédiatement. Les absents (ce que Mathlib n'a pas encore) restent documentés dans le module lui-même, section « ce que Mathlib a et n'a pas encore »."
+    "La sortie énumère les `#check` que `MathlibMap.lean` fait passer au noyau — les noms effectivement présents dans le Mathlib vendu au moment du build. Lisez la structure de la liste : les premières entrées (`yoneda`, `coyoneda`) attestent le socle de théorie des catégories ; viennent ensuite la hiérarchie cribles puis topologies de Grothendieck (`trivial`, `discrete`, `dense` — les trois topologies extrémales du cours) ; puis les faisceaux (`IsSheaf`, `IsSeparated`, `TopCat.Sheaf`) ; enfin le monde des schémas (`Scheme`, `Spec`, `Γ` le foncteur des sections globales, et les deux foncteurs d'oubli vers `TopCat` et `LocallyRingedSpace`). Ce qui fait la valeur de cet index : chaque entrée a été **vérifiée par compilation**, pas copiée d'une documentation — si une future version de Mathlib renomme `Scheme.Γ`, le `#check` correspondant passera au rouge et signalera la divergence immédiatement. Les absents (ce que Mathlib n'a pas encore) restent documentés dans le module lui-même, section « ce que Mathlib a et n'a pas encore »."
    ]
   },
   {
@@ -2937,24 +2937,24 @@
     "\n",
     "### Recapitulatif\n",
     "\n",
-    "| Module | Lignes | Contenu | Theoremes cles |\n",
-    "|--------|--------|---------|---------------|\n",
-    "| `CategoryAndSites` | 106 | Cribles, topologies, 3 axiomes | `top_covers`, `pullback_cover`, `transitivity` |\n",
-    "| `SchemesTour` | 79 | Scheme, Spec, Gamma | Foncteurs d'oubli, homeomorphisme d'isos |\n",
-    "| `ZariskiSite` | 84 | Pretopologie -> topologie | `zariski_topology_eq`, sous-canonique |\n",
-    "| `MathlibMap` | 90 | Index vivant #check | 16 verifications structurelles |\n",
-    "| `Calibration` | 80 | 4 micro-preuves P1-P4 | `trivial_le_discrete`, `pullback_top`, `zariski_eq_pretopology`, `isSheaf_trivial` |\n",
-    "| `SieveLattice` | 88 | Pullback identities | `pullback_id`, `pullback_pullback`, `pullback_bot`, `pullback_monotone` |\n",
+    "| Module | Contenu | Theoremes cles |\n",
+    "|--------|---------|---------------|\n",
+    "| `CategoryAndSites` | Cribles, topologies, 3 axiomes | `top_covers`, `pullback_cover`, `transitivity` |\n",
+    "| `SchemesTour` | Scheme, Spec, Gamma | Foncteurs d'oubli, homeomorphisme d'isos |\n",
+    "| `ZariskiSite` | Pretopologie -> topologie | `zariski_topology_eq`, sous-canonique |\n",
+    "| `MathlibMap` | Index vivant #check | verifications structurelles |\n",
+    "| `Calibration` | micro-preuves P1-P4 | `trivial_le_discrete`, `pullback_top`, `zariski_eq_pretopology`, `isSheaf_trivial` |\n",
+    "| `SieveLattice` | Pullback identities | `pullback_id`, `pullback_pullback`, `pullback_bot`, `pullback_monotone` |\n",
     "\n",
     "### Points cles a retenir\n",
     "\n",
     "1. **Le langage de Grothendieck est naturel en Lean** : les definitions de Mathlib epousent celles de SGA 4.\n",
     "2. **Les preuves sont courtes** : les micro-preuves P1-P4 font 1-3 lignes chacune, mais chacune illustre un pattern différent.\n",
-    "3. **Le pullback est central** : 5 des 8 theoremes du projet impliquent `Sieve.pullback`.\n",
+    "3. **Le pullback est central** : la majorite des theoremes du projet impliquent `Sieve.pullback`.\n",
     "4. **Le treillis est complet** : `Sieve X` et `GrothendieckTopology C` sont des treillis complets.\n",
-    "5. **Le projet est sorry = 0** : toutes les preuves sont closes sur l'ensemble des modules.\n",
+    "5. **Le projet est exempt de sorry** : toutes les preuves sont closes sur l'ensemble des modules.\n",
     "\n",
-    "> **Etendue du projet** : les modules avances supplementaires (Parts 7-23) couvrent les opérations sur cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation et son exactitude a gauche, points d'un site, sous-canonicite, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris et cohomologie de Cech. Ils sont verifies par la cellule d'inventaire ci-dessus (selection modules par rapport au projet, 0 sorry).\n",
+    "> **Etendue du projet** : les modules avances supplementaires (Parts 7-23) couvrent les opérations sur cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation et son exactitude a gauche, points d'un site, sous-canonicite, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris et cohomologie de Cech. Ils sont verifies par la cellule d'inventaire ci-dessus (selection modules par rapport au projet, sans sorry).\n",
     "\n",
     "### Pour aller plus loin\n",
     "\n",