costFromCharacter_jq
plain-language theorem explainer
The verifier rational of the cost generated by a ratio-orbit character equals the classical J-cost of that character's rational value. Structural-ledger uniqueness proofs cite this bridge when they pass between character factorization and the J display on Q. The proof is a one-line alias of the existing cost-from-character to-rational expansion.
Claim. For any map $\chi$ from ratio orbits to ratio orbits and any ratio orbit $q$, the verifier rational of the cost generated by $\chi$ at $q$ equals $J((\chi(q))^{\mathrm{rat}})$, where $J(t)=(t+t^{-1})/2-1$.
background
In the Primitive Recognition Calculus, a ratio orbit packages a signed integer numerator over a nonzero distinction denominator. The map to ordinary rationals is a verifier display (transport by cross-multiplication). Native cost on a ratio orbit is the on-orbit J construction; a character $\chi$ produces a cost by first applying $\chi$ and then that construction.
The structural ledger works with the rational J-display $J(t)=(t+t^{-1})/2-1$. Upstream, the cost-from-character to-rational theorem already expands the display as $((\chi q)^{\mathrm{rat}}+((\chi q)^{\mathrm{rat}})^{-1})/2-1$. The present lemma packages that expansion under the name of the J display, matching the T5 landmark $J(x)=(x+x^{-1})/2-1$.
proof idea
One-line wrapper: the claim is exactly the conclusion of the upstream cost-from-character to-rational theorem, which itself reduces by applying the on-ratio-orbit to-rational identity at $\chi(q)$. No extra algebra is done; the lemma only introduces the rational J abbreviation on the right-hand side.
why it matters
Display bridge between character factorization and the Recognition Composition Law cost $J$ (the same $J$ forced unique at T5). Downstream, the monotone-multiplicative readout on positive integers uses it to equate a factorized cost display with $J(\chi(\cdot)^{\mathrm{rat}})$; the round-5 engine calibrates the character so $J(\chi(n))=J(n)$ for $n\ge 1$; gauge rigidity and the terminal structural uniqueness target then force the canonical cost on the ledger. Without this packaging, character data and the J display stay in separate languages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.