Blueprint Summary🔗

Overview

Total entries54completed: 53; deps incomplete: 0; sorries: 0; no proof: 1

Ready now1Entries with an actionable next formalization step.

Fully closed53Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (54)

Definitions25completed: 25; deps incomplete: 0; sorries: 0; no proof: 0

Lemmas27completed: 27; deps incomplete: 0; sorries: 0; no proof: 0

Theorems2completed: 1; deps incomplete: 0; sorries: 0; no proof: 1

Informal-only entries1

Definition Index (25)

«def:CyclicTripleSum»(Definition)
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom
«def:VirasoroVermaModule»(Definition)
Associated lean decls (1)
- VirasoroProject.VirasoroVerma
«def:LieVermaModule»(Definition)
Associated lean decls (3)
«def:LieTwoCohomology»(Definition)
Associated lean decls (1)
- VirasoroProject.LieTwoCohomology
«def:TriangularDecomposition»(Definition)
Associated lean decls (1)
- VirasoroProject.TriangularDecomposition
«def:CentralExtensionOfCocycle»(Definition)
Associated lean decls (2)
- VirasoroProject.LieTwoCocycle.CentralExtension
- VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
«def:HeisenbergCocycle»(Definition)
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
«def:LieExtension»(Definition)
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsExtension
«def:VirasoroBasis»(Definition)
Associated lean decls (1)
- VirasoroProject.VirasoroAlgebra.basisLC
«def:VirasoroTriangular»(Definition)
Associated lean decls (1)
- VirasoroProject.virasoroTri
«def:HeisenbergBasis»(Definition)
Associated lean decls (1)
- VirasoroProject.HeisenbergAlgebra.basisJK
«def:HeisenbergTriangular»(Definition)
Associated lean decls (1)
- VirasoroProject.heisenbergTri
«def:LieTwoCocycle»(Definition)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle
«def:VirasoroCocycle»(Definition)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.virasoroCocycle
«def:ChargedFockSpaceSugawara»(Definition)
Associated lean decls (2)
- VirasoroProject.ChargedFockSpace.sugawaraRepresentation
- VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
«def:VirasoroAlgebra»(Definition)
Associated lean decls (3)
«def:ChargedFockSpace»(Definition)
Associated lean decls (1)
- VirasoroProject.ChargedFockSpace
«def:WittAlgebra»(Definition)
Associated lean decls (2)
- VirasoroProject.WittAlgebra
- VirasoroProject.WittAlgebra.bracket
«def:SugawaraOperator»(Definition)
Associated lean decls (1)
- VirasoroProject.sugawaraGen
«def:VermaModule»(Definition)
Associated lean decls (2)
- VirasoroProject.VermaModule
- VirasoroProject.instModuleVermaModule
«def:LieTwoCoboundary»(Definition)
Associated lean decls (1)
- VirasoroProject.LieOneCochain_bdryHom
«def:HeisenbergAlgebra»(Definition)
Associated lean decls (3)
«def:NormalOrdering»(Definition)
Associated lean decls (1)
- VirasoroProject.pairNO
«def:LieCentralExtension»(Definition)
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsCentralExtension
«def:LieOneCochain»(Definition)
Associated lean decls (1)
- VirasoroProject.LieOneCochain

Theorem / Proposition / Lemma / Corollary Index (29)

