before_irrefl
plain-language theorem explainer
The irreflexivity of the before relation on real-valued Z-complexity ensures no moment precedes itself under the temporal ordering induced by Berry phase accumulation. Researchers modeling emergent time in discrete lattice models cite this when verifying that the induced order forms a strict partial order. The proof is a one-line term wrapper that unfolds the definition of isBefore and invokes the irreflexivity of the strict order on reals.
Claim. For every real number $z$, it is not the case that $z < z$, where $<$ denotes the before relation on Z-complexity values.
background
The ArrowOfTime module derives directed time from Berry phase monotonicity on the ledger. The before relation is defined directly as isBefore z1 z2 := z1 < z2, so that higher Z-complexity occurs after lower Z-complexity. This supplies an intrinsic temporal order without importing thermodynamics, as forward R-hat steps accumulate positive Berry phase while reversal preserves absolute Z values. The upstream lemma lt_irrefl establishes irreflexivity of the strict order on the underlying numeric type, here instantiated on reals.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of isBefore to expose the negation of z < z, then applies the irreflexivity lemma lt_irrefl directly to z.
why it matters
This result supplies one of the three core order properties (irreflexive, transitive, asymmetric) needed to make the arrow of time a strict partial order inside the Recognition Science framework. It supports the module's key claims on forward Berry phase accumulation and absolute Z monotonicity, advancing the Q3 derivation of directed time from lattice unitary evolution. The parent results on entropy emergence from coarse-grained Z lie immediately downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.