Constants Phi Ladder Fibonacci Phi Pow Succ Bracket

The bracket theorem

The golden ratio, φ = (1 + √5)/2 ≈ 1.61803398875, is the positive solution to the equation x² = x + 1. This self-referential property means its powers can be written as linear combinations of φ and 1, with coefficients that are consecutive Fibonacci numbers. For example, φ² = φ + 1, φ³ = 2φ + 1, and φ⁴ = 3φ + 2. The general identity, known since the 19th century, states that φ^(n+1) = F(n+1)·φ + F(n), where F(n) is the nth Fibonacci number (F(0)=0, F(1)=1). This identity holds for all natural numbers n.

The bracket theorem, phi_pow_succ_bracket, is a computational refinement of this identity. It says that if you have a lower bound lo and an upper bound hi for φ, then the power φ^(n+1) lies between F(n+1)·lo + F(n) and F(n+1)·hi + F(n). In other words, it converts a known interval for φ into a corresponding interval for every power of φ, using the Fibonacci coefficients as scaling factors. This is not a new mathematical fact about the golden ratio; it is a tool for working with φ's powers when only approximate values are available.

In Recognition Science, the framework models particle masses as lying on a ladder of φ-powers, indexed by integers rather than natural numbers. The framework's machine-checked library of formal theorems proves a stronger result: every ladder value φ^n can be written as F(n)·φ + F(n-1) with integer coefficients, and because φ is irrational, this representation is unique. This means the ladder map from integers to real numbers is injective: each rung has a distinct value, and no two different rungs share the same number. The framework uses this to argue that a predicted mass cannot be silently relabeled onto a different rung to make it fit observations, since the rung is an arithmetic property of the number itself.

The bracket theorem itself is a modest lemma: it provides the interval bounds that make numerical computations with φ-powers practical. Its significance in the framework is that it supports the uniqueness results, which are the load-bearing claims. The theorem does not, by itself, say anything about particle masses, the fine-structure constant, or any physical measurement. It is a pure statement about real numbers and Fibonacci numbers, proved by elementary algebra from the defining equation of φ.

/-- **Any bounds on φ lift to every rung.** The bracket width is `F (n+1)` times the
width of the input bracket, so supplying more digits of φ tightens every rung at
once. -/
theorem phi_pow_succ_bracket (n : ℕ) {lo hi : ℝ} (hlo : lo ≤ phi) (hhi : phi ≤ hi) :
    (Nat.fib (n + 1) : ℝ) * lo + (Nat.fib n : ℝ) ≤ phi ^ (n + 1) ∧
      phi ^ (n + 1) ≤ (Nat.fib (n + 1) : ℝ) * hi + (Nat.fib n : ℝ) := by
  have hfib : (0 : ℝ) ≤ (Nat.fib (n + 1) : ℝ) := by positivity
  rw [phi_pow_succ_eq_fib n]
  exact ⟨by nlinarith, by nlinarith⟩

/-- The natural-exponent form, in exactly the shape the 287 instances are written in:
`phi ^ (n+1) = F (n+1) * phi + F n`. -/
theorem phi_pow_succ_eq_fib (n : ℕ) :
    phi ^ (n + 1) = (Nat.fib (n + 1) : ℝ) * phi + (Nat.fib n : ℝ) := by
  rw [phi_eq_goldenRatio, ← Real.goldenRatio_mul_fib_succ_add_fib n]
  ring

/-- **The Fibonacci pair is recoverable from the ladder value.** Two rungs with the
same value have the same Fibonacci pair, and conversely. Together with
`int_combination_unique` this says the pair `(F n, F (n-1))` is a faithful integer
fingerprint of the real number `φ ^ n`. -/
theorem fib_pair_of_value_unique {m n : ℤ} (h : phi ^ m = phi ^ n) :
    Int.fib m = Int.fib n ∧ Int.fib (m - 1) = Int.fib (n - 1) := by
  rw [phi_zpow_eq_fib, phi_zpow_eq_fib] at h
  exact int_combination_unique h

theorem ladder_injective : Function.Injective (fun n : ℤ => phi ^ n) :=
  fun _ _ h => rung_of_value_unique h

What this page does not claim

The bracket theorem does not by itself establish any physical claim about particle masses or couplings. The bracket theorem does not prove that the golden ratio is irrational; that is a separate classical result. The bracket theorem does not quantify over integer exponents; that is the role of the stronger phi_zpow_eq_fib theorem.

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/Constants/PhiLadderFibonacci.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: