phi_inv3_gt
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 in Recognition Science
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).
scope and limits
- Does not supply an upper bound on (φ^{-1})^3.
- Does not derive the numerical constant 0.2359 from first principles.
- Does not apply outside the real numbers.
- Does not claim the bound is optimal.
formal statement (Lean)
420theorem phi_inv3_gt : (0.2359 : ℝ) < goldenRatio⁻¹ ^ 3 := by
proof body
Term-mode proof.
421 have h1 := phi_inv_gt
422 have h2 := phi_inv2_gt
423 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
424 have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
425 nlinarith [sq_nonneg goldenRatio⁻¹]
426