before_asymm
plain-language theorem explainer
The before relation on real numbers is asymmetric: if z1 precedes z2 then z2 does not precede z1. Researchers building the Recognition Science arrow of time from Berry-phase monotonicity cite this when they need the ordering to be a strict partial order. The proof is a one-line wrapper that unfolds the definition of isBefore and invokes linear arithmetic.
Claim. If $z_1 < z_2$ then it is not the case that $z_2 < z_1$.
background
The module derives the arrow of time from monotonic accumulation of Berry phase on the ledger. The relation isBefore is defined by isBefore (z1 z2 : ℝ) := z1 < z2, so temporal order is simply the standard ordering on the real-valued Z-complexity. Upstream results include the entropy definition (entropy proportional to total defect) and the PhiForcingDerived structure that supplies the J-cost underlying Z.
proof idea
One-line wrapper that unfolds isBefore at both hypotheses and applies linarith to the resulting strict inequality.
why it matters
It supplies the asymmetry half of the strict partial order needed for the arrow of time. The module shows that forward R-hat steps accumulate positive Berry phase while reversal subtracts phase but leaves absolute Z unchanged, so the ordering is intrinsically directed. This step closes the topological asymmetry without importing an external second law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.