fromNat_zero
plain-language theorem explainer
Researchers reconstructing arithmetic inside the logic structure generated by the functional equation cite this fact to anchor the base case of the natural-number embedding. The declaration states that the recursive map from naturals to LogicNat sends zero to the base element. The proof holds by direct reflexivity on the clause of the map definition that returns the identity constructor.
Claim. Let $f:ℕ→L$ be the map on the inductive type $L$ generated by the functional equation, defined by $f(0)=$ identity and $f(n+1)=$ step$(f(n))$. Then $f(0)=$ zero.
background
The ArithmeticFromLogic module reconstructs the natural numbers inside LogicNat, the inductive type whose constructors are identity and step, obtained from the Recognition Composition Law. The upstream definition of fromNat iterates the step constructor starting from identity at input zero. A parallel fromNat in LedgerUnits embeds naturals into delta subgroups via the integer embedding, but the present declaration uses the LogicNat version.
proof idea
One-line wrapper that applies reflexivity to the zero clause of the fromNat definition in ArithmeticFromLogic.
why it matters
This base-case identification supports the subsequent construction of addition, successor, and induction inside the same module. It supplies the zero anchor required by the forcing chain that derives arithmetic from the functional equation before reaching the eight-tick octave and spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.