abileneParadoxCert
plain-language theorem explainer
The declaration defines a bundled certificate packaging eight properties of the Abilene paradox expressed via the σ-charge operator and collective J-cost. Decision theorists applying Recognition Science to multi-agent preference aggregation would cite it to replace earlier literal cost assignments with derived facts. The definition assembles the record by direct field assignment to per-agent σ lemmas, group summation theorems, and the collective cost positivity result.
Claim. The Abilene paradox certificate is the structure whose fields assert: for any agent $a$, if private preference equals public vote then its σ-charge is zero; the Abilene-pattern agent has σ-charge one; any truthful group has collective σ-charge zero; an $n$-agent Abilene group has collective σ-charge $n$; per-agent J-cost equals $J(2)$; collective J-cost for $n$ agents equals $n/4$; collective J-cost is strictly positive for $n>0$; and the cost dichotomy holds for positive group size.
background
In the Abilene paradox module agents are structures pairing a private preference (stay or go) with a public vote. The σ-charge of an agent is the real difference between these two values, hence nonzero precisely when the agent misrepresents its preference. The module encodes the classic Abilene setup in which every agent privately prefers stay yet publicly votes go under a polite aggregation rule, yielding collective σ-charge exactly $n$ for an $n$-agent group. This replaces the v4 skeleton's asserted per-agent cost $1/φ$ with derivations from the σ-operator and the J-cost function supplied by the Cost module. Upstream results include the theorem that collective J-cost equals $n/4$ (proved by unfolding and ring simplification) and the strict positivity theorem for positive $n$ (proved by rewriting to the closed form and linarith).
proof idea
The definition constructs the AbileneParadoxCert record by assigning each field to an existing lemma or definition in the same module. sigma_truthful_zero is set to Agent.sigma_truthful, sigma_abilene_one to Agent.sigma_abilene, group_sigma_truthful to the equality theorem group_sigma_truthful_eq_zero, group_sigma_abilene_eq_n to group_sigma_abilene, per_agent_cost_eq_J2 to rfl, collective_cost_eq to abileneCollectiveJCost_eq, and cost_strict_pos to abileneCollectiveJCost_pos. The final dichotomy clause is proved inline by applying the positivity theorem and discharging the resulting inequality with linarith.
why it matters
This definition supplies the master certificate for the Abilene paradox in the decision module, bundling all σ-charge and J-cost facts derived from the per-agent operator. It directly replaces the v4 skeleton's literal cost assignment and thereby closes the derivation of the paradox from σ-conservation on the bilateral game tree. The certificate supports downstream applications of Recognition Science to multi-agent decision problems in which polite aggregation produces measurable σ-violations. It does not connect to the T0-T8 forcing chain or the Recognition Composition Law, leaving open whether the same σ-cost structure appears in other decision domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.