A symmetric injective matrix-product family with four physical levels

Abstract

Four physical levels with nonzero charge values admit a normalized, symmetric matrix-product family of bond dimension three that is injective at block length two.

Definition 1.1 (Periodic matrix-product amplitudes).

$$\forall \left(d:\mathbb{N}\right),\left(\forall \left(a:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right),\left(\forall \left(n:\mathbb{N}\right),\left(\forall \left(w:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(4\right)\right)\right),\left(\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.amplitude\left(a,n,w\right):\mathbb{C}\right)=D5.S3.Observer.SourceJetCyclicTraces.orderedTraceWord\left(\left(\lambda \left(i:\mathrm{Fin}\left(n\right)\right)\mapsto \left(a\left(w\left(i\right)\right)\right)\right),\mathrm{id}\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.amplitude (✓ std3).

Citation. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

In Symmetries191208.tex, lines 222–237, the amplitude of a periodic, translationally invariant matrix-product state is the trace of the ordered product of its local matrices. Here a assigns a complex d by d matrix to each of the four physical labels, and w lists the labels along a chain of length n. The identity ordering retains the order of the sites; at n = 0 the empty product is the identity matrix.

Definition 1.2 (The spectral one-site action).

$$\forall \left(w:Matrix.unitaryGroup\left(\mathrm{Fin}\left(4\right),\mathbb{C}\right)\right),\left(\forall \left(ch:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathbb{R}\right)\right),\left(\forall \left(\phi :\mathbb{R}\right),\left(\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.u1Rep\left(w,ch,\phi \right):\mathrm{Matrix}\left(\mathrm{Fin}\left(4\right),\mathrm{Fin}\left(4\right),\mathbb{C}\right)\right)=Unitary.conjStarAlgAut\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(4\right),\mathrm{Fin}\left(4\right),\mathbb{C}\right),w\right)\left(Matrix.diagonal\left(\left(\lambda \left(k:\mathrm{Fin}\left(4\right)\right)\mapsto \left(Complex.exp\left(\left(\left(Complex.ofReal\left(\phi \right)\right)\cdot \left(Complex.ofReal\left(ch\left(k\right)\right)\right)\right)\cdot \left(Complex.I\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.u1Rep (✓ std3).

Citation. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

Symmetries191208.tex, lines 727–738, considers a local action generated by a Hermitian matrix. In spectral coordinates, ch gives its four real eigenvalues and w is a unitary change of basis. The diagonal entries are exp(i φ ch(k)), and conjugation by w expresses the action in the original basis. The definition accepts arbitrary real eigenvalues and a real parameter φ; it does not impose an integrality or periodicity condition. The real factors in the exponential are explicitly included in the complex numbers.

Definition 1.3 (Symmetry up to a phase).

$$\forall \left(d:\mathbb{N}\right),\left(\forall \left(a:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right),\left(\forall \left(w:Matrix.unitaryGroup\left(\mathrm{Fin}\left(4\right),\mathbb{C}\right)\right),\left(\forall \left(ch:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathbb{R}\right)\right),\left(\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.IsSymmetric\left(a,w,ch\right)\right)\iff \left(\forall \left(\phi :\mathbb{R}\right),\left(\forall \left(n:\mathbb{N}\right),\left(\left(\left(0:\mathbb{N}\right)<n\right)\to \left(\exists \left(\theta :\mathbb{R}\right),\left(Matrix.mulVec\left(D5.S3.Quantum.Recovery.ProductPrefixRigidity.productMap\left(Function.const\left(\mathrm{Fin}\left(n\right),\mathrm{Fin}\left(4\right)\right),Function.const\left(\mathrm{Fin}\left(n\right),D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.u1Rep\left(w,ch,\phi \right)\right)\right),D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.amplitude\left(a,n\right)\right)=\left(\lambda \left(v:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(4\right)\right)\right)\mapsto \left(\left(Complex.exp\left(\left(Complex.ofReal\left(\theta \right)\right)\cdot \left(Complex.I\right)\right)\right)\cdot \left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.amplitude\left(a,n,v\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.IsSymmetric (✓ std3).

Citation. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

Equation (1) of Symmetries191208.tex, lines 134–140, expresses invariance under the tensor power of a one-site action up to a scalar phase. For every real φ and every positive chain length n, the same one-site matrix acts at every site. There must be a real θ for which the resulting amplitude function is multiplied by exp(i θ). The phase may depend on both φ and n. Function.const expresses the constant family of physical label types and the constant family of one-site matrices.

Definition 1.4 (Injectivity of a boundary-to-state map).

$$\forall \left(d:\mathbb{N}\right),\left(\forall \left(a:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right),\left(\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.IsInjective\left(a\right)\right)\iff \left(\exists \left(n:\mathbb{N}\right),\left(Function.Injective\left(\left(\lambda \left(x:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\mapsto \left(\left(\lambda \left(w:\left(\mathrm{Fin}\left(n\right)\right)\to \left(\mathrm{Fin}\left(4\right)\right)\right)\mapsto \left(Matrix.trace\left(\left(x\right)\cdot \left(List.prod\left(List.ofFn\left(\left(\lambda \left(i:\mathrm{Fin}\left(n\right)\right)\mapsto \left(a\left(w\left(i\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.IsInjective (✓ std3).

Citation. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

Symmetries191208.tex, lines 267–276, defines injectivity by the existence of a block length for which the map from a boundary matrix x to the amplitudes tr(x a(w(0)) ⋯ a(w(n−1))) is injective. Thus equality of these amplitudes for every word determines the boundary matrix. List.ofFn lists the site matrices in order and List.prod multiplies that list. The quantified block length is an arbitrary natural number.

Definition 1.5 (The proposed four-level obstruction).

$$\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.claim\right)\iff \left(\forall \left(d:\mathbb{N}\right),\left(\forall \left(a:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right),\left(\forall \left(w:Matrix.unitaryGroup\left(\mathrm{Fin}\left(4\right),\mathbb{C}\right)\right),\left(\forall \left(ch:\left(\mathrm{Fin}\left(4\right)\right)\to \left(\mathbb{R}\right)\right),\left(\left(\forall \left(k:\mathrm{Fin}\left(4\right)\right),\left(a\left(k\right)\ne \left(0:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right)\right)\to \left(\left(\sum _{k:\mathrm{Fin}\left(4\right)}\left(\left(a\left(k\right)\right)\cdot \left(\mathrm{star}\left(a\left(k\right)\right)\right)\right)=\left(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\right)\right)\to \left(\left(\forall \left(k:\mathrm{Fin}\left(4\right)\right),\left(ch\left(k\right)\ne \left(0:\mathbb{R}\right)\right)\right)\to \left(\left(\exists \left(k:\mathrm{Fin}\left(4\right)\right),\left(\exists \left(l:\mathrm{Fin}\left(4\right)\right),\left(ch\left(k\right)\ne ch\left(l\right)\right)\right)\right)\to \left(\left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.IsSymmetric\left(a,w,ch\right)\right)\to \left(\neg \left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.IsInjective\left(a\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

Symmetries191208.tex, lines 748–751, asks about spin three halves after exhibiting a U(1)-symmetric injective family with only nonzero generator eigenvalues at larger physical dimension, lines 726–746. The proposition here asks whether every four-level family is noninjective when all four local matrices are nonzero, their products with their conjugate transposes sum to the identity, all four real eigenvalues are nonzero, at least two eigenvalues differ, and the family is symmetric at every positive chain length. The unitary change of basis and the bond dimension are arbitrary. This is the reading with general generator eigenvalues; lines 719–721 separately give an obstruction for the usual spin generator with equally spaced half-integer eigenvalues.

Theorem 1.6 (A normalized injective family of bond dimension three).

$$\neg \left(D5.S3.Quantum.SpinChains.FourLevelU1SymmetricInjectiveMPS.claim\right)$$

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

Resolves. Problems/sanz-wolf-perez-garcia-cirac-2009-spin-three-halves-u1-injective-mps (refuted) by D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.result.

Source. Repository-derived.

Acknowledgement. M. Sanz; M. M. Wolf; D. Pérez-García; J. I. Cirac (2009). Matrix product states: Symmetries and two-body Hamiltonians. DOI: 10.1103/PhysRevA.79.042308. URL: https://arxiv.org/abs/0901.2223v1.

Commentary.

Use bond dimension 3 and the identity change of physical basis. With matrix units Eᵢⱼ indexed by 0, 1, 2, set A₀ = (3/5)(E₀₁ + E₁₂), A₁ = (4/5)(E₁₀ + E₂₁), A₂ = (4/5)E₀₂ and A₃ = (3/5)E₂₀. Take the four generator eigenvalues to be (−1, 1, −2, 2). Each local matrix has a nonzero entry. Direct multiplication gives Σₖ AₖAₖ† = I: each diagonal entry is 9/25 + 16/25 = 1 and every off-diagonal entry vanishes. Each eigenvalue is nonzero, and the first two differ.

For real φ let V(φ) = diag(1, exp(iφ), exp(2iφ)) and V(φ)⁻¹ = diag(1, exp(−iφ), exp(−2iφ)). Their product is the identity because the exponents cancel in each diagonal entry. Entrywise multiplication gives V(φ)AₖV(φ)⁻¹ = exp(iφλₖ)Aₖ for each k. Induction on a list of physical labels extends this identity to its ordered matrix product: the empty product uses V(φ)V(φ)⁻¹ = I, and the induction step inserts V(φ)⁻¹V(φ) = I between two factors. Taking traces and using invariance under conjugation shows that the product of the scalar phases times the trace of the word equals the original trace.

At the identity change of basis the one-site action is diagonal. Its tensor power is diagonal as well, so its action on a word amplitude is multiplication by the product of exp(iφλₖ) over that word. The trace identity therefore fixes every periodic amplitude. Choosing θ = 0 establishes symmetry at every positive chain length.

For injectivity, the length-two products satisfy A₀A₀ = (9/25)E₀₂, A₁A₁ = (16/25)E₂₀, A₀A₃ = (9/25)E₁₀, A₃A₀ = (9/25)E₂₁, A₁A₂ = (16/25)E₁₂, A₂A₁ = (16/25)E₀₁, A₂A₃ = (12/25)E₀₀, A₃A₂ = (12/25)E₂₂, and A₀A₁ − A₂A₃ = (12/25)E₁₁. Suppose tr(x AᵢAⱼ) = 0 for every pair of physical labels. For any nonzero complex c, the identity tr(x cEᵢⱼ) = c xⱼᵢ forces xⱼᵢ = 0 when this trace vanishes. The first eight products force x₂₀, x₀₂, x₀₁, x₁₂, x₂₁, x₁₀, x₀₀ and x₂₂ to vanish. Subtracting the traces for A₀A₁ and A₂A₃ forces x₁₁ = 0, so x = 0.

If boundary matrices x and y give equal amplitudes for every word of length two, evaluate their amplitude functions on the word with labels i and j. Linearity of the trace gives tr((x − y)AᵢAⱼ) = 0 for every pair. The preceding argument gives x − y = 0, hence x = y. Thus block length two gives injectivity. Applying the proposed obstruction to these local matrices, the identity unitary and these eigenvalues contradicts that injectivity. The example has general integer generator eigenvalues and does not assert SU(2) symmetry or symmetry under the usual spin-three-halves generator.

References

• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.IsInjective
• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.IsSymmetric
• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.amplitude
• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.claim
• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.result
• Truth anchor: D5/S3/Quantum/SpinChains/FourLevelU1SymmetricInjectiveMPS.u1Rep
• Dependency: D5/S3/Observer/SourceJetCyclicTraces
• Dependency: D5/S3/Quantum/QuantumChannels/MarginalApproximationWorstFidelity