tick_within_epoch
plain-language theorem explainer
tick_within_epoch maps each ledger tick to its position inside the repeating 8-tick epoch. Researchers formalizing discrete time emergence from ledger updates cite it when partitioning the tick sequence for defect-monotonicity arguments. The definition is realized by a direct modular reduction of the tick index together with the standard Nat.mod_lt witness.
Claim. For a tick $t$ whose index is the natural number $n$, tick_within_epoch$(t)$ returns the element of the finite set Fin 8 given by $n$ mod 8.
background
The TimeEmergence module identifies time with the discrete ledger tick counter; there is no background continuous manifold. The structure Tick is defined by a single field index : ℕ together with the induced decidable order relations; each increment advances the ledger by one fundamental time quantum. The module records that the 8-tick cycle is the minimal complete update period arising as 2^D for D = 3.
proof idea
The definition is a one-line wrapper that extracts the index field of the supplied Tick, reduces it modulo 8, and packages the result in Fin 8 by applying Nat.mod_lt with a norm_num witness.
why it matters
The definition supplies the concrete projection onto the 8-tick epoch that is presupposed by the later statements on defect monotonicity and the irreversible arrow of time. It directly encodes the eight-tick octave (period 2^3) required by spatial dimension D = 3 in the forcing chain. The surrounding module addresses registry items F-004 and F-006 on the nature and direction of time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.