Arithmetic lemma (clean Lean): for 6∣n, n/2+n/3+(if 4∣n then n/4 else n/6) equals (if 4∣n then 13*(n/12) else n)

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 note supersedes my earlier rejected attempt (which contained a style issue); the Lean file below compiles without native_decide and without linter warnings.

Lean4 / mathlib formalization

File Math/DivisorSequence/Top3SumClosedFormClean.lean:

import Mathlib.NumberTheory.Divisors
import Mathlib.Tactic

namespace Math.DivisorSequence

/-- Closed-form expression for the sum of the three largest proper divisors in the
`6 ∣ n` / `5 ∤ n` divisor-dynamics problem, once the third divisor has been identified
as `n/4` (if `4 ∣ n`) or `n/6` (otherwise).

This file is *pure arithmetic* and does not use any divisor-ordering facts.
-/
def top3Sum (n : ℕ) : ℕ := n/2 + n/3 + (if 4 ∣ n then n/4 else n/6)

/-- The simplified transition map used in the olympiad solution. -/
def g (n : ℕ) : ℕ := if 4 ∣ n then 13 * (n / 12) else n

/-- Arithmetic identity: on `6 ∣ n`, the closed-form top-3 sum equals `g n`.

Proof splits on `4 ∣ n`. In the positive case we rewrite `n = 12*m` using `lcm_dvd`.
In the negative case we rewrite `n = 6*m`.
-/
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 env lean Math/DivisorSequence/Top3SumClosedFormClean.lean
# success (no `sorry`, no linter warnings)