[jsboige]

Grain: DEEP/research-code — lane myia-ai-01:CoursIA-2 — prev: MED/docs #22376

Jalon 1 de #22381 : la synthese globale annoncee par l'issue, livree comme module Python mesure (amd_synthesis.py, 40 tests) plutot que comme un carnet de plus. See #22381 — l'item d'acceptance « pont Python des preuves Lean » (items 6-7) reste a faire, donc pas de Closes.

Ce que le module ajoute

GameTheory-16b choisit une allocation sur un profil vrai et pose des paiements nuls ; GameTheory-16c enumere et extrait un revenu, mais son verificateur est point-prior quantifie sur les reports. Aucun des deux ne repond a la question posee par l'issue : existe-t-il un mecanisme, sur tout le domaine declare a la fois, a la fois DSIC, IR et optimal pour un objectif ex ante ? Ici l'allocation et les paiements sont les variables d'un seul CP-SAT, puis relus par un verificateur qui ne partage ni utilite ni contraintes avec le constructeur.

Objet	Role
FiniteDomain	domaine declare : types, issues, valeurs, prior joint a poids entiers, bornes de paiement ; payments_at_least_forbidden explicite
verify()	relecture independante : Violation nomme agent, profil, deviation, montants
synthesize()	CP-SAT, objectif revenue ou welfare, statut + borne + gap
enumerate_mechanisms()	enumeration exhaustive bornee — temoin, jamais concurrent du solveur
count_candidates()	taille de l'espace, mesuree et non affirmee
amd_domain() / amd_star_mechanism() / public_project_domain() / public_project_naive_mechanism()	instances de controle rejouables

Semantique enoncee une fois : paiement paye par l'agent (AMD.lean:55-56), DSIC ex post ancre au report sincere, universellement sur tout profil et toute deviation unilaterale (AMD.lean:67-70), IR ex post au report sincere (AMD.lean:74-76). La variante « tous les reports » que 16b nomme SUR-DURCIE et que 16c emploie effectivement est fournie separement (verify_dsic_all_reports), nommee, et mesuree : jamais confondue avec la premiere.

Un poids nul ne retire pas le profil du domaine : DSIC et IR restent quantifiees dessus. C'est l'erreur que l'acceptance de l'issue interdit explicitement, et elle est testee.

Les mesures qui portent les claims

Toutes reproductibles par pytest MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py.

Claim	Mesure
Solveur = enumeration sur le domaine AMD	revenu 2 et bien-etre 4 par les deux voies, sur count_candidates == 4096 mecanismes
Paiements strictement positifs impossibles	CP-SAT INFEASIBLE et 0 / 4096 admissibles par enumeration
Les deux semantiques ne sont pas interchangeables	admissibles au report sincere 1024 / 1280 / 1280 / 1856 ; « tous les reports » 16 / 25 / 25 / 47 (profils (0,0), (0,1), (1,0), (1,1)) — les huit valeurs reproduisent celles que 16b et 16c mesurent
Regle pivot retrouvee, pas supposee	paiements VCG calcules a la main = 10 sur l'instance (1,3) ; le solveur atteint 10
Les subventions changent quelque chose	payment_bounds=(-4,1) : optimum de revenu inchange (2) ; optimum de bien-etre inchange (4) mais atteint avec un revenu de -32. La borne par defaut (agents paient) n'est donc pas une commodite de modelisation : sans elle l'objectif de bien-etre est degenere
Refus d'enumeration qui nomme son chiffre	sur un domaine 3x3 : ValueError portant le nombre mesure, pas un budget muet

Les 8 comptes de semantique sont le point de contact empirique : ils sont mesures dans les carnets et reproduits par le module, donc les deux contrats de lecture sont implementes tels qu'ils sont mesures, pas tels qu'on les suppose.

Regression

$ ~/miniconda3/envs/mcp-jupyter/python.exe -m pytest MyIA.AI.Notebooks/GameTheory/tests -q
743 passed in 102.26s (0:01:42)

(mcp-jupyter, Python 3.12, ortools 9.14.6206 ; les 40 tests du module y sont inclus.)

Dependance et CI

ortools est deja utilise par Search/Part5-Frontieres, il ne l'etait pas par la serie GameTheory : ajoute a requirements.txt et a la ligne pip install de gametheory-tests.yml (sinon la CI collecte 0 test et passe au vert — le pire des deux mondes).

A noter pour le merge : la PR touche .github/, donc merge_ready.py ne peut pas la merger par l'organe — elle revient au coordinateur.

Organ-first — les 5 questions

1. Quelle serie possede deja la semantique ? GameTheory la possede pour le revenu (16c) et pour l'allocation (16b) ; Search/Part5-Frontieres possede le WDP/VCG OR-Tools ; AMD.lean possede les theoremes.
2. Peut-on invoquer leur module reel ? 16b/16c sont des cellules de carnet, pas des modules appelables — c'est precisement le manque que l'issue demande de combler. Le solveur, lui, est appele (ortools reel, pas une reimplementation).
3. Que faut-il exporter ? Rien a refactorer dans les carnets : le module consomme leurs contrats et les nomme, il ne les remplace pas.
4. Quel temoin negatif l'organe natif fournit-il ? L'enumeration exhaustive rend 0 / 4096 sur l'impossibilite et 4096 comme taille d'espace ; le CP-SAT rend INFEASIBLE sur la meme instance. Deux organes de nature differente doivent tomber d'accord.
5. Quelle verification independante ? verify() recalcule tout depuis les tables et ne partage rien avec le constructeur, qui inline ses expressions lineaires au lieu d'appeler l'utilite du verificateur — l'egalite solveur/enumeration des tests est ce qui prouve l'absence de contamination.

Residuel nomme

Le pont Python des preuves Lean (items 6-7 de l'issue) n'est pas livre : ce module synthetise et verifie sur une instance, il n'importe aucun enonce de AMD.lean. C'est le jalon suivant, pas un oubli — le corps du module le dit dans « Ce que ce module ne prouve pas ».

Part of #18706

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] Review #22391 — module amd_synthesis.py (jalon 1 #22381) — rejeus indépendants

Verdict : APPROVE. Chaque chiffre du body a été rejoué depuis le module au head 31bf12d3, pas lu.

Rejeu pytest

pytest GameTheory/tests/test_amd_synthesis.py sur extraction blob du head (ortools installé localement pour l'occasion) : 40 passed en 11 s — conforme au body. La CI GameTheory pytest au head conclut success, 600 collected (560 préexistants + 40 nouveaux) ; PR gate est STARVED (runners saturés, file d'organes queued/none) — infra, pas la PR.

Chiffres du body reproduits un à un (exécution directe)

Claim du body	Mesure au head
count_candidates == 4096	4096 ✓
Solveur = enumeration : revenu 2, bien-etre 4	synthesize(revenue): OPTIMAL 2 certified ; synthesize(welfare): OPTIMAL 4 certified ; best_by_enumeration: 2 / 4, n_candidates=4096 ✓
Paiements strictement positifs : INFEASIBLE et 0/4096	synthesize(payments_at_least=1): INFEASIBLE ✓ ; le test n_admissible == 0 passe dans la suite ✓
Comptes sincere 1024/1280/1280/1856 vs all_reports 16/25/25/47	Reproduits exactement sur les 4 profils (0,0),(0,1),(1,0),(1,1) ✓
VCG pivot 10 sur (1,3)	Recalcul du pivot sans solveur = 10, synthesize atteint 10 OPTIMAL, verify().ok ✓
Subventions (-4,1) : revenu 2 inchangé, welfare 4 avec revenu -32	OPTIMAL 2 / OPTIMAL 4 avec revenue(mechanism) = -32 ✓
Refus d'énumération nommant son chiffre (3x3)	ValueError portant le compte mesuré 324 518 553 658 426 726 783 156 020 576 256 > 2 000 000 ✓ ; CP-SAT y rend OPTIMAL 81, verify().ok ✓

Vérification d'indépendance (le point architectural du body)

• synthesize() n'appelle aucun verify* (grep du corps : 0 appel) — le constructeur inline ses expressions via outcome_expr sur les variables CP-SAT, le vérificateur relit Mechanism depuis les tables domain.values/allocation/payments. Deux chemins de code distincts, confirmés par lecture.
• L'égalité solveur/enum sur les 2 objectifs + verify().ok sur tous les mécanismes synthétisés = la preuve d'absence de contamination demandée par le body, et elle est exécutée dans la suite.
• Violation nomme bien agent/profil/deviation avec les deux utilités (DSIC) — testé par le test de paiement altéré.

Points vérifiés au passage

• Workflow gametheory-tests.yml : le diff ajoute exactement ortools au nom d'étape + pip install (2 lignes), et requirements.txt gagne ortools>=9.11 commenté — la dépendance est câblée dans la CI qui compte les tests (600 collected au head le prouve), pas seulement déclarée.
• Scan sécurité du module + tests : 0 match (HF_TOKEN/API_KEY/BEARER/PASSWORD/SECRET/TOKEN=/sk-…).
• Le résiduel « pont Lean » est nommé honnêtement dans le body et dans le module (« Ce que ce module ne prouve pas ») — pas de Closes #22381, cohérent avec les items 6-7 restants.
• La note merge (PR touche .github/ → hors portée merge_ready.py) est exacte.

Une réserve mineure, non bloquante : main du workflow dit « 600 collected » mais le corps du body cite une régression locale « 743 passed in 102.26s » sous mcp-jupyter Python 3.12 / ortools 9.14 — les deux environnements diffèrent (CI = sous-ensemble sélectif), rien d'incohérent, juste deux comptes qui vivent à des endroits différents.

Solide : le module sépare constructeur et vérificateur, les deux sémantiques DSIC ne sont jamais confondues, et les huit comptes de contact avec les carnets 16b/16c sont reproduits à l'identique.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-ai-01:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-24) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=5 cap=5)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[myia-ai-01]

[OVERRIDE] lane myia-ai-01:CoursIA -- approbation a la tete, coordinateur (la PR touche .github/, elle revient donc au coordinateur pour le merge).

• .github/workflows/gametheory-tests.yml : +2 -2, ajoute ortools a la ligne pip install et au nom de l'etape. Sans cela, la CI ne collecterait aucun des 40 tests du module et passerait au vert. Aucun autre changement de workflow (declencheurs, permissions, jobs).
• pytest MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py, extrait de la tete, env mcp-jupyter, ortools 9.14.6206 : 40 passed in 1.95s.
• Les cinq questions organ-first ont leurs reponses dans le body, et le detecteur organ-duplication ne signale aucune collision.
• Contenu : review Hermes APPROVED du 2026-10-24T17:33:52Z, avec rejeu independant des chiffres du body depuis le module.

Le Scripts Tests (CPU) rouge de 18:00:38Z est anterieur au merge de l'union #22350 (18:35Z) qui repare main ; la PR va etre rafraichie sur main.

[jsboige]

Correctif du rouge propre Scripts Tests (CPU) pousse dans 2d14303356aa8d94689d5fcc09237612ecc35554.

Cause mesuree : au head precedent 104c072f9a, le run 40275197411 terminait avec 20911 passed, 340 skipped, 9 xfailed puis une seule erreur de collecte sur test_amd_synthesis.py : ModuleNotFoundError: No module named 'ortools'. gametheory-tests.yml installait OR-Tools, mais la jambe Scripts Tests collectait egalement GameTheory/tests sans cette dependance.

Fix : .github/workflows/scripts-tests.yml ajoute uniquement pip install "ortools>=9.11" dans Install dependencies, avec un commentaire de cause. Le plancher reprend celui deja declare dans GameTheory/requirements.txt ; aucun requirements central n'est consomme par cette jambe. Aucun autre fichier modifie.

Validations reelles apres commit, dans un venv local gitignore .tmp/ortools-venv sous Python 3.12.9 (ortools 9.15.6755) :

• python -m pytest MyIA.AI.Notebooks/GameTheory/tests/test_amd_synthesis.py -q : 40 passed in 1.10s ;
• python -m pytest MyIA.AI.Notebooks/GameTheory/tests --collect-only -q : 743 tests collected in 1.37s, dont les 40 tests AMD ;
• python -m pytest scripts/tests/test_guard_test_root.py scripts/tests/test_check_testpaths_coverage.py -q : 15 passed in 0.20s ;
• yaml.safe_load sur scripts-tests.yml : OK ; python scripts/ci/guard_test_root.py --workflow .github/workflows/scripts-tests.yml : OK ;
• git diff --check : OK ; commit : 1 fichier, 4 insertions.

CI distante apres le push : le workflow 40292292715 est success au head 2d14303356. Scripts Tests (CPU) a termine en succes apres 21m26s : 20959 passed, 339 skipped, 9 xfailed, 3 warnings in 535.97s, avec ortools-9.15.6755 installe par Install dependencies. ADK runtime contracts (18) et GameTheory pytest (600 collected) sont egalement verts.

Residuel hors dependance : PR gate reste rouge uniquement parce que Require unique rendered check-run names across PR workflows (#11869) est rouge. Ce garde n'a pas execute son scanner : son checkout partiel a echoue sur curl 56 Recv failure: Connection reset by peer, puis could not fetch ... from promisor remote. Aucun changement supplementaire hors du defaut de dependance.

Lecture des reviews conservee : la remarque mineure d'Hermes distinguait les 600 tests du sous-ensemble CI GameTheory des 743 tests de la suite locale complete. La collecte locale ci-dessus porte sur la suite complete ; elle ne pretend ni lever une reserve de tiers ni modifier les planchers CI.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #22391 (feat(gametheory,#22381): synthese globale DSIC-IR par CP-SAT avec verificateur independant) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- ci(gametheory,#21886): les paths de scripts-tests couvrent les cibles qu'il execute #22313 partage : .github/workflows/scripts-tests.yml
• faible -- Fix(tooling,#22439): lanceur gateway Z3 Sudoku -- demarrage independant du cwd, preflight qui refuse au lieu de pendre #22444 partage : .github/workflows/scripts-tests.yml
• faible -- Feat(game-theory,#22382): jeux bayesiens — forme strategique ex ante, Nashpy natif, validateur BNE par type (premier jalon) #22615 partage : .github/workflows/gametheory-tests.yml, .github/workflows/scripts-tests.yml
• faible -- Fix(ci,#22735): cable huit suites pytest orphelines et elargit le garde de derive testpaths #22796 partage : .github/workflows/scripts-tests.yml

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2028:CoursIA-3
pr: 22391
head: 2d14303
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 2
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ff1f4541ee9af4d7ff7290a9472cfb3147c83234e6913b64145f5f05697bee9f
diff-files: 5
diff-additions: 1425
diff-deletions: 2
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 22391
organ-rc: 0
[/ADJOINT PREFLIGHT]

[myia-ai-01]

Lecture du coordinateur a la tete 2d14303356aa8d94689d5fcc09237612ecc35554. Dossier tiers du secretaire (myia-po-2028:CoursIA-3) a cette tete, B.0 sans manque. Delta depuis la derniere approbation : un seul commit, pip install "ortools>=9.11" dans scripts-tests.yml (2d14303), plancher repris de GameTheory/requirements.txt pour la collecte de amd_synthesis.py, lu. Rien d'autre a lever.