Equal degree differences do not determine stored work

Abstract

Fourteen-qubit circulant stabilizer batteries with degree pairs (4,8) and (2,6) have the same degree difference but store different work at time π/4.

Definition 1.1 (The degree-difference assertion).

$$let(A:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(N\right)\to Prop)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \lambda (j:\mathrm{Fin}\left(N\right))\mapsto (i\ne j)\wedge (\exists (d:\mathbb{N}),(d\in Finset.\mathrm{range}\left(Nat.\mathrm{div}\left(K,2\right)\right))\wedge (((j).val=Nat.\mathrm{mod}\left((i).val+(d+1),N\right))\vee ((i).val=Nat.\mathrm{mod}\left((j).val+(d+1),N\right)))));let(S:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to \mathrm{Operator}\left(N\right)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \mathrm{wordOp}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (ifj=ithenPauli.Xelse(ifA\left(N,K,i,j\right)thenPauli.ZelsePauli.I))\right));let(H:\forall (N:\mathbb{N}),(\mathbb{N}\to \mathrm{Operator}\left(N\right))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \sum _{i:\mathrm{Fin}\left(N\right)}(S\left(N,K,i\right)));let(M:(\mathbb{N}\to \mathbb{N})):=(\lambda (N:\mathbb{N})\mapsto (if\mathrm{Even}\left(N\right)thenN-2elseN-1));let(G:\forall (N:\mathbb{N}),(\mathrm{Operator}\left(N\right)\to (\mathrm{State}\left(N\right)\to Prop))):=(\lambda (N:\mathbb{N})\mapsto \lambda (H:\mathrm{Operator}\left(N\right))\mapsto \lambda (g:\mathrm{State}\left(N\right))\mapsto (\sum _{b:(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))}(\Vert g\left(b\right){\Vert }^2)=1)\wedge (\forall (v:\mathrm{State}\left(N\right)),(\sum _{b:(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))}(\Vert v\left(b\right){\Vert }^2)=1\to Complex.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(g\right),Matrix.\mathrm{mulVec}\left(H,g\right)\right)\right)\le Complex.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(v\right),Matrix.\mathrm{mulVec}\left(H,v\right)\right)\right))));let(W:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathbb{N}\to (\mathrm{State}\left(N\right)\to (\mathbb{R}\to \mathbb{R}))))):=(\lambda (N:\mathbb{N})\mapsto \lambda (Kb:\mathbb{N})\mapsto \lambda (Kc:\mathbb{N})\mapsto \lambda (g:\mathrm{State}\left(N\right))\mapsto \lambda (t:\mathbb{R})\mapsto let({\rho }_0:\mathrm{Operator}\left(N\right)):=(Matrix.\mathrm{vecMulVec}\left(g,\mathrm{star}\left(g\right)\right));let(U:\mathrm{Operator}\left(N\right)):=(NormedSpace.\exp \left(SMul.\mathrm{smul}\left(-(Complex.I\cdot (Complex.\mathrm{ofReal}\left((t:\mathbb{R})\right):\mathbb{C})),H\left(N,Kc\right)\right)\right));Complex.\mathrm{re}\left(Matrix.\mathrm{trace}\left((U\cdot {\rho }_0\cdot Matrix.\mathrm{conjTranspose}\left(U\right)-{\rho }_0)\cdot H\left(N,Kb\right)\right)\right));\mathrm{claim}⟺(\forall (N:\mathbb{N}),(2<N\to (\neg (4\mid N)\to \forall (Kb:\mathbb{N}),\forall (Kc:\mathbb{N}),\forall (Lb:\mathbb{N}),\forall (Lc:\mathbb{N}),((\mathrm{Even}\left(Kb\right))\wedge ((2\le Kb)\wedge (Kb+2\le M\left(N\right)))\to ((\mathrm{Even}\left(Kc\right))\wedge ((2\le Kc)\wedge (Kc+2\le M\left(N\right)))\to ((\mathrm{Even}\left(Lb\right))\wedge ((2\le Lb)\wedge (Lb+2\le M\left(N\right)))\to ((\mathrm{Even}\left(Lc\right))\wedge ((2\le Lc)\wedge (Lc+2\le M\left(N\right)))\to (Kb\ne Kc\to (Lb\ne Lc\to (Nat.\mathrm{dist}\left(Kc,Kb\right)=Nat.\mathrm{dist}\left(Lc,Lb\right)\to \forall (g:\mathrm{State}\left(N\right)),\forall (h:\mathrm{State}\left(N\right)),(G\left(N,H\left(N,Kb\right),g\right)\to (G\left(N,H\left(N,Lb\right),h\right)\to \forall (t:\mathbb{R}),(0\le t\to W\left(N,Kb,Kc,g,t\right)=W\left(N,Lb,Lc,h,t\right))))))))))))))$$

