Agent
plain-language theorem explainer
The Agent structure pairs a private preference with a public vote, each a binary choice between stay and go. Decision theorists deriving collective violations from individual preference misrepresentation cite this record when summing per-agent σ-charges. It is introduced directly as a record type with decidable equality and representation.
Claim. An agent is a pair $(p, v)$ where $p, v$ each belong to the set of binary preferences (stay or go).
background
Pref is the abbrev for Bool with true denoting stay and false denoting go. The module models the Abilene paradox on a bilateral game tree: each of n agents holds private_pref = stay yet believes others prefer go, so all cast public_vote = go under a polite rule. The σ-charge of an agent is the signed mismatch (private_pref - public_vote) cast to reals, nonzero exactly on misrepresentation. Upstream results supply the reversal map on Fin 8 and the gap product of closure and Fibonacci factors, but the local setting centers on σ-conservation: truthful reporting yields collective charge zero while polite-Abilene yields charge n.
proof idea
one-line wrapper that defines the record type Agent with fields private_pref and public_vote of type Pref.
why it matters
Agent supplies the atomic object for the AbileneParadoxCert and the abilene_dichotomy theorem, which derive group_sigma = n and collective J-cost = n/4 for polite aggregation versus zero for truthful aggregation. This fills the Track A6 derivation of the paradox from the σ-conservation operator, replacing the v4 skeleton's asserted per-agent cost 1/φ with quantities obtained from Cost.Jcost. It anchors the one-statement theorem that truthful aggregation is strictly superior on both σ-charge and J-cost axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.