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

sin2ThetaW_RS_approx

show as:
view Lean formalization →

Recognition Science yields the bound 0.228 < sin²θ_W < 0.232 for the Weinberg parameter. Precision electroweak analyses cite this interval when testing RS mass predictions against collider data. The proof reduces the claim to the known numerical bounds on the golden ratio φ by direct substitution and linear arithmetic.

claimIn Recognition Science the square of the Weinberg angle is predicted to satisfy $0.228 < sin^2 θ_W < 0.232$.

background

The Q3Representations module encodes the quaternion group Q3 as the symmetry of the eight-tick cycle in Recognition Science. The electroweak symmetry breaking pattern splits the Higgs doublet into spin-1 Goldstone modes absorbed by the W and Z bosons and a remaining spin-0 Higgs. The Weinberg angle parametrizes the mixing and appears in the RS mass ladder as an offset determined by the Casimir eigenvalues of the two sectors.

proof idea

Unfold the definition of the RS Weinberg parameter. Split the conjunction into separate inequalities. Rewrite each using the division rule for positive constants. Apply linarith to the supplied bounds on φ to finish both sides.

why it matters in Recognition Science

The theorem is invoked directly by the WeinbergAngleScoreCard to fill the RS bracket row and by the HiggsRungCert theorem that certifies the full Higgs mass prediction. It completes the tree-level Standard Model embedding inside the Recognition Science forcing chain, connecting the eight-tick octave to observable electroweak quantities. The interval contains the experimental value, leaving open whether higher-order effects remain inside the same bounds.

scope and limits

formal statement (Lean)

 152theorem sin2ThetaW_RS_approx : 0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232 := by

proof body

Term-mode proof.

 153  unfold sin2ThetaW_RS
 154  constructor
 155  · rw [lt_div_iff₀ (by norm_num : (0:ℝ) < 6)]
 156    linarith [phi_lt_onePointSixTwo]
 157  · rw [div_lt_iff₀ (by norm_num : (0:ℝ) < 6)]
 158    linarith [phi_gt_onePointSixOne]
 159
 160/-! ## The Higgs Rung Assignment -/
 161
 162/-- The W-boson rung on the φ-ladder (from the mass law). -/

used by (2)

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

depends on (15)

Lean names referenced from this declaration's body.