add_comm
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.