V_RS_at_vacuum
plain-language theorem explainer
The recognition cost potential for the Higgs field vanishes exactly at the vacuum point h = 0. Collider physicists matching effective potentials to the Standard Model would cite this result when verifying the minimum of the RS-derived quartic. The proof is a direct one-line reduction that invokes the cosh equivalence and the elementary identity cosh(0) = 1.
Claim. $V_{RS}(Λ, v, 0) = 0$ for all real $Λ, v$, where the potential is defined by $V_{RS}(Λ, v, h) := Λ^4 (cosh(h/v) - 1)$.
background
The Higgs EFT Bridge module constructs the effective scalar potential from recognition cost geometry. The potential takes the form $V_{RS}(Λ, v, h) = Λ^4 J(exp(h/v))$, with $J$ the reciprocal cost functional that satisfies $J(exp ε) = cosh ε - 1$. This equivalence is established by the upstream theorem $V_{RS_eq_cosh}$. The module sets the vacuum at $h = 0$ to match the electroweak scale $v$ supplied by the recognition substrate.
proof idea
The proof applies the rewriting rule from $V_{RS_eq_cosh}$ to replace the potential with its cosh form, then uses simp to evaluate cosh(0) - 1 = 0.
why it matters
This theorem supplies the vacuum_zero clause in the higgsEFTBridgeCert certificate, which certifies the full bridge from RS geometry to the Standard Model Higgs potential. It completes the first step of the chain described in the module documentation, ensuring the potential minimum sits at zero as required for spontaneous symmetry breaking. It touches the J-uniqueness property in the forcing chain by relying on the cosh representation of the cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.