box_divisor_mul_complement
plain-language theorem explainer
The theorem states that for any divisor-exponent box tied to square budget N squared, the product of the selected divisor and its complement equals N squared. Number theorists closing finite cases of the Erdős-Straus conjecture in the Recognition Science setting would cite this identity to confirm complementary pairs. The proof is a direct one-line extraction of the square_budget field from the box structure.
Claim. Let $(d,e)$ be a divisor-exponent box for square budget $N^2$. Then $d · e = N^2$.
background
The module isolates the finite combinatorial part of the residual Erdős-Straus proof. A divisor-exponent box for square budget $N^2$ is represented by a complementary pair $(d,e)$ with $d·e = N^2$, avoiding explicit prime factorization. The structure DivisorExponentBox packages positive divisors $d$ and $e$ together with the square-budget equality as its defining field.
proof idea
The proof is a one-line term that applies the square_budget field of the DivisorExponentBox structure.
why it matters
This identity supplies the complementary-pair relation required by the RCL skeleton in the finite Erdős-Straus setting. It feeds the downstream theorem box_phase_hit_gives_balanced_pair, which converts a phase hit into balanced-pair support. The result sits inside the square-budget phase module and closes the combinatorial step before balanced residual phases are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.