tickRecursor
plain-language theorem explainer
The definition supplies the recursion operator for the Tick type by iterating a function f from an initial value x a number of times equal to the tick index. Physicists and mathematicians establishing the natural-number object structure for time in Recognition Science cite this when verifying the universal property of Tick. The implementation reduces the operation to the standard recursor on the underlying natural numbers.
Claim. For any type $X$, initial value $x$ in $X$, function $f: X$ to $X$, and tick $t$, the recursor yields the result of applying $f$ iteratively to $x$ exactly index($t$) times.
background
Tick is the structure with natural-number index that serves as the atomic discrete unit of temporal progression; time advances only by these ticks with no background manifold. The TimeAsOrbit module claims that this Tick is canonically the natural-number object forced by recognition and equivalent to the orbit construction from ArithmeticFromLogic. Upstream results establish the ordered index on Tick and the universal property of natural-number objects in UniversalForcing.NaturalNumberObject.
proof idea
The definition is a direct one-line wrapper that applies the standard natural-number recursor to the index field of the tick, starting from the given initial value and iterating the supplied function.
why it matters
This supplies the recursor component required by tick_isNNO to establish that Tick with tickZero and tickSucc satisfies the universal property of a Lawvere natural-number object. It fills the structural claim in TimeAsOrbit that recognition steps generate the iteration object, linking to the forcing chain where time emerges as the canonical NNO. The result supports the identification of the recognition orbit with the tick count up to isomorphism while leaving metric time and the arrow of time to separate work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.