add
plain-language theorem explainer
Addition on the logic-induced natural numbers is defined by recursion on the second argument. Researchers deriving Peano arithmetic inside Recognition Science would cite this construction. The definition proceeds by pattern matching on the constructors of LogicNat, returning the first argument on identity and applying step to the recursive call on step m.
Claim. The addition operation on the natural numbers induced by the Law of Logic satisfies $n + 0 = n$ and $n + S(m) = S(n + m)$, where $0$ is the identity constructor and $S$ is the step constructor.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost element, multiplicative identity in the orbit) and step (one more iteration of the generator). This mirrors the smallest subset of positive reals closed under multiplication by the self-similar fixed point and containing 1. The module ArithmeticFromLogic derives basic arithmetic from the Law of Logic after importing LogicAsFunctionalEquation and Mathlib. Upstream results include the definition of LogicNat itself, the successor function (one application of the generator), and the identity event at J-cost minimum.
proof idea
The declaration is a direct recursive definition by pattern matching on the second argument. The identity case returns the first argument unchanged. The step case applies the step constructor to the result of the recursive call on the predecessor.
why it matters
This supplies the addition operation required to state further arithmetic theorems inside the Recognition framework. It forms part of the early foundation that precedes the forcing chain T0-T8 and the Recognition Composition Law. No downstream theorems are listed in the current graph, but the construction enables the induction principle and subsequent number-theoretic results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.