One hundred files of this corpus say “operator algebra”. One names a C*-algebra and none names a von Neumann algebra. This asks the prior question — is it an algebra — and then builds the one that is.
WP-82 §3 gives Volume XII to operator algebras with the note that the phrase “is used across 76 files and has never had a volume”, and adds a forced position: noncommutative geometry is what a C*-algebra becomes when it is taken seriously as a space, so XII must precede XVI. Before either can be written, something has to be settled that no page has settled. Counted at HEAD, entity-aware, with this page classified out:
| pattern | files | chapters |
|---|---|---|
| operator algebra | 100 | 74 |
| semigroup | 28 | 20 |
| monoid | 10 | 5 |
| Gelfand | 4 | 4 |
| operator norm | 3 | 3 |
| C*-algebra | 1 | 1 |
| *-algebra | 1 | 1 |
| commutant | 1 | 1 |
| von Neumann algebra | 0 | 0 |
| Banach algebra | 0 | 0 |
| Gelfand–Naimark | 0 | 0 |
| Wedderburn | 0 | 0 |
Israel Gelfand's Normierte Ringe (1941) and, with Mark Naimark, the 1943 embedding theorem are the two results that let this corpus's Part II plan exist at all. The second says that any abstractly defined C*-algebra can be represented faithfully as operators on a Hilbert space — so a C*-algebra is an operator algebra, whether or not it was handed to you as one. The first, in its commutative case, says something stronger and stranger: a commutative C*-algebra is exactly the continuous functions on a compact space, and that space can be recovered from the algebra alone, as its set of characters. The space is not lost when you pass to the algebra; it is encoded in it. That sentence is what WP-82's rung 33 is built on — “stop requiring a manifold at all and let the algebra of functions be the space” — and it is why the missing floor at rung 29 matters. The move to Connes is only available if there is a C*-algebra to move.
The corpus's own page says what the four operators are, and block [1] checks each phrase against the flattened source rather than trusting a reading:
An algebra is a vector space carrying a product. To have one you need a sum, a scalar multiple, and — for a *-algebra — an involution and a norm. A nonlinear map is not an element of a vector space: F(x+y) is not F(x)+F(y), and the corpus says F is nonlinear in so many words. No page supplies a sum of C, K, F and U, none supplies an involution, and “operator norm” occurs in three files, none of them about this chain. What composition does supply is associativity and an identity, and that is a monoid.
The phrase “the operator algebra of C → K → F → U” denotes a composition monoid. Nothing is wrong with a monoid; the finding is that the name promises a different object, and that Gelfand, Naimark and GNS have nothing to act on until one is supplied. Supplying one is the rest of this page.
The corpus's own commutation argument is already linear, and its own refutation names the finite statement: a static gate composed with a sitewise map commutes exactly; a gate and an inter-site coupling do not. Make that finite. Put n sites on a ring, let K = diag(χ) with χ the mask, and let S be the cyclic shift standing in for the transport inside F. Then
Block [3] checks that equivalence over every one of the 120 masks for n = 3…6, exactly, over the rationals. That is the corpus's own dichotomy, finite and provable, and with no Lean file standing between the reader and it.
Let p be the minimal period of the mask χ under the shift, p | n. Then with A = C*(K, S) acting on ℂn:
dim A = n p A ≅ (Mp(ℂ))⊕ n/p dim A′ = n/p
Checked over all 248 masks for n = 3…7, exact over ℚ, with the algebra generated to closure rather than truncated, and zero violations. The Wedderburn data is then forced: ∑ni² = (n/p)p² = np, ∑mi² = n/p with every mi = 1, and ∑nimi = n.
The algebra is exactly as large as the gate is asymmetric. A constant mask gives the smallest algebra the shift admits; a mask with no symmetry at all gives the whole of Mn(ℂ), which is simple, contains everything, and therefore distinguishes nothing. The interesting cases are the ones in between — a mask with a period, where the algebra splits into n/p blocks and the number of blocks is the symmetry of the gate. Two of those rows corrected an expectation while this was being written: a first pass truncated the generation and reported dim 33 where the commutant forces 36, and the alternating mask at n = 4 is not the full matrix algebra at all.
At p = 1 the algebra is the circulants: commutative, dimension n. Gelfand–Naimark then says it is C(X) for X its character space, and here X is n points — the n-th roots of unity — with the Gelfand transform being the DFT. Block [5] exhibits the eigenvectors at n = 4, 6, 8, worst residual 5×10−16.
Which puts Volume I's Theorem 5.3 in a light it has not been put in. “C, K, F, U do not commute” is, in this model, the statement p > 1 — and therefore the statement that the algebra is not an algebra of functions on a space. That is precisely the sentence WP-82 needs for the step from rung 29 to rung 33, and the corpus has been one theorem away from it in seventy-four chapters without writing it down.
The word “operator” in “operator algebra” is doing work: it asserts that the elements act on a space. GNS is the construction that supplies the space from the algebra and a state, and it occurs in this corpus in two files, both written today. Block [6] runs it on the trace τ(a) = (1/n)Tr(a), which is faithful, so nothing is quotiented out: dim ℋ = n² at n = 2, 3, 4, computed as the rank of the Gram matrix of ⟨a,b⟩ = τ(b*a), with the cyclic vector Ω = I reproducing the state exactly, to zero error over the rationals.
It is three lines of linear algebra. It is also the step the phrase has been promising a hundred times, and the reason Volume XII is listed as consolidation rather than new ground: the material is present, and what is missing is the sentence that says which object it is.
The finite model is not the corpus's system. K and F act on
a continuum, F is nonlinear, and the shift on n sites is a stand-in chosen because the corpus's
own refutation argument is already exactly a statement about masks and shifts. Whether the
continuum algebra is a crossed product, and whether p has a continuum analogue, is untouched.
The Lean names on the source page (gate_commutes,
coupling_not_commute) are not relied on here —
ZeoliteCommutation.lean is already recorded in docs/audit-log.md as
resolving nowhere under any root, so block [3] re-derives the finite statement instead of
citing it.
| Gelfand 1941 | I. M. Gelfand, “Normierte Ringe”, Matematicheskii Sbornik 9. |
| Gelfand–Naimark 1943 | I. M. Gelfand and M. A. Naimark, “On the imbedding of normed rings into the ring of operators in Hilbert space”, Matematicheskii Sbornik 12. |
| in-corpus | HVEH Proof I — Operator Algebra (the chain, the mask, the advective F) · Vol I Theorem 5.3 · WP-82 §3 (Volume XII) · ch-connes · ch-conley |
| verification | book7/ch-gelfand-verify.py — eight blocks, standard library only, exact over ℚ where exactness is available. Every number on this page is printed by it. |
No priority is claimed. Gelfand–Naimark, the GNS construction, Burnside's theorem and Wedderburn's are classical, and the period rule of Part V is an exercise in them — derived here rather than looked up, and stated as classical rather than as new. What belongs to this corpus is only the question it answers.