Elementary family: three modulo four

Proved

ErdosStraus242.family_C

by alexcarter · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

egyptian-fractionsnumber-theory

For a natural number $n>2$ with $n≡3\pmod4$ , put $u=(n+1)/4$ and $t=nu$ . Then $1≤ u<t+1<t(t+1)$ and $4/n=1/u+1/(t+1)+1/(t(t+1))$ in the rationals. The quotient defining $u$ is exact.

Preamble

import Definitions.Def_ErdosStraus242
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Finset.Insert

Formal statement

namespace ErdosStraus242
theorem family_C (n : ℕ) (hn : 2 < n) (hmod : n % 4 = 3) :
    let u := (n+1)/4
    let t := n*u
    1 ≤ u ∧ u < t+1 ∧ t+1 < t*(t+1) ∧
      (4 / n : ℚ) = 1 / u + 1 / (t+1 : ℕ) + 1 / (t*(t+1) : ℕ) := by sorry
end ErdosStraus242

Source

Bloom–Elsholtz (2022), p. 239, the

3\pmod4

two-term identity, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf, followed by the independently verified splitting

1/t=1/(t+1)+1/(t(t+1))

. Distinct refinement proved locally.

Read-back

What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)

For every natural number $n$ such that $n>2$ and the remainder of $n$ upon division by $4$ is $3$ , let $u=\lfloor(n+1)/4\rfloor$ , where this quotient is computed by natural-number division, and let $t=nu$ . Then $1\le u$ , $u<t+1$ , and $t+1<t(t+1)$ , and the rational-number identity $\frac{4}{n}=\frac{1}{u}+\frac{1}{t+1}+\frac{1}{t(t+1)}$ holds, with all natural-number denominators interpreted as rational numbers in the fractions. The hypotheses exclude $n=0,1,2$ and include $n=3$ , for which the three denominators are $1,4,12$ ; the asserted inequalities ensure that all three denominators are positive and pairwise distinct, so no division by zero occurs.

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by alexcarter · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph