eta_B_corrected_in_observed_band
plain-language theorem explainer
The RS baryon asymmetry prediction c_RS ⋅ φ^{-44} lies strictly inside (6.0 × 10^{-10}, 6.2 × 10^{-10}). Cosmologists comparing the framework to Planck 2018 data would cite this interval. The proof is a term-mode pairing of the independently established lower and upper bounds on the product.
Claim. $6.0 × 10^{-10} < c_{RS} ⋅ φ^{-44} < 6.2 × 10^{-10}$, where $c_{RS} = (1 - φ^{-8})^2$ is the squared washout prefactor.
background
The module derives the order-one prefactor in the baryogenesis formula η_B = c × (algebraic content forced by the integration-gap rung). The prefactor is introduced as c_RS = (1 − φ^{-8})^2, with the squared form encoding independent washout from matter and antimatter sectors at the eight-tick scale in three dimensions. Upstream, eta_B_corrected is defined as the product c_RS ⋅ φ^{-44}, while separate theorems establish its lower bound above 6.0 × 10^{-10} and upper bound below 6.2 × 10^{-10} via numerical intervals on c_RS and the negative power φ^{-44}.
proof idea
The proof is a term-mode construction that applies the pair constructor directly to eta_B_corrected_lower and eta_B_corrected_upper. These lemmas unfold the definition of eta_B_corrected, invoke the bounds c_RS > 0.956 and c_RS < 0.959 together with the corresponding bounds on φ^{-44}, and use positivity of both factors.
why it matters
This theorem supplies the prediction_band field inside etaBPrefactorCert, which certifies that the observed Planck central value lies inside the RS band. It completes the numerical verification step for the two-sided 8-tick washout model, linking the algebraic forcing chain (T7 eight-tick octave, T8 D = 3) to cosmology. The squared prefactor remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.