costFromCharacter_toRat
plain-language theorem explainer
The rational display of the cost generated by any character χ at a ratio orbit q equals J(χ(q)) = (χ(q) + χ(q)⁻¹)/2 − 1. Native-cost uniqueness, minimality certificates, and continuum forcing cite this identity whenever they compare generated costs to the canonical J-display. The proof is a one-line application of the on-orbit rational display lemma.
Claim. For any map $\chi$ from ratio orbits to ratio orbits and any ratio orbit $q$, the rational value of the cost generated by $\chi$ at $q$ equals $\frac{r + r^{-1}}{2} - 1$, where $r$ is the rational value of $\chi(q)$.
background
In the Primitive Recognition Calculus, ratio orbits are the discrete carriers of positive (and signed) scale data, with a rational display map sending each orbit to its underlying rational. Characters are maps on ratio orbits; the cost generated by a character at an orbit is the native cost attached to the image orbit under the standard on-orbit cost constructor.
The Recognition J-cost is the unique symmetric cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ (T5). On ratio orbits this appears as the rational identity for the on-orbit cost: its toRat display is exactly that algebraic expression in the orbit's rational value.
This module packages native-cost uniqueness for PRC. The present lemma is the bridge from the abstract generated-cost constructor to the explicit J-formula on rationals, so later calibration and cross-equality arguments can work entirely at the rational level.
proof idea
One-line term proof. By definition the cost generated by χ at q is the on-orbit cost of the image orbit χ(q). Apply the existing rational-display identity for on-orbit cost to χ(q); that identity expands the display to $((\chi q).\mathrm{toRat} + (\chi q).\mathrm{toRat}^{-1})/2 - 1$. No extra hypotheses on χ are required.
why it matters
This is the rational J-display for every character-generated cost. Downstream, generated_cost_formula on the continuum completion is a direct re-export; the structural ledger records the same identity as equality with the rational J-function jq. Minimality certificates for the two-adic generated native cost use it to discharge signed-unit and zero-orbit calibration via crossEq_iff_toRat_eq. Uniqueness arguments (e.g. ruling out the absolute-value character on the negative-one orbit) rewrite through this lemma to obtain a concrete rational contradiction.
In the forcing chain this is the discrete PRC face of T5 J-uniqueness: once costs are generated by characters on ratio orbits, their only rational display is the canonical J-expression. That pins native-cost comparison and feeds prime-pair calibration transport in the minimality ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.