darkEnergyEoSDepthCert
plain-language theorem explainer
The declaration constructs a certificate DarkEnergyEoSDepthCert that packages the count of five dark energy models, the identity phi^5 equals 5 phi plus 3, and the strict bounds 0 less than deltaBound less than 0.1. Cosmologists working inside the Recognition Science framework cite it to certify the equation-of-state depth on the phi-ladder for the BIT kernel. The definition is a direct structure constructor that wires each field to its supporting theorem.
Claim. The certificate asserts that the cardinality of the type of DarkEnergyModel equals 5, that $phi^5 = 5 phi + 3$, that $0 < deltaBound$ where $deltaBound = 1/phi^5$, and that $deltaBound < 0.1$.
background
The module treats the dark energy equation of state at S3 depth, with w(z) corrections of order phi to the minus n on the phi-ladder. Five canonical models are enumerated: LambdaCDM with w equals minus 1, constant-w wCDM, the CPL w0wa parametrization, quintessence, and phantom. The canonical BIT kernel is w_BIT(z) equals minus 1 plus delta with delta bounded by 1 over phi^5 approximately 0.09. The structure DarkEnergyEoSDepthCert collects the model count, the phi^5 Fibonacci identity, and the positivity and smallness of deltaBound. Upstream theorems establish phi^5 equals 5 phi plus 3 by successive nlinarith reductions from phi squared equals phi plus 1, and bound deltaBound using phi greater than 1.61.
proof idea
The definition constructs an instance of the DarkEnergyEoSDepthCert structure by direct field assignment: five_models receives the result of darkEnergyModel_count, phi5_fibonacci receives phi5_eq, delta_pos receives deltaBound_pos, and delta_bounded receives deltaBound_small. Each assignment is a one-line reference to the theorem that proves the corresponding proposition.
why it matters
This definition supplies the verified certificate for dark energy equation-of-state depth inside the Recognition Science cosmology pipeline. It closes the local verification of the five-model count and the phi^5 equals 5 phi plus 3 identity that recurs in the Hubble tension, inflaton potential, and OmegaLambda modules. Within the framework it supports the BIT kernel bound delta less than or equal to 1 over phi^5 for w_BIT(z). No downstream uses are recorded, leaving open its integration into full cosmological simulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.