ci(lean): wire proof-integrity gate onto ProgramGames (B.3 hole, #15221 follow-up)

.github/workflows/lean-social-choice.yml

@@ -15,6 +15,8 @@ on:
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction/**.lean'
+      - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames.lean'
+      - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/**.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain'
       # The gates' own implementation: a change to them must re-run them
@@ -33,6 +35,8 @@ on:
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction/**.lean'
+      - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames.lean'
+      - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/**.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean'
       - 'MyIA.AI.Notebooks/GameTheory/game_theory_lean/lean-toolchain'
       - '.github/workflows/lean-social-choice.yml'
@@ -109,6 +113,19 @@ jobs:
   # STRETCH doctrine), not a certified module. target-modules is pinned to
   # SocialChoice/CERTIFIED.txt by
   # scripts/tests/test_check_certified_sorry.py::test_workflow_targets_match_manifest.
+  #
+  # ProgramGames (B.3 wiring, #15221 follow-up): the L1 bounded-core modules
+  # (Basic + Basic_en, 0 sorry, 0 native_decide -- #15221) join target-modules
+  # as companion targets, same status as Abstraction. Bounded + Bounded_en
+  # landed AFTER this scope was written (#15395, 2026-09-10); they are added
+  # here (review digest on #15379) for the same reason: the path filter already
+  # fires on ProgramGames/**.lean, so leaving them out of target-modules would
+  # keep the B.3 hole for exactly the modules the filter was added for. The root
+  # ProgramGames.lean is a docstring-only aggregator (no decls), so it is not a
+  # target -- same precedent as the SocialChoice root. Gate coverage on these
+  # modules was the hole ai-01 named on #15221 (2026-09-08T19:22Z): the gate was
+  # wired on the lake but out of target for them, so a green proof-integrity
+  # certified nothing about ProgramGames.
   proof-integrity:
     # c.327 (ai-01 CHANGES_REQUESTED 2026-09-08): the two REAL compiles (`build`
     # and `proof-integrity`) must serialize. Depending only on the cheap
@@ -122,7 +139,7 @@ jobs:
     with:
       project-path: MyIA.AI.Notebooks/GameTheory/game_theory_lean
       display-name: game_theory_lean
-      target-modules: "SocialChoice.AMD,SocialChoice.Arrow,SocialChoice.Arrow_en,SocialChoice.Basic,SocialChoice.Basic_en,SocialChoice.Framework,SocialChoice.Framework_en,SocialChoice.MechanismDesign,SocialChoice.MechanismDesign_en,SocialChoice.Sen,SocialChoice.Sen_en,SocialChoice.SortedListCounting,SocialChoice.SortedListCounting_en,SocialChoice.Voting,SocialChoice.Voting_en,Abstraction,Abstraction.Basic"
+      target-modules: "SocialChoice.AMD,SocialChoice.Arrow,SocialChoice.Arrow_en,SocialChoice.Basic,SocialChoice.Basic_en,SocialChoice.Framework,SocialChoice.Framework_en,SocialChoice.MechanismDesign,SocialChoice.MechanismDesign_en,SocialChoice.Sen,SocialChoice.Sen_en,SocialChoice.SortedListCounting,SocialChoice.SortedListCounting_en,SocialChoice.Voting,SocialChoice.Voting_en,Abstraction,Abstraction.Basic,ProgramGames.Basic,ProgramGames.Basic_en,ProgramGames.Bounded,ProgramGames.Bounded_en"
       # allow-axioms inherits the workflow default (named standard set:
       # propext, funext, Classical.choice, Quot.*) -- same contract as conway.
       fail-on-sorry: true

docs/reference/lean-axiom-coverage.md

@@ -204,6 +204,7 @@ forbidden union : []
 | `asymmetric_information_lean` | `lean-asymmetric-information.yml` | OUI (#13139, 2026-08-26) | **GREEN mesuré** (exécution locale du step exact du gate, 2026-08-26 : 51 déclarations sur 6 modules, clôture axiomatique = `propext` + `Quot.sound` seulement, 0 `sorryAx`, 0 `native_decide`, 0 `Classical.choice`) ; `target-modules: "*"` + `fail-on-sorry: true` cohérent avec baseline 0. **Premier lake du dépôt avec un `[[require]]` cross-lake par chemin** (`../lean_game_defs_ext`) : le caller déclenche aussi sur les sources de la dépendance — un gate aveugle à la moitié de ses entrées n'est pas un gate. `lake build` local WSL SUCCESS (28 jobs, toolchain v4.32.1) |
 | `percolation_lean` | `lean-percolation.yml` | OUI (#14904, 2026-09-06) | **GREEN mesuré** — `distinct_code_sorry = 0` (`count_code_sorry.py --json`, 13 fichiers), 0 `native_decide` / 0 `sorryAx` (grep FR + `#print axioms` des tranches #14896/#14897/#14907 = `[propext, Classical.choice, Quot.sound]`, sous-ensemble des défauts du workflow réutilisable). `target-modules: "*"` (dérivation runtime #10889, `_en` exclus par défaut) + `fail-on-sorry: true` cohérent avec baseline 0. **Contrôle positif HARD exécuté** : mutation `sorry` temporaire sur `probe/*` → `proof-integrity` ROUGE, retirée → vert sur la tête propre |
 | `planning_lean` | `lean-planning.yml` | OUI (#15305, 2026-09-09) | **GREEN par défaut** — source mesuré: `count_code_sorry --lake planning_lean` `code=0` (les 5 `grep` naive sont en commentaire/docstring, pas du code), 0 `native_decide` (token fiable §1.1), 0 `noncomputable` (aucune inférence `Classical.choice`); `target-modules: "*"` (dérivation runtime #10889, `_en` exclus par défaut → `Planning.Strips`/`Relaxation`/`Admissibility`) + `fail-on-sorry: true` cohérent baseline 0. Advisory `target-coverage` 6/6 (100 %, no blind spot). La clôture `#print axioms` est mesurée par le gate au run PR CI |
+| `game_theory_lean` | `lean-social-choice.yml` | OUI — partiel (subtree, #12330 ; étendu ProgramGames 2026-09-10, PR B.3 #15221 follow-up) | GREEN sur les cibles câblées : SocialChoice.* (16 modules FR+EN, pinning `SocialChoice/CERTIFIED.txt`) + `Abstraction`/`Abstraction.Basic` + `ProgramGames.Basic`/`ProgramGames.Basic_en` (L1 noyau borné #15176/#15221) + `ProgramGames.Bounded`/`ProgramGames.Bounded_en` (module atterri **après** la rédaction du scope, #15395 — ajouté sur demande du digest de review #15379) : 0 sorry, 0 `native_decide` — grep FR/EN firsthand ; `fail-on-sorry: true`, companions épinglés par `test_workflow_targets_match_manifest`. **Hors cible délibérée** : `RepeatedGames.Folk` (stretch sorry #4880), racines agrégateurs (`SocialChoice.lean`, `ProgramGames.lean`, sans decls). Reste du lake (StableMarriage, CooperativeGames, RepeatedGames, Swaps) non ciblé — candidat aux tranches #11699 |
 | 15 autres lacs | workflows existants | **NON** | GREEN si câblés (sauf 3 borderline sur `Classical.choice` : `sudoku_lean`, `learning_theory_lean`, `decision_theory_lean`) |
 
 Le câblage du gate sur les lacs non-pilotes est un travail séparé qui sort du scope #8738 (chaque workflow lake est un livrable à part avec son `target-modules` adapté). Voir #11699 pour la roadmap tranche-par-tranche des 15 restants (mimo_lean = tranche 1 livrée par PR de cette PR).

scripts/tests/test_check_certified_sorry.py

@@ -178,7 +178,17 @@ def test_workflow_targets_match_manifest():
     raw = wf["jobs"]["proof-integrity"]["with"]["target-modules"]
     actual = {m.strip() for m in raw.split(",")}
     expected_set = set(expected)
-    allowed_companions = {"Abstraction", "Abstraction.Basic"}
+    # Companion targets are gated modules living OUTSIDE SocialChoice/ in the
+    # same lake. ProgramGames.Basic/_en joined via the B.3 wiring (#15221
+    # follow-up): same review status as Abstraction, pinned here so a future
+    # addition to target-modules is an explicit test change, never a silent
+    # drift. The root ProgramGames.lean is a docstring-only aggregator (no
+    # decls) and is deliberately NOT a target, same as the SocialChoice root.
+    allowed_companions = {
+        "Abstraction", "Abstraction.Basic",
+        "ProgramGames.Basic", "ProgramGames.Basic_en",
+        "ProgramGames.Bounded", "ProgramGames.Bounded_en",
+    }
     assert expected_set <= actual, (
         f"lean-social-choice.yml target-modules omitted entries from "
         f"SocialChoice/CERTIFIED.txt: workflow={sorted(actual)} "
@@ -191,10 +201,13 @@ def test_workflow_targets_match_manifest():
     required_paths = {
         "MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction.lean",
         "MyIA.AI.Notebooks/GameTheory/game_theory_lean/Abstraction/**.lean",
+        "MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames.lean",
+        "MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/**.lean",
     }
     triggers = wf.get("on", wf.get(True))
     for event in ("push", "pull_request"):
         actual_paths = set(triggers[event]["paths"])
         assert required_paths <= actual_paths, (
             f"lean-social-choice.yml {event} does not trigger for all "
-            f"Abstraction modules: missing={sorted(required_paths - actual_paths)}")
+            f"companion modules (Abstraction, ProgramGames): "
+            f"missing={sorted(required_paths - actual_paths)}")