recursor_zero
plain-language theorem explainer
The base case identity for the primitive recursion operator on LogicNat returns the supplied base value. Researchers verifying the natural-number-object universal property in the category of types cite this identity when checking the zero-commuting square. The proof is immediate reflexivity from the pattern-matching definition of the recursor.
Claim. $forall (alpha : Type) (b : alpha) (f : alpha to alpha), recursor b f (LogicNat.identity) = b$
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, modeling the orbit under repeated multiplication by the generator as forced by the Law of Logic. The recursor is the function implementing primitive recursion via pattern matching on these constructors. The module bridges the strict categorical realization to Mathlib by proving the two NNO commuting diagrams for LogicNat, specifically the zero and successor cases.
proof idea
This is a one-line wrapper that applies reflexivity directly to the definition of recursor, which matches the identity constructor to the base argument.
why it matters
It supplies the recursor_zero field required by the IsNaturalNumberObject structure. This field is instantiated for LogicNat in logicNat_isNNO and then used to show Tick is an NNO in tick_isNNO. The identity completes one of the two structural equations needed for the NNO bridge in UniversalForcing, linking to the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.