mul_zero_crossEq
plain-language theorem explainer
Multiplying any ratio orbit by the zero orbit is cross-equivalent to zero under the internal PRC cross-multiplication relation. Ordered-field and integer-order constructions on ratio orbits cite this absorption law. The proof rewrites through the rational verifier display and closes by ring arithmetic.
Claim. For every ratio orbit $a$, the product $a \cdot 0$ is cross-equivalent to the zero orbit: $a \cdot 0 \sim_{\times} 0$, where cross-equivalence means the signed-orbit balance $a_{\mathrm{num}}\cdot b_{\mathrm{den}} \simeq b_{\mathrm{num}}\cdot a_{\mathrm{den}}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. It is the internal PRC stand-in for a rational, defined entirely on $\delta$-orbit positions rather than on classical $\mathbb{Q}$.
Cross-equivalence (K4.10) is the internal equality relation: two ratio orbits $a,b$ satisfy $\mathrm{crossEq}(a,b)$ when $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$ as signed orbits. The bridge theorem states this agrees with equality of the verifier displays: $\mathrm{crossEq}(a,b)\leftrightarrow a.toRat=b.toRat$. Multiplication of ratio orbits is likewise faithful on the display: $(a\cdot b).toRat=a.toRat\cdot b.toRat$, and the zero orbit displays as $0$.
This lemma lives in the integer-order layer that equips those ratio orbits with a signed order surface closed under the usual arithmetic identities.
proof idea
Term-mode rewrite chain, then ring. First replace cross-equivalence by equality of rational displays via crossEq_iff_toRat_eq. Unfold the product display with mul_toRat, so the goal becomes $(a.toRat)\cdot(zero.toRat)=zero.toRat$. Simplify the zero display by zero_toRat to obtain $a.toRat\cdot 0=0$, which ring discharges.
why it matters
Absorption of zero under multiplication is a basic field axiom fragment. It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: the certificate packages display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags on signed orbits.
Within Recognition Science this sits in the foundation stack that builds rationals and order from $\delta$-orbits before the forcing chain (T5 J-uniqueness through T8 dimension) is applied. Without zero-absorption, the ratio-orbit arithmetic cannot support the ordered-field identities the later cost and ladder constructions assume. The result is fully proved; it closes a routine but necessary algebraic cell rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.