Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28
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 eigenvalues of the orthogonal compression of a self-adjoint endomorphism to a hyperplane interlace those of the original endomorphism

Statement

Let T:VV be self-adjoint on an n-dimensional real inner product space, let WV be a hyperplane, and let

C:=PWTW:WW

be the orthogonal compression, where PW is the orthogonal projection onto W. If the eigenvalues of T and C are ordered by

λ1λn,μ1μn1,

then

λiμiλi+1(1in1).

Facts & Assumptions

Given: A self-adjoint endomorphism T:VV on an n-dimensional real inner product space, a hyperplane WV, and its orthogonal projection PW.

[L2]

Courant-Fischer characterises the ordered eigenvalues of a self-adjoint operator by min-max formulas (Courant-Fischer min-max principle for self-adjoint endomorphisms on finite-dimensional real inner product spaces).

Proof

technique · direct
1.1

For u,vW, the decomposition in [L1] gives PWTu,v=Tu,v=u,Tv=u,PWTv, so C is self-adjoint on W. Also RC(u)=Cu,uu,u=Tu,uu,u=RT(u) for every nonzero uW.

L1algebra
2.1

For any 1in1, Courant-Fischer in W and step 1.1 give μi=maxdimU=i, UWmin0uURC(u)=maxdimU=i, UWmin0uURT(u)λi, because the maximisation is over fewer i-dimensional subspaces than in [L2]. Likewise μi=mindimL=ni, LWmax0uLRC(u)=mindimL=ni, LWmax0uLRT(u)λi+1, because ni=(n1)i+1 is the subspace dimension appearing in Courant-Fischer for the (i+1)-st eigenvalue of T. Hence λiμiλi+1.

L2step 1.1

Depends on

Used by

Dependency tree · two levels

9 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