vacuumCorrection
plain-language theorem explainer
The vacuum correction from a gauge sector s is the product of its coupling divided by pi and the factor exp(-boson mass over coherence energy). Cosmologists working on non-Abelian contributions to the dark energy density cite this expression when separating the U(1) term from suppressed SU(2) and SU(3) pieces. It is supplied by a direct one-line definition that unfolds to the stated product.
Claim. For a gauge sector with coupling constant $α$ and boson mass $M$, the vacuum correction evaluated at coherence energy $E$ equals $(α/π) exp(-M/E)$.
background
GaugeSector is the structure holding a string name, real coupling $α$, real boson mass $M$, and the two positivity hypotheses $0 < α$ and $0 ≤ M$. The module sets the local context that U(1) is massless while SU(2) and SU(3) carry mass gaps or confinement scales, so only the photon contributes an unsuppressed term to $Ω_Λ = 11/16$. Upstream, RSNativeUnits.U fixes the native units in which $c = 1$ and the coherence energy is identified with $φ^{-5}$.
proof idea
One-line wrapper that directly returns the product of the sector coupling over pi and the real exponential of the negative mass-to-energy ratio.
why it matters
This definition supplies the common expression used by the downstream theorems massless_correction, massive_suppression, u1_dominates and the certificate structure NonAbelianSuppressionCert. It encodes the leading-order claim of Dark_Energy_Mode_Counting.tex §8 Theorem 8.1 that only the U(1) sector survives at the scale $E_{coh} = φ^{-5}$. The construction closes the gap between the Recognition Composition Law and the observed cosmological constant by making the non-Abelian pieces numerically invisible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.