module module moderate

`IndisputableMonolith.StandardModel.ElectroweakBreaking`

The module assembles definitions for the Higgs potential, vacuum expectation value, and associated boson masses in the Standard Model using J-cost minimization. Physicists constructing electroweak symmetry breaking from discrete self-similar ledgers would cite these objects. It consists of a collection of definitions and one-line lemmas that link the phi-ladder to observed vev and mass ratios.

claimThe Higgs potential is realized as the J-cost function $J_{ m Higgs}( u)$ on the vacuum expectation value $ u$, with $ u$ minimizing $J_{ m Higgs}$ and yielding $m_W$, $m_Z$, and $m_H$ via the phi-ladder scaling.

background

The module imports the RS time quantum $ au_0 = 1$ tick from Constants, the J-cost structure from Cost, and the forcing of $\phi$ by self-similarity in a discrete ledger from PhiForcing. PhiForcing states that $oldsymbol{ ext{This module proves that }oldsymbol{ ext{φ is forced by self-similarity in a discrete ledger with J-cost}}}$. Sibling declarations introduce higgsPotential, vev, jcostHiggs, and vev_minimizes_jcost, all expressed in RS-native units where $c=1$, $ar h=oldsymbol{ ext{φ}}^{-5}$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the electroweak-breaking layer that connects T5 J-uniqueness and T6 phi fixed point to the Standard Model Higgs sector. It prepares the ground for mass formulas of the form yardstick $ imesoldsymbol{ ext{φ}}^{rung-8+gap(Z)}$ and for the alpha band constraint. No downstream theorems are recorded in the supplied graph.

scope and limits

Does not derive the full SU(2)$\times$U(1) gauge Lagrangian.
Does not compute running couplings or loop corrections.
Does not address fermion mass generation or Yukawa sector.
Does not prove stability of the potential beyond the listed minimizer.

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