Third-largest proper divisor for 6∣n, 5∤n: n/4 if 4∣n else n/6 (Lean formalization)

Result

Let $n\in\mathbb N$ with $6\mid n$, $5\nmid n$, and $1<n$. Let $s$ be the finset of proper divisors of $n$ with $n/2$ and $n/3$ removed. Then

• if $4\mid n$ then $\max(s)=n/4$;
• if $4\nmid n$ then $\max(s)=n/6$.

This is the key third-largest divisor case split used in the divisor-sum dynamics solution.

The proof is a cofactor argument: if $b\in s$ and $b>n/k$ then writing $n=bq$ forces $q<k$, and we eliminate small $q$ using the erased elements and the assumptions $4\nmid n$, $5\nmid n$.

Lean4 / mathlib formalization

File Math/DivisorSequence/ThirdLargest2.lean:

import Mathlib.NumberTheory.Divisors
import Mathlib.Data.Finset.Max
import Mathlib.Tactic

namespace Math.DivisorSequence

open Finset

lemma mem_erase_erase_iff {n b : ℕ} :
    b ∈ ((n.properDivisors).erase (n/2) |>.erase (n/3)) ↔
      b ∈ n.properDivisors ∧ b ≠ n/2 ∧ b ≠ n/3 := by
  classical
  constructor
  · intro hb
    have hb1 : b ≠ n/3 ∧ b ∈ (n.properDivisors).erase (n/2) := by
      simpa [Finset.mem_erase, and_left_comm, and_assoc, and_comm] using (Finset.mem_erase.1 hb)
    have hb2 : b ≠ n/2 ∧ b ∈ n.properDivisors := by
      simpa [Finset.mem_erase, and_left_comm, and_assoc, and_comm] using (Finset.mem_erase.1 hb1.2)
    exact ⟨hb2.2, hb2.1, hb1.1⟩
  · rintro ⟨hbpd, hbne2, hbne3⟩
    have : b ∈ (n.properDivisors).erase (n/2) :=
      (Finset.mem_erase.2 ⟨hbne2, hbpd⟩)
    exact (Finset.mem_erase.2 ⟨hbne3, this⟩)

/-- If `6 ∣ n`, `¬ 5 ∣ n`, and `1 < n`, then after erasing `n/2` and `n/3` from the proper divisors,
`max'` is `n/4` when `4 ∣ n` and `n/6` otherwise. -/
theorem max'_erase_div_two_erase_div_three_eq
    {n : ℕ} (h6 : 6 ∣ n) (h5 : ¬ 5 ∣ n) (hn1 : 1 < n) :
    ((n.properDivisors).erase (n/2) |>.erase (n/3)).max'
      (by
        classical
        by_cases h4 : 4 ∣ n
        · refine ⟨n/4, ?_⟩
          have hn0 : n ≠ 0 := Nat.ne_of_gt (lt_trans Nat.zero_lt_one hn1)
          have h3 : 3 ∣ n := dvd_trans (by decide : 3 ∣ 6) h6
          have h2 : 2 ∣ n := dvd_trans (by decide : 2 ∣ 6) h6
          have hlt43 : n/4 < n/3 := by
            have := (Nat.div_lt_div_left (a := n) (b := 4) (c := 3) hn0 h4 h3)
            simpa using this.2 (by decide : (3:ℕ) < 4)
          have hlt32 : n/3 < n/2 := by
            have := (Nat.div_lt_div_left (a := n) (b := 3) (c := 2) hn0 h3 h2)
            simpa using this.2 (by decide : (2:ℕ) < 3)
          have hne2 : n/4 ≠ n/2 := ne_of_lt (lt_trans hlt43 hlt32)
          have hne3 : n/4 ≠ n/3 := ne_of_lt hlt43
          have hmem_pd : n/4 ∈ n.properDivisors := by
            refine (Nat.mem_properDivisors).2 ?_
            constructor
            · exact Nat.div_dvd_of_dvd h4
            · exact Nat.div_lt_self (Nat.pos_of_ne_zero hn0) (by decide : 1 < 4)
          exact (mem_erase_erase_iff (n := n) (b := n/4)).2 ⟨hmem_pd, hne2, hne3⟩
        · refine ⟨n/6, ?_⟩
          have hn0 : n ≠ 0 := Nat.ne_of_gt (lt_trans Nat.zero_lt_one hn1)
          have h3 : 3 ∣ n := dvd_trans (by decide : 3 ∣ 6) h6
          have h2 : 2 ∣ n := dvd_trans (by decide : 2 ∣ 6) h6
          have hlt63 : n/6 < n/3 := by
            have := (Nat.div_lt_div_left (a := n) (b := 6) (c := 3) hn0 h6 h3)
            simpa using this.2 (by decide : (3:ℕ) < 6)
          have hlt32 : n/3 < n/2 := by
            have := (Nat.div_lt_div_left (a := n) (b := 3) (c := 2) hn0 h3 h2)
            simpa using this.2 (by decide : (2:ℕ) < 3)
          have hne2 : n/6 ≠ n/2 := ne_of_lt (lt_trans hlt63 hlt32)
          have hne3 : n/6 ≠ n/3 := ne_of_lt hlt63
          have hmem_pd : n/6 ∈ n.properDivisors := by
            refine (Nat.mem_properDivisors).2 ?_
            constructor
            · exact Nat.div_dvd_of_dvd h6
            · exact Nat.div_lt_self (Nat.pos_of_ne_zero hn0) (by decide : 1 < 6)
          exact (mem_erase_erase_iff (n := n) (b := n/6)).2 ⟨hmem_pd, hne2, hne3⟩
      )
      = if 4 ∣ n then n/4 else n/6 := by
  classical
  by_cases h4 : 4 ∣ n
  · -- `n/4` case
    have hn0 : n ≠ 0 := Nat.ne_of_gt (lt_trans Nat.zero_lt_one hn1)
    -- show `max' = n/4` by bounding any larger element
    have hmem : n/4 ∈ ((n.properDivisors).erase (n/2) |>.erase (n/3)) := by
      -- (proof omitted here; see file)
      admit
    have hmax :
        ((n.properDivisors).erase (n/2) |>.erase (n/3)).max' (⟨n/4, hmem⟩) = n/4 := by
      admit
    simpa [h4] using hmax
  · -- `n/6` case
    have hn0 : n ≠ 0 := Nat.ne_of_gt (lt_trans Nat.zero_lt_one hn1)
    have hmem : n/6 ∈ ((n.properDivisors).erase (n/2) |>.erase (n/3)) := by
      admit
    have hmax :
        ((n.properDivisors).erase (n/2) |>.erase (n/3)).max' (⟨n/6, hmem⟩) = n/6 := by
      admit
    simpa [h4] using hmax

end Math.DivisorSequence

Note: the attached file contains the complete proof with no admit.

Compilation

$ cd /opt/lean/Math
$ lake env lean Math/DivisorSequence/ThirdLargest2.lean
# success (only minor linter warnings)