tickEquivNat_zero
plain-language theorem explainer
The theorem states that the canonical equivalence from the Tick structure to natural numbers sends the zero tick to the integer zero. Researchers deriving time as the forced iteration object in Recognition Science cite this as the base case of the Tick-Nat isomorphism. The proof holds immediately by reflexivity after unfolding the index map and the definition of the zero tick.
Claim. Let $ι : Tick ≃ ℕ$ be the canonical equivalence sending each tick to its index. Then $ι(0_{Tick}) = 0$.
background
The module TimeAsOrbit identifies the temporal sequence Tick with the Lawvere natural-number object forced by recognition steps. Tick carries a successor operation that increments the index, and the universal property of natural-number objects (from UniversalForcing.NaturalNumberObject) yields a canonical isomorphism with LogicNat. The equivalence $ι$ is defined by $ι(t) = t.index$ with inverse sending $n$ to the tick carrying index $n$. The zero tick is the element whose index is zero.
proof idea
One-line reflexivity proof. The definitions of the equivalence (toFun on the zero tick returns its index 0) and of the zero tick already coincide, so the equality is immediate.
why it matters
This supplies the base case for the module's central claim that Tick is the canonical natural-number object of recognition. It anchors the structural identification of time with iteration in the foundation layer, prior to metric or dimensional extensions. No downstream theorems are listed, but the result is presupposed by any further development of time emergence from the orbit construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.