Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2006P5

module

public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Data.Nat.Factorization.Defs
public import Mathlib.Order.Lattice.Nat
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Lemmas
public import Mathlib.Tactic.NormNum.DivMod
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic
public import Mathlib.Tactic.Zify

public section


/-!
# USA Mathematical Olympiad 2006, Problem 5

A mathematical frog jumps along the number line. The frog starts at 1,
and jumps according to the following rule: if the frog is at integer n,
then it can jump either to n + 1 or to n + 2 ^ (mₙ + 1), where 2 ^ mₙ is
the largest power of 2 that is a factor of n. Show that if k ≥ 2 is a
positive integer and i is a nonnegative integer, then the minimum number
of jumps needed to reach 2 ^ i * k is greater than the minimum number of
jumps needed to reach 2 ^ i.
-/

namespace Usa2006P5

/-- The exponent of the largest power of `2` dividing the integer `x`
(the 2-adic valuation of `x`). -/
noncomputable def nu (x : ℤ) : ℕ := x.natAbs.factorization 2

/-- `ValidPath x ss` holds when the list `ss` of jump lengths can legally be
performed by the frog starting at position `x`: each jump has length `1` or
length `2 ^ (ν₂ n + 1)`, where `n` is the position the frog jumps from. -/
def ValidPath : ℤ → List ℕ → Prop
  | _, [] => True
  | x, s :: ss => (s = 1 ∨ s = 2 ^ (nu x + 1)) ∧ ValidPath (x + (s : ℤ)) ss

/-- The frog can reach position `m` in exactly `j` jumps starting from `1`. -/
def Reachable (m : ℤ) (j : ℕ) : Prop :=
  ∃ ss : List ℕ, ValidPath 1 ss ∧ (1 : ℤ) + (ss.sum : ℤ) = m ∧ ss.length = j

/-- The minimum number of jumps the frog needs to reach position `m`. -/
noncomputable def minJumps (m : ℤ) : ℕ := sInf { j | Reachable m j }

theorem usa2006_p5 (k : ℕ) (hk : 2 ≤ k) (i : ℕ) :
    minJumps ((2 : ℤ) ^ i * (k : ℤ)) > minJumps ((2 : ℤ) ^ i) := sorry

File author(s): Kimi K3

This problem has a complete formalized solution.