perAgentJCost_pos
plain-language theorem explainer
The theorem establishes that the per-agent J-cost for a silenced preference equals 1/4 and is therefore strictly positive. Decision theorists modeling the Abilene paradox in Recognition Science cite this when quantifying the total cost of polite aggregation across n agents. The proof is a one-line reduction to the known value of J(2) followed by numerical verification of the inequality.
Claim. The per-agent J-cost satisfies $0 < J(2)$, where $J$ denotes the Recognition Science cost function and each silenced preference contributes the doubling-step cost $J(2) = 1/4$.
background
In the Abilene paradox model, n agents each hold a private preference to stay but publicly vote to go under a polite aggregation rule. The σ-charge of an agent is the real-valued mismatch between private preference and public vote; every agent in the polite scenario has mismatch 1. The per-agent J-cost is defined as the Recognition cost function evaluated at argument 2, which equals the doubling-step identity J(2) = 1/4. This cost is the unit contribution to the collective σ-violation of the group. The module derives the paradox from the σ-conservation operator on a bilateral game tree rather than asserting costs by fiat. Upstream results supply the J-cost definition via the multiplicative recognizer and the explicit equality perAgentJCost = 1/4.
proof idea
The proof rewrites the target inequality using the upstream equality theorem that sets the per-agent J-cost to 1/4, then applies norm_num to confirm that 0 is strictly less than 1/4.
why it matters
This result supplies the concrete positive cost per silenced preference that the module uses to show polite aggregation produces a collective σ-violation of exactly n. It anchors the Abilene derivation in the J-cost framework (T5 J-uniqueness) and the Recognition Composition Law. The declaration closes the gap between the abstract σ-mismatch and the numerical cost that appears in the group-level accounting. No downstream uses are recorded yet, leaving open how the per-agent cost propagates into larger decision trees.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.