add_succ_eq
plain-language theorem explainer
On the distinction orbit, addition obeys the successor clause: a plus the successor of b equals the successor of a plus b. Anyone assembling Peano arithmetic or orbit-trace extension on DistinctionNat cites this. The equality is definitional; the proof is reflexivity from the recursive clause of addition.
Claim. For all distinction-orbit naturals $a,b$, one has $a + S(b) = S(a+b)$, where $S$ is the successor constructor on the finite orbit of repeated distinction.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and a successor constructor, the primitive recognition calculus stand-in for the naturals. Successor is one more application of the generator; the same inductive shape appears in the logic-derived naturals, where Peano axioms are theorems rather than postulates.
Addition on this orbit is defined by recursion on the second argument (siblings: add, add_def, add_zero_eq). The zero clause is a + 0 = a; the successor clause is exactly the present identity. The module builds the usual arithmetic laws (commutativity, associativity, cancellation, and the bridge to ordinary Nat) from these two clauses alone.
proof idea
One-line definitional proof: rfl. Once addition is defined by recursion with the clause a + succ b := succ (a + b), the stated equality is judgmentally true and needs no rewriting or induction.
why it matters
This is the successor half of the addition specification on the distinction orbit. Downstream, add_comm and add_assoc induct on the second summand and rewrite with this clause (and its zero twin) to close the inductive step. The same rewrite appears in succ_mul_eq when distributing successor through multiplication, and in orbitPositionTrace_add_extends_left when showing that extending an orbit-position trace by r steps is compatible with left addition of r.
In the Recognition stack this sits under Primitive Recognition Calculus arithmetic: the orbit must carry a Peano-style monoid before native cost uniqueness and trace-extension arguments can treat positions as additive. It is foundation scaffolding for later forcing-chain and cost work, not a physics claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.