left_not_crossEq_zero_of_one_crossEq_mul
plain-language theorem explainer
If two ratio orbits multiply to one under cross-equivalence, the left factor is not cross-equivalent to zero. Order and field-structure proofs for PRC rationals cite this to keep multiplicative inverses off the zero class. The proof is a one-line projection of the two-sided factor nonzeroness lemma.
Claim. Let $a,b$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If $1$ is cross-equivalent to the product $a\cdot b$ (cross-multiplication balances the scaled numerators), then $a$ is not cross-equivalent to $0$.
background
In the Primitive Recognition Calculus, a ratio orbit is an internal rational display: a signed orbit numerator over a nonzero distinction-nat denominator. Equality of such displays is not classical $\mathbb{Q}$-equality; it is the cross-multiplication relation crossEq, which holds when the two scaled numerators balance as signed orbits (K4.10).
The local module builds an order surface on these integer and rational orbit displays. Multiplicative structure must respect the zero class: a product that is a unit cannot have a zero factor. The two-factor form already records that if $1$ is cross-equivalent to $a\cdot b$, then neither factor is cross-equivalent to zero.
That two-factor statement is the immediate upstream prior; the present lemma isolates the left conjunct for call sites that only need the first factor.
proof idea
One-line term wrapper. Apply factors_not_crossEq_zero_of_one_crossEq_mul to $a$, $b$, and the hypothesis that one is cross-equivalent to $a\cdot b$, then project the first conjunct of the resulting conjunction. No extra algebra is performed here.
why it matters
Feeds integer_order_certificate, which closes the internal signed-orbit order surface (truncated subtraction, $\le$ display, absolute difference, and nonnegativity flags all match their integer readings). Without left-factor nonzeroness when a product is a unit, the rational order and inverse machinery on ratio orbits would admit a zero divisor class and the certificate could not seal.
This sits in the foundation layer of PRC integer/rational displays that underwrite later Recognition forcing (cost uniqueness, ladder arithmetic). It is local bookkeeping rather than a T0–T8 landmark, but the order certificate it supports is part of making the native integer surface indisputable before physics constants are read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.