  29    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  30
  31/-- The Maillard cascade is symmetric in water-activity ratio. -/
  32theorem maillard_symmetric {r : ℝ} (hr : 0 < r) :
  33    Jcost r = Jcost r⁻¹ := Jcost_symm hr
  34
  35structure MaillardThresholdCert where
  36  equilibrium_below : Jcost 1 = 0
  37  cascade_above : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  38  symmetric : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
  39
  40def maillardThresholdCert : MaillardThresholdCert where
  41  equilibrium_below := below_threshold_equilibrium
  42  cascade_above := above_threshold_positive
  43  symmetric := maillard_symmetric
  44
  45end IndisputableMonolith.Chemistry.MaillardThresholdFromJCost

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.