character_mul_toRat
plain-language theorem explainer
A primitive recognition ratio character is multiplicative on the verifier rational display: the rational image of the character at a product equals the product of the rational images. Calibration and rigidity arguments that close under products cite this bridge. The proof rewrites native character multiplicativity through the cross-equality/to-rational equivalence and the orbit product formula.
Claim. Let $\chi$ be a primitive recognition ratio character on ratio orbits. For all ratio orbits $x,y$, if $(\cdot)^{\mathrm{rat}}$ denotes the verifier rational display, then $(\chi(x\cdot y))^{\mathrm{rat}} = (\chi x)^{\mathrm{rat}}\,(\chi y)^{\mathrm{rat}}$.
background
Ratio orbits are the discrete rational display used by the primitive recognition calculus: an integer numerator (signed orbit) over a nonzero distinction-nat denominator. The verifier map sends such an orbit to an ordinary rational by dividing the integer value of the numerator by the natural value of the denominator. Equality of two orbits in this display is equivalent to cross-multiplication equality of their components.
A primitive recognition ratio character is a map on ratio orbits that inherits the algebraic structure of a $J$-automorphism (in particular multiplicativity) at the orbit level, typically stated via cross-equality rather than bare rational equality. The CostAlgebra fact that $J$-automorphisms preserve products is the conceptual parent of that multiplicativity field.
This lemma lives in the continuum character-rigidity forcing module: it transports the character's native product law onto ordinary rational arithmetic so later calibration and rigidity steps can work with $\mathbb{Q}$ identities.
proof idea
Short tactic proof. Instantiate the character's multiplicativity field at $x$ and $y$ to obtain a cross-equality between $\chi(x\cdot y)$ and $\chi x\cdot\chi y$. Rewrite that cross-equality into equality of rational displays via the K4.10 bridge (cross-equality iff equal toRat values). Finish by substituting the orbit product formula, which states that the rational display of a product is the product of the displays.
why it matters
Feeds calibrated_mul in the same module: calibration (identity on the rational display at given orbits) is closed under products precisely because multiplicativity on the display turns two identity equalities into one at the product. That closure is a step toward character rigidity on the continuum side of the primitive recognition calculus, where characters that fix a generating set are forced to be the identity character, and cost functionals built from them become rigid.
In the broader Recognition Science stack this is bookkeeping on the rational display that underwrites uniqueness of the native cost (the $J$-cost lineage from the forcing chain), not a new physical constant. It does not itself invoke $\phi$, the eight-tick octave, or $D=3$; those enter only after cost uniqueness and continuum forcing are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.