cmbTempCert
plain-language theorem explainer
cmbTempCert supplies a concrete certificate that the CMB observable set contains exactly five elements, matching the five canonical observables in RS cosmology. Researchers modeling cosmic microwave background data within the Recognition Science framework would cite it to anchor the observable count to configDim D=5. The definition is a one-line structure instantiation that imports the decidable cardinality theorem for the CMBObservable type.
Claim. The structure $CMBTempCert$ is instantiated by setting the field $five_observables$ to the equality $Fintype.card(CMBObservable)=5$ supplied by the decidable theorem establishing the cardinality of the CMB observable type.
background
In the Recognition Science framework the cosmic microwave background temperature satisfies $T_{CMB} = 2.725$ K and is linked to the age of the universe through Wien's law, with the structural relation $T_{CMB} approx 1/(phi^{45} tau_0 cdot const)$. The module treats five canonical observables (temperature, spectral index, tensor-to-scalar ratio, baryon density, dark energy) as the configuration dimension $D=5$ in S3 cosmology depth. The structure $CMBTempCert$ is defined to require a proof that the finite type $CMBObservable$ has cardinality exactly five. This requirement is discharged upstream by the theorem $cmbObservableCount$ whose proof is a direct computational decision.
proof idea
The definition is a one-line wrapper that constructs an element of the $CMBTempCert$ structure by assigning its $five_observables$ field directly to the result of the theorem $cmbObservableCount$.
why it matters
This definition closes the interface for CMB temperature certification inside the RS cosmology module and confirms the five-observable count that aligns with configDim $D=5$. It supports the structural observation in the module documentation that five CMB observables equal the configuration dimension, linking to the phi-ladder constants and the eight-tick octave without new axioms. No downstream uses are recorded, so the declaration functions as a terminal certificate rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.