Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 21 results · all verified · 11 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 10 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Operator splitting ADMM and primal dual methods

1 · Prerequisites

2 · Summary

This page develops three distinct finite-dimensional methods. Douglas–Rachford splitting is treated for two maximal-monotone relations; its resolvent theorem is proved locally from a one-point nonexpansive extension argument, and the shadow converges when the operator sum has a zero. Two-block ADMM has a separate exact-attainment guard: under a saddle point and attained exact subproblems, the primal residual and objective converge and the unscaled dual sequence converges, while convergence of the primal iterates is not asserted. A finite capped solver reports failure or exhaustion unless it certifies an exact minimizer.

The Chambolle–Pock primal-dual hybrid-gradient recurrence uses proper closed convex objectives, exact proximal updates, and the strict bound $τ σ ∥ K ∥_{2}^{2} < 1$ . Its proved rate is an $O (1 / N)$ ergodic saddle-gap bound. It supplies no pointwise objective rate. The A page defines naive sequential three-block ADMM, and the companion examples page proves that its convergence failure can occur; the construction does not weaken the two-block theorem or extend it to nonconvex objectives.

All convergence arguments here are over finite-dimensional real Euclidean spaces and use no additional choice principle. The four declared supplier pages provide optimization-function conventions, prox interfaces, sparse-matrix contracts, and Lanczos bounds; their current bodies and acceptance remain recorded in the batch evidence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Monotone and maximal-monotone relations on Euclidean space

Definition

Fix $n \in N$ and the Euclidean space $E = R^{n}$ with inner product and norm from The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . A relation $A$ on $E$ is a subset of $E \times E$ ; write $a \in A (x)$ exactly when $(x, a) \in A$ . Its graph is this subset. The relation is monotone if $⟨ x - x^{'}, a - a^{'} ⟩ \geq 0 for all (x, a), (x^{'}, a^{'}) \in A .$ It is maximal monotone if it is monotone and no strictly larger subset of $E \times E$ is monotone. This definition is finite-dimensional and makes no claim about infinite-dimensional spaces.

Facts & Assumptions

Given: $n \in N$ and $E = R^{n}$ .

[A1]

The ambient space is $E = R^{n}$ and $A \subseteq E \times E$ .

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $⟨ x, y ⟩ = \sum_{i < n} x_{i} y_{i}$ is a real bilinear inner product on $E$ .

Proof

1.1A1givenF1given

A relation is a graph of ordered pairs $(x, a)$ with both coordinates in $E$ ; the notation $a \in A (x)$ is the same membership statement. The displayed inequality therefore quantifies over two graph points and is well-defined by [F1].

2.1A1givenF1given∎

Maximality is inclusion-maximality among monotone graphs: it rules out a monotone proper extension and does not mean that the graph is a largest monotone subset. These are the graph-level conventions used below.

DefinitionDefinition: Literature-sourcedProof: AI-generatedprecheck passOpen item page →

Saddle points of extended-real Lagrangians

Definition

Let $X, Y$ be nonempty subsets of finite-dimensional real Euclidean spaces and let $Ψ : X \times Y \to [- \infty, + \infty]$ be an extended-real function. A pair $(x_{*}, y_{*})$ is a saddle point of $Ψ$ if $Ψ (x_{*}, y_{*})$ is finite and $Ψ (x_{*}, y) \leq Ψ (x_{*}, y_{*}) \leq Ψ (x, y_{*}) (x \in X, y \in Y) .$ The inequalities must be defined at the arguments they display. For an equality-constrained problem the primal set may be a product set of finite-valued pairs $(x, z)$ .

Facts & Assumptions

Given: Nonempty subsets $X, Y$ of finite-dimensional real Euclidean spaces and an extended-real function $Ψ$ as above.

[A1]

The displayed evaluations are defined and the central value is finite.

[F1]

The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined: extended-real values are ordered in $[- \infty, + \infty]$ .

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : each finite-dimensional Euclidean space carries a real inner product and its induced norm.

Proof

1.1A1givenF1F2

The definition is a pair of quantified order inequalities with a finite central value. Only the displayed evaluations are needed, so a partial formula such as $f (x) + ⟨ K x, y ⟩ - g^{*} (y)$ is safe when each displayed saddle evaluation is defined.

2.1A1givenF1algebra∎

Restricting $X, Y$ can remove a violation of a saddle inequality, so a saddle point on the restricted sets need not be one on the original sets. For a fixed finite central value, the inequalities extend to the original sets precisely when every omitted left-hand value is at most that central value and every omitted right-hand value is at least it, with all evaluations defined. In particular, omitted $- \infty$ values on the left and $+ \infty$ values on the right cause no obstruction. No minimax interchange or existence theorem follows from this definition.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Picard iterates of a firmly nonexpansive map converge in finite dimensions

Statement

Let $T : E \to E$ be firmly nonexpansive on $E = R^{n}$ , suppose $Fix (T) = {p : T (p) = p}$ is nonempty, and start at any $w_{0}$ . Then the Picard sequence $w_{k + 1} = T (w_{k})$ converges to a fixed point of $T$ .

Facts & Assumptions

Given: The map $T$ , a fixed point $p$ , and $w_{0} \in E$ .

[A1]

The map is firmly nonexpansive, its fixed-point set is nonempty, and the start is in $E$ .

[F1]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: the Euclidean norm is a norm and satisfies Cauchy–Schwarz.

[F2]

For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence: for $n \geq 1$ , every bounded sequence in $R^{n}$ has a convergent subsequence.

[F3]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of the single zero vector.

Proof

1.1A1givenF1F3algebra

If $n = 0$ , [F3] gives $E = {0}$ and the nonempty fixed-point set forces $T (0) = 0$ ; since $w_{0} = 0$ , every iterate equals the fixed point. It remains to consider $n \geq 1$ . Firm nonexpansiveness applied to $w_{k}$ and a fixed point $p$ gives $∥ w_{k + 1} - p ∥_{2}^{2} \leq ⟨ w_{k + 1} - p, w_{k} - p ⟩$ . Expanding $w_{k} - p = (w_{k + 1} - p) + (w_{k} - w_{k + 1})$ and rearranging yields $∥ w_{k + 1} - p ∥_{2}^{2} + ∥ w_{k + 1} - w_{k} ∥_{2}^{2} \leq ∥ w_{k} - p ∥_{2}^{2} .$ Summing this inequality shows that the distances to $p$ are nonincreasing, the sequence is bounded, and $\sum_{k} ∥ w_{k + 1} - w_{k} ∥_{2}^{2} < \infty$ , so the increments tend to zero.

2.1A1F1F2step 1.1algebra

By [F2], some subsequence $w_{k_{j}}$ converges to $\overset{ˉ}{w}$ . Firm nonexpansiveness and [F1] imply $T$ is 1-Lipschitz, hence continuous. Since $w_{k_{j} + 1} - w_{k_{j}} \to 0$ , continuity gives $T (\overset{ˉ}{w}) = \overset{ˉ}{w}$ .

3.1A1step 1.1step 2.1algebra∎

Apply the inequality of step 1.1 with the fixed point $\overset{ˉ}{w}$ in place of $p$ . The distances $∥ w_{k} - \overset{ˉ}{w} ∥_{2}$ are nonincreasing, and along the subsequence $k_{j}$ they tend to zero. A nonincreasing nonnegative sequence with a subsequence tending to zero tends to zero; thus $w_{k} \to \overset{ˉ}{w}$ .

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

One-point extension of a nonexpansive map in finite dimensions

Statement

