vev
plain-language theorem explainer
Physicists modeling electroweak symmetry breaking from J-cost minima cite this definition of the vacuum expectation value. It sets the VEV to the positive square root of mu squared over twice lambda under the given positivity conditions on the parameters. The definition is realized by direct substitution of the algebraic minimum formula for the quartic potential.
Claim. The vacuum expectation value $v$ of the Higgs field is $v = sqrt(mu^2 / (2 lambda))$ for real parameters satisfying $mu^2 > 0$ and $lambda > 0$.
background
The module identifies the Higgs potential with the J-cost functional of Recognition Science. The vacuum expectation value marks the minimum of this potential, which triggers spontaneous symmetry breaking from SU(2)_L × U(1)_Y to U(1)_EM. Upstream results include the RS VEV defined as the golden ratio phi in QFT.HiggsMechanism, where the VEV is positive for symmetry breaking.
proof idea
This definition is a direct one-line expression that applies Real.sqrt to the ratio mu_sq / (2 * lambda). The positivity hypotheses ensure the argument is positive so that the square root is real.
why it matters
This definition supplies the VEV used in downstream results such as higgs_mechanism_nonzero_vev, which establishes that the VEV is nonzero, and massParameter, which evaluates the J-cost at this point to set the particle mass scale. It implements the RS mechanism in which the Higgs potential equals the J-cost functional and the VEV is its minimum, linking to the phi-ladder and the eight-tick octave in the forcing chain. It leaves open the numerical matching of this expression to the observed 246 GeV scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.