ratioOrbit_mul_congr
plain-language theorem explainer
Multiplication of ratio orbits respects cross-multiplication equivalence: equivalent factors yield equivalent products. Anyone assembling multiplicative characters, cost-from-character maps, or native-cost uniqueness on the PRC rational display cites this congruence. The argument rewrites cross-equivalence as rational equality and applies the multiplicative display law twice.
Claim. Let $a_1,a_2,b_1,b_2$ be ratio orbits. If $a_1$ is cross-equivalent to $a_2$ and $b_1$ is cross-equivalent to $b_2$, then the product orbit $a_1 b_1$ is cross-equivalent to $a_2 b_2$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are cross-equivalent when the scaled numerators balance under cross-multiplication of denominators; this is the internal PRC stand-in for rational equality, defined entirely on $\delta$-orbit positions (K4.10).
The verifier map toRat sends each ratio orbit to an ordinary rational. Upstream, cross-equivalence is proved equivalent to equality of those displays, and multiplication of ratio orbits is proved to display as ordinary rational multiplication.
The present lemma sits in the native-cost uniqueness module, where ratio-orbit algebra underpins characters and cost functionals before any continuum identification.
proof idea
Short rewrite proof. First replace both hypotheses and the goal by the iff that cross-equivalence means equal toRat displays. Then rewrite both product displays via the multiplicative display law (mul a b).toRat = a.toRat * b.toRat, substitute the two equalities from the hypotheses, and finish.
why it matters
Native-cost uniqueness needs multiplication to be well-defined on cross-equivalence classes so that characters and cost maps descend. Downstream uses include the division congruence for cost-from-character, the orbit-product identity and reciprocal identities for PRC ratio characters, the lift from prime-level identity/reciprocal data to positive-ratio statements, two-adic axis-twist image lemmas, and the packaging of absolute-value-generated native-cost hypotheses.
In the broader Recognition chain this is bookkeeping on the rational display that later feeds J-cost uniqueness (T5) and the Recognition Composition Law: without multiplicative congruence, character-generated costs cannot be shown unique on ratio orbits. It closes no open scaffold; it is a proved algebraic step inside the uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.