isBefore
The definition equips real-valued Z-complexity with a strict ordering that formalizes the arrow of time arising from Berry-phase accumulation. Physicists modeling emergent directionality from unitary lattice evolution cite it to ground before-after distinctions without external thermodynamics. The implementation is a direct one-line abbreviation of the standard less-than predicate on the reals.
claimThe arrow of time is the binary relation on real numbers $z_1, z_2$ defined by $z_1 < z_2$.
background
Z-complexity is the absolute Berry phase accumulated under forward R-hat steps on the simplicial ledger; the module shows that reversal traverses the same loop with opposite orientation yet leaves the absolute value unchanged, so Z is monotonically non-decreasing. This supplies an intrinsic temporal order once the before relation is introduced on the Z values themselves. The local setting is the discrete unitary evolution of the ledger that nevertheless produces a directed time arrow, as stated in the module documentation on Berry-phase monotonicity.
proof idea
One-line definition that directly equates the before relation to the standard strict inequality on the reals.
why it matters in Recognition Science
The definition is the predicate used by the three immediate theorems that establish asymmetry, irreflexivity and transitivity of the temporal order. It realizes the module claim that Berry-phase accumulation alone produces a directed time arrow. In the larger framework it supplies the sequencing step required for entropy emergence as coarse-grained Z and for the eight-tick octave structure, while leaving open the explicit link from Z-monotonicity to the second law.
scope and limits
- Does not prove that Z is non-decreasing under forward steps.
- Does not derive thermodynamic entropy from Z.
- Does not address the underlying ledger dynamics or their reversibility.
- Does not incorporate phi-scaling or spatial dimension D=3.
formal statement (Lean)
73def isBefore (z1 z2 : ℝ) : Prop := z1 < z2
proof body
Definition body.
74
75/-- The before relation is transitive (time is ordered). -/