succ_add
The left-distribution rule for successor over addition holds in the naturals generated by the logic orbit. Researchers establishing commutativity or ordering lemmas in the same module cite it directly. The argument is a one-line induction on the second summand that reduces via the companion right-successor theorem and reflexivity at the base.
claimFor all $n, m$ in the logic-forced natural numbers, $succ(n) + m = succ(n + m)$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost element, multiplicative identity in the orbit) and step (one further iteration of the generator); it mirrors the orbit {1, γ, γ², …} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1. The successor operation is the single application of the generator to any element. Addition is defined inductively on the second argument, so the companion theorem n + succ m = succ(n + m) holds by definition.
proof idea
Induction on m. The identity case is reflexivity. The step case rewrites both sides with the right-successor addition rule and applies the induction hypothesis.
why it matters in Recognition Science
This result is invoked by add_comm, lt_iff_succ_le, and succ_le_succ. It supplies one of the Peano-style arithmetic identities derived as theorems from the Law of Logic, feeding the transition from the functional equation through the forcing chain to the eight-tick octave and D = 3.
scope and limits
- Does not address multiplication or exponentiation.
- Does not apply to types other than LogicNat.
- Does not establish associativity of addition.
- Does not supply a computational reduction outside the inductive definition.
Lean usage
rw [succ_add]formal statement (Lean)
147theorem succ_add (n m : LogicNat) : succ n + m = succ (n + m) := by
proof body
Term-mode proof.
148 induction m with
149 | identity => rfl
150 | step m ih =>
151 show succ n + succ m = succ (n + succ m)
152 rw [add_succ, add_succ, ih]
153