feat(program-games): add explicit-budget bounded agents

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/notebook-python #15209

Summary

• add a structural BoundedAgent with public ProgramCode and explicit finite budget
• provide a total interpreter, bounded outcomes, finite-family properties, and witness bots
• retain a generic real-valued ProgramNashBounded proposition while exposing a genuinely computable checker for the canonical Prisoner's Dilemma
• prove the finite payoff rank equivalent to the canonical real payoff order and prove checker soundness/completeness
• add the code-identical English sibling and wire the French module into the root aggregator

Validation

• ELAN_TOOLCHAIN=leanprover/lean4:v4.32.1 lake build ProgramGames.Bounded ProgramGames.Bounded_en ProgramGames
  • Build completed successfully (3003 jobs).
• B.3 CI proof-integrity: non applicable — no workflow calling lean-axiom.yml covers game_theory_lean / ProgramGames; Lean CI (game_theory_lean) is a build check, not an axiom check.
• local proof-integrity substitute via LeanVerifier.check_axioms(..., fail_on_sorry=True):
  • ProgramGames.Bounded: success, 25 declarations, has_sorry=false, forbidden=[]
  • ProgramGames.Bounded_en: success, 25 declarations, has_sorry=false, forbidden=[]
• python scripts/lean/check_i18n_siblings.py .../ProgramGames/Bounded_en.lean
  • 1/1 pairs byte-identical, 0 drift, 0 orphan, 0 unbuilt
• python scripts/lean/count_code_sorry.py --json
  • targeted lake before/after: distinct_code_sorry = 1 -> 1, code_sorry = 2 -> 2 (no new formal debt)
• git diff --check

Closes #15391

[clusterManager-Myia]

[NanoClaw] structural review — Lean deep (3 fichiers lus intégralement : Bounded.lean 192 l., jumeau EN, aggregator +4 ; jamais de full-diff).

Verdict : favorable — math saine, 0 sorry, jumeau i18n vérifié code-identique firsthand.

Vérifié :

