Numerics Interval Pow

Rigorous bounds for powers

Interval arithmetic is a way to make numerical calculations trustworthy. Instead of asking a computer for one answer, you give it a range, say from 1.618 to 1.619, and it returns a range that is guaranteed to contain the true result. The power function x^y, where x is positive, is handled through the identity x^y = exp(y * log x). The computation produces a range for log x, multiplies it by the range for y, then applies exp to get the final interval. For the special case of x^n with n a natural number, direct computation is used because it is more precise.

This matters because the golden ratio, the number φ = (1 + √5)/2, appears throughout Recognition Science as a fundamental scaling constant. The results prove that φ lies in the interval from 1.618 to 1.619, and they pin down several powers of φ with tight bounds. For example, φ^5 lies between 11.09 and 11.1, φ^8 between 46.97 and 46.99, and φ^16 between 2206.9 and 2207.5. Even a very large power like φ^51 is bounded between 45,537,548,334 and 45,537,549,354. These are not estimates; they are machine-checked theorems that state the true value falls inside the given range.

The results also prove monotonicity properties of the golden ratio's power function. Since φ is greater than 1, the function x ↦ φ^x is strictly increasing: if y < z then φ^y < φ^z. This gives a simple way to bound φ^x for any x in an interval: the lower bound is φ^lo and the upper bound is φ^hi. The same idea extends to negative exponents, where the function x ↦ φ^(-x) is decreasing instead.

In Recognition Science, the framework models physical constants as coming from a forcing chain of theorems. The golden ratio emerges as the unique self-similar scaling, and its powers appear in particle masses and other constants. This work provides the numerical backbone: it guarantees that when the framework refers to a value like φ^5 or 2^(-22), the number is not floating-point guesswork but a rigorously bounded interval. The library is a machine-checked collection of formal theorems, so every bound here is verified by the kernel, not by convention.

What this establishes in plain language is that the framework's constants are numerically anchored. If a theorem says a mass sits at φ^5, the results confirm the exact value lies between 11.09 and 11.1, with no rounding error possible. That is the difference between a calculation you trust and a calculation you hope is right.

/-- φ is in phiInterval - PROVEN using sqrt bounds -/
theorem phi_in_phiInterval : phiInterval.contains ((1 + Real.sqrt 5) / 2) := by
  simp only [Interval.contains, phiInterval]
  constructor
  · have h := phi_gt_1618
    have h1 : ((1618 / 1000 : ℚ) : ℝ) < (1 + Real.sqrt 5) / 2 := by
      calc ((1618 / 1000 : ℚ) : ℝ) = (1.618 : ℝ) := by norm_num
        _ < (1 + Real.sqrt 5) / 2 := h
    exact le_of_lt h1
  · have h := phi_lt_16185
    have h1 : (1 + Real.sqrt 5) / 2 < ((1619 / 1000 : ℚ) : ℝ) := by
      calc (1 + Real.sqrt 5) / 2 < (1.6185 : ℝ) := h
        _ < (1.619 : ℝ) := by norm_num
        _ = ((1619 / 1000 : ℚ) : ℝ) := by norm_num
    exact le_of_lt h1

theorem phi_pow_5_in_interval : phi_pow_5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (5 : ℝ)) := by
  simp only [Interval.contains, phi_pow_5_interval]
  rw [← phi_eq_formula]
  have h : goldenRatio ^ (5 : ℝ) = goldenRatio ^ 5 := by
    have : (5 : ℝ) = (5 : ℕ) := by norm_num
    rw [this, Real.rpow_natCast]
  rw [h]
  constructor
  · have h1 := phi_pow5_gt
    calc ((1109 / 100 : ℚ) : ℝ) = (11.09 : ℝ) := by norm_num
      _ ≤ goldenRatio ^ 5 := le_of_lt h1
  · have h1 := phi_pow5_lt
    calc goldenRatio ^ 5 ≤ (11.1 : ℝ) := le_of_lt h1
      _ = ((111 / 10 : ℚ) : ℝ) := by norm_num

/-- φ > 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

/-- 2^(-22) is in the interval - PROVEN -/
theorem two_pow_neg22_in_interval : two_pow_neg22_interval.contains ((2 : ℝ) ^ (-22 : ℤ)) := by
  simp only [Interval.contains, two_pow_neg22_interval]
  -- 2^(-22) = 1/2^22 = 1/4194304
  have h : (2 : ℝ) ^ (-22 : ℤ) = 1 / 4194304 := by
    have h2 : (2 : ℝ) ^ (22 : ℤ) = 4194304 := by norm_num
    have h3 : (2 : ℝ) ^ (-22 : ℤ) = ((2 : ℝ) ^ (22 : ℤ))⁻¹ := by
      rw [zpow_neg]
    rw [h3, h2]
    norm_num
  rw [h]
  constructor
  · -- 238/1000000000 ≤ 1/4194304
    -- 238 * 4194304 ≤ 1000000000
    -- 998223552 ≤ 1000000000 ✓
    norm_num
  · -- 1/4194304 ≤ 239/1000000000
    -- 1000000000 ≤ 239 * 4194304
    -- 1000000000 ≤ 1002438656 ✓
    norm_num

What this page does not claim

This work does not derive the golden ratio or any physical constant; it only bounds known values. The intervals here do not cover every power of φ, only the specific ones listed in the module. No claim is made about the speed or efficiency of the interval computation, only its correctness.

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: