succ_add_eq
plain-language theorem explainer
Left successor distributes over addition on the distinction naturals: succ(a)+b equals succ(a+b). Anyone proving Peano-style laws (commutativity, cancellation) on the finite distinction orbit cites this. The proof is induction on b: reflexivity at zero, then rewrite by the inductive hypothesis.
Claim. For all distinction naturals $a$ and $b$, $\mathrm{succ}(a)+b=\mathrm{succ}(a+b)$, where addition is the recursively defined sum on the finite distinction orbit and $\mathrm{succ}$ is one further distinction step.
background
DistinctionNat is the inductive type of finite orbits of repeated distinction (K2.12): constructors zero and succ. It is the base-neutral carrier on which the module builds arithmetic from recognition structure rather than from an axiomatic Peano package.
Successor is one more application of the generator (as in the LogicNat development: each Peano axiom is a theorem of the inductive structure, none is posited). Addition on DistinctionNat is defined by recursion on the second argument in the usual way (siblings: add, add_def, add_zero_eq, add_succ_eq).
This lemma is the left-successor companion to add_succ_eq. Together with zero_add_eq and add_zero_eq it supplies the elementary transport identities needed before commutativity and associativity.
proof idea
Term-mode induction on the second summand b.
Zero case: both sides reduce by the definition of addition with zero, so rfl closes.
Successor case: the goal is rewritten to succ(succ a + n) = succ(succ(a + n)); the inductive hypothesis rewrites the inner sum, and the outer successors match.
No external lemmas beyond the inductive structure and the recursive clauses of +.
why it matters
Feeds add_comm in the same module: the successor case of commutativity needs to move succ across the sum, which is exactly this identity (paired with add_succ_eq and the zero laws).
In the Recognition foundation stack, arithmetic is recovered from the distinction orbit rather than assumed. Establishing that succ and + interact as in Peano is a prerequisite for later orbit-counting, eight-tick period structure, and any rung arithmetic on the phi-ladder that treats DistinctionNat as a discrete clock.
No open scaffold: claim_status is proved. It is local infrastructure inside PrimitiveRecognitionCalculus.OrbitArithmetic, not a forcing-chain landmark (T0–T8), but it underwrites the discrete counting those landmarks eventually use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.