IndisputableMonolith.QFT.CasimirZetaRegularization

   1import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
   2import IndisputableMonolith.QFT.CasimirPlateModes
   3
   4/-!
   5# Casimir Zeta Regularization
   6
   7This module supplies the analytic special-value input for the ideal
   8parallel-plate Casimir energy.  The hard QFT boundary-mode analysis is still a
   9bridge model, but the special value `ζ(-3) = 1/120` is imported from Mathlib's
  10Bernoulli-number theorem.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace QFT
  15namespace CasimirZetaRegularization
  16
  17open CasimirPlateModes
  18open Constants
  19
  20noncomputable section
  21
  22/-- Mathlib-backed special value: `ζ(-3) = 1/120`. -/
  23theorem zeta_neg_three_value :
  24    riemannZeta (-(3 : ℂ)) = (1 / 120 : ℂ) := by
  25  have h := riemannZeta_neg_nat_eq_bernoulli 3
  26  rw [bernoulli_eq_bernoulli'_of_ne_one (by decide : 4 ≠ 1), bernoulli'_four] at h
  27  norm_num at h
  28  simpa using h
  29
  30/-- The real special value used by the scalar plate-energy expression. -/
  31noncomputable def zetaNegThreeReal : ℝ := 1 / 120
  32
  33/-- The real special value is the real shadow of Mathlib's complex zeta value. -/
  34theorem zetaNegThreeReal_complex :
  35    (zetaNegThreeReal : ℂ) = riemannZeta (-(3 : ℂ)) := by
  36  rw [zeta_neg_three_value]
  37  unfold zetaNegThreeReal
  38  norm_num
  39
  40/-- Regularized scalar mode sum after subtracting the continuum exterior and
  41retaining the finite plate-dependent term.  The `1/6` geometry factor converts
  42`ζ(-3)=1/120` into the standard `1/720` coefficient. -/
  43noncomputable def regularizedModeSum (a : PlateSeparation) : ℝ :=
  44  -(Real.pi ^ 2 * hbar * c / (6 * a.value ^ 3)) * zetaNegThreeReal
  45
  46/-- Zeta regularization recovers the ideal parallel-plate energy density. -/
  47theorem idealEnergyDensity_from_zeta (a : PlateSeparation) :
  48    idealEnergyDensity a = regularizedModeSum a := by
  49  unfold idealEnergyDensity regularizedModeSum idealEnergyCoefficient zetaNegThreeReal
  50  have ha : a.value ≠ 0 := ne_of_gt a.pos
  51  have ha3 : a.value ^ 3 ≠ 0 := pow_ne_zero 3 ha
  52  field_simp [ha, ha3]
  53  ring
  54
  55/-- Zeta-regularization certificate. -/
  56structure ZetaRegularizationCert where
  57  zeta_value : riemannZeta (-(3 : ℂ)) = (1 / 120 : ℂ)
  58  energy_density :
  59    ∀ a : PlateSeparation, idealEnergyDensity a = regularizedModeSum a
  60
  61/-- Certificate instance for the zeta-regularized Casimir energy. -/
  62def zetaRegularizationCert : ZetaRegularizationCert where
  63  zeta_value := zeta_neg_three_value
  64  energy_density := idealEnergyDensity_from_zeta
  65
  66end
  67
  68end CasimirZetaRegularization
  69end QFT
  70end IndisputableMonolith
  71