erdos_straus_five_mod_twelve
plain-language theorem explainer
The declaration supplies an explicit three-term unit-fraction decomposition for the rational 4/(12k+5) that satisfies the Erdős-Straus condition for every natural number k. Number theorists examining the conjecture would cite it to cover the residue class n ≡ 5 (mod 12). The proof proceeds by establishing positivity of the three denominators, deriving their non-vanishing, then invoking field simplification and ring normalization to verify the identity.
Claim. For every natural number $k$, $$4/(12k+5)=1/(3k+2)+1/(2(3k+2)(2k+1))+1/(2(12k+5)(3k+2)(2k+1))$$.
background
The module records algebraic reductions for attacking the Erdős-Straus conjecture via the Recognition Composition Law ledger. After selecting the first denominator x, the residual equation becomes c/N = 1/y + 1/z where c = 4x - n and N = n x. Clearing denominators yields the balanced factor-pair condition (c y - N)(c z - N) = N², the discrete form of the reciprocal split. This theorem handles the case n = 12k + 5 by taking the gate-3 divisor pair with d = 3k + 2. The upstream results supply structural properties from the meta-realization axioms and an explicit log-derivative bound for phase lifting on the circle.
proof idea
The proof first asserts positivity of the three denominators 3k+2, 2k+1 and 12k+5. It derives their non-vanishing from these inequalities. It then applies field_simp to clear the rational equation and ring to confirm the resulting polynomial identity.
why it matters
This result supplies the rational identity needed for the natural-number version erdos_straus_nat_five_mod_twelve, which asserts existence of positive integers x, y, z satisfying the three-term decomposition for every n = 12k + 5. It forms part of the systematic case analysis modulo 12 in the RCL attack on the Erdős-Straus conjecture. The approach ties into the Recognition Composition Law by reducing the reciprocal split to a balanced factor pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.