recursor_zero
plain-language theorem explainer
The base case of primitive recursion on LogicNat returns the supplied base element. Researchers establishing Lawvere natural-number objects for the time-as-orbit construction cite this when verifying the commuting diagrams for LogicNat. The proof is immediate reflexivity once the recursor pattern match on the identity constructor is unfolded.
Claim. For any type $X$, element $b : X$, and map $s : X → X$, the recursion operator satisfies $recursor(b, s, identity) = b$, where $identity$ is the zero constructor of LogicNat.
background
LogicNat is the inductive type whose constructors identity (the zero-cost multiplicative identity) and step generate the orbit under the generator, as the smallest subset of positive reals closed under multiplication by γ and containing 1. The recursor is the primitive recursion principle on this type, defined by pattern matching that sends the identity case to the base and the step case to the iterated application of the step function. This module supplies the Mathlib bridge that transports the two NNO structural equations through the LogicNat ≃ Nat equivalence, without constructing a full category instance.
proof idea
One-line wrapper that applies reflexivity after the recursor definition matches the identity constructor directly to the base case.
why it matters
This identity supplies one of the two commuting-square equations required for LogicNat to satisfy the Lawvere NNO universal property (see logicNat_isNNO). It is invoked in tick_isNNO to equip Tick with the same structure and in isInitial to obtain initiality in the category of pointed endomap algebras. The result therefore closes the algebraic content of an NNO in Type that the module doc identifies as the bridge goal, supporting downstream orbit and time constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.