Numerics Interval Pow Phi Pow Neg3 In Interval

A bounded check

The golden ratio, usually written φ, is the number (1 + √5)/2, about 1.618. Raising it to a negative power gives a reciprocal: φ⁻³ is about 1 divided by 4.236, which is roughly 0.236. The declaration in question, from a machine-checked library of formal theorems, proves that this value lies between 0.2359 and 0.237. That is the entire content: a rigorous interval bound, not a new physical law.

The proof works by interval arithmetic. The library defines a narrow interval for φ itself, between 1.618 and 1.619. It then uses the fact that the power function xʸ is monotone in y when x is greater than 1. Since φ is greater than 1, increasing the exponent increases the result. The negative exponent flips the direction, so the bounds on φ translate into bounds on φ⁻³. The final interval, from 0.2359 to 0.237, is stated and verified in the formal system.

This is a numerical fact, not a claim about the origin of the golden ratio. It does not say why φ appears in the framework's forcing chain, nor does it assert that φ⁻³ has any special physical meaning. It is a building block, a checked calculation that other results can rely on. The declaration's value is precision: anyone using φ⁻³ in a later proof knows it sits in that interval, with no floating-point guesswork.

In Recognition Science, the golden ratio emerges as the unique self-similar scaling in the framework's cost theory. This interval bound is a supporting detail for that larger story. It confirms that the negative powers of φ, which appear in the framework's constants, are computable to known accuracy. The bound itself is neutral: it would hold in any context where φ is defined as (1 + √5)/2.

What the declaration does not claim is broader than what it does. It does not prove that φ⁻³ is irrational, though it is. It does not give the exact decimal expansion, only a range. And it does not connect φ⁻³ to any measured physical constant. The theorem is a small, solid piece of arithmetic, useful precisely because it is small and solid.

theorem phi_pow_neg3_in_interval : phi_pow_neg3_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-3 : ℝ)) := by
  simp only [Interval.contains, phi_pow_neg3_interval]
  rw [← phi_eq_formula]
  have hpos : (0 : ℝ) < goldenRatio := Real.goldenRatio_pos
  have h : goldenRatio ^ (-3 : ℝ) = goldenRatio⁻¹ ^ 3 := by
    rw [Real.rpow_neg (le_of_lt hpos)]
    have : (3 : ℝ) = (3 : ℕ) := by norm_num
    rw [this, Real.rpow_natCast, inv_pow]
  rw [h]
  have hcontains := phi_inv3_in_interval_proven
  simp only [Interval.contains, phi_inv3_interval_proven] at hcontains
  constructor
  · have h1 : ((2359 / 10000 : ℚ) : ℝ) = (0.2359 : ℝ) := by norm_num
    linarith [hcontains.1]
  · have h1 : ((237 / 1000 : ℚ) : ℝ) = (0.237 : ℝ) := by norm_num
    linarith [hcontains.2]

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

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

What this page does not claim

The declaration does not claim that φ⁻³ has any special physical meaning. It does not provide an exact decimal expansion, only an interval bound. It does not assert that the golden ratio itself is derived from the interval arithmetic.

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: