recombination_energy_approx_eV
plain-language theorem explainer
The declaration bounds the recombination energy scale k_B T^* strictly between 0.25 eV and 0.27 eV. Cosmologists deriving the present-day CMB temperature from the recombination epoch in Recognition Science would cite this interval when converting the Saha-equation temperature to energy units. The proof is a one-line term wrapper that splits the conjunction and normalizes the explicit real definitions of the Boltzmann constant and recombination temperature.
Claim. $0.25 < k_B T^* < 0.27$, where $k_B = 8.617times 10^{-5}$ eV/K is the Boltzmann constant and $T^* = 3000$ K is the recombination temperature obtained from the Saha equation at 50 percent ionization with the RS baryon-to-photon ratio.
background
The module derives the CMB blackbody temperature T_0 = 2.725 K from the recombination epoch via T_0 = T^/(1 + z^) with z^* ≈ 1100. The recombination temperature T^* ≈ 3000 K is obtained from the Saha equation using RS η ≈ 6.1 × 10^{-10}, yielding k_B T^* ≈ 0.3 eV at 50 percent ionization and refined to 3000 K by detailed balance. The Boltzmann constant is supplied as the explicit real kB_eV_per_K := 8.617e-5. Upstream results characterize recombination_temperature_K as the positive real 3000 K and kB_eV_per_K as the conversion factor from Kelvin to electron-volts.
proof idea
The proof is a one-line term-mode wrapper. Constructor splits the conjunction into the two strict inequalities; norm_num then evaluates the product against the numeric definition of kB_eV_per_K, confirming 0.25 < 0.25851 < 0.27.
why it matters
This numerical bound supplies the energy scale for the recombination epoch inside the Recognition Science derivation of the CMB temperature. It directly supports the formula T_0 = T^/(1 + z^) that recovers the observed 2.725 K blackbody spectrum and the first acoustic peak at ℓ ≈ 220. The result closes the conversion step between the Saha-equation temperature and the present-day CMB within the RS framework, consistent with the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.