Qft Casimir Pfa

The proximity force approximation

The proximity force approximation, or PFA, is a standard shortcut in quantum field theory for estimating the Casimir force, the attractive pull between two uncharged conducting plates caused by quantum vacuum fluctuations. For a sphere of radius R hovering above a flat plate, PFA says the force equals 2πR times the energy density of the parallel-plate setup at the closest separation. This turns a hard curved-geometry calculation into a simpler flat-plate one, and it is the usual way experimentalists interpret sphere-plate measurements. The approximation was introduced in the 1930s by Hendrik Casimir and Dirk Polder, who first derived the force between two atoms, and it was later extended to macroscopic bodies.

The approximation is attractive for any positive radius and separation, which matches the physical expectation that the vacuum pulls the sphere toward the plate. It also scales with the cube of the separation: the force grows as the inverse third power of the gap. In symbols, the PFA force F satisfies a³(−F) = Rπ³ħc/360, where a is the separation and ħ and c are the reduced Planck constant and the speed of light. This cubic scaling is a signature of the PFA that experiments can check directly, since it predicts how the force changes as the sphere-plate distance varies.

In Recognition Science, the framework models the PFA in its machine-checked library of formal theorems, a collection of statements verified by a computer kernel. The library defines the PFA force exactly as 2πR times the ideal parallel-plate energy density, and then proves two theorems about it: that the force is always attractive for positive radius, and that it obeys the cubic scaling law above. These are not empirical claims but formal derivations from the definition, so they hold by construction for any real numbers satisfying the hypotheses. The library also bundles these results into a certificate structure, a single object that packages the attractiveness, the scaling, and the fact that the ideal energy density matches a zeta-regularized sum over modes, which is the standard technique for handling the infinite vacuum energy.

The practical payoff is that the PFA, despite being an approximation, carries rigorous properties that a computer has checked. For an experimentalist, the cubic scaling law is a direct test: if the measured force deviates from the a⁻³ trend, that signals the approximation is breaking down and the full curved-geometry calculation is needed. For the framework, the certificate shows that even an approximate tool used in real measurements can be stated and verified with the same precision as an exact theorem. The PFA does not replace the exact Casimir calculation, but it gives a reliable bridge from theory to experiment, and the library has now made that bridge explicit and auditable.

/-- PFA force is attractive for positive radius and positive separation. -/
theorem pfaForce_attractive_of_R_pos
    (R : ℝ) (a : PlateSeparation) (hR : 0 < R) :
    pfaForce R a < 0 := by
  unfold pfaForce idealEnergyDensity
  have hcoef : 0 < idealEnergyCoefficient := idealEnergyCoefficient_pos
  have henergy : -idealEnergyCoefficient / a.value ^ 3 < 0 := by
    exact div_neg_of_neg_of_pos (neg_neg_of_pos hcoef) (pow_pos a.pos 3)
  exact mul_neg_of_pos_of_neg (mul_pos (mul_pos (by norm_num) Real.pi_pos) hR) henergy

/-- PFA has cubic separation scaling. -/
theorem pfaForce_cubic_scaling
    (R : ℝ) (a : PlateSeparation) :
    a.value ^ 3 * (-pfaForce R a) =
      R * (Real.pi ^ 3 * hbar * c) / 360 := by
  unfold pfaForce idealEnergyDensity idealEnergyCoefficient
  have ha : a.value ≠ 0 := ne_of_gt a.pos
  have ha3 : a.value ^ 3 ≠ 0 := pow_ne_zero 3 ha
  field_simp [ha, ha3]
  ring

/-- Certificate instance for sphere-plate PFA. -/
def spherePlateCert : SpherePlateCert where
  attractive := pfaForce_attractive_of_R_pos
  cubic_scaling := pfaForce_cubic_scaling
  zeta_backed_energy := CasimirZetaRegularization.idealEnergyDensity_from_zeta

What this page does not claim

The PFA is an exact solution to the Casimir problem, not an approximation. The framework derives the PFA from more fundamental principles; it defines and proves properties of the approximation. The measured Casimir force matches the PFA prediction to any stated precision.

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