The n = 3 collapse of the genuine four-party multi-entropy for stabilizer states

S. Akella, N. Iizuka and A. Miyata, Genuine Multi-Entropy in the Toric Code, arXiv:2607.06050v2, state for stabilizer states the reduction $\mathrm{GM}^{(4)}_{3}(A:B:C:D)=-\left(a-\tfrac19\right)I_3$ (Eq. (3)), where $I_3$ is the Rényi tripartite information and $a$ the convention parameter of the genuine multi-entropy, note that "this reduction is not a consequence of the Coxeter structure", and ask in §6 "Whether there is a similar counting argument for $n = 3$ case is an open question." The verbatim definitions are in the literature note.

Issue #13575 reads Eq. (3) as a theorem about every normalized pure qubit stabilizer state and every assignment of its qubits to four labelled parties (parties may be empty), for every real $a$, together with positivity of every replica partition function $Z_3^{(\mathtt q)}$ so that every logarithm is defined.

For a Kitaev–Preskill partition $I_3$ is the negative topological entanglement entropy, so the collapse says the $n=3$ genuine multi-entropy of a stabilizer state carries no four-partite information beyond it. The paper establishes the $n=2$ case by a Coxeter counting argument and the $n=3$ case by computation; D5/S3/Quantum/Entanglement/StabilizerMultiEntropyCollapse.result proves it for all stabilizer states through ternary Fourier blocks. Its original partition_count now uses a structural counting argument: ternary mode orbits classify anchored partitions, and a quotient-colouring bijection transports the merger sums before the finite partition coefficients cancel.

Issue #13575 records the literature check before any Lean: the follow-up arXiv:2608.29627 reports the $n=3$ case as established numerically for qubit stabilizer states; arXiv:2601.16258 gives the $n=2$ argument only; abstract searches for "multi-entropy" with "stabilizer" found no proof; the repository had no result. not-found-in-searched-scope.

1. Every stabilizer state is $c,(U_1\otimes\cdots\otimes U_N)$ applied to a graph amplitude $(-1)^{\sum_{i<j}\Gamma_{ij}x_ix_j}$, and $Z$ is unchanged by identical local unitaries on all replicas (BinaryStabilizerGraphNormalForm.stabilizer_graph_normal_form).
2. For a graph amplitude the replica product is $(-1)^{F(\Gamma,\delta,x)}$, with $\delta_u$ the colour vector of qubit $u$ in $G=(\mathbb Z/3)^{\mathtt q-1}$.
3. The $\mathbb F_4$ Fourier transform over $G$ splits $F$ into bilinear blocks $y_t^{\mathsf T}C_tz_t$ over representatives $t$ of ${t,-t}$ (TernaryTranslationQuadraticNormalForm); each block sums to $2^{2N-\operatorname{rank}C_t}$, so $Z_3^{(\mathtt q)}=2^{-\sum_t\operatorname{rank}C_t}$.
4. $S_3^{(\mathtt q)}=\frac{\log2}{2\cdot3^{\mathtt q-2}}\sum_t\operatorname{rank}C_t$, and $\operatorname{rank}C_t$ depends only on the partition of the parties into the classes of $c\mapsto t\cdot\delta_c$. TernaryPartitionOrbit proves that every nonzero anchored ternary mode has exactly one representative with the same partition in any chosen opposite-pair representative family. A colouring compatible with a surjective merger factors through the quotient; subtracting the quotient colouring's value at its chosen target anchor normalizes it without changing its partition. This gives a bijection transporting arbitrary weighted sums.
5. With four labels, pigeonhole excludes the discrete partition and nonzero anchored modes exclude the indiscrete partition. The finite partition coefficients of the full term, six pair mergers, four singleton cuts and three balanced cuts cancel on the remaining support. Thus the original partition_count is a structural identity for any separation-matrix weight; the 13, 4 and 1 modes instantiate arbitrary opposite-pair representative families. Applying it to the ranks gives $\mathrm{GM}^{(4)}3+(a-\tfrac19)I{3,3}=0$.

The settlement is stated for the replica convention of the paper's Appendix A. Other conventions (for example, shifting the last party) and mixed or non-stabilizer states are outside the claim and are not addressed.

