phi_sq_gt
plain-language theorem explainer
The declaration establishes the strict inequality 2.618 < φ² for the golden ratio φ. Numerics researchers tightening interval bounds in the Recognition Science project cite it when deriving companion inequalities for negative powers. The proof is a short term-mode argument that invokes the prior lower bound 1.618 < φ, substitutes the algebraic identity φ² = φ + 1, and finishes by linear arithmetic.
Claim. $2.618 < φ^2$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of the square root. It starts from the elementary inequalities 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185 and then refines selected constants further. The upstream result phi_gt_1618 supplies the concrete lower bound 1.618 < φ that this theorem consumes.
proof idea
The proof invokes the lemma phi_gt_1618 to obtain 1.618 < φ, substitutes the algebraic identity goldenRatio ^ 2 = goldenRatio + 1, and concludes by linarith.
why it matters
This bound is consumed by the downstream theorem phi_neg2_lt, which derives the companion inequality φ^{-2} < 0.382. Within the Recognition Science framework the golden ratio appears as the self-similar fixed point whose powers generate the phi-ladder used for mass and resonance calculations. The result closes a small gap in the numeric scaffolding for the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.