darkEnergyEoSCert
plain-language theorem explainer
The declaration constructs a certification that exactly five dark energy models exist and that the baseline equation-of-state parameter equals negative one. Cosmologists working in the Recognition Science framework would cite it when establishing the model count prior to deriving the J(φ)-bounded deviation of w_0 from -1. The construction is a direct structure instance that pulls the model cardinality from a decidable theorem and obtains the baseline equality by reflexivity.
Claim. The structure certifying that the finite cardinality of the set of dark energy models equals five and that the baseline equation-of-state parameter satisfies $w_0 = -1$.
background
The module treats the dark energy equation of state in S3 cosmology depth. Recognition Science predicts that the BIT correction produces a deviation from the cosmological-constant value w = -1, with w_0 lying in the interval (-1 - J(φ), -1) where J(φ) ≈ 0.118. The upstream theorem darkEnergyModelCount establishes by decision procedure that the finite type of dark energy models has cardinality exactly five. The referenced structure DarkEnergyEoSCert packages this cardinality together with the baseline equality wLambda = -1.
proof idea
The definition is a one-line structure constructor. It supplies the five_models field directly from the theorem darkEnergyModelCount and obtains the baseline_w field by reflexivity on the equality wLambda = -1.
why it matters
This definition supplies the concrete instance required by the DarkEnergyEoSCert structure, completing the model-enumeration step that precedes bounds on the equation-of-state deviation. It anchors the RS prediction |w_0 + 1| ≤ J(φ) drawn from the forcing chain and the Recognition Composition Law. No downstream results are recorded, leaving open its use in larger derivations of Omega_Lambda from the BIT kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.