Lifting a three-coordinate Hlawka bound to every finite real dimension

For a finite index set $\iota$ and a real vector $v:\iota\to\mathbb R$, write $\|v\|_p:=\big(\sum_{i\in\iota}|v_i|^p\big)^{1/p}$ (lpNorm) for the coordinate $p$-norm. For real vectors $u,v,w$ on a common index set, write the triple deficit

and the pair-deficit sum $\mathrm{pairGapSum}(u,v,w)$ for the sum of the three pair deficits $\|a\|_p+\|b\|_p-\|a+b\|_p$ over $\{u,v\},\{u,w\},\{v,w\}$. Say $\|\cdot\|_p$ has Hlawka constant $C$ (HasHlawkaConstant) when

Let $\iota$ be any finite index set, $p>1$, and $K\ge\tfrac12$. Suppose $\|\cdot\|_p$ has Hlawka constant $K$ on three real coordinates:

Then $\|\cdot\|_p$ has Hlawka constant $K$ on $\iota\to\mathbb R$ too:

This is the dimension-independence half of the sharp diagonal construction on the real side: an admissible Hlawka constant for three real coordinates is automatically admissible in every finite real dimension, with no dependence on the size of $\iota$. Combined with the fact that the explicit cyclic constant $K_p=\sup_{1/2\le t\le2}R_p(t)$ (cyclicConstant; $R_p(t)$ is the ratio of triple deficit to pair-deficit sum for the triple $(-t,1,1),(1,-t,1),(1,1,-t)$) is such a three-coordinate constant for every real $p\ge256$ (established elsewhere) and the later complex transfer step, this is what allows the Hlawka bound with constant $K_p$ for diagonal Schatten $p$-norms to hold in every finite dimension, including dimension zero.

Formalization Note $\iota$ ranges over an arbitrary finite type (via a Fintype instance), not just Fin n, and may be empty.