InflationModel
plain-language theorem explainer
Recognition Science cosmology enumerates five canonical inflation models: Starobinsky, natural, Higgs, chaotic, and axion monodromy. This fixes the model count to match the configuration dimension of five. The inductive definition directly lists the constructors and derives the necessary typeclass instances for equality and finiteness.
Claim. The set of inflation models consists of five elements: Starobinsky inflation, natural inflation, Higgs inflation, chaotic inflation, and axion monodromy inflation.
background
The module presents inflationary cosmology within Recognition Science by listing five models backed by the framework. Starobinsky uses an R squared potential with n_s = 1-2/N and r = 12/N squared at N around 44 or 45; natural inflation employs a cosine potential; Higgs inflation introduces non-minimal coupling xi; chaotic inflation follows a power-law potential; axion monodromy uses a linear potential. The count of five equals configDim D equals five.
proof idea
The declaration is a direct inductive definition with five constructors that automatically derives DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This enumeration supplies the model list required by CosmicInflationCert, which asserts Fintype.card equals 5 together with the reheating condition J(1) = 0. It realizes the framework step that five models correspond to configDim D equals five and supports derivation of inflationary cosmology from the J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.