before
plain-language theorem explainer
The before relation orders ledger snapshots strictly by their tick indices, supplying the discrete temporal order for the Recognition Science ledger. Researchers proving the arrow of time from defect monotonicity cite this definition when showing that recognition steps are irreversible within an epoch. It is introduced by a direct equational definition that delegates the order to the natural-number index comparison.
Claim. For ledger snapshots $A$ and $B$, $A$ precedes $B$ if and only if the index of the tick belonging to $A$ is strictly smaller than the index of the tick belonging to $B$.
background
The TimeEmergence module formalizes time as the ledger tick counter with no independent background parameter. A LedgerSnapshot is a structure holding a Tick together with a nonnegative real defect; the state space is therefore indexed by discrete ticks rather than a continuous time coordinate. The module records that the minimal complete update period is the eight-tick octave arising from three spatial dimensions and that the arrow of time follows from the fact that defect can only decrease toward the cost minimum inside an epoch.
proof idea
The declaration is a direct definition that sets the before predicate equal to the strict inequality on the natural-number tick indices. An accompanying instance registers the relation as decidable by forwarding to the standard decidable less-than predicate on Nat.
why it matters
This definition supplies the ordering needed for the arrow-of-time theorems, including before_irrefl and arrow_well_defined in the ArrowOfTime sibling module. It realizes the module's core claim that recognition is a one-way operation because defect is non-increasing (F-006). The construction sits inside the forcing chain that derives the eight-tick period and D=3, and it is invoked by downstream results on recognition categories, continuum limits, and nucleosynthesis chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.