zeroPointModeEnergy
plain-language theorem explainer
Defines the zero-point energy of one oscillator mode as half ħ times its angular frequency. Casimir and QFT workers cite it as the per-mode building block before summing or regularizing plate spectra. The body is the textbook assignment E₀ = ħω/2 using the RS-native ħ.
Claim. For a real angular frequency $\omega$, the zero-point energy of that mode is $E_0(\omega) = \hbar\,\omega/2$, where $\hbar$ is the reduced Planck constant in RS-native units.
background
The module isolates the ideal parallel-plate Casimir spine: it takes the continuum energy law as analytic input and derives force sign, scaling, and RS-native constant consequences, without re-proving zeta or Lifshitz regularization from scratch.
Zero-point energy is the ground-state energy of a harmonic mode. In units where the mode frequency is $\omega$, the textbook assignment is $E_0 = \hbar\omega/2$. Here $\hbar$ is the RS-native action quantum, defined as $E_{\mathrm{coh}}\cdot\tau_0 = \varphi^{-5}$ (with a separate CODATA numerical twin available for SI comparisons).
Sibling definitions in the same file build transverse wave numbers, mode frequencies from plate separation, and the ideal energy density coefficient $K = \pi^2\hbar c/720$ that yields $E/A = -K/a^3$.
proof idea
Pure definition: the body is the product of the imported RS-native $\hbar$ with $\omega/2$. No lemmas, tactics, or proof obligations.
why it matters
Supplies the per-mode energy atom for the RS Casimir lane. Downstream siblings (ideal energy coefficient, density, pressure, and their positivity/sign lemmas) assemble continuum plate energetics from this seed and the standard mode spectrum. The module doc is explicit that regularization is imported, not derived; this definition keeps that boundary clean so force and scaling theorems stay local. In the broader framework it sits under QFT consequences of the forcing chain (native $\hbar = \varphi^{-5}$), not under T0–T8 themselves. No used-by edges are wired yet in the graph snapshot, so it is presently a leaf definition awaiting the energy-sum lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.