c_RS_expanded
plain-language theorem explainer
The equality equates the RS baryogenesis prefactor to (1 - φ^{-8})^2 by direct unfolding of its definition. Cosmologists bounding the baryon asymmetry η_B in Recognition Science cite this to place c_RS inside (0.956, 0.959). The proof is a one-line wrapper that unfolds c_RS and correctionFactor.
Claim. Let c_{RS} be the two-sided 8-tick washout prefactor. Then c_{RS} = (1 - φ^{-8})^2, where the single-tick correction factor is 1 - φ^{-8}.
background
In the η_B prefactor module the two-sided 8-tick washout prefactor c_RS is defined to encode suppression of matter and antimatter sectors, each carrying one integration-gap rung of fermionic degrees of freedom and washed out at rate φ^{-8} per fundamental tick at D = 3. The single-tick correction factor is introduced as correctionFactor := 1 - φ^{-8}, so c_RS := correctionFactor^2. The module states that this squared form is the structural derivation of the order-one prefactor in η_B = c × (algebraic content forced by integration-gap rung). Upstream definitions include the leading-log c_RS = -log φ / 2 from BlackHoleEntropyFromLedger and the native-unit speed c_RS = 1 from PropagationSpeed.
proof idea
The proof is a one-line wrapper that unfolds the definitions of c_RS and correctionFactor.
why it matters
This expanded equality is the reference form used by the bounding theorems c_RS_lower, c_RS_upper and c_RS_lt_one, which together certify the prefactor band inside etaBPrefactorCert. It supplies the structural step that links the eight-tick octave (T7) and D = 3 from the unified forcing chain to the predicted η_B interval (6.0 × 10^{-10}, 6.2 × 10^{-10}). The module notes that the squared interpretive form remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.