ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Randomized and cyclic updates on a rank-one quadratic

Example

For $f (x) = \frac{1}{2} (x_{1} + 2 x_{2})^{2}$ from $x^{0} = (1, 0)$ , the block Lipschitz constants are $L_{1} = 1$ and $L_{2} = 4$ . A uniform randomized gradient update with common majorizers $M_{1} = M_{2} = L_{\max} = 4$ has expected objective $9 / 64$ after one update, while an exact cyclic sweep in order $1, 2$ reaches the minimizer $(0, 0)$ .

Facts & Assumptions

Given: $f (x) = \frac{1}{2} (x_{1} + 2 x_{2})^{2}$ , $x^{0} = (1, 0)$ , two singleton blocks, uniform sampling, common majorizers $M_{1} = M_{2} = 4$ , randomized budget $K = 1$ with no stopping predicate, and cyclic sweep budget $K = 1$ .

[F1]

Randomized coordinate gradient descent: a sampled coordinate $i$ is updated by $x_{i}^{+} = x_{i} - M_{i}^{- 1} \nabla_{i} f (x)$ .

[F2]

Cyclic exact block minimization: a cyclic sweep exactly minimizes the selected coordinate slice.

Proof

1.1F1givenalgebra

Writing $s = x_{1} + 2 x_{2}$ , we have $\nabla_{1} f = s$ , $\nabla_{2} f = 2 s$ , and their coordinate Lipschitz constants are $1$ and $4$ . At $x^{0}$ , $s = 1$ and $f (x^{0}) = 1 / 2$ . If coordinate $1$ is sampled with common majorizer $4$ , $x_{1}$ becomes $3 / 4$ , so $f = \frac{1}{2} (3 / 4)^{2} = 9 / 32$ ; if coordinate $2$ is sampled, $x_{2}$ becomes $- 1 / 2$ , so $f = 0$ .

2.1F2step 1.1algebra∎

Uniform averaging of the two outcomes gives expected objective $(9 / 32 + 0) / 2 = 9 / 64$ . In cyclic minimization, the first coordinate minimizer at $x_{2} = 0$ is $x_{1} = 0$ , and the second coordinate minimizer at $x_{1} = 0$ is $x_{2} = 0$ ; hence the sweep reaches the global minimum.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Stephen J. Wright, Coordinate Descent Algorithms, §§3.1 and 3.3 (standard reference, not scraped)
Clément Royer, Regularized, Large-Scale and Distributed Optimization, Lecture 3, §§3.1–3.3 (standard reference, not scraped)