add_assoc
plain-language theorem explainer
Associativity of addition holds on LogicNat, the naturals constructed from the Law of Logic. Researchers deriving arithmetic operations inside the Recognition framework cite this when composing cost functions or ring structures. The proof runs by induction on the third argument, reducing the successor case with three rewrites of add_succ followed by the induction hypothesis.
Claim. For all elements $a, b, c$ of the natural numbers generated by the Law of Logic, addition satisfies $(a + b) + c = a + (b + c)$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator), reproducing the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ. Addition is defined recursively on this type; the companion lemma add_succ states that n + succ m = succ (n + m) and is used as a rewrite rule. The module ArithmeticFromLogic derives the Peano axioms as theorems rather than postulates, importing only the functional-equation foundation and a cellular-automaton step operation.
proof idea
Induction is applied on the third argument c. The identity base case closes by reflexivity. In the successor case the goal is rewritten by add_succ on the left-hand sum, on the right-hand sum, and on the combined term; the induction hypothesis then finishes the equality.
why it matters
The result supplies the additive associativity required by downstream theorems such as H_dAlembert (which converts the Recognition Composition Law into the d'Alembert equation for J-cost) and the PhiRingObj and PhiInt constructions inside RecognitionCategory. It therefore sits inside the arithmetic layer that supports the forcing chain from T5 (J-uniqueness) through T8 (D = 3) and the eight-tick octave. No open scaffolding questions are attached to this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.