q3_correction_pos
plain-language theorem explainer
The theorem proves positivity of the product between the RS Weinberg angle (3-φ)/6 and the Q3 correction factor 17/16. Researchers deriving the Higgs mass from the φ-ladder cite it to secure the sign of the level-3 prediction m_H = v √(sin²θ_W · 17/16). The proof is a direct one-line application of the multiplication-positivity lemma to the already-established positivity of sin²θ_W_RS together with a numerical check.
Claim. $0 < ((3 - φ)/6) · (17/16)$ holds, where φ is the golden ratio and the factor 17/16 encodes the Q₃ mode budget (16 addressing modes plus the physical Higgs singlet).
background
The Higgs Rung Assignment module derives the Higgs mass from the φ-ladder using Q₃ geometry. It defines sin²θ_W_RS := (3 - φ)/6 and sets m_H = v · √(sin²θ_W_RS · 17/16), where the 17/16 correction arises because the Q₃ structure supplies 16 addressing modes and the 17th mode is the physical Higgs singlet. The module states that this places m_H in (120, 130) GeV once the vev ratio and one-loop EW correction are included, completing the RS particle mass table.
proof idea
The proof is a one-line wrapper that applies the mul_pos lemma to the upstream theorem sin2ThetaW_RS_pos together with a norm_num tactic that confirms positivity of 17/16.
why it matters
The result is invoked directly by the downstream theorem mH_rs_level3_pos to establish positivity of the level-3 Higgs mass prediction. It thereby supports the module's core claim that m_H lies in (120, 130) GeV and closes the Q10 question from biggest-questions.md. Within the Recognition framework the positivity check confirms that the Q₃ correction preserves the sign required for physical masses on the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.