pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS

show as:
view Lean formalization →

The module encodes the cosmic microwave background temperature as a structural band (2.7, 2.8) K that follows from Recognition Science. Cosmologists comparing RS predictions to Planck data would cite the interval when checking consistency with observed blackbody radiation. The module organizes definitions for observables and certificates around the imported time quantum without proofs.

claimThe cosmic microwave background temperature satisfies $T_0 = 2.7255$ K and lies in the structural interval $(2.7, 2.8)$ K.

background

The module imports IndisputableMonolith.Constants, whose sole documented content is the fundamental RS time quantum τ₀ = 1 tick. It introduces sibling declarations CMBObservable, cmbTempLow, cmbTempHigh, CMBTempCert and related count and span functions that together package the temperature band as a certified observable. The local setting is the translation of Recognition Science constants into concrete physical quantities, with the temperature interval presented as a direct structural output rather than a fitted parameter.

proof idea

This is a definition module, no proofs. The structure consists of type declarations for the observable, numeric bounds for the low and high edges of the band, a certification predicate, and a count function that records the number of admissible values inside the interval.

why it matters in Recognition Science

The module supplies the CMB temperature band that Recognition Science must reproduce from its single functional equation and the imported time quantum. It places the interval (2.7, 2.8) K as a fixed structural consequence available for use in any downstream cosmological claim, even though the current graph shows no explicit used_by edges.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)