Constants Phi Ladder Fibonacci Phi Pow Succ Eq Fib

The Fibonacci ladder

The golden ratio φ, defined as (1 + √5)/2, has a remarkable relationship with the Fibonacci sequence. The declaration phi_pow_succ_eq_fib establishes that for any natural number n, φ raised to the power n+1 equals the (n+1)th Fibonacci number times φ, plus the nth Fibonacci number. In symbols: φ^(n+1) = F(n+1)·φ + F(n). This is a theorem in the framework's machine-checked library of formal theorems, proved for all natural exponents at once, rather than one instance at a time.

The classical identity itself is known: it follows from the defining equation φ² = φ + 1, which encodes the golden ratio's self-similarity. The framework's contribution is to extend this to the full integer ladder, where the exponent can be negative as well as positive. For example, φ⁻³ equals 2φ - 3, a value that appears in the framework's identifiability threshold. The general integer form, φ^n = F(n)·φ + F(n-1), uses integer-indexed Fibonacci numbers, a version absent from the standard library and needed for the framework's physics.

The deeper consequence is injectivity. Because φ is irrational, the representation of any ladder value as an integer combination of φ and 1 is unique. The theorem rung_of_value_unique proves that if φ^m equals φ^n, then m equals n: the ladder map from integers to real numbers is injective. A ladder value therefore determines its rung. This means a prediction cannot be relabeled onto a different rung to make it fit; the rung is an arithmetic property of the number, not a modelling choice.

In Recognition Science, the framework models particle masses as sitting on this φ-power ladder. The uniqueness result is the general form of a claim the mass modules prove one particle at a time: the rung is forced by the value. The framework's library writes the sentence that 287 separate lemmas were shadows of, and draws the consequence that only the general form can reach.

What the declaration does not claim: it does not identify which rung corresponds to which physical particle, and it does not derive the value of any coupling constant. It establishes an arithmetic fact about the golden ratio and the Fibonacci sequence, not a physical law.

/-- 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 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 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 declaration does not identify which rung corresponds to which physical particle. The declaration does not derive the value of any coupling constant. The declaration does not prove the full forcing chain from the cost function to particle masses.

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: