InflationModelsCert
plain-language theorem explainer
The structure certifies that exactly five inflation models exist when the configuration dimension equals five. Cosmologists comparing slow-roll predictions across chaotic quadratic, plateau, hybrid, natural axion-like, and alpha-attractor families would cite the cardinality result. The definition consists of a single field that directly records the Fintype cardinality of the five-constructor inductive type.
Claim. Let $M$ be the inductive type whose constructors are chaoticQuadratic, newInflationPlateau, hybrid, naturalAxionLike, and alphaAttractor. InflationModelsCert is the structure whose sole field asserts that the cardinality of $M$ equals five: $|M|=5$.
background
The module introduces five canonical inflaton-potential families for configDim D=5: the chaotic quadratic potential (m²φ²), the new inflation plateau, the hybrid model, the natural axion-like potential, and the alpha-attractor conformal model. Each family produces distinct slow-roll predictions for the scalar spectral index n_s and the tensor-to-scalar ratio r. The upstream results supply parallel inductive definitions of InflationModel in three sibling cosmology modules, each also enumerating five variants with only minor naming differences.
proof idea
The structure is introduced directly as a definition whose single field records the cardinality of the InflationModel inductive type. The Fintype instance is obtained automatically from the five-constructor inductive declaration; no lemmas or tactics are invoked.
why it matters
This definition supplies the cardinality certificate consumed by the downstream inflationModelsCert construction. It anchors the five-model enumeration required for the configDim=5 case in the Recognition Science cosmology module. The module documentation identifies these five families as the canonical set whose slow-roll predictions are to be compared against observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.