zero_not_crossEq_mul_iff
plain-language theorem explainer
The product of two ratio orbits is not cross-equivalent to zero exactly when neither factor is. Anyone building the internal rational order or a zero-divisor-free certificate on RatioOrbit cites this. The proof is a short De Morgan dual of the already-proved zero-product law under cross-equivalence.
Claim. For ratio orbits $a,b$, $\neg\,\mathrm{crossEq}(0, a\cdot b)$ if and only if $\neg\,\mathrm{crossEq}(a,0)$ and $\neg\,\mathrm{crossEq}(b,0)$, where $\mathrm{crossEq}$ is equality of ratio orbits by balanced cross-multiplication of signed-orbit numerators and denominators.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are related by crossEq when the scaled products of numerator and opposite denominator balance as signed orbits (the internal PRC stand-in for ordinary rational equality).
The sibling theorem zero_crossEq_mul_iff already records the zero-product law: the product is cross-equivalent to zero precisely when at least one factor is. The present statement is the negated dual, needed wherever one reasons about nonzero factors and nonzero products without leaving the orbit language.
Local setting is the IntegerOrder module, which builds the signed-orbit order surface (nonneg/negative flags, trichotomy, and the order certificate) entirely on these δ-orbit positions.
proof idea
One rewrite applies the positive form zero_crossEq_mul_iff, turning the goal into the classical De Morgan equivalence $\neg(P\lor Q)\leftrightarrow(\neg P\land\neg Q)$. A constructor splits both directions: the forward arm discharges each conjunct by feeding the corresponding Or.inl/Or.inr into the hypothesis; the reverse arm cases on the disjunction and applies the matching conjunct. No further arithmetic on orbits is required.
why it matters
Feeds the one-sided corollary zero_not_crossEq_mul_of_not_crossEq_zero and sits in the dependency cone of integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages the display lemmas for truncated subtraction, absolute difference, and nonnegativity flags that underwrite integer order inside PRC.
In the Recognition framework this is bookkeeping on the rational layer of the forcing chain: once ratio orbits behave like a zero-divisor-free field under cross-equivalence, the later order and cost uniqueness arguments can treat nonzero products as nonzero without exiting the native orbit calculus. It does not itself force φ, the eight-tick octave, or $D=3$; it keeps the rational substrate clean for those steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.