ew_vector_gauge
plain-language theorem explainer
EW vector gauge supplies the electroweak sector parameters B_B = 2 and r0 = 55 with 0.12 percent mismatch for phi-ladder alignment. Mass spectroscopists and unification modelers cite this when matching W and Z boson masses to the common structural scale. The definition directly instantiates the SectorGauge record using the electroweak entry from the upstream r0 function.
Claim. The electroweak vector boson yardstick is the structure with multiplicative gauge $B_B = 2$, additive rung offset $r_0 = 55$, and empirical mismatch $0.0012$.
background
SectorGauge is the record type holding three fields: B_B as the multiplicative amplitude gauge, r0 as the additive rung offset including global phase shift, and mismatch as the empirical percentage deviation. The module formalizes sector-global gauge parameters that align the phi-ladder across fermionic sectors. Upstream, the r0 function in Masses.Anchor derives the electroweak offset as 3 times W plus 4, equaling 55, while scale provides the phi^k ladder steps.
proof idea
The definition populates the SectorGauge structure directly with the electroweak values B_B equal to 2 to the power 1, r0 equal to 55, and mismatch 0.0012.
why it matters
This definition supplies the electroweak entry among the sector yardsticks, enabling the mass formula alignment m_i = A_B * phi^(r_i + f_B) to the common scale. It supports the gauge alignment result stated in the module comment. In the Recognition framework it instantiates the phi-ladder alignment for the electroweak sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.