Gorard #19741 — greffe lot Serre100 (06 + 10)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA — prev: DEEP/qc #19670

Greffe du lot Serre100 de la chaîne Gorard — l'un des cinq grains de livraison ouverts par #19741 (plan de distillation : issuecomment-6042350850). Livre les trois cellules décrites par #19747.

Ce que la PR change

Trois cellules markdown ajoutées, aucune cellule de code touchée : exception C.2, aucune re-exécution due. Diff : 2 fichiers, 36 insertions, 0 suppression — pure addition, aucun reformatage.

Carnet	Ajoutée après	Timestamp	Apport
Serre100/10-empilements-borne-lp-cohn-elkies	c271e800 (index 18)	[02:04]	le cas Viazovska, cité par Gorard comme jalon de son propre basculement
Serre100/10-empilements-borne-lp-cohn-elkies	ec0c5c65 (index 11)	[01:54] + [02:12]	certifier sur grille fermée vs vérification par un noyau
Serre100/06-bulles-minkowski	cell-16 (index 17)	[00:00] + [00:24]	thèse de Lanyon AI : exécutable = constructible

Ancrage par id, jamais par index

Le body de #19747 cite des index (17 et 10) qui ont dérivé de +1 depuis sa rédaction : main porte désormais 25 cellules dans le carnet 10, et les deux cibles sont en index 18 et 11. Les ids, eux, sont stables et ont été contre-vérifiés (c271e800, ec0c5c65, cell-16). La greffe s'ancre donc sur les ids ; l'écart d'index est consigné ici parce qu'il est la cause directe du point « Organes » ci-dessous.

Une seule histoire, deux greffes

Le contexte de la transcription (fenêtre 95-150 s) montre que [01:54] et [02:04] ne sont pas deux faits distincts : c'est un seul récit. Gorard raconte qu'en mars 2026 une preuve auto-formalisée, de bout en bout, a été produite par une société d'autoformalisation — et précise juste après que le résultat était l'empilement en dimensions 8 et 24, celui de Viazovska. Les deux greffes se répartissent donc le même passage : l'une sur le résultat, l'autre sur l'autonomie de la vérification.

Vérification

• Citations relues firsthand contre la transcription archivée (G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2026 - Gorard - ....json), horodatages [00:00], [00:24], [01:54], [02:12], [02:04]. La citation [00:24] vient du montage d'ouverture (l'invité, pas le narrateur) — d'où le *ibid.* du second bloc de la greffe 06.
• Deconfliction : la greffe Borcherds de Borcherds #18286 — greffe lot Serre100 (06 Viazovska + 07 Euler + 09 Ramanujan) #18366 vit en cell-14 du carnet 06 (« Dimensions hautes »), la mienne en cell-16, fin de la même section. Relues ensemble, elles ne se recouvrent pas et ne se fusionnent pas.
• Organes relus après greffe, tous au niveau de la base : check_split_reading_cells, check_interp_positioning, check_lecture_anchor, check_cell_source_parses, check_duplicate_sections, scan_md_hierarchy, detect_code_in_markdown_cells.
• check_accent_restoration_invariants rend rc=0 (avec --fail-on-findings) et n'est pas câblé en CI. Ses findings sont l'artefact de sa comparaison positionnelle (zip par index, l.108) sur un fichier qui gagne 2 cellules : son propre finding CELL_COUNT_CHANGED base 25 vs head 27 le nomme, et les insertions aux index 11 et 18 d'un fichier de 25 cellules produisent exactement les 14 appariements décalés constatés.
• nbformat.validate sur les deux carnets : VALIDE (27 et 28 cellules).

Note de plancher

Ce grain est déclaré MED : c'est une greffe de contenu pédagogique, pas un résultat nouveau. Il ne tient donc pas le plancher G-VAR-1 (DEEP de contenu) — dit ici explicitement, comme le veut G.3.

Closes #19747 · See #19741 · See #16334

