solution.lean

import Mathlib
set_option linter.style.setOption false
set_option maxHeartbeats 800000

/- Recursive definition of the odd part of a natural number -/
def oddPart (n : ℕ) : ℕ :=
  if n = 0 then 0
  else if n % 2 = 0 then oddPart (n / 2)
  else n
termination_by n
decreasing_by omega

/- Unfolding lemma for oddPart -/
lemma oddPart_eq (n : ℕ) :
    oddPart n = if n = 0 then 0 else if n % 2 = 0 then oddPart (n / 2) else n := by
  rw [oddPart]

lemma oddPart_even {n : ℕ} (hn : n ≠ 0) (he : n % 2 = 0) : oddPart n = oddPart (n / 2) := by
  rw [oddPart_eq]; simp [hn, he]

lemma oddPart_odd {n : ℕ} (hn : n ≠ 0) (ho : ¬ n % 2 = 0) : oddPart n = n := by
  rw [oddPart_eq]; simp [hn, ho]

/- The odd part of a positive number is positive -/
lemma oddPart_pos {n : ℕ} (hn : 0 < n) : 0 < oddPart n := by
  induction n using oddPart.induct with
  | case1 => omega
  | case2 _ h1 h2 ih => rw [oddPart_even h1 h2]; exact ih (by omega)
  | case3 _ h1 h2 => rw [oddPart_odd h1 h2]; omega

/- oddPart(2*n) = oddPart(n) for n > 0 -/
lemma oddPart_two_mul {n : ℕ} (hn : 0 < n) : oddPart (2 * n) = oddPart n := by
  rw [oddPart_even (by omega) (by omega : (2 * n) % 2 = 0)]
  congr 1; omega

/- oddPart(m*n) = m * oddPart(n) when m is odd -/
lemma oddPart_odd_mul {m n : ℕ} (hm : m % 2 = 1) (hn : 0 < n) :
    oddPart (m * n) = m * oddPart n := by
  have hm0 : m ≠ 0 := by
    intro hmz; simp [hmz] at hm
  induction n using oddPart.induct with
  | case1 => omega
  | case2 n h1 h2 ih =>
    -- n even
    have h2dvd : 2 ∣ n := Nat.dvd_of_mod_eq_zero h2
    rcases h2dvd with ⟨t, rfl⟩
    have ht0 : t ≠ 0 := by
      intro ht
      apply h1
      simp [ht]
    have htpos : 0 < t := Nat.pos_of_ne_zero ht0
    -- simplify oddPart (2*t)
    have hodd_n : oddPart (2 * t) = oddPart t := by
      -- even case reduces to dividing by 2
      have h := oddPart_even (n := 2 * t) (by exact Nat.mul_ne_zero (by decide) ht0) (by simp)
      simpa [Nat.mul_div_left] using h
    rw [hodd_n]
    -- handle lhs oddPart (m*(2*t))
    have hmn_ne : m * (2 * t) ≠ 0 := Nat.mul_ne_zero hm0 (by simp [ht0])
    have hmn_even : (m * (2 * t)) % 2 = 0 := by simp [Nat.mul_mod]
    rw [oddPart_even hmn_ne hmn_even]
    -- simplify division
    have hdiv : m * (2 * t) / 2 = m * t := by
      rw [Nat.mul_div_assoc m (dvd_mul_right 2 t)]
      simp [Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]
    rw [hdiv]
    -- apply IH (note (2*t)/2 = t)
    have htpos2 : 0 < (2 * t) / 2 := by simpa [Nat.mul_div_left] using htpos
    simpa [Nat.mul_div_left] using ih htpos2
  | case3 n h1 h2 =>
    -- n odd
    rw [oddPart_odd h1 h2]
    have hmn_ne : m * n ≠ 0 := Nat.mul_ne_zero hm0 h1
    have hnmod : n % 2 = 1 := by
      have h' := Nat.mod_two_eq_zero_or_one n
      cases h' with
      | inl hz => cases h2 hz
      | inr ho => exact ho
    have hmn_odd : ¬ (m * n) % 2 = 0 := by
      have : (m * n) % 2 = 1 := by
        simp [Nat.mul_mod, hm, hnmod]
      omega
    rw [oddPart_odd hmn_ne hmn_odd]

