IndisputableMonolith.QFT.CasimirPlateModes

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Casimir Plate Modes
   6
   7This module is the clean ideal parallel-plate spine for the RS Casimir lane.
   8It does not pretend to prove the zeta/Lifshitz regularization from first
   9principles.  Instead it isolates that analytic input as the ideal plate energy
  10law and proves the force, sign, scaling, and RS-native constant consequences.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace QFT
  15namespace CasimirPlateModes
  16
  17open Constants
  18
  19noncomputable section
  20
  21/-- A positive separation between two ideal parallel plates. -/
  22structure PlateSeparation where
  23  value : ℝ
  24  pos : 0 < value
  25
  26/-- The `n`th transverse wave number for ideal parallel plates separated by `a`.
  27The physical mode index is usually `n >= 1`; Lean keeps `n : ℕ` and downstream
  28statements can impose `0 < n` when needed. -/
  29noncomputable def transverseWaveNumber (a : PlateSeparation) (n : ℕ) : ℝ :=
  30  (n : ℝ) * Real.pi / a.value
  31
  32/-- Photon frequency for a transverse mode in the one-dimensional scalar toy
  33model.  This is the part of the full electromagnetic spectrum that carries the
  34`1/a` scaling. -/
  35noncomputable def modeFrequency (a : PlateSeparation) (n : ℕ) : ℝ :=
  36  c * transverseWaveNumber a n
  37
  38/-- Zero-point energy for a single mode, `E_0 = ℏω/2`. -/
  39noncomputable def zeroPointModeEnergy (ω : ℝ) : ℝ :=
  40  hbar * ω / 2
  41
  42/-- The positive coefficient `K = π² ℏ c / 720` in the ideal parallel-plate
  43energy density `E/A = -K/a³`. -/
  44noncomputable def idealEnergyCoefficient : ℝ :=
  45  Real.pi ^ 2 * hbar * c / 720
  46
  47/-- Ideal renormalized Casimir energy per unit area for parallel conducting
  48plates.  The analytic input is the regularized mode-sum law. -/
  49noncomputable def idealEnergyDensity (a : PlateSeparation) : ℝ :=
  50  -idealEnergyCoefficient / a.value ^ 3
  51
  52/-- The derivative of `idealEnergyDensity` with respect to the plate separation,
  53given by the elementary derivative of `-K a^{-3}`. -/
  54noncomputable def idealEnergyDerivative (a : PlateSeparation) : ℝ :=
  55  3 * idealEnergyCoefficient / a.value ^ 4
  56
  57/-- Ideal attractive Casimir pressure between parallel conducting plates. -/
  58noncomputable def idealPressure (a : PlateSeparation) : ℝ :=
  59  -Real.pi ^ 2 * hbar * c / (240 * a.value ^ 4)
  60
  61/-- The ideal energy coefficient is positive. -/
  62theorem idealEnergyCoefficient_pos : 0 < idealEnergyCoefficient := by
  63  unfold idealEnergyCoefficient
  64  apply div_pos
  65  · exact mul_pos (mul_pos (sq_pos_of_pos Real.pi_pos) hbar_pos) c_pos
  66  · norm_num
  67
  68/-- The elementary energy derivative is positive for positive separation. -/
  69theorem idealEnergyDerivative_pos (a : PlateSeparation) :
  70    0 < idealEnergyDerivative a := by
  71  unfold idealEnergyDerivative
  72  apply div_pos
  73  · exact mul_pos (by norm_num) idealEnergyCoefficient_pos
  74  · exact pow_pos a.pos 4
  75
  76/-- Pressure is minus the derivative of the ideal renormalized energy density. -/
  77theorem idealPressure_eq_neg_energyDerivative (a : PlateSeparation) :
  78    idealPressure a = -idealEnergyDerivative a := by
  79  unfold idealPressure idealEnergyDerivative idealEnergyCoefficient
  80  ring
  81
  82/-- The ideal Casimir pressure is attractive. -/
  83theorem idealPressure_negative (a : PlateSeparation) :
  84    idealPressure a < 0 := by
  85  rw [idealPressure_eq_neg_energyDerivative]
  86  exact neg_neg_of_pos (idealEnergyDerivative_pos a)
  87
  88/-- Magnitude form of the ideal pressure. -/
  89theorem neg_idealPressure_eq_derivative (a : PlateSeparation) :
  90    -idealPressure a = idealEnergyDerivative a := by
  91  rw [idealPressure_eq_neg_energyDerivative]
  92  ring
  93
  94/-- The characteristic `a^{-4}` pressure scaling: multiplying by `a^4` removes
  95the separation dependence. -/
  96theorem idealPressure_fourth_power_scaling (a : PlateSeparation) :
  97    a.value ^ 4 * (-idealPressure a) = Real.pi ^ 2 * hbar * c / 240 := by
  98  rw [neg_idealPressure_eq_derivative]
  99  unfold idealEnergyDerivative idealEnergyCoefficient
 100  have ha : a.value ≠ 0 := ne_of_gt a.pos
 101  have ha4 : a.value ^ 4 ≠ 0 := pow_ne_zero 4 (ne_of_gt a.pos)
 102  field_simp [ha4, ha]
 103  ring_nf
 104
 105/-- RS-native substitution of Planck's constant in the ideal pressure law. -/
 106theorem idealPressure_hbar_phi_form (a : PlateSeparation) :
 107    idealPressure a =
 108      -Real.pi ^ 2 * (phi ^ (-(5 : ℝ))) * c / (240 * a.value ^ 4) := by
 109  unfold idealPressure
 110  rw [hbar_eq_phi_inv_fifth]
 111
 112/-- The ideal pressure law has no zero at finite positive separation. -/
 113theorem idealPressure_ne_zero (a : PlateSeparation) :
 114    idealPressure a ≠ 0 := by
 115  exact ne_of_lt (idealPressure_negative a)
 116
 117/-- A compact certificate for the ideal parallel-plate core. -/
 118structure IdealPlateCert where
 119  coefficient_pos : 0 < idealEnergyCoefficient
 120  pressure_from_energy :
 121    ∀ a : PlateSeparation, idealPressure a = -idealEnergyDerivative a
 122  attractive : ∀ a : PlateSeparation, idealPressure a < 0
 123  fourth_power_scaling :
 124    ∀ a : PlateSeparation,
 125      a.value ^ 4 * (-idealPressure a) = Real.pi ^ 2 * hbar * c / 240
 126  hbar_phi_form :
 127    ∀ a : PlateSeparation,
 128      idealPressure a =
 129        -Real.pi ^ 2 * (phi ^ (-(5 : ℝ))) * c / (240 * a.value ^ 4)
 130
 131/-- The ideal parallel-plate Casimir certificate. -/
 132def idealPlateCert : IdealPlateCert where
 133  coefficient_pos := idealEnergyCoefficient_pos
 134  pressure_from_energy := idealPressure_eq_neg_energyDerivative
 135  attractive := idealPressure_negative
 136  fourth_power_scaling := idealPressure_fourth_power_scaling
 137  hbar_phi_form := idealPressure_hbar_phi_form
 138
 139end
 140
 141end CasimirPlateModes
 142end QFT
 143end IndisputableMonolith
 144