vacuum_zero_potential
plain-language theorem explainer
The theorem states that the Higgs potential vanishes exactly at the vacuum ratio in the recognition framework. Model builders working on electroweak symmetry breaking via J-cost would cite this to fix the ground-state energy. The proof is a direct term application of the upstream Jcost unit lemma.
Claim. The Higgs potential at the vacuum ratio satisfies $V(1) = 0$, where $V(r) := J(r) = (r + r^{-1})/2 - 1$.
background
The module identifies the Standard Model Higgs potential with the J-cost on the normalized field ratio r = |H| / (v/√2). J(r) is defined as (r + r^{-1})/2 - 1 and reaches its unique minimum at r = 1. The upstream lemma Jcost_unit0 asserts Jcost 1 = 0 by direct simplification of the squared-ratio form J(x) = (x-1)^2/(2x).
proof idea
Term proof that applies the lemma Jcost_unit0 from the Cost library.
why it matters
The result supplies the vacuum_zero field inside the HiggsPotentialCert structure that collects the four structural properties of the potential. It confirms the recognition-vacuum claim that the electroweak VEV is the zero-cost ground state, consistent with the module's listed facts on symmetry and the second-derivative calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.