/- Key descent: oddPart(d_next) * g = oddPart(d) when d_next * g = 2 * d, g odd -/
lemma oddPart_descent {d_next d g : ℕ}
    (h_eq : d_next * g = 2 * d) (hg_odd : g % 2 = 1) (hd : 0 < d) :
    oddPart d_next * g = oddPart d := by
  have hg_pos : 0 < g := by omega
  have hd_next_pos : 0 < d_next := by
    by_contra h; push_neg at h; interval_cases d_next; simp at h_eq; omega
  have hg_cop2 : Nat.Coprime g 2 := by
    rw [Nat.coprime_comm, Nat.coprime_two_left, Nat.odd_iff]; exact hg_odd
  have hg_dvd_d : g ∣ d := by
    have hg_dvd_2d : g ∣ (2 * d) := ⟨d_next, by linarith⟩
    exact hg_cop2.dvd_of_dvd_mul_left hg_dvd_2d
  obtain ⟨q, hq⟩ := hg_dvd_d
  have hq_pos : 0 < q := by nlinarith
  have hd_next_eq : d_next = 2 * q := by nlinarith
  rw [hd_next_eq, oddPart_two_mul hq_pos, hq]
  rw [mul_comm (oddPart q) g, ← oddPart_odd_mul hg_odd hq_pos]

/- General lemma: antitone w with strict decrease on S implies S finite -/
lemma finite_of_antitone_strict_on {w : ℕ → ℕ}
    (hle : ∀ k, w (k + 1) ≤ w k) {S : Set ℕ}
    (hlt : ∀ k ∈ S, w (k + 1) < w k) : S.Finite := by
  by_contra hinf; rw [Set.not_finite] at hinf
  have hanti : Antitone w := antitone_nat_of_succ_le hle
  -- For each element of S, there's a strictly larger one
  have hex_gt : ∀ j, ∃ k ∈ S, j < k := by
    intro j; exact (Set.infinite_iff_exists_gt.mp hinf) j
  -- Get one element of S
  obtain ⟨s0, hs0⟩ : ∃ k, k ∈ S := by
    obtain ⟨k, hk, _⟩ := hex_gt 0; exact ⟨k, hk⟩
  -- Build strictly increasing sequence in S
  have : ∃ f : ℕ → ℕ, f 0 ∈ S ∧ (∀ n, f n ∈ S) ∧ (∀ n, f n < f (n + 1)) := by
    choose g hgS hglt using hex_gt
    exact ⟨fun n => Nat.rec s0 (fun _ x => g x) n,
      hs0,
      fun n => by induction n with | zero => exact hs0 | succ n ih => exact hgS _,
      fun n => by induction n with | zero => exact hglt s0 | succ n ih => exact hglt _⟩
  obtain ⟨f, _, hfS, hfmono⟩ := this
  -- w drops by at least 1 at each element of the sequence
  suffices key : ∀ n, w (f n + 1) + n ≤ w (f 0) by have := key (w (f 0) + 1); omega
  intro n; induction n with
  | zero => simp; exact (hlt _ (hfS 0)).le
  | succ n ih =>
    have h1 : w (f (n + 1) + 1) < w (f (n + 1)) := hlt _ (hfS _)
    have h2 : w (f (n + 1)) ≤ w (f n + 1) := by
      apply hanti; have := hfmono n; omega
    omega

/- Helper: Int.gcd expressed via Nat.gcd for odd naturals -/
lemma int_gcd_eq_nat_gcd (m n : ℕ) :
    Int.gcd (2 * ↑m + 1 : ℤ) (2 * ↑n + 1 : ℤ) = Nat.gcd (2 * m + 1) (2 * n + 1) := by
  simp only [Int.gcd]; congr 1

/- Helper: numerator of (2m+1)/(2n+1) as rational -/
lemma rat_num_eq (m n : ℕ) :
    ((2 * (m : ℚ) + 1) / (2 * (n : ℚ) + 1)).num =
    ((2 * (m : ℤ) + 1) / (Int.gcd (2 * ↑m + 1) (2 * ↑n + 1) : ℤ)) := by
  conv_lhs =>
    rw [show (2 * (m : ℚ) + 1) / (2 * (n : ℚ) + 1) =
      ((2 * (m : ℤ) + 1 : ℤ) : ℚ) / ((2 * (n : ℤ) + 1 : ℤ) : ℚ) from by push_cast; ring]
    rw [← Rat.divInt_eq_div]
  rw [Rat.num_divInt]
  simp [Int.sign_eq_one_of_pos (show (0 : ℤ) < 2 * ↑n + 1 from by omega), Int.gcd_comm]

/- Helper: denominator of (2m+1)/(2n+1) as rational -/
lemma rat_den_eq (m n : ℕ) :
    ((2 * (m : ℚ) + 1) / (2 * (n : ℚ) + 1)).den =
    ((2 * n + 1) / Nat.gcd (2 * m + 1) (2 * n + 1)) := by
  conv_lhs =>
    rw [show (2 * (m : ℚ) + 1) / (2 * (n : ℚ) + 1) =
      ((2 * (m : ℤ) + 1 : ℤ) : ℚ) / ((2 * (n : ℤ) + 1 : ℤ) : ℚ) from by push_cast; ring]
    rw [← Rat.divInt_eq_div]
  rw [Rat.den_divInt]
  simp only [show (2 * (n : ℤ) + 1) ≠ 0 from by omega, ↓reduceIte]
  congr 1
  rw [int_gcd_eq_nat_gcd n m, Nat.gcd_comm]

/- gcd of two odd numbers is odd -/
lemma gcd_odd (m n : ℕ) : (Nat.gcd (2 * m + 1) (2 * n + 1)) % 2 = 1 := by
  by_contra h
  have heven : 2 ∣ Nat.gcd (2 * m + 1) (2 * n + 1) := by omega
  have h1 : 2 ∣ (2 * m + 1) := dvd_trans heven (Nat.gcd_dvd_left _ _)
  have h2 : 2 ∣ (2 * n + 1) := dvd_trans heven (Nat.gcd_dvd_right _ _)
  omega

/- Distance function: |m(k) - n(k)| -/
def dist_mn (m n : ℕ → ℕ) (k : ℕ) : ℕ := Int.natAbs ((m k : ℤ) - n k)

