Skip to content

Docs(gametheory,#22683): Dynamics-04b (ex GT-06k) hors chronologie de livraison #24192

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 2 commits into from
Nov 3, 2026
Merged

Docs(gametheory,#22683): Dynamics-04b (ex GT-06k) hors chronologie de livraison #24192

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0799124
Docs(gametheory,#22683): Dynamics-04b (ex GT-06k) hors chronologie de…
jsboige Nov 2, 2026
089ea09
Docs(ledger,#14442): cloture du residu « carnets contendus » du sweep…
jsboige Nov 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions MyIA.AI.Notebooks/GameTheory/Dynamics/Dynamics-04b-FairBot-Loeb-Lean.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
"\n",
"**Navigation** : [<< 06e-OpenSource](Dynamics-04-Open-Source-Game-Theory-Python.ipynb) | [Index](../README.md) | [compagnon L1](Dynamics-05-Agents-Bornes-Lean.ipynb) | [06f-AgentsBornés >>](Dynamics-05-Agents-Bornes-Python.ipynb)\n",
"\n",
"Ce carnet est le **compagnon natif** du module [`ProgramGames.FairBot`](../game_theory_lean/ProgramGames/FairBot.lean) du lake [`game_theory_lean`](../game_theory_lean/README.md) — le niveau **L2** de l'équilibre en programmes de l'EPIC #15062 « Math for AI Safety ». Il câble le consommateur pédagogique qui manquait au module ([issue #20379](https://github.com/jsboige/CoursIA/issues/20379)).\n",
"Ce carnet est le **compagnon natif** du module [`ProgramGames.FairBot`](../game_theory_lean/ProgramGames/FairBot.lean) du lake [`game_theory_lean`](../game_theory_lean/README.md) — le niveau **L2** de l'équilibre en programmes de l'EPIC #15062 « Math for AI Safety ». Il câble le consommateur pédagogique qui manquait au module.\n",
"\n",
"Trois voisins le situent :\n",
"\n",
Expand All @@ -45,7 +45,7 @@
"\n",
"**Fait** : charger `ProgramGames.FairBot`, rendre chacun des théorèmes-phare par le noyau `lean4-wsl` (`#check` + `#print axioms` — aucune alternative `sorry`, aucun axiome au-delà des trois standard), rappeler la faille L1 (`ProgramGames.Basic`), et faire tourner un duel concret sur une **instance-témoin pédagogique** explicitement étiquetée.\n",
"\n",
"**Ne fait pas** : dériver le théorème de Löb. Dans l'architecture du module, Löb est un **champ postulé de l'interface** `ModalProvability` — une hypothèse explicite que toute instance doit fournir, dont l'indépendance est mesurée dans le module (`bump_loeb_fails`) et la non-vacuité attestée par le témoin externe `FormalLogic.GLBridge.loeb_schema` (PR #15923). Le carnet respecte cette architecture : il ne définit aucune instance prétendant être « la » prouvabilité — uniquement un témoin trivial dont le rôle est pédagogique (exhiber ce que l'hypothèse de cohérence exclut)."
"**Ne fait pas** : dériver le théorème de Löb. Dans l'architecture du module, Löb est un **champ postulé de l'interface** `ModalProvability` — une hypothèse explicite que toute instance doit fournir, dont l'indépendance est mesurée dans le module (`bump_loeb_fails`) et la non-vacuité attestée par le témoin externe `FormalLogic.GLBridge.loeb_schema`. Le carnet respecte cette architecture : il ne définit aucune instance prétendant être « la » prouvabilité — uniquement un témoin trivial dont le rôle est pédagogique (exhiber ce que l'hypothèse de cohérence exclut)."
]
},
{
Expand Down Expand Up @@ -1781,7 +1781,7 @@
"| `fairBot_vs_coopBot` / `fairBot_vs_defectBot` | la table pédagogique, hypothèses apparentes |\n",
"| `coopToy` (instance-témoin) | la solidité de la coopération est celle du champ Löb de l'instance |\n",
"\n",
"**La limite honnête, répétée** : Löb est postulé au champ de l'interface — ce carnet ne le dérive pas, et son instance-témoin ne prétend pas être une prouvabilité réelle. La chaîne de confiance traverse trois livrables : l'indépendance mesurée ici (`bump_loeb_fails`), la non-vacuité attestée par le témoin GL noyau-vérifié (L3, lake `formal_logic_lean`, PR #15923), et la dérivation de Barasz et al. (2014) formalisée dans le module.\n",
"**La limite honnête, répétée** : Löb est postulé au champ de l'interface — ce carnet ne le dérive pas, et son instance-témoin ne prétend pas être une prouvabilité réelle. La chaîne de confiance traverse trois livrables : l'indépendance mesurée ici (`bump_loeb_fails`), la non-vacuité attestée par le témoin GL noyau-vérifié (L3, lake `formal_logic_lean`), et la dérivation de Barasz et al. (2014) formalisée dans le module.\n",
"\n",
"**Ponts** : les `_toy` de [06e](Dynamics-04-Open-Source-Game-Theory-Python.ipynb) (heuristiques déclarées), la limite explicite de [06f-Lean](Dynamics-05-Agents-Bornes-Lean.ipynb) (L1 s'arrête avant Löb — ce carnet la franchit), le pont GL de [Lean-34b](../../SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb) (L3, logique de la prouvabilité).\n",
"\n",
Expand All @@ -1791,7 +1791,7 @@
"- LaVictor (2015), « Robust cooperation in the Prisoner's Dilemma: program equilibrium via provability logic », arXiv:1401.5577 appendices.\n",
"- Critch (2016), « Parametric Bounded Löb's Theorem and Robust Cooperation of Bounded Agents », arXiv:1602.04184.\n",
"\n",
"Carnet livré par l'issue #20379 — le module `ProgramGames.FairBot` a désormais son consommateur pédagogique."
"Le module `ProgramGames.FairBot` a désormais son consommateur pédagogique."
]
}
],
Expand Down
45 changes: 38 additions & 7 deletions docs/ledgers/14442-chronology-sweep-2026-10-26.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ la source et les résultats. Ils forment le backlog de tranches de #14442 :
| Carnet | Cellule(s) | Récit de livraison à retirer |
|---|---|---|
| **GT-20** (livré par la PR associée) | 36 | « l'EPIC #12205 prescrit », « GT-3b (#12213) », « GT-3b livré (#12253) », « GOL-06 … (#12286) » |
| GT-06k FairBot-Loeb | 0, 1, 34 | « Carnet livré par l'issue #20379 », « PR #15923 » |
| GT-06k FairBot-Loeb — désormais `GameTheory/Dynamics/Dynamics-04b-FairBot-Loeb-Lean.ipynb` | 0, 1, 34 | « Carnet livré par l'issue #20379 », « PR #15923 » |
| GT-13d Optimistic-CFR | 1, 16 | « livré sur main par #13350, commit … », « (socle #13350) », « Voir aussi : #13291 / #13290 / #13350 » |
| GT-06j Bounded-Proofs | 31 | « DISPATCH ai-01, EPIC #15062, PR #15175, MERGED 2026-09-09… » |
| GT-03d Le-Joueur-LLM | 5, 25 | « ai-01 dans la review PR #12295 », « Substrat EPITA (#12254) » |
Expand All @@ -108,10 +108,10 @@ côté. Les lignes marquées **[nouveau]** n'étaient pas dans le tableau de tra
| 3 | GT-20 | 36 | « chambres / murs / make_tie : GT-3b livré (#12253) » | CHRONOLOGIE | traité — #22658 |
| 4 | GT-20 | 36 | « GOL-06 translateur Life (#12286) » | CHRONOLOGIE | traité — #22658 |
| 5 | GT-06k FairBot-Loeb | 0 | « le niveau **L2** de l'équilibre en programmes de l'**EPIC #15062** « Math for AI Safety » » | **PROVENANCE_UTILE** | **conserver** **[nouveau]** |
| 6 | GT-06k | 0 | « le consommateur pédagogique qui manquait au module ([issue #20379](…)) » | CHRONOLOGIE | retirer le n°, garder la phrase **[nouveau]** |
| 7 | GT-06k | 1 | « le témoin externe `FormalLogic.GLBridge.loeb_schema` (PR #15923) » | CHRONOLOGIE | retirer le n° — l'artefact est déjà nommé |
| 8 | GT-06k | 34 | « le témoin GL noyau-vérifié (L3, lake `formal_logic_lean`, PR #15923) » | CHRONOLOGIE | retirer le n° |
| 9 | GT-06k | 34 | « Carnet livré par l'issue #20379 — le module `ProgramGames.FairBot` a désormais son consommateur pédagogique. » | CHRONOLOGIE | retirer le récit de livraison, **garder** la seconde phrase |
| 6 | GT-06k | 0 | « le consommateur pédagogique qui manquait au module ([issue #20379](…)) » | CHRONOLOGIE | traité — #24192 (le lien retiré, la phrase gardée) **[nouveau]** |
| 7 | GT-06k | 1 | « le témoin externe `FormalLogic.GLBridge.loeb_schema` (PR #15923) » | CHRONOLOGIE | traité — #24192 (le n° retiré, l'artefact déjà nommé) |
| 8 | GT-06k | 34 | « le témoin GL noyau-vérifié (L3, lake `formal_logic_lean`, PR #15923) » | CHRONOLOGIE | traité — #24192 (le n° retiré) |
| 9 | GT-06k | 34 | « Carnet livré par l'issue #20379 — le module `ProgramGames.FairBot` a désormais son consommateur pédagogique. » | CHRONOLOGIE | traité — #24192 (le récit de livraison retiré, la seconde phrase gardée) |
| 10 | GT-13d Optimistic-CFR | 1 | « `Info-CFR-Python.ipynb` (livré sur main par `#13350`, commit `0…` » | CHRONOLOGIE | traité — #22874 |
| 11 | GT-06j Bounded-Proofs | 31 | « Issue #15335 (DISPATCH ai-01) » | CHRONOLOGIE | traité — #22661 |
| 12 | GT-06j | 31 | « (PR #15175, MERGED 2026-09-09T03:59:10Z) » | CHRONOLOGIE | traité — #22661 |
Expand Down Expand Up @@ -193,9 +193,34 @@ Rien n'est laissé en silence : ce qui n'est pas traité est **nommé** ici.
| Résidu | Où | Pourquoi pas traité | Suite |
|---|---|---|---|
| Commentaire de tête `Fix #17882` | GT-13d, **cellule 2 (code)** | L'organe ne parcourt que les **cellules markdown** ; le corriger suppose d'éditer une cellule de code, donc une **re-exécution complète** du carnet (C.2) — carnet sous OpenSpiel, sorties `tqdm` bridées par un ratchet de volume | Tranche code, à instruire à la prochaine re-exécution du carnet |
| Renvois de GT-06k, GT-09b, GT-03d | cellules 0 / 1 / 34, 24, 5 / 25 | Carnets **contendus** par des PRs ouvertes d'autres lanes (#20442 sur GT-06k et GT-09b, #22177 et #22193 sur GT-09b, #22351 sur GT-03d) | Reprise quand ces PRs sont mergées |
| Renvois de GT-06k, GT-09b, GT-03d | cellules 0 / 1 / 34, 24, 5 / 25 | **Levée le 2026-11-02** — voir la mesure de clôture ci-dessous | Traités : GT-06k par #24192, GT-09b par #23254, GT-03d par #22177/#20442 |
| GT-16g | cellule 0 | Issue de suivi dédiée **#22682** | Portée par #22682 |

### Mesure de clôture du résidu « carnets contendus » (2026-11-02)

La barrière inscrite dans ce ledger était « reprise quand ces PRs sont mergées ». Elles le
sont toutes, mesuré à la source plutôt que supposé : **#20442** (2026-10-31T22:23:17Z),
**#22177** (2026-10-29T00:32:18Z), **#22193** (2026-10-29T05:10:12Z), **#22351**
(2026-11-01T04:32:04Z).

Organe rejoué sur les quatre carnets à l'état de `main` (`ba2199363`), plus deux contrôles
de contenu pour distinguer « dé-chronologisé » de « contenu disparu » :

| Carnet (chemin actuel) | Ex-nom | Marqueurs | Contrôle de contenu |
|---|---|---|---|
| `Dynamics/Dynamics-04b-FairBot-Loeb-Lean.ipynb` | GT-06k | **5 → 1** (la provenance `EPIC #15062`) | traité par **#24192** |
| `GameTheory-09b-Commitment-Stackelberg-Python.ipynb` | GT-09b | 0 | « en cours de livraison » présent, `#12212` absent → n° retiré, phrase gardée |
| `Dynamics/Dynamics-10-Joueur-LLM-Python.ipynb` | GT-03d | 0 | « Substrat EPITA » présent, `#12254` / `12295` absents → n° retirés, phrase gardée |
| `SocialChoice/10-Manipulation-Strategique-MultiWinner.ipynb` | SocialChoice/10 | 0 | `#21632` absent, « encore ouverte » absent → renvoi retiré |

Les deux colonnes de droite comptent : un carnet à zéro marqueur peut l'être parce qu'on a
**supprimé la phrase**, ce qui serait une régression de contenu. Ici la substance est
présente dans les trois cas, seuls les numéros sont partis — c'est le geste prescrit.

**Deux carnets ont été renumérotés entre-temps** (GT-06k → `Dynamics-04b`, GT-03d →
`Dynamics-10`) : les chemins de ce ledger se lisent donc sur le nom du carnet, pas sur son
numéro d'origine.

## Portée de la PR associée

- **livré** : l'organe de détection (+ la correction de son patron `pr_paren`) + ce sweep
Expand All @@ -209,9 +234,15 @@ Rien n'est laissé en silence : ce qui n'est pas traité est **nommé** ici.
révélée par la correction du patron, dans l'issue de suivi nommée #22682) et le défaut 2
de l'issue (déplacer l'annexe hors de GT-04). Les autres carnets du tableau sont des
**tranches de suivi** de #14442, chacune dans sa PR : #22661 (GT-06j), #22664 (GT-13c),
#22665 (GT-11b), #22666 (SocialChoice/10), #22874 (GT-13d). L'issue reste ouverte ; la PR est
#22665 (GT-11b), #22666 (SocialChoice/10), #22874 (GT-13d), #23254 (GT-09b), #24192
(GT-06k, désormais `Dynamics-04b`). L'issue reste ouverte ; la PR est
`See #14442`.

**État des tranches au 2026-11-02** : sur les neuf carnets du tableau de backlog, **huit
sont mesurés à 0 marqueur de la classe CHRONOLOGIE** ; le seul marqueur restant est le
renvoi de provenance `EPIC #15062` de `Dynamics-04b`, délibérément conservé. Le résidu
réel de ce sweep n'est plus GameTheory : c'est **GT-16g** (issue #22682).

## Reprise

```bash
Expand Down
Loading