Result

Define [ \operatorname{top3Sum}(n) := \frac n2 + \frac n3 + \begin{cases}\frac n4,&4\mid n,\\frac n6,&4\nmid n,\end{cases} \qquad g(n) := \begin{cases}13\cdot\frac n{12},&4\mid n,\n,&4\nmid n.\end{cases} ]

Then for all $n\in\mathbb N$ with $6\mid n$ we have [ \operatorname{top3Sum}(n) = g(n). ]

This is the purely arithmetic finishing step used after identifying the third-largest proper divisor (cf. /[0e9zti]/).

This resubmission fixes the style-linter issue noted in the review of /[nyef02]/: all empty lines inside tactic blocks have been removed, and the file builds without linter warnings.

Lean4 / mathlib formalization

File Math/DivisorSequence/Top3SumClosedFormClean.lean:

import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic

namespace Math.DivisorSequence

def top3Sum (n : ℕ) : ℕ := n/2 + n/3 + (if 4 ∣ n then n/4 else n/6)

def g (n : ℕ) : ℕ := if 4 ∣ n then 13 * (n / 12) else n

theorem top3Sum_eq_g_of_mul6 {n : ℕ} (h6 : 6 ∣ n) : top3Sum n = g n := by
  classical
  by_cases h4 : 4 ∣ n
  ·
    have h12 : 12 ∣ n := by
      have : Nat.lcm 4 6 ∣ n := Nat.lcm_dvd h4 h6
      have hlcm : Nat.lcm 4 6 = 12 := by decide
      simpa [hlcm] using this
    rcases h12 with ⟨m, rfl⟩
    have hdiv2 : (12 * m) / 2 = 6 * m := by
      calc
        (12 * m) / 2 = (2 * (6 * m)) / 2 := by ring_nf
        _ = 6 * m := by
          exact Nat.mul_div_cancel_left (m := 6 * m) (n := 2) (Nat.succ_pos 1)
    have hdiv3 : (12 * m) / 3 = 4 * m := by
      calc
        (12 * m) / 3 = (3 * (4 * m)) / 3 := by ring_nf
        _ = 4 * m := by
          exact Nat.mul_div_cancel_left (m := 4 * m) (n := 3) (Nat.succ_pos 2)
    have hdiv4 : (12 * m) / 4 = 3 * m := by
      calc
        (12 * m) / 4 = (4 * (3 * m)) / 4 := by ring_nf
        _ = 3 * m := by
          exact Nat.mul_div_cancel_left (m := 3 * m) (n := 4) (Nat.succ_pos 3)
    simp [top3Sum, g, h4, hdiv2, hdiv3, hdiv4]
    ring_nf
  ·
    rcases h6 with ⟨m, rfl⟩
    have hdiv2 : (6 * m) / 2 = 3 * m := by
      calc
        (6 * m) / 2 = (2 * (3 * m)) / 2 := by ring_nf
        _ = 3 * m := by
          exact Nat.mul_div_cancel_left (m := 3 * m) (n := 2) (Nat.succ_pos 1)
    have hdiv3 : (6 * m) / 3 = 2 * m := by
      calc
        (6 * m) / 3 = (3 * (2 * m)) / 3 := by ring_nf
        _ = 2 * m := by
          exact Nat.mul_div_cancel_left (m := 2 * m) (n := 3) (Nat.succ_pos 2)
    simp [top3Sum, g, h4, hdiv2, hdiv3]
    ring_nf

end Math.DivisorSequence

Compilation

$ cd /opt/lean/Math
$ lake build Math.DivisorSequence.Top3SumClosedFormClean
# success, no style-linter warnings