epoch_length
plain-language theorem explainer
The epoch length is fixed at eight ticks as the minimal complete ledger update cycle forced by three spatial dimensions. Researchers formalizing discrete time or the arrow of time in Recognition Science cite this when establishing the tick-count definition of time. The definition is a direct alias to the eight_tick constant from the dimension forcing module.
Claim. The duration of one epoch is defined to be $8$, which equals $2^3$.
background
The TimeEmergence module formalizes time as the ledger tick counter with no independent background continuum. The minimal period for a complete update cycle is the eight-tick epoch, arising because D = 3 spatial dimensions force a period of 2^D = 8. This matches the eight-tick octave in the unified forcing chain (T7). Upstream results establish eight_tick as 8 in multiple contexts, with RRF.Foundation.Constants stating that dimension D = 3 forces the 8-tick period (2^D = 8) and DimensionForcing identifying it as the eight-tick period.
proof idea
This is a one-line definition that directly aliases DimensionForcing.eight_tick.
why it matters
This definition supplies the fixed epoch length required by the time emergence certificate (F-004/F-006), which establishes that time equals tick count, the arrow arises from defect decrease, and recognition is irreversible. It instantiates the T7 eight-tick octave and D = 3 from the forcing chain. The result is used to prove time_is_discrete and the full F-004/F-006 certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.