Elementary family: five modulo eight

Proved

ErdosStraus242.family_D

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

egyptian-fractionsnumber-theory

For a natural number $n>2$ with $n≡5\pmod8$ , put $u=(n+3)/4$ . Then $1≤ u<nu/2<nu$ and $4/n=1/u+1/(nu/2)+1/(nu)$ in the rationals. The displayed quotients are computed in the natural numbers; the congruence makes both exact.

Preamble

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

Formal statement

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

Source

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

8t+5

identity, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. Reparameterized with

u=2(t+1)

; all divisibility and order conditions 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$ satisfying $2<n$ and having remainder $5$ upon division by $8$ , let $u=\lfloor(n+3)/4\rfloor$ , where this is division in the natural numbers. Then $1\le u$ , $u<\lfloor nu/2\rfloor$ , and $\lfloor nu/2\rfloor<nu$ , and the following equality holds in the rational numbers: $4/n=1/u+1/\lfloor nu/2\rfloor+1/(nu)$ . Here $nu$ is the natural-number product and $\lfloor nu/2\rfloor$ is computed by natural-number division before being used as a rational denominator; all divisions in the rational equality use the natural-number denominators interpreted as rational numbers. The quantification includes $n=5$ , the smallest permitted value, and the asserted inequalities make all three denominators positive and strictly increasing.

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