erdos_straus_five_mod_seven
plain-language theorem explainer
The identity supplies an explicit three-term Egyptian fraction decomposition of 4 divided by the linear form 168m + 145, which parametrizes the residue class n ≡ 5 mod 7 under the c = 7 gate. Number theorists studying modular closures of the Erdős-Straus conjecture cite it to eliminate one of the four remaining classes modulo 7 once n ≡ 1 mod 4 is fixed. The proof proceeds by establishing positivity of the three linear denominators, deriving their non-vanishing, then invoking field_simp followed by ring to confirm the cleared polynomial holds.
Claim. For every natural number $m$, $$4/(168m + 145) = 1/(2(21m + 19)) + 1/(6(21m + 19)(8m + 7)) + 1/(3(168m + 145)(21m + 19)(8m + 7)).$$
background
The Erdős-Straus conjecture states that every integer n ≥ 2 admits a representation 4/n = 1/a + 1/b + 1/c with positive integers a, b, c. This module supplies explicit parametric identities that close the c = 7 gate for all n ≡ 1 mod 4 whose residue modulo 7 lies in {0, 3, 5, 6}. The present declaration handles the class n ≡ 5 mod 7 by setting n = 168m + 145 and exhibiting the corresponding three-unit-fraction formula. These closures extend the earlier c = 3 layer and, when combined with higher gates such as c = 11, shrink the set of unresolved residues without eliminating it entirely.
proof idea
The tactic first applies positivity to the three linear expressions 21m + 19, 8m + 7 and 168m + 145, then uses ne_of_gt to obtain the corresponding non-zero facts. field_simp normalizes the rational equation by clearing all denominators, after which ring reduces the resulting polynomial identity to zero.
why it matters
The theorem supplies one of the four explicit closures enumerated in the module documentation for the c = 7 gate. It therefore participates in the systematic reduction of residue classes that the Erdős-Straus problem inherits from lower gates, consistent with the Recognition Science pattern of modular identities that collapse to algebraic tautologies. No downstream theorems are recorded, indicating that the result functions as a terminal closure within the present module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.