su3_sector
plain-language theorem explainer
The su3_sector definition supplies the SU(3) gauge sector parameters used to show non-abelian corrections remain negligible for the vacuum energy density. Cosmologists working within the Recognition Science derivation of dark energy would cite it when assembling the full set of gauge sectors. The definition is realized by direct assignment of name, coupling 0.118, and boson mass 1.5 to the GaugeSector structure, with the two positivity conditions discharged by norm_num.
Claim. The SU(3) gauge sector is the structure with name SU(3), coupling constant $0.118$, and boson mass $1.5$ (in GeV), satisfying $0 < 0.118$ and $0.5$ is nonnegative.
background
GaugeSector is the structure that packages a gauge factor by its name, coupling strength, and boson mass together with the two inequalities that the coupling is positive and the mass is nonnegative. The module NonAbelianSuppression places this structure inside the argument that only the U(1) factor supplies a leading-order correction to Ω_Λ = 11/16 while SU(2) and SU(3) are exponentially suppressed by their mass gaps relative to the coherence scale φ^{-5}. Upstream, the RS-native units definition supplies the normalization in which c = 1 and the scale function from LargeScaleStructureFromRS supplies the powers of φ used to compare masses to E_coh.
proof idea
The definition constructs the GaugeSector instance by literal field assignment for name, coupling, and boson_mass, then applies the norm_num tactic to the two field proofs coupling_pos and mass_nonneg.
why it matters
This definition completes the concrete data for the three gauge sectors required by the module-level claim that non-abelian corrections vanish at the coherence scale. It directly supports the statement in Dark_Energy_Mode_Counting.tex §8, Theorem 8.1 that the α/π correction is carried entirely by the abelian sector. Within the Recognition Science chain the construction keeps the eight-tick octave and D = 3 spatial dimensions free of additional non-abelian contributions at leading order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.