left_not_crossEq_zero_of_mul_not_crossEq_zero
plain-language theorem explainer
If a product of two ratio orbits is not cross-equal to zero, the left factor is not cross-equal to zero. Order and arithmetic lemmas on PRC rational orbits cite this one-sided nonzeroness projection. The proof is a one-line term that takes the left conjunct of the two-sided product nonzeroness equivalence.
Claim. Let $a,b$ be ratio orbits (signed-orbit numerator over nonzero distinction-nat denominator). If $a\cdot b$ is not cross-equal to the zero ratio orbit, then $a$ is not cross-equal to zero. Cross-equality means the cross-multiplied signed orbits balance: $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$.
background
In the Primitive Recognition Calculus integer layer, a ratio orbit is a rational display: a signed orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are cross-equal when the cross-multiplied numerators balance as signed orbits; that is the internal PRC stand-in for rational equality, defined entirely on $\delta$-orbit positions (K4.10).
Multiplication of ratio orbits is the usual product of fractions on these displays. The zero ratio orbit is the class of the zero numerator. The sibling lemma mul_not_crossEq_zero_iff states the full product rule: the product fails to be cross-equal to zero if and only if both factors fail to be cross-equal to zero.
This module builds the internal order surface on signed and ratio orbits (reflexivity, transitivity, trichotomy, sign flags) that later feeds the integer-order certificate.
proof idea
One-line term proof. Apply the left-to-right direction of the product nonzeroness equivalence (mul_not_crossEq_zero_iff) to the hypothesis that the product is not cross-equal to zero, then project the first conjunct of the resulting pair. No further case analysis or rewriting is needed.
why it matters
Nonzeroness of factors is a standing obligation when ordering or inverting ratio orbits and when relating signed-orbit signs to rational displays. This left projection packages that obligation for the left factor so downstream order proofs need not reopen the full iff.
It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate bundles display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags. In the broader Recognition stack this sits under the foundation forcing chain: clean rational arithmetic on orbits is prerequisite scaffolding for cost uniqueness and the J-cost calculus (T5), not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.