«lem:AlternativeNormalOrdering»(Lemma)
Associated lean decls (1)
- VirasoroProject.heiOper_pairNO_eq_pairNO'
«lem:WittTwoCocycleSupport»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
«lem:SugawaraCommutatorSeries»(Lemma)
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
«thm:CentralExtensionOfCohomologyClass»(Theorem)
«lem:LieTwoCocycle_vectorSpace»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.instModule
«lem:AuxiliaryCentralChargeCalculation»(Lemma)
Associated lean decls (1)
- VirasoroProject.bosonic_sugawara_cc_calc_nonneg
«lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
Associated lean decls (2)
- VirasoroProject.LieOneCochain_bdryHom
- VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
«lem:WittTwoCocycleEquation»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
«lem:HeisenbergCocycleNontrivial»(Lemma)
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero
«lem:HeisenbergEventuallyCommute»(Lemma)
Associated lean decls (1)
- VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
«lem:VermaUniversalProperty»(Lemma)
Associated lean decls (3)
«lem:VirasoroCocycleNontrivial»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
«lem:CommutatorSugawaraNormalOrderedPair»(Lemma)
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiPairNO'
«lem:LieTwoCocycle_skew_symmetry»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.skew
«lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.virasoroCocycle
«lem:WittTwoCohomologyIsOneDimensional»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
«lem:NormalOrderingFiniteSupport»(Lemma)
Associated lean decls (1)
- VirasoroProject.hasFiniteSupport_smul_pairNO_apply
«lem:NormalOrderingTruncation»(Lemma)
Associated lean decls (1)
- VirasoroProject.pairNO_apply_eq_zero
«def:HighestWeightVector»(Lemma)
Associated lean decls (3)
«lem:CommutatorSugawaraHeisenberg»(Lemma)
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiOper
«lem:LieOneCochain_vectorSpace»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieOneCochain.instModule
«lem:OfCocycleIsCentralExtension»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
«lem:LieTwoCohomology_abelian»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
«lem:CommutatorSugawara»(Lemma)
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen
«thm:SugawaraRepresentation»(Theorem)
Associated lean decls (1)
- VirasoroProject.sugawaraRepresentation
«lem:VacuumHighestWeightVector»(Lemma)
Associated lean decls (3)
«lem:WittAlgebraIsLieAlgebra»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.instLieAlgebra
«lem:TruncationForChargedFockSpace»(Lemma)
Associated lean decls (1)
- VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
«lem:WittTwoCocycleNormalization»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle

Dependency insights

Statement-used entries32Entries reused in statement dependencies.

Proof-used entries17Entries reused in proof-only dependencies.

Most used in statements (32)

«def:LieTwoCocycle»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 31
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle
«def:SugawaraOperator»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
Associated lean decls (1)
- VirasoroProject.sugawaraGen
«def:LieTwoCohomology»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
- VirasoroProject.LieTwoCohomology
«def:CentralExtensionOfCocycle»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 16
Associated lean decls (2)
- VirasoroProject.LieTwoCocycle.CentralExtension
- VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
«def:NormalOrdering»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
Associated lean decls (1)
- VirasoroProject.pairNO
«lem:WittAlgebraIsLieAlgebra»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 14
Associated lean decls (1)
- VirasoroProject.WittAlgebra.instLieAlgebra
«def:VirasoroCocycle»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
Associated lean decls (1)
- VirasoroProject.WittAlgebra.virasoroCocycle
«def:LieTwoCoboundary»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
Associated lean decls (1)
- VirasoroProject.LieOneCochain_bdryHom
«def:TriangularDecomposition»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
Associated lean decls (1)
- VirasoroProject.TriangularDecomposition
«def:VermaModule»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
Associated lean decls (2)
- VirasoroProject.VermaModule
- VirasoroProject.instModuleVermaModule
Show all 22 more statement-used entries
- «def:WittAlgebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (2)
  - VirasoroProject.WittAlgebra
  - VirasoroProject.WittAlgebra.bracket
- «def:HeisenbergCocycle»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
- «def:HeisenbergBasis»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.basisJK
- «def:LieVermaModule»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «def:VirasoroBasis»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - VirasoroProject.VirasoroAlgebra.basisLC
- «lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «def:LieExtension»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsExtension
- «def:LieCentralExtension»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsCentralExtension
- «def:LieOneCochain»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain
- «lem:LieOneCochain_vectorSpace»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain.instModule
- «lem:LieTwoCocycle_vectorSpace»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.instModule
- «lem:NormalOrderingFiniteSupport»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 8
  Associated lean decls (1)
  - VirasoroProject.hasFiniteSupport_smul_pairNO_apply
