IndisputableMonolith.Cosmology.EWPhaseTransition
Defines the electroweak phase-transition epoch in RS-native units: the φ-ladder rung for the EW scale, the transition temperature T_EW, the relativistic d.o.f. count g_*(T_EW), and the Hubble rate squared at that temperature. Cosmology and baryogenesis lanes cite these as the fixed EW background. Values are assembled from the Z-boson rung, the g_* threshold model, and the RS Newton constant, with positivity lemmas.
claimFix the electroweak rung $r_{\mathrm{EW}}=51$ from $m_Z=2\varphi^{51}/10^6\,\mathrm{MeV}$. Set $T_{\mathrm{EW}}\approx m_Z>0$, take $g_*(T_{\mathrm{EW}})$ from the instantaneous SM threshold model, and form $H^2(T_{\mathrm{EW}})=(8\pi/3)G_{\mathrm{RS}}\rho(T_{\mathrm{EW}})$ with $G_{\mathrm{RS}}=\varphi^5/\pi$ and $\rho\propto g_* T^4$, all strictly positive.
background
Recognition Science places particle masses on a discrete $\varphi$-ladder. In the electroweak sector the Z boson sits at rung 51 via $m_Z=2\varphi^{51}/10^6,\mathrm{MeV}$; the EW phase-transition temperature is identified with that scale in natural units ($c=\hbar=1$).
Cosmology needs the radiation-era Hubble rate at that temperature. The energy density is $\rho=(\pi^2/30)g_(T)T^4$, with $g_(T)$ the effective relativistic degrees of freedom. The imported GStarThresholds module supplies a step-function $g_*(T)$ over Standard Model content (status: model, not a first-principles RS derivation). The RS Newton constant is $G_{\mathrm{RS}}=\varphi^5/\pi$.
SphaleronRate and PhaseSaturationVacuum sit upstream as the baryon-violation and dark-energy context; this module only freezes the EW kinematic background those lanes consume.
proof idea
Definition-and-positivity module, not a deep derivation. ew_rung is the constant 51. T_ew is built from the Z-mass / rung identification and proved positive. g_star_ew is the threshold function evaluated at $T_{\mathrm{EW}}$, with a matching lemma to GStarThresholds and a positivity proof. G_rs is the RS value $\varphi^5/\pi$ (positive). The Friedmann coefficient and hubble_sq_at_ew assemble $H^2\propto G,g_* T^4$ and discharge positivity by multiplying the positive factors. No dynamical phase-transition calculation is performed.
why it matters in Recognition Science
BaryogenesisStaging imports this module to anchor the electroweak epoch where sphalerons freeze out; that staging file holds the B−L zero-protection obstruction and refuses to fake a missing source. BaryonAsymmetryExact closes $\eta_B$ on $\varphi$-rung −44 and the balance $\eta_B\times\varphi^{45}=\varphi$; it needs a definite $T_{\mathrm{EW}}$, $g_$, and $H(T_{\mathrm{EW}})$ so the freeze-out and yield normalizations sit on the same ladder. Without a single EW background object, those lanes would re-introduce ad hoc SM temperature and $g_$ choices. The module does not itself prove baryogenesis; it only supplies the kinematic stage for the forcing chain that runs through sphaleron equilibration into the exact asymmetry rung.
scope and limits
- Does not derive a first-order vs crossover EW transition dynamics or bubble nucleation rate.
- Does not compute $g_*(T)$ from RS; uses the imported SM step-function model.
- Does not prove sphaleron freeze-out or any B−L source; only fixes $T_{\mathrm{EW}}$ and $H^2$.
- Does not identify $T_{\mathrm{EW}}$ beyond the $T\approx m_Z$ natural-unit convention.
- Does not address finite-temperature effective potential or Higgs VEV running.
used by (2)
depends on (5)
declarations in this module (18)
-
def
ew_rung -
def
T_ew -
theorem
T_ew_pos -
def
g_star_ew -
theorem
g_star_ew_pos -
theorem
g_star_ew_matches_threshold_fn -
def
friedmann_coeff -
theorem
friedmann_coeff_pos -
def
G_rs -
theorem
G_rs_pos -
def
hubble_sq_at_ew -
theorem
hubble_sq_at_ew_pos -
def
sphaleron_hubble_ratio -
theorem
sphaleron_hubble_ratio_pos -
def
effective_washout -
theorem
effective_washout_pos -
structure
EWTransitionCert -
theorem
ew_transition_cert