eta_B_corrected_pos
plain-language theorem explainer
The theorem proves that the RS-corrected baryon asymmetry eta_B_corrected is strictly positive. Cosmologists using the Recognition Science phi-ladder for baryogenesis predictions would cite it to anchor the lower edge of the predicted band. The proof is a one-line term-mode wrapper that unfolds the definition and applies the mul_pos lemma to c_RS_pos together with zpow_pos on phi_pos at exponent -44.
Claim. $0 < c_{RS} · ϕ^{-44}$, where $c_{RS} = (1 - ϕ^{-8})^2$ is the squared washout prefactor and the full expression is the corrected RS prediction for the baryon-to-photon ratio η_B.
background
The EtaBPrefactorDerivation module defines the order-one prefactor c_RS as (1 − ϕ^{−8})^2 to capture two independent washout channels, each carrying one integration-gap rung of fermionic degrees of freedom at the eight-tick scale. The definition eta_B_corrected := c_RS * phi^(-44) multiplies this prefactor by the Fibonacci-derived suppression at rung 44. The upstream theorem c_RS_pos establishes 0 < c_RS by unfolding to correctionFactor and invoking one_minus_phi_neg8_lower with positivity tactics.
proof idea
The proof unfolds eta_B_corrected to expose the product form, then applies the mul_pos lemma directly to the already-established c_RS_pos and the zpow_pos instance for phi_pos at exponent -44.
why it matters
This result supplies the positivity half of the band-level claim documented in the module, confirming the predicted η_B lies above 6.0 × 10^{-10} and matches the Planck 2018 central value. It supports the eight-tick octave and D = 3 by keeping the algebraic content positive on the phi-ladder. The squared prefactor remains hypothesis-grade pending a first-principles Boltzmann derivation, while the numerical band itself is theorem-grade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.