deltaBound
plain-language theorem explainer
deltaBound sets the deviation scale for the BIT kernel dark energy equation of state at 1 over phi to the fifth. Cosmologists parametrizing w(z) corrections on the phi-ladder cite it to bound S3 model depth across the five canonical cases. The definition is a direct real-number assignment that invokes the algebraic identity phi^5 equals five phi plus three.
Claim. $δ = ϕ^{-5}$, where $ϕ$ is the golden ratio satisfying $ϕ^5 = 5ϕ + 3$.
background
The module treats w(z) on the phi-ladder as adjacent-redshift ratio corrections of order phi to the minus n. Five canonical models are enumerated: LambdaCDM with w equals minus one, wCDM, w0wa CPL, quintessence, and phantom. The BIT kernel is introduced as w_BIT(z) equals minus one plus delta, with delta bounded above by 1 over phi to the fifth.
proof idea
One-line definition that directly assigns the real value one divided by phi raised to the fifth power.
why it matters
The bound supplies the concrete numerical depth required by the DarkEnergyEoSDepthCert structure, which also records the five-model count and the phi^5 Fibonacci identity. It anchors the S3 depth claim inside the Recognition Science cosmology by linking the deviation scale to the phi-ladder and the T6 self-similar fixed point. The downstream deltaBound_pos and deltaBound_small theorems then discharge the positivity and less-than-0.1 checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.