Qft Casimir Plate Modes

The Ideal Plate Law

The Casimir effect is a physical phenomenon predicted in 1948 by Dutch physicist Hendrik Casimir. Two uncharged, perfectly conducting parallel plates placed close together in a vacuum experience a mutual attraction. This force arises from quantum fluctuations of the electromagnetic field: only certain standing wave modes can exist between the plates, while all modes exist outside. The imbalance in zero-point energy pushes the plates together. The effect has been measured in laboratories, confirming the reality of this quantum force.

For ideal plates, the energy per unit area depends on the separation a as E/A = -π²ħc/(720a³). The pressure, or force per unit area, is its derivative: P = -π²ħc/(240a⁴). This is the famous result: the pressure is negative, meaning attractive, and it scales as the inverse fourth power of the separation. Halving the distance between the plates makes the force sixteen times stronger.

The framework's machine-checked library of formal theorems, called the Recognition Science library, isolates the clean mathematical spine of this result. It defines the transverse wave numbers and mode frequencies for the ideal geometry, and the zero-point energy per mode as ħω/2. The library does not attempt to derive the zeta-function regularization that produces the π²/720 coefficient from first principles. Instead, it takes that regularized energy law as an analytic input and proves the consequences that follow from it.

What the library proves is the structure of the law. It shows the energy coefficient is positive, the pressure is exactly the negative derivative of the energy density, and the pressure is always negative, so the force is always attractive for any positive plate separation. It proves the fourth-power scaling law: multiplying the pressure by a⁴ removes all separation dependence, leaving only the constant π²ħc/240. It also proves the pressure never vanishes at any finite separation; the plates always attract.

Within the framework, Planck's constant is not a free parameter. The library substitutes its derived value, ħ = φ⁻⁵, where φ is the golden ratio, into the pressure law. This yields the form P = -π²(φ⁻⁵)c/(240a⁴). This is a formal consequence of the framework's constants, not an empirical fit. The library packages all these results into a single certificate structure, a compact formal object that bundles the coefficient positivity, the pressure-energy relation, the attractive sign, the scaling law, and the golden-ratio form into one verified unit.

The practical upshot is a rigorous, machine-checked account of the ideal parallel-plate Casimir law. The framework proves the force is attractive, scales as a⁻⁴, and connects to its derived value of Planck's constant. This provides a clean foundation for further work on the Casimir effect within the framework, such as extensions to realistic materials or finite-temperature corrections.

/-- Pressure is minus the derivative of the ideal renormalized energy density. -/
theorem idealPressure_eq_neg_energyDerivative (a : PlateSeparation) :
    idealPressure a = -idealEnergyDerivative a := by
  unfold idealPressure idealEnergyDerivative idealEnergyCoefficient
  ring

/-- The ideal Casimir pressure is attractive. -/
theorem idealPressure_negative (a : PlateSeparation) :
    idealPressure a < 0 := by
  rw [idealPressure_eq_neg_energyDerivative]
  exact neg_neg_of_pos (idealEnergyDerivative_pos a)

/-- The characteristic `a^{-4}` pressure scaling: multiplying by `a^4` removes
the separation dependence. -/
theorem idealPressure_fourth_power_scaling (a : PlateSeparation) :
    a.value ^ 4 * (-idealPressure a) = Real.pi ^ 2 * hbar * c / 240 := by
  rw [neg_idealPressure_eq_derivative]
  unfold idealEnergyDerivative idealEnergyCoefficient
  have ha : a.value ≠ 0 := ne_of_gt a.pos
  have ha4 : a.value ^ 4 ≠ 0 := pow_ne_zero 4 (ne_of_gt a.pos)
  field_simp [ha4, ha]
  ring_nf

/-- RS-native substitution of Planck's constant in the ideal pressure law. -/
theorem idealPressure_hbar_phi_form (a : PlateSeparation) :
    idealPressure a =
      -Real.pi ^ 2 * (phi ^ (-(5 : ℝ))) * c / (240 * a.value ^ 4) := by
  unfold idealPressure
  rw [hbar_eq_phi_inv_fifth]

What this page does not claim

The module does not prove the zeta-function regularization from first principles. The module does not derive the Casimir force for non-ideal or finite-temperature plates. The module does not establish the physical bridge from the framework's recognition ledger to continuous quantum field theory.

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