Scale a strictly ordered decomposition

Proved

ErdosStraus242.scale_witness

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

egyptian-fractionsnumber-theory

For natural numbers $n,x,y,z,k$ , assume $k>0$ , $1≤ x<y<z$ , and $4/n=1/x+1/y+1/z$ in the rationals. Then $1≤ kx<ky<kz$ and $4/(kn)=1/(kx)+1/(ky)+1/(kz)$ in the rationals.

Preamble

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

Formal statement

namespace ErdosStraus242
theorem scale_witness (n x y z k : ℕ) (hk : 0 < k)
    (hx : 1 ≤ x) (hxy : x < y) (hyz : y < z)
    (h : (4 / n : ℚ) = 1 / x + 1 / y + 1 / z) :
    1 ≤ k*x ∧ k*x < k*y ∧ k*y < k*z ∧
      (4 / (k*n) : ℚ) = 1 / (k*x) + 1 / (k*y) + 1 / (k*z) := by sorry
end ErdosStraus242

Source

Bloom–Elsholtz, Egyptian fractions (2022), p. 239, scaling observation, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf. Explicit witness/order refinement proved locally.

Read-back

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

For every choice of natural numbers $n,x,y,z,k$ , if $k>0$ , $1\le x$ , $x<y$ , $y<z$ , and $\frac{4}{n}=\frac{1}{x}+\frac{1}{y}+\frac{1}{z}$ , then $1\le kx$ , $kx<ky$ , $ky<kz$ , and $\frac{4}{kn}=\frac{1}{kx}+\frac{1}{ky}+\frac{1}{kz}$ . All fractions are interpreted in rational arithmetic, with natural-number denominators embedded in the rationals and division by zero defined to be zero. The quantifier on $n$ includes $n=0$ , but in that case the hypotheses cannot all hold, since the left side of the assumed equality is zero while its right side is positive.

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