phi_inv5_lt
This theorem establishes that the fifth power of the reciprocal of the golden ratio is strictly less than 0.091. Numerics researchers in Recognition Science cite it when tightening interval bounds on negative powers of phi for constant certification. The proof combines prior bounds on the second and third powers with positivity facts, a ring rewrite expressing the fifth power as their product, and a nonlinear arithmetic solver.
claimLet $phi = (1 + sqrt(5))/2$ be the golden ratio. Then $phi^{-5} < 0.091$.
background
The module supplies rigorous algebraic bounds on the golden ratio and its powers, starting from the observation that 2.236 squared is less than 5 which is less than 2.237 squared. This yields 2.236 < sqrt(5) < 2.237 and hence 1.618 < phi < 1.6185, with tighter decimal refinements obtained similarly. An Interval is a closed interval with rational endpoints lo ≤ hi. Upstream results include the bound (phi inverse) squared less than 0.383 and (phi inverse) cubed less than 0.237, both obtained by the same nlinarith style from the basic Interval structure defined over the reals in the Certification module.
proof idea
The proof first calls the already-established theorems bounding the second and third powers of the reciprocal golden ratio. It records positivity of the reciprocal and its second and third powers. A ring tactic rewrites the fifth power as the product of those two powers. The nlinarith tactic then closes the inequality from the component bounds and the positivity facts.
why it matters in Recognition Science
The result supplies the upper bound needed to certify that phi inverse to the fifth lies inside a proven interval, directly feeding the containment theorem that follows it in the same module. Within Recognition Science this supports the assignment hbar = phi^{-5} in native units and the phi-ladder mass formula. It closes one numerical link in the forcing chain from T5 J-uniqueness through T6 phi fixed point to concrete constant bounds.
scope and limits
- Does not give the exact numerical value of phi^{-5}.
- Does not extend the bound to non-integer exponents.
- Does not replace the algebraic derivation with a decimal expansion proof.
- Does not address floating-point rounding errors beyond the stated real inequality.
formal statement (Lean)
501theorem phi_inv5_lt : goldenRatio⁻¹ ^ 5 < (0.091 : ℝ) := by
proof body
Tactic-mode proof.
502 have h2 := phi_inv2_lt
503 have h3 := phi_inv3_lt
504 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
505 have hpos2 : 0 < goldenRatio⁻¹ ^ 2 := sq_pos_of_pos hpos
506 have hpos3 : 0 < goldenRatio⁻¹ ^ 3 := pow_pos hpos 3
507 have h : goldenRatio⁻¹ ^ 5 = goldenRatio⁻¹ ^ 2 * goldenRatio⁻¹ ^ 3 := by ring
508 nlinarith
509
510/-- Interval containing (φ⁻¹)⁵ - PROVEN -/