IndisputableMonolith.StandardModel.WeakCoupling

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.Alpha
   4import IndisputableMonolith.Masses.ElectroweakMasses
   5
   6/-!
   7# The Weak Coupling Constant α_W from RS First Principles
   8
   9This module defines the SU(2) weak coupling constant α_W by combining
  10two independently RS-derived quantities:
  11
  12- α (EM fine-structure constant) from `Constants/Alpha.lean`
  13- sin²θ_W = (3 − φ)/6 from `Masses/ElectroweakMasses.lean`
  14
  15via the tree-level electroweak identity: α = α_W · sin²θ_W.
  16
  17Input status (honest, 2026-07-06):
  18- α here is the RS CONSTRUCTION value (44π · exp(−f_gap/44π), band
  19  (137.030, 137.039)). The construction's exact value is EXCLUDED by
  20  measurement at >30,000σ (`Constants.AlphaGenesis.MeasurementVerdict`),
  21  and within RS the exact α is a free boundary datum
  22  (`Constants.AlphaGenesis.KappaGammaIrreducibility`). So α_W built on it
  23  is a construction-band object, NOT a parameter-free derivation of the
  24  measured weak coupling.
  25- sin²θ_W = (3 − φ)/6 is φ-structural from the gauge embedding at D = 3.
  26
  27## Main Results
  28
  29- `alpha_W`: the weak coupling constant = α / sin²θ_W
  30- `alpha_W_pos`: α_W is positive
  31- `alpha_W_gt_alpha`: α_W > α (since sin²θ_W < 1)
  32- `WeakCouplingCert`: the combination identity (construction-band input)
  33
  34## Status: 0 sorry, 0 axiom
  35-/
  36
  37namespace IndisputableMonolith
  38namespace StandardModel
  39namespace WeakCoupling
  40
  41open Constants Masses.ElectroweakMasses
  42
  43noncomputable section
  44
  45/-! ## Part 1: Definition -/
  46
  47/-- The weak coupling constant α_W = α / sin²θ_W.
  48    From the tree-level electroweak identity: α_EM = α_W · sin²θ_W,
  49    so α_W = α_EM / sin²θ_W. -/
  50def alpha_W : ℝ := alpha / sin2_theta_W_rs
  51
  52/-- α_W expressed in terms of RS primitives:
  53    α_W = (1/alphaInv) / ((3 − φ)/6) = 6 / (alphaInv · (3 − φ)) -/
  54theorem alpha_W_expanded :
  55    alpha_W = alpha / ((3 - Constants.phi) / 6) := rfl
  56
  57/-! ## Part 2: Positivity and Bounds -/
  58
  59private lemma alpha_pos_aux : 0 < alpha := by
  60  unfold alpha alphaInv alpha_seed; positivity
  61
  62/-- α_W is positive (both α and sin²θ_W are positive). -/
  63theorem alpha_W_pos : 0 < alpha_W := by
  64  unfold alpha_W
  65  exact div_pos alpha_pos_aux sin2_theta_positive
  66
  67/-- α_W > α (since sin²θ_W < 1, dividing by it increases α). -/
  68theorem alpha_W_gt_alpha : alpha < alpha_W := by
  69  unfold alpha_W
  70  rw [lt_div_iff₀ sin2_theta_positive]
  71  calc alpha * sin2_theta_W_rs
  72      < alpha * 1 := by {
  73        apply mul_lt_mul_of_pos_left _ alpha_pos_aux
  74        linarith [sin2_theta_lt_half]
  75      }
  76    _ = alpha := mul_one _
  77
  78/-- sin²θ_W > 0 (needed for division). -/
  79theorem sin2_pos : 0 < sin2_theta_W_rs := sin2_theta_positive
  80
  81/-- sin²θ_W < 1/2 (the weak mixing is mild). -/
  82theorem sin2_lt_half : sin2_theta_W_rs < 1/2 := sin2_theta_lt_half
  83
  84/-- α_W > 2α (since sin²θ_W < 1/2). -/
  85theorem alpha_W_gt_two_alpha : 2 * alpha < alpha_W := by
  86  unfold alpha_W
  87  rw [lt_div_iff₀ sin2_theta_positive]
  88  calc 2 * alpha * sin2_theta_W_rs
  89      < 2 * alpha * (1/2) := by {
  90        apply mul_lt_mul_of_pos_left sin2_lt_half
  91        exact mul_pos (by norm_num) alpha_pos_aux
  92      }
  93    _ = alpha := by ring
  94
  95/-! ## Part 3: Structural Certificate -/
  96
  97/-- The α_W combination identity, with honest input status:
  98    - α is the RS CONSTRUCTION value (44π seed + f_gap from 8-tick); its
  99      exact value is a boundary datum in RS, not a derived constant
 100      (`Constants.AlphaGenesis.KappaGammaIrreducibility`), so this cert
 101      certifies the combination STRUCTURE, not a parameter-free value of
 102      the measured weak coupling.
 103    - sin²θ_W = (3 − φ)/6 from gauge embedding geometry (φ-structural). -/
 104structure WeakCouplingCert where
 105  alpha_from_cube : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))
 106  sin2_from_phi : sin2_theta_W_rs = (3 - Constants.phi) / 6
 107  alpha_W_def : alpha_W = alpha / sin2_theta_W_rs
 108  alpha_W_positive : 0 < alpha_W
 109  alpha_W_exceeds_alpha : alpha < alpha_W
 110
 111theorem weak_coupling_cert : WeakCouplingCert where
 112  alpha_from_cube := rfl
 113  sin2_from_phi := rfl
 114  alpha_W_def := rfl
 115  alpha_W_positive := alpha_W_pos
 116  alpha_W_exceeds_alpha := alpha_W_gt_alpha
 117
 118end
 119
 120end WeakCoupling
 121end StandardModel
 122end IndisputableMonolith
 123