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

alpha_W_gt_two_alpha

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  79theorem alpha_W_gt_two_alpha : 2 * alpha < alpha_W := by

proof body

Tactic-mode proof.

  80  unfold alpha_W
  81  rw [lt_div_iff₀ sin2_theta_positive]
  82  calc 2 * alpha * sin2_theta_W_rs
  83      < 2 * alpha * (1/2) := by {
  84        apply mul_lt_mul_of_pos_left sin2_lt_half
  85        exact mul_pos (by norm_num) alpha_pos_aux
  86      }
  87    _ = alpha := by ring
  88
  89/-! ## Part 3: Structural Certificate -/
  90
  91/-- α_W is fully RS-derived: no free parameters enter its computation.
  92    - α comes from the EMAlphaCert (44π seed + f_gap from 8-tick)
  93    - sin²θ_W = (3 − φ)/6 from gauge embedding geometry
  94    Both trace to Q₃ cube structure + golden ratio φ. -/

depends on (17)

Lean names referenced from this declaration's body.