phi_gt_161803395
plain-language theorem explainer
Golden ratio φ satisfies φ > 1.61803395. Numerics researchers in Recognition Science cite this when anchoring interval arithmetic or logarithmic estimates for φ. The proof is a one-line wrapper that unfolds the definition of goldenRatio, invokes the companion bound 2.2360679 < √5, and closes with linear arithmetic.
Claim. $1.61803395 < φ$ where $φ = (1 + √5)/2$.
background
The module supplies rigorous decimal bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties of squares. It proceeds by establishing 2.236² < 5 < 2.237² to obtain 2.236 < √5 < 2.237 and then dividing by two. This local setting supports downstream interval containments and logarithmic comparisons. The immediate upstream result is the theorem asserting 2.2360679 < √5, proved by rewriting the square-root inequality and applying monotonicity of the square-root function.
proof idea
The proof unfolds the definition of goldenRatio to expose (1 + √5)/2. It obtains the fact 2.2360679 < √5 from the companion theorem sqrt5_gt_22360679. Linear arithmetic then yields the target strict inequality.
why it matters
This bound feeds parent results including containment of φ inside phiIntervalTight and lower bounds on log φ such as log_phi_gt_048. It supplies a concrete decimal anchor for the self-similar fixed point φ (T6) inside the Recognition framework. The result supports computations that rely on the phi-ladder and eight-tick octave without floating-point approximations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.