mul_crossEq_zero_iff
plain-language theorem explainer
Product of two ratio orbits is cross-equivalent to zero exactly when at least one factor is. Anyone building the ordered field structure on PRC rationals cites this as the no-zero-divisors law under the internal cross-multiplication relation. The proof transports the claim to rational displays via toRat and finishes with the LogicInt zero-divisor theorem.
Claim. For ratio orbits $a,b$ (integer numerator over nonzero orbit denominator), the product $a\cdot b$ is cross-equivalent to the zero orbit if and only if $a$ is cross-equivalent to zero or $b$ is. Cross-equivalence means the signed-orbit cross-multiplication balance $a_{\mathrm{num}}\cdot b_{\mathrm{den}}\sim b_{\mathrm{num}}\cdot a_{\mathrm{den}}$.
background
Ratio orbits are the PRC internal display of rationals: a signed orbit numerator over a nonzero distinction-nat denominator (K4.7). Cross-equivalence is the internal equality relation on those displays: two orbits match when the scaled numerators balance as signed orbits (K4.10). That relation is designed to agree with ordinary rational equality of the verifier maps toRat.
Multiplication of ratio orbits is defined so that it intertwines with ordinary multiplication of rationals: (mul a b).toRat = a.toRat * b.toRat. The zero ratio orbit maps to the rational $0$.
Upstream, LogicInt (integers forced from logic) already has no zero divisors: a * b = 0 ↔ a = 0 ∨ b = 0, forced by the ring isomorphism with Int. The present lemma lifts that fact from the integer layer to the ratio-orbit layer under cross-equivalence.
proof idea
Term-mode rewrite chain, then a single external lemma. Rewrite both sides with crossEq_iff_toRat_eq so the claim becomes an equality of rationals. Unfold the product via mul_toRat and the zero orbit via zero_toRat, reducing to a.toRat * b.toRat = 0 ↔ a.toRat = 0 ∨ b.toRat = 0. Discharge that by mul_eq_zero from IntegersFromLogic (no zero divisors on LogicInt, transported through the rational display).
why it matters
Closes the zero-divisor law for the PRC rational surface under the native cross-equivalence relation. Immediate children are the dual form zero_crossEq_mul_iff and the negated form mul_not_crossEq_zero_iff (product nonzero iff both factors nonzero). Those feed the integer-order certificate that declares the internal signed-orbit order surface closed.
In the Recognition foundation stack this is bookkeeping on the integer/rational layer beneath the forcing chain, not a T5–T8 landmark itself. It ensures the ratio-orbit algebra behaves like a domain before order and cost uniqueness are installed on top of it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.