zero_mul
plain-language theorem explainer
Left multiplication by the zero PRC-integer annihilates every PRC-integer. Anyone building ring or module structure on the signed-orbit integers cites this as the left zero law. The proof is a two-line injectivity argument: push both sides through the integer display and simplify.
Claim. For every PRC-integer $a$ (a balanced-length quotient class of signed orbits), $\mathrm{mul}(0,a)=0$.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation. Each class has a verifier display toInt into ordinary $\mathbb{Z}$; injectivity of that display is the standard way to transfer algebraic identities from $\mathbb{Z}$ back to the quotient.
Multiplication on signed orbits is defined componentwise on the positive and negative legs so that the display intertwines: $(\mathrm{mul},a,b).\mathrm{toInt}=a.\mathrm{toInt}\cdot b.\mathrm{toInt}$. The zero class is the class whose display is $0$. Upstream, the same left-zero law already holds for the logic naturals (LogicNat), recovered under toNat.
This module sits in the Primitive Recognition Calculus layer that builds integers and rationals from orbit arithmetic before any classical choice is introduced for the rational field.
proof idea
Apply injectivity of the integer display toInt on PRC-integers. Both sides of the desired equality become ordinary integer products after mul_toInt and zero_toInt; simp closes the goal because $0\cdot n=0$ in $\mathbb{Z}$. No induction on the orbit is needed at this layer.
why it matters
The left zero law is part of the ring axioms for PRC-integers and is consumed broadly: Phi-ring coefficients, gap-weight positivity, baryogenesis source-off limits, Fermi–Dirac occupation identities, and the Aczél–d'Alembert classification path all simplify products involving a zero factor through this lemma (or its Mathlib counterpart once the display is in play).
In the Recognition stack it sits under the arithmetic-from-logic recovery chain that feeds the cost functional and the forcing landmarks (J-uniqueness, $\varphi$, eight-tick structure). It does not itself force a physical constant; it keeps the integer layer algebraically clean so later uniqueness and positivity arguments do not carry extra zero cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.