boxComplement
plain-language theorem explainer
boxComplement extracts the complementary divisor e from a divisor-exponent box point for square budget N squared. Number theorists closing the Erdős-Straus conjecture via finite phase conditions cite this selector to obtain the second leg of a balanced pair. The definition is realized as a direct field projection on the box structure.
Claim. Let $(d,e)$ be a divisor-exponent box for square budget $N^2$, so $d,e>0$ and $d·e=N^2$. The complementary divisor selected by the box is $e$.
background
The Erdős-Straus square-budget box phase module isolates the finite combinatorial part of the residual Erdős-Straus proof. A divisor exponent box is a structure holding a divisor d and its complement e with d·e=N² together with positivity and square-budget proofs. This representation encodes exponent choices in the prime factorization of N² without explicit factorization API overhead.
proof idea
The definition is a one-line field projection that returns the e component of the input box.
why it matters
This selector is invoked by box_divisor_mul_complement to recover the square-budget identity and by box_phase_hit_gives_balanced_pair to build the balanced-pair support required by the RCL skeleton. It appears inside HitsBalancedPhase and in SubsetProductPhaseHit witnesses. It supplies the combinatorial closure step for the Erdős-Straus finite phase argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.