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

Spectrum of the unilateral shift

Example

Assume the Axiom of Choice (The Axiom of Choice). Let 2=2(N0) be identified with L2 of the counting measure on N0={0,1,2,} (p is the Lp space of counting measure, Counting measure on an arbitrary set, Counting measure is a measure, Complex completeness, density, and inner product: the consumer interface), with coordinate vectors en, and let S be the unilateral shift

Sen:=en+1,extended linearly and by continuity to all of 2.

Then SB(2) is an isometry, and

σ(S)=D,σp(S)=,σr(S)=σcp(S)=D,σc(S)=σap(S)=T,

where D={z<1}, D its closure and T the unit circle (scalar spectrum in Spectrum and resolvent set in a Banach algebra, point/continuous/residual spectrum in Point continuous and residual spectrum, approximate point and compression spectrum in Approximate point and compression spectrum, all inside B(2) of Bounded operators form a Banach algebra, noncommutative in dimension at least two).

Facts & Assumptions

Given: The Axiom of Choice, the Hilbert space 2=2(N0) with orthonormal coordinate vectors en, and the isometric coordinate shift Sen=en+1.

[L1]

Elements of 2 are determined by their coordinates, almost-everywhere equality for the counting measure is pointwise equality, and x22=nxn2; the inner product is x,y=nxnyn (p is the Lp space of counting measure, Counting measure on an arbitrary set, Counting measure is a measure, Complex completeness, density, and inner product: the consumer interface).

[L2]

S is bounded with S=1 and Sx=x for all x, so (Sλ)xSxλx=(1λ)x for λ<1; an operator that is not bounded below is not invertible (A bounded operator that is bounded below, Spectrum and resolvent set in a Banach algebra, Bounded operators form a Banach algebra, noncommutative in dimension at least two).

[L3]

λσp(S) means Sλ is not injective; λσc(S) means injective with dense non-surjective range; λσr(S) means injective with non-dense range; λσap(S) means Sλ is not bounded below; λσcp(S) means Sλ has non-dense range; and σ(S) is the set of non-invertible Sλ (Point continuous and residual spectrum, Approximate point and compression spectrum, Spectrum and resolvent set in a Banach algebra).

Verification

technique · direct
1.1

Shift identities: (Sx)n=xn1 for n1 and (Sx)0=0, so Sx=x and S=1; moreover Sλ is injective for every λ: from (Sλ)x=0 the recursion xn1=λxn gives x=0 for λ0 and Sx=0 gives x=0 for λ=0, since S is injective.

L1L2algebra
1.2

Spectral containment: if λ>1 then S/λ<1 and Sλ=λ(1S/λ) is invertible by the Neumann series; if λ<1 then (Sλ)x(1λ)x by [L2], so Sλ is bounded below.

L2algebra
2.1

Non-density in the open disc: for λ<1 the vector c:=(λn)n0 lies in 2 and annihilates the range: for every x2, (Sλ)x,c=nxn(cn+1λcn)=nxn(λn+1λλn)=0. So ran(Sλ) is not dense for λ<1, and σcp(S)D.

step 1.1L1L3algebra
2.2

Approximate eigenvectors on the circle: for λ=1 and N1 put vN:=N1/2k<Nλkek, a unit vector; since SvN=N1/2k<Nλkek+1, the interior terms cancel in (Sλ)vN and only the two boundary terms survive, (Sλ)vN=N1/2(λ(N1)eNλe0), so (Sλ)vN=2N1/22N1/20 and Sλ is not bounded below.

step 1.1L2L3algebra
3.1

Density on the unit circle: if cran(Sλ) then the same computation gives cn+1=λcn for all n, that is, cn=λnc0. For λ=1 this makes cn=c0 for every n, so c2 forces c0=0 and the orthogonal complement is {0}: the range is dense there. For λ<1, on the other hand, cn=λnc0 decays, the vector c=(λn)n0 is a nonzero element of 2 orthogonal to the range, and the range is not dense — the non-density already computed in [step 2.1].

step 2.1L1algebra
3.2

Point spectrum empty and residual spectrum: injectivity is [step 1.1], so σp(S)=; for λ<1 the range is non-dense by [step 2.1], so λσr(S) and also λσcp(S); for λ>1 the operator is invertible by [step 1.2], so those points are outside every spectral set.

step 1.1step 1.2step 2.1L3
4.1

Combining: σ(S)=D because λ>1 gives invertibility [step 1.2] and every λ1 lies in σc(S) or σr(S) by [step 3.2] and [step 2.2]; σap(S)=T by [step 1.2] (bounded below inside the disc), [step 2.2] (on the circle) and [step 1.2] again (invertible, hence bounded below, outside); σc(S)=T because those points are injective with dense range [step 1.1, step 3.1] and non-surjective (else invertible); σr(S)=σcp(S)=D by [step 2.1], [step 3.1] and [step 3.2].

step 1.2step 2.1step 3.1step 3.2step 2.2L3

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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