add_def
plain-language theorem explainer
On DistinctionNat, the infix sum a + b is definitionally identical to the recursive operation add a b. Anyone simplifying orbit arithmetic or transporting Nat lemmas will cite this. The proof is pure reflexivity: + is notation for add.
Claim. For all distinction naturals $a$ and $b$, the infix sum equals the recursive addition map: $a + b = \mathrm{add}(a,b)$.
background
DistinctionNat is the inductive type of base-neutral finite orbits of repeated distinction (K2.12 in the Orbit module): constructors zero and succ, the same shape as ordinary Nat but interpreted as successive recognition steps rather than pure counting.
OrbitArithmetic equips that type with the usual Peano-style operations. The binary map add is the recursive sum; the module then installs + as notation for it. The parallel theorem in ArithmeticFromLogic does the same job for LogicNat, so the two foundations share the same simp surface.
Local setting is the Primitive Recognition Calculus layer: arithmetic is rebuilt from distinction orbits before it is used in path sums and gap probes.
proof idea
One-line wrapper by reflexivity. Because the + instance is defined to be add, the equality a + b = add a b holds by rfl with no further lemmas.
why it matters
Gives the simp bridge between notation and the named recursive sum on distinction orbits. Downstream, Gravity.SevenGaps.PathSumProbes.addBit_add_right relies on Fin and Nat addition commuting with bit flips; the same notational discipline appears here so orbit sums can be rewritten cleanly. It mirrors ArithmeticFromLogic.add_def, keeping LogicNat and DistinctionNat arithmetic interchangeable at the notation layer. In the Recognition stack this is scaffolding for building numbers from repeated distinction before the forcing chain (T5–T8) and mass or path-sum formulas consume them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.