u1_dominates
plain-language theorem explainer
The declaration shows that the vacuum correction from the U(1) electromagnetic sector strictly exceeds the correction from the SU(2) weak sector at every positive energy scale E. Cosmologists computing the leading-order dark-energy density would cite the result to drop non-Abelian gauge contributions from the Ω_Λ budget. The argument is a term-mode reduction that rewrites the U(1) side to its unsuppressed α/π value and bounds the SU(2) side below its coupling/π value by the exponential mass-gap inequality.
Claim. For every real number $E > 0$, the vacuum correction of the SU(2) gauge sector is strictly smaller than the vacuum correction of the U(1) gauge sector: $v(su2,E) < v(u1,E)$, where $v(s,E) = g_s/π · exp(-m_s/E)$, $g_{u1} = 1/137.036$, $m_{u1} = 0$, $g_{su2} = 1/(137.036·0.231)$, and $m_{su2} = 80.4$.
background
The module shows that non-Abelian gauge corrections to the vacuum energy are exponentially suppressed relative to the U(1) contribution. The vacuum correction for a gauge sector s at coherent energy E is defined by $v(s,E) = g_s/π · exp(-m_s/E)$, where g_s is the coupling constant and m_s the boson mass. For the U(1) sector the mass vanishes, so the exponential factor equals one and the correction equals α/π. For the SU(2) sector the W/Z bosons carry mass 80.4 GeV, producing an enormous negative exponent at the relevant scale E ≈ 0.09 eV.
proof idea
The proof is a term-mode reduction. It first rewrites the U(1) term by invoking the massless_correction lemma with the reflexivity proof that the U(1) boson mass is zero. It then applies the massive_suppression lemma to the SU(2) term, supplying a norm_num proof that the SU(2) boson mass is positive. The two steps together establish the strict inequality.
why it matters
The result fills the leading-order claim of Dark_Energy_Mode_Counting.tex §8, Theorem 8.1 that only the U(1) correction survives. Within the Recognition Science framework it confirms that the coherent energy scale set by φ^{-5} renders the non-Abelian mass gaps irrelevant, consistent with the forcing chain that fixes D = 3 and the eight-tick octave. The module as a whole closes the argument that Ω_Λ receives its dominant correction solely from the electromagnetic sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.