fibonacci_mass_recursion

formal source

 317      y · φ^(n+2) = y · φ^(n+1) + y · φ^n
 318
 319    **The particle mass spectrum is a Fibonacci sequence.** -/
 320theorem fibonacci_mass_recursion (y : ℝ) (n : ℕ) :
 321    y * phi ^ (n + 2) = y * phi ^ (n + 1) + y * phi ^ n := by
 322  rw [phi_fibonacci_recursion]; ring
 323
 324/-- The ratio of consecutive masses = φ. -/
 325theorem mass_ratio_is_phi (y : ℝ) (hy : 0 < y) (n : ℕ) :
 326    (y * phi ^ (n + 1)) / (y * phi ^ n) = phi := by
 327  have hphin : (0 : ℝ) < phi ^ n := pow_pos phi_pos n
 328  field_simp [ne_of_gt hy, ne_of_gt hphin]; ring
 329
 330/-- Fibonacci triple: m_r + m_{r+1} = m_{r+2} (inverse Fibonacci form). -/
 331theorem fibonacci_triple_sum (y : ℝ) (n : ℕ) :
 332    y * phi ^ n + y * phi ^ (n + 1) = y * phi ^ (n + 2) := by
 333  linarith [fibonacci_mass_recursion y n]
 334
 335/-- Mass ladder is strictly increasing: φ > 1 implies each rung is heavier. -/
 336theorem mass_ladder_strictly_increasing (y : ℝ) (hy : 0 < y) (n : ℕ) :
 337    y * phi ^ n < y * phi ^ (n + 1) := by
 338  apply mul_lt_mul_of_pos_left _ hy
 339  calc phi ^ n
 340      = phi ^ n * 1   := (mul_one _).symm
 341    _ < phi ^ n * phi := mul_lt_mul_of_pos_left one_lt_phi (pow_pos phi_pos n)
 342    _ = phi ^ (n + 1) := by ring
 343
 344/-- The Fibonacci structure extends to Fibonacci number exponents.
 345    φ^(F_{n+2}) = φ^(F_{n+1}) + φ^(F_n) — all Fibonacci-level masses relate. -/
 346theorem phi_pow_fibonacci_sum_le (n : ℕ) :
 347    phi ^ n + phi ^ (n + 1) = phi ^ (n + 2) := by
 348  linarith [phi_fibonacci_recursion n]
 349
 350/-! ## §6  The Complete QG Octave Duality Certificate -/