zero_def
plain-language theorem explainer
The zero_def theorem equates the standard numeral zero to the identity constructor in the natural numbers forced by the Law of Logic. Researchers building arithmetic on the Recognition Science foundation cite it when reducing expressions in inductive arguments over this type. The proof is a direct reflexivity that unfolds the definition without further steps.
Claim. In the type of natural numbers forced by the Law of Logic, where the identity constructor represents the zero-cost element, the standard numeral $0$ equals the zero constructor.
background
LogicNat is the inductive type of natural numbers forced by the Law of Logic. Its two constructors are identity, the zero-cost multiplicative identity in the orbit, and step, one iteration of the generator; this structure mirrors the smallest subset of positive reals closed under multiplication by the generator and containing 1. The module ArithmeticFromLogic constructs Peano-style primitives on this type after importing LogicAsFunctionalEquation, which supplies the underlying functional equation.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the numeral zero in the LogicNat type.
why it matters
This declaration anchors the arithmetic layer by linking the standard zero to the identity element in the naturals forced by the Law of Logic. It supports later constructions such as successor, addition, and induction in the same module, consistent with the forcing chain from logic to arithmetic primitives. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.