u1_sector
plain-language theorem explainer
The declaration defines the U(1) electromagnetic gauge sector with coupling 1/137.036 and zero boson mass. Cosmologists modeling dark energy corrections in Recognition Science cite it as the source of the unsuppressed α/π term. It is a direct GaugeSector structure instance whose positivity and non-negativity fields are discharged by norm_num and le_refl.
Claim. The U(1) gauge sector is the structure with name string U(1), coupling constant $1/137.036$, boson mass $0$, together with the proofs that the coupling is positive and the mass is non-negative.
background
GaugeSector is the structure type carrying a name string, a real coupling, a real boson mass, and the two side conditions that the coupling is positive and the mass is non-negative. The module NonAbelianSuppression states that the U(1) electromagnetic sector supplies the complete leading-order correction α/π to Ω_Λ = 11/16 while the SU(2) and SU(3) sectors are exponentially suppressed by their mass gaps relative to the coherence scale E_coh = φ^{-5}. Upstream, RSNativeUnits.U fixes the native units with c = 1, and le_refl supplies the trivial non-negativity fact for the zero mass.
proof idea
The definition is a direct structure literal. The coupling field is set to the literal 1/137.036, the boson mass to the literal 0, the coupling_pos field is discharged by norm_num, and the mass_nonneg field is discharged by le_refl from ArithmeticFromLogic.
why it matters
u1_sector is the concrete U(1) datum supplied to NonAbelianSuppressionCert and to the u1_dominates theorem, which together prove that the α/π correction is complete while non-abelian corrections vanish. It realises the U(1) case of Theorem 8.1 in Dark_Energy_Mode_Counting.tex §8. In the Recognition framework it anchors the massless photon contribution at zero momentum inside the gauge structure of Aut(Q₃), consistent with the eight-tick octave and the alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.