fromNat_zero
plain-language theorem explainer
The embedding from natural numbers into logic-native naturals sends zero to the identity element. Researchers deriving arithmetic operations from the Recognition Science functional equation cite this base case when simplifying expressions that start at the origin. The proof is a direct reflexivity reduction to the zero clause in the recursive definition of the embedding.
Claim. The embedding map $i : {N} {to} {LogicNat}$ satisfies $i(0) = 0$, where $0$ on the right denotes the identity element of $LogicNat$.
background
In ArithmeticFromLogic the type LogicNat is built from the functional equation developed in LogicAsFunctionalEquation. The map fromNat is defined by recursion: it returns the identity element at input 0 and applies the successor step constructor to the image of the predecessor. This supplies the base case needed to lift ordinary natural-number arithmetic into the logic-native setting. The upstream definition states that fromNat is the inverse map that builds the orbit by iterating the step.
proof idea
One-line wrapper that applies reflexivity to the zero clause of the fromNat definition, which returns the identity element by construction.
why it matters
The result supplies the zero base for the inductive arithmetic layer that sits above the Recognition Science forcing chain (T0-T8). It enables simplification of expressions involving the phi-ladder and the Recognition Composition Law when they are instantiated at the origin. No downstream theorems are recorded, leaving open whether further arithmetic identities will be proved by induction on this foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.