- «def:HeisenbergAlgebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (3)
- «def:VirasoroAlgebra»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (3)
- «def:HeisenbergTriangular»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - VirasoroProject.heisenbergTri
- «def:ChargedFockSpace»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace
- «def:HighestWeightVector»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (3)
- «def:VirasoroTriangular»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.virasoroTri
- «lem:TruncationForChargedFockSpace»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
- «thm:SugawaraRepresentation»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.sugawaraRepresentation
- «def:ChargedFockSpaceSugawara»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - VirasoroProject.ChargedFockSpace.sugawaraRepresentation
  - VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
- «def:VirasoroVermaModule»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - VirasoroProject.VirasoroVerma

Most used in proofs (17)

«lem:WittTwoCocycleEquation»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
«def:CyclicTripleSum»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 15
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom
«lem:NormalOrderingTruncation»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (1)
- VirasoroProject.pairNO_apply_eq_zero
«lem:NormalOrderingFiniteSupport»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 8
Associated lean decls (1)
- VirasoroProject.hasFiniteSupport_smul_pairNO_apply
«lem:SugawaraCommutatorSeries»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 6
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
«lem:AlternativeNormalOrdering»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
- VirasoroProject.heiOper_pairNO_eq_pairNO'
«lem:CommutatorSugawaraHeisenberg»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 5
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiOper
«lem:AuxiliaryCentralChargeCalculation»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- VirasoroProject.bosonic_sugawara_cc_calc_nonneg
«lem:CommutatorSugawaraNormalOrderedPair»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiPairNO'
«lem:CommutatorSugawara»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen
Show all 7 more proof-used entries
- «lem:HeisenbergEventuallyCommute»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
- «lem:LieTwoCocycle_skew_symmetry»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.skew
- «lem:WittTwoCocycleSupport»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
- «lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - VirasoroProject.LieOneCochain_bdryHom
  - VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
- «lem:VermaUniversalProperty»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «lem:VirasoroCocycleNontrivial»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
- «lem:WittTwoCocycleNormalization»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle

Metadata

Metadata audit

Missing owner54

Missing effort54

Untagged54

Missing owner (54)

«def:CentralExtensionOfCocycle»(Definition)

Missing owner metadata.
Associated lean decls (2)
- VirasoroProject.LieTwoCocycle.CentralExtension
- VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
«def:ChargedFockSpaceSugawara»(Definition)

Missing owner metadata.
Associated lean decls (2)
- VirasoroProject.ChargedFockSpace.sugawaraRepresentation
- VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
«def:ChargedFockSpace»(Definition)

Missing owner metadata.
Associated lean decls (1)
- VirasoroProject.ChargedFockSpace
«def:CyclicTripleSum»(Definition)

Missing owner metadata.
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom
«def:HeisenbergAlgebra»(Definition)

Missing owner metadata.
Associated lean decls (3)
«def:HeisenbergBasis»(Definition)

Missing owner metadata.
Associated lean decls (1)
- VirasoroProject.HeisenbergAlgebra.basisJK
«def:HeisenbergCocycle»(Definition)

Missing owner metadata.
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
«def:HeisenbergTriangular»(Definition)

Missing owner metadata.
Associated lean decls (1)
- VirasoroProject.heisenbergTri
«def:HighestWeightVector»(Lemma)

Missing owner metadata.
Associated lean decls (3)
«def:LieCentralExtension»(Definition)

Missing owner metadata.
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsCentralExtension
Show all 44 more entries missing owner
- «def:LieExtension»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsExtension
- «def:LieOneCochain»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain
- «def:LieTwoCoboundary»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain_bdryHom
- «def:LieTwoCocycle»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle
- «def:LieTwoCohomology»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCohomology
- «def:LieVermaModule»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «def:NormalOrdering»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO
- «def:SugawaraOperator»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraGen
- «def:TriangularDecomposition»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.TriangularDecomposition
- «def:VermaModule»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - VirasoroProject.VermaModule
  - VirasoroProject.instModuleVermaModule
