phi_sq_lt
plain-language theorem explainer
The theorem establishes that the square of the golden ratio is strictly less than 2.619. Researchers deriving inverse powers of phi for mass estimates or quark ladders in Recognition Science numerics would cite this result. The proof is a short algebraic reduction that invokes the prior upper bound on phi, substitutes the quadratic identity, and closes with linear arithmetic.
Claim. $ (1 + 5^{1/2})/2 ^2 < 2.619 $
background
The module supplies rigorous numerical bounds on the golden ratio using algebraic properties of square roots. It begins from the elementary inequalities 2.236 squared less than 5 less than 2.237 squared, which force 2.236 less than square root of 5 less than 2.237 and therefore 1.618 less than phi less than 1.6185. The upstream result phi less than 1.6185 is obtained exactly by unfolding the definition of the golden ratio and applying the square-root bound via linear arithmetic.
proof idea
The proof invokes the theorem phi less than 1.6185, substitutes the identity that goldenRatio squared equals goldenRatio plus one, and concludes by linear arithmetic.
why it matters
This bound is the immediate parent of the theorem establishing phi to the negative two greater than 0.3818, which supplies the numerical control needed for quark-mass estimates on the phi-ladder. It therefore supports the self-similar fixed point phi forced at step T6 of the unified forcing chain and the Recognition Composition Law. No open scaffolding questions are closed by this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.