correction_moves_toward_cmb
plain-language theorem explainer
The first-order 8-tick washout correction to the baryon asymmetry is strictly smaller than the leading φ-ladder term φ^{-44}. Cosmologists comparing the RS η_B prediction to Planck cite this to confirm the correction moves toward the observed ~6.104×10^{-10}. The proof is a one-line alias of the algebraic inequality that multiplies the positive leading term by a washout factor less than one.
Claim. The corrected baryon asymmetry satisfies $\eta_B^{(1)} < \varphi^{-44}$, where $\eta_B^{(1)} = \varphi^{-44}\,(1 - \varphi^{-8})$ is the leading RS prediction times the first-order 8-tick washout factor.
background
In Recognition Science the baryon-to-photon ratio sits on the φ-ladder at rung −44. The leading prediction is $\eta_B = \varphi^{-44} \approx 6.376 \times 10^{-10}$. Planck 2018 reports $(6.104 \pm 0.058) \times 10^{-10}$, a ~4.5% excess that cannot be tuned away because RS has zero free parameters.
This module adds a first-order correction from 8-tick defect washout at the electroweak transition. Sphalerons stay active for about $N_{\mathrm{sph}} \approx \varphi^8$ cycles; each cycle reduces defect by $\delta = \varphi^{-8}$, so the net washout is $(1 - \varphi^{-8}) \approx 0.9853$. The corrected prediction is $\eta_B^{(1)} = \varphi^{-44} \times (1 - \varphi^{-8})$.
Upstream, the φ-scale definition is exactly $\varphi^{-44}$. The sibling result already proves the corrected value is strictly below that leading scale, from positivity of the leading term and the fact that the correction factor is less than one.
proof idea
One-line term-mode wrapper. The claim is definitionally the same as the sibling inequality that the corrected prediction is less than the leading term. That sibling unfolds the corrected value as the leading φ-scale times the correction factor, then uses positivity of the leading term and the correction factor being strictly less than one to get a strict product inequality.
why it matters
Names the directional claim that the 8-tick washout moves RS $\eta_B$ toward the CMB value rather than away from it. The leading term overshoots Planck by ~4.5%; multiplying by $(1 - \varphi^{-8})$ cuts the prediction to ~$6.28 \times 10^{-10}$ and roughly halves the gap. The factor $\varphi^{-8}$ is the same rung-8 that appears in the eight-tick octave (forcing chain T7). No downstream theorems currently depend on this alias; it is a named structural claim for the cosmology narrative and for reading against the module's explicit falsifier bands on $\eta_B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.