add
plain-language theorem explainer
Defines addition on orbit positions (DistinctionNat) by recursion on the second argument: concatenating one orbit of repeated distinction onto another. Anyone building Peano arithmetic or rung arithmetic on the distinction orbit cites this. The body is the standard inductive clause pair, plus an Add typeclass instance so `+` works.
Claim. Addition on the base-neutral finite orbit of repeated distinction is the binary operation $+:\mathrm{DistinctionNat}\times\mathrm{DistinctionNat}\to\mathrm{DistinctionNat}$ given by $a+0=a$ and $a+S(b)=S(a+b)$, where $S$ is the successor (one more generator application). This is also the instance of the additive structure on that type.
background
DistinctionNat (K2.12) is the inductive type of finite orbits of repeated distinction: constructors zero and succ, base-neutral so it is not yet tied to a particular radix. It is the carrier for orbit arithmetic in the Primitive Recognition Calculus.
Successor on this type (and on the related LogicNat) means one more application of the generator. Upstream, ArithmeticFromLogic treats Peano structure as theorems of the inductive construction rather than axioms; the same recursive pattern appears here for orbits.
The local module builds arithmetic operations on those orbit positions. Addition is interpreted as concatenation of repetition: placing one finite distinction-orbit after another.
proof idea
Not a proof: a recursive definition by pattern match on the second argument. The zero clause returns the first summand unchanged. The successor clause wraps succ around the recursive call, so each step of the second orbit contributes one generator application. The Add instance is the one-line package ⟨add⟩ so notation + resolves to this operation.
why it matters
K4.5 in the Primitive Recognition Calculus: addition of orbit positions as concatenation of repetition. It is the first binary operation on DistinctionNat and the substrate for the sibling lemmas in this module (zero/succ equations, commutativity, associativity, cancellation, and the bridge toNat_add).
In the broader Recognition stack, orbit arithmetic sits under the forcing chain and the phi-ladder mass formula: finite distinction counts must add before they can be mapped to rungs, ticks, or eight-tick structure (T7). No downstream edges are recorded yet; the immediate consumers are the equational lemmas that follow in OrbitArithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.