boxDivisor
plain-language theorem explainer
boxDivisor extracts the divisor component d from a DivisorExponentBox structure encoding a complementary pair for square budget N squared. Number theorists closing finite cases in the Erdős-Straus conjecture cite this selector when building balanced-pair witnesses from box points. The definition performs a direct field projection onto the d component of the input structure.
Claim. Let $B$ be a divisor-exponent box for $N$, consisting of positive integers $d$ and $e$ satisfying $d e = N^2$. Then the selected divisor is $d$.
background
The Erdős-Straus Square-Budget Box Phase module isolates the finite combinatorial fragment of the residual proof. A divisor-exponent box for square budget $N^2$ is a structure holding a complementary pair of positive divisors $d$ and $e$ together with the equality $d e = N^2$; this encodes exponent choices in the prime factorization of $N$ without invoking factorization primitives.
proof idea
The definition is a one-line field projection returning the d component of the supplied DivisorExponentBox.
why it matters
boxDivisor supplies the divisor component required by box_divisor_mul_complement (recovering the square-budget identity) and by box_phase_hit_gives_balanced_pair (constructing BalancedPairPhaseSupport for the RCL skeleton). It therefore closes the finite box-to-phase step in the Erdős-Straus argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.