IndisputableMonolith.Cosmology.EWPhaseTransition

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.Alpha
   4import IndisputableMonolith.Cosmology.SphaleronRate
   5import IndisputableMonolith.Cosmology.PhaseSaturationVacuum
   6import IndisputableMonolith.Cosmology.GStarThresholds
   7
   8/-!
   9# Electroweak Phase Transition on the φ-Ladder
  10
  11STATUS TAG: **MODEL (RS-native-unit scaffold)**, honestly scoped per the
  122026-06-25 external review. This module formalizes the electroweak transition
  13temperature T_EW on the φ-ladder and the radiation-era Hubble rate H(T_EW),
  14yielding a sphaleron-to-Hubble ratio. What it does and does not do:
  15
  16- It DOES implement the full radiation-era Friedmann combination
  17  H² = (8π²/90)·G·g★·T⁴ INCLUDING the T⁴ factor (the review caught an
  18  earlier version that wrote T⁴ in comments but omitted it from
  19  `hubble_sq_at_ew`; that is fixed below — `hubble_sq_at_ew` now carries
  20  `T_ew ^ 4` explicitly).
  21- It does NOT feed the resulting washout ratio into the Planck-matched
  22  η_B = φ⁻⁴⁴·(1−φ⁻⁸)² expression. That expression contains no g★ and no
  23  Γ_sph/H; the quantities built here are a separate, positive-definite
  24  scaffold for a future genuine Boltzmann-transport treatment. Do not cite
  25  `effective_washout` as the origin of the η_B prefactor.
  26
  27## The φ-Ladder Rung for T_EW
  28
  29The Z boson mass sits at EW sector rung 51, giving m_Z = 2 × φ⁵¹ / 10⁶ MeV
  30(from ElectroweakMasses.lean). The EW phase transition temperature
  31T_EW ≈ m_Z (standard EW baryogenesis: T_EW ~ 100 GeV). In RS-native units
  32we take T_EW = φ⁵¹ on the ladder (the sector prefactor 2/10⁶ MeV is a unit
  33choice, not part of the dimensionless ratio built here).
  34
  35## The Hubble Rate
  36
  37In the radiation-dominated era, the Friedmann equation gives:
  38
  39  H² = (8π/3) · G · ρ_rad = (8π/3) · G · (π²/30) · g★ · T⁴
  40
  41In RS-native units with G = φ⁵/π:
  42
  43  H² = (8π²/90) · (φ⁵/π) · g★ · T⁴ = (8π/90) · φ⁵ · g★ · T⁴
  44
  45The ratio Γ_sph / (H·T) gives the washout efficiency.
  46
  47## Main Results
  48
  49- `ew_rung`: the φ-ladder rung for the EW scale = 51
  50- `T_ew`: the RS-native EW temperature φ⁵¹
  51- `hubble_sq_at_ew`: the full H² = coeff · G · g★ · T⁴ (T⁴ included)
  52- `sphaleron_hubble_ratio`: Γ_sph / (H·T) at T_EW
  53- `washout_efficiency`: the dimensionless washout factor (scaffold only;
  54  NOT the source of the η_B prefactor)
  55- `g_star_ew_matches_threshold_fn`: the fixed 106.75 used here equals the
  56  high-T evaluation of the g_star(T) step function (GStarThresholds)
  57
  58## Status: 0 sorry, 0 axiom
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Cosmology
  63namespace EWPhaseTransition
  64
  65open Real Constants SphaleronRate
  66
  67noncomputable section
  68
  69/-! ## Part 1: The EW Scale on the φ-Ladder -/
  70
  71/-- The φ-ladder rung for the electroweak scale.
  72    The Z boson mass is at rung 51 in the EW sector mass formula:
  73    m_Z = 2 × φ⁵¹ / 10⁶ MeV (from ElectroweakMasses.z_pred_eq).
  74    The EW phase transition temperature T_EW ≈ m_Z in natural units. -/
  75def ew_rung : ℤ := 51
  76
  77/-- The RS-native EW temperature: T_EW = φ⁵¹ on the ladder (the EW-sector
  78    unit prefactor is absorbed into the unit choice; only φ-power structure
  79    matters for the RS-native ratios below). -/
  80def T_ew : ℝ := phi ^ (51 : ℕ)
  81
  82theorem T_ew_pos : 0 < T_ew := pow_pos phi_pos 51
  83
  84/-- The effective degrees of freedom at the EW scale: the standard
  85    high-temperature SM value 106.75. Honest provenance (see
  86    StandardModel.RelativisticDOF header): the gauge GROUP and generation
  87    COUNT are RS-derived; the matter representations, minimal-neutrino
  88    convention, and the 7/8 thermal integral are imported SM content. This
  89    fixed number is the high-T evaluation of the temperature-dependent step
  90    function Cosmology.GStarThresholds.g_star (bridge theorem below). -/
  91def g_star_ew : ℝ := 106.75
  92
  93theorem g_star_ew_pos : 0 < g_star_ew := by norm_num [g_star_ew]
  94
  95/-- The fixed g★ = 106.75 used at T_EW equals the high-temperature
  96    evaluation of the g_star(T) threshold step function: the constant is a
  97    function value, not a free-standing number. -/
  98theorem g_star_ew_matches_threshold_fn :
  99    g_star_ew = ((GStarThresholds.g_star 200 : ℚ) : ℝ) := by
 100  rw [GStarThresholds.g_star_high]
 101  norm_num [g_star_ew]
 102
 103/-! ## Part 2: The Hubble Rate at T_EW -/
 104
 105/-- The Friedmann radiation-era coefficient.
 106    H² = friedmann_coeff · G · g★ · T⁴
 107    where friedmann_coeff = 8π²/90 from the Stefan-Boltzmann law for
 108    relativistic species.
 109
 110    In RS-native units: G = φ⁵/π, so:
 111    H² = (8π²/90) · (φ⁵/π) · g★ · T⁴ = (8π/90) · φ⁵ · g★ · T⁴ -/
 112def friedmann_coeff : ℝ := 8 * Real.pi ^ 2 / 90
 113
 114theorem friedmann_coeff_pos : 0 < friedmann_coeff := by
 115  unfold friedmann_coeff
 116  positivity
 117
 118/-- G in RS-native units: G = φ⁵/π. -/
 119def G_rs : ℝ := phi ^ (5 : ℕ) / Real.pi
 120
 121theorem G_rs_pos : 0 < G_rs := by
 122  unfold G_rs
 123  exact div_pos (pow_pos phi_pos 5) Real.pi_pos
 124
 125/-- H² at T_EW in RS-native units, with the T⁴ factor INCLUDED:
 126    H² = friedmann_coeff · G_rs · g★ · T_EW⁴.
 127    (The 2026-06-25 review caught the earlier omission of T⁴; this
 128    definition now matches the header formula exactly.) -/
 129def hubble_sq_at_ew : ℝ := friedmann_coeff * G_rs * g_star_ew * T_ew ^ 4
 130
 131theorem hubble_sq_at_ew_pos : 0 < hubble_sq_at_ew := by
 132  unfold hubble_sq_at_ew
 133  exact mul_pos (mul_pos (mul_pos friedmann_coeff_pos G_rs_pos) g_star_ew_pos)
 134    (pow_pos T_ew_pos 4)
 135
 136/-! ## Part 3: The Sphaleron-to-Hubble Ratio -/
 137
 138/-- The dimensionless sphaleron-to-Hubble ratio at T_EW:
 139    R = Γ_sph / (H · T³·T) = (Γ_sph/T⁴) · T³ / H
 140    with Γ_sph/T⁴ = sphaleron_rate_dimensionless and H = √(H²), i.e.
 141    R = sphaleron_rate_dimensionless · T_EW³ / √hubble_sq_at_ew.
 142    (The T³ factor is now explicit, consistent with the T⁴ in H².)
 143
 144    This ratio determines the washout efficiency: if R >> 1,
 145    sphalerons are fast and wash out any asymmetry; if R ~ 1,
 146    they are just active enough to generate asymmetry. -/
 147def sphaleron_hubble_ratio : ℝ :=
 148  sphaleron_rate_dimensionless * T_ew ^ 3 / Real.sqrt hubble_sq_at_ew
 149
 150/-- The ratio is positive (both numerator and denominator are positive). -/
 151theorem sphaleron_hubble_ratio_pos : 0 < sphaleron_hubble_ratio := by
 152  unfold sphaleron_hubble_ratio
 153  exact div_pos (mul_pos sphaleron_rate_pos (pow_pos T_ew_pos 3))
 154    (Real.sqrt_pos.mpr hubble_sq_at_ew_pos)
 155
 156/-! ## Part 4: The Washout Efficiency -/
 157
 158/-- The washout efficiency factor: sphaleron_hubble_ratio / g★.
 159
 160    In standard electroweak baryogenesis, the baryon asymmetry is
 161    η_B ∝ (ε_CP / g★) × min(1, R) where ε_CP is the CP asymmetry and R the
 162    sphaleron-Hubble ratio; this quantity is the combination R / g★.
 163
 164    HONEST SCOPE (per the 2026-06-25 review): this is a positive-definite
 165    SCAFFOLD, not a thermal washout calculation. It is NOT connected to the
 166    Planck-matched η_B = φ⁻⁴⁴·(1−φ⁻⁸)² expression, which contains no g★ and
 167    no Γ_sph/H. A genuine connection requires Boltzmann transport through
 168    the transition, which is OPEN. -/
 169def effective_washout : ℝ := sphaleron_hubble_ratio / g_star_ew
 170
 171theorem effective_washout_pos : 0 < effective_washout := by
 172  unfold effective_washout
 173  exact div_pos sphaleron_hubble_ratio_pos g_star_ew_pos
 174
 175/-! ## Part 5: Certificate -/
 176
 177structure EWTransitionCert where
 178  ew_scale : ew_rung = 51
 179  g_star_val : g_star_ew = 106.75
 180  t_ew_positive : 0 < T_ew
 181  friedmann_positive : 0 < friedmann_coeff
 182  G_positive : 0 < G_rs
 183  hubble_positive : 0 < hubble_sq_at_ew
 184  ratio_positive : 0 < sphaleron_hubble_ratio
 185  washout_positive : 0 < effective_washout
 186
 187theorem ew_transition_cert : EWTransitionCert where
 188  ew_scale := rfl
 189  g_star_val := rfl
 190  t_ew_positive := T_ew_pos
 191  friedmann_positive := friedmann_coeff_pos
 192  G_positive := G_rs_pos
 193  hubble_positive := hubble_sq_at_ew_pos
 194  ratio_positive := sphaleron_hubble_ratio_pos
 195  washout_positive := effective_washout_pos
 196
 197end
 198
 199end EWPhaseTransition
 200end Cosmology
 201end IndisputableMonolith
 202