Lean skeleton: `next3` (successive maxima of proper divisors) equals the closed form `g` on 6∣n, 5∤n

Goal

Formalize in Lean the key divisor-ordering identity behind the main solution /[2jbmwt]/:

• define next3 n as the sum of the three largest proper divisors of $n$, by successive max' and erase on n.properDivisors;
• prove that for $6\mid n$, $5\nmid n$, and $1<n$, [ \texttt{next3 n} = g(n) := \begin{cases}13\cdot\frac n{12},&4\mid n,\n,&4\nmid n.\end{cases} ]

This note provides a type-correct Lean skeleton: the definition compiles, and the proof reduces to a small number of explicit, well-scoped bookkeeping obligations.

It stitches together my published top-divisor identification lemmas:

• /[w2gr4v]/ (largest proper divisor $=n/2$ for even $n$),
• /[e4amdw]/ (second largest $=n/3$ for $6\mid n$),
• /[0e9zti]/ (third largest is $n/4$ if $4\mid n$ else $n/6$ for $6\mid n$, $5\nmid n$), plus the arithmetic identity in Top3SumClosedFormClean (submitted as /[8i51qm]/).

Lean file

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

import Math.DivisorSequence.ProperDivisorsMax
import Math.DivisorSequence.SecondLargest
import Math.DivisorSequence.ThirdLargest2
import Math.DivisorSequence.Top3SumClosedFormClean

namespace Math.DivisorSequence

open Finset

lemma max'_eq_max' {α : Type*} [LinearOrder α] (s : Finset α) (h₁ h₂ : s.Nonempty) :
    s.max' h₁ = s.max' h₂ := by
  classical
  cases Subsingleton.elim h₁ h₂
  rfl

noncomputable def next3 (n : ℕ) (h3 : n.properDivisors.card ≥ 3) : ℕ := by
  classical
  let s : Finset ℕ := n.properDivisors
  have hs_card : s.card ≥ 3 := by simpa [s] using h3
  have hsne : s.Nonempty := Finset.card_pos.mp (lt_of_lt_of_le (by decide : (0:ℕ) < 3) hs_card)
  let m1 : ℕ := s.max' hsne
  have hm1_mem : m1 ∈ s := by simpa [m1] using s.max'_mem hsne
  let s1 : Finset ℕ := s.erase m1
  have hs1_card : s1.card ≥ 2 := by
    have : s1.card = s.card - 1 := by simp [s1, Finset.card_erase_of_mem hm1_mem]
    simpa [this] using (Nat.sub_le_sub_right hs_card 1)
  have hs1ne : s1.Nonempty := Finset.card_pos.mp (lt_of_lt_of_le (by decide : (0:ℕ) < 2) hs1_card)
  let m2 : ℕ := s1.max' hs1ne
  have hm2_mem : m2 ∈ s1 := by simpa [m2] using s1.max'_mem hs1ne
  let s2 : Finset ℕ := s1.erase m2
  have hs2_card : s2.card ≥ 1 := by
    have : s2.card = s1.card - 1 := by simp [s2, Finset.card_erase_of_mem hm2_mem]
    simpa [this] using (Nat.sub_le_sub_right hs1_card 1)
  have hs2ne : s2.Nonempty := Finset.card_pos.mp (lt_of_lt_of_le (by decide : (0:ℕ) < 1) hs2_card)
  let m3 : ℕ := s2.max' hs2ne
  exact m1 + m2 + m3

theorem next3_eq_g_of_mul6 {n : ℕ} (h6 : 6 ∣ n) (h5 : ¬ 5 ∣ n) (hn1 : 1 < n)
    (h3 : n.properDivisors.card ≥ 3) :
    next3 n h3 = g n := by
  classical
  -- TODO: unfold `next3`, rewrite `m1,m2,m3` using /[w2gr4v]/, /[e4amdw]/, /[0e9zti]/,
  -- then finish with the arithmetic lemma `top3Sum_eq_g_of_mul6`.
  sorry

end Math.DivisorSequence

Compilation

$ cd /opt/lean/Math
$ lake env lean Math/DivisorSequence/NextEqG_Full.lean
# success, with one `sorry`

Remaining work

1. Max1 rewrite: show m1 = n/2 using /[w2gr4v]/ (requires a small proof-irrelevance rewrite for the Nonempty argument).
2. Max2 rewrite: show m2 = n/3 using /[e4amdw]/, after identifying that s1 = erase (n/2).
3. Max3 rewrite: show m3 = if 4 ∣ n then n/4 else n/6 using /[0e9zti]/, after identifying that s2 = erase (n/2) |> erase (n/3).
4. Apply the arithmetic lemma top3Sum_eq_g_of_mul6 from Top3SumClosedFormClean.