V_RS_eq_cosh
plain-language theorem explainer
Recognition Science yields the Higgs effective potential in the form V_RS(Λ, v, h) = Λ⁴ (cosh(h/v) − 1). Effective field theorists bridging recognition geometry to the Standard Model would cite this reduction when normalising the scalar potential. The identity follows at once from the definition of V_RS together with the Jcost-to-cosh lemma.
Claim. For all real numbers $Λ, v, h$, the recognition-science Higgs potential satisfies $V_{RS}(Λ, v, h) = Λ^4 (cosh(h/v) - 1)$.
background
The module formalises the link from RS cost geometry to the canonical Higgs EFT. The potential is defined by V_RS(Λ, v, h) := Λ⁴ · Jcost(exp(h/v)), where Jcost is the recognition cost functional satisfying J(exp t) = cosh t − 1. This identity is supplied by the upstream lemma Jcost_exp_cosh. The local setting is the first two arrows of the chain RS cost geometry → effective scalar coordinate → canonical Higgs EFT, with ε = h/v the dimensionless coordinate and Λ⁴ the dimensionful prefactor.
proof idea
The proof unfolds the definition of V_RS and rewrites the Jcost term via the Jcost_exp_cosh lemma from the Cost module.
why it matters
This theorem supplies the cosh form required by the Higgs EFT bridge certificate (higgsEFTBridgeCert) and is used to establish vacuum zero and non-negativity of the potential. It closes the first two arrows of the reviewer chain by matching the RS cost geometry onto the Standard-Model parametrisation V_SM h = ½ m_H² h² + (λ_SM / 4) h⁴ + ⋯, yielding m_H² = Λ⁴ / v² and λ_SM = Λ⁴ / (6 v⁴). The result relies on the J-uniqueness property from the forcing chain and enables the subsequent quartic expansion steps in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.