inflationModelsCert
plain-language theorem explainer
The definition constructs a certificate structure asserting that exactly five canonical inflaton-potential families exist at configuration dimension five. Cosmologists using Recognition Science would cite it to anchor the enumeration of slow-roll models before deriving spectral indices. The construction is a direct one-line wrapper that assigns the decidable cardinality result to the structure field.
Claim. Let $I$ be the finite type of canonical inflaton potentials. The definition yields a certificate $C$ such that the field $C.five_models$ satisfies $|I|=5$.
background
The module treats five canonical inflaton-potential families as the content of configuration dimension five: chaotic inflation ($m^2 phi^2$), new inflation (plateau), hybrid, natural (axion-like), and alpha-attractors (conformal). Each family produces distinct slow-roll predictions for the scalar index and tensor ratio. The certificate structure requires a field proving that the finite type of these models has cardinality five. An upstream theorem establishes this cardinality by direct decision procedure.
proof idea
The definition is a one-line wrapper that directly assigns the result of the cardinality theorem to the five_models field of the certificate structure.
why it matters
This definition certifies the five-model count inside the cosmology module, supplying the discrete enumeration required by the configDim construction. It supports the framework step that ties configuration dimension to the set of viable inflaton families. No parent theorems or downstream uses are recorded, leaving open its insertion into derivations of $n_s$ and $r$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.