SocialChoice Lean : core des élections de comité par approbation (Becker-Greger-Peters 2026) au-dessus de SocialChoiceLean

[myia-ai-01]

Origine

Suite nommée de #16848 (option B). L'option A est livrée : carnet GameTheory/SocialChoice/07-Committees-Core.ipynb (PR #16896). Le commentaire de livraison gardait l'option B en suivi dans #16848 ; elle vit désormais ici, pour que #16848 puisse se fermer sur ce qui est fait.

Objet

Le résultat de Becker, Greger et Peters (arXiv 2609.11912) établit que le core existe toujours dans les élections de comité par approbation, avec une preuve constructive (optimum local d'un objectif d'entropie harmonique sur des systèmes de paiement). Dominik Peters est l'auteur de SocialChoiceLean, que le dépôt épingle dans GameTheory/social_choice_lean_peters/ (rev 94a4c650, le tour importe SocialChoice.Axioms.Core).

État amont mesuré (2026-09-26 19:20Z)

• Aucun commit sur DominikPeters/SocialChoiceLean depuis le 2026-09-01.
• La recherche de code « approval core » dans ce dépôt ne rend que AGENTS.md et Pivato/pivato.tex : pas de formalisation du core d'approbation.

Travail attendu

1. Re-sonder l'amont au moment du claim (mêmes deux mesures). Si Peters a publié la formalisation, le geste devient une montée de pin et une section du tour, pas un port.
2. Sinon, formaliser au-dessus de la bibliothèque épinglée : élection par approbation, quota (Hare n/k, Droop n/(k+1)), core d'un comité. Réutiliser SocialChoice.Axioms.Core s'il couvre déjà une partie.
3. Prouver ce qui est à portée sans sorry sur main : au minimum la caractérisation par systèmes de paiement (théorème 3.3 du papier) ou un cas borné explicite. Le théorème d'existence complet est un objectif, pas une condition de sortie.

Critère de sortie

Une PR sur le lake SocialChoice qui livre (1) ou (2)+(3), avec compte sorry réel avant/après (python scripts/lean/count_code_sorry.py --json) et build du lake. Si la lane juge après lecture que la formalisation est hors de portée en un cycle DEEP, elle l'écrit ici avec ce qu'elle a mesuré, et l'issue se ferme sur ce constat.

Périmètre

MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ uniquement. Pas de native_decide (axiome interdit par le gate proof-integrity).

See #16848

[jsboige]

[CLAIMED] lane myia-po-2024:CoursIA-2 — DEEP/lean CONTENU, démarrage analyse amont Becker-Greger-Peters arXiv 2609.11912 sur SocialChoiceLean (rev 94a4c650)

[jsboige]

#17988 — Plan de livraison par tranches (c.1485, lane myia-po-2024:CoursIA-2)

[c.1485] Premier contact avec le grain DEEP/lean — pivot depuis le narrow-cache repair #17851. Claim posé cid 5850363535.

État amont first-hand (vérifications G.1)

Item	Body de l'issue	Vérifié c.1485
Head upstream DominikPeters/SocialChoiceLean	94a4c650, 2026-07-21	✅ 94a4c650b6 confirmé via gh api .../commits
Présence formalisation "approval core" upstream	absente (seuls AGENTS.md + Pivato/pivato.tex)	✅ grep -rli 'approval' dans le local _peters/ retourne 0 fichier
Présence formalisation "approval core" localement	(idem)	✅ idem — pas de duplication (Tell G.1 durci)
Type d'attache au dépôt CoursIA	le body dit « submodule épinglé »	Nuance : _peters n'apparaît PAS dans .gitmodules (5 submodules : MetaGeneticSharp, Z3.Linq, Automata, Argumentum, semantic-fleet). C'est un dossier versionné ordinaire + un sous-projet Lake. Le submodule upstream est consommé via lakefile require mathlib + dépendances Lake implicites (PetersTour.lean utilise SocialChoice.Axioms.Core etc., qui sont des modules de l'upstream, pas locaux).

Scope délimité (1 grain DEEP/lean ↔ plusieurs cycles)

