QFTNaiveVacuumEnergy
plain-language theorem explainer
Defines the textbook QFT-naive vacuum energy density as the fourth power of a positive UV cutoff scale. Cosmologists and QG auditors cite it as the straw-man side of the 10^120 cosmological-constant discrepancy. The body is a one-line definition: ρ_vac(Λ_UV) := Λ_UV^4, with the proportionality constant absorbed into the type.
Claim. For any positive real UV cutoff $\Lambda_{\mathrm{UV}}$, the QFT-naive vacuum energy density is $\rho_{\mathrm{vac}}(\Lambda_{\mathrm{UV}}) := \Lambda_{\mathrm{UV}}^4$ (proportionality constant absorbed). At $\Lambda_{\mathrm{UV}} = M_{\mathrm{Planck}}$ this recovers the canonical $\sim 10^{120}$ excess over the observed cosmological constant.
background
Track 4.B of the RS quantum-gravity plan addresses the vacuum-fluctuation discrepancy structurally. The standard 10^120 cosmological-constant problem assumes QFT zero-point modes contribute to Λ on equal footing with classical gravity. The naive estimate integrates modes up to a UV cutoff and yields $\rho_{\mathrm{vac}} \propto \Lambda_{\mathrm{UV}}^4$.
The parameter type is any positive real (a hypothetical QFT UV cutoff). RS does not use this mechanism: its dark-energy density is the closed form $\Omega_\Lambda = 11/16 - \alpha/\pi$, forced by eight-tick ledger combinatorics plus a measured fine-structure correction, with no vacuum-mode sum.
This definition is the straw-man side of that contrast. Upstream, omega_lambda is the 0-arity RS prediction; the cutoff type merely packages the QFT dependence that RS deliberately lacks.
proof idea
Pure definition, not a theorem. The body projects the positive real out of the subtype and raises it to the fourth power: $\Lambda_{\mathrm{UV}}.\mathrm{val}^4$. No lemmas, no tactics. The proportionality constant of the continuum mode integral is absorbed into the type, matching the usual dimensional estimate used in the 10^120 lore.
why it matters
Supplies the cutoff-dependent side of the structural distinction proved downstream: the QFT-naive estimate varies with the UV cutoff, while RS $\Omega_\Lambda$ is identical for every cutoff (definitionally, since it has no cutoff parameter). That conjunction is the content of the comparison theorem and is packaged into the Track 4.B master certificate VacuumFluctuationStructuralCert.
In the framework this closes the claim that the 10^120 discrepancy never arises inside RS: the phase-mode budget (11/16 from [4,2,2] Gray-code × eight-tick addressing, minus $\alpha/\pi$) bypasses the QFT vacuum-sum path entirely. No T0–T8 forcing step is reopened here; the module is a cosmology-track structural address, not a new forcing link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.