arrowCount

formal source

  27  | thermodynamic | cosmological | causal | psychological | quantum
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem arrowCount : Fintype.card ThermodynamicArrow = 5 := by decide
  31
  32theorem jcost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ Jcost r := by
  33  by_cases h : r = 1
  34  · rw [h, Jcost_unit0]
  35  · exact le_of_lt (Jcost_pos_of_ne_one r hr h)
  36
  37theorem equilibrium_zero : Jcost 1 = 0 := Jcost_unit0
  38
  39theorem time_reversal_symmetric {r : ℝ} (hr : 0 < r) :
  40    Jcost r = Jcost r⁻¹ := Jcost_symm hr
  41
  42structure EntropyArrowCert where
  43  five_arrows : Fintype.card ThermodynamicArrow = 5
  44  nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ Jcost r
  45  equilibrium : Jcost 1 = 0
  46  time_reversal : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
  47
  48def entropyArrowCert : EntropyArrowCert where
  49  five_arrows := arrowCount
  50  nonneg := jcost_nonneg
  51  equilibrium := equilibrium_zero
  52  time_reversal := time_reversal_symmetric
  53
  54end IndisputableMonolith.Physics.EntropyArrowFromJCost