Foundation Arrow Of Time Before Asymm

The before relation

The declaration before_asymm establishes a precise, formal property of the framework's definition of time. In plain terms, it proves that if one moment is recognized as being before another, then the reverse cannot also be true. The definition of 'before' is built on a quantity called Z, which the framework calls Z-complexity: a running total of the absolute magnitudes of accumulated Berry phases at each step of a discrete process. Because Z is a sum of absolute values, it never decreases as steps are added. The theorem before_asymm then states that the relation 'is before', defined as having a strictly smaller Z value, is asymmetric: if Z at time t1 is less than Z at time t2, then Z at t2 is not less than Z at t1.

This asymmetry is the core of the framework's account of the arrow of time. The framework models a discrete ledger of events, where each step can be run forward or backward. Running a step backward traverses the same loop but subtracts phase, while Z takes absolute values, so reversal does not decrease Z. The result is that Z-complexity is monotonically non-decreasing, giving an intrinsic direction to time without importing thermodynamics. The theorem before_asymm is a logical consequence of this monotonicity: it formalizes that the ordering induced by Z is a strict partial order, meaning it is transitive, irreflexive, and asymmetric. This is a proved theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions.

What the declaration does not claim is equally important. It does not claim that this asymmetry is a physical law of the universe, nor does it claim that the arrow of time is a fundamental feature of reality. The framework treats this as a structural consequence of its own definitions: given the ledger and the Berry phase accumulation, the before relation is asymmetric. The theorem also does not claim that Z-complexity is the same as thermodynamic entropy, although the framework defines a separate quantity, entropyFromZ, which is monotone in Z and is intended to model the second law. The declaration before_asymm itself is a purely formal statement about the ordering relation, not a claim about the physical content of that ordering.

/-- The before relation is asymmetric (if t1 < t2, then not t2 < t1). -/
theorem before_asymm (z1 z2 : ℝ) (h : isBefore z1 z2) : ¬isBefore z2 z1 := by
  unfold isBefore at *; linarith

/-- Z-complexity at step k: sum of absolute Berry phases up to k. -/
def zAtStep (seq : TemporalSequence) (k : Fin seq.n_steps) : ℝ :=
  (Finset.univ.filter (fun i : Fin seq.n_steps => i.val ≤ k.val)).sum
    (fun i => |seq.berry_at_step i|)

/-- The before relation is transitive (time is ordered). -/
theorem before_transitive (z1 z2 z3 : ℝ) (h12 : isBefore z1 z2) (h23 : isBefore z2 z3) :
    isBefore z1 z3 := by
  unfold isBefore at *; linarith

/-- The before relation is irreflexive (a moment is not before itself). -/
theorem before_irrefl (z : ℝ) : ¬isBefore z z := by
  unfold isBefore; exact lt_irrefl z

/-- The before relation is asymmetric (if t1 < t2, then not t2 < t1). -/
theorem before_asymm (z1 z2 : ℝ) (h : isBefore z1 z2) : ¬isBefore z2 z1 := by
  unfold isBefore at *; linarith

What this page does not claim

This theorem does not claim that the arrow of time is a fundamental physical law of the universe. This theorem does not claim that Z-complexity is identical to thermodynamic entropy. This theorem does not claim that the before relation applies to continuous time or to the standard model of particle physics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ArrowOfTime.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: