eta_B_corrected
plain-language theorem explainer
The definition supplies the RS-corrected baryon asymmetry as the product of the two-sided 8-tick washout prefactor c_RS and phi to the power minus 44. Cosmologists comparing Recognition Science predictions to Planck data would cite this expression when checking the interval (6.0e-10, 6.2e-10). It is assembled by a direct one-line definition that composes the already-bounded prefactor with the algebraic content fixed by the integration-gap rung.
Claim. The corrected baryon asymmetry is defined by $c_{RS} := (1 - phi^{-8})^2$ and $eta_B^{corrected} := c_{RS} phi^{-44}$.
background
In the Recognition Science treatment of baryogenesis the prefactor c in the formula eta_B = c times algebraic content is obtained from the two-sided 8-tick washout. Each sector carries one integration-gap worth of fermionic degrees of freedom and is suppressed at rate phi^{-8} per fundamental tick in three spatial dimensions; the squared form encodes the two independent channels. The upstream sibling definition c_RS := correctionFactor ^ 2 supplies the numerical interval (0.956, 0.959) once phi^8 is bounded via the Fibonacci identity phi^8 = 21 phi + 13.
proof idea
The declaration is a one-line definition that multiplies the washout prefactor c_RS by the algebraic factor phi to the power minus 44. No tactics are invoked; the expression is assembled directly from the sibling definitions c_RS and the power phi ^ (-44 : Z).
why it matters
This definition supplies the explicit numerical prediction certified by the downstream band theorem eta_B_corrected_in_observed_band and the structure EtaBPrefactorCert, which places the Planck central value 6.10 times 10^{-10} inside (6.0 times 10^{-10}, 6.2 times 10^{-10}). It completes the T7 eight-tick octave step by fixing the exponent -44 and thereby closes the cosmology module's contribution to the Recognition Science derivation of constants. The squared washout interpretation remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.