zero_mul_crossEq
plain-language theorem explainer
Multiplying the zero ratio orbit by any ratio orbit yields a ratio orbit cross-equivalent to zero. Arithmetic and order lemmas on the internal rational display cite this to keep zero absorbing under multiplication. The proof rewrites cross-equivalence as rational equality, applies the product and zero display lemmas, and finishes with the ring identity 0·q = 0.
Claim. For every ratio orbit $a$ (integer numerator over a nonzero orbit denominator), the product of the zero ratio orbit with $a$ is cross-equivalent to the zero ratio orbit: if $\mathrm{crossEq}$ is the internal cross-multiplication relation on ratio orbits, then $\mathrm{crossEq}(0\cdot a,\,0)$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero orbit denominator. It is the internal stand-in for a rational display, built only from δ-orbit positions rather than classical ℚ.
Cross-equivalence of two ratio orbits means their cross-multiplied numerators balance as signed orbits: $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$. Upstream, this relation is proved equivalent to equality of the verifier rational displays (toRat). Multiplication of ratio orbits is likewise compatible with ordinary rational multiplication on those displays, and the zero ratio orbit displays as $0$.
The local module develops the order surface on signed and ratio orbits. Zero-absorption under multiplication is a basic algebraic fact needed before the order certificate can treat the rational display as a coherent ordered field fragment.
proof idea
Term-style tactic proof in three rewrites plus ring. First replace cross-equivalence by equality of toRat displays via the K4.10 bridge. Then expand the product display with the multiplication compatibility lemma, and replace the zero display by the constant $0$. The goal is the rational identity $0\cdot q=0$, discharged by ring.
why it matters
Feeds integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display lemmas for truncated subtraction, nonnegativity flags, and related order primitives; zero must act as a multiplicative absorber so the rational display stays consistent with the signed-orbit order.
Within Recognition Science foundation work this is bookkeeping on the PRC rational layer (K4.7–K4.11), not a forcing-chain step. It keeps the internal arithmetic aligned with classical rationals so later uniqueness and cost results can quote ordered-field facts without leaving the δ-orbit vocabulary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.