eta_B_corrected_upper
plain-language theorem explainer
The corrected baryon asymmetry eta_B equals c_RS times phi to the power -44 and is shown to lie strictly below 6.2 times 10 to the -10. Cosmologists testing Recognition Science baryogenesis against Planck data would cite this bound to close the upper edge of the predicted interval. The proof unfolds the definition of eta_B_corrected and feeds four pre-established inequalities (upper bounds on c_RS and on phi^{-44} together with positivity) directly into nlinarith.
Claim. Let $c_{RS} = (1 - phi^{-8})^2$ be the two-sided 8-tick washout prefactor. Define the corrected baryon-to-photon ratio by $eta_B = c_{RS} cdot phi^{-44}$. Then $eta_B < 6.2 times 10^{-10}$.
background
In the Recognition Science module on eta_B, the prefactor c_RS is defined as the square of (1 - phi^{-8}), where the exponent -8 encodes one rung per fundamental tick in the eight-tick octave at D = 3. Each factor of (1 - phi^{-8}) represents washout of one integration-gap sector of fermionic degrees of freedom. The corrected eta_B is then obtained by multiplying this prefactor by phi^{-44}, which supplies the algebraic mass-scale content forced by the integration-gap rung. Upstream lemmas establish c_RS < 0.959, phi^{-44} < 6.40e-10, and the positivity of both quantities.
proof idea
The proof is a one-line wrapper. It unfolds eta_B_corrected to the product c_RS * phi^{-44}, then supplies the four facts c_RS_upper, phi_zpow_neg44_upper, c_RS_pos, and zpow_pos. These inequalities are passed to nlinarith, which closes the strict upper bound.
why it matters
This theorem supplies the upper half of the two-sided band proved in eta_B_corrected_in_observed_band, which places the Recognition Science prediction inside the Planck 2018 interval (6.10 plus or minus 0.04) times 10^{-10}. It quantifies the T7 eight-tick octave contribution to the forcing chain by bounding the washout at rung -8 and the rung -44 factor. The numerical band itself is theorem-grade; the squared interpretive form of c_RS remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.