repr_of_gate_divisor_pair
plain-language theorem explainer
The theorem shows that nonzero rationals n, x, c, N, d, q satisfying N = n x, x = (n + c)/4, d q = N, and the two specified denominators nonzero imply that n admits a rational Erdős-Straus representation. Number theorists reducing the conjecture via RCL ledger splits would cite this for arbitrary residual gates. The proof derives the balanced factor-pair identity d (N q) = N^2 and applies the sibling lemma on balanced factor pairs after two field simplifications.
Claim. Let $n, x, c, N, d, q$ be nonzero rationals satisfying $N = n x$, $x = (n + c)/4$, $d q = N$, $(N + d)/c ≠ 0$, and $(N + N q)/c ≠ 0$. Then there exist nonzero rationals $x', y', z'$ such that $4/n = 1/x' + 1/y' + 1/z'$.
background
In the Erdős-Straus RCL Ledger Reduction the residual equation after the first denominator x 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^2, the discrete ledger form of the reciprocal split. HasRationalErdosStrausRepr n is the statement that such nonzero rationals x, y, z exist with 4/n equal to the sum of their reciprocals.
proof idea
The proof first obtains c = 4x - n by rewriting the definition of x and simplifying. It then records d (N q) = N^2 from the divisor hypothesis. It refines directly to the balanced factor pair lemma, supplying y = (N + d)/c and z = (N + N q)/c, and discharges the two remaining nonzeroness conditions by field_simp.
why it matters
This supplies the general residual-gate divisor split that feeds repr_c3_of_divisor_pair for the dominant c = 3 hard-class case and gate_closure_witness_gives_repr in the rotation hierarchy. It advances the algebraic ledger attack on the Erdős-Straus conjecture inside the Recognition Science framework, where the RCL governs defect composition and the balanced factor-pair condition encodes the reciprocal split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.