Qft Casimir Polder Atom Surface

The atom-surface force

The Casimir-Polder force is the attraction between a neutral atom and a flat surface, caused by fluctuations of the electromagnetic field. It is a member of the Casimir family, which also includes the force between two uncharged plates. The effect is real and measurable: it is one of the quantum forces that matter at microscopic distances.

The force has two distinct regimes. Far from the surface, the potential falls as the inverse fourth power of distance, a⁻⁴; this is the retarded law, where the finite speed of light matters. Close to the surface, the potential falls as the inverse cube, a⁻³; this is the nonretarded van der Waals form, where the field adjusts almost instantly. The two regimes meet at a crossover length equal to c/ω, where c is the speed of light and ω is a characteristic atomic frequency.

In Recognition Science, the framework models this physical situation with two explicit formulas. The retarded potential is V(a) = −3ℏcα / (8πa⁴), and the nonretarded potential is V(a) = −3ℏcα / (8π(c/ω)a³), where α is the atom's polarizability. These are definitions, not derived theorems; the framework chooses these forms to match the standard physics.

What the framework establishes is the behavior of these definitions. Its machine-checked library of formal theorems shows that both potentials are negative when the polarizability is positive, meaning the force is attractive. It also establishes the crossover property: at the distance a = c/ω, the two formulas give exactly the same value. A certificate structure bundles these three facts, providing a compact guarantee of the framework's content.

The practical consequence is a clean, verified description of a real quantum effect. An engineer designing a microelectromechanical device, or a physicist studying atom-surface interactions, can rely on these formulas and their proven signs without re-deriving them. The framework's contribution here is not a new prediction but a formal check that the standard laws are internally consistent and attractive.

/-- Retarded Casimir-Polder potential for positive polarizability. -/
noncomputable def casimirPolderRetarded (alpha : ℝ) (a : PlateSeparation) : ℝ :=
  -3 * hbar * c * alpha / (8 * Real.pi * a.value ^ 4)

/-- Nonretarded van der Waals form normalized by an atomic frequency `omega`.
The crossover length is `c / omega`. -/
noncomputable def vanDerWaalsNonretarded
    (alpha omega : ℝ) (a : PlateSeparation) : ℝ :=
  -3 * hbar * c * alpha / (8 * Real.pi * (c / omega) * a.value ^ 3)

/-- The retarded potential is attractive for positive polarizability. -/
theorem casimirPolderRetarded_negative
    (alpha : ℝ) (a : PlateSeparation) (halpha : 0 < alpha) :
    casimirPolderRetarded alpha a < 0 := by
  unfold casimirPolderRetarded
  have hnum : 0 < 3 * hbar * c * alpha := by
    exact mul_pos (mul_pos (mul_pos (by norm_num) hbar_pos) c_pos) halpha
  have hnum_neg : -3 * hbar * c * alpha < 0 := by
    nlinarith
  have hden : 0 < 8 * Real.pi * a.value ^ 4 := by
    exact mul_pos (mul_pos (by norm_num) Real.pi_pos) (pow_pos a.pos 4)
  exact div_neg_of_neg_of_pos hnum_neg hden

/-- The nonretarded potential is attractive for positive polarizability and
positive atomic frequency. -/
theorem vanDerWaalsNonretarded_negative
    (alpha omega : ℝ) (a : PlateSeparation)
    (halpha : 0 < alpha) (homega : 0 < omega) :
    vanDerWaalsNonretarded alpha omega a < 0 := by
  unfold vanDerWaalsNonretarded
  have hcrossover : 0 < c / omega := div_pos c_pos homega
  have hnum : 0 < 3 * hbar * c * alpha := by
    exact mul_pos (mul_pos (mul_pos (by norm_num) hbar_pos) c_pos) halpha
  have hnum_neg : -3 * hbar * c * alpha < 0 := by
    nlinarith
  have hden : 0 < 8 * Real.pi * (c / omega) * a.value ^ 3 := by
    exact mul_pos (mul_pos (mul_pos (by norm_num) Real.pi_pos) hcrossover) (pow_pos a.pos 3)
  exact div_neg_of_neg_of_pos hnum_neg hden

/-- At the crossover length `a = c / omega`, the normalized nonretarded law
matches the retarded law. -/
theorem crossover_retarded_eq_nonretarded
    (alpha omega : ℝ) (homega : 0 < omega) :
    casimirPolderRetarded alpha ⟨c / omega, div_pos c_pos homega⟩ =
      vanDerWaalsNonretarded alpha omega ⟨c / omega, div_pos c_pos homega⟩ := by
  unfold casimirPolderRetarded vanDerWaalsNonretarded
  have hω : omega ≠ 0 := ne_of_gt homega
  have hcω : c / omega ≠ 0 := ne_of_gt (div_pos c_pos homega)
  field_simp [hω, hcω]

What this page does not claim

The module does not derive the Casimir-Polder force from first principles; it defines the standard laws and proves their properties. The framework does not claim a new numerical prediction for the force strength beyond the standard formulas. This page does not cover the force between two plates, which is a separate member of the Casimir family.

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