Le travail substantiel (formalisation d'un résultat publié en septembre 2026) demande plusieurs cycles :

Tranche 1 — Socle de définitions (c.1485+ ou c.1486) :

• Créer SocialChoice/Committees/Approval/Defs.lean + _en.lean siblings i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 :
  • Ballot (multi-ensemble d'approbations)
  • ApprovalProfile (collection de ballots + taille du comité)
  • Committee (sous-ensemble de candidats de taille k)
  • Happiness (utilité additive d'un comité pour un ballot — nombre d'approbations satisfaites)
  • PaymentFunction (vecteur de paiements vers les votants, contraints à somme nulle)
  • ObjectiveFunction (objectif à optimiser)
• Couple minimale au corpus existant (SocialChoice.Profile, etc.) via lake build.
• Lake build SUCCESS = plancher DEEP tenu.

Tranche 2 — Core definition (après Tranche 1) :

• Core.lean : un comité S est dans le core ssi il n'existe aucune coalition T et aucun paiement p qui améliore strictement tous les votants de T.
• Lemme d'identité : core vide ⇒ pas d'amélioration possible pour aucune coalition.
• Théorème BGP 2026 : le core d'approbation est non-vide pour tout profil et tout k ≥ 1.

Tranche 3 — Énoncé + preuve constructive (plusieurs cycles, maximum d'effort) :

• Formaliser le résultat arXiv 2609.11912 — algorithme « harmonic entropy local optimum ».

Justification de la cadence par cycles

Un grain DEEP/lean CONTENU par cycle ne tient pas G-VAR-1 strict : il faut Livrer ≠ Promettre. Chaque tranche doit produire une PR mergeable, pas une ébauche en développement. Le claim ne tient pas une PR à lui seul : la règle du dépôt est « Claim + PR livrée avant [DONE] ».

Décision c.1485 : claim + commentaire de plan seulement, pas de PR ce cycle. Le commentaire PR suit, et la Tranche 1 commence à c.1486 (prochain grain).

Risques et points de vigilance

1. Convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : tous les nouveaux fichiers *.lean du Peters submodule doivent avoir un sibling _en.lean byte-identique sauf docstrings. Verification post-write via scripts/lean/check_i18n_siblings.py.
2. Pas de duplication d'organe : vérifier que Peters upstream n'a pas déjà Approval/Defs.lean au moment du commit (re-check à chaque cycle, fast-forward peut le faire apparaître). gh api repos/DominikPeters/SocialChoiceLean/contents/SocialChoice/Committees/Approval à intégrer au scope check.
3. Pas de sorry INTRINSIC sans bumper baseline : si la preuve BGP est trop dure, ne pas feinter avec un sorry qui n'est pas dans la doctrine (cf PR fix(lean,#1453,#17756): Angel.lean + Angel_en.lean - header cleanup (revue ai-01 5324529283, tete e13c3f67a4) #17756 qui a retiré son sorry framework). Si le résultat est hors de portée Mathlib 4 actuelle → escalade ai-01 avant tout sorry.
4. Submodule maintenance : R3 strict du submodule-maintenance ne s'applique PAS ici (_peters n'est pas un submodule), mais le submodule upstream est par défaut non versionné dans CoursIA. Sa présence dans le projet Lake le rend dépendance externe implicite — un commit qui break la base upstream ne se verra qu'à lake build.

Liens / références croisées

• Issue [Veille→Distillation] arXiv 2609.11912 — Existence du core dans les élections de comité par approbation : la question ouverte #1 du multi-winner résolue — ancrage Peters (notre dépendance Lake) + pont core élections ↔ core coopératif #16848 (option B reportée) — fermeture candidate une fois Tranche 3 livrée.
• PR feat(social-choice,#16848): notebook 07-Committees-Core — core des elections de comite par approbation #16896 — carnet 07-Committees-Core.ipynb (option A livrée).
• PR fix(lean,#1453,#17756): Angel.lean + Angel_en.lean - header cleanup (revue ai-01 5324529283, tete e13c3f67a4) #17756 — nettoie le sorry framework de Angel.lean en Conway. Leçon : ne pas déclarer INTRINSIC ce qui n'est pas hors de Mathlib 4.
• Submodule upstream : DominikPeters/SocialChoiceLean rev 94a4c650b6.
• PetersTour.lean — visite guidée existante (couplage aux modules upstream).

🤖 Generated with Claude Code

[jsboige]

Tranche 0 livrée : PR #17995 (cadrage, 1 fichier +199). PR ouverte contre main, en attente re-review design. Claim inchangé, périmètre Tranches 1-3 suivra après acquittement du design.

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA -- Tranche 2 (#17988) : ApprovalCore.lean + ApprovalCore_en.lean (definition InCore, lemme d'identite, condition suffisante) + bump des globs lakefile.lean.

Reprise d'un claim stale : celui de myia-po-2024:CoursIA-2 (pose le 2026-09-26T22:13:54Z) a 190 h sans mouvement de fichier depuis. Tranche 1 (ApprovalDefs.lean, PR #18786) est mergee sur main (commit 987dd4f18791) ; l'issue ne l'enregistre dans aucun commentaire.

paths: MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalCore*.lean, MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean