T_ew
plain-language theorem explainer
The electroweak transition temperature in RS-native units is fixed as φ to the 51st power on the recognition ladder. Anyone computing the radiation-era Hubble rate or the sphaleron-to-Hubble washout ratio at the EW scale cites this as the temperature input. It is a pure definition: the sector unit prefactor is absorbed into the unit choice, leaving only the φ-power.
Claim. The electroweak phase-transition temperature in Recognition Science native units is $T_{\mathrm{EW}} = \varphi^{51}$, where $\varphi$ is the golden-ratio fixed point of the recognition cost.
background
This module treats the electroweak phase transition as an RS-native-unit scaffold on the φ-ladder. The Z boson mass sits at EW-sector rung 51, so $m_Z = 2 \times \varphi^{51}/10^6,\mathrm{MeV}$ in the electroweak mass ladder. Standard EW baryogenesis takes $T_{\mathrm{EW}} \sim m_Z \sim 100,\mathrm{GeV}$; in RS-native units the sector prefactor is dropped and only the φ-power is kept, giving $T_{\mathrm{EW}} = \varphi^{51}$.
The local goal is the radiation-era Friedmann combination $H^2 = (8\pi^2/90),G,g_\star,T^4$ at this temperature, with $G = \varphi^5/\pi$ in RS units, and from it the dimensionless sphaleron-to-Hubble ratio that controls washout efficiency. The module is explicitly scoped as a positive-definite scaffold, not a full Boltzmann-transport derivation of $\eta_B$.
proof idea
One-line definition: assign the real $T_{\mathrm{EW}}$ to $\varphi^{51}$ via ordinary natural-number exponentiation. No lemmas are invoked; positivity is discharged separately by the sibling theorem that applies pow_pos to the positivity of $\varphi$.
why it matters
This temperature is the scale input for the entire EW-transition scaffold. It appears in hubble_sq_at_ew as the $T^4$ factor in the radiation-era Friedmann equation, in sphaleron_hubble_ratio as the $T^3$ numerator against $\sqrt{H^2}$, and as the positivity obligation inside the certificate structure EWTransitionCert (which packages $T_{\mathrm{EW}}>0$ with $g_\star=106.75$ and the Friedmann coefficient). Downstream washout efficiency is built as that ratio divided by $g_\star$. The definition does not feed the Planck-matched $\eta_B = \varphi^{-44}(1-\varphi^{-8})^2$ expression; that formula carries neither $g_\star$ nor $\Gamma_{\mathrm{sph}}/H$. Landmark contact is the φ-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}}$) and the RS-native $G=\varphi^5/\pi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.