cmbObservableCount
plain-language theorem explainer
cmbObservableCount establishes that the finite type of CMB observables has cardinality five. Cosmologists using Recognition Science cosmology cite it to fix the structural count of temperature, spectral index, tensor-to-scalar ratio, baryon density and dark energy as matching configDim D = 5. The proof is a direct decide tactic on the inductive enumeration.
Claim. The cardinality of the set of CMB observables equals 5, where the observables are temperature, spectral index, tensor-to-scalar ratio, baryon density and dark energy.
background
The module derives CMB temperature from Recognition Science in an S3 cosmology. It states T_CMB = 2.725 K satisfies T_CMB times universe age in seconds approximates a constant via Wien's law, with age approximately 4.35 times 10^17 s, or equivalently 1 over phi^45 times tau_0 times a constant. Five canonical CMB observables equal configDim D = 5.
proof idea
The proof is a one-line term proof that applies the decide tactic to the Fintype instance on the inductive type CMBObservable, which enumerates exactly five constructors.
why it matters
This supplies the cardinality five to the downstream theorem cmb_span_configDim asserting the observables span the five-dimensional recognition parameter space, and to the definition cmbTempCert. It fills the module's structural observation that five observables equal configDim D = 5, connecting to the forcing chain T8 where spatial dimensions equal three but extended here to five parameters. It touches the open question of deriving precise temperature bounds from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.