Spin covariance and Dicke coordinates

Abstract

Orthogonal Pauli rotations act on collective spins and their quadratic products.

Theorem 1.1 (Pauli conjugation gives an orthogonal matrix).

$$\forall \left(u:CoeSort.coe\left(Matrix.specialUnitaryGroup\left(\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right)\right),\left(\exists \left(r:\mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{R}\right)\right),\left(\left(\left(Matrix.transpose\left(r\right)\right)\cdot \left(r\right)=1\right)\wedge \left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\left(\left(Subtype.val\left(u\right)\right)\cdot \left(\mathrm{pauli}\left(a\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(Subtype.val\left(u\right)\right)\right)=\left(\sum \left(c:\mathrm{Fin}\left(3\right)\right),\left(HSMul.hSMul\left(Complex.ofReal\left(r\left(a,c\right)\right),\mathrm{pauli}\left(c\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.pauli_rotation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugation by a special unitary qubit matrix preserves the real space of traceless Hermitian matrices. Expand each conjugated Pauli matrix in the Pauli basis, with coefficient one half of the real part of its trace product with the corresponding Pauli matrix. Preservation of these trace products gives r times its transpose equal to the identity, hence also its transpose times r equal to the identity. The assertion requires orthogonality; it does not assert a determinant condition.

Theorem 1.2 (An orthogonal change of a sandwich family).

$$\forall \left(k:\mathrm{Type}\ast \right),\left(\forall \left(n:\mathrm{Type}\ast \right),\left([\mathrm{Fintype}\left(k\right)],[\mathrm{Fintype}\left(n\right)],[\mathrm{DecidableEq}\left(k\right)],\left(\forall \left(q:\mathrm{Matrix}\left(k,k,\mathbb{C}\right)\right),\left(\left(\left(Matrix.transpose\left(q\right)\right)\cdot \left(q\right)=1\right)\to \left(\forall \left(s:\left(k\right)\to \left(\mathrm{Matrix}\left(n,n,\mathbb{C}\right)\right)\right),\left(\forall \left(x:\mathrm{Matrix}\left(n,n,\mathbb{C}\right)\right),\left(\left(\sum \left(a:k\right),\left(\left(\left(\left(\sum \left(c:k\right),\left(HSMul.hSMul\left(q\left(a,c\right),s\left(c\right)\right)\right)\right)\right)\cdot \left(x\right)\right)\cdot \left(\left(\sum \left(e:k\right),\left(HSMul.hSMul\left(q\left(a,e\right),s\left(e\right)\right)\right)\right)\right)\right)\right)=\left(\sum \left(c:k\right),\left(\left(\left(s\left(c\right)\right)\cdot \left(x\right)\right)\cdot \left(s\left(c\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.orthogonal_sandwich (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a complex matrix q satisfying q transpose times q equal to the identity, replacing each member of a matrix family s by its q-linear combination leaves the sum of s c times x times s c unchanged. Expand both combinations and contract the two q coefficients by column orthogonality. This is a bilinear identity: the hypothesis uses transpose, and neither occurrence of s c is conjugate-transposed.

Theorem 1.3 (A tensor power is unitary).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(u:CoeSort.coe\left(Matrix.specialUnitaryGroup\left(\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right)\right),\left(\left(Matrix.conjTranspose\left(\mathrm{tensorOp}\left(Function.const\left(\mathrm{Fin}\left(n\right),Subtype.val\left(u\right)\right)\right)\right)\right)\cdot \left(\mathrm{tensorOp}\left(Function.const\left(\mathrm{Fin}\left(n\right),Subtype.val\left(u\right)\right)\right)\right)=1\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.tensor_unitary (✓ std3). ∎

Source. Repository-derived.

Commentary.

The tensor product of n copies of a special unitary qubit matrix is unitary. The constant family has domain Fin n, including the empty tensor product at n equal to zero.

Theorem 1.4 (A local matrix changes one coordinate).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(k:\mathrm{Fin}\left(n\right)\right),\left(\forall \left(a:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right),\left(\forall \left(f:\left(\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right)\right)\to \left(\mathbb{C}\right)\right),\left(\forall \left(x:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right)\right),\left(Matrix.mulVec\left(\mathrm{localOp}\left(k,a\right),f\right)\left(x\right)=\left(\sum \left(b:\mathrm{Fin}\left(2\right)\right),\left(\left(a\left(x\left(k\right),b\right)\right)\cdot \left(f\left(Function.update\left(x,k,b\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.local_action (✓ std3). ∎

Source. Repository-derived.

Commentary.

At a computational basis word x, the action of a matrix on site k sums over the replacement bit b. Split a word into its k-th coordinate and the remaining coordinates. The identity factors at the other sites force those coordinates to agree with x.

Definition 1.5 (Collective spin operators).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\left(\mathrm{collectiveSpin}\left(n,a\right):\mathrm{Matrix}\left(\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right),\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right),\mathbb{C}\right)\right)=HSMul.hSMul\left(\left(\frac{1}{2}:\mathbb{C}\right),\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(\mathrm{localOp}\left(k,\mathrm{pauli}\left(a\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.collectiveSpin (✓ std3).

Source. Repository-derived.

Commentary.

The collective spin in axis a is one half of the sum of the Pauli operator at every site. It acts on computational basis words of length n.

Theorem 1.6 (Collective spins inherit the Pauli rotation).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(u:CoeSort.coe\left(Matrix.specialUnitaryGroup\left(\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right)\right),\left(\forall \left(r:\mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{R}\right)\right),\left(\left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\left(\left(Subtype.val\left(u\right)\right)\cdot \left(\mathrm{pauli}\left(a\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(Subtype.val\left(u\right)\right)\right)=\left(\sum \left(c:\mathrm{Fin}\left(3\right)\right),\left(HSMul.hSMul\left(Complex.ofReal\left(r\left(a,c\right)\right),\mathrm{pauli}\left(c\right)\right)\right)\right)\right)\right)\to \left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\left(\left(\mathrm{tensorOp}\left(Function.const\left(\mathrm{Fin}\left(n\right),Subtype.val\left(u\right)\right)\right)\right)\cdot \left(\mathrm{collectiveSpin}\left(n,a\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(\mathrm{tensorOp}\left(Function.const\left(\mathrm{Fin}\left(n\right),Subtype.val\left(u\right)\right)\right)\right)\right)=\left(\sum \left(c:\mathrm{Fin}\left(3\right)\right),\left(HSMul.hSMul\left(Complex.ofReal\left(r\left(a,c\right)\right),\mathrm{collectiveSpin}\left(n,c\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.collective_tensor_rotation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume the same coefficient matrix r expresses each conjugated Pauli matrix in the Pauli basis. Conjugating a local operator by the constant tensor power conjugates its single nonidentity factor. Summing this identity over the sites and interchanging the finite sums gives the collective-spin transformation.

Theorem 1.7 (Rotation of quadratic spin products).

$$\forall \left(n:\mathrm{Type}\ast \right),\left([\mathrm{Fintype}\left(n\right)],[\mathrm{DecidableEq}\left(n\right)],\left(\forall \left(d:\mathrm{Matrix}\left(n,n,\mathbb{C}\right)\right),\left(\left(\left(Matrix.conjTranspose\left(d\right)\right)\cdot \left(d\right)=1\right)\to \left(\forall \left(r:\mathrm{Matrix}\left(\mathrm{Fin}\left(3\right),\mathrm{Fin}\left(3\right),\mathbb{R}\right)\right),\left(\left(\left(Matrix.transpose\left(r\right)\right)\cdot \left(r\right)=1\right)\to \left(\forall \left(j:\left(\mathrm{Fin}\left(3\right)\right)\to \left(\mathrm{Matrix}\left(n,n,\mathbb{C}\right)\right)\right),\left(\left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\left(\left(d\right)\cdot \left(j\left(a\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(d\right)\right)=\left(\sum \left(c:\mathrm{Fin}\left(3\right)\right),\left(HSMul.hSMul\left(Complex.ofReal\left(r\left(a,c\right)\right),j\left(c\right)\right)\right)\right)\right)\right)\to \left(\forall \left(\kappa :\mathbb{C}\right),\left(\forall \left(a:\mathrm{Fin}\left(3\right)\right),\left(\forall \left(b:\mathrm{Fin}\left(3\right)\right),\left(\left(\left(d\right)\cdot \left(HSMul.hSMul\left(\left(\frac{1}{2}:\mathbb{C}\right),\left(j\left(a\right)\right)\cdot \left(j\left(b\right)\right)+\left(j\left(b\right)\right)\cdot \left(j\left(a\right)\right)\right)-HSMul.hSMul\left(\left(\mathrm{if}a=b\mathrm{then}\kappa \mathrm{else}0\right),1\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(d\right)\right)=\left(\sum \left(c:\mathrm{Fin}\left(3\right)\right),\left(\left(\sum \left(e:\mathrm{Fin}\left(3\right)\right),\left(HSMul.hSMul\left(\left(Complex.ofReal\left(r\left(a,c\right)\right)\right)\cdot \left(Complex.ofReal\left(r\left(b,e\right)\right)\right),HSMul.hSMul\left(\left(\frac{1}{2}:\mathbb{C}\right),\left(j\left(c\right)\right)\cdot \left(j\left(e\right)\right)+\left(j\left(e\right)\right)\cdot \left(j\left(c\right)\right)\right)-HSMul.hSMul\left(\left(\mathrm{if}c=e\mathrm{then}\kappa \mathrm{else}0\right),1\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.quadratic_rotation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Suppose d is unitary, r is real orthogonal, and the family j transforms under conjugation by d with coefficients r. Inserting d adjoint times d between two factors gives the product transformation. Row orthogonality expresses the diagonal correction as the contraction of two r coefficients. Consequently the symmetrized quadratic product, with any complex diagonal correction κ, transforms with two copies of r.

Definition 1.8 (Normalized Dicke embedding).

$$\forall \left(n:\mathbb{N}\right),\left(\left(\mathrm{dickeIsometry}\left(n\right):\mathrm{Matrix}\left(\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right),\mathrm{Fin}\left(n+1\right),\mathbb{C}\right)\right)=\left(\lambda \left(x:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right)\right)\mapsto \left(\left(\lambda \left(r:\mathrm{Fin}\left(n+1\right)\right)\mapsto \left(\left(\mathrm{if}\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right)=Fin.val\left(r\right)\mathrm{then}Inv.inv\left(Complex.ofReal\left(Real.sqrt\left(\left(Nat.cast\left(Nat.choose\left(n,Fin.val\left(r\right)\right)\right):\mathbb{R}\right)\right)\right)\right)\mathrm{else}0\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dickeIsometry (✓ std3).

Source. Repository-derived.

Commentary.

The r-th column is supported on bit words with exactly r.val entries equal to one. Each supported entry is the reciprocal of the square root of Nat.choose n r.val. The binomial coefficient is cast from the natural numbers to the reals before taking its square root, and the result is included in the complex numbers before inversion. The spin index therefore counts ones.

Theorem 1.9 (Partial trace through a product embedding).

$$\forall \left(a:\mathrm{Type}\ast \right),\left(\forall \left(b:\mathrm{Type}\ast \right),\left(\forall \left(i:\mathrm{Type}\ast \right),\left(\forall \left(j:\mathrm{Type}\ast \right),\left([\mathrm{Fintype}\left(a\right)],[\mathrm{Fintype}\left(b\right)],[\mathrm{Fintype}\left(i\right)],[\mathrm{Fintype}\left(j\right)],[\mathrm{DecidableEq}\left(j\right)],\left(\forall \left(v:\mathrm{Matrix}\left(a,i,\mathbb{C}\right)\right),\left(\forall \left(w:\mathrm{Matrix}\left(b,j,\mathbb{C}\right)\right),\left(\left(\left(Matrix.conjTranspose\left(w\right)\right)\cdot \left(w\right)=1\right)\to \left(\forall \left(z:\mathrm{Matrix}\left(\left(\left(i\right)\times \left(j\right)\right),\left(\left(i\right)\times \left(j\right)\right),\mathbb{C}\right)\right),\left(\mathrm{partialTraceRight}\left(\left(\left(Matrix.kronecker\left(v,w\right)\right)\cdot \left(z\right)\right)\cdot \left(Matrix.conjTranspose\left(Matrix.kronecker\left(v,w\right)\right)\right)\right)=\left(\left(v\right)\cdot \left(\mathrm{partialTraceRight}\left(z\right)\right)\right)\cdot \left(Matrix.conjTranspose\left(v\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.partialTrace_isometries (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugate z by the Kronecker product of v and w, where w adjoint times w is the identity. In the partial trace over the second factor, the sum of a w coefficient times the conjugate of another is a Kronecker delta. Contracting that delta leaves v times the partial trace of z times v adjoint. No isometry hypothesis on v is needed.

Definition 1.10 (Dicke coefficient at a given weight).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(w:\mathbb{N}\right),\left(\forall \left(r:\mathbb{N}\right),\left(\left(\mathrm{dickeCoefficient}\left(n,w,r\right):\mathbb{C}\right)=\left(\mathrm{if}w=r\mathrm{then}Inv.inv\left(Complex.ofReal\left(Real.sqrt\left(\left(Nat.cast\left(Nat.choose\left(n,r\right)\right):\mathbb{R}\right)\right)\right)\right)\mathrm{else}0\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dickeCoefficient (✓ std3).

Source. Repository-derived.

Commentary.

For natural numbers n, w and r, this coefficient is zero unless the word weight w equals r. When they agree it is the reciprocal complex inclusion of the square root of the real cast of Nat.choose n r.

Theorem 1.11 (Summing the single-site Dicke transitions).

$$\forall \left(n:\mathbb{N}\right),\left(\forall \left(a:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right),\left(\forall \left(x:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(2\right)\right)\right),\left(\forall \left(r:\mathrm{Fin}\left(n+1\right)\right),\left(\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(\left(\sum \left(b:\mathrm{Fin}\left(2\right)\right),\left(\left(a\left(x\left(k\right),b\right)\right)\cdot \left(\mathrm{dickeIsometry}\left(n,Function.update\left(x,k,b\right),r\right)\right)\right)\right)\right)\right)=\left(\left(Nat.cast\left(n\right):\mathbb{C}\right)-\left(Nat.cast\left(\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right)\right):\mathbb{C}\right)\right)\cdot \left(\left(a\left(0,0\right)\right)\cdot \left(\mathrm{dickeCoefficient}\left(n,\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right),Fin.val\left(r\right)\right)\right)+\left(a\left(0,1\right)\right)\cdot \left(\mathrm{dickeCoefficient}\left(n,\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right)+1,Fin.val\left(r\right)\right)\right)\right)+\left(\left(Nat.cast\left(\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right)\right):\mathbb{C}\right)\right)\cdot \left(\left(a\left(1,0\right)\right)\cdot \left(\mathrm{dickeCoefficient}\left(n,\left(\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right)-1:\mathbb{N}\right),Fin.val\left(r\right)\right)\right)+\left(a\left(1,1\right)\right)\cdot \left(\mathrm{dickeCoefficient}\left(n,\left(\sum \left(k:\mathrm{Fin}\left(n\right)\right),\left(Fin.val\left(x\left(k\right)\right)\right)\right),Fin.val\left(r\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dicke_site_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The weight of a word is the natural-number sum of its bit values. Updating site k changes that weight by the new bit minus the old bit. Separate the sites at which x k is zero from those at which it is one. There are n minus the weight sites of the first kind and weight sites of the second kind. The two possible replacement bits yield the four displayed matrix entries and Dicke coefficients. Subtraction in the weight-minus-one argument is natural-number subtraction; the multiplicities are cast to complex scalars.

References

• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.collectiveSpin
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.collective_tensor_rotation
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dickeCoefficient
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dickeIsometry
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.dicke_site_sum
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.local_action
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.orthogonal_sandwich
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.partialTrace_isometries
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.pauli_rotation
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.quadratic_rotation
• Truth anchor: D5/S3/Quantum/Measurement/AnticoherenceSpinCovariance.tensor_unitary
• Dependency: D5/S3/Quantum/Dynamics/SpinCoupledEvenHypercubeGroverFixedPoint
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm
• Dependency: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings
• Dependency: D5/S3/QuantumChannels/ChannelTimeReversalNoGo