Constants Phi Ladder Fibonacci Rung Of Value Unique

The value fixes the rung

The golden ratio, φ = (1 + √5)/2 ≈ 1.618, is the unique positive number whose square is one more than itself: φ² = φ + 1. Its powers form a ladder: φ² = φ + 1, φ³ = 2φ + 1, φ⁴ = 3φ + 2, and so on. The coefficients are the Fibonacci numbers (1, 1, 2, 3, 5, 8, ...), where each is the sum of the two before. This connection between φ and Fibonacci numbers is classical, known since the 19th century through Binet's formula.

The ladder extends to negative and fractional steps, and it is one-to-one: each rung has a distinct value. The machine-checked library of formal theorems proves this injectivity in a theorem called rung_of_value_unique. It states that if φ^m = φ^n for any integers m and n, then m = n. The proof is short: take the real logarithm of both sides, use the fact that log φ is not zero, and cancel it. This is a ledger, a discrete record of events, where each entry is a power of φ and its position is fixed by its value.

The stronger companion theorem, fib_pair_of_value_unique, shows why the coefficients matter. Every power φ^n can be written as F(n)·φ + F(n−1), where F(n) is the nth Fibonacci number. Because φ is irrational, this representation is unique: if two such expressions are equal, their coefficients must match. So a real number of this form determines its Fibonacci pair, and therefore its rung, without any ambiguity.

In Recognition Science, this uniqueness is load-bearing. The framework models particle masses as sitting on this φ-ladder, and it proves that a predicted mass cannot be relabeled onto a different rung to make it fit a measurement. The rung is an arithmetic property of the number itself, not a modelling choice. This is a theorem, not a physical measurement: it guarantees the ladder's internal consistency, not that any particular particle sits on it.

What the theorem does not claim is equally important. It does not say which rung any real particle occupies, nor that the ladder's values match any measured mass. It only says that the map from integers to powers of φ is injective. The physical identification of a rung with a particle is a separate, empirical question, and the theorem is silent on it.

/-- **The rung is recoverable from the value.** The ladder map `n ↦ φ ^ n` is
injective on `ℤ`, so a ladder value belongs to exactly one rung.

This is the general form of the no-relabelling argument that the mass modules prove
one particle at a time. It says the rung index is an arithmetic property of the real
number, not a choice the modeller gets to make. -/
theorem rung_of_value_unique {m n : ℤ} (h : phi ^ m = phi ^ n) : m = n := by
  have hlog : Real.log (phi ^ m) = Real.log (phi ^ n) := by rw [h]
  rw [Real.log_zpow, Real.log_zpow] at hlog
  have hpos : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
  have hmn : (m : ℝ) = (n : ℝ) := mul_right_cancel₀ hpos hlog
  exact_mod_cast hmn

/-- **The rung is recoverable from the value.** The ladder map `n ↦ φ ^ n` is
injective on `ℤ`, so a ladder value belongs to exactly one rung.

This is the general form of the no-relabelling argument that the mass modules prove
one particle at a time. It says the rung index is an arithmetic property of the real
number, not a choice the modeller gets to make. -/
theorem rung_of_value_unique {m n : ℤ} (h : phi ^ m = phi ^ n) : m = n := by
  have hlog : Real.log (phi ^ m) = Real.log (phi ^ n) := by rw [h]
  rw [Real.log_zpow, Real.log_zpow] at hlog
  have hpos : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
  have hmn : (m : ℝ) = (n : ℝ) := mul_right_cancel₀ hpos hlog
  exact_mod_cast hmn

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

/-- The representation of a real number as `a·φ + b` with integer `a, b` is unique,
because `φ` is irrational. -/
theorem int_combination_unique {a b c d : ℤ}
    (h : (a : ℝ) * phi + (b : ℝ) = (c : ℝ) * phi + (d : ℝ)) : a = c ∧ b = d := by
  have hirr : Irrational phi := phi_irrational
  have hac : a = c := by
    by_contra hne
    have hk : ((a - c : ℤ) : ℝ) ≠ 0 := Int.cast_ne_zero.mpr (sub_ne_zero.mpr hne)
    have hval : phi = ((d - b : ℤ) : ℝ) / ((a - c : ℤ) : ℝ) := by
      rw [eq_div_iff hk]
      push_cast
      linear_combination h
    exact hirr.ne_rational (d - b) (a - c) hval
  refine ⟨hac, ?_⟩
  subst hac
  have : (b : ℝ) = (d : ℝ) := by linarith
  exact_mod_cast this

theorem phi_irrational : Irrational phi := by
  rw [phi_eq_goldenRatio]; exact Real.goldenRatio_irrational

What this page does not claim

The theorem does not identify any measured particle mass with a specific rung. The theorem does not prove that the φ-ladder contains all real numbers, only that its rungs are distinct. The theorem does not rely on any physical measurement; it is a purely arithmetic statement.

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: