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.
Regularity of a vertex operator algebra
Definition
Let be a conformal vertex algebra of CFT type. Say that is regular if every weak -module, meaning a module with the field axioms but no grading assumption, is an internal direct sum of simple ordinary -modules. “Ordinary” means semisimple with finite-dimensional eigenspaces and weights bounded below. Regularity is stronger than complete reducibility of admissible modules and does not itself assert -cofiniteness.
Statement references
Facts & Assumptions
Given: is a conformal vertex algebra of CFT type.
Conformal vertex algebra of CFT type: CFT type supplies the conformal grading and the operator used in ordinary modules.
Module for an ordinary vertex algebra: a weak module satisfies lower truncation, vacuum and module Jacobi, with no grading requirement.
Ordinary module: an ordinary module has semisimple , finite-dimensional eigenspaces and a lower bound on real parts of weights.
Proof
The definition quantifies over every module satisfying [F2] and requires it to be an internal direct sum of simple -submodules. The zero module is the empty direct sum.
The summands must satisfy each clause of [F3]; no grading of a general weak module, rationality, or -cofiniteness is included in this definition.
Proof status
This definition records weak-module complete reducibility into ordinary modules under the explicit CFT-type convention; it asserts no equivalence with other notions.