Zero-magic-gap three-dimensional subspaces in every power-of-two dimension

Abstract

For every qudit dimension divisible by four, and so for every power of two at least four, some three-dimensional subspace has zero average stabilizer entropy gap.

Theorem 1.1 (Entries of an unphased Weyl displacement).

$$\forall d:\mathbb{N},d\ne 0\Rightarrow \forall a:\mathbb{Z}/d\mathbb{Z},\forall b:\mathbb{Z}/d\mathbb{Z},\forall x:\mathbb{Z}/d\mathbb{Z},\forall y:\mathbb{Z}/d\mathbb{Z},\mathrm{displacement}\left(d,a,b,x,y\right)=\mathrm{ite}\left(\mathrm{val}\left(x\right)=\mathrm{mod}\left(\mathrm{val}\left(y\right)+\mathrm{val}\left(a\right),d\right),\mathrm{windowRoot}{\left(d\right)}^{\mathrm{val}\left(b\right)\times \mathrm{val}\left(y\right)},0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.displacement_entry (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every nonzero natural dimension d and a, b, x, y in ZMod d, the unphased word X to val(a) times Z to val(b) has one nonzero entry per column. The column y is shifted by a and its phase is windowRoot(d) to val(b) times val(y). Here displacement denotes WeylDisplacement.displacement, before the tau phase of paperDisplacement.

Definition 1.2 (The displacement phase).

$$\mathrm{tau}\left(d\right)=-\exp \left(\frac{\pi i}{d}\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.tau (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

The phase τ = −e^{iπ/d} of the displacement operators, as in §II.A of arXiv:2512.23013v1.

Definition 1.3 (The displacement operators).

$$\forall a:\mathbb{Z}/d\mathbb{Z}\times \mathbb{Z}/d\mathbb{Z},\mathrm{paperDisplacement}\left(d,a\right)=\mathrm{tau}{\left(d\right)}^{a_1\times a_2}\cdot \mathrm{displacement}\left(d,a_1,a_2\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.paperDisplacement (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

D_a = τ^{a₁a₂} X^{a₁} Z^{a₂} for a = (a₁, a₂) in (ℤ/dℤ)². The word X^{a₁} Z^{a₂} is the frozen Weyl displacement of D5/S3/Quantum/Algebra/WeylDisplacement, built from the shift X|k⟩ = |k + 1⟩ and the clock Z|k⟩ = ω^k|k⟩, ω = e^{2πi/d}, of D5/S3/Observer/WindowRegister; the phase does not affect any quantity below because each operator occurs together with its adjoint.

Definition 1.4 (The fourth tensor power).

$$power4\left(V\right)=\mathrm{productMap}\left(i\mapsto V\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.power4 (✓ std3).

Source. Repository-derived.

Commentary.

V^{⊗4} for a rectangular matrix V, written with the frozen fourfold product productMap of D5/S3/Quantum/Recovery/PurifiedLocalPath, whose entry at (x, y) is the product over the four factors of the entries at (x_i, y_i).

Definition 1.5 (The alternating fourfold product).

$$\mathrm{alt}\left(A\right)=\mathrm{productMap}\left(A,(A{)}^{\ast },A,(A{)}^{\ast }\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.alt (✓ std3).

Source. Repository-derived.

Commentary.

A ⊗ A† ⊗ A ⊗ A†, the summand of Q.

Definition 1.6 (The permutation operators).

$$T\left(H,\sigma \right)(x,y)=\mathrm{ite}\left(x=y\circ {\sigma }^{-1},1,0\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.T (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

T_σ permutes the four tensor factors of a fourfold tensor power over a finite index type H (it is the permutation matrix of the induced permutation of index tuples); the paper writes T_σ = Σ |σ(i,j,k,l)⟩⟨ijkl|.

Definition 1.7 (The stabilizer entropy operator).

$$Q\left(d\right)=d^{-2}\cdot \sum _a\mathrm{alt}\left(\mathrm{paperDisplacement}\left(d,a\right)\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.Q (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

Q = d^{-2} Σ_a (D_a ⊗ D_a†)^{⊗2}, so that the linear stabilizer entropy of a pure state is M(ψ) = 1 − d tr(Q ψ^{⊗4}).

Definition 1.8 (The Haar fourth moment in closed form).

$$A4\left(H\right)=\mathrm{binom}{\left(\Vert H\Vert +3,4\right)}^{-1}\cdot \frac{1}{24}\cdot \sum _{\sigma \in S4}T\left(H,\sigma \right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.A4 (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

A₄ is the paper’s closed form of the Haar average E_U[(UψU†)^{⊗4}], the normalized projector onto the symmetric subspace of four tensor factors. The module takes this closed form as the definition; the Schur–Weyl identity with the Haar integral is quoted from the paper and not formalized.

Definition 1.9 (The average extrinsic term).

$$\mathrm{score}\left(V\right)=dB\times \mathrm{tr}\left(Q\left(dB\right)power4\left(V\right)A4\left(\mathrm{Fin}\left(3\right)\right)(power4\left(V\right){)}^{\ast }\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.score (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

For an isometry V from ℂ³ into ℂ^{d_B}, the term d_B tr(Q_B E^{⊗4}(A₄)) of the gap, with E(ρ) = VρV†.

Definition 1.10 (The average stabilizer entropy gap).

$$\mathrm{aseGap}\left(V\right)=3\times \mathrm{tr}\left(Q\left(3\right)A4\left(\mathbb{Z}/3\mathbb{Z}\right)\right)-\mathrm{score}\left(V\right)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.aseGap (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

ΔM(E) = d_S tr(Q_S A₄) − d_B tr(Q_B E^{⊗4}(A₄)) for d_S = 3, as in §III of the paper.

Definition 1.11 (The power-of-two observation).

$$claim\iff (\forall m:\mathbb{N},2\le m\Rightarrow \exists V:\mathrm{Matrix}\left(\mathbb{Z}/2^m\mathbb{Z},\mathrm{Fin}\left(3\right),\mathbb{C}\right),(V{)}^{\ast }\times V=1\wedge \mathrm{aseGap}\left(V\right)=0)$$

Formalization. D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.claim (✓ std3).

Citation. S. Cepollaro, G. Cuffaro, M. B. Weiss, S. Cusumano, A. Hamma, S. Lloyd (2025). Stabilizer Entropy of Subspaces. DOI: 10.48550/arXiv.2512.23013. URL: https://arxiv.org/abs/2512.23013v1.

Commentary.

The observation of §V.A of arXiv:2512.23013v1, “when d_B is a power of 2, a zero ASE subspace of dimension three is always achievable”: for every m ≥ 2 some isometry from ℂ³ into ℂ^{2^m} has zero gap (ℂ² has no three-dimensional subspace).

Theorem 1.12 (Every power of two at least four has a zero-gap three-dimensional subspace).

$$claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.result (✓ std3). ∎

Resolves. Problems/cepollaro-2025-power-of-two-zero-magic-gap (proved) by D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.result.

Source. Repository-derived.

Commentary.

The proof gives more: write d_B = 4r and take the subspace spanned by |r⟩, |3r⟩ and (|0⟩ − |2r⟩)/√2. Its vectors are supported on the subgroup rℤ_{4r}, so X^a Z^b compresses to zero unless r divides a, and for a = ur it compresses to the ququart operator X^u Z^{b mod 4}, each residue of b having r lifts; hence the extrinsic term equals that of the ququart subspace span{|1⟩, |3⟩, (|0⟩ − |2⟩)/√2} for every r. The sixteen compressed 3 × 3 operators have fourth moments 1 (once), 1/5 (three times) and 1/15 (twelve times), computed from the permutation sum over the 24 elements of S₄, so the extrinsic term is (1 + 3/5 + 12/15)/4 = 3/5; the qutrit term is (1 + 8/10)/3 = 3/5. The gap vanishes, and 2^m = 4 · 2^{m−2} for m ≥ 2.

References

• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.A4
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.Q
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.T
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.alt
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.aseGap
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.claim
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.displacement_entry
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.paperDisplacement
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.power4
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.result
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.score
• Truth anchor: D5/S3/Quantum/Magic/CepollaroPowerOfTwoZeroMagicGap.tau
• Dependency: D5/S3/Quantum/Algebra/WeylDisplacementPowers
• Dependency: D5/S3/Quantum/Algebra/WeylDisplacementTrace
• Dependency: D5/S3/Quantum/Recovery/PurifiedLocalPath