truthfulStay
plain-language theorem explainer
truthfulStay defines the agent who privately prefers stay and publicly votes stay. Decision theorists modeling preference aggregation under the Abilene paradox cite it as the zero-mismatch baseline. The definition is a direct record construction from the Agent structure with both fields set to the stay preference.
Claim. The truthful stay agent is the record with private preference equal to stay and public vote equal to stay.
background
In this module each agent is a structure with private preference and public vote drawn from Pref (true denotes stay). The σ-charge is the real difference between private and public report, nonzero exactly when the agent misreports. The module derives the Abilene paradox from explicit σ-conservation violations on a small bilateral game tree rather than asserting costs, with truthful aggregation as the zero-violation case.
proof idea
One-line record construction that instantiates the Agent structure with private_pref and public_vote both set to true.
why it matters
This definition supplies the truthful baseline used by abilene_dichotomy, which proves that truthful aggregation yields σ-charge zero and J-cost zero while polite-Abilene aggregation yields n and n/4. It anchors the σ-conservation comparison in the Abilene setup and supports the claim that truthful reporting conserves σ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.