right_not_crossEq_zero_of_one_crossEq_mul
plain-language theorem explainer
If the product of two ratio orbits is cross-equivalent to one, the right factor cannot be cross-equivalent to zero. Arithmetic and order lemmas in the Primitive Recognition Calculus cite this to keep multiplicative structure free of zero divisors on the unit. The proof is a one-line projection of the second conjunct from the two-sided factor nonzeroness lemma.
Claim. Let $a$ and $b$ be ratio orbits. If $1$ is cross-equivalent to the product $a\cdot b$ under the internal cross-multiplication relation, then $b$ is not cross-equivalent to zero.
background
A ratio orbit (K4.7) is the PRC-native rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence (K4.10) is the internal rational equality on these displays: two ratio orbits $a$ and $b$ satisfy it when $a$ scaled on the numerator by $b$'s denominator balances $b$ scaled on the numerator by $a$'s denominator as signed orbits. The relation is defined entirely on $\delta$-orbit positions.
This module equips those displays with an integer order surface (sign flags, nonnegativity, trichotomy). Multiplicative structure must then guarantee that a product cross-equivalent to the unit has no zero factors, so inverses and order flags stay coherent.
The upstream two-factor theorem already states both halves: if $1\sim a\cdot b$, then neither $a$ nor $b$ is cross-equivalent to zero.
proof idea
One-line term wrapper. Instantiate the two-sided factor lemma (if $1$ is cross-equivalent to $a\cdot b$, then neither factor is cross-equivalent to zero) at $a$, $b$, and the given hypothesis, then project the second conjunct of the resulting conjunction.
why it matters
Feeds the integer-order certificate, which closes the internal signed-orbit order surface by packaging display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags. Right-factor nonzeroness is a zero-divisor guard for the multiplicative monoid of ratio orbits relative to the unit; without it, ordered-field-like structure on the PRC rational layer would not be well-posed.
That rational layer sits inside Primitive Recognition Calculus foundation work that underwrites the forcing chain landmarks (J-cost uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$). The declaration is a proved projection, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.