Correctness of Condat's Proposed Algorithm (Fig. 2): the output is $P_\Delta(y)$ and $K$ counts its nonzeros

Proved

SimplexProj.Condat.condat_algorithm_correct

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

algorithmcorrectnessprojectionsimplex

Let $N \ge 1$ , $y = (y_1, \dots, y_N) \in \mathbb{R}^N$ and $a > 0$ . Run Condat's Proposed Algorithm (Fig. 2) on $y$ and $a$ ; it terminates with a threshold $\tau$ and a count $K$ . Set $x_n := \max\{y_n - \tau, 0\}$ for $n = 1, \dots, N$ (step 6). Then $x$ is the Euclidean projection of $y$ onto the simplex of radius $a$ , and $K$ is the number of nonzero entries of $x$ :

x = P_\Delta(y), \qquad K = \#\{\, n \in \{1, \dots, N\} : x_n \ne 0 \,\}.

This is the correctness claim of Condat's algorithm (Fig. 2 and its caption, argued in Sect. 3): the algorithm computes the projection exactly and in finite time, for every input, with no assumption on the order or distinctness of the entries of $y$ .

Formalization Note. The algorithm is the total function condatAlgorithm a (List.ofFn y), returning $(\tau, K)$ ; termination is part of the definition (well-founded recursion), so the theorem is about every input. $x = P_\Delta(y)$ is the predicate IsSimplexProjection a y x; $K$ is compared with the number of indices $n$ with $x_n \ne 0$ (a count over indices, not distinct values).

Preamble

import Mathlib
import Definitions.Def_SimplexProj_Condat_IsSimplexProjection
import Definitions.Def_SimplexProj_Condat_condatAlgorithm

Formal statement

namespace SimplexProj.Condat

/-- Condat, Sect. 3, Fig. 2 and its caption (p. 6): for `N ≥ 1`, `y ∈ ℝ^N`, `a > 0`, the
Proposed Algorithm run on `(y_1, …, y_N)` terminates with `(τ, K)` such that
`x = (max {y_n - τ, 0})_{n=1}^N` (step 6) is the Euclidean projection `P_Δ(y)` of `y` onto the
simplex of radius `a`, and `K` is the number of nonzero elements of `x`. -/
theorem condat_algorithm_correct (N : ℕ) (hN : 1 ≤ N) (a : ℝ) (ha : 0 < a) (y : Fin N → ℝ)
    (τ : ℝ) (K : ℕ) (hout : condatAlgorithm a (List.ofFn y) = (τ, K)) :
    IsSimplexProjection a y (fun n => max (y n - τ) 0) ∧
      K = (Finset.univ.filter (fun n => max (y n - τ) 0 ≠ 0)).card := by sorry

end SimplexProj.Condat

Source

Condat, Fast Projection onto the Simplex and the ℓ1 Ball, HAL hal-01056171v2, p. 6, Sect. 3, Fig. 2 and caption

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The statement concerns a whole number $N$ , a real number $a$ , a vector $y = (y_0, y_1, \dots, y_{N-1}) \in \mathbb{R}^N$ (indexed by $\{0, 1, \dots, N-1\}$ ), a real number $\tau$ and a whole number $K$ . It assumes:

$N \ge 1$ ;
$a > 0$ ;
$\mathrm{condatAlgorithm}(a, [y_0, y_1, \dots, y_{N-1}]) = (\tau, K)$ . Here $\mathrm{condatAlgorithm}$ is a function defined in an imported file that is not shown. It takes the real number $a$ and the finite list of the entries of $y$ in index order, and returns a pair made of a real number and a whole number. The hypothesis says that the pair it returns on this input is exactly $(\tau, K)$ .

From these data, define the vector $x \in \mathbb{R}^N$ entry by entry:

x_n = \max(y_n - \tau,\ 0), \qquad n = 0, \dots, N-1.

The conclusion is the conjunction of two claims.

$\mathrm{IsSimplexProjection}(a, y, x)$ holds. This is a predicate on a real number $a$ , a vector $y \in \mathbb{R}^N$ and a vector $x \in \mathbb{R}^N$ , defined in another imported file that is not shown. Its meaning is fixed entirely by that hidden definition and cannot be read from this declaration. The name suggests " $x$ is the Euclidean projection of $y$ onto a simplex of radius $a$ ," but only the imported definition decides what is actually asserted.
$K$ is the number of indices $n \in \{0, \dots, N-1\}$ with $x_n \neq 0$ . Since every $x_n \ge 0$ , this is the same as the number of indices with $y_n > \tau$ :

K = \#\{\, n : \max(y_n - \tau, 0) \neq 0 \,\} = \#\{\, n : y_n > \tau \,\}.

The text in the code comment above the theorem (it cites Condat, Sect. 3, Fig. 2) is documentation only and is not part of what is asserted.

Degenerate cases. $N = 0$ is excluded by the hypothesis $N \ge 1$ , and $a \le 0$ is excluded by $a > 0$ , so the statement says nothing about the algorithm's output in those cases. $N = 1$ is allowed: then $y$ is a single number $y_0$ , $x_0 = \max(y_0 - \tau, 0)$ , and the claims are that $\mathrm{IsSimplexProjection}(a, y, x)$ holds and that $K$ is $1$ if $y_0 > \tau$ and $0$ otherwise. Entries of $y$ may be equal, negative or arbitrarily large; nothing restricts them.

Because $\mathrm{condatAlgorithm}$ is a function, its output on the given input is a single pair. So the hypothesis fixes $\tau$ and $K$ to exactly that pair, and the theorem is a claim about the algorithm's actual output, not about arbitrary $(\tau, K)$ . The hypothesis can therefore always be satisfied, and the statement is not vacuous on that account. The function has to return some value on every input, whether or not the procedure it encodes "terminates" in an informal sense. Any default or placeholder values it produces internally (for example from division by zero or subtraction of whole numbers) are part of its hidden definition and are not visible here. The whole content of the first claim, including whether it is strong, weak or trivially satisfied, depends on the unseen definition of $\mathrm{IsSimplexProjection}$ .

Human review

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

View graph

Correctness of Condat's Proposed Algorithm (Fig. 2): the output is PΔ(y)P_\Delta(y)PΔ​(y) and KKK counts its nonzeros

Correctness of Condat's Proposed Algorithm (Fig. 2): the output is $P_\Delta(y)$ and $K$ counts its nonzeros