module module moderate

`IndisputableMonolith.StandardModel.ElectroweakBreaking`

Defines the electroweak sector of the Standard Model in Recognition Science units: the Higgs potential, its vacuum expectation value, and the derived W, Z, and Higgs masses. A working particle theorist would cite it when matching RS ladder predictions to collider observables. The module is mostly definitions plus one minimization identity linking the VEV to the J-cost.

claimThe module introduces the Higgs potential $V(H)$, the vacuum expectation value $v = \langle H \rangle$, observed anchors $v_{\mathrm{obs}}$, $m_H^{\mathrm{obs}}$, $m_W^{\mathrm{obs}}$, $m_Z^{\mathrm{obs}}$, the derived masses $m_H$, $m_W$, $m_Z$, the ratio $m_W/m_Z$, the Higgs J-cost $J_{\mathrm{Higgs}}$, and the claim that $v$ minimizes that cost.

background

Recognition Science works in RS-native units with $c=1$ and constants fixed by the golden ratio $\varphi$ (from PhiForcing: self-similarity of a discrete ledger with J-cost forces $\varphi$). The Cost module supplies the unique cost $J(x)=(x+x^{-1})/2-1$ that satisfies the Recognition Composition Law.

This module sits in the StandardModel domain and packages the classical electroweak breaking data against that cost. The Higgs potential is the usual quartic; the vacuum expectation value is its minimum. Observed masses and the VEV are recorded as numeric anchors so later ladder or rung comparisons can be stated without leaving Lean.

Sibling definitions cover $V(H)$, $v$, $m_H$, $m_W$, $m_Z$, the ratio $m_W/m_Z$, the Higgs-sector J-cost, and the statement that the VEV minimizes that cost.

proof idea

Primarily a definition module. Constants, Cost, and PhiForcing are imported for units and the J-cost. Most siblings are bare defs or numeric anchors (potential, VEV, observed masses, derived boson masses, W/Z ratio, Higgs J-cost). The substantive claim is the minimization identity: the recorded VEV is a critical point (minimum) of the Higgs J-cost, proved by direct calculus or algebraic completion against $J$.

why it matters in Recognition Science

Gives the electroweak breaking layer that later RS mass-ladder and coupling work must match: Higgs VEV, $m_H$, $m_W$, $m_Z$ in one place, tied to $J$. No downstream used_by edges are recorded yet, so this is a leaf packaging module rather than a proved forcing step (not T0–T8). It prepares comparisons of collider anchors to $\varphi$-ladder predictions and to the RS-native constants ($\hbar=\varphi^{-5}$, etc.). The minimization link is the bridge from ordinary SM potential language into the J-cost calculus used elsewhere in the monolith.

scope and limits

Does not derive the Higgs potential from the forcing chain T0–T8.
Does not prove mass formulas on the phi-ladder; only records SM-side anchors.
Does not compute alpha, G, or other gauge couplings.
Does not establish uniqueness of electroweak breaking beyond the local J-cost minimum.
Does not feed recorded downstream theorems yet (used_by is empty).

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (25)

def higgsPotential L51
def vev L55
def vev_observed L59
def higgsMass L62
def higgsMass_observed L66
def wBosonMass L73
def zBosonMass L78
def wZRatio L83
def mW_observed L89
def mZ_observed L90
def jcostHiggs L101
theorem vev_minimizes_jcost L109
theorem symmetry_breaking_from_jcost L125
theorem vev_higgs_ratio L138
theorem vev_higgs_ratio_not_one L146
theorem hierarchy_problem L162
theorem rs_hierarchy L179
def goldstoneBosons L196
theorem photon_massless L203
theorem observed_wz_mass_hierarchy L208
def higgsDiscovery L225
def higgsFermionCoupling L235
def higgsGaugeCoupling L236
def summary L248
structure ElectroweakBreakingFalsifier L262