mul_one_crossEq
plain-language theorem explainer
Right-unit law for ratio-orbit multiplication under cross-equality: multiplying any ratio orbit by the unit orbit is cross-equivalent to the original. Order and rational-structure proofs in the primitive recognition calculus cite it when normalizing products. The proof reduces cross-equality to rational equality, applies the toRat homomorphism for mul and one, then closes by ring.
Claim. For every ratio orbit $a$ (signed-orbit numerator over a nonzero distinction-nat denominator), the product $a \cdot 1$ is cross-equivalent to $a$: the cross-multiplication balance $a_{\mathrm{num}}\cdot 1_{\mathrm{den}} \sim 1_{\mathrm{num}}\cdot a_{\mathrm{den}}$ holds as signed orbits, equivalently $(a\cdot 1)^{\sim}=a^{\sim}$ in $\mathbb{Q}$.
background
In the primitive recognition calculus, a ratio orbit is an integer-like display: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equality is the internal rational relation (K4.10): two ratio orbits are related when the scaled products of numerator and denominator balance as signed orbits. That relation is designed to live entirely on $\delta$-orbit positions, without presupposing classical $\mathbb{Q}$.
The verifier map toRat sends each ratio orbit to a rational. Upstream, cross-equality is proved equivalent to equality of those displays, multiplication of ratio orbits is a homomorphism for toRat, and the unit orbit maps to $1$. The present lemma is the right-unit instance of that rational structure, stated intrinsically via cross-equality rather than via the display.
proof idea
Term-mode rewrite chain. First replace cross-equality by equality of toRat displays via crossEq_iff_toRat_eq. Then apply mul_toRat so the left side becomes $a^{\sim}\cdot 1^{\sim}$, and one_toRat to replace $1^{\sim}$ by $1$. The remaining goal $a^{\sim}\cdot 1=a^{\sim}$ is discharged by ring.
why it matters
Feeds integer_order_certificate, which packages the closed internal signed-orbit order surface (truncated subtraction, $\le$ display, absolute difference, nonnegativity flags). Without a unit law under the native cross-relation, the rational display would not be a monoid at the orbit level, and order comparisons that normalize by units would leak classical $\mathbb{Q}$ assumptions.
In the Recognition foundation stack this sits in the integer/rational layer beneath cost uniqueness and the forcing chain: ratio orbits are the discrete carriers on which later J-cost and ladder constructions read magnitudes. It is a small algebraic hygiene step, not a T5–T8 landmark, but it keeps the order certificate fully internal to PRC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.