phi_sub_one_pos
plain-language theorem explainer
The lemma establishes that the golden ratio exceeds unity, specifically φ > 1. Numerics modules handling interval arithmetic and absolute values cite this to justify simplifications around φ - 1. The proof is a one-line wrapper that imports the lower bound 1.618 < φ from phi_gt_1618 and applies linear arithmetic.
Claim. $0 < φ - 1$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module Numerics.Interval.PhiBounds supplies rigorous bounds on the golden ratio using algebraic inequalities from √5. It derives 1.618 < φ < 1.6185 from 2.236² < 5 < 2.237². The upstream result phi_gt_1618 states 1.618 < φ and is proved by unfolding goldenRatio and invoking sqrt5_gt_2236.
proof idea
The proof invokes phi_gt_1618, which asserts 1.618 < goldenRatio, then applies linarith to deduce goldenRatio - 1 > 0.
why it matters
This result supports the absolute-value identity phi_minus_one_abs and the interval membership phi_sub_one_mem_Icc. It contributes to the chain of φ bounds used for mass verification such as phi_pow6_gt. In the Recognition framework the bound ensures precise numerical handling of the self-similar fixed point φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.