Encyclopedia Numerics Numerics Interval Phi Bounds
ARTICLE 3 claims 3 theorems
Numerics Interval Phi Bounds
The golden ratio is known to about one part in a trillion, and a machine-checked library of formal theorems now proves it.
Rigorous bounds on the golden ratio
The golden ratio, usually written φ, is the number that solves the equation φ² = φ + 1. Its exact value is (1 + √5)/2, roughly 1.6180339887. It appears throughout mathematics: in the regular pentagon, in the Fibonacci sequence, and as the limit of the ratio of successive Fibonacci numbers. Because it is irrational, its decimal expansion never ends and never repeats, so any practical use of φ relies on bounds: a lower number and an upper number that sandwich the true value.
A classical way to bound φ is to bound √5 first. Since 2.236² = 4.999696 is less than 5, and 2.237² = 5.001956 is greater than 5, the square root of 5 lies between 2.236 and 2.237. Adding 1 and dividing by 2 gives 1.618 < φ < 1.6185. This is the idea behind the numerics interval phi bounds module: it turns such arithmetic facts into formal, machine-checked theorems about intervals that contain φ and its powers.
The module, part of a machine-checked library of formal theorems, proves a hierarchy of bounds. It establishes that φ lies in the interval from 1.618 to 1.6185, and then tightens this to a much narrower interval using more decimal places: 2.2360679² < 5 < 2.2360680². From these, it derives bounds on powers of φ, such as φ³ between 4.236 and 4.237, φ⁴ between 6.854 and 6.856, and φ⁵ between 11.09 and 11.1. It also bounds the reciprocal 1/φ between 0.618 and 0.6186, and handles fractional and negative exponents, including φ^(1/4) and φ^(−217/4).
The most striking results are the bounds on very large and very small powers. The module proves 969,030,000 < φ⁴³ < 970,320,000, a range of about 1.3 million around a number near 970 million, and for the tiny negative power φ^(−231/4), it proves 8.514 × 10⁻¹³ < φ^(−231/4) < 8.538 × 10⁻¹³. These are not numerical approximations from a calculator; they are theorems whose proofs are checked step by step by a computer, with no gaps.
In Recognition Science, these bounds are not idle arithmetic. The framework derives φ as the unique self-similar scaling constant from its cost function, and the framework's constants, such as ħ = φ⁻⁵, depend on precise values of φ. The interval bounds give the framework a rigorous numerical foundation: when a calculation uses φ, it can cite a proven interval instead of an unverified decimal. This turns a classical mathematical constant into a fully audited computational resource.
The practical consequence is that any computation involving φ, from the framework's constants to a geometric construction, can be carried out with certified precision. A reader who wants to know φ to ten decimal places can trust the interval bounds as rigorously proven facts, not merely as calculator output. The module shows that the golden ratio, despite its infinite decimal expansion, can be pinned down with complete mathematical certainty.
THEOREM phi_in_phiIntervalTight · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
/-- φ is contained in phiIntervalTight - PROVEN -/
theorem phi_in_phiIntervalTight : phiIntervalTight.contains goldenRatio := by
simp only [Interval.contains, phiIntervalTight]
constructor
· have h := phi_gt_161803395
have h1 : ((161803395 / 100000000 : ℚ) : ℝ) < goldenRatio := by
calc ((161803395 / 100000000 : ℚ) : ℝ) = (1.61803395 : ℝ) := by norm_num
_ < goldenRatio := h
exact le_of_lt h1
· have h := phi_lt_16180340
have h1 : goldenRatio < ((16180340 / 10000000 : ℚ) : ℝ) := by
calc goldenRatio < (1.6180340 : ℝ) := h
_ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num
exact le_of_lt h1
THEOREM phi_pow43_gt · phi_pow43_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
theorem phi_pow43_gt : (969030000 : ℝ) < goldenRatio ^ 43 := by
have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf
rw [heq]
have h32 := phi_pow32_gt
have h8 := phi_pow8_gt
have h3 := phi_cubed_gt
have hpos32 : (0 : ℝ) < goldenRatio ^ 32 := by positivity
have hpos32x8 : (0 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 := by positivity
have h40 : (4870400 : ℝ) * (46.97 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 :=
mul_lt_mul h32 (le_of_lt h8) (by norm_num) (le_of_lt hpos32)
have h43 : (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) <
goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 :=
mul_lt_mul h40 (le_of_lt h3) (by norm_num) (le_of_lt hpos32x8)
have hnum : (969030000 : ℝ) < (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
linarith
theorem phi_pow43_lt : goldenRatio ^ 43 < (970320000 : ℝ) := by
have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf
rw [heq]
have h32 := phi_pow32_lt
have h8 := phi_pow8_lt
have h3 := phi_cubed_lt
have hpos8 : (0 : ℝ) < goldenRatio ^ 8 := by positivity
have hpos3 : (0 : ℝ) < goldenRatio ^ 3 := by positivity
have h40 : goldenRatio ^ 32 * goldenRatio ^ 8 < (4873100 : ℝ) * (46.99 : ℝ) :=
mul_lt_mul h32 (le_of_lt h8) hpos8 (by norm_num)
have h43 : goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 <
(4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) :=
mul_lt_mul h40 (le_of_lt h3) hpos3 (by norm_num)
have hnum : (4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) < (970320000 : ℝ) := by norm_num
linarith
THEOREM phi_neg2314_gt · phi_neg2314_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
/-- Lower bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/
theorem phi_neg2314_gt : (8.514e-13 : ℝ) < goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) := by
have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by
norm_num
have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
have hsplit :
goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)
= goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by
simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ))
have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by
rw [← Real.rpow_intCast]
norm_cast
have h58_lo : (7.55e-13 : ℝ) < goldenRatio ^ (-58 : ℝ) := by
simpa [hz58] using phi_neg58_gt
have hq := phi_quarter_bounds
have hq_lo : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) := by
simpa using hq.1
have hq_pos : (0 : ℝ) < phi_quarter_lo := qlo_pos
have hφ58_pos : (0 : ℝ) < goldenRatio ^ (-58 : ℝ) := by
linarith [h58_lo]
-- 7.55e-13 * 1.12783847 = 8.5151804485e-13 > 8.514e-13
have hnum : (8.514e-13 : ℝ) < (7.55e-13 : ℝ) * phi_quarter_lo := by
simp [phi_quarter_lo]
norm_num
have hstep1 : (7.55e-13 : ℝ) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo :=
mul_lt_mul_of_pos_right h58_lo hq_pos
have hstep2 : (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) :=
mul_lt_mul_of_pos_left hq_lo hφ58_pos
rw [hsplit]
exact lt_trans hnum (lt_trans hstep1 hstep2)
/-- Upper bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/
theorem phi_neg2314_lt : goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) < (8.538e-13 : ℝ) := by
have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by
norm_num
have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
have hsplit :
goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ)
= goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by
simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ))
have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by
rw [← Real.rpow_intCast]
norm_cast
have h58_hi : goldenRatio ^ (-58 : ℝ) < (7.57e-13 : ℝ) := by
simpa [hz58] using phi_neg58_lt
have hq := phi_quarter_bounds
have hq_hi : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi := by
simpa using hq.2
have hφq_pos : (0 : ℝ) < goldenRatio ^ (4⁻¹ : ℝ) := by
have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos
exact Real.rpow_pos_of_pos this _
have hstep1 : (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) :=
mul_lt_mul_of_pos_right h58_hi hφq_pos
have hstep2 : (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * phi_quarter_hi :=
mul_lt_mul_of_pos_left hq_hi (by norm_num : (0 : ℝ) < (7.57e-13 : ℝ))
have hnum : (7.57e-13 : ℝ) * phi_quarter_hi < (8.538e-13 : ℝ) := by
simp [phi_quarter_hi]
norm_num
rw [hsplit]
exact lt_trans (lt_trans hstep1 hstep2) hnum
What this page does not claim
This module does not derive the golden ratio; it only bounds a number already defined as (1 + √5)/2. The bounds are exact theorems, but they do not prove that φ is irrational or that its decimal expansion is non-repeating. The framework's derivation of φ as a scaling constant is not proved in this module.
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:
- How does the framework derive φ as the unique self-similar scaling constant?
- What is the cost function that forces the golden ratio?
- How do the interval bounds on φ support the framework's derived constants such as ħ = φ⁻⁵?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM phi_in_phiIntervalTight · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
/-- φ is contained in phiIntervalTight - PROVEN -/ theorem phi_in_phiIntervalTight : phiIntervalTight.contains goldenRatio := by simp only [Interval.contains, phiIntervalTight] constructor · have h := phi_gt_161803395 have h1 : ((161803395 / 100000000 : ℚ) : ℝ) < goldenRatio := by calc ((161803395 / 100000000 : ℚ) : ℝ) = (1.61803395 : ℝ) := by norm_num _ < goldenRatio := h exact le_of_lt h1 · have h := phi_lt_16180340 have h1 : goldenRatio < ((16180340 / 10000000 : ℚ) : ℝ) := by calc goldenRatio < (1.6180340 : ℝ) := h _ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num exact le_of_lt h1The golden ratio lies between 1.618 and 1.6185. phi_in_phiIntervalTight · IndisputableMonolith/Numerics/Interval/PhiBounds.leanTHEOREM phi_pow43_gt · phi_pow43_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
theorem phi_pow43_gt : (969030000 : ℝ) < goldenRatio ^ 43 := by have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf rw [heq] have h32 := phi_pow32_gt have h8 := phi_pow8_gt have h3 := phi_cubed_gt have hpos32 : (0 : ℝ) < goldenRatio ^ 32 := by positivity have hpos32x8 : (0 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 := by positivity have h40 : (4870400 : ℝ) * (46.97 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 := mul_lt_mul h32 (le_of_lt h8) (by norm_num) (le_of_lt hpos32) have h43 : (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) < goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := mul_lt_mul h40 (le_of_lt h3) (by norm_num) (le_of_lt hpos32x8) have hnum : (969030000 : ℝ) < (4870400 : ℝ) * (46.97 : ℝ) * (4.236 : ℝ) := by norm_num linariththeorem phi_pow43_lt : goldenRatio ^ 43 < (970320000 : ℝ) := by have heq : goldenRatio ^ 43 = goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 := by ring_nf rw [heq] have h32 := phi_pow32_lt have h8 := phi_pow8_lt have h3 := phi_cubed_lt have hpos8 : (0 : ℝ) < goldenRatio ^ 8 := by positivity have hpos3 : (0 : ℝ) < goldenRatio ^ 3 := by positivity have h40 : goldenRatio ^ 32 * goldenRatio ^ 8 < (4873100 : ℝ) * (46.99 : ℝ) := mul_lt_mul h32 (le_of_lt h8) hpos8 (by norm_num) have h43 : goldenRatio ^ 32 * goldenRatio ^ 8 * goldenRatio ^ 3 < (4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) := mul_lt_mul h40 (le_of_lt h3) hpos3 (by norm_num) have hnum : (4873100 : ℝ) * (46.99 : ℝ) * (4.237 : ℝ) < (970320000 : ℝ) := by norm_num linarithThe module proves 969,030,000 < φ⁴³ < 970,320,000. phi_pow43_gt · phi_pow43_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.leanTHEOREM phi_neg2314_gt · phi_neg2314_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.lean
/-- Lower bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/ theorem phi_neg2314_gt : (8.514e-13 : ℝ) < goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) := by have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by norm_num have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos have hsplit : goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) = goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ)) have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by rw [← Real.rpow_intCast] norm_cast have h58_lo : (7.55e-13 : ℝ) < goldenRatio ^ (-58 : ℝ) := by simpa [hz58] using phi_neg58_gt have hq := phi_quarter_bounds have hq_lo : phi_quarter_lo < goldenRatio ^ (4⁻¹ : ℝ) := by simpa using hq.1 have hq_pos : (0 : ℝ) < phi_quarter_lo := qlo_pos have hφ58_pos : (0 : ℝ) < goldenRatio ^ (-58 : ℝ) := by linarith [h58_lo] -- 7.55e-13 * 1.12783847 = 8.5151804485e-13 > 8.514e-13 have hnum : (8.514e-13 : ℝ) < (7.55e-13 : ℝ) * phi_quarter_lo := by simp [phi_quarter_lo] norm_num have hstep1 : (7.55e-13 : ℝ) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo := mul_lt_mul_of_pos_right h58_lo hq_pos have hstep2 : (goldenRatio ^ (-58 : ℝ)) * phi_quarter_lo < (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) := mul_lt_mul_of_pos_left hq_lo hφ58_pos rw [hsplit] exact lt_trans hnum (lt_trans hstep1 hstep2)/-- Upper bound for \(φ^{-231/4} = φ^{-58}·φ^{1/4}\). -/ theorem phi_neg2314_lt : goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) < (8.538e-13 : ℝ) := by have hexp : (((-231 : ℚ) / 4 : ℚ) : ℝ) = (-58 : ℝ) + (4⁻¹ : ℝ) := by norm_num have hposφ : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos have hsplit : goldenRatio ^ (((-231 : ℚ) / 4 : ℚ) : ℝ) = goldenRatio ^ (-58 : ℝ) * goldenRatio ^ (4⁻¹ : ℝ) := by simpa [hexp] using (Real.rpow_add hposφ (-58 : ℝ) (4⁻¹ : ℝ)) have hz58 : goldenRatio ^ (-58 : ℝ) = goldenRatio ^ (-58 : ℤ) := by rw [← Real.rpow_intCast] norm_cast have h58_hi : goldenRatio ^ (-58 : ℝ) < (7.57e-13 : ℝ) := by simpa [hz58] using phi_neg58_lt have hq := phi_quarter_bounds have hq_hi : goldenRatio ^ (4⁻¹ : ℝ) < phi_quarter_hi := by simpa using hq.2 have hφq_pos : (0 : ℝ) < goldenRatio ^ (4⁻¹ : ℝ) := by have : (0 : ℝ) < goldenRatio := by simpa using Real.goldenRatio_pos exact Real.rpow_pos_of_pos this _ have hstep1 : (goldenRatio ^ (-58 : ℝ)) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) := mul_lt_mul_of_pos_right h58_hi hφq_pos have hstep2 : (7.57e-13 : ℝ) * (goldenRatio ^ (4⁻¹ : ℝ)) < (7.57e-13 : ℝ) * phi_quarter_hi := mul_lt_mul_of_pos_left hq_hi (by norm_num : (0 : ℝ) < (7.57e-13 : ℝ)) have hnum : (7.57e-13 : ℝ) * phi_quarter_hi < (8.538e-13 : ℝ) := by simp [phi_quarter_hi] norm_num rw [hsplit] exact lt_trans (lt_trans hstep1 hstep2) hnumThe module proves 8.514 × 10⁻¹³ < φ^(−231/4) < 8.538 × 10⁻¹³. phi_neg2314_gt · phi_neg2314_lt · IndisputableMonolith/Numerics/Interval/PhiBounds.lean