fix(gametheory,#15408): executer le compagnon Lean 06g et reparer son seul blocage de compilation

[jsboige]

Grain: DEEP/notebook-lean -- lane myia-po-2024:CoursIA-2 -- prev: DEEP/lean #18004

fix(gametheory,#15408): executer le compagnon Lean 06g et reparer son seul blocage de compilation

GameTheory-06g-Bounded-Agents-Lean.ipynb avait ete fusionne avec ses 9 cellules de code a execution_count: null et sans aucune sortie. L'acceptance de #15408 demande, en premier critere, une execution de bout en bout avec outputs reels et verdict EXEC_PROVED. Le compagnon Python (06f) satisfaisait ce critere ; le compagnon Lean non.

Cette PR l'execute pour de vrai, et corrige un blocage que le commit sans execution avait masque.

Le defaut trouve en executant

La premiere execution authentique a rendu 9/9 cellules, 1 erreur (Lean) — la cellule 11 portait 16 diagnostics Unknown identifier :

Unknown identifier `cooperate`     (x8)
Unknown identifier `defect`        (x9)

La cellule 11 reduit payoffRank cooperate cooperate, payoffRank cooperate defect, payoffRank defect cooperate, payoffRank defect defect sur des identifiants nus. Or cooperate / defect sont les constructeurs de RepeatedGames.PDAction, et PDAction n'est pas dans la portee du carnet : la cellule 2 n'ouvre que ProgramGames. Le module ProgramGames/Bounded.lean ouvre RepeatedGames PDAction dans son propre namespace, ce qui ne se propage pas a un carnet qui l'importe.

Reparation — la cellule 2 ouvre desormais RepeatedGames PDAction, comme l'en-tete du module qu'elle demontre. Les quatre #reduce rendent leurs valeurs (3, 0, 5, 1). Aucune autre cellule n'est touchee.

Le contraste avec le compagnon Python est instructif : 06f ecrit des stubs (result = None # TODO etudiant), 06g portait la solution complete — et une solution complete qui ne compile pas. C'est precisement ce que l'absence d'execution laissait passer.

Execution reelle (C.2 / H.3)

Mesure	Valeur
Commande	wsl_papermill.py execute <nb> --kernel lean4-wsl --cwd <lake-root>
Lake	game_theory_lean, lake build ProgramGames.Bounded — 3008 jobs, SUCCESS
Mathlib	db584cd6d46c ; toolchain v4.33.0
Resultat	9/9 cellules, 0 erreur (29,8 s)
Cellules de code a execution_count nul	0
Cellules de code sans outputs	0

Les sorties commitees sont celles de cette execution. Chaque #check rend le type annonce (cooperate_cooperate, defectBotBounded_unexploitable, defect_profile_programNash, programNashCheck_eq_true, payoffRank_le_iff), chaque #reduce la valeur attendue (mutualCooperationCheck -> true, unexploitableCheck mirrorBot basicFamily -> true, programNashCheck basicFamily defectBotBounded defectBotBounded -> true). Rien n'a ete edite a la main.

Reparation d'environnement (regle F, pas un contournement). Le lake n'avait aucun .lake. Le lake exe cache get lance sur /mnt/d (drvfs) s'est avere inexploitable : 11 s de CPU en 15 min, 677 Mo extraits — un gisement bloque sur l'I/O, pas un travail. Le lake a ete construit sur le FS natif WSL, en semant .lake/packages depuis un lake deja construit portant un lake-manifest.json byte-identique (cal433) : la construction locale est tombee a 67 s. Le carnet execute contre ce lake ; aucun paquet n'a ete deplace ni contourne.

Diagnostic dérive (C.4)

Le garde Kernel drift guard (base vs PR) signale un ecart sur ce carnet :

language_info.version: '4.32.1' -> ''   (major.minor 4.32 -> )

Cause classee (a) env / kernel, verdict CAUSE_FIXED.

Ce qui s'est passe. La version de base portait un tampon 4.32.1 sous name: "Lean". L'execution sur le noyau lean4-wsl a reecrit language_info avec ce que le noyau declare reellement : name: "lean4", mimetype: "text/x-lean4", et aucune cle version — le noyau n'en rapporte pas.

Pourquoi le tampon de base etait faux, et non la nouvelle valeur. lean-toolchain du lake pin leanprover/lean4:v4.33.0. Le 4.32.1 enregistre n'a donc jamais ete la version de ce lake : c'etait la trace du siege qui a redige le carnet, pas celle de ce qui tourne. Le carnet Lean frere de la meme serie, GameTheory-04b-Lean-NashExistence.ipynb, porte exactement la signature que cette execution produit ({"codemirror_mode": "lean4", "file_extension": ".lean", "mimetype": "text/x-lean4", "name": "lean4"}, sans version). Le carnet rejoint donc la convention reelle de sa serie.

Aucun effet observable sur le livrable. Le garde ne rapporte aucun signature_drift_cells : aucune sortie de cellule n'a change de texte. C'est le point qui compte — ce garde existe pour attraper la derive de repr() de flottants entre versions d'interpreteur, et un carnet Lean n'en expose aucune : ses sorties sont des Nat, des constructeurs PDAction et des types. L'ecart se limite a la ligne de version elle-meme, remplacee par la verite du noyau.

Ce qui n'est pas fait, et pourquoi ce n'est pas une jambe de bois. Rien n'est fige a la main : ni version reinjectee, ni language_info reecrit. Reinjecter 4.33.0 aurait fabrique une valeur que le noyau ne rapporte pas — la derive que ce garde interdit, commise dans l'autre sens. Il n'y a pas de defaut residuel a tracker : la metadata honnete est en place et identique a celle des carnets freres.

Deux points releves, non traites ici (signales pour arbitrage)

1. Les trois cellules « Exercice » de 06g portent la solution complete (def cooperateBudget : BoundedAgent := ⟨.cooperateBot, 2⟩ suivi des #reduce qui rendent le verdict demande par la consigne), la ou 06f ecrit des stubs. Requalifier ces cellules en exemple guide — ou les stubber — est une decision pedagogique, pas une execution : elle n'est pas tranchee ici. Les scanners scan_enrich_quality.py et scan_cell_ordering.py sont muets sur ce carnet.
2. La conclusion du carnet portait un verdict perime : « EXEC_PROVED — a confirmer par execution authentique », en attribuant ses sorties a une machine « qui n'a pas pu aboutir a un #check/#reduce nominal faute de .lake/ accessible ». Cette phrase decrivait l'etat anterieur ; elle decrit maintenant ce qui a reellement tourne. Seules deux cellules de source changent dans cette PR : la cellule 2 (le correctif) et la cellule 24 (cette phrase).

Verifications (sur le diff committe)

Organe	Resultat
wsl_papermill.py execute	9/9 cellules, 0 erreur
count_cell_errors (organe de la meme outil)	(0 Jupyter, 0 Lean)
check_notebook_outputs_required.py --path <nb>	0 cellule defectueuse
check_kernel_drift.py origin/main	1 finding, couvert par la section C.4 ci-dessus ; 0 signature_drift_cells
check_prose_quantitative_claims.py --diff origin/main...HEAD	[OK] aucun compteur quantitatif en prose
C.1 (raise NotImplementedError / assert False / 1/0)	0 construction
Cellules de code : execution_count + outputs	9 / 9 renseignes
Cellules de code du carnet	25 cellules avant, 25 apres (aucune ajoutee ni retiree)

metadata.papermill.input_path / output_path sont normalises au basename, comme sur le carnet frere 06b — normalisation de metadata toleree, pas une sortie de cellule.

Liens

• Issue : [GameTheory][ProgramGames] Deux notebooks compagnons Lean et Python pour Bounded #15408 (See, pas Closes : les deux autres points releves ci-dessus restent ouverts et appartiennent a l'issue)
• Module demontre : game_theory_lean/ProgramGames/Bounded.lean (le carnet ouvre desormais le meme couple que son en-tete open RepeatedGames PDAction)
• Compagnon Python : GameTheory-06f-Bounded-Agents-Python.ipynb
• Carnet frere Lean dont la metadata est identique apres execution : GameTheory-04b-Lean-NashExistence.ipynb

🤖 Generated with Claude Code

[github-actions]

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

[github-actions]

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

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]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.9s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.2s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.4s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	19.1s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.2s

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

[github-actions]

Notebook PR Validation: PASS

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

[clusterManager-Myia]

[Hermes] — review full-read head 67a0017 (P4 : >1000 lignes).

Verdict : APPROVE — compagnon Lean réellement exécuté, réparation de scope vérifiée à la source.

Vérifications :

1. Full read 25 cellules (9 code) via vue structurelle : headers uniques, 9 lectures placées immédiatement après leur cellule de code, aucune narration post-solution, prose non pilotée par un seuil de densité.
2. Gates #17040 programmatiques : exec_count 1→9 séquentiel sans trou, outputs authentiques lean4_jupyter (blocs Raw input/Raw output, compteur env 0→8) ; chaque valeur citée dans une lecture est présente dans l'output committé — le seul hit initial (« 44 »/« 48 ») est le pointeur « lignes 44-48 » de Bounded.lean, vérifié exact à la source : la branche | 0 => defect de act s'y trouve bien.
3. Cause racine du fix : la cellule 2 porte désormais open RepeatedGames PDAction (visible dans la sortie text/plain committée) — c'est bien ce qui remet les constructeurs nus cooperate/defect en portée (les 16 Unknown identifier de la cellule 11), fix minimal sans sur-scope.
4. Sécurité : 0 match credential sur le diff.
5. CI : organes verts (Golden-set, Exec-sequence ratchet, Markdown claims anchored, GameTheory pytest). Le FAIL « PR gate » est un agrégat périmé : complété 22:15:50Z sur un « Kernel drift guard » en échec, lequel a été re-roulé en succès sur le même head à 22:25:38Z (vérifié via check-runs API) — l'agrégat se lèvera au balayage horaire. Documenté, non bloquant.

[Hermes hermes-pr-review, cycle :22 27/09, host f6be46d1b7a3, sig=287da5d1]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 18141
head: 67a0017
complete: true
body: read
comments-reviewed: 5
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c16e9395209ea26170a41072fc6358756d87616465b96c86c8ca215aeb227d35
diff-files: 1
diff-additions: 1012
diff-deletions: 167
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Prévalidation tierce à tête exacte, sans approbation ni décision de merge. Body et issue #15408 lus ; cinq commentaires de bot, review Hermes APPROVED après le commit et zéro thread inline ; diff du seul carnet GameTheory-06g lu. Claim de myia-po-2024:CoursIA-2 borné au carnet, sans collision ; aucun veto de campagne gelée. Neuf cellules code portent des comptes séquentiels 1 à 9, sorties non vides et zéro erreur ; Papermill terminé en 28,57 s. Le correctif de source ajoute open RepeatedGames PDAction au vrai module ProgramGames.Bounded ; la sortie Lean réexécutée reflète cette commande, les valeurs 3/0/5/1 et programNashCheck ... → true. La prose de diagnostic annonce l'environnement et la limite de preuve, sans clore l'issue à deux carnets ni effacer les exercices à revoir. check_run_state.py --pr 18141 : 110 jambes / 91 noms, derniers états verts, PR gate SUCCESS à 00:13:53Z ; les échecs antérieurs étaient le minuteur DWELL, et les jambes annulées ont des successeurs verts. B.0 rc=0. À la capture : OPEN/MERGEABLE, mais mergeStateStatus: UNSTABLE malgré le pliage vert ; ai-01 doit vérifier la mergeabilité au moment de décider. Aucune exécution locale supplémentaire par l'adjoint : sorties et checks post-fix lus. Décision de merge réservée à ai-01.