erdos_straus_zero_mod_seven
plain-language theorem explainer
The identity supplies an explicit three-term Egyptian fraction decomposition of 4 divided by 168j plus 49 that holds for every natural number j. Researchers on the Erdős–Straus conjecture cite it to close the n ≡ 0 mod 7 case once n ≡ 1 mod 4 is fixed. The verification proceeds by positivity checks on the three linear denominators, followed by field_simp and ring to confirm the cleared polynomial identity.
Claim. For every natural number $j$, $$4/(168j + 49) = 1/(14(3j + 1)) + 1/(28(24j + 7)(3j + 1)) + 1/(28(24j + 7)(3j + 1)).$$
background
The module supplies explicit Egyptian-fraction identities that close the c = 7 gate of the Erdős–Straus conjecture for the four residue classes n mod 7 in {0, 3, 5, 6}, under the standing hypothesis n ≡ 1 mod 4. These identities extend the earlier c = 3 layer and reduce the remaining search space when combined with higher gates such as c = 11. The present case indexes the arithmetic progression n = 168j + 49 and absorbs the extra factors into the divisor 3j + 1 together with the repeated term involving 24j + 7.
proof idea
The tactic proof first invokes positivity to obtain strict inequalities for 3j + 1, 24j + 7 and 168j + 49, then derives the corresponding non-zero statements via ne_of_gt. It finishes with field_simp to clear the common denominator and ring to verify the resulting polynomial identity.
why it matters
This theorem supplies one of the four parametric closures that together seal the c = 7 gate for n ≡ 1 mod 4. It directly realizes the reduction 4/n = (n + 7)/(n x) with x = (n + 7)/4 for the zero class modulo 7, as described in the module documentation. No downstream uses are recorded, so the lemma functions as a terminal building block inside the number-theoretic scaffolding that shrinks the residual classes of the Erdős–Straus problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.