Qft Casimir Lifshitz

The Lifshitz skeleton

The Casimir effect is a physical phenomenon where two uncharged, conducting plates placed very close together in a vacuum attract each other. The attraction comes from quantum fluctuations of the electromagnetic field: the plates restrict which field modes can exist between them, and the resulting imbalance in vacuum pressure pushes the plates together. The standard formula for this force, derived by Hendrik Casimir in 1948, predicts a pressure that depends only on the plate separation and fundamental constants.

The Lifshitz formula, developed by Evgeny Lifshitz in 1956, generalizes the Casimir effect to real materials with finite conductivity and dispersive properties. Instead of assuming perfect conductors, it uses the frequency-dependent dielectric response of the materials to compute the pressure. The full formula is an integral over imaginary frequencies of a complicated expression involving the dielectric functions of both plates and the medium between them.

In Recognition Science, the framework models the Casimir-Lifshitz system as a skeleton: it keeps the dielectric response as structured data but focuses on proving two exact limiting cases. The first limit is the ideal conductor, where the dielectric response has full contrast. For this case, the framework proves that the Lifshitz pressure reduces exactly to the ideal Casimir pressure. The second limit is vacuum response, where the contrast is zero, and the framework proves that the pressure becomes exactly zero.

These two theorems are machine-checked in the framework's library of formal theorems. They establish that the skeleton is consistent: it correctly recovers the known ideal-conductor limit and the trivial vacuum limit. The full dispersive physics, with a frequency-dependent dielectric function, remains as structured model data, not as a derived theorem.

The practical consequence is that the framework can serve as a reliable foundation for further work on the Casimir effect. Researchers can extend the skeleton by adding the full frequency integral, knowing that the two extreme cases are already verified. The framework's contribution is not a new physical prediction but a formal guarantee that its model reduces correctly in the two simplest physical situations.

/-- Ideal-conductor Lifshitz limit recovers the ideal Casimir pressure. -/
theorem lifshitz_ideal_conductor_limit (a : PlateSeparation) :
    lifshitzPressure idealConductorResponse a = idealPressure a := by
  unfold lifshitzPressure idealConductorResponse
  ring

/-- Vacuum-response Lifshitz limit gives zero pressure. -/
theorem lifshitz_vacuum_limit (a : PlateSeparation) :
    lifshitzPressure vacuumResponse a = 0 := by
  unfold lifshitzPressure vacuumResponse
  ring

/-- Dielectric response sampled on imaginary frequency, with a scalar contrast
factor for the pressure skeleton. -/
structure DielectricResponse where
  epsilon : ℝ → ℝ
  positive : ∀ ξ : ℝ, 0 < epsilon ξ
  contrast : ℝ

What this page does not claim

The full dispersive Lifshitz formula is not proved here. The skeleton does not predict new physics beyond the two limits. The framework does not derive the Casimir force from first principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/QFT/CasimirLifshitz.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: