TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Uniqueness of the pointed cyclic GNS representation

Statement

Assume the Axiom of Choice. Let $G$ be a topological group. For $j = 1, 2$ , let $H_{j}$ be a complex Hilbert space, let $π_{j} : G \to U (H_{j})$ be a strongly continuous unitary representation, and let $ξ_{j} \in H_{j}$ be cyclic. Suppose their diagonal coefficients agree:

⟨ π_{1} (g) ξ_{1}, ξ_{1} ⟩ = ⟨ π_{2} (g) ξ_{2}, ξ_{2} ⟩ (g \in G) .

Then there is a unique unitary intertwiner $U : H_{1} \to H_{2}$ such that $U ξ_{1} = ξ_{2}$ .

Facts & Assumptions

Given: The Axiom of Choice; a topological group $G$ ; two strongly continuous unitary representations $(π_{j}, H_{j})$ with cyclic vectors $ξ_{j}$ ; and equality of their diagonal coefficients. All Hilbert pairings are linear in the first variable.

[F1]

A strongly continuous unitary representation is a homomorphism into bijective complex-linear isometries; every orbit map is norm-continuous (Strongly continuous unitary representations, invariant linear subspaces and intertwiners).

[F2]

The diagonal coefficient is $g \mapsto ⟨ π (g) ξ, ξ ⟩$ , with this first-variable-linear convention (Matrix coefficient of a unitary representation).

[F3]

A cyclic vector has dense complex-linear orbit span; the zero-space representation is cyclic (Cyclic vector and cyclic unitary representation).

[F4]

The diagonal coefficient of a strongly continuous unitary representation is continuous and of positive type, and its value at $e$ is $∥ ξ ∥^{2}$ (Diagonal unitary coefficients have positive type).

[F5]

For finitely supported $f, h : G \to C$ , $B_{φ} (f, h) = \sum_{x, y} f (x) \overline{h (y)} φ (y^{- 1} x)$ is the positive-semidefinite GNS form, and its quotient inner product has $B_{φ} (δ_{x}, δ_{y}) = φ (y^{- 1} x)$ (Positive-type functions define the GNS pre-Hilbert form).

[F6]

Under AC, the GNS construction supplies $Q_{φ} = C^{(G)} / N_{φ}$ , its Hilbert completion $H_{φ}$ and dense isometric embedding $κ_{φ}$ , and the representation extending left translations, with cyclic vector $ξ_{φ} = κ_{φ} ([δ_{e}])$ (GNS construction for a continuous positive-type function).

[F7]

Complex inner products are linear in their first variable, conjugate linear in their second, and induce the norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ (Real and complex inner-product spaces and their induced length).

[F8]

A completion is a Banach space with a dense linear isometric embedding; every complex Hilbert space is Banach. The induced inner-product norm is a norm (Completion of a normed space, Hilbert space, The induced length is a norm).

[F9]

Under Countable Choice, a bounded linear map from a normed space into a Banach space extends uniquely and boundedly to its completion, with the same bound (Bounded linear maps extend uniquely across the completion).

[F10]

A linear map obeys the linearity identities, and it is bounded when $∥ T x ∥ \leq C ∥ x ∥$ for some $C \geq 0$ (Linear map between vector spaces over the same field, A bounded linear operator between normed spaces).

[F11]

AC implies DC and then Countable Choice (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F12]

On the GNS quotient, left translation is $L_{g} f (x) = f (g^{- 1} x)$ , and its extension to $H_{φ}$ is the strongly continuous representation $π_{φ}$ (The GNS translation action is unitary and strongly continuous).

Proof

Bekka–de la Harpe–Valette prove the GNS existence and uniqueness theorem in Theorem C.4.10, Appendix C §C.4, printed pp. 376–377: they realize the positive kernel, map its feature vectors to the given cyclic orbit, extend the resulting isometry, and obtain the intertwining relation by cyclic density. Bekka–de la Harpe, Proposition 1.B.8, Chapter 1 §1.B, printed p. 29, computes the matching orbit-vector Gram norms and defines the corresponding map on the finite orbit span; its formal bijection is restricted to normalized positive-type functions and unit cyclic vectors, and the proof leaves the extension checks implicit. The proof here derives the arbitrary-norm statement from the canonical GNS quotient and records those checks, including the zero case.

Proof technique: direct.

1.1F2F4

Let $φ (g) = ⟨ π_{1} (g) ξ_{1}, ξ_{1} ⟩$ . By [F2] and [F4], $φ \in P (G)$ and $φ (e) = ∥ ξ_{1} ∥^{2}$ . Equality of the coefficients gives $φ (g) = ⟨ π_{2} (g) ξ_{2}, ξ_{2} ⟩$ for all $g$ , so [F4] also gives $φ (e) = ∥ ξ_{2} ∥^{2}$ .

2.1F3step 1.1

If $φ = 0$ , then $∥ ξ_{1} ∥ = ∥ ξ_{2} ∥ = 0$ by step 1.1, so both vectors are zero. Their cyclicity [F3] forces $H_{1} = H_{2} = {0}$ , where the unique map is the required unitary intertwiner. For the rest of the proof we may assume $φ \neq 0$ .

2.2F4F6step 1.1

By [F6], form the canonical GNS quotient $Q_{φ}$ , its Hilbert completion $H_{φ}$ , embedding $κ_{φ}$ , and canonical triple $(π_{φ}, H_{φ}, ξ_{φ})$ . The input $φ \in P (G)$ was established in step 1.1.

3.1F1F6F7step 2.2algebra

A complex-linear norm isometry $W$ between inner-product spaces preserves inner products: expanding squared norms gives $∥ u + v ∥^{2} - ∥ u - v ∥^{2} = 4 Re ⟨ u, v ⟩, ∥ u + i v ∥^{2} - ∥ u - i v ∥^{2} = 4 Im ⟨ u, v ⟩ .$ Both differences are unchanged under $W$ , so $⟨ W u, W v ⟩ = ⟨ u, v ⟩$ . Thus every $π_{j} (g)$ preserves the inner product by [F1], and the same calculation applies to each $π_{φ} (g)$ , which is a complex-linear norm isometry by [F6].

4.1F1F5F7F10step 2.2step 3.1algebra

For $j = 1, 2$ and finitely supported $f : G \to C$ , set ${\tilde{V}}_{j} (f) : = \sum_{x \in G} f (x) π_{j} (x) ξ_{j} .$ The sum is finite. Using step 3.1, the homomorphism law, and equality of the diagonal coefficients, we obtain $∥ {\tilde{V}}_{j} (f) ∥^{2} = \sum_{x, y} f (x) \overline{f (y)} ⟨ π_{j} (x) ξ_{j}, π_{j} (y) ξ_{j} ⟩ = \sum_{x, y} f (x) \overline{f (y)} ⟨ π_{j} (y^{- 1} x) ξ_{j}, ξ_{j} ⟩ = \sum_{x, y} f (x) \overline{f (y)} φ (y^{- 1} x) = B_{φ} (f, f) = ∥ [f] ∥_{Q_{φ}}^{2} .$ Consequently, if $[f] = [h]$ , then $B_{φ} (f - h, f - h) = 0$ and ${\tilde{V}}_{j} (f) - {\tilde{V}}_{j} (h) = 0$ . Thus ${\tilde{V}}_{j}$ factors through a well-defined linear isometry $V_{j} : Q_{φ} \to H_{j}$ with bound $1$ , including the zero vector.

5.1F8F9F11step 4.1choose

The space $Q_{φ}$ is normed by its quotient inner-product norm [F5, F8], and $H_{j}$ is Banach [F8]. Step 4.1 makes $V_{j}$ a bounded linear map with bound $1$ [F10]. By AC and [F11], Countable Choice holds, so [F9] gives a unique bounded extension ${\hat{V}}_{j} : H_{φ} \to H_{j}$ with ${\hat{V}}_{j} κ_{φ} = V_{j}$ . To see it is isometric, use Countable Choice and density of $κ_{φ} [Q_{φ}]$ to choose, for any $z \in H_{φ}$ , a sequence $κ_{φ} ([f_{n}]) \to z$ . Continuity and the norm identity in step 4.1 give $∥ {\hat{V}}_{j} z ∥ = \lim_{n} ∥ V_{j} ([f_{n}]) ∥ = \lim_{n} ∥ κ_{φ} ([f_{n}]) ∥ = ∥ z ∥ .$ Thus ${\hat{V}}_{j}$ is an isometry.

