CMBObservable
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign numerical values or error bars to any observable.
- Does not derive relations among the observables from the J-cost or Recognition Composition Law.
- Does not connect the observables to the phi-ladder mass formula or Berry creation threshold.
- Does not compute the temperature from first principles inside this declaration.
formal statement (Lean)
26inductive CMBObservable where
27 | temperature | spectralIndex | tensorScalar | baryonDensity | darkEnergy
28 deriving DecidableEq, Repr, BEq, Fintype
29