abileneCollectiveJCost_succ
plain-language theorem explainer
The theorem establishes that collective J-cost of a polite-Abilene group increases by exactly 1/4 with each added agent. Decision theorists modeling σ-mismatch in preference aggregation would cite this when summing per-agent contributions to total violation. The proof is a direct algebraic reduction that substitutes the closed-form collective cost twice and simplifies the resulting arithmetic identity.
Claim. Let $C(n)$ be the collective J-cost of a polite-Abilene group of $n$ agents. Then $C(n+1) = C(n) + 1/4$ for every natural number $n$.
background
The Abilene module encodes each agent as a pair of private preference and public vote, with σ-charge nonzero precisely on misrepresentation. Collective J-cost is defined as $n$ times the per-agent J-cost, where the per-agent term equals $1/4$ by the upstream equality that unfolds the definition and applies the quarter-cost identity from the multiplicative recognizer. Upstream results supply the J-cost of a recognition event as the derived cost on positive ratios and the active-edge count $A$ that anchors the φ-power balance at three dimensions.
proof idea
The proof applies the closed-form equality for collective J-cost to both sides, casts the successor natural number to a real, and reduces the arithmetic by ring.
why it matters
This fills the linear-growth step inside the Abilene collective-cost derivation, supporting the claim that σ-violation scales directly with group size under polite aggregation. It belongs to the Decision domain and rests on the J-cost definitions from ObserverForcing and MultiplicativeRecognizerL4. The result precedes the truth-telling enforcement section that shows the cost vanishes when every agent reports its private preference honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.