module module moderate

`IndisputableMonolith.Physics.CMBTemperature`

This module defines constants and derived quantities for the cosmic microwave background temperature in the Recognition Science framework. It supplies the hydrogen ionization energy in eV, Boltzmann constant in eV/K, recombination temperature and redshift, plus the approximate CMB temperature of 2.725 K. The definitions rest on the imported JcostCore for the underlying J-function. The module contains only definitions and positivity assertions with no theorems.

claimThe module defines the hydrogen ionization energy $E_ion$ in eV, Boltzmann constant $k_B$ in eV/K, recombination temperature $T_rec$ in K, recombination redshift $z_rec$, and CMB temperature $T_CMB approx 2.725$ K.

background

Recognition Science derives all physics from the J-cost function in the imported JcostCore module, satisfying the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) with J(x) = (x + x^{-1})/2 - 1. This module introduces concrete constants in the physics domain: hydrogen ionization energy, k_B scaled to eV per K, recombination temperature in Kelvin, and redshift. These quantities support mapping the abstract phi-ladder and forcing chain (T0-T8) onto cosmological observables such as the present-day CMB temperature.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the approximate CMB temperature value for use in Recognition Science cosmology derivations. It connects the J-cost framework to the observed 2.725 K background, providing a concrete anchor point that can feed into comparisons with the eight-tick octave and D=3 spatial dimensions from the unified forcing chain.

scope and limits

Does not derive the temperature from the full expansion history or Friedmann equations.
Does not include error bars or sensitivity to phi-ladder rung assignments.
Does not address the Berry creation threshold or Z_cf in the recombination context.
Does not prove exact numerical agreement beyond the stated approximation.

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