repr_of_balanced_factor_pair
plain-language theorem explainer
The theorem shows that a balanced factor pair (d, e) whose defects multiply to the square budget N squared yields a rational Erdős-Straus representation for n. Number theorists reducing the conjecture via ledger identities would cite this algebraic closure step. The proof derives the reciprocal sum by successive linear and nonlinear arithmetic rewrites that isolate the inner product identity and close the ring equation.
Claim. Let $n, x, c, N, d, e, y, z$ be nonzero rationals satisfying $N = n x$, $c = 4x - n$, $d e = N^2$, $c y = N + d$, and $c z = N + e$. Then there exist nonzero rationals $x, y, z$ such that $4/n = 1/x + 1/y + 1/z$.
background
The Erdős-Straus RCL Ledger Reduction module records the algebraic reduction of the conjecture to residual two-denominator splits. HasRationalErdosStrausRepr n asserts the existence of nonzero rationals x, y, z such that 4/n equals the sum of their reciprocals; this is the rational form of the integer problem. After fixing the first denominator x, one sets N = n x and c = 4x - n, then requires the residual equation c/N = 1/y + 1/z to hold via the balanced factor-pair condition (c y - N)(c z - N) = N^2, which is the discrete ledger form of the reciprocal split.
proof idea
The proof first obtains N ≠ 0 from mul_eq_zero applied to hn and hx. It rewrites the defects via linarith to produce hd_eq and he_eq, substitutes into the given product to reach hquad, then applies nlinarith to factor out c and isolate hinner. Field simplification yields the reciprocal sum hsplit; direct substitution and ring simplification produce hfirst. The existential witness is refined and the identity is closed by ring.
why it matters
This supplies the core ledger identity that closes the residual split in the RCL attack on the Erdős-Straus conjecture. It directly feeds repr_of_gate_divisor_pair and repr_of_residual_square inside the same module, and supports balanced_pair_phase_support_gives_repr in the rotation hierarchy file. Within Recognition Science it instantiates the Recognition Composition Law for number-theoretic ledger reductions, advancing the finite reciprocal-pair closure that links to the eight-tick octave and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.