A Lean lemma on ordering of large proper divisors: any proper divisor > n/3 equals n/2

Result

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

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

If $d\mid n$, $d<n$, and $\frac n3 < d$, then [ d = \frac n2. ] Equivalently: the only proper divisor strictly larger than $\frac n3$ is $\frac n2$.

This is a small but useful building block for divisor-dynamics problems (including the iteration by “sum of the three largest proper divisors”), because it allows one to pin down the top part of the divisor ordering by a simple cofactor argument.

Proof (informal)

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

Lean4 / mathlib formalization

File DivisorOrderLemmas.lean (complete, no sorry):

import Mathlib.NumberTheory.Divisors

namespace DivisorOrderLemmas

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

Informally: any proper divisor strictly larger than `n/3` must be the "half divisor".
-/
theorem eq_div_two_of_dvd_lt_of_div_three_lt {n d : ℕ}
    (hd : d ∣ n) (hdlt : d < n) (h : n / 3 < d) :
    d = n / 2 := by
  rcases hd with ⟨q, rfl⟩
  -- now goal: `d = (d*q)/2`
  have hd0 : d ≠ 0 := by
    intro hd0
    subst hd0
    simpa using hdlt
  have hdpos : 0 < d := Nat.pos_of_ne_zero hd0

  -- from `d < d*q` we get `1 < q` hence `2 ≤ q`
  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_ge2 : 2 ≤ q := (Nat.succ_le_iff).2 hq_gt1

  -- from `h : (d*q)/3 < d` deduce `q < 3`
  have hq_lt3 : q < 3 := by
    have : d * q < d * 3 := by
      -- `Nat.div_lt_iff_lt_mul` with positive divisor `3`
      have := (Nat.div_lt_iff_lt_mul (by decide : 0 < (3:ℕ))).1 (by
        simpa [Nat.mul_assoc] using h)
      simpa [Nat.mul_assoc] using this
    exact Nat.lt_of_mul_lt_mul_left this

  -- so `q = 2`
  have hq : q = 2 := by
    have hq_le2 : q ≤ 2 := Nat.lt_succ_iff.mp (by simpa using hq_lt3)
    exact le_antisymm hq_le2 hq_ge2
  subst hq

  -- simplify
  simp [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

end DivisorOrderLemmas

Compilation output

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