DarkEnergyModel
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define explicit redshift functions w(z) for any constructor.
- Does not derive dynamical equations or stability criteria.
- Does not reference or equate to the upstream model list in the sibling module.
- Does not compute numerical values of δ or w.
formal statement (Lean)
20inductive DarkEnergyModel where
21 | lambdaCDM
22 | wCDM
23 | w0wa_CPL
24 | quintessence
25 | phantom
26 deriving DecidableEq, Repr, BEq, Fintype
27