pith. machine review for the scientific record. sign in
def definition def or abbrev high

mH_naive

show as:
view Lean formalization →

The naive Higgs mass prediction in Recognition Science sets m_H equal to the vacuum expectation value v. Particle physicists deriving the phi-ladder mass table cite this as the Level 1 baseline before Q3 and Weinberg corrections are applied. It is a direct one-line alias to the imported vev definition.

claim$m_H^{naive} := v$, where $v$ is the Higgs vacuum expectation value satisfying $m_H^2 = 2λ_{RS} v^2$ with $λ_{RS} = 1/2$.

background

The HiggsRungAssignment module derives the Higgs boson mass from the phi-ladder using Q3 geometry to complete the RS particle mass table. The naive Level 1 step sets m_H = v, which follows from the J-cost potential curvature forcing λ_RS = 1/2 and thus m_H² = v². The observed v ≈ 246 GeV produces the natural scale 246 GeV, while the measured Higgs mass is 125.2 GeV.

proof idea

This is a one-line definition that directly aliases the vev constant imported from StandardModel.ElectroweakBreaking. No lemmas or tactics are invoked beyond the module import of vev.

why it matters in Recognition Science

This definition supplies the Level 1 baseline that subsequent siblings mH_rs_level2 and mH_prediction_in_interval build upon by inserting the sin²θ_W correction. It fills the initial rung in the module's derivation of the (120, 130) GeV interval and closes the hypothesis for the Higgs mass assignment in the Recognition framework. The parent result is the full interval claim; the exact one-loop correction remains open.

scope and limits

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.