[Lean][GameTheory] Consolider les lakes GT : Arrow et Sen prouves deux fois, huit lakes sans carte (Concern #24179)

Part of #4362 · See #23097 · See #23022 · See #4365

D'où vient cette issue

Concern de jsboigeEPF sur #24179 (2026-11-02), verbatim :

Je n'ai toujours pas compris pourquoi on a: game_theory_lean/SocialChoice, lean_game_defs, SocialChoice/social_choice_lean_peters, lean_game_defs_ext, social_choice_lean. C'est absolument illisible et a priori on retrouve 2 version concurrentes de Arrow dans les deux premiers. J'ai déjà fait remonter mon concern, mais j'ai l'impression qu'il n'est pas pris en compte à la hauteur de la confusion.

Le Concern antérieur est celui de #23030, cité dans le body de #23097 (« l'effort n'a pas été suivi et l'entropie a repris le dessus »). Cette issue est le point de rendez-vous unique de la consolidation des lakes GameTheory ; la tranche T3 de #23097 (lean_game_defs contre lean_game_defs_ext) y est reprise.

Ce qui est mesuré (`origin/main` @ `1dc9c3fdaa8`, rejouable)

Deux théorèmes prouvés deux fois

Théorème	`game_theory_lean` (Mathlib, `Finset`)	`lean_game_defs` (Lean core, `Fin n`)
Arrow	`SocialChoice/Arrow.lean:691` `theorem arrow` — prouvé depuis le 2026-07-11 (absorption #6058 sous #4365), 0 `sorry`	`SocialChoice.lean:894` `theorem arrow_impossibility` — `axiom` jusqu'au 2026-10-28, prouvé par le port de #23022 (#23030, #23074, #23078)
Sen	`SocialChoice/Sen.lean:71` `theorem sen_impossibility`	`SocialChoice.lean:986` `theorem sen_impossibility` — étage 5 du même port (#23143, 2026-11-01)

Chacun a son miroir _en : huit fichiers portent deux fois les deux mêmes résultats.

git grep -n -E '^theorem (arrow|arrow_impossibility|sen_impossibility)\b' origin/main -- 'MyIA.AI.Notebooks/GameTheory/**/*.lean'

Huit lakes dans la série, sans carte lisible

Lake	`.lean` (FR+EN)	Toolchain	Né le	Dépendance
`game_theory_lean`	64	v4.33.0	2026-07-10	Mathlib, 8 `lean_lib`
`lean_game_defs`	12	v4.33.0	2026-06-10	aucune (Lean core)
`lean_game_defs_ext`	29	v4.33.0	2026-06-10	— (lib `Bayesian`)
`minimax_lean`	9	v4.33.0	2026-06-24	séparé par la clause anti-god-lake de #4365
`conway_cgt_lean`	3	v4.33.0-rc1	2026-06-05	idem
`assignment_lean`	13	v4.33.0	2026-08-23	né après la clôture de #4365
`asymmetric_information_lean`	12	v4.33.0	2026-08-26	idem
`SocialChoice/social_choice_lean_peters`	15	v4.32.1	2026-10-05	lake de Peters (vote par approbation), rangé sous un dossier de carnets et non à la racine des lakes

Plus social_choice_lean/ : coquille de 4 .md, 0 .lean (tombstone de #10151), qui se lit comme un neuvième lake.

lean_game_defs et lean_game_defs_ext portent chacun un module Bayesian et un module Regret : recouvrement de contenu à mesurer, pas encore mesuré.

Pourquoi c'est arrivé

lean_game_defs : arrow_impossibility est un axiome declare, pas une preuve (trouve par le gate #22519) #23022 n'offrait que deux sorties : porter la preuve, ou documenter l'écart. La troisième (le théorème est déjà prouvé dans game_theory_lean, y renvoyer) manquait. La question 1 de organ-first-implementation.md (« quelle série possède déjà la sémantique ? ») n'a jamais été posée. L'issue est née d'une tranche de CI (ci(lean): cabler le gate proof-integrity sur les 13 lakes matriciels qui n'en portent pas #22519), donc du périmètre du coordinateur.
[Lean][infra] Carte du materiel Lean et regle d'accretion d'un lac (suite de #4365) #23097 a mesuré la duplication par collision de noms de module. Un tel instrument est structurellement aveugle à Arrow.lean contre SocialChoice.lean. Sa phrase « aucune duplication de preuves entre lacs » est fausse.
Le port a continué après le Concern sur Feat(lean,#23022): port de la preuve d'Arrow -- coalitions decisives, expansions, cloture du champ et contraction (etages 1-3) #23030. Ce Concern a été rangé dans une issue au lieu d'arrêter le grain, puis les étages 4a, 4b et 5 (Sen) ont été mergés.

Doctrine des lakes : validée le 2026-11-02

Le user a validé les quatre règles proposées dans #4362. Il a aussi validé la redescente des libs de game_theory_lean dans leurs sous-séries, ce qui renverse #4365 :

R1 : le site d'un lake suit les carnets qui l'utilisent.
R2 : on ne fusionne plus pour gagner du disque ou des jobs CI, puisque les jonctions Mathlib et la matrice CI s'en chargent.
R3 : on ne fusionne que si les lakes s'importent, ou s'ils redéfinissent les mêmes objets. La clause anti-god-lake est maintenue.
R4 : un résultat a une maison canonique, et un doublon se déclare.

Le texte de référence sera docs/reference/lean-lakes-doctrine.md (PR à venir).

Gel

Le gel des absorptions dans un hub est remplacé par la doctrine. Une seule interdiction reste en vigueur jusqu'à la fin de T1 : aucun nouveau théorème dans lean_game_defs/SocialChoice*.lean. Les autres PRs Lean GT continuent.

Tranches, dans l'ordre

T0 — L'instrument qui manquait : doublons au niveau des théorèmes

Un organe (extension de scripts/lean/lean_material_map.py ou script voisin) qui repère, entre lakes, les déclarations theorem qui énoncent le même résultat : nom normalisé et mots-clés de docstring, au minimum. Contrôle positif obligatoire : l'organe doit trouver Arrow et Sen ci-dessus. Il tourne sur tout le dépôt, pas seulement sur GameTheory, car rien ne dit que la maladie est locale. Sortie : la liste, publiée dans docs/reference/lean-material-map.md.

T1 — Deux preuves qui se connaissent : une consolidation consciente

Révisé le 2026-11-02 sur réponse du user (fil de coordination) : deux preuves du même théorème sont une richesse, à condition d'être comparées plutôt que de s'ignorer. On ne retire rien en T1.

Deux stratégies.
- game_theory_lean/SocialChoice/Arrow.lean est un port d'asouther4/lean-social-choice. C'est la première preuve de Geanakoplos (2005), par pivot, avec Mathlib et Finset.
- lean_game_defs/SocialChoice.lean est écrit de zéro (lean_game_defs : arrow_impossibility est un axiome declare, pas une preuve (trouve par le gate #22519) #23022). Il procède par coalitions décisives et expansion du champ, en Lean seul, sur Fin n.
- Sen n'est pas dans le même cas (correction du 2026-11-02). La mesure de reprise de social_choice_lean/NOTICE.md (section « Mesure de reprise ») compte 0 nom amont dans game_theory_lean/SocialChoice/Sen.lean, classé « ajout CoursIA ». Les deux preuves de Sen sont donc écrites par CoursIA, et la licence ne les départage pas. Sa maison canonique suit celle d'Arrow, dans le même module et sur les mêmes objets. La note de comparaison dit ce que chacune apporte.
Pour Arrow, la licence désigne la maison canonique.
- L'amont asouther4 n'a pas de licence (license: null). La demande du 2026-10-25 (Could you add a license to the repository? asouther4/lean-social-choice#12) est restée sans réponse, et le dépôt n'a reçu aucun push depuis 2021 (licence: 7 repertoires portent un NOTICE sans copie du texte de licence (depot public) #14955).
- La preuve indépendante devient donc canonique, et le port d'asouther4 devient une preuve alternative déclarée.
- Décision du user le 2026-11-02 : on garde le port d'asouther4, sans date butoir, avec la notice d'attribution qui doit l'accompagner.
Livrables de T1
- Une NOTICE d'attribution à côté du code. Aujourd'hui, elle n'existe que dans la coquille social_choice_lean/NOTICE.md. Elle est déplacée par git mv vers game_theory_lean/SocialChoice/NOTICE.md, avec ses liens relatifs corrigés. On y ajoute que Arrow.lean et Basic.lean sont une preuve alternative déclarée, et l'on y cite la maison canonique. La coquille garde un pointeur d'une ligne jusqu'à T3.
- Une note de comparaison, versée dans le README du lake et dans une section du carnet SocialChoice/01b-Lean-SocialChoice-Formal (carnet modifié via le MCP jupyter-papermill, puis ré-exécuté). Elle porte sur les axiomes atteints, la longueur, la généralité (Finset contre Fin n) et ce que chaque stratégie enseigne.
- Des renvois croisés dans les docstrings des deux théorèmes.
- Ce que la version Mathlib a de meilleur passe dans la version canonique, avec les lignes citées.
Aucun axiom ne revient ; le gate d'axiomes (Fix(lean,#23022): vider la whitelist gamedefs -- l'axiome arrow_impossibility est tombe #24179) l'interdit.

L'emplacement final de la version canonique suit la doctrine, désormais validée : le site suit le consommateur, donc GameTheory/SocialChoice/. Le déplacement est une tranche de T3, qui vient après T0 et T1 ; T1 ne déplace aucun .lean.

T2 — `lean_game_defs` et `lean_game_defs_ext` : un lake, ou deux justifiés

C'est la T3 de #23097, reprise ici. Il s'agit de mesurer le recouvrement des modules Bayesian et Regret, puis de choisir : fusionner (le nom _ext le suggère), ou écrire pourquoi les deux lakes restent séparés.

T3 — Une arborescence qu'on lit

Redescendre (R1, validé le 2026-11-02). La lib SocialChoice de game_theory_lean descend sous GameTheory/SocialChoice/, avec sa NOTICE ; le lien avec la preuve canonique se tranche à ce moment-là. Pour les sept autres libs du hub (CooperativeGames, StableMarriage, RepeatedGames, Swaps, Abstraction, ProgramGames, StackelbergBilevel), on mesure d'abord, par les imports des carnets, celles qui ont une sous-série, puis on fait une PR par descente.
Retirer la coquille social_choice_lean/, après une preuve de préservation des 4 .md.
Décider de la place de social_choice_lean_peters : lake de Peters (toolchain divergente, INTRINSIC docs(gt,#4365): document INTRINSIC verdict for social_choice_lean_peters #7081), mais rangé sous SocialChoice/.
Ajouter au README GameTheory une carte des lakes : une ligne par lake survivant, qui dit ce qu'il prouve et pourquoi il est séparé, générée par l'organe de T0 et non écrite à la main.

Acceptance

T0 : organe livré, avec contrôle positif (Arrow et Sen trouvés), sortie publiée.
T1 : game_theory_lean/SocialChoice/NOTICE.md existe à côté du code ; note de comparaison des deux preuves d'Arrow et de Sen, publiée (README du lake et carnet 01b) ; renvois croisés dans les docstrings ; la preuve indépendante est déclarée canonique et le port d'asouther4 est déclaré preuve alternative, gardé avec sa notice.
T2 : décision écrite et mise en œuvre pour lean_game_defs et lean_game_defs_ext.
T3 : SocialChoice redescendue sous GameTheory/SocialChoice/ ; descente mesurée, et faite là où elle s'applique, pour les sept autres libs du hub ; coquille retirée ; carte des lakes dans le README GameTheory.
Chaque déplacement est une PR dédiée, avec preuve de préservation (théorèmes conservés, lake build SUCCESS, renvois de carnets mis à jour) ; anti-régression selon anti-regression.md.

🤖 Generated with Claude Code

[CLAIMED] lane myia-ai-01:CoursIA-2 -- T0 : organe de detection des doublons au niveau des theoremes entre lakes, controle positif Arrow+Sen, tout le depot (claim pose au dispatch par le coordinateur) -- paths: scripts/lean/lean_material_map.py, scripts/lean/lean_theorem_duplicates.py, scripts/lean/tests/**, docs/reference/lean-material-map.md

[CLAIMED] lane myia-po-2023:CoursIA -- T1 puis T2 : analyse du port Arrow/Sen de lean_game_defs contre game_theory_lean/SocialChoice (etape 1 de la consolidation, lecture seule tant que T0 n'est pas mergee), puis lean_game_defs contre lean_game_defs_ext (claim pose au dispatch par le coordinateur) -- paths: MyIA.AI.Notebooks/GameTheory/lean_game_defs/, MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/**

[myia-ai-01] T1 revisee sur reponse du user (body mis a jour) : deux preuves sont une richesse a condition qu'elles se connaissent. On ne retire plus rien en T1. La preuve independante de lean_game_defs devient canonique, puisqu'elle est propre en droits : l'amont asouther4 n'a pas de licence, cf. #14955 et asouther4/lean-social-choice#12, sans reponse. Le port d'asouther4 devient une preuve alternative declaree. Livrable : note de comparaison et renvois croises. Aucun deplacement de fichier avant la validation, par le user, de la doctrine des lakes (« le site suit le consommateur »).

[CLAIMED-AMEND] lane myia-po-2023:CoursIA -- T1 revisee (comparaison consciente, aucun retrait) puis T2 (amend pose par le coordinateur) -- paths: MyIA.AI.Notebooks/GameTheory/lean_game_defs/, MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/**, MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb

T1 étape 1 — analyse lecture seule (lane myia-po-2023:CoursIA, dispatch c2754 + amend). Toutes les lignes citées sont mesurées sur origin/main à la tête du 02/11 (git show origin/main:<chemin>).

Ce que le port `lean_game_defs/SocialChoice.lean` (1045 l.) apporte et que la version Mathlib n'a pas

1. Profils par utilités entières, en Lean core. represents (l.143), prefFromUtility (l.147), rank3 (l.174), prefOfUtility (l.179) construisent une Preference A depuis une utilité A → Int. La preuve de Sen les utilise : chaque profil témoin est prefOfUtility (rank3 z x y 3 2 1) (l.988-991), et chaque obligation de Décisivité/Pareto se clos par simp [...] <;> decide (l.1000-1044) — la preuve est calculatoire : le contre-exemple est une affectation d'entiers que Lean vérifie. La version Mathlib construit ses profils par chirurgie abstraite (maketop_pref, makeabove/makebelow, Arrow.lean l.115-144) et prouve les propriétés à la main.

2. L'échelle des coalitions décisives, palier par palier. Decisive (l.190) puis decisive_unanimous (199), decisive_expand_right (211), decisive_expand_left (287), decisive_swap (362), decisive_field (381), decisive_split (417), empty_not_decisive (611), decisive_global (629), decisive_singleton_dictator (669), decisive_congr (786), exists_dictator_of_decisive (824) — l'argument classique de propagation de la décisivité d'Arrow, chaque palier est un théorème nommé et citable. arrow_impossibility (894) est la conveyor belt terminale en 35 lignes. C'est la version qui se découpe en cours.

3. Sen : une forme plus forte ET un diagnostic pédagogique intégré. Le port réfute l'axiomatique elle-même : sen_impossibility {I A} [DecidableEq ...] (swf) (h_pareto) : ¬ SenLiberalism swf (l.986) — sans IIA, sans hypothèse de cardinalité sur I, sans Fintype. Et le fichier documente pourquoi la définition naïve ne marche pas : MinimalLiberalism (l.125) est trop faible car dictatorship_minimally_liberal (972) prouve qu'une dictature la satisfait — d'où SenLiberalism (960) exigeant deux individus distincts sur deux paires croisées. La docstring (l.946-958) explique le recouvrement des paires comme condition de l'impossibilité, pas comme détail.

4. Zéro dépendance. lakefile.toml : « Self-contained lake project (core Lean only, zero dependency) ». C'est le socle de droits propre (l'amont asouther4 n'a pas de licence, #14955) — c'est ce qui en fait la canonique selon l'amend.

Ce que la version Mathlib (`game_theory_lean/SocialChoice/`, Arrow.lean 714 l. + Sen.lean 363 l.) a de meilleur

1. Généralité. arrow (f : SWF ι σ) (X : Finset σ) (hwp) (hind) (hX : 3 ≤ X.card) : is_dictatorship f X (Arrow.lean:691) — types ι σ arbitraires (société infinie comprise) et agenda local (3 alternatives parmi un ensemble plus grand). Le port est borné à Fin nI/Fin nA avec nA ≥ 3 global (l.894). Limite structurante à écrire dans la note : Finset est Mathlib — ce plafond du port n'est pas un oubli, c'est le prix de la zéro-dépendance.

2. Forme positive. arrow (691) construit le dictateur (is_dictatorship f X), no_perfect_swf (710) en dérive la forme négative. Le port n'a que la forme négative (¬ NonDictatorial, l.894). Versement naturel dans la canonique : un corollaire nommé « existe le dictateur ».

3. Une deuxième stratégie de preuve. Méthode du pivot (variante Geanakoplos) : extremal_lemma (207), pivot_exists (288), pivot_is_dictator_except_b (418), partial_dictator_is_full_dictator (603) — face à la propagation de décisivité du port. La note de comparaison peut enseigner les deux stratégies sur les mêmes énoncés.

4. Sen en forme contre-existentielle. sen_impossibility ... : ∃ prof : Profile ι σ, ¬∃ best, is_best_element best X (f prof).rel (Sen.lean:71) — exhibe le profil cyclique (avec sous-cases commentés l.78-95), là où le port refute l'axiomatique. Deux lectures du même théorème : « voici le profil qui cycle » vs « ces axiomes ne peuvent pas coexister ». Complémentaires.

Clôture axiomatique (mesures existantes citées, pas de build local ce cycle)

Port : étage 4b (28/10) — 14 jobs SUCCESS dont Proof integrity (lean_game_defs), distinct_code_sorry = 0, aucune classe d'axiome interdite (§4.1.1 docs/reference/lean-axiom-coverage.md). L'ancien axiom arrow_impossibility est tombé : c'est un theorem (l.894) depuis l'étage 4b.
Mathlib : contrat no-sorry CERTIFIED.txt (gate check_certified_sorry.py, absorption PR feat(lean,#4365): absorb SocialChoice (Arrow+Sen+Voting FR+EN) into game_theory_lean — anti-proliferation GT 6->2 #6058) ; 0 sorry mesuré sur Arrow.lean et Sen.lean à la tête ; jambes Lean CI (game_theory_lean) + proof-integrity à la tête.

Consommateurs mesurés (le point conditionnel du dispatch)

GameTheory-02b-Lean-Definitions-Lean.ipynb : 6 réf. lean_game_defs, 0 game_theory_lean → le port est une dépendance vivante de 02b ; tout retrait l'aurait cassé (l'amend a tranché : aucun retrait).
SocialChoice/01b-Lean-SocialChoice-Formal.ipynb : 18 réf. game_theory_lean + 14 réf. arrow_impossibility (le nom du port) → le carnet croise déjà les deux preuves : c'est le point d'ancrage naturel de la section de comparaison (étape 2 amendée).

Étape 2 amendée — plan de versement (à exécuter après livraison du grain en cours sur cette lane)

Note de comparaison (axes ci-dessus : axiomes atteints, longueur, généralité Fin n vs Finset, ce que chaque stratégie enseigne) versée au README du lake lean_game_defs + section du carnet 01b.
Renvois croisés dans les docstrings des 4 théorèmes FR (arrow_impossibility, sen_impossibility, arrow, sen_impossibility Mathlib) et miroirs EN (SocialChoice_en.lean, Arrow_en.lean, Sen_en.lean).
Versements Mathlib → canonique : forme positive (corollaire dictateur), mention de la méthode du pivot et de la forme contre-existentielle de Sen dans la note. Citation des lignes sources.
Carnet via MCP jupyter-papermill, re-exécution avant commit ; lake build dans un scope WSL borné ; une PR, preuve de préservation (aucun retrait, aucun déplacement).

[myia-ai-01] Réponse du user (2026-11-02, ~10:00Z) : la doctrine est validée, le port d'asouther4 est gardé. J'ai mis le body à jour en conséquence.

Verbatim : « a) Je valide b) OK poure redescendre c) On le garde avec la notice qui doit exister, et on documente la comparaison des preuves comme tu as proposé ».

Doctrine R1-R4 validée. Le gel des absorptions est levé et remplacé par la doctrine. Une seule interdiction reste en vigueur jusqu'à la fin de T1 : aucun nouveau théorème dans lean_game_defs/SocialChoice*.lean. Le texte de référence partira en PR dans docs/reference/lean-lakes-doctrine.md.
Redescente autorisée : [Lean][infra] Regrouper les lakes cohesifs post-convergence (GameTheory 6->2, modele multi-module) #4365 est renversé pour game_theory_lean. C'est une tranche de T3, qui vient après T0 et T1. La lib SocialChoice descend sous GameTheory/SocialChoice/. Pour les sept autres libs du hub, on mesure d'abord, par les imports des carnets.
Port d'asouther4 gardé, sans date butoir, comme preuve alternative déclarée d'Arrow. La date butoir que je proposais est abandonnée.

Ce qui s'ajoute à T1 : la notice « qui doit exister ». Aujourd'hui, elle n'existe que dans la coquille social_choice_lean/NOTICE.md, et rien n'accompagne le code dans game_theory_lean/SocialChoice/ (git ls-tree à la tête : aucun NOTICE* ni LICENSE*). T1 la déplace par git mv vers game_theory_lean/SocialChoice/NOTICE.md, avec ses liens relatifs corrigés et le statut « preuve alternative déclarée » ajouté. La coquille garde un pointeur d'une ligne jusqu'à T3.

Correction d'une phrase de mon body. J'avais écrit que Sen était « dans le même cas » qu'Arrow. C'est faux. La section « Mesure de reprise » de la NOTICE compte 0 nom amont dans game_theory_lean/SocialChoice/Sen.lean, classé « ajout CoursIA ». Seuls Arrow.lean et Basic.lean portent l'amont. Pour Sen, les deux preuves sont donc écrites par CoursIA, et la licence ne les départage pas. Sa maison canonique suit celle d'Arrow, et la note de comparaison dit ce que chacune apporte. L'analyse de la lane (commentaire précédent, points 3 et 4 de chaque côté) le montre déjà : réfutation de l'axiomatique contre profil cyclique exhibé.

À myia-po-2023:CoursIA : ton analyse de l'étape 1 est reçue, et ton plan d'étape 2 est validé, avec la NOTICE en plus. Le claim amendé couvre déjà game_theory_lean/SocialChoice/**.

[CLAIMED-AMEND] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/, MyIA.AI.Notebooks/GameTheory/social_choice_lean/, MyIA.AI.Notebooks/GameTheory/lean_game_defs/**, MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb

T1 étape 2 améndée (DM c2754 msg-20261102T100650-bctfcp, amend c2754-amend-24183-t1). Aucun retrait, aucun déplacement de .lean : le port lean_game_defs/SocialChoice.lean reste la maison canonique, game_theory_lean/SocialChoice/ reste la preuve alternative déclarée.

Livrables de cet amendement

git mv MyIA.AI.Notebooks/GameTheory/social_choice_lean/NOTICE.md -> MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/NOTICE.md — la notice rejoint son code ; liens relatifs corrigés ; paragraphe « Tombstone » réécrit ; Arrow.lean et Basic.lean déclarés preuve alternative avec renvoi nommé à lean_game_defs/SocialChoice.lean ; pointeur d'une ligne laissé dans social_choice_lean/ (il disparaîtra en T3).
Note de comparaison (axiomes atteints, longueur, Fin n vs Finset, méthode de preuve, forme de l'énoncé) versée au README du lake lean_game_defs et à une section du carnet 01b.
Renvois croisés dans les docstrings des théorèmes concernés (FR et miroirs _en) : arrow_impossibility / sen_impossibility côté port, arrow / sen_impossibility côté game_theory_lean.
Correction factuelle versée dans la note : Sen n'est pas un port de l'amont — 0 nom amont dans Sen.lean, les deux Sen sont écrits par CoursIA, la licence ne les départage pas.

Hors scope : la redescente de la lib SocialChoice sous GameTheory/SocialChoice/ reste T3, après T0 (organe chez ai-01:CoursIA-2). Aucun fichier hors des quatre globs ci-dessus.

[CLAIMED-AMEND] lane myia-ai-01:CoursIA-2 -- T0 : l'organe porte son propre fichier (scripts/lean/lean_theorem_duplicates.py), son test et sa propre page generee ; la table n'est PAS integree a lean-material-map.md, dont la page est touchee par #24166 (lane myia-po-2024:CoursIA) -- paths: scripts/lean/lean_theorem_duplicates.py, scripts/lean/tests/test_lean_theorem_duplicates.py, docs/reference/lean-theorem-duplicates.md, docs/README.md

[DELIVERED] lane myia-ai-01:CoursIA-2 -- paths: scripts/lean/lean_theorem_duplicates.py, scripts/lean/tests/test_lean_theorem_duplicates.py, docs/reference/lean-theorem-duplicates.md, docs/README.md -- PR #24189

T0 livree : l'organe qui repond par le contenu des declarations a la question posee par #24183 (Arrow et Sen prouves deux fois ?).

scripts/lean/lean_theorem_duplicates.py : index des declarations theorem/lemma par tokens de nom, paires de lacs differents retenues sur un token discriminant (rare dans le depot) cite par les DEUX docstrings ; classement forte / faible.
Controle positif : les paires Arrow et Sen sont trouvees et classees fortes ; les lemmes generiques (refl, trans, card, step) ne le sont pas. Verifie sur cet head par scripts/lean/tests/test_lean_theorem_duplicates.py.
Page generee : docs/reference/lean-theorem-duplicates.md (--write / --check).

La table n'est pas integree a lean-material-map.md : cette page est touchee par #24166 (lane myia-po-2024:CoursIA, ouverte) — collision de fichiers. L'organe est donc autonome.

docs/README.md est modifie simultanement par plusieurs PRs ouvertes (#24126, #24129, #24156, #24157, #24158, #24088) ; la ligne ajoutee est additive, en fin de table « Outils & methodologie ». Point de rendez-vous : #24183.

[DELIVERED] lane myia-po-2023:CoursIA -- PR #24193 -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/, MyIA.AI.Notebooks/GameTheory/social_choice_lean/, MyIA.AI.Notebooks/GameTheory/lean_game_defs/**, MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb

T1 (etape 2 amendee) est livre, en attente de review sur #24193.

Ce que la PR etablit : la NOTICE des deux preuves d'Arrow et de Sen rejoint le code qu'elle documente (game_theory_lean/SocialChoice/NOTICE.md, git mv depuis social_choice_lean/, liens et Tombstone reecrits), et les deux implementations cessent de s'ignorer — lean_game_defs/SocialChoice.lean est declaree maison canonique (1045 l., coeur Lean seul), game_theory_lean/SocialChoice/Arrow.lean et Sen.lean preuves alternatives declarees, avec renvois croises dans les docstrings FR et EN (8 fichiers). La comparaison elle-meme (axiomes, generalite, strategie de preuve, taille 1045 vs 714+363) est dans le README de lean_game_defs et au SS4.3 du carnet 01b.

Le point qui manquait au dossier : Sen n'est pas un portage. 0 des 4 noms de lean_game_defs y sont repris, et minimal_liberal y est strictement plus faible que SenLiberalism — il n'exige pas que les deux paires se croisent. Le carnet montre qu'il existe meme une quatrieme notion de liberalisme dans sa propre cellule inline. La notice le dit desormais au lieu de le laisser deviner.

Verifications : lean_game_defs compile apres retouches (Build completed successfully (14 jobs), SocialChoice et SocialChoice_en inclus). Carnet : aucun re-exec du (C.2) — la modification est markdown seule plus la suppression de six cles "language" hors schema nbformat, defaut preexistant sur main qui bloquait l'ecrivain MCP ; sorties committes inchangees.

Hors perimetre : aucun .lean deplace (T3 apres T0). Suite : T2 mesure le recouvrement lean_game_defs vs lean_game_defs_ext.

Fix(gametheory,#24183): social_choice_lean -- trois renvois perimes v…

T2 — recouvrement `lean_game_defs` / `lean_game_defs_ext` : mesuré, puis tranché

Mesure sur origin/main (blobs lus par git show, jamais l'arbre de travail partagé), siblings _en exclus — ce sont des traductions, pas du contenu concurrent. Instrument rejouable : t2_overlap.py, extraction des déclarations def/theorem/lemma/abbrev/structure/inductive/class/instance.

Volume

Lake	Fichiers `.lean` (hors `_en`)	Déclarations
`lean_game_defs`	6	116
`lean_game_defs_ext`	15	240

Recouvrement par nom : 2 sur 116 et 240

Nom	`lean_game_defs`	`lean_game_defs_ext`
`externalRegret`	`Regret.lean:85` (`def`)	`Bayesian/Regret.lean:43` (`def`)
`FictitiousPlayState`	`Regret.lean:167` (`structure`)	`Bayesian/FictitiousPlay.lean:31` (`structure`)

Par module de ext, le partage est nul partout sauf ces deux-là : Bayesian/Regret.lean 1/26, Bayesian/FictitiousPlay.lean 1/13, et 0/… sur les treize autres (Auction 0/13, BNE 0/8, Examples 0/6, InfoGames 0/20, Information 0/16, InformationNoisy 0/54, Max 0/11, Reputation 0/32, Sum 0/12, Types 0/7, Vickrey 0/9, VoiBench 0/13).

Les deux noms partagés sont des homonymes, pas des doublons

C'est le point qui compte, et il change la conclusion : les deux paires portent le même nom pour deux définitions différentes.

externalRegret — même nom, deux espaces d'actions et deux arithmétiques :

lean_game_defs/Regret.lean:85
  def externalRegret (T : Nat) (payoffs : Fin T → (Fin n → Float))
      (played : Fin T → Fin n) : Float            -- Float, espace Fin n

lean_game_defs_ext/Bayesian/Regret.lean:43
  def externalRegret (T nA : Nat) (payoff : Fin T → Fin (nA + 1) → Int)
      (played : Fin T → Fin (nA + 1)) : Int       -- Int, espace Fin (nA+1), via maxFin/fixedTotal/realizedTotal

FictitiousPlayState — même nom, deux structures :

lean_game_defs/Regret.lean:167      FictitiousPlayState (n : Nat)   { actionCounts : Fin n → (Fin m → Nat) ; rounds : Nat }
lean_game_defs_ext/Bayesian/FictitiousPlay.lean:31  FictitiousPlayState  { nAct, nOpp, opponentCounts : Fin (nOpp+1) → Nat, round }

Aucune duplication sémantique sous des noms différents n'a été trouvée sur le thème bayésien, où les deux jeux de définitions sont franchement distincts :

defs/Bayesian.lean (22 déclarations) prend le modèle de Harsanyi complet — TypeSpace, CommonPrior, BayesianGame, expectedPayoffBayesian, isBayesianNashEquilibrium — plus SignalingGame, FirstPriceAuction, et le poker de Kuhn (KuhnCard, KuhnState, kuhnPayoff…) ;
ext/Bayesian/ prend une spécialisation à deux joueurs en arithmétique entière (BayesGame2, interimU1, isBNE), une théorie de la valeur de l'information (DecisionProblem, Signal, valueNoInfo/valueSignal/valuePerfect, umbrella_*), et une couche de lemmes de bibliothèque que defs n'a pas du tout (sumFin_* 12 lemmes, maxFin_*/argmaxFin_* 11 lemmes), plus Vickrey, Reputation, InfoGames, FictitiousPlay.

Fond structurel : rien ne les relie

lean_game_defs/lakefile.toml se déclare « Self-contained lake project (core Lean only, zero dependency) », cible LeanGameDefs.
lean_game_defs_ext/lakefile.toml déclare une seule lib, Bayesian, et n'importe ni LeanGameDefs ni Mathlib : la totalité de ses imports est interne (Bayesian.BNE, Bayesian.Sum, Bayesian.Max, …).
Zéro import croisé dans les deux sens, deux namespaces distincts, deux cibles de build distinctes.

Décision : séparation, et elle est écrite ici

Fusionner demanderait de renommer au moins un membre de chaque paire homonyme, ce qui casserait les siblings _en, les renvois de carnets et la propriété « core Lean, zéro dépendance » que lean_game_defs revendique et qui est la raison d'être de ce lake (les carnets GameTheory-02b ont besoin d'Arrow et du regret sans Mathlib). Le gain d'une fusion serait nul : il n'y a rien à dédupliquer, les 2 noms communs étant deux choses différentes.

Ce qui manque n'est donc pas un merge, c'est une déclaration — exactement le défaut que #24183 corrige pour Arrow et Sen, et qui se répète ici : deux formalisations coexistent sans que rien ne dise lesquelles. Il y a en plus un risque concret, absent du cas Arrow/Sen : les deux homonymes ont des types incompatibles, donc un consommateur qui importe les deux lakes se heurte à une erreur de typage là où le nom lui laissait croire à un remplacement.

Suite bornée que je propose de livrer : un paragraphe dans chaque README.md de lake qui nomme l'autre lake, dit ce que chacun porte, et déclare explicitement les deux homonymes (externalRegret, FictitiousPlayState) comme non interchangeables, avec le renvoi file:line de chaque côté. Aucun .lean déplacé, aucune preuve touchée : c'est de la prose, et le lake build des deux cibles doit rester vert.

Mesure et décision sont posées ; je passe à ce paragraphe sauf contre-indication.

[DELIVERED] lane myia-po-2023:CoursIA -- PR #24206 -- paths: MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/README.md

T2 livre. Mesure : 116 declarations d'un cote, 240 de l'autre, 2 noms communs seulement, et ce sont des homonymes de types incompatibles (externalRegret Float/Fin n contre Int/Fin (nA+1) ; FictitiousPlayState indexe par n contre nAct/nOpp/opponentCounts). Aucune duplication semantique sous des noms differents sur le theme bayesien.

Decision : separation, ecrite dans les deux README (aucun .lean touche, +19/-0). Aucun lakefile ne porte de require vers l'autre, aucun module n'importe l'autre, et les deux paires sont declarees en racine (aucun namespace dans les modules FR) : la collision est latente, pas active, et c'est precisement ce que la note de part et d'autre rend visible.

Le meme defaut de fond que T1 (deux formalisations coexistent sans que rien ne le declare), avec une gravite propre ici : les types sont incompatibles, donc un consommateur qui croiserait les deux noms aurait une erreur de typage la ou le nom laisse croire a un remplacement.

T1 reste en PR #24193 (autocorrection du README de la coquille poussee ce cycle, 87fe311293e). T0 et T3 ne sont pas de mon perimetre.

docs(lean,#4362): doctrine des lakes R1-R4 -- le site suit le consomm…

Fix(gametheory,#24183): T1 -- retirer le compteur de lignes de la tab…

Fix(gametheory,#24183): carte des lakes -- theoreme orthographie comm…

Grain: DEEP/notebook-lean — lane myia-po-2028:CoursIA-2 — prev: DEEP/notebook-lean #24567

[CLAIMED] lane myia-po-2028:CoursIA-2 -- T1 suite : le renvoi croise du miroir EN (lean_game_defs/SocialChoice_en.lean) est pose sur le commentaire de definition MinimalLiberalism au lieu de la docstring sen_impossibility -- paths: MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice_en.lean

Portee : un seul fichier, le miroir EN du lac canonique. Le canonique FR lean_game_defs/SocialChoice.lean n'est pas touche.

Ecart mesure (scripts/lean/check_i18n_token_fidelity.py, sur le fichier seul) : 1 ecart DUR (span SenLiberalism porte par le canonique FR a l'ancre sen_impossibility, absent du miroir EN a la meme ancre) et 3 ADVISORY cote EN sur l'ancre MinimalLiberalism (game_theory_lean/SocialChoice/Sen.lean, minimal_liberal, ∃ prof, ¬∃ best) : le miroir EN porte le meme paragraphe, mais a l'autre ancre.

Origine : les deux ancres ont ete posees par le meme commit (febb394b5d, PR #24193), dont le message annonce « renvois croises dans les docstrings des quatre theoremes, FR et miroirs _en ». La docstring EN sen_impossibility est donc restee sans son renvoi. Correction = relocation du paragraphe sur l'ancre FR, dans le miroir EN seul : aucune modification de code, de signature ni de preuve (docstrings et commentaires seuls, conformement a la convention i18n Option A).

Verrou : le [DELIVERED] lane myia-po-2023:CoursIA -- PR #24193 ferme la revendication de po-2023 sur lean_game_defs/** (semantique v1 de scripts/check_lane_claim.py : [DELIVERED] clot la revendication ; la semantique conditionnelle v2 n'est pas implementee). Verifie a la source, pas sur le libelle : blocking_lanes: [] pour le chemin vise, scope_intersection_paths: [].

Collision : balayage des 239 PRs ouvertes (gh api repos/jsboige/CoursIA/pulls/<N>/files --paginate, la sortie --json files de gh pr list plafonnant a 100 fichiers par PR) : aucune ne touche lean_game_defs/SocialChoice_en.lean ni lean_game_defs/SocialChoice.lean. Les correspondances SocialChoice trouvees sont dans d'autres repertoires (game_theory_lean/SocialChoice/, SocialChoice/, social_choice_lean_peters/).

Grain: DEEP/notebook-lean — lane myia-po-2028:CoursIA-2 — prev: DEEP/notebook-lean #24567

[DELIVERED] lane myia-po-2028:CoursIA-2 -- PR #24722 -- paths: MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice_en.lean

Le renvoi croisé de sen_impossibility est porté par la docstring du miroir EN
lean_game_defs/SocialChoice_en.lean — l'ancre que le canonique FR utilise.

Mesure sur le fichier seul (scripts/lean/check_i18n_token_fidelity.py) :
1 ecart DUR + 13 ADVISORY → 0 ecart DUR + 4 ADVISORY. Les 4 restants sont
des faux positifs documentes dans le corps de la PR (elision francaise
l'IIA, en-tetes traduits).

Perimetre : 1 fichier, 9 lignes inserees et 9 supprimees, toutes dans des
docstrings ou des commentaires ; aucune modification de code, de signature ni
de preuve. scripts/lean/check_i18n_siblings.py sur lean_game_defs : 6/6
paires byte-identiques, 0 drift, 0 orphan (rc=0).

T1 de #24183 : le renvoi croisé manquant côté miroir EN est pose ; le critère
« renvois croises dans les docstrings des deux theoremes » est désormais tenu
des deux cotes (FR l. 895 et 992 ; EN l. 899 et 997). La T1 reste ouverte sur
ses autres livrables (les raisins du port Mathlib a reprendre dans la version
canonique).

Aucun build lake local : la compilation est prouvee par la CI (verdict user du
2026-11-01).

See #24143

Docs(lean,#24183): T0 ballotage -- triage des 14 paires de l'organe d…

Docs(lean,#24273): declarer le doublon one_sub_pow_le_exp entre learn…

Fix(lean): la page derivee ne cite plus les numeros de ligne, et sa d…

Fix(lean,#24730): regenerer les pages derivees apres l'ajout de Repea…

Docs(gametheory,#24183): T3 -- la carte des lakes dit pourquoi chacun…

Feat(lean,#4362): colonnes de conformite R1 et R4 de la carte du mate…

Docs(gametheory,#24183): les renvois du bloc social choice pointent s…

Prérequis de T3 — dépendance code : MyIA.AI.Notebooks/GameTheory/scripts/validate_lean_setup.py, fonction check_social_choice_lean() (l. 169-179), vérifie encore l'existence de social_choice_lean/lakefile.lean, retiré depuis #4365 — le check échoue déjà sur main. À corriger avant le retrait de la coquille (PR #24496, commit b5bb72869cf, le nomme dans le tableau des prérequis T3 du README.md de la coquille ; le script n'y est pas réparé, hors périmètre).

Docs(lean,#24183): regenerer la carte du materiel Lean apres la march…

Docs(gametheory,#9535): preuve de preservation de la coquille social_…

Fix(gametheory,#24183): le renvoi croise Sen dans le miroir EN, sur l…

Feat(prover,#1453): panel de sorry documentes -- decision_theory_lean…

Navigation Menu

Repository navigation

[Lean][GameTheory] Consolider les lakes GT : Arrow et Sen prouves deux fois, huit lakes sans carte (Concern #24179) #24183

D'où vient cette issue

Ce qui est mesuré (`origin/main` @ `1dc9c3fdaa8`, rejouable)

Deux théorèmes prouvés deux fois

Huit lakes dans la série, sans carte lisible

Pourquoi c'est arrivé

Doctrine des lakes : validée le 2026-11-02

Gel

Tranches, dans l'ordre

T0 — L'instrument qui manquait : doublons au niveau des théorèmes

T1 — Deux preuves qui se connaissent : une consolidation consciente

T2 — `lean_game_defs` et `lean_game_defs_ext` : un lake, ou deux justifiés

T3 — Une arborescence qu'on lit

Acceptance

Ce que le port `lean_game_defs/SocialChoice.lean` (1045 l.) apporte et que la version Mathlib n'a pas

Ce que la version Mathlib (`game_theory_lean/SocialChoice/`, Arrow.lean 714 l. + Sen.lean 363 l.) a de meilleur

Clôture axiomatique (mesures existantes citées, pas de build local ce cycle)

Consommateurs mesurés (le point conditionnel du dispatch)

Étape 2 amendée — plan de versement (à exécuter après livraison du grain en cours sur cette lane)

T2 — recouvrement `lean_game_defs` / `lean_game_defs_ext` : mesuré, puis tranché

Volume

Recouvrement par nom : 2 sur 116 et 240

Les deux noms partagés sont des homonymes, pas des doublons

Fond structurel : rien ne les relie

Décision : séparation, et elle est écrite ici

17 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

[Lean][GameTheory] Consolider les lakes GT : Arrow et Sen prouves deux fois, huit lakes sans carte (Concern #24179) #24183

Description

D'où vient cette issue

Ce qui est mesuré (origin/main @ 1dc9c3fdaa8, rejouable)

Deux théorèmes prouvés deux fois

Huit lakes dans la série, sans carte lisible

Pourquoi c'est arrivé

Doctrine des lakes : validée le 2026-11-02

Gel

Tranches, dans l'ordre

T0 — L'instrument qui manquait : doublons au niveau des théorèmes

T1 — Deux preuves qui se connaissent : une consolidation consciente

T2 — lean_game_defs et lean_game_defs_ext : un lake, ou deux justifiés

T3 — Une arborescence qu'on lit

Acceptance

Activity

myia-ai-01 commented on Nov 2, 2026

myia-ai-01 commented on Nov 2, 2026

myia-ai-01 commented on Nov 2, 2026

myia-ai-01 commented on Nov 2, 2026

jsboigeEpita commented on Nov 2, 2026

Ce que le port lean_game_defs/SocialChoice.lean (1045 l.) apporte et que la version Mathlib n'a pas

Ce que la version Mathlib (game_theory_lean/SocialChoice/, Arrow.lean 714 l. + Sen.lean 363 l.) a de meilleur

Clôture axiomatique (mesures existantes citées, pas de build local ce cycle)

Consommateurs mesurés (le point conditionnel du dispatch)

Étape 2 amendée — plan de versement (à exécuter après livraison du grain en cours sur cette lane)

myia-ai-01 commented on Nov 2, 2026

jsboigeEpita commented on Nov 2, 2026

jsboige commented on Nov 2, 2026

jsboige commented on Nov 2, 2026

jsboige commented on Nov 2, 2026

jsboige commented on Nov 2, 2026

T2 — recouvrement lean_game_defs / lean_game_defs_ext : mesuré, puis tranché

Volume

Recouvrement par nom : 2 sur 116 et 240

Les deux noms partagés sont des homonymes, pas des doublons

Fond structurel : rien ne les relie

Décision : séparation, et elle est écrite ici

jsboige commented on Nov 2, 2026

17 remaining items

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 6, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Ce qui est mesuré (`origin/main` @ `1dc9c3fdaa8`, rejouable)

T2 — `lean_game_defs` et `lean_game_defs_ext` : un lake, ou deux justifiés

Ce que le port `lean_game_defs/SocialChoice.lean` (1045 l.) apporte et que la version Mathlib n'a pas

Ce que la version Mathlib (`game_theory_lean/SocialChoice/`, Arrow.lean 714 l. + Sen.lean 363 l.) a de meilleur

T2 — recouvrement `lean_game_defs` / `lean_game_defs_ext` : mesuré, puis tranché