su2_sector
plain-language theorem explainer
The SU(2) weak sector is instantiated as a GaugeSector record carrying coupling 1/(137.036 * 0.231) and boson mass 80.4 GeV. Cosmologists modeling vacuum-energy corrections cite this record to quantify the exponential suppression of non-Abelian terms relative to the U(1) photon contribution at the coherence scale. The definition is assembled by direct structure construction with norm_num discharging the two positivity obligations.
Claim. The SU(2) gauge sector is the structure with name ``SU(2)'', coupling constant $1/(137.036 times 0.231)$, boson mass $80.4$ GeV, and proofs that the coupling is positive and the mass is nonnegative.
background
A GaugeSector is a structure containing a name string, a real coupling, a real boson mass, and proofs that the coupling is positive and the mass is nonnegative. The module instantiates separate sectors for U(1), SU(2) and SU(3) so that their vacuum corrections can be compared at the coherence energy $E_{coh} = phi^{-5} approx 0.09$ eV. The upstream result mass_nonneg states that mass extracted from any spatial ledger is nonnegative and is invoked to satisfy the structure field.
proof idea
The definition supplies the four fields of the GaugeSector structure directly. The two proof obligations (coupling positive and mass nonnegative) are discharged by the norm_num tactic, which reduces the numerical inequalities to decidable arithmetic.
why it matters
This definition supplies the concrete parameters required by the certificate NonAbelianSuppressionCert and by the comparison theorem u1_dominates. It thereby completes the argument that only the U(1) correction survives at leading order while the SU(2) term is suppressed by exp(-M_W / E_coh) with ratio approximately 9 times 10^11. The construction directly supports the claim in Dark_Energy_Mode_Counting.tex section 8 that non-Abelian contributions are negligible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.