two_sided_corrected_lt_one_sided
plain-language theorem explainer
The two-sided washout-corrected baryon asymmetry is strictly smaller than the one-sided first-order correction. Cosmologists ranking RS η_B predictions cite this to place the squared prefactor below the linear one on the same φ-ladder scale. The proof multiplies the factor inequality by the positive φ^{-44} scale and closes with linear arithmetic.
Claim. The two-sided corrected baryon-to-photon ratio is strictly smaller than the one-sided corrected ratio: $\eta_B^{\mathrm{two\text{-}sided}} < \eta_B^{\mathrm{one\text{-}sided}}$, where the one-sided value is the bare $\phi$-ladder scale $\phi^{-44}$ times the linear washout factor $(1-\phi^{-8})$, and the two-sided value multiplies the same scale by the squared prefactor $(1-\phi^{-8})^2$.
background
In the RS baryogenesis stack the bare scale is $\eta_B\sim\phi^{-44}$. A first-order correction multiplies by the linear washout factor $(1-\phi^{-8})$, tied to the eight-tick octave (T7). The two-sided ansatz instead multiplies by $c_{\mathrm{RS}}=(1-\phi^{-8})^2$, motivated by applying one factor to each of the matter and antimatter sectors.
The module itself retracts any claim that the square is derived from a Boltzmann or $\Gamma/H$ calculation: $c_{\mathrm{RS}}$ is a selected order-one lookalike that moves the bare rung into the Planck band. What remains proved is algebra and interval arithmetic on that defined quantity.
Upstream, positivity of the $\phi^{-44}$ scale is already available, and a sibling lemma records that the squared factor is strictly stronger (smaller) than the linear factor on $(0,1)$.
proof idea
Term-mode proof. Unfold both corrected predictions to expose the common positive scale $\phi^{-44}$ times the respective washout factors. Invoke the sibling inequality that the two-sided factor is strictly smaller than the one-sided factor. Multiply that strict inequality on the right by the positive scale (via mul_lt_mul_of_pos_right and the positivity theorem for the $\phi$-ladder scale). Close the resulting comparison with linarith.
why it matters
Feeds the master certificate eta_B_prefactor_cert, which packages unit-interval membership of $c_{\mathrm{RS}}$, the expanded form $(1-\phi^{-8})^2$, and the numerical band for the two-sided prediction against the observed $\eta_B$.
Within the framework this sits on the eight-tick octave (T7) and the $\phi$-ladder mass/scale structure: the washout defect is one rung of $\phi^{-8}$. The comparison is purely algebraic ranking of two defined corrections; it does not close the open Boltzmann/rate derivation flagged in the module honesty note. It does, however, make precise that adopting the squared prefactor systematically lowers the prediction relative to the linear first-order correction on the same scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.