cosmoPerturbCert
plain-language theorem explainer
The declaration supplies a certificate that exactly five perturbation types exist in the RS cosmological model. Researchers modeling structure formation from primordial fluctuations would reference this count when enumerating degrees of freedom. The construction is a direct instantiation of the CosmoPerturbCert structure using the decidable cardinality result for the PerturbationType type.
Claim. Defines the certificate that the number of cosmological perturbation types equals five: $Fintype.card(PerturbationType) = 5$.
background
Cosmological perturbations seed structure formation in the Recognition Science framework. The module enumerates five canonical types (scalar, vector, tensor, isocurvature, entropy) and equates this count to the configuration dimension D = 5. The upstream theorem perturbationTypeCount establishes the cardinality of the PerturbationType enumeration as exactly five via a decidable proof.
proof idea
The definition is a one-line wrapper that constructs the CosmoPerturbCert record by setting the five_types field to the value of the perturbationTypeCount theorem.
why it matters
This definition anchors the cosmological perturbation sector by certifying the five-type count that matches the recognition degrees of freedom at the RS inflation threshold. It supports the module claim that these types excite the primordial power spectrum P(k) ∝ k^(n_s-1) with n_s ∈ (0.95, 0.96). No downstream uses appear yet, but the fact supplies the basic cardinality input for further perturbation analysis in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.