TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

GNS construction for a continuous positive-type function

Statement

Assume the Axiom of Choice. Let $G$ be a topological group and let $φ : G \to C$ be a continuous function of positive type. Set $Q_{φ} = C^{(G)} / N_{φ}$ , let $H_{φ}$ be its Hilbert completion, and let $κ_{φ} : Q_{φ} \to H_{φ}$ be the canonical dense isometric embedding. Let $π_{φ}$ be the strongly continuous unitary representation obtained by extending left translations, and define $ξ_{φ} : = κ_{φ} ([δ_{e}])$ . Then $ξ_{φ}$ is cyclic and

φ (g) = ⟨ π_{φ} (g) ξ_{φ}, ξ_{φ} ⟩ (g \in G), ∥ ξ_{φ} ∥^{2} = φ (e) .

If $φ = 0$ , then $Q_{φ} = H_{φ} = {0}$ and $ξ_{φ} = 0$ ; the zero representation is cyclic under the stated convention.

Facts & Assumptions

Given: AC; a topological group $G$ ; a continuous positive-type function $φ : G \to C$ ; its GNS form $B_{φ}$ , null space $N_{φ}$ , and quotient $Q_{φ}$ .

[F1]

Under AC, left translations on $Q_{φ}$ extend to a homomorphism $π_{φ} : G \to U (H_{φ})$ on its Hilbert completion, and every vector orbit is norm-continuous (The GNS translation action is unitary and strongly continuous).

[F2]

The form $B_{φ}$ is positive semidefinite and linear in its first argument; its null space is orthogonal to every finitely supported function, and the quotient inner product satisfies $B_{φ} (δ_{x}, δ_{y}) = φ (y^{- 1} x)$ (Positive-type functions define the GNS pre-Hilbert form).

[F3]

The canonical completion map is a dense linear isometry (Completion of a normed space).

[F4]

A vector is cyclic when the complex linear span of its representation orbit is dense; the representation on the zero Hilbert space is cyclic (Cyclic vector and cyclic unitary representation).

[F5]

The diagonal matrix coefficient of a unitary representation is $g \mapsto ⟨ π (g) ξ, ξ ⟩$ (Matrix coefficient of a unitary representation).

[F6]

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

Proof

Bekka–de la Harpe–Valette state the existence of the cyclic GNS triple in Theorem C.4.10 and prove it by realizing the positive kernel, extending the left-translation isometries, checking the group law and continuity, and taking $f (e)$ as the cyclic vector (Appendix C §C.4, printed pp. 376–377). Bekka and de la Harpe give the finite-support form and quotient-completion construction in Construction 1.B.5 (§1.B, printed pp. 27–28). The proof below uses the already checked local form and translation-action lemmas, and derives the zero case directly from the null-radical property.

Proof technique: direct.

1.1F1F2F3construct

For every $g \in G$ , left translation sends $δ_{e}$ to $δ_{g}$ ; because $π_{φ} (g)$ extends the induced quotient map, $π_{φ} (g) ξ_{φ} = κ_{φ} ([δ_{g}])$ .

1.2F2F3

The same quotient inner product gives $∥ ξ_{φ} ∥^{2} = B_{φ} (δ_{e}, δ_{e}) = φ (e)$ , which is a nonnegative real because $B_{φ}$ is positive semidefinite.

1.3F2

If $φ (e) = 0$ , then [F2] gives $B_{φ} (δ_{e}, δ_{e}) = 0$ , so $δ_{e} \in N_{φ}$ . The null space is orthogonal to every finitely supported function; in particular $B_{φ} (δ_{e}, δ_{g}) = 0$ for every $g$ . The point-mass formula gives $B_{φ} (δ_{e}, δ_{g}) = φ (g^{- 1})$ , so $φ$ vanishes identically. Thus a positive-type function with zero value at the identity is necessarily the zero function.

2.1F1F2F3F5step 1.1

Using the isometry of $κ_{φ}$ and the point-mass formula in [F2], $⟨ π_{φ} (g) ξ_{φ}, ξ_{φ} ⟩ = ⟨ κ_{φ} ([δ_{g}]), κ_{φ} ([δ_{e}]) ⟩ = B_{φ} (δ_{g}, δ_{e}) = φ (g)$ . By [F5] this is the diagonal matrix coefficient of the constructed representation.

2.2F2F3F4step 1.1

Every finitely supported function is a finite linear combination of point masses, with the empty support giving the zero function as the empty linear combination, so the span of $[δ_{g}]$ over $g \in G$ is $Q_{φ}$ . By step 1.1 the orbit of $ξ_{φ}$ maps onto the point masses under $κ_{φ}$ , and $κ_{φ} (Q_{φ})$ is dense in $H_{φ}$ ; hence the orbit span is dense and $ξ_{φ}$ is cyclic by [F4], including when the quotient is zero.

3.1F1F2F3F4step 2.1step 1.2

If $φ = 0$ , then $B_{φ} = 0$ , hence $N_{φ} = C^{(G)}$ and $Q_{φ} = H_{φ} = {0}$ . The unique action on the zero space is strongly continuous; $ξ_{φ} = 0$ , its orbit span is dense by [F4], and the coefficient and norm identities from steps 2.1 and 1.2 both read $0 = 0$ .

4.1F1F6step 1.1step 3.1∎

AC is used only through Countable Choice in [F6] for the Hilbert completion and unique bounded extensions supplied by [F1]. Steps 1.1–3.1 use no additional choice: the point masses and their finite linear combinations are specified, and all quotient, coefficient, and zero-case calculations are choice-free.

Depends on

Used by

Dependency tree · two levels

34 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 (GNS Construction) (standard reference, not scraped)
Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (standard reference, not scraped)