/- Key recurrence: dist(k+1) * gcd = 2 * dist(k) -/
lemma dist_succ_eq (M N : ℕ → ℕ)
    (hm : ∀ k : ℕ, (M (k + 1) : ℤ) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).num)
    (hn : ∀ k : ℕ, N (k + 1) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).den)
    (k : ℕ) :
    dist_mn M N (k + 1) * Nat.gcd (2 * M k + 1) (2 * N k + 1) = 2 * dist_mn M N k := by
  set g := Nat.gcd (2 * M k + 1) (2 * N k + 1) with hg_def
  have hg_pos : 0 < g := Nat.pos_of_ne_zero (by intro h; simp_all [g])
  have hga : (g : ℤ) ∣ (2 * (M k : ℤ) + 1) := by exact_mod_cast Nat.gcd_dvd_left ..
  have hgb : (g : ℤ) ∣ (2 * (N k : ℤ) + 1) := by exact_mod_cast Nat.gcd_dvd_right ..
  have hm_eq : (M (k + 1) : ℤ) = (2 * (M k : ℤ) + 1) / g := by
    rw [hm k, rat_num_eq]; congr 1
  have hn_eq : (N (k + 1) : ℤ) = (2 * (N k : ℤ) + 1) / g := by
    have h1 : N (k + 1) = (2 * N k + 1) / g := by rw [hn k, rat_den_eq]
    zify [Nat.gcd_dvd_right (2 * M k + 1) (2 * N k + 1)] at h1
    exact_mod_cast h1
  have hg_cop2 : Nat.Coprime g 2 := by
    rw [Nat.coprime_comm, Nat.coprime_two_left, Nat.odd_iff]; exact gcd_odd (M k) (N k)
  have hg_cop2_int : IsCoprime (↑g : ℤ) 2 := by exact_mod_cast hg_cop2
  have hg_dvd_diff : (↑g : ℤ) ∣ ((M k : ℤ) - N k) := by
    have hab_dvd : (↑g : ℤ) ∣ (2 * ((M k : ℤ) - N k)) := by
      have := dvd_sub hga hgb; convert this using 1; ring
    exact hg_cop2_int.dvd_of_dvd_mul_left hab_dvd
  obtain ⟨c, hc⟩ := hg_dvd_diff
  unfold dist_mn
  rw [hm_eq, hn_eq]
  have key : (2 * ↑(M k) + 1) / (↑g : ℤ) - (2 * ↑(N k) + 1) / ↑g = 2 * c := by
    rw [show (2 * ↑(M k) + 1) / (↑g : ℤ) - (2 * ↑(N k) + 1) / ↑g =
      ((2 * ↑(M k) + 1) - (2 * ↑(N k) + 1)) / ↑g from by
      rw [Int.sub_ediv_of_dvd_sub]; exact dvd_sub hga hgb]
    rw [show (2 * ↑(M k) + 1 : ℤ) - (2 * ↑(N k) + 1) = 2 * (↑g * c) from by rw [← hc]; ring]
    rw [mul_comm (↑g) c, ← mul_assoc, Int.mul_ediv_cancel _ (by exact_mod_cast hg_pos.ne')]
  rw [key, hc]
  rw [Int.natAbs_mul, show Int.natAbs (2 : ℤ) = 2 from rfl, Int.natAbs_mul, Int.natAbs_natCast]
  ring

/- dist(k) > 0 for all k when m(0) ≠ n(0) -/
lemma dist_mn_pos (M N : ℕ → ℕ) (h0 : M 0 ≠ N 0)
    (hm : ∀ k : ℕ, (M (k + 1) : ℤ) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).num)
    (hn : ∀ k : ℕ, N (k + 1) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).den)
    (k : ℕ) : 0 < dist_mn M N k := by
  induction k with
  | zero => simp [dist_mn, Int.natAbs_pos]; omega
  | succ k ih =>
    have h := dist_succ_eq M N hm hn k
    by_contra h2; push_neg at h2
    have : dist_mn M N (k + 1) = 0 := by omega
    simp [this] at h; omega

/- oddPart of distance is non-increasing -/
lemma oddPart_dist_antitone (M N : ℕ → ℕ) (h0 : M 0 ≠ N 0)
    (hm : ∀ k : ℕ, (M (k + 1) : ℤ) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).num)
    (hn : ∀ k : ℕ, N (k + 1) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).den)
    (k : ℕ) : oddPart (dist_mn M N (k + 1)) ≤ oddPart (dist_mn M N k) := by
  set g : ℕ := Nat.gcd (2 * M k + 1) (2 * N k + 1)
  have hg_pos : 0 < g := by
    simpa [g] using Nat.gcd_pos_of_pos_left (2 * M k + 1) (2 * N k + 1) (by omega)
  have hdescent : oddPart (dist_mn M N (k + 1)) * g = oddPart (dist_mn M N k) := by
    simpa [g] using
      (oddPart_descent (d_next := dist_mn M N (k + 1)) (d := dist_mn M N k) (g := g)
        (dist_succ_eq M N hm hn k) (gcd_odd (M k) (N k)) (dist_mn_pos M N h0 hm hn k))
  have hle : oddPart (dist_mn M N (k + 1)) ≤ oddPart (dist_mn M N (k + 1)) * g :=
    Nat.le_mul_of_pos_right _ hg_pos
  simpa [hdescent] using hle

