etaBPrefactorCert
plain-language theorem explainer
The declaration certifies that the RS prefactor c_RS equals (1 - φ^{-8})^2 and lies in (0.956, 0.959), while the corrected baryon asymmetry η_B lies in (6.0 × 10^{-10}, 6.2 × 10^{-10}) and contains the Planck 2018 central value. Baryogenesis calculations would cite it to anchor the numerical prediction to the eight-tick washout. The proof is a direct term-mode record construction that assembles the five fields of EtaBPrefactorCert from the supporting bound and expansion lemmas.
Claim. Let $c_{RS} := (1 - φ^{-8})^2$. Then $0 < c_{RS} < 1$, $0.956 < c_{RS} < 0.959$, the corrected baryon asymmetry satisfies $6.0 × 10^{-10} < η_B < 6.2 × 10^{-10}$, and the observed value $6.10 × 10^{-10}$ lies inside that interval.
background
In the η_B prefactor module the order-one prefactor c in the baryogenesis formula η_B = c × (algebraic content forced by integration-gap rung) is identified with c_RS = (1 - φ^{-8})^2. The squared form encodes two independent washout channels for matter and antimatter sectors, each carrying one integration-gap worth of fermionic degrees of freedom and each washed out at rate φ^{-8} (one rung per fundamental tick at D = 3). The module derives φ^8 = 21φ + 13 from the Fibonacci identity and obtains the numerical band c_RS ∈ (0.956, 0.959) together with the predicted η_B band c_RS · φ^{-44} ∈ (6.0 × 10^{-10}, 6.2 × 10^{-10}).
proof idea
The proof is a term-mode record construction for the EtaBPrefactorCert structure. It supplies the prefactor_in_unit field by the pair (c_RS_pos, c_RS_lt_one), the prefactor_band field by (c_RS_lower, c_RS_upper), the expanded field by the equality c_RS_expanded, the prediction_band field by eta_B_corrected_in_observed_band, and the observed_inside field by observed_in_predicted_band.
why it matters
The theorem supplies the master certificate for the two-sided 8-tick washout prefactor inside the cosmology module. It realizes the T7 eight-tick octave and the D = 3 spatial dimensions from the forcing chain by fixing the washout exponent at -8. The module states that the band-level theorem is proved while the interpretive squared form remains hypothesis-grade pending a first-principles Boltzmann-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.