module module high

`IndisputableMonolith.QFT.HiggsMechanism`

The QFT.HiggsMechanism module defines the J-cost functional J(x) = ½(x + 1/x) - 1 together with vev, symmetry_broken, massParameter, YukawaCoupling, and particleMass to support Higgs mechanism constructions in Recognition Science. Researchers deriving particle masses from the phi-ladder would cite these objects when extending the framework to QFT. The module is purely definitional and supplies the objects required by the parent QFT module.

claim$J(x) = ½(x + x^{-1}) - 1$ for $x > 0$, with definitions of vacuum expectation value, symmetry breaking condition, mass parameter, Yukawa coupling, and particle mass on the phi-ladder.

background

The module lies in the QFT domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost framework from Cost. Its central object is the J-cost functional, which quantifies recognition cost for positive reals and serves as the starting point for symmetry breaking and mass generation. Key sibling definitions introduce the vacuum expectation value, the symmetry_broken predicate, massParameter, YukawaCoupling, and particleMass derived from the phi-ladder.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

These definitions feed the parent QFT module, which collects Tier 2 derivations of quantum field theory fundamentals from Recognition Science. The module supplies the concrete objects needed to connect the J-cost and phi-ladder to the Higgs mechanism and particle masses.

scope and limits

Does not contain theorems or proofs.
Does not reference the full forcing chain or T0-T8 steps.
Does not compute numerical mass values or spectra.
Does not address gauge boson masses or renormalization.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.QFT module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (27)

def J L58
theorem J_min_at_one L61
theorem J_at_one L69
theorem J_symmetric L74
def vev L83
theorem vev_pos L86
theorem vev_gt_one L89
theorem symmetry_broken L96
def massParameter L115
theorem mass_parameter_pos L118
structure YukawaCoupling L127
def particleMass L137
theorem mass_positive L141
structure HiggsBoson L149
def higgsMassSquared L157
theorem higgs_mass_squared_pos L165
structure GaugeBosonMass L174
def wBosonMass L183
def zBosonMass L186
def photonMass L190
theorem photon_massless L193
theorem phi_gt_one' L198
theorem phi_symmetry_breaking L202
theorem higgs_mechanism_nonzero_vev L211
theorem higgs_mechanism_vev_ne_one L214
theorem mass_parameter_ne_zero L219
structure HiggsFalsifier L228