The All-Dimensional Hypercube Inequality

Abstract

The determinant-defined Hypercube Inequality holds in every positive dimension.

Definition 1.1 (The augmented cube matrix).

$$\begin{array}{r}\forall d\in \mathbb{N},A\left(d\right):\left(\left(\mathrm{Fin}\left(d\right)+\{\ast \}\right)\times \{0,1{\}}^d\right)\to \mathbb{Z},\\ A\left(d,\mathrm{inl}\left(i\right),v\right)=v_i,A\left(d,\mathrm{inr}\left(\ast \right),v\right)=1.\end{array}$$

Formalization. D5/S0/FiniteGeometry/HypercubeInequality.augmentedCube (✓ std3).

Citation. Gennadiy Averkov; Katherina von Dichter; Ivan Soprunov (2026). On the Log-submodularity for zonoids: from Mixed Volume inequalities to the Hypercube. URL: https://arxiv.org/html/2608.14909v1#S4.E16.

Commentary.

The columns are indexed by Boolean cube vertices. The first d rows are the vertex coordinates, cast to integers, and the final row is one. Thus every maximal minor is the oriented normalized volume of its unordered (d+1)-vertex subset.

Definition 1.2 (The weighted normalized-volume sum).

$$\begin{array}{r}\forall d\in \mathbb{N},x:\{0,1{\}}^d\to \mathbb{R},\\ W\left(d,x\right)=\sum _{S\subseteq \{0,1{\}}^d,\mathrm{card}\left(S\right)=d+1}\left|\det \left(\mathrm{columns}\left(A\left(d\right),S\right)\right)\right|\prod _{v\in S}{x}_v.\end{array}$$

Formalization. D5/S0/FiniteGeometry/HypercubeInequality.hypercubeWeight (✓ std3).

Citation. Gennadiy Averkov; Katherina von Dichter; Ivan Soprunov (2026). On the Log-submodularity for zonoids: from Mixed Volume inequalities to the Hypercube. URL: https://arxiv.org/html/2608.14909v1#S4.E16.

Commentary.

The sum ranges once over every finite subset of cube vertices with cardinality d+1. Its coefficient is the absolute integer determinant of the actual augmented columns, multiplied by the weights on the subset. There is no ordering multiplicity and no factorial normalization.

Theorem 1.3 (Equation (16) in every positive dimension).

$$\begin{array}{r}\forall d\in \mathbb{N},1\le d,\\ \forall x:\{0,1{\}}^d\to \mathbb{R},\left(\forall v\in \{0,1{\}}^d,0\le x_v\right)⟹\\ W\left(d,x\right){\left(\sum _{v\in \{0,1{\}}^d}{x}_v\right)}^{d-1}\le \prod _{i\in \mathrm{Fin}\left(d\right)}\left(\sum _{v\in \{0,1{\}}^d,v_i=0}{x}_v\right)\left(\sum _{v\in \{0,1{\}}^d,v_i=1}{x}_v\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S0/FiniteGeometry/HypercubeInequality.result (✓ std3). ∎

Resolves. Problems/hypercube-inequality (proved) by D5/S0/FiniteGeometry/HypercubeInequality.result.

Source. Repository-derived.

Acknowledgement. Gennadiy Averkov; Katherina von Dichter; Ivan Soprunov (2026). On the Log-submodularity for zonoids: from Mixed Volume inequalities to the Hypercube. URL: https://arxiv.org/html/2608.14909v1#S4.E16.

Commentary.

For every d at least one and every nonnegative real weight on the Boolean cube, the determinant-weighted sum times the total weight to the power d-1 is bounded by the product of the two opposite facet sums in every coordinate.

The proof first expands the weighted Gram determinant by maximal minors using the characteristic-polynomial minor formula and det(1+PQ)=det(1+QP). Integer determinants satisfy |det| <= |det|^2, so the source weight is bounded by this positive semidefinite determinant.

If the total weight is zero, nonnegativity makes every weight and both sides zero. Otherwise the final scalar block is positive. Its Schur complement, scaled by the total weight, is positive semidefinite and has diagonal entries equal to the products of the two exact coordinate-facet sums. A Gram factorization and the orientation volume bound compare its determinant with the product of those diagonal entries. The Schur determinant identity supplies exactly the factor s^(d-1). Singular Gram matrices and zero facet sums require no division or positivity assumption beyond the separated total-zero case.

References

• Truth anchor: D5/S0/FiniteGeometry/HypercubeInequality.augmentedCube
• Truth anchor: D5/S0/FiniteGeometry/HypercubeInequality.hypercubeWeight
• Truth anchor: D5/S0/FiniteGeometry/HypercubeInequality.result