correction_factor_pos
plain-language theorem explainer
The first-order 8-tick washout factor $1-\varphi^{-8}$ is strictly positive. Cosmology proofs that build the corrected baryon asymmetry $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})$, or the squared RS prefactor $c_{RS}$, cite this positivity. The proof unfolds the definition and applies linear arithmetic to $\delta<1$.
Claim. Let $\delta=\varphi^{-8}$ be the per-cycle sphaleron washout rate and let the first-order correction factor be $1-\delta$. Then $0<1-\delta$.
background
The module treats the first subleading correction to the RS baryon asymmetry $\eta_B=\varphi^{-44}$. Leading order overshoots the Planck 2018 CMB value by about 4.5%. With no free parameters, the gap is addressed by an 8-tick washout: sphalerons run for $N_{\mathrm{sph}}\approx\varphi^8$ cycles, each reducing defect by $\delta=\varphi^{-8}$, so the net factor is approximately $1-\delta$.
Here correction_factor is defined as $1-\delta_{\mathrm{washout}}$ with $\delta_{\mathrm{washout}}=\varphi^{-8}$. The upstream lemma delta_lt_one records $\varphi^{-8}<1$ (since $\varphi>1$), which is exactly the arithmetic input needed for positivity of $1-\delta$. The eight-tick octave (forcing chain T7) fixes the cycle structure behind this rate.
proof idea
Term-mode proof in two steps. Unfold correction_factor to $1-\delta_{\mathrm{washout}}$. Then linarith closes $0<1-\delta$ from the single hypothesis delta_lt_one ($\delta_{\mathrm{washout}}<1$). No further lemmas are required.
why it matters
Positivity is the first half of the interval certificate $0<1-\delta<1$, packaged as correction_factor_in_interval and fed into baryon_correction_cert (the module's main hypothesis certificate that $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})$ halves the 4.5% CMB gap). It also supplies eta_B_corrected_pos via mul_pos with the leading term, and in EtaBPrefactorDerivation it gives $c_{RS}=(1-\delta)^2>0$ and the comparison that the two-sided prefactor is strictly stronger than the one-sided factor.
Framework landmarks: T7 eight-tick octave sets the washout cadence; the $\varphi$-ladder mass/yardstick structure supplies $\varphi^{-44}$ and $\varphi^{-8}$. The corrected band remains a hypothesis with an explicit CMB falsifier in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.