zero_add
plain-language theorem explainer
Left addition by the zero class is the identity on primitive recognition calculus integers. Anyone assembling an additive monoid or group structure on the signed-orbit quotient cites this. The proof pushes equality through the injective integer display and finishes by simplification of the orbit-level addition laws.
Claim. For every primitive recognition calculus integer $a$, $\mathrm{add}(0,a)=a$.
background
PRC integers are quotient classes of signed orbits under 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 prove equalities of classes without unpacking the quotient by hand.
Addition on signed orbits is componentwise on the positive and negative distinction-nat parts. The bridge add_toInt records that this orbit addition is compatible with ordinary integer addition under the display. The zero class is the class of the balanced empty orbit, and zero_toInt sends it to $0\in\mathbb{Z}$.
The module sits in the Primitive Recognition Calculus layer that rebuilds $\mathbb{Z}$ and $\mathbb{Q}$ from orbit arithmetic rather than importing Mathlib integers as primitives. Upstream, the same left-zero law already holds for the underlying logic naturals (ArithmeticFromLogic.zero_add).
proof idea
One short tactic proof. Apply injectivity of the integer display on PRC integers, reducing the goal to an equality in $\mathbb{Z}$. Then simp rewrites via the display bridges: orbit addition becomes integer addition (add_toInt), the zero class displays as $0$ (zero_toInt), and Mathlib's left-zero law on $\mathbb{Z}$ closes the goal.
why it matters
This is the left unit law for the additive structure on PRC integers, a basic monoid axiom needed before the quotient can support rings, modules, or cost calculus. Downstream it is consumed widely: PhiInt (elements of $\mathbb{Z}[\varphi]$) and F2-power group structure sit on integer arithmetic; cost-side results such as hasDerivAt_JcostDeriv, dAlembert_even, and unit-from-minimality use zero-addition when simplifying J-cost identities; alpha coordinate fixation and Fermi occupation kernels likewise reduce through integer zero laws.
In the Recognition chain this is scaffolding under K4.8 (integers as signed-orbit classes), not a forcing step T0–T8 itself. It keeps the arithmetic layer choice-light and display-faithful so later RCL and J-uniqueness arguments can treat integer coefficients as native PRC objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.