Ordered-algebraic transfer of a Hlawka-type inequality through a model functional

Let $E$ be a type with an addition operation (no norm is assumed on $E$), and let $H$ be a normed additive commutative group (no inner product is assumed on $H$). Let $\mathrm{size},\mathrm{modelSize}:E\to\mathbb R$ be two real-valued functionals on $E$, and let $\mathrm{map}:E\to H$ be any function (not assumed linear or continuous). For a functional $s:E\to\mathbb R$ and $u,v\in E$ (respectively $u,v,w\in E$), write the pair deficit $\mathrm{pgap}(s)(u,v)=s(u)+s(v)-s(u+v)$ and the triple deficit $\mathrm{tgap}(s)(u,v,w)=s(u)+s(v)+s(w)-s(u+v+w)$ (pairGap, tripleGap), and $\mathrm{pgapsum}(s)(u,v,w)$ for the sum of the three pair deficits of $u,v,w$ (pairGapSum). Define the analogous mapped pair deficit $\mathrm{mpgap}(u,v)=\mathrm{modelSize}(u)+\mathrm{modelSize}(v)-\|\mathrm{map}(u)+\mathrm{map}(v)\|$, using the norm of $H$ on the mapped term, and likewise the mapped triple deficit $\mathrm{mtgap}$ and mapped pair-deficit sum $\mathrm{mpgapsum}$ (mappedTripleGap, mappedPairGap, mappedPairGapSum).

Fix $x,y,z\in E$ and real numbers $m>0$, $M\ge0$. Suppose:

1. (triple upper bound) $\mathrm{tgap}(\mathrm{size})(x,y,z) \le 2M\cdot\mathrm{mtgap}(x,y,z)$;
2. (pair lower bounds) $2m\cdot\mathrm{mpgap}(x,y)\le\mathrm{pgap}(\mathrm{size})(x,y)$, and likewise for the pairs $(x,z)$ and $(y,z)$;
3. (model Hlawka inequality) $\mathrm{mtgap}(x,y,z)\le\mathrm{mpgapsum}(x,y,z)$.

Then

This is the final, purely ordered-algebraic assembly step of the Bregman–Mazur route to a dimension-independent Hlawka constant: given a triple upper bound and three pair lower bounds relating the true deficits of $\mathrm{size}$ to their mapped, model counterparts, together with a Hlawka-type inequality already established for the model, the two factors of $2$ cancel exactly and only the ratio $M/m$ survives as the constant for $\mathrm{size}$.

Formalization Note The mapped quantities use only the norm of $H$, so the theorem needs $H$ to be a normed additive commutative group and nothing more — no inner product, and $\mathrm{map}$ need not be linear or continuous.