Three soluble congruence classes modulo eleven with distinct denominators

Proved

ErdosStraus242.family_mod11

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

congruencesegyptian-fractionsnumber-theory

For every natural number $n>2$ with $n\bmod11\in\{7,8,10\}$ , there are natural numbers $1\le x<y<z$ such that $4/n=1/x+1/y+1/z$ in $\mathbb Q$ .

This is an explicit specialization of the Bloom–Elsholtz parametrization on p. 239. For $n=11k+7$ , take $(3k+2,3n,3(3k+2)n)$ . For $n=11k+8$ with $k\ge3$ , take $(3(k+1),3n,(k+1)n)$ . For $n=11k+10$ with $k\ge1$ , take $(3(k+1),3n,3(k+1)n)$ . The finitely many smaller inputs have explicit distinct witnesses. This family gives a further congruence sieve within the mission's six residual classes modulo $840$ .

Preamble

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

Formal statement

namespace ErdosStraus242
theorem family_mod11 (n : ℕ) (hn : 2 < n)
    (hmod : n % 11 ∈ ({7, 8, 10} : Finset ℕ)) : IsErdosStraus n := by sorry
end ErdosStraus242

Source

Bloom and Elsholtz, Egyptian fractions, Nieuw Archief voor Wiskunde 5/23 no. 4 (2022), p. 239, the displayed identity following c*n+a=(4*a*c*d-1)*b: 4/n=1/(a*b*d)+1/(a*c*d*n)+1/(b*c*d*n). https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. Specialize (a,c,d) to (1,3,1), (3,1,1), and (1,1,3). The source identity is retained exactly; the explicit ordering checks and small-boundary witnesses are supplied in this formalization.

View graph