module module moderate

`IndisputableMonolith.StandardModel.ElectroweakBreaking`

This module defines the Higgs potential together with the vacuum expectation value and boson masses in Recognition Science units. Particle physicists checking electroweak-scale predictions against the phi-ladder would cite these objects. The module is a collection of definitions that import J-cost and phi-forcing results without performing derivations.

claimThe Higgs potential takes the form $V(H) = f(J(H), v)$ where $v$ is the vacuum expectation value that minimizes the J-cost on the phi-ladder, yielding $m_W$ and $m_Z$ via the standard electroweak relations in RS-native units.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants, the J-cost ledger structure from Cost, and the self-similarity argument that forces φ from PhiForcing. These supply the discrete ledger and cost function used to express electroweak quantities. The local setting is the Standard Model Higgs sector re-expressed so that the vacuum expectation value arises from J-cost minimization rather than an independent parameter.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the Higgs sector that connects the phi-forced constants to the observed W and Z masses inside the Standard Model construction. They prepare the ground for later mass-formula applications on the phi-ladder and for any future derivation of the potential shape from the Recognition Composition Law.

scope and limits

Does not derive the quartic form of the potential from the J-functional equation.
Does not compute numerical values for vev or boson masses.
Does not address fermion masses or the number of generations.
Does not include loop corrections or running couplings.

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