feat(gametheory,#14773): Lean v4.33.0 + Mathlib db584cd6 — game_theory_lean, asymmetric_information_lean, repeated_games_lean

[jsboige]

Grain: DEEP/lean — lane myia-po-2027:CoursIA — prev: MED/guard #17611

Tranche GameTheory — Lean v4.32.1 → v4.33.0 / Mathlib db584cd6d46c92f209a44c0f1c829460d327499d

Trois lakes migrés (issue #14773, Phase 4). Périmètre mesuré au départ : 8 lakes sur v4.32.1 dans le dépôt ; cette tranche livre les 3 lakes GameTheory, dont un home canonique (game_theory_lean) et une coquille archive (repeated_games_lean).

État par lake

Lake	Toolchain	Pin Mathlib	Manifest	lake build	distinct_code_sorry	Sondes #print axioms
game_theory_lean	v4.33.0	db584cd6	régénéré par Lake (22 lignes)	SUCCESS — 8770 jobs	1 (= baseline, inchangé)	[propext, Classical.choice, Quot.sound] max
asymmetric_information_lean	v4.33.0	inchangé (path-dep, byte-identique)	inchangé	SUCCESS (28 modules)	0	[propext, Quot.sound] max
repeated_games_lean	v4.33.0	db584cd6	régénéré par Lake	n/a — coquille archive (lib neutralisée #6146 : home canonique = game_theory_lean/RepeatedGames/, couvert par le build 8770 jobs ci-dessus)	0	couvert par game_theory

Deux adaptations de preuve (Mathlib 4.33, FR+EN siblings)

1. StableMarriage.proposedCount.initial (Lemmas.lean:112, Lemmas_en.lean:118) — la famille Set.setOf a été renommée/dépréciée (vers Set.mem_ofPred/Set.iInter_ofPred) : le simp [proposedCount, proposedSet, gsInitial] d'origine ne ferme plus le but d'appartenance {mw | False}. Nouvelle preuve par dépliage contrôlé : simp only [proposedCount, proposedSet, Finset.card_eq_zero] (delta pur, aucune forme setOf créée) puis ext mw + simp only [Finset.mem_filter, Finset.mem_univ] et simp [gsInitial] final sur un but sans setOf.
2. TUGame.marginalVector_dominates (Basic.lean:569, Basic_en.lean:569) — le comportement defeq de Fintype.equivFin a changé en 4.33 : unfold enumIndex; simp ne ferme plus heq. Remplacé par la forme term-mode (Fintype.equivFin N).symm_apply_apply i (defeq par delta sur enumIndex + eta structurelle + irrélevance de preuve — vérifié par sonde sur définitions répliquées, puis build).

Aucune régression : aucune preuve existante remplacée par sorry/stub ; seules ces deux preuves ont été adaptées au changement d'API, même énoncé, siblings FR/EN édités à l'identique.

Vérifications

• lake build SUCCESS sur les 3 lakes, exécuté en staging WSL avec Mathlib chaud vérifié au pin exact (git rev-parse HEAD = db584cd6…) — pas de replay de .olean périmés.
• python scripts/lean/count_code_sorry.py --lake … : game_theory 1 (baseline 1 — sorry résiduel préexistant, non touché), asymmetric 0, repeated 0.
• python scripts/lean/check_i18n_siblings.py game_theory_lean : 23/24 byte-identical + 1 consumer-pattern, 0 drift, 0 orphan (exit 0).
• Sonde axiomes manuelle (#print axioms sur TUGame.marginalVector_dominates, TUGame.bondareva_shapley, StableMarriage.proposedCount.initial/stepWith, StableMarriage.womenBestState.initial, AsymmetricInformation.BayesianLink.bridgeStrategy_isBNE, AsymmetricInformation.Lemons.poolingTenable_iff_cross/_mono) : aucun sorryAx, aucun native_decide.* ; Classical.choice uniquement en usage standard (tactique classical/Mathlib).

B.3 — applicable sur deux lakes du périmètre (corrigé après mesure des check-runs de la tête, adjoint c.61)

La déclaration initiale « non applicable » était inexacte — les check-runs de la tête 9375195 montrent deux jobs proof-integrity verts :

• proof-integrity / Proof integrity (game_theory_lean) : SUCCESS (23:47:02Z). Câblage lean-social-choice.yml — ses target-modules (SocialChoice.*, Abstraction*, ProgramGames.*) n'atteignent pas les modules modifiés (CooperativeGames/Basic(_en), StableMarriage/Lemmas(_en)) : le vert est hors-cible pour ces fichiers (cas (b)), les sondes #print axioms manuelles ci-dessus restent la preuve qui les couvre.
• proof-integrity / Proof integrity (asymmetric_information_lean) : SUCCESS (23:54:18Z), câblage lean-asymmetric-information.yml target-modules "*" — couvre le lake entier, fichiers modifiés inclus.
• repeated_games_lean : aucun workflow lean-axiom (cas (a)) — coquille archive, couvert par le build game_theory_lean.

Hors périmètre documenté

• social_choice_lean : exception upstream — DominikPeters/SocialChoiceLean master gelé au pin 94a4c650 avec toolchain v4.32.0 (vérifié via contents API au moment de la sélection du grain).
• Les 5 autres lakes sur v4.32.1 (hors GameTheory) restent à migrer dans d'autres tranches.

See #14773 (livraison partielle : 3 lakes / périmètre GameTheory de la Phase 4).

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] VERDICT: LGTM — bump Lean v4.32.1→v4.33.0 / Mathlib db584cd6, 3 lakes GameTheory (issue #14773 Phase 4).

Vérifié firsthand :

• Diff complet lu (293 l.) : toolchain + pins manifest x2 + 2 adaptations de preuve FR/EN à l'identique (symm_apply_apply pour heq defeq 4.33 ; dépliage simp only+ext pour initial après renommage Set.setOf). Même énoncé, aucun sorry ajouté (baseline 1 inchangé, sondes #print axioms sans sorryAx).
• Preuve-vive CI : Lean CI (game_theory_lean) 12m55s et Proof integrity (game_theory_lean) 13m27s verts sur ce head — compilation réelle des fichiers .lean modifiés, pas une jambe hors périmètre. asymmetric_information_lean : Lean CI + Proof integrity verts (28 modules), et son lakefile.toml confirme le path-dep lean_game_defs_ext voisin → manifest inchangé cohérent. repeated_games_lean coquille archive #6146 neutralisée, couverte par le home canonique — absence de job dédié acceptée.
• PR gate fail = DWELL (minuteur 25 min < plancher 120, #15197), pas un défaut de code — rien à corriger.
• 0 secret (grep du diff), 0 notebook touché, i18n siblings 23/24 byte-identical.

Note mineure : les inputRev pointent sur le SHA brut db584cd6… plutôt qu'un tag — lisible, mais un commentaire du SHA (ex. « pré-tag v4.33.0, cf. #14773 ») dans lakefile aiderait les tranches suivantes. Non bloquant.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17613
head: 9375195
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 3766017b74fcdcdf6424891293ed37c1317ad5ef0dc3640be04bbfadec3dc65e
diff-files: 11
diff-additions: 39
diff-deletions: 33
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier tiers au head 9375195f6a3fe36c32f436f1dc50c772aed43eb8. 41 jambes / 31 noms : aucun rouge, PR gate success 2026-09-24T04:43:48Z, aucune DWELL. REST : MERGEABLE/CLEAN. Zero commentaire ; une seule review, clusterManager-Myia, state=APPROVED, prefixe [Hermes] VERDICT: LGTM (etat et body concordants) ; 0 thread inline.

Diff +39/-33 sur 11 fichiers, aucun notebook : 3 toolchains portes a v4.33.0, pins mathlib db584cd6 dans les lakefiles et les manifests, asymmetric_information_lean ne change que son toolchain, et exactement 2 adaptations de preuve FR/EN a l'identique. Anti-regression mesuree : sorry ajoutees 0, native_decide ajoute 0, admit ajoute 0, retirees 0.

Le point B.3 du body est verifie firsthand : lean-social-choice.yml declare target-modules: "SocialChoice.*, ...", qui n'atteint ni CooperativeGames.Basic(_en) ni StableMarriage.Lemmas(_en) — le vert proof-integrity (game_theory_lean) est donc bien hors-cible, cas (b) que le body declare ; lean-asymmetric-information.yml porte target-modules: "*" et couvre son lake. Les deux declarations du body sont exactes.

Restent a ai-01 : lecture B.0 finale, verdict G-VAR sur le grain DEEP/lean, decision de merge. Non verifie par l'adjoint : lake build non rejoue — appui sur les jambes CI vertes au head exact.