erdos_straus_thirteen_mod_twentyfour
plain-language theorem explainer
The declaration supplies an explicit three-term Egyptian fraction decomposition of 4/n for every n of the form 24m + 13, realizing the balanced factor-pair condition of the Recognition Composition Law ledger. Number theorists studying the Erdős-Straus conjecture would cite this identity to cover the residue class 13 modulo 24. The proof proceeds by establishing positivity of all denominators, then applying field_simp followed by ring normalization to verify the rational equality.
Claim. For every natural number $m$, let $n = 24m + 13$ and $A = n(3m + 2)$. Then $$4/n = 1/(6m + 4) + 3/(2(A + 1)) + 3/(2A(A + 1)).$$
background
The module records algebraic reductions for the Erdős-Straus conjecture inside the Recognition Composition Law ledger. After selecting the first denominator x the residual equation is c/N = 1/y + 1/z with c = 4x - n and N = nx; clearing denominators produces the balanced factor-pair condition (c y - N)(c z - N) = N^2, the discrete ledger form of the reciprocal split. Upstream results supply the active edge count A (set to 1) and the identity event at zero J-cost, providing the broader Recognition Science context in which these number-theoretic identities are embedded.
proof idea
The tactic proof first uses positivity to obtain strict inequalities for the three linear expressions 6m + 4, 3m + 2 and 24m + 13 together with their products. It then invokes field_simp to clear all denominators and ring to confirm the resulting polynomial identity.
why it matters
This theorem supplies one modular case in the RCL attack on the Erdős-Straus conjecture, parallel to the sibling identities for five and nine modulo twelve. It advances the ledger-reduction program described in the module doc-comment by furnishing an explicit representation when (n + 3)/4 is even. The result sits inside the Recognition Science framework that derives all physics from the single functional equation and the eight-tick octave, though it does not yet close the full conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.