tickRecursor_zero
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive metric time or continuous evolution.
- Does not produce the eight-tick octave or spatial dimension D=3.
- Applies only to the discrete combinatorial structure of Tick.
- Does not address Berry-phase monotonicity or the arrow of time.
Lean usage
recursor_zero := fun {X} x f => tickRecursor_zero x fformal statement (Lean)
84@[simp] theorem tickRecursor_zero {X : Type u} (x : X) (f : X → X) :
85 tickRecursor x f tickZero = x := rfl
proof body
86