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.

Positive square root of a compact positive operator

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let H be a real or complex Hilbert space (Hilbert space) and let TB(H) be a compact self-adjoint positive operator (Compact linear operator, Self-adjoint, positive, unitary and normal operators, A bounded linear operator between normed spaces), so that Tx,x is a nonnegative real for every x. Then there is a compact self-adjoint positive operator SB(H) with S2=T, and it is unique: if RB(H) is compact and positive (Self-adjoint, positive, unitary and normal operators) with R2=T, then R=S. The root acts by multiplication by λ on each positive eigenspace Eλ(T)=ker(TλI), λ>0, and by zero on kerT; in particular S is the operator denoted T or T1/2.

Facts & Assumptions

Given: Countable Choice, a real or complex Hilbert space H, a compact self-adjoint positive T, the set Σ={λ>0:λ is an eigenvalue of T}, the eigenspaces Eλ, and M:=spanλΣEλ.

[A1]

Spectral theorem for T. Σ is finite or countably infinite, each Eλ has finite dimension and an orthonormal basis, distinct eigenspaces are orthogonal, M=(kerT)=ranT, and H=MkerT with Tx=λΣλPλx in norm for xH, where Pλ is the orthogonal projection onto Eλ (Spectral theorem for compact self adjoint operators, Eigenspaces of a self adjoint operator are orthogonal, Eigenvalues, eigenvectors, eigenspaces Eλ(T)=ker(TλI), and the spectrum σF(T) of an endomorphism, Orthonormal families, complete orthonormal systems and Hilbert bases).

[A2]

Stability data. The Pλ are finite sums of rank-one maps xx,ee and satisfy Pλx,y=x,Pλy and PλxEλ; the family (Pλx)λ is orthogonal with λPλx2x2 (Bessel) and the expansion of x over the union of orthonormal bases of the Eλ converges to the component of x in M (The finite Bessel inequality and best approximation by a finite orthonormal family, Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space, Orthogonality and the orthogonal complement, Real and complex inner-product spaces and their induced length).

[A3]

Square-summable orthogonal families. If (xi) is an orthogonal family in a Hilbert space with ixi2<+, then the finite-subset net of ixi converges and the limit s satisfies s2=ixi2 (Square-summable orthogonal families have norm-convergent finite sums, Square-summable families on an arbitrary index set and the space 2(I)).

[A4]

Orthogonal decomposition. For a closed subspace M one has H=MM with M closed and MM direct, and a bounded linear operator that vanishes on M and on M is zero; limits of convergent sequences are unique (Orthogonal decomposition by a closed subspace, Linear subspace of a vector space, Convergence of a sequence in a metric space: xkx iff d(xk,x)0 in R, Hilbert space, Banach space).

[A5]

Compactness and finite rank. A finite-rank bounded operator is compact; under ACω a norm limit of compact operators into a Banach space is compact; scalar multiples and images of compact sets under continuous maps are compact (Bounded finite rank operators are compact, Norm limit of compact operators is compact, Compact linear operator, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, For a linear operator, boundedness, continuity at 0, continuity, and Lipschitz continuity are equivalent).

[A7]

Finite spectral thresholds. For each real ε>0 there are only finitely many λΣ with λε; in particular Fn:={λΣ:λ1/(n+1)} is finite for every nN (Spectral theorem for compact self adjoint operators).

Proof

technique · direct

Given: Countable Choice, the compact self-adjoint positive T, its positive eigenvalues Σ, the eigenspaces Eλ and the projections Pλ, and M=spanλΣEλ.

1.1

Construction of the root. Positivity forces λ0 for every eigenvalue λ of T, because for a unit eigenvector e one has λ=Te,e0; hence Σ consists of positive numbers and 0 is an eigenvalue only in the form of the kernel [A1]. For xH set Sx:=λΣλPλx, a finite-subset net over the at most countable index set Σ. The family (λPλx)λ is orthogonal with λλPλx2=λλPλx2=Tx,xTx2<+, using the expansion, orthogonality and Bessel [A1, A2]; so [A3] makes the net converge, S is well defined with Sx2=λλPλx2=Tx,xTx2, and S is linear with ST. Moreover Sx,x=λλPλx,x=λλPλx20, because Pλ is self-adjoint and Pλx(xPλx) [A2]; and S is self-adjoint, since Sx,y=λλPλx,y=λλx,Pλy=x,Sy by absolute convergence and self-adjointness of each Pλ. Finally S2=T: on Eλ one has S=λI whence S2=λI=T, both operators are continuous and agree on the linear span of Eλ, hence on M by continuity, and both vanish on kerT (for xkerT, Pλx=0 for all λ because EλkerT and x is in every Eλ), so S2=T on H=MkerT by [A4].

A1A2A3A4
1.2

Every positive square root kills the kernel. Let R be compact and positive with R2=T, and let xkerT. Put y:=Rx, so Ry=R2x=0. For every real t, positivity at x+ty gives 0R(x+ty),x+ty=y,x+ty2. Here y,x=Rx,x is real and nonnegative. If y0, choosing t=(y,x+1)/y2 makes the right side 1, impossible. Thus Rx=0 for every xkerT. This works over both scalar fields and uses neither self-adjointness nor compactness of R.

givenA2algebra
1.3

The root is compact. For each nN let Fn:={λΣ:λ1/(n+1)}, finite by [A7], and put Sn:=λFnλPλ. This operator has finite-dimensional range by [A1], so is compact by [A5], including when Fn is empty. For every xH, the orthogonal summation identity [A3] and Bessel [A2] give (SSn)x2=λFnλPλx2(n+1)1λFnPλx2(n+1)1x2. Thus SSn(n+1)1/20. Since H is Banach, [A5] implies that S is compact. The same zero-based sequence handles empty, finite and infinite Σ.

A1A2A3A5A7
2.1

A positive square root acts diagonally. Let R be as in [step 1.2], let λΣ, and put a:=λ>0. For xEλ(T) set v:=(RaI)x. The identity R2x=Tx=λx=a2x gives Rv=a2xaRx=av. Positivity therefore implies 0Rv,v=av2, forcing v=0. Hence Rx=λx on the entire eigenspace, without a diagonalization of R or an assumption that R is self-adjoint.

step 1.2A1algebra
2.2

Existence. By [step 1.1] and [step 1.3] the operator S is a compact self-adjoint positive operator with S2=T, and by construction it acts as λI on each Eλ(T), λΣ, and as 0 on kerT.

step 1.1step 1.3
3.1

Uniqueness. Let R be compact and positive with R2=T. By [step 1.2] R vanishes on kerT, by [step 2.1] it equals λI on each Eλ(T), and by [step 2.2] the same two descriptions hold for S; hence the bounded operator RS vanishes on kerT and on each Eλ(T). Since H is the closed linear span of kerTλΣEλ(T) by [A1], continuity gives RS=0.

step 1.2step 2.1step 2.2A1A4
4.1

Conclusion. The operator S of [step 1.1] is compact, self-adjoint and positive with S2=T by [step 2.2], and [step 3.1] shows that every compact positive R with R2=T equals S; the action of S on the positive eigenspaces and on the kernel is stated in [step 2.2]. This proves the lemma, including the uniqueness among compact positive square roots.

step 2.2step 3.1A4

Depends on

Used by

Dependency tree · two levels

130 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