DivisorExponentBox
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct explicit pairs for a given N.
- Does not prove the Erdős-Straus conjecture.
- Does not encode prime-factorization data.
- Does not address limits or infinite families.
formal statement (Lean)
24structure DivisorExponentBox (N : ℕ) where
25 d : ℕ
26 e : ℕ
27 d_pos : 0 < d
28 e_pos : 0 < e
29 square_budget : d * e = N ^ 2
30
31/-- The divisor selected by a box point. -/