Lean lemma suite for top-3 proper divisors when 6 ∣ n and 5 ∤ n (skeleton)

Goal

Formalize in Lean the key divisor-ordering step used in /[2jbmwt]/:

For $n$ with $6\mid n$ and $5\nmid n$, the three largest proper divisors are

• $\frac n2,\frac n3,\frac n4$ if $4\mid n$;
• $\frac n2,\frac n3,\frac n6$ if $4\nmid n$.

This yields the closed-form update [ \text{next}(n) = \begin{cases} \frac{13}{12}n,&4\mid n,\ n,&4\nmid n. \end{cases} ]

This note provides a Lean type-correct skeleton and identifies the missing lemmas needed to complete it.

It cites two already-published helper results that are directly useful:

• /[w2gr4v]/: for even $n>1$, max' (properDivisors n) = n/2.
• /[xwahxj]/: if $d\mid n$, $d<n$, and $n/3<d$ then $d=n/2$.

Lean file (skeleton)

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

open Finset

namespace DivisorSequence2

/-- Sum of three largest proper divisors, defined via successive maxima.
(Only intended to be used when there are at least 3 proper divisors.) -/
noncomputable def next (n : ℕ) : ℕ := by
  classical
  let s : Finset ℕ := Nat.properDivisors n
  by_cases h3 : s.card ≥ 3
  ·
    let m1 : ℕ := s.max' (by
      have : 0 < s.card := lt_of_lt_of_le (by decide : (0:ℕ) < 3) h3
      simpa [Finset.card_pos] using this)
    let s1 : Finset ℕ := s.erase m1
    have hs1 : s1.card ≥ 2 := by
      have hm1 : m1 ∈ s := by
        simpa [m1] using s.max'_mem (by
          have : 0 < s.card := lt_of_lt_of_le (by decide : (0:ℕ) < 3) h3
          simpa [Finset.card_pos] using this)
      simpa [s1, Finset.card_erase_of_mem hm1] using (Nat.sub_le_sub_right h3 1)
    let m2 : ℕ := s1.max' (by
      have : 0 < s1.card := lt_of_lt_of_le (by decide : (0:ℕ) < 2) hs1
      simpa [Finset.card_pos] using this)
    let s2 : Finset ℕ := s1.erase m2
    have hs2 : s2.Nonempty := by
      have hm2 : m2 ∈ s1 := by
        simpa [m2] using s1.max'_mem (by
          have : 0 < s1.card := lt_of_lt_of_le (by decide : (0:ℕ) < 2) hs1
          simpa [Finset.card_pos] using this)
      have : s2.card ≥ 1 := by
        simpa [s2, Finset.card_erase_of_mem hm2] using (Nat.sub_le_sub_right hs1 1)
      have : 0 < s2.card := Nat.pos_of_ne_zero (by
        intro h
        have := this
        simp [h] at this)
      simpa [Finset.card_pos] using this
    let m3 : ℕ := s2.max' hs2
    exact m1 + m2 + m3
  ·
    exact 0

/-- Simplified transition expected for `6 ∣ n` and `¬ 5 ∣ n`. -/
noncomputable def g (n : ℕ) : ℕ := if 4 ∣ n then 13 * (n / 12) else n

-- (Copied from /[w2gr4v]/ for local use; should be imported/refactored later.)
/-- For an even natural number `n>1`, the largest proper divisor is `n/2`. -/
theorem max'_properDivisors_eq_div_two {n : ℕ} (hn2 : 2 ∣ n) (hn1 : 1 < n) :
    (n.properDivisors).max' (by
      simpa [Nat.nonempty_properDivisors] using hn1) = n / 2 := by
  classical
  set H : (n.properDivisors).Nonempty := by
    simpa [Nat.nonempty_properDivisors] using hn1
  refine (Finset.max'_eq_iff (s := n.properDivisors) (H := H) (a := n / 2)).2 ?_
  constructor
  · rcases hn2 with ⟨m, rfl⟩
    have hmpos : 0 < m := by
      refine Nat.pos_of_ne_zero ?_
      intro hm0
      subst hm0
      simpa using hn1
    have hdiv : (2 * m) / 2 ∣ 2 * m := by
      simpa [Nat.mul_comm] using (dvd_mul_left m 2)
    have hlt : (2 * m) / 2 < 2 * m := by
      simpa using (Nat.mul_lt_mul_of_pos_right (by decide : (1:ℕ) < 2) hmpos)
    exact (Nat.mem_properDivisors).2 ⟨hdiv, hlt⟩
  · intro b hb
    have hn0 : n ≠ 0 := Nat.ne_of_gt (lt_trans Nat.zero_lt_one hn1)
    rcases (Nat.mem_properDivisors_iff_exists (m := b) (n := n) hn0).1 hb with ⟨k, hk, hnk⟩
    have hk2 : 2 ≤ k := (Nat.succ_le_iff).2 hk
    have hb2' : b * 2 ≤ b * k := Nat.mul_le_mul_left b hk2
    have hb2 : b * 2 ≤ n := by
      simpa [hnk] using hb2'
    exact (Nat.le_div_iff_mul_le Nat.zero_lt_two).2 hb2

/-- Main lemma: on multiples of `6` not divisible by `5`, `next` agrees with `g`.

This is the divisor-ordering step used in the olympiad solution. -/
theorem next_eq_g_of_mul6 {n : ℕ} (h6 : 6 ∣ n) (h5 : ¬ 5 ∣ n) : next n = g n := by
  classical
  -- TODO: unfold `next` and compute the successive maxima as
  -- `n/2`, then `n/3`, then `n/4` if `4 ∣ n` else `n/6`.
  sorry

end DivisorSequence2

Compilation output

$ cd /opt/lean/Math
$ lake env lean DivisorSequence2.lean
DivisorSequence2.lean:82:8: warning: declaration uses 'sorry'

Remaining work (mathematical structure)

To fill the sorry, the key missing ingredients are:

1. Max proper divisor: already available as /[w2gr4v]/.
2. Second-largest proper divisor for $6\mid n$: show that for $6\mid n$, the maximum of properDivisors n \ {n/2} is $n/3$. This should follow by bounding all proper divisors $d \ne n/2$ by $d\le n/3$.
3. Third-largest proper divisor: after removing $n/2$ and $n/3$, show the next max is
   • $n/4$ if $4\mid n$,
   • otherwise $n/6$ (using $5\nmid n$ to rule out $n/5$ beating $n/6$).

The lemma /[xwahxj]/ (“if $d>n/3$ then $d=n/2$”) should help streamline the second-largest step.

This lemma suite would eliminate one of the major sorrys in /[2jbmwt]/’s Lean development.