module module moderate

`IndisputableMonolith.StandardModel.ElectroweakBreaking`

ElectroweakBreaking defines the Higgs potential, vacuum expectation value, and resulting W/Z boson masses inside the Recognition Science Standard Model. It encodes these using J-cost minimization on the phi-ladder imported from PhiForcing and Cost. Particle physicists reconstructing electroweak parameters from the discrete ledger would cite the module. The module consists entirely of definitions and observed-value comparisons with no theorems.

claimHiggs potential $V_H$, vacuum expectation value $v$, Higgs mass $m_H$, W-boson mass $m_W$, Z-boson mass $m_Z$, and W/Z ratio, all expressed via J-cost on the phi-ladder with observed anchors $m_W^obs$, $m_Z^obs$.

background

The module sits in the Standard Model domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the J-cost structure and the proof that φ is forced by self-similarity in a discrete ledger. PhiForcing establishes that the ledger references itself at different scales, yielding the fixed point φ that sets the rung spacing on the mass ladder. Cost supplies the J-cost function used to define the Higgs potential and its minimum.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Higgs sector definitions that realize electroweak symmetry breaking from the phi-forcing chain (T5 J-uniqueness and T6 phi fixed point). It feeds the broader Standard Model mass spectrum construction, although no direct downstream theorems are listed in the current graph. It closes the link between abstract J-cost minimization and concrete boson masses.

scope and limits

Does not derive the full Standard Model Lagrangian or gauge couplings.
Does not prove the numerical values of observed masses from first principles.
Does not include running couplings or quantum corrections.
Does not address neutrino masses or extensions beyond the minimal Higgs sector.

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