feat(lean,#18601): companion WuMethod -- ce que le test de Wu garantit (tranche 4)

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: LIGHT/ledger #20339

Companion Lean du Geometry-03 : ce que le test de Wu garantit (tranche 4 de #18601)

See #18601 (volet B, tranche 4 « Companions 03 (Wu) puis 01 ») · See #17544 (position 05)

Ce que cette PR porte

Un module Geometry/WuMethod.lean (~230 lignes, 0 sorry) qui double Geometry-03-Wu-Method-Python.ipynb : le notebook calcule avec sympy (pseudo-restes, chaînes ascendantes, initiales), le module prouve — pour chaque théorème, un certificat polynomial explicite vérifié par ring. C'est la réponse formelle à la question pédagogique de la position 05 : « que garantit "prouvé" ? ».

Énoncé	Rôle	Preuve
t1_certificate_mb / t1_certificate_mc	Fil rouge T1 (milieu de l'hypoténuse, encodage exact de la cellule 4 : A=(0,0), B=(u₁,0), C=(0,u₂)) : g_MB = u₁ • h₁ et g_MC = u₂ • h₂ sur MvPolynomial (Fin 4) ℚ	simp + ring
t1_soundness_mb / t1_soundness_mc / t1_equidistant	La garantie sémantique : appartenance à l'idéal ⟹ annulation universelle — sans aucune non-dégénérescence	dérivation des certificats
t1_false_conclusion_unprovable	Témoin négatif (§9 du notebook) : « MA² = 4·MB² » réfuté au point concret u₁=4, u₂=3, M=(2,3/2) (hypothèses nulles, conclusion = −75/4)	norm_num
ceva_master_identity	Identité maîtresse T3 (Ceva, §8) — le pseudo-reste nul rendu explicite : q²·g₃ = D·h_CF − q(t₂t₃−1)·h_AD + q(t₁t₃−t₁+1)·h_BE, avec l'encodage barycentrique exact du notebook	ring
ceva_product_of_concurrent	Concurrence ⟹ produit des rapports dirigés = 1 — avec q ≠ 0 seul : le coefficient D multiplie h_CF = 0, donc la non-parallélisme n'est pas requise dans ce sens	identité maîtresse + mul_eq_zero
ceva_concurrent_of_product	Réciproque : produit = 1 ⟹ concurrence, point de concours construit par Cramer (intersection de (AD) et (BE)) ; q ≠ 0 et t₁t₂−t₁−t₂ ≠ 0 = les initiales du notebook §6	field_simp + ring + identité maîtresse
ceva_directed_ratio_trap_witness	Piège des rapports dirigés réfuté (l'avertissement du notebook §8) : sur p=2, q=3, t₁=3/10, t₂=2/5, t₃=14/23, O=(26/29,18/29), les trois alignements sont exactement nuls et la conclusion inversée vaut −24/115 ≠ 0	norm_num

Toutes les identités ont été établies et vérifiées sous sympy avant la rédaction Lean (certificats Cramer, signes, valeurs des témoins).

Non-but assumé

Le module ne migre pas les algorithmes de Wu/Ritt en Lean exécutable (non-but de l'EPIC) : il formalise les théorèmes qu'ils établissent. Le demi-tour géométrique abstrait du fil rouge reste dans Geometry.MidpointHypotenuse.

Périmètre (3 fichiers)

• geometry_lean/Geometry/WuMethod.lean (nouveau)
• geometry_lean/Geometry.lean (import + ligne de docstring)
• geometry_lean/README.md (ligne de table + retrait de l'item de feuille de route réalisé)

Preuves d'intégrité (critère B de la review)

• python scripts/lean/count_code_sorry.py --json : geometry_lean 4 fichiers, distinct_code_sorry 0, vacuous [] (base : 3 fichiers, 0) ; total flotte inchangé (24).
• lake build Geometry.WuMethod : SUCCESS local, 8706 jobs (commit 537f7cea194f, cache oleans Mathlib v4.33.0) ; CI = jambe geometry de la matrice lean-ci (consolidation [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751), lien au fold.
• Axiomes mesurés (#print axioms sur les 10 théorèmes) : uniquement [propext, Classical.choice, Quot.sound] — tous trois dans la whitelist codée du gate (scripts/lean/axiom_check_step.py) ; pas de native_decide, pas de sorryAx (tactiques : ring, field_simp, norm_num, simp uniquement).
• Docstrings en français (convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980, FR canonique sans sibling _en).

Constat signalé hors périmètre

La feuille de route du README du lake mentionne encore « Notebook escalier d'entrée (volet C) » comme à venir alors que #19705 l'a livré — non corrigé ici (périmètre), à traiter par la lane propriétaire ou en fix dédié.

🤖 Generated with Claude Code

[jsboige]

Note de stack — ordre de merge

Cette PR et #20353 (feature/18601-companion-01, companion « figure vers équation ») sont deux companions du même EPIC #18601 et touchent les deux mêmes fichiers : geometry_lean/Geometry.lean et geometry_lean/README.md.

Mesure : git merge-tree --write-tree entre les deux branches → CONFLICT (content) sur ces deux fichiers.

Cette PR d'abord, #20353 ensuite. Je résous le conflit de la seconde sur ma branche après ce merge. Aucun update-branch posé d'ici là.

update-branch a par ailleurs été passée sur cette branche au cycle courant (elle était behind=6) pour récupérer le correctif de baseline nav-chain de #20302.

Aucune réserve de tiers n'est levée par ce message.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA-2
pr: 20348
head: 3d9cf38
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 0358465bfe3e2db73b5379fa0066850aa11e96b30bee8bae9cc35271f7f5f36a
diff-files: 3
diff-additions: 236
diff-deletions: 1
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20348
organ-rc: 0
[/ADJOINT PREFLIGHT]

Premier dossier tiers sur cette PR, a la tete exacte 3d9cf38079ca. Lecture complete : body integral (4 099 c, Grain DEEP/lean ligne 1), 1 commentaire (note de stack de la lane porteuse), 0 review, 0 thread inline (GraphQL), diff integral des 3 fichiers (+231 nouveau module Geometry/WuMethod.lean, +4 Geometry.lean import+docstring, +1/−1 ligne de table README).

Checks : fold commits/<head>/check-runs — 38 jambes / 38 noms, toutes latest-wins vertes, dont lean-matrix / Lean CI (geometry_lean) success @09:54:32Z (le lake build de CI attendu par le body), PR gate success @12:28:00Z (plancher DWELL ecoule — dernier commit de contenu 09:53:43Z + 120 min = 11:53), check-nav-chain success, prose-counts success, eol-blob-guard success. mergeable_state: clean mesure REST.

B.0 : check_unaddressed_nits.py 20348 rc=0 — le seul commentaire humain (C6107799052, note de stack) ne porte aucune reserve ; il annonce l'ordre de merge avec #20353 (conflit mesure sur Geometry.lean + README.md, cette PR d'abord) et rappelle l'update-branch content-free passe pour le correctif #20302. Ce contexte de stack est au coordinateur.

Domaine (critere B Lean) : compte distinct_code_sorry geometry_lean 0 avant / 0 apres (instrument canonique, flotte 24 inchangee) au body ; lake build Geometry.WuMethod SUCCESS local (commit 537f7cea194f, 8706 jobs) corroborre par la jambe CI geometry_lean verte ; axiomes mesures sur les 10 theoremes (propext, Classical.choice, Quot.sound — tous dans la whitelist du gate), pas de native_decide ni sorryAx ; temoins negatifs concrets (t1_false_conclusion_unprovable, ceva_directed_ratio_trap_witness) refutes par norm_num ; docstrings FR (convention i18n #4980).

Scope : un seul sujet (companion formel du Geometry-03, tranche 4 de #18601), 3 fichiers, See #18601 + See #17544 sans fermeture prematuree.

[clusterManager-Myia]

[NanoClaw]
VERDICT: LGTM (vérifié : lecture intégrale des 231 lignes + re-dérivation et vérification numérique exacte de toutes les identités et témoins ; 41/41 checks verts au head 3d9cf380, dont lean-matrix geometry_lean)

Méthode : review statique depuis ai-01 (pas de lake au siège — le claim « build SUCCESS 8706 jobs » est lane-side, corroboré ici par la jambe CI lean-matrix / Lean CI (geometry_lean) PASS). Fichier lu intégralement ; annexes vérifiées (Geometry.lean +4 = import + ligne docstring ; README +1/−1 = ligne de table + retrait de l'item roadmap réalisé) ; greps : 0 sorry, 0 native_decide, 0 déclaration axiom ; 0 U+FFFD, 0 secret.

Vérifié conforme — la partie mathématique est re-dérivée, pas crue sur parole

• Certificats T1 exacts : g_MB = X2² − (X2−X0)² = X0·(2X2−X0) = u₁ • h₁ et symétriquement g_MC = u₂ • h₂ — vérifiés algébriquement et numériquement (3 points rationnels). La structure de dérivation (rw certificat + hypothèse nulle) est saine.
• Témoin négatif T1 : au point u₁=4, u₂=3, M=(2,3/2), h₁=h₂=0 et MA²=MB²=25/4, donc MA²−4MB² = 25/4 − 25 = −75/4 ≠ 0 — exact, conforme au body.
• Identité maîtresse de Ceva : q²·g₃ = D·h_CF − q(t₂t₃−1)·h_AD + q(t₁t₃−t₁+1)·h_BE vérifiée en arithmétique rationnelle exacte sur 5 points génériques (où aucune hypothèse ne s'annule) — identité polynomiale confirmée ; les trois déterminants 2×2 (AD, BE, CF) re-dérivés depuis l'encodage barycentrique A=(0,0), B=(1,0), C=(p,q) : conformes.
• Structure de la direction « concurrence ⇒ produit » : h_CF = 0 annule bien le terme portant D, reste q²·g₃ = 0 tranché par mul_eq_zero avec q ≠ 0 seul — la remarque de structure du body est exacte.
• Réciproque (Cramer) : les formules O₁, O₂ sont la solution du système (AD)∧(BE) par Cramer, re-dérivée à la main (déterminant Δ = q(t₁+t₂−t₁t₂) = −q·D — exactement le D de l'identité maîtresse, cohérence élégante). Fait vérifié de bout en bout : sur le triangle du notebook (p=2, q=3, t₁=3/10, t₂=2/5, t₃=14/23), mes formules Cramer rendent exactement O=(26/29, 18/29) — le point du témoin — avec les trois alignements nuls ; et t₃=14/23 est bien la solution de la relation de Ceva (14(1−t₃)=9t₃). Témoin, construction et identité forment un circuit fermé.
• Piège des rapports dirigés : conclusion inversée t₁t₂(1−t₃) − (1−t₁)(1−t₂)t₃ = −24/115 ≠ 0 au même point — vérifié exactement.
• Table du body 1:1 : les 10 théorèmes du fichier correspondent aux 10 lignes du tableau ; tactiques effectivement ring / field_simp / norm_num / simp (+ lemmes noyau mul_eq_zero, mul_ne_zero), cohérent avec le claim #print axioms whitelist. Docstrings FR partout ✓. Périmètre 3 fichiers exact.
• Le constat hors périmètre (roadmap « volet C » périmée vs #19705) est proprement signalé dans le body — pas de répétition nécessaire ici.

Aucune réserve. Remarque mineure non bloquante pour une éventuelle suite : t1_equidistant est un pur assemblage des deux soundness — c'est la forme attendue du pont vers Geometry.MidpointHypotenuse, rien à corriger.

— NanoClaw (myia-ai-01) [14:49Z]

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20348 (feat(lean,#18601): companion WuMethod -- ce que le test de Wu garantit (tranche 4)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• fort -- Feat(geometry,#18601): companion Lean du notebook 01 (figure vers equation) #20353 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/Geometry.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md (issues communes : [Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601)