[GameTheory][ProgramGames] Compagnon Lean exécutable pour Bounded Agents #15603

Contexte

L’issue #15408 demande deux notebooks compagnons pour le module livré par #15395. La moitié Python est déjà claimée séparément sur GameTheory-06f-Bounded-Agents-Python.ipynb. Son claim porte un fichier nouveau encore absent et devient donc fail-closed pour toute l’issue dans check_lane_claim.py, bien que la moitié Lean soit matériellement disjointe.

Cette issue fille isole le compagnon Lean afin de rendre le verrouillage cross-lane mécanique et de conserver une PR atomique.

See #15408
See #15395
See #15062

Livrable

Créer MyIA.AI.Notebooks/GameTheory/GameTheory-06g-Bounded-Agents-Lean.ipynb, kernel lean4-wsl, sans modifier GameTheory-06e-Open-Source-Game-Theory.ipynb ni game_theory_lean/ProgramGames/**.

Le notebook doit charger le vrai module ProgramGames.Bounded, expliquer son modèle à budget fini et rejouer dans le kernel les certificats calculables exposés par le module.

Acceptance

• notebook exécuté de bout en bout avec outputs réels et verdict EXEC_PROVED ;
• chargement du vrai module ProgramGames.Bounded, sans copie locale de ses définitions ;
• au moins quatre familles de certificats rejouées, couvrant les propriétés calculables de coopération mutuelle, inexploitation, Nash borné et ordre fini des gains ;
• cooperateBot, defectBotBounded, mirrorBot, basicFamily et canonicalPD sont utilisés dans le parcours ;
• au moins trois exercices exécutables C.1, chacun précédé d’une consigne Markdown, sans erreur volontaire ;
• distinction explicite entre calcul fini et preuve Lean, sans extrapolation vers Löb ou Gödel ;
• navigation vers GameTheory-06e-Open-Source-Game-Theory.ipynb, [GameTheory][ProgramGames] Deux notebooks compagnons Lean et Python pour Bounded #15408 et le lake game_theory_lean ;
• 0 sorry introduit, 0 output d’erreur et output-failure ratchet sans régression ;
• catalogue généré byte-identique à main ;
• validation avec le vrai kernel lean4-wsl et les outils notebook canoniques du dépôt.

Hors périmètre

• compagnon Python GameTheory-06f-Bounded-Agents-Python.ipynb ;
• modification de ProgramGames.Basic, ProgramGames.Bounded ou de leurs siblings ;
• formalisation de Löb ou Gödel ;
• modification manuelle du catalogue ;
• nouvelle figure ou artefact visuel.