erdos_straus_nat_nine_mod_twelve
plain-language theorem explainer
The theorem asserts that every natural number of the form 12k + 9 admits positive integers x, y, z satisfying 4/n = 1/x + 1/y + 1/z. Number theorists studying the Erdős-Straus conjecture would cite this as a verified case for the residue class 9 mod 12. The proof constructs explicit denominators and reduces the natural-number identity to the rational version via casting and ring normalization.
Claim. For every natural number $k$, there exist positive integers $x, y, z$ such that $$4/(12k + 9) = 1/x + 1/y + 1/z.$$
background
The module records algebraic reductions for attacking the Erdős-Straus conjecture via the Recognition Composition Law ledger. After selecting the first denominator, 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², the discrete ledger form of the reciprocal split.
proof idea
The tactic proof refines explicit positive integers x = 3k + 3 and y = z = 6(4k + 3)(k + 1). It invokes the sibling rational lemma erdos_straus_nine_mod_twelve, casts the denominator to equate natural and rational forms, applies push_cast and ring, then converts the identities.
why it matters
This result fills the n ≡ 9 mod 12 case in the RCL ledger reduction of the Erdős-Straus conjecture and supports the discrete c = 3 divisor sufficiency for sub-residue classes. It advances the algebraic attack using the composition law within the Recognition Science framework, though no downstream applications are recorded. It touches the open question of full coverage for all positive integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.