time_is_discrete
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive D = 3 from more primitive axioms.
- Does not address continuous approximations at large tick counts.
- Does not prove absence of sub-tick dynamics beyond the definition.
- Does not connect the tick count to specific measurements.
formal statement (Lean)
151theorem time_is_discrete : epoch_length = 2 ^ (3 : ℕ) := by
proof body
Term-mode proof.
152 simp [epoch_length, DimensionForcing.eight_tick]
153
154/-- **Theorem**: The minimal temporal resolution is one tick.
155 No sub-tick dynamics exist. Events are quantized in time. -/