Theorem 1.1 — $L^k$ has a polyhedral $\varepsilon$-approximation with $p_k+q_k\le O(1)\,k\ln(2/\varepsilon)$

There is an absolute constant $C>0$ such that for every positive integer $k$ and every $\varepsilon\in(0,1]$ the Lorentz cone

admits a polyhedral $\varepsilon$-approximation, i.e. a linear map $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^{p_k}\to\mathbb R^{q_k}$ such that (i) every $(y,t)\in L^k$ has some $u$ with $\Pi(y,t,u)\ge0$ and (ii) $\Pi(y,t,u)\ge0$ for some $u$ implies $\|y\|_2\le(1+\varepsilon)t$, whose sizes satisfy

A conic quadratic program can therefore be approximated to relative accuracy $\varepsilon$ by a linear program whose size grows only like $k\ln(1/\varepsilon)$, not exponentially in $k$.

Formalization Note The paper's $O(1)$ is an absolute constant; it is the existential $C$, quantified before $k$ and $\varepsilon$. $\Pi$ must be $\mathbb R$-linear (→ₗ[ℝ]), vectors of $\mathbb R^k$ are Fin k → ℝ, and $\|\cdot\|_2$ is the Euclidean norm written out as a square root of a sum of squares. $\ln$ is Real.log.