sigma_truthful
plain-language theorem explainer
The declaration shows that an agent's σ-charge is zero when private preference equals public vote. Decision theorists working on preference aggregation under the Abilene paradox cite it to establish the truthful baseline. The proof is a direct algebraic reduction that unfolds the sigma definition, substitutes the hypothesis, and simplifies with ring.
Claim. For any agent $a$ with private preference equal to public vote, the charge satisfies $σ(a)=0$.
background
In this module each agent is a structure with fields private_pref and public_vote, both of type Pref. The charge operator sigma is defined by subtracting the indicator of the public vote from the indicator of the private preference, yielding +1, -1 or 0. The module derives the Abilene paradox from σ-conservation on a small bilateral game tree, replacing earlier skeleton assertions with explicit per-agent mismatch arithmetic.
proof idea
The term proof unfolds the local definition of sigma, rewrites the resulting expression with the supplied hypothesis, and closes with the ring tactic.
why it matters
This supplies the zero-charge case required by abileneParadoxCert and by the extension group_sigma_truthful_eq_zero. It anchors the truth-telling baseline against which the module measures the collective σ-violation of n polite agents. The result fills the truthful half of the σ-conservation comparison that replaces the v4 skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.