Operator algebras

Naimark's problem

Brief report available

A proposed ZFC construction and its formal-source record

The Brief Report presents a proposed ZFC construction of a unital, simple, infinite-dimensional C*-algebra whose nonzero irreducible representations are all unitarily equivalent, yet which admits a faithful tracial representation on a separable Hilbert space. Its two principal arguments classify the irreducible representations of one concrete generated algebra and show that extending the trace of its CAR subalgebra does not enlarge the cyclic GNS space. The manuscript includes proofs, point-of-use references, and cardinality consequences. Its formal-source and manuscript-correspondence records are distinct.

The mathematical claim

CLAIM PRESENTED IN THE BRIEF REPORT

The Brief Report presents a proposed ZFC construction of a unital, simple, infinite-dimensional C*-algebra whose nonzero irreducible representations are all unitarily equivalent, yet which admits a faithful tracial representation on a separable Hilbert space. Its two principal arguments classify the irreducible representations of one concrete generated algebra and show that extending the trace of its CAR subalgebra does not enlarge the cyclic GNS space. The manuscript includes proofs, point-of-use references, and cardinality consequences. Its formal-source and manuscript-correspondence records are distinct.

The proposed construction, its formal source, and manuscript-correspondence records are distinct.

The earlier Brief Report is preserved as a preliminary, AI-assisted record. The subsequent arXiv paper is listed below.

Verification record

These entries refer to different aspects of the project. They must not be combined into a single claim of independent verification of the paper or the earlier Brief Report.

Prior-art searchDocumented through 20 September 2026
Scope and evidence

No equivalent result identified in the sources examined. This bounded finding is neither a novelty guarantee nor a verification of the proposed proof.

Lean formalizationMathlibAnnex v0.4.0 source public
Scope and evidence

The public MathlibAnnex v0.4.0 source includes this Project. Its recorded qualification is separate from manuscript correspondence.

Text ↔ formal sourceTargeted correspondence recorded
Scope and evidence

Corollary 6.2 has a targeted accepted mapping to five formal endpoints and a standard Hilbert-space consequence. This does not approve the other 13 correspondence groups. Orthonormal-basis cardinality is not a direct Lean endpoint or a Hamel-dimension statement.

LFH reading materialsResearch Companion available
Scope and evidence

68 selected Declaration Cards with exact source and dependency-guided routes; the separate CH route reuses two density Cards and adds one CH consequence, giving 69 distinct Naimark Cards in the Catalog.

Paper / public releasePreprint available on arXiv
Scope and evidence

arXiv v1 was submitted on 22 September 2026. This is a preprint, without a claim of journal acceptance, peer review or independent verification. Brief Report Draft R1 and Prior-Art Search R1 were first published on 21 September 2026.

What these distinctions mean

Report and related materials

The Brief Report is a preliminary mathematical record. Its preparation date is distinct from publication and review dates.

Brief ReportPDF · draft-r1 · Prepared 21 Sept 2026 · 9 pages
File details
Size
327,459 bytes
SHA-256
88f9e2c78553a99558b76c00328470c967b8a981e67a0cc7652472e1ea6e6b88
Read brief report (PDF)
Prior-Art Search NotePDF · r1 · Prepared 21 Sept 2026 · 4 pages
File details
Size
254,335 bytes
SHA-256
75d6d04c768850e7b5ac6d2c9a55b06eb6c6d37b64994da2568081e53f0cb0d0
Read prior-art search note (PDF)

Comments, corrections, and collaborative verification are welcome. People and contact

Formalization and LFH

MathlibAnnex source v0.4.0 is public, at commit 437e6e46228bbb8e91211ebded349d7a30020e73. Recorded source qualification is separate from manuscript correspondence.

The Research Companion contains 68 selected Declaration Cards, with a separate CH route: Open Companion · PDF · JSON.

Corollary 6.2 retains its targeted mapping to five endpoints and a standard Hilbert-space consequence. Other correspondence groups have not been reapproved.

The arXiv paper's formalization claim excludes Corollary 5.4 (tracial weak closure). The orthonormal-basis cardinalities in Corollary 6.2 are standard consequences of density statements, not dedicated formal endpoints. Result-level correspondence is distinct from line-by-line formalization; the paper listing adds no new mapping approval.

Version and publication record

Brief Report Draft R1 and Prior-Art Search R1 first published 21 Sept 2026.

Responsible for publication: Ryotaro Tanaka. No mathematical author is named. Citation metadata · Version history.

Prior-art search

Prior-art search: Documented through 20 September 2026.

The comparison concerns the proposed ZFC construction of a single C*-algebra with one irreducible equivalence class and a faithful separable tracial representation. Rosenberg's theorem assumes an irreducible action on a separable Hilbert space [1]; it does not state the same hypothesis as a faithful reducible action. Akemann–Weaver construct a counterexample under Jensen's diamond principle [2]. The closest inspected general construction, Calderón–Farah's Theorem 5.4, uses a weaker diamond principle together with CH and leaves the ZFC-only question open [3]. Their separably represented examples with at least two irreducible classes do not give the combined conclusion considered here. The note also distinguishes established homogeneity, excision, and GNS arguments from the proposed construction.

Finding: No equivalent result identified in the sources examined. This is a record of the sources examined, not a guarantee that no earlier result exists or a verification of the proposed proof. See the accompanying English Prior-Art Search Note.

Selected references: [1] Rosenberg (1953), Theorem 4, p.530. [2] Akemann–Weaver (2004). [3] Calderón–Farah (2023), Theorem 5.4 and §8.

Prior-Art Search Note (PDF)

About the report

Publication responsibility

Responsible for publication: Ryotaro Tanaka. This covers release, versioning, corrections and withdrawal, and does not imply mathematical authorship or independent verification.

Read about MathlibAnnex

Record history

Preprint v1

Submitted at 18:23:08 UTC (23 September, 03:23:08 JST). This submission time is not an announcement time or an HP publication date.

First public report editions

Brief Report Draft R1 remains available as a preliminary, AI-assisted record. Targeted correspondence records do not constitute approval of all 14 correspondence groups.

Brief Report Draft R1 and Prior-Art Search R1 are public. The search cutoff remains 20 September 2026. Publication adds no new mathematical review or whole-document correspondence approval.

First public editions prepared for review

Brief Report Draft R1 and Prior-Art Search R1 were prepared for review. The search cutoff remains 20 September 2026; preparation did not constitute publication.

Send a correction or prior-art reference for this page or Brief Report
Back to top ↑