erdos_straus_nat_five_mod_twelve
plain-language theorem explainer
Every integer of the form 12k + 5 admits an explicit Erdős-Straus decomposition into three positive unit fractions. Number theorists examining the Erdős-Straus conjecture would cite this closed-form solution for the residue class 5 mod 12. The proof supplies concrete positive integer values for the denominators and reduces the statement to the rational case by casting and conversion.
Claim. For every natural number $k$, there exist positive integers $x, y, z$ such that $4/(12k + 5) = 1/x + 1/y + 1/z$.
background
The module records the algebraic reduction behind the RCL attack on the Erdős-Straus conjecture. After choosing the first denominator $x$, the residual equation is $c/N = 1/y + 1/z$, with $c = 4x - n$ and $N = n x$. Clearing denominators produces the balanced factor-pair condition $(c y - N)(c z - N) = N^2$, the discrete ledger form of the reciprocal split.
proof idea
The tactic proof refines the existential with explicit positive integers for the three denominators. It invokes the upstream rational identity for the residue class 5 mod 12, casts the natural number $12k + 5$ to a rational, and applies convert to align the sides.
why it matters
This declaration completes the natural-number case for the residue class 5 mod 12 in the Erdős-Straus RCL ledger reduction. It supports the algebraic attack on the conjecture described in the module documentation. No immediate downstream theorems depend on it, indicating it functions as a terminal explicit construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.