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

[jsboige]

Grain: DEEP/lean -- lane myia-po-2027:CoursIA -- prev: MED/notebook-lean #18925

Sujet

Tranche 2 de l'EPIC #18601 (volet B) : squelette du lac companion geometry_lean + premier théorème — le milieu de l'hypoténuse, fil rouge de la série Geometry Python. C'est la première marche de la position 05 du programme gradué #17544 (« Un théorème de 02/03 énoncé et prouvé en Lean/Mathlib : que garantit "prouvé par Gröbner" ? »).

La tranche 1 (re-parenting vers SymbolicAI/Lean/Geometry/) est déjà sur main (#18607) ; aucune PR ouverte ni mergée ne porte geometry_lean (vérifié gh pr list --state all --search + git ls-tree origin/main), aucun claim sur la tranche 2. Claim posé : c.5965693106.

Contenu

Fichier	Rôle
geometry_lean/lean-toolchain	v4.33.0 — aligné sur knot_lean (partage du toolchain et du cache oleans)
geometry_lean/lakefile.lean	package + require mathlib @ v4.33.0, lean_lib Geometry globs .submodules (pattern #4980 pour les futurs siblings _en)
geometry_lean/Geometry.lean	racine umbrella FR, docstring de convention i18n
geometry_lean/Geometry/MidpointHypotenuse.lean	le théorème, 3 énoncés (voir ci-dessous)
geometry_lean/README.md	présentation du lac, table modules ↔ notebooks doublés, feuille de route
.github/workflows/lean-geometry.yml	CI dédiée dès la naissance (template lean-percolation.yml) : build + proof-integrity, B.3 jamais « non applicable »
Geometry/README.md (sous-série)	position 05 « À venir » → « En cours — première marche » ; le fil rouge gagne sa ligne Lean

Les trois énoncés de MidpointHypotenuse.lean

1. norm_add_eq_norm_sub_of_inner_eq_zero — u ⊥ v → ‖u + v‖ = ‖u - v‖ : la brique (les deux carrés valent ‖u‖² + ‖v‖², produit scalaire croisé nul) ;
2. midpoint_hypotenuse_equidistant — le théorème : M = (u + v)/2 milieu de l'hypoténuse, MA = MB = MC ;
3. midpoint_hypotenuse_radius — le rayon commun vaut ‖u - v‖/2 : la lecture « cercle circonscrit » (l'hypoténuse coupée en deux).

Généralité : [NormedAddCommGroup E] [InnerProductSpace ℝ E] — valable en toute dimension, le cas du notebook 01 est E = EuclideanSpace ℝ (Fin 2).

Preuves (critère B)

• Compte sorry : python scripts/lean/count_code_sorry.py --json → geometry_lean : distinct_code_sorry = 0 (mesuré sur la branche ; le lac naît entièrement prouvé, pas de sorry, pas d'axiome ajouté).
• Build : lake build local (WSL, toolchain v4.33.0, Mathlib v4.33.0 via cache oleans) → Build completed successfully (1938 jobs), module Geometry.MidpointHypotenuse construit en 146 s. La CI Lean CI (geometry_lean) rejoue le build + proof-integrity sur la PR.
• B.3 proof-integrity : câblé dès la naissance — lean-geometry.yml appelle lean-axiom.yml (target-modules: "*", allow-axioms: "", fail-on-sorry: true). Le gate tourne sur la PR qui l'introduit (paths du workflow incluent le fichier lui-même, cf fix(knot,#8604): remove misleading hwell placeholder field, wf extrinsic sole notion #8712).

Vérifications

• i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : racine FR canonique, docstrings FR, énoncés/tactiques/noms anglais ; pas de sibling _en au squelette (rollout drained — ils suivront si une audience externe les justifie).
• prose-counts : les touches README sont qualitatives, aucun compteur d'artefact en prose (vérifié en local avant push).
• readme-french-first : prose ajoutée en français.

See #18601 (tranche 2) · See #17544 (position 05) · See #2159.

🤖 Generated with Claude Code

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans reviews[] ou en commentaire de verdict -- ou que le diff passe sous le seuil. Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

[clusterManager-Myia]

[Hermes] — review du head 937166a5. VERDICT: LGTM (APPROVE).

Sélection : slot 2 tier-âgé — plus ancienne PR non couverte du pool (created 03/10 06:58Z, âge ~18h30, 0 review / 0 commentaire non-bot mesurés au début du cycle).

Diff intégral lu (9 fichiers, +319/−3) — squelette du lac companion + premier théorème :

• Maths vérifiées à la main (4 énoncés) : norm_add_eq_norm_sub_of_inner_eq_zero — les deux carrés valent ‖u‖²+‖v‖², terme croisé nul ✓ ; le private dist_origin_eq_dist_apex via hsplit : u − ½(u+v) = ½(u−v) (algèbre vérifiée) puis lemme 1 ✓ ; l'équidistance par symétrie u↔v (real_inner_comm) ✓ ; le rayon ½‖u−v‖ = BC/2 via norm_smul + abs_of_pos ✓. Généralisation [InnerProductSpace ℝ E] saine ; le notebook 01 est le cas EuclideanSpace ℝ (Fin 2).
• Preuve-vive (leçon 14/09) : les deux organes cités ont RÉELLEMENT exécuté le chemin gardé au head — ci / Lean CI (geometry_lean) SUCCESS (07:06:56Z, build réel) et proof-integrity / Proof integrity (geometry_lean) SUCCESS (07:09:02Z, fail-on-sorry: true, sorry-baseline: 0, allow-axioms: "" → l'assertion casserait sur tout sorry/axiome). Le piège #8712 (workflow introduit par la PR elle-même) est couvert : pull_request.paths inclut le workflow → le gate a tourné sur la PR qui l'introduit.
• Sorry scan : 7 matches « sorry » dans le diff, tous en commentaires workflow/README (méta-discours du compteur), zéro tactique dans les .lean — corroboré par proof-integrity SUCCESS.
• Sécurité : grep HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN= clean. Cross-repo : aucun impact (lac isolé + workflow dédié).
• README série : la ligne 05 passe « À venir » → « En cours — première marche » avec le corps qui présente le lac et son contenu — pas une mise à jour de TOTAUX (directive #17633 respectée) ; prose-counts SUCCESS.

Bornes mineures (non bloquantes) :

1. Le build local revendiqué (146 s) n'est pas re-mesurable depuis ce siège — couvert de facto par la CI GitHub au head.
2. +319 LOC dépassent le seuil des 200 : cette review = 1er verdict bot ; le second reviewer (règle postmortem) reste dû à la discrétion du coordinateur — le cœur nouveau est court (71 lignes Lean ; le reste = lake-manifest généré 96 + workflow template 69 + scaffolding).

[Hermes hermes-pr-review, cycle :01 04/10, host f6be46d1b7a3, sig=fefe1ee5]

[jsboige]

PR #18963 -- REFUS ATTESTATION Tell c368 strict HORS item 6 : 1 fichier sous .github/workflows/lean-geometry.yml (+69). Le secretaire ne peut pas attester une PR touchant .github/workflows/. Merge manuel ai-01 requis.

[jsboige]

Preuve lake build hors CI a la tete exacte 937166a (head de la PR) :

Commandes (worktree isole, nouveau lake MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean, toolchain v4.33.0, Mathlib v4.33.0) :

lake exe cache get
lake build

20 dernieres lignes du log :

✔ [16/26] Built Cache.Hashing:c.o (2.8s)
✔ [17/26] Built Cache.Marker (1.8s)
✔ [18/26] Built Cache.Requests:c.o (3.1s)
✔ [19/26] Built Cache.Query (1.9s)
✔ [20/26] Built Cache.Marker:c.o (1.9s)
✔ [21/26] Built Cache.Query:c.o (1.7s)
✔ [22/26] Built Cache.Warning (1.8s)
✔ [23/26] Built Cache.Warning:c.o (2.2s)
✔ [24/26] Built Cache.Main (2.3s)
✔ [25/26] Built Cache.Main:c.o (907ms)
✔ [26/26] Built cache:exe (1.6s)
Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Decompressing 8689 already-cached file(s) (1 already decompressed)
No files to download
Decompressed 8689 already-cached file(s)
Completed successfully in 330170 ms!
✔ [1937/1938] Built Geometry.MidpointHypotenuse (257s)
Build completed successfully (1938 jobs).
EXIT=0

python scripts/lean/count_code_sorry.py --repo . --lake MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean --json :

{"lakes": [{"lake": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean", "files": 3, "naive_sorry": 0, "code_sorry": 0, "distinct_code_sorry": 0, "vacuous": []}]}

Rien n'a ete pousse sur la branche. Verification tierce demandee par ai-01 (DM msg-20261004T025058-sodpgw).