phi_pow_fib
The identity states that φ raised to n+1 equals the (n+1)th Fibonacci number times φ plus the nth Fibonacci number. Cosmologists computing the exact algebraic form of the baryon asymmetry prefactor cite this to obtain closed expressions such as φ^8 = 21φ + 13 without approximation error. The proof is by induction on n, substituting the inductive hypothesis into the recurrence for Fibonacci numbers and reducing via the quadratic relation φ² = φ + 1.
claimFor every natural number $n$, $φ^{n+1} = F_{n+1} φ + F_n$, where $F_k$ denotes the $k$th Fibonacci number with $F_0 = 0$, $F_1 = 1$.
background
The golden ratio φ satisfies the equation φ² = φ + 1, as established by phi_sq_eq from the minimal polynomial x² - x - 1 = 0. The Fibonacci sequence follows the standard Mathlib definition with F_0 = 0, F_1 = 1 and the recurrence F_{k+2} = F_{k+1} + F_k. This theorem sits inside the module deriving the prefactor c_RS = (1 - φ^{-8})^2 for the baryon-to-photon ratio η_B, where the eight-tick washout at D = 3 supplies the factor φ^{-8} and the squared form encodes independent matter and antimatter channels.
proof idea
The proof is by induction on n. The base case n = 0 reduces directly to φ = φ after applying Nat.fib_zero = 0, Nat.fib_one = 1 and simplification. The inductive step rewrites the left side as φ^{n+1} · φ, substitutes the inductive hypothesis, expands with ring, replaces φ² by φ + 1 via phi_sq_eq, collects terms, and matches the Fibonacci recurrence Nat.fib (n+2) = Nat.fib n + Nat.fib (n+1) to reach the target form.
why it matters in Recognition Science
This supplies the exact closed form required by phi_pow_44_fib to evaluate φ^{44} = 701408733 φ + 433494437 and thereby bound c_RS · φ^{-44} inside (6.0 × 10^{-10}, 6.2 × 10^{-10}), the interval containing the Planck 2018 value of η_B. It is also invoked by the universality results fibonacciPhiCert and phi_pow_bounded_by_fib in the cross-domain Fibonacci-phi module. Within the Recognition framework it implements the algebraic content of the eight-tick octave (T7) and the phi-ladder needed for the integration-gap rung at D = 3.
scope and limits
- Does not derive the squared washout interpretation of c_RS from a Boltzmann equation.
- Does not prove that the integration gap equals φ^5.
- Does not address the full transport dynamics of baryogenesis.
- Does not establish uniqueness of the phi-ladder mass formula.
Lean usage
have hfib := phi_pow_fib 43formal statement (Lean)
147private theorem phi_pow_fib (n : ℕ) :
148 phi ^ (n + 1) = (Nat.fib (n + 1) : ℝ) * phi + (Nat.fib n : ℝ) := by
proof body
Tactic-mode proof.
149 induction n with
150 | zero =>
151 simp only [Nat.fib_zero, Nat.cast_zero, add_zero]
152 rw [show Nat.fib 1 = 1 from rfl]; simp
153 | succ n ih =>
154 have hfib : Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1) := Nat.fib_add_two
155 calc phi ^ (n + 1 + 1) = phi ^ (n + 1) * phi := by ring
156 _ = ((Nat.fib (n + 1) : ℝ) * phi + (Nat.fib n : ℝ)) * phi := by rw [ih]
157 _ = (Nat.fib (n + 1) : ℝ) * phi ^ 2 + (Nat.fib n : ℝ) * phi := by ring
158 _ = (Nat.fib (n + 1) : ℝ) * (phi + 1) + (Nat.fib n : ℝ) * phi := by rw [phi_sq_eq]
159 _ = ((Nat.fib (n + 1) : ℝ) + (Nat.fib n : ℝ)) * phi + (Nat.fib (n + 1) : ℝ) := by ring
160 _ = (↑(Nat.fib n + Nat.fib (n + 1)) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by
161 simp only [Nat.cast_add]; ring
162 _ = (Nat.fib (n + 2) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by rw [hfib]
163