module module high

`IndisputableMonolith.StandardModel.HiggsEFTBridge`

This module defines the RS Higgs effective potential at canonical mass dimension four. Downstream modules in the Standard Model chain cite it to link recognition cost geometry to canonical EFT. The module consists of definitions and supporting lemmas for non-negativity, quartic expansion, and truncation error bounds.

claim$V_{RS}(\Lambda, v, h) = \Lambda^4 \cdot J(\exp(h/v))$

background

The module imports the RS time quantum from Constants and the J-cost function from Cost. J-cost satisfies the recognition composition law and equals cosh(log x) - 1. The potential is built by evaluating this cost on the exponential map from the Higgs field coordinate scaled by the substrate vacuum expectation value v.

The local theoretical setting is the effective scalar coordinate that arises once the recognition substrate scale is fixed. Sibling definitions establish the quartic canonical form together with explicit error controls on the truncation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the master certificate in HiggsEFTLowEnergyLimit, which formalises the chain RS cost geometry to effective scalar coordinate to canonical Higgs EFT. It also supports ElectroweakMassBridge and LongitudinalVectorScattering. It supplies the quartic potential structure required by the T5-T8 forcing chain.

scope and limits

Does not compute numerical values for partial widths or branching ratios.
Does not derive gauge-boson mass relations.
Does not include higher-dimensional operators beyond dimension four.
Does not fix the numerical value of the vacuum expectation value v.

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith module_import
IndisputableMonolith.StandardModel.ElectroweakMassBridge module_import
IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit module_import
IndisputableMonolith.StandardModel.HiggsObservableSkeleton module_import
IndisputableMonolith.StandardModel.LongitudinalVectorScattering module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

def V_RS L67
theorem V_RS_eq_cosh L70
theorem V_RS_at_vacuum L76
theorem V_RS_nonneg L81
def V_RS_quartic L91
theorem exp_sub_trunc6_le L99
theorem cosh_quartic_error L115
theorem jcost_quartic_error L142
theorem V_RS_quartic_error L156
def quadratic_coefficient L176
def quartic_coefficient_canonical L179
theorem V_RS_quartic_canonical L183
def NormalizationHypothesis L201
theorem mass_term_matches_SM L206
theorem quartic_coupling_from_normalization L220
structure HiggsEFTBridgeCert L238
def higgsEFTBridgeCert L262
theorem higgsEFTBridgeCert_inhabited L271