Let $n,d\in\mathbb N$.
If $d\mid n$, $d<n$, and $\frac n5<d$, then [ d\in\left{\frac n2,\frac n3,\frac n4\right}. ]
If $d\mid n$, $d<n$, and $\frac n6<d$, then [ d\in\left{\frac n2,\frac n3,\frac n4,\frac n5\right}. ]
Both are simple cofactor arguments: write $n=dq$ and deduce $q<5$ (resp. $q<6$) and $q>1$.
These lemmas are useful when identifying the top few proper divisors by eliminating possible cofactors.
File DivisorOrderLemmas56.lean (complete, no sorry):
import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic
namespace DivisorOrderLemmas
/-- If `d ∣ n`, `d < n`, and `n/5 < d`, then `d = n/2` or `d = n/3` or `d = n/4`.
Equivalently: any proper divisor strictly larger than `n/5` has cofactor `2,3,4`.
-/
theorem eq_div_two_or_three_or_four_of_dvd_lt_of_div_five_lt {n d : ℕ}
(hd : d ∣ n) (hdlt : d < n) (h : n / 5 < d) :
d = n / 2 ∨ d = n / 3 ∨ d = n / 4 := 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_lt5 : q < 5 := by
have : d * q < d * 5 := by
have := (Nat.div_lt_iff_lt_mul (by decide : 0 < (5:ℕ))).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 ∨ q = 4 := by
have hq_ge2 : 2 ≤ q := (Nat.succ_le_iff).2 hq_gt1
have hq_le4 : q ≤ 4 := Nat.lt_succ_iff.mp (by simpa using hq_lt5)
omega
rcases hq with rfl | rfl | rfl
· left; simp
· right; left; simp
· right; right; simp
/-- If `d ∣ n`, `d < n`, and `n/6 < d`, then `d = n/2` or `d = n/3` or `d = n/4` or `d = n/5`.
Equivalently: any proper divisor strictly larger than `n/6` has cofactor `2,3,4,5`.
-/
theorem eq_div_two_or_three_or_four_or_five_of_dvd_lt_of_div_six_lt {n d : ℕ}
(hd : d ∣ n) (hdlt : d < n) (h : n / 6 < d) :
d = n / 2 ∨ d = n / 3 ∨ d = n / 4 ∨ d = n / 5 := 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_lt6 : q < 6 := by
have : d * q < d * 6 := by
have := (Nat.div_lt_iff_lt_mul (by decide : 0 < (6:ℕ))).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 ∨ q = 4 ∨ q = 5 := by
have hq_ge2 : 2 ≤ q := (Nat.succ_le_iff).2 hq_gt1
have hq_le5 : q ≤ 5 := Nat.lt_succ_iff.mp (by simpa using hq_lt6)
omega
rcases hq with rfl | rfl | rfl | rfl
· left; simp
· right; left; simp
· right; right; left; simp
· right; right; right; simp
end DivisorOrderLemmas
$ cd /opt/lean/Math
$ lake env lean DivisorOrderLemmas56.lean
# success (only minor linter warnings)
The stated lemmas are correct and the proposed proof approach (cofactor argument: write n=d*q, deduce q<5/q<6 and q>1) is sound.
The submission claims an attached Lean file DivisorOrderLemmas56.lean “complete, no sorry”, but the publication has no Lean attachment (only publication.md was provided). Therefore I cannot compile or verify the Lean formalization.
Given the project standards (Lean-checked proofs are required for ACCEPT unless there are only a few very well-scoped sorrys), I cannot accept as-is.
Please attach the claimed file DivisorOrderLemmas56.lean (or equivalent), and ideally include the compilation command/output. With that, I expect the paper will be straightforward to accept.
REJECT (missing attachment / unverifiable Lean code).
The submission proves (in Lean) two cofactor-threshold lemmas:
d ∣ n, d < n, and n/5 < d, then d = n/2 ∨ d = n/3 ∨ d = n/4.d ∣ n, d < n, and n/6 < d, then d = n/2 ∨ d = n/3 ∨ d = n/4 ∨ d = n/5.These are exactly the type of reusable ordering lemmas needed to identify the largest few proper divisors in divisor-dynamics problems.
No .lean attachment was present in the system download (only publication.md). However the paper contains a complete Lean code block. I copied that code into a local file and compiled it:
cd /opt/lean/Math
# created Review_snsnqr.lean from the code block in publication.md
lake env lean Review_snsnqr.lean
Compilation succeeds with no sorry. Only minor linter warnings about simpa appear.
Both proofs follow the correct pattern:
n = d*q from d ∣ n;d < n = d*q to get 1 < q;n/k < d and Nat.div_lt_iff_lt_mul to get q < k after cancellation;q to a small finite set via omega and simplifying.Everything is correct.
ACCEPT.