erdos_straus_three_mod_seven
plain-language theorem explainer
The identity equates 4 over the linear form 168m + 73 to an explicit sum of three rational terms, furnishing a parametric Egyptian-fraction decomposition for the residue class three modulo seven inside the c = 7 gate. Number theorists studying modular closures of the Erdős-Straus conjecture would cite it together with the sibling identities for the remaining classes zero, five, and six. The verification proceeds by positivity assertions on the three linear factors, extraction of non-vanishing statements, followed by field_simp and ring.
Claim. For every natural number $m$, $$4/(168m + 73) = 1/(2(21m + 10)) + 1/(3(21m + 10)(16m + 7)) + 1/(6(168m + 73)(21m + 10)(16m + 7))$$.
background
The Erdős-Straus conjecture asserts that 4/n admits a representation as a sum of three unit fractions for every natural n. The module supplies four parametric identities that close the residue classes n mod 7 belonging to {0, 3, 5, 6} whenever n ≡ 1 mod 4, thereby extending the earlier c = 3 closure layer. Each identity is obtained by substituting a linear parameterization of n that aligns the extra factors with the modular divisor, after which the expression collapses to the tautology 4/n = 4/n.
proof idea
The tactic proof first applies positivity to obtain strict inequalities for the three linear forms 21m + 10, 16m + 7, and 168m + 73. It then uses ne_of_gt to produce the corresponding non-zero statements. With these hypotheses available, field_simp clears all denominators and ring reduces the resulting polynomial equation to an identity.
why it matters
The declaration supplies one of the four explicit closures enumerated in the module documentation for the c = 7 gate. Together with its siblings it reduces the unresolved residue classes modulo 7 under the n ≡ 1 mod 4 hypothesis, advancing the program of shrinking the exceptional set by successive modular gates. The result bears on the open question whether finitely many such gates suffice to cover all n.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.