correction_factor
plain-language theorem explainer
The first-order correction factor for the baryon asymmetry is $1-\varphi^{-8}$, the survival fraction after one 8-tick washout step. Cosmologists assembling the RS $\eta_B$ prediction cite it when forming the corrected asymmetry $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})$. The body is a one-line subtraction of the washout rate $\delta=\varphi^{-8}$ from unity.
Claim. Define the first-order correction factor by $C := 1 - \delta$, where the washout rate per 8-tick cycle is $\delta = \varphi^{-8}$ and $\varphi$ is the golden ratio. Equivalently, $C = 1 - \varphi^{-8}$.
background
This module treats the first subleading correction to the RS baryon asymmetry $\eta_B = \varphi^{-44}$. The leading value $\varphi^{-44} \approx 6.376 \times 10^{-10}$ overshoots the Planck 2018 CMB band $(6.104 \pm 0.058) \times 10^{-10}$ by about 4.5%. With no free parameters, the gap can only shrink by computing higher-order 8-tick defect propagation.
During the electroweak phase transition, sphalerons remain active for roughly $N_{\mathrm{sph}} \approx \varphi^8$ cycles of the eight-tick octave (T7). Each cycle the recognition operator applies one defect-reduction step at the natural RS rate $\delta = \varphi^{-8}$ (one rung per active period). The per-cycle survival factor is therefore $1-\delta$.
Upstream, delta_washout is defined exactly as $\varphi^{-8}$. The present definition packages the complementary factor $1-\delta$ used throughout the corrected $\eta_B$ chain.
proof idea
Pure definitional abbreviation: unfold to $1 - \texttt{delta_washout}$, and substitute the upstream definition $\texttt{delta_washout} = \varphi^{-8}$. No tactics or lemmas are required; positivity and the bound $C < 1$ are proved in the immediate sibling theorems by linarith against $\delta > 0$ and $\delta < 1$.
why it matters
This factor is the algebraic core of the first-order washout correction $\eta_B^{(1)} = \varphi^{-44}(1-\varphi^{-8}) \approx 6.28 \times 10^{-10}$, which roughly halves the 4.5% gap to CMB data. Downstream it appears in the corrected prediction, the decomposition $\eta_B^{\mathrm{corr}} = \varphi^{-44} - \varphi^{-52}$, the strict inequality against the leading term, the interval certificate $C \in (0,1)$, and the hypothesis structure BaryonCorrectionCert that packages leading term, correction, and corrected prediction.
Framework landmarks: T7 (eight-tick octave) supplies the cycle count and the rung $\varphi^{-8}$; the mass/phi-ladder language identifies the correction term as rung $-52$. The surrounding module marks the 8-tick washout as HYPOTHESIS, with explicit falsifiers on the $\eta_B$ windows. It is also consumed by the prefactor derivation c_RS in EtaBPrefactorDerivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.