Main properties (ii): sufficient conditions for exact cyclic translation invariance

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.cyclic_translation_invariance

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $N,D\ge1$ and consider the periodic trace MPS vector $M(A)$ and the RAGE vector $R(A,\Phi,V)$ . Suppose that $M(A)$ is exactly invariant under one cyclic shift, that the graph weights are circulant, and that all local unitaries are the same:

\Phi_{j+1,k+1}=\Phi_{j,k},\qquad V_j=V_k,

with indices taken modulo $N$ . Then

T R(A,\Phi,V)=R(A,\Phi,V),

where $T$ is the cyclic permutation of qubits. This is a sufficient condition on the underlying MPS vector, graph, and rotations; it does not require identical site tensors. It is an exact raw-vector identity and also covers $N=1$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P57

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix

namespace QAlgorithms.Papers.Independent.Intakethird100.P57

attribute [local instance] Classical.propDecidable

/-- PDF p.2, Main properties (ii): sufficient conditions only. Invariance of the MPS
vector is assumed, rather than the narrower requirement that all tensors be equal. -/
theorem cyclic_translation_invariance {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ)
    (hA : CyclicInvariant (traceMPS A))
    (hG : ∀ i j, G.weight (nextSite i) (nextSite j) = G.weight i j)
    (hV : ∀ i j, V i = V j) : CyclicInvariant (rage A G V) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Main properties (ii): sufficient conditions for exact cyclic translation invariance

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every pair of natural numbers $N,D$ with $N\ge1$ and $D\ge1$ , take arbitrary complex $D\times D$ matrices $A_k(t)$ for sites $k\in\{0,\ldots,N-1\}$ and bits $t$ , real weights $w_{k\ell}$ satisfying symmetry, zero diagonal, and $0\le w_{k\ell}<2\pi$ , and unitary $2\times2$ matrices $V_k$ . Write $\sigma(k)=(k+1)\bmod N$ and

m(b)=\operatorname{tr}\!\left(A_0(b_0)\cdots A_{N-1}(b_{N-1})\right).

Assume that $m(b\circ\sigma)=m(b)$ for every bit string $b$ , that $w_{\sigma(k),\sigma(\ell)}=w_{k\ell}$ for every pair of sites, and that $V_k=V_\ell$ for every pair of sites. Then the vector

r(b)= \sum_{c\in\{0,1\}^N} \left(\prod_{k=0}^{N-1}V_k(b_k,c_k)\right) \exp\!\left(\mathrm{i}\sum_{k<\ell}w_{k\ell}c_kc_\ell\right)m(c)

satisfies $r(b\circ\sigma)=r(b)$ for every $b$ . Products of the matrices $A_k$ are in increasing site order, and the statement includes $N=1$ , when the cyclic shift is the identity.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph