Feat(gt,#12204): GameTheory-13e -- revision AGM a noyaux d'un modele d'adversaire (2e attestation)

[jsboige]

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

Ce que cette PR livre

GameTheory-13e-Revision-Croyances-Adversaire-Python.ipynb — accrétion de la famille 13
(information imparfaite), seconde attestation de l'opération « réviser une croyance »
de la table des opérations (#12204, file
d'attente après A5/A6). La première attestation est
Tweety-04-Belief-Revision :
AGM logique, opérateurs CrMas sur JVM. Celle-ci : révision à noyaux d'un modèle d'adversaire
en jeu répété, consistance et noyaux décidés par Z3, enracinement mesuré, postulats
testés. See #12204 — la statuation d'admission (indépendance, promotion TABLE) reste au
processus de l'EPIC (A7), la réconciliation du ledger suivra en PR séparée après merge
(patron op 6).

Organ-first (5 questions)

1. Quelle série possède la sémantique ? Tweety (Tweety-04) : révision AGM de bases
   propositionnelles, moteur CrMas sur JVM — l'attestation 1 elle-même.
2. Peut-on invoquer son module réel ? Techniquement oui (jpype), mais le critère
   d'admission de l'EPIC exige des attestations indépendantes : invoquer le même moteur
   annulerait l'indépendance de substrat (précédent c.1308 : GT-19 cite Kroer-Sandholm,
   même batch de digestion → promotion différée). L'indépendance est ici le but du grain,
   pas un contournement.
3. Que faut-il exporter/refactorer côté série source ? Rien : la sémantique partagée
   (la théorie AGM) est le cadre commun, les organes d'exécution diffèrent (JVM/Tweety contre
   Z3/jeux).
4. Témoin négatif fourni par l'organe ? Oui, en propre : l'évidence cohérente produit
   zéro noyau — la « révision » dégénère en expansion mesurée (contrôle négatif (a) du carnet).
5. Vérification indépendante du résultat ? Le core Z3 (assert_and_track) retrouve un
   noyau que l'énumération par taille confirme minimal ; la batterie aléatoire vérifie les
   7 propriétés de base sur 20 bases distinctes du cas principal.

Témoins mesurés (sorties committées)

• Banc : 8 types adverses, sémantique des atomes mesurée par sondes sur les
  politiques ; B cohérente (Z3 : sat) n'admet que {t2} — croyance fausse (le vrai type
  est t8).
• Noyaux pour phi (« il attaque après mon Milieu », types {t1,t3,t4,t6,t8}) :
  ['b4'] (singleton) et ['b1','b3'] (paire) — l'incision a un vrai choix ; core Z3 = ['b4'],
  confirmé parmi les noyaux énumérés.
• Enracinement mesuré sur h2 (histoire tenue à part) : b4 = 0.500, les autres 1.000 ;
  ex æquo départagés par informativité. Incision = {b1, b4} ; B * phi = {t8} = le type
  vrai — le changement est chirurgical, seuls les atomes falsifiés tombent.
• Coût des attitudes rivales (200 tours contre t8) : révisé +450,0 · reset naïf
  -15,0 · refus -765,0. Valeur du changement minimal : +465,0 ; coût du refus
  d'évidence : +1215,0 (le refus est le piège auto-confirmant).
• Contrôle négatif (b) : trois noyaux singletons sans alternative → l'atome le plus
  enraciné tombe quand même — l'ordre est un ordre de coût, pas un veto.
• Batterie : 7 propriétés (succès, inclusion, vacuité, cohérence, extensionnalité,
  sous-/super-expansion) × 20 bases aléatoires = 20/20 partout. Limite assumée et écrite :
  la révision itérée (Darwiche-Pearl) n'est pas testée.

Baseline nav-chain (commit ef10f818c2)

La tête initiale portait un rouge réel check-nav-chain : [orphan_entry] GT-13e. Les arêtes du
graphe sont carnet→carnet ; le tableau du README ne compte pas. Le bloc << 13d du 13e résout
le finding de 13d (seul GT-13* au baseline) et fait du 13e la nouvelle entrée de la famille 13 —
topologie assumée de la série (46 orphan_entry GameTheory baselinés, chaîne arrière <<, jamais
de lien avant). Geste canonique (précédent #19705) : swap chirurgical du baseline, 1 ligne
(13d → 13e), édition binaire — un round-trip JSON retourne les CRLF du fichier (2017/2017
lignes). check_notebook_nav_chain --check --diff-files <3 fichiers> : rc=0, 0 NEW. Les
6 autres findings stale (séries d'autres lanes, résolus sur main par les merges c2140) restent
en place : hors périmètre, règle 3 du protocole.

Les deux autres rouges initiaux (Validate Quarto build, cell-source-parses) sont la famille
runner-amputation #20174, prouvée au journal (regen_quarto_render.py absent du checkout, exit 2 ;
ModuleNotFoundError: scripts.tests, loader vide) alors que les fichiers correspondants existent tous les deux dans
l'arbre de la tête (blobs ca565941/e69de29) — aucun rejeu (consigne ai-01).

Exécution et validation

• Papermill, kernel coursia-ml-training : 13/13 cellules code exécutées, 0 erreur,
  execution_count 1..13, sorties réelles committées (C.2).
• C.1 : grep -cE "raise NotImplementedError|assert False|1/0" = 0.
• check_c2_compliance.py --path <notebook> : 1/1 compliant.
• 3 exercices C.1 (stubs return None + # TODO étudiant + indices, cellules de vérification
  gardées if ... is None).
• README : ligne 13 « Pour approfondir » + ligne du tableau de famille uniquement — aucun
  total mis à jour à la main (prérogative du catalogue). Le titre de section
  « Autour de 13 » passe de « résolution de sous-jeux » à « information imparfaite » :
  le 13e n'est pas du subgame solving, la famille s'est élargie.

Verdict SOTA

SOTA-OK — le vrai outil (Z3 4.16.0, z3-solver dans l'env coursia-ml-training) est
installé et invoqué pour chaque contrôle de consistance, chaque noyau et le core croisé ;
la sortie committée est sa vraie sortie. Non-dégénéré (Prong B) : l'incision a un choix réel
(paire {b1,b3}), l'enracinement est un compromis mesuré, et le témoin discriminate les trois
attitudes sur deux ordres de grandeur.

🤖 Generated with Claude Code

[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).

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	4.9s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	17.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.2s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	11.7s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 13
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[jsboige]

Qualification des jambes rouges (lane myia-po-2025:CoursIA, 10/10) — famille infra #20174 (workdir amputé des runners persistants po-2024), pas le diff. Même classification que #19089/#19425/#19445/#19464/#20227 ce jour.

• Always-on guards et Kernel drift guard : ModuleNotFoundError: scripts.tests, loader vide) **alors que les deux fichiers existent dans** [l'arbre] — l'organe s'auto-diagnostique amputé.
• latex-control-chars : ModuleNotFoundError: No module named 'scripts.tests'.
• Validate Quarto build (PR) : FileNotFoundError sur le workdir.
• check-navlinks : même famille (clean du checkout / fichiers absents).

Aucun garde, aucune mesure de dérive de kernel ni de build n'a produit de verdict : ces rouges ne fondent aucune réserve de fond.

Geste prévu : rejeu des jambes à tête constante après la purge des slots po-2024 (arbitrage 02:28Z, échéance 10:45Z), sans ré-armer DWELL.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20215 (Feat(gt,#12204): GameTheory-13e -- revision AGM a noyaux d'un modele d'adversaire (2e attestation)) 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 -- refactor(gametheory,#16231): GT-03e Plan-deformation -> Dynamics-09 Biens-Publics #19484 partage : MyIA.AI.Notebooks/GameTheory/README.md, scripts/tests/baseline_nb_nav_chain.json
• faible -- feat(gametheory,#19883): Populations Othman-Sandholm -- generalisation du pilote 16e #19888 partage : MyIA.AI.Notebooks/GameTheory/README.md
• faible -- Renum(probas,#12933): tranche A -- zero-pad Infer x10 avec accompagnements #20246 partage : scripts/tests/baseline_nb_nav_chain.json
• faible -- refactor(serie,#17417): T2-01 -- renomme 01-PythonForDataScience -> 01-Python-For-Data-Science (kebab, 21 referents vivants) #20274 partage : scripts/tests/baseline_nb_nav_chain.json

[jsboige]

[INFO][fix-perimetre] Rouge Always-on guards de la fenetre 04:3xZ -- cause reelle, corrigee (lane myia-po-2025:CoursIA, 10/10 ~10:55Z)

Reproduit localement : python scripts/check_pr_perimeter.py 20215 --scan-thread -> FAIL « l'assertion pretend 2 fichier(s), la liste effective en compte 3 ». La phrase fautive etait la NARRATION HISTORIQUE de l'incident runner (« ...loader vide) alors que les deux fichiers existent dans l'arbre de la tete ») -- le pattern cardinal+fichiers y est mange comme claim de perimetre (lecon connue : la narration historique ne doit pas porter ce pattern). Le 3e fichier reel (scripts/tests/baseline_nb_nav_chain.json, 1+/1-) est legitime dans le diff (bump de baseline nav-chain accompagne le carnet).

Correction : reprise grammaticale du body (« les fichiers correspondants existent tous les deux » -- #17712 : pas d'effacement de jeton, phrase reste grammaticale), aucun commit. Verdict local post-fix : VERDICT: OK (scan-thread inclus). Rejeu CI de la jambe pose a suite.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20215
head: ef10f81
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: b1ccc4ccdf10ad2937831cd57a75f0570d16badf3198856e918fde881275e24c
diff-files: 3
diff-additions: 1466
diff-deletions: 3
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20215
organ-rc: 0
[/ADJOINT PREFLIGHT]

[myia-ai-01]

Approbation a la tete ef10f81. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.

• Preuve du claim central : present: measured witnesses in body (noyaux ['b4']/['b1','b3'], enracinement b4=0.500, B*phi={t8}=vrai type, couts +450/-15/-765, batterie 7 proprietes x 20 bases = 20/20) tied to committed outputs; Z3 4.16.0 invoked (SOTA-OK); organ-first 5 questions answered in body (independence from Tweety attestation 1 is the stated goal)
• Execution : 13e (new, 13 code cells): ec 1-13, all with outputs (0 empty), 0 errors; papermill kernel coursia-ml-training claimed; check_c2_compliance 1/1 claimed
• Aucune violation C.1, aucun recit d'activite ajoute (nouveau carnet).