Lean statement

Energy bounds, strong locality, and an irreducible conformal net

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.MinimalVertex.main

Lean statement file: VertexAlgebraNet.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 280 link it.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem main (_hSimple : A.toVertexAlgebra.IsSimple)    (hSR : A.IsStronglyRational.{u,v}) :    A.PolynomialEnergyBounds ∧ OAI.MinimalVertex.CKLWStrongLocal U hSR.2.2 ∧      Nonempty (OAI.MinimalVertex.IrreducibleConformalNetStructure (OAI.MinimalVertex.intervalAlgebra U hSR.2.2)) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.StronglyRationalVOA.StateField line 11

noncomputable abbrev StateField (V : Type u) (W : Type v)    [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] :=  V →ₗ[ℂ] VertexOperator ℂ W

definition OAI.StronglyRationalVOA.mode line 15

noncomputable def mode {W : Type v} [AddCommGroup W] [Module ℂ W]    (Y : OAI.StronglyRationalVOA.StateField V W) (a : V) (n : ℤ) : Module.End ℂ W :=  VertexOperator.ncoeff (Y a) n

definition OAI.StronglyRationalVOA.JacobiIdentity line 19

noncomputable def JacobiIdentity (Y : OAI.StronglyRationalVOA.StateField V V) : Prop :=  ∀ (a b c : V) (m n k : ℤ),    (∑ᶠ j : ℕ, Ring.choose (m : ℂ) j •      OAI.StronglyRationalVOA.mode Y (OAI.StronglyRationalVOA.mode Y a (n + j) b) (m + k - j) c) =    ∑ᶠ j : ℕ, ((-1 : ℂ) ^ j * Ring.choose (n : ℂ) j) •      (OAI.StronglyRationalVOA.mode Y a (m + n - j) (OAI.StronglyRationalVOA.mode Y b (k + j) c) -        (-1 : ℂ) ^ n • OAI.StronglyRationalVOA.mode Y b (n + k - j) (OAI.StronglyRationalVOA.mode Y a (m + j) c))

structure OAI.StronglyRationalVOA.VertexAlgebra line 27

structure VertexAlgebra (V : Type u) [AddCommGroup V] [Module ℂ V] where  vacuum : V  fields : OAI.StronglyRationalVOA.StateField V V  vacuum_mode : ∀ (n : ℤ), OAI.StronglyRationalVOA.mode fields vacuum n = if n = -1 then 1 else 0  creation : ∀ a : V, OAI.StronglyRationalVOA.mode fields a (-1) vacuum = a  creation_truncation : ∀ (a : V) (n : ℤ), 0 ≤ n → OAI.StronglyRationalVOA.mode fields a n vacuum = 0  jacobi : OAI.StronglyRationalVOA.JacobiIdentity fields

definition OAI.StronglyRationalVOA.VertexAlgebra.translation line 41

noncomputable def translation : Module.End ℂ V where  toFun a := OAI.StronglyRationalVOA.mode A.fields a (-2) A.vacuum  map_add' a b := by simp [OAI.StronglyRationalVOA.mode]  map_smul' z a := by simp [OAI.StronglyRationalVOA.mode]

definition OAI.StronglyRationalVOA.VertexAlgebra.c2 line 46

noncomputable def c2 : Submodule ℂ V :=  Submodule.span ℂ {x | ∃ a b : V, x = OAI.StronglyRationalVOA.mode A.fields a (-2) b}

definition OAI.StronglyRationalVOA.VertexAlgebra.C2Cofinite line 49

noncomputable def C2Cofinite : Prop := FiniteDimensional ℂ (V ⧸ A.c2)

definition OAI.StronglyRationalVOA.VertexAlgebra.IsIdeal line 51

noncomputable def IsIdeal (I : Submodule ℂ V) : Prop :=  (∀ a : V, ∀ n : ℤ, ∀ x ∈ I, OAI.StronglyRationalVOA.mode A.fields a n x ∈ I) ∧  ∀ x ∈ I, A.translation x ∈ I

definition OAI.StronglyRationalVOA.VertexAlgebra.IsSimple line 55

noncomputable def IsSimple : Prop :=  A.vacuum ≠ 0 ∧ ∀ I : Submodule ℂ V, A.IsIdeal I → I = ⊥ ∨ I = ⊤

definition OAI.StronglyRationalVOA.ModuleJacobiIdentity line 63

noncomputable def ModuleJacobiIdentity {W : Type v} [AddCommGroup W] [Module ℂ W]    (A : OAI.StronglyRationalVOA.VertexAlgebra V) (Y : OAI.StronglyRationalVOA.StateField V W) : Prop :=  ∀ (a b : V) (c : W) (m n k : ℤ),    (∑ᶠ j : ℕ, Ring.choose (m : ℂ) j •      OAI.StronglyRationalVOA.mode Y (OAI.StronglyRationalVOA.mode A.fields a (n + j) b) (m + k - j) c) =    ∑ᶠ j : ℕ, ((-1 : ℂ) ^ j * Ring.choose (n : ℂ) j) •      (OAI.StronglyRationalVOA.mode Y a (m + n - j) (OAI.StronglyRationalVOA.mode Y b (k + j) c) -        (-1 : ℂ) ^ n • OAI.StronglyRationalVOA.mode Y b (n + k - j) (OAI.StronglyRationalVOA.mode Y a (m + j) c))

structure OAI.StronglyRationalVOA.WeakModule line 72

structure WeakModule (A : OAI.StronglyRationalVOA.VertexAlgebra V) (W : Type v)    [AddCommGroup W] [Module ℂ W] where  fields : OAI.StronglyRationalVOA.StateField V W  vacuum_mode : ∀ n : ℤ, OAI.StronglyRationalVOA.mode fields A.vacuum n = if n = -1 then 1 else 0  jacobi : OAI.StronglyRationalVOA.ModuleJacobiIdentity A fields

definition OAI.StronglyRationalVOA.WeakModule.IsInvariant line 85

noncomputable def IsInvariant (I : Submodule ℂ W) : Prop :=  ∀ a : V, ∀ n : ℤ, ∀ x ∈ I, OAI.StronglyRationalVOA.mode M.fields a n x ∈ I

definition OAI.StronglyRationalVOA.WeakModule.CompletelyReducible line 88

noncomputable def CompletelyReducible : Prop :=  ∀ I : Submodule ℂ W, M.IsInvariant I →    ∃ J : Submodule ℂ W, M.IsInvariant J ∧ IsCompl I J

structure OAI.StronglyRationalVOA.CFTTypeVOA line 97

structure CFTTypeVOA (V : Type u) [AddCommGroup V] [Module ℂ V]    extends OAI.StronglyRationalVOA.VertexAlgebra V where

Show the remaining 20 lines

  conformalVector : V  centralCharge : ℂ  grade : ℕ → Submodule ℂ V  grading_internal : DirectSum.IsInternal grade  grade_finite : ∀ d, FiniteDimensional ℂ (grade d)  vacuum_ne_zero : vacuum ≠ 0  grade_zero : grade 0 = ℂ ∙ vacuum  conformal_mem : conformalVector ∈ grade 2  conformal_energy : ∀ d, ∀ a ∈ grade d,    OAI.StronglyRationalVOA.mode fields conformalVector 1 a = (d : ℂ) • a  conformal_translation : OAI.StronglyRationalVOA.mode fields conformalVector 0 = toVertexAlgebra.translation  translation_covariance : ∀ a : V, ∀ n : ℤ,    OAI.StronglyRationalVOA.mode fields (toVertexAlgebra.translation a) n =      (-(n : ℂ)) • OAI.StronglyRationalVOA.mode fields a (n - 1)  virasoro : ∀ m n : ℤ,    (OAI.StronglyRationalVOA.mode fields conformalVector (m + 1)).comp (OAI.StronglyRationalVOA.mode fields conformalVector (n + 1)) -      (OAI.StronglyRationalVOA.mode fields conformalVector (n + 1)).comp (OAI.StronglyRationalVOA.mode fields conformalVector (m + 1)) =    ((m - n : ℤ) : ℂ) • OAI.StronglyRationalVOA.mode fields conformalVector (m + n + 1) +      (if m + n = 0 then (centralCharge / 12) * ((m : ℂ)^3 - m) else 0) •        (1 : Module.End ℂ V)

definition OAI.StronglyRationalVOA.CFTTypeVOA.virasoroMode line 126

noncomputable def virasoroMode (m : ℤ) : Module.End ℂ V :=  OAI.StronglyRationalVOA.mode A.fields A.conformalVector (m + 1)

definition OAI.StronglyRationalVOA.CFTTypeVOA.physicalMode line 129

noncomputable def physicalMode (a : V) (d : ℕ) (m : ℤ) : Module.End ℂ V :=  OAI.StronglyRationalVOA.mode A.fields a (m + d - 1)