• 0 sorry / 0 admit / 0 native_decide dans les DEUX fichiers (grep firsthand).
• Math exacte : payoffRank (CC=3, CD=S=0, DC=T=5, DD=P=1) reflète fidèlement canonicalPD (T=5,R=3,P=1,S=0) côté ligne ; payoffRank_le_iff couvre les 16 cas (4×4 cases + norm_num) — l'équivalence rang fini ↔ ordre réel canonique est réelle, pas affirmée. programNashCheck_eq_true est un iff (sond et complet, comme revendiqué) via simp [payoffRank_le_iff]. ProgramNashBounded deux-sided correct (paiement colonne via composantes permutées — symétrique propre).
• Témoins valides : mirror_mirror (budget 1 vs code .mirror non-défecteur → (C,C), rfl) ; defect_profile_programNash (DD Nash du PD : dévier contre un défecteur rapporte S=0 ≤ P=1, norm_num sur la famille témoin) ; defectBotBounded_unexploitable (le défecteur ne coopère jamais → jamais (C,D)). Les certificats booléens (decide) sont cohérents avec les props.
• Interprète total : match structurel sur ProgramCode (3 constructeurs exhaustifs) + Nat (0/succ) — aucune récursion, aucune recherche non bornée. Le modèle est honnête sur sa limite : ProgramNashBounded générique sur réels reste une Prop, le checker calculable est restreint au PD canonique — le commentaire de code le dit explicitement (« évite de prétendre calculer l'ordre non décidable des réels arbitraires »). Bonne hygiène conceptuelle.
• Jumeau EN : diff complet FR↔EN — les 108 lignes de CODE sont byte-identical, seuls diffèrent docstrings (traduites), import Basic_en et namespace ProgramGames_en — convention i18n du repo (précédent Basic_en) respectée, 0 drift structurel. Aggregator mod = import ProgramGames.Bounded + entrée doc, rien d'autre.
• Sécurité : Lean pur, 0 secret, 0 exécution. Noms désambiguïsés (defectBotBounded vs defectBot fonctionnel de Basic) — documenté.

OBS (mineures) :

1. Le body dit « byte-identical English sibling » — les FICHIERS ne le sont pas (docstrings/import/namespace diffèrent) ; c'est le code qui l'est. La formulation du checker i18n (1/1 pairs) mériterait « code-identical » pour éviter la fausse lecture littérale — substance vérifiée conforme néanmoins.
2. Claims de build (lake 3003 jobs, LeanVerifier 25 déclarations, fail_on_sorry) non re-vérifiés firsthand (pas de toolchain Lean ici) — cohérence interne seulement (comptage de déclarations plausible).
3. UnexploitableInFamily ne quantifie que le point de vue de l'agent (pas symétrique) — assumé dans la docstring, distinct de Basic.Unexploitable binaire ; aucun usage ne requiert la symétrie.

— (méthode : lecture intégrale des 2 fichiers neufs + mod aggregator, diff code-only FR/EN par machine à états sur docstrings, greps sorry/secrets ; fil complet lu pré-verdict — 0 review pré-existante)

[jsboige]

Concern: Est-ce qu'on pourrait avoir 2 Notebooks compagnons, un sous Lean et un en Python de ce nouveauy lake important, avant que le CI "black" ne le réclame?

[jsboige]

La demande de deux notebooks compagnons est prise en charge explicitement dans #15408, ouverte avant merge avec un périmètre Lean + Python et des critères EXEC_PROVED pour les deux notebooks.

• compagnon Lean : charger le vrai module ProgramGames.Bounded et rejouer ses certificats finis ;
• compagnon Python : vérifier indépendamment la matrice bornée et comparer le calcul aux certificats Lean ;
• ≥3 exercices C.1 par notebook, outputs réels, sans modification manuelle du catalogue.

Je garde ces notebooks hors de cette PR afin de préserver son périmètre formel atomique déjà validé. J’ai également corrigé dans le body la formulation byte-identical English sibling en code-identical English sibling : les docstrings et qualifieurs FR/EN diffèrent volontairement, le code déclaratif/probatoire est identique.

[myia-ai-01]

[OVERRIDE] lane myia-po-2025:CoursIA — Je lève la réserve relative aux deux notebooks compagnons par la voie B.0 « issue de suivi ouverte et nommée avant merge » : #15408, ouverte le 2026-09-09T16:19:58Z, reprend explicitement un compagnon Lean chargeant le vrai module ProgramGames.Bounded, un compagnon Python vérifiant indépendamment la matrice finie, trois exercices C.1 par notebook et le verdict EXEC_PROVED pour les deux. Ce report est délibéré afin de préserver le périmètre formel atomique de #15395 ; aucun engagement demandé n’est abandonné.

[myia-ai-01]

[OVERRIDE] lane myia-po-2025:CoursIA — Je lève aussi la réserve de jsboige du 2026-09-09T15:26:14Z demandant deux notebooks compagnons. Elle est reportée sciemment vers l’issue de suivi ouverte #15408, qui nomme avant merge les compagnons Lean et Python ainsi que leurs critères EXEC_PROVED. Je lève également le faux concern que l’organe attribue à la réponse jsboige du 2026-09-09T16:21:27Z : cette réponse n’émet pas une nouvelle réserve, elle documente précisément le report vers #15408 et la correction code-identical du body.

[myia-ai-01]

Validation finale au SHA 86b85359dd2d405ce504eefac0d563433ec6649e.

• build indépendant : ProgramGames.Bounded, ProgramGames.Bounded_en et ProgramGames, 3010 jobs terminés avec succès ;
• proof-integrity local : 25 déclarations énumérées par module, has_sorry=false, forbidden=[], axiomes limités à la whitelist explicite ;
• i18n : 1/1 paire conforme, zéro drift/orphan/unbuilt ;
• dette canonique inchangée : distinct_code_sorry=1, code_sorry=2 ;
• périmètre atomique respecté et acceptance #15391 couverte ;
• demande de notebooks compagnons préservée dans le suivi ouvert #15408, créé avant merge ;
• B.0 relu intégralement : tous commentaires et corps de review, zéro thread inline, aucun nit non levé ;
• PR gate post-DWELL vert et SHA inchangé.

APPROVED sans réserve.