eta_B_corrected_two_sided
plain-language theorem explainer
The fully corrected RS prediction for the baryon-to-photon ratio is the product of the selected order-one prefactor c_RS = (1 − φ^(−8))^2 and the bare φ-ladder scale φ^(−44). Cosmologists matching RS η_B to the Planck 2018 band cite this quantity. It is a one-line definitional product of two already-named real constants; no tactics are involved.
Claim. Define the corrected RS baryon-to-photon ratio by $\eta_B^{\mathrm{RS}} := c_{\mathrm{RS}} \cdot \varphi^{-44}$, where $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$ is the selected two-sided washout prefactor and $\varphi^{-44}$ is the bare rung scale.
background
In Recognition Science the baryon-to-photon ratio is predicted to sit on the φ-ladder at rung −44, so the leading scale is $\varphi^{-44} \approx 6.41 \times 10^{-10}$. An order-one prefactor is then applied to land inside the observed Planck band.
This module defines $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$. The module docstring is explicit that the squared form is a selected ansatz, not a Boltzmann derivation: it was chosen among comparable order-one lookalikes because it moves the bare rung into $(6.0, 6.2) \times 10^{-10}$. The two-sided washout story (one factor of $(1-\delta)$ per matter/antimatter sector at the 8-tick rung) is retained only as motivating heuristic.
Upstream, the bare scale is simply $\varphi^{-44}$, and $c_{\mathrm{RS}}$ expands to $(1-\varphi^{-8})^2$ via the correction factor tied to the eight-tick octave.
proof idea
One-line definitional product: the corrected prediction is $c_{\mathrm{RS}}$ times the bare scale $\varphi^{-44}$. No tactics or lemmas are required; both factors are already defined reals in the module and its imports.
why it matters
This definition is the quantity whose positivity, strict inequality below the bare rung, and membership in $(6.0, 6.2)\times 10^{-10}$ are proved immediately downstream (positivity, corrected less than leading, lower/upper bounds, and the observed-band theorem). It also feeds the η_B prefactor certificate and the T6–T8 bridge to cosmology constants in the unified forcing chain.
Framework landmarks: φ is forced at T6; the eight-tick octave at T7 supplies $\delta = \varphi^{-8}$ inside $c_{\mathrm{RS}}$. The module honesty note matters: algebra and interval arithmetic are kernel-checked facts about a defined quantity, while the physical washout reading remains an open hypothesis with no rate calculation behind it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.