Qft Casimir Zeta Regularization

The 1/120 that pays the rent

The Casimir effect is the small, attractive force between two uncharged conducting plates placed close together in a vacuum. Predicted by Hendrik Casimir in 1948, the effect is now a measured laboratory phenomenon. The standard calculation sums the energy of every allowed electromagnetic wave between the plates. That sum is infinite, because there are infinitely many modes, each with a tiny but nonzero energy. Zeta regularization is one way to assign a finite value to such a divergent series, and it recovers the textbook result: the energy density between ideal plates is proportional to -π²ħc/(720a³), where a is the plate separation.

The trick is to treat the divergent sum as a special value of the Riemann zeta function, the function ζ(s) that sums 1/n^s. The sum of mode energies corresponds to ζ(-3), a value where the original series diverges. Analytic continuation, a standard technique that extends the zeta function beyond its original domain, gives ζ(-3) = 1/120. This single number is the entire content of the regularization: it converts a meaningless infinity into the finite coefficient that matches experiment.

In Recognition Science, the framework models physical structure through a discrete record of events called a ledger, and its machine-checked library of formal theorems imports this classical result. The framework establishes, as a proved theorem, that ζ(-3) = 1/120 in the complex numbers, and that this value is the real shadow used in the plate-energy expression. It then proves that the regularized mode sum, built from this special value, exactly equals the ideal energy density already defined in the framework. The framework packages both facts into a single certificate structure, a formal object that records the zeta value and the energy-density equality as a bundled proof.

The practical consequence is that the framework does not need to invent its own regularization scheme. It inherits the standard special value from the classical theory and proves, in the kernel, that the zeta-regularized expression matches the ideal plate energy. What the framework does not do is derive the boundary-mode analysis from first principles; that part of the physical bridge remains a model, not a theorem. The special value is imported, not re-derived from the ledger axioms, and the framework's own constants, such as ħ, appear in the final formula as defined quantities.

The result matters because it shows the framework can carry a real, measurable prediction from quantum field theory without altering its content. The 1/120 is not a framework invention; it is the same number that appears in every textbook derivation, now anchored in a machine-checked proof. For a reader, the takeaway is simple: the infinite sum that naively describes the vacuum energy between plates is tamed by a single classical value, and that value is now part of the framework's formal library.

/-- Mathlib-backed special value: `ζ(-3) = 1/120`. -/
theorem zeta_neg_three_value :
    riemannZeta (-(3 : ℂ)) = (1 / 120 : ℂ) := by
  have h := riemannZeta_neg_nat_eq_bernoulli 3
  rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 4 ≠ 1), bernoulli'_four] at h
  norm_num at h
  simpa using h

/-- Zeta regularization recovers the ideal parallel-plate energy density. -/
theorem idealEnergyDensity_from_zeta (a : PlateSeparation) :
    idealEnergyDensity a = regularizedModeSum a := by
  unfold idealEnergyDensity regularizedModeSum idealEnergyCoefficient zetaNegThreeReal
  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

/-- Zeta-regularization certificate. -/
structure ZetaRegularizationCert where
  zeta_value : riemannZeta (-(3 : ℂ)) = (1 / 120 : ℂ)
  energy_density :
    ∀ a : PlateSeparation, idealEnergyDensity a = regularizedModeSum a

What this page does not claim

The boundary-mode analysis is not derived from the ledger axioms. The special value ζ(-3) is imported from classical mathematics, not re-derived within the framework. The framework does not prove the physical existence of the Casimir force, only the equality of two formal expressions.

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