phi_neg2_lt
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 in Recognition Science
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.
scope and limits
- Does not supply an exact closed-form expression for φ^{-2}.
- Does not extend to arbitrary negative powers without further lemmas.
- Applies only to the standard ordering on the reals.
formal statement (Lean)
242theorem phi_neg2_lt : goldenRatio ^ (-2 : ℤ) < (0.382 : ℝ) := by
proof body
Tactic-mode proof.
243 have h := phi_sq_gt -- 2.618 < φ²
244 have hpos_bound : (0 : ℝ) < 2.618 := by norm_num
245 have heq : goldenRatio ^ (-2 : ℤ) = (goldenRatio ^ 2)⁻¹ :=
246 zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 2)
247 rw [heq]
248 have h1 : (goldenRatio ^ 2)⁻¹ < (2.618 : ℝ)⁻¹ :=
249 inv_strictAnti₀ hpos_bound h
250 have h2 : (2.618 : ℝ)⁻¹ < (0.382 : ℝ) := by norm_num
251 linarith
252
253/-! ## Negative powers of φ (using φ⁻¹ = φ - 1) -/
254
255/-- φ⁻¹ = φ - 1 ≈ 0.618 -/