box_phase_hit_gives_repr
plain-language theorem explainer
A box phase hit for natural numbers n and c yields a rational Erdős-Straus representation of n. Number theorists studying finite reductions of the Erdős-Straus conjecture cite this combinatorial closure step. The proof is a one-line wrapper that composes the box-to-balanced-pair extraction lemma with the balanced-pair representation theorem.
Claim. If HitsBalancedPhase(n, c) holds, then there exist nonzero rationals x, y, z such that 4/n = 1/x + 1/y + 1/z.
background
The module isolates the finite combinatorial part of the residual Erdős-Straus proof. For a square budget N², a divisor exponent box is represented by a complementary pair (d, e) with d · e = N². This construction avoids unnecessary factorization API overhead in the finite closure lemma. HitsBalancedPhase n c asserts the existence of x, N and such a box where N = n x, c = 4x - n, and c divides both N + d and N + e, ensuring the reciprocal defects land in phase -N modulo c.
proof idea
The proof is a one-line wrapper that applies balanced_pair_phase_support_gives_repr to the BalancedPairPhaseSupport witness produced by box_phase_hit_gives_balanced_pair h.
why it matters
This theorem supplies the rational representation directly from a box phase hit and feeds box_phase_hit_gives_repr_logic together with generated_phase_hit_gives_repr. It completes the finite closure step in the Erdős-Straus square-budget box phase, linking the divisor box structure to the core RCL ledger identity. The result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.