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

rs_eta

show as:
view Lean formalization →

The declaration supplies the Recognition Science baryon-to-photon ratio as the constant 6.1 times 10 to the minus 10, obtained from RS baryogenesis. Cosmologists modeling recombination or the cosmic microwave background would cite this value when inserting RS-derived inputs into the Saha equation. The entry is a bare numerical definition with no lemmas or reduction steps.

claimThe baryon-to-photon ratio equals $6.1 times 10^{-10}$.

background

The CMB Temperature module derives the present-day temperature from the recombination epoch using the Saha equation with the RS baryon-to-photon ratio. Recombination occurs near 3000 K when the ionization fraction reaches 50 percent, and the module states that the CMB temperature follows from T zero equals T star over one plus z star with z star near 1100. Upstream results include the dimensionless bridge ratio K defined as the square root of phi from the Constants module, which supports balance conditions in the framework.

proof idea

This is a direct definition that assigns the numerical value 6.1e-10 without invoking any lemmas or reduction steps.

why it matters in Recognition Science

The definition provides the RS-derived baryon-to-photon ratio required for the recombination temperature calculation that yields the CMB temperature of 2.725 K. It is referenced across the diagonal and off-diagonal components in the Metric Unification module. This constant closes the input from RS baryogenesis into the T0-T8 chain for deriving spatial dimensions and constants.

scope and limits

formal statement (Lean)

  34def rs_eta : ℝ := 6.1e-10

proof body

Definition body.

  35
  36/-! ## Recombination Temperature -/
  37
  38/-- **RECOMBINATION TEMPERATURE** from Saha equation.
  39    At x_e = 0.5 (50% ionization), the Saha equation gives:
  40    k_B T* ≈ E_ion / ln(η⁻¹ × factor) ≈ 0.3 eV ≈ 3500 K
  41
  42    More precisely, T* ≈ 3000 K (accounting for detailed balance). -/

used by (8)

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

depends on (11)

Lean names referenced from this declaration's body.