cmbTempHigh
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not derive 2.8 from the phi-ladder or any forcing-chain step.
- Does not state units or conversion factors explicitly.
- Does not connect the value to specific RS constants such as phi or tau_0.
- Does not provide an error interval or observational uncertainty.
formal statement (Lean)
34def cmbTempHigh : ℝ := 2.8
proof body
Definition body.
35
36/-- The 5 CMB observables span the 5-dimensional recognition parameter space. -/