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

add_comm

show as:
view Lean formalization →

Addition is commutative on the natural numbers forced by the logic functional equation. Foundation researchers cite this when building arithmetic from the orbit structure before moving to cost functions or ring objects. The proof applies induction on the second argument, reducing the successor case with the recursive addition lemmas and the induction hypothesis.

claimFor all elements $a, b$ in the forced natural numbers, $a + b = b + a$, where addition is the recursively defined operation on the inductive type with zero and successor constructors.

background

The module constructs arithmetic from the Law of Logic by defining the forced natural numbers as an inductive type with identity (the zero-cost element, multiplicative identity in the orbit) and step (one iteration of the generator), mirroring the multiplicative orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. Addition satisfies the recursive rules n + zero = n and n + succ m = succ (n + m), together with the symmetric zero + n = n and succ n + m = succ (n + m). This setup derives Peano arithmetic as theorems rather than axioms, upstream from the cellular automata step definition and the observer forcing identity.

proof idea

The proof proceeds by induction on the second argument. The identity case rewrites directly with the zero rules. The successor case rewrites with the successor rules then applies the induction hypothesis.

why it matters in Recognition Science

This result feeds into the d'Alembert theorem for the cost function H, where it supports the equation H(xy) + H(x/y) = 2 H(x) H(y), and into the PhiRing and RecognitionCategory constructions. In the framework it advances the derivation of arithmetic from the logic equation, a prerequisite for the forcing chain to three dimensions and the phi-ladder mass formula.

scope and limits

formal statement (Lean)

 161theorem add_comm (a b : LogicNat) : a + b = b + a := by

proof body

Term-mode proof.

 162  induction b with
 163  | identity =>
 164    show a + zero = zero + a
 165    rw [add_zero, zero_add]
 166  | step b ih =>
 167    show a + succ b = succ b + a
 168    rw [add_succ, succ_add, ih]
 169
 170/-- Multiplication by recursion on the second argument. -/

used by (40)

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

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.