one_mul_crossEq
plain-language theorem explainer
Left multiplication by the unit ratio orbit is invisible under cross-equivalence: $1\cdot a\sim a$ for every ratio orbit $a$. Ordered-field and certificate work on the PRC rational display cites this unit law. The proof rewrites cross-equivalence to rational equality, applies the display lemmas for mul and one, and closes by ring.
Claim. For every ratio orbit $a$ (integer numerator over a nonzero orbit denominator), the product of the unit ratio orbit with $a$ is cross-equivalent to $a$: the signed-orbit balance $n_1\cdot d_a \sim n_a\cdot d_1$ holds, equivalently $(1\cdot a)^{\mathrm{toRat}}=a^{\mathrm{toRat}}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Cross-equivalence is the internal rational relation: two ratio orbits match when the scaled numerators balance as signed orbits (K4.10). The verifier display toRat sends each ratio orbit to an ordinary rational; cross-equivalence is exactly equality of those displays.
Multiplication of ratio orbits is defined so that the display is a ring homomorphism: (mul a b).toRat = a.toRat * b.toRat. The unit ratio orbit displays as $1$. The IntegerOrder module builds the ordered surface on these internal displays; unit laws for mul under cross-equivalence are the algebraic scaffolding for that order certificate.
proof idea
Term-mode rewrite chain. First replace crossEq by equality of toRat displays via crossEq_iff_toRat_eq. Then expand the left-hand product with mul_toRat and the unit with one_toRat, obtaining the rational identity $1\cdot a^{\mathrm{toRat}}=a^{\mathrm{toRat}}$. Close with ring.
why it matters
Feeds the single downstream consumer integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (truncated subtraction, $\le$, abs-diff, and nonnegativity flags all match their integer displays). Without left-unit cross-equivalence, the rational display would not be a unital monoid under mul, and the order certificate could not treat ratio orbits as an ordered field fragment inside PRC.
This sits in the foundation layer that underwrites later forcing-chain arithmetic (T5 J-cost uniqueness and the phi ladder both need a coherent rational display). It is pure algebraic hygiene: no new physics constant is fixed here, but the certificate that the order surface is closed depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.