IndisputableMonolith.NumberTheory.Erdos_C7_Closure
This module closes the Erdős–Straus conjecture for the residue classes 0, 3, 5, and 6 modulo 7 by supplying explicit positive integers a, b, c satisfying 4/n = 1/a + 1/b + 1/c in each case. Number theorists formalizing Diophantine decompositions in Lean would cite these four theorems to cover the listed congruences. The module consists of four independent sibling declarations with no shared central argument.
claimFor each $k$ in the set {0, 3, 5, 6}, the module proves that every integer $n ≥ 2$ satisfying $n ≡ k mod 7$ admits positive integers $a, b, c$ such that $4/n = 1/a + 1/b + 1/c$.
background
The module IndisputableMonolith.NumberTheory.Erdos_C7_Closure resides in the NumberTheory domain and imports only Mathlib. It addresses the Erdős–Straus conjecture asserting that 4/n is the sum of three unit fractions for every integer n ≥ 2. The four sibling theorems handle the congruence classes n mod 7 in {0, 3, 5, 6} via direct constructions, with no upstream dependencies listed.
proof idea
The module structures its content as four separate theorems, one per residue class (six, zero, five, three mod seven). Each theorem proceeds by exhibiting explicit formulas for a, b, c in terms of n and verifying the target equation through algebraic identities or direct computation.
why it matters in Recognition Science
These results close the C7 cases of the Erdős–Straus conjecture and serve as a building block toward a complete formal proof of the statement. In the Recognition Science setting they supply modular number-theoretic facts that may later connect to the phi-ladder or J-cost constructions, although no downstream uses are recorded yet.
scope and limits
- Does not cover residue classes 1, 2, or 4 modulo 7.
- Does not establish the full Erdős–Straus conjecture for all n.
- Contains no asymptotic estimates or complexity bounds.
- Depends only on Mathlib and performs no cross-module reductions.