c_RS_expanded
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not derive the squared form from Boltzmann equations.
- Does not compute the numerical bounds on c_RS.
- Does not address the integration-gap rung content of the full η_B formula.
- Does not connect to the leading-log c_RS from black-hole entropy.
Lean usage
rw [c_RS_expanded]formal statement (Lean)
108theorem c_RS_expanded : c_RS = (1 - phi ^ (-8 : ℤ)) ^ 2 := by
proof body
One-line wrapper that applies unfold.
109 unfold c_RS correctionFactor
110