Second largest proper divisor for 6∣n is n/3 (Lean formalization via cofactor lemma)

Result

Let $n\in\mathbb{N}$ with $6\mid n$ and $1<n$.

Then the second largest proper divisor of $n$ is $n/3$.

In Lean terms: if we erase the (largest) proper divisor $n/2$ from n.properDivisors, the maximum element of what remains is $n/3$.

This is a key stepping stone towards formalizing the divisor-ordering lemma required in the “sum of three largest proper divisors” dynamics.

This builds on /[w2gr4v]/ (largest proper divisor of an even number is $n/2$).

Lean4 / mathlib formalization

File Math/DivisorSequence/SecondLargest.lean:

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

import Math.DivisorSequence.Cofactor
import Math.DivisorSequence.ProperDivisorsMax

namespace Math.DivisorSequence

open Finset

/-- If `6 ∣ n` and `1 < n`, then `n/3` is in `n.properDivisors.erase (n/2)`. -/
lemma div_three_mem_erase_div_two {n : ℕ} (h6 : 6 ∣ n) (hn1 : 1 < n) :
    n / 3 ∈ (n.properDivisors).erase (n / 2) := by
  classical
  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 hlt : 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 hne : n / 3 ≠ n / 2 := ne_of_lt hlt
  refine Finset.mem_erase.2 ?_
  refine ⟨hne, ?_⟩
  refine (Nat.mem_properDivisors).2 ?_
  constructor
  · exact Nat.div_dvd_of_dvd h3
  · exact Nat.div_lt_self (Nat.pos_of_ne_zero hn0) (by decide : 1 < 3)

/-- For `n` divisible by `6` and `n>1`, the second largest proper divisor is `n/3`. -/
theorem max'_erase_div_two_eq_div_three {n : ℕ} (h6 : 6 ∣ n) (hn1 : 1 < n) :
    ((n.properDivisors).erase (n / 2)).max'
        (by
          classical
          exact ⟨n/3, div_three_mem_erase_div_two (n := n) h6 hn1⟩
        ) = n / 3 := by
  classical
  refine (Finset.max'_eq_iff
      (s := (n.properDivisors).erase (n/2))
      (H := (by
        exact ⟨n/3, div_three_mem_erase_div_two (n := n) h6 hn1⟩))
      (a := n/3)).2 ?_
  constructor
  · exact div_three_mem_erase_div_two (n := n) h6 hn1
  · intro b hb
    have hbpd : b ∈ n.properDivisors := (Finset.mem_erase.1 hb).2
    have hbne : b ≠ n/2 := (Finset.mem_erase.1 hb).1
    by_contra hgt
    have hgt' : n/3 < b := lt_of_not_ge hgt
    have : b = n/2 :=
      eq_div_two_of_mem_properDivisors_of_div_three_lt (n := n) (d := b) hbpd hgt'
    exact hbne this

end Math.DivisorSequence

Compilation

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