The Hlawka deficit of a candidate constant on a coordinate triple

hlawkaDeficit packages the Hlawka inequality for the finite coordinate power functional and a candidate constant as a single real number, for vectors $x,y,z$ indexed by an arbitrary finite type:

using the finite coordinate power functional $\|\cdot\|_p$ (DiagonalConstruction.lpNorm), which is a norm for $p\ge1$. The definition itself accepts every real $p$.

Equivalently, by a theorem in the same source module, $\operatorname{hlawkaDeficit}(p,K,x,y,z)$ equals $K$ times the pair-deficit sum minus the triple deficit for $x,y,z$ (pairGapSum, tripleGap). So $\operatorname{hlawkaDeficit}(p,K,x,y,z)\ge 0$ says exactly that the triple deficit for $x,y,z$ is at most $K$ times their pair-deficit sum, and a negative value witnesses a strict failure of that bound for the constant $K$.

This single real-valued packaging is what lets the theorems that accompany it manipulate a hypothetical failure algebraically: for $K\ge1$, relabeling — permuting $x,y,z$ and, if needed, replacing $x$ by $-(x+y+z)$ — so that the total norm $\|x+y+z\|_p$ is at least as large as each of $\|x\|_p,\|y\|_p,\|z\|_p$, which can only decrease a negative deficit; and then, for $p>0$, rescaling so that $\|x\|_p+\|y\|_p+\|z\|_p=1$, which multiplies the deficit by a positive factor.