def hypothesis interface def or abbrev

`NormalizationHypothesis`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 201def NormalizationHypothesis (Λ v m_H : ℝ) : Prop :=

proof body

Definition body.

 202  Λ ^ 4 = m_H ^ 2 * v ^ 2
 203
 204/-- Under the normalisation hypothesis, the SM kinetic-normalised Higgs mass
 205    appears as the coefficient of `½ h²` in the RS quartic Taylor potential. -/

used by (6)

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

HiggsEFTBridgeCert in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use
mass_term_matches_SM in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use
quartic_coupling_from_normalization in IndisputableMonolith.StandardModel.HiggsEFTBridge decl_use
HiggsEFTLowEnergyLimitCert in IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit decl_use
higgsEFTLowEnergyLimitCert_inhabited in IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit decl_use
yukawa_SM_phi_pow_scaling in IndisputableMonolith.StandardModel.HiggsYukawaBridge decl_use

depends on (6)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use