phi_inv3_lt
plain-language theorem explainer
Establishes that (golden ratio inverse) cubed is strictly less than 0.237. Numerics code chaining successive power bounds on phi inverse cites this result to reach higher exponents. The term proof obtains the linear and quadratic cases from prior theorems then feeds them with the non-negative square into nlinarith.
Claim. $ (φ^{-1})^3 < 0.237 $ where $ φ = (1 + √5)/2 $ denotes the golden ratio.
background
The module develops rigorous decimal bounds on the golden ratio and its negative powers by refining approximations to √5. The Interval structure from Basic is a closed interval with rational endpoints lo ≤ hi. Upstream theorems phi_inv_lt and phi_inv2_lt supply the linear bound φ^{-1} < 0.6186 and the quadratic bound (φ^{-1})^2 < 0.383, both obtained by linarith or nlinarith on the algebraic definition of phi.
proof idea
The term proof first retrieves the linear bound via phi_inv_lt and the quadratic bound via phi_inv2_lt. It asserts positivity of φ^{-1} by inv_pos.mpr goldenRatio_pos then applies nlinarith to the non-negative square term to conclude the cubic inequality.
why it matters
This bound is invoked by phi_inv3_in_interval_proven to verify containment in a proven interval and by phi_inv5_lt to reach the fifth-power case. It advances the phi-ladder numerics that underwrite Recognition Science constants such as ħ = φ^{-5} and the dream fraction φ^{-3}. The result supplies a concrete numerical step toward the eight-tick octave and D = 3 without adding hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.