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.

A two-block least-squares calibration sweep

Example

Consider $J (α, β) = \frac{1}{2} ∥ y - a α - b β ∥_{2}^{2} + \frac{1}{2} α^{2} + β^{2}$ , with $y = (2, 1)^{T}$ , $a = (1, 0)^{T}$ , and $b = (1, 1)^{T}$ . A cyclic exact sweep from $(0, 0)$ in the order $α, β$ gives $(1, 1 / 2)$ , residual $(1 / 2, 1 / 2)$ , and objective $1$ .

Facts & Assumptions

Given: The quadratic objective and vectors in the Example, cyclic order $α$ then $β$ , and sweep budget $K = 1$ .

[F1]

Cyclic exact block minimization: each scalar update is a global minimizer of that coordinate slice.

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the vector norm squares and dot products are the standard Euclidean quadratic and bilinear forms.

Proof

1.1F1F2givenalgebra

With $β = 0$ , bilinearity [F2] expands the terms depending on $α$ as $\frac{1}{2} (∥ a ∥_{2}^{2} + 1) α^{2} - (a^{T} y) α$ plus a constant. Here $∥ a ∥_{2}^{2} + 1 = 2$ and $a^{T} y = 2$ , so completing the square gives $α^{2} - 2 α = (α - 1)^{2} - 1$ plus a constant. Thus the unique global slice minimizer is $α = 1$ .

2.1F1F2step 1.1algebra∎

With $α = 1$ , bilinearity [F2] expands the terms depending on $β$ as $\frac{1}{2} (∥ b ∥_{2}^{2} + 2) β^{2} - b^{T} (y - a) β$ plus a constant. Here $∥ b ∥_{2}^{2} + 2 = 4$ and $b^{T} (y - a) = 2$ , so completing the square gives $2 β^{2} - 2 β = 2 (β - 1 / 2)^{2} - 1 / 2$ plus a constant. Thus $β = 1 / 2$ is the unique global slice minimizer. The residual is $(1 / 2, 1 / 2)$ and $J = \frac{1}{2} (1 / 2) + \frac{1}{2} + 1 / 4 = 1$ . At the initial point $J (0, 0) = 5 / 2$ , so the exact sweep decreases the objective.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

P. Tseng, Convergence of a Block Coordinate Descent Method for Nondifferentiable Minimization, §2 (standard reference, not scraped)
Clément Royer, Regularized, Large-Scale and Distributed Optimization, Lecture 3, §3.1 (standard reference, not scraped)