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

An untuned heavy-ball recurrence diverges on a scalar quadratic

Example

Let $F : R \to R$ be $F (x) = \frac{1}{2} x^{2}$ . Run heavy-ball momentum with $α = \frac{27}{8}$ , $β = \frac{1}{4}$ , and $w_{0} = w_{1} = 1$ . For every integer $t \geq 0$ , the resulting iterates are

$w_{t} = - \frac{3}{5} (- 2)^{t} + \frac{8}{5} {(- \frac{1}{8})}^{t},$

so the iterate sequence is unbounded and does not converge to a real limit.

Example references

Heavy-ball momentum

Matrix quadratic forms have the expected first derivative and Hessian

Completeness of the real numbers

Every complete ordered field is Archimedean

Facts & Assumptions

Given: $F (x) = \frac{1}{2} x^{2}$ , heavy-ball parameters $α = \frac{27}{8}$ and $β = \frac{1}{4}$ , and initial values $w_{0} = w_{1} = 1$ .

[F1]

Heavy-ball momentum: for fixed parameters, $w_{t + 1} = w_{t} - α \nabla F (w_{t}) + β (w_{t} - w_{t - 1})$ .

[F2]

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

[F3]

The reals are complete: with its usual order and field structure, $R$ is a complete ordered field.

[F4]

Every complete ordered field is Archimedean: in every complete ordered field, for every element $M$ there is a canonical natural number $n \geq 1$ whose field embedding satisfies $M < n$ .

Verification

1.1givenF1F2algebra

Taking $C = [1]$ in [F2] gives $\nabla F (x) = x$ . Substituting the parameters and this gradient into [F1] yields $w_{t + 1} = - \frac{17}{8} w_{t} - \frac{1}{4} w_{t - 1}$ for every $t \geq 1$ .

2.1givenstep 1.1algebrainduction

The characteristic polynomial is $r^{2} + \frac{17}{8} r + \frac{1}{4} = (r + 2) (r + \frac{1}{8})$ . Each geometric sequence $(- 2)^{t}$ and $(- \frac{1}{8})^{t}$ therefore satisfies the recurrence in step 1.1. The stated linear combination has $w_{0} = 1$ and $w_{1} = \frac{6}{5} - \frac{1}{5} = 1$ , so the recurrence and these initial values prove the displayed formula for all $t$ by induction.

3.1givenF3F4step 2.1algebrainduction∎

For $t \geq 1$ , factor the expression as $w_{t} = (- 2)^{t} (- \frac{3}{5} + \frac{8}{5} 16^{- t})$ . Since $16^{- t} \leq 1 / 16$ , the term in parentheses is at most $- \frac{1}{2}$ , hence $∣ w_{t} ∣ \geq 2^{t - 1}$ . Induction gives $2^{t - 1} \geq t$ for $t \geq 1$ . For any starting index $N \geq 1$ and any real $R > 0$ , put $B = \max {N, R}$ ; since $R$ is a complete ordered field by [F3], [F4] supplies a natural number $t > B$ , which we use under the usual embedding as an integer iteration index. Thus $t \geq N$ and $∣ w_{t} ∣ \geq t > R$ . Every tail is therefore unbounded. If the sequence converged to a real $ℓ$ , some tail would satisfy $∣ w_{t} - ℓ ∣ < 1$ and hence $∣ w_{t} ∣ < ∣ ℓ ∣ + 1$ , a contradiction.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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