isBefore
plain-language theorem explainer
The isBefore definition sets one Z-complexity value before another exactly when the first is numerically smaller. Researchers formalizing the emergence of temporal direction from Berry phase accumulation in lattice models cite this when building the ordering properties of time. It is a direct abbreviation of the standard ordering on the reals that immediately supports the irreflexivity, asymmetry, and transitivity theorems proved in the same module.
Claim. For Z-complexity values $z_1, z_2$, the relation $z_1$ precedes $z_2$ holds precisely when $z_1 < z_2$.
background
The Arrow of Time module derives directed time from monotonic non-decreasing Z-complexity, where Z is the absolute value of Berry phase accumulated under forward R-hat steps on the simplicial ledger. Forward evolution increases Z while reversal negates the phase orientation but leaves the absolute value unchanged, producing an intrinsic asymmetry without imported thermodynamics. The module builds on TimeEmergence.before, which defines temporal order via tick indices on LedgerSnapshot.
proof idea
This is a definition that directly equates the before relation to the built-in less-than predicate on real numbers. No lemmas or tactics are invoked; the declaration serves as the base case for the ordering properties established in the sibling theorems before_irrefl, before_asymm, and before_transitive.
why it matters
The definition supplies the core ordering used by before_asymm, before_irrefl, and before_transitive to establish the arrow of time. It realizes the module claim that Z-complexity monotonicity induces temporal direction from Berry phase accumulation alone. In the Recognition framework it supports the eight-tick octave and the emergence of spatial dimensions by furnishing the directed time structure required for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.