Pref
plain-language theorem explainer
Pref is the Boolean type alias used for an agent's private preference in the Abilene paradox model, with true for stay and false for go. Decision theorists studying multi-agent σ-conservation violations would cite this when building agent records for group aggregation analysis. The declaration is a direct type abbreviation with no proof obligations.
Claim. Let $Pref$ denote the Boolean type, where $true$ stands for the preference to stay and $false$ for the preference to go.
background
The AbileneParadox module models the classic paradox as a σ-conservation violation on a small bilateral game tree. Each of n agents holds a private preference and casts a public vote; the per-agent σ-charge is the real difference between these two Booleans, so that collective σ-charge equals minus n under polite aggregation. The module replaces an earlier skeleton assertion of individual σ-cost with a derivation from the σ-conservation operator. Pref supplies the common Boolean carrier for both private_pref and public_vote fields inside the downstream Agent structure.
proof idea
One-line abbreviation that sets Pref to the Boolean type.
why it matters
Pref supplies the type for the Agent structure that records per-agent σ-mismatch. It therefore supports the module's derivation that truthful aggregation conserves σ while polite Abilene aggregation violates it by exactly n units. The construction sits inside Track A6 of the Recognition Science plan and applies the same σ operator used in the T0-T8 forcing chain and the Recognition Composition Law to decision-theoretic aggregation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.