deltaBound_pos
plain-language theorem explainer
The declaration proves that the dark energy depth bound is positive. Cosmologists certifying phi-ladder models would cite it to confirm the BIT kernel bound. The proof unfolds the definition and invokes positivity of division and powers.
Claim. $0 < 1/phi^5$
background
In this cosmology module the equation of state depth delta is bounded above by the quantity defined as 1 over phi to the fifth. This supports w(z) models with corrections of order phi to the minus n across five canonical cases including LambdaCDM. The upstream definition states that the bound equals 1 over phi to the fifth using phi to the fifth equals five phi plus three.
proof idea
Unfold the definition of the bound then apply the exact tactic with div_pos one_pos (pow_pos phi_pos 5) to conclude positivity.
why it matters
The positivity feeds directly into the dark energy equation of state depth certificate that certifies the five models, the phi5 relation, and the bounded delta. It supports the canonical BIT kernel w_BIT(z) = -1 + delta with delta at most 1 over phi to the fifth, linking to the phi-ladder and Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.