costFromCharacter
plain-language theorem explainer
Defines the cost attached to a rational character χ by evaluating the PRC J-cost on the image χ(q). The identity character recovers the canonical native cost. Continuum rigidity and forced-J theorems cite this as the generated cost object that calibration collapses to J. The body is a one-line composition with the ratio-orbit J map.
Claim. Given a map $\chi$ from ratio orbits to ratio orbits and a ratio orbit $q$, the cost generated by $\chi$ at $q$ is the PRC rational $J$-cost of $\chi(q)$, namely $J(\chi(q)) = \bigl((\chi(q)+\chi(q)^{-1})/2\bigr)-1$ as a ratio-orbit object. When $\chi$ is the identity, this is the canonical PRC cost $J(q)$.
background
Primitive Recognition Calculus works with ratio orbits: integer-numerator over nonzero-denominator displays of rational scale factors (K4.7). On that discrete carrier the native cost is the ratio-orbit object
$J(q)=((q+q^{-1})/2)-1$,
implemented as onRatioOrbit, not yet the real-analytic uniqueness theorem.
A rational character is a multiplicative map $\chi$ on ratio orbits. The present definition packages “apply $J$ after $\chi$” so that later rigidity statements can compare the generated cost to the canonical $J$ without re-inlining the formula. The module sits in the PRC native-cost uniqueness layer that feeds continuum character-rigidity and forced-$J$-on-completion arguments toward T5 $J$-uniqueness.
proof idea
Pure definition: return the PRC rational $J$-cost of the image point, i.e. compose the character evaluation $q\mapsto\chi(q)$ with the already-defined ratio-orbit map $J(q)=((q+q^{-1})/2)-1$. No proof obligations.
why it matters
This is the generated-cost hook used throughout continuum forcing. Downstream, calibrated character rigidity proves that if $\chi$ is a PRC ratio character calibrated at $p$ ($\chi(p)\approx p$), then the generated cost equals canonical $J$ at $p$; the same equality appears in prime-direction rigidity, doubled-trace rigidity, and the calibrated-forcing / cyclic-subgroup propagation lemmas that feed forced_J_on_completion and canonical_cost_is_J_formula.
In the Recognition chain this is the discrete bridge from multiplicative characters to the unique cost functional $J(x)=(x+x^{-1})/2-1$ (T5 / RCL), before completion to the reals. Without a named generated-cost object, those rigidity theorems would have to restate $J\circ\chi$ ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.