zero_add_eq
plain-language theorem explainer
Left identity for addition on the base-neutral finite orbit of repeated distinction: zero plus any orbit equals that orbit. Cited by anyone assembling Peano-style arithmetic on recognition orbits, especially commutativity and unit laws for multiplication. Proof is induction on the second summand: reflexivity at zero, then rewrite by the inductive hypothesis under successor.
Claim. For every finite distinction orbit $a$, $0 + a = a$, where $+$ is the recursively defined addition on the inductive type of distinction orbits (zero and successor).
background
DistinctionNat is the inductive type of finite orbits of repeated distinction: a zero constructor and a successor that applies one more distinction step. It is the base-neutral carrier for arithmetic built inside the primitive recognition calculus, not a posited Peano sort.
Addition on these orbits is defined by recursion on the first argument in the usual way (siblings cover the zero and successor clauses). The present lemma is the left-unit law complementary to the right-unit law already available from that recursive definition.
Upstream, successor is the generator step on the related LogicNat construction ("one more application of the generator"), and DistinctionNat itself is documented as the K2.12 base-neutral finite orbit. The local module develops the full additive structure (commutativity, associativity, cancellation, and the bridge to ordinary Nat) from these primitives.
proof idea
Tactic induction on $a$. The zero case is definitional reflexivity. In the successor case the goal is rewritten to $\mathrm{succ}(0+n)=\mathrm{succ},n$, then the inductive hypothesis closes it by rewrite. No external lemmas beyond the inductive structure and the recursive clauses of addition are required.
why it matters
This is a basic Peano identity on recognition orbits, needed before addition can be treated as a commutative monoid operation. Downstream, add_comm uses it in the zero case of its own induction (paired with the right-unit law). The unit law for multiplication also rewrites through it after expanding multiplication by one as a successor step from zero.
In the Recognition framework this sits in the foundation layer that derives arithmetic from distinction rather than assuming Peano axioms. It supports the orbit-arithmetic scaffolding under the forcing chain, where counting structure must be native to recognition before constants, ladders, and dimensional claims are attached. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.