tickZero
plain-language theorem explainer
tickZero supplies the base element of the Tick type as the record with natural-number index zero. Researchers establishing the natural-number object structure on temporal ticks cite it to anchor recursion and the orbit equivalence. The definition is a direct constructor application from the Tick structure definition.
Claim. Let $Tick$ be the structure whose sole field is an index in the natural numbers. Then $tickZero := ⟨0⟩$ is the canonical zero element of $Tick$.
background
Tick is defined in TimeEmergence as the structure with field index : ℕ, ordered by index comparison; it represents the atomic discrete unit of temporal progression with no background manifold. The module TimeAsOrbit shows that Tick, equipped with successor fun t => ⟨t.index + 1⟩, forms a Lawvere natural-number object whose universal property yields primitive recursion and uniqueness. This identification equates the temporal sequence to the orbit construction LogicNat from ArithmeticFromLogic.
proof idea
The definition is a one-line constructor application that builds the Tick record directly from the natural number zero.
why it matters
tickZero anchors the zero case required by tick_isNNO to establish that Tick satisfies the Lawvere natural-number object axioms. It feeds directly into tick_orbit_eq_logicNat, which produces the canonical isomorphism between the tick orbit and LogicNat. In the Recognition framework this realizes the module claim that the temporal sequence is the natural-number object forced by recognition, closing the combinatorial identification of time with iteration without external manifold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.