/- At bad steps (non-coprime), oddPart strictly decreases -/
lemma oddPart_dist_strict_at_bad (M N : ℕ → ℕ) (h0 : M 0 ≠ N 0)
    (hm : ∀ k : ℕ, (M (k + 1) : ℤ) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).num)
    (hn : ∀ k : ℕ, N (k + 1) = ((2 * ↑(M k) + 1) / (2 * ↑(N k) + 1) : ℚ).den)
    (k : ℕ) (hbad : ¬(2 * M k + 1).Coprime (2 * N k + 1)) :
    oddPart (dist_mn M N (k + 1)) < oddPart (dist_mn M N k) := by
  set g : ℕ := Nat.gcd (2 * M k + 1) (2 * N k + 1)
  have hg_pos : 0 < g := by
    simpa [g] using Nat.gcd_pos_of_pos_left (2 * M k + 1) (2 * N k + 1) (by omega)
  have hdescent : oddPart (dist_mn M N (k + 1)) * g = oddPart (dist_mn M N k) := by
    simpa [g] using
      (oddPart_descent (d_next := dist_mn M N (k + 1)) (d := dist_mn M N k) (g := g)
        (dist_succ_eq M N hm hn k) (gcd_odd (M k) (N k)) (dist_mn_pos M N h0 hm hn k))
  have hg_ne1 : g ≠ 1 := by
    intro hg1
    apply hbad
    apply (Nat.coprime_iff_gcd_eq_one).2
    simpa [g, hg1]
  have hg_ge1 : 1 ≤ g := Nat.succ_le_iff.mp hg_pos
  have hg_gt1 : 1 < g := by
    refine lt_of_le_of_ne hg_ge1 ?_
    intro h
    exact hg_ne1 h.symm
  have ha_pos : 0 < oddPart (dist_mn M N (k + 1)) :=
    oddPart_pos (dist_mn_pos M N h0 hm hn (k + 1))
  have hlt : oddPart (dist_mn M N (k + 1)) < oddPart (dist_mn M N (k + 1)) * g :=
    lt_mul_of_one_lt_right ha_pos hg_gt1
  simpa [hdescent] using hlt

theorem putnam_2025_a1 (m n : ℕ → ℕ)
  (h0 : m 0 > 0 ∧ n 0 > 0 ∧ m 0 ≠ n 0)
  (hm : ∀ k : ℕ, m (k + 1) = ((2 * m k + 1) / (2 * n k + 1) : ℚ).num)
  (hn : ∀ k : ℕ, n (k + 1) = ((2 * m k + 1) / (2 * n k + 1) : ℚ).den):
  {k | ¬ (2 * m k + 1).Coprime (2 * n k + 1)}.Finite := by
  have hm' : ∀ k : ℕ, (m (k + 1) : ℤ) = ((2 * ↑(m k) + 1) / (2 * ↑(n k) + 1) : ℚ).num := by
    intro k; exact_mod_cast hm k
  have hn' : ∀ k : ℕ, n (k + 1) = ((2 * ↑(m k) + 1) / (2 * ↑(n k) + 1) : ℚ).den := by
    intro k; exact_mod_cast hn k
  exact finite_of_antitone_strict_on
    (w := fun k => oddPart (dist_mn m n k))
    (oddPart_dist_antitone m n h0.2.2 hm' hn')
    (oddPart_dist_strict_at_bad m n h0.2.2 hm' hn')