corrected_decomposition
plain-language theorem explainer
The first-order corrected baryon asymmetry equals the leading φ-ladder term minus that term times the per-cycle washout rate: φ⁻⁴⁴ − φ⁻⁴⁴·φ⁻⁸. Cosmologists matching the RS η_B prediction to CMB data cite this algebraic split. The proof unfolds the product definition and closes by ring.
Claim. The first-order corrected baryon asymmetry equals the leading scale minus the leading scale times the washout rate: $\eta_B^{(1)} = \varphi^{-44} - \varphi^{-44}\,\varphi^{-8}$. Equivalently $\eta_B^{(1)} = \varphi^{-44}(1-\varphi^{-8}) = \varphi^{-44}-\varphi^{-52}$.
background
Recognition Science places the baryon-to-photon ratio on the φ-ladder at rung −44, so the leading prediction is $\eta_B = \varphi^{-44}$. That value sits about 4.5% above the Planck 2018 CMB central value. With no free parameters available to tune, the module studies the first subleading correction from 8-tick defect washout during the electroweak epoch.
The washout rate per 8-tick cycle is $\delta = \varphi^{-8}$ (one rung). The first-order correction factor is $1-\delta$, and the corrected asymmetry is defined as the product of the leading scale with that factor. The physical picture is that sphalerons remain active for roughly $N_{\mathrm{sph}}\approx\varphi^8$ cycles, each applying one recognition-operator defect reduction step.
Upstream, eta_B_phi_scale is exactly $\varphi^{-44}$; delta_washout is $\varphi^{-8}$; correction_factor is $1-\delta$; and eta_B_corrected is their product. The present identity simply expands that product.
proof idea
Term-mode proof by definitional expansion. Unfold the corrected asymmetry (product of the leading scale with the correction factor) and the correction factor itself ($1-\delta$). The goal becomes $\varphi^{-44}\cdot(1-\delta)=\varphi^{-44}-\varphi^{-44}\cdot\delta$, which ring discharges as a commutative-ring identity. No external lemmas are required.
why it matters
This identity is the algebraic content of the first-order 8-tick correction advertised in the module: $\eta_B^{(1)}=\varphi^{-44}(1-\varphi^{-8})=\varphi^{-44}-\varphi^{-52}$. It converts the product form used in positivity and interval lemmas into an explicit two-term φ-ladder decomposition (rungs −44 and −52).
In the broader RS chain the eight-tick octave is landmark T7; the washout rate $\delta=\varphi^{-8}$ is one full octave on the ladder. Numerically the correction multiplies the leading $6.376\times10^{-10}$ by $\approx0.9853$, yielding $\approx6.28\times10^{-10}$ and roughly halving the gap to Planck. The module marks the washout mechanism itself as hypothesis, with explicit falsifiers on the $\eta_B$ windows $[5.5,7.5]\times10^{-10}$ (leading) and $[6.0,6.5]\times10^{-10}$ (corrected). No downstream theorems yet consume the identity; it stands as the clean expansion step for any later comparison or error-budget argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.