eta_B_corrected_pos

This module treats the first subleading correction to the RS baryon asymmetry. The leading prediction is $\eta_B = \phi^{-44}\approx 6.376\times 10^{-10}$, about 4.5% above the Planck 2018 CMB central value. With no free parameters, the gap cannot be tuned; the proposed fix is an 8-tick sphaleron washout.

During the electroweak epoch, sphalerons run for roughly $N_{\mathrm{sph}}\approx\phi^8$ cycles of the fundamental eight-tick octave. Each cycle multiplies residual defect by a factor involving $\delta=\phi^{-8}$, so the net correction factor is $1-\delta=(1-\phi^{-8})\approx 0.985$. The corrected quantity is therefore the product of the leading $\phi$-scale term and that factor.

Upstream, the leading scale is already known positive, and the correction factor is positive because $\delta<1$. The fundamental tick $\tau_0=1$ fixes the discrete time unit behind the eight-tick period.

One-line term proof. Unfold the corrected asymmetry as the product of the leading $\phi$-scale term and the washout factor, then apply real multiplication-positivity to the two prior lemmas: the leading term is positive, and the correction factor is positive (from $\delta<1$). No further arithmetic is required.

Positivity is the lower half of the sandwich used by corrected_in_range, which places the corrected prediction strictly between 0 and the leading term, and it is packaged into the baryon-correction certificate that records the full first-order claim $\eta_B\mapsto\phi^{-44}(1-\phi^{-8})$.

In the RS forcing chain this sits on T6–T7: $\phi$ as the self-similar fixed point and the eight-tick octave as the evolution period. The washout picture is still marked HYPOTHESIS in the module: if precision data put $\eta_B$ outside $[6.0,6.5]\times 10^{-10}$ at $>3\sigma$, the corrected prediction fails; outside $[5.5,7.5]\times 10^{-10}$ at $>5\sigma$ even the leading term fails. This lemma does not resolve that empirical question; it only guarantees the corrected number stays physically signed.