add_zero
plain-language theorem explainer
The theorem establishes that zero functions as the right additive identity on LogicNat, the inductive naturals forced by the Law of Logic. Researchers building arithmetic layers for Recognition Science algebras and cosmology derivations cite it when simplifying sums that involve the identity element. The proof is a one-line reflexivity that follows immediately once addition is defined by recursion on the LogicNat constructors.
Claim. For every $n$ in the inductive type of natural numbers induced by the Law of Logic, $n + 0 = n$, where $0$ is the identity constructor.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), mirroring the orbit under multiplication by the golden ratio. The module ArithmeticFromLogic constructs Peano arithmetic on this type after importing the functional equation from LogicAsFunctionalEquation. The sole upstream dependency is the LogicNat inductive definition itself, which supplies the constructors used to define addition.
proof idea
The proof is a one-line wrapper that applies reflexivity after the addition operation has been defined by recursion on the LogicNat structure.
why it matters
This identity anchors the arithmetic layer that supports PhiRing, F2Power, and RecognitionCategory constructions, as well as downstream results such as plot_composition_cancels_iff and resonance_increases_stability. It fills the basic additive-identity step required to move from the Law of Logic to the phi-ladder and eight-tick octave used in mass formulas and coherence theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.