Numerics Interval Phi Bounds Phi Inv3 In Interval Proven

A proven interval for phi inverse cubed

The golden ratio φ is the positive solution of x² = x + 1, about 1.6180339887. Its reciprocal, 1/φ, is about 0.6180339887, and the cube of that reciprocal is about 0.2360679775. The declaration phi_inv3_interval_proven is a formal object in the framework's machine-checked library of formal theorems. It records a proof that 0.2359 < (1/φ)³ < 0.237, with both bounds given as exact rational numbers.

The proof does not rely on decimal approximations or a calculator. It starts from the classical fact that φ = (1 + √5)/2. The library first proves tight bounds on √5 by squaring nearby decimals: 2.236² = 4.999696 < 5 and 2.237² = 5.001956 > 5. This yields 1.618 < φ < 1.6185. From those bounds, the library derives the reciprocal interval 0.618 < 1/φ < 0.6186, and then cubes those bounds to reach the final interval for (1/φ)³.

In Recognition Science, this interval is a numerical anchor. The framework derives φ as the unique self-similar scaling forced by its cost function, and particle masses sit on a φ-power ladder. The declaration provides a rigorous numerical handle on one rung of that ladder: φ⁻³. The number 0.2360679775 is not a measured quantity; it is a consequence of the definition of φ. The interval is a proof certificate, not a new physical claim.

What the declaration does not claim is just as important. It does not assert that φ⁻³ has any special physical meaning on its own. It does not say that the interval is tight in any optimal sense; it is simply a correct bound. The declaration does not prove that φ is irrational, does not prove the forcing chain that motivates φ, and does not connect φ⁻³ to any measured particle mass. It only certifies a decimal interval for one algebraic expression.

/-- Interval containing (φ⁻¹)³ - PROVEN -/
def phi_inv3_interval_proven : Interval where
  lo := 2359 / 10000
  hi := 237 / 1000
  valid := by norm_num

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

What this page does not claim

The declaration does not assign any physical meaning to φ⁻³ on its own. The interval is not claimed to be optimal or tight in any sense beyond being correct. The declaration does not prove the irrationality of φ or the forcing chain that motivates it.

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: