IndisputableMonolith.Chemistry.MaillardTemperatureLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Maillard Reaction Temperature on the Phi-Ladder
   6
   7The Maillard wrapper (`Chemistry/MaillardReactionThresholdFromJCost`)
   8applies the canonical band to the J-cost on the surface-temperature
   9ratio. This deep follow-on adds the explicit temperature-rung ladder.
  10
  11Reference: Maillard onset at 140°C = rung 0.
  12Predicted ladder:
  13- rung 0: 140°C (Maillard onset, first browning)
  14- rung 1: 140 · φ ≈ 226°C (Maillard peak, optimal browning)
  15- rung 2: 140 · φ² ≈ 366°C (Maillard–char boundary, acrylamide formation)
  16
  17Empirical bench: caramelisation peak ≈ 170-190°C (close to rung 1 but
  18at a lower sub-step); thermal degradation / charring > 350°C (near rung
  192). The ladder gives a structural prediction for any sugar-amine pair.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Chemistry
  26namespace MaillardTemperatureLadder
  27
  28open Constants
  29
  30noncomputable section
  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
  65  one_step_ratio : ∀ k, tempAtRung (k + 1) = tempAtRung k * phi
  66  strictly_increasing : ∀ k, tempAtRung k < tempAtRung (k + 1)
  67  adjacent_ratio_eq_phi : ∀ k, tempAtRung (k + 1) / tempAtRung k = phi
  68
  69/-- Maillard-temperature-ladder certificate. -/
  70def maillardTemperatureCert : MaillardTemperatureCert where
  71  temp_pos := tempAtRung_pos
  72  one_step_ratio := tempAtRung_succ_ratio
  73  strictly_increasing := tempAtRung_strictly_increasing
  74  adjacent_ratio_eq_phi := temp_adjacent_ratio
  75
  76end
  77end MaillardTemperatureLadder
  78end Chemistry
  79end IndisputableMonolith
  80