- «def:VirasoroAlgebra»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «def:VirasoroBasis»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroAlgebra.basisLC
- «def:VirasoroCocycle»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «def:VirasoroTriangular»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.virasoroTri
- «def:VirasoroVermaModule»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroVerma
- «def:WittAlgebra»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - VirasoroProject.WittAlgebra
  - VirasoroProject.WittAlgebra.bracket
- «lem:AlternativeNormalOrdering»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.heiOper_pairNO_eq_pairNO'
- «lem:AuxiliaryCentralChargeCalculation»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.bosonic_sugawara_cc_calc_nonneg
- «lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - VirasoroProject.LieOneCochain_bdryHom
  - VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
- «lem:CommutatorSugawaraHeisenberg»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiOper
- «lem:CommutatorSugawaraNormalOrderedPair»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiPairNO'
- «lem:CommutatorSugawara»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen
- «lem:HeisenbergCocycleNontrivial»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero
- «lem:HeisenbergEventuallyCommute»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
- «lem:LieOneCochain_vectorSpace»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain.instModule
- «lem:LieTwoCocycle_skew_symmetry»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.skew
- «lem:LieTwoCocycle_vectorSpace»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.instModule
- «lem:LieTwoCohomology_abelian»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
- «lem:NormalOrderingFiniteSupport»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.hasFiniteSupport_smul_pairNO_apply
- «lem:NormalOrderingTruncation»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO_apply_eq_zero
- «lem:OfCocycleIsCentralExtension»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
- «lem:SugawaraCommutatorSeries»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
- «lem:TruncationForChargedFockSpace»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
- «lem:VacuumHighestWeightVector»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:VermaUniversalProperty»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:VirasoroCocycleNontrivial»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
- «lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «lem:WittAlgebraIsLieAlgebra»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.instLieAlgebra
- «lem:WittTwoCocycleEquation»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
- «lem:WittTwoCocycleNormalization»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle
- «lem:WittTwoCocycleSupport»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
- «lem:WittTwoCohomologyIsOneDimensional»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
- «thm:CentralExtensionOfCohomologyClass»(Theorem)
  
  Missing owner metadata.
- «thm:SugawaraRepresentation»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraRepresentation

Missing effort (54)

«def:CentralExtensionOfCocycle»(Definition)

Missing effort metadata.
Associated lean decls (2)
- VirasoroProject.LieTwoCocycle.CentralExtension
- VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
«def:ChargedFockSpaceSugawara»(Definition)

Missing effort metadata.
Associated lean decls (2)
- VirasoroProject.ChargedFockSpace.sugawaraRepresentation
- VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
«def:ChargedFockSpace»(Definition)

Missing effort metadata.
Associated lean decls (1)
- VirasoroProject.ChargedFockSpace
«def:CyclicTripleSum»(Definition)

Missing effort metadata.
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom
«def:HeisenbergAlgebra»(Definition)

Missing effort metadata.
Associated lean decls (3)
«def:HeisenbergBasis»(Definition)

Missing effort metadata.
Associated lean decls (1)
- VirasoroProject.HeisenbergAlgebra.basisJK
«def:HeisenbergCocycle»(Definition)

Missing effort metadata.
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
«def:HeisenbergTriangular»(Definition)

Missing effort metadata.
Associated lean decls (1)
- VirasoroProject.heisenbergTri
«def:HighestWeightVector»(Lemma)

Missing effort metadata.
Associated lean decls (3)
«def:LieCentralExtension»(Definition)

Missing effort metadata.
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsCentralExtension
Show all 44 more entries missing effort
- «def:LieExtension»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsExtension
- «def:LieOneCochain»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain
- «def:LieTwoCoboundary»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain_bdryHom
- «def:LieTwoCocycle»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle
- «def:LieTwoCohomology»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCohomology
- «def:LieVermaModule»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «def:NormalOrdering»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO
- «def:SugawaraOperator»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraGen
- «def:TriangularDecomposition»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.TriangularDecomposition
- «def:VermaModule»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - VirasoroProject.VermaModule
  - VirasoroProject.instModuleVermaModule