The canonical sources are D5/S3/Quantum/Entanglement/StabilizerMultiEntropyCollapse.lean (public shift, Z, S, I3, GM4, claim, result), the structural classification source D5/S3/Combinatorics/Partitions/TernaryPartitionOrbit.lean (public SamePartition, anchored, result), and its consumer D5/S3/Combinatorics/Partitions/TernaryPartitionCounting.lean (public merger_sum_transport, result), together with the graph/Fourier helper modules D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.lean (public complex_sign_val, graphAmp, stabilizer_graph_normal_form) and D5/S3/QuadraticForms/TernaryTranslationQuadraticNormalForm.lean (public F, C, ternary_translation_quadratic_normal_form). They reuse the frozen StabilizedBy, pauliSet, tensorOp, pauliMatrix, s2, hadamard, the frozen BinaryLagrangianGraphForm.sp, swapAt, swapAt_involutive and lagrangian_graph_form, and, of the frozen D5/S3/VertexAlgebra/LatticeTwistedGroundRealization, the sign SignQuotient.complexSign with complexSign_add, the sign laws sign_zero, sign_one, sign_square, sign_nonzero and sign_sum, and the binary quadratic exponent normalExponent with normal_exponent_add and symmetric_pairing_split. The axiom closure of result is exactly propext, Classical.choice and Quot.sound; there is no sorry, native_decide, or new axiom. The original Eq. (3) settlement, before the structural counting extension, recorded module statement sha256:66bb7b09e5459cd8efabbfdfa34a5f80a927227c135f2a1f07720856af3467c3, the result statement sha256:22e959e28055a09148222953a819dd9ed1c924acc40720eeb4b40849663a8058 and the claim statement sha256:d03e6b2def7dac64eebedf5658fa68874521789aa2d7db8ec375a93d7f9f3dc2; its Freeze event is sha256:e7cc50fa88839ce0c5f608e87468ca2a5351eff427a5239064db634c87f7ce41, with the two helper modules as project-level prerequisites. The helper BinaryStabilizerGraphNormalForm has module statement sha256:689b31c1238a39bc0b4635018d5bba4f6ea9aaae0f430517aed413bae442a25d and Freeze event sha256:5680f65f23e7c7424be9539b788cfb3e0a306d5172204e1ccd84655fae916897, with the frozen prerequisites BinaryStabilizerLocalInequivalence, BinaryLagrangianGraphForm and LatticeTwistedGroundRealization; the helper TernaryTranslationQuadraticNormalForm has module statement sha256:ad5c634ce99317530919c1b96b82781a4886f19aa96ba17d32de5894cefd56cb and Freeze event sha256:aa9f115cc367f3df30554f95efd2c447fdba777ad866069b19b5ab0bad91c55b, with no project-level prerequisite.

Tier 1 open question of a July 2026 paper, preregistered in issue #13575 before any Lean; pursued as a research line with layered modules. theorem; resolution proved.

| declaration | proof_shape | escape_witness | admission_basis | | --- | --- | --- | --- | | result | content after structural helper expansion | merger-to-partition transport | open-problem-resolution |

The original graph/Fourier helpers remain consumed on the proof path of result. The new arbitrary-index orbit classification and merger transport supply structural content; the finite catalogue and coefficient checks are consumed normalization auxiliaries, not separate delivered instance certificates or a general Mobius formula. The Lean source identifies their actual consumers (CLAUDE.md §3.2 「有消费的辅助声明」). Utility is none; there is no digestion atom.

What the settlement shows

Proved by result: for every normalized pure qubit stabilizer state $\psi$ and every $\mathrm{party}:\mathrm{Fin},N\to\mathrm{Fin},4$, every $Z_3^{(\mathtt q)}$ is a positive real and $\mathrm{GM}^{(4)}3=-(a-\tfrac19)I{3,3}$ for every real $a$.

Established inside the proof. $Z_3^{(\mathtt q)}=2^{-\sum_{t\in P}\operatorname{rank}C_t}$ for every number of colours $\mathtt q$ and every colouring, with $C_t$ the graph matrix masked to pairs of qubits whose colours $t$ separates.

Structural counting established inside the proof. A nonzero ternary mode with an extra zero anchor induces a nonconstant colouring with at most three blocks. Equality of anchored partitions is exactly equality up to sign. The quotient-colouring argument above therefore transports each merger sum to a sum over compatible partitions with multiplicity one. The finite coefficient cancellation is applied to an arbitrary real weight on separation matrices, before specializing to graph-block ranks. It is not restricted to one numerical entropy evaluation.

Argued, not formalized.

• Why $n=4$ fails. For $n=4$ the group $(\mathbb Z/4)^3$ has even order, the Fourier transform over a field of characteristic two is not invertible, and characters of order four see four-block partitions; the counting identity has no analogue, consistent with the paper's threshold $n=\mathtt q$.
• Other $\mathtt q$ at $n=3$. Steps 1–3 of the route hold for every $\mathtt q$; whether the collapse holds for $\mathtt q\ge5$, $n=3$ reduces to the corresponding coefficient identity over partitions into at most three blocks (not checked here).
• Other odd $n$ (candidate, open). For $n=5$ the characters of $(\mathbb Z/5)^{\mathtt q-1}$ take values in $\mathbb F_{16}$, and multiplication by $2$ permutes the nonzero characters in orbits of length four, so the pairing ${t,-t}$ of the $n=3$ argument is replaced by Frobenius orbits; the block form of the replica quadratic form and its Gauss sum over the splitting field would have to be established first. No claim beyond $n=3$ is made.

Open. The structural counting argument is for the four-party n=3 identity in Eq. (3). It does not identify a Coxeter group or prove a partition coefficient formula for arbitrary party counts. The general conjecture of the abstract ($\mathtt q\ge4$, $n<\mathtt q$) beyond $\mathtt q=4$, $n=3$, and the qudit (level $k$) analogues, are not settled here.

Effect on the paper. Eq. (3) holds for every normalized pure qubit stabilizer state, and its original production proof now uses a structural counting argument. This addresses the n=3 four-party counting mechanism without claiming the other cases of the paper's general conjecture.

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.