perturbationTypeCount
plain-language theorem explainer
The theorem establishes that the finite set of cosmological perturbation types contains exactly five elements. Modelers of structure formation in Recognition Science cosmology cite this count when equating perturbations to the five recognition degrees of freedom at the inflation threshold. The proof is a one-line decision procedure that computes the cardinality directly from the inductive definition of the type.
Claim. The finite set of cosmological perturbation types has cardinality five: $|$PerturbationType$| = 5$, where the types are the scalar, vector, tensor, isocurvature, and entropy modes.
background
The module defines five canonical cosmological perturbation types that seed structure formation and correspond to configuration dimension D = 5. These types are excited by the five recognition degrees of freedom at the RS inflation threshold, with the primordial power spectrum satisfying P(k) ∝ k^(n_s-1) for n_s in (0.95, 0.96). The upstream inductive definition lists exactly the constructors scalar, vector, tensor, isocurvature, entropy and derives Fintype, Repr, and DecidableEq.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive type derives Fintype, making its cardinality decidable and equal to the number of listed constructors.
why it matters
This supplies the five_types field inside the cosmoPerturbCert definition, confirming that the perturbation count matches the five recognition degrees of freedom. It fills the explicit step in the module that sets the count equal to configDim D = 5. In the Recognition Science framework the result aligns with the forcing chain that produces D = 3 spatial dimensions while isolating the five perturbation modes at the inflation threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.