Constants Phi Ladder Fibonacci Fib Pair Of Value Unique

The rung is in the number

The golden ratio, usually written φ, is the number (1 + √5)/2, about 1.618. It is the positive solution to the equation r² = r + 1, which means its powers and the Fibonacci numbers are bound together. For instance, φ² is φ + 1, φ³ is 2φ + 1, and φ⁴ is 3φ + 2. In general, every power φⁿ can be written as F(n)·φ + F(n−1), where F(n) is the nth Fibonacci number (F(0)=0, F(1)=1, and each term is the sum of the two before it). This identity is classical and was known long before any modern framework.

The theorem fib_pair_of_value_unique in the framework's machine-checked library of formal theorems states a sharp consequence: if two integer powers of φ are equal, then their Fibonacci coefficient pairs are equal. The proof is short and rests on two facts. First, every power φⁿ equals an integer combination a·φ + b with integers a and b, by the identity above. Second, φ is irrational, so such a representation is unique: if a·φ + b equals c·φ + d, then a must equal c and b must equal d. Therefore, if φᵐ equals φⁿ, the pairs (F(m), F(m−1)) and (F(n), F(n−1)) must be identical.

In Recognition Science, this theorem does real work. The framework indexes its ladder of physical constants by integer powers of φ, called rungs. A companion theorem, rung_of_value_unique, goes one step further: because the coefficient pair is unique and φ is irrational, the map from integers to powers of φ is injective. That is, a ladder value determines its rung. If two rungs gave the same number, you could not tell them apart; this theorem rules that out. The practical consequence is that a prediction assigned to one rung cannot be silently relabeled onto another rung to make it fit a measurement. The rung is an arithmetic property of the number, not a modelling choice.

What this theorem does not claim is just as important. It does not say that every real number is a power of φ, nor that the Fibonacci signature identifies a rung from an arbitrary approximation. It only says that if two exact powers are equal, their rungs agree. The framework has separate results about identifying rungs from approximate values, which require a tolerance condition. Nor does this theorem assign any physical meaning to a rung; it is a pure statement about the golden ratio and the integers, and the framework's physical interpretation of the ladder is a separate matter.

/-- **Every integer power of φ is a Fibonacci pair.** For all `n : ℤ`,
`φ ^ n = F n · φ + F (n-1)`, where `F` is the Fibonacci sequence extended to the
negative integers.

This is the statement the library's 287 hand-written instances are shadows of, and
unlike Mathlib's natural-exponent version it covers the negative rungs that
Recognition Science actually uses. -/
theorem phi_zpow_eq_fib (n : ℤ) :
    phi ^ n = (Int.fib n : ℝ) * phi + (Int.fib (n - 1) : ℝ) := by
  have hφ : Real.goldenRatio ≠ 0 := Real.goldenRatio_ne_zero
  have hψ : Real.goldenConj ≠ 0 := Real.goldenConj_ne_zero
  have h5 : Real.sqrt 5 ≠ 0 := by positivity
  have hsub : Real.goldenRatio - Real.goldenConj = Real.sqrt 5 :=
    Real.goldenRatio_sub_goldenConj
  rw [phi_eq_goldenRatio, Real.coe_intFib_eq, Real.coe_intFib_eq,
      zpow_sub₀ hφ, zpow_sub₀ hψ, zpow_one, zpow_one]
  -- `φ⁻¹ = -ψ` and `ψ⁻¹ = -φ` are what make the conjugate terms cancel.
  have e1 : Real.goldenRatio ^ n / Real.goldenRatio
      = -(Real.goldenRatio ^ n * Real.goldenConj) := by
    rw [div_eq_mul_inv, Real.inv_goldenRatio]; ring
  have e2 : Real.goldenConj ^ n / Real.goldenConj
      = -(Real.goldenConj ^ n * Real.goldenRatio) := by
    rw [div_eq_mul_inv, Real.inv_goldenConj]; ring
  rw [e1, e2, div_mul_eq_mul_div, ← add_div, eq_div_iff h5, ← hsub]
  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

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

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

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

What this page does not claim

This theorem does not claim that every real number is a power of φ. This theorem does not assign physical meaning to any rung of the ladder. This theorem does not address identifying rungs from approximate values.

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: