V_RS_nonneg
plain-language theorem explainer
The RS potential V_RS(Λ, v, h) = Λ⁴ (cosh(h/v) − 1) is nonnegative for all real parameters. Effective-field theorists matching recognition cost geometry to the Standard Model Higgs sector cite this result to confirm vacuum stability. The short tactic proof rewrites via the cosh identity, invokes positivity of the fourth power, and applies the elementary bound cosh x ≥ 1.
Claim. For all real numbers Λ, v, h the RS potential satisfies $0 ≤ Λ⁴ (cosh(h/v) − 1)$.
background
In the Higgs EFT Bridge module the recognition cost geometry supplies an effective scalar potential for the canonically normalised Higgs field h. The potential is defined as V_RS(Λ, v, h) := Λ⁴ · Jcost(exp(h/v)), where Jcost is the reciprocal cost functional J(x) = (x + x^{-1})/2 − 1. The upstream theorem V_RS_eq_cosh establishes the equivalent expression Λ⁴ (cosh(h/v) − 1). The module sets the dimensionless coordinate ε = h/v and matches the resulting Taylor expansion to the Standard-Model Higgs potential.
proof idea
The proof is a short tactic sequence. It first rewrites the goal using V_RS_eq_cosh, which replaces V_RS with Λ⁴ (cosh(h/v) − 1). Positivity of Λ⁴ is obtained by the positivity tactic. The inequality 1 ≤ cosh(h/v) follows from Real.one_le_cosh, and subtraction yields a nonnegative remainder. Multiplication of two nonnegative quantities closes the argument.
why it matters
V_RS_nonneg supplies the nonnegativity clause inside the higgsEFTBridgeCert definition, which certifies the full bridge from recognition cost to the Standard-Model Higgs EFT. It directly supports the vacuum stability required by the recognition substrate and closes the first two arrows of the reviewer chain described in the module documentation. The result relies on the J-uniqueness property that forces the cosh form of the cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.