PerturbationType
plain-language theorem explainer
The inductive definition enumerates the five cosmological perturbation modes scalar, vector, tensor, isocurvature, and entropy. Modelers of structure formation in Recognition Science cosmology cite it to fix the configuration dimension at five when counting degrees of freedom excited at the RS inflation threshold. The declaration is a direct enumeration that derives Fintype to support immediate cardinality computation.
Claim. Let $P$ be the inductive type whose constructors are the scalar, vector, tensor, isocurvature, and entropy modes. The type carries decidable equality, representation, Boolean equality, and finite-type instances.
background
The module treats cosmological perturbations as seeds of structure formation within the Recognition Science framework. Five canonical types are identified with the configuration dimension $D=5$, excited by the five recognition degrees of freedom at the RS inflation threshold where the primordial spectrum satisfies $P(k)propto k^{n_s-1}$ for $n_s$ in (0.95,0.96). Upstream entropy definitions equate entropy to total defect count in the initial-condition setting, to $k_B(ln Z + beta avg E)$ in the partition-function setting, and to $beta avg E + k ln Z$ in the Boltzmann setting; these supply the thermodynamic content for the entropy mode.
proof idea
The declaration is a direct inductive definition listing the five constructors and deriving the four type-class instances in one line. No separate proof body or tactic steps are present; Fintype is obtained automatically from the finite enumeration.
why it matters
The definition supplies the five types required by the downstream structure CosmoPerturbCert (which records Fintype.card = 5) and by the theorem perturbationTypeCount (proved by decide). It implements the module claim that five recognition degrees of freedom are active at the RS inflation threshold, closing the local step that sets configDim = 5 while the forcing chain fixes spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.