Papers With

← All papers
First page of Property F implies weak integrality for non-degenerate pivotal braided fusion categories

Property F implies weak integrality for non-degenerate pivotal braided fusion categories

Justin Asher, Jonah Berean-Dutcher, Clay Cordova, Julio Parra-Martinez, Richard Tuddenham

math.QA Nov 9, 2026 · v1 cond-mat.str-el hep-th
formalization category-theory algebra
Read PDF arXiv abstract Code
TL;DR
The proof that property F implies pseudo-unitarity and weak integrality for non-degenerate pivotal braided fusion categories is also formalized in Lean.
Abstract
We prove that every non-degenerate pivotal braided fusion category with property F is pseudo-unitary and weakly integral. In particular, every modular category with property F is weakly integral. Neither sphericality nor pseudo-unitarity is assumed. Passing to the Drinfeld centre extends the result to degenerate categories whose dimensions are positive on the intersection of the Müger centre with the adjoint subcategory; these include every braided fusion category with a pseudo-unitary Galois conjugate. Physically, the result connects the arithmetic of topological orders to the computational power of anyon braiding: non-integer squared total quantum dimension guarantees infinite braid group images, a necessary condition for universal quantum computation.
Problem

The Naidu–Rowell conjecture states that a braided fusion category has property F (all braid group images finite) exactly when it is weakly integral. The direction from property F to weak integrality was open for non-degenerate categories in general, without assuming sphericality or pseudo-unitarity.

Approach

A trace argument places overlapping copies of a unitary on increasingly many strands. This bounds traces of unitaries in the span of the braid group images, and gives a saturation lemma linking the categorical dimension and the Frobenius–Perron dimension of a simple object. Applying it to the Frobenius–Perron object shows pseudo-unitarity, and Galois conjugation then forces integrality. Degenerate categories are handled by passing to the Drinfeld centre, and the argument is also formalized in Lean.

Results

Every non-degenerate pivotal braided fusion category with property F is pseudo-unitary with dim = FPdim in the integers, so every modular category with property F is weakly integral. The result extends to degenerate categories whose dimensions are positive on the intersection of the Müger centre with the adjoint subcategory.