add_zero_eq
plain-language theorem explainer
Right-identity for addition on the finite distinction orbit: adjoining the zero orbit leaves any orbit unchanged. Cited by anyone building Peano-style arithmetic or cost uniqueness on the primitive recognition calculus. The equality is definitional, discharged by reflexivity from the recursive clause of orbit addition.
Claim. For every finite distinction orbit $a$, $a + 0 = a$, where $0$ is the empty orbit and $+$ is the recursively defined orbit sum.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, isomorphic in shape to the Peano naturals but carrying the recognition-calculus reading of successive distinctions rather than bare counting.
This module equips that orbit with addition and multiplication so that later cost and trace arguments can stay inside the native type. Addition is defined by recursion on the second argument, with the zero clause reading $a + 0 := a$ and the successor clause $a + \mathrm{succ},b := \mathrm{succ}(a + b)$.
The present lemma records the zero clause as an equational fact usable under rewriting.
proof idea
One-line reflexivity. Because addition is defined by matching on the second argument with the zero branch equal to the first argument, the goal $a + \mathrm{zero} = a$ is definitionally true and closes by rfl.
why it matters
This is the right-unit law that every later arithmetic identity on DistinctionNat rewrites through. Downstream it appears in the zero case of commutativity of addition, in the zero case of the successor-multiplication identity, in the verification that orbit addition displays as ordinary Nat addition (K4.5), in the zero-multiplication law, and in the left-extension property of orbit-position traces used by native cost uniqueness.
Within the Recognition foundation it keeps the primitive orbit arithmetic aligned with Peano structure without importing Lean Nat as the carrier, so cost and forcing arguments can stay on the distinction orbit until a display map is needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.