module module moderate

`IndisputableMonolith.Physics.CMBTemperature`

Recognition Science constants and arithmetic for the CMB temperature, built from hydrogen ionization energy, Boltzmann's constant, and an RS efficiency factor. Cosmologists checking the predicted T_CMB against the observed 2.725 K band would cite rs_cmb_temperature and the numerical lemma rs_cmb_approx_2725. The module is definitional arithmetic plus positivity and approximation lemmas.

claimThe module fixes the hydrogen ionization energy $E_{\mathrm{ion}}$ (eV), Boltzmann constant $k_B$ (eV/K), and RS efficiency $\eta$, then defines the recombination temperature $T_{\mathrm{rec}}=E_{\mathrm{ion}}/(k_B\eta)$, recombination redshift $z_{\mathrm{rec}}$, and CMB temperature $T_{\mathrm{CMB}}=T_{\mathrm{rec}}/(1+z_{\mathrm{rec}})$, with positivity lemmas and a numerical claim $T_{\mathrm{CMB}}\approx 2.725\,\mathrm{K}$.

background

In standard cosmology the CMB temperature is the redshifted recombination temperature of hydrogen. Recombination occurs when the thermal energy falls below a fraction of the ionization energy $E_{\mathrm{ion}}\approx 13.6,\mathrm{eV}$; the ratio is set by an efficiency (Saha) factor, written here as the RS parameter $\eta$. The present-day temperature is then $T_{\mathrm{CMB}}=T_{\mathrm{rec}}/(1+z_{\mathrm{rec}})$.

The module sits in the Physics domain and imports only Mathlib plus the J-cost compatibility surface. It does not invoke the forcing chain or the Recognition Composition Law directly; it packages laboratory constants and RS-native dimensionless factors into named Lean values so downstream physics developments can quote a single CMB temperature object.

Sibling definitions include ionization_energy_eV, kB_eV_per_K, rs_eta, the derived recombination_temperature_K and rs_recombination_redshift, and the final cmb_temperature / rs_cmb_temperature pair, together with positivity and the numerical approximation rs_cmb_approx_2725.

proof idea

Definition module: most declarations are bare defs fixing physical constants and composing $T_{\mathrm{rec}}$ and $T_{\mathrm{CMB}}$ by ordinary field arithmetic. Positivity lemmas (recombination_temperature_positive, recombination_redshift_positive, cmb_temperature_positive) are short tactic proofs from positivity of the input constants. The approximation lemma rs_cmb_approx_2725 is a numerical comparison against the conventional 2.725 K value. No deep algebraic identity or forcing-chain step is required.

why it matters in Recognition Science

Gives Recognition Science a single, citable CMB temperature object in kelvin, aligned with the observed $2.725,\mathrm{K}$ band. Downstream physics developments that need a present-day photon temperature (blackbody spectra, photon-baryon ratios, or late-universe thermodynamics) can import this module rather than re-deriving recombination arithmetic. The module does not yet appear in the used-by graph, so it is a leaf physics package rather than a step inside the T0–T8 forcing chain. It sits alongside other RS-native constant packages (c, $\hbar$, G, $\alpha$) as an observational anchor.

scope and limits

Does not derive $\eta$ or $z_{\mathrm{rec}}$ from the forcing chain or J-cost; they are input parameters.
Does not prove agreement with Planck or WMAP error bars beyond the named numerical approximation.
Does not model helium recombination, Silk damping, or full Saha ionization history.
Does not connect $T_{\mathrm{CMB}}$ to the eight-tick octave or $D=3$ spatial forcing.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (22)

def ionization_energy_eV L28
def kB_eV_per_K L31
def rs_eta L34
abbrev recombination_temperature_K L43
theorem recombination_temperature_positive L46
theorem recombination_energy_approx_eV L50
abbrev rs_recombination_redshift L59
theorem recombination_redshift_positive L62
def cmb_temperature L68
theorem cmb_temperature_positive L71
def rs_cmb_temperature L78
theorem rs_cmb_approx_2725 L82
theorem rs_cmb_consistent_with_firas L91
def planck_radiance L98
theorem planck_positive L102
theorem cmb_is_planck_spectrum L111
def first_acoustic_peak_ell L122
def acoustic_peak L125
theorem acoustic_peaks_positive L127
theorem acoustic_peak_positions L133
theorem cmb_temperature_scales_with_redshift L141
theorem cmb_temperature_now L149