costFromCharacter_rigid
plain-language theorem explainer
A PRC ratio character calibrated at a single orbit point generates the canonical PRC J-cost there, up to cross-equivalence. Continuum forcing arguments that pin J from one calibration datum cite this equality. The proof is a one-line wrapper: calibration is exactly the cross-equivalence that identifies the generated cost with the orbit display of J.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits, and let $p$ be an orbit at which $\chi$ is calibrated, meaning $\chi(p)$ is cross-equivalent to $p$. Then the cost generated by $\chi$ at $p$ is cross-equivalent to the canonical PRC orbit cost at $p$: $\mathrm{cost}_\chi(p)\approx J_{\mathrm{orbit}}(p)$.
background
In the Primitive Recognition Calculus continuum layer, ratio orbits are the discrete multiplicative skeleton on which characters and costs live before completion. A PRC ratio character is a multiplicative map on those orbits (with the usual reciprocal and unit laws). The cost generated from a character at a point is the recognition cost that character induces along that orbit direction.
Calibration is a single-point identity condition: $\chi$ is calibrated at $q$ when $\chi(q)$ is cross-equivalent to $q$ itself, so $\chi$ acts as the identity character on that orbit direction. The module notes that calibration at two is the concrete datum the PRC cost hypotheses actually carry; the statement here is the general pointwise form.
Cross-equivalence is the equality relation used throughout this layer for comparing orbit-valued displays (costs, characters, traces) without committing to a particular real embedding. The canonical orbit cost is the PRC display of the unique J-cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law (T5).
proof idea
One-line term proof. The calibration hypothesis is definitionally $\mathrm{crossEq}(\chi(p),p)$. The sibling lemma that converts calibration into cost-level cross-equivalence is applied directly: it identifies the cost generated by the character at $p$ with the canonical orbit cost at $p$. No further character axioms are unfolded in this wrapper; multiplicativity is used only upstream when building the generated cost and the calibration helpers.
why it matters
This is the cost-level half of calibrated character rigidity. Downstream, the same-module theorem on prime-direction rigidity packages it with identity on $p\cdot p$ and $p^{-1}$, and the doubled d'Alembert-trace rigidity theorem lifts it to $2(F+1)$. In ForcedJOnCompletion, calibrated-character-forces-J is literally this result, and the capstone forced-J-on-completion quotes it as clause (1): any calibrated PRC ratio character generates $J(p)$ at the calibration point.
That capstone is the continuum statement of T5 J-uniqueness on the completion: reciprocal-symmetric RCL, normalization, and one calibration datum force $J(x)=(x+1/x)/2-1$ up to the reciprocal gauge. Without this cost identification, the character-to-J bridge fails and the forcing chain cannot close on $R_\delta$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.