zero_not_crossEq_mul_of_not_crossEq_zero
plain-language theorem explainer
If two ratio orbits are each not cross-equivalent to zero, their product is not cross-equivalent to zero. Order and rational-arithmetic developments in the primitive recognition calculus cite this as the one-sided product-nonzero rule. The proof is a one-line application of the right-to-left direction of the corresponding biconditional.
Claim. Let $a$ and $b$ be ratio orbits. If $a$ is not cross-equivalent to zero and $b$ is not cross-equivalent to zero, then the product $a \cdot b$ is not cross-equivalent to zero.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (K4.7). Two ratio orbits are cross-equivalent when the scaled numerators balance as signed orbits: $a.num \cdot b.den$ balances $b.num \cdot a.den$ (K4.10). That relation is the internal PRC stand-in for rational equality, defined entirely on $\delta$-orbit positions.
Zero as a ratio orbit is the zero numerator over a unit denominator. Cross-equivalence to zero therefore means the orbit represents the rational zero. The local module builds an integer order surface on these displays; product and reciprocal lemmas keep the nonzero locus closed under the rational operations used later in certificates.
The upstream biconditional states that the product is not cross-equivalent to zero if and only if both factors are not. The present statement is the convenient one-direction form used at call sites.
proof idea
One-line term proof. Apply the right-to-left direction (.mpr) of zero_not_crossEq_mul_iff at $a$ and $b$, packing the two hypotheses into the conjunction required by that iff. No further rewriting or case analysis.
why it matters
Closes the nonzero locus of ratio orbits under multiplication, a basic algebraic hygiene fact for the internal rational layer. Downstream it feeds the reciprocal-pair variants (product of reciprocals stays nonzero when both inputs are nonzero) and sits in the dependency cone of integer_order_certificate, whose doc-comment records that the internal signed-orbit order surface is closed.
Within Recognition Science this is foundation scaffolding rather than a forcing-chain landmark: it keeps PRC rational arithmetic consistent so later cost and order uniqueness results can treat nonzero denominators and products without ad hoc side conditions. No open scaffold remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.