group_sigma_abilene
plain-language theorem explainer
A group of n Abilene agents, each privately preferring stay but publicly voting go, carries total σ-charge exactly n. Decision theorists deriving the Abilene paradox from σ-conservation cite this identity to quantify collective violation under polite aggregation. The proof runs by induction on n, applying the nil and cons recursion for group_sigma together with the unit per-agent mismatch and normalizing the arithmetic.
Claim. Let $G_n$ denote the list of $n$ Abilene agents, where each agent has private preference stay and public vote go. The group σ-charge of $G_n$ equals $n$.
background
The module models the Abilene paradox as a multi-agent σ-violation on a bilateral game tree. An agent is a structure carrying a private preference and a public vote; its σ-charge is the signed gap between them, yielding +1 precisely for the Abilene agent (private stay, public go). Group σ-charge is defined as the sum of individual charges, with the empty list giving zero and the cons case adding the head charge to the tail sum.
proof idea
The proof is by induction on n. The base case n=0 invokes group_sigma_nil. The successor step expands the replicated list with replicate_succ, decomposes the sum via group_sigma_cons, substitutes the unit value from Agent.sigma_abilene, applies the inductive hypothesis, casts to reals, and closes with ring.
why it matters
This supplies the σ-charge identity required by abilene_dichotomy (which contrasts polite versus truthful aggregation) and by abilene_paradox_one_statement (which packages the full paradox). It realizes the Track A6 derivation of the n-unit collective violation rather than an asserted constant. The result illustrates linear aggregation of σ-mismatch under polite rules inside the broader σ-conservation framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.