definition OAI.StronglyRationalVOA.CFTTypeVOA.energyShift line 132

noncomputable def energyShift : Module.End ℂ V := 1 + A.virasoroMode 0

definition OAI.StronglyRationalVOA.CFTTypeVOA.gradingEquiv line 134

noncomputable def gradingEquiv : V ≃ₗ[ℂ] DirectSum ℕ (fun d => A.grade d) :=  (LinearEquiv.ofBijective (DirectSum.coeLinearMap A.grade) A.grading_internal).symm

definition OAI.StronglyRationalVOA.CFTTypeVOA.IsAdmissible line 137

noncomputable def IsAdmissible {W : Type v} [AddCommGroup W] [Module ℂ W]    (M : OAI.StronglyRationalVOA.WeakModule A.toVertexAlgebra W) : Prop :=  ∃ G : ℤ → Submodule ℂ W,    DirectSum.IsInternal G ∧ (∀ k : ℤ, k < 0 → G k = ⊥) ∧      ∀ d : ℕ, ∀ a ∈ A.grade d, ∀ n k : ℤ, ∀ x ∈ G k,        OAI.StronglyRationalVOA.mode M.fields a n x ∈ G (k + d - n - 1)

definition OAI.StronglyRationalVOA.CFTTypeVOA.IsRational line 144

noncomputable def IsRational : Prop :=  ∀ (W : Type v) [AddCommGroup W] [Module ℂ W]    (M : OAI.StronglyRationalVOA.WeakModule A.toVertexAlgebra W),    A.IsAdmissible M → M.CompletelyReducible

definition OAI.StronglyRationalVOA.CFTTypeVOA.PolynomialEnergyBound line 155

noncomputable def PolynomialEnergyBound (a : V) : Prop :=  ∃ C : ℝ, 0 < C ∧ ∃ p k : ℕ, ∀ (n : ℤ) (b : V),    ‖OAI.StronglyRationalVOA.mode A.fields a n b‖ ≤ C * (1 + |(n : ℝ)|) ^ p * ‖(A.energyShift ^ k) b‖

definition OAI.StronglyRationalVOA.CFTTypeVOA.PolynomialEnergyBounds line 159

noncomputable def PolynomialEnergyBounds : Prop := ∀ a : V, A.PolynomialEnergyBound a

structure OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure line 161

structure UnitaryStructure where

Show the remaining 13 lines

  pct : V →ₛₗ[starRingEnd ℂ] V  pct_involutive : Function.Involutive pct  pct_vacuum : pct A.vacuum = A.vacuum  pct_conformal : pct A.conformalVector = A.conformalVector  pct_modes : ∀ (a b : V) (n : ℤ),    pct (OAI.StronglyRationalVOA.mode A.fields a n b) = OAI.StronglyRationalVOA.mode A.fields (pct a) n (pct b)  vacuum_norm : ‖A.vacuum‖ = 1  invariant : ∀ d : ℕ, ∀ a ∈ A.grade d, ∀ n : ℤ, ∀ b c : V,    inner ℂ (OAI.StronglyRationalVOA.mode A.fields a n b) c =      inner ℂ b (((-1 : ℂ) ^ d) •        ∑ j ∈ Finset.range (d + 1), ((j.factorial : ℂ)⁻¹) •          OAI.StronglyRationalVOA.mode A.fields ((A.virasoroMode 1 ^ j) (pct a))            (2 * (d : ℤ) - j - n - 2) c)

definition OAI.StronglyRationalVOA.HilbertCore._root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space line 183

noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℂ V] :    Submodule ℂ (Completion V) :=  LinearMap.range (Completion.toComplₗᵢ : V →ₗᵢ[ℂ] Completion V).toLinearMap

46 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: algebra, algebras, bounds, braided, conformal, energy, equivalence, irreducible and eleven more.

Theorem 1.1 of Strongly rational unitary vertex operator algebras and conformal nets

Theorem

Let V be a simple unitary strongly rational vertex operator algebra over \mathbb C. Then:

(1)
V has polynomial energy bounds and is CKLW-strongly local. The algebras (eq:intro-net) form an irreducible conformal net A_V.
(2)
V is completely unitary: every simple grading-restricted module is unitarizable, and all canonical invariant Hermitian fusion forms are positive definite.
(3)
Every unitary grading-restricted finite-length module is strongly integrable, with the closed-field equality (eq:intro-cwx).
(4)
The net A_V is completely rational.
(5)
After choosing invariant positive forms on the simple modules, the Carpi–Weiner–Xu functor gives a braided unitary tensor equivalence
\Rep(V)\simeq\Rep^u(V) \xrightarrow{\ F_{\mathrm{CWX}}^V\ }\Rep^f(A_V).
The tensor structure and braiding on the right are Connes fusion and DHR braiding, with a common orientation convention for the circle.

Section 1, Introduction Read it in the paper TeX source, line 96

Show the TeX

Let $V$ be a simple unitary strongly rational vertex operator algebra over $\mathbb C$. Then:
\begin{enumerate}[label=\textup{(\arabic*)}]
\item $V$ has polynomial energy bounds and is CKLW-strongly local. The algebras \eqref{eq:intro-net} form an irreducible conformal net $A_V$.
\item $V$ is completely unitary: every simple grading-restricted module is unitarizable, and all canonical invariant Hermitian fusion forms are positive definite.
\item Every unitary grading-restricted finite-length module is strongly integrable, with the closed-field equality \eqref{eq:intro-cwx}.
\item The net $A_V$ is completely rational.
\item After choosing invariant positive forms on the simple modules, the Carpi--Weiner--Xu functor gives a braided unitary tensor equivalence
\[
 \Rep(V)\simeq\Rep^u(V)
 \xrightarrow{\ F_{\mathrm{CWX}}^V\ }\Rep^f(A_V).
\]
The tensor structure and braiding on the right are Connes fusion and DHR braiding, with a common orientation convention for the circle.
\end{enumerate}

Other possible paper matches, closest wording first

Corollary 6.3 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: lifted, commutant, smooth, observable, charge, integers and 20 more.
Theorem 5.3 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: family, domains, rotations, equality, unique, action and 14 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: includes.
Corollary 3.4 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: generate, cklw, smeared, vertex, irreducible, net and eight more.
Theorem 3.1 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: order, linear, virasoro, polynomial, one, integer and twelve more.
Corollary 9.3 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: extending, cft, one, unique, completely, vector and 13 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: extensions, described, equivalence, tensor and braided.
Proposition 5.1 of Strongly rational unitary vertex operator algebras and conformal nets. Words of the Lean statement, its names split into words, that also appear in the theorem: smooth, observable, charged, interval, disjoint, smear and nine more.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

Accepted Their term: “accepted”.
Re-run through Comparator with Lean’s kernel: accepted (the check took 177 s).
Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 280’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet
Finds part of it stated, or a narrower or weaker statement Their term: “partial”.
Only a special case is stated, or a co-equal headline claim has no challenge statement. Their record
Their note: MinimalVertex.main (hSimple : A.toVertexAlgebra.IsSimple) (hSR : A.IsStronglyRational) : A.PolynomialEnergyBounds ∧ CKLWStrongLocal U _ ∧ Nonempty (IrreducibleConformalNetStructure (intervalAlgebra U _)): polynomial energy bounds, strong locality (intervalAlgebra I ≤ (intervalAlgebra I.complement).commutant) and an irreducible conformal net (isotony, locality, Möbius and Diff(S¹) covariance, unique vacuum, positive energy) for a simple unitary strongly rational VOA, i.e. the strong-locality core of the summary. Not stated: complete rationality of the net (the summary says it generates a COMPLETELY RATIONAL net), unitarizability of all simple modules, and the braided unitary tensor equivalence of Rep(V) with the net's finite-index sectors (docs: 'does not include complete rationality ... unitarizability ... the braided tensor equivalence').
Definitions the group asks readers to compare with the paper: Entire VOA/conformal-net stack is hand-built (VertexAlgebra, CFTTypeVOA, IsStronglyRational := IsSelfContragredient ∧ IsRational ∧ C2Cofinite, smearedMap, closedSmoothField, localAlgebra, IrreducibleConformalNetStructure), with many definitions using junk defaults: smearedMap := if h : ∀ v, Summable (..) then tsumMap else 0, smoothSmearedField := if h : .. then .. else 0, resolvent/flow := if h : ∃ L, .. then h.choose else 0, projectiveStandardAction := if h : ∃ L, .. then h.choose else 1. Not Mathlib notions; fidelity rests on these encodings.
Carlos Toledo’s cert-machine
Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — DECLARED”.
The challenge statements state less than the headline, and OpenAI’s Lean note says so. Their record
Their note: Complete rationality of the net, unitarizability of simple modules, and the braided unitary tensor equivalence.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states part of a paper’s theorem”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

830 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 243 to its own declarations, 403 to Mathlib’s documentation. 82 declared names also link to the same declaration in OpenAI’s library. 6 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlib/-! The strongly rational unitary vertex operator algebra main result, clause (1). -/noncomputable sectionuniverse u v wnamespace OAI.StronglyRationalVOAvariable {V : Type u} [AddCommGroup V] [Module ℂ V]noncomputable abbrev StateField (V : Type u) (W : Type v)    [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] :=  V →ₗ[ℂ] VertexOperator ℂ Wnoncomputable def mode {W : Type v} [AddCommGroup W] [Module ℂ W]    (Y : OAI.StronglyRationalVOA.StateField V W) (a : V) (n : ℤ) : Module.End ℂ W :=  VertexOperator.ncoeff (Y a) nnoncomputable def JacobiIdentity (Y : OAI.StronglyRationalVOA.StateField V V) : Prop :=  ∀ (a b c : V) (m n k : ℤ),    (∑ᶠ j : ℕ, Ring.choose (m : ℂ) j •      OAI.StronglyRationalVOA.mode Y (OAI.StronglyRationalVOA.mode Y a (n + j) b) (m + k - j) c) =    ∑ᶠ j : ℕ, ((-1 : ℂ) ^ j * Ring.choose (n : ℂ) j) •      (OAI.StronglyRationalVOA.mode Y a (m + n - j) (OAI.StronglyRationalVOA.mode Y b (k + j) c) -        (-1 : ℂ) ^ n • OAI.StronglyRationalVOA.mode Y b (n + k - j) (OAI.StronglyRationalVOA.mode Y a (m + j) c))structure VertexAlgebra (V : Type u) [AddCommGroup V] [Module ℂ V] where  vacuum : V  fields : OAI.StronglyRationalVOA.StateField V V  vacuum_mode : ∀ (n : ℤ), OAI.StronglyRationalVOA.mode fields vacuum n = if n = -1 then 1 else 0  creation : ∀ a : V, OAI.StronglyRationalVOA.mode fields a (-1) vacuum = a  creation_truncation : ∀ (a : V) (n : ℤ), 0 ≤ n → OAI.StronglyRationalVOA.mode fields a n vacuum = 0  jacobi : OAI.StronglyRationalVOA.JacobiIdentity fieldsend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.VertexAlgebravariable {V : Type u} [AddCommGroup V] [Module ℂ V]variable (A : VertexAlgebra V)noncomputable def translation : Module.End ℂ V where  toFun a := OAI.StronglyRationalVOA.mode A.fields a (-2) A.vacuum  map_add' a b := by simp [OAI.StronglyRationalVOA.mode]  map_smul' z a := by simp [OAI.StronglyRationalVOA.mode]noncomputable def c2 : Submodule ℂ V :=  Submodule.span ℂ {x | ∃ a b : V, x = OAI.StronglyRationalVOA.mode A.fields a (-2) b}noncomputable def C2Cofinite : Prop := FiniteDimensional ℂ (V ⧸ A.c2)noncomputable def IsIdeal (I : Submodule ℂ V) : Prop :=  (∀ a : V, ∀ n : ℤ, ∀ x ∈ I, OAI.StronglyRationalVOA.mode A.fields a n x ∈ I) ∧  ∀ x ∈ I, A.translation x ∈ Inoncomputable def IsSimple : Prop :=  A.vacuum ≠ 0 ∧ ∀ I : Submodule ℂ V, A.IsIdeal I → I = ⊥ ∨ I = ⊤end OAI.StronglyRationalVOA.VertexAlgebranamespace OAI.StronglyRationalVOAvariable {V : Type u} [AddCommGroup V] [Module ℂ V]noncomputable def ModuleJacobiIdentity {W : Type v} [AddCommGroup W] [Module ℂ W]    (A : OAI.StronglyRationalVOA.VertexAlgebra V) (Y : OAI.StronglyRationalVOA.StateField V W) : Prop :=  ∀ (a b : V) (c : W) (m n k : ℤ),    (∑ᶠ j : ℕ, Ring.choose (m : ℂ) j •      OAI.StronglyRationalVOA.mode Y (OAI.StronglyRationalVOA.mode A.fields a (n + j) b) (m + k - j) c) =    ∑ᶠ j : ℕ, ((-1 : ℂ) ^ j * Ring.choose (n : ℂ) j) •      (OAI.StronglyRationalVOA.mode Y a (m + n - j) (OAI.StronglyRationalVOA.mode Y b (k + j) c) -        (-1 : ℂ) ^ n • OAI.StronglyRationalVOA.mode Y b (n + k - j) (OAI.StronglyRationalVOA.mode Y a (m + j) c))structure WeakModule (A : OAI.StronglyRationalVOA.VertexAlgebra V) (W : Type v)    [AddCommGroup W] [Module ℂ W] where  fields : OAI.StronglyRationalVOA.StateField V W  vacuum_mode : ∀ n : ℤ, OAI.StronglyRationalVOA.mode fields A.vacuum n = if n = -1 then 1 else 0  jacobi : OAI.StronglyRationalVOA.ModuleJacobiIdentity A fieldsend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.WeakModulevariable {V : Type u} [AddCommGroup V] [Module ℂ V]variable {W : Type v} [AddCommGroup W] [Module ℂ W]    {A : VertexAlgebra V} (M : WeakModule A W)noncomputable def IsInvariant (I : Submodule ℂ W) : Prop :=  ∀ a : V, ∀ n : ℤ, ∀ x ∈ I, OAI.StronglyRationalVOA.mode M.fields a n x ∈ Inoncomputable def CompletelyReducible : Prop :=  ∀ I : Submodule ℂ W, M.IsInvariant I →    ∃ J : Submodule ℂ W, M.IsInvariant J ∧ IsCompl I Jend OAI.StronglyRationalVOA.WeakModulenamespace OAI.StronglyRationalVOAvariable {V : Type u} [AddCommGroup V] [Module ℂ V]structure CFTTypeVOA (V : Type u) [AddCommGroup V] [Module ℂ V]    extends OAI.StronglyRationalVOA.VertexAlgebra V where  conformalVector : V  centralCharge : ℂ  grade : ℕ → Submodule ℂ V  grading_internal : DirectSum.IsInternal grade  grade_finite : ∀ d, FiniteDimensional ℂ (grade d)  vacuum_ne_zero : vacuum ≠ 0  grade_zero : grade 0 = ℂ ∙ vacuum  conformal_mem : conformalVector ∈ grade 2  conformal_energy : ∀ d, ∀ a ∈ grade d,    OAI.StronglyRationalVOA.mode fields conformalVector 1 a = (d : ℂ) • a  conformal_translation : OAI.StronglyRationalVOA.mode fields conformalVector 0 = toVertexAlgebra.translation  translation_covariance : ∀ a : V, ∀ n : ℤ,    OAI.StronglyRationalVOA.mode fields (toVertexAlgebra.translation a) n =      (-(n : ℂ)) • OAI.StronglyRationalVOA.mode fields a (n - 1)  virasoro : ∀ m n : ℤ,    (OAI.StronglyRationalVOA.mode fields conformalVector (m + 1)).comp (OAI.StronglyRationalVOA.mode fields conformalVector (n + 1)) -      (OAI.StronglyRationalVOA.mode fields conformalVector (n + 1)).comp (OAI.StronglyRationalVOA.mode fields conformalVector (m + 1)) =    ((m - n : ℤ) : ℂ) • OAI.StronglyRationalVOA.mode fields conformalVector (m + n + 1) +      (if m + n = 0 then (centralCharge / 12) * ((m : ℂ)^3 - m) else 0) •        (1 : Module.End ℂ V)end OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.CFTTypeVOAvariable {V : Type u} [AddCommGroup V] [Module ℂ V]variable (A : CFTTypeVOA V)noncomputable def virasoroMode (m : ℤ) : Module.End ℂ V :=  OAI.StronglyRationalVOA.mode A.fields A.conformalVector (m + 1)noncomputable def physicalMode (a : V) (d : ℕ) (m : ℤ) : Module.End ℂ V :=  OAI.StronglyRationalVOA.mode A.fields a (m + d - 1)noncomputable def energyShift : Module.End ℂ V := 1 + A.virasoroMode 0noncomputable def gradingEquiv : V ≃ₗ[ℂ] DirectSum ℕ (fun d => A.grade d) :=  (LinearEquiv.ofBijective (DirectSum.coeLinearMap A.grade) A.grading_internal).symmnoncomputable def IsAdmissible {W : Type v} [AddCommGroup W] [Module ℂ W]    (M : OAI.StronglyRationalVOA.WeakModule A.toVertexAlgebra W) : Prop :=  ∃ G : ℤ → Submodule ℂ W,    DirectSum.IsInternal G ∧ (∀ k : ℤ, k < 0 → G k = ⊥) ∧      ∀ d : ℕ, ∀ a ∈ A.grade d, ∀ n k : ℤ, ∀ x ∈ G k,        OAI.StronglyRationalVOA.mode M.fields a n x ∈ G (k + d - n - 1)noncomputable def IsRational : Prop :=  ∀ (W : Type v) [AddCommGroup W] [Module ℂ W]    (M : OAI.StronglyRationalVOA.WeakModule A.toVertexAlgebra W),    A.IsAdmissible M → M.CompletelyReducibleend OAI.StronglyRationalVOA.CFTTypeVOAnamespace OAI.StronglyRationalVOA.CFTTypeVOAvariable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V]    (A : CFTTypeVOA V)noncomputable def PolynomialEnergyBound (a : V) : Prop :=  ∃ C : ℝ, 0 < C ∧ ∃ p k : ℕ, ∀ (n : ℤ) (b : V),    ‖OAI.StronglyRationalVOA.mode A.fields a n b‖ ≤ C * (1 + |(n : ℝ)|) ^ p * ‖(A.energyShift ^ k) b‖noncomputable def PolynomialEnergyBounds : Prop := ∀ a : V, A.PolynomialEnergyBound astructure UnitaryStructure where  pct : V →ₛₗ[starRingEnd ℂ] V  pct_involutive : Function.Involutive pct  pct_vacuum : pct A.vacuum = A.vacuum  pct_conformal : pct A.conformalVector = A.conformalVector  pct_modes : ∀ (a b : V) (n : ℤ),    pct (OAI.StronglyRationalVOA.mode A.fields a n b) = OAI.StronglyRationalVOA.mode A.fields (pct a) n (pct b)  vacuum_norm : ‖A.vacuum‖ = 1  invariant : ∀ d : ℕ, ∀ a ∈ A.grade d, ∀ n : ℤ, ∀ b c : V,    inner ℂ (OAI.StronglyRationalVOA.mode A.fields a n b) c =      inner ℂ b (((-1 : ℂ) ^ d) •        ∑ j ∈ Finset.range (d + 1), ((j.factorial : ℂ)⁻¹) •          OAI.StronglyRationalVOA.mode A.fields ((A.virasoroMode 1 ^ j) (pct a))            (2 * (d : ℤ) - j - n - 2) c)end OAI.StronglyRationalVOA.CFTTypeVOAnamespace OAI.StronglyRationalVOA.HilbertCoreopen Filteropen UniformSpacevariable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℂ V] :    Submodule ℂ (Completion V) :=  LinearMap.range (Completion.toComplₗᵢ : V →ₗᵢ[ℂ] Completion V).toLinearMapnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.equiv (V : Type*) [NormedAddCommGroup V] [InnerProductSpace ℂ V] :    V ≃ₗ[ℂ] (OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space V) :=  LinearEquiv.ofInjective (Completion.toComplₗᵢ : V →ₗᵢ[ℂ] Completion V).toLinearMap    (Completion.toComplₗᵢ : V →ₗᵢ[ℂ] Completion V).injectivenoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.operator (T : V →ₗ[ℂ] Completion V) : Completion V →ₗ.[ℂ] Completion V where  domain := (OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.space V)  toFun := T.comp (OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.equiv V).symm.toLinearMapend OAI.StronglyRationalVOA.HilbertCorenamespace OAI.StronglyRationalVOAopen Filternoncomputable def RapidCoefficients (f : ℤ → ℂ) : Prop :=  ∀ p : ℕ, Summable (fun n : ℤ => ‖f n‖*(1+|(n : ℝ)|)^p)end OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.SummableLinearFamilyopen Filtervariable {ι V H : Type*} [NormedAddCommGroup V] [NormedSpace ℂ V]    [NormedAddCommGroup H] [NormedSpace ℂ H]noncomputable def tsumMap (T : ι → V →ₗ[ℂ] H) (hT : ∀ v, Summable (fun n => T n v)) : V →ₗ[ℂ] H where  toFun v := ∑' n, T n v  map_add' v w := by simpa only [map_add] using (hT v).tsum_add (hT w)  map_smul' z v := by    simpa only [map_smul, RingHom.id_apply] using (hT v).tsum_const_smul zend OAI.StronglyRationalVOA.SummableLinearFamilynamespace OAI.StronglyRationalVOAopen Filteropen scoped ContDiffstructure SmoothCircleFunction where  toFun : ℝ → ℂ  periodic : Function.Periodic toFun (2*Real.pi)  smooth : ContDiff ℝ ∞ toFunend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.SmoothCircleFunctionopen Filteropen scoped ContDiffnoncomputable instance : CoeFun OAI.StronglyRationalVOA.SmoothCircleFunction (fun _ => ℝ → ℂ) := ⟨OAI.StronglyRationalVOA.SmoothCircleFunction.toFun⟩noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.coefficient (f : OAI.StronglyRationalVOA.SmoothCircleFunction) (n : ℤ) : ℂ := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleFunction_period_pos  : 0 < 2*Real.pi := by positivity  exact    fourierCoeffOn h_OAI_StronglyRationalVOA_SmoothCircleFunction_period_pos f nend OAI.StronglyRationalVOA.SmoothCircleFunctionnamespace OAI.StronglyRationalVOA.ClosedGraphDataopen Filteropen scoped ContDiffvariable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]noncomputable abbrev _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double (H : Type u) := WithLp 2 (H × H)noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.graph (T : H →ₗ.[ℂ] H) : Submodule ℂ (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H) :=  T.graph.comap (WithLp.prodContinuousLinearEquiv 2 ℂ H H).toLinearEquiv.toLinearMapnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.projection (T : H →ₗ.[ℂ] H) (hT : T.IsClosed) : (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H) →L[ℂ] (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H) := by  classical  have h_OAI_StronglyRationalVOA_ClosedGraphData_graph_closed {H : Type u} [instLocal1 : NormedAddCommGroup H] [instLocal2 : InnerProductSpace ℂ H]  {T : H →ₗ.[ℂ] H} (hT : T.IsClosed) :      IsClosed ((OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.graph T) : Set (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H)) :=    hT.preimage (WithLp.prodContinuousLinearEquiv 2 ℂ H H).continuous  letI : IsClosed ((OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.graph T) : Set (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H)) := (h_OAI_StronglyRationalVOA_ClosedGraphData_graph_closed hT)  exact (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.graph T).starProjectionnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.inclusion (i : Bool) : H →L[ℂ] (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H) :=  (WithLp.prodContinuousLinearEquiv 2 ℂ H H).symm.toContinuousLinearMap.comp    (if i then ContinuousLinearMap.inr ℂ H H else ContinuousLinearMap.inl ℂ H H)noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.coordinate (i : Bool) : (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.Double H) →L[ℂ] H :=  (if i then ContinuousLinearMap.snd ℂ H H else ContinuousLinearMap.fst ℂ H H).comp    (WithLp.prodContinuousLinearEquiv 2 ℂ H H).toContinuousLinearMapnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.entry (T : H →ₗ.[ℂ] H) (hT : T.IsClosed) (i j : Bool) : H →L[ℂ] H :=  (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.coordinate i).comp ((OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.projection T hT).comp (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.inclusion j))end OAI.StronglyRationalVOA.ClosedGraphDatanamespace OAI.StronglyRationalVOA.LocalOperatorAlgebraopen Filteropen scoped ContDiffvariable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]open scoped Pointwisenoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.LocalOperatorAlgebra.generated (s : Set (H →L[ℂ] H)) : VonNeumannAlgebra H where  toStarSubalgebra := StarSubalgebra.centralizer ℂ (StarSubalgebra.centralizer ℂ s : Set (H →L[ℂ] H))  centralizer_centralizer' := by    change Set.centralizer (Set.centralizer      (StarSubalgebra.centralizer ℂ (StarSubalgebra.centralizer ℂ s : Set (H →L[ℂ] H)) : Set (H →L[ℂ] H))) =        (StarSubalgebra.centralizer ℂ (StarSubalgebra.centralizer ℂ s : Set (H →L[ℂ] H)) : Set (H →L[ℂ] H))    rw [StarSubalgebra.coe_centralizer_centralizer]    rw [Set.centralizer_centralizer_centralizer]end OAI.StronglyRationalVOA.LocalOperatorAlgebranamespace OAI.StronglyRationalVOA.SmoothCircleFunctionopen Filteropen scoped ContDiffnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.onCircle (f : OAI.StronglyRationalVOA.SmoothCircleFunction) : AddCircle (2*Real.pi) → ℂ :=  f.periodic.liftend OAI.StronglyRationalVOA.SmoothCircleFunctionnamespace OAI.StronglyRationalVOAopen Filteropen scoped ContDiffstructure ProperCircleArc where  left : ℝ  right : ℝ  nonempty' : left < right  nondense' : right < left + 2*Real.piend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.ProperCircleArcopen Filteropen scoped ContDiffnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier (I : OAI.StronglyRationalVOA.ProperCircleArc) : Set (AddCircle (2*Real.pi)) :=  (fun t : ℝ => (t : AddCircle (2*Real.pi))) '' Set.Ioo I.left I.rightnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.complement (I : OAI.StronglyRationalVOA.ProperCircleArc) : OAI.StronglyRationalVOA.ProperCircleArc where  left := I.right  right := I.left + 2*Real.pi  nonempty' := I.nondense'  nondense' := by linarith [I.nonempty']end OAI.StronglyRationalVOA.ProperCircleArcnamespace OAI.StronglyRationalVOA.BoundedFlowopen scoped Topologyopen Filteropen scoped Topologyopen Filteropen scoped Topologyvariable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]local instance _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.BoundedFlow.boundedFlowRationalNormedAlgebra : NormedAlgebra ℚ (H →L[ℂ] H) :=  .restrictScalars ℚ ℂ (H →L[ℂ] H)noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.BoundedFlow.flow (K : H →L[ℂ] H) (t : ℝ) : H →L[ℂ] H := NormedSpace.exp (t • K)end OAI.StronglyRationalVOA.BoundedFlownamespace OAI.StronglyRationalVOAopen scoped ContDiffstructure SmoothCircleLift where  toOrderIso : ℝ ≃o ℝ  smooth : ContDiff ℝ ∞ toOrderIso  inverse_smooth : ContDiff ℝ ∞ toOrderIso.symm  period : ∀ t, toOrderIso (t+2*Real.pi)=toOrderIso t+2*Real.piend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.SmoothCircleLiftopen scoped ContDiffnoncomputable instance : CoeFun OAI.StronglyRationalVOA.SmoothCircleLift (fun _ => ℝ → ℝ) := ⟨fun F => F.toOrderIso⟩noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity : OAI.StronglyRationalVOA.SmoothCircleLift where  toOrderIso := OrderIso.refl ℝ  smooth := contDiff_id  inverse_smooth := contDiff_id  period := fun _ => rflnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose (F G : OAI.StronglyRationalVOA.SmoothCircleLift) : OAI.StronglyRationalVOA.SmoothCircleLift where  toOrderIso := G.toOrderIso.trans F.toOrderIso  smooth := F.smooth.comp G.smooth  inverse_smooth := G.inverse_smooth.comp F.inverse_smooth  period := by intro t; change F (G (t+2*Real.pi))=F (G t)+2*Real.pi; rw [G.period,F.period]noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.inverse (F : OAI.StronglyRationalVOA.SmoothCircleLift) : OAI.StronglyRationalVOA.SmoothCircleLift where  toOrderIso := F.toOrderIso.symm  smooth := F.inverse_smooth  inverse_smooth := F.smooth  period := by    intro t    apply F.toOrderIso.injective    rw [F.toOrderIso.apply_symm_apply,F.period,F.toOrderIso.apply_symm_apply]noncomputable instance _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.instGroup : Group OAI.StronglyRationalVOA.SmoothCircleLift := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleLift_ext  {F G : OAI.StronglyRationalVOA.SmoothCircleLift} (h : ∀ t, F t=G t) : F=G := by    cases F with    | mk f hf hfi hp =>      cases G with      | mk g hg hgi hgp =>        have he : f=g := DFunLike.ext _ _ h        subst g        rfl  exact {    mul := OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose    one := OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity    inv := OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.inverse    npow := @npowRec OAI.StronglyRationalVOA.SmoothCircleLift      ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity⟩      ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose⟩    div := fun F G => OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose F      (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.inverse G)    zpow := @zpowRec OAI.StronglyRationalVOA.SmoothCircleLift      ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity⟩      ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose⟩      ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.inverse⟩      (@npowRec OAI.StronglyRationalVOA.SmoothCircleLift        ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.identity⟩        ⟨OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.compose⟩)    mul_assoc F G H := by apply h_OAI_StronglyRationalVOA_SmoothCircleLift_ext; intro t; rfl    one_mul F := by apply h_OAI_StronglyRationalVOA_SmoothCircleLift_ext; intro t; rfl    mul_one F := by apply h_OAI_StronglyRationalVOA_SmoothCircleLift_ext; intro t; rfl    inv_mul_cancel F := by apply h_OAI_StronglyRationalVOA_SmoothCircleLift_ext; intro t; exact F.toOrderIso.symm_apply_apply t  }noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle (F : OAI.StronglyRationalVOA.SmoothCircleLift) : AddCircle (2*Real.pi) → AddCircle (2*Real.pi) := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleLift_one_apply  (t : ℝ) : (1 : OAI.StronglyRationalVOA.SmoothCircleLift) t=t := rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_mul_apply  (F G : OAI.StronglyRationalVOA.SmoothCircleLift) (t : ℝ) : (F*G) t=F (G t) := rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_circle_periodic  (F : OAI.StronglyRationalVOA.SmoothCircleLift) : Function.Periodic (fun t : ℝ => (F t : AddCircle (2*Real.pi))) (2*Real.pi) := by    intro t    change ((F.toOrderIso (t+2*Real.pi) : ℝ) : AddCircle (2*Real.pi)) =      (F.toOrderIso t : AddCircle (2*Real.pi))    rw [F.period,AddCircle.coe_add]    simp  exact    (h_OAI_StronglyRationalVOA_SmoothCircleLift_circle_periodic F).liftnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleHomeomorph (F : OAI.StronglyRationalVOA.SmoothCircleLift) :    AddCircle (2*Real.pi) ≃ₜ AddCircle (2*Real.pi) := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleLift_one_apply  (t : ℝ) : (1 : OAI.StronglyRationalVOA.SmoothCircleLift) t=t := rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_one  (t : AddCircle (2*Real.pi)) : (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle 1 t)=t := by    induction t using QuotientAddGroup.induction_on with    | H t => rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_mul  (F G : OAI.StronglyRationalVOA.SmoothCircleLift) (t : AddCircle (2*Real.pi)) :      (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle (F * G) t)=(OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle G t)) := by    induction t using QuotientAddGroup.induction_on with    | H t => rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_inverse  (F : OAI.StronglyRationalVOA.SmoothCircleLift) (t : AddCircle (2*Real.pi)) : (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F⁻¹ (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F t))=t := by    rw [← h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_mul,inv_mul_cancel,h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_one]  have h_OAI_StronglyRationalVOA_SmoothCircleLift_continuous_onCircle  (F : OAI.StronglyRationalVOA.SmoothCircleLift) : Continuous (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F) := by    exact ((AddCircle.continuous_mk' (2*Real.pi)).comp F.smooth.continuous).quotient_liftOn' _  have h_OAI_StronglyRationalVOA_SmoothCircleLift_mul_apply  (F G : OAI.StronglyRationalVOA.SmoothCircleLift) (t : ℝ) : (F*G) t=F (G t) := rfl  exact {    toFun := (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F)    invFun := (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F⁻¹)    left_inv := (h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_inverse F)    right_inv := by intro t; simpa [h_OAI_StronglyRationalVOA_SmoothCircleLift_one_apply, h_OAI_StronglyRationalVOA_SmoothCircleLift_mul_apply] using (h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_inverse F⁻¹ t)    continuous_toFun := (h_OAI_StronglyRationalVOA_SmoothCircleLift_continuous_onCircle F)    continuous_invFun := (h_OAI_StronglyRationalVOA_SmoothCircleLift_continuous_onCircle F⁻¹)  }noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction : OAI.StronglyRationalVOA.SmoothCircleLift →* Equiv.Perm (AddCircle (2*Real.pi)) := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_one  (t : AddCircle (2*Real.pi)) : (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle 1 t)=t := by    induction t using QuotientAddGroup.induction_on with    | H t => rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_mul  (F G : OAI.StronglyRationalVOA.SmoothCircleLift) (t : AddCircle (2*Real.pi)) :      (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle (F * G) t)=(OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle F (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.onCircle G t)) := by    induction t using QuotientAddGroup.induction_on with    | H t => rfl  exact {    toFun F := (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleHomeomorph F).toEquiv    map_one' := by ext x; exact (h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_one x)    map_mul' F G := by ext x; exact (h_OAI_StronglyRationalVOA_SmoothCircleLift_onCircle_mul F G x)  }end OAI.StronglyRationalVOA.SmoothCircleLiftnamespace OAI.StronglyRationalVOAopen scoped ContDiffnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism := OAI.StronglyRationalVOA.SmoothCircleLift ⧸ (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).kernoncomputable instance _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.instGroupSmoothCircleDiffeomorphism : Group OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism := inferInstanceAs  (Group (OAI.StronglyRationalVOA.SmoothCircleLift ⧸ (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).ker))end OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOAopen UniformSpacenoncomputable def scalarPhaseSubgroup (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] :    Subgroup (H ≃ₗᵢ[ℂ] H) where  carrier := {E | ∃ c : ℂ, ‖c‖=1 ∧ ∀ x : H, E x=c • x}  one_mem' := ⟨1,by simp,fun x => (one_smul ℂ x).symm⟩  mul_mem' := by    rintro E F ⟨c,hc,he⟩ ⟨d,hd,hf⟩    refine ⟨c*d,by rw [norm_mul,hc,hd,one_mul],?_⟩    intro x    change E (F x)=(c*d) • x    rw [hf,he,mul_smul]  inv_mem' := by    rintro E ⟨c,hc,he⟩    have hn : c ≠ 0 := by intro h; rw [h,norm_zero] at hc; norm_num at hc    refine ⟨c⁻¹,by rw [norm_inv,hc,inv_one],?_⟩    intro x    apply E.injective    change E (E.symm x)=E (c⁻¹ • x)    rw [E.apply_symm_apply,map_smul,he,smul_smul,inv_mul_cancel₀ hn,one_smul]noncomputable instance scalarPhaseSubgroup_normal (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] :    (OAI.StronglyRationalVOA.scalarPhaseSubgroup H).Normal where  conj_mem := by    rintro E ⟨c,hc,he⟩ F    refine ⟨c,hc,?_⟩    intro x    change F (E (F.symm x))=c • x    rw [he,map_smul,F.apply_symm_apply]noncomputable abbrev ProjectiveUnitaryGroup (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] :=  (H ≃ₗᵢ[ℂ] H) ⧸ OAI.StronglyRationalVOA.scalarPhaseSubgroup Hend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.SmoothCircleLiftopen Filter Setopen scoped Topology ContDiffnoncomputable def jet (F : OAI.StronglyRationalVOA.SmoothCircleLift) (k : ℕ) : C(ℝ,ℝ) :=  ⟨iteratedDeriv k F, F.smooth.continuous_iteratedDeriv k    (by exact_mod_cast (le_top : (k : ℕ∞) ≤ ⊤))⟩noncomputable instance : TopologicalSpace OAI.StronglyRationalVOA.SmoothCircleLift :=  TopologicalSpace.induced (fun F => OAI.StronglyRationalVOA.SmoothCircleLift.jet F) inferInstanceend OAI.StronglyRationalVOA.SmoothCircleLiftnamespace OAI.StronglyRationalVOAopen UniformSpace Filter Setopen scoped Topologynoncomputable instance unitaryStrongTopology (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] :    TopologicalSpace (H ≃ₗᵢ[ℂ] H) :=  TopologicalSpace.induced (fun E : H ≃ₗᵢ[ℂ] H => (E : H → H)) inferInstancenoncomputable instance _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.instTopologicalSpaceSmoothCircleDiffeomorphism : TopologicalSpace OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism := inferInstanceAs  (TopologicalSpace (OAI.StronglyRationalVOA.SmoothCircleLift ⧸ (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).ker))end OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.CircleMobiusGeometryopen Setopen scoped MatrixGroupsnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel (M : SL(2,ℝ)) (x y : ℝ) : Prop :=  (M 0 0*Real.cos (x/2)+M 0 1*Real.sin (x/2))*Real.sin (y/2)=    (M 1 0*Real.cos (x/2)+M 1 1*Real.sin (x/2))*Real.cos (y/2)noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements (M : SL(2,ℝ)) (F : OAI.StronglyRationalVOA.SmoothCircleLift) : Prop := ∀ x, (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel M x ((OAI.StronglyRationalVOA.SmoothCircleLift.toOrderIso F) x))noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts : Subgroup OAI.StronglyRationalVOA.SmoothCircleLift := by  classical  have h_OAI_StronglyRationalVOA_SmoothCircleLift_one_apply  (t : ℝ) : (1 : OAI.StronglyRationalVOA.SmoothCircleLift) t=t := rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_mul_apply  (F G : OAI.StronglyRationalVOA.SmoothCircleLift) (t : ℝ) : (F*G) t=F (G t) := rfl  have h_OAI_StronglyRationalVOA_SmoothCircleLift_apply_inv_apply  (F : OAI.StronglyRationalVOA.SmoothCircleLift) (t : ℝ) : F (F⁻¹ t)=t := F.toOrderIso.apply_symm_apply t  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_inv  {M : SL(2,ℝ)} {F : OAI.StronglyRationalVOA.SmoothCircleLift}      (hF : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements M F)) : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements M⁻¹ F⁻¹) := by    intro x    have h := hF (F⁻¹ x)    rw [OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel,(h_OAI_StronglyRationalVOA_SmoothCircleLift_apply_inv_apply F)] at h    simp only [OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel,Matrix.SpecialLinearGroup.SL2_inv_expl,Matrix.cons_val_zero,      Matrix.cons_val_one,Matrix.cons_val_fin_one]    linear_combination -h  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_one  : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements 1 1) := by    intro x    simp [h_OAI_StronglyRationalVOA_SmoothCircleLift_one_apply, OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel,mul_comm]  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_collinear_unit  {p q c s : ℝ} (hu : c^2+s^2=1) (h : p*s=q*c) :      (p*c+q*s)*c=p ∧ (p*c+q*s)*s=q := by    constructor    · linear_combination p*hu-s*h    · linear_combination q*hu+c*h  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_cos_sq_add_sin_sq  (x : ℝ) : Real.cos x^2+Real.sin x^2=1 := by    nlinarith [Real.sin_sq_add_cos_sq x]  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_mul  {M N : SL(2,ℝ)} {F G : OAI.StronglyRationalVOA.SmoothCircleLift}      (hF : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements M F)) (hG : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements N G)) : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements (M * N) (F * G)) := by    intro x    have hh := hF (G x)    have hg := hG x    obtain ⟨hr1,hr2⟩ := (h_OAI_StronglyRationalVOA_CircleMobiusGeometry_collinear_unit    (h_OAI_StronglyRationalVOA_CircleMobiusGeometry_cos_sq_add_sin_sq      ((OAI.StronglyRationalVOA.SmoothCircleLift.toOrderIso G) x / 2))    hg)    let r := (N 0 0*Real.cos (x/2)+N 0 1*Real.sin (x/2))*Real.cos (G x/2)+      (N 1 0*Real.cos (x/2)+N 1 1*Real.sin (x/2))*Real.sin (G x/2)    change r*Real.cos (G x/2)=N 0 0*Real.cos (x/2)+N 0 1*Real.sin (x/2) at hr1    change r*Real.sin (G x/2)=N 1 0*Real.cos (x/2)+N 1 1*Real.sin (x/2) at hr2    change (M 0 0*Real.cos (G x/2)+M 0 1*Real.sin (G x/2))*Real.sin (F (G x)/2)=      (M 1 0*Real.cos (G x/2)+M 1 1*Real.sin (G x/2))*Real.cos (F (G x)/2) at hh    simp only [OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Rel,(h_OAI_StronglyRationalVOA_SmoothCircleLift_mul_apply),Matrix.SpecialLinearGroup.coe_mul,      Matrix.mul_apply,Fin.sum_univ_two]    linear_combination r*hh+(M 1 0*Real.cos (F (G x)/2)-M 0 0*Real.sin (F (G x)/2))*hr1+      (M 1 1*Real.cos (F (G x)/2)-M 0 1*Real.sin (F (G x)/2))*hr2  exact {    carrier := {F | ∃ M : SL(2,ℝ), (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements M F)}    one_mem' := ⟨1,h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_one⟩    mul_mem' := by rintro F G ⟨M,hM⟩ ⟨N,hN⟩; exact ⟨M*N,(h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_mul hM hN)⟩    inv_mem' := by rintro F ⟨M,hM⟩; exact ⟨M⁻¹,(h_OAI_StronglyRationalVOA_CircleMobiusGeometry_implements_inv hM)⟩  }noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.rotationMatrix (s : ℝ) : SL(2,ℝ) := by  classical  have h_OAI_StronglyRationalVOA_CircleMobiusGeometry_cos_sq_add_sin_sq  (x : ℝ) : Real.cos x^2+Real.sin x^2=1 := by    nlinarith [Real.sin_sq_add_cos_sq x]  exact    ⟨!![Real.cos (s/2),-Real.sin (s/2);Real.sin (s/2),Real.cos (s/2)],by        simp only [Matrix.det_fin_two_of]        nlinarith [(h_OAI_StronglyRationalVOA_CircleMobiusGeometry_cos_sq_add_sin_sq (s / 2))]⟩noncomputable abbrev _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Group := OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts ⧸ ((OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).comp OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts.subtype).kernoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.inclusion : OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Group →* OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism :=  QuotientGroup.lift ((OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).comp OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts.subtype).ker    ((QuotientGroup.mk' (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).ker).comp OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts.subtype) (by      intro F hF      exact (QuotientGroup.eq_one_iff _).mpr hF)end OAI.StronglyRationalVOA.CircleMobiusGeometrynamespace OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphismopen Setopen scoped Topology MatrixGroupsnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism.action : OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism →* Equiv.Perm (AddCircle (2*Real.pi)) :=  QuotientGroup.lift (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction).ker (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleLift.circleAction)    (fun _ h => h)end OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphismnamespace OAI.StronglyRationalVOAopen Setopen scoped Topology MatrixGroupsnoncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.projectiveConjugation {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]    [CompleteSpace H] : OAI.StronglyRationalVOA.ProjectiveUnitaryGroup H → ((H →L[ℂ] H) ≃⋆ₐ[ℂ] (H →L[ℂ] H)) := by  classical  have h_OAI_StronglyRationalVOA_projective_equality_conjugation  {H : Type _} [NormedAddCommGroup H]      [InnerProductSpace ℂ H] [CompleteSpace H] (E F : H ≃ₗᵢ[ℂ] H)      (h : (QuotientGroup.mk E : OAI.StronglyRationalVOA.ProjectiveUnitaryGroup H)=QuotientGroup.mk F) :      E.conjStarAlgEquiv=F.conjStarAlgEquiv := by    obtain ⟨c,_,hc⟩ := QuotientGroup.eq.mp h    have he (x : H) : F x=c • E x := by      have H := congrArg E (hc x)      change E (E.symm (F x))=E (c • x) at H      simpa only [E.apply_symm_apply,map_smul] using H    ext B x    change E (B (E.symm x))=F (B (F.symm x))    have hi : E.symm x=c • F.symm x := by      apply E.injective      rw [E.apply_symm_apply,map_smul,← he,F.apply_symm_apply]    rw [hi,map_smul,map_smul,← he]  exact    Quotient.lift (fun E : H ≃ₗᵢ[ℂ] H => E.conjStarAlgEquiv) (by        intro E F h        exact (h_OAI_StronglyRationalVOA_projective_equality_conjugation E F (Quotient.sound h)))noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.globalObservableAlgebra {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]    [CompleteSpace H] (N : OAI.StronglyRationalVOA.ProperCircleArc → VonNeumannAlgebra H) :    Subalgebra ℂ (H →L[ℂ] H) :=  Algebra.adjoin ℂ (⋃ I, (N I : Set (H →L[ℂ] H)))noncomputable def _root_.OAI.MinimalVertex.Code.StronglyRationalVOA.globalCyclicSpace {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]    [CompleteSpace H] (N : OAI.StronglyRationalVOA.ProperCircleArc → VonNeumannAlgebra H) (Ω : H) : Submodule ℂ H :=  (Submodule.span ℂ {x | ∃ B ∈ (OAI.MinimalVertex.Code.StronglyRationalVOA.globalObservableAlgebra N), x=B Ω}).topologicalClosureend OAI.StronglyRationalVOAnamespace OAI.StronglyRationalVOA.CFTTypeVOAvariable {V : Type u} [AddCommGroup V] [Module ℂ V] (A : CFTTypeVOA V)noncomputable abbrev GradedDual := DirectSum ℕ (fun d => Module.Dual ℂ (A.grade d))noncomputable def gradedDualPairing (φ : A.GradedDual) (b : V) : ℂ := by  classical  exact φ.sum (fun d f => f (A.gradingEquiv b d))noncomputable def IsSelfContragredient : Prop :=  ∃ e : V ≃ₗ[ℂ] A.GradedDual,    ∀ d : ℕ, ∀ a ∈ A.grade d, ∀ n : ℤ, ∀ b c : V,      A.gradedDualPairing (e (OAI.StronglyRationalVOA.mode A.fields a n b)) c =        ((-1 : ℂ)^d) * ∑ j ∈ Finset.range (d+1), ((j.factorial : ℂ)⁻¹) *          A.gradedDualPairing (e b)            (OAI.StronglyRationalVOA.mode A.fields ((A.virasoroMode 1 ^ j) a) (2*(d:ℤ)-j-n-2) c)noncomputable def IsStronglyRational : Prop :=  A.IsSelfContragredient ∧ A.IsRational.{u,v} ∧ A.toVertexAlgebra.C2Cofiniteend OAI.StronglyRationalVOA.CFTTypeVOAnamespace OAI.MinimalVertexopen Filter Set UniformSpaceopen scoped Topology MatrixGroupsopen StronglyRationalVOAvariable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V]  {A : CFTTypeVOA V}noncomputable def smearedMap (A : OAI.StronglyRationalVOA.CFTTypeVOA V) (a : V) (d : ℕ) (_ha : A.PolynomialEnergyBound a)    (f : ℤ → ℂ) (_hf : OAI.StronglyRationalVOA.RapidCoefficients f) : V →ₗ[ℂ] Completion V := by  classical  let family : ℤ → (V →ₗ[ℂ] Completion V) := fun m =>    f m • (Completion.toComplₗᵢ : V →ₗᵢ[ℂ] Completion V).toLinearMap.comp      (A.physicalMode a d m)  exact if h : ∀ v, Summable (fun m => family m v) then    SummableLinearFamily.tsumMap family h  else 0noncomputable def smoothSmearedField (_U : A.UnitaryStructure) (_hc : A.toVertexAlgebra.C2Cofinite)    (a : V) (d : ℕ) (f : OAI.StronglyRationalVOA.SmoothCircleFunction) : Completion V →ₗ.[ℂ] Completion V := by  classical  exact if h : A.PolynomialEnergyBounds ∧ OAI.StronglyRationalVOA.RapidCoefficients (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.coefficient f) then    (OAI.MinimalVertex.Code.StronglyRationalVOA.HilbertCore.operator  (OAI.MinimalVertex.smearedMap A a d (And.left h a) (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.coefficient f)    (And.right h)))  else 0noncomputable def closedSmoothField (U : A.UnitaryStructure) (hc : A.toVertexAlgebra.C2Cofinite)    (a : V) (d : ℕ) (f : OAI.StronglyRationalVOA.SmoothCircleFunction) : Completion V →ₗ.[ℂ] Completion V :=  (OAI.MinimalVertex.smoothSmearedField U hc a d f).closurenoncomputable def localGraphData (U : A.UnitaryStructure) (hc : A.toVertexAlgebra.C2Cofinite)    (O : Set (AddCircle (2*Real.pi))) : Set (Completion V →L[ℂ] Completion V) :=  {x | ∃ (a : V) (d : ℕ), a ∈ A.grade d ∧ ∃ (f : OAI.StronglyRationalVOA.SmoothCircleFunction),      tsupport (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleFunction.onCircle f) ⊆ O ∧ ∃ (h : (OAI.MinimalVertex.closedSmoothField U hc a d f).IsClosed),        ∃ i j : Bool, x = (OAI.MinimalVertex.Code.StronglyRationalVOA.ClosedGraphData.entry (OAI.MinimalVertex.closedSmoothField U hc a d f) h i j)}noncomputable def localAlgebra (U : A.UnitaryStructure) (hc : A.toVertexAlgebra.C2Cofinite)    (O : Set (AddCircle (2*Real.pi))) : VonNeumannAlgebra (Completion V) :=  (OAI.MinimalVertex.Code.StronglyRationalVOA.LocalOperatorAlgebra.generated (OAI.MinimalVertex.localGraphData U hc O))noncomputable def intervalAlgebra (U : A.UnitaryStructure) (hc : A.toVertexAlgebra.C2Cofinite)    (I : OAI.StronglyRationalVOA.ProperCircleArc) : VonNeumannAlgebra (Completion V) :=  OAI.MinimalVertex.localAlgebra U hc (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I)noncomputable def CKLWStrongLocal (U : A.UnitaryStructure) (hc : A.toVertexAlgebra.C2Cofinite) : Prop :=  (∀ a : V, A.PolynomialEnergyBound a) ∧    ∀ I : OAI.StronglyRationalVOA.ProperCircleArc, OAI.MinimalVertex.intervalAlgebra U hc I ≤      (OAI.MinimalVertex.intervalAlgebra U hc (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.complement I)).commutantend OAI.MinimalVertexnamespace OAI.MinimalVertexopen Filter Set UniformSpaceopen scoped Topology MatrixGroupsopen StronglyRationalVOAvariable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]noncomputable def resolvent (T : H →ₗ.[ℂ] H) (_hs : IsSelfAdjoint T) (z : ℂ) (_hz : 1 ≤ |z.im|) :    H →L[ℂ] H := by  classical  exact if h : ∃ R : H →L[ℂ] H, ∀ y, (R y, y + z • R y) ∈ T.graph then h.choose  else 0noncomputable def boundedGenerator (T : H →ₗ.[ℂ] H) (hs : IsSelfAdjoint T)    (r : ℝ) (hr : 1 ≤ r) : H →L[ℂ] H :=  ((r : ℂ)^2/2) •    (OAI.MinimalVertex.resolvent T hs ((r : ℂ)*Complex.I) (by simpa [abs_of_nonneg (by linarith : 0 ≤ r)] using hr) +     OAI.MinimalVertex.resolvent T hs (-((r : ℂ)*Complex.I)) (by simpa [abs_of_nonneg (by linarith : 0 ≤ r)] using hr))noncomputable def approximatingFlow (T : H →ₗ.[ℂ] H) (hs : IsSelfAdjoint T) (n : ℕ) (t : ℝ) : H →L[ℂ] H :=  (OAI.MinimalVertex.Code.StronglyRationalVOA.BoundedFlow.flow  (Complex.I • OAI.MinimalVertex.boundedGenerator T hs (↑n + 1) (le_add_of_nonneg_left (Nat.cast_nonneg n))) t)end OAI.MinimalVertexnamespace OAI.MinimalVertexopen Filter Set UniformSpaceopen scoped Topology MatrixGroupsopen StronglyRationalVOAnoncomputable def flow {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]    (T : H →ₗ.[ℂ] H) (hs : IsSelfAdjoint T) (t : ℝ) : H →L[ℂ] H := by  classical  exact if h : ∃ L : H →L[ℂ] H, ∀ x,      Tendsto (fun n => OAI.MinimalVertex.approximatingFlow T hs n t x) atTop (𝓝 (L x)) then    h.choose  else 0noncomputable def projectiveStandardAction : PSL(2,ℝ) →* (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Group) := by  classical  exact if h : ∃ L : PSL(2,ℝ) →* (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Group),      ∀ M : SL(2,ℝ), ∃ F : OAI.StronglyRationalVOA.SmoothCircleLift, ∃ hF : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.Implements M F),        L (QuotientGroup.mk M) =          QuotientGroup.mk (⟨F, M, hF⟩ : (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.lifts)) then h.choose  else 1structure IrreducibleConformalNetStructure {H : Type*} [NormedAddCommGroup H]    [InnerProductSpace ℂ H] [CompleteSpace H]    (N : OAI.StronglyRationalVOA.ProperCircleArc → VonNeumannAlgebra H) where  separable : TopologicalSpace.SeparableSpace H  carrier_congr : ∀ I J, (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I)=(OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier J) → N I=N J  isotony : ∀ I J, (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I) ⊆ (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier J) → N I ≤ N J  locality : ∀ I J, Disjoint (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I) (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier J) → N I ≤ (N J).commutant  mobius : PSL(2,ℝ) →* (H ≃ₗᵢ[ℂ] H)  mobius_continuous : Continuous mobius  diffeomorphism : OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism →* OAI.StronglyRationalVOA.ProjectiveUnitaryGroup H  diffeomorphism_continuous : Continuous diffeomorphism  extends_mobius : ∀ F, diffeomorphism ((OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.inclusion) (OAI.MinimalVertex.projectiveStandardAction F))=QuotientGroup.mk (mobius F)  covariance : ∀ F I J, (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier J)=(OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism.action) F '' (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I) →    ∀ B : H →L[ℂ] H, OAI.MinimalVertex.Code.StronglyRationalVOA.projectiveConjugation (diffeomorphism F) B ∈ N J ↔ B ∈ N I  local_action : ∀ F I, (∀ x ∈ (OAI.MinimalVertex.Code.StronglyRationalVOA.ProperCircleArc.carrier I), (OAI.MinimalVertex.Code.StronglyRationalVOA.SmoothCircleDiffeomorphism.action) F x=x) →    ∀ B ∈ N I, OAI.MinimalVertex.Code.StronglyRationalVOA.projectiveConjugation (diffeomorphism F) B=B  vacuum : H  vacuum_norm : ‖vacuum‖=1  vacuum_invariant : ∀ F, mobius F vacuum=vacuum  vacuum_unique : ∀ x : H, (∀ F, mobius F x=x) → ∃ c : ℂ, x=c • vacuum  vacuum_cyclic : (OAI.MinimalVertex.Code.StronglyRationalVOA.globalCyclicSpace N vacuum)=⊤  hamiltonian : H →ₗ.[ℂ] H  hamiltonian_selfAdjoint : IsSelfAdjoint hamiltonian  positive_energy : ∀ x y, (x,y) ∈ hamiltonian.graph → 0 ≤ (inner ℂ x y).re  rotation_flow : ∀ t : ℝ,    (mobius (QuotientGroup.mk (OAI.MinimalVertex.Code.StronglyRationalVOA.CircleMobiusGeometry.rotationMatrix t))).toLinearIsometry.toContinuousLinearMap=      OAI.MinimalVertex.flow hamiltonian hamiltonian_selfAdjoint t  irreducible : ∀ Q : H →L[ℂ] H, (∀ I, Q ∈ (N I).commutant) →    ∃ c : ℂ, Q=c • (1 : H →L[ℂ] H)end OAI.MinimalVertexnamespace OAI.MinimalVertexopen Filter Set UniformSpaceopen scoped Topology MatrixGroupsopen StronglyRationalVOAvariable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℂ V]  {A : CFTTypeVOA V} (U : A.UnitaryStructure)theorem main (_hSimple : A.toVertexAlgebra.IsSimple)    (hSR : A.IsStronglyRational.{u,v}) :    A.PolynomialEnergyBounds ∧ OAI.MinimalVertex.CKLWStrongLocal U hSR.2.2 ∧      Nonempty (OAI.MinimalVertex.IrreducibleConformalNetStructure (OAI.MinimalVertex.intervalAlgebra U hSR.2.2)) := by  sorryend OAI.MinimalVertexend

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Strongly rational unitary vertex operator algebras and conformal nets

Theorem

Let V be a simple unitary strongly rational vertex operator algebra over \mathbb C. Then:

(1)
V has polynomial energy bounds and is CKLW-strongly local. The algebras (eq:intro-net) form an irreducible conformal net A_V.
(2)
V is completely unitary: every simple grading-restricted module is unitarizable, and all canonical invariant Hermitian fusion forms are positive definite.
(3)
Every unitary grading-restricted finite-length module is strongly integrable, with the closed-field equality (eq:intro-cwx).
(4)
The net A_V is completely rational.
(5)
After choosing invariant positive forms on the simple modules, the Carpi–Weiner–Xu functor gives a braided unitary tensor equivalence
\Rep(V)\simeq\Rep^u(V) \xrightarrow{\ F_{\mathrm{CWX}}^V\ }\Rep^f(A_V).
The tensor structure and braiding on the right are Connes fusion and DHR braiding, with a common orientation convention for the circle.

Section 1, Introduction Read it in the paper TeX source, line 96

Show the TeX

Let $V$ be a simple unitary strongly rational vertex operator algebra over $\mathbb C$. Then:
\begin{enumerate}[label=\textup{(\arabic*)}]
\item $V$ has polynomial energy bounds and is CKLW-strongly local. The algebras \eqref{eq:intro-net} form an irreducible conformal net $A_V$.
\item $V$ is completely unitary: every simple grading-restricted module is unitarizable, and all canonical invariant Hermitian fusion forms are positive definite.
\item Every unitary grading-restricted finite-length module is strongly integrable, with the closed-field equality \eqref{eq:intro-cwx}.
\item The net $A_V$ is completely rational.
\item After choosing invariant positive forms on the simple modules, the Carpi--Weiner--Xu functor gives a braided unitary tensor equivalence
\[
 \Rep(V)\simeq\Rep^u(V)
 \xrightarrow{\ F_{\mathrm{CWX}}^V\ }\Rep^f(A_V).
\]
The tensor structure and braiding on the right are Connes fusion and DHR braiding, with a common orientation convention for the circle.
\end{enumerate}

Configuration and file facts

File: lean/ComparatorChallenges/VertexAlgebraNet.lean
OpenAI’s Lean catalogue: OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 280 link it.
Solution module: OAI.RepresentationTheory.VertexAlgebra.MinimalComparator
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 89 local vocabulary declarations
Lines of Lean, without comments or blank lines: 535
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas