weinberg_angle_in_range
The theorem establishes that the square of the Weinberg angle derived in the Recognition Science framework lies strictly between zero and one. Electroweak model builders would cite it when confirming that the RS prediction for the mixing angle remains inside the physically allowed interval for sin²θ_W. The proof is a short tactic sequence that unfolds the definition involving the golden ratio and applies elementary real-number inequalities on square roots together with linarith.
claim$0 < w^2 < 1$, where $w$ is the Weinberg mixing angle obtained from the RS unification scale on the φ-ladder.
background
The module derives renormalization-group running of gauge couplings from the RS φ-ladder, with the anchor scale μ* = 182.201 GeV fixed at a stationarity point of the flow. The β-function is obtained as the ladder derivative (1/ln φ) dg/dr, and the sign of β_QCD is fixed by the SU(3) structure forced by Q₃. Upstream, the unification theorem supplies the three definitional Aristotelian conditions (identity, non-contradiction, totality) plus the primitive observer once a recognizer has nontrivial recognition; the fourth condition (composition consistency) is supplied separately.
proof idea
The tactic proof unfolds the definition of the squared angle and of φ, introduces the auxiliary facts that sqrt(5) > 0 and sqrt(5) < 3 (via sqrt_lt_sqrt and norm_num), then splits into two goals. Positivity follows from div_pos after linarith; the upper bound follows from rewriting the inequality as a division less than one and applying linarith again.
why it matters in Recognition Science
The result supplies a basic consistency check inside the gauge-coupling-unification block of the running-couplings development. It rests on the φ-ladder scale definitions and on the unification theorem that extracts Aristotelian logic from any nontrivial recognizer. The declaration therefore closes a small but necessary sanity condition before the module proceeds to asymptotic-freedom criteria and one-loop running formulas for α_s.
scope and limits
- Does not compute a numerical value for the angle.
- Does not derive the angle expression from the J-cost or defect distance.
- Does not address scale dependence or running of the angle.
- Does not compare the RS value with experimental measurements.
formal statement (Lean)
197theorem weinberg_angle_in_range : 0 < rs_weinberg_angle_sq ∧ rs_weinberg_angle_sq < 1 := by
proof body
Tactic-mode proof.
198 unfold rs_weinberg_angle_sq φ
199 have h5pos : (0 : ℝ) < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
200 have h5lt3 : Real.sqrt 5 < 3 := by
201 have h9 : Real.sqrt 9 = 3 := by
202 rw [show (9:ℝ) = 3^2 from by norm_num, Real.sqrt_sq (by norm_num)]
203 have h : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
204 linarith [h9 ▸ h]
205 constructor
206 · apply div_pos _ (by norm_num)
207 linarith
208 · rw [div_lt_one (by norm_num)]
209 linarith
210
211/-! ## Gauge Coupling Unification -/
212
213/-- At unification scale μ_GUT, the three SM couplings converge.
214 The RS prediction: μ_GUT lies on the φ-ladder at some integer rung. -/