diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour.lean new file mode 100644 index 0000000000..0f5f679518 --- /dev/null +++ b/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 diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/DifferentialTour_en.lean new file mode 100644 index 0000000000..b82c7ded1b --- /dev/null +++ b/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 diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/README.md new file mode 100644 index 0000000000..e3c7be97b9 --- /dev/null +++ b/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 + + +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. + + +## 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 » diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lake-manifest.json b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lake-manifest.json new file mode 100644 index 0000000000..f4f41402f0 --- /dev/null +++ b/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} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lakefile.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lakefile.lean new file mode 100644 index 0000000000..0e298f6584 --- /dev/null +++ b/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] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lean-toolchain b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lean-toolchain new file mode 100644 index 0000000000..a8afa7d1b0 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/differential_lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1