module module high

`IndisputableMonolith.QFT.HiggsMechanism`

This module defines the J-cost functional together with vacuum expectation value, symmetry breaking, mass parameters and Yukawa couplings for the Higgs sector in Recognition Science QFT. It supplies the algebraic objects needed to generate particle masses from the recognition cost. Researchers deriving electroweak symmetry breaking from the RS forcing chain would cite these definitions. The module contains only definitions and no theorems.

claim$J(x) = ½(x + x^{-1}) - 1$ for $x > 0$, with vacuum expectation value, symmetry-broken state, mass parameter, Yukawa coupling and particle mass derived from the same functional.

background

The module sits inside the Recognition Science QFT derivations and imports the fundamental time quantum τ₀ = 1 tick together with the cost structures. Its central object is the J-cost functional J(x) = ½(x + 1/x) - 1, which attains its minimum at x = 1. Sibling definitions introduce the vacuum expectation value, the condition for symmetry breaking, the mass parameter, the Yukawa coupling and the resulting particle mass, all expressed in terms of J.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into the parent IndisputableMonolith.QFT module, which assembles Tier 2 derivations of quantum field theory from the Recognition Science framework. They supply the Higgs-mechanism ingredients required to complete the mass-generation step that follows from the J-cost and the forcing chain.

scope and limits

Does not derive the full Higgs potential or its dynamics.
Does not compute numerical mass values or coupling constants.
Does not address gauge boson masses or the full electroweak Lagrangian.

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