costFromCharacter_mul_congr
plain-language theorem explainer
Multiplicativity of a ratio character lifts through the native J-cost: the cost of a product is cross-equivalent to J of the product of the character values. Anyone assembling the Recognition Composition Law on ratio orbits cites this step. The proof unfolds the cost definition and feeds the character's multiplicativity axiom into congruence of the rational J-cost map.
Claim. Let $\chi$ be a map on ratio orbits satisfying the PRC ratio-character axioms (unit, multiplicativity, and reciprocity, all up to cross-equivalence). For any ratio orbits $x,y$, the cost generated by $\chi$ at the product $xy$ is cross-equivalent to $J(\chi(x)\cdot\chi(y))$, where $J(q)=((q+q^{-1})/2)-1$ is the rational J-cost on ratio orbits.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Equality is not definitional; the internal relation is cross-equivalence (cross-multiplication balance of scaled signed orbits), so all identities stay quotient-native.
The rational J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$. A PRC ratio character is a map $\chi$ on ratio orbits that preserves the unit, multiplies products, and respects reciprocals, each only up to cross-equivalence. The cost generated from such a character is the composite $q\mapsto J(\chi(q))$; the identity character recovers the canonical PRC cost.
This module builds native uniqueness and composition identities for that cost without leaving the ratio-orbit layer, bridging later to the real-analytic J-uniqueness theorem.
proof idea
Term-mode, two steps. Unfold the definition of cost-from-character, which is $J\circ\chi$. The goal becomes cross-equivalence of $J(\chi(xy))$ with $J(\chi(x)\cdot\chi(y))$. Apply congruence of the rational J-cost map under cross-equivalence to the character's multiplicativity axiom at $(x,y)$, which already supplies $\chi(xy)\sim\chi(x)\cdot\chi(y)$.
why it matters
This is the multiplicativity bridge used by the canonical RCL theorem for character-generated costs in the same module: that parent result assembles the full Recognition Composition Law identity $J_\chi(xy)+J_\chi(x/y)=2J_\chi(x)J_\chi(y)+2J_\chi(x)+2J_\chi(y)$ (up to cross-equivalence) from character axioms plus J-cost algebra. In the forcing chain this sits under T5 (J-uniqueness) and the RCL landmark: once costs are forced to arise from characters via $J\circ\chi$, composition must hold on the ratio-orbit layer before the real bridge. It does not itself force $\chi$ unique; uniqueness and the identity-character specialization are handled by sibling results in the native-cost uniqueness development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.