sin2ThetaW_RS_pos
plain-language theorem explainer
Recognition Science assigns sin²θ_W the explicit value (3 - φ)/6. Model builders in the Standard Model sector cite this positivity to confirm the sign of correction factors in Higgs mass assignments. The proof unfolds the definition and reduces the inequality via division positivity together with the numerical bound φ < 1.62.
Claim. $0 < (3 - φ)/6$ where φ is the golden ratio appearing in the Recognition Science constants.
background
The Q3Representations module formalizes the quaternion group Q3 as the symmetry of the 8-tick cycle under electroweak symmetry breaking SU(2)×U(1) → U(1). The Higgs doublet splits into three Goldstone modes eaten by W± and Z plus one physical spin-0 Higgs, with mass ratios set by Casimir eigenvalues of the spin-0 and spin-1 sectors of Q3 together with the phi-ladder rung assignments.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of sin²θ_W^RS to the fraction (3 - φ)/6, applies div_pos to split the positivity claim, invokes linarith on the imported bound phi_lt_onePointSixTwo to obtain 3 - φ > 0, and uses norm_num for the positive denominator.
why it matters
This positivity statement is invoked by the downstream theorem q3_correction_pos to establish 0 < sin²θ_W^RS · (17/16). It supplies a required sign check inside the Q3 representation framework for the Higgs rung assignment, consistent with the eight-tick octave and the phi-ladder mass formula in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.