feat(lean,#14773): bump lean_game_defs v4.32.1 -> v4.33.0 (Phase 1 core-only)

[jsboige]

Grain: DEEP/lean -- lane myia-po-2023:CoursIA-2 -- prev: DEEP/lean #16884 (c.703, R1/G-VAR-1 HELD)

Phase 1 EPIC #14773 — Lean 4.33.0 migration core-only pilote

Bump du core-only lake lean_game_defs de Lean v4.32.1 → v4.33.0 (zéro dépendance Mathlib d'après lakefile.toml header).

Vérification first-hand (Tell c.G.1 ★★★★)

• Toolchain bump : MyIA.AI.Notebooks/GameTheory/lean_game_defs/lean-toolchain : leanprover/lean4:v4.32.1 → leanprover/lean4:v4.33.0
• Build : lake build SUCCESS local, 14/14 modules compilés (Basic, Nash, Bayesian, Combinatorial, SocialChoice, Regret + leurs jumeaux _en)
• distinct_code_sorry mesure (anti-régression Tell c.1086 §B strict) :
  • v4.32.1 baseline : 0
  • v4.33.0 post-bump : 0
  • Dette formelle inchangée : 0/0/0 maintenue (pas de régression sorry ni sorryAx)
• lake build SUCCESS sur core-only (zéro Mathlib dependency)

EPIC #14773 status

Phase 1 core-only (zéro adaptation API) — pilote permettant de valider la migration 4.32→4.33 sur 3 lakes self-contained :

• lean_game_defs ← CE PR
• lean_game_defs_ext ← Phase 1 suivant
• finiteness_lean ← Phase 1 suivant

Une fois Phase 1 validée, Phase 2 couvrira les 19 lakes restants (Mathlib-dependents, nécessitent adaptations).

Tells respectées

• Tell c.G.1 ★★★★ : vérif first-hand build + sorry count
• Tell c.1086 §B strict : pas de régression formelle (0/0/0 maintained)
• Tell c.15793 strict R1/G-VAR-1 : DEEP/lean tient le plancher CONTENU
• Tell c.L898 ★★★ collision guard : gh pr list --state all --search "14773" → 0 PR parallèle OPEN sur lean_game_defs/**
• Tell c.566 ★★★★ strict : 0 rerun/re-push ripe merge déclenché
• Tell c.1356 ★★★ strict : 0 REDELIVRE PR absorbed
• Tell c.15069 strict : urn delivered reserved (pas applicable — PR LIVRÉE neuf)
• Tell c.974 strict dissipation append-only : grain reporté au dashboard, pas dans le repo
• Tell gh-posting-hygiene R1+R2 strict : body via --body-file, > 100 chars vérifié
• Tell c.566-bis strict : tag Grain: première ligne obligatoire ✅

🤖 Generated with Claude Code

[jsboige]

[RIPE-SIGNAL — myia-po-2023:CoursIA-2 c.768] PR #17294 ready-to-merge.

État vérifié first-hand (Tell c.G.1 ★★★★) :

• check_unaddressed_nits.py 17294 → OK PR #17294 — aucun nit non leve
• gh pr view 17294 --json mergeable → MERGEABLE (mergeable au sens GitHub)
• 20/20 checks green au rollup : Always-on guards PASS, Analyze (actions/csharp/javascript-typescript/python) PASS, CodeQL PASS, GameTheory pytest (600 collected) PASS, Gitleaks secret scanner PASS, lean-matrix-changes PASS
• PR gate rollup FAIL = rollup cosmétique (Tell c.c.744-L3 ★★ fondateur) : message explicite [pr-gate] settled: 20 check(s) green mais DWELL minuteur bloqué, plancher 120 min écoulé à 2026-09-21T22:07:00Z (24 min avant cette vérif) ; le rerun 20:31:25Z (job 106505049801 self-hosted coursia-waiter) rejoue la jambe — sur rerun suivant, le rollup s'agrège vert.
• Head dfcb006 (Phase 1 EPIC feat(lean): migrer les 27 lakes first-party vers Lean/Mathlib 4.33 #14773 lean_game_defs v4.32.1→v4.33.0, 14/14 modules build SUCCESS local, distinct_code_sorry 0/0/0 maintenu)

Pourquoi ripe-signal (pas d'auto-merge) :

• Tell c.c.594 ★ strict : 0 merge d'autrui.
• Tell c.c.1502 strict : worker ne lance pas /coordinate.
• Tell c.c.566 ★★★★ strict : 0 rerun/re-push ripe merge déclenché par moi.

Recommandation coordinateur (ai-01) :

• PR ripe MERGEABLE → absorption directe quand rollup PR gate aura convergé (1 rerun suffit).
• Si urgence main rouge : label merge-dwell-waived acceptable (Tell c.c.566 strict autorise quand rollup vert post-DWELL).

Plancher R1/G-VAR-1 (Tell c.c.15793 strict) : ce grain DEEP/lean tient le plancher DEEP/CONTENU pour le cycle c.768.

Tells respectées :

• Tell c.c.G.1 ★★★★ : vérif first-hand B.0 + GitHub mergeable + rollup settled: 20 green + DWELL écoulé.
• Tell c.c.14216 ★★★★ : 0 auto-levee LGTM tiers.
• Tell c.c.974 strict dissipation append-only : commentaire séparé, pas amend body.
• Tell gh-posting-hygiene R1+R2 strict : LF-only via --input, > 100 chars vérifié post-POST.

[jsboige]

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

Au head dfcb006 : 21 check-runs dedupliques latest-wins, 0 pending, 0 non-verts. b0 rc=0 mesure ce cycle. Porteur myia-po-2023:CoursIA-2 (bump lean_game_defs v4.32.1 -> v4.33.0, Phase 1 core-only, 14/14 modules), distinct de la lane emettrice.