V_RS
plain-language theorem explainer
V_RS defines the recognition-science Higgs effective potential as Λ⁴ times Jcost of exp(h/v). Collider physicists matching recognition cost geometry to the Standard Model would cite this definition when deriving the quartic coupling and mass terms from the recognition substrate. The definition directly encodes the exponential map from the scalar field to the recognition coordinate with no additional steps.
Claim. The RS Higgs effective potential is defined by $V_{RS}(Λ, v, h) := Λ^4 · J( exp(h/v) )$, where $J(x) = ½(x + x^{-1}) - 1$.
background
This module formalises the first link in the chain RS cost geometry → effective scalar coordinate → canonical Higgs EFT. The dimensionless RS coordinate is ε = h/v where h is the canonically normalised collider scalar field and v > 0 is the electroweak scale supplied by the recognition substrate. A dimensionful prefactor Λ⁴ is required to match the Standard-Model Lagrangian normalisation. The recognition-cost potential is V_RS Λ v h := Λ^4 · J(exp (h / v)) where J(x) = ½(x + x^{-1}) − 1 is the canonical reciprocal cost functional and J(e^ε) = cosh ε − 1.
proof idea
This is a direct definition. Subsequent results such as V_RS_eq_cosh unfold the definition and apply Cost.Jcost_exp_cosh to obtain the equivalent form Λ⁴ (cosh(h/v) − 1).
why it matters
This definition supplies the core object for the HiggsEFTBridgeCert structure, which certifies the map from cost geometry to scalar EFT. It fills the first arrow in the chain described in the module documentation and enables the SM-to-RS dictionary m_H² = Λ⁴ / v², λ_SM = (1/6) · Λ⁴ / v⁴. It rests on the J functional from the forcing chain (T5) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.