GaugeSector
plain-language theorem explainer
GaugeSector packages the data for one gauge factor: a string name, positive real coupling, and non-negative real boson mass, each with its positivity proof. Cosmologists decomposing the vacuum-energy shift into U(1), SU(2) and SU(3) contributions cite the record when isolating the unsuppressed photon term from the exponentially damped weak and strong sectors. The definition is a plain four-field structure whose two proof obligations are discharged by norm_num or reflexivity.
Claim. A gauge sector is a record consisting of a string identifier, a coupling constant $0 < g$, and a boson mass $M$ satisfying $M = 0$ or $M > 0$, together with the two field proofs $0 < g$ and $0 ≤ M$.
background
The module shows that non-Abelian gauge corrections to Ω_Λ are exponentially suppressed. Only the U(1) photon contributes the leading α/π term; SU(2) and SU(3) sectors are suppressed by factors exp(−M/E_coh) where E_coh = φ^{-5}. The vacuum is the gauge-bond configuration with every bond at rung zero. Mass non-negativity is inherited from the density non-negativity of any spatial ledger. The phi-ladder supplies the finite-N correction 1/(φ N) to quantum-channel capacity.
proof idea
The structure is introduced directly by declaring its four fields and attaching the two positivity conditions as proof obligations. Both obligations are discharged by the norm_num tactic or by le_refl.
why it matters
GaugeSector supplies the common interface for the three sectors that appear in the vacuum-correction decomposition. It is instantiated by u1_sector, su2_sector and su3_sector and is the input type for both massless_correction and massive_suppression. The record therefore justifies the claim in Dark_Energy_Mode_Counting.tex §8, Theorem 8.1, that only the U(1) term survives at cosmological scales while the non-Abelian contributions are negligible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.