Logarithmic linear program for the box theorem (source code)

= Logarithmic linear program for the box theorem
{title2=$\max\sum_i x_i:\ \sum_{i\in A}x_i\leq\log|S_A|$}

Set $x_i=\log b_i$ for candidate <axis-parallel box> side lengths. Its coordinate-projection constraints are the displayed <linear program>. The dual feasible weights are <fractional uniform covers>. Its optimal extreme point is rational, so the <uniform covers theorem> forces its objective to be at least $\log|S|$. Weight one on the full coordinate set attains that value. <Strong duality> therefore supplies box side lengths with volume $|S|$ and no larger coordinate projections.