- «def:VirasoroAlgebra»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «def:VirasoroBasis»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroAlgebra.basisLC
- «def:VirasoroCocycle»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «def:VirasoroTriangular»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.virasoroTri
- «def:VirasoroVermaModule»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroVerma
- «def:WittAlgebra»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - VirasoroProject.WittAlgebra
  - VirasoroProject.WittAlgebra.bracket
- «lem:AlternativeNormalOrdering»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.heiOper_pairNO_eq_pairNO'
- «lem:AuxiliaryCentralChargeCalculation»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.bosonic_sugawara_cc_calc_nonneg
- «lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - VirasoroProject.LieOneCochain_bdryHom
  - VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
- «lem:CommutatorSugawaraHeisenberg»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiOper
- «lem:CommutatorSugawaraNormalOrderedPair»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiPairNO'
- «lem:CommutatorSugawara»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen
- «lem:HeisenbergCocycleNontrivial»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero
- «lem:HeisenbergEventuallyCommute»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
- «lem:LieOneCochain_vectorSpace»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain.instModule
- «lem:LieTwoCocycle_skew_symmetry»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.skew
- «lem:LieTwoCocycle_vectorSpace»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.instModule
- «lem:LieTwoCohomology_abelian»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
- «lem:NormalOrderingFiniteSupport»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.hasFiniteSupport_smul_pairNO_apply
- «lem:NormalOrderingTruncation»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO_apply_eq_zero
- «lem:OfCocycleIsCentralExtension»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
- «lem:SugawaraCommutatorSeries»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
- «lem:TruncationForChargedFockSpace»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
- «lem:VacuumHighestWeightVector»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:VermaUniversalProperty»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:VirasoroCocycleNontrivial»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
- «lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «lem:WittAlgebraIsLieAlgebra»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.instLieAlgebra
- «lem:WittTwoCocycleEquation»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
- «lem:WittTwoCocycleNormalization»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle
- «lem:WittTwoCocycleSupport»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
- «lem:WittTwoCohomologyIsOneDimensional»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
- «thm:CentralExtensionOfCohomologyClass»(Theorem)
  
  Missing effort metadata.
- «thm:SugawaraRepresentation»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraRepresentation

Untagged (54)

«def:CentralExtensionOfCocycle»(Definition)

Missing tag metadata.
Associated lean decls (2)
- VirasoroProject.LieTwoCocycle.CentralExtension
- VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
«def:ChargedFockSpaceSugawara»(Definition)

Missing tag metadata.
Associated lean decls (2)
- VirasoroProject.ChargedFockSpace.sugawaraRepresentation
- VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
«def:ChargedFockSpace»(Definition)

Missing tag metadata.
Associated lean decls (1)
- VirasoroProject.ChargedFockSpace
«def:CyclicTripleSum»(Definition)

Missing tag metadata.
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom
«def:HeisenbergAlgebra»(Definition)

Missing tag metadata.
Associated lean decls (3)
«def:HeisenbergBasis»(Definition)

Missing tag metadata.
Associated lean decls (1)
- VirasoroProject.HeisenbergAlgebra.basisJK
«def:HeisenbergCocycle»(Definition)

Missing tag metadata.
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
«def:HeisenbergTriangular»(Definition)

Missing tag metadata.
Associated lean decls (1)
- VirasoroProject.heisenbergTri
«def:HighestWeightVector»(Lemma)

Missing tag metadata.
Associated lean decls (3)
«def:LieCentralExtension»(Definition)

Missing tag metadata.
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsCentralExtension
Show all 44 more untagged entries
- «def:LieExtension»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsExtension
- «def:LieOneCochain»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain
- «def:LieTwoCoboundary»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain_bdryHom
- «def:LieTwoCocycle»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle
- «def:LieTwoCohomology»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCohomology
- «def:LieVermaModule»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «def:NormalOrdering»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO
- «def:SugawaraOperator»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraGen
- «def:TriangularDecomposition»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.TriangularDecomposition
- «def:VermaModule»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - VirasoroProject.VermaModule
  - VirasoroProject.instModuleVermaModule
