group_sigma_nil
plain-language theorem explainer
The summation operator for group σ-charge returns zero on the empty list of agents. Decision theorists modeling preference misrepresentation cite this base case when inducting over group size in aggregation paradoxes such as Abilene. The proof is a one-line term wrapper that unfolds the list-sum definition and reduces the empty sum via simplification.
Claim. The σ-charge of the empty collection of agents is zero: $group_σ(∅) = 0$, where $group_σ(A) = ∑_{a∈A} σ(a)$ and $σ(a)$ is the real difference between an agent's private preference and public vote.
background
In the Abilene model each agent is a record with private preference and public vote (both Boolean). The individual σ-charge equals the real difference between these values and is nonzero exactly when the agent misrepresents its preference. The group σ-charge is defined as the sum of the individual charges over any finite list of agents.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of group_sigma (the sum of mapped individual σ values) and applies simp to reduce the empty-list sum to zero.
why it matters
This zero element anchors the inductive arguments in the downstream theorems group_sigma_abilene (all-Abilene group of n agents carries charge n) and group_sigma_truthful_eq_zero (truthful groups carry charge zero). It supplies the identity for the σ-conservation operator in the Abilene derivation of Track A6, where truthful aggregation conserves charge while polite aggregation violates it by exactly the number of agents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.