Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

A trace eigenspace objective and a Lanczos start-angle bound

Example

Let A=diag⁡(5,2,0) and minimize f(x)=−xTAx on St⁡(3,1)=S2. The top eigenspace is span⁡(e1), so the optimum is −5. Start Lanczos at b=(1,1,1)T/3 and use the two-dimensional Krylov space. The normalized vector generated by p(A)b, with p(λ)=(λ−1)/4, has Rayleigh quotient 41/9 for A, objective value −41/9, and objective gap 4/9. The Chebyshev start-angle theorem bounds the largest Ritz-value gap by 5/8. Direct arithmetic also gives 4/9≤5/8 for this explicit candidate; the candidate need not maximize the Rayleigh quotient on the Krylov space.

Facts & Assumptions

Given: The diagonal matrix A, unit starting vector b, and the Stiefel trace objective above.

[F1]

The Stiefel gradient is the tangent projection of the ambient Euclidean gradient (Projected Euclidean gradients are the Stiefel and Grassmann gradients).

[F2]

For a simple top eigenvalue, a nonzero top-eigenspace component of the start vector gives the stated Chebyshev Ritz-value error bound (Lanczos largest Ritz values obey a Chebyshev start-angle bound, including degenerate branches).

Proof

technique · explicit polynomial filtering and exact Rayleigh-quotient arithmetic
1.1F1F2givenalgebra

The ambient gradient of f is −2Ax. At x=e2, the Stiefel projection in [F1] is zero, so the eigendirection is stationary; at the global minimizer e1, f(e1)=−5. For the displayed start, p(A)b=(1,1/4,−1/4)T/3 is nonzero and belongs to K2(A,b)=span⁡{b,Ab}.

2.1givenstep 1.1algebra

The squared norm of this vector is (1+1/16+1/16)/3=3/8, and its A-quadratic form is (5+2/16)/3=41/24. Dividing gives Rayleigh quotient 41/9, hence objective −41/9 and gap 5−41/9=4/9.

3.1F2givenstep 1.1step 2.1algebra∎

Here λ1=5, λ2=2, λ3=0, the top multiplicity is one, and τ=∥(I−P)b∥/∥Pb∥=2. Since step 1.1 places the candidate in K2, its quotient shows θ2≥41/9. For Krylov dimension m=2, the theorem [F2] gives λ1−θ2≤(5−0)(2)2T1(1+2(5−2)/(2−0))2=1042=58. Since θ2≥41/9, its Ritz gap obeys 0≤λ1−θ2≤4/9≤5/8, so the candidate comparison and source bound agree. Also b and Ab are independent because the third coordinate of Ab is zero while that of b is nonzero, so the two-dimensional Krylov space is attained without breakdown.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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