isBefore
plain-language theorem explainer
The definition sets the before relation on Z-complexity values to the standard strict inequality on the reals. Researchers modeling emergent time direction from Berry phase accumulation cite it as the base for order properties. It directly translates the tick-index ordering from TimeEmergence into the Z measure used throughout the Arrow of Time module.
Claim. The temporal order is defined by $z_1 < z_2$ for real numbers $z_1, z_2$ that represent Z-complexity.
background
The Arrow of Time module shows how directed time arises from Berry phase monotonicity without importing thermodynamics. Z-complexity accumulates only under forward R-hat steps on the ledger; reversal traverses loops in opposite orientation but absolute values keep Z non-decreasing. This yields an intrinsic before-after distinction.
proof idea
The declaration is a direct definition that equates the before relation to the standard strict order on reals. No lemmas or tactics are applied; it serves as the abbreviation used by the three order theorems in the same file.
why it matters
This definition supplies the base relation for before_transitive, before_irrefl, and before_asymm. It implements the arrow_from_z step described in the module doc-comment, linking Z-monotonicity to the directed order that emerges from the topological asymmetry of Berry phase loops. The parent results establish the three order axioms that turn Z into a temporal coordinate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.