two_sided_stronger_than_one_sided

In the baryon-asymmetry layer the bare RS scale is $\varphi^{-44}$. A first-order washout multiplies by the correction factor $1 - \delta$ with $\delta = \varphi^{-8}$ (the eight-tick rung). Upstream lemmas place that factor strictly in $(0,1)$: it is positive because $\delta < 1$, and less than 1 because $\delta > 0$.

This module defines the squared prefactor $c_{RS} = (1 - \varphi^{-8})^2$, motivated by a two-sided washout heuristic in which matter and antimatter each contribute one factor of $(1 - \delta)$. The module docstring is explicit that the square is a selected ansatz, not a Boltzmann or rate derivation; it was chosen because it moves the bare rung into the observed $\eta_B$ band.

The local setting is therefore algebraic comparison of two defined order-one factors, not a claim that either factor is the physical washout.

Unfold $c_{RS}$ to the square of the correction factor. Pull in the two upstream facts that the correction factor lies strictly in $(0,1)$. A three-line calc then finishes: $x^2 = x \cdot x < 1 \cdot x = x$, using right-multiplication of the strict inequality $x < 1$ by the positive quantity $x$, then the unit law for multiplication.

Immediate parent is the comparison of full predictions: the two-sided corrected $\eta_B$ is strictly smaller than the one-sided corrected value (BaryonHigherOrder.eta_B_corrected). That lift multiplies the present prefactor inequality by the positive bare scale $\varphi^{-44}$.

In the Recognition framework this sits in the cosmology attempt to place $\eta_B$ near $6 \times 10^{-10}$ via the $\varphi$-ladder and the eight-tick octave (T7). The module itself flags $c_{RS}$ as selected rather than derived, so the inequality is algebraic bookkeeping on an ansatz. It does not close the open Boltzmann/rate gap named in the module docstring.