correction_factor_lt_one

This module treats the first subleading correction to the RS baryon asymmetry. The leading prediction is $\eta_B=\varphi^{-44}\approx 6.376\times 10^{-10}$, about 4.5% above the Planck 2018 CMB central value. With no free parameters, the gap is addressed by an 8-tick washout during the electroweak sphaleron epoch.

Each of roughly $N_{\mathrm{sph}}\approx\varphi^8$ active 8-tick cycles multiplies residual defect by a factor $1-\delta$ with natural rate $\delta=\varphi^{-8}$. The first-order correction factor is therefore defined as $1-\delta=1-\varphi^{-8}$. Upstream, positivity of $\delta$ is already proved from $\varphi>0$ via the negative power $\varphi^{-8}$.

The local goal is to place this factor strictly inside $(0,1)$ so that the corrected prediction $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})$ is a genuine downward shift of the leading term.

Term-mode proof in two steps. Unfold the definition of the correction factor to $1-\delta$. Invoke the upstream positivity lemma $0<\delta$ (itself a one-line application of positivity of negative powers of $\varphi$). Linear arithmetic then closes $1-\delta<1$.

The inequality is the upper half of the certificate that the washout factor lies in $(0,1)$. It is packed into the baryon-correction certificate structure, used to prove that the corrected $\eta_B$ is strictly below the leading $\varphi^{-44}$ term, and combined with positivity to obtain the open interval statement.

Downstream prefactor work squares the same factor: the RS prefactor $c_{\mathrm{RS}}=(1-\varphi^{-8})^2$ is shown less than one, and the two-sided correction is shown strictly stronger than the one-sided factor, both by quoting this bound. In the broader RS chain the 8-tick octave (T7) supplies the natural period whose defect reduction produces $\delta=\varphi^{-8}$; the result is a proved arithmetic lemma inside a still-hypothetical washout mechanism whose falsifiers are stated in the module doc.