theorem proved term proof

`recombination_energy_approx_eV`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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

proof body

Term-mode proof.

  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. -/

depends on (3)

Lean names referenced from this declaration's body.

and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
kB_eV_per_K in IndisputableMonolith.Physics.CMBTemperature decl_use
recombination_temperature_K in IndisputableMonolith.Physics.CMBTemperature decl_use