Prove2Me

§2, Eq. (5) — the tower of 3-dimensional cones represents ∥y∥2≤t\|y\|_2\le t

Proved
PolyhedralSOC.UpperBound.tower_representation

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedral-approximationsecond-order-cone

Let θ≥1\theta\ge1, k=2θk=2^\theta, y∈Rky\in\mathbb R^k and t∈Rt\in\mathbb R. Then (y,t)(y,t) can be extended to a tower of variables yiℓy_i^\ell (with yi0=yiy_i^0=y_i, y1θ=ty_1^\theta=t) solving

[y2i−1ℓ−1]2+[y2iℓ−1]2≤yiℓ,i=1,…,2θ−ℓ, ℓ=1,…,θ,(5)\sqrt{[y_{2i-1}^{\ell-1}]^2+[y_{2i}^{\ell-1}]^2}\le y_i^\ell,\qquad i=1,\dots,2^{\theta-\ell},\ \ell=1,\dots,\theta,\tag{5}

if and only if (y,t)(y,t) solves (CQI):

y12+⋯+yk2≤t.\sqrt{y_1^2+\dots+y_k^2}\le t.

The conic quadratic constraint of dimension k+1k+1 is thereby represented exactly by k−1k-1 conic quadratic constraints of dimension 3.

Formalization Note The norm is the Euclidean norm. The hypothesis θ≥1\theta\ge1 excludes the degenerate case k=1k=1, in which generation 00 and generation θ\theta would be the same variable.

Preamble
import Mathlib
import Definitions.Def_PolyhedralSOC_UpperBound_Tower
Formal statement
namespace PolyhedralSOC.UpperBound

/-- Ben-Tal & Nemirovski, *On Polyhedral Approximations of the Second-Order Cone*,
Math. Oper. Res. 26(2):193–205 (2001), §2, Eq. (5), p. 199 (PDF p. 7): for `k = 2^θ`,
`θ ≥ 1`, a pair `(y, t)` can be extended to a tower `Y` solving (5) if and only if
`(y, t)` solves (CQI) `√(y_1² + ⋯ + y_k²) ≤ t`. -/
theorem tower_representation (θ : ℕ) (hθ : 1 ≤ θ) (y : Fin (2 ^ θ) → ℝ) (t : ℝ) :
    (∃ Y : ℕ → ℕ → ℝ, IsTowerOf θ y t Y ∧ TowerSystem5 θ Y) ↔ Shared.eucNorm y ≤ t := by sorry

end PolyhedralSOC.UpperBound
Source
Ben-Tal & Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Math. Oper. Res. 26(2):193–205 (2001), §2, p. 199, Eq. (5)
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph