ExampleConstruction: 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.

Adjoint, norm and trace of an operator of rank at most one

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a real or complex Hilbert space with the pairing linear in the first argument (Hilbert space, Real and complex inner-product spaces and their induced length), let $u, v \in H$ and let $T : = T_{u, v} \in B (H), T x : = ⟨ x, v ⟩ u .$ Then:

the Hilbert adjoint is $T^{*} x = ⟨ x, u ⟩ v$ (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities);
$∥ T ∥ = ∥ u ∥ ∥ v ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum);
$T$ is trace class (Trace class operator); if $u \neq 0$ and $v \neq 0$ its singular values are $s_{1} (T) = ∥ u ∥ ∥ v ∥$ and $s_{n} (T) = 0$ for $n \geq 2$ , so it has exactly one nonzero singular value, and $∥ T ∥_{1} = ∥ u ∥ ∥ v ∥$ ; if $u = 0$ or $v = 0$ then $T = 0$ and all singular values vanish;
$tr (T) = ⟨ u, v ⟩$ (Trace is absolutely convergent and basis independent).

Facts & Assumptions

Given: Countable Choice, the Hilbert space $H$ , vectors $u, v \in H$ and the operator of rank at most one $T = ⟨ \cdot, v ⟩ u$ .

[A1]

Pairing and adjoint. The pairing is linear in the first argument, conjugate-linear in the second, conjugate symmetric with $⟨ w, w ⟩ = ∥ w ∥^{2} \geq 0$ ; the Hilbert adjoint is characterised by $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ and satisfies $T^{* *} = T$ , $(S T)^{*} = T^{*} S^{*}$ (Real and complex inner-product spaces and their induced length, The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities, Hilbert space).

[A2]

Cauchy–Schwarz and norm. $∣ ⟨ x, v ⟩ ∣ \leq ∥ x ∥ ∥ v ∥$ , and the operator norm is the unit-ball supremum (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces).

[A3]

Compactness and spectral data. Every bounded finite-rank operator is compact (Bounded finite rank operators are compact). A nonzero compact self-adjoint positive operator has a largest eigenvalue equal to its norm with unit eigenvector, its nonzero eigenvalues are positive with finite multiplicities accumulating only at $0$ , its closed span is $(\ker \cdot)^{⊥}$ , and the positive square root is unique; the singular values of a compact operator are the positive eigenvalues of $∣ T ∣$ with multiplicity, in nonincreasing order with zero padding (Norm point of a compact self adjoint operator is an eigenvalue up to sign, Spectral theorem for compact self adjoint operators, Positive square root of a compact positive operator, Absolute value and singular values of a compact operator, Singular value decomposition for compact operators).

[A4]

Trace machinery. A compact operator with $\sum_{n} s_{n} < + \infty$ is trace class with $∥ T ∥_{1} = \sum_{n} s_{n}$ ; for a nuclear representation $T = \sum_{j} ⟨ \cdot, u_{j} ⟩ v_{j}$ the trace is $\sum_{j} ⟨ v_{j}, u_{j} ⟩$ , independently of the representation, and $∣ tr (T) ∣ \leq ∥ T ∥_{1}$ (Trace class operator, Nuclear series characterizes trace norm, Trace is absolutely convergent and basis independent, Trace of a trace class operator).

Verification

technique · direct

Given: Countable Choice, the vectors $u, v$ , the operator $T = ⟨ \cdot, v ⟩ u$ , and the candidate $T^{*} : = ⟨ \cdot, u ⟩ v$ .

1.1

The adjoint. The candidate is linear by first-variable linearity and bounded by $∥ ⟨ x, u ⟩ v ∥ \leq ∥ u ∥ ∥ v ∥ ∥ x ∥$ using [A2]. For all $x, y \in H$ , $⟨ T x, y ⟩ = ⟨ ⟨ x, v ⟩ u, y ⟩ = ⟨ x, v ⟩ ⟨ u, y ⟩$ and $⟨ x, T^{*} y ⟩ = ⟨ x, ⟨ y, u ⟩ v ⟩ = \overline{⟨ y, u ⟩} ⟨ x, v ⟩ = ⟨ u, y ⟩ ⟨ x, v ⟩$ by conjugate symmetry [A1]; the two expressions agree, so by uniqueness of the Hilbert adjoint $T^{*} = ⟨ \cdot, u ⟩ v$ .

A1A2

1.2

The norm. For every $x$ , $∥ T x ∥ = ∣ ⟨ x, v ⟩ ∣ ∥ u ∥ \leq ∥ u ∥ ∥ v ∥ ∥ x ∥$ by [A2], so $∥ T ∥ \leq ∥ u ∥ ∥ v ∥$ ; if $v \neq 0$ then testing $x = v / ∥ v ∥$ gives $∥ T x ∥ = ∥ v ∥ ∥ u ∥$ , whence equality, and if $v = 0$ then $T = 0$ and both sides are $0$ .

A1A2algebra

2.1

The singular value. The range of $T$ is contained in $span {u}$ , when $u, v \neq 0$ , $T (v / ∥ v ∥^{2}) = u$ , so its range has ordered basis $(u)$ ; if either vector is zero its range has the empty basis. Thus the bounded operator $T$ has finite rank and is compact by [A3]. Compute $T^{*} T x = ⟨ x, v ⟩ ∥ u ∥^{2} v$ using [step 1.1] and conjugate linearity in the second argument [A1]; hence $T^{*} T = ∥ u ∥^{2} ∥ v ∥^{2} P$ where $P : = ⟨ \cdot, v / ∥ v ∥ ⟩ v / ∥ v ∥$ is the orthogonal projection onto $span {v}$ when $v \neq 0$ , and put $P = 0$ when $v = 0$ , so the displayed formula holds in that case too. For $v \neq 0$ , writing $e = v / ∥ v ∥$ gives $P^{2} = P$ , $P^{*} = P$ and $⟨ P x, x ⟩ = ∣ ⟨ x, e ⟩ ∣^{2} \geq 0$ directly from [A1]. The operator $S : = ∥ u ∥ ∥ v ∥ P$ is bounded by [A2] and has the one-vector range basis $(v)$ when $u, v \neq 0$ , otherwise the empty range basis. It is therefore compact by [A3], and is self-adjoint and positive with $S^{2} = T^{*} T$ , so $∣ T ∣ = S$ by uniqueness of the positive square root [A3]; its nonzero eigenvalues are the single number $∥ u ∥ ∥ v ∥$ with multiplicity one when $u, v \neq 0$ , and there are none when $u = 0$ or $v = 0$ . By [A3] the singular values of $T$ are exactly this data, and [A4] gives $∥ T ∥_{1} = ∥ u ∥ ∥ v ∥ < + \infty$ , so $T$ is trace class.

step 1.1A1A2A3A4algebra

3.1

The trace. Assume $u, v \neq 0$ (otherwise $T = 0$ and the trace is $0 = ⟨ u, v ⟩$ ). Then, writing $e : = v / ∥ v ∥$ and $s : = ∥ u ∥ ∥ v ∥$ , the identity $T x = s ⟨ x, e ⟩ (u / ∥ u ∥)$ exhibits $T$ as the positive-integer-indexed nuclear representation with $u_{1} : = e$ , $v_{1} : = s u / ∥ u ∥ = ∥ v ∥ u$ and $u_{j} = v_{j} = 0$ for $j \geq 2$ . Its zero-based partial-sum sequence has $R_{0} = 0$ and $R_{m} = T$ for every $m \geq 1$ , so it converges to $T$ exactly as required by [A4]. Therefore $tr (T) = ⟨ v_{1}, u_{1} ⟩ = ⟨ ∥ v ∥ u, v / ∥ v ∥ ⟩ = ⟨ u, v ⟩$ , since scalar multiplication in the first argument and conjugate-linearity in the second give $⟨ ∥ v ∥ u, v / ∥ v ∥ ⟩ = ∥ v ∥ \overline{∥ v ∥^{- 1}} ⟨ u, v ⟩ = ⟨ u, v ⟩$ .

step 2.1A1A4algebra

4.1

Conclusion. Claims 1–4 are [step 1.1], [step 1.2], [step 2.1] and [step 3.1]; in the degenerate cases $u = 0$ or $v = 0$ the operator is $0$ with $∥ T ∥ = ∥ T ∥_{1} = 0$ and $tr (T) = 0 = ⟨ u, v ⟩$ .

step 1.1step 1.2step 2.1step 3.1∎

Depends on

Used by

The unilateral shift obstructs a cyclic linear trace extension Counterexample

Dependency tree · two levels

91 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

Anthony W. Knapp, Advanced Real Analysis — Chapter II, §5, rank-one operators (standard reference, not scraped)