add_def
The theorem equates the infix addition operator on LogicNat to the separately defined add function. Researchers building arithmetic from the Law of Logic cite it to maintain standard notation in derivations. The proof reduces to a single reflexivity step that matches the notation abbreviation.
claimFor all $n, m$ in the inductive type of natural numbers forced by the Law of Logic (constructors identity and step), $n + m = add(n, m)$.
background
LogicNat is the inductive type whose identity constructor is the zero-cost multiplicative identity and whose step constructor iterates the generator, forming the smallest orbit closed under multiplication by the generator and containing 1. The module ArithmeticFromLogic derives Peano-style arithmetic primitives from the functional equation of logic, importing the LogicAsFunctionalEquation module that supplies the underlying forcing. The upstream LogicNat inductive supplies the carrier on which the add function and its notation are defined.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definitional equality between the + notation and the add function.
why it matters in Recognition Science
This supplies notational consistency for the arithmetic layer that follows the LogicNat construction in the same module. It supports the Recognition Science program of extracting natural-number arithmetic directly from the functional equation without external set-theoretic assumptions. No downstream uses are recorded yet, leaving its role as a local bridge to later addition and induction results.
scope and limits
- Does not prove algebraic laws such as associativity or commutativity of addition.
- Does not define the add function itself.
- Does not apply to number systems other than LogicNat.
- Does not invoke constants such as phi or spatial dimensions.
formal statement (Lean)
132@[simp] theorem add_def (n m : LogicNat) : n + m = add n m := rfl