epoch_length
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove why D equals 3.
- Does not derive the tick structure from the functional equation.
- Does not address sub-tick phenomena.
- Does not connect to continuous limits for large tick counts.
Lean usage
theorem time_is_discrete : epoch_length = 2 ^ (3 : ℕ) := by simp [epoch_length]formal statement (Lean)
52def epoch_length : ℕ := DimensionForcing.eight_tick
proof body
Definition body.
53