pith. machine review for the scientific record. sign in
def definition def or abbrev high

c_RS

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 106def c_RS : ℝ := correctionFactor ^ 2

proof body

Definition body.

 107

used by (28)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.