pith. sign in
module module high

IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit

show as:
view Lean formalization →

This module assembles the master certificate for the recognition cost-geometry to Standard-Model EFT low-energy limit bridge. It composes the certificates of the electroweak mass bridge, Higgs EFT bridge, Yukawa bridge, observable skeleton, and longitudinal scattering modules. A researcher auditing the full SM chain from the RS substrate would cite this surface. The structure is a pure composition exposing one named auditable interface for Anil's chain.

claimThe master certificate for the cost-geometry to SM-EFT bridge is the structural composition of the certificates from the electroweak mass relations $m_W^2 = g^2 v^2/4$, Higgs EFT coordinate $ε = h/v$, Yukawa couplings $y_f = √2 m_f/v$, observable skeleton, and longitudinal vector scattering unitarity restoration.

background

The module sits in the Standard Model domain of Recognition Science and bridges the RS cost geometry to the low-energy effective field theory of the Higgs sector. Upstream modules supply the electroweak mass relations from the recognition-substrate scale $v$ and generic positive gauge couplings $g,g'$, the dimensionless RS coordinate $ε = h/v$ for the canonically normalised collider scalar field, the Yukawa couplings as ratios of RS-derived masses to $v$, the target observables as abstract structural objects, and the cancellation in longitudinal vector-boson scattering that restores perturbative unitarity.

proof idea

This is a definition module with no proofs. The structure is a pure composition of the master certificates from the five imported modules: ElectroweakMassBridge, HiggsEFTBridge, HiggsYukawaBridge, HiggsObservableSkeleton, and LongitudinalVectorScattering. Each component contributes its own certificate to form the unified surface.

why it matters in Recognition Science

This module earns its place by providing the single named auditable surface for the cost-geometry to SM-EFT bridge in the Recognition framework. It feeds directly into the root IndisputableMonolith module, completing the six-module Standard-Model Higgs effective-field-theory low-energy-limit chain cited in the companion paper. The composition supports Anil's chain by exposing the full low-energy limit without new theorems.

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (3)