tickEquivNat
plain-language theorem explainer
The definition supplies the canonical bijection identifying each discrete time tick with a natural number via its index. Researchers on the Recognition Science foundation cite it when treating the temporal sequence as the natural-number object forced by recognition. The construction directly specifies the forward map extracting the index, the inverse wrapping a natural number, and verifies both round-trip identities by case analysis and reflexivity.
Claim. The canonical equivalence $Tick ≃ ℕ$ sending each tick $t$ to its index $t.index$, with inverse sending each natural number $n$ to the tick $⟨n⟩$.
background
In the Recognition Science setting, time is not a background manifold but the discrete sequence of recognition steps. The upstream structure Tick from TimeEmergence is defined as a ledger tick with field index : ℕ, ordered by index comparison, and declared to be time itself. The module TimeAsOrbit asserts that this sequence is the Lawvere natural-number object under successor, canonically equivalent to the orbit construction LogicNat from ArithmeticFromLogic.
proof idea
Direct definition of the equivalence: toFun extracts the index, invFun constructs the tick via the index constructor, left_inv proceeds by case analysis on the tick reducing to reflexivity, and right_inv holds by reflexivity on the natural number.
why it matters
This equivalence is the immediate predecessor of tickEquivLogicNat, which composes it with LogicNat.equivNat.symm to identify Tick with the logic-based natural-number object. It closes the combinatorial half of the time-as-orbit claim, confirming that recognition steps generate the iteration object. The result relies on the universal property proved in UniversalForcing.NaturalNumberObject and leaves metric time, the eight-tick cycle, and the arrow of time to separate modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.