IndisputableMonolith.QFT.CasimirPolderAtomSurface

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Casimir-Polder Atom-Surface Force
   6
   7This module records the atom-surface member of the Casimir family.  The
   8retarded law scales as `a^{-4}`; the nonretarded law scales as `a^{-3}` and is
   9normalized to agree with the retarded law at `a = c / ω`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirPolderAtomSurface
  15
  16open CasimirPlateModes
  17open Constants
  18
  19noncomputable section
  20
  21/-- Retarded Casimir-Polder potential for positive polarizability. -/
  22noncomputable def casimirPolderRetarded (alpha : ℝ) (a : PlateSeparation) : ℝ :=
  23  -3 * hbar * c * alpha / (8 * Real.pi * a.value ^ 4)
  24
  25/-- Nonretarded van der Waals form normalized by an atomic frequency `omega`.
  26The crossover length is `c / omega`. -/
  27noncomputable def vanDerWaalsNonretarded
  28    (alpha omega : ℝ) (a : PlateSeparation) : ℝ :=
  29  -3 * hbar * c * alpha / (8 * Real.pi * (c / omega) * a.value ^ 3)
  30
  31/-- Crossover length between nonretarded and retarded atom-surface regimes. -/
  32noncomputable def crossoverLength (omega : ℝ) : ℝ :=
  33  c / omega
  34
  35/-- The retarded potential is attractive for positive polarizability. -/
  36theorem casimirPolderRetarded_negative
  37    (alpha : ℝ) (a : PlateSeparation) (halpha : 0 < alpha) :
  38    casimirPolderRetarded alpha a < 0 := by
  39  unfold casimirPolderRetarded
  40  have hnum : 0 < 3 * hbar * c * alpha := by
  41    exact mul_pos (mul_pos (mul_pos (by norm_num) hbar_pos) c_pos) halpha
  42  have hnum_neg : -3 * hbar * c * alpha < 0 := by
  43    nlinarith
  44  have hden : 0 < 8 * Real.pi * a.value ^ 4 := by
  45    exact mul_pos (mul_pos (by norm_num) Real.pi_pos) (pow_pos a.pos 4)
  46  exact div_neg_of_neg_of_pos hnum_neg hden
  47
  48/-- The nonretarded potential is attractive for positive polarizability and
  49positive atomic frequency. -/
  50theorem vanDerWaalsNonretarded_negative
  51    (alpha omega : ℝ) (a : PlateSeparation)
  52    (halpha : 0 < alpha) (homega : 0 < omega) :
  53    vanDerWaalsNonretarded alpha omega a < 0 := by
  54  unfold vanDerWaalsNonretarded
  55  have hcrossover : 0 < c / omega := div_pos c_pos homega
  56  have hnum : 0 < 3 * hbar * c * alpha := by
  57    exact mul_pos (mul_pos (mul_pos (by norm_num) hbar_pos) c_pos) halpha
  58  have hnum_neg : -3 * hbar * c * alpha < 0 := by
  59    nlinarith
  60  have hden : 0 < 8 * Real.pi * (c / omega) * a.value ^ 3 := by
  61    exact mul_pos (mul_pos (mul_pos (by norm_num) Real.pi_pos) hcrossover) (pow_pos a.pos 3)
  62  exact div_neg_of_neg_of_pos hnum_neg hden
  63
  64/-- At the crossover length `a = c / omega`, the normalized nonretarded law
  65matches the retarded law. -/
  66theorem crossover_retarded_eq_nonretarded
  67    (alpha omega : ℝ) (homega : 0 < omega) :
  68    casimirPolderRetarded alpha ⟨c / omega, div_pos c_pos homega⟩ =
  69      vanDerWaalsNonretarded alpha omega ⟨c / omega, div_pos c_pos homega⟩ := by
  70  unfold casimirPolderRetarded vanDerWaalsNonretarded
  71  have hω : omega ≠ 0 := ne_of_gt homega
  72  have hcω : c / omega ≠ 0 := ne_of_gt (div_pos c_pos homega)
  73  field_simp [hω, hcω]
  74
  75/-- Casimir-Polder certificate. -/
  76structure CasimirPolderCert where
  77  retarded_attractive :
  78    ∀ (alpha : ℝ) (a : PlateSeparation), 0 < alpha →
  79      casimirPolderRetarded alpha a < 0
  80  nonretarded_attractive :
  81    ∀ (alpha omega : ℝ) (a : PlateSeparation), 0 < alpha → 0 < omega →
  82      vanDerWaalsNonretarded alpha omega a < 0
  83  crossover :
  84    ∀ (alpha omega : ℝ) (homega : 0 < omega),
  85      casimirPolderRetarded alpha ⟨c / omega, div_pos c_pos homega⟩ =
  86        vanDerWaalsNonretarded alpha omega ⟨c / omega, div_pos c_pos homega⟩
  87
  88/-- Certificate instance. -/
  89def casimirPolderCert : CasimirPolderCert where
  90  retarded_attractive := casimirPolderRetarded_negative
  91  nonretarded_attractive := vanDerWaalsNonretarded_negative
  92  crossover := crossover_retarded_eq_nonretarded
  93
  94end
  95
  96end CasimirPolderAtomSurface
  97end QFT
  98end IndisputableMonolith
  99