Constants Phi Ladder Fibonacci Int Combination Unique

The unique ladder

The golden ratio φ, the number (1 + √5)/2 ≈ 1.618, has a famous arithmetic habit: its powers can be written using Fibonacci numbers. For example, φ² = φ + 1, and φ³ = 2φ + 1. The pattern continues for all integer powers, positive and negative: φ raised to the n-th power equals F(n)·φ + F(n−1), where F is the Fibonacci sequence extended to negative integers. This identity is classical for natural exponents; the machine-checked library of formal theorems in Recognition Science extends it to all integers, which is the version its physics needs.

The key consequence, proved in the framework's library, is that this representation is unique. The theorem int_combination_unique states that if a·φ + b = c·φ + d for integers a, b, c, d, then a = c and b = d. Because φ is irrational, no two different integer pairs can describe the same real number. This means the coefficient pair (F(n), F(n−1)) is a perfect fingerprint of the exponent n: the map from integers to powers of φ is injective. A ladder value therefore determines its rung, and you cannot relabel a prediction onto a different rung to make it fit.

In Recognition Science, the framework models particle masses as sitting on a φ-power ladder, indexed by integers. The uniqueness theorem guarantees that each rung has a single arithmetic identity, not a modelling choice. The library proves this in two forms: rung_of_value_unique shows that if φ^m = φ^n then m = n, and fib_pair_of_value_unique shows the Fibonacci coefficients themselves match. This generalizes the 287 hand-written lemmas that each stated one specific power, such as φ⁸ = 21φ + 13, into a single quantified statement.

What the theorem does not claim is any empirical content. It is a pure arithmetic fact about the golden ratio; it says nothing about which rung, if any, corresponds to a measured particle mass. The comparison of predicted masses against measured values is a separate empirical check, not part of this theorem. The uniqueness result only guarantees that if the ladder is used, the labels are unambiguous.

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

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

What this page does not claim

No measured particle mass is identified with any specific rung by this theorem. The theorem does not prove that the φ-ladder is the correct model for particle masses. It does not claim that the Fibonacci representation is unique for real coefficients, only for integer pairs.

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: