mul_zero
plain-language theorem explainer
Multiplication on PRC integers annihilates on the right by zero: for every signed-orbit integer class $a$, $a\cdot 0=0$. Anyone building ring or module structure on the PRC integer quotient cites this as the standard zero law. The proof is a two-step tactic: injectivity of the $\mathbb{Z}$-display, then simplification against the underlying signed-orbit and LogicNat multiplication rules.
Claim. For every PRC integer $a$ (a balanced-length quotient class of signed orbits), the product of $a$ with the zero class equals the zero class.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation (K4.8). Each class has a verifier display toInt into ordinary $\mathbb{Z}$; injectivity of that display is the standard way to transfer equalities from $\mathbb{Z}$ back to the quotient.
Multiplication of signed orbits is defined componentwise on the positive and negative legs and is already known to intertwine with toInt (mul_toInt: $(ab).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$). At the LogicNat layer, right-multiplication by zero is definitional (mul_zero on LogicNat, recovered under toNat_mul).
The local module builds integer and rational arithmetic from primitive recognition orbits without classical choice on the integer hub, routing equivalence through cross-multiplication characterizations that stay in $\mathbb{Z}$.
proof idea
Apply injectivity of the integer display toInt on PRC integers, reducing the goal to an equality in $\mathbb{Z}$. Then simp discharges the displayed equation using the signed-orbit multiplication identity mul_toInt together with the underlying LogicNat fact that $n\cdot 0=0$ and the corresponding zero display lemmas. No case split or induction is required at the quotient level.
why it matters
Zero annihilation is the first ring axiom needed once PRC integers are equipped with multiplication. Downstream it is consumed heavily: inertia in the quadratic-limit action calculus (newton_first_law reduces the EL equation when the force term vanishes), the $\mathbb{Z}[\varphi]$ coefficient ring (PhiInt pairs), quasicrystal energy minima (min_energy_zero via mul_zero after sub_self), and several baryogenesis staging lemmas that kill source terms once a time derivative or charge factor is zero (a3SourceBL_zero_of_chiDot_zero, b0_closure_certificate, relic and wall certificates).
In the Recognition foundation this sits under K4.8 integer construction, feeding the arithmetic substrate on which the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and later physical modules rest. It is fully proved scaffolding, not an open interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.