Formalization. D5/S3/Quantum/Dynamics/StabilizerBatteryDegreeDifferenceRefutation.claim (✓ std3).

Citation. Debkanta Ghosh; Tanoy Kanti Konar; Gianluca Francica; Amit Kumar Pal; Aditi Sen De (2025). Quantum advantage unlocked: Charging quantum batteries with K-regular graph stabilizers. URL: https://arxiv.org/abs/2512.22908v2.

Commentary.

Equations (1) and (2) define the periodic circulant generators and their Hamiltonian sum. The mathematical symbols A, S and H denote the neighbourhood relation, its Pauli generators and that sum. The centre carries X, each neighbour carries Z, and every other site carries the identity. The maximum even degree is M(N). All arithmetic on natural degrees, including subtraction, is natural arithmetic; Nat.div is the integer quotient and Nat.mod is the remainder.

A State N is a complex vector on binary functions on Fin N, and an Operator N is a matrix on those indices. G(N,H,g) says that g has squared norm one and minimizes the real energy among all vectors v of squared norm one. The initial density is the outer product of g and its complex conjugate. The charging exponential and the real trace expression W are the unitary evolution and work of Section II, Figures of merit. Complex.ofReal explicitly embeds a real scalar into the complex numbers. The star on a vector is coordinatewise conjugation; the superscript H on a matrix is conjugate transpose.

The Section III remark reports unchanged work at fixed degree difference for the investigated sizes N at most ten outside multiples of four, and leaves the larger-size conclusion unresolved. The assertion displayed here quantifies over all sizes N greater than two not divisible by four, all four positive interior even degrees, all ground states g and h, and every nonnegative real time t. Interior means K + 2 at most M(N). Nat.dist is the absolute difference of two natural numbers.

Theorem 1.2 (A fourteen-qubit counterexample).

$$\neg (\mathrm{claim})$$

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

Resolves. Problems/ghosh-konar-francica-pal-sen-de-2025-stabilizer-battery-degree-difference-refutation (refuted) by D5/S3/Quantum/Dynamics/StabilizerBatteryDegreeDifferenceRefutation.result.

Source. Repository-derived.

Acknowledgement. Debkanta Ghosh; Tanoy Kanti Konar; Gianluca Francica; Amit Kumar Pal; Aditi Sen De (2025). Quantum advantage unlocked: Charging quantum batteries with K-regular graph stabilizers. URL: https://arxiv.org/abs/2512.22908v2.

Commentary.

Take N = 14, battery-charger pairs (Kb,Kc) = (4,8) and (Lb,Lc) = (2,6), and t = π/4. The maximum degree is 12, all four degrees are positive and interior, and both differences equal four. For each battery choose the negative-eigenvalue graph-state vector below. In its exponent, val is the natural representative of a binary residue. The linear term changes every graph-generator eigenvalue to minus one. Its normalization and the Hermitian-involution energy bound make it a ground state of the corresponding battery.

$$let(A:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(N\right)\to Prop)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \lambda (j:\mathrm{Fin}\left(N\right))\mapsto (i\ne j)\wedge (\exists (d:\mathbb{N}),(d\in Finset.\mathrm{range}\left(Nat.\mathrm{div}\left(K,2\right)\right))\wedge (((j).val=Nat.\mathrm{mod}\left((i).val+(d+1),N\right))\vee ((i).val=Nat.\mathrm{mod}\left((j).val+(d+1),N\right)))));let(S:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to \mathrm{Operator}\left(N\right)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \mathrm{wordOp}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (ifj=ithenPauli.Xelse(ifA\left(N,K,i,j\right)thenPauli.ZelsePauli.I))\right));let(H:\forall (N:\mathbb{N}),(\mathbb{N}\to \mathrm{Operator}\left(N\right))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \sum _{i:\mathrm{Fin}\left(N\right)}(S\left(N,K,i\right)));let(G:\forall (N:\mathbb{N}),(\mathrm{Operator}\left(N\right)\to (\mathrm{State}\left(N\right)\to Prop))):=(\lambda (N:\mathbb{N})\mapsto \lambda (H:\mathrm{Operator}\left(N\right))\mapsto \lambda (g:\mathrm{State}\left(N\right))\mapsto (\sum _{b:(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))}(\Vert g\left(b\right){\Vert }^2)=1)\wedge (\forall (v:\mathrm{State}\left(N\right)),(\sum _{b:(\mathrm{Fin}\left(N\right)\to \mathrm{Fin}\left(2\right))}(\Vert v\left(b\right){\Vert }^2)=1\to Complex.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(g\right),Matrix.\mathrm{mulVec}\left(H,g\right)\right)\right)\le Complex.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(v\right),Matrix.\mathrm{mulVec}\left(H,v\right)\right)\right))));\forall (N:\mathbb{N}),\forall (K:\mathbb{N}),let(g:\mathrm{State}\left(N\right)):=(\lambda (b:(\mathrm{Fin}\left(N\right)\to \mathrm{ZMod}\left(2\right)))\mapsto ((Complex.\mathrm{ofReal}\left((Real.\mathrm{sqrt}\left((2:\mathbb{R}{)}^N\right):\mathbb{R})\right):\mathbb{C}){)}^{-1}\cdot (-1:\mathbb{C}{)}^{{\sum }_{i:\mathrm{Fin}\left(N\right)}((b\left(i\right)).val)+{\sum }_{i:\mathrm{Fin}\left(N\right)}(Finset.\mathrm{sum}\left(Finset.\mathrm{filter}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (i<j)\wedge (A\left(N,K,i,j\right)),Finset.\mathrm{univ}\right),\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (b\left(i\right)).val\cdot (b\left(j\right)).val\right))});(G\left(N,H\left(N,K\right),g\right))\wedge (\forall (i:\mathrm{Fin}\left(N\right)),Matrix.\mathrm{mulVec}\left(S\left(N,K,i\right),g\right)=-g)$$

For each degree K the generators commute and square to the identity. Thus their charging exponential factors as follows, with factors in increasing Fin N order. The real cosine and sine are explicitly embedded into the complex scalars.

$$let(A:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(N\right)\to Prop)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \lambda (j:\mathrm{Fin}\left(N\right))\mapsto (i\ne j)\wedge (\exists (d:\mathbb{N}),(d\in Finset.\mathrm{range}\left(Nat.\mathrm{div}\left(K,2\right)\right))\wedge (((j).val=Nat.\mathrm{mod}\left((i).val+(d+1),N\right))\vee ((i).val=Nat.\mathrm{mod}\left((j).val+(d+1),N\right)))));let(S:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to \mathrm{Operator}\left(N\right)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \mathrm{wordOp}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (ifj=ithenPauli.Xelse(ifA\left(N,K,i,j\right)thenPauli.ZelsePauli.I))\right));let(H:\forall (N:\mathbb{N}),(\mathbb{N}\to \mathrm{Operator}\left(N\right))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \sum _{i:\mathrm{Fin}\left(N\right)}(S\left(N,K,i\right)));\forall (N:\mathbb{N}),\forall (K:\mathbb{N}),\forall (t:\mathbb{R}),NormedSpace.\exp \left(SMul.\mathrm{smul}\left(-(Complex.I\cdot (Complex.\mathrm{ofReal}\left((t:\mathbb{R})\right):\mathbb{C})),H\left(N,K\right)\right)\right)=List.\mathrm{prod}\left(List.\mathrm{ofFn}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto SMul.\mathrm{smul}\left((Complex.\mathrm{ofReal}\left((Real.\cos \left(t\right):\mathbb{R})\right):\mathbb{C}),(1:\mathrm{Operator}\left(N\right))\right)-SMul.\mathrm{smul}\left(Complex.I\cdot (Complex.\mathrm{ofReal}\left((Real.\sin \left(t\right):\mathbb{R})\right):\mathbb{C}),S\left(N,K,j\right)\right)\right)\right)$$

At time π/4 each factor is (I - i S)/sqrt(2). Let J be the increasing list of charger indices whose generators anticommute with the battery generator at i. The conjugated generator Qᵢ is the battery generator multiplied by the factors -i S at indices in J. For both degree pairs, J has four elements at every i.

$$let(A:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to (\mathrm{Fin}\left(N\right)\to Prop)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \lambda (j:\mathrm{Fin}\left(N\right))\mapsto (i\ne j)\wedge (\exists (d:\mathbb{N}),(d\in Finset.\mathrm{range}\left(Nat.\mathrm{div}\left(K,2\right)\right))\wedge (((j).val=Nat.\mathrm{mod}\left((i).val+(d+1),N\right))\vee ((i).val=Nat.\mathrm{mod}\left((j).val+(d+1),N\right)))));let(S:\forall (N:\mathbb{N}),(\mathbb{N}\to (\mathrm{Fin}\left(N\right)\to \mathrm{Operator}\left(N\right)))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \lambda (i:\mathrm{Fin}\left(N\right))\mapsto \mathrm{wordOp}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto (ifj=ithenPauli.Xelse(ifA\left(N,K,i,j\right)thenPauli.ZelsePauli.I))\right));let(H:\forall (N:\mathbb{N}),(\mathbb{N}\to \mathrm{Operator}\left(N\right))):=(\lambda (N:\mathbb{N})\mapsto \lambda (K:\mathbb{N})\mapsto \sum _{i:\mathrm{Fin}\left(N\right)}(S\left(N,K,i\right)));\forall (N:\mathbb{N}),\forall (Kb:\mathbb{N}),\forall (Kc:\mathbb{N}),\forall (i:\mathrm{Fin}\left(N\right)),let(U:\mathrm{Operator}\left(N\right)):=(NormedSpace.\exp \left(SMul.\mathrm{smul}\left(-(Complex.I\cdot (Complex.\mathrm{ofReal}\left((\frac{\pi }{4}:\mathbb{R})\right):\mathbb{C})),H\left(N,Kc\right)\right)\right));let(J:\mathrm{List}\left(\mathrm{Fin}\left(N\right)\right)):=(List.\mathrm{filter}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto \mathrm{decide}\left(\prod _{k:\mathrm{Fin}\left(N\right)}(\mathrm{sgn}\left((ifk=ithenPauli.Xelse(ifA\left(N,Kb,i,k\right)thenPauli.ZelsePauli.I)),(ifk=jthenPauli.Xelse(ifA\left(N,Kc,j,k\right)thenPauli.ZelsePauli.I))\right))=(-1:\mathbb{Z})\right),List.\mathrm{ofFn}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto j\right)\right));Matrix.\mathrm{conjTranspose}\left(U\right)\cdot S\left(N,Kb,i\right)\cdot U=S\left(N,Kb,i\right)\cdot List.\mathrm{prod}\left(List.\mathrm{map}\left(\lambda (j:\mathrm{Fin}\left(N\right))\mapsto SMul.\mathrm{smul}\left(-Complex.I,S\left(N,Kc,j\right)\right),J\right)\right)$$

Write a Pauli word as a scalar times X to a binary vector x followed by Z to a binary vector z, and let the binary adjacency matrix of the battery be Γ. Its graph-state expectation is a binary character sum. It vanishes unless the Z-part equals Γ applied to the X-part, that is z = Γx. For (4,8), every Qᵢ passes this test and its phase gives expectation -1. For (2,6), every Qᵢ fails the test and has expectation zero. The work is the sum over i of one plus the real part of this expectation, so the two work values are 0 and 14. Equal degree difference therefore does not suffice, even with both endpoint degrees excluded.

References

• Truth anchor: D5/S3/Quantum/Dynamics/StabilizerBatteryDegreeDifferenceRefutation.claim
• Truth anchor: D5/S3/Quantum/Dynamics/StabilizerBatteryDegreeDifferenceRefutation.result
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm
• Dependency: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation