phi_inv2_lt
The inequality (φ^{-1})^2 < 0.383 holds in the reals for the golden ratio φ. Researchers tightening numerical intervals on successive powers of the inverse golden ratio cite this result during algebraic verification. The proof chains the established linear upper bound on φ^{-1} with positivity of the inverse and non-linear arithmetic on the square.
claimLet φ = (1 + √5)/2 denote the golden ratio. Then (φ^{-1})^2 < 0.383.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 and its inverse by exploiting algebraic inequalities from Mathlib. It begins with the elementary comparison 2.236² < 5 < 2.237² to obtain 2.236 < √5 < 2.237, hence the coarse interval 1.618 < φ < 1.6185, and then refines the decimals. The immediate predecessor result supplies the linear bound φ^{-1} < 0.6186.
proof idea
The argument recalls the linear upper bound on φ^{-1}, records that the inverse is positive via the standard positivity lemma for reciprocals, and invokes non-linear arithmetic together with the non-negativity of squares to obtain the squared inequality.
why it matters in Recognition Science
This bound continues the chain of power inequalities on φ^{-1} that underpins numerical checks for Recognition Science constants such as ħ = φ^{-5}. It is invoked directly to establish the cubic bound φ^{-3} < 0.237 and the quintic bound φ^{-5} < 0.091. These intervals support the phi-ladder mass formula and the Berry creation threshold inside the T5–T8 forcing chain.
scope and limits
- Does not supply a matching lower bound for (φ^{-1})^2.
- Does not extend the inequality to number systems other than the reals.
- Does not derive the result without the prior linear bound on φ^{-1}.
- Does not quantify the gap between 0.383 and the true value of (φ^{-1})^2.
formal statement (Lean)
414theorem phi_inv2_lt : goldenRatio⁻¹ ^ 2 < (0.383 : ℝ) := by
proof body
Term-mode proof.
415 have h := phi_inv_lt
416 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
417 nlinarith [sq_nonneg goldenRatio⁻¹]
418
419/-- (φ⁻¹)³ bounds -/