phi_lt_16185
plain-language theorem explainer
The golden ratio satisfies an upper bound of 1.6185. Researchers verifying the fine-structure constant and mass ladders in Recognition Science cite this result for numerical control. The proof is a one-line wrapper that applies the companion square-root bound and closes with linear arithmetic.
Claim. The golden ratio satisfies $phi < 1.6185$, where $phi = (1 + sqrt(5))/2$.
background
The module supplies rigorous bounds on the golden ratio using the algebraic identity $phi = (1 + sqrt(5))/2$. It establishes that $2.236^2 < 5 < 2.237^2$, hence $2.236 < sqrt(5) < 2.237$ and therefore $1.618 < phi < 1.6185$. The upstream theorem states $sqrt(5) < 2.237$ and is invoked directly.
proof idea
Unfold the definition of the golden ratio. Apply the theorem establishing $sqrt(5) < 2.237$. Close the resulting inequality with linear arithmetic.
why it matters
This bound feeds the upper estimate in the alpha-G score card and multiple power inequalities on phi used for mass verification. It supplies the numerical precision required for the phi-ladder in the Recognition Science framework, where phi is the self-similar fixed point from the forcing chain. Downstream results such as the phi-cubed bound and the phi^17 lemma rely on it directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.