No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
196structure HiggsRungCert where
197 /-- sin²θ_W = (3-φ)/6 (from WeinbergAngle) -/
198 weinberg_angle : 0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232
199 /-- Level 2 prediction in (110, 125) -/
200 level2_range : 110 < mH_rs_level2 ∧ mH_rs_level2 < 125
201 /-- Level 3 prediction in (120, 130) — contains 125.2 GeV -/
202 level3_range : 120 < mH_rs_level3 ∧ mH_rs_level3 < 130
203 /-- Higgs rung is between 21 and 22 -/
204 higgs_rung_range : (w_rung : ℝ) < higgs_rung_from_prediction ∧
205 higgs_rung_from_prediction < (w_rung : ℝ) + 1
206 /-- Within 5% of observed -/
207 within_5_percent : |mH_rs_level3 - mH_obs| / mH_obs < 0.05
208
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
higgsRungCert
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use
depends on (24)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
contains
in IndisputableMonolith.Ethics.StakeGraph
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
contains
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
higgs_rung_from_prediction
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use
-
mH_obs
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use
-
mH_rs_level2
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use
-
mH_rs_level3
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use
-
sin2ThetaW_RS
in IndisputableMonolith.StandardModel.Q3Representations
decl_use
-
w_rung
in IndisputableMonolith.StandardModel.Q3Representations
decl_use