Key assignment-sum formulas (tree graph formula, core-2/core-3, triangle and four-vertex loop cores) are machine-verified in Lean 4, with code in a public repository.
Abstract
Rényi multi-entropy probes multi-partite structure beyond bipartite spectra, but its behavior in general quantum states and the entanglement structure it captures remain poorly understood. We develop a finite field Gauss sum framework for calculating it in stabilizer states. Within this framework, the replica contraction reduces to a quadratic Gauss sum if and only if the state is locally unitarily equivalent to a stabilizer state. We obtain analytic expressions for the Rényi multi-entropy of all tree graph states and large families of loop graph states. In contrast to their flat bipartite Rényi spectra, stabilizer states generically have nonflat Rényi multi-entropy spectra.
Problem
Rényi multi-entropy probes multipartite entanglement beyond bipartite spectra, but it is hard to compute and poorly understood even for stabilizer states.
Approach
The replica contraction for stabilizer (graph) states is recast as a finite field Gauss sum problem using a core-graph representation with GHZ block sizes. Assignment sums are evaluated for tree graphs via a connected-subtree formula proved by induction, and for loop graphs through a recursive decomposition into loop-core coefficients. Key finite-assignment results are formally verified in Lean 4, starting from the finite-field assignment formulation.
Figure 3: A graph state, which is LC-equivalent to a core-2 state defined in ( 24 ).
Results
A closed formula covers all tree graph states, and explicit coefficients are given for triangle, four- and five-vertex loop cores and odd cycles. Loop graphs show different behavior at even and odd replica index, and stabilizer states generically have nonflat multi-entropy spectra. The tree, core-2, core-3, triangle and four-vertex loop results are machine-checked in Lean 4.
