kB_eV_per_K
The definition supplies the Boltzmann constant k_B in electronvolt per kelvin units as the fixed numerical value 8.617 × 10^{-5}. Researchers computing recombination energies or the present CMB temperature within the Recognition Science derivation of T₀ = 2.725 K would reference it directly. The declaration consists of a bare constant assignment with no lemmas or reduction steps.
claimThe Boltzmann constant expressed in electronvolt per kelvin units equals $k_B = 8.617 × 10^{-5}$.
background
The module derives the CMB blackbody temperature T₀ = 2.725 K from the recombination epoch redshift z* ≈ 1100 together with the recombination temperature T* ≈ 3000 K obtained via the Saha equation at the RS baryon-to-photon ratio η ≈ 6.1 × 10^{-10}. This definition supplies the conversion factor that turns temperatures into energies measured in eV, enabling direct comparison with the observed spectrum and the first acoustic peak at ℓ ≈ 220. The upstream theorem from PrimitiveDistinction establishes the seven axioms that reduce to four structural conditions plus three definitional facts, providing the logical foundation for all subsequent physical constants in the framework.
proof idea
The declaration is a direct numerical assignment of the constant 8.617e-5. No lemmas are invoked and no tactics are executed; the value is introduced as a primitive for downstream energy calculations.
why it matters in Recognition Science
The definition feeds the recombination_energy_approx_eV result that bounds k_B T* between 0.25 eV and 0.27 eV, confirming the recombination scale before the redshift factor produces the present-day temperature. It thereby closes one link in the chain from RS baryogenesis through the Saha equation to the observed CMB temperature, as outlined in the module's reference to RS_CMB_Temperature.tex.
scope and limits
- Does not derive the numerical value from the J-cost function or the Recognition Composition Law.
- Does not include unit conversions beyond the stated eV/K assignment.
- Does not address temperature dependence or quantum corrections to the constant.
- Does not connect the value to the phi-ladder or the eight-tick octave structure.
Lean usage
theorem example_use : 0.25 < kB_eV_per_K * 3000 ∧ kB_eV_per_K * 3000 < 0.27 := by constructor <;> norm_num [kB_eV_per_K]formal statement (Lean)
31def kB_eV_per_K : ℝ := 8.617e-5
proof body
Definition body.
32
33/-- **RS baryon-to-photon ratio**: η ≈ 6.1 × 10⁻¹⁰ from RS baryogenesis. -/