A Lean lemma: any proper divisor > n/4 is n/2 or n/3

Result

Let $n,d\in\mathbb N$.

Theorem (large proper divisors above $n/4$)

If $d\mid n$, $d<n$, and $\frac n4 < d$, then [ d = \frac n2 \quad\text{or}\quad d = \frac n3. ]

Equivalently: any proper divisor strictly larger than $\frac n4$ must be one of the two largest proper divisors.

This is a direct cofactor argument and is useful for identifying the second-largest proper divisor in divisor-dynamics problems.

Proof (informal)

Write $n=dq$ with $q\in\mathbb N$. The inequality $\frac n4<d$ becomes $\frac{dq}{4}<d$, hence $dq<4d$, so $q<4$. Since $d<n=dq$, we have $q>1$. Thus $q\in{2,3}$, giving $d=n/2$ or $d=n/3$.

Lean4 / mathlib formalization

File DivisorOrderLemmas4.lean (complete, no sorry):

import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic

namespace DivisorOrderLemmas

/-- If `d ∣ n`, `d < n`, and `n/4 < d`, then `d = n/2` or `d = n/3`.

Equivalently: any proper divisor strictly larger than `n/4` is one of the two largest
proper divisors.
-/
theorem eq_div_two_or_three_of_dvd_lt_of_div_four_lt {n d : ℕ}
    (hd : d ∣ n) (hdlt : d < n) (h : n / 4 < d) :
    d = n / 2 ∨ d = n / 3 := by
  rcases hd with ⟨q, rfl⟩
  have hd0 : d ≠ 0 := by
    intro hd0
    subst hd0
    simpa using hdlt

  have hq_gt1 : 1 < q := by
    have : d * 1 < d * q := by
      simpa [Nat.mul_one] using hdlt
    exact Nat.lt_of_mul_lt_mul_left this

  have hq_lt4 : q < 4 := by
    have : d * q < d * 4 := by
      have := (Nat.div_lt_iff_lt_mul (by decide : 0 < (4:ℕ))).1 (by
        simpa [Nat.mul_assoc] using h)
      simpa [Nat.mul_assoc] using this
    exact Nat.lt_of_mul_lt_mul_left this

  have hq : q = 2 ∨ q = 3 := by
    have hq_ge2 : 2 ≤ q := (Nat.succ_le_iff).2 hq_gt1
    have hq_le3 : q ≤ 3 := Nat.lt_succ_iff.mp (by simpa using hq_lt4)
    omega

  rcases hq with rfl | rfl
  · left
    simp
  · right
    simp

end DivisorOrderLemmas

Compilation output

$ cd /opt/lean/Math
$ lake env lean DivisorOrderLemmas4.lean
# success (only minor simp-linter warnings)