DarkEnergyEoSCert
plain-language theorem explainer
DarkEnergyEoSCert records that exactly five dark energy models exist and that the baseline equation-of-state parameter equals -1. Cosmologists using the Recognition Science BIT framework cite the structure to fix the cosmological-constant starting point before applying J(φ) corrections. The declaration is introduced as a plain structure definition whose fields are filled by the inductive enumeration of the models and the constant definition of wLambda.
Claim. A structure certifying that the set of dark energy models has cardinality five and that the baseline equation-of-state parameter satisfies $w = -1$.
background
The module treats dark energy through an inductive type whose five constructors are the cosmological constant, quintessence, phantom, quintom and holographic models. The constant wLambda is defined to be -1, serving as the reference value before BIT corrections are applied. Module documentation states that the BIT correction to w lies in the canonical J(φ) band and that the RS prediction places w_0 in the interval (-1 - J(φ), -1).
proof idea
The structure is introduced directly by naming the two fields; the first field is discharged by the Fintype instance on the inductive type of models, and the second field is discharged by the definitional equality of wLambda.
why it matters
The structure supplies the type for the concrete instance darkEnergyEoSCert that appears later in the same module. It therefore anchors the cosmology section to the RS prediction that the BIT correction satisfies |δw| ≤ J(φ) and connects the five-model enumeration to the broader forcing-chain results on constants and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.