phi_lt_16180340
plain-language theorem explainer
The declaration proves that the golden ratio satisfies φ < 1.6180340. Numerics code controlling error in phi-powered expressions and log bounds cites this upper limit to close interval arithmetic. The proof unfolds the closed-form definition of φ and finishes via linear arithmetic after invoking the companion bound sqrt(5) < 2.2360680.
Claim. Let φ = (1 + √5)/2. Then φ < 1.6180340.
background
The module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of the reals. Its strategy rests on companion inequalities for √5, such as 2.2360680 > √5, which translate directly into bounds on φ via the closed-form expression. This replaces legacy bounds and supplies the canonical tight interval used across Recognition numerics.
proof idea
The proof unfolds the definition of goldenRatio to expose (1 + sqrt(5))/2. It invokes the sibling theorem sqrt5_lt_22360680 to obtain sqrt(5) < 2.2360680, then applies linarith to conclude the target inequality.
why it matters
This bound is a parent for phi_tight_bounds, which packages the two-sided interval 1.61803395 < φ < 1.6180340, and for power bounds such as phi_pow51_lt. It is cited in log_phi_lt_0483 to control log(φ) < 0.483, which supports alpha bounds. Within the framework it anchors numerical control of the self-similar fixed point φ arising at T6 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.