corrected_lt_leading
plain-language theorem explainer
The two-sided corrected baryon asymmetry η_B^RS = c_RS · φ^(-44) is strictly smaller than the bare leading rung φ^(-44). Cosmology proofs that place the corrected value below the leading term, or certify motion toward the CMB band, cite this inequality. The argument is a short calc: multiply the already-proved bound c_RS < 1 by the positive scale φ^(-44).
Claim. Let $\eta_B^{\mathrm{lead}} = \varphi^{-44}$ and let $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$. Then the corrected prediction $\eta_B^{\mathrm{RS}} := c_{\mathrm{RS}} \cdot \eta_B^{\mathrm{lead}}$ satisfies $\eta_B^{\mathrm{RS}} < \eta_B^{\mathrm{lead}}$.
background
In the RS baryon-asymmetry ladder the bare prediction sits on rung $-44$: $\eta_B^{\mathrm{lead}} = \varphi^{-44}$. The module defines an order-one prefactor $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$, motivated by a two-sided 8-tick washout heuristic (one factor per matter/antimatter sector). The fully corrected quantity is then $\eta_B^{\mathrm{RS}} = c_{\mathrm{RS}} \cdot \varphi^{-44}$.
The module docstring is explicit that $c_{\mathrm{RS}}$ is a selected ansatz, not a Boltzmann derivation: any residual factor in $(0.9,1)$ would land near the Planck band. What is kernel-checked is pure algebra on that defined quantity: positivity, $c_{\mathrm{RS}} < 1$, and the numerical band $c_{\mathrm{RS}}\cdot\varphi^{-44}\in(6.0,6.2)\times 10^{-10}$.
Upstream facts used here are positivity of the leading scale (eta_B_phi_scale_pos) and the strict bound $c_{\mathrm{RS}} < 1$ (c_RS_lt_one).
proof idea
Unfold the definition $\eta_B^{\mathrm{RS}} = c_{\mathrm{RS}}\cdot\eta_B^{\mathrm{lead}}$. Invoke $c_{\mathrm{RS}} < 1$ and $0 < \eta_B^{\mathrm{lead}}$. Then
$$c_{\mathrm{RS}}\cdot\eta_B^{\mathrm{lead}} < 1\cdot\eta_B^{\mathrm{lead}} = \eta_B^{\mathrm{lead}}$$
by right-multiplication of a strict inequality by a positive real, followed by one_mul. No interval arithmetic or rung estimates are needed beyond those two lemmas.
why it matters
This is the two-sided analogue of the single-factor inequality in BaryonHigherOrder.corrected_lt_leading. Downstream, corrected_in_range packages positivity with this strict upper bound; correction_moves_toward_cmb reuses the same comparison to argue the correction points toward the CMB value $\sim 6.1\times 10^{-10}$ (below the bare $\varphi^{-44}\approx 6.4\times 10^{-10}$); and baryon_correction_cert records the structural certificate for the washout story.
Framework context: the 8-tick octave (T7) supplies the $\varphi^{-8}$ gap inside $c_{\mathrm{RS}}$, while the bare rung $-44$ is the decade-level RS match. The module honesty note still applies: the inequality is algebraic on a defined prefactor; it does not close the open Boltzmann/rate derivation of the squared form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.