Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1993P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Nat.Factorization.Basic
public import Mathlib.Tactic.NormNum.Ineq

public section


/-!
# USA Mathematical Olympiad 1993, Problem 4

The sequence aₙ of odd positive integers is defined as follows:
a₁ = r, a₂ = s, and aₙ is the greatest odd divisor of aₙ₋₁ + aₙ₋₂.
Show that, for sufficiently large n, aₙ is constant and find this
constant (in terms of r and s).
-/

namespace Usa1993P4

/-- The constant value that the sequence eventually takes. -/
/- determine -/ abbrev constant_value (r s : ℕ) : ℕ := sorry

theorem usa1993_p4 (r s : ℕ) (hr : Odd r) (hs : Odd s) (a : ℕ → ℕ)
    (ha0 : a 0 = r) (ha1 : a 1 = s)
    (han : ∀ n, a (n + 2) = ordCompl[2] (a (n + 1) + a n)) :
    ∃ N, ∀ n, N ≤ n → a n = constant_value r s := sorry

end Usa1993P4

File author(s): Kimi K3

This problem has a complete formalized solution.