abileneCollectiveJCost_pos
plain-language theorem explainer
Researchers modeling multi-agent preference aggregation cite this result to confirm that polite-Abilene groups incur strictly positive collective J-cost for any non-empty group. The positivity follows from the linear cost expression derived from per-agent J(2). The short tactic proof rewrites via the equality lemma then applies linear arithmetic to the positive real cast of n.
Claim. For every positive integer $n$, the collective J-cost of an n-agent polite-Abilene group satisfies $0 < n/4$.
background
In the Abilene Paradox module, n agents each hold private preference stay but vote go under polite aggregation, producing per-agent σ-mismatch of 1 and collective σ-charge n. The collective J-cost is defined as n times perAgentJCost, where the upstream equality abileneCollectiveJCost_eq shows this equals n/4 because perAgentJCost = J(2) = 1/4. The cost function itself is the J-cost of a recognition event, taken from the ObserverForcing and MultiplicativeRecognizerL4 modules.
proof idea
The tactic proof first rewrites the goal with abileneCollectiveJCost_eq, reducing it to 0 < (n : ℝ)/4. It then proves (0 : ℝ) < (n : ℝ) by exact_mod_cast on the hypothesis 0 < n, and finishes with linarith.
why it matters
The result is invoked directly by abilene_dichotomy to supply the cost component of the polite-Abilene case and by abilene_paradox_one_statement to include positivity in the three-fact summary of the paradox. Within Recognition Science it quantifies the defect cost of σ-violation using the J-cost induced by the multiplicative recognizer, supporting the strict improvement of truthful aggregation over the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.