one_lt_phi
plain-language theorem explainer
The golden ratio is proven to exceed 1. Workers on self-similar scaling in Recognition Science applications cite this bound when deriving inequalities for J-cost in acoustics, agronomy, and architecture. The tactic proof chains real number comparisons of square roots, applies linarith for the key inequality 2 < 1 + sqrt(5), divides by 2, and simplifies to the definition of phi.
Claim. The golden ratio satisfies $1 < phi$.
background
Constants introduces the golden ratio phi along with its elementary inequalities. The module sets the RS time quantum to one tick. An upstream theorem in PhiSupport asserts phi > 1, while a lemma there applies simp to phi_def and Real.one_lt_goldenRatio.
proof idea
The tactic proof opens by confirming 0 < 2 and sqrt(1) < sqrt(5) via norm_num and sqrt_lt_sqrt. Linarith then establishes 2 < 1 + sqrt(5). Division by 2 yields 1 < (1 + sqrt(5))/2. The final simpa step substitutes the definition of phi to complete the proof.
why it matters
This basic inequality is invoked in 40 places, feeding theorems such as pitchJNDFraction_lt_one in acoustics and resonant_minimization in coherence technology. It corresponds to the phi > 1 requirement following the forcing of the self-similar fixed point at T6. Downstream doc-comments note its use in showing zero geometric strain for resonant scales that are powers of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.