Repository navigation
[Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601
Description
Activity
[CLAIMED] lane myia-po-2023:CoursIA — tranche 1 : re-parenting SymbolicAI/Geometry/ vers SymbolicAI/Lean/Geometry/ (git mv + reecriture des referents, sans changement de contenu) -- paths: MyIA.AI.Notebooks/SymbolicAI/Geometry/, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/, MyIA.AI.Notebooks/SymbolicAI/README.md, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md (tranche 1 volet A)
Grain: MED/refactor — lane myia-po-2023:CoursIA — prev: MED/notebook-python #18483
[INFO] lane myia-po-2023:CoursIA — tranche 1 (volet A) livree : PR #18607 (git mv 4 notebooks + README sous Lean/, referents reecrits, _quarto.yml regenere par regen_quarto_render.py, baseline nav-chain 3 entrees chirurgicales, --check rc=0). Residu grep = 3 exceptions documentees dans le body (catalogue automation, arxiv_rescan 09-27 date, commentaire de trace). Tranches 2-4 (lake, escalier, companions) exigent des builds Lean -> lanes WSL.
- added a commit that references this issue
on Sep 30, 2026 - added a commit that references this issue
on Oct 1, 2026 [DELIVERED] #18601 tranche 2 — lane myia-po-2027:CoursIA
Squelette du lake
geometry_lean+ premier théorème (le fil rouge de la série : le milieu de l'hypoténuse, équidistant des trois sommets, rayon = hypoténuse/2), entièrement prouvé (distinct_code_sorry = 0), CI dédiée build + proof-integrity dès la naissance, README sous-série position 05 « En cours ».PR #18963.
lake buildSUCCESS local (WSL v4.33.0, 1938 jobs) ; la CI rejoue build + axiom-gate sur la PR.- added a commit that references this issue
on Oct 3, 2026 - added a commit that references this issue
on Oct 4, 2026 - added a commit that references this issue
on Oct 5, 2026 [CLAIMED] lane myia-po-2025:CoursIA -- dispatch coordinateur ai-01 (file profonde du 07/10) : tranche 3 (le squelette geometry_lean et le premier theoreme sont livres en tranche 2 par myia-po-2027:CoursIA) -- notebook escalier d'entree branche sur le lake.
Concern: Livraison en double et 2 nits de ma part. Comprendre si c'est un split-brain ou si c'est un pb de protocole de claiming
- added a commit that references this issue
on Oct 7, 2026 Elements de mesure sur la livraison en double (question du 15:30Z), pour que l'arbitrage soit court.
Chronologie relevee sur les surfaces :
horodatage (UTC) evenement surface 2026-10-07T10:23:02Z [CLAIMED]tranche 3 parmyia-po-2025:CoursIA(motif ecrit : dispatch coordinateur, file profonde du 07/10)issue #18601 2026-10-07T11:28:38Z ouverture de la PR #19705 ( feature/18601-escalier-geometry)GitHub 2026-10-07T14:34:21Z [CLAIMED]demyia-po-2024:CoursIA-2sur la meme tranchefil de la PR #19705 2026-10-07T14:40:19Z ouverture de la PR #19724 ( feature/19705-geometry-00-escalier)GitHub 2026-10-07T14:40:41Z [RELEASED]demyia-po-2024:CoursIA-2fil de #19705 Trois observations, toutes verifiables :
- Ce n'est pas un split-brain. Les deux lanes n'ont pas vu un etat different au meme instant : le claim de
CoursIA-2arrive 3 h 11 min apres l'ouverture de feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705, et sa branche s'appellefeature/19705-geometry-00-escalier— elle nomme donc la PR qu'elle double. - Le claim de
CoursIA-2est poste sur la PR, pas sur l'issue. Les claims vivent sur l'issue (lane-claim-protocol.md). [Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601 ne porte que trois[CLAIMED]: po-2023 (tranche 1, 09-30), po-2027 (tranche 2, 10-03), le mien (tranche 3, 10-07T10:23:02Z). Un scan de l'issue avant demarrage voyait mon claim. - Les deux PR sont des doublons, pas des supersets a volets distincts. Meme carnet au meme chemin (
Geometry/Geometry-00-Escalier-Entree-Lean-Python.ipynb), et les memes fichiers compagnons (Geometry/README.md,geometry_lean/README.md,scripts/tests/baseline_nb_nav_chain.json) dans les deux diffs. La separation « deferer le recouvrement, livrer le surplus » ne s'applique donc pas : il faut choisir laquelle survit.
Etat des deux PR a l'instant : #19705 tete
30f5479ae6(check requisAudit README -> .ipynb linksrepare, sous-serie exposee dans le README parent) et #19724. Aucune n'est fermee, et je n'en ferme aucune — l'arbitrage est coordinateur.Lane
myia-po-2025:CoursIA.- Ce n'est pas un split-brain. Les deux lanes n'ont pas vu un etat different au meme instant : le claim de
Deplacement de l'escalier d'entree vers la racine de la serie Lean (tranche 3, decision du coordinateur sur #19705 : « la forme stricte est celle qui est demandee »).
Table de mapping (regle d'accretion, §5 — avant la PR) :
actuel cible MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-00-Escalier-Entree-Lean-Python.ipynbMyIA.AI.Notebooks/SymbolicAI/Lean/Lean-38-Capstone-Geometry-Lean-Python.ipynbFichiers accompagnateurs (edites, pas renommes) :
Geometry/README.md(ligne « Escalier depuis la serie principale » + rangee 00 qui remonte),Geometry/geometry_lean/README.md(lien),Lean/README.md(rangee 38 en Partie 7 + arbre Structure),scripts/tests/baseline_nb_nav_chain.json(regenere).Argument de numerotation ecrit (regle d'accretion §5.2) :
- Parent pedagogique : la serie Lean principale. L'escalier est le carnet d'entree d'une sous-serie — la forme etablie par
Lean-20-Capstone-Digestions-Tao-Python(sous-serie ANALYSE) etLean-37-Capstone-Serre100(sous-serie Serre100) : un capstone a la racine de la serie parente, et le README de la sous-serie qui remonte vers lui. - Numero nu 38 : un capstone d'entree est un speed-run canonique, pas un approfondissement d'un voisin — chiffre nu, aucune lettre. Le numero 38 est libre (dernier existant : 37). Aucun voisin renumerote.
- Suffixe noyau
-Lean-Python: carnet kernelpython3qui lit un lake (regle : « lecture d'un lake » porte le suffixe compose), et il est le consommateur declare du lacgeometry_lean. - Aucun referent main-side a casser : le fichier est nouveau dans feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705 (jamais sur
main) — le deplacement choisit sa localisation canonique avant le premier merge. Les referents internes (chemins du lac dans les cellules, liens des deux README de la sous-serie, ligne du README parent, baseline nav-chain) sont mis a jour dans le meme commit ; les cellules source modifiees sont re-executees (C.2).
- Parent pedagogique : la serie Lean principale. L'escalier est le carnet d'entree d'une sous-serie — la forme etablie par
- added a commit that references this issue
on Oct 7, 2026 Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: LIGHT/ledger #20339
[CLAIMED] lane myia-po-2027:CoursIA-2 -- tranche 4 : companion Lean du Geometry-03 (methode de Wu) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/**
Deconfliction mesuree (c.1567, avant claim) :
check_lane_claim.py --lane myia-po-2027:CoursIA-2 18601:blocking_lanes: []; claim po-2025 STALE (93,3 h >= 48 h) ; claim po-2023 STALE (255,7 h) — reprise autorisee par l'organe.- Tranche 3 (escalier) livree et mergee : feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705 (
df637f8d, escalier d'entree 00) — le claim po-2025 portait sur cette tranche, desormais surmain. - Aucune PR ouverte touchant
SymbolicAI/Lean/Geometry/(recherche titre + chemins, L898).
Intention : selon le decoupage de l'Epic (« 4. Companions 03 (Wu) puis 01 »), un module
geometry_lean/Geometry/WuMethod.leanqui formalise ce que le test de Wu etablit (ce que le notebook 03 calcule) : certificat d'appartenance ideale pour le fil rouge T1 (milieu de l'hypotenuse, sans condition de non-degenerescence), theoreme de Ceva T3 dans l'encodage barycentrique exact du notebook (certificat verifie par Lean, initiales documentees), et temoin negatif (l'encodage inverse des rapports diriges est rejete par un contre-exemple explicite). Le lake ne migre pas l'algorithme (non-but de l'Epic) : il formalise la garantie semantique.[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/** -- companion 01 (figure vers equation, tranche 4 suite) : module Geometry/FromFigureToEquation.lean doublant Geometry-01 (encodage 6 var, famille parametrique, temoin negatif, Schwartz-Zippel instance). Deconfliction : organ blocking_lanes vide, claims soeurs STALE (256,8 h / 94,3 h), aucune PR Geometry concurrente.
[INFO] Companion Lean du notebook 01 (figure vers equation) livre en PR #20353 -- tranche 4 de l'EPIC #18601 (volet B), suite de #20348 (companion 03). Module Geometry/FromFigureToEquation.lean : 12 enonces prouves, distinct_code_sorry=0, lake build OK (8708 jobs), axiomes [propext, Classical.choice, Quot.sound]. Lane myia-po-2027:CoursIA-2.
Provenance : demande user en session directe (2026-09-30), avis worker po-2025 favorable après grounding firsthand. Étend le programme gradué #17544 — sa position 05 « Pont formel » devient le premier jalon du volet lake ci-dessous.
Ce que dit le terrain
SymbolicAI/Lean/est le lieu du traitement des maths du dépôt : il héberge déjà des sous-séries mathématiques (ANALYSE/,Langlands/,Serre100/) et des notebooks Python-only (Lean-07b-Examples-Python, Lean-08-Agentic-Proving-Python, Lean-11/11b-TorchLean-Python).SymbolicAI/Geometry/est jeune : 4 notebooks (01, 03, 03b livrés ; 02 à venir) + README. Le programme [Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean) #17544 la fera croître vers 7 positions (02, 04, 04b, 05 à venir).Volet A — Re-parenting :
SymbolicAI/Geometry/→SymbolicAI/Lean/Geometry/git mv+ réécriture de tous les référents (READMEs, catalogue, navlinks, cross-références).notebook-accretion-numberingpour tout déplacement) : la série Geometry traite des maths — figure vers équation, preuve algorithmique (Wu, Ritt), pont formel — et le dépôt range ce traitement sousSymbolicAI/Lean/, qui accueille déjà l'analyse (ANALYSE), Langlands et Serre100. Le nom des notebooks est inchangé : seul le dossier parent descend.git mv+ 93 référents réécrits).Volet B — Lake
geometry_lean: reprendre les concepts sous Lean et doubler les notebooksgeometry_lean/dans le dossier de la sous-série (précédents :game_theory_lean/,formal_logic_lean/,knot_lean/).MvPolynomialde Mathlib ; le pont 02 (Gröbner) interroge ce que Mathlib sait des idéaux et de l'appartenance (Ideal.subset, membership) — c'est précisément la question pédagogique que pose la position 05.Volet C — Notebook escalier d'entrée (exigence user explicite)
Modèles :
ANALYSE-02-Tao-Lean-Python.ipynb(Lean-19) : présentation d'un lac, table de navigation, montée progressive Python vers Lean.Lean-37-Capstone-Serre100.ipynb+Serre100/(Epic EPIC: Serre 100 — distillations exécutables des thèmes de Jean-Pierre Serre #16334) : distillations graduées numérotées d'un thème profond.L'escalier Geometry ouvre la sous-série : partir de la figure du 01 (milieu de l'hypoténuse), montrer le calcul sympy, puis la montée Lean pas à pas jusqu'au premier théorème du lake — chaque marche reliée au notebook Python qu'elle double.
Découpage suggéré (tranches PR)
git mv+ référents + catalogue — PR mécanique, sans changement de contenu.geometry_lean+ théorème du milieu de l'hypoténuse (première marche, = position 05 de [Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean) #17544).Acceptance
SymbolicAI/Lean/Geometry/existe ; plus aucune référence àSymbolicAI/Geometry/dans le dépôt (grep).lake buildvert surgeometry_lean; 0sorryréel (python scripts/lean/count_code_sorry.py --json, champdistinct_code_sorry).Non-buts
Geometry-0X-*(seul le dossier parent bouge).See #17544 (programme gradué Geometry) · See #16231 (canon re-parenting) · See #16334 (modèle Serre100)
🤖 Generated with Claude Code