boxComplement
plain-language theorem explainer
boxComplement returns the complementary divisor e from a DivisorExponentBox point for square budget N squared. Number theorists closing the finite part of the Erdős-Straus conjecture would cite this selector when building balanced residual pairs. It is realized as a direct field projection from the box structure.
Claim. Let $B$ be a divisor exponent box for $N$, consisting of positive integers $d$ and $e$ satisfying $d e = N^2$. The complementary divisor selected by $B$ is the second component $e$.
background
The Erdős-Straus Square-Budget Box Phase module isolates the finite combinatorial part of the residual Erdős-Straus proof. For a square budget $N^2$, a divisor exponent-box point is represented by a complementary pair $(d,e)$ with $d e = N^2$. This encoding chooses exponents $0 ≤ a_p ≤ 2 v_p(N)$ without invoking full factorization API.
proof idea
One-line wrapper that projects the e field of the DivisorExponentBox structure.
why it matters
This definition supplies the complementary divisor required by box_divisor_mul_complement (which recovers the square-budget identity) and by box_phase_hit_gives_balanced_pair (which converts a HitsBalancedPhase witness into BalancedPairPhaseSupport). It therefore feeds the RCL skeleton used in the Erdős-Straus closure. The module documentation states that the pair $(d,e)$ avoids unnecessary factorization overhead in the finite closure lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.