ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Right shift powers converge in wot not sot

Example

On real or complex $ℓ^{2}$ indexed by $k \geq 0$ , let $R (x_{0}, x_{1}, \dots) = (0, x_{0}, x_{1}, \dots)$ . Then $R^{n} \to 0$ in WOT but not in SOT.

Facts & Assumptions

[F1]

SOT tests pointwise norm convergence; WOT tests each bounded scalar functional on each fixed vector (Strong and weak operator topologies).

[F2]

Sequence norms use square sums ( $ℓ^{p}$ is the $L^{p}$ space of counting measure). Finite real Cauchy–Schwarz bounds sums of products of nonnegative coordinate moduli (The Cauchy-Schwarz inequality for finite sums).

[F3]

Conjugation satisfies $b \overline{b} = ∣ b ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Verification

Given: the right shift $R$ and a bounded scalar-linear $F$ on $ℓ^{2}$ .

1.1

Put $b_{k} = F (e_{k})$ and test $F$ on $v = \sum_{k < N} {\overline{b}}_{k} e_{k}$ . By F3, $B_{N} = F (v) = \sum_{k < N} ∣ b_{k} ∣^{2} \leq ∥ F ∥ \sqrt{B_{N}}$ , giving $B_{N} \leq ∥ F ∥^{2}$ , also when $B_{N} = 0$ . Thus $b \in ℓ^{2}$ . Truncations converge in the square-sum norm, so $F (x) = \lim_{N} \sum_{k < N} x_{k} b_{k} = \sum_{k} x_{k} b_{k}$ , with absolute convergence: F2 bounds every finite sum $\sum_{k < N} ∣ x_{k} b_{k} ∣$ by $∥ x ∥_{2} ∥ b ∥_{2}$ , and the nonnegative partial sums converge to their finite supremum. The same finite inequality applied to tails gives the infinite tail bound used below.

givenF2F3

2.1

Consequently $F (R^{n} x) = \sum_{k \geq 0} x_{k} b_{k + n}$ and $∣ F (R^{n} x) ∣ \leq ∥ x ∥_{2} (\sum_{j \geq n} ∣ b_{j} ∣^{2})^{1 / 2} \to 0$ . This proves WOT convergence. But $∥ R^{n} x ∥_{2}^{2} = \sum_{k} ∣ x_{k} ∣^{2} = ∥ x ∥_{2}^{2}$ , so at $x = e_{0}$ the norms remain one. Thus SOT convergence to zero fails. $□$

step 1.1F1F2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

Bühler–Salamon, Functional Analysis (2017); exact harvest in batch coverage (standard reference, not scraped)
Teschl, Topics in Real and Functional Analysis (2017); exact harvest in batch coverage (standard reference, not scraped)