AbileneParadoxCert
plain-language theorem explainer
AbileneParadoxCert packages eight properties that certify zero σ-charge for truthful agents, unit σ-charge for each Abilene-pattern agent, linear scaling of group σ-charge, and collective J-cost of n/4 with strict positivity. Decision modelers working on preference aggregation under σ-conservation cite it to replace earlier asserted costs with operator-derived values. It is introduced as a record type whose fields are later instantiated by lemmas on the sigma operator and Cost.Jcost.
Claim. A structure whose fields assert: for any agent $a$, private preference equals public vote implies σ-charge of $a$ is zero; σ-charge of the Abilene agent equals 1; any truthful group has group σ-charge zero; a group of $n$ Abilene agents has group σ-charge $n$; per-agent J-cost equals $J(2)$; collective J-cost of $n$ agents equals $n/4$; collective J-cost is strictly positive for $n>0$; and collective J-cost strictly exceeds the truthful baseline of zero for $n>0$.
background
The module encodes the Abilene paradox as a multi-agent σ-violation on a bilateral game tree. Each agent is a record with private preference and public vote (true for stay). The σ-charge is the signed mismatch: +1 when an agent privately prefers stay but votes go, zero when reports match. Group σ-charge is the sum of individual charges. Per-agent J-cost is defined as Cost.Jcost 2, which equals 1/4, and collective J-cost scales as n times that value. The module states: 'The σ-charge of an agent is σ(a) := (private_pref - public_vote) cast to ℝ : non-zero precisely when the agent has misrepresented their preference.' Truthful aggregation conserves σ while polite aggregation violates it by exactly n units.
proof idea
The declaration is a structure definition that simply lists the eight properties as fields. Instantiation occurs downstream in abileneParadoxCert, which supplies the concrete lemmas Agent.sigma_truthful for the zero case, group_sigma_abilene for the scaling, and rfl for the Jcost equality.
why it matters
It supplies the master certificate for the Abilene paradox in the Decision track (A6 of Plan v5), replacing the v4 skeleton's literal 1/φ cost with a derivation from the σ operator and Cost.Jcost. It is used by abileneParadoxCert. In the Recognition framework it demonstrates how σ-mismatch produces J-cost in collective choice, with the per-agent term tied to the doubling step of the J function. It touches the modeling of preference misrepresentation under conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.