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)
78noncomputable def mH_naive : ℝ := vev
proof body
Definition body.
79
80/-- Level 2: RS prediction with sin²θ_W correction.
81 m_H = v · √(sin²θ_W) — the dominant correction from Q₃ symmetry breaking. -/
depends on (5)
Lean names referenced from this declaration's body.
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
correction
in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi
decl_use
-
vev
in IndisputableMonolith.QFT.HiggsMechanism
decl_use
-
vev
in IndisputableMonolith.StandardModel.ElectroweakBreaking
decl_use
-
vev
in IndisputableMonolith.StandardModel.HiggsRungAssignment
decl_use