phi_neg2_lt
plain-language theorem explainer
The inequality establishes φ^{-2} < 0.382 where φ denotes the golden ratio. Researchers deriving bottom-quark mass intervals and neutrino fraction predictions cite this numerical anchor inside the Recognition Science mass ladder. The proof invokes the companion lower bound on φ², rewrites the negative power as a reciprocal, applies strict monotonicity of inversion on the positives, and closes with a direct numerical comparison.
Claim. $φ^{-2} < 0.382$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio using algebraic properties of √5. The strategy starts from 2.236² < 5 < 2.237², which forces 1.618 < φ < 1.6185; tighter decimal places refine the interval further. The companion result establishes 2.618 < φ² < 2.619 by invoking the defining relation φ² = φ + 1 together with the lower bound on φ itself.
proof idea
The proof invokes the lower bound φ² > 2.618, rewrites φ^{-2} as the reciprocal of φ² via the negative-power identity, applies the strict decrease of the reciprocal map on positive reals to obtain 1/φ² < 1/2.618, and finally compares 1/2.618 < 0.382 by direct norm_num evaluation followed by linarith.
why it matters
This bound supplies the numerical precision required by the PMNS solar-angle match, the neutrino mass-fraction lemma, and the bottom-quark mass prediction. It anchors the φ-ladder mass formula at rung -2 inside the Recognition Science framework, where the eight-tick octave and phi-forcing chain convert such bounds into observable particle masses and mixing angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.