c_RS_in_unit_interval

In the η_B module the order-one prefactor is defined by $c_{\mathrm{RS}} := (1 - \varphi^{-8})^2$, equivalently the square of a correction factor built from the eight-tick rung. The module docstring is explicit that this squared form is a selected ansatz, not a Boltzmann derivation: it was chosen among comparable order-one lookalikes because it moves the bare rung $\varphi^{-44}$ into the observed Planck band.

Positivity of the correction factor and the identity $\varphi^2 = \varphi + 1$ are already available upstream. Two sibling theorems establish $0 < c_{\mathrm{RS}}$ (by squaring a positive base) and $c_{\mathrm{RS}} < 1$ (by multiplying a factor strictly less than one by itself). The present statement simply packages those two bounds as a single conjunctive claim that the prefactor is order-one.

One-line term proof: the pair constructor assembles the two sibling theorems c_RS_pos and c_RS_lt_one into the conjunction $0 < c_{\mathrm{RS}} \land c_{\mathrm{RS}} < 1$. No further algebra is performed here; both conjuncts are already closed.

This unit-interval fact is a required field of the η_B prefactor certificate (eta_B_prefactor_cert), which records that the corrected RS prediction $c_{\mathrm{RS}}\cdot\varphi^{-44}$ lands in $(6.0,6.2)\times 10^{-10}$ and that the observed value sits inside the predicted band. The eight-tick exponent ties the construction to the T7 octave (period $2^3$) in the forcing chain, even though the squared washout reading itself remains an interpretive hypothesis with no rate calculation behind it. The theorem therefore closes only the algebraic side of the prefactor story: positivity and strict contractivity of a defined quantity, not a derivation of the physical washout.