Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

Orthogonal complement of an eigenspace is invariant

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real or complex Hilbert space (Hilbert space), let TB(H) be self-adjoint (Self-adjoint, positive, unitary and normal operators) and let λ be an eigenvalue of T (Eigenvalues, eigenvectors, eigenspaces Eλ(T)=ker(TλI), and the spectrum σF(T) of an endomorphism) with eigenspace Eλ=Eλ(T)=ker(TλI). Then:

  1. Eλ is a closed linear subspace of H and T(Eλ)Eλ;
  2. Eλ (Orthogonality and the orthogonal complement) is a closed linear subspace of H and T(Eλ)Eλ;
  3. the restrictions TEλ and TEλ satisfy the self-adjoint identity Tu,v=u,Tv for all u,v in the respective subspace.

Facts & Assumptions

Given: A Hilbert space H, a self-adjoint bounded T, an eigenvalue λ, and Eλ=ker(TλI).

[A1]
[A2]

Continuity and limits. The bounded operator TλI is continuous, so xnx implies (TλI)xn(TλI)x, and limits of convergent sequences in a metric space are unique (A bounded linear operator between normed spaces, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent, Convergence of a sequence in a metric space: xkx iff d(xk,x)0 in R, A sequence in a metric space has at most one limit).

[A3]

Complements and closedness. For every subset S of an inner-product space the orthogonal complement S is a closed linear subspace (Orthogonal complements are closed, Orthogonality and the orthogonal complement); vS means v,s=0 for every sS, and the pairing is linear in the first argument and conjugate-linear in the second (Real and complex inner-product spaces and their induced length).

[A4]

Countable Choice is the standing hypothesis of this pair's Hilbert-space interface (The Axiom of Countable Choice (ACω)).

Proof

technique · direct

Given: Countable Choice and the data above.

1.1

Eλ is a closed linear subspace. Let xnEλ with xnx; then (TλI)xn=0 for all n, so by continuity [A2] both (TλI)xn(TλI)x and (TλI)xn0, and uniqueness of limits gives (TλI)x=0, i.e. xEλ; with the linear-subspace statement of [A1] this proves closedness.

A1A2
1.2

Eλ is T-invariant. If vEλ then Tv=λvEλ by [A1] and linearity of the subspace.

A1
1.3

Eλ is closed. The general closedness of orthogonal complements [A3] applied to the subset Eλ gives that Eλ is a closed linear subspace of H.

A3
1.4

Eλ is T-invariant. Let xEλ and yEλ. By self-adjointness and Ty=λy, Tx,y=x,Ty=x,λy=λx,y=0, since x,y=0 by definition of the orthogonal complement; as yEλ was arbitrary, Tx,y=0 for all yEλ, that is TxEλ.

A1A3
2.1

The restrictions are self-adjoint. If u,v both lie in Eλ, or both lie in Eλ, then u,vH and [A1] gives Tu,v=u,Tv in H, which is exactly the defining identity of self-adjointness for the restricted operator on that subspace; [step 1.2] and [step 1.4] show that each restriction maps its subspace into itself, and [step 1.1] and [step 1.3] give the closedness statements of claims 1 and 2.

step 1.1step 1.2step 1.3step 1.4A1A4

Depends on

Used by

Dependency tree · two levels

61 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