recursor_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the recursion operator.
- Does not extend to dependent recursion or higher inductive types.
- Does not invoke Mathlib's full CategoryTheory limits or HasInitialObject.
- Does not address computational complexity or termination of recursion.
formal statement (Lean)
55theorem recursor_zero {α : Type*} (base : α) (step : α → α) :
56 recursor base step LogicNat.zero = base := rfl
proof body
57