referenceTemp

formal source

  31
  32/-- Reference Maillard onset temperature (RS-native dimensionless 1,
  33calibrated at 140°C). -/
  34def referenceTemp : ℝ := 1
  35
  36/-- Maillard reaction temperature at φ-ladder rung `k`. -/
  37def tempAtRung (k : ℕ) : ℝ := referenceTemp * phi ^ k
  38
  39theorem tempAtRung_pos (k : ℕ) : 0 < tempAtRung k := by
  40  unfold tempAtRung referenceTemp
  41  have : 0 < phi ^ k := pow_pos Constants.phi_pos k
  42  linarith [this]
  43
  44theorem tempAtRung_succ_ratio (k : ℕ) :
  45    tempAtRung (k + 1) = tempAtRung k * phi := by
  46  unfold tempAtRung; rw [pow_succ]; ring
  47
  48theorem tempAtRung_strictly_increasing (k : ℕ) :
  49    tempAtRung k < tempAtRung (k + 1) := by
  50  rw [tempAtRung_succ_ratio]
  51  have hk : 0 < tempAtRung k := tempAtRung_pos k
  52  have hphi_gt_one : (1 : ℝ) < phi := by
  53    have := Constants.phi_gt_onePointFive; linarith
  54  have : tempAtRung k * 1 < tempAtRung k * phi :=
  55    mul_lt_mul_of_pos_left hphi_gt_one hk
  56  simpa using this
  57
  58theorem temp_adjacent_ratio (k : ℕ) :
  59    tempAtRung (k + 1) / tempAtRung k = phi := by
  60  rw [tempAtRung_succ_ratio]
  61  field_simp [(tempAtRung_pos k).ne']
  62
  63structure MaillardTemperatureCert where
  64  temp_pos : ∀ k, 0 < tempAtRung k