reverse_subtracts

formal source

  57  linarith [abs_pos.mpr hn]
  58
  59/-- Reversing a loop subtracts phase (opposite sign). -/
  60theorem reverse_subtracts (phase : ℝ) :
  61    let forward_phase := phase
  62    let reverse_phase := -phase
  63    forward_phase + reverse_phase = 0 := by
  64  simp only
  65  ring
  66
  67/-- Z-complexity uses absolute values, so reversal adds to Z, not subtracts. -/
  68theorem z_absolute_immune_to_reversal (phase : ℝ) (hp : phase ≠ 0) :
  69    |phase| = |-phase| := by
  70  rw [abs_neg]
  71
  72/-- The arrow of time: if Z(t₁) < Z(t₂), then t₁ is before t₂. -/
  73def isBefore (z1 z2 : ℝ) : Prop := z1 < z2
  74
  75/-- The before relation is transitive (time is ordered). -/
  76theorem before_transitive (z1 z2 z3 : ℝ) (h12 : isBefore z1 z2) (h23 : isBefore z2 z3) :
  77    isBefore z1 z3 := by
  78  unfold isBefore at *; linarith
  79
  80/-- The before relation is irreflexive (a moment is not before itself). -/
  81theorem before_irrefl (z : ℝ) : ¬isBefore z z := by
  82  unfold isBefore; exact lt_irrefl z
  83
  84/-- The before relation is asymmetric (if t1 < t2, then not t2 < t1). -/
  85theorem before_asymm (z1 z2 : ℝ) (h : isBefore z1 z2) : ¬isBefore z2 z1 := by
  86  unfold isBefore at *; linarith
  87
  88/-- Thermodynamic entropy as coarse-grained Z:
  89    entropy = log of the number of microstates with Z ≤ current Z.
  90    This is monotone in Z, giving the second law. -/