perAgentJCost
plain-language theorem explainer
Defines the unit per-agent σ-mismatch cost in the Abilene model as the Recognition Science J-function evaluated at 2. Decision theorists modeling group preference violations cite this base unit when summing collective costs over n agents. The definition is a direct one-line reference to the upstream cost constructor at the doubling argument.
Claim. The unit per-agent cost is defined as $J(2)$, where $J$ is the Recognition Science cost function satisfying the doubling-step identity $J(2) = 1/4$.
background
The Abilene Paradox module encodes agents as records with private_pref and public_vote fields. The σ operator measures mismatch as a real number, yielding σ = 1 for each agent in the polite-Abilene pattern and collective charge n for a group of n agents. This replaces v4 literal cost assignments with a derivation from the σ-conservation operator on the game tree.
proof idea
This is a one-line definition that applies the Cost.Jcost function to the argument 2.
why it matters
This supplies the base unit for the collective J-cost of an n-agent group and for the AbileneParadoxCert structure that certifies the eight paradox clauses from σ-charge. It implements the v5 replacement of the skeleton's literal 1/φ cost with a derivation from the J-function, connecting to T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.