massless_correction
plain-language theorem explainer
For a gauge sector with zero boson mass the vacuum correction equals the coupling divided by pi. Cosmologists modeling the leading dark energy correction from the photon sector cite this when separating U(1) from non-abelian contributions. The proof is a direct algebraic reduction that substitutes the mass hypothesis into the exponential definition and simplifies with zero and multiplication identities.
Claim. Let $s$ be a gauge sector with coupling strength $a$ and boson mass $M=0$, and let $E>0$. Then the vacuum correction from $s$ at scale $E$ equals $a/π$.
background
A gauge sector is a structure recording a gauge factor's coupling strength and its boson mass. The vacuum correction function is defined as (coupling / π) times exp(-boson mass / E), where E is the coherent energy scale. The module establishes that the U(1) photon is massless while SU(2) and SU(3) sectors carry large mass gaps, so only the photon term survives at leading order. This isolates the α/π correction to Ω_Λ = 11/16 as stated in the module's opening argument.
proof idea
The term proof unfolds the vacuum correction definition, then rewrites using the supplied massless hypothesis together with the facts that exp(0)=1, division by zero yields zero in the exponent argument, and the arithmetic identity n * 1 = n.
why it matters
This theorem supplies the U(1) case inside the non-abelian suppression certificate and inside the u1_dominates comparison. It completes the paper's Theorem 8.1 by confirming that the photon sector alone furnishes the unsuppressed α/π term while non-abelian corrections remain exponentially small. The result therefore anchors the claim that the observed dark energy density receives its leading correction from the abelian gauge factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.