group_sigma_cons
plain-language theorem explainer
The declaration states that prepending an agent to a list adds its individual σ-charge to the group total. Modelers of collective preference misrepresentation cite it when inducting over agent lists in bilateral games. The proof is a one-line wrapper that unfolds the sum definition and applies simplification.
Claim. For any agent $a$ and list of agents $as$, the group σ-charge satisfies $group_σ(a :: as) = σ(a) + group_σ(as)$, where $σ(a)$ equals the difference between the agent's private preference indicator and public vote indicator.
background
The Abilene Paradox module encodes agents as structures holding a private preference and a public vote, both of type Pref. The per-agent σ-charge is the real-valued gap (private_pref indicator minus public_vote indicator), nonzero exactly when the agent misreports. Group σ-charge is defined as the sum of these individual charges over a list of agents. The module derives the paradox from σ-conservation failure under polite aggregation versus truthful reporting, where the latter yields zero collective charge.
proof idea
The proof unfolds the group_sigma definition (map sigma then sum) then applies simp to reduce the cons case directly to addition of the head term.
why it matters
It supplies the cons case required by the two immediate downstream theorems: group_sigma_abilene (all-Abilene lists carry charge exactly n) and group_sigma_truthful_eq_zero (truthful lists carry charge zero). The result therefore closes the recursive step that converts per-agent misrepresentation into a quantifiable σ-violation of size n, completing the derivation promised in the module's Track A6 setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.