# Unitary vertex operator algebras and conformal nets

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Strongly rational unitary vertex operator algebras and conformal nets](../../preprints/Strongly-rational-unitary-vertex-operator-algebras-and-conformal-nets-September-25-2026/paper.pdf)

## Scope

The linked formalization proves the first construction step relating strongly rational unitary vertex operator algebras to conformal nets. For a simple unitary strongly rational vertex operator algebra, it establishes polynomial energy bounds and strong locality and constructs an irreducible conformal net with the stated covariance, vacuum, and positive-energy properties.

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.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Energy bounds, strong locality, and an irreducible conformal net | [VertexAlgebraNet.lean](../ComparatorChallenges/VertexAlgebraNet.lean) |