cmbTempHigh
plain-language theorem explainer
The declaration supplies the numerical constant 2.8 as the high-end value for cosmic microwave background temperature in the Recognition Science S3 cosmology model. Modelers working with the five canonical CMB observables would cite the bound when checking the span of the recognition parameter space against data. The definition is a direct constant assignment with no reduction steps or external lemmas.
Claim. Define the high CMB temperature bound by the real number $2.8$ (kelvin).
background
The module sets the observed CMB temperature at 2.725 K and notes the structural relation T_CMB times universe age in seconds is approximately constant, with age near 4.35 times 10^17 s. It further states that T_CMB is approximately 1 over (phi to the 45 times tau_0 times a constant) and that the five canonical observables (temperature, spectral index, tensor-to-scalar ratio, baryon density, dark energy) span a five-dimensional recognition parameter space. The module imports only Mathlib and the Constants module; no upstream lemmas are referenced.
proof idea
Direct definition that assigns the literal real number 2.8.
why it matters
The constant anchors the upper edge of the CMB temperature range required to close the five-dimensional observable span (configDim D = 5) asserted in the module documentation. It supplies the concrete numerical value needed to compare the RS structural prediction against the observed 2.725 K and to support later span calculations such as cmb_span_configDim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.