feat(lean,#18601): lake geometry_lean — squelette + théorème du milieu de l'hypoténuse (tranche 2)

.github/workflows/lean-geometry.yml

@@ -0,0 +1,69 @@
+name: Lean CI (geometry_lean)
+
+# CI for geometry_lean (MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry).
+# Companion lake of the Geometry series (EPIC #18601 volet B): each Python
+# concept notebook gets a Lean module formalizing what the algorithm computes.
+# First theorem: the midpoint of the hypotenuse (position 05 of #17544).
+# 0 sorry (raw=0, verified), fully proven from birth.
+# Template: lean-percolation.yml (small lake, sorry-filter-mode: real).
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain'
+      # The gate's own implementation: a change to it must re-run the gate
+      # (same rationale as lean-galois.yml / lean-conway.yml, cf #8951).
+      - '.github/workflows/lean-geometry.yml'
+      - '.github/workflows/lean-axiom.yml'
+      # The axiom step is a Python program (`from lean_server import LeanVerifier`);
+      # lean_server.py + lean_utils.py ARE gate inputs (cf #8722).
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/lean_utils.py'
+  pull_request:
+    types: [opened, synchronize, edited, reopened]
+    paths:
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain'
+      # The gate must run on the PR that introduces or changes it (cf #8712).
+      - '.github/workflows/lean-geometry.yml'
+      - '.github/workflows/lean-axiom.yml'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/lean_server.py'
+      - 'MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/lean_utils.py'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: lean-geometry-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  ci:
+    uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main
+    with:
+      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean
+      display-name: geometry_lean
+      sorry-baseline: "0"
+      sorry-filter-mode: real
+
+  # Level 3 proof-integrity gate (criterion B.3 of pr-review-discipline):
+  # a lake born with a dedicated workflow -- B.3 never reads "non applicable".
+  # fail-on-sorry: true -- sorry-baseline is 0, the lake is fully proven.
+  # target-modules: "*" (issue #10889) -- the module list is derived at runtime
+  # from the lake walk, so it cannot drift out of view. The `_en` i18n siblings
+  # are EXCLUDED by default (FR-only measurement; the byte-parity of the i18n
+  # pair is covered structurally by `lean-i18n-drift.yml`, #10007).
+  proof-integrity:
+    needs: ci  # serialize the two compiles (parity with knot_lean #14922)
+    uses: jsboige/CoursIA/.github/workflows/lean-axiom.yml@main
+    with:
+      project-path: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean
+      display-name: geometry_lean
+      target-modules: "*"
+      allow-axioms: ""
+      fail-on-sorry: true

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

@@ -14,7 +14,7 @@ Le programme est **gradué** : chaque notebook principal ne suppose que ce qui l
 | 03b | [Geometry-03b-Ritt-Decomposition-Python.ipynb](Geometry-03b-Ritt-Decomposition-Python.ipynb) | Licence | Accrétion du 03 : le théorème du papillon — la conclusion est un quotient, scission de Ritt, bord dégénéré où l'énoncé est **muet** et non faux, contrôle sur 400 figures | Livré (#17511) |
 | 04 | [Geometry-04-DD-AR-Python.ipynb](Geometry-04-DD-AR-Python.ipynb) | Licence | Base de déduction à règles (DD) et raisonnement algébrique (AR), la moitié symbolique d'AlphaGeometry : fermeture à point fixe, trace de preuve lisible, la limite combinatoire sans construction, AR (`sympy.groebner`) en oracle ; fil rouge et témoin négatif réfuté deux fois | Livré |
 | 04b | Geometry-04b — IMO-AG-30 | Recherche | Wu associé à DD+AR (Sinha et al. 2024), proposeur neuronal | À venir |
-| 05 | Geometry-05 — Pont formel | Recherche | Un théorème de 02/03 énoncé et prouvé en Lean/Mathlib : que garantit « prouvé par Gröbner » ? | À venir |
+| 05 | Geometry-05 — Pont formel | Recherche | Un théorème de 02/03 énoncé et prouvé en Lean/Mathlib : que garantit « prouvé par Gröbner » ? | En cours — première marche : le lac companion [`geometry_lean`](geometry_lean/) prouve le fil rouge (milieu de l'hypoténuse) |
 
 Les notebooks 01, 02 et 03 forment la **première volée** : ils se mergent ensemble, dans l'ordre — le premier état public de la série est déjà une progression complète.
 
@@ -25,9 +25,10 @@ Le **théorème du milieu de l'hypoténuse** traverse 01, 02 et 03 :
 - en 01, on le **vérifie numériquement** sur 10 000 figures, et on mesure ce que cette vérification prouve (preuve probabiliste Schwartz–Zippel) et ne prouve pas ;
 - en 02, on le **démontre** : la conclusion appartient à l'idéal des hypothèses, décidée exactement par Gröbner ;
 - en 03, on le **redémontre** par la méthode de Wu, avec les conditions de non-dégénérescence explicites ;
-- en 04, on le regarde par **DD + AR** : la fermeture de règles démontre le combinatoire, s'arrête devant le métrique — et l'algèbre prouve le reste, avec un énoncé faux réfuté deux fois.
+- en 04, on le regarde par **DD + AR** : la fermeture de règles démontre le combinatoire, s'arrête devant le métrique — et l'algèbre prouve le reste, avec un énoncé faux réfuté deux fois ;
+- dans le lac companion [`geometry_lean`](geometry_lean/), il est **prouvé formellement** en Lean/Mathlib — la position 05 du programme ouvre le pont entre « prouvé par Gröbner » et « prouvé au noyau ».
 
-Quatre regards sur le même objet — on compare des *méthodes*, pas des exemples.
+Cinq regards sur le même objet — on compare des *méthodes*, pas des exemples.
 
 ## Prérequis et coût
 

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/.gitignore

@@ -0,0 +1,2 @@
+.lake/
+build/

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean

@@ -0,0 +1,21 @@
+/-
+  Geometry — racine du lac `geometry_lean`
+  =======================================
+
+  * Racine du lac companion de la série Geometry (`SymbolicAI/Lean/Geometry/`,
+    EPIC #18601 volet B), présentée selon la convention i18n #4980 :
+    `Geometry.lean` canonique FR ; les siblings `_en` suivront si une
+    audience externe les justifie (l'umbrella les globbe via `.submodules`).
+
+  * Cible : doubler chaque notebook Python de concept (01 figure vers
+    équation, 02 Gröbner, 03 Wu, 03b Ritt) d'un module qui formalise ce que
+    l'algorithme Python calcule. Le lac ne remplace pas sympy : il en
+    formalise la sémantique.
+
+  * Modules :
+    - `Geometry.MidpointHypotenuse` — le théorème du milieu de l'hypoténuse,
+      fil rouge de la série Python et première marche du pont formel
+      (position 05 du programme gradué #17544).
+-/
+
+import Geometry.MidpointHypotenuse

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry/MidpointHypotenuse.lean

@@ -0,0 +1,71 @@
+/-
+  MidpointHypotenuse — le milieu de l'hypoténuse
+  =============================================
+
+  Premier théorème du lac `geometry_lean` (EPIC #18601 volet B, position 05 du
+  programme gradué #17544). C'est le fil rouge de la série Geometry Python :
+  le notebook `Geometry-01-From-Figure-To-Equation.ipynb` part de la figure
+  du milieu de l'hypoténuse ; ce module en donne la preuve formelle.
+
+  Formulation : un triangle `ABC` rectangle en `A`, vu depuis `A` prise pour
+  origine, a ses deux côtés portés par des vecteurs orthogonaux `u` (vers `B`)
+  et `v` (vers `C`). Le milieu `M` de l'hypoténuse `[BC]` est alors
+  équidistant des trois sommets : `MA = MB = MC`. Autrement dit, `M` est le
+  centre du cercle circonscrit et le rayon vaut la moitié de l'hypoténuse —
+  c'est la réciproque du théorème de Pythagore qui « voit » le cercle.
+
+  Les notebooks Python de la série calculent (sympy) ; ce lac prouve (Lean).
+-/
+
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Tactic.Module
+
+open scoped InnerProductSpace
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+
+/-- Égalité des diagonales d'un parallélogramme « rectangle » : si `u` et `v`
+sont orthogonaux, la somme `u + v` et la différence `u - v` ont même norme.
+Chaque carré vaut `‖u‖² + ‖v‖²` — le terme croisé `±2⟪u, v⟫` de l'identité
+de polarisation est nul — donc les deux normes valent la même racine
+`√(‖u‖² + ‖v‖²)`, par les deux formes du théorème de Pythagore (additive et
+soustractive) de Mathlib. -/
+theorem norm_add_eq_norm_sub_of_inner_eq_zero {u v : E} (huv : ⟪u, v⟫_ℝ = 0) :
+    ‖u + v‖ = ‖u - v‖ := by
+  rw [norm_add_eq_sqrt_iff_real_inner_eq_zero.2 huv,
+      norm_sub_eq_sqrt_iff_real_inner_eq_zero.2 huv]
+
+/-- Composante « sommet `B` » : la distance de l'origine `A` au milieu `M`
+égale la distance de `B = u` à `M`. Les deux se réduisent à `2⁻¹ • ‖u - v‖`
+par l'identité de Pythagore (lemme ci-dessus) : `M - B` vaut la moitié de
+`u - v` (une demi-diagonale du rectangle construit sur `u` et `v`). -/
+private theorem dist_origin_eq_dist_apex_of_inner_eq_zero {u v : E}
+    (huv : ⟪u, v⟫_ℝ = 0) :
+    ‖(2 : ℝ)⁻¹ • (u + v)‖ = ‖u - (2 : ℝ)⁻¹ • (u + v)‖ := by
+  have hsplit : u - (2 : ℝ)⁻¹ • (u + v) = (2 : ℝ)⁻¹ • (u - v) := by
+    module
+  rw [hsplit, norm_smul, norm_smul, norm_add_eq_norm_sub_of_inner_eq_zero huv]
+
+/-- **Théorème du milieu de l'hypoténuse.** Dans un triangle rectangle en `A`
+(l'origine), de côtés `B = u` et `C = v` avec `u ⊥ v`, le milieu
+`M = (u + v) / 2` de l'hypoténuse `[BC]` est équidistant des trois sommets :
+`MA = MB = MC`. La composante `MC` s'obtient par symétrie : échanger les rôles
+de `u` et `v` échange `B` et `C` sans toucher au milieu ni à l'orthogonalité. -/
+theorem midpoint_hypotenuse_equidistant {u v : E} (huv : ⟪u, v⟫_ℝ = 0) :
+    ‖(2 : ℝ)⁻¹ • (u + v)‖ = ‖u - (2 : ℝ)⁻¹ • (u + v)‖ ∧
+      ‖(2 : ℝ)⁻¹ • (u + v)‖ = ‖v - (2 : ℝ)⁻¹ • (u + v)‖ :=
+  ⟨dist_origin_eq_dist_apex_of_inner_eq_zero huv, by
+    have hvu : ⟪v, u⟫_ℝ = 0 := by
+      rw [real_inner_comm, huv]
+    have h := dist_origin_eq_dist_apex_of_inner_eq_zero hvu
+    rwa [add_comm v u] at h⟩
+
+/-- Le rayon commun vaut la moitié de l'hypoténuse : la distance de `A`
+(origine) au milieu `M` est `‖u - v‖ / 2`, soit `BC / 2`. C'est la lecture
+« cercle circonscrit » du théorème : le rayon est l'hypoténuse coupée en deux,
+d'où la construction du cercle circonscrit au compas par le seul milieu de
+l'hypoténuse. -/
+theorem midpoint_hypotenuse_radius {u v : E} (huv : ⟪u, v⟫_ℝ = 0) :
+    ‖(2 : ℝ)⁻¹ • (u + v)‖ = (2 : ℝ)⁻¹ * ‖u - v‖ := by
+  rw [norm_smul, norm_add_eq_norm_sub_of_inner_eq_zero huv, Real.norm_eq_abs,
+    abs_of_pos (by positivity)]

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md

@@ -0,0 +1,34 @@
+# geometry_lean — companion Lean de la série Geometry
+
+Lac companion de la série [`SymbolicAI/Lean/Geometry/`](../) : chaque notebook
+Python de concept reçoit un module Lean qui formalise ce que l'algorithme
+Python calcule. Le lac ne remplace pas sympy — il en formalise la sémantique.
+C'est le volet B de l'EPIC #18601 ; la première marche réalise la position 05
+du programme gradué #17544 (« que garantit "prouvé par Gröbner" ? »).
+
+## Modules
+
+| Module | Contenu | Notebook Python doublé |
+|---|---|---|
+| `Geometry.MidpointHypotenuse` | Théorème du milieu de l'hypoténuse : équidistance du milieu aux trois sommets, rayon = hypoténuse/2 | `Geometry-01-From-Figure-To-Equation.ipynb` (fil rouge) |
+
+## Construire
+
+```bash
+lake exe cache get   # oleans Mathlib pré-compilées (toolchain v4.33.0)
+lake build           # 0 sorry — le lac est intégralement prouvé
+```
+
+La CI
+([`lean-geometry.yml`](https://github.com/jsboige/CoursIA/blob/main/.github/workflows/lean-geometry.yml))
+rejoue le build et le gate proof-integrity (axiomes) sur chaque PR touchant le
+lac.
+
+## Feuille de route
+
+- Companion du 03 (méthode de Wu) : s'appuyer sur `MvPolynomial` de Mathlib.
+- Companion du 02 (bases de Gröbner) : interroger ce que Mathlib sait des
+  idéaux et de l'appartenance (`Ideal` membership) — c'est précisément la
+  question pédagogique de la position 05.
+- Notebook escalier d'entrée (volet C de #18601) : figure du 01 → calcul
+  sympy → montée Lean pas à pas jusqu'au premier théorème du lac.

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lake-manifest.json

@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": false,
+   "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": "geometry_lean",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lakefile.lean

@@ -0,0 +1,21 @@
+import Lake
+open Lake DSL
+
+package «geometry_lean» where
+  leanOptions := #[⟨`autoImplicit, false⟩]
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.0"
+
+-- Lake companion de la serie Geometry (SymbolicAI/Lean/Geometry/, EPIC #18601
+-- volet B) : chaque notebook Python de concept (01 figure vers equation, 02
+-- Groebner, 03 Wu, 03b Ritt) recevra un module qui formalise ce que
+-- l'algorithme Python calcule. Le lac ne remplace pas sympy : il en formalise
+-- la semantique. Premier theorème : le milieu de l'hypotenuse (fil rouge de la
+-- serie Python, position 05 du programme #17544).
+
+@[default_target]
+lean_lib «Geometry» where
+  -- `.submodules `Geometry` couvre les Geometry.* (modules FR puis leurs
+  -- siblings `_en` le jour ou l'audience externe les justifie, pattern #4980).
+  globs := #[.submodules `Geometry]

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/lean-toolchain

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