Numerics Interval Pow Phi Pow Neg5 In Interval

A certified bound for phi to the minus fifth

The golden ratio, usually written φ, is the number (1 + √5)/2, approximately 1.6180339887. It is the positive solution to the equation x² = x + 1, and it appears throughout geometry, art, and number theory. When raised to the power −5, φ⁻⁵ is about 0.0901699437. This value is not just an approximation; it can be bounded exactly between two rational numbers.

The declaration phi_pow_neg5_in_interval, part of a machine-checked library of formal theorems, establishes precisely this: the number φ⁻⁵ lies in the closed interval from 89/1000 to 91/1000. In decimal form, that means 0.089 ≤ φ⁻⁵ ≤ 0.091. The proof is rigorous, meaning it does not rely on numerical approximation or floating-point arithmetic. Instead, it uses the monotonicity of the power function and the definition of φ to verify the bounds symbolically.

This interval bound is a building block, not a destination. The library uses such certified intervals to support larger claims about the golden ratio and its powers. The specific interval for φ⁻⁵ is notable because this quantity appears in the framework's constants, where it is identified with the reduced Planck constant in natural units. The theorem does not assert that identification; it only certifies the numerical range.

What the declaration does not claim is just as important. It does not say that φ⁻⁵ is exactly 0.09, nor does it claim any physical significance for the number. It does not assert that the golden ratio itself is rational or irrational; that is a separate matter. The theorem is purely about the interval: a precise, machine-verified statement that the value falls between two rational bounds. This kind of exactness is what makes the larger framework's numerical claims auditable.

theorem phi_pow_neg5_in_interval : phi_pow_neg5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-5 : ℝ)) := by
  -- φ^(-5) = (φ⁻¹)^5
  simp only [Interval.contains, phi_pow_neg5_interval]
  rw [← phi_eq_formula]
  have hpos : (0 : ℝ) < goldenRatio := Real.goldenRatio_pos
  have h : goldenRatio ^ (-5 : ℝ) = goldenRatio⁻¹ ^ 5 := by
    rw [Real.rpow_neg (le_of_lt hpos)]
    have : (5 : ℝ) = (5 : ℕ) := by norm_num
    rw [this, Real.rpow_natCast, inv_pow]
  rw [h]
  have hcontains := phi_inv5_in_interval_proven
  simp only [Interval.contains, phi_inv5_interval_proven] at hcontains
  constructor
  · have h1 : ((89 / 1000 : ℚ) : ℝ) = (0.089 : ℝ) := by norm_num
    linarith [hcontains.1]
  · have h1 : ((91 / 1000 : ℚ) : ℝ) = (0.091 : ℝ) := by norm_num
    linarith [hcontains.2]

/-- φ > 1, so φ^x is strictly increasing in x -/
lemma phi_rpow_strictMono : StrictMono (fun x : ℝ => goldenRatio ^ x) := by
  intro y z hyz
  exact Real.rpow_lt_rpow_of_exponent_lt Real.one_lt_goldenRatio hyz

/-- φ = (1 + √5)/2 (Mathlib definition) -/
theorem phi_eq_formula : goldenRatio = (1 + Real.sqrt 5) / 2 := rfl

What this page does not claim

The theorem does not assert that φ⁻⁵ equals any specific decimal value. It does not claim physical significance for the number φ⁻⁵. It does not state whether the golden ratio is rational or irrational.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/Pow.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: