pith. machine review for the scientific record. sign in
theorem proved term proof high

add_assoc

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 154theorem add_assoc (a b c : LogicNat) : (a + b) + c = a + (b + c) := by

proof body

Term-mode proof.

 155  induction c with
 156  | identity => rfl
 157  | step c ih =>
 158    show (a + b) + succ c = a + (b + succ c)
 159    rw [add_succ, add_succ, add_succ, ih]
 160

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.