mul_left_crossEq_iff_of_not_crossEq_zero
plain-language theorem explainer
Left multiplication by a nonzero ratio orbit is injective for cross-equality: ca is cross-equal to cb exactly when a is cross-equal to b. Developers of the Primitive Recognition Calculus integer order surface cite this to cancel a common nonzero factor. The proof rewrites cross-equality to rational display equality, extracts nonzeroness of c, and cancels via the field inverse.
Claim. Let $a$, $b$, and $c$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If $c$ is not cross-equal to the zero ratio orbit, then $c\cdot a$ is cross-equal to $c\cdot b$ if and only if $a$ is cross-equal to $b$.
background
A ratio orbit is the PRC display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator. Cross-equality is the internal rational relation: two ratio orbits are cross-equal when the scaled numerators balance under cross-multiplication of denominators (K4.10). The verifier map toRat sends each ratio orbit to a rational, and cross-equality is equivalent to equality of those displays.
Multiplication of ratio orbits is defined so that the display is multiplicative: the display of a product is the product of the displays. The zero ratio orbit has display zero. The local setting is the integer-order layer of Primitive Recognition Calculus, which builds a closed order surface on signed orbits and ratio orbits without leaving the $\delta$-orbit language.
proof idea
Rewrite both sides via the bridge that cross-equality iff display equality, and replace each product display by the product of displays. From the hypothesis that $c$ is not cross-equal to zero, deduce that the display of $c$ is nonzero (contrapositive through the same bridge and the zero-display lemma). Build the unit identity that the inverse display times the display equals one. One direction of the biconditional is a short calculation that left-multiplies by the inverse and cancels; the other direction is substitution of equal displays.
why it matters
The integer-order certificate packages the closed order surface on signed orbits and distinction nats (truncated subtraction, absolute difference, nonnegativity flags, and their display bridges). Left-cancellation of nonzero ratio factors is part of the arithmetic needed so that order comparisons on ratio orbits behave like the ordered field of rationals while remaining internal to PRC. Without injectivity of nonzero left multiplication on cross-equality, equality and order lemmas that cancel common factors would not close. The result sits in the foundation stack that underwrites later forcing and mass-ladder work; it is pure arithmetic infrastructure rather than a T5–T8 landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.