🤖 Generated with Claude Code

[github-actions]

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #19753 (Gorard #19741 — greffe lot Serre100 (06 + 10)) 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.

• terminal -- Fix(serre100,#17601): carnet 10 — ajouter le ## Plan manquant #19648 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/10-empilements-borne-lp-cohn-elkies.ipynb, recouvrement de chemins 50% -- Fix(serre100,#17601): carnet 10 — ajouter le ## Plan manquant #19648 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

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]

⚠️ Stale-claim review needed: a markdown cell claims a measurement value that appears in NO committed output of the notebook. Advisory, NOT a merge gate — triage against the JSON artifact.

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]

✅ 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]

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]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=4 cap=3)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=0 genre=4 cap=3)
• 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]

Notebook PR Validation: PASS

• Notebooks checked: 2
• Code cells validated: 20
• 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]

Trois rouges traités à la tête 5db2ce9 ("fusionner les lectures ajoutées dans leur paragraphe existant") :

1. Split-reading ratchet (base vs PR) — exit 2 mesuré sur 5e6e3c8 : trois SECOND_READING (06 c.18 citation Gorard ; 10 c.12 « Pourquoi certifier » et c.20 « vu de l'entretien »). Cause : la greffe posait une seconde cellule de lecture sur des sorties qui en portaient déjà une. Fix canonique du mandat ("une sortie = une lecture", #16554/#17464) : fusion verbatim dans la cellule hôte — 06 c.17 (Lecture), 10 c.11 (section 4, intro) et 10 c.19 (### Lecture du résultat) ; 985+1318+1066 chars préservés, aucune suppression (anti-régression). Vérifié : check_split_reading_cells.py --base-ref origin/main --head HEAD --fail-on-findings → exit 0, 0 régression.

2. arXiv attributions registry — exit 1 mesuré : l'entrée 1603.06518 (PR #19186) pointait cell_index 24, la greffe avait décalé la citation (Ressources du 10) à 26. La fusion ci-dessus la ramène à 24 : FAIL levé sans éditer le registre. Vérifié : check_arxiv_attributions.py → exit 0, 14 PASS / 0 FAIL. Aucun nouvel ID arXiv dans le diff ajouté (scan mécanique du diff : 0).

3. latex-control-chars — le rouge CI n'était pas un finding de contenu : la jambe est morte au checkout (git fetch --unshallow échoué 3× — "missing blob object 263f09ba…", "remote did not send all necessary objects", annotations du run), l'organe n'a jamais tourné. Mesuré localement sur le scope PR : check_latex_control_chars.py --pr-diff origin/main HEAD → exit 0, 0 occurrence (le scan whole-repo ne voit que 6 occurrences préexistantes sur main, hors des deux carnets Serre100, grandfathered hors scope PR) ; tests unitaires 25/25 OK. Le push de 5db2ce9 relance la jambe.

Cellules modifiées : markdown uniquement (aucune sortie touchée, pas de re-exécution due).

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	10.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.6s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.8s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	35.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	7.2s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	21.2s

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

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19753
head: 5db2ce9
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: dc2e5da21b08db999e905726a1d75025021b11686af68df24073c0e180833889
diff-files: 2
diff-additions: 21
diff-deletions: 3
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19753
organ-rc: 3
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA
pr: 19753
head: 5db2ce9
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e1133ab1cc78d02073f95e042e4e235f756c92133223a64d3c011f0cdc6c36c8
diff-files: 2
diff-additions: 21
diff-deletions: 3
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
supersedes: 11
supersedes-why: le dossier BLOCKED precedent attestait un etat de jambes ou de levees depasse ; a la meme tete, la derivation live rend checks verts, B.0 clear
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19753
organ-rc: 0
[/ADJOINT PREFLIGHT]

Derivation live READY a la tete vive : le dossier BLOCKED anterieur attestait des jambes alors en cours ; jambes latest-wins vertes, B.0 clear, aucun thread non resolu.