tickSucc_index
plain-language theorem explainer
The successor on discrete time ticks increments the index by one. Researchers establishing the natural-number object property of the tick sequence in Recognition Science cite this when verifying the successor axiom for the forced iteration object. The proof is a direct reflexivity after unfolding the successor definition.
Claim. For every tick $t$, the index of the successor tick equals the index of $t$ plus one.
background
Tick is the atomic unit of temporal progression: a structure carrying a natural-number index, with time advancing discretely by index steps rather than on a background manifold. The successor operation advances any tick by incrementing its index by one, making the sequence of ticks a Lawvere natural-number object under this successor map. The module establishes that this Tick coincides with the canonical arithmetic object forced by recognition, via the universal property of natural-number objects proved in the upstream NaturalNumberObject construction.
proof idea
One-line wrapper that applies reflexivity after the successor definition unfolds directly to the index increment.
why it matters
This declaration supplies the successor axiom needed to identify Tick as the natural-number object of recognition, closing the combinatorial identification of time with the orbit construction. It supports the module claim that recognition steps generate the iteration object without adding time as an external structure. The result sits inside the forcing chain that derives the temporal sequence from the Recognition Composition Law and the initial Peano object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.