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

eta

show as:
view Lean formalization →

The baryon-to-photon ratio is defined as the constant 6.1 × 10^{-10}. Cosmologists computing Big Bang nucleosynthesis yields cite this value to fix the neutron-to-proton ratio and subsequent light-element formation. The declaration is a direct numerical binding with no further reduction steps.

claimThe baryon-to-photon ratio is the real number satisfying $η = 6.1 × 10^{-10}$.

background

The module COS-012 derives light-element abundances from Recognition Science principles during the first minutes after the Big Bang. Abundances of deuterium, helium-4, and lithium-7 depend on the baryon-to-photon ratio η together with neutrino species count and nuclear rates; the module states that η ~ 10^{-10} follows from the golden ratio φ and the eight-tick structure. Upstream definitions supply the shifted cost H(x) = J(x) + 1 that turns the Recognition Composition Law into d'Alembert's equation, and the Chain structure that sequences recognition steps.

proof idea

The declaration is a direct numerical assignment of the real number 6.1e-10. No lemmas or tactics are invoked; the body simply binds the constant.

why it matters in Recognition Science

This definition supplies the baryon-to-photon ratio required by the BBN reaction chain and feeds sibling calculations of helium mass fraction, deuterium ratio, and lithium abundance. It realizes the RS mechanism stated in the module documentation, where η ~ 10^{-10} is obtained from φ via the T5 J-uniqueness and T7 eight-tick octave. The constant therefore closes the link from the forcing chain (T0-T8) to observable cosmological yields.

scope and limits

formal statement (Lean)

  60noncomputable def eta : ℝ := 6.1e-10

proof body

Definition body.

  61
  62/-! ## The BBN Chain -/
  63
  64/-- The nuclear reaction chain in BBN:
  65
  66    1. n + p → D + γ (deuterium formation)
  67    2. D + D → ³He + n (and other branches)
  68    3. D + D → ³H + p
  69    4. ³He + n → ³H + p
  70    5. ³H + D → ⁴He + n
  71    6. ³He + D → ⁴He + p
  72    7. ⁴He + ³H → ⁷Li + γ
  73
  74    Most neutrons end up in ⁴He! -/

used by (21)

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

depends on (7)

Lean names referenced from this declaration's body.