DarkEnergyModel
plain-language theorem explainer
The inductive definition enumerates five canonical dark energy models (ΛCDM, wCDM, w0wa_CPL, quintessence, phantom) for w(z) on the φ-ladder. Recognition Science cosmologists cite it to fix the discrete model space when bounding deviations in the BIT kernel. It is realized directly as an inductive type deriving Fintype for immediate cardinality theorems.
Claim. Let $M$ be the inductive type whose five constructors are the models ΛCDM ($w=-1$), constant-$w$ CDM, $w_0w_a$ CPL, quintessence, and phantom. Then $M$ carries decidable equality and has cardinality 5.
background
The module treats $w(z)$ on the φ-ladder, where adjacent-redshift corrections are of order φ^{-n}. Five canonical models are fixed: ΛCDM with $w=-1$, wCDM with constant $w$, w0wa_CPL, quintessence, and phantom. The BIT kernel is defined as $w_{BIT}(z)=-1+δ$ with $δ≤1/φ^5≈0.09$ (MODULE_DOC). This inductive type is the depth-specific enumeration; the upstream result in the parent module uses a different list (cosmologicalConstant, quintessence, phantom, quintom, holographic) and is not referenced here.
proof idea
The declaration is the inductive definition itself, introducing the five constructors and deriving DecidableEq, Repr, BEq, Fintype in one step. No tactics or lemmas are applied; the Fintype instance is generated automatically to support downstream cardinality statements.
why it matters
The definition supplies the model space for DarkEnergyEoSDepthCert, which asserts Fintype.card DarkEnergyModel=5 together with φ^5=5φ+3 and 0<deltaBound<0.1. It realizes the configDim D=5 count required by the Recognition framework for the dark-energy sector and links directly to the φ-ladder bounds on δ. It closes the depth-specific scaffolding for equation-of-state calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.