Skip to content

feat(gametheory,#14450): oracles réflexifs — tranches 2..N, restriction finie vérifiée, CDT/EDT, frontière #16265

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
jsboige merged 2 commits into from
Sep 15, 2026
Merged

feat(gametheory,#14450): oracles réflexifs — tranches 2..N, restriction finie vérifiée, CDT/EDT, frontière #16265

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
92f7bad
feat(gametheory,#14450): oracles reflexifs — restriction finie verifi…
jsboige Sep 15, 2026
78c6596
fix(gametheory,#14450): restore skeleton canonical statements + twin …
jsboige Sep 15, 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
3 changes: 2 additions & 1 deletion MyIA.AI.Notebooks/GameTheory/GameTheory-04-NashEquilibrium.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1751,7 +1751,8 @@
"tags": []
},
"source": [
"> **Lien avec la formalisation Lean** : Le théorème d'existence de Nash est formalisé dans le notebook compagnon [GT-4b-Lean-NashExistence](GameTheory-04b-Lean-NashExistence.ipynb) (kernel Lean 4). On y trouve la construction du simplexe standard (`Simplex`), le produit de simplexes (`SimplexProduct`), la structure `FiniteGame`, les profils de stratégies mixtes, le gain espéré et la définition formelle de l'équilibre de Nash — le tout sans import Mathlib. Le théorème de Brouwer (point fixe sur le simplexe) y est axiomatisé comme fondement de la preuve d'existence. Le notebook Python [GT-4c-NashExistence-Python](GameTheory-04c-NashExistence-Python.ipynb) illustre numériquement ces mêmes concepts."
"> **Lien avec la formalisation Lean** : Le théorème d'existence de Nash est formalisé dans le notebook compagnon [GT-4b-Lean-NashExistence](GameTheory-04b-Lean-NashExistence.ipynb) (kernel Lean 4). On y trouve la construction du simplexe standard (`Simplex`), le produit de simplexes (`SimplexProduct`), la structure `FiniteGame`, les profils de stratégies mixtes, le gain espéré et la définition formelle de l'équilibre de Nash — le tout sans import Mathlib. Le théorème de Brouwer (point fixe sur le simplexe) y est axiomatisé comme fondement de la preuve d'existence. Le notebook Python [GT-4c-NashExistence-Python](GameTheory-04c-NashExistence-Python.ipynb) illustre numériquement ces mêmes concepts.\n",
"> **Prolongement computationnel** : [GameTheory-04e — Oracles réflexifs](GameTheory-04e-Reflective-Oracles.ipynb) — auto-référence, décision causale (CDT/EDT) et restriction finie vérifiée (#14450)."
]
},
{
Expand Down
5 changes: 3 additions & 2 deletions MyIA.AI.Notebooks/GameTheory/GameTheory-04b-Lean-NashExistence.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4049,7 +4049,8 @@
"\n",
"***\n",
"\n",
"**Navigation** : [<< 4-NashEquilibrium (track principal)](GameTheory-04-NashEquilibrium.ipynb) | [Index](README.md) | [4c-NashExistence-Python >>](GameTheory-04c-NashExistence-Python.ipynb)"
"**Navigation** : [<< 4-NashEquilibrium (track principal)](GameTheory-04-NashEquilibrium.ipynb) | [Index](README.md) | [4c-NashExistence-Python >>](GameTheory-04c-NashExistence-Python.ipynb)\n",
"> **Prolongement computationnel** : [GameTheory-04e — Oracles réflexifs](GameTheory-04e-Reflective-Oracles.ipynb) — auto-référence, décision causale (CDT/EDT) et restriction finie vérifiée (#14450)."
]
}
],
Expand Down Expand Up @@ -4080,4 +4081,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
5 changes: 3 additions & 2 deletions MyIA.AI.Notebooks/GameTheory/GameTheory-04c-NashExistence-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1968,7 +1968,8 @@
"tags": []
},
"source": [
"> **Lien avec la formalisation Lean** : Les concepts de ce notebook — simplexe standard, produit de simplexes, théorème de Brouwer (axiomatisé), structure `FiniteGame`, profils de stratégies mixtes et équilibre de Nash — sont construits interactivement dans le notebook compagnon [GT-4b-Lean-NashExistence](GameTheory-04b-Lean-NashExistence.ipynb) (kernel Lean 4), sans import Mathlib. La chaîne de preuves complète (Scarf → Sperner → Brouwer → Nash) est détaillée dans le dépôt externe `math-xmum/Brouwer/Nash.lean`."
"> **Lien avec la formalisation Lean** : Les concepts de ce notebook — simplexe standard, produit de simplexes, théorème de Brouwer (axiomatisé), structure `FiniteGame`, profils de stratégies mixtes et équilibre de Nash — sont construits interactivement dans le notebook compagnon [GT-4b-Lean-NashExistence](GameTheory-04b-Lean-NashExistence.ipynb) (kernel Lean 4), sans import Mathlib. La chaîne de preuves complète (Scarf → Sperner → Brouwer → Nash) est détaillée dans le dépôt externe `math-xmum/Brouwer/Nash.lean`.\n",
"> **Prolongement computationnel** : [GameTheory-04e — Oracles réflexifs](GameTheory-04e-Reflective-Oracles.ipynb) — auto-référence, décision causale (CDT/EDT) et restriction finie vérifiée (#14450)."
]
},
{
Expand Down Expand Up @@ -2063,4 +2064,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading
Loading