weinberg_angle_in_range
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.