higgs_unique_minimum
plain-language theorem explainer
The declaration proves that the Higgs potential, realized as the J-cost on the normalized field ratio r, vanishes if and only if r equals one for positive r. Model builders deriving the electroweak vacuum from recognition cost minimization would cite this uniqueness result. The proof is a direct biconditional split that invokes the strict positivity of J-cost away from unity together with its explicit vanishing at unity.
Claim. For every real number $r > 0$, the Higgs potential $V(r) := J(r)$ satisfies $V(r) = 0$ if and only if $r = 1$, where $J(r) = (r + r^{-1})/2 - 1$.
background
The module recasts the Standard Model Higgs potential in recognition terms. With $r$ the ratio of the Higgs field magnitude to the electroweak VEV, the potential is identified with the J-cost: $V_{RS}(r) = J(r) = ½(r + r^{-1}) - 1$. The vacuum sits at $r = 1$, where the cost is zero, and the second derivative at that point supplies the Higgs mass scale in RS units.
proof idea
The term proof first unfolds higgsPotential to Jcost. It then applies constructor to split the biconditional. The left-to-right direction assumes the potential is zero, supposes $r ≠ 1$, and obtains a contradiction from the positivity lemma Jcost_pos_of_ne_one. The right-to-left direction substitutes $r = 1$ and invokes the unit lemma Jcost_unit0.
why it matters
The theorem supplies the unique-minimum clause inside higgsPotentialCert, the certificate that packages all structural properties of the recognition Higgs potential. It thereby completes the three key facts listed in the module documentation: zero at the vacuum, symmetry about the minimum, and uniqueness of that minimum. The result directly instantiates the J-uniqueness property (T5) of the forcing chain and anchors the calibration condition $V''(1) = 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.