tickRecursor_zero
plain-language theorem explainer
The base case for the Tick recursor states that applying the iteration operator to the zero tick returns the initial value x unchanged. Researchers establishing that Tick forms a Lawvere natural-number object cite this to verify the zero axiom of primitive recursion. The proof is immediate reflexivity from the definition of tickRecursor at index zero.
Claim. For any type $X$, element $x : X$, and map $f : X → X$, the recursor that iterates $f$ exactly $t.index$ times starting from $x$ satisfies recursor$(x,f,0) = x$, where $0$ denotes the canonical zero tick.
background
The module shows that Tick is the natural-number object forced by recognition, canonically equivalent to LogicNat. The recursor is defined by Nat.rec x (fun _ acc => f acc) t.index, which performs exactly t.index iterations of f from the base value x. The zero tick is the element with index 0. This construction sits inside the universal property of natural-number objects proved in UniversalForcing.NaturalNumberObject, where primitive recursion must be unique.
proof idea
One-line wrapper that reduces by reflexivity to the definition of the recursor at tickZero, which by construction returns the base value x without applying f.
why it matters
This supplies the recursor_zero field required by tick_isNNO, which asserts that Tick with tickZero and tickSucc satisfies the full universal property of a Lawvere natural-number object. It thereby completes the structural claim that recognition steps generate the canonical iteration object of time, as stated in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.