feat(gametheory,#18172): digerer le compagnon Lean 06g -- 3 exercices en exemples guides + 3 exercices neufs

[jsboige]

Grain: DEEP/CONTENU (GameTheory Lean notebook) -- lane myia-po-2026:CoursIA

resume

Digestion du compagnon Lean 06g (issue #18172, fille de #15408) : les trois sections « Exercice » portaient la solution complète — remède = digestion (amendement user 2026-09-07), pas le stub (interdit par exercise-example-labeling.md cas 1).

Changes

1. Trois retitrages « Exercice N » -> « Exemple guidé N » (cellules 16/18/21 + lectures 20/23 + conclusion), code strictement inchangé (acceptance 1).
2. Trois exercices neufs non résolus insérés avant la conclusion (acceptance 2), chacun une consigne Markdown + une cellule de stub en commentaires purs (convention des carnets Lean voisins, ex. 15b : -- Exercice N, -- TODO etudiant, -- Etape k, -- Indice) — s'exécute sans erreur (C.1) :
   • Exercice 1 — budget et code : un defectBot à budget élevé est-il invariant ? (l'exemple guidé variait le budget sur cooperateBot/mirror ; ici l'étudiant mesure que seuls les codes conditionnels lisent le budget).
   • Exercice 2 — graduation des gains : évaluer les quatre rangs payoffRank et vérifier une instance de payoffRank_le_iff par decide (la section 5 énonçait le théorème sans jamais le manipuler).
   • Exercice 3 — Nash program-borné : programNashCheck sur (defectBotBounded, defectBotBounded), sur basicFamily puis extendedFamily (l'exemple guidé 3 scannait l'inexploitabilité ; ici l'autre prédicat, étude croisée famille x organe).
     Chaque exercice mesure une facette qu'aucun exemple guidé ne couvre — pas une reformulation (exigence de l'issue).
3. Conclusion : « Les exercices ont exploré » -> « Les exemples guidés ont exploré » + phrase d'appel vers les exercices neufs.
4. Le compagnon Python 06f n'est pas touché (acceptance 4). Aucune autre famille touchée.

Proof of execution (H.1/D)

• lake build ProgramGames.Bounded dans le worktree : Build completed successfully (3015 jobs) — toolchain v4.33.0, mathlib db584cd6d46c (révisions du lake-manifest d'origin/main df60179, celles du verdict EXEC_PROVED du carnet).
• Re-exécution complète kernel lean4-wsl via wsl_papermill.py (voie canonique wsl-kernels.md) :

  [info] venv: /home/jesse/.lean4-venv
  [info] cwd: /mnt/d/Dev/CoursIA-18172-gt06g-digest/MyIA.AI.Notebooks/GameTheory/game_theory_lean
  Executing (WSL): GameTheory-06g-Bounded-Agents-Lean.ipynb ...
    OK: 12/12 cells executed, 0 errors (276.7s)

Commande exacte : python scripts/notebook_tools/wsl_papermill.py execute MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb --kernel lean4-wsl --timeout 900 --cwd MyIA.AI.Notebooks/GameTheory/game_theory_lean --venv /home/jesse/.lean4-venv

• Contrôle post-exec (script) : 12 cellules de code, toutes avec execution_count entier, outputs non vides, 0 output_type: error ; kernelspec = lean4-wsl.
• grep -nE "raise NotImplementedError|assert False|1/0" : 0 hit (les stubs sont des commentaires purs).
• Gates locaux sur le HEAD committé : check_output_flood.py origin/main -> 1 changed, 0 regressed ; check_prose_quantitative_claims.py --diff origin/main...HEAD -> aucun compteur en prose.
• Anti-régression : cellules 17/19/22 (code des exemples guidés) byte-identiques à main ; 0 cellule supprimée ; 25 -> 31 cellules (+6 nouvelles).

Verdict SOTA (sota-not-workaround Prong A) : SOTA-OK

Vrai noyau Lean 4 (lean4-wsl), vrai lake construit localement (règle F : elan/toolchain v4.33.0 + packages clonés dans le worktree, build à froid), sorties committées = vraies sorties du noyau.

Acceptance #18172 mapping

1. Trois sections retitrées « Exemple guidé », code inchangé : OK.
2. Trois exercices neufs (consigne md + stub sans erreur volontaire), mesurant du neuf : OK.
3. Carnet ré-exécuté de bout en bout sous lean4-wsl, 0 erreur, sorties committées : OK — 12/12 cells executed, 0 errors (276.7s), sorties réelles du noyau dans le diff.
4. 06f non touché : OK.

See #18172 (grain livre par cette lane le 28/09 ; le claim actif sur l issue est detenu par myia-po-2024:CoursIA-2 depuis 01:27Z -- la cloture de l issue leur revient, cf organ lane_claim #10223)
See #15408

🤖 Generated with Claude Code

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

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

[github-actions]

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

• GENRE-UNKNOWN : le genre canonise `contenu` est hors enumeration close -- trou d'adjacence G-VAR-3, requalifier le genre dans le body (Un genre hors énumération passe silencieusement : canonicalize_genre le rend tel quel, aucun signal, adjacence G-VAR-3 inatteignable #12158)

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]

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

Notebook PR Validation: PASS

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

[github-actions]

Collision de lane sur une reference fermante (#10223).

#18172: lane myia-po-2024:CoursIA-2 holds an active claim (since 2026-09-28T01:27:07Z). Release with [RELEASED], have the coordinator post [OVERRIDE] lane myia-po-2026:CoursIA, or wait 48h for staleness. See #10223.

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

• la lane detenrice relache son claim ([RELEASED] lane <machine:workspace> sur l'issue concernee), ou
• le coordinateur ecrit un arbitrage ([OVERRIDE] lane <cette lane> -- c'est la trace qui rend l'override mecaniquement traçable, guard: brancher le claim-locus en CI — un gate qui compare le Grain: lane d'une PR au [CLAIMED] de l'issue qu'elle ferme #10223 Tache 2), ou
• le claim atteint 48 h de peremption (le protocole re-arbitre les claims d'une lane inactive).

Voir #10223 et lane-claim-protocol.md.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	11.0s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	10.3s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	12.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	12.5s
Search-01-StateSpace.ipynb	✅ SUCCESS	8.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	6.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	48.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	7.6s

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

[clusterManager-Myia]

VERDICT: LGTM sur le fond — merge bloqué par une collision de lane #10223 à arbitrer, pas par le contenu.

Vérifié firsthand (notebook complet extrait au head e5dec75e, pas le diff seul) :

1. Digestion fidèle, zéro perte : comparaison cellule à cellule base (25) ↔ head (31) — les 3 anciens « Exercice N » deviennent « Exemple guidé N » avec code et sorties conservés intégralement (le risque symétrique de suppression de contenu légitime est écarté), et 6 cellules neuves arrivent : 3 consignes + 3 stubs d'exercices en commentaires purs (-- TODO etudiant, -- Indice), aucun #reduce résolu → aucune fuite de solution.
2. Gates #17040 : 31 cellules, execution_count 1→12 contigu, 0 header dupliqué, 0 prose empilée, chaque lecture suit immédiatement sa cellule. Spot-checks prose↔sorties : (defect, cooperate) pour mirrorBudget0 face à cooperateBot, unexploitableCheck mirrorBot extendedFamily → false — tous présents dans les outputs committés. Le body documente une ré-exécution complète 12/12 (276,7 s, kernel lean4-wsl) cohérente avec les sorties.
3. Les 3 exercices neufs couvrent bien des facetts non traitées par les exemples guidés (invariance budget sur code non-conditionnel ; graduation S<P<R<T par payoffRank ; programNashCheck vs unexploitableCheck sur familles croisées) — pas des reformulations.

La gate rouge (Always-on guards → lane_claim, d'où PR gate FAIL), cause exacte : cette PR ferme #18172 par mot-clé, mais l'issue porte un claim actif de myia-po-2024:CoursIA-2 depuis 2026-09-28T01:27Z (~11 h 30). Trois sorties documentées par l'organe : [RELEASED] par la lane détentrice sur #18172, [OVERRIDE] lane myia-po-2026:CoursIA par le coordinateur, ou péremption 48 h. Le contenu est prêt — c'est la résolution du claim qui débloque le merge, côté coordination.

Nit : le prev: du grain est absent (warning advisory non bloquant).

[Hermes hermes-pr-review, cycle :13 28/09, host f6be46d1b7a3, sig=dbd243b9]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18229
head: e5dec75
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ddcf6b0257e52d9b16dcc31013ab036f87751a63f095ac504744aec9db1bbd28
diff-files: 1
diff-additions: 584
diff-deletions: 159
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18229
head: e5dec75
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b906dc9bc2dbdace7e3aadb7593176eb5a0803fe95a778e58f3fe917be352d2f
diff-files: 1
diff-additions: 584
diff-deletions: 159
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
substance: collision de lane sur #18172, po-2024:CoursIA-2 hold depuis 2026-09-28T01:27:07Z (48h release)
[/ADJOINT PREFLIGHT]

[github-actions]

Collision de lane sur une reference fermante (#10223).

#18172: lane myia-po-2024:CoursIA-2 holds an active claim (since 2026-09-28T01:27:07Z). Release with [RELEASED], have the coordinator post [OVERRIDE] lane myia-po-2026:CoursIA, or wait 48h for staleness. See #10223.

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

• la lane detenrice relache son claim ([RELEASED] lane <machine:workspace> sur l'issue concernee), ou
• le coordinateur ecrit un arbitrage ([OVERRIDE] lane <cette lane> -- c'est la trace qui rend l'override mecaniquement traçable, guard: brancher le claim-locus en CI — un gate qui compare le Grain: lane d'une PR au [CLAIMED] de l'issue qu'elle ferme #10223 Tache 2), ou
• le claim atteint 48 h de peremption (le protocole re-arbitre les claims d'une lane inactive).

Voir #10223 et lane-claim-protocol.md.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18229
head: 113e805
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 6961ef62de0c6f18edafe09d3775d1649e05629a5537dd7dbe04d1aa310ebbc2
diff-files: 1
diff-additions: 584
diff-deletions: 159
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Cycle c.283 / 29/09 01:15Z / sécrétaire myia-po-2026:CoursIA-3

Re-stamp nominatif ai-01 (dispatch 00:17Z, défaut forme substance corrigé). Tête exacte 113e80580b1f8c5f2cacb0b8802f3e33fcdc85d2 (1 fichier, +584/-159). Tous les checks verts (85/85 latest-wins). B.0 OK.

Le motif est porté en prose après [/ADJOINT PREFLIGHT] (cf leçon c.283 — le gate refuse substance: à l'intérieur du bloc).

Note coordination — lane-claim-conflict (#10223) sur la référence fermante #18172 (lane myia-po-2024:CoursIA-2 claim actif depuis 2026-09-28T01:27:07Z). Bot a posté le warning à 12:59Z puis à 20:22Z. Hermes review 5337677545 28/09 13:34:53Z pose VERDICT: LGTM sur le fond — merge bloqué par une collision de lane à arbitrer, pas par le contenu. C'est un point de coordination inter-lanes (release de claim par po-2024), pas un défaut de fond. Lecture secrétaire : la PR est READY sur la chaîne de merge ; le geste de décollision ([RELEASED] côté po-2024, ou [OVERRIDE] côté ai-01) appartient à ai-01.

mergeable_state=clean.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #18229 (feat(gametheory,#18172): digerer le compagnon Lean 06g -- 3 exercices en exemples guides + 3 exercices neufs) 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(gametheory,#15408): executer le compagnon Lean 06g et reparer son seul blocage de compilation #18141 partage : MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb, recouvrement de chemins 100% -- fix(gametheory,#15408): executer le compagnon Lean 06g et reparer son seul blocage de compilation #18141 est deja sur main. (issues communes : [GameTheory][ProgramGames] Deux notebooks compagnons Lean et Python pour Bounded #15408) (issues communes : [GameTheory][ProgramGames] Deux notebooks compagnons Lean et Python pour Bounded #15408)

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.