Pith. sign in
module module high

IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit

show as:
view Lean formalization →

This module assembles the master certificates from the five Higgs-EFT bridge components into one named, auditable surface for the cost-geometry to SM-EFT link. Researchers tracing the Recognition Science derivation of Standard Model low-energy observables would cite it as the top-level composition. The structure is a pure aggregation of existing certificates with no new theorems proved.

claimThe master certificate $C$ for the Higgs EFT low-energy limit is the structural composition of the electroweak mass relations $m_W^2 = g^2 v^2/4$, $m_Z^2 = (g^2+g'^2)v^2/4$, the RS coordinate $\\varepsilon = h/v$, the Yukawa ratios $y_f = \\sqrt{2} m_f/v$, the observable skeleton, and the longitudinal scattering unitarity cancellation.

background

Recognition Science derives the Standard Model low-energy limit from the forcing chain (T0-T8) and Recognition Composition Law applied to the J-cost function on a phi-ladder. The module composes five upstream bridges: ElectroweakMassBridge supplies the gauge-boson masses from the recognition substrate scale $v$ and couplings $g,g'$; HiggsEFTBridge maps the dimensionless RS coordinate $\varepsilon = h/v$ to canonical Higgs EFT; HiggsYukawaBridge gives $y_f = \sqrt{2} m_f/v$; HiggsObservableSkeleton parametrizes partial widths and signal strengths; LongitudinalVectorScattering encodes the Higgs cancellation of $s^2/v^4$ growth in $W_L W_L$ scattering.

proof idea

This is a composition module with no proofs. It aggregates the master certificates of the five imported modules (ElectroweakMassBridge, HiggsEFTBridge, HiggsObservableSkeleton, HiggsYukawaBridge, LongitudinalVectorScattering) into a single named object for Anil's chain.

why it matters in Recognition Science

This module feeds the root IndisputableMonolith, which exposes the master forcing-chain theorem plus the six-module Standard-Model Higgs EFT low-energy-limit chain. It supplies the final auditable surface for the cost-geometry to SM-EFT bridge cited in the companion paper, closing the 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)