phi_inv_gt
The theorem establishes that the reciprocal of the golden ratio exceeds 0.618. Numerics researchers tightening interval estimates for φ in the Recognition Science framework would cite this when building successive power bounds. The proof rewrites the reciprocal via the algebraic identity φ^{-1} = φ - 1, invokes the lower bound 1.618 < φ, and concludes by linear arithmetic.
claim$0.618 < φ^{-1}$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module supplies rigorous bounds on the golden ratio using algebraic properties of square roots. It first shows 2.236 < √5 < 2.237, which yields the interval 1.618 < φ < 1.6185. The upstream result phi_inv_eq records the identity 1/φ = φ - 1. A sibling theorem supplies the concrete lower bound 1.618 < φ.
proof idea
The proof rewrites the target inequality by the identity φ^{-1} = φ - 1. It then applies the theorem 1.618 < φ and closes the argument by linear arithmetic.
why it matters in Recognition Science
This bound feeds the next power inequalities phi_inv2_gt and phi_inv3_gt as well as the interval-containment theorem in the same module. It supplies the numerical foundation for the phi-ladder mass formulas and resonance calculations that appear in the T5 J-uniqueness and T6 self-similar fixed-point steps of the forcing chain.
scope and limits
- Does not establish an upper bound on φ^{-1}.
- Does not supply bounds at higher decimal precision.
- Does not address convergence or approximation rates.
- Does not extend the inequality to complex or p-adic settings.
formal statement (Lean)
262theorem phi_inv_gt : (0.618 : ℝ) < goldenRatio⁻¹ := by
proof body
Term-mode proof.
263 rw [phi_inv_eq]
264 have h := phi_gt_1618
265 linarith
266