higgsPotential
The Higgs potential is defined by the expression -mu_sq * phi^2 + lambda * phi^4. Researchers deriving electroweak symmetry breaking from J-cost minimization cite this when matching the Standard Model Lagrangian to Recognition Science. The definition is a direct one-line transcription of the classical Mexican-hat form with no lemmas or reductions applied.
claimThe Higgs potential is given by $V(phi, mu^2, lambda) = -mu^2 phi^2 + lambda phi^4$.
background
The module targets derivation of electroweak symmetry breaking from J-cost, with the Higgs mechanism supplying the Mexican hat potential that breaks SU(2)_L × U(1)_Y to U(1)_EM at the vacuum expectation value. In Recognition Science the potential is identified with the J-cost functional on the field ratio, where J(x) = (x + x^{-1})/2 - 1. Upstream results establish convexity and unique minimization at unity (PhysicsComplexityStructure), calibration of J on the positive reals (LedgerFactorization), and the discrete phi-tiers for physical quantities (NucleosynthesisTiers).
proof idea
The definition is a direct transcription of the standard polynomial expression. It is a one-line definition with no lemmas applied and no tactics invoked.
why it matters in Recognition Science
This definition supplies the classical expression that is matched to J-cost in the QRFT module, feeding into HiggsPotentialCert, higgs_nonneg, higgs_symmetric, and SMLagrangianSkeleton. It realizes the SM-009 target by linking the potential to J-cost minimization, consistent with the Recognition Composition Law and the phi-ladder. It leaves open the fixing of mu_sq and lambda from the forcing chain steps T5-T8.
scope and limits
- Does not derive numerical values for mu_sq or lambda from the phi-ladder.
- Does not prove equivalence to the J-cost form; that is handled in the QRFT module.
- Does not include the full electroweak Lagrangian or gauge boson mass terms.
- Does not address spontaneous symmetry breaking dynamics or thermal effects.
formal statement (Lean)
51noncomputable def higgsPotential (phi mu_sq lambda : ℝ) : ℝ :=
proof body
Definition body.
52 -mu_sq * phi^2 + lambda * phi^4
53
54/-- The VEV (vacuum expectation value) of the Higgs field. -/