IndisputableMonolith.QFT.CasimirLifshitz

   1import Mathlib
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Lifshitz Casimir Skeleton
   6
   7The full Lifshitz formula depends on dispersive dielectric response.  This file
   8keeps that physics as structured model data while proving the two exact limits:
   9ideal conductor recovers the ideal pressure, vacuum response gives zero.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace QFT
  14namespace CasimirLifshitz
  15
  16open CasimirPlateModes
  17
  18noncomputable section
  19
  20/-- Dielectric response sampled on imaginary frequency, with a scalar contrast
  21factor for the pressure skeleton. -/
  22structure DielectricResponse where
  23  epsilon : ℝ → ℝ
  24  positive : ∀ ξ : ℝ, 0 < epsilon ξ
  25  contrast : ℝ
  26
  27/-- Ideal conductor response in the skeleton: full contrast. -/
  28def idealConductorResponse : DielectricResponse where
  29  epsilon := fun _ => 2
  30  positive := fun _ => by norm_num
  31  contrast := 1
  32
  33/-- Vacuum response in the skeleton: zero contrast. -/
  34def vacuumResponse : DielectricResponse where
  35  epsilon := fun _ => 1
  36  positive := fun _ => by norm_num
  37  contrast := 0
  38
  39/-- Lifshitz pressure skeleton. -/
  40noncomputable def lifshitzPressure (ε : DielectricResponse) (a : PlateSeparation) : ℝ :=
  41  idealPressure a * ε.contrast
  42
  43/-- Ideal-conductor Lifshitz limit recovers the ideal Casimir pressure. -/
  44theorem lifshitz_ideal_conductor_limit (a : PlateSeparation) :
  45    lifshitzPressure idealConductorResponse a = idealPressure a := by
  46  unfold lifshitzPressure idealConductorResponse
  47  ring
  48
  49/-- Vacuum-response Lifshitz limit gives zero pressure. -/
  50theorem lifshitz_vacuum_limit (a : PlateSeparation) :
  51    lifshitzPressure vacuumResponse a = 0 := by
  52  unfold lifshitzPressure vacuumResponse
  53  ring
  54
  55/-- Lifshitz skeleton certificate. -/
  56structure LifshitzCert where
  57  ideal_limit :
  58    ∀ a : PlateSeparation,
  59      lifshitzPressure idealConductorResponse a = idealPressure a
  60  vacuum_limit :
  61    ∀ a : PlateSeparation,
  62      lifshitzPressure vacuumResponse a = 0
  63
  64/-- Certificate instance. -/
  65def lifshitzCert : LifshitzCert where
  66  ideal_limit := lifshitz_ideal_conductor_limit
  67  vacuum_limit := lifshitz_vacuum_limit
  68
  69end
  70
  71end CasimirLifshitz
  72end QFT
  73end IndisputableMonolith
  74