feat(geometry,#17544): notebook Geometry-05 -- le pont formel (Grobner vs noyau) by jsboige · Pull Request #20062 · jsboige/CoursIA

jsboige · 2026-10-09T08:55:24Z

Grain: DEEP/notebook-python — lane myia-po-2025:CoursIA — prev: DEEP/notebook-lean #19705

Ce que cette PR livre

Position 05 du programme gradué de la série Geometry (Epic #17544) — la dernière marche du chemin principal, celle que le README de série annonçait comme « le pont formel ».

Un même carnet confronte le théorème fil rouge (le milieu de l'hypoténuse est équidistant des trois sommets) à ses deux verdicts :

	Gröbner (positions 02/03)	noyau Lean (cette position)
objet produit	un certificat (cofacteurs)	un terme de preuve
ce qui le vérifie	remultiplication par un lecteur	le noyau, automatiquement
dépendance à l'encodage	oui — §5 la mesure	aucune, le lac est coordinate-free

Contenu mesuré, pas repris d'un manuel

Chaque affirmation est calculée dans le carnet, et a été vérifiée hors carnet avant d'être écrite :

§1 lit le module Lean geometry_lean/Geometry/MidpointHypotenuse.lean comme texte — 4 énoncés dont 1 privé — aucun lake build, donc exécution CPU ;
§2 encode le fil rouge (B à l'origine, M milieu de [AC]) et réduit trois conclusions par sympy.groebner : restes nuls ;
§3 le certificat : cofacteurs (xa - xc), (ya - yc), 1, remultiplication à écart exactement nul ;
§4 le témoin négatif MA² = MB²/4 : reste (3/4)(xm² + ym²), somme de deux carrés — nul sur ℝ à la seule origine. La sortie étiquette explicitement les racines complexes que sympy rend par défaut, et le carnet explique pourquoi « où le reste s'annule-t-il » n'a pas de réponse sans dire sur quel corps ;
§5 rotation (forme invariante) contre cisaillement (forme périmée → reste non nul) : le verdict algébrique ne peut pas distinguer « théorème faux » de « encodage périmé » ;
§6 le tableau des deux garanties, plus le comptage textuel des axiomes interdits, déclaré comme indicateur — la mesure d'autorité reste l'organe du dépôt (scripts/lean/count_code_sorry.py, champ distinct_code_sorry) et la jambe proof-integrity.

Preuve d'exécution (C.2)

python scripts/notebook_tools/notebook_tools.py execute <nb> --python-only → SUCCESS, ~6 s, 10/10 cellules de code, execution_count non nul partout, 0 cellule en erreur, sorties committées.

C.1 : les trois exercices sont des stubs non bloquants (print("Exercice a completer")) — le carnet s'exécute de bout en bout non complété.

Le carnet n'utilise pas de LaTeX $…$ : check_math_render.py --path rend 0 occurrence.

Les 5 questions « organe d'abord »

Quelle série possède déjà la sémantique ? La série Geometry elle-même : sympy.groebner est l'organe des positions 02 et 03 ; la lecture du lac est le patron de Lean-38, l'escalier d'entrée.
Peut-on invoquer son module réel ? Oui — c'est ce que fait le carnet : sympy.groebner(..., order="lex", domain=sp.QQ) et le lac lu par candidats de chemin.
Sinon, que faudrait-il exporter ? Rien : aucun organe n'est contourné ni réimplémenté.
Quel témoin négatif l'organe natif fournit-il ? §4 — un énoncé faux sur le même encodage, rejeté avec son résidu nommé.
Quelle autre série assure la vérification indépendante ? Le lac Lean lui-même : MidpointHypotenuse.lean prouve le même énoncé sans coordonnées, et la jambe proof-integrity de lean-geometry.yml interroge les axiomes réellement utilisés. C'est le cœur du carnet : deux organes indépendants, deux garanties différentes.

Périmètre

6 fichiers : le carnet Geometry-05-Pont-Formel-Python.ipynb, le README de série, le README parent, _quarto.yml, et — pour mailler la chaîne de navigation — les pieds de page de Geometry-02-From-Equation-To-Proof.ipynb et de Geometry-04-DD-AR-Python.ipynb.

Trois corrections de cohérence dans le même geste :

la ligne 02 du README de série disait « À venir » alors que le fichier est sur main depuis feat(geometry,#17544): notebook Geometry-02 -- preuve par algebre (ideaux, Groebner, saturation) #17588 ;
la position 05 sort de « À venir » dans le README parent, où 04b reste la seule accrétion à venir ;
les pieds de page de 02 et 04 sont complétés (02 -> 03 et 04 -> 05) : sans eux la série avait deux entrées et les carnets 01/03/03b/04 étaient inatteignables depuis la base.

Chaîne de navigation vérifiée : check_notebook_nav_chain.py --check → rc=0, aucune nouvelle infraction. Garde prose quantitative : [OK] aucun compteur quantitatif en prose. Catalogue laissé byte-identique — il appartient à l'automatisation.

See #17544

🤖 Generated with Claude Code

…ve par Grobner » face au noyau Position 05 du programme gradue de la serie Geometry, derniere marche du chemin principal : le theoreme fil rouge (milieu de l'hypotenuse) est confronte dans un meme carnet a ses deux verdicts -- le certificat algebrique de Grobner (positions 02/03) et le terme de preuve du noyau Lean/Mathlib (lac companion geometry_lean). Contenu mesure, pas repris d'un manuel : - §1 lit le module Lean comme TEXTE (4 enonces, dont 1 prive) : aucun lake build, donc execution CPU en ~6 s ; - §2 encode le fil rouge (B a l'origine, M milieu de [AC]) et reduit trois conclusions par la base de Grobner : restes nuls ; - §3 verifie le certificat par remultiplication (ecart exactement nul) ; - §4 temoin negatif MA^2 = MB^2/4 : reste (3/4)(xm^2+ym^2), somme de deux carres -- nul sur R a la seule origine ; - §5 rotation (forme invariante) contre cisaillement (forme perimee, reste non nul) : le verdict algebrique n'a aucun moyen de distinguer « theoreme faux » de « encodage perime » ; - §6 le tableau des deux garanties, plus le comptage textuel des axiomes interdits (indicateur ; la mesure d'autorite reste l'organe du depot, scripts/lean/count_code_sorry.py, et la jambe proof-integrity). C.1 : trois exercices a stubs non bloquants. C.2 : 10/10 cellules, 0 erreur, execution_count non nul partout, sorties commitees. README de serie : la ligne 02 passe de « A venir » a « Livre (#17588) » (le fichier est sur main depuis cette PR) et la ligne 05 est liee. README parent : 05 sort de « A venir », 04b y reste. _quarto.yml : ajout du carnet. Chaine de navigation verifiee (--check rc=0, aucune nouvelle infraction). See #17544 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

github-actions · 2026-10-09T09:33:47Z

✅ 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-09T09:33:49Z

✅ 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-09T09:33:51Z

✅ 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-09T09:39:36Z

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-09T09:43:58Z

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	5.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	6.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	7.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	6.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	5.2s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	42.0s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.2s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	23.8s

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

github-actions · 2026-10-09T10:01:00Z

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

…metry-05 Le notebook neuf portait `../../Lean-38-Capstone-Geometry-Lean-Python.ipynb` alors qu'il vit dans `SymbolicAI/Lean/Geometry/` ; le fichier cible est dans `SymbolicAI/Lean/`, donc un seul niveau remonte. Corrige dans les DEUX cellules markdown qui portent le renvoi (introduction et conclusion) — le scanner dedoublonne par href et n'en signalait qu'une. Rouge impute a la PR : jambe `No enrich-quality regression in changed notebooks`, dont l'annotation du check-run nomme le notebook. Preuve, meme dossier et meme arbre, seule la version du contenu change : scripts/notebook_tools/enrich_quality_ci.py --base NONE --head <nb> -> rc=1 sur le contenu d'avant (1 finding [HREF_MISSING]), rc=0 apres. Le controle positif est refait dans le dossier du notebook : lance hors de l'arbre du depot, le meme organe fabrique deux faux positifs (`../README.md`, `geometry_lean/README.md`, valides mais irresolubles depuis le dossier temporaire). Modification markdown seule : aucune re-execution due (regle C.2, exception markdown). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

check-nav-chain rouge a la tete 9238a74 : le nouveau carnet 05 sans lien entrant faisait passer la serie a deux entrees (orphan_entry x2). Apres ce lien, la cause remontait plus haut : l'entree de serie (02) n'avait AUCUN lien sortant -- 01/03/03b/04 etaient deja unreachable en baseline, et 05 allait les rejoindre comme seul finding NOUVEAU. Deux lignes de pied de page au style maison (03b) : - 02 -> 03 : toute la chaine 02->03->03b->04->05 devient atteignable (8 findings baseline resolus, 0 nouveau) - 04 -> 05 : le nouveau carnet gagne son lien entrant Markdown seul, aucune cellule code touchee. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-09T12:02:37Z

check-nav-chain : cause racine traitée (a6920aa). Deux étages, le second invisible dans le premier diagnostic :

Étage apparent — le nouveau carnet 05 n'avait aucun lien entrant : la série passait à deux entrées (02, 05) et le garde émettait orphan_entry ×2. Fix : pied de page maison (style 03b) 04 → 05.
Étage révélé par le fix — l'entrée de série 02 n'avait aucun lien sortant : rien n'était atteignable depuis la base (01/03/03b/04 déjà unreachable en baseline), et 05 allait rejoindre cette dette comme seul finding NOUVEAU (unreachable). Fix : pied de page 02 → 03 — la chaîne 02 → 03 → 03b → 04 → 05 devient atteignable.

Vérifié localement à la tête poussée : check_notebook_nav_chain.py --check → OK: 0 NEW finding vs baseline — et 8 findings baseline résolus (la chaîne désormais maillée retire 03/03b/04/05 de l'unreachable). Markdown seul, aucune cellule code touchée (C.2 non déclenché), hooks pre-commit 12/12 Passed.

github-actions · 2026-10-09T15:37:57Z

Path-collision (organ #13359/#13615)

Cette PR #20062 (feat(geometry,#17544): notebook Geometry-05 -- le pont formel (Grobner vs 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 -- feat(sociochoice,#19371): SC-09 STV/Monroe/Chamberlin-Courant -- tranche 3 EPIC #19263 #19372 partage : _quarto.yml
faible -- refactor(gametheory,#16231): GT-03e Plan-deformation -> Dynamics-09 Biens-Publics #19484 partage : _quarto.yml
faible -- docs(research,#19452): Cartier-Miller P1 pseudocode C++ identity↔code #19504 partage : _quarto.yml
faible -- docs(research,#19494): Percolation-03 critique -- scoping finite-size scaling (palier 3) #19531 partage : _quarto.yml
faible -- feat(notebook,#19494): Percolation-03b critique -- extensions L=128, L=256 (convergence asymptotique) #19548 partage : _quarto.yml
faible -- docs(research,#19494): Percolation-04 Sharpness -- scoping (palier 4) #19556 partage : _quarto.yml
faible -- docs(notebook,#19494): Percolation-04 Sharpness -- execution (palier 4, c.1108) #19567 partage : _quarto.yml
faible -- feat(lean,#19644): Lean-17 Conway-Bridge-to-Knots - portail escalier #19669 partage : _quarto.yml
faible -- feat(notebook,#19681): SC-08 Mariage Stable -- Gale-Shapley + twin game_theory_lean/StableMarriage #19702 partage : _quarto.yml
faible -- fix(site,#18422): fix_hr_separator couvre les .md + conversion hr des 50 docs exclus #19792 partage : _quarto.yml
faible -- feat(lean,#19729 grain 1): ANALYSE-05-KLS-Lean-Python -- théorème 1.1 Bizeul-Klartag-Lehec en Lean + Python #19830 partage : _quarto.yml
faible -- feat(gametheory,#19883): Populations Othman-Sandholm -- generalisation du pilote 16e #19888 partage : _quarto.yml
faible -- ci(quarto,#19895): workflow quarto-render-list-freshness + regen _quarto.yml (purger la dette main) #19901 partage : _quarto.yml
faible -- feat(lean,#19908): tranche B pli 2 -- carnet ANALYSE-06 (companion natif des familles 127/132/186/192) #19916 partage : _quarto.yml
faible -- feat(19920,#19898): ANALYSE-07 Percolation-Critique -- pli 3 Origami (tranches A+B) #19943 partage : _quarto.yml
faible -- feat(genai,#19949): serie 3D -- NeRF from scratch + cinq limitations mesurees #19965 partage : _quarto.yml
faible -- Add(genai,#16754): Backdoor Code -- Houdini 3 etages vs Guard majority-vote (R12 Fig 12-13) #20031 partage : _quarto.yml
faible -- Add(notebooks,#16756): compagnon Lean 2.9f — apprendre, extraire, prouver sur EffectiveTheory #20063 partage : _quarto.yml
faible -- feat(notebooks,#20196): carnet SC-08b — economie du pool (frais, perte non-permanente, MEV) #20203 partage : _quarto.yml
faible -- feat(notebooks,#20211): QC-Py-43 -- diffusion sur series de rendements, controle negatif bootstrap et mesure d'augmentation #20212 partage : _quarto.yml
faible -- fix(lean,#18423): Lean-12 -- separateurs hr --- vers *** + _quarto.yml regenere (garde #11451) #20213 partage : _quarto.yml
faible -- Rename(ict,#16760): ICT-44 -> ICT-22c -- le carnet de la direction de verite rejoint le voisinage ICT-22x #20219 partage : _quarto.yml

github-actions · 2026-10-09T19:53:14Z

Notebook PR Validation: PASS

Notebooks checked: 3
Code cells validated: 37
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)

jsboige · 2026-10-10T07:24:10Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 20062
head: a6920aa
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: f5064c5b318f3dc807cef010460a6bb7a9037a2e7ea7d42690eb641b1d1ae60d
diff-files: 6
diff-additions: 1032
diff-deletions: 11
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20062
organ-rc: 0
[/ADJOINT PREFLIGHT]

READY — attestation tierce a la tete a6920aa027.

checks : latest-wins-green — pli live sans aucune jambe hors {success, skipped, neutral}. Observation : GitHub rapporte mergeStateStatus: UNSTABLE a la meme tete ; l'ecart entre les deux instruments n'a pas ete qualifie ici, il n'affecte pas ce contrat, qui ne lit que le pli des check-runs.
b0 : clear — check_unaddressed_nits.py 20062 rc=0 ; aucune review n'a ete postee sur cette PR (aucune remarque a lever), 0 thread inline.
scope : pass — 6 fichiers, +1032/-11 : le carnet neuf Geometry-05-Pont-Formel-Python.ipynb (1016 lignes), retouches de navigation sur Geometry-02 et Geometry-04, les deux README de serie et 1 ligne de _quarto.yml ; conforme au titre, COURSE_CATALOG non touche.
domain : not-applicable — carnet Python place sous SymbolicAI/Lean/Geometry/ mais qui ne touche aucun *.lean ; aucun projet QC ni artefact ML.

Commentaire tierce de prevalidation — n'approuve ni ne merge. Lane emettrice : myia-po-2023:CoursIA (file c2142).

myia-ai-01

Relu a la tete exacte. Geometry-05 : 27 cellules, ec 1..10, 0 erreur, trois exercices en stubs corrects ; les modifications de Geometry-02/04 sont des liens de navigation additifs. Remarque pour la suite (Epic #20250, phase 3) : la prose cite l'EPIC #18601 et l'EPIC #17544 et une « tranche 2 » ; mentions isolees, tolerees, a regrouper en pied de carnet lors du nettoyage de la serie. B.0 rc=0.

…pas re-chiffre Tranche Forensic de la non-regression appairee de #13778, seconde et derniere paire du claim vivant de cette lane (« Whale+FBI »). Re-execution par l'executeur canonique (kernel .net-csharp, cwd = dossier du carnet), sous le sous-module au gitlink de main : 9/9 cellules, 0 erreur, 41,1 s. VERDICT : NO REGRESSION sur la qualite -- medianes 37,0 (MGS) et 43,5 (mealpy), etendues [25-39] et [43-45], MGS gagne 4/4 graines, determinisme 8/8 : identique au chiffre pres. PROSE RECALEE (cellules 5 et 12) -- cinq passages, dont un qui ne pouvait pas etre re-chiffre : - course temoin : 458 ms -> 387 ms (runs anterieurs 458 ms, run original 322 ms) ; - ecart moteur ms/eval mealpy/MGS : 5,63x (0,031 contre 0,174) -> 6,47x (0,027 contre 0,173) ; - ecart fitness C#/Python : 5,13x (0,006 contre 0,031) -> 6,59x (0,007 contre 0,045) ; - vitesse du verdict : 5,63x -> 6,47x ; - **L'ENONCE QUI S'INVERSE.** Le carnet affirmait : « cette fois l'ecart moteur (5,63x) depasse l'ecart fitness (5,13x), a la difference de DE et SA ». Sur cette execution les deux ratios sont 6,47x et 6,59x : l'ordre BASCULE, et de 2 % seulement. L'enonce est donc RETIRE -- il n'est pas re-chiffre en son contraire, ce qui serait fabriquer une conclusion a partir d'un ecart de bruit. Ce qui est ecrit a la place : les deux ratios sont indiscernables ici, leur ordre a bascule d'une execution a l'autre, la paire ne soutient plus l'enonce qu'elle portait, et ce qui reste mesure est ce que chaque ratio dit separement. Ce que la tranche ne fait PAS : elle ne modifie aucune cellule de code, ne touche ni fonction de cout, ni budget, ni graines. La prose qualitative (separation totale de qualite, FBI devant SA) survit inchangee et verifiee. Diff 78 insertions / 438 suppressions. Comme sur MGS-25, la mesure cellule par cellule des tailles de sortie montre que la perte reelle est le blob JS probeAddresses de la cellule 2 (retire par strip_probe_banner.py) ; le solde est du compte rendu JSON et les metadonnees papermill/execution du run anterieur, que l'executeur .NET ne reecrit pas. Grain: DEEP/notebook-dotnet -- lane myia-po-2025:CoursIA -- prev: DEEP/notebook-python #20062 See #13778 Part of #1203 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

… Forensic (#20268) * Fix(mgs,#13778): MGS-25 non-regression Whale -- prose de cout re-ancree, sorties fraiches Tranche Whale de la non-regression appairee de #13778 -- claim vivant de cette lane, et restant nomme par la correction de liste du 10/10 (« Whale+FBI (claims vivants po-2025) »). Re-execution par l'executeur canonique (dotnet_executor.py, kernel .net-csharp, cwd = dossier du carnet), sous le sous-module au gitlink de main (2b21a6ae, GeneticSharp 4406ad7, reconstruit Debug net9.0, 0 erreur) : 9/9 cellules, 0 erreur, 42,5 s. VERDICT : NO REGRESSION. Qualite identique au chiffre pres -- medianes 49,5 / 49,5 / 51,0 conflits, etendues [46-51] / [46-53] / [50-54], memes conflits par graine sur les 12 paires graine-moteur, determinisme 12/12. Seules les colonnes de temps et la ligne d'environnement bougent. PROSE RE-ANCREE (cellule 12) -- deux passages citaient des nombres perimes : - ratio moteur ms/eval mealpy/MGS : 1,77x (0,039 contre 0,069) -> 2,46x (0,031 contre 0,077). Le nombre ne se substitue pas seul : a 2,46x il tombe DANS la bande du DE/SA (2,4x-3,3x) et non plus entre celle-ci et le coude-a-coude du PSO (0,8x-1,0x). La phrase est donc REECRITE, pas re-chiffree, et le ratio moteur est desormais declare sensible a la machine ET a la charge (1,69x run original, 1,77x run committe, 2,85x re-execution chargee, 2,46x ici) ; - ratio fitness C#/Python : 6,24x (0,007 contre 0,043) -> 6,40x (0,006 contre 0,039). L'ecart moteur (2,46x) reste sous l'ecart fitness : la revendication de la phrase survit telle quelle. SORTIES FRAICHES (C.2). La banniere probeAddresses (blob JS de 3168 car., 97 lignes JSON) est retiree par strip_probe_banner.py --apply, comme sur MGS-22/23/24/28/30. La banniere nuget de la cellule 6 passe de « Installed Packages pythonnet, 3.1.0 » a « Installing Packages pythonnet » -- forme que portent 5 des 9 carnets de la serie, donc pas un artefact isole. Le diff (86 insertions / 459 suppressions, net -373) se lit par la mesure, pas par le compte : la taille des sorties, cellule par cellule, ne baisse qu'en cellule 2 (-3168 car., le blob) et cellule 6 (-5 car., la banniere). Le reste des suppressions est du compte rendu JSON (le blob ligne a ligne) et les metadonnees papermill/execution du run du 02/10, que l'executeur .NET ne reecrit pas -- les conserver laisserait des metadonnees decrivant une provenance qui n'est plus la leur. Forme deja portee par MGS-22/26/28/30. Grain: DEEP/notebook-dotnet -- lane myia-po-2025:CoursIA -- prev: DEEP/notebook-python #20062 See #13778 Part of #1203 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Fix(mgs,#13778): MGS-27 non-regression Forensic -- un enonce retire, pas re-chiffre Tranche Forensic de la non-regression appairee de #13778, seconde et derniere paire du claim vivant de cette lane (« Whale+FBI »). Re-execution par l'executeur canonique (kernel .net-csharp, cwd = dossier du carnet), sous le sous-module au gitlink de main : 9/9 cellules, 0 erreur, 41,1 s. VERDICT : NO REGRESSION sur la qualite -- medianes 37,0 (MGS) et 43,5 (mealpy), etendues [25-39] et [43-45], MGS gagne 4/4 graines, determinisme 8/8 : identique au chiffre pres. PROSE RECALEE (cellules 5 et 12) -- cinq passages, dont un qui ne pouvait pas etre re-chiffre : - course temoin : 458 ms -> 387 ms (runs anterieurs 458 ms, run original 322 ms) ; - ecart moteur ms/eval mealpy/MGS : 5,63x (0,031 contre 0,174) -> 6,47x (0,027 contre 0,173) ; - ecart fitness C#/Python : 5,13x (0,006 contre 0,031) -> 6,59x (0,007 contre 0,045) ; - vitesse du verdict : 5,63x -> 6,47x ; - **L'ENONCE QUI S'INVERSE.** Le carnet affirmait : « cette fois l'ecart moteur (5,63x) depasse l'ecart fitness (5,13x), a la difference de DE et SA ». Sur cette execution les deux ratios sont 6,47x et 6,59x : l'ordre BASCULE, et de 2 % seulement. L'enonce est donc RETIRE -- il n'est pas re-chiffre en son contraire, ce qui serait fabriquer une conclusion a partir d'un ecart de bruit. Ce qui est ecrit a la place : les deux ratios sont indiscernables ici, leur ordre a bascule d'une execution a l'autre, la paire ne soutient plus l'enonce qu'elle portait, et ce qui reste mesure est ce que chaque ratio dit separement. Ce que la tranche ne fait PAS : elle ne modifie aucune cellule de code, ne touche ni fonction de cout, ni budget, ni graines. La prose qualitative (separation totale de qualite, FBI devant SA) survit inchangee et verifiee. Diff 78 insertions / 438 suppressions. Comme sur MGS-25, la mesure cellule par cellule des tailles de sortie montre que la perte reelle est le blob JS probeAddresses de la cellule 2 (retire par strip_probe_banner.py) ; le solde est du compte rendu JSON et les metadonnees papermill/execution du run anterieur, que l'executeur .NET ne reecrit pas. Grain: DEEP/notebook-dotnet -- lane myia-po-2025:CoursIA -- prev: DEEP/notebook-python #20062 See #13778 Part of #1203 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Fix(mgs,#13778): reserve NanoClaw -- retraction du positionnement WOA dans la bande DE/SA + clause valeurs non arrondies MGS-27 MGS-25 : le point 2,46x renversait le positionnement du run committé (1,77x) sous une derive a signe constant des timings (8 MGS ameliores, 4 mealpy degrades) -- signature d'une condition de run, pas d'une propriete de la paire. Meme traitement retractatif que la paire FBI : la plage mesuree (1,69x-2,85x) devient le chiffre de tete, le positionnement dans la bande est retire, ce qui est stable (MGS devant dans toutes les conditions mesurees) est enonce. MGS-27 : clause 'ratio calcule sur les valeurs non arrondies' ajoutee (quotient affiche 6,41x vs 6,47x imprime), aligne sur le carnet WOA. Markdown-only, aucune cellule code touchee, outputs et execution_count inchangs (splice chirurgical, pas de round-trip nbformat). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>

github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Oct 9, 2026

github-actions Bot added the variation-adjacency-deep-med Adjacence DEEP/MED hors LIGHT : §2 l'autorise si substance distincte (coordinateur) label Oct 9, 2026

github-actions Bot removed the variation-adjacency-deep-med Adjacence DEEP/MED hors LIGHT : §2 l'autorise si substance distincte (coordinateur) label Oct 9, 2026

This was referenced Oct 9, 2026

feat(genai,#19949): serie 3D -- NeRF from scratch + cinq limitations mesurees #19965

Merged

Add(genai,#16754): Backdoor Code -- Houdini 3 etages vs Guard majority-vote (R12 Fig 12-13) #20031

Merged

github-actions Bot mentioned this pull request Oct 9, 2026

Add(notebooks,#16756): compagnon Lean 2.9f — apprendre, extraire, prouver sur EffectiveTheory #20063

Merged

This was referenced Oct 9, 2026

docs(research,#19494): Percolation-03 critique -- scoping finite-size scaling (palier 3) #19531

Merged

feat(notebooks,#20196): carnet SC-08b — economie du pool (frais, perte non-permanente, MEV) #20203

Merged

myia-ai-01 approved these changes Oct 10, 2026

View reviewed changes

myia-ai-01 merged commit 57674c7 into main Oct 10, 2026
117 of 125 checks passed

myia-ai-01 mentioned this pull request Oct 10, 2026

Gate de prevalidation : aveugle aux sommets de pile (une PR ouverte porte une version plus recente des memes fichiers) #20251

Open

jsboige mentioned this pull request Oct 10, 2026

fix(mgs,#13778): non-regression des deux paires restantes -- Whale et Forensic #20268

Merged

Navigation Menu

Repository navigation

feat(geometry,#17544): notebook Geometry-05 -- le pont formel (Grobner vs noyau) - #20062

feat(geometry,#17544): notebook Geometry-05 -- le pont formel (Grobner vs noyau)#20062
myia-ai-01 merged 3 commits into
mainfrom
feature/17544-geometry-05-pont-formel

jsboige commented Oct 9, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

jsboige commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

myia-ai-01 left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

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

Uh oh!

Ce que cette PR livre

Contenu mesuré, pas repris d'un manuel

Preuve d'exécution (C.2)

Les 5 questions « organe d'abord »

Périmètre

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Oct 9, 2026

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

Uh oh!

jsboige commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Path-collision (organ #13359/#13615)

Uh oh!

github-actions Bot commented Oct 9, 2026

Notebook PR Validation: PASS

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

myia-ai-01 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jsboige commented Oct 9, 2026 •

edited

Loading

github-actions Bot commented Oct 9, 2026 •

edited

Loading

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

github-actions Bot commented Oct 9, 2026 •

edited

Loading