§9.1 — projection onto Boolean vectors by coordinatewise rounding

Proved

BoydADMM.Nonconvex.boolean_projection

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

boolean-optimizationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-bookp2o-v1projection

Let $v\in\mathbb R^n$ . Round each entry independently to its nearest value in $\{0,1\}$ , choosing zero when $v_i=1/2$ , and call the resulting vector $w$ . Then $w$ is Boolean and

\|w-v\|_2^2\le\|x-v\|_2^2\quad\text{for every }x\in\{0,1\}^n.

This is the exact Euclidean projection used for Boolean constraints in nonconvex ADMM.

Formalization Note At a tie, both zero and one are nearest; the chosen convention fixes a candidate without claiming uniqueness.

Preamble

import Mathlib
import Definitions.Def_BoydADMM_Nonconvex_ProjectionBasics

Formal statement

namespace BoydADMM.Nonconvex

/-- §9.1, p. 74: rounding each entry to a nearest Boolean value gives a
Euclidean projection onto the Boolean cube. -/
theorem boolean_projection {n : ℕ} (v : Fin n → ℝ) :
    roundBoolean v ∈ booleanSet ∧
    ∀ x ∈ booleanSet, sqDist (roundBoolean v) v ≤ sqDist x v := by sorry

end BoydADMM.Nonconvex

Source

Boyd, Parikh, Chu, Peleato, Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Found. Trends Mach. Learn. 3(1) (2011), p. 74, §9.1, Boolean constraints bullet

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph