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

ionization_energy_eV

show as:
view Lean formalization →

The declaration supplies the hydrogen ionization energy value 13.6 eV for use in Saha-equation calculations of recombination temperature within the CMB module. Modelers of the RS-derived T₀ = 2.725 K from z* ≈ 1100 cite it when combining with RS eta. It is introduced by direct numerical assignment with no internal computation or lemma application.

claimThe ionization energy of hydrogen is $13.6$ eV.

background

The CMB Temperature module derives T₀ from the recombination epoch using T* ≈ 3000 K and z* ≈ 1100, with the Saha equation parameterized by RS eta. The ionization energy supplies the threshold scale for hydrogen recombination in that equation. Upstream, K is defined as the dimensionless bridge ratio φ^{1/2} and also appears as the curvature functional K(λ) = λ²/λ_rec² - 1; the scalar constant supplies a uniform field value.

proof idea

The definition is a direct real-number assignment of 13.6. No lemmas or tactics are invoked; it functions as a primitive constant imported from standard atomic physics for use by sibling definitions such as recombination_energy_approx_eV.

why it matters in Recognition Science

This constant anchors the energy scale in the module's derivation of recombination temperature and CMB temperature T₀, directly supporting the key results listed in the module documentation and the paper RS_CMB_Temperature.tex. It supplies the input needed for the Saha equation step that yields T* before the redshift division that produces the observed 2.725 K value.

scope and limits

formal statement (Lean)

  28def ionization_energy_eV : ℝ := 13.6

proof body

Definition body.

  29
  30/-- Boltzmann constant in eV/K. -/

depends on (3)

Lean names referenced from this declaration's body.