predicts
plain-language theorem explainer
The declaration asserts that the binary preference model for the Abilene paradox yields perfect linear correlation between per-agent σ-mismatches and collective charge violation. Decision theorists working in Recognition Science would cite it when mapping social aggregation failures to conservation operators. The statement is issued directly from the module definitions with no separate proof body or tactic steps supplied.
Claim. Under the binary preference model, each agent has a private preference and public vote in the set {stay, go}. The signed difference between them, cast to the reals, produces a collective σ-charge of exactly $-n$ for a group of $n$ agents that all misrepresent their preference, establishing perfect linear correlation between the number of silenced agents and the total violation.
background
The module treats the Abilene paradox as a multi-agent σ-violation on a small bilateral game tree. The agent structure consists of a private preference and a public vote, both drawn from the binary Pref type. The σ-charge is defined as the real-valued gap between these two reports: nonzero precisely when an agent misrepresents its preference.
proof idea
The declaration is issued as a direct statement with an empty proof body. It follows immediately from the per-agent σ definition and the uniform Abilene configuration in which every private preference is stay while every public vote is go.
why it matters
The result supplies the predictive claim for the decision track (A6 of Plan v5), replacing an earlier skeleton assertion with a derivation from the σ-conservation operator. It is referenced by downstream results on bond angles, periodic-table neutrality, J-cost phase transitions, dark-energy density, flatness tests, galaxy rotation profiles, and nucleosynthesis abundances. The placement ties the social-choice example to the broader J-cost and phi-ladder machinery imported via the Cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.