before_asymm
plain-language theorem explainer
The asymmetry of the temporal order follows directly from defining isBefore as strict inequality on the reals. Researchers deriving an intrinsic arrow of time from Berry phase accumulation in discrete lattice models would cite this to rule out cycles in the ordering. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic to the resulting inequality.
Claim. For real numbers $z_1, z_2$, if $z_1 < z_2$ then it is not the case that $z_2 < z_1$.
background
The ArrowOfTime module defines the before relation by isBefore z1 z2 := z1 < z2, where the real values represent Z-complexity obtained from absolute Berry phase. This ordering supplies the directedness of time once forward R-hat steps are shown to increase Z while reversal cannot decrease it. The module setting starts from unitary lattice evolution that preserves the ledger yet produces monotonic Z via phase accumulation only in one orientation.
proof idea
The proof is a one-line wrapper. It unfolds the definition of isBefore to replace the hypothesis with the strict inequality z1 < z2, then invokes linarith on the ordered field of real numbers to obtain the negation of z2 < z1.
why it matters
This result supplies the asymmetry leg of the temporal order, completing the trio with before_transitive and before_irrefl that together make the arrow a strict partial order. It directly supports the module claim that directed time emerges from Berry phase monotonicity without imported thermodynamics, as stated in the Q3 section. The theorem anchors downstream statements such as entropy_monotone by guaranteeing that Z-ordering cannot loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.