Epoch
plain-language theorem explainer
A ledger epoch is defined as a structure anchored at a starting tick that completes one full 8-tick cycle. Researchers deriving the arrow of time from ledger updates would reference this when establishing discrete temporal periods. The declaration consists of a direct structure definition that equips the type with decidable equality.
Claim. A ledger epoch is a structure with a single field start of type tick, where each epoch spans exactly 8 ticks equal to $2^D$ for $D=3$.
background
The Time Emergence module formalizes time as the ledger tick counter rather than a continuous background. A tick is the atomic unit of temporal progression, represented as a structure with a natural number index that induces the order on time. The epoch captures the minimal complete update cycle of 8 ticks, which is $2^D$ for $D=3$ as forced in the dimension chain.
proof idea
The declaration is a structure definition introducing the epoch type with a start field of type tick and automatically deriving decidable equality. No upstream lemmas are invoked in the definition itself.
why it matters
This definition fills the role of the minimal period in the time emergence results (F-004, F-006), directly implementing the eight-tick octave from the forcing chain T7. It provides the temporal unit needed for theorems on the arrow of time and recognition irreversibility. The structure connects to the phi-ladder and J-cost minimization through the ledger factorization dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.