DivisorExponentBox
plain-language theorem explainer
DivisorExponentBox encodes a complementary pair of positive integers d and e whose product equals N squared for any fixed natural number N. Number theorists examining the combinatorial core of the Erdős-Straus conjecture cite this structure when isolating square-budget divisor selection. The definition is a direct structure declaration that bundles the two divisors with their positivity requirements and the exact product equation.
Claim. A divisor-exponent box for a natural number $N$ is a pair of positive integers $d$ and $e$ satisfying $d e = N^2$.
background
The Erdős-Straus Square-Budget Box Phase module isolates the finite combinatorial fragment of the residual Erdős-Straus argument. For a square budget $N^2$, the module represents divisor choices by complementary pairs $(d,e)$ with $d e = N^2$, sidestepping explicit prime-factorization machinery. This representation directly supports later phase-hit and subset-product constructions in the same file.
proof idea
The declaration is a structure definition that introduces five fields: the divisor $d$, its complement $e$, the two positivity hypotheses, and the product equation. No lemmas are applied; the structure simply packages the stated constraints.
why it matters
The structure supplies the core type used by boxDivisor, boxComplement, box_divisor_mul_complement, HitsBalancedPhase, and SubsetProductPhaseHit. It therefore anchors the combinatorial closure step inside the Recognition Science treatment of the Erdős-Straus conjecture, feeding the balanced-residual-phase witness that appears in the downstream subset-product phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.