feat(lean,#17988): Tranche 1 -- ApprovalDefinitions Peters (socle core approbation BGP 2026)

MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs.lean

@@ -0,0 +1,90 @@
+/-
+  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
+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
+
+/-- 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] [DecidableEq A]
+    (P : ApprovalProfile V A) (S : Committee A P.committeeSize)
+    (v : V) : ℕ :=
+  ((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
+    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 en la composition du comité) qui ne dépendent pas du log
+    lui-même.
+
+    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] [DecidableEq 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

MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/ApprovalDefs_en.lean

@@ -0,0 +1,90 @@
+/-
+  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
+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
+
+/-- 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] [DecidableEq A]
+    (P : ApprovalProfile V A) (S : Committee A P.committeeSize)
+    (v : V) : ℕ :=
+  ((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). -/
+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 in committee composition) that do not depend on
+    the log itself.
+
+    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] [DecidableEq 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

MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/lakefile.lean

@@ -38,3 +38,15 @@ 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`.
+-/
+@[default_target]
+lean_lib «ApprovalDefs» where
+  globs := #[`ApprovalDefs, `ApprovalDefs_en]