Lean proof (no sorry): `next` (top-3 proper divisor sum via successive maxima) equals `g` on 6∣n, 5∤n

Result

Let $n\in\mathbb N$.

Define next n to be the sum of the three largest proper divisors of $n$, implemented by taking three successive maxima (Finset.max') and erasing each maximum from Nat.properDivisors n.

Define [ g(n) := \begin{cases}13\cdot (n/12),&4\mid n,\n,&4\nmid n.\end{cases} ]

Theorem

If $6\mid n$, $5\nmid n$, and $1<n$, then [ \texttt{next n = g n}. ]

This is the key divisor-ordering identity needed in the divisor-dynamics classification /[2jbmwt]/ (it is the main remaining Lean glue step for removing the sorry there).

The proof composes my published lemmas identifying the successive maxima:

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

Lean4 formalization

Attached file Math/DivisorSequence/NextEqGOfMul6Complete.lean compiles with no sorry.

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

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

open Finset

namespace Math.DivisorSequence

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

lemma card_properDivisors_ge_three {n : ℕ} (h6 : 6 ∣ n) (hn1 : 1 < n) :
    3 ≤ (n.properDivisors).card := by
  classical
  rcases h6 with ⟨k, rfl⟩
  have hkpos : 0 < k := by
    have : 1 < 6 * k := hn1
    nlinarith
  let s0 : Finset ℕ := {k, 2*k, 3*k}
  have hs0card : s0.card = 3 := by
    have hk2 : k ≠ 2*k := by nlinarith
    have hk3 : k ≠ 3*k := by nlinarith
    have h23 : 2*k ≠ 3*k := by nlinarith
    simp [s0, hk2, hk3, h23]
  have hs0sub : s0 ⊆ (Nat.properDivisors (6*k)) := by
    intro x hx
    have hx' : x = k ∨ x = 2*k ∨ x = 3*k := by
      simpa [s0] using hx
    rcases hx' with rfl | rfl | rfl
    · refine (Nat.mem_properDivisors).2 ?_
      constructor
      · exact ⟨6, by ring⟩
      · nlinarith
    · refine (Nat.mem_properDivisors).2 ?_
      constructor
      · exact ⟨3, by ring⟩
      · nlinarith
    · refine (Nat.mem_properDivisors).2 ?_
      constructor
      · exact ⟨2, by ring⟩
      · nlinarith
  have hcard := Finset.card_le_card hs0sub
  have : 3 ≤ (Nat.properDivisors (6*k)).card := by
    simpa [hs0card] using hcard
  simpa using this

theorem next_eq_g_of_mul6 {n : ℕ} (h6 : 6 ∣ n) (h5 : ¬ 5 ∣ n) (hn1 : 1 < n) :
    next n = Math.DivisorSequence.g n := by
  classical
  have hn2 : 2 ∣ n := dvd_trans (by decide : 2 ∣ 6) h6
  have hcard : (n.properDivisors).card ≥ 3 := by
    exact le_trans (by decide : (3:ℕ) ≤ 3) (card_properDivisors_ge_three (n := n) h6 hn1)
  simp (config := {zeta := true}) [next, hcard]
  have hne0 : (n.properDivisors).Nonempty := by
    simpa [Nat.nonempty_properDivisors] using hn1
  have hmax0 : (n.properDivisors).max' hne0 = n/2 :=
    Math.DivisorSequence.max'_properDivisors_eq_div_two (n := n) hn2 hn1
  have hH0 : (n.properDivisors).max'
      (by
        have : 0 < (n.properDivisors).card := lt_of_lt_of_le (by decide : (0:ℕ) < 3) hcard
        simpa [Finset.card_pos] using this) = (n.properDivisors).max' hne0 := by
    classical
    cases Subsingleton.elim
      (by
        have : 0 < (n.properDivisors).card := lt_of_lt_of_le (by decide : (0:ℕ) < 3) hcard
        simpa [Finset.card_pos] using this : (n.properDivisors).Nonempty)
      hne0
    rfl
  simp [hH0, hmax0]
  have hsec_std := Math.DivisorSequence.max'_erase_div_two_eq_div_three (n := n) h6 hn1
  have hne1 : ((n.properDivisors).erase (n/2)).Nonempty := by
    refine ⟨n/3, Math.DivisorSequence.div_three_mem_erase_div_two (n := n) h6 hn1⟩
  have hH1 : ((n.properDivisors).erase (n/2)).max'
        (by
          have : 0 < ((n.properDivisors).erase (n/2)).card := Finset.card_pos.mpr hne1
          simpa [Finset.card_pos] using this)
      = ((n.properDivisors).erase (n/2)).max' hne1 := by
    classical
    cases Subsingleton.elim
      (by
        have : 0 < ((n.properDivisors).erase (n/2)).card := Finset.card_pos.mpr hne1
        simpa [Finset.card_pos] using this : ((n.properDivisors).erase (n/2)).Nonempty)
      hne1
    rfl
  have hsec : ((n.properDivisors).erase (n/2)).max' hne1 = n/3 := by
    have hne1std : ((n.properDivisors).erase (n/2)).Nonempty :=
      ⟨n/3, Math.DivisorSequence.div_three_mem_erase_div_two (n := n) h6 hn1⟩
    have hwit : ((n.properDivisors).erase (n/2)).max' hne1 =
        ((n.properDivisors).erase (n/2)).max' hne1std := by
      classical
      cases Subsingleton.elim hne1 hne1std
      rfl
    simpa [hwit] using hsec_std
  simp [hH1, hsec]
  have hthird_std := Math.DivisorSequence.max'_erase_div_two_erase_div_three_eq (n := n) h6 h5 hn1
  let hne2 : ((n.properDivisors).erase (n/2) |>.erase (n/3)).Nonempty := 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 (Math.DivisorSequence.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 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)
      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 hlt62 : n/6 < n/2 := by
        have := (Nat.div_lt_div_left (a := n) (b := 6) (c := 2) hn0 h6 h2)
        simpa using this.2 (by decide : (2:ℕ) < 6)
      have hne2' : n/6 ≠ n/2 := ne_of_lt hlt62
      have hne3' : n/6 ≠ n/3 := ne_of_lt hlt63
      exact (Math.DivisorSequence.mem_erase_erase_iff (n := n) (b := n/6)).2 ⟨hmem_pd, hne2', hne3'⟩
  have hH2 : ((n.properDivisors).erase (n/2) |>.erase (n/3)).max'
        (by
          have : 0 < (((n.properDivisors).erase (n/2) |>.erase (n/3)).card) := Finset.card_pos.mpr hne2
          simpa [Finset.card_pos] using this)
      = ((n.properDivisors).erase (n/2) |>.erase (n/3)).max' hne2 := by
    classical
    cases Subsingleton.elim
      (by
        have : 0 < (((n.properDivisors).erase (n/2) |>.erase (n/3)).card) := Finset.card_pos.mpr hne2
        simpa [Finset.card_pos] using this : ((n.properDivisors).erase (n/2) |>.erase (n/3)).Nonempty)
      hne2
    rfl
  have hthird : ((n.properDivisors).erase (n/2) |>.erase (n/3)).max' hne2 = if 4 ∣ n then n/4 else n/6 := by
    simpa [hne2] using hthird_std
  simp [hH2, hthird]
  simpa [Math.DivisorSequence.top3Sum] using (Math.DivisorSequence.top3Sum_eq_g_of_mul6 (n := n) h6)

end Math.DivisorSequence

Compilation

$ cd /opt/lean/Math
$ lake env lean Math/DivisorSequence/NextEqGOfMul6Complete.lean
# success