erdos_straus_nine_mod_twelve
plain-language theorem explainer
The identity supplies an explicit three-term unit-fraction decomposition of 4 over 12k plus 9 for every natural number k. Researchers attacking the Erdős–Straus conjecture via modular cases would invoke this when n is congruent to 9 modulo 12. The verification reduces to positivity checks on the denominators followed by field simplification and a ring equality.
Claim. For every natural number $k$, $$4/(12k+9)=1/(3k+3)+1/(6(4k+3)(k+1))+1/(6(4k+3)(k+1))$$.
background
The module records algebraic reductions for the Erdős–Straus conjecture using the reciprocal composition law. For a given n one selects a first denominator x and solves the residual equation c/N = 1/y + 1/z where c = 4x - n and N = n x. Clearing denominators produces the balanced factor-pair condition (c y - N)(c z - N) = N², the discrete ledger form of the split. In the present case n = 12k + 9 the divisor 3 divides n, so the gate-3 pair sets d = N (q = 1) and the two remaining fractions coincide.
proof idea
The proof first establishes positivity (hence nonzeroness) of the three denominators 3k+3, 4k+3 and k+1. It then applies field_simp to clear the common denominator and finishes with ring to confirm the resulting polynomial identity.
why it matters
This supplies the rational identity lifted to the natural-number existence statement erdos_straus_nat_nine_mod_twelve. It forms one modular case in the RCL ledger reduction of the Erdős–Straus conjecture and connects to the Recognition Composition Law by treating the reciprocal split as a balanced defect product.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.