higgsPotential
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.