before_transitive

formal source

  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. -/
  91noncomputable def entropyFromZ (z : ℝ) (density : ℝ) : ℝ :=
  92  Real.log (1 + z * density)
  93
  94/-- Entropy is monotone in Z (second law from Berry phase). -/
  95theorem entropy_monotone (z₁ z₂ d : ℝ) (hd : 0 < d) (hz : 0 ≤ z₁) (h : z₁ < z₂) :
  96    entropyFromZ z₁ d < entropyFromZ z₂ d := by
  97  unfold entropyFromZ
  98  apply Real.log_lt_log (by nlinarith)
  99  nlinarith
 100
 101end
 102
 103end IndisputableMonolith.Foundation.ArrowOfTime