darkEnergyModel_count
plain-language theorem explainer
The declaration fixes the enumeration of dark energy models at exactly five elements inside the phi-ladder cosmology module. Workers certifying equation-of-state depth on the Recognition Science framework cite this count to anchor the configuration dimension. The proof is a single decision tactic that exhausts the derived Fintype instance on the inductive type.
Claim. The finite set of canonical dark energy models has cardinality five: $ |M| = 5 $, where $M$ consists of the models with constant equation of state $w=-1$, constant $w$, CPL parametrization, quintessence, and phantom.
background
The module treats $w(z)$ on the phi-ladder with adjacent-redshift ratio corrections of order phi to negative powers. It enumerates five canonical models: LambdaCDM ($w=-1$), wCDM (constant $w$), w0wa CPL, quintessence, and phantom, setting configDim D equal to five. The upstream inductive definition in the parent DarkEnergyEquationOfState module lists a parallel but distinct set of five models (cosmologicalConstant, quintessence, phantom, quintom, holographic) that supplies the Fintype instance used here.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic evaluates the cardinality directly from the Fintype instance derived for the inductive type with exactly five constructors.
why it matters
The result populates the five_models field of the downstream darkEnergyEoSDepthCert definition, which also incorporates the phi^5 bound on delta and its positivity. It completes the enumeration step required for the depth certificate in the phi-ladder cosmology, consistent with the eight-tick octave and the overall forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.