From 537f7cea194f297c3038059195e9a8483a4e10f8 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Sun, 11 Oct 2026 10:27:48 +0200 Subject: [PATCH] feat(lean,#18601): companion WuMethod du Geometry-03 -- ce que le test de Wu garantit Module Geometry/WuMethod.lean (~230 lignes, 0 sorry) : certificats ideaux T1 (milieu de l'hypotenuse, g = u*h par composante, sans non-degenerescence), garantie semantique (appartenance -> annulation universelle), temoin negatif refute par norm_num, theoreme de Ceva T3 dans l'encodage barycentrique exact du notebook -- identite maitresse q^2*g3 = D*h_CF - q(t2t3-1)*h_AD + q(t1t3-t1+1)*h_BE verifiee par ring, direction concurrence=>produit avec q != 0 seul, reciproque constructive par Cramer, piege des rapports diriges refute par contre-exemple exact. Defs polynomial noncomputable (AddMonoidAlgebra.ring). Axiomes : [propext, Classical.choice, Quot.sound] uniquement, dans la whitelist du gate. lake build Geometry.WuMethod SUCCESS (8706 jobs). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Lean/Geometry/geometry_lean/Geometry.lean | 4 + .../geometry_lean/Geometry/WuMethod.lean | 231 ++++++++++++++++++ .../Lean/Geometry/geometry_lean/README.md | 2 +- 3 files changed, 236 insertions(+), 1 deletion(-) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry/WuMethod.lean diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean index 73ed486b82..a8d8534761 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean @@ -16,6 +16,10 @@ - `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). + - `Geometry.WuMethod` — companion du `Geometry-03` : ce que le test de + Wu garantit (certificats d'appartenance idéale T1, identité maîtresse + de Ceva T3, témoins négatifs). -/ import Geometry.MidpointHypotenuse +import Geometry.WuMethod diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry/WuMethod.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry/WuMethod.lean new file mode 100644 index 0000000000..f9f8151823 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry/WuMethod.lean @@ -0,0 +1,231 @@ +/- + WuMethod — companion Lean du notebook Geometry-03 (méthode de Wu) + ================================================================ + + Deuxième module du lac `geometry_lean` (EPIC #18601 volet B, tranche 4 : + « Companions 03 (Wu) puis 01 »). Il double + `Geometry-03-Wu-Method-Python.ipynb` en formalisant **ce que le test de Wu + garantit** — la question pédagogique de la position 05 du programme gradué + #17544 (« que garantit "prouvé par Gröbner" ? »). + + Ce que le notebook calcule avec sympy (pseudo-restes, chaînes ascendantes, + initiales), ce module le prouve : pour chaque théorème, un **certificat + polynomial explicite** — une identité de la forme + `J • g = Σ aᵢ • hᵢ` — dont Lean vérifie la validité par `ring`. C'est + exactement la substance du pseudo-reste nul : la conclusion `g` appartient + à l'idéal des hypothèses `hᵢ` à un facteur de non-dégénérescence `J` près, + donc s'annule partout où les hypothèses s'annulent et `J` ne s'annule pas. + + Deux familles d'énoncés, calquées sur les sections du notebook : + + * **T1, le fil rouge** (milieu de l'hypoténuse) : encodage polynomial en + quatre variables, certificat d'appartenance idéale `g = u₁ • h₁` sans + aucune condition de non-dégénérescence, et lue sémantique sur + `MvPolynomial (Fin 4) ℚ` — l'appartenance à l'idéal implique + l'annulation universelle. S'y ajoute le **témoin négatif** (§9 du + notebook) : la conclusion fausse « MA² = 4·MB² » est réfutée par un + contre-exemple explicite — un outil de preuve doit aussi savoir dire non. + + * **T3, le théorème de Ceva** (§8 du notebook) : encodage barycentrique + exact du notebook — `A = (0,0)`, `B = (1,0)`, `C = (p,q)`, points de côté + paramétrés par `t₁ t₂ t₃`, point de concours `O = (o₁,o₂)`, hypothèses + d'alignement par déterminants 2×2. L'identité maîtresse ci-dessous joue + le rôle du pseudo-reste nul ; la direction « concurrence ⇒ produit des + rapports dirigés » n'exige que `q ≠ 0` (triangle non plat), la réciproque + construit explicitement le point de concours par Cramer. Le **piège des + rapports dirigés** du notebook (inverser `CE/EA`) est lui aussi réfuté + par un contre-exemple numérique exact. + + Non-but assumé (non-buts de l'EPIC) : ce module ne migre pas les + algorithmes de Wu ou de Ritt en Lean exécutable — il formalise les + théorèmes qu'ils établissent. Le demi-tour « preuve géométrique abstraite » + du fil rouge vit dans `Geometry.MidpointHypotenuse`. +-/ + +import Mathlib + +open MvPolynomial + +/-! ## T1 — le fil rouge : milieu de l'hypoténuse (notebook §2) + +Encodage du notebook, cellule « Encodage de T1 » : `A = (0,0)`, `B = (u₁,0)`, +`C = (0,u₂)` — l'angle droit en `A` porte les côtés sur les axes — et +`M = (xₘ,yₘ)` le milieu de l'hypoténuse `[BC]`. Les hypothèses disent que +`M` est le milieu : `h₁ : 2xₘ − u₁ = 0` (abscisse) et `h₂ : 2yₘ − u₂ = 0` +(ordonnée). Les variables sont indicées `X 0 = u₁`, `X 1 = u₂`, `X 2 = xₘ`, +`X 3 = yₘ`. -/ + +/-- Hypothèse `h₁ : 2·xₘ − u₁` — l'abscisse du milieu de `[BC]` vaut +`u₁/2` (notebook Geometry-03, cellule 4). -/ +noncomputable def t1H1 : MvPolynomial (Fin 4) ℚ := 2 * X 2 - X 0 + +/-- Hypothèse `h₂ : 2·yₘ − u₂` — l'ordonnée du milieu de `[BC]` vaut +`u₂/2`. -/ +noncomputable def t1H2 : MvPolynomial (Fin 4) ℚ := 2 * X 3 - X 1 + +/-- Conclusion `g_{MB} : MA² − MB²` — le milieu est à égale distance de `A` +et de `B`. -/ +noncomputable def t1GMB : MvPolynomial (Fin 4) ℚ := + (X 2)^2 + (X 3)^2 - ((X 2 - X 0)^2 + (X 3)^2) + +/-- Conclusion `g_{MC} : MA² − MC²` — le milieu est à égale distance de `A` +et de `C` (composante symétrique, échangée par `u₁ ↔ u₂`, `xₘ ↔ yₘ`). -/ +noncomputable def t1GMC : MvPolynomial (Fin 4) ℚ := + (X 2)^2 + (X 3)^2 - ((X 2)^2 + (X 3 - X 1)^2) + +/-- **Certificat T1 côté `B`.** La conclusion `g_{MB}` est égale au produit +`u₁ • h₁` : elle appartient à l'idéal engendré par la seule hypothèse +d'abscisse — c'est le contenu du pseudo-reste nul du notebook pour T1, sans +aucune condition de non-dégénérescence. La composante ordonnée `h₂` n'intervient +pas : `MB` ne mobilise que l'abscisse de `B`. -/ +theorem t1_certificate_mb (z : Fin 4 → ℚ) : + eval z t1GMB = z 0 * eval z t1H1 := by + simp [t1GMB, t1H1, eval_sub, eval_mul, eval_pow, eval_X] <;> ring + +/-- **Certificat T1 côté `C`.** Symétrique du précédent : `g_{MC} = u₂ • h₂`. +Avec le certificat côté `B`, l'équidistance complète +`MA = MB = MC` du `Geometry.MidpointHypotenuse` abstrait se lit ici en +coordonnées, une hypothèse par composante. -/ +theorem t1_certificate_mc (z : Fin 4 → ℚ) : + eval z t1GMC = z 1 * eval z t1H2 := by + simp [t1GMC, t1H2, eval_sub, eval_mul, eval_pow, eval_X] <;> ring + +/-- **La garantie sémantique du test de Wu (T1).** Partout où l'hypothèse +d'abscisse s'annule, la conclusion `MA² = MB²` s'annule : l'appartenance à +l'idéal implique l'annulation universelle. C'est la réponse formelle à +« que garantit "prouvé" ? » pour le fil rouge. -/ +theorem t1_soundness_mb (z : Fin 4 → ℚ) (h1 : eval z t1H1 = 0) : + eval z t1GMB = 0 := by + rw [t1_certificate_mb, h1, mul_zero] + +/-- Garantie sémantique, composante `C`. -/ +theorem t1_soundness_mc (z : Fin 4 → ℚ) (h2 : eval z t1H2 = 0) : + eval z t1GMC = 0 := by + rw [t1_certificate_mc, h2, mul_zero] + +/-- Équidistance complète en coordonnées : si `M` est le milieu (les deux +hypothèses), alors `MA² = MB²` et `MA² = MC²`. -/ +theorem t1_equidistant (z : Fin 4 → ℚ) (h1 : eval z t1H1 = 0) + (h2 : eval z t1H2 = 0) : + eval z t1GMB = 0 ∧ eval z t1GMC = 0 := + ⟨t1_soundness_mb z h1, t1_soundness_mc z h2⟩ + +/-- Conclusion **fausse** du témoin négatif (§9 du notebook) : +`MA² − 4·MB²`, vraie seulement pour des triangles très particuliers. -/ +noncomputable def t1GFaux : MvPolynomial (Fin 4) ℚ := + (X 2)^2 + (X 3)^2 - 4 * ((X 2 - X 0)^2 + (X 3)^2) + +/-- **Témoin négatif : l'outil de preuve sait dire non.** L'énoncé faux +« MA² = 4·MB² sous les hypothèses du milieu » n'est PAS prouvable : au point +concret du notebook `u₁ = 4`, `u₂ = 3`, `M = (2, 3/2)` (triangle rectangle +3-4-5), les deux hypothèses s'annulent mais la conclusion fausse vaut +`−75/4 ≠ 0`. Là où le test de Wu rend un reste non nul, Lean exhibe le +contre-exemple — la dissymétrie saine entre outil de recherche et outil de +preuve. -/ +theorem t1_false_conclusion_unprovable : + ¬ (∀ z : Fin 4 → ℚ, eval z t1H1 = 0 → eval z t1H2 = 0 → + eval z t1GFaux = 0) := by + intro h + have hw := h ![4, 3, 2, (3 / 2 : ℚ)] + (by simp [t1H1, eval_sub, eval_mul, eval_X] <;> norm_num) + (by simp [t1H2, eval_sub, eval_mul, eval_X] <;> norm_num) + simp [t1GFaux, eval_sub, eval_add, eval_mul, eval_pow, eval_X] at hw + norm_num at hw + +/-! ## T3 — le théorème de Ceva (notebook §8) + +Encodage barycentrique exact du notebook : `A = (0,0)`, `B = (1,0)`, +`C = (p,q)` ; les points de côté `D ∈ (BC)`, `E ∈ (CA)`, `F ∈ (AB)` par leurs +paramètres `t₁ t₂ t₃` — `D = B + t₁(C−B)`, `E = A + t₂(C−A)`, `F = A + t₃(B−A)` +— et `O = (o₁,o₂)` le point de concours. Les trois hypothèses d'alignement +sont des déterminants 2×2 nuls. La conclusion (rapports **dirigés**) : +`t₁(1−t₂)t₃ − (1−t₁)t₂(1−t₃) = 0`. -/ + +/-- **Identité maîtresse de T3** — le pseudo-reste nul du notebook, rendu +explicite : `q² • g₃ = D • h_{CF} − q(t₂t₃−1) • h_{AD} + q(t₁t₃−t₁+1) • h_{BE}` +avec `D = (t₁t₂−t₁−t₂)·(−q)` le déterminant 2×2 des céviennes `(AD)` et +`(BE)`. Chaque coefficient est polynomial ; Lean vérifie l'identité par +`ring`. C'est elle qui joue, côté preuve vérifiée, le rôle du calcul +`prem(g₃, CS(T3)) = 0` du notebook. -/ +theorem ceva_master_identity (p q t1 t2 t3 o1 o2 : ℚ) : + q * q * (t1 * (1 - t2) * t3 - (1 - t1) * t2 * (1 - t3)) + = (t1 * t2 - t1 - t2) * (-q) * ((o1 - p) * (-q) - (o2 - q) * (t3 - p)) + - q * (t2 * t3 - 1) * (o1 * (t1 * q) - o2 * ((1 - t1) + t1 * p)) + + q * (t1 * t3 - t1 + 1) * ((o1 - 1) * (t2 * q) - o2 * (t2 * p - 1)) := by + ring + +/-- **Ceva, direction « concurrence ⇒ produit ».** Si les trois cévianes +`(AD)`, `(BE)`, `(CF)` sont concourantes en `O` et si le triangle n'est pas +plat (`q ≠ 0`), alors le produit des rapports dirigés vaut 1. Remarque de +structure : le certificat porte `D • h_{CF}` — l'hypothèse d'alignement déjà +nulle annule le terme en `D`, donc **cette direction n'exige que `q ≠ 0`**, +pas la non-parallélisme des céviannes ; les initiales plus riches du +notebook servent à sa chaîne algorithmique et à la réciproque. -/ +theorem ceva_product_of_concurrent {p q t1 t2 t3 o1 o2 : ℚ} (hq : q ≠ 0) + (hAD : o1 * (t1 * q) - o2 * ((1 - t1) + t1 * p) = 0) + (hBE : (o1 - 1) * (t2 * q) - o2 * (t2 * p - 1) = 0) + (hCF : (o1 - p) * (-q) - (o2 - q) * (t3 - p) = 0) : + t1 * (1 - t2) * t3 - (1 - t1) * t2 * (1 - t3) = 0 := by + have key := ceva_master_identity p q t1 t2 t3 o1 o2 + rw [hCF, hAD, hBE] at key + simp only [mul_zero, add_zero, sub_zero] at key + exact (mul_eq_zero.mp key).resolve_left (mul_ne_zero hq hq) + +/-- **Ceva, direction « produit ⇒ concurrence ».** Si le produit des rapports +dirigés vaut 1, le triangle n'est pas plat (`q ≠ 0`) et les céviannes `(AD)` +et `(BE)` sont sécantes (`t₁t₂ − t₁ − t₂ ≠ 0`, leur déterminant), alors les +trois céviannes sont concourantes : le point de concours est construit +explicitement par Cramer — c'est l'intersection de `(AD)` et `(BE)`, et +l'identité maîtresse garantit qu'il est sur `(CF)`. Les conditions +`q ≠ 0` et `t₁t₂ − t₁ − t₂ ≠ 0` sont les initiales du notebook (§6) : +triangle non plat, céviannes bien définies et sécantes. -/ +theorem ceva_concurrent_of_product {p q t1 t2 t3 : ℚ} (hq : q ≠ 0) + (hden : t1 * t2 - t1 - t2 ≠ 0) + (hg : t1 * (1 - t2) * t3 - (1 - t1) * t2 * (1 - t3) = 0) : + ∃ o1 o2 : ℚ, + o1 * (t1 * q) - o2 * ((1 - t1) + t1 * p) = 0 ∧ + (o1 - 1) * (t2 * q) - o2 * (t2 * p - 1) = 0 ∧ + (o1 - p) * (-q) - (o2 - q) * (t3 - p) = 0 := by + set O1 : ℚ := + -(((1 - t1) + t1 * p) * (t2 * q)) / (q * (t1 * t2 - t1 - t2)) with hO1 + set O2 : ℚ := + -((t1 * q) * (t2 * q)) / (q * (t1 * t2 - t1 - t2)) with hO2 + have hdn : (q * (t1 * t2 - t1 - t2) : ℚ) ≠ 0 := mul_ne_zero hq hden + have h1 : O1 * (t1 * q) - O2 * ((1 - t1) + t1 * p) = 0 := by + rw [hO1, hO2] + set d : ℚ := q * (t1 * t2 - t1 - t2) with hd_def + have hd_ne : d ≠ 0 := mul_ne_zero hq hden + field_simp [hd_ne] + ring + have h2 : (O1 - 1) * (t2 * q) - O2 * (t2 * p - 1) = 0 := by + rw [hO1, hO2] + set d : ℚ := q * (t1 * t2 - t1 - t2) with hd_def + have hd_ne : d ≠ 0 := mul_ne_zero hq hden + field_simp [hd_ne] + ring + have key := ceva_master_identity p q t1 t2 t3 O1 O2 + rw [h1, h2] at key + simp only [hg, mul_zero, add_zero, sub_zero] at key + refine ⟨O1, O2, h1, h2, ?_⟩ + exact (mul_eq_zero.mp key.symm).resolve_left + (mul_ne_zero hden (neg_ne_zero.mpr hq)) + +/-- **Le piège des rapports dirigés, réfuté formellement** (§8 du notebook). +L'encodage naïf qui inverserait le rapport `CE/EA` conclurait à +`t₁t₂(1−t₃) − (1−t₁)(1−t₂)t₃ = 0`. Sur le triangle concret du notebook +(`p = 2`, `q = 3`, `t₁ = 3/10`, `t₂ = 2/5`, `t₃ = 14/23` dérivé de la vraie +relation de Ceva), le point `O = (26/29, 18/29)` réalise exactement les trois +alignements — et la conclusion inversée vaut `−24/115 ≠ 0`. Un énoncé faux +ne devient pas théorème : la vérification numérique du notebook a son +contrepartie exacte en Lean. -/ +theorem ceva_directed_ratio_trap_witness : + (26:ℚ) / 29 * ((3 / 10) * 3) - (18 / 29) * ((1 - 3 / 10) + (3 / 10) * 2) = 0 ∧ + ((26:ℚ) / 29 - 1) * ((2 / 5) * 3) - (18 / 29) * ((2 / 5) * 2 - 1) = 0 ∧ + ((26:ℚ) / 29 - 2) * (-(3:ℚ)) - (18 / 29 - 3) * (14 / 23 - 2) = 0 ∧ + ((3:ℚ) / 10) * (2 / 5) * (1 - 14 / 23) - (1 - 3 / 10) * (1 - 2 / 5) * (14 / 23) ≠ 0 := by + refine ⟨?_, ?_, ?_, ?_⟩ + · norm_num + · norm_num + · norm_num + · intro hcon + norm_num at hcon diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md index 6019c81220..58485201e4 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md @@ -11,6 +11,7 @@ du programme gradué #17544 (« que garantit "prouvé par Gröbner" ? »). | 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) | +| `Geometry.WuMethod` | Ce que le test de Wu garantit : certificat idéal T1 (milieu de l'hypoténuse, `MvPolynomial`), théorème de Ceva T3 par identité maîtresse (deux directions), témoin négatif et piège des rapports dirigés réfutés | `Geometry-03-Wu-Method-Python.ipynb` | L'escalier d'entrée de la sous-série — [`Lean-38-Capstone-Geometry-Lean-Python.ipynb`](../../Lean-38-Capstone-Geometry-Lean-Python.ipynb), carnet de la série parente — est le consommateur pédagogique de ce premier module : il part de la figure du 01, calcule avec `sympy`, puis monte jusqu'à la preuve formelle ci-dessus. @@ -29,7 +30,6 @@ 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.