mul_not_crossEq_zero_of_not_crossEq_zero
plain-language theorem explainer
If two rational orbits are each nonzero under cross-multiplication equality, their product is nonzero. Order and field-structure proofs in the primitive recognition calculus cite this to keep products off the zero class. The argument is a one-line extraction of the reverse direction of the corresponding biconditional.
Claim. Let $a$ and $b$ be ratio orbits (signed-orbit numerator over a nonzero distinction-nat denominator). If $a$ is not cross-equal to the zero orbit and $b$ is not cross-equal to the zero orbit, then the product orbit $a\cdot b$ is not cross-equal to zero. Cross-equality means the scaled numerators balance as signed orbits: $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$.
background
In the primitive recognition calculus, a ratio orbit is an internal rational display: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Equality of such displays is not raw structural equality; it is cross-multiplication balance of scaled numerators (K4.10), written as the relation that two orbits are equivalent when $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits.
The zero ratio orbit is the additive identity class under that relation. Multiplication of ratio orbits is the internal product on these displays. The sibling biconditional states that a product fails to be cross-equal to zero if and only if both factors do. That characterization is the immediate upstream fact used here.
The surrounding IntegerOrder module builds the signed-orbit order surface (reflexivity, transitivity, trichotomy, sign flags) needed to certify that the internal integer and rational order is closed.
proof idea
One-line term proof. Apply the reverse implication of the biconditional mul_not_crossEq_zero_iff to the pair of hypotheses that $a$ and $b$ are each not cross-equal to zero, yielding that the product is not cross-equal to zero. No further case analysis or rewriting is required at this site; the iff already packages the product-zero characterization.
why it matters
This is a workhorse non-vanishing lemma for ratio-orbit multiplication. Downstream it feeds the family of reciprocal and product identities that keep products and reciprocal pairs off the zero class (for example product-then-reciprocal cross-equal to one, reciprocal-pair non-vanishing, and the commutative variants). Those lemmas in turn support the integer-order certificate, whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition foundation stack this sits below the forcing chain (T0–T8) and the J-cost calculus: it is pure internal arithmetic hygiene on δ-orbit rationals, ensuring the multiplicative monoid of nonzero ratio orbits is well-defined before cost uniqueness and order displays are certified. It does not itself force φ, the eight-tick octave, or D = 3; it keeps the rational layer consistent so those later steps can quote a closed order surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.