fix(lean,#17357): Lean-16a Conway -- deux comptes perimes et un toolchain faux

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20122

Deux comptes périmés et un numéro de toolchain faux dans Lean-16a-Conway-Man-and-Work.ipynb — deuxième carnet de la file #17357 pour cette lane.

Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (2 constats), et 1 FAUX POSITIVE nommé et mesuré ci-dessous. Audit source : commentaire 5843605593 (Hermes, campagne #17073).

Diff : 5 insertions, 4 suppressions, 3 cellules markdown.

Constat 1 — « 4 théorèmes » pour Conway/Nim.lean (CONFIRMÉ, 2 sites)

Le fichier versionné (blob c7bd6000bf) porte 2 def + 15 theorem :

$ grep -c '^theorem' conway_lean/Conway/Nim.lean
15

et la sortie committée de la cellule suivante (show_lean('Conway/Nim.lean')) les liste tous les 15 (nimSum_nil … winning_move_verified_357). Le lecteur qui vérifiait la promesse comptait 15 pour un texte qui en annonçait 4.

Corrigé aux deux endroits : la ligne Nim du tableau de la section 3 et le paragraphe 3.3.

Occurrences sœurs vérifiées une à une — le tableau de la section 3 porte six lignes, et le défaut était isolé sur une seule :

Ligne	Annoncé	Mesuré	Verdict
Doomsday	5 théorèmes	grep -c '^theorem' → 5	exact
Look-and-Say	3 théorèmes	→ 3	exact
Nim / nim-sum	4 théorèmes	→ 15	périmé
Problème de l'Ange	4 théorèmes	→ 4	exact
Game of Life	7 micro-preuves	8 théorèmes dont le helper mem_sortDedup → 7 micro-preuves (block, beehive, blinker×2, toad, beacon, glider)	exact
MathlibMap	10 #check	→ 10	exact

Constat 2 — toolchain du projet conway_cgt_lean (CONFIRMÉ, mais le site de l'audit est faux)

L'audit nommait un commentaire de la cellule code 38, censé dire v4.31.0-rc1. Ce commentaire ne porte plus aucun numéro de toolchain :

# Build du module CGTTour (projet independant ; toolchain lue dans son propre lake)

Le défaut existe, mais ailleurs — dans deux cellules markdown qui annoncent v4.31.0-rc2 :

• tableau de la section 3 : « second projet Lake … (toolchain v4.31.0-rc2) » ;
• section 3.9 : « Ce second projet Lake (conway_cgt_lean/, toolchain v4.31.0-rc2) ».

La source de vérité est le fichier du projet : conway_cgt_lean/lean-toolchain → leanprover/lean4:v4.33.0-rc1, ce que la sortie committée de la cellule 37 imprime déjà (Toolchain : leanprover/lean4:v4.33.0-rc1). Corrigé aux deux endroits, là où le faux vit.

Constat 3 — FAUX POSITIVE (« 13 #check annoncés, 12 lignes de table, 14 en sortie »)

Le compte de l'audit est faux : la sortie committée liste 13 entrées numérotées, pas 14 — l'audit a compté les occurrences du motif #check, ce qui double la ligne de total « Total : 13 declarations #check ».

Les trois nombres sont réconciliables, pas contradictoires :

Mesure	Valeur	Ce qu'elle compte
CGTTour.lean sur disque	13	lignes #check du fichier
Entrées numérotées en sortie	13	la même liste, énumérée
Cibles distinctes	12	LinearOrder Surreal apparaît lignes 99 et 110
Table du markdown	12	les 12 cibles distinctes
Message de succès (cellule 38)	12	les 12 cibles distinctes

La seconde occurrence est délibérée : elle re-vérifie l'ordre total après l'instance CommRing Surreal (ligne 109). Le markdown annonce donc exactement ce que le fichier contient, et le tableau présente les 12 cibles distinctes. Rien à corriger — signalé nommément sur #17357, conformément au dispatch.

Portée du diff

Trois cellules markdown (indices 15, 22, 36) — les seules touchées :

3c2008ea  md  1698 -> 1699   (15 théorèmes, toolchain v4.33.0-rc1)
6a917c75  md   296 ->  297   (15 théorèmes)
fb21226a  md  1518 -> 1518   (toolchain v4.33.0-rc1)

Cellules, outputs, metadata, execution_count et types : inchangés sur les 48 cellules (vérifié champ par champ contre HEAD).

Aucune ré-exécution due : les trois corrections sont des cellules markdown (exception C.2 explicite). Les sorties committées — qui listent bien les 15 théorèmes et impriment bien v4.33.0-rc1 — étaient déjà justes ; c'est le texte qui ne l'était pas. La correction met le texte en accord avec la sortie, pas l'inverse.

Normalisation déclarée : l'outil MCP a complété l'id manquant d'une cellule markdown (index 39, désormais be806737) — le carnet n'était pas conforme nbformat 4.5 sur ce point. Une seule cellule concernée, aucune autre modification.

Observation non demandée (hors périmètre, signalée sans être traitée)

La sortie committée de la cellule 38 est un build en échec (error: Lean exited with code 139 sur Mathlib.Tactic.Lift et Mathlib.Init, build failed). Le code 139 est un SIGSEGV pendant la construction de Mathlib ; c'est un artefact d'environnement (checkout de dépendance bloqué), pas un défaut du carnet — et il n'entre dans aucun des trois constats de l'audit. Non traité ici : le périmètre de cette PR est les trois findings.

See #17357 — la file de cette lane compte 11 carnets ; ceci en traite 2 (Lean-11 en #20122). Les 9 autres suivent en PR séparées ([RELEASED] à la dernière).

🤖 Generated with Claude Code

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

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

✅ 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-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-09) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=4)
• 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]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.0s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.6s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.4s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	20.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.7s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	13.1s

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

[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 #20123 (fix(lean,#17357): Lean-16a Conway -- deux comptes perimes et un toolchain faux) 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(lean,#15629): Lean-16a conway -- encoding=utf-8 sur l'appel subprocess text=True du helper lake #19415 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb, recouvrement de chemins 100% -- Fix(lean,#15629): Lean-16a conway -- encoding=utf-8 sur l'appel subprocess text=True du helper lake #19415 est deja sur main.
• terminal -- Gorard #19741 — greffe Lean-16a (épilogue 2.3b) #19844 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb, recouvrement de chemins 100% -- Gorard #19741 — greffe Lean-16a (épilogue 2.3b) #19844 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.

[jsboige]

Le rouge markdown-rendering guard @21:38:26Z est un échec de CHECKOUT sur le runner auto-hébergé, pas un défaut du carnet

L'unique annotation d'échec du job (exit code 2) est :

Path 'MyIA.AI.Notebooks/GenAI/Security/Oversight/Backdoor-Code-From-Scratch.ipynb'
not uptodate; will not remove from working tree.

Ce fichier n'appartient ni à cette PR ni à main. Le diff de la PR touche un seul carnet (Lean-16a-Conway-Man-and-Work.ipynb) ; git log -- <chemin> sur main rend zéro commit — le carnet n'existe que sur la branche de la PR #20031 (Add(genai,#16754): Backdoor Code, po-2026). Le runner coursia-ephemeral a conservé le worktree d'un job antérieur de #20031 (le carnet y est suivi et modifié — vraisemblablement par un garde qui exécute les carnets), et le actions/checkout de ce job-ci n'a pas pu le retirer : le garde n'a jamais tourné.

Reproduction locale à la tête exacte cb89bcdf68 (worktree dédié, commands du workflow) :

• detect_markdown_rendering.py --selfcheck → rc=0 (8 familles de contrôles OK) ;
• detect_markdown_rendering.py --check --baseline ... → rc=0, « OK: no new ERROR-level markdown-rendering violations ».

Le job a été rejoué (gh run rerun 37953763207 --job 113970188723) : s'il retombe sur le même runner pollué, le rouge se reproduira sans que le contenu y soit pour rien — c'est alors un signalement runner-fleet (3e instance de la famille : #19669 « Could not read », #19853 « remote did not send all necessary objects », ici « not uptodate »).

See #17357

— lane myia-po-2023:CoursIA-2 (worker, cycle c.1233)

[github-actions]

Notebook PR Validation: PASS

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

[INFO] — lane myia-po-2023:CoursIA-2 — les 3 jambes rouges à la tête cb89bcdf68 sont la famille pollution runner (arbitrage #20174 c.6092735664 : runner_name cité, sans rejeu).

1. markdown-rendering guard (main-repo notebooks) @23:11Z — runner myia-po-2024-linux-persist-3. Reproduction locale à la tête exacte : --selfcheck OK + --check --baseline → OK: no new ERROR-level markdown-rendering violations (exit 0).
2. Consecutive code cells >= 2 advisory @18:23Z — runner myia-ai-01-wsl-6. Annotations : « Failed to traverse parents of commit / Could not read » = dépôt corrompu sur le runner (objets git manquants), pas un verdict pédagogique — l'organe advisory est « ALWAYS exit 0 » par contrat.
3. PR gate @17:46Z — dérivatif : agrège un timeout de la jambe 1 (« hit their declared timeout-minutes... cancelled, 10m22s »), pas un verdict.

Aucun rejeu lancé (arbitrage) ; le stale sweep re-conduira les jambes.

[jsboige]

Le rouge de l'advisory est fabrique — l'advisory n'a jamais tourne

La jambe Consecutive code cells >= 2 advisory (label, non-blocking) est bien failure a la tete cb89bcdf68b1, et elle produit un mergeStateStatus: UNSTABLE. Mais ce rouge n'emet aucun verdict sur ce carnet : le job est tombe avant la mesure.

Preuve (job 113898935978, run 37953763150)

Etape	Conclusion
1 Set up job	success
2 Checkout PR	failure
3 Set up Python	skipped
4 Advisory check on modified notebooks	skipped

Runner : myia-ai-01-wsl-6 — labels self-hosted, coursia-ephemeral, coursia-linux.

Les annotations du check-run disent la meme chose, en clair : Failed to traverse parents of commit 1da5be53631b79a050b7845c47e50be27ea50ec6 puis Could not read <sha> (une dizaine de commits). Le workflow demande fetch-depth: 0 parce qu'il fait un git diff a trois points ($BASE...$HEAD) : c'est cette lecture d'historique qui echoue, pas l'organe. Les etapes 3 et 4 etant skipped, detect_consecutive_code_cells.py n'a pas ete invoque — le rouge est un echec de checkout, jamais un finding.

Le verdict reel, mesure localement a la tete exacte avec la commande CI (detect_consecutive_code_cells.py --json --stdin) :

{'unmeasured': 0, 'total': 1, 'judged': 1, 'exempt': 0, 'consecutive': 1}

soit 2 runs de longueur 2 — et main porte exactement le meme consecutive: 1 sur ce carnet. Le finding est donc herite de la base, pas introduce ici (le diff de la PR sur ce fichier est de 5 insertions / 4 suppressions, une correction de texte). L'advisory est de surcroit non bloquant par construction.

Consequence : aucun CHANGES_REQUESTED, aucune action sur le carnet. Le UNSTABLE vient d'un rouge fabrique sur une jambe non requise, et c'est le seul obstacle residuel a un etat propre.

Classe et suite : meme famille que #20174 (checkout incapable de lire les objets — arbre/historique incomplet sur le slot), sur un autre workflow et un autre runner que ceux du lot Always-on guards. Conformement a l'arbitrage de cette classe : dossier (runner_name ci-dessus), pas de rejeu, pas de chasse, et pas d'update-branch (il perimerait le dossier exact-head de l'adjoint). Le volet de fond — un conteneur persistant qui porte le label coursia-ephemeral — appartient a la lane qui detient ces conteneurs.

🤖 Generated with Claude Code