one_lt_phi
plain-language theorem explainer
The golden ratio satisfies 1 < φ. Researchers in Recognition Science cite this to bound reciprocals and derived ratios below unity in applications from acoustics to astrophysics. The proof is a one-line term reference to the identical fact already shown in Constants.
Claim. $1 < φ$ where $φ = (1 + √5)/2$ is the positive root of $x^2 = x + 1$.
background
The module records the defining quadratic $φ^2 = φ + 1$ whose positive solution is the golden ratio. Upstream, Constants.one_lt_phi establishes the same inequality by showing $√1 < √5$, hence $2 < 1 + √5$, and therefore $1 < (1 + √5)/2$. LawOfExistence.Constants supplies an abstract bundle of CPM constants but is not invoked in the present statement.
proof idea
Term-mode one-line wrapper that directly invokes Constants.one_lt_phi.
why it matters
This inequality is the basic bound required for all subsequent claims that a φ-derived quantity is less than one. It is used by resonant_minimization (zero geometric strain at resonant scales), goldenDivision_lt_one, pitchJNDFraction_lt_one, agronomicTipPoint_lt_one, and fastRadioBurstFromBITCert. It underwrites the self-similar fixed-point property of φ (T6) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.