epoch_length_eq
plain-language theorem explainer
The declaration fixes the epoch length at exactly eight ticks in the ledger-based time model. Researchers deriving discrete time from recognition cycles cite it to anchor the minimal update period. The proof is a direct reflexivity step that follows from the definition of epoch length as the eight-tick value.
Claim. The duration of one epoch equals eight fundamental time quanta: $epoch_length = 8$, where $epoch_length$ is defined as the eight-tick cycle forced by three spatial dimensions.
background
The TimeEmergence module treats time as the ledger tick counter with no background continuum. The fundamental tick is the RS-native time quantum τ₀ = 1. Epoch length is defined as DimensionForcing.eight_tick, which encodes the minimal complete update cycle of length 2^D for D = 3.
proof idea
This is a term-mode proof that applies reflexivity directly to the definition of epoch_length. The definition unfolds to the constant eight supplied by the eight_tick construction in DimensionForcing.
why it matters
The equality supplies the concrete numerical value required by the time_emergence_certificate theorem, which assembles the F-004/F-006 results on time as tick count, defect-driven arrow, and recognition irreversibility. It realizes the eight-tick octave (T7) and D = 3 (T8) from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.