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.
Operator-Algebraic States and GNS Representations
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Gelfand Theory and Commutative C Star Algebras
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
This page routes C*-algebra states and GNS representations to the existing general results and supplies the finite-matrix C*-algebra fact used by the worked examples. It introduces no new general GNS theorem.
Reading prerequisite
The planned representation and tensor gateway is algebraic-representation-and-tensor-symmetry-map. The group C*-algebra prerequisite is group-c-star-algebras-and-the-fell-unitary-dual.
States on C*-algebras
For a complex C*-algebra , a state is a bounded positive linear functional of norm one (States and positive functionals on a C star algebra). Under the Axiom of Choice, C star state GNS construction, purity and Polish pure-state spaces constructs its general GNS representation: a nondegenerate bounded *-representation with a unit cyclic vector, using the inner product linear in its first variable. The same item proves uniqueness up to a unique pointed unitary. Its additional clauses retain their stated hypotheses: purity is equivalent to irreducibility; separability is assumed for the separable-Hilbert-space and Polish pure-state conclusions; and the nonunital state-space clause uses norm-one restrictions from the minimal unitization.
Group-positive-type GNS
GNS construction for a continuous positive-type function has a different input: a topological group and a continuous positive-type function . Under AC it constructs a strongly continuous unitary group representation from that function. This theorem does not replace GNS for a state on an arbitrary C*-algebra. The group C*-algebra route on group-c-star-algebras-and-the-fell-unitary-dual retains its locally compact group, Haar measure, and hypotheses.
Inner-product convention
The mathematical convention throughout this route is first-variable-linear. The published QFT Fock convention in def-qft-fock-and-test-spaces is second-variable-linear, with . When comparing the GNS coefficient, translate The matrix examples on the companion page use the mathematical convention.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Finite matrix algebras with the operator norm are C star algebras
Statement
Let , let with inner product and induced Euclidean norm, and let act on by matrix multiplication. Give it the conjugate-transpose involution and the operator norm Then is a unital complex C*-algebra.
Facts & Assumptions
Given: An integer , the standard basis of , and the stated inner product, matrix operations, involution, and operator norm.
Real and complex inner-product spaces and their induced length: a complex inner product is linear in its first variable and conjugate-linear in its second; its induced norm is .
The operator norm as the least bound and as the unit-sphere or unit-ball supremum: for a bounded linear map, the operator norm is the supremum on the unit ball; rescaling gives the bound .
Cauchy–Schwarz: , with equality exactly for dependent pairs: for vectors in a real or complex inner-product space.
Every finite-dimensional normed space is Banach: a normed complex vector space with a finite ordered basis is complete.
C star algebra: a complex C*-algebra is a complete complex normed associative algebra with submultiplicative norm and a conjugate-linear involution satisfying and .
is a field, every element is uniquely , and every nonzero element has inverse and Real and imaginary parts, complex conjugation, and modulus: has conjugate and modulus ; the displayed coordinate addition and multiplication laws give the conjugation identities used below.
The induced length is a norm: the length induced by an inner product is a norm, so it satisfies absolute homogeneity and the triangle inequality; these properties are used for the Euclidean vector norm below.
Proof
Given: The data above, with .
By distributing finite sums the displayed form is linear in its first variable, and conjugating the sum gives . Also is nonnegative and zero only for , by [F6]. Thus it satisfies the complex inner-product conditions [F1]. The matrix units form a basis of the complex vector space . Matrix multiplication is bilinear by its coordinate formula, has unit , and is associative because both and equal . Entrywise conjugation and transposition make conjugate-linear and give and : the entry of is , which is the entry of by [F6]. Also by expanding the finite coordinate sums using [F1] and [F6]. The coordinate formula makes complex-linear. For each row , apply [F3] to and to get , so and every matrix action is bounded. Conversely, every linear map on is represented by its columns in this basis. Hence .
For and , rescaling the unit-ball definition [F2] gives , so taking the supremum yields . For any matrix , [F3] and the adjoint identity in step 1.1 show : the inner supremum over equals (choose if , which has unit norm by [F7]), and the adjoint identity swaps the two unit-ball suprema. Therefore . For every unit vector , by [F1] and [F3]; taking the supremum over the nonempty unit sphere gives the reverse inequality . Thus the C*-identity holds.
The operator norm is nonnegative by [F2]. The vector norm is absolutely homogeneous by [F7], so the unit-ball formula gives ; its triangle inequality [F7] gives for every unit-ball vector , hence . If , then each basis vector has , so by [F7]; all columns vanish and . Conversely, has norm zero by the definition. Thus the operator norm is a norm. The basis is finite, so [F4] makes complete for this norm. Steps 1.1 and 2.1 supply associativity, the unit, the involution, submultiplicativity, and the C*-identity; these are exactly the clauses in [F5]. Since , , so the algebra is unital under the library's convention.
Remarks
No choice principle is used. The matrix units, the coordinate estimates, and the finite-dimensional completeness result are all explicit.
5 · Examples, counterexamples and false statements
None yet.