6.1F3F5F6F8F12step 2.2step 5.1

For every $g \in G$ , the canonical GNS action extends left translation, so ${\hat{V}}_{j} κ_{φ} ([δ_{g}]) = V_{j} ([δ_{g}]) = π_{j} (g) ξ_{j} .$ By [F12], $π_{φ} (g) ξ_{φ} = κ_{φ} ([δ_{g}])$ . The classes of point masses span $Q_{φ}$ and their images under $κ_{φ}$ are dense in $H_{φ}$ [F5, F6, F8]. The range of ${\hat{V}}_{j}$ therefore contains the dense cyclic orbit span of $ξ_{j}$ [F3].

7.1F6F8F11step 5.1step 6.1choose

The range of ${\hat{V}}_{j}$ is closed. Indeed, for any $η$ in its closure, Countable Choice [F11] selects $z_{n} \in H_{φ}$ with $∥ {\hat{V}}_{j} z_{n} - η ∥ < 1 / (n + 1)$ . The isometry in step 5.1 makes $(z_{n})$ Cauchy. Completeness of $H_{φ}$ gives a limit $z$ , and continuity of ${\hat{V}}_{j}$ yields ${\hat{V}}_{j} z = η$ . Therefore the range is both dense and closed by step 6.1, hence is all of $H_{j}$ .

7.2F1F5F6F8F12step 5.1step 6.1

For $k, g \in G$ , the left-translation action [F12] and step 6.1 give ${\hat{V}}_{j} π_{φ} (k) κ_{φ} ([δ_{g}]) = {\hat{V}}_{j} κ_{φ} ([δ_{k g}]) = π_{j} (k g) ξ_{j} = π_{j} (k) {\hat{V}}_{j} κ_{φ} ([δ_{g}]) .$ The point-mass span is dense and both sides are continuous linear maps, so ${\hat{V}}_{j} π_{φ} (k) = π_{j} (k) {\hat{V}}_{j}$ on $H_{φ}$ . Also, ${\hat{V}}_{j} ξ_{φ} = ξ_{j}$ by the point-mass case $g = e$ . Thus ${\hat{V}}_{j}$ is a surjective unitary intertwiner carrying the canonical vector to $ξ_{j}$ .

8.1F1step 7.1step 7.2construct

Define $U = {\hat{V}}_{2} {\hat{V}}_{1}^{- 1} : H_{1} \to H_{2}$ . The inverse exists by step 7.1, and step 7.2 shows $U$ is unitary, intertwines $π_{1}$ with $π_{2}$ , and satisfies $U ξ_{1} = ξ_{2}$ .

9.1F1F3step 8.1

If $U^{'}$ is another pointed unitary intertwiner, then for every $g \in G$ , $U^{'} π_{1} (g) ξ_{1} = π_{2} (g) ξ_{2} = U π_{1} (g) ξ_{1} .$ The two bounded maps agree on the dense orbit span of $ξ_{1}$ by linearity, and hence agree on all of $H_{1}$ by continuity and [F3]. This proves uniqueness.

10.1F6F9F11F12step 5.1step 7.1∎

The construction uses AC for the GNS triple and translation action [F6, F12]. AC implies DC and Countable Choice by [F11]; Countable Choice is used for the completion extensions [F9] and for the sequences in steps 5.1 and 7.1. The finite Gram identity, the specified point-mass calculations, and uniqueness on the given dense cyclic span use no further choice.

Depends on

Used by

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

Bekka, de la Harpe and Valette, Kazhdan's Property (T), Theorem C.4.10 and complete proof (standard reference, not scraped)
Bekka and de la Harpe, Unitary Representations of Groups, Duals, and Characters, Proposition 1.B.8 and complete proof (standard reference, not scraped)