phi_inv3_gt
plain-language theorem explainer
This theorem establishes the strict lower bound 0.2359 < (φ^{-1})^3 for the golden ratio reciprocal. Numerics work in Recognition Science that tightens interval bounds on successive powers of φ^{-1} cites it to support higher-order estimates. The proof is a short term-mode argument that chains the already-proven lower bounds on φ^{-1} and (φ^{-1})^2 together with positivity facts and nonlinear arithmetic.
Claim. $0.2359 < (φ^{-1})^3$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2 and its reciprocal using the defining quadratic equation. It starts from the elementary inequalities 2.236 < √5 < 2.237 and tightens them by additional decimal places. Upstream results supply the base cases: phi_inv_gt states (φ^{-1}) > 0.618 and phi_inv2_gt states (φ^{-1})^2 > 0.381, both obtained by rewriting φ^{-1} = φ - 1 and applying linear arithmetic.
proof idea
The proof first recalls the lower bounds phi_inv_gt and phi_inv2_gt. It then records positivity of φ^{-1} via inv_pos and of its square via sq_pos_of_pos. Finally nlinarith is invoked on the non-negativity of (φ^{-1})^2 to close the inequality for the cube.
why it matters
The result is invoked directly by phi_inv3_in_interval_proven to certify interval membership and by phi_inv5_gt to obtain the fifth-power lower bound. It therefore supports the Recognition Science phi-ladder mass formula and the assignment ħ = φ^{-5}. The bound closes one link in the numerical verification of the eight-tick octave (T7) and the three-dimensional forcing chain (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.