tickSucc
plain-language theorem explainer
The successor on the Tick structure advances the discrete ledger index by one natural-number step. Researchers establishing the Lawvere natural-number object for time in Recognition Science cite this when proving the universal property and the equivalence to the LogicNat orbit. It is realized by direct application of the Tick constructor to the incremented index.
Claim. The successor function on ledger ticks is defined by advancing the index: for a tick $t$ with index $i$ in the natural numbers, the next tick is the structure whose index is $i+1$.
background
Tick is the structure from TimeEmergence whose sole field is a natural-number index; it carries the order relation by index comparison and serves as the atomic unit of discrete temporal progression. The TimeAsOrbit module shows that Tick, equipped with zero and this successor, forms a Lawvere natural-number object canonically equivalent to the orbit construction LogicNat from ArithmeticFromLogic. Upstream results supply the Tick structure itself and the universal property of natural-number objects in UniversalForcing.NaturalNumberObject.
proof idea
One-line definition that applies the Tick constructor to the successor of the input index.
why it matters
This supplies the successor map required for the IsNaturalNumberObject instance on Tick, which is proved in tick_isNNO and used to establish the equivalence tick_orbit_eq_logicNat. Downstream theorems such as recognitionStep_iterates_succ and tickEquivNat_succ rely on it to link ledger dynamics to the abstract iteration object. In the framework it realizes the combinatorial time-as-orbit claim without metric or dimensional content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.