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 repeated eigenvalue gives a continuum of Grassmann minimizers

Example

Let A=diag⁡(0,0,2) and minimize the rank-one trace objective f([x])=xTAx on Gr⁡(1,3). Every line in span⁡(e1,e2) is a global minimizer. The repeated bottom eigenvalue therefore produces a continuum of minimizers represented by one Grassmann critical set.

Facts & Assumptions

Given: The matrix A and the rank-one Grassmann objective in the Example.

[F1]

A Grassmann objective must be invariant under changing an orthonormal frame of the same subspace, and its gradient is the horizontal projection (Projected Euclidean gradients are the Stiefel and Grassmann gradients).

[F2]

The horizontal tangent at a unit vector x consists of vectors z with xTz=0 (Tangent spaces and Frobenius projections on Stiefel and Grassmann).

Proof

technique · evaluate the Rayleigh quotient and its horizontal gradient
1.1F1givenalgebra

For q=±1∈O⁡(1), (xq)TA(xq)=xTAx, so the objective is well-defined on lines by [F1]. Since A is positive semidefinite, f([x])≥0 for every unit x. If x∈span⁡(e1,e2), then Ax=0 and f([x])=0, so every such line is a global minimizer.

2.1F1F2givenstep 1.1algebra∎

The vectors x=(cos⁡θ)e1+(sin⁡θ)e2 for 0≤θ<π are unit and give distinct lines: two such vectors span the same line only when their angles differ by a multiple of π, which cannot occur for distinct parameters in this half-open interval. Thus they parametrize continuum many distinct lines. At each such x, Ax=0, so the ambient gradient 2Ax and its horizontal projection vanish. The family is a continuum of Grassmann critical minimizers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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