one_lt_phi
plain-language theorem explainer
The lemma asserts that the golden ratio φ exceeds 1. Researchers cite it whenever a ratio or inverse power of φ must be shown strictly less than one, as occurs in JND fractions, agronomic tip points, and resonant scale arguments. The proof is a direct term-mode simplification that reduces the claim to the definition of φ together with Mathlib's built-in fact that the golden ratio is greater than one.
Claim. $1 < phi$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The PhiSupport.Lemmas module supplies elementary golden-ratio facts used inside certificates. It records the closed-form definition phi = Real.goldenRatio, the relation phi^2 = phi + 1, and the fixed-point identity phi = 1 + 1/phi, all resting on real algebra alone. The local setting is that these lemmas carry no Recognition-specific hypotheses and depend only on Mathlib's goldenRatio library facts. Upstream, phi_def equates Constants.phi to Real.goldenRatio, while the same inequality is already recorded in Constants.one_lt_phi.
proof idea
The proof is a one-line term-mode wrapper. It applies simp with the lemmas phi_def and Real.one_lt_goldenRatio, which together unfold the definition and invoke the library inequality for the golden ratio.
why it matters
The inequality is invoked in more than forty downstream certificates that bound geometric quantities below unity by taking reciprocals or negative powers of phi. It directly supports resonant_minimization, preferredAspectRatio_gt_one, goldenDivision_lt_one, pitchJNDFraction_lt_one, and agronomicTipPoint_lt_one. Within the Recognition framework it supplies the elementary bound required for the phi-ladder mass formula and the self-similar fixed point at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.