- «def:VirasoroAlgebra»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «def:VirasoroBasis»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroAlgebra.basisLC
- «def:VirasoroCocycle»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «def:VirasoroTriangular»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.virasoroTri
- «def:VirasoroVermaModule»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.VirasoroVerma
- «def:WittAlgebra»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - VirasoroProject.WittAlgebra
  - VirasoroProject.WittAlgebra.bracket
- «lem:AlternativeNormalOrdering»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.heiOper_pairNO_eq_pairNO'
- «lem:AuxiliaryCentralChargeCalculation»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.bosonic_sugawara_cc_calc_nonneg
- «lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - VirasoroProject.LieOneCochain_bdryHom
  - VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
- «lem:CommutatorSugawaraHeisenberg»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiOper
- «lem:CommutatorSugawaraNormalOrderedPair»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_heiPairNO'
- «lem:CommutatorSugawara»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen
- «lem:HeisenbergCocycleNontrivial»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero
- «lem:HeisenbergEventuallyCommute»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
- «lem:LieOneCochain_vectorSpace»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain.instModule
- «lem:LieTwoCocycle_skew_symmetry»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.skew
- «lem:LieTwoCocycle_vectorSpace»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.instModule
- «lem:LieTwoCohomology_abelian»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
- «lem:NormalOrderingFiniteSupport»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.hasFiniteSupport_smul_pairNO_apply
- «lem:NormalOrderingTruncation»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.pairNO_apply_eq_zero
- «lem:OfCocycleIsCentralExtension»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
- «lem:SugawaraCommutatorSeries»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
- «lem:TruncationForChargedFockSpace»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
- «lem:VacuumHighestWeightVector»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:VermaUniversalProperty»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:VirasoroCocycleNontrivial»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
- «lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «lem:WittAlgebraIsLieAlgebra»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.instLieAlgebra
- «lem:WittTwoCocycleEquation»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
- «lem:WittTwoCocycleNormalization»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle
- «lem:WittTwoCocycleSupport»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
- «lem:WittTwoCohomologyIsOneDimensional»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
- «thm:CentralExtensionOfCohomologyClass»(Theorem)
  
  Missing tag metadata.
- «thm:SugawaraRepresentation»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - VirasoroProject.sugawaraRepresentation

Structure and coverage

Informal-only1Statements with no associated Lean code yet.

Ready to formalize1Entries with an actionable next formalization step.

Fully closed53Local code and ancestor closure are both complete.

Heaviest prerequisites (45)

«lem:WittTwoCohomologyIsOneDimensional»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 3proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
«lem:WittTwoCocycleNormalization»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle
«lem:WittTwoCocycleSupport»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero
«lem:CommutatorSugawaraNormalOrderedPair»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiPairNO'
«lem:CommutatorSugawara»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen
«lem:VacuumHighestWeightVector»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (3)
«thm:SugawaraRepresentation»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- VirasoroProject.sugawaraRepresentation
«lem:CommutatorSugawaraHeisenberg»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 5
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_heiOper
«lem:NormalOrderingFiniteSupport»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 8
Associated lean decls (1)
- VirasoroProject.hasFiniteSupport_smul_pairNO_apply
«lem:SugawaraCommutatorSeries»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 6
Associated lean decls (1)
- VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply
Show all 35 more heaviest-prerequisite entries
- «lem:TruncationForChargedFockSpace»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero
- «lem:WittAlgebraIsLieAlgebra»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 3downstream unlocks: 14
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.instLieAlgebra
- «thm:CentralExtensionOfCohomologyClass»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 0downstream unlocks: 0
- «def:CentralExtensionOfCocycle»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 16
  Associated lean decls (2)
  - VirasoroProject.LieTwoCocycle.CentralExtension
  - VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra
- «def:ChargedFockSpaceSugawara»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - VirasoroProject.ChargedFockSpace.sugawaraRepresentation
  - VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra
- «def:ChargedFockSpace»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.ChargedFockSpace
- «def:HeisenbergAlgebra»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (3)
- «def:HeisenbergTriangular»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - VirasoroProject.heisenbergTri
- «def:LieTwoCoboundary»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain_bdryHom
- «def:LieVermaModule»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «def:SugawaraOperator»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 7
  Associated lean decls (1)
  - VirasoroProject.sugawaraGen
- «def:VirasoroAlgebra»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (3)
- «def:VirasoroCocycle»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle
- «def:VirasoroTriangular»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.virasoroTri
- «def:VirasoroVermaModule»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - VirasoroProject.VirasoroVerma
- «lem:CentralExtensionOfCocycleModCoboundary»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - VirasoroProject.LieOneCochain_bdryHom
  - VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary
- «lem:HeisenbergCocycleNontrivial»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero
- «lem:VermaUniversalProperty»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- «lem:VirasoroCocycleNontrivial»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero
- «lem:WittTwoCocycleEquation»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero
- «def:HeisenbergBasis»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.basisJK
- «def:HeisenbergCocycle»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle
- «def:HighestWeightVector»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (3)
- «def:LieCentralExtension»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (1)
  - VirasoroProject.LieAlgebra.IsCentralExtension
- «def:LieTwoCohomology»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 5
  Associated lean decls (1)
  - VirasoroProject.LieTwoCohomology
- «def:VirasoroBasis»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - VirasoroProject.VirasoroAlgebra.basisLC
- «lem:AlternativeNormalOrdering»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (1)
  - VirasoroProject.heiOper_pairNO_eq_pairNO'
- «lem:HeisenbergEventuallyCommute»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen
- «lem:LieOneCochain_vectorSpace»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.LieOneCochain.instModule
- «lem:LieTwoCocycle_skew_symmetry»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.skew
- «lem:LieTwoCocycle_vectorSpace»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.instModule
- «lem:LieTwoCohomology_abelian»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
- «lem:NormalOrderingTruncation»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - VirasoroProject.pairNO_apply_eq_zero
- «lem:OfCocycleIsCentralExtension»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
- «lem:VirasoroCocycle_is_TwoCocycle»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - VirasoroProject.WittAlgebra.virasoroCocycle

No prerequisites (9)

«lem:AuxiliaryCentralChargeCalculation»(Lemma)
Associated lean decls (1)
- VirasoroProject.bosonic_sugawara_cc_calc_nonneg
«def:TriangularDecomposition»(Definition)
Associated lean decls (1)
- VirasoroProject.TriangularDecomposition
«def:LieExtension»(Definition)
Associated lean decls (1)
- VirasoroProject.LieAlgebra.IsExtension
«def:WittAlgebra»(Definition)
Associated lean decls (2)
- VirasoroProject.WittAlgebra
- VirasoroProject.WittAlgebra.bracket
«def:VermaModule»(Definition)
Associated lean decls (2)
- VirasoroProject.VermaModule
- VirasoroProject.instModuleVermaModule
«def:NormalOrdering»(Definition)
Associated lean decls (1)
- VirasoroProject.pairNO
«def:LieOneCochain»(Definition)
Associated lean decls (1)
- VirasoroProject.LieOneCochain
«def:LieTwoCocycle»(Definition)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle
«def:CyclicTripleSum»(Definition)
Associated lean decls (2)
- VirasoroProject.cyclicTripleSum
- VirasoroProject.cyclicTripleSumHom

No dependents (6)

«thm:CentralExtensionOfCohomologyClass»(Theorem)
«lem:OfCocycleIsCentralExtension»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension
«lem:LieTwoCohomology_abelian»(Lemma)
Associated lean decls (1)
- VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap
«lem:VacuumHighestWeightVector»(Lemma)
Associated lean decls (3)
«lem:WittTwoCohomologyIsOneDimensional»(Lemma)
Associated lean decls (1)
- VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one
«lem:HeisenbergCocycleNontrivial»(Lemma)
Associated lean decls (1)
- VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero