Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: 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.

The unilateral shift obstructs a cyclic linear trace extension

Statement refuted

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let ℓ2:=ℓ2(N,F) with standard basis (un)n∈N given by un(m)=δmn, and let S∈B(ℓ2) be the unilateral forward shift Sun:=un+1(n∈N), extended linearly and by continuity, with P0:=⟨⋅,u0⟩u0. Then S∗S=I,SS∗=I−P0,S∗S−SS∗=P0, neither S∗S=I nor SS∗=I−P0 is trace class (Trace class operator), while P0 is rank one with tr⁡(P0)=1 (Adjoint, norm and trace of an operator of rank at most one). Consequently there is no linear functional τ on a linear subspace of B(ℓ2) that contains the trace-class operators, S∗S, and SS∗, agrees with the usual trace on trace-class operators, and satisfies τ(S∗S)=τ(SS∗). Thus the cyclicity identity tr⁡(ST)=tr⁡(TS) of Cyclicity of the trace has no linear cyclic extension whose domain contains this pair of nonsummable products.

Facts & Assumptions

Given: Countable Choice, the space ℓ2 with its standard basis (un), the forward shift S, and the projection P0=⟨⋅,u0⟩u0.

[A1]

The standard basis and shifts. The vectors un∈ℓ2 satisfy ⟨um,un⟩=δmn and ∥un∥2=1, and if a∈ℓ2 has ⟨a,un⟩=0 for every n then a=0, so the zero-complement characterisation makes (un) a complete orthonormal family, a Hilbert basis of ℓ2; hence every x∈ℓ2 equals ∑n⟨x,un⟩un and two vectors with equal coefficients coincide (Square-summable families on an arbitrary index set and the space ℓ2(I), Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases, Real and complex inner-product spaces and their induced length). The forward shift has ∥Sun∥=1, is an isometry, and its adjoint satisfies S∗u0=0, S∗un=un−1 for n≥1, the adjoint being characterised by ⟨Sx,y⟩=⟨x,S∗y⟩ (Hilbert-adjoint identities, The Hilbert-space adjoint of a bounded operator, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces).

[A2]

Trace-class diagonal test. If T is trace class and E is a Hilbert basis, then ∑e∈E∣⟨Te,e⟩∣≤∥T∥1<+∞; hence an operator T for which some Hilbert basis has infinitely many e with ⟨Te,e⟩=1 is not trace class (Trace of a trace class operator, Trace is absolutely convergent and basis independent, Trace class operator, Square-summable families on an arbitrary index set and the space ℓ2(I)).

[A3]

Rank-one operators. For u,v∈H the operator ⟨⋅,v⟩u has adjoint ⟨⋅,u⟩v, norm ∥u∥∥v∥, and trace ⟨u,v⟩; in particular P0=⟨⋅,u0⟩u0 has trace ⟨u0,u0⟩=1 (Adjoint, norm and trace of an operator of rank at most one, Orthonormal families, complete orthonormal systems and Hilbert bases).

[A4]

Cyclicity theorem. If T is trace class and S is bounded then ST and TS are trace class and have equal traces (Cyclicity of the trace).

Counterexample

technique · direct

Given: Countable Choice, the shift S, the projection P0, and the standard basis.

1.1A1

The products. Since S is an isometry, ⟨S∗Sx,y⟩=⟨Sx,Sy⟩=⟨x,y⟩ for all x,y by [A1], so S∗S=I. Similarly ⟨SS∗x,un⟩=⟨S∗x,S∗un⟩ for n≥1 equals ⟨S∗x,un−1⟩=⟨x,un⟩, while ⟨SS∗x,u0⟩=⟨S∗x,S∗u0⟩=0; hence SS∗ fixes each un with n≥1 and annihilates u0, that is SS∗x=x−⟨x,u0⟩u0=(I−P0)x for all x, and S∗S−SS∗=P0.

1.2A1A2

Neither product is trace class. For I with the Hilbert basis (un), every diagonal coefficient is ⟨Iun,un⟩=1, so ∑n∣⟨Iun,un⟩∣=+∞ and I is not trace class by [A2]. For I−P0, the coefficients at un with n≥1 are ⟨(I−P0)un,un⟩=1, again infinitely many equal to 1, so I−P0 is not trace class by [A2].

1.3A3

The difference has trace one. P0=⟨⋅,u0⟩u0 is a rank-one operator whose trace is ⟨u0,u0⟩=1 by [A3]; note that u0≠0 because it is a unit vector.

2.1step 1.1step 1.2step 1.3A4assume-contradischarge-contradiction∎

Conclusion. Suppose that a linear functional τ on a linear subspace containing the trace-class operators, S∗S, and SS∗ agreed with the usual trace on trace-class operators and satisfied τ(S∗S)=τ(SS∗). By linearity, [step 1.1], and [step 1.3], 0=τ(S∗S)−τ(SS∗)=τ(P0)=tr⁡(P0)=1, a contradiction. Hence no such cyclic linear extension exists. The products themselves are not trace class by [step 1.2], so [A4] neither asserts nor assigns their individual traces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

81 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