phi_minus_one_abs_lt_one
plain-language theorem explainer
The lemma establishes that the absolute value of the golden ratio minus one is strictly less than one. Interval arithmetic work on logarithm bounds for the golden ratio cites this to confirm the contraction condition needed for Taylor error estimates on log(1 + x). The proof is a one-line wrapper that rewrites the absolute value via a positivity identity and invokes the direct comparison goldenRatio - 1 < 1.
Claim. $|φ - 1| < 1$, where $φ$ denotes the golden ratio.
background
The declaration lives in the module supplying rigorous interval bounds for the natural logarithm. The module strategy restricts to intervals inside (0, ∞) and, for arguments of the form 1 + x with |x| < 1, invokes the Taylor series log(1 + x) = x - x²/2 + x³/3 - … together with the remainder bound |x|^{n+1}/((n+1)(1 - |x|)). The concrete choice x = φ - 1 ≈ 0.618 is singled out because it satisfies 0 < x < 1, allowing the bounds to be applied directly to log(φ).
proof idea
The proof is a one-line wrapper. It rewrites the absolute-value expression by the lemma phi_minus_one_abs (which converts |φ - 1| into φ - 1 using the positivity fact φ - 1 > 0) and then applies the exact match to the upstream inequality phi_sub_one_lt_one.
why it matters
The result supplies the contraction hypothesis required by the logarithm interval machinery when the argument is the golden ratio. It therefore supports the numerical evaluation of log(φ) inside the phi-ladder arithmetic that Recognition Science uses to derive constants such as ħ = φ^{-5} and the fine-structure interval (137.030, 137.039). The lemma closes a prerequisite step for the logPhiInterval construction in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.