phi_inv_gt
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.