From 08ae5d89b83579296ab2ef3f90cb3aba24edd238 Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 2 Oct 2026 02:48:04 +0200 Subject: [PATCH 1/3] feat(lean,#17988): Tranche 1 -- ApprovalDefinitions Peters et agregat utility Tranche 1 du plan d'execution de l'issue #17988 (Becker-Greger-Peters 2026, arXiv 2609.11912) : poser le socle de definitions du core d'approbation au-dessus de SocialChoiceLean. * ApprovalBallot : sous-ensemble des candidats approuves par un votant * ApprovalProfile : collection de ballots indexee par votants + taille du comite * Committee : sous-ensemble de candidats de cardinalite fixee k * Happiness : cardinal de l'intersection approbation x comite (utilite additive) * PaymentFunction : vecteur de paiements aux votants, somme nulle * ApprovalAggregateUtility : somme ponderee des bonheurs (proxy sans logarithme pour HarmonicEntropy) Le proxy est documente en Tranche 1 : il suffit pour les lemmes techniques de Tranche 2 (monotonie, concavite) qui ne dependent pas du log lui-meme. HarmonicEntropy avec log viendra en Tranche 3. Lake build : nouveau lean_lib ApprovalDefs avec globs FR + EN explicites (orphan-trap #6749). Convention i18n #4980 : 2/2 pairs byte-identical (ApprovalDefs / ApprovalDefs_en), 0 drift, 0 orphan. Verifie par scripts/lean/check_i18n_siblings.py. Compte sorry reel : 0 (avant et apres). Validation par scripts/lean/count_code_sorry.py --json. References : #17988, arXiv 2609.11912. See #17988 --- .../ApprovalDefs.lean | 78 +++++++++++++++++++ .../ApprovalDefs_en.lean | 77 ++++++++++++++++++ .../social_choice_lean_peters/lakefile.lean | 11 +++ 3 files changed, 166 insertions(+) create mode 100644 MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean create mode 100644 MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean new file mode 100644 index 0000000000..1783865f74 --- /dev/null +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean @@ -0,0 +1,78 @@ +/- + Socle de définitions — Core d'approbation (Becker-Greger-Peters 2026) + ===================================================================== + + Ce fichier pose les structures et fonctions de base pour la formalisation + du core d'approbation, conformément au résultat de Becker, Greger et + Peters (2026), arXiv 2609.11912. + + Tranche 1 du plan d'exécution de l'issue #17988 : + - `ApprovalBallot` — sous-ensemble des candidats approuvés par un votant + - `ApprovalProfile` — collection de ballots indexée par votants + taille comité + - `Committee` — sous-ensemble de candidats de cardinalité fixée `k` + - `Happiness` — utilité additive (cardinal de l'intersection approbation × comité) + - `PaymentFunction` — vecteur de paiements aux votants, somme nulle + - `ApprovalAggregateUtility` — somme pondérée des bonheurs (proxy sans logarithme) + + Les définitions de `Core` (Tranche 2) et le théorème principal (Tranche 3) + vivent dans des fichiers séparés `ApprovalCore.lean` (Tranche 2) et + `ApprovalBGP2026.lean` (Tranche 3). + + Convention i18n #4980 : ce fichier porte le namespace `ApprovalDefs` (FR). + Le sibling `ApprovalDefs_en.lean` porte le namespace `ApprovalDefs_en` (EN). + Préservation byte-identity hors docstrings — vérifiée par + `scripts/lean/check_i18n_siblings.py`. +-/ + +import SocialChoice.Profile + +namespace ApprovalDefs + +/-- Un ballot d'approbation : sous-ensemble des candidats approuvés par un votant. -/ +structure ApprovalBallot (A : Type) [Fintype A] where + approved : Finset A + +/-- Un profil d'approbation : collection de ballots indexée par votants, + avec une taille de comité cible. -/ +structure ApprovalProfile (V A : Type) [Fintype V] [Fintype A] where + ballots : V → ApprovalBallot A + committeeSize : ℕ + +/-- Un comité : sous-ensemble de candidats de cardinalité fixée `k`. -/ +def Committee (A : Type) [Fintype A] (k : ℕ) : Type := + { S : Finset A // S.card = k } + +/-- Bonheur d'un votant `v` sous un comité `S` : nombre de candidats + approuvés par `v` qui sont dans `S`. -/ +def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] + (P : ApprovalProfile V A) (S : Committee A P.committeeSize) + (v : V) : ℕ := + (P.ballots v).approved ∩ S.val |>.card + +/-- Fonction de paiement : vecteur de paiements aux votants, contraints à + somme nulle (les paiements transfèrent de l'argent aux votants, financés + par un budget total nul). -/ +structure PaymentFunction (V : Type) [Fintype V] where + payments : V → ℚ + zero_sum : (∑ v, payments v) = 0 + +/-- Utilité agrégée d'approbation : somme pondérée des bonheurs individuels, + où le coefficient de chaque votant est `1 / (1 + p.v)` (interprétation : + un paiement positif réduit le poids du votant, un paiement négatif + l'augmente — c'est la **base** de la fonction objectif de BGP 2026 sans + le logarithme). + + Cette définition sert de **proxy** à `HarmonicEntropy` (qui introduira le + logarithme via `Mathlib.Analysis.SpecialFunctions.Log` à la Tranche 3). + Le proxy est suffisant pour exprimer les lemmes techniques de Tranche 2 + (monotonie, concavité) qui ne dépendent pas du log lui-même. + + Les poids sont strictement positifs dès lors que `p.v > -1` (hypothèse + que la Tranche 2 documentera comme standard pour les paiements + budgétairement neutres). -/ +def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] + (P : ApprovalProfile V A) (S : Committee A P.committeeSize) + (p : PaymentFunction V) : ℚ := + ∑ v, (1 : ℚ) / (1 + p.payments v) * (Happiness P S v : ℚ) + +end ApprovalDefs \ No newline at end of file diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean new file mode 100644 index 0000000000..40e80e56f1 --- /dev/null +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean @@ -0,0 +1,77 @@ +/- + Definitions core — Approval core (Becker-Greger-Peters 2026) + ============================================================ + + This file lays out the basic structures and functions for the formalisation + of the approval core, following the result by Becker, Greger and Peters + (2026), arXiv 2609.11912. + + Tranche 1 of the execution plan for issue #17988 : + - `ApprovalBallot` — subset of approved candidates per voter + - `ApprovalProfile` — collection of ballots indexed by voters + committee size + - `Committee` — subset of candidates of fixed cardinality `k` + - `Happiness` — additive utility (cardinal of approval × committee intersection) + - `PaymentFunction` — payment vector to voters, zero sum + - `ApprovalAggregateUtility` — weighted sum of individual happinesses (no logarithm) + + The `Core` definitions (Tranche 2) and the main theorem (Tranche 3) live + in separate files `ApprovalCore.lean` (Tranche 2) and `ApprovalBGP2026.lean` + (Tranche 3). + + i18n convention #4980: this file carries the namespace `ApprovalDefs_en` + (EN). The sibling `ApprovalDefs.lean` carries `ApprovalDefs` (FR). + Byte-identity preserved except docstrings — verified by + `scripts/lean/check_i18n_siblings.py`. +-/ + +import SocialChoice.Profile + +namespace ApprovalDefs_en + +/-- An approval ballot: subset of candidates approved by a voter. -/ +structure ApprovalBallot (A : Type) [Fintype A] where + approved : Finset A + +/-- An approval profile: collection of ballots indexed by voters, with + a target committee size. -/ +structure ApprovalProfile (V A : Type) [Fintype V] [Fintype A] where + ballots : V → ApprovalBallot A + committeeSize : ℕ + +/-- A committee: subset of candidates of fixed cardinality `k`. -/ +def Committee (A : Type) [Fintype A] (k : ℕ) : Type := + { S : Finset A // S.card = k } + +/-- Happiness of a voter `v` under a committee `S`: the number of candidates + approved by `v` that lie in `S`. -/ +def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] + (P : ApprovalProfile V A) (S : Committee A P.committeeSize) + (v : V) : ℕ := + (P.ballots v).approved ∩ S.val |>.card + +/-- Payment function: vector of payments to voters, constrained to zero sum + (payments transfer money to voters, financed by a total zero budget). -/ +structure PaymentFunction (V : Type) [Fintype V] where + payments : V → ℚ + zero_sum : (∑ v, payments v) = 0 + +/-- Aggregate approval utility: weighted sum of individual happinesses, + where each voter's coefficient is `1 / (1 + p.v)` (interpretation: a + positive payment reduces the voter's weight, a negative payment raises + it — the **base** of the BGP 2026 objective function without the + logarithm). + + This definition serves as a **proxy** for `HarmonicEntropy` (which will + introduce the logarithm via `Mathlib.Analysis.SpecialFunctions.Log` in + Tranche 3). The proxy is sufficient to express the technical lemmas of + Tranche 2 (monotonicity, concavity) that do not depend on the log + itself. + + The weights are strictly positive whenever `p.v > -1` (an assumption + Tranche 2 will document as standard for budget-neutral payments). -/ +def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] + (P : ApprovalProfile V A) (S : Committee A P.committeeSize) + (p : PaymentFunction V) : ℚ := + ∑ v, (1 : ℚ) / (1 + p.payments v) * (Happiness P S v : ℚ) + +end ApprovalDefs_en \ No newline at end of file diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean index 87f6b59a1d..7c1e1e9e39 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean @@ -38,3 +38,14 @@ lean_lib «PetersTour» where -- aussi : sans cela, PetersTour_en.lean n'est jamais élaboré et un Lean CI -- vert est un faux pass (orphan-trap #6749). Même pattern que sudoku_lean. globs := #[`PetersTour, `PetersTour_en] + +/- + Tranche 1 du plan #17988 (issue parente) — socle de définitions du core + d'approbation (Becker-Greger-Peters 2026, arXiv 2609.11912). + + `ApprovalDefs` (FR) et `ApprovalDefs_en` (EN) forment une paire i18n #4980 + (sibling byte-identical hors commentaires). Le glob EN est explicite pour + éviter l'orphan-trap #6749. Voir `scripts/lean/check_i18n_siblings.py`. +-/ +lean_lib «ApprovalDefs» where + globs := #[`ApprovalDefs, `ApprovalDefs_en] From 54a7a4d9fe555772c596bb16ce5eee89ec2e9e1d Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 3 Oct 2026 15:55:43 +0200 Subject: [PATCH 2/3] fix(lean,#17988): retirer la promesse de concavite (contre-exemple p=(a,-a), c.5969321192) + zero_sum n'implique pas p.v>-1 Docstrings only, code byte-identique (i18n checker 2/2 pairs, 0 drift) : - concavite remplacee par monotonie en la composition du comite + contre-exemple documente - positivite des poids : hypothese p.v > -1 explicite, zero_sum seul ne l'implique pas - body : faisabilite 1 <= k <= |A| au plan Tranche 3 + B.3 non-applicable ecrit + run Lean CI cite Co-Authored-By: Claude Sonnet 5.5 --- .../social_choice_lean_peters/ApprovalDefs.lean | 14 ++++++++++---- .../ApprovalDefs_en.lean | 15 +++++++++++---- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean index 1783865f74..fd0de12289 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean @@ -65,11 +65,17 @@ structure PaymentFunction (V : Type) [Fintype V] where Cette définition sert de **proxy** à `HarmonicEntropy` (qui introduira le logarithme via `Mathlib.Analysis.SpecialFunctions.Log` à la Tranche 3). Le proxy est suffisant pour exprimer les lemmes techniques de Tranche 2 - (monotonie, concavité) qui ne dépendent pas du log lui-même. + (monotonie en la composition du comité) qui ne dépendent pas du log + lui-même. - Les poids sont strictement positifs dès lors que `p.v > -1` (hypothèse - que la Tranche 2 documentera comme standard pour les paiements - budgétairement neutres). -/ + Aucune concavité n'est promise dans la dimension des paiements : pour + deux votants de bonheurs égaux et `p = (a, -a)`, l'agrégat vaut + `1/(1+a) + 1/(1-a)`, soit 2 en `a = 0` et 8/3 en `a = ±1/2` — convexe, + pas concave (contre-exemple mesuré en arithmétique exacte c.5969321192). + + Les poids sont strictement positifs dès lors que `p.v > -1`. La + contrainte `zero_sum` seule ne l'implique pas (`p = (-2, 2)` est de + somme nulle) ; la Tranche 2 posera `p.v > -1` comme hypothèse explicite. -/ def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (p : PaymentFunction V) : ℚ := diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean index 40e80e56f1..80f3789e9e 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean @@ -64,11 +64,18 @@ structure PaymentFunction (V : Type) [Fintype V] where This definition serves as a **proxy** for `HarmonicEntropy` (which will introduce the logarithm via `Mathlib.Analysis.SpecialFunctions.Log` in Tranche 3). The proxy is sufficient to express the technical lemmas of - Tranche 2 (monotonicity, concavity) that do not depend on the log - itself. + Tranche 2 (monotonicity in committee composition) that do not depend on + the log itself. - The weights are strictly positive whenever `p.v > -1` (an assumption - Tranche 2 will document as standard for budget-neutral payments). -/ + No concavity is claimed in the payment dimension: for two voters with + equal happiness and `p = (a, -a)`, the aggregate equals + `1/(1+a) + 1/(1-a)`, i.e. 2 at `a = 0` and 8/3 at `a = ±1/2` — convex, + not concave (counter-example measured in exact arithmetic, see review + c.5969321192). + + The weights are strictly positive whenever `p.v > -1`. The `zero_sum` + constraint alone does not imply it (`p = (-2, 2)` sums to zero); + Tranche 2 will state `p.v > -1` as an explicit assumption. -/ def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (p : PaymentFunction V) : ℚ := From 821ada4174791def5bd3a6808e5c19e0045284dc Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 3 Oct 2026 21:31:59 +0200 Subject: [PATCH 3/3] fix(lean,#18786): elabore ApprovalDefs (cible + imports Mathlib + DecidableEq) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Trois corrections source pour permettre a `lake -R build ApprovalDefs` de verifier reellement le module (sans cible, le CI vert n'elaborait que `PetersTour` et masquait l'absence de compilation du nouveau socle). 1. `@[default_target]` pose sur `lean_lib «ApprovalDefs»` dans lakefile.lean : le module est desormais elabore par `lake build` par defaut (parallelement a PetersTour). 2. Imports Mathlib dans ApprovalDefs.lean et ApprovalDefs_en.lean : le code reference `Finset`, `Fintype`, `ℚ`, `BigOperators` mais n'importait que `SocialChoice.Profile`. La resolution de type class echouait en cascade (`Unknown identifier ℚ`, `failed to synthesize Inter (Finset A)`). 3. `DecidableEq A` ajoute sur `Happiness` et `ApprovalAggregateUtility` : `Finset.filter` exige `DecidablePred` (donc `DecidableEq A`), et la coercition `(Happiness P S v : ℚ)` propage la meme contrainte. Substitution locale `∩` -> `filter (fun x => x ∈ S.val)` : la notation `∩` repose sur `Inter` via Lattice, qui exige un ordre partiel sur les elements ; `filter` est plus direct et n'impose que DecidableEq. Verifications : - `lake -R build ApprovalDefs` -> Build completed successfully (792 jobs) - ApprovalDefs et ApprovalDefs_en compiles, 0 sorry dans les deux fichiers - Convention i18n #4980 preservee (imports identiques dans les deux siblings) Refs #18786, #17988, Tell c.anti-regression fondateur, Tell c.16765 strict. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../social_choice_lean_peters/ApprovalDefs.lean | 12 +++++++++--- .../social_choice_lean_peters/ApprovalDefs_en.lean | 12 +++++++++--- .../social_choice_lean_peters/lakefile.lean | 1 + 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean index fd0de12289..c89c3015d0 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean @@ -25,6 +25,12 @@ -/ import SocialChoice.Profile +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.Lattice.Basic +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.Rat.Cast.Defs +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Order.Lattice namespace ApprovalDefs @@ -44,10 +50,10 @@ def Committee (A : Type) [Fintype A] (k : ℕ) : Type := /-- Bonheur d'un votant `v` sous un comité `S` : nombre de candidats approuvés par `v` qui sont dans `S`. -/ -def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] +def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] [DecidableEq A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (v : V) : ℕ := - (P.ballots v).approved ∩ S.val |>.card + ((P.ballots v).approved).filter (fun x => x ∈ S.val) |>.card /-- Fonction de paiement : vecteur de paiements aux votants, contraints à somme nulle (les paiements transfèrent de l'argent aux votants, financés @@ -76,7 +82,7 @@ structure PaymentFunction (V : Type) [Fintype V] where Les poids sont strictement positifs dès lors que `p.v > -1`. La contrainte `zero_sum` seule ne l'implique pas (`p = (-2, 2)` est de somme nulle) ; la Tranche 2 posera `p.v > -1` comme hypothèse explicite. -/ -def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] +def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] [DecidableEq A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (p : PaymentFunction V) : ℚ := ∑ v, (1 : ℚ) / (1 + p.payments v) * (Happiness P S v : ℚ) diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean index 80f3789e9e..ebaefa3233 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean @@ -25,6 +25,12 @@ -/ import SocialChoice.Profile +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.Lattice.Basic +import Mathlib.Data.Fintype.Basic +import Mathlib.Data.Rat.Cast.Defs +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Order.Lattice namespace ApprovalDefs_en @@ -44,10 +50,10 @@ def Committee (A : Type) [Fintype A] (k : ℕ) : Type := /-- Happiness of a voter `v` under a committee `S`: the number of candidates approved by `v` that lie in `S`. -/ -def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] +def Happiness {V A : Type} [instV : Fintype V] [instA : Fintype A] [DecidableEq A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (v : V) : ℕ := - (P.ballots v).approved ∩ S.val |>.card + ((P.ballots v).approved).filter (fun x => x ∈ S.val) |>.card /-- Payment function: vector of payments to voters, constrained to zero sum (payments transfer money to voters, financed by a total zero budget). -/ @@ -76,7 +82,7 @@ structure PaymentFunction (V : Type) [Fintype V] where The weights are strictly positive whenever `p.v > -1`. The `zero_sum` constraint alone does not imply it (`p = (-2, 2)` sums to zero); Tranche 2 will state `p.v > -1` as an explicit assumption. -/ -def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] +def ApprovalAggregateUtility {V A : Type} [instV : Fintype V] [instA : Fintype A] [DecidableEq A] (P : ApprovalProfile V A) (S : Committee A P.committeeSize) (p : PaymentFunction V) : ℚ := ∑ v, (1 : ℚ) / (1 + p.payments v) * (Happiness P S v : ℚ) diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean index 7c1e1e9e39..6c34938564 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean @@ -47,5 +47,6 @@ lean_lib «PetersTour» where (sibling byte-identical hors commentaires). Le glob EN est explicite pour éviter l'orphan-trap #6749. Voir `scripts/lean/check_i18n_siblings.py`. -/ +@[default_target] lean_lib «ApprovalDefs» where globs := #[`ApprovalDefs, `ApprovalDefs_en]