feat(lean,#18205): enveloppe differential_lean -- 3 fermetures + #print axioms

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour.lean

@@ -0,0 +1,37 @@
+/-
+  Visite — trois petites fermetures de qinz1yang/differential-geometry v0.1.3
+  ===========================================================================
+
+  Ce fichier ne reimplemente rien et ne recopie rien : il importe trois
+  modules de l'amont — declare en dependance Lake dans lakefile.lean — et
+  demande au noyau Lean la liste des axiomes dont depend un theoreme-tete de
+  chacune des trois fermetures citees par l'EPIC #18205 :
+
+  1. lemme de Morse          Topology/Morse/ExtremumChart.lean
+  2. cohomologie de de Rham  Tensor/Exterior/Cochain.lean
+  3. Bonnet-Myers            Geometry/Comparison/BonnetMyers/Diameter.lean
+
+  La sortie de `#print axioms` est le temoin de cette visite : un theoreme qui
+  dependrait d'un axiome prohibe (`sorryAx`, `native_decide.*`) est visible
+  ici, en clair, sans qu'aucune preuve n'ait ete reecrite.
+
+  L'amont annonce n'utiliser que `propext`, `Classical.choice` et `Quot.sound`.
+  Ce fichier mesure cette annonce sur trois points d'entree, il ne la reprend
+  pas sur parole.
+
+  Depot  : https://github.com/qinz1yang/differential-geometry
+  Licence : Apache-2.0
+-/
+
+import DifferentialGeometry.Topology.Morse.ExtremumChart
+import DifferentialGeometry.Tensor.Exterior.Cochain
+import DifferentialGeometry.Geometry.Comparison.BonnetMyers.Diameter
+
+-- 1. Lemme de Morse : existence d'une carte quadratique en un minimum local.
+#print axioms DifferentialGeometry.Topology.Morse.exists_quadratic_chart_of_isLocalMin
+
+-- 2. Cohomologie de de Rham : l'identite induit l'identite en cohomologie.
+#print axioms DifferentialGeometry.DifferentialForm.pullbackCohomologyMap_id
+
+-- 3. Bonnet-Myers : borne de diametre sous borne inferieure de courbure de Ricci.
+#print axioms DifferentialGeometry.Geometry.Riemannian.BonnetMyers.bonnet_myers_diameter_le_of_complete_metric

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour_en.lean

@@ -0,0 +1,41 @@
+/-
+  Tour — three small closures of qinz1yang/differential-geometry v0.1.3
+  ====================================================================
+
+  English companion to `DifferentialTour.lean` (FR canonical) per the i18n
+  #4980 sibling-pair convention. Only docstrings/comments differ; Lean code,
+  imports and `#print axioms` commands are byte-identical to the canonical.
+
+  This file reimplements nothing and copies nothing: it imports three modules
+  of the upstream package — declared as a Lake dependency in lakefile.lean —
+  and asks the Lean kernel for the axiom list each headline theorem depends on,
+  for the three closures cited by EPIC #18205:
+
+  1. Morse lemma          Topology/Morse/ExtremumChart.lean
+  2. de Rham cohomology   Tensor/Exterior/Cochain.lean
+  3. Bonnet-Myers         Geometry/Comparison/BonnetMyers/Diameter.lean
+
+  The `#print axioms` output is this tour's witness: a theorem depending on a
+  forbidden axiom (`sorryAx`, `native_decide.*`) shows up here, in the open,
+  without any proof having been rewritten.
+
+  The upstream claims to use only `propext`, `Classical.choice` and
+  `Quot.sound`. This file measures that claim at three entry points; it does
+  not take it on faith.
+
+  Repository : https://github.com/qinz1yang/differential-geometry
+  License    : Apache-2.0
+-/
+
+import DifferentialGeometry.Topology.Morse.ExtremumChart
+import DifferentialGeometry.Tensor.Exterior.Cochain
+import DifferentialGeometry.Geometry.Comparison.BonnetMyers.Diameter
+
+-- 1. Morse lemma: existence of a quadratic chart at a local minimum.
+#print axioms DifferentialGeometry.Topology.Morse.exists_quadratic_chart_of_isLocalMin
+
+-- 2. de Rham cohomology: the identity induces the identity in cohomology.
+#print axioms DifferentialGeometry.DifferentialForm.pullbackCohomologyMap_id
+
+-- 3. Bonnet-Myers: diameter bound under a lower Ricci curvature bound.
+#print axioms DifferentialGeometry.Geometry.Riemannian.BonnetMyers.bonnet_myers_diameter_le_of_complete_metric

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/README.md

@@ -0,0 +1,119 @@
+# `differential_lean` — enveloppe de visite de `qinz1yang/differential-geometry`
+
+Lake d'enveloppe de l'EPIC **#18205** (« origami » : géométrie différentielle en Lean —
+conjecture de Poincaré et flot de Ricci). Pli 1, sub-grain 1.
+
+## Ce que ce lake est — et ce qu'il n'est pas
+
+Ce lake ne **recopie aucune source** de l'amont, ne **forke rien**, et n'ouvre **aucune PR**
+chez l'amont : il déclare `qinz1yang/differential-geometry` comme **dépendance Lake**
+épinglée sur un tag de release. C'est exactement la forme du précédent
+[`GameTheory/social_choice_lean_peters/`](../../../GameTheory/SocialChoice/social_choice_lean_peters/)
+(Peters, MIT), dont `lakefile.lean` et le fichier de visite sont repris.
+
+| | |
+|---|---|
+| Dépôt amont | [`qinz1yang/differential-geometry`](https://github.com/qinz1yang/differential-geometry) |
+| Tag épinglé | **`v0.1.3`** — commit `7a48598d35109aa99d1cc678e2724c213cdf4ff3` |
+| Licence amont | **Apache-2.0** |
+| `lean-toolchain` amont | `leanprover/lean4:v4.33.1` |
+| Mathlib amont | `leanprover-community/mathlib4` @ `v4.33.1` |
+
+## L'exception de toolchain, assumée
+
+Ce lake reste en **Lean `v4.33.1`** alors que le parc CoursIA est en `v4.33.0`. C'est une
+**exception documentée**, de même nature que celle de Peters : l'amont déclare lui-même
+`leanprover/lean4:v4.33.1` dans son `lean-toolchain`, et un lake d'enveloppe qui ne suit pas
+la toolchain de sa dépendance ne s'élabore pas. L'exception est portée par le fichier
+`lean-toolchain` de ce répertoire, pas par une option de build.
+
+## Ce que la visite mesure
+
+`DifferentialTour.lean` (et son jumeau anglais `DifferentialTour_en.lean`, convention
+i18n #4980) importe trois modules de l'amont et demande au noyau Lean, par `#print
+axioms`, la liste des axiomes dont dépend un théorème-tête de chacune des trois **petites
+fermetures** citées par l'EPIC :
+
+| Fermeture | Module importé | Théorème-tête |
+|---|---|---|
+| Lemme de Morse | `DifferentialGeometry.Topology.Morse.ExtremumChart` | `exists_quadratic_chart_of_isLocalMin` |
+| Cohomologie de de Rham | `DifferentialGeometry.Tensor.Exterior.Cochain` | `pullbackCohomologyMap_id` |
+| Bonnet–Myers | `DifferentialGeometry.Geometry.Comparison.BonnetMyers.Diameter` | `bonnet_myers_diameter_le_of_complete_metric` |
+
+La sortie de `#print axioms` est le **témoin** : l'amont annonce n'utiliser que `propext`,
+`Classical.choice` et `Quot.sound`. Ce lake **mesure** cette annonce sur trois points
+d'entrée ; il ne la reprend pas sur parole, et il ne réécrit aucune preuve.
+
+## Construire
+
+```bash
+cd MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean
+lake update                 # récupère l'amont épinglé et Mathlib v4.33.1
+lake exe cache get          # oleans Mathlib précompilés
+lake build                  # élabore DifferentialTour + DifferentialTour_en
+```
+
+`lake build` n'est **pas** branché sur la CI du dépôt : inscrire ce lake dans la matrice
+partagée toucherait des surfaces CI hors du périmètre de cette visite, et la fermeture de
+Bonnet–Myers en fait la plus lourde enveloppe du dépôt — c'est un arbitrage de budget CI,
+qui revient au coordinateur et non à la PR qui livre la visite. Les coûts mesurés sont dans
+la table **Mesures relevées** ci-dessous, qui fait foi ; ce paragraphe n'en recopie aucun.
+L'amont est compilé depuis ses sources par sa propre CI. Le build est donc un **geste de
+visite reproductible**, exécuté hors CI et journalisé dans la PR.
+
+## Mesures relevées
+
+<!-- MESURES:START -->
+Exécutées le **2026-10-07** sur `myia-po-2025`, **hors CI**, sur cette branche. Mathlib
+v4.33.1 était déjà présent dans le cache de la machine (`lake exe cache get` ne
+télécharge rien) — le temps de la visite est donc celui de l'élaboration, pas d'un
+téléchargement.
+
+| Étape | rc | Temps | Pic RSS `lean.exe` |
+|---|---:|---:|---:|
+| `lake update` | 0 | 491 s | — |
+| `lake exe cache get` | 0 | 33 s | — |
+| `lake build DifferentialGeometry.Tensor.Exterior.Cochain` | 0 | 285 s | — |
+| `lake build DifferentialGeometry.Topology.Morse.ExtremumChart` | 0 | 215 s | 2 805 Mo |
+| `lake build …Geometry.Comparison.BonnetMyers.Diameter` | 0 | **1 859 s** | 2 526 Mo |
+| `lake build` (défaut : `DifferentialTour` + `_en`) | 0 | 70 s | 1 854 Mo |
+
+**Total ≈ 2 953 s (49 min)** pour la visite complète ; le build des trois fermetures à
+lui seul ≈ 2 359 s (39 min), **dominé par Bonnet–Myers** (détail des fermetures dans
+la table ci-dessous).
+
+### Fermetures d'imports (modules `DifferentialGeometry.*`, Mathlib exclu)
+
+| Fermeture | Modules | Lignes |
+|---|---:|---:|
+| `Tensor/Exterior/Cochain` (de Rham) | 33 | 13 432 |
+| `Topology/Morse/ExtremumChart` (Morse) | 47 | 23 522 |
+| `Geometry/Comparison/BonnetMyers/Diameter` | 383 | 181 252 |
+
+### Le témoin `#print axioms`
+
+Les trois théorèmes-têtes, interrogés **dans les deux siblings**, ne dépendent que de
+**`propext`, `Classical.choice`, `Quot.sound`** — aucun `sorryAx`, aucun `native_decide.*` :
+
+```text
+info: DifferentialTour.lean:31:0: '…Topology.Morse.exists_quadratic_chart_of_isLocalMin' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+info: DifferentialTour.lean:34:0: '…DifferentialForm.pullbackCohomologyMap_id' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+info: DifferentialTour.lean:37:0: '…Riemannian.BonnetMyers.bonnet_myers_diameter_le_of_complete_metric' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound]
+```
+
+L'annonce de l'amont est donc **mesurée sur trois points d'entrée**, pas reprise sur parole.
+<!-- MESURES:END -->
+
+## Voir aussi
+
+- [#18205](https://github.com/jsboige/CoursIA/issues/18205) — EPIC origami géométrie différentielle
+- [`docs/lean/origami-reconnaissance.md`](../../../../docs/lean/origami-reconnaissance.md) —
+  Pli 1, sub-grains 3 (sources tierces) et 4 (emplacement), livrés par #18978
+- [`social_choice_lean_peters/`](../../../GameTheory/SocialChoice/social_choice_lean_peters/) — précédent
+  de la forme « enveloppe par dépendance, jamais par copie »

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lake-manifest.json

@@ -0,0 +1,106 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/qinz1yang/differential-geometry",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7a48598d35109aa99d1cc678e2724c213cdf4ff3",
+   "name": "DifferentialGeometry",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.1.3",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "differential_lean",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lakefile.lean

@@ -0,0 +1,40 @@
+/-
+  Enveloppe de visite — qinz1yang/differential-geometry
+  =====================================================
+
+  Ce projet declare le depot amont qinz1yang/differential-geometry comme
+  dependance Lake, epinglee sur le tag de release v0.1.3
+  (commit 7a48598d35109aa99d1cc678e2724c213cdf4ff3).
+
+  Aucune source de l'amont n'est recopiee, aucun fork n'est fait : la surface
+  est une dependance, exactement comme GameTheory/social_choice_lean_peters/
+  (precedent du depot, meme forme).
+
+  Le lake reste en Lean v4.33.1 alors que le parc CoursIA est en v4.33.0 :
+  c'est une exception documentee, comme pour Peters — l'amont declare
+  lui-meme `leanprover/lean4:v4.33.1` dans son lean-toolchain.
+
+  Reference : https://github.com/qinz1yang/differential-geometry
+  Licence   : Apache-2.0
+  Issue     : #18205 (EPIC origami geometrie differentielle, Pli 1)
+-/
+
+import Lake
+open Lake DSL
+
+package «differential_lean» where
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩,
+    ⟨`autoImplicit, false⟩
+  ]
+
+require DifferentialGeometry from git
+  "https://github.com/qinz1yang/differential-geometry" @ "v0.1.3"
+
+@[default_target]
+lean_lib «DifferentialTour» where
+  -- globs incluent le sibling EN (i18n #4980) pour que `lake build` l'elabore
+  -- aussi : sans cela, DifferentialTour_en.lean n'est jamais compile et un
+  -- Lean CI vert est un faux pass (orphan-trap #6749). Meme pattern que
+  -- social_choice_lean_peters et sudoku_lean.
+  globs := #[`DifferentialTour, `DifferentialTour_en]

MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1