tickRecursor_succ
plain-language theorem explainer
The successor clause for the tick recursor states that recursion on the successor of a tick applies the step function to the value obtained by recursing on the prior tick. Researchers establishing the natural-number object structure of time in Recognition Science cite this when verifying the universal property of Tick. The proof holds by direct reflexivity from the definition of the recursor.
Claim. Let $R$ be the recursor on the Tick type. For any type $X$, element $x$ of $X$, function $f: X to X$, and tick $t$, $R(x,f,mathrm{succ}(t)) = f(R(x,f,t))$, where succ denotes the successor on ticks.
background
The module TimeAsOrbit constructs Tick as the orbit under recognition steps and shows it forms a Lawvere natural-number object together with tickZero and tickSucc. This equates the combinatorial iteration of recognition with the natural numbers, using the universal property proved in UniversalForcing.NaturalNumberObject. The recursor tickRecursor implements primitive recursion on this object.
proof idea
This is a one-line term proof by reflexivity. It follows directly from the definition of tickRecursor on the successor case, with no additional lemmas required.
why it matters
This theorem supplies the recursor_step field in tick_isNNO, which asserts that Tick is a Lawvere natural-number object. It completes the structural identification of time as the canonical iteration object of recognition, aligning with the T7 eight-tick octave in the forcing chain. The module notes that metric time and the arrow of time remain outside this combinatorial result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.