mul_not_crossEq_zero_iff
plain-language theorem explainer
A product of two ratio orbits fails to be cross-equal to zero exactly when both factors fail to be cross-equal to zero. Order and factorization lemmas in the primitive recognition calculus cite this as the nonzero half of the zero-product law. The proof is the De Morgan dual of the positive zero-product statement, obtained by rewrite plus case split on the disjunction.
Claim. For ratio orbits $a$ and $b$, $\neg(a\cdot b \sim 0)$ if and only if $\neg(a \sim 0)$ and $\neg(b \sim 0)$, where $\sim$ is cross-multiplication equality of ratio orbits (signed-orbit balance of cross products) and $0$ is the zero ratio orbit.
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 as signed orbits under cross-multiplication. This is the PRC-native stand-in for ordinary rational equality, defined entirely on $\delta$-orbit positions (K4.10).
Multiplication of ratio orbits is the usual product of fractions on these displays. The sibling lemma mul_crossEq_zero_iff already records the zero-product law: the product is cross-equal to zero exactly when at least one factor is. The present statement is the negated dual, needed wherever one must preserve nonzeroness under products (inverses, units, and order certificates).
The local module builds the signed-orbit order surface used by the integer-order certificate: nonnegativity flags, trichotomy, and comparison displays that must stay consistent with the rational structure.
proof idea
One-line rewrite of the goal by the positive zero-product law mul_crossEq_zero_iff, which turns $\neg(ab\sim 0)$ into $\neg(a\sim 0 \lor b\sim 0)$. The rest is pure propositional De Morgan: constructor splits the biconditional; the forward direction feeds each conjunct into the disjunction via Or.inl/Or.inr; the reverse direction cases on the disjunction and applies the matching conjunct. No arithmetic on orbits is reopened.
why it matters
This is the nonzero half of the ratio-orbit zero-product law inside IntegerOrder. Downstream, the one-sided projections left_not_crossEq_zero_of_mul_not_crossEq_zero and right_not_crossEq_zero_of_mul_not_crossEq_zero, the introduction form mul_not_crossEq_zero_of_not_crossEq_zero, and factors_not_crossEq_zero_of_mul_crossEq_one all apply it directly: a product cross-equal to one cannot have a zero factor. Those facts feed the closed integer-order certificate (integer_order_certificate), which packages the signed-orbit order surface as a finished interface. In the broader Recognition stack this keeps the rational display free of zero-divisor pathologies before cost uniqueness and ladder arithmetic are attached; it is foundation plumbing rather than a T5–T8 forcing step, but the order certificate sits under every later comparison that treats ratio orbits as a field-like ordered structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.