Let $E = R^{n}$ with its Euclidean norm, let $D \subseteq E$ , and let $T : D \to E$ satisfy $∥ T (p) - T (p^{'}) ∥_{2} \leq ∥ p - p^{'} ∥_{2}$ for all $p, p^{'} \in D$ . For every $y \in E$ there exists $q \in E$ such that $∥ q - T (p) ∥_{2} \leq ∥ y - p ∥_{2} (p \in D) .$ Equivalently, one value can be added at the new input $y$ without violating the Lipschitz constant $1$ .

Facts & Assumptions

Given: $E, D, T, y$ as in the Statement.

[A1]

The map $T : D \to E$ is 1-Lipschitz and $y \in E$ .

[F1]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: for $n \geq 1$ , $∥ \cdot ∥_{2}$ is a norm inducing $d_{2}$ , and the parallelogram and polarization identities hold.

[F2]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: for $n \geq 1$ , a closed bounded subset of $R^{n}$ is compact.

[F3]

Semicontinuous extreme value theorem on compact Euclidean sets: for $n \geq 1$ , a continuous real function on a nonempty compact subset of $R^{n}$ attains its minimum.

[F4]

Every point has a unique nearest point in a nonempty closed Euclidean convex set and Metric projection onto a closed convex set satisfies the variational inequality: in $R^{n}$ for $n \geq 1$ , a nonempty closed convex subset has a nearest point to any point, and that projection satisfies the variational inequality.

[F5]

A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection: a family of closed subsets of a compact space with the finite-intersection property has nonempty total intersection.

Proof

1.1A1givenF1F2F3construct

If $n = 0$ , then $E = {0}$ . If $D$ is empty choose $q = 0$ ; if it is nonempty then $D = {0}$ , $y = p = T (p) = 0$ , and $q = 0$ satisfies the inequality. Hence assume $n \geq 1$ . If $D = \emptyset$ , any $q$ works. Otherwise consider any finite nonempty list $p_{1}, \dots, p_{m} \in D$ and set $h_{i} (q) = ∥ q - T p_{i} ∥_{2}^{2} - ∥ y - p_{i} ∥_{2}^{2}, H (q) = \max_{1 \leq i \leq m} h_{i} (q) .$ By [F1], $∣ ∥ u ∥_{2} - ∥ v ∥_{2} ∣ \leq ∥ u - v ∥_{2} = d_{2} (u, v)$ , so each $h_{i}$ and their finite maximum $H$ are continuous. Also, when $∥ q ∥_{2} \geq ∥ T p_{i} ∥_{2}$ , $h_{i} (q) \geq (∥ q ∥_{2} - ∥ T p_{i} ∥_{2})^{2} - ∥ y - p_{i} ∥_{2}^{2},$ which tends to $+ \infty$ as $∥ q ∥_{2} \to \infty$ ; thus $H$ is coercive. The nonempty sublevel ${H \leq H (0)}$ is closed and bounded, hence compact by [F2]; [F3] gives a global minimizer $q_{0}$ of $H$ .

2.1A1F1F2F4step 1.1contradictionalgebra

Let $I = {i : h_{i} (q_{0}) = H (q_{0})}$ be the nonempty active set. Its gradients' convex hull is the image of the closed bounded simplex ${α \in R^{m} : α_{i} \geq 0, \sum_{i} α_{i} = 1}$ under the continuous affine map $α \mapsto \sum_{i \in I} α_{i} 2 (q_{0} - T p_{i})$ (with zero weights outside $I$ ). The simplex is compact by [F2]; pulling an open cover back to it shows its continuous image is compact, and [F2] then makes that image closed. If $0$ were not in the convex hull, project $0$ onto it using [F4]. The projection vector $v \neq 0$ obeys $⟨ v, 2 (q_{0} - T p_{i}) ⟩ \geq ∥ v ∥_{2}^{2}$ for each $i \in I$ , by the variational inequality. For sufficiently small $ϵ > 0$ , every active $h_{i} (q_{0} - ϵ v)$ decreases strictly; the finitely many inactive terms have a strict gap below $H (q_{0})$ and remain below it by continuity. This contradicts minimality. Therefore there are weights $α_{i} \geq 0$ , supported on $I$ , with $\sum_{i} α_{i} = 1$ and $q_{0} = \sum_{i} α_{i} T p_{i}$ .

3.1A1F1step 2.1algebra

Put $\overset{ˉ}{p} = \sum_{i} α_{i} p_{i}$ . Expanding squares and using $q_{0} = \sum_{i} α_{i} T p_{i}$ gives $H (q_{0}) = \sum_{i} α_{i} h_{i} (q_{0}) = \frac{1}{2} \sum_{i, j} α_{i} α_{j} ∥ T p_{i} - T p_{j} ∥_{2}^{2} - \sum_{i} α_{i} ∥ y - p_{i} ∥_{2}^{2} .$ The nonexpansive hypothesis bounds the double sum by $\frac{1}{2} \sum_{i, j} α_{i} α_{j} ∥ p_{i} - p_{j} ∥_{2}^{2} = \sum_{i} α_{i} ∥ p_{i} - \overset{ˉ}{p} ∥_{2}^{2}$ . The variance identity also gives $\sum_{i} α_{i} ∥ y - p_{i} ∥_{2}^{2} = ∥ y - \overset{ˉ}{p} ∥_{2}^{2} + \sum_{i} α_{i} ∥ p_{i} - \overset{ˉ}{p} ∥_{2}^{2}$ . Hence $H (q_{0}) \leq - ∥ y - \overset{ˉ}{p} ∥_{2}^{2} \leq 0$ . Thus every finite family of the closed balls $\overline{B} (T p, ∥ y - p ∥_{2})$ has nonempty intersection.

4.1A1F2F5step 3.1choose∎

Choose one $p_{0} \in D$ . The ball $C_{0} = \overline{B} (T p_{0}, ∥ y - p_{0} ∥_{2})$ is compact by [F2]. The sets $C_{0} \cap \overline{B} (T p, ∥ y - p ∥_{2})$ are closed in $C_{0}$ , and every finite intersection is nonempty by step 3.1 applied with $p_{0}$ included. [F5] therefore supplies a point $q$ in their total intersection, which satisfies every required inequality. The proof used only finite-dimensional compactness and finite convex combinations; no choice principle is invoked.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Schur reduction preserves strict unit-disk root location

Statement

Let $p (z) = z^{n} + a_{n - 1} z^{n - 1} + \dots + a_{0}$ be a real monic polynomial of degree $n \geq 1$ with $∣ a_{0} ∣ < 1$ . Define the reversed polynomial $p^{#} (z) = z^{n} p (1 / z)$ and $q (z) = \frac{p (z) - a_{0} p^{#} (z)}{z (1 - a_{0}^{2})} .$ If every zero of $p$ lies strictly inside the unit disk, then every zero of $q$ does too.

Facts & Assumptions

Given: A real monic polynomial $p$ of degree at least one, $∣ a_{0} ∣ < 1$ , and the assumption that all its zeros lie in $∣ z ∣ < 1$ .

[A1]

The real polynomial is monic of degree at least one, $∣ p (0) ∣ < 1$ , and every root of $p$ is strictly inside the unit disk.

[F1]

Rouche's theorem in the classical strict-inequality form: if $∣ g (z) ∣ < ∣ f (z) ∣$ on a simple closed contour, then $f$ and $f + g$ have the same number of zeros inside, counted with multiplicity.

Proof

1.1A1givenF1algebra

On $∣ z ∣ = 1$ , real coefficients give $p^{#} (z) = z^{n} \overline{p (z)}$ , so $∣ p^{#} (z) ∣ = ∣ p (z) ∣$ . The strict root hypothesis makes $p$ nonzero on the unit circle, and $∣ a_{0} p^{#} (z) ∣ < ∣ p (z) ∣$ . Apply [F1] to $p$ and $- a_{0} p^{#}$ ; $p - a_{0} p^{#}$ has the same $n$ zeros in the disk as $p$ .

2.1A1givenstep 1.1algebra∎

The polynomial $p - a_{0} p^{#}$ has constant term zero and leading coefficient $1 - a_{0}^{2} \neq 0$ , so it is $z$ times a degree- $(n - 1)$ polynomial. One of its $n$ disk zeros is the factor zero at $z = 0$ ; the remaining $n - 1$ zeros are exactly those of the quotient. Dividing by the nonzero scalar $1 - a_{0}^{2}$ changes no roots. Hence all zeros of $q$ lie strictly inside the disk.

AlgorithmAlgorithm: Literature-sourcedProof: AI-generatedprecheck passOpen item page →

Naive sequential three-block ADMM

Definition

For proper closed convex $f_{i} : R^{n_{i}} \to (- \infty, + \infty]$ , linear $A_{i} : R^{n_{i}} \to R^{p}$ , data $b \in R^{p}$ , penalty $ρ > 0$ , and scaled multiplier $u^{k}$ , the naive sequential three-block ADMM sweep is $x_{1}^{k + 1} \in \arg \min_{x_{1}} f_{1} (x_{1}) + \frac{ρ}{2} ∥ A_{1} x_{1} + A_{2} x_{2}^{k} + A_{3} x_{3}^{k} - b + u^{k} ∥^{2},$ then $x_{2}^{k + 1}$ minimizes the same augmented residual with $x_{1}^{k + 1}$ , $x_{2}$ variable and $x_{3}^{k}$ fixed; then $x_{3}^{k + 1}$ minimizes it with the first two new blocks; finally $u^{k + 1} = u^{k} + A_{1} x_{1}^{k + 1} + A_{2} x_{2}^{k + 1} + A_{3} x_{3}^{k + 1} - b .$ These formulas specify the exact recurrence conditional on attained block minima; proper closed convexity alone does not ensure attainment.

The executable procedure takes the data above, a current state $(x_{1}^{k}, x_{2}^{k}, x_{3}^{k}, u^{k})$ , three positive integer caps $C_{i}$ , and, for each block, a supplied deterministic solver program $S_{i}$ and Boolean certificate checker $V_{i}$ . Their complete instructions and data representations are part of the input. Each program uses discrete steps that terminate; the checker is also such a program. A solver takes its displayed block objective and may halt with failed or a candidate-certificate pair $(v, e)$ . Admissibility requires that $V_{i} (H, v, e) = t r u e$ implies $H (v) < + \infty$ and $H (v) \leq H (w)$ for every block vector $w$ . This is a soundness requirement on supplied checkers, not a claim that such certificates can always be found or that arbitrary function descriptions can be checked automatically.

Execute one sweep as follows. Return invalid-input for mismatched dimensions, nonpositive $ρ$ , or caps that are not positive integers. Keep the old state and store tentative blocks separately. For $i = 1, 2, 3$ in that order, form its block objective using the already computed new blocks and the remaining old blocks. Run $S_{i}$ on that objective, then, if it returns $(v, e)$ , run $V_{i}$ on this triple, allowing at most $C_{i}$ program steps in total for this solver-checker pair. After each step inspect for termination: an explicit failure, malformed output, or a false checker result returns block- $i$ -solve-failed; a true result stores $v$ as the tentative block. If the budget is used without such a result or failure, return block- $i$ -cap-exhausted. A true result on the last allowed step is accepted. Any failure returns the unchanged old state. Only after all three blocks are accepted, perform the displayed multiplier update, commit the four new vectors, and return success with that state. A requested finite run repeats this sweep for an input nonnegative integer number of sweeps and stops at its first nonsuccess status. No convergence is asserted.

Facts & Assumptions

Given: The three proper closed convex objectives, linear maps, $b$ , $ρ > 0$ , current state, positive integer caps, and the supplied solver and sound certificate-checker programs in the Definition.

[A1]

Dimensions match, $f_{i}$ are proper closed convex, $ρ > 0$ , caps are positive integers, and the supplied programs satisfy the Definition's step and certificate-soundness requirements.

[F1]

Proper closed convex extended-real functions on $R^{n}$ : each objective is proper closed convex.

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the augmented residual norm is the Euclidean norm in $R^{p}$ .

Verification

1.1A1F1F2givengiven

Each displayed block objective is the corresponding convex objective plus a nonnegative continuous quadratic in its block variable; the order fixes later blocks at their newest available values. The update is therefore precisely the sequential Gauss–Seidel extension of the two-block recurrence.

2.1A1F1given∎

An exact update requires each argmin to be nonempty and attained; [F1] alone does not guarantee this. The supplied programs and the ordered solver-then-checker calls specify the capped implementation, including which status to return and whether to commit the tentative state. The certificate requirement concerns exact attained minimizers, so an approximate point cannot be accepted merely because the cap has been used.

AlgorithmAlgorithm: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Scaled two-block ADMM with explicit capped-solve statuses

Definition

Let $f : R^{n} \to (- \infty, + \infty]$ and $g : R^{m} \to (- \infty, + \infty]$ be proper closed convex, let $K : R^{n} \to R^{p}$ and $L : R^{m} \to R^{p}$ be linear, let $c \in R^{p}$ , and let $ρ > 0$ . The primal problem is $\min_{x, z} f (x) + g (z) subject to K x + L z = c,$ and its Lagrangian is $L ((x, z), y) = f (x) + g (z) + ⟨ y, K x + L z - c ⟩$ . A saddle point means a saddle pair in the sense of Saddle points of extended-real Lagrangians.

Conditional on both block minima being attained, an exact outer sweep with scaled dual $u^{k}$ computes, in order, $x^{k + 1} \in \arg \min_{x} (f (x) + \frac{ρ}{2} ∥ K x + L z^{k} - c + u^{k} ∥_{2}^{2}),$ $z^{k + 1} \in \arg \min_{z} (g (z) + \frac{ρ}{2} ∥ K x^{k + 1} + L z - c + u^{k} ∥_{2}^{2}),$ then set $r^{k + 1} = K x^{k + 1} + L z^{k + 1} - c$ and $u^{k + 1} = u^{k} + r^{k + 1}$ . Report also the unscaled dual $y^{k} = ρ u^{k}$ , objective $p_{k} = f (x^{k}) + g (z^{k})$ , and primal residual $r^{k}$ . If an exact subproblem has multiple minimizers, choose the unique minimum-norm member of its nonempty closed convex minimizer set; existence and uniqueness of that tie-break follow from Every point has a unique nearest point in a nonempty closed Euclidean convex set.

The finite procedure takes the problem data, a current state $(x^{k}, z^{k}, u^{k})$ , positive integer caps $C_{x}, C_{z}$ , and deterministic solver programs $S_{x}, S_{z}$ and Boolean certificate-checker programs $V_{x}, V_{z}$ with their complete instructions and data representations. Each program uses discrete steps that terminate. A solver takes its block objective $H$ and may halt with failed or a candidate-certificate pair $(v, e)$ . The supplied checkers must be sound: $V (H, v, e) = t r u e$ implies $H (v) < + \infty$ , $H (v) \leq H (w)$ for every block vector $w$ , and $∥ v ∥_{2} \leq ∥ w ∥_{2}$ for every minimizer $w$ of $H$ . These are admissibility conditions on the input programs, not an automatic test of arbitrary programs or a promise that an exact certificate is available. In particular, proper closed convexity alone does not imply block attainment.

Return invalid-input for mismatched dimensions, $ρ \leq 0$ , or caps that are not positive integers. Retain the old state and proceed in order through the $x$ and $z$ objectives above, using the tentative new $x$ for the $z$ objective. For block $b \in {x, z}$ , start $S_{b} (H)$ and, if it returns $(v, e)$ , run $V_{b} (H, v, e)$ , using at most $C_{b}$ program steps in total for the solver and checker. After each step inspect for termination. An explicit failure, malformed output, or false checker result returns $b$ -solve-failed with the unchanged old state. A true checker result stores $v$ as the tentative block; accept it even on the last allowed step. If the budget is used without a true result or failure, return $b$ -cap-exhausted with the old state. Only after both blocks are accepted, perform the residual and dual assignments above, commit the new state, and return success with that state, $y^{k + 1}$ , $p_{k + 1}$ and $r^{k + 1}$ . A requested finite run repeats this sweep for an input nonnegative integer number of sweeps and stops at its first nonsuccess status. Failure, including on a problem without a block minimizer, never advances the outer state. These statuses give no approximate convergence guarantee.

Facts & Assumptions

Given: The finite-dimensional problem data above, initial $(x^{0}, z^{0}, u^{0})$ , positive integer caps, and supplied solver and sound certificate-checker programs as specified in the Definition.

[A1]

The dimensions $n, m, p \in N$ may be zero; they match, $f, g$ are proper closed convex, $ρ > 0$ , caps are positive integers, and the supplied programs satisfy the Definition's step and certificate-soundness requirements.

[F1]

Proper closed convex extended-real functions on $R^{n}$ : each objective is proper, convex and has closed epigraph.

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : each residual space has its Euclidean inner product and norm.

[F3]

Every point has a unique nearest point in a nonempty closed Euclidean convex set: in positive-dimensional Euclidean space, every nonempty closed convex minimizer set has a unique point nearest the origin.

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of the single zero vector.

Verification

1.1A1F1F2givenalgebra

For either block write its subproblem objective as $F (v) + Q (v)$ , where $F$ is $f$ or $g$ and $Q$ is the finite continuous convex residual quadratic from [F2]. Its epigraph is the inverse image of the closed set $epi F$ under the continuous map $(v, s) \mapsto (v, s - Q (v))$ , so it is closed by [F1]. If its minimum is attained, the minimum value $a$ is finite: properness gives a finite competitor and neither summand takes $- \infty$ . Its minimizer set is nonempty and equals ${v : F (v) + Q (v) \leq a}$ , the inverse image of that closed epigraph under $v \mapsto (v, a)$ , hence is closed. The sum of the two convex functions is convex; at two minimizers, convexity bounds every segment value by $a$ , while minimality bounds it below by $a$ . Thus the minimizer set is convex.

2.1A1F3F4step 1.1givenalgebra∎

For either block, if its dimension is zero then [F4] makes its Euclidean space the singleton ${0}$ , so the nonempty minimizer set in step 1.1 is that singleton and its minimum-norm member is unique. In positive dimension, [F3] gives a unique point nearest the origin in the nonempty closed convex minimizer set. Thus, conditional on attainment, the specified tie-break exists and is unique in every dimension. The finite procedure calls the supplied solver and checker programs with the specified budget and preserves the old state on either failure branch; the existence of the tie-break does not provide a finite evaluator or imply that any cap succeeds.

DefinitionDefinition: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Fenchel conjugate of an extended-real function

Definition

Let $f : R^{n} \to (- \infty, + \infty]$ . Its Fenchel conjugate is the extended-real function on the same Euclidean space $f^{*} (s) : = \sup_{x \in R^{n}} {⟨ s, x ⟩ - f (x)} .$ When $f (x) = + \infty$ , the corresponding term is $- \infty$ and does not increase the supremum. Its effective domain is $dom f^{*} = {s : f^{*} (s) < + \infty}$ .

Facts & Assumptions

Given: $n \in N$ , $f : R^{n} \to (- \infty, + \infty]$ , and the Euclidean pairing.

[A1]

Function values lie in $(- \infty, + \infty]$ and the pairing is Euclidean.

[F1]

Proper closed convex extended-real functions on $R^{n}$ : the domain of a proper function is nonempty, and its values lie in $(- \infty, + \infty]$ .

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $⟨ s, x ⟩$ is a finite real number for $s, x \in R^{n}$ .

Proof

1.1A1givenF1F2given

For every $x$ with finite $f (x)$ , the expression $⟨ s, x ⟩ - f (x)$ is real; for $f (x) = + \infty$ it contributes $- \infty$ under the stated convention. Thus the supremum is unambiguously defined in $[- \infty, + \infty]$ .

2.1A1F1step 1.1choose∎

If $f$ is proper, choose one $x_{0} \in dom f$ . The finite term $⟨ s, x_{0} ⟩ - f (x_{0})$ shows $f^{*} (s) > - \infty$ for every $s$ ; it may still be $+ \infty$ . This definition alone does not assert finiteness everywhere.

DefinitionDefinition: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Resolvent of a monotone relation

Definition

For a relation $A \subseteq E \times E$ and $ρ > 0$ , define its resolvent as the inverse relation $J_{ρ A} : = (I + ρ A)^{- 1}, J_{ρ A} (y) = {x \in E : y - x \in ρ A (x)},$ where $ρ A (x) = {ρ a : a \in A (x)}$ . Its domain is the set of $y$ for which this value set is nonempty. At this point it may be partial and set-valued; full domain and single-valuedness are separate conclusions of A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive.

Facts & Assumptions

Given: A relation $A$ on $E$ and a scalar $ρ > 0$ .

[A1]

The relation is on $E$ and $ρ > 0$ .

[F1]

Monotone and maximal-monotone relations on Euclidean space: $A (x)$ denotes the set of $a$ with $(x, a) \in A$ .

Proof

1.1A1givenF1given

The equation $y - x \in ρ A (x)$ means that some $a \in A (x)$ satisfies $y = x + ρ a$ ; this is precisely the inverse graph of $I + ρ A$ .

2.1A1givenF1given∎

The value $J_{ρ A} (y)$ is a set and may be empty until a theorem proves existence; the definition itself asserts no surjectivity or uniqueness.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Optimality relations for exact two-block ADMM subproblems

Statement

For any exact two-block ADMM sweep from Scaled two-block ADMM with explicit capped-solve statuses, put $Δ z^{k + 1} = z^{k + 1} - z^{k}$ and $y^{k + 1} = ρ u^{k + 1}$ . Then $- K^{*} (y^{k + 1} - ρ L Δ z^{k + 1}) \in \partial f (x^{k + 1}), - L^{*} y^{k + 1} \in \partial g (z^{k + 1}) .$

Facts & Assumptions

Given: Proper convex $f, g$ , linear $K, L$ , $ρ > 0$ , and an exact attained sweep.

[A1]

The algorithm's proper closed convex objectives and linear maps are in force, and both subproblem minimizers are attained exactly.

[F1]

Scaled two-block ADMM with explicit capped-solve statuses: the exact $x$ and $z$ subproblems and update $y^{k + 1} = y^{k} + ρ r^{k + 1}$ are as displayed there.

[F2]

Subdifferentials of proper extended-real convex functions: for a proper convex extended-real function and a finite-valued point $x$ , $a \in \partial f (x)$ iff $f (v) \geq f (x) + ⟨ a, v - x ⟩$ for every $v$ ; the same convention applies to $g$ .

[F3]

Every linear map between finite-dimensional inner product spaces has a unique adjoint gives the unique adjoints of the finite-dimensional Euclidean maps $K, L$ ; The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ K x, y ⟩ = ⟨ x, K^{*} y ⟩$ and similarly for $L$ .

Proof

1.1A1F1F2F3givenalgebra

Write the $x$ -subproblem objective as $f (x) + Q (x)$ , where $\nabla Q (x^{k + 1}) = ρ K^{*} (K x^{k + 1} + L z^{k} - c + u^{k})$ by [F3]. For any $v \in dom f$ and $0 < t < 1$ , convexity bounds $f (x^{k + 1} + t (v - x^{k + 1}))$ above by $(1 - t) f (x^{k + 1}) + t f (v)$ . Minimality and differentiability of $Q$ , after dividing the resulting nonnegative objective difference by $t$ and letting $t ↓ 0$ , give $f (v) \geq f (x^{k + 1}) - ⟨ \nabla Q (x^{k + 1}), v - x^{k + 1} ⟩$ . For $v \notin dom f$ this inequality is automatic, so $- \nabla Q (x^{k + 1}) \in \partial f (x^{k + 1})$ by [F2].

2.1A1F1F2F3step 1.1algebra∎

Since $K x^{k + 1} + L z^{k} - c = r^{k + 1} - L Δ z^{k + 1}$ and $y^{k + 1} = ρ (u^{k} + r^{k + 1})$ , the gradient in step 1.1 equals $K^{*} (y^{k + 1} - ρ L Δ z^{k + 1})$ . This proves the first inclusion. Applying the same segment argument to the $z$ -subproblem gives $- ρ L^{*} (K x^{k + 1} + L z^{k + 1} - c + u^{k}) \in \partial g (z^{k + 1})$ ; the bracket times $ρ$ is $y^{k + 1}$ , proving the second inclusion.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The Fenchel conjugate of a proper closed convex function is proper closed convex

Statement

If $f : R^{n} \to (- \infty, + \infty]$ is proper, closed and convex, then its conjugate $f^{*}$ from Fenchel conjugate of an extended-real function is also proper, closed and convex. The affine-minorant result cited below is used only to prove properness; closedness and convexity follow directly from the supremum formula.

Facts & Assumptions

Given: Proper closed convex $f$ on $R^{n}$ .

[A1]

The function $f$ is proper, closed and convex.

[F1]

Fenchel conjugate of an extended-real function: $f^{*} (s) = \sup_{x} (⟨ s, x ⟩ - f (x))$ .

[F2]

A proper closed convex function has an affine minorant: some $a \in R^{n}, b \in R$ satisfy $f (x) \geq ⟨ a, x ⟩ + b$ for every $x$ .

[F3]

Proper closed convex extended-real functions on $R^{n}$ : $f$ has a nonempty effective domain, is convex, and has a closed epigraph.

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the pairing is bilinear and finite on all vectors.

[F5]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , and for $n \geq 1$ , $d_{2} (u, v) = ∥ u - v ∥_{2}$ .

Proof

1.1A1F1F2F3choose

Choose $x_{0} \in dom f$ by [F3]. The affine minorant [F2] gives $⟨ a, x ⟩ - f (x) \leq - b$ for every $x$ with finite $f (x)$ , so $f^{*} (a) \leq - b < + \infty$ . The term at $x_{0}$ gives $f^{*} (a) \geq ⟨ a, x_{0} ⟩ - f (x_{0}) > - \infty$ . Thus $f^{*}$ is proper.

1.2A1F1F4F5algebra

If $n = 0$ , [F4] gives the singleton $R^{0} = {0}$ and properness makes $f (0)$ finite, so $f^{*} (0) = - f (0)$ is proper, closed and convex directly. Hence assume $n \geq 1$ . For each $x \in dom f$ and $s, s^{'} \in R^{n}$ , [F5] gives $∣ ⟨ s, x ⟩ - ⟨ s^{'}, x ⟩ ∣ \leq ∥ s - s^{'} ∥_{2} ∥ x ∥_{2} = d_{2} (s, s^{'}) ∥ x ∥_{2}$ . Thus $s \mapsto ⟨ s, x ⟩ - f (x)$ is finite continuous affine. A pointwise supremum of these affine functions is convex: apply each affine function to $(1 - θ) s_{0} + θ s_{1}$ , bound by $(1 - θ) f^{*} (s_{0}) + θ f^{*} (s_{1})$ , then take the supremum.

2.1A1F1F3F4F5step 1.2algebra∎

The epigraph of $f^{*}$ is the intersection, over $x \in dom f$ , of the closed half-spaces ${(s, t) : t \geq ⟨ s, x ⟩ - f (x)} .$ Each half-space is closed because its defining affine function is continuous by step 1.2, and any intersection of closed sets is closed. Hence $f^{*}$ is closed in the epigraph convention of [F3].

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passOpen item page →

Fenchel–Young inequality and its equality case

Statement

Let $f : R^{n} \to (- \infty, + \infty]$ be proper and convex. For every $x, s \in R^{n}$ , $f (x) + f^{*} (s) \geq ⟨ s, x ⟩,$ with extended-real interpretation. Equality holds exactly when $x \in dom f$ , $f^{*} (s) < + \infty$ , and $s \in \partial f (x)$ ; equivalently, for proper convex $f$ , equality itself forces the two finiteness conditions and the subgradient membership.

Facts & Assumptions

Given: Proper convex $f$ , $x, s \in R^{n}$ .

[A1]

The function $f$ is proper and convex.

[F1]

Fenchel conjugate of an extended-real function: $f^{*} (s) = \sup_{z} (⟨ s, z ⟩ - f (z))$ .

[F2]

Subdifferentials of proper extended-real convex functions: for $x \in dom f$ , $s \in \partial f (x)$ iff $f (z) \geq f (x) + ⟨ s, z - x ⟩$ for every $z \in R^{n}$ .

Proof

1.1A1F1given

If $f (x) = + \infty$ , the left side is $+ \infty$ because [F1] and properness ensure $f^{*} (s) > - \infty$ , so the inequality is true and equality is impossible. If $f (x) < + \infty$ , the term $z = x$ in [F1] gives $f^{*} (s) \geq ⟨ s, x ⟩ - f (x)$ , proving the inequality; if $f^{*} (s) = + \infty$ , equality is again impossible.

2.1A1F1F2step 1.1algebra∎

Assume now $f (x)$ and $f^{*} (s)$ are finite. Equality in step 1.1 holds iff the supremum in [F1] equals its $z = x$ term, which is equivalent to $⟨ s, z ⟩ - f (z) \leq ⟨ s, x ⟩ - f (x) for every z \in dom f .$ Rearranging gives precisely the inequalities in [F2]; for $z \notin dom f$ they hold automatically. Thus equality is equivalent to $s \in \partial f (x)$ , and the converse follows by reversing these inequalities.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive

Statement

Let $A$ be maximal monotone on $E = R^{n}$ and let $ρ > 0$ . For every $y \in E$ there is a unique $x \in E$ with $y - x \in ρ A (x)$ . Thus the resolvent from Resolvent of a monotone relation is an everywhere-defined map and, for all $y, y^{'} \in E$ , $∥ J_{ρ A} y - J_{ρ A} y^{'} ∥_{2}^{2} \leq ⟨ J_{ρ A} y - J_{ρ A} y^{'}, y - y^{'} ⟩ .$ This is firm nonexpansiveness; it also implies the map is 1-Lipschitz.

Facts & Assumptions

Given: A maximal-monotone relation $A$ and $ρ > 0$ .

[A1]

The relation $A$ is maximal monotone and $ρ > 0$ .

[F1]

Monotone and maximal-monotone relations on Euclidean space: monotonicity means $⟨ x - x^{'}, a - a^{'} ⟩ \geq 0$ for graph pairs, and maximality excludes any proper monotone graph extension.

[F2]

Resolvent of a monotone relation: $x \in J_{ρ A} (y)$ iff $y = x + ρ a$ for some $a \in A (x)$ .

[F3]

One-point extension of a nonexpansive map in finite dimensions: a 1-Lipschitz map on any subset of $E$ admits a value at each added point satisfying all 1-Lipschitz inequalities.

[F4]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ v, w ⟩ ∣ \leq ∥ v ∥_{2} ∥ w ∥_{2}$ .

Proof

1.1A1F1constructalgebra

Transform every graph pair $(x, a) \in A$ into $p = x + ρ a$ and $q = x - ρ a$ . If two graph pairs are used, then $∥ q - q^{'} ∥_{2}^{2} \leq ∥ p - p^{'} ∥_{2}^{2},$ because the difference of the right and left sides is $4 ρ ⟨ x - x^{'}, a - a^{'} ⟩ \geq 0$ by [F1]. Also, if $p = p^{'}$ , this inequality forces $q = q^{'}$ . Thus the rule $T (p) = q$ is a well-defined 1-Lipschitz map on its range $D = {x + ρ a : (x, a) \in A}$ .

2.1A1F1F2F3step 1.1algebra

Fix arbitrary $y \in E$ . By [F3], extend $T$ at $y$ by some $q$ satisfying $∥ q - (x - ρ a) ∥_{2} \leq ∥ y - (x + ρ a) ∥_{2}$ for every $(x, a) \in A$ . Set $\tilde{x} = (y + q) / 2$ and $\tilde{a} = (y - q) / (2 ρ)$ . Expanding the squared inequality shows $⟨ \tilde{x} - x, \tilde{a} - a ⟩ \geq 0$ for every graph pair, so adjoining $(\tilde{x}, \tilde{a})$ preserves monotonicity. By maximality in [F1], it already belongs to $A$ . Hence $y = \tilde{x} + ρ \tilde{a}$ , proving existence. This also covers an initially empty graph: [F3] gives the extension and maximality rules out the empty graph.

3.1A1F1F2step 2.1algebra

If $x, x^{'}$ both satisfy $y - x \in ρ A (x)$ and $y - x^{'} \in ρ A (x^{'})$ , monotonicity gives $0 \leq ⟨ x - x^{'}, (y - x) - (y - x^{'}) ⟩ = - ∥ x - x^{'} ∥_{2}^{2}$ . Thus $x = x^{'}$ , so the resolvent is single-valued.

4.1A1F1F2F4step 3.1algebra∎

For inputs $y, y^{'}$ , write $x = J_{ρ A} y$ , $x^{'} = J_{ρ A} y^{'}$ . Monotonicity applied to $(x, (y - x) / ρ)$ and $(x^{'}, (y^{'} - x^{'}) / ρ)$ gives $∥ x - x^{'} ∥_{2}^{2} \leq ⟨ x - x^{'}, y - y^{'} ⟩ .$ Cauchy–Schwarz [F4] then gives $∥ x - x^{'} ∥_{2} \leq ∥ y - y^{'} ∥_{2}$ when $x \neq x^{'}$ , and the inequality is immediate when $x = x^{'}$ . This proves firm nonexpansiveness and the Lipschitz consequence.

AlgorithmAlgorithm: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Douglas–Rachford splitting for two maximal-monotone relations

Definition

Given maximal-monotone $A, B$ on $E = R^{n}$ , $ρ > 0$ , and $w_{0} \in E$ , define for $k \geq 0$ $p_{k} = J_{ρ B} (w_{k}), q_{k} = J_{ρ A} (2 p_{k} - w_{k}), w_{k + 1} = w_{k} + q_{k} - p_{k} .$ The shadow is $p_{k}$ . Each exact update exists and is unique by A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive. This recurrence specifies exact real arithmetic; a finite implementation that cannot evaluate a resolvent must report failure and must not advance the exact recurrence. No termination or convergence claim is part of this algorithm definition.

Facts & Assumptions

Given: Maximal-monotone $A, B$ , $ρ > 0$ , and a state $w_{k} \in E$ .

[A1]

Both relations are maximal monotone, $ρ > 0$ , and $w_{0} \in E$ .

[F1]

Resolvent of a monotone relation: $J_{ρ A} (y) = {x : y - x \in ρ A (x)}$ , and similarly for $B$ .

[F2]

A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive: each such resolvent is a unique-valued map defined on all of $E$ .

Proof

1.1A1givenF1F2

Since $w_{k} \in E$ , [F2] gives a unique $p_{k}$ and then a unique $q_{k}$ at the input $2 p_{k} - w_{k}$ . The displayed formula therefore defines exactly one next state $w_{k + 1}$ .

2.1A1givenF1F2given∎

If a numerical routine does not return those exact resolvent values, the recurrence has not been completed; the item makes no convergence or approximate-solve assertion. The shadow sequence is precisely the first resolvent output $p_{k}$ .

AlgorithmAlgorithm: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Chambolle–Pock primal-dual hybrid gradient

Definition

Let $X = R^{n}$ , $Y = R^{m}$ , let $f : X \to (- \infty, + \infty]$ and $g : Y \to (- \infty, + \infty]$ be proper closed convex, and let $K : X \to Y$ be linear. Its unique adjoint $K^{*} : Y \to X$ exists by Every linear map between finite-dimensional inner product spaces has a unique adjoint, including zero-dimensional spaces. Identify $K$ with its matrix in the standard Euclidean bases when using the induced matrix norm below. The primal problem is $\min_{x} f (x) + g (K x)$ , with saddle function $Φ (x, y) = f (x) + ⟨ K x, y ⟩ - g^{*} (y),$ where $g^{*}$ is defined by Fenchel conjugate of an extended-real function. The saddle function $Φ$ is evaluated on $dom f \times dom g^{*}$ , where both function values are finite; no undefined extended-real subtraction is used outside this domain. Assume $τ, σ > 0$ and $τ σ ∥ K ∥_{2}^{2} < 1$ , where $∥ K ∥_{2}$ is the induced Euclidean operator norm of The matrix norm induced by a published vector p-norm. Starting from $x^{0}, y^{0}$ and ${\overset{ˉ}{x}}^{0} = x^{0}$ , the exact recurrence is $y^{k + 1} = {prox}_{σ g^{*}} (y^{k} + σ K {\overset{ˉ}{x}}^{k}), x^{k + 1} = {prox}_{τ f} (x^{k} - τ K^{*} y^{k + 1}), {\overset{ˉ}{x}}^{k + 1} = 2 x^{k + 1} - x^{k} .$ In positive-dimensional spaces the proximal maps are everywhere single-valued by Existence, resolvent characterization, and firm nonexpansiveness of the proximal map; in a zero-dimensional space its sole input and output are the zero vector, so that proximal call is single-valued directly. The proper closed convexity of $g^{*}$ follows from The Fenchel conjugate of a proper closed convex function is proper closed convex. These are mathematical existence statements, not finite evaluators.

The finite procedure also takes positive integer caps $C_{y}, C_{x}$ and supplied deterministic solver programs $S_{y}, S_{x}$ and Boolean certificate-checker programs $V_{y}, V_{x}$ , with their complete instructions and data representations. Each program uses discrete steps that terminate. On input $(h, t, v)$ , a solver may halt with failed or a candidate-certificate pair $(w, e)$ . The supplied checker is admissible only if $V (h, t, v, w, e) = t r u e$ implies that $h (w)$ is finite and $w$ minimizes $h (z) + ∥ z - v ∥_{2}^{2} / (2 t)$ over all $z$ in its Euclidean space. This is a soundness condition on supplied programs; it does not promise that an arbitrary proximal map has an exact finite evaluator or that a certificate is always found. Proper closed convexity and the strict step-size condition remain admissibility assumptions on the mathematical data.

Initialize ${\overset{ˉ}{x}}^{0} = x^{0}$ . At each sweep retain the old state $(x^{k}, y^{k}, {\overset{ˉ}{x}}^{k})$ . Return invalid-input for mismatched dimensions, nonpositive $τ$ or $σ$ , or caps that are not positive integers. First call $S_{y}$ on $(g^{*}, σ, y^{k} + σ K {\overset{ˉ}{x}}^{k})$ , then, if it returns $(w, e)$ , call $V_{y}$ on those inputs and that pair. Allow at most $C_{y}$ program steps in total for the solver and checker. After each step inspect for termination: an explicit failure, malformed output, or false checker result returns prox-call-failed with call = dual; a true result stores $w$ as tentative $y^{k + 1}$ . Accept a true result on the last allowed step. If the budget is used without such a result or failure, return prox-cap-exhausted with call = dual. After dual success, apply the identical rule with $S_{x}, V_{x}, C_{x}$ to $(f, τ, x^{k} - τ K^{*} y^{k + 1})$ , recording call = primal on failure or exhaustion. Every failure returns the unchanged old state. Only after both calls succeed, commit $x^{k + 1}, y^{k + 1}$ and ${\overset{ˉ}{x}}^{k + 1} = 2 x^{k + 1} - x^{k}$ , and return success with this state. A requested finite run repeats this sweep for an input nonnegative integer number of sweeps and stops at its first nonsuccess status. No convergence claim is made for a failed run.

Facts & Assumptions

Given: Proper closed convex $f, g$ , finite Euclidean spaces, linear $K$ , positive $τ, σ$ satisfying the strict step condition, initial $x^{0}, y^{0}$ , positive integer caps and the supplied solver and sound certificate-checker programs in the Definition.

[A1]

The functions are proper closed convex; $τ, σ > 0$ ; $τ σ ∥ K ∥_{2}^{2} < 1$ ; caps are positive integers; and the supplied programs satisfy the Definition's step and certificate-soundness requirements.

[F1]

Proper closed convex extended-real functions on $R^{n}$ : $f, g$ are proper closed convex functions.

[F2]

Fenchel conjugate of an extended-real function: $g^{*} (y) = \sup_{v} (⟨ y, v ⟩ - g (v))$ .

[F3]

The Fenchel conjugate of a proper closed convex function is proper closed convex: $g^{*}$ is proper closed convex.

[F4]

Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: for each positive-dimensional space, every input and positive parameter give a unique proximal output satisfying its subgradient optimality condition.

[F5]

The matrix norm induced by a published vector p-norm: $∥ K ∥_{2} = \sup_{∥ x ∥_{2} \leq 1} ∥ K x ∥_{2}$ .

[F6]

Every linear map between finite-dimensional inner product spaces has a unique adjoint gives the unique finite-dimensional adjoint; The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ K x, y ⟩ = ⟨ x, K^{*} y ⟩$ .

[F7]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of the single zero vector.

Verification

1.1A1F1F2F3F4F7given

By [F1] and [F3], both proximal inputs in the recurrence are proper closed convex functions; [F2] supplies the defining conjugate expression for the dual term. If a proximal space has positive dimension, [F4] gives an everywhere unique output. If it is zero-dimensional, [F7] makes it the singleton ${0}$ and properness gives the unique zero output directly. Since $τ, σ > 0$ , every exact update exists uniquely, including when $K = 0$ ; the strict step inequality then reads $0 < 1$ .

2.1A1F5F6givenF4∎

The three assignments specify the exact state and extrapolated value; $K^{*}$ in the primal update is the adjoint of [F6], and the step-size condition uses the induced norm [F5]. The finite wrapper separately specifies supplied solver/checker programs, their ordered calls, shared per-call budgets and distinct failure versus exhaustion branches. Its certificates concern exactly the unique proximal outputs of [F4]; their existence alone supplies no evaluator. No pointwise convergence is asserted.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Two-block ADMM energy descent and objective gap estimates

Statement

Suppose proper closed convex $f, g$ have a saddle point $(x_{*}, z_{*}, y_{*})$ for the Lagrangian in Scaled two-block ADMM with explicit capped-solve statuses, with $K x_{*} + L z_{*} = c$ , and every subproblem in the exact ADMM sequence is attained. Put $Δ z^{k + 1} = z^{k + 1} - z^{k}$ and $V^{k} = \frac{1}{ρ} ∥ y^{k} - y_{*} ∥_{2}^{2} + ρ ∥ L (z^{k} - z_{*}) ∥_{2}^{2} .$ For every $k \geq 1$ , $V^{k + 1} \leq V^{k} - ρ ∥ r^{k + 1} ∥_{2}^{2} - ρ ∥ L Δ z^{k + 1} ∥_{2}^{2} .$ The index begins at $k = 1$ : an arbitrary initial $z^{0}$ need not satisfy a previous $z$ -subproblem optimality condition. Also, with $p_{k} = f (x^{k}) + g (z^{k})$ and $p_{*} = f (x_{*}) + g (z_{*})$ , every exact sweep satisfies $p_{k + 1} - p_{*} \leq - ⟨ y^{k + 1}, r^{k + 1} ⟩ + ρ ⟨ L Δ z^{k + 1}, r^{k + 1} - L (z^{k + 1} - z_{*}) ⟩,$ $p_{*} - p_{k + 1} \leq ⟨ y_{*}, r^{k + 1} ⟩ .$

Facts & Assumptions

Given: A saddle point, exact ADMM sweeps, $ρ > 0$ , and the notation above.

[A1]

A saddle point exists, $ρ > 0$ , and every ADMM subproblem is attained exactly.

[F1]

Scaled two-block ADMM with explicit capped-solve statuses: $r^{k + 1} = K x^{k + 1} + L z^{k + 1} - c$ and $y^{k + 1} - y^{k} = ρ r^{k + 1}$ .

[F2]

Optimality relations for exact two-block ADMM subproblems: $a^{k + 1} = - K^{*} y^{k + 1} + ρ K^{*} L Δ z^{k + 1} \in \partial f (x^{k + 1})$ and $b^{k + 1} = - L^{*} y^{k + 1} \in \partial g (z^{k + 1})$ .

[F3]

Saddle points of extended-real Lagrangians: $L ((x_{*}, z_{*}), y) \leq p_{*} \leq L ((x, z), y_{*})$ for every $x, z, y$ , with the center finite.

[F4]

Subdifferentials of proper extended-real convex functions: for a finite-valued point of a proper convex extended-real function, each subgradient gives its defining inequality against every competitor.

[F5]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : adjoints move $K, L$ between inner products.

Proof

1.1A1F2F3F4F5givenalgebra

For every $x \in dom f$ , the right saddle inequality at $(x, z_{*})$ and feasibility give $f (x) \geq f (x_{*}) + ⟨ - K^{*} y_{*}, x - x_{*} ⟩$ ; the same argument with $(x_{*}, z)$ gives $- L^{*} y_{*} \in \partial g (z_{*})$ . Thus [F4] gives both saddle subgradient inclusions. For $k \geq 1$ , the preceding exact sweep also gives $- L^{*} y^{k} \in \partial g (z^{k})$ from [F2]. The inequalities at $z^{k + 1}$ and $z^{k}$ read $g (z^{k + 1}) - g (z^{k}) \leq - ⟨ y^{k + 1}, L Δ z^{k + 1} ⟩$ and $g (z^{k + 1}) - g (z^{k}) \geq - ⟨ y^{k}, L Δ z^{k + 1} ⟩$ . Combining them gives $⟨ y^{k + 1} - y^{k}, L Δ z^{k + 1} ⟩ \leq 0$ . This is the sign needed below and is why the estimate starts at $k = 1$ .

2.1A1F2F3F4F5step 1.1algebra

Adding the two defining subgradient inequalities shows subgradient monotonicity. At the $f$ -block this gives $0 \leq ⟨ a^{k + 1} + K^{*} y_{*}, x^{k + 1} - x_{*} ⟩ = - ⟨ y^{k + 1} - y_{*}, K (x^{k + 1} - x_{*}) ⟩ + ρ ⟨ L Δ z^{k + 1}, K (x^{k + 1} - x_{*}) ⟩ .$ At the $g$ -block it gives $0 \leq ⟨ b^{k + 1} + L^{*} y_{*}, z^{k + 1} - z_{*} ⟩ = - ⟨ y^{k + 1} - y_{*}, L (z^{k + 1} - z_{*}) ⟩$ . Add the two inequalities and use $K x_{*} + L z_{*} = c$ to obtain $⟨ y^{k + 1} - y_{*}, r^{k + 1} ⟩ \leq ρ ⟨ L Δ z^{k + 1}, K (x^{k + 1} - x_{*}) ⟩ .$ Substitute $K (x^{k + 1} - x_{*}) = r^{k + 1} - L (z^{k + 1} - z_{*})$ .

3.1A1F1step 1.1step 2.1algebra

The identity $y^{k + 1} - y^{k} = ρ r^{k + 1}$ gives $\frac{∥ y^{k + 1} - y_{*} ∥^{2} - ∥ y^{k} - y_{*} ∥^{2}}{ρ} = 2 ⟨ y^{k + 1} - y_{*}, r^{k + 1} ⟩ - ρ ∥ r^{k + 1} ∥^{2} .$ The analogous expansion for $L (z^{k} - z_{*})$ is $ρ (∥ L (z^{k + 1} - z_{*}) ∥^{2} - ∥ L (z^{k} - z_{*}) ∥^{2}) = 2 ρ ⟨ L Δ z^{k + 1}, L (z^{k + 1} - z_{*}) ⟩ - ρ ∥ L Δ z^{k + 1} ∥^{2} .$ Add these identities, use step 2.1, and then use step 1.1 to bound $2 ⟨ y^{k + 1} - y^{k}, L Δ z^{k + 1} ⟩ \leq 0$ . The asserted energy descent follows.

4.1A1F2F3F4step 2.1algebra∎

The two subgradient inequalities [F2,F4] at $(x^{k + 1}, z^{k + 1})$ against $(x_{*}, z_{*})$ give $p_{k + 1} - p_{*} \leq ⟨ a^{k + 1}, x^{k + 1} - x_{*} ⟩ + ⟨ b^{k + 1}, z^{k + 1} - z_{*} ⟩ = - ⟨ y^{k + 1}, r^{k + 1} ⟩ + ρ ⟨ L Δ z^{k + 1}, K (x^{k + 1} - x_{*}) ⟩ .$ Replace $K (x^{k + 1} - x_{*})$ by $r^{k + 1} - L (z^{k + 1} - z_{*})$ to obtain the upper estimate. The right saddle inequality [F3] at $(x^{k + 1}, z^{k + 1})$ is $p_{k + 1} + ⟨ y_{*}, r^{k + 1} ⟩ \geq p_{*}$ , which rearranges to the lower estimate.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The Douglas–Rachford fixed-point map is firmly nonexpansive

Statement

For maximal-monotone $A, B$ and $ρ > 0$ , let $T = I - J_{ρ B} + J_{ρ A} (2 J_{ρ B} - I) .$ Then $T : E \to E$ is firmly nonexpansive: $∥ T (w) - T (w^{'}) ∥_{2}^{2} \leq ⟨ T (w) - T (w^{'}), w - w^{'} ⟩ .$

Facts & Assumptions

Given: Maximal-monotone $A, B$ , $ρ > 0$ , and $w, w^{'} \in E$ .

[A1]

Both relations are maximal monotone, $ρ > 0$ , and the inputs lie in $E$ .

[F1]

Douglas–Rachford splitting for two maximal-monotone relations: the update map is $T (w) = w + J_{ρ A} (2 J_{ρ B} w - w) - J_{ρ B} w$ .

[F2]

A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive: each resolvent $J$ obeys $∥ J v - J v^{'} ∥^{2} \leq ⟨ J v - J v^{'}, v - v^{'} ⟩$ .

Proof

1.1A1F2algebra

For any firmly nonexpansive $J$ , its reflector $R = 2 J - I$ is nonexpansive: with $d = v - v^{'}$ and $e = J v - J v^{'}$ , [F2] gives $∥ 2 e - d ∥_{2}^{2} = ∥ d ∥_{2}^{2} + 4 ∥ e ∥_{2}^{2} - 4 ⟨ e, d ⟩ \leq ∥ d ∥_{2}^{2} .$ Thus $R_{A} R_{B}$ is nonexpansive because it is a composition of two nonexpansive maps.

2.1A1F1step 1.1algebra∎

Expanding the reflectors gives $T = (I + R_{A} R_{B}) / 2$ . For $d = w - w^{'}$ and $s = R_{A} R_{B} w - R_{A} R_{B} w^{'}$ , nonexpansiveness gives $∥ s ∥_{2} \leq ∥ d ∥_{2}$ , and ${∥ \frac{d + s}{2} ∥}_{2}^{2} \leq ⟨ \frac{d + s}{2}, d ⟩$ is equivalent after multiplying by $4$ and cancelling common terms to $∥ s ∥_{2}^{2} \leq ∥ d ∥_{2}^{2}$ . This is the firm inequality for $T$ .

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

PDHG one-step primal-dual gap telescope

Statement

For the exact recurrence of Chambolle–Pock primal-dual hybrid gradient, put $κ = \sqrt{τ σ} ∥ K ∥_{2} < 1$ and $Φ (x, y) = f (x) + ⟨ K x, y ⟩ - g^{*} (y)$ . For every $x \in dom f$ , $y \in dom g^{*}$ and integer $N \geq 1$ , $\sum_{k = 0}^{N - 1} (Φ (x^{k + 1}, y) - Φ (x, y^{k + 1})) \leq \frac{∥ x - x^{0} ∥_{2}^{2}}{2 τ} + \frac{∥ y - y^{0} ∥_{2}^{2}}{2 σ} .$ The formula includes $K = 0$ and uses ${\overset{ˉ}{x}}^{0} = x^{0}$ .

Facts & Assumptions

Given: The exact PDHG recurrence, $τ, σ > 0$ , $κ < 1$ , and test points in the stated domains.

[A1]

The exact recurrence is used, $κ = \sqrt{τ σ} ∥ K ∥_{2} < 1$ , and the test points are in the stated domains.

[F1]

Chambolle–Pock primal-dual hybrid gradient: the proximal updates, ${\overset{ˉ}{x}}^{0} = x^{0}$ , and ${\overset{ˉ}{x}}^{k} = 2 x^{k} - x^{k - 1}$ for $k \geq 1$ .

[F2]

Existence, resolvent characterization, and firm nonexpansiveness of the proximal map: in positive dimension, if $u = {prox}_{t g} (v)$ , then $(v - u) / t \in \partial g (u)$ .

[F3]

Subdifferentials of proper extended-real convex functions: for a finite-valued point of a proper convex extended-real function, $a \in \partial f (u)$ implies $f (z) \geq f (u) + ⟨ a, z - u ⟩$ for every $z$ .

[F4]

The matrix norm induced by a published vector p-norm: $∥ K x ∥_{2} \leq ∥ K ∥_{2} ∥ x ∥_{2}$ .

[F5]

[F6]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of the single zero vector.

Proof

1.1A1F1F2F3F5F6algebra

For each positive-dimensional proximal space, the optimality condition [F2] and extended-real subgradient definition [F3] give the relevant inequality. If a proximal space is zero-dimensional, [F6] says its only point is $0$ ; its update and test point are both $0$ , so the same inequality is equality in that coordinate. Therefore in every dimension the two inequalities are $g^{*} (y) - g^{*} (y^{k + 1}) \geq ⟨ \frac{y^{k} - y^{k + 1}}{σ} + K {\overset{ˉ}{x}}^{k}, y - y^{k + 1} ⟩,$ $f (x) - f (x^{k + 1}) \geq ⟨ \frac{x^{k} - x^{k + 1}}{τ} - K^{*} y^{k + 1}, x - x^{k + 1} ⟩ .$ The identity $- ⟨ a - b, c - b ⟩ = (∥ c - a ∥^{2} - ∥ c - b ∥^{2} - ∥ b - a ∥^{2}) / 2$ applied to the primal and dual displacement terms gives the two distance differences $E_{k} - E_{k + 1} - X_{k + 1}$ and $E_{k} - E_{k + 1} - Y_{k + 1}$ in their respective coordinates. The bilinear terms from the primal inequality and the gap expand as $⟨ y^{k + 1}, K (x - x^{k + 1}) ⟩ + ⟨ K x^{k + 1}, y ⟩ - ⟨ K x, y^{k + 1} ⟩ = ⟨ K x^{k + 1}, y - y^{k + 1} ⟩$ . Adding the dual update term $⟨ K {\overset{ˉ}{x}}^{k}, y^{k + 1} - y ⟩$ gives $⟨ K ({\overset{ˉ}{x}}^{k} - x^{k + 1}), y^{k + 1} - y ⟩$ in the upper bound for $G_{k + 1}$ . Moving this term to the other side yields $E_{k} \geq G_{k + 1} + E_{k + 1} + X_{k + 1} + Y_{k + 1} + ⟨ K (x^{k + 1} - {\overset{ˉ}{x}}^{k}), y^{k + 1} - y ⟩,$ where $G_{k + 1} = Φ (x^{k + 1}, y) - Φ (x, y^{k + 1})$ , $E_{j} = ∥ x - x^{j} ∥^{2} / (2 τ) + ∥ y - y^{j} ∥^{2} / (2 σ)$ , $X_{j} = ∥ x^{j} - x^{j - 1} ∥^{2} / (2 τ)$ , and $Y_{j} = ∥ y^{j} - y^{j - 1} ∥^{2} / (2 σ)$ .

2.1A1F1F4F5step 1.1algebra

Define $x^{- 1} = x^{0}$ , so $X_{0} = 0$ , and $B_{k} = ⟨ K (x^{k} - x^{k - 1}), y^{k} - y ⟩$ . The extrapolation in [F1] gives $⟨ K (x^{k + 1} - {\overset{ˉ}{x}}^{k}), y^{k + 1} - y ⟩ = B_{k + 1} - B_{k} - ⟨ K (x^{k} - x^{k - 1}), y^{k + 1} - y^{k} ⟩ .$ By [F4,F5] and $2 a b \leq a^{2} + b^{2}$ , $∣ ⟨ K (x^{k} - x^{k - 1}), y^{k + 1} - y^{k} ⟩ ∣ \leq κ (X_{k} + Y_{k + 1}) .$ Substitution into step 1.1 therefore gives $E_{k} \geq G_{k + 1} + E_{k + 1} + (1 - κ) Y_{k + 1} + X_{k + 1} - κ X_{k} + B_{k + 1} - B_{k} .$

3.1A1F1F4F5step 2.1algebra∎

Sum step 2.1 for $k = 0, \dots, N - 1$ . The $B$ terms telescope, $B_{0} = 0$ , and the $X$ terms satisfy $\sum_{k = 0}^{N - 1} (X_{k + 1} - κ X_{k}) = (1 - κ) \sum_{k = 1}^{N - 1} X_{k} + X_{N} \geq 0$ . Thus $\sum_{k = 0}^{N - 1} G_{k + 1} + E_{N} + (1 - κ) \sum_{k = 1}^{N} Y_{k} + (1 - κ) \sum_{k = 1}^{N - 1} X_{k} + X_{N} + B_{N} \leq E_{0} .$ For the terminal cross term, [F4,F5] and $2 a b \leq a^{2} + b^{2}$ give $- B_{N} \leq ∥ K ∥_{2} ∥ x^{N} - x^{N - 1} ∥_{2} ∥ y^{N} - y ∥_{2} \leq X_{N} + τ σ ∥ K ∥_{2}^{2} \frac{∥ y^{N} - y ∥_{2}^{2}}{2 σ} .$ Since $E_{N}$ contains $∥ y^{N} - y ∥^{2} / (2 σ)$ and $τ σ ∥ K ∥_{2}^{2} = κ^{2} < 1$ , these terminal terms leave a nonnegative remainder; all increment terms are also nonnegative because $κ < 1$ . Drop them to obtain $\sum G_{k + 1} \leq E_{0}$ , the claimed estimate. When $K = 0$ , $κ = 0$ and the same inequalities hold without division by $∥ K ∥_{2}$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

Two-block ADMM residual, objective and dual sequence convergence

Statement

Use the equality-constrained problem and exact recurrence of Scaled two-block ADMM with explicit capped-solve statuses. Suppose $f, g$ are proper closed convex, a Lagrangian saddle point $(x_{*}, z_{*}, y_{*})$ exists, $ρ > 0$ , and every outer subproblem is attained exactly. Write $p_{*} = f (x_{*}) + g (z_{*})$ . Then $r^{k} \to 0, f (x^{k}) + g (z^{k}) \to p_{*}, y^{k} \to \overset{ˉ}{y}$ for some dual optimum $\overset{ˉ}{y}$ of $d (y) = \inf_{x, z} L ((x, z), y)$ . The theorem does not assert convergence of $x^{k}$ or $z^{k}$ .

Facts & Assumptions

Given: The stated finite-dimensional problem, one saddle point, $ρ > 0$ , and an exact attained ADMM sequence.

[A1]

A saddle point exists, $ρ > 0$ , and every ADMM subproblem is attained exactly.

[F1]

Scaled two-block ADMM with explicit capped-solve statuses: the exact recurrence, residual $r^{k}$ , unscaled dual $y^{k} = ρ u^{k}$ , and Lagrangian $L ((x, z), y)$ .

[F2]

Saddle points of extended-real Lagrangians: $L ((x_{*}, z_{*}), y) \leq p_{*} \leq L ((x, z), y_{*})$ for all $x, z, y$ .

[F3]

Two-block ADMM energy descent and objective gap estimates: from $k \geq 1$ , the energy descends by $ρ (∥ r^{k + 1} ∥^{2} + ∥ L Δ z^{k + 1} ∥^{2})$ and the two one-sided objective estimates hold.

[F4]

Fenchel conjugate of an extended-real function: $f^{*} (s) = \sup_{x} (⟨ s, x ⟩ - f (x))$ and likewise for $g^{*}$ .

[F5]

The Fenchel conjugate of a proper closed convex function is proper closed convex: the conjugate of a proper closed convex function is proper, closed and convex, in particular it never takes $- \infty$ .

[F6]

Fenchel–Young inequality and its equality case: $f (x) + f^{*} (s) = ⟨ s, x ⟩$ iff $s \in \partial f (x)$ with the required finite values.

[F7]

For $n \geq 1$ every bounded sequence in $R^{n}$ has a convergent subsequence: for a positive dimension, every bounded sequence in that finite-dimensional Euclidean space has a convergent subsequence.

[F8]

Optimality relations for exact two-block ADMM subproblems: each exact sweep has the stated $f$ - and $g$ -subgradient inclusions.

[F9]

[F10]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $R^{0}$ consists of the single zero vector.

Proof

1.1A1F1F2givencontradiction

The left saddle inequality forces $K x_{*} + L z_{*} = c$ : otherwise taking $y = y_{*} + t (K x_{*} + L z_{*} - c)$ and letting $t \to + \infty$ contradicts its finite upper bound. The right saddle inequality then says every feasible pair has objective at least $p_{*}$ , so $(x_{*}, z_{*})$ is primal optimal. For every $y$ , the dual value $d (y)$ is at most $L ((x_{*}, z_{*}), y) = p_{*}$ . At $y_{*}$ , the right saddle inequality gives $d (y_{*}) \geq p_{*}$ ; hence $d (y_{*}) = p_{*}$ and $y_{*}$ is dual optimal.

1.2A1F1F3F8algebra

The subgradient inequalities underlying [F3] imply, for every fixed $x, z$ and every sweep, $f (x) + g (z) + ⟨ y^{k + 1}, K x + L z - c ⟩ \geq p_{k + 1} + ⟨ y^{k + 1}, r^{k + 1} ⟩ + ρ ⟨ L Δ z^{k + 1}, K x - K x^{k + 1} ⟩ .$ Indeed, apply the $f$ - and $g$ -subgradient inclusions [F8] at the new iterates, use their defining inequalities, add them, and substitute $K x^{k + 1} + L z^{k + 1} - c = r^{k + 1}$ .

2.1A1F1F2F4F5F6step 1.1algebraalgebra

Fixing $z = z_{*}$ and then $x = x_{*}$ in the right saddle inequality gives $- K^{*} y_{*} \in \partial f (x_{*})$ and $- L^{*} y_{*} \in \partial g (z_{*})$ . By [F6], $f (x_{*}) + f^{*} (- K^{*} y_{*}) = - ⟨ y_{*}, K x_{*} ⟩, g (z_{*}) + g^{*} (- L^{*} y_{*}) = - ⟨ y_{*}, L z_{*} ⟩ .$ Each component infimum is below a finite value because $f, g$ are proper, so neither equals $+ \infty$ . If both are finite, choosing independent points within any $ϵ > 0$ of them proves that the joint infimum is their sum; if either is $- \infty$ , fixing a finite competitor in the other block and sending the first block value down shows the joint infimum is $- \infty$ . Thus separating the $x$ and $z$ infima and using [F4] gives the extended-real identity $d (y) = - f^{*} (- K^{*} y) - g^{*} (- L^{*} y) - ⟨ y, c ⟩ .$ The terms are well-defined because [F5] excludes $- \infty$ conjugate values. Substituting the two equalities and feasibility into the formula gives $d (y_{*}) = p_{*}$ . The dual solution set $Y_{*} : = {y : d (y) = p_{*}}$ is nonempty. Weak duality gives $d (y) \leq p_{*}$ , so $y \in Y_{*}$ iff $L ((x, z), y) \geq p_{*}$ for every $x, z$ . Each finite-valued pair $(x, z)$ imposes a closed affine half-space in $y$ ; an infinite-valued pair imposes no restriction. Thus $Y_{*}$ is closed and convex as an intersection of closed convex sets.

2.2A1F3step 1.1algebra

Sum the descent inequality [F3] from $k = 1$ to $N$ . Since $V^{N + 1} \geq 0$ , $\sum_{k = 1}^{N} (∥ r^{k + 1} ∥_{2}^{2} + ∥ L Δ z^{k + 1} ∥_{2}^{2}) \leq V^{1} / ρ .$ Each nonnegative term of a convergent bounded partial sum tends to zero, so $r^{k} \to 0$ and $L Δ z^{k} \to 0$ . The energy bound also makes $y^{k}$ and $L (z^{k} - z_{*})$ bounded.

3.1A1F3F9step 2.2algebra

The objective estimates [F3] now force convergence. In the upper estimate, $⟨ y^{k + 1}, r^{k + 1} ⟩ \to 0$ by boundedness and residual convergence; both terms paired with $L Δ z^{k + 1}$ tend to zero because $r^{k + 1} \to 0$ and $L (z^{k + 1} - z_{*})$ is bounded. The lower estimate $p_{*} - p_{k + 1} \leq ⟨ y_{*}, r^{k + 1} ⟩$ also tends to zero. Hence $p_{k + 1} \to p_{*}$ .

4.1A1F1F2step 1.1step 2.2step 3.1step 1.2algebra

Along any convergent subsequence $y^{k_{j} + 1} \to \overset{ˉ}{y}$ , the quantities $K x^{k_{j} + 1} = c - L z^{k_{j} + 1} + r^{k_{j} + 1}$ are bounded by step 2.2. Taking limits in step 1.2, using steps 2.2 and 3.1, gives $f (x) + g (z) + ⟨ \overset{ˉ}{y}, K x + L z - c ⟩ \geq p_{*} for all x, z .$ Since the primal optimizer is feasible, $d (\overset{ˉ}{y}) \geq p_{*}$ , while weak duality from step 1.1 gives $d (\overset{ˉ}{y}) \leq p_{*}$ . Thus every dual cluster point belongs to $Y_{*}$ . The inequality at the fixed primal optimizer also makes it a saddle point with $\overset{ˉ}{y}$ .

5.1A1F3F7F10step 2.1step 2.2step 4.1algebra

If $p = 0$ , then $R^{p} = {0}$ by [F10], so $y^{k} = 0$ for every $k$ ; step 2.1 shows this unique dual vector is optimal, and dual convergence follows. Assume henceforth $p \geq 1$ . Boundedness from step 2.2 and [F7] give at least one dual cluster point. Let $y_{1}, y_{2} \in Y_{*}$ be any two cluster points. Each pairs with the same primal optimizer to form a saddle point, so [F3] makes both energy sequences $V^{k} (y_{i}) = ρ^{- 1} ∥ y^{k} - y_{i} ∥_{2}^{2} + ρ ∥ L (z^{k} - z_{*}) ∥_{2}^{2} (i = 1, 2)$ nonincreasing from $k = 1$ and bounded below; each therefore converges. Expanding the two squared norms gives $V^{k} (y_{1}) - V^{k} (y_{2}) = \frac{2}{ρ} ⟨ y^{k}, y_{2} - y_{1} ⟩ + \frac{∥ y_{1} ∥_{2}^{2} - ∥ y_{2} ∥_{2}^{2}}{ρ},$ so $⟨ y^{k}, y_{2} - y_{1} ⟩$ converges. Along subsequences tending to $y_{1}$ and $y_{2}$ the limits are equal, so $⟨ y_{1} - y_{2}, y_{2} - y_{1} ⟩ = - ∥ y_{1} - y_{2} ∥_{2}^{2} = 0$ and $y_{1} = y_{2}$ .

6.1A1F7step 5.1contradiction∎

In the remaining case $p \geq 1$ , there is exactly one cluster point. If the bounded sequence $y^{k}$ did not converge to it, some subsequence would stay a fixed positive distance away; [F7] would give a convergent subsubsequence with a different cluster point, a contradiction. Therefore the whole unscaled dual sequence converges to a point of $Y_{*}$ . No convergence of primal iterates was used.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Douglas–Rachford shadows converge to a zero of the operator sum

Statement

Let $A, B$ be maximal monotone on $E = R^{n}$ , let $ρ > 0$ , and assume there is $p \in E$ with $0 \in (A + B) (p)$ , meaning that $a \in A (p)$ and $b \in B (p)$ can be chosen with $a + b = 0$ . The Douglas–Rachford recurrence of Douglas–Rachford splitting for two maximal-monotone relations has a state sequence converging to a fixed point of its map $T$ , and its shadow $J_{ρ B} (w_{k})$ converges to a zero of $A + B$ .

Facts & Assumptions

Given: $A, B, ρ, p$ as in the Statement.

[A1]

Both relations are maximal monotone, $ρ > 0$ , and $0 \in (A + B) (p)$ for some $p$ .

[F1]

Douglas–Rachford splitting for two maximal-monotone relations: $T (w) = w + q - p_{B}$ , where $p_{B} = J_{ρ B} w$ and $q = J_{ρ A} (2 p_{B} - w)$ .

[F2]

The Douglas–Rachford fixed-point map is firmly nonexpansive: $T$ is firmly nonexpansive.

[F3]

Picard iterates of a firmly nonexpansive map converge in finite dimensions: if $T$ is firmly nonexpansive and has a fixed point, its Picard iterates converge to a fixed point.

[F4]

A maximal-monotone resolvent is everywhere-defined and firmly nonexpansive: each resolvent is everywhere-defined and 1-Lipschitz.

Proof

1.1A1givenF1F4choose

Choose $b \in B (p)$ and $a \in A (p)$ with $a + b = 0$ . The resolvent identities give $J_{ρ B} (p + ρ b) = p$ and $J_{ρ A} (p - ρ b) = p$ . At $w_{*} = p + ρ b$ , the second input is $2 p - w_{*} = p - ρ b$ , so the update has $p_{B} = q = p$ and $T (w_{*}) = w_{*}$ . Thus $T$ has a fixed point.

2.1A1F2F3step 1.1

Apply [F3] using firm nonexpansiveness [F2]. It follows that the states $w_{k} = T^{k} (w_{0})$ converge to some $w_{*}^{'}$ with $T (w_{*}^{'}) = w_{*}^{'}$ .

3.1A1F1F4step 2.1algebra

Put $p^{'} = J_{ρ B} (w_{*}^{'})$ and $q^{'} = J_{ρ A} (2 p^{'} - w_{*}^{'})$ . Fixedness says $q^{'} = p^{'}$ . The resolvent inclusions yield $w_{*}^{'} - p^{'} \in ρ B (p^{'})$ and $p^{'} - w_{*}^{'} \in ρ A (p^{'})$ ; adding them gives $0 \in (A + B) (p^{'})$ .

4.1A1F1F4step 2.1algebra∎

The shadow $p_{k} = J_{ρ B} (w_{k})$ converges to $p^{'}$ because the resolvent is 1-Lipschitz by [F4] and $w_{k} \to w_{*}^{'}$ . Thus the shadow converges to a zero of the sum.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

PDHG has an O(1/k) ergodic saddle-gap bound

Statement

Assume the hypotheses of Chambolle–Pock primal-dual hybrid gradient and that $Φ (x, y) = f (x) + ⟨ K x, y ⟩ - g^{*} (y)$ has a saddle point $(x_{*}, y_{*})$ in the sense of Saddle points of extended-real Lagrangians. For $N \geq 1$ define ${\overset{ˉ}{x}}_{N} = \frac{1}{N} \sum_{k = 0}^{N - 1} x^{k + 1}, {\overset{ˉ}{y}}_{N} = \frac{1}{N} \sum_{k = 0}^{N - 1} y^{k + 1} .$ For every $x \in dom f$ , $y \in dom g^{*}$ , $Φ ({\overset{ˉ}{x}}_{N}, y) - Φ (x, {\overset{ˉ}{y}}_{N}) \leq \frac{1}{N} (\frac{∥ x - x^{0} ∥_{2}^{2}}{2 τ} + \frac{∥ y - y^{0} ∥_{2}^{2}}{2 σ}) .$ In particular, the saddle gap $Φ ({\overset{ˉ}{x}}_{N}, y_{*}) - Φ (x_{*}, {\overset{ˉ}{y}}_{N})$ is nonnegative and obeys this bound with $(x, y) = (x_{*}, y_{*})$ . On bounded test sets the displayed upper bound is $O (1 / N)$ . This is an ergodic gap statement; it is not a pointwise objective bound and does not assert pointwise iterate convergence.

Facts & Assumptions

Given: The exact PDHG recurrence, positive steps with $τ σ ∥ K ∥_{2}^{2} < 1$ , and a saddle point.

[A1]

The exact recurrence, strict step condition, and a saddle point hold.

[F1]

Chambolle–Pock primal-dual hybrid gradient: $f, g^{*}$ are proper closed convex and the iterates follow the exact recurrence.

[F2]

PDHG one-step primal-dual gap telescope: for every test pair and $N \geq 1$ , the sum of the first $N$ saddle differences is at most the initial weighted squared distance.

[F3]

Saddle points of extended-real Lagrangians: $Φ (x_{*}, y) \leq Φ (x_{*}, y_{*}) \leq Φ (x, y_{*})$ for all $x, y$ .

Proof

1.1A1F1givenalgebra

Every exact proximal output lies in the effective domain of its function. Convexity therefore puts ${\overset{ˉ}{x}}_{N}$ in $dom f$ and ${\overset{ˉ}{y}}_{N}$ in $dom g^{*}$ .

2.1A1F1F2step 1.1algebra

By convexity in [F1], $f ({\overset{ˉ}{x}}_{N}) \leq N^{- 1} \sum_{k < N} f (x^{k + 1})$ and $g^{*} ({\overset{ˉ}{y}}_{N}) \leq N^{- 1} \sum_{k < N} g^{*} (y^{k + 1})$ ; linearity gives $K {\overset{ˉ}{x}}_{N} = N^{- 1} \sum K x^{k + 1}$ . Hence $Φ ({\overset{ˉ}{x}}_{N}, y) - Φ (x, {\overset{ˉ}{y}}_{N}) \leq \frac{1}{N} \sum_{k = 0}^{N - 1} (Φ (x^{k + 1}, y) - Φ (x, y^{k + 1})) .$ Apply [F2] and divide by $N$ to get the bound.

3.1A1F3step 2.1∎

By the saddle inequalities [F3], $Φ ({\overset{ˉ}{x}}_{N}, y_{*}) \geq Φ (x_{*}, y_{*})$ and $Φ (x_{*}, {\overset{ˉ}{y}}_{N}) \leq Φ (x_{*}, y_{*})$ , so their difference is nonnegative. Step 2.1 at $(x_{*}, y_{*})$ supplies the same $O (1 / N)$ upper bound. The ergodic estimate makes no claim about a single nonaveraged objective difference or pointwise iterate convergence.

5 · Examples, counterexamples and false statements

None yet.