sigma_truthfulGo
plain-language theorem explainer
The σ-charge operator returns zero on the truthfulGo agent, establishing the baseline case of no misrepresentation cost when private preference matches public vote. Decision theorists working on preference aggregation and collective action problems would cite this as the zero-violation reference point. The proof is a one-line wrapper that unfolds the sigma definition and normalizes the resulting arithmetic.
Claim. Let truthfulGo be the agent with private preference go and public vote go. Let σ(a) be the real-valued charge (private indicator minus public indicator). Then σ(truthfulGo) = 0.
background
In this module the Abilene Paradox is recast as a σ-conservation violation on a bilateral preference game. An Agent is a structure carrying a private preference (Pref) and a public vote (Pref). The sigma function computes the charge as (1 if private_pref is stay else 0) minus (1 if public_vote is stay else 0), so that truthful reporting yields zero charge while misrepresentation yields ±1. The truthfulGo constant is the concrete agent whose private and public fields are both go (false). Upstream results supply the Agent structure and the sigma definition; the module itself derives the collective violation of n units under polite aggregation from these per-agent charges.
proof idea
The proof is a one-line wrapper that unfolds sigma on truthfulGo and applies numeric normalization to the resulting difference of indicators.
why it matters
This theorem supplies the zero baseline required to contrast truthful aggregation (collective σ-charge zero) with the Abilene polite aggregation (collective σ-charge −n). It therefore anchors the module's claim that the paradox is a derived σ-violation rather than an asserted cost. The result sits inside the broader Recognition Science program of enforcing conservation laws, here applied to decision structures rather than physical fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.