module module moderate

`IndisputableMonolith.Physics.CMBTemperature`

This module defines constants and derived quantities for cosmic microwave background temperature in the Recognition Science framework, including hydrogen ionization energy, Boltzmann constant, recombination temperature, redshift, and an approximation to the observed 2.725 K value. Researchers modeling early-universe thermodynamics via J-cost would reference these definitions. The module consists of definitions and positivity statements built directly on the imported JcostCore.

claimDefines $E_i = 13.6$ eV (hydrogen ionization energy), $k_B$ in eV/K, recombination temperature $T_r$ in K, recombination redshift $z_r$, CMB temperature $T_{CMB}$, and the approximation $T_{CMB} = 2.725$ K with associated positivity statements.

background

The module imports Mathlib and IndisputableMonolith.Cost.JcostCore. JcostCore supplies the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) together with the J-cost functional equation and phi-ladder structures. The module opens with the hydrogen ionization energy in eV and proceeds through eta, recombination temperature, and redshift to the final CMB temperature value.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the temperature scale for the cosmic microwave background epoch within Recognition Science. It feeds calculations that connect the J-cost core to observable cosmology and indirectly supports the alpha band and eight-tick octave through the shared phi-ladder machinery.

scope and limits

Does not derive CMB temperature from the T0-T8 forcing chain.
Does not compute the full CMB power spectrum.
Does not incorporate observational error bars beyond positivity.
Does not interface with external data sets.

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