generated_cost_formula
plain-language theorem explainer
Any ratio character generates a cost whose rational display is exactly the classical J-formula at the character image: (χ(q)+χ(q)⁻¹)/2−1. Continuum-forcing arguments that lift discrete characters to the unique J-cost on the real completion cite this identity. The proof is a one-line application of the character-cost rationalization lemma.
Claim. For every character $\chi$ on ratio orbits and every ratio orbit $q$, the rational display of the cost generated by $\chi$ at $q$ equals $\frac{\chi(q)+\chi(q)^{-1}}{2}-1$.
background
In the Primitive Recognition Calculus, positive ratios are tracked up to the orbit equivalence that identifies units of the same magnitude class (RatioOrbit). A character $\chi$ is a map on those orbits; the derived object costFromCharacter turns $\chi$ into a cost value at each orbit $q$.
The classical recognition cost is the J-cost of T5 uniqueness: $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The Recognition Composition Law is the functional equation that forces this shape. The present module works on the continuum completion: discrete character data must display as J before calibrated rigidity can pin the global cost.
Upstream cost constructions (observer cost as J-cost of the event state; multiplicative-recognizer derived cost; rung-coarsen total cost under a ratio weight) all treat J as the native magnitude-of-mismatch measure. This lemma records the rational display of the character-generated cost in that same closed form.
proof idea
One-line term wrapper: apply the already-proved rationalization lemma costFromCharacter_toRat at the given character $\chi$ and orbit $q$. No extra algebraic rearrangement is performed here; the equality is exactly that lemma's conclusion.
why it matters
This identity is the display step inside ForcedJOnCompletion. Immediately downstream in the same module, calibrated forcing uses it: any character calibrated at a point $p$ (so $\chi(p)\approx p$) generates the canonical J-cost at $p$, written costFromCharacter χ p ≈ onRatioOrbit p = J(p). Sibling results then propagate calibration along cyclic subgroups and obtain forced J on the completion, plus existence of a forced cost and a global identity from one-point calibration.
In the Recognition Science chain this is local bookkeeping for T5 J-uniqueness on character-generated costs, before the continuum rigidity theorems close the gap between discrete ratio data and the unique continuum cost. No external used_by edges are recorded yet; the lemma is consumed inside this forcing file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.