HasRationalErdosStrausRepr
plain-language theorem explainer
Defines the predicate that a rational n admits a rational Erdős-Straus representation when 4/n equals the sum of three nonzero rational reciprocals. Number theorists extending the conjecture via ledger reductions would cite this to lift the integer case. It is introduced as the direct existential statement over the denominators after the first split.
Claim. A rational number $n$ has a rational Erdős-Straus representation if there exist nonzero rationals $x,y,z$ such that $4/n = 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 = nx$. Clearing denominators produces the balanced factor-pair condition $(cy - N)(cz - N) = N^2$, the discrete ledger form of the reciprocal split.
proof idea
As a definition it directly encodes the existential condition for the three-term unit-fraction sum. No lemmas or tactics are applied; the body is the unfolded Prop statement.
why it matters
This predicate is the target of closure results such as box_phase_hit_gives_repr and erdos_straus_residual_from_effectivePrimePhaseInput. It encodes the core ledger identity for the residual two-denominator split and advances the RCL attack on the Erdős-Straus conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.