inflationModel_count
plain-language theorem explainer
The theorem asserts that the inductive type enumerating five canonical inflaton-potential families under configDim = 5 has cardinality exactly five. Cosmologists working in the Recognition Science setting would cite the count when classifying slow-roll models for comparison against CMB constraints on n_s and r. The proof is a single decision tactic that exhausts the finite inductive type via its derived Fintype instance.
Claim. Let $M$ be the finite type whose elements are the five inflaton-potential families chaoticQuadratic, newInflationPlateau, hybrid, naturalAxionLike and alphaAttractor. Then $|M| = 5$.
background
The module InflationModelsFromConfigDim defines an inductive type InflationModel with five constructors that label distinct slow-roll potentials: chaoticQuadratic for the m²φ² model, newInflationPlateau for plateau potentials, hybrid for hybrid inflation, naturalAxionLike for axion-like natural inflation, and alphaAttractor for conformal alpha-attractor models. The module documentation states that these five families each produce distinct slow-roll predictions for n_s and r when configDim is set to 5. Upstream results supply three independently declared InflationModel types, one each in CosmicInflationFromJCost, the present module, and InflationaryCosmologyFromRS, each carrying five variants with overlapping but differently named constructors.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card InflationModel = 5, using the automatically generated DecidableEq, BEq and Fintype instances for the inductive type.
why it matters
The theorem supplies the cardinality field required by the downstream definition inflationModelsCert, which packages the count into an InflationModelsCert structure. It completes the enumeration step in the A2-depth treatment of inflation models from configDim, supporting the Recognition Science derivation of cosmological structure from the J-cost functional. The result enables direct comparison of the five models' predictions with CMB observables while leaving open the explicit reduction of each family to the underlying Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.