DarkEnergyEoSDepthCert
plain-language theorem explainer
DarkEnergyEoSDepthCert packages the cardinality of the five dark energy models, the identity phi^5 equals 5 phi plus 3, and the positivity and upper bound on deltaBound. Recognition Science cosmologists cite it to fix the deviation scale of the BIT kernel at 1 over phi^5. The structure is assembled directly from sibling definitions and the upstream phi5_fibonacci theorem with no additional reasoning steps.
Claim. A structure certifying that the inductive type of dark energy models has cardinality five, that $phi^5 = 5 phi + 3$, that $0 < deltaBound$, and that $deltaBound < 0.1$, where $deltaBound := 1/phi^5$.
background
The module treats the dark energy equation of state w(z) on the phi-ladder, with adjacent-redshift ratio corrections of order phi to negative powers. It lists five canonical models via the inductive DarkEnergyModel: lambdaCDM (w equals -1), wCDM (constant w), w0wa_CPL, quintessence, and phantom. The BIT kernel is w_BIT(z) equals -1 plus delta with delta at most 1 over phi^5 approximately 0.09. Upstream, the phi5_fibonacci theorem proves phi^5 equals 5 phi plus 3 by nlinarith from phi_sq_eq, while deltaBound is defined as 1 over phi to the fifth.
proof idea
Direct structure definition that bundles four fields taken from sibling declarations: the Fintype.card of DarkEnergyModel, the phi5_fibonacci identity, and the positivity and smallness facts on deltaBound. No tactics or reductions occur; the structure merely packages already-established facts.
why it matters
The certificate supplies the concrete data required by the downstream darkEnergyEoSDepthCert definition that constructs an instance of the structure. It anchors the five-model count and the phi^5 relation that sets the deviation scale in the Recognition Science cosmology treatment. The construction aligns with the phi-ladder and the T5 J-uniqueness step by fixing the bound at phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.