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