  62    E_0 = ℏω/2
  63
  64    This is the minimum energy of a quantum harmonic oscillator. -/
  65noncomputable def zeroPointEnergy (ω : ℝ) : ℝ := hbar * ω / 2
  66
  67/-- The vacuum state is NOT the zero-energy state.
  68    It's the minimum-energy state, with E_0 > 0 for each mode. -/
  69theorem vacuum_has_energy :
  70    ∀ ω > 0, zeroPointEnergy ω > 0 := by
  71  intro ω hω
  72  unfold zeroPointEnergy
  73  apply div_pos
  74  · exact mul_pos hbar_pos hω
  75  · norm_num
  76
  77/-! ## Casimir Effect -/
  78
  79/-- The Casimir effect: Force between parallel plates in vacuum.
  80
  81    Boundary conditions restrict allowed modes between plates.
  82    Fewer modes → lower vacuum energy → attractive force.
  83
  84    F/A = -π²ℏc/(240 d⁴)
  85
  86    where d = plate separation. -/
  87noncomputable def casimirPressure (d : ℝ) (hd : d > 0) : ℝ :=
  88  -π^2 * hbar * c / (240 * d^4)
  89
  90theorem casimir_is_attractive (d : ℝ) (hd : d > 0) :
  91    casimirPressure d hd < 0 := by
  92  unfold casimirPressure
  93  -- The numerator is negative (−π²ℏc < 0) and denominator is positive (240d⁴ > 0)
  94  -- so the quotient is negative
  95  have h_num : -π^2 * hbar * c < 0 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.