add_assoc
plain-language theorem explainer
Addition on DistinctionNat (the base-neutral orbit of repeated distinction) is associative. Anyone assembling Peano-style arithmetic, cost algebra, or phi-ladder bookkeeping on the primitive recognition calculus cites this. The proof is induction on the third summand, reducing via the successor-addition identity.
Claim. For all distinction naturals $a,b,c$, $(a+b)+c = a+(b+c)$.
background
DistinctionNat is the inductive type of finite orbits of repeated distinction: constructors zero and succ. It is the base-neutral counting object of the primitive recognition calculus (Orbit module, K2.12), parallel to LogicNat in ArithmeticFromLogic but tied to recognition orbits rather than pure logical generation.
Addition on DistinctionNat is defined recursively in the usual Peano way. The sibling identity add_succ_eq records $a + \mathrm{succ}, b = \mathrm{succ}(a+b)$ definitionally. The same associativity pattern already appears for LogicNat in ArithmeticFromLogic and, later, for PRC integers via injection into Lean Int.
This module sits in Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic: it equips the orbit type with the elementary arithmetic laws needed before transporting counts to Lean Nat (K4.5) and before cost or phi-ring constructions consume them.
proof idea
Induct on $c$. The zero case is definitional (rfl). In the successor case the goal is $(a+b)+\mathrm{succ}, n = a+(b+\mathrm{succ}, n)$. Rewrite three times with add_succ_eq to push successors outward on both sides, then apply the inductive hypothesis. The argument is the standard Peano induction for associativity, matching the LogicNat proof shape in ArithmeticFromLogic.
why it matters
Associativity is the first non-trivial ring-like law on the recognition orbit counters. Downstream it is consumed widely: CostAlgebra's d'Alembert form for $H$ (the multiplicative equation whose continuous solution is cosh, feeding the Recognition Composition Law and J-cost uniqueness T5), Jcost small-strain and product bounds, F2Power group laws, PhiInt bookkeeping in the phi-ring, and numerical side lemmas in AlphaGenesis measurement verdicts.
Without this lemma the orbit type cannot host the additive monoid structure that later layers treat as given when they lift counts into cost functionals, ladder rungs, and constant bounds. It is pure foundation scaffolding that closes a Peano axiom as a theorem rather than a postulate, in the same spirit as ArithmeticFromLogic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.