WeakCouplingCert

formal source

  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 φ. -/
  95structure WeakCouplingCert where
  96  alpha_from_cube : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))
  97  sin2_from_phi : sin2_theta_W_rs = (3 - Constants.phi) / 6
  98  alpha_W_def : alpha_W = alpha / sin2_theta_W_rs
  99  alpha_W_positive : 0 < alpha_W
 100  alpha_W_exceeds_alpha : alpha < alpha_W
 101
 102theorem weak_coupling_cert : WeakCouplingCert where
 103  alpha_from_cube := rfl
 104  sin2_from_phi := rfl
 105  alpha_W_def := rfl
 106  alpha_W_positive := alpha_W_pos
 107  alpha_W_exceeds_alpha := alpha_W_gt_alpha
 108
 109end
 110
 111end WeakCoupling
 112end StandardModel
 113end IndisputableMonolith