time_is_discrete
plain-language theorem explainer
The epoch length in the Recognition ledger equals exactly eight ticks. Researchers modeling emergent discrete time or foundational spacetime would cite this when fixing the minimal temporal resolution. The proof is a one-line simplification that reduces the epoch length definition directly against the eight-tick constant.
Claim. The length of an epoch equals $2^3$, so the minimal complete ledger update cycle consists of eight fundamental time quanta.
background
The TimeEmergence module treats time as the count of ledger ticks with no background continuum. The fundamental time quantum is the tick, denoted τ₀ = 1. An epoch is the minimal complete update cycle whose length is fixed by the eight-tick period, which equals 2^D for D = 3 spatial dimensions.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of epoch_length and substitutes the constant eight_tick from DimensionForcing.
why it matters
This supplies the discrete-time property required by the downstream time_emergence_certificate, which bundles F-004 and F-006 results on the arrow of time. It realizes the T7 eight-tick octave and T8 D = 3 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.