phi_inv2_lt
plain-language theorem explainer
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.
Claim. Let φ = (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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.