IndisputableMonolith.QFT.CasimirThermal

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Thermal Casimir Correction
   6
   7Finite-temperature Casimir physics is represented here by a leading structural
   8correction factor.  The coefficient is a model parameter; zero-temperature
   9recovery is theorem-level.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirThermal
  15
  16open CasimirPlateModes
  17
  18noncomputable section
  19
  20/-- Leading thermal correction coefficient. -/
  21noncomputable def thermalCoefficient : ℝ := 1
  22
  23/-- Leading thermal correction, proportional to temperature and separation. -/
  24noncomputable def thermalCorrection (T a : ℝ) : ℝ :=
  25  thermalCoefficient * T * a
  26
  27/-- Thermal pressure model. -/
  28noncomputable def thermalPressure (T : ℝ) (a : PlateSeparation) : ℝ :=
  29  idealPressure a * (1 + thermalCorrection T a.value)
  30
  31/-- Zero temperature recovers the ideal pressure. -/
  32theorem thermalPressure_zero_temperature (a : PlateSeparation) :
  33    thermalPressure 0 a = idealPressure a := by
  34  unfold thermalPressure thermalCorrection
  35  ring
  36
  37/-- Vanishing thermal coefficient recovers the ideal pressure. -/
  38theorem thermalPressure_zero_coefficient (T : ℝ) (a : PlateSeparation)
  39    (hcoef : thermalCoefficient = 0) :
  40    thermalPressure T a = idealPressure a := by
  41  unfold thermalPressure thermalCorrection
  42  rw [hcoef]
  43  ring
  44
  45/-- Thermal correction certificate. -/
  46structure ThermalCasimirCert where
  47  zero_temperature :
  48    ∀ a : PlateSeparation, thermalPressure 0 a = idealPressure a
  49  zero_coefficient :
  50    ∀ (T : ℝ) (a : PlateSeparation), thermalCoefficient = 0 →
  51      thermalPressure T a = idealPressure a
  52
  53/-- Certificate instance. -/
  54def thermalCasimirCert : ThermalCasimirCert where
  55  zero_temperature := thermalPressure_zero_temperature
  56  zero_coefficient := thermalPressure_zero_coefficient
  57
  58end
  59
  60end CasimirThermal
  61end QFT
  62end IndisputableMonolith
  63