pith. machine review for the scientific record. sign in
theorem proved term proof

mH_rs_level3_pos

show as:
view Lean formalization →

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)

 117theorem mH_rs_level3_pos : 0 < mH_rs_level3 := by

proof body

Term-mode proof.

 118  unfold mH_rs_level3 vev
 119  exact mul_pos (by norm_num) (Real.sqrt_pos.mpr q3_correction_pos)
 120
 121/-- **KEY THEOREM**: The RS Higgs mass prediction is in (120, 130) GeV.
 122
 123    This contains the observed value 125.2 GeV and establishes the prediction
 124    as a HYPOTHESIS (not yet THEOREM since the full one-loop EW correction
 125    is not yet formalized). -/

used by (1)

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

depends on (19)

Lean names referenced from this declaration's body.