CMBObservable
plain-language theorem explainer
The inductive type enumerates the five canonical CMB observables in Recognition Science cosmology. A researcher deriving T_CMB bounds from the phi-ladder would cite it to fix the dimension of the observable space at five. It is introduced by a direct inductive definition that automatically derives decidable equality, representation, and finite-type structure.
Claim. Let $O$ denote the set of CMB observables. Then $O$ consists of the five elements temperature, spectral index, tensor-to-scalar ratio, baryon density, and dark-energy density.
background
The module states that five canonical CMB observables (temperature, spectral index, tensor/scalar, baryon density, dark energy) equal configDim D = 5, with T_CMB = 2.725 K linked to the age of the universe via Wien's law and an approximate relation T_CMB ≈ 1 / (φ^45 × τ₀ × constant). Upstream, spectralIndex is defined in the inflation module as 1 - 6ε + 2η ≈ 0.96 and in the cosmic-ray module as 1 + φ. Temperature is defined in the Boltzmann module as the inverse of the Lagrange multiplier β, satisfying the thermodynamic relation dE/dS = T.
proof idea
Direct inductive definition with five explicit constructors. The deriving clauses for DecidableEq, Repr, BEq, and Fintype are supplied by the Lean type-class mechanism with no lemmas or tactics required.
why it matters
This definition supplies the five observables whose cardinality is established by the downstream theorem cmbObservableCount and packaged into the structure CMBTempCert. It realizes the module claim that the five observables span configDim D = 5, extending the Recognition Science forcing chain (T8) from D = 3 spatial dimensions to the observable parameter space and supporting the structural temperature relation without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.