phi_sub_one_lt_one
plain-language theorem explainer
The lemma establishes that the golden ratio minus one is strictly less than one. Numerics code for interval arithmetic on φ cites it to obtain both the absolute-value bound and closed-interval membership for φ - 1. The short proof applies the library inequality goldenRatio < 2 and finishes with linear arithmetic.
Claim. $φ - 1 < 1$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module supplies rigorous algebraic bounds on the golden ratio φ = (1 + √5)/2. It proceeds from the elementary inequalities 2.236² < 5 < 2.237² to conclude 1.618 < φ < 1.6185, then tightens the decimals as needed. The present lemma supplies one half of the interval membership statement that places φ - 1 inside [0, 1].
proof idea
It is a one-line wrapper that invokes Real.goldenRatio_lt_two to obtain goldenRatio < 2 and then applies linarith to deduce the target inequality.
why it matters
The lemma is used by phi_minus_one_abs_lt_one (which records |φ - 1| < 1) and by phi_sub_one_mem_Icc (which records φ - 1 ∈ [0, 1]). These two facts support the numerical layer that treats φ as the self-similar fixed point forced at step T6 of the Recognition Science chain. No open question is directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.