Numerics Interval Phi Bounds Phi Pow8 In Interval Proven

A certified interval for φ⁸

The golden ratio φ = (1 + √5)/2 ≈ 1.6180339887 is an irrational number, so its powers never land exactly on a simple decimal. Yet many calculations need a reliable stand-in: a certified interval that is guaranteed to contain the true value. The declaration phi_pow8_interval_proven supplies exactly that for φ⁸, the eighth power of the golden ratio. It states, as a formally verified fact, that φ⁸ lies strictly between 46.97 and 46.99. In symbols: 46.97 < φ⁸ < 46.99.

The proof is not an approximate computation but a rigorous chain of inequalities. It starts from the elementary bounds 2.236 < √5 < 2.237, which follow from squaring those decimals and comparing with 5. Halving and adding 1/2 gives 1.618 < φ < 1.6185. Raising these bounds to the eighth power, with careful handling of the inequalities, yields the interval for φ⁸. The entire argument is checked by a machine, line by line, in a formal library of theorems. The declaration itself is a definition of an interval object whose validity is established by the accompanying theorems phi_pow8_gt and phi_pow8_lt.

This kind of certified bound matters because later results in the framework build on it. The interval for φ⁸ is not an isolated curiosity; it feeds into bounds for higher powers and for expressions involving φ, such as φ⁵¹ and φ⁻²³¹⁄⁴, which appear in the same module. When a later theorem needs to know that some quantity is smaller or larger than a threshold, it can cite this interval as a trusted fact rather than re-derive the bound from scratch. The machine-checked nature of the proof means the interval is not a numerical guess but a proven statement, on the same logical footing as any other theorem in the library.

What this declaration does not claim is just as important. It does not say that φ⁸ is rational, or that it has a terminating decimal expansion; the interval is a range, not an exact value. It does not assert that 46.97 or 46.99 are themselves powers of φ, or that they have any special significance beyond being tight bounds. The interval is a tool, not a discovery about the nature of φ⁸. It also does not claim anything about the physical or geometric meaning of φ⁸ within the broader Recognition Science framework; it is a purely numerical fact, established by arithmetic and inequality reasoning, independent of any physical interpretation.

theorem phi_pow8_gt : (46.97 : ℝ) < goldenRatio ^ 8 := by
  rw [phi_pow8_eq]
  have h := phi_gt_1618
  linarith

theorem phi_pow8_lt : goldenRatio ^ 8 < (46.99 : ℝ) := by
  rw [phi_pow8_eq]
  have h := phi_lt_16185
  linarith

/-- 2.236² < 5 -/
theorem sq_2236_lt_5 : (2.236 : ℝ)^2 < 5 := by norm_num

/-- 5 < 2.237² -/
theorem five_lt_sq_2237 : (5 : ℝ) < (2.237 : ℝ)^2 := by norm_num

/-- Interval containing φ⁸ - PROVEN -/
def phi_pow8_interval_proven : Interval where
  lo := 4697 / 100
  hi := 4699 / 100
  valid := by norm_num

What this page does not claim

This declaration does not claim that φ⁸ is rational or has a terminating decimal expansion. This declaration does not assign any physical or geometric meaning to φ⁸ within the Recognition Science framework. This declaration does not claim that the bounds 46.97 and 46.99 are themselves significant constants.

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/PhiBounds.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: