feat(geometry,#19705): escalier d entree 00 -- de la figure au noyau by jsboige · Pull Request #19724 · jsboige/CoursIA

jsboige · 2026-10-07T14:40:19Z

Grain: DEEP/notebook-lean -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/notebook-python #19702

Résumé

Geometry-00 — L'escalier d'entrée : de la figure au noyau. Premier carnet de la série (volet C de #18601), qui traverse cinq marches de garantie croissante sur un même énoncé fil rouge (le milieu de l'hypoténuse, équidistant des trois sommets) :

Marche	Méthode	Garantie
1	flottant (`numpy`)	constat numérique
2	`sympy` symbolique	identité exacte universelle
3	témoin négatif	exclusion des cas non-rectangles
4	lecture du lac `geometry_lean/Geometry/MidpointHypotenuse.lean`	énoncé existe côté Lean
5	audit axiomes	`sorry` / `native_decide` / `Classical.choice` absents

Le carnet est le consommateur pédagogique du premier module du lac : il lit le fichier .lean réel, pas une copie. Il relie les méthodes de la série (01 figure/équation, 03 Wu, 03b Ritt, 04 DD+AR) et laisse au lecteur l'escalier « figure => noyau » que le programme gradué annonçait sans le montrer.

Fichiers

MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-00-Escalier-Entree-Lean-Python.ipynb (nouveau, 26 cellules, 6 code, 3 exercices, ~10 s de bout en bout, kernel python3 3.13.14, sympy 1.14.0 + numpy 2.4.2 + lecture du lac)
MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/README.md : ligne 00 ajoutée au programme, paragraphe « fil rouge » enrichi pour nommer l'escalier
MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md : l'escalier est nommé comme consommateur du premier module, ligne « roadmap escalier » marquée livrée

Validation (organes du dépôt, sur la tête `63a6994d62`)

Organe	Résultat
`validate_pr_notebooks.py origin/main <nb>`	1/1 PASS (6/6 cellules de code)
`check_cell_source_parses.py --pr-diff`	0 finding
`check_prose_quantitative_claims.py --diff`	`[OK] aucun compteur quantitatif en prose`
`count_exercises.py`	conforme (3 exercices détectés : repère oblique, témoin négatif symbolique, corollaire du rayon)

Sorties committées

Toutes les cellules de code sont exécutées (execution_count 1..6, aucun nul) avec leurs outputs réels. 0 erreur. Le carnet est exécutable de bout en bout (sympy + numpy + lecture du fichier Lean), seed 20261007 fixé, reproductibilité HIGH.

Leçon de fond

L'escalier complet, c'est la confiance vérifiée : on ne se contente pas de dire que le théorème est vrai, on montre où il est vrai (marches 1, 2), pourquoi il ne l'est pas ailleurs (marche 3 — sans témoin négatif, on ne sait pas si on a un théorème ou une coïncidence), et comment la preuve formelle tient sans axiome interdit (marches 4, 5).

Refs

Issue : feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705 (claim posé par lane myia-po-2024:CoursIA-2 le 2026-10-07)
EPIC parente : [Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601 (volet C)
Programme gradué : [Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean) #17544 (position 05 — Pont formel)
Lac companion : geometry_lean/Geometry/MidpointHypotenuse.lean (volet B de [Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601)
Re-parenting de la série : SymbolicAI/Geometry/ -> SymbolicAI/Lean/Geometry/ (volet A de [Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601)

🤖 Generated with Claude Code

Le notebook Geometry-00 est l'escalier d'entree de la serie : un meme enonce (le milieu de l'hypotenuse, fil rouge) traverse cinq marches de garantie croissante : 1. un triangle rectangle concret, distances mesurees (flottant) 2. le meme enonce en sympy, triangle quelconque (identite exacte) 3. triangle non-rectangle : le calcul sait dire non (temon negatif) 4. lecture du lac companion geometry_lean/Geometry/MidpointHypotenuse.lean 5. audit des axiomes interdits (sorry, native_decide, Classical.choice) Le carnet est le CONSOMMATEUR pedagogique du premier module du lac : il lit le fichier .lean reel, pas une copie. Il relie les methodes de la serie (01 figure/equation, 03 Wu, 03b Ritt, 04 DD+AR) et laisse au lecteur l'escalier 'figure => noyau' que le programme gradue annoncait sans le montrer. Fichiers : - Geometry-00-Escalier-Entree-Lean-Python.ipynb (nouveau, 26 cellules, 6 code, sorties committes ; kernel python3 3.13.14, ~10 s de bout en bout, sympy 1.14.0 + numpy 2.4.2 + lecture du lac ; seed 20261007) - README.md : ligne 00 ajoutee au programme, paragraphe 'fil rouge' enrichi pour nommer l'escalier d'entree - geometry_lean/README.md : nom de l'escalier comme consommateur du premier module, ligne 'roadmap escalier' marquee livree Validation organes (sur la tete 55f44cb) : - validate_pr_notebooks.py : PASS (6/6 cellules de code) - check_cell_source_parses.py : 0 finding - check_prose_quantitative_claims.py : 0 finding - count_exercises.py : conforme (3 exercices : repere oblique, temoin negatif symbolique, corollaire du rayon) Voir #18601 (EPIC parent), #17544 (programme gradue). Refs #19705. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

github-actions · 2026-10-07T14:47:39Z

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

github-actions · 2026-10-07T14:49:33Z

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

github-actions · 2026-10-07T14:49:34Z

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

github-actions · 2026-10-07T14:49:36Z

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

github-actions · 2026-10-07T14:50:39Z

Grain tag obligatoire (#10045, bloquant).

Grain tag absent (no Grain: / in body).

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

github-actions · 2026-10-07T14:51:01Z

Notebook outputs-required (H.4 schema): PASS (every code cell carries an `outputs: list`)

github-actions · 2026-10-07T14:53:10Z

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.4s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	26.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	8.2s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	18.5s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

github-actions · 2026-10-07T14:57:39Z

Notebook PR Validation: PASS

Notebooks checked: 1
Code cells validated: 6
Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

…ne nav-chain) - Geometry-00 (cells 18, 24): liens vers `.claude/rules/pr-review-discipline.md` corriges en 4 ups (chemin notebook = 4 niveaux sous la racine : notebook dans `MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/`). - Geometry-00: ligne 00 du tableau de programme dans Geometry/README.md passee de `.ipynb` a `.html` (le notebook est dans la render-list : la cible Pages est `.html`, pas la source brute). - baseline_nb_nav_chain.json : entree `orphan_entry` ajoutee pour Geometry-00 (coherent avec 01, 02, 03 deja en baseline : la serie Geometry n'a pas de chaine de navigation formelle, la baseline porte les entrees individuelles). Gates : - check-notebook-navlinks : OK 0 NEW (cellules 18/24 ne cassent plus la nav) - check-notebook-nav-chain : OK 0 NEW (Geometry-00 entre en baseline) - scan-enrich-quality : 0 finding - regen_quarto_render --check-readme-links : 2357 -> 2357 (0 nouveau) Refs #19724, cycle worker myia-po-2024:CoursIA-2 c.86.

jsboige · 2026-10-07T15:29:09Z

Concern: l'escalier doit vivre dans la série principale et permettre de descendre dans la sous-série

github-actions · 2026-10-07T16:24:27Z

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2023:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-07) :

CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=2 cap=1)
NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

github-actions · 2026-10-07T17:24:56Z

Path-collision (organ #13359/#13615)

Cette PR #19724 (feat(geometry,#19705): escalier d entree 00 -- de la figure au noyau) 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.

faible -- rename(search,#19253): decoupe PR-b -- Frontieres-07..09 (re-executes) completent la Partie 5 #19472 partage : scripts/tests/baseline_nb_nav_chain.json
faible -- refactor(gametheory,#16231): GT-03e Plan-deformation -> GT-23a Biens-Publics #19484 partage : scripts/tests/baseline_nb_nav_chain.json
faible -- feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-00-Escalier-Entree-Lean-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/README.md, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/geometry_lean/README.md, scripts/tests/baseline_nb_nav_chain.json

myia-ai-01 · 2026-10-07T18:24:52Z

Fermée par le coordinateur : cette PR double #19705.

Les deux PRs livrent le même carnet au même chemin, avec les mêmes trois fichiers compagnons. Le claim sur #18601 est celui de myia-po-2025:CoursIA (10:23Z), et #19705 a été ouverte à 11:28Z, trois heures avant celle-ci. Le claim posé sur #19705 à 14:34Z a été relâché à 14:40Z.

Le Concern du 15:29Z posé ici vaut aussi pour #19705, qui le portait déjà à 11:46Z : l'escalier vit dans la série parente et ouvre la descente vers la sous-série. Il se traite sur #19705.

La branche est conservée.

jsboige mentioned this pull request Oct 7, 2026

feat(geometry,#18601): escalier d'entree 00 -- de la figure au noyau #19705

Merged

github-actions Bot added the variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) label Oct 7, 2026

jsboige mentioned this pull request Oct 7, 2026

docs(vibe-coding,#14529): photo de famille — voix po-2026:Embeddings + addendum session historique #19715

Merged

github-actions Bot removed the variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) label Oct 7, 2026

jsboige mentioned this pull request Oct 7, 2026

[Epic] Geometry sous Lean : re-parenting de la serie, lake geometry_lean doublant les notebooks, notebook escalier d'entree #18601

Open

5 tasks

This was referenced Oct 7, 2026

rename(search,#19253): decoupe PR-b -- Frontieres-07..09 (re-executes) completent la Partie 5 #19472

Merged

refactor(gametheory,#16231): GT-03e Plan-deformation -> GT-23a Biens-Publics #19484

Open

myia-ai-01 closed this Oct 7, 2026

Navigation Menu

Repository navigation

feat(geometry,#19705): escalier d entree 00 -- de la figure au noyau - #19724

feat(geometry,#19705): escalier d entree 00 -- de la figure au noyau#19724
jsboige wants to merge 2 commits into
mainfrom
feature/19705-geometry-00-escalier

jsboige commented Oct 7, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

jsboige commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

myia-ai-01 commented Oct 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jsboige commented Oct 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Résumé

Fichiers

Validation (organes du dépôt, sur la tête 63a6994d62)

Sorties committées

Leçon de fond

Refs

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

Uh oh!

github-actions Bot commented Oct 7, 2026

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Oct 7, 2026

Notebook PR Validation: PASS

Uh oh!

jsboige commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Uh oh!

github-actions Bot commented Oct 7, 2026

Path-collision (organ #13359/#13615)

Uh oh!

myia-ai-01 commented Oct 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jsboige commented Oct 7, 2026 •

edited

Loading

Validation (organes du dépôt, sur la tête `63a6994d62`)

Notebook outputs-required (H.4 schema): PASS (every code cell carries an `outputs: list`)