higgsMass_observed
plain-language theorem explainer
The declaration supplies the empirical Higgs boson mass of 125 GeV as an input constant for electroweak calculations in Recognition Science. Researchers embedding the Standard Model would cite it when forming ratios with the vacuum expectation value. It is introduced by direct numerical assignment matching the measured value, with no derivation steps required.
Claim. The observed Higgs boson mass $m_H$ equals 125 GeV.
background
The module derives electroweak symmetry breaking from the J-cost functional, identifying the Higgs potential with the Mexican-hat form whose minimum sets the vacuum expectation value. Mass is introduced as an alias for the reals in RS-native units. Upstream results establish generations as the finite type Fin 3 matching the cube dimension and show that primitive distinctions reduce seven axioms to four structural conditions plus three definitional facts.
proof idea
The definition is a direct constant assignment of the experimental value 125 GeV. No lemmas are invoked; the body simply returns the numeral for use in ratio calculations.
why it matters
This definition supplies the numerator for the parent theorems vev_higgs_ratio and vev_higgs_ratio_not_one, which establish that the VEV-to-Higgs-mass ratio lies in (1.9, 2.1) and differs from 1. It anchors the J-cost minimum to the observed spectrum, consistent with the phi-ladder mass formula and the eight-tick octave. It leaves open the derivation of the precise numerical value from the Recognition Composition Law without external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.