module module moderate

`IndisputableMonolith.QFT.HiggsMechanism`

Module that recasts the Higgs mechanism in Recognition Science QFT using the unique J-cost. It defines a vacuum expectation value above the J-minimum, records spontaneous symmetry breaking, and builds particle masses from a positive mass parameter times Yukawa couplings. Mass-spectrum workers cite vev and particleMass. The file is mostly definitions plus short positivity and ordering lemmas.

claimThe module introduces the J-cost $J(x)=\frac12(x+1/x)-1$ for $x>0$ (minimum uniquely at $x=1$), a vacuum expectation value $\mathrm{vev}>1$, the assertion that symmetry is broken when the vacuum sits away from that minimum, a positive mass parameter, Yukawa couplings, and the induced particle masses.

background

Recognition Science forces a unique nonnegative cost on positive reals via the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$, with $J(1)=0$ and $J(x)=J(1/x)$. In the QFT layer this cost replaces the usual Mexican-hat potential; the vacuum is required to sit at a point where $J>0$, so residual scale symmetry that would keep masses zero is broken.

The module imports Constants (RS-native units, including the tick $\tau_0$) and Cost (the J-functional and its elementary identities). Sibling definitions supply the vacuum expectation value, proofs that it is positive and strictly larger than 1, a symmetry-broken flag, a positive mass parameter, a Yukawa coupling type, and the resulting particle-mass map.

proof idea

Definition module with supporting lemmas, not a single deep theorem. J and its minimum-at-one, value-at-one, and reflection symmetry are taken from Cost or restated. vev is introduced by definition; vev_pos and vev_gt_one are short positivity/ordering arguments. symmetry_broken is the proposition that the vacuum lies off the J-minimum. massParameter, its positivity, YukawaCoupling, and particleMass are straight definitions assembling the usual mass-generation formula in RS units.

why it matters in Recognition Science

Anchors the classical Higgs story inside the RS forcing chain by tying the vacuum to the T5-unique J-cost. Supplies the QFT-side bridge from Cost to massive excitations that later mass-ladder and spectrum results are expected to consume (particleMass on the phi-ladder). No downstream used_by edges are recorded yet; the module is the local interface rather than a leaf of a finished proof.

scope and limits

Does not derive a dynamical Higgs potential beyond identifying it with J.
Does not prove uniqueness or dynamical selection of the numerical vev.
Does not encode SU(2) x U(1) gauge structure or Goldstone counting.
Does not evaluate numerical particle masses or match PDG values.
Does not address renormalization or loop corrections.

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