left_not_crossEq_zero_of_mul_crossEq_one
plain-language theorem explainer
If the product of two ratio orbits is cross-equivalent to one, the left factor is not cross-equivalent to zero. Cited when characterizing unit products via reciprocals in the PRC integer-order layer. One-line projection of the two-factor nonzeroness lemma.
Claim. Let $a$ and $b$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a \cdot b$ is cross-equivalent to $1$ under balanced cross-multiplication, then $a$ is not cross-equivalent to $0$.
background
In Primitive Recognition Calculus, a ratio orbit is an integer-style rational display: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Equality of such displays is internal: two ratio orbits are cross-equivalent when the scaled products of numerator and denominator balance as signed orbits (K4.10). That relation is the PRC stand-in for ordinary rational equality, defined only on $\delta$-orbit positions.
Multiplication of ratio orbits and the unit orbit one live in the same layer. The companion lemma factors_not_crossEq_zero_of_mul_crossEq_one already records that a product cross-equivalent to one forces both factors off zero: the product itself cannot balance zero, and zero-divisors are ruled out under the orbit arithmetic.
This module builds the signed-orbit order surface used by the integer-order certificate. Nonzeroness of factors under unit products is a prerequisite for reciprocal characterizations of those products.
proof idea
One-line term wrapper. Apply factors_not_crossEq_zero_of_mul_crossEq_one to $a$, $b$, and the unit-product hypothesis; project the left conjunct of the resulting conjunction with .1. No extra case analysis.
why it matters
Supplies the left-factor nonzeroness half needed to turn unit products into reciprocal statements. Downstream, crossEq_recip_left_of_mul_crossEq_one uses it to conclude $b$ is cross-equivalent to the reciprocal of $a$. The two biconditionals mul_crossEq_one_iff_left_not_crossEq_zero_and_crossEq_recip and mul_crossEq_one_iff_left_not_crossEq_zero_and_recip_crossEq package the same fact as an iff with the reciprocal side.
Those reciprocal laws feed the closed integer-order certificate (integer_order_certificate), which asserts that the internal signed-orbit order surface is complete. In the broader Recognition stack this sits under the foundation forcing chain: clean rational arithmetic on orbits is required before cost uniqueness and the J-functional layer can treat ratios as well-defined displays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.