before_transitive
The before relation on real numbers, defined by strict inequality of Z-complexity, is transitive. Researchers modeling emergent time from Berry phase accumulation cite this to guarantee ordered temporal sequences without external thermodynamics. The proof is a one-line term that unfolds the definition and applies linear arithmetic.
claimIf $z_1 < z_2$ and $z_2 < z_3$ then $z_1 < z_3$, where each $z_i$ is the absolute Berry phase complexity at successive snapshots.
background
The module derives the arrow of time from Berry phase monotonicity on the ledger. The relation isBefore is defined directly as $z_1 < z_2$ for real numbers $z$ that track absolute accumulated phase. Upstream, the before predicate on LedgerSnapshot compares tick indices: $a.tick.index < b.tick.index$. The module states that Z-complexity is monotonically non-decreasing, supplying an intrinsic before-after distinction.
proof idea
The term proof unfolds isBefore on the hypotheses and goal, then invokes linarith to obtain transitivity of the strict order on the reals.
why it matters in Recognition Science
This result confirms that the Z-induced temporal order is transitive, supporting directed time in the Recognition framework. It underpins entropy_monotone and related claims in the same module. The module doc notes that forward R-hat steps accumulate phase while reversal does not decrease absolute Z, yielding the asymmetry.
scope and limits
- Does not prove that Z-complexity increases under every physical evolution.
- Does not link the ordering to measurable observables outside the ledger.
- Does not address reversibility questions in quantum or continuous settings.
formal statement (Lean)
76theorem before_transitive (z1 z2 z3 : ℝ) (h12 : isBefore z1 z2) (h23 : isBefore z2 z3) :
77 isBefore z1 z3 := by
proof body
Term-mode proof.
78 unfold isBefore at *; linarith
79
80/-- The before relation is irreflexive (a moment is not before itself). -/