repr_of_residual_square
plain-language theorem explainer
This theorem shows that a nonzero rational n admits a rational Erdős-Straus representation once nonzero y and z are found whose residual defects multiply exactly to N squared. Algebraic number theorists reducing the conjecture via ledger splits would cite the result. The proof is a one-line wrapper that invokes the balanced factor pair lemma and discharges the two auxiliary conditions by ring normalization.
Claim. Let $n,x,c,N,y,z$ be nonzero rationals with $N=nx$ and $c=4x-n$. If $(cy-N)(cz-N)=N^2$, then there exist nonzero rationals $x',y',z'$ such that $4/n=1/x'+1/y'+1/z'$.
background
The module records the algebraic reduction of the Erdős-Straus conjecture inside the Recognition Composition Law ledger. After fixing the first denominator $x$, the residual equation becomes $c/N=1/y+1/z$ with $c=4x-n$ and $N=nx$. Clearing denominators produces the balanced factor-pair identity $(cy-N)(cz-N)=N^2$, which is the discrete ledger form of the reciprocal split. HasRationalErdosStrausRepr n is the statement that $4/n$ equals the sum of three nonzero rational reciprocals. The upstream balanced ledger definition from LedgerForcing supplies the structural invariance that every ledger event list is balanced by construction.
proof idea
The proof is a term-mode one-line wrapper. It refines the sibling lemma repr_of_balanced_factor_pair by substituting the concrete defects $d=cy-N$ and $e=cz-N$, passes the given hypotheses hn,hx,hc,hy,hz,hN,hcdef,hres, and discharges the two remaining subgoals by the ring tactic.
why it matters
The declaration supplies one concrete reduction step in the RCL ledger attack on the Erdős-Straus conjecture. It feeds the module's other representation theorems that convert the factor-pair condition into an explicit three-term sum. Within the Recognition Science framework it instantiates the Recognition Composition Law identity J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y) at the level of residual defects, closing one link in the forcing chain from T5 J-uniqueness to the discrete ledger form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.