costFromCharacter_canonical_rcl
plain-language theorem explainer
Any cost built from a PRC ratio-character satisfies the Recognition Composition Law on ratio orbits, up to cross-equivalence. Cite this when checking that character-generated native costs obey RCL before uniqueness or admissibility arguments. The proof reduces to the surface RCL identity on the character images, then transports both sides by congruence lemmas and crossEq transitivity.
Claim. Let $\chi$ be a ratio-orbit map that is a PRC ratio-character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence). For nonzero ratio orbits $x,y$, writing $C=\mathrm{costFromCharacter}(\chi)$, one has $$C(xy)+C(x/y)\;\sim\; 2\,C(x)C(y)+2\,C(x)+2\,C(y)$$ under ratio-orbit cross-equivalence (cross-multiplication balance of signed orbits).
background
Primitive Recognition Calculus works on ratio orbits rather than bare rationals. Equality is the internal relation crossEq: two orbits match when cross-multiplication of numerators and denominators balances as signed orbits (K4.10). Costs and characters are therefore stated quotient-natively.
A PRC ratio-character $\chi$ is a map on ratio orbits with $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, and reciprocal compatibility, all under cross-equivalence. The associated cost costFromCharacter $\chi$ is the d'Alembert-style cost read off that character (the native stand-in for the classical $J$-cost built from a multiplicative character).
The Recognition Composition Law (RCL) is the functional identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ that forces the unique admissible cost shape in the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Here the same identity is proved at the orbit level for every character-generated cost.
proof idea
Set $X=\chi(x)$ and $Y=\chi(y)$. Nonzero-preservation from the character hypothesis gives $X,Y$ nonzero on the rational display. Apply the surface identity canonical_rcl_surface to $X,Y$: the RCL holds for the canonical on-orbit cost of those images.
Left-hand transport: ratioOrbit_add_congr of costFromCharacter_mul_congr and costFromCharacter_div_congr shows $C(xy)+C(x/y)$ is cross-equivalent to the surface left-hand side on $(X,Y)$.
Right-hand side: unfolding costFromCharacter makes $C(x)=\mathrm{onRatioOrbit}(X)$ and $C(y)=\mathrm{onRatioOrbit}(Y)$ definitionally, so the surface right-hand side matches by crossEq_refl.
Finish with two applications of crossEq_trans.
why it matters
This is the RCL half of the native-cost interface for character-generated costs inside PRC native-cost uniqueness. Downstream, twoAdicGeneratedNativeCost_hypotheses and absValueGeneratedNativeCost_native_hypotheses assemble full PRCNativeCostHypotheses packages; both routes need the composition law on the generated cost.
In the broader framework this is the orbit-level avatar of the Recognition Composition Law that underwrites T5 $J$-uniqueness. Establishing RCL for every PRC ratio-character cost means candidate generators (two-adic, absolute-value) sit inside the same functional class as the classical $J$-cost before uniqueness or admissibility upgrades.
The nearby module comment flags the remaining delicate point: exact unit_zero is definitional equality, not mere cross-equivalence, so RCL alone does not close the admissibility-upgrade route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.