darkEnergyModelCount
plain-language theorem explainer
The finite enumeration of dark energy models in the Recognition Science cosmology module contains exactly five entries. Researchers bounding the BIT equation of state deviation from a cosmological constant would cite this cardinality when constructing the certification object. The proof is a one-line decision procedure that exhausts the Fintype instance on the inductive type.
Claim. The finite set of dark energy models, consisting of the cosmological constant, quintessence, phantom, quintom, and holographic cases, has cardinality five: $|M_{DE}|=5$.
background
The module establishes the dark energy equation of state within S3 Cosmology Depth. Its opening documentation states that the BIT dark-energy equation of state deviates from w = -1, with the RS prediction w_0 ∈ (-1 - J(φ), -1) ≈ (-1.13, -1) and the bound δw_0 ≤ J(φ) ≈ 0.118 drawn from RS_Omega_Lambda_From_BIT.tex. The local inductive type enumerates precisely five models and derives Fintype, DecidableEq, and Repr instances for direct cardinality computation.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on Fintype.card applied to the inductive type. Lean reduces the five constructors directly to the numeral 5 without further lemmas.
why it matters
This cardinality is referenced by the downstream darkEnergyEoSCert definition to populate the five_models field and establish the baseline_w equality. It supplies the model count required for the module's stated goal of proving the J(φ)-band bound on w_0, consistent with the Recognition Composition Law and the phi-ladder structure used elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.