Qft Casimir Thermal

Thermal Casimir correction

The Casimir effect is a physical force between two uncharged, parallel conducting plates placed close together in a vacuum. Quantum field theory says the vacuum is not empty; it seethes with fleeting virtual particles. The plates restrict which of these quantum fluctuations can exist between them, and the imbalance in the pressure from these fluctuations pushes the plates together. This force was predicted by Hendrik Casimir in 1948 and has been measured in the laboratory. At absolute zero temperature, the force depends only on the plate separation and the fundamental constants.

Real experiments do not run at absolute zero. When the plates have a finite temperature, the thermal radiation and the thermal motion of the charges in the metal add a correction to the Casimir force. The standard result in the physics literature is that at high temperature, the leading correction to the pressure grows linearly with temperature and with the plate separation. This is the effect that the model represents.

The framework's machine-checked library of formal theorems defines a model, a deliberately simplified mathematical description, for this thermal correction. The model sets the leading correction to be proportional to temperature and separation, with a coefficient that is a free parameter. The pressure at temperature T and separation a is the ideal pressure multiplied by one plus that correction. The model makes no claim about the numerical value of that coefficient; it is a placeholder for a more complete theory.

What the model establishes is not the size of the thermal effect, but its structure. Two theorems, checked by the machine, show that the model behaves correctly at its limits. At zero temperature, the thermal pressure equals the ideal pressure exactly. And if the thermal coefficient is set to zero, the thermal pressure also equals the ideal pressure. These are not approximations; they are exact identities in the formal system. The model packages these two facts into a certificate, a single object that guarantees the model reduces to the known zero-temperature case.

This matters because it separates what is known from what is chosen. The zero-temperature recovery is a theorem, a fact proved from the definitions. The linear-in-temperature form is a model, a definitional choice that a future derivation may replace. The plain lesson is that the thermal Casimir model is a scaffold: it fixes the correct limiting behavior and leaves the coefficient open for further work.

/-- Zero temperature recovers the ideal pressure. -/
theorem thermalPressure_zero_temperature (a : PlateSeparation) :
    thermalPressure 0 a = idealPressure a := by
  unfold thermalPressure thermalCorrection
  ring

/-- Vanishing thermal coefficient recovers the ideal pressure. -/
theorem thermalPressure_zero_coefficient (T : ℝ) (a : PlateSeparation)
    (hcoef : thermalCoefficient = 0) :
    thermalPressure T a = idealPressure a := by
  unfold thermalPressure thermalCorrection
  rw [hcoef]
  ring

/-- Leading thermal correction, proportional to temperature and separation. -/
noncomputable def thermalCorrection (T a : ℝ) : ℝ :=
  thermalCoefficient * T * a

What this page does not claim

No claim that the thermal coefficient equals one is derived from first principles. No claim that this model reproduces the full measured thermal Casimir force. No claim that the linear temperature dependence is proved rather than chosen.

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/CasimirThermal.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: