goldstoneBosons
plain-language theorem explainer
The declaration enumerates the three Goldstone modes that appear when SU(2)_L × U(1)_Y breaks to U(1)_EM. A researcher modeling spontaneous symmetry breaking or the Higgs sector in Recognition Science would reference it to record the assignment of the broken generators to the longitudinal polarizations of W⁺, W⁻ and Z⁰. The definition is a direct list construction with no computation or lemmas.
Claim. The Goldstone bosons arising from electroweak symmetry breaking are the list $G^+$, $G^-$, $G^0$ that become the longitudinal components of $W^+$, $W^-$ and $Z^0$ respectively.
background
Module SM-009 derives electroweak symmetry breaking from the J-cost functional. The Higgs potential is identified with the J-cost, the vacuum expectation value is the J-cost minimum, and spontaneous breaking corresponds to the ledger selecting one configuration among the degenerate minima. The upstream constants supply the RS-native units (c = 1, ħ = ϕ⁻⁵) and the gravitational constant G expressed in the same units, but are not invoked by this definition.
proof idea
The declaration is a direct definition that constructs the three-element list of string descriptions. No tactics or lemmas are applied; the body simply enumerates the standard Goldstone-to-gauge-boson mappings.
why it matters
It supplies the explicit Goldstone content required by the electroweak-breaking mechanism (SM-009) inside the Recognition Science derivation of the Standard Model. The parent chain step is the spontaneous breaking SU(2)_L × U(1)_Y → U(1)_EM that leaves the photon massless while giving mass to W and Z via the J-cost minimum. No downstream theorems yet reference the list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.