mul_right_crossEq_iff_of_not_crossEq_zero
plain-language theorem explainer
Right-multiplication by a nonzero ratio orbit cancels in the cross-equality relation: ac ~ bc if and only if a ~ b. Anyone building order or field structure on the internal PRC rationals cites this cancellation law. The proof rewrites cross-equality to rational equality of verifier displays, obtains c ≠ 0 in ℚ, and cancels by the multiplicative inverse.
Claim. Let $a,b,c$ be ratio orbits (integer numerator over a nonzero orbit denominator). If $c$ is not cross-equivalent to the zero orbit, then $\mathrm{mul}(a,c)$ is cross-equivalent to $\mathrm{mul}(b,c)$ if and only if $a$ is cross-equivalent to $b$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) 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, entirely on δ-orbit positions (K4.10).
The verifier display toRat sends each ratio orbit to a rational; the key bridge is that cross-equality holds exactly when the displays agree. Multiplication of ratio orbits is defined so that the display is multiplicative: (mul a b).toRat = a.toRat * b.toRat.
This lemma lives in the IntegerOrder module, which equips the signed-orbit and ratio-orbit layers with an order surface compatible with those displays. The nonzero hypothesis is stated internally as failure of cross-equality with the zero orbit, not as a raw rational inequality.
proof idea
Rewrite both sides via crossEq_iff_toRat_eq and push multiplication through mul_toRat, so the goal becomes a.toRat * c.toRat = b.toRat * c.toRat ↔ a.toRat = b.toRat.
From ¬ crossEq c zero, deduce c.toRat ≠ 0 by contraposition through crossEq_iff_toRat_eq and zero_toRat. Then field_simp gives the unit identity c.toRat * (c.toRat)⁻¹ = 1.
The forward direction is a short calc chain: insert the unit, associate, rewrite by the product equality, and cancel the inverse. The reverse direction is a one-line rewrite of the common factor.
why it matters
Cancellation of nonzero right factors is basic field arithmetic on the internal rationals. Without it, order and equality lemmas that compare scaled ratio orbits cannot drop common multipliers.
The sole recorded consumer is integer_order_certificate, which packages the closed signed-orbit order surface (truncated subtraction, leq display, absolute difference, nonnegativity flags). That certificate is the module-level seal that the PRC integer/rational order layer is self-contained.
In the broader Recognition stack this sits under the foundation forcing chain: the ratio-orbit calculus is the discrete arithmetic substrate on which later continuum and physical identifications (J-cost, φ-ladder, eight-tick structure) are built. The lemma itself is pure algebraic hygiene, not a physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.