recursor_zero
plain-language theorem explainer
The base case of the primitive recursion principle on LogicNat asserts that the recursor applied to the identity element returns exactly the supplied base value. Researchers constructing Lawvere natural-number objects in type theory cite this when verifying the universal property for LogicNat as a Peano structure. The proof is immediate by reflexivity because the recursor is defined by direct pattern matching on the constructors.
Claim. Let $X$ be any type, $b : X$ a base element, and $s : X → X$ a successor map. The primitive recursion operator on LogicNat satisfies $rec(b, s, 0) = b$, where $0$ denotes the identity constructor of LogicNat.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, realizing the natural numbers forced by the Law of Logic as the smallest orbit closed under multiplication by the generator. The recursor is the function implementing primitive recursion via pattern matching on these constructors, returning the base on identity and applying the step function to the recursive call on step n. This module bridges the strict categorical realization of LogicNat to Mathlib's CategoryTheory by proving the two structural identities required for the natural-number object universal property in the category of types: recursor applied to zero equals base, and recursor applied to successor equals the step function applied to the recursive value.
proof idea
The proof is a one-line wrapper that applies reflexivity. Because the recursor definition matches directly on LogicNat.identity to return the base argument, the equality holds definitionally without further computation.
why it matters
This identity supplies one of the two commuting diagrams needed to witness that LogicNat with identity and step forms a Lawvere natural-number object, as recorded in logicNat_isNNO. It is invoked in the construction of tick_isNNO and in the initiality proofs for Peano objects in NaturalNumberObject, thereby supporting the time-as-orbit realization and the eight-tick octave structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.