add_zero
plain-language theorem explainer
Right additive identity on PRC integers: adding the zero class leaves any class unchanged. Cited wherever ledger arithmetic, Φ-ring coefficients, or cosmology staging need a + 0 = a without leaving the signed-orbit quotient. Proof reduces equality to the ℤ display via injectivity, then simplifies with the display laws for add and zero.
Claim. For every PRC integer $a$ (a balanced-length quotient class of signed orbits), $a + 0 = a$, where $0$ is the zero class and $+$ is the induced addition on the quotient.
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 integers; addition on representatives is componentwise on the positive and negative distinction-nat parts, and descends to the quotient.
Zero is the class of the zero signed orbit. Upstream, add_toInt says the display intertwines addition: the integer of a sum is the sum of the integers. The LogicNat layer already has n + 0 = n by reflexivity on the constructors. The local module builds integer and rational arithmetic choice-free from recognition orbits before any Mathlib ℚ bridge.
proof idea
One short tactic proof. Apply injectivity of the toInt display on PRC integers, reducing the goal to equality in ℤ. Then simp discharges using the display lemmas: addition maps to integer addition and zero maps to 0, so the identity is the ordinary right-zero law on ℤ. No case split on representatives is needed once injectivity is in hand.
why it matters
Closes the right-unit law for the additive monoid (and later group) structure on PRC integers, the integer layer under the φ-ladder and Recognition Composition Law scaffolding. Downstream it is used heavily: residual α-inverse correction at zero load (corrected_at_zero), sphaleron translation invariance in baryogenesis staging, BIT kernel occupancy at rung zero, Fibonacci–φ power identities, foam Euler characteristic, and the Φ-integer coefficient ring. Without this identity, every “drop the zero correction” or “translate by a kernel element” rewrite fails inside the RS-native arithmetic rather than Mathlib ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.