c_RS
plain-language theorem explainer
c_RS defines the two-sided 8-tick washout prefactor in the baryogenesis formula as the square of the single-tick correction. Cosmologists computing the Recognition Science η_B band cite this to obtain the interval (0.956, 0.959) that contains the Planck 2018 measurement. The construction is a direct algebraic definition that squares the output of correctionFactor.
Claim. $c_{RS} := (1 - φ^{-8})^2$
background
The module derives the order-one prefactor c in the baryogenesis formula η_B = c × (algebraic content forced by integration-gap rung). correctionFactor supplies the single-tick term 1 − φ^{−8}. The module states that matter and antimatter sectors each carry one integration-gap-worth of fermionic degrees of freedom and each is washed out at rate φ^{−8} (one rung per fundamental tick at D = 3); the squared form encodes two independent washout channels. Upstream, correctionFactor is defined as 1 - phi ^ (-8 : ℤ).
proof idea
This declaration is a one-line definition that squares the value of correctionFactor.
why it matters
The definition supplies the prefactor for c_RS_expanded and the bound theorems c_RS_lower, c_RS_upper, c_RS_pos that place the predicted η_B band inside the Planck 2018 interval. It realizes the eight-tick octave washout at D = 3 from the forcing chain. The module notes that 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.