truthful_strictly_improves
plain-language theorem explainer
In the Abilene paradox model, truthful aggregation yields zero collective J-cost for any group of n ≥ 1 agents while polite aggregation produces strictly positive cost. A decision theorist working in Recognition Science would cite this to quantify the penalty of preference misrepresentation. The proof is a one-line term application of the positivity theorem for the collective cost function.
Claim. For every positive integer $n$, the collective J-cost of a polite-Abilene group of $n$ agents is strictly positive, where this cost equals $n$ times the per-agent contribution $J(2) = 1/4$.
background
The module models the Abilene paradox as a multi-agent σ-violation on a bilateral game tree. Each agent is an object with private preference (stay) and public vote (go) under polite aggregation; the σ-charge of an agent is the real difference between private and public values, so the collective σ-charge equals −n. The J-cost is obtained from the cost function of a multiplicative recognizer via the Recognition Composition Law, with each silenced preference contributing exactly J(2) = 1/4; the collective cost is therefore the linear sum n/4. Upstream results supply the positivity of this linear expression once n > 0 and the definition of cost as the derived comparator cost on positive ratios.
proof idea
The declaration is a one-line term proof that directly invokes the positivity theorem abileneCollectiveJCost_pos on the hypothesis 0 < n.
why it matters
The result supplies the strict-improvement half of the dichotomy stated in the module’s §5, confirming that truthful aggregation σ-conserves with zero J-cost while polite aggregation violates conservation by exactly n units. It anchors the decision-theoretic track to the same J-function used for physical constants and the forcing chain (T5–T8), and closes the v4 skeleton that had asserted individual costs without derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.