tickEquivNat_succ
plain-language theorem explainer
The successor operation on ticks commutes with the canonical equivalence to the natural numbers. Researchers modeling discrete time as the orbit forced by recognition steps would cite this to confirm that Tick forms a Peano structure isomorphic to the naturals. The proof holds by direct reduction of both sides to the underlying index plus one.
Claim. For any tick $t$, if $s$ denotes the successor on ticks and $e$ the canonical equivalence from ticks to natural numbers, then $e(s(t)) = e(t) + 1$.
background
The module identifies the temporal sequence with the natural-number object forced by recognition. Tick is the structure carrying a single natural-number index that advances discretely; no background manifold is assumed. The successor advances this index by one, while the equivalence extracts the index to produce a bijection with the naturals. This construction rests on the orbit definition of LogicNat, the initial Peano object supplied by any logic realization, and the universal property of natural-number objects proved in the upstream NaturalNumberObject module.
proof idea
The proof is a one-line term that applies reflexivity. Both sides reduce immediately to the index of the input tick plus one by the definitions of successor and the equivalence map.
why it matters
The result verifies that the equivalence preserves successor, so Tick satisfies the universal property of the natural-number object. It thereby completes the combinatorial identification of time as the canonical iteration object of recognition, without invoking metric time or the eight-tick cycle. The module doc states that this closes the time-as-orbit frontier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.