deltaBound_small
plain-language theorem explainer
The theorem shows that the dark energy deviation bound 1/φ^5 is strictly smaller than 0.1. Model builders in Recognition Science cosmology cite it when confirming that the BIT kernel correction remains under ten percent. The proof substitutes the Fibonacci relation φ^5 = 5φ + 3, applies the lower bound φ > 1.61, and finishes with linear arithmetic.
Claim. Let δ := 1/φ^5. Then δ < 0.1.
background
The module examines the equation of state w(z) on the φ-ladder for dark energy models. The canonical BIT kernel takes the form w_BIT(z) = -1 + δ with the deviation δ bounded above by 1/φ^5. The definition of deltaBound is exactly this quantity 1/φ^5. The supporting identity φ^5 = 5φ + 3 is proved in phi5_eq by successive nlinarith steps from the quadratic equation for φ. The lower bound φ > 1.61 is given by the lemma phi_gt_onePointSixOne.
proof idea
The tactic proof first unfolds deltaBound to expose 1/φ^5. It then rewrites using the equality φ^5 = 5φ + 3 supplied by phi5_eq. The lower bound φ > 1.61 is introduced from phi_gt_onePointSixOne. Positivity and a concrete lower estimate for the denominator 5φ + 3 are established by linarith. The inequality is rewritten via div_lt_iff₀ and closed by nlinarith.
why it matters
This bound is assembled into the certification object darkEnergyEoSDepthCert together with the model count, the phi5 identity, and positivity. It places the Recognition Science dark-energy deviation inside the interval (0, 0.1), consistent with the φ-ladder mass formula and the alpha band constraints. The result closes one link in the cosmology pipeline without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.