add_succ
plain-language theorem explainer
The theorem states that addition in LogicNat obeys the successor recursion on the second argument. It is referenced in all subsequent proofs of associativity, commutativity, and distributivity within the arithmetic derived from the logic functional equation. The proof reduces immediately to reflexivity because addition is defined by recursion on the second argument.
Claim. For all $n, m$ in the inductive type LogicNat, $n + succ(m) = succ(n + m)$.
background
LogicNat is the inductive type with constructors identity (the zero-cost base element) and step (one iteration of the generator), representing the smallest subset of positive reals closed under multiplication by the generator and containing 1. The successor is defined locally as succ n := step n. This module derives Peano arithmetic as theorems from the Law of Logic rather than positing axioms, with upstream results supplying the inductive structure and the generator application.
proof idea
This is a one-line wrapper that applies reflexivity (rfl), as the addition operation is defined recursively to satisfy exactly this relation.
why it matters
It is invoked directly in the proofs of add_assoc, add_comm, mul_add, embed_add, le_succ, and lt_iff_succ_le, which together establish that LogicNat carries a semiring structure. This completes the translation of the orbit into standard arithmetic operations, supporting the multiplicative embedding and the later forcing chain steps that recover dimensions and constants from the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.