GaugeBosonMass
plain-language theorem explainer
This structure packages a gauge boson identifier, its real mass, and gauge coupling for use in the Recognition Science derivation of electroweak masses. Researchers modeling spontaneous symmetry breaking via J-cost would cite it when assembling relations for W and Z bosons from the vacuum expectation value. The declaration is a bare structure definition with three fields and no proof body.
Claim. A gauge boson mass record consists of a string identifier for the boson, a real number $m$ for its mass, and a real number $g$ for its gauge coupling constant.
background
The module derives the Higgs mechanism from the J-cost functional $J(x) = ½(x + 1/x) - 1$, which has a minimum of zero at $x=1$ and obeys the symmetry $J(x)=J(1/x)$. Symmetry breaking occurs when the vacuum selects the golden-ratio fixed point, after which particle masses arise proportional to the J-cost evaluated at that point times the vacuum expectation value. Upstream, Mass is defined as the real numbers, while W and Z anchors supply integer maps from sectors and charges that feed into mass ladders.
proof idea
This is a plain structure definition that introduces the record type with three fields: boson name, mass value, and gauge coupling.
why it matters
The record supports the SM-002 target of deriving spontaneous symmetry breaking and gauge-boson masses from J-cost structure. It supplies the data container needed to state the mass-generation formula $m ∝ J(v) × vev$ once the vacuum expectation value is fixed by the phi-ladder. It connects directly to T5 J-uniqueness and the eight-tick octave that fixes spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.