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.
Integrable WZW insertions on a punctured sphere
Definition
Fix a finite-dimensional complex simple , its invariant form with long roots of square , dual Coxeter number , and highest root . At level , an integrable WZW insertion of label at a marked point is the affine module of lem-cft-wzw-integrable-affine-highest-weight-modules-exist-positive-energy, where is dominant integral and . The affine bracket is the one in def-untwisted-affine-central-extension, with central generator acting by , and . The highest vector has -weight zero. The horizontal top is the degree-zero space , with its finite-dimensional -action. A finite collection of such insertions uses one common level and the same normalized form.
The Sugawara denominator is , which is nonzero under these hypotheses. The grading asserted here is the lower-bounded affine degree ; restrictedness has the exact meaning in def-positive-energy-affine-module. It does not assert an integral Sugawara -spectrum, unitarity, a finite-rank conformal-block bundle, or a full left-right CFT.
Definition references
Facts & Assumptions
Given: The normalized affine convention and the level, dominant-weight, and integrability hypotheses above.
Full AC is assumed through The Axiom of Choice, as required by the finite-dimensional highest-weight classification.
Integrable affine WZW highest-weight modules are graded and restricted proves existence, integrability, finite-dimensional horizontal top, degree grading, and restrictedness.
Untwisted affine central extension fixes the central term and normalized form used by the Sugawara denominator.
Restricted affine-current module calls a module restricted when every vector is killed by all sufficiently high positive current modes; this definition alone supplies no degree grading.
Dual Coxeter number for the normalized invariant form defines the dual Coxeter number for the normalized form; it is positive for a finite-dimensional simple .
Highest-weight classification classifies the finite-dimensional simple horizontal top by its dominant integral highest weight.
Proof
The lemma [F1] applies to every allowed , so the module named in the Definition exists, is simple and integrable, and has the specified finite-dimensional top. The classification in [F5] fixes that top as . Its current action is at level with the bracket [F2]. This makes the label data a well-defined collection of affine insertions.
Since and by [F4], . The degree and restrictedness assertions are precisely those proved in [F1] using the actual meaning [F3]; no integer -spectrum is inferred.