def
definition
rs_eta
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CMBTemperature on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31def kB_eV_per_K : ℝ := 8.617e-5
32
33/-- **RS baryon-to-photon ratio**: η ≈ 6.1 × 10⁻¹⁰ from RS baryogenesis. -/
34def rs_eta : ℝ := 6.1e-10
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). -/
43abbrev recombination_temperature_K : ℝ := 3000 -- Kelvin
44
45/-- Recombination temperature is positive. -/
46theorem recombination_temperature_positive :
47 0 < recombination_temperature_K := by norm_num
48
49/-- In energy units: k_B T* ≈ 0.26 eV. -/
50theorem recombination_energy_approx_eV :
51 0.25 < kB_eV_per_K * recombination_temperature_K ∧
52 kB_eV_per_K * recombination_temperature_K < 0.27 := by
53 constructor <;> norm_num [kB_eV_per_K]
54
55/-! ## Recombination Redshift -/
56
57/-- **RS RECOMBINATION REDSHIFT**: z* ≈ 1100.
58 From Saha equation with RS η and Ω_b h² = 0.022. -/
59abbrev rs_recombination_redshift : ℝ := 1100
60
61/-- Recombination redshift is positive. -/
62theorem recombination_redshift_positive : 0 < rs_recombination_redshift := by norm_num
63
64/-! ## CMB Temperature Formula -/