regularizedModeSum
plain-language theorem explainer
The regularized scalar mode sum at plate separation a is the finite, plate-dependent Casimir energy density after continuum subtraction: −(π² ℏ c /(6 a³))·ζ(−3). Anyone matching zeta regularization to the ideal parallel-plate formula cites it. It is a direct algebraic definition that folds the geometry factor with the real special value ζ(−3)=1/120 into the classical 1/720 coefficient.
Claim. For plate separation $a>0$, the regularized scalar mode sum is $-\frac{\pi^2 \hbar c}{6 a^3}\,\zeta(-3)$, where $\zeta(-3)=1/120$ is taken as a real number. Equivalently the expression equals $-\frac{\pi^2 \hbar c}{720 a^3}$.
background
The module supplies analytic special-value input for the ideal parallel-plate Casimir energy. Hard QFT boundary-mode analysis remains a bridge model; the special value $\zeta(-3)=1/120$ is imported from Mathlib's Bernoulli-number theorem.
Plate separation $a$ is a positive real parameter. The native action quantum is $\hbar=\varphi^{-5}$ in RS units (with $c$ the speed of light). The real special value $\zeta(-3)$ is packaged as a real constant equal to $1/120$. The geometry prefactor $1/6$ converts that special value into the textbook $1/720$ coefficient of the parallel-plate energy density.
Upstream, the definition only needs the constants $\hbar$, $c$, the plate-separation carrier, and the real embedding of $\zeta(-3)$. No mode-sum convergence proof is performed here.
proof idea
Definitional packaging, not a proof. The body multiplies the signed prefactor $-\pi^2 \hbar c/(6 a^3)$ by the real constant equal to $\zeta(-3)$. The $1/6$ is the geometric conversion that turns $1/120$ into $1/720$; no tactics or lemmas are invoked beyond evaluating those constants.
why it matters
This is the explicit zeta-regularized energy density that the certificate and equality theorems identify with the ideal parallel-plate formula. Downstream, idealEnergyDensity_from_zeta proves the ideal density equals this expression by unfolding and field simplification. ZetaRegularizationCert packages the Mathlib identity $\zeta(-3)=1/120$ together with that equality for every separation. The sphere-plate PFA certificate also consumes the same regularized density when checking attractive cubic scaling.
In the broader RS stack the object is bridge infrastructure: it locks the classical Casimir $1/a^3$ law to a certified special value while the full boundary-mode QFT analysis stays external. It does not itself touch the forcing chain (T5–T8) or the mass ladder; it only feeds the QFT Casimir layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.