ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

A two-pixel TV denoising PDHG step in CSR form

Statement

Let $K = [- 1 1]$ , $f (x) = \frac{1}{2} ∥ x - (1, 0) ∥_{2}^{2}$ on $R^{2}$ , $g (v) = ∣ v ∣$ on $R$ , $τ = σ = 1 / 2$ , and $x^{0} = y^{0} = 0$ with ${\overset{ˉ}{x}}^{0} = x^{0}$ . Encode $K$ by the canonical CSR record $r = (0, 2)$ , $c = (0, 1)$ , $v = (- 1, 1)$ . The exact updates are $y^{1} = 0, x^{1} = (1 / 3, 0), y^{2} = - 1 / 3, x^{2} = (4 / 9, 1 / 9) .$ Moreover $τ σ ∥ K ∥_{2}^{2} = 1 / 2 < 1$ .

Facts & Assumptions

Given: The matrix, functions, step sizes and initial state in the Statement.

[A1]

The matrix, functions, step sizes, and initial state are exactly those in the Statement.

[F1]

Chambolle–Pock primal-dual hybrid gradient: $y^{k + 1} = {prox}_{σ g^{*}} (y^{k} + σ K {\overset{ˉ}{x}}^{k})$ , $x^{k + 1} = {prox}_{τ f} (x^{k} - τ K^{*} y^{k + 1})$ , and ${\overset{ˉ}{x}}^{k + 1} = 2 x^{k + 1} - x^{k}$ .

[F2]

Compressed sparse row matrices with stored-entry semantics: the record stores two entries in the sole row and represents $K_{00} = - 1, K_{01} = 1$ .

[F3]

Validated compressed sparse row matrix-vector product and CSR matrix-vector multiplication returns the represented product: the validated exact product is $K x = - x_{0} + x_{1}$ .

[F4]

CSR storage and exact matrix-vector operation counts: with $m = 1$ and $s = 2$ , CSR stores $2 s + m + 1 = 6$ data slots and the product performs exactly two field multiplications and two field additions, plus one zero initialization.

[F5]

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

[F6]

PDHG has an O(1/k) ergodic saddle-gap bound: the strict step condition is required for the ergodic gap theorem, which makes no pointwise objective assertion.

Proof

1.1A1F2F3F4algebra

The record has valid row pointers $0 = r_{0} \leq r_{1} = 2 = s$ and valid columns $0, 1$ . By [F2,F3], its exact matrix-vector product is $- x_{0} + x_{1}$ ; its transpose sends $y$ to $(- y, y)$ . By [F4], its stored-entry count is $s = 2$ , slot count is $6$ , and the exact operation count is two multiplications, two additions, and one output initialization.

1.2A1F1algebracases

The conjugate of $g (v) = ∣ v ∣$ is the indicator of $[- 1, 1]$ : if $∣ y ∣ \leq 1$ , then $y v - ∣ v ∣ \leq 0$ for every $v$ and equality occurs at $v = 0$ ; if $y > 1$ , taking $v \to + \infty$ makes the supremum infinite, and if $y < - 1$ , taking $v \to - \infty$ does so. Therefore ${prox}_{σ g^{*}}$ is Euclidean projection onto $[- 1, 1]$ . Also, direct completion of squares gives ${prox}_{τ f} (w) = \frac{w + τ (1, 0)}{1 + τ} .$

2.1A1F1step 1.1step 1.2algebra

Initially $K {\overset{ˉ}{x}}^{0} = 0$ , so $y^{1} = {proj}_{[- 1, 1]} (0) = 0$ , then $x^{1} = (0 + (1 / 2) (1, 0)) / (3 / 2) = (1 / 3, 0)$ . Thus ${\overset{ˉ}{x}}^{1} = (2 / 3, 0)$ and $y^{2} = {proj}_{[- 1, 1]} ((1 / 2) K {\overset{ˉ}{x}}^{1}) = {proj}_{[- 1, 1]} (- 1 / 3) = - 1 / 3$ .

3.1A1F1F5F6step 2.1algebra∎

Since $K^{T} y^{2} = (1 / 3, - 1 / 3)$ , $x^{2} = \frac{x^{1} - (1 / 2) K^{T} y^{2} + (1 / 2) (1, 0)}{3 / 2} = \frac{(1 / 6, 1 / 6) + (1 / 2, 0)}{3 / 2} = (4 / 9, 1 / 9) .$ Finally, for any $(a, b)$ , $∥ K (a, b) ∥_{2}^{2} = (- a + b)^{2} \leq 2 (a^{2} + b^{2})$ with equality at $(a, b) = (1, - 1) / \sqrt{2}$ . Hence $∥ K ∥_{2}^{2} = 2$ by [F5] and $τ σ ∥ K ∥_{2}^{2} = (1 / 4) 2 = 1 / 2 < 1$ , so the step-size hypothesis of [F6] is satisfied.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Antonin Chambolle and Thomas Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §6.1 (standard reference, not scraped)
Richard Barrett et al., Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods, 2nd ed., §4.3 (standard reference, not scraped)