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

Polar decomposition of the unilateral shift

Example

Assume AC. On $H = ℓ^{2} (N_{0}; C)$ let $S$ be the unilateral shift $S e_{n} = e_{n + 1}$ . Then $S^{*} S = I$ , $S S^{*} = I - P$ where $P$ is the orthogonal projection onto $C e_{0}$ , and $∣ S ∣ = I$ ; the polar partial isometry of $S$ is $S$ itself, with initial space $H$ and final space $(C e_{0})^{⊥}$ . In particular $S$ is an isometry that is not a coisometry and not unitary.

Facts & Assumptions

[A1]

$ℓ^{2} (N_{0}; C)$ has orthonormal basis $(e_{n})$ with $⟨ x, e_{n} ⟩ = x_{n}$ , and every $x$ is the norm limit of its finite expansions $\sum_{n < N} ⟨ x, e_{n} ⟩ e_{n}$ ; the closed linear span of ${e_{n} : n \geq 1}$ is exactly $(C e_{0})^{⊥}$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , A Hilbert space with a given orthonormal basis is $ℓ^{2}$ of the index set, Fourier expansion in a Hilbert space, The Hilbert orthogonal projection onto a closed subspace).

[A2]

$⟨ S^{*} x, y ⟩ = ⟨ x, S y ⟩$ , so $S^{*} S$ and $S S^{*}$ are determined by their values on the basis; an isometry is exactly an operator with $U^{*} U = I$ , a coisometry has $U U^{*} = I$ , and a partial isometry vanishes on its kernel and is isometric on the orthogonal complement of the kernel (Hilbert-adjoint identities, Isometry coisometry and partial isometry).

[A3]

$∣ S ∣ = (S^{*} S)^{1 / 2}$ is the unique positive square root, and the polar partial isometry $U$ satisfies $S = U ∣ S ∣$ and $\ker U = \ker S$ , with initial space $\overline{ran ∣ S ∣}$ and final space $\overline{ran S}$ (Absolute value of a bounded operator, Polar decomposition for bounded operators).

[A4]

AC is the hypothesis of the polar-decomposition and Hilbert-space suppliers (The Axiom of Choice).

Verification

technique · direct

Given: The shift $S$ on $ℓ^{2} (N_{0}; C)$ defined by $S e_{n} = e_{n + 1}$ .

1.1

$S$ is a well-defined bounded linear isometry: for $x = \sum_{n} x_{n} e_{n}$ the series $S x = \sum_{n} x_{n} e_{n + 1}$ converges with $∥ S x ∥_{2}^{2} = \sum_{n} ∣ x_{n} ∣^{2} = ∥ x ∥_{2}^{2}$ , so $S^{*} S = I$ and $∥ S ∥ = 1$ .

A1A2

2.1

$S S^{*} = I - P$ : for the basis vectors $S^{*} e_{0} = 0$ and $S^{*} e_{n + 1} = e_{n}$ , so $⟨ S S^{*} e_{m}, e_{k} ⟩ = ⟨ S^{*} e_{m}, S^{*} e_{k} ⟩$ equals $1$ for $m = k \geq 1$ and $0$ otherwise; hence $S S^{*}$ is the identity on the closed span of ${e_{n} : n \geq 1} = (C e_{0})^{⊥}$ and vanishes on $C e_{0}$ .

step 1.1A1A2

2.2

$∣ S ∣ = I$ : since $S^{*} S = I$ , the identity is positive with square $I = S^{*} S$ , so by uniqueness of the positive square root $∣ S ∣ = I$ .

step 1.1A3

3.1

Consequently $\ker S = {0}$ and $ran S = (C e_{0})^{⊥}$ , and $S$ is an isometry that is not a coisometry: $S S^{*} \neq I$ because $S S^{*} e_{0} = 0$ .

step 1.1step 2.1

4.1

The polar partial isometry of $S$ is $U = S$ : indeed $S = S \cdot I = S ∣ S ∣$ , $\ker S = {0} = \ker U$ , and $S$ is a partial isometry, being isometric on $H = (\ker S)^{⊥}$ and vanishing on $\ker S = {0}$ ; uniqueness in the polar decomposition identifies it.

step 3.1step 2.2A2A3

5.1

The initial space is $(\ker S)^{⊥} = H$ and the final space is $\overline{ran S} = (C e_{0})^{⊥}$ , as asserted.

step 4.1A4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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

John B. Conway, A Course in Functional Analysis, 2nd ed., Chapter IX §3, printed pp.239–243 (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis, §5.3, printed pp.235–245 (standard reference, not scraped)