ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge 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.

The spectrum 1, 4, 9 gives tuned root factor one half

Example

Let $A = diag (1, 4, 9)$ , $F (w) = \frac{1}{2} w^{T} A w$ on $R^{3}$ , and $w_{0} = w_{1} = (1, 1, 1)$ . With $c = 1$ and $L = 9$ , tuned heavy-ball has $α = \frac{1}{4}$ , $β = \frac{1}{4}$ , and modal root factor $\frac{1}{2}$ at all three eigenvalues. Its endpoint characteristic polynomials are repeated-root polynomials. Gradient descent with step $γ = \frac{1}{5}$ has modal multipliers $\frac{4}{5}, \frac{1}{5}, - \frac{4}{5}$ , so its worst modal factor is $\frac{4}{5}$ .

Example references

Tuned heavy-ball has the minimax root factor on positive-definite quadratics

Heavy-ball momentum

Gradient descent

Facts & Assumptions

Given: The diagonal matrix $A = diag (1, 4, 9)$ , objective $F (w) = \frac{1}{2} w^{T} A w$ , initial vector $w_{0} = w_{1} = (1, 1, 1)$ , and the two fixed-step update rules.

[F1]

Tuned heavy-ball has the minimax root factor on positive-definite quadratics: for $c = 1$ , $L = 9$ , the tuned parameters are $α = 4 / (\sqrt{L} + \sqrt{c})^{2}$ and $β = ((\sqrt{L} - \sqrt{c}) / (\sqrt{L} + \sqrt{c}))^{2}$ , with modal root factor $q = (\sqrt{L} - \sqrt{c}) / (\sqrt{L} + \sqrt{c})$ .

[F2]

Heavy-ball momentum: the update is $w_{t + 1} = w_{t} - α \nabla F (w_{t}) + β (w_{t} - w_{t - 1})$ .

[F3]

Gradient descent: in fixed-step mode, the update is $x \mapsto x - γ \nabla F (x)$ .

[F4]

Matrix quadratic forms have the expected first derivative and Hessian: for $q (x) = \frac{1}{2} ∥ C x ∥_{2}^{2}$ , the gradient is $C^{*} C x$ .

Verification

1.1givenF1algebra

The eigenvalues of $A$ are $1, 4, 9$ , so $c = 1$ , $L = 9$ , $κ = 9$ , and $q = (3 - 1) / (3 + 1) = 1 / 2$ . Substitution into [F1] gives $α = 4 / (3 + 1)^{2} = 1 / 4$ and $β = q^{2} = 1 / 4$ .

1.2givenF2F4algebra

Taking $C = diag (1, 2, 3)$ gives $C^{T} C = A$ , so [F4] yields $\nabla F (w) = A w$ . Projecting [F2]'s update onto each standard coordinate gives polynomial $p_{λ} (r) = r^{2} - (1 + β - α λ) r + β$ . For $λ = 1$ it is $r^{2} - r + 1 / 4 = (r - 1 / 2)^{2}$ ; for $λ = 4$ it is $r^{2} - r / 4 + 1 / 4$ , whose roots are $1 / 8 \pm i \sqrt{15} / 8$ and have modulus $1 / 2$ ; for $λ = 9$ it is $r^{2} + r + 1 / 4 = (r + 1 / 2)^{2}$ . Thus each root factor is $1 / 2$ , and the endpoint roots are repeated.

2.1givenF3algebra∎

By [F3], gradient descent with $γ = 1 / 5$ has multiplier $1 - λ / 5$ on an eigenvector of eigenvalue $λ$ . The multipliers at $1, 4, 9$ are $4 / 5, 1 / 5, - 4 / 5$ , whose largest absolute value is $4 / 5$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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.