Strong locality of unitary vertex operator algebras

Strong locality of unitary vertex operator algebras concerns the passage between two mathematical formulations of chiral conformal field theory. A vertex operator algebra (VOA) records field modes and their algebraic identities. A conformal net assigns von Neumann algebras of bounded observables to intervals of the circle. Carpi, Kawahigashi, Longo and Weiner conjectured that every simple unitary VOA is strongly local, so that its smeared fields generate a conformal net. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September 2026, claims the conjecture for strongly rational VOAs. It also claims a comparison of the full representation theories in that setting. This page summarizes the published claims and lists publicly available follow-up work.

Background

• Definitions, as in the manuscript.
  • A VOA V is strongly rational if it is of CFT type, isomorphic to its graded contragredient, rational (admissible modules are completely reducible) and C₂-cofinite. Unitarity means a normalized positive invariant Hermitian form with its antilinear PCT involution.
  • Polynomial energy bounds bound each mode a_(n) by a polynomial in |n| times a power of 1 + L₀. They make the smeared fields closable. For an interval I of the circle, A_V(I) is the von Neumann algebra generated by the closed smeared fields with support in I.
  • V is CKLW-strongly local if it is energy-bounded and A_V(I) commutes with A_V(I′) for the complementary interval I′. A conformal net is completely rational if it is irreducible, split and strongly additive with finite μ-index.
• As recounted in the introduction of the manuscript:
  • The conjecture. Carpi, Kawahigashi, Longo and Weiner made strong locality the analytic condition for constructing a conformal net from a simple unitary VOA, and conjectured it for every simple unitary VOA (Conjecture 8.18 of From vertex operator algebras to conformal nets and back, Memoirs of the AMS 254 (2018), no. 1213; arXiv:1503.01260v4). Their examples include unitary affine and Virasoro VOAs and the moonshine VOA. The manuscript notes that commuting unbounded fields on a common domain need not generate commuting von Neumann algebras.
  • Tensor structures. Huang proved rigidity and modularity for strongly rational VOAs, and Kawahigashi, Longo and Müger proved modularity for completely rational conformal nets.
  • Known cases of the comparison. Complete unitarity, the braided equivalence and complete rationality were known for affine VOAs at positive integral levels, even positive-definite lattice VOAs, parafermion VOAs and type ADE discrete-series W-algebras. Gui's results extend this to finite tensor products, regular cosets and, under stated hypotheses, extensions.
  • The converse direction. Henriques and Tener construct a unitary VOA from a conformal net with finite-dimensional vacuum energy spaces and reconstruct modules from net representations.
  • Analytic methods. Carpi, Tanimoto and Weiner showed that optimal energy order for Hermitian primary generators implies strong locality. Carpi and Tomassini obtained an exponential bound from C₂-cofiniteness and a contraction that improves it to polynomial growth.

The original result

• Strongly rational unitary VOAs (25 September 2026). The manuscript Strongly rational unitary vertex operator algebras and conformal nets, Theorem 1.1: let V be a simple unitary strongly rational VOA over C. Then:
  • V has polynomial energy bounds and is CKLW-strongly local, and the algebras A_V(I) form an irreducible conformal net A_V;
  • V is completely unitary: every simple grading-restricted module is unitarizable, and all canonical invariant Hermitian fusion forms are positive definite;
  • every unitary grading-restricted finite-length module is strongly integrable;
  • the net A_V is completely rational;
  • the Carpi–Weiner–Xu functor gives a braided unitary tensor equivalence from the module category Rep(V) onto the finite-index sectors of A_V, with Connes fusion and DHR braiding.
• The manuscript states that Theorem 1.1 establishes Conjecture 8.18 of Carpi, Kawahigashi, Longo and Weiner under strong rationality. A corollary, through Gui's extension theorems, identifies normalized irreducible finite-index local extensions of these nets with simple CFT-type conformal extensions of the VOAs.
• Method, as described:
  • C₂-cofiniteness controls the normal products of a finite generating family. Two contraction inequalities give polynomial energy bounds and then the optimal energy order needed for locality.
  • Annulus estimates give bounded local regularizations of creation fields; these integrate every already unitary module.
  • Positivity of the fusion forms is proved for unitary inputs, and a permutation-orbifold argument (flip-fixed subalgebra of V ⊗ V) unitarizes every simple module.
  • Gui's hypotheses for the tensor embedding are then verified. A reconstruction argument based on Henriques–Tener shows that every irreducible sector is in the image, and the Longo–Xu dichotomy gives complete rationality.
• Source. Commit 1581d4c of the openai/math repository: Strongly rational unitary vertex operator algebras and conformal nets.
• Formalization, as described by the repository.
  • The scope note lean/docs/280.md describes the formalized result as "the first construction step": for a simple unitary strongly rational VOA, polynomial energy bounds and strong locality, and an irreducible conformal net with the stated covariance, vacuum and positive-energy properties. It adds: "The selected statement does not include complete rationality of the net, unitarizability of all simple modules, the braided tensor equivalence, or the classification of local extensions described in the paper."
  • The Comparator challenge VertexAlgebraNet.lean states OAI.MinimalVertex.main. Its hypotheses are that the VOA is simple and strongly rational (on a unitary structure); its conclusion is the conjunction of polynomial energy bounds, CKLW strong locality and the existence of an irreducible conformal net structure on the interval algebras.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial". The challenge states the strong-locality core (energy bounds, strong locality and an irreducible conformal net with covariance, unique vacuum and positive energy). Complete rationality, unitarizability of all simple modules and the braided tensor equivalence are not stated. Records a sandboxed Comparator pass for VertexAlgebraNet.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list VertexAlgebraNet. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38051470892	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the VertexAlgebraNet solution (702 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.

Notes

• The kernel checks above concern the formal statement OAI.MinimalVertex.main as written, which covers the strong-locality part of Theorem 1.1. Complete rationality, unitarizability of all simple modules, the braided tensor equivalence and the extension correspondence have no formal statement in the collection.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.