IndisputableMonolith.QFT.CasimirPFA

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirZetaRegularization
   3
   4/-!
   5# Proximity Force Approximation
   6
   7Sphere-plate Casimir measurements are usually interpreted through the
   8proximity force approximation: the sphere-plate force is `2πR` times the
   9parallel-plate energy density at the closest separation.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirPFA
  15
  16open CasimirPlateModes
  17open Constants
  18
  19noncomputable section
  20
  21/-- Proximity-force approximation for a sphere of radius `R` above a plate. -/
  22noncomputable def pfaForce (R : ℝ) (a : PlateSeparation) : ℝ :=
  23  2 * Real.pi * R * idealEnergyDensity a
  24
  25/-- PFA force is attractive for positive radius and positive separation. -/
  26theorem pfaForce_attractive_of_R_pos
  27    (R : ℝ) (a : PlateSeparation) (hR : 0 < R) :
  28    pfaForce R a < 0 := by
  29  unfold pfaForce idealEnergyDensity
  30  have hcoef : 0 < idealEnergyCoefficient := idealEnergyCoefficient_pos
  31  have henergy : -idealEnergyCoefficient / a.value ^ 3 < 0 := by
  32    exact div_neg_of_neg_of_pos (neg_neg_of_pos hcoef) (pow_pos a.pos 3)
  33  exact mul_neg_of_pos_of_neg (mul_pos (mul_pos (by norm_num) Real.pi_pos) hR) henergy
  34
  35/-- PFA has cubic separation scaling. -/
  36theorem pfaForce_cubic_scaling
  37    (R : ℝ) (a : PlateSeparation) :
  38    a.value ^ 3 * (-pfaForce R a) =
  39      R * (Real.pi ^ 3 * hbar * c) / 360 := by
  40  unfold pfaForce idealEnergyDensity idealEnergyCoefficient
  41  have ha : a.value ≠ 0 := ne_of_gt a.pos
  42  have ha3 : a.value ^ 3 ≠ 0 := pow_ne_zero 3 ha
  43  field_simp [ha, ha3]
  44  ring
  45
  46/-- Sphere-plate PFA certificate. -/
  47structure SpherePlateCert where
  48  attractive :
  49    ∀ (R : ℝ) (a : PlateSeparation), 0 < R → pfaForce R a < 0
  50  cubic_scaling :
  51    ∀ (R : ℝ) (a : PlateSeparation),
  52      a.value ^ 3 * (-pfaForce R a) =
  53        R * (Real.pi ^ 3 * hbar * c) / 360
  54  zeta_backed_energy :
  55    ∀ a : PlateSeparation,
  56      idealEnergyDensity a =
  57        CasimirZetaRegularization.regularizedModeSum a
  58
  59/-- Certificate instance for sphere-plate PFA. -/
  60def spherePlateCert : SpherePlateCert where
  61  attractive := pfaForce_attractive_of_R_pos
  62  cubic_scaling := pfaForce_cubic_scaling
  63  zeta_backed_energy := CasimirZetaRegularization.idealEnergyDensity_from_zeta
  64
  65end
  66
  67end CasimirPFA
  68end QFT
  69end IndisputableMonolith
  70