tickRecursor_zero
plain-language theorem explainer
The base case for the recursor on the Tick type states that recursion from any initial value x under any function f returns x exactly when the input is the zero tick. Researchers verifying the natural-number object structure for the temporal sequence would cite this lemma. The proof is immediate reflexivity from the definition of the recursor via standard natural-number recursion on the index.
Claim. For any type $X$, element $x$ of $X$, and map $f: Xto X$, the primitive recursion operator applied to the zero tick satisfies $rec(x,f,0)=x$.
background
The module shows that Tick forms the natural-number object forced by recognition steps, with successor given by incrementing the index. The recursor is defined to iterate $f$ from $x$ exactly $t.index$ times via Nat.rec. The zero tick is the element whose index is zero. Upstream documentation states: 'Recursor on Tick: iterate f from x exactly t.index times.' The module documentation notes that Tick is canonically equivalent to the orbit construction and satisfies the universal property of the natural-number object.
proof idea
One-line wrapper that applies reflexivity. The definition of the recursor reduces the zero-tick case directly to the base clause of Nat.rec, which returns the initial value x.
why it matters
This base case supplies the recursor_zero field in the downstream definition of tick_isNNO, which asserts that Tick is a Lawvere natural-number object. The module documentation states that this identification shows 'the temporal sequence is canonically the natural-number object forced by recognition.' It fills the combinatorial half of the time-as-orbit claim without addressing metric time or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.