CZX parent-Lindbladian window channel

Abstract

The CZX parent-Lindbladian window channel and its gauge calculus.

Definition 1.1 (The two-site change of basis).

$D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU = 1000001000010100$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxU (✓ std3).

Citation. Yuhan Liu; Alberto Ruiz-de-Alarcón; Georgios Styliaris; Xiao-Qi Sun; David Pérez-García; J. Ignacio Cirac (2026). Parent Lindbladians for matrix product density operators. DOI: 10.1103/1qyd-59z7. URL: https://arxiv.org/abs/2501.10552v2.

Commentary.

The 4 by 4 permutation matrix is the two-site change of basis displayed in Appendix F, with the computational basis in source order (main.tex l. 4858–4863).

Definition 1.2 (The signed four-site permutation).

$D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz x V = λ (r : Fin (16)) \mapsto (λ (c : Fin (16)) \mapsto (ite ((r, c) \in {(0, 0), (1, 15), (2, 2), (3, 13), (4, 4), (5, 11), (6, 6), (8, 1), (9, 14), (10, 3), (12, 5), (13, 10), (14, 7), (15, 8)}, (1 : C), ite ((r, c) = (7, 9) \lor (r, c) = (11, 12), - (1 : C), (0 : C)))))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxV (✓ std3).

Commentary.

The 16 by 16 signed permutation has the fourteen positive entries and two negative entries listed in Appendix F (main.tex l. 4933–4937). Its row and column indices are the four-bit window words.

Definition 1.3 (The two-site block weight).

$D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . m u = \frac{Real . s q r t ( 3 )}{4}$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.mu (✓ std3).

Commentary.

The common block weight is the positive real number square root of three divided by four (main.tex l. 4870).

Definition 1.4 (The four-site block weight).

$D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . n u = \frac{Real . s q r t ( 3 )}{16}$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.nu (✓ std3).

Commentary.

The multiplicity block weight is square root of three divided by sixteen (main.tex l. 4930).

Definition 1.5 (The four-to-two renormalization channel).

$\forall (x : Matrix (Fin (16), Fin (16), C)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . re n or m S (x) = ((Matrix . co nj T r an s p ose (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU)) \cdot (Matrix . o f λ (r : Fin (4)) \mapsto (λ (s : Fin (4)) \mapsto (ite Fin . d i v N a t (2, 2, r) = Fin . d i v N a t (2, 2, s), m : Fin (4) \sum (((D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz x V) \cdot (x)) \cdot (Matrix . co nj T r an s p ose (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz x V))) (Fin . mk ((((8) \cdot (Fin . v a l (Fin . d i v N a t (2, 2, r)))) + ((2) \cdot (Fin . v a l (m)))) + (Fin . v a l (Fin . m o d N a t (2, 2, r)))), Fin . mk ((((8) \cdot (Fin . v a l (Fin . d i v N a t (2, 2, s)))) + ((2) \cdot (Fin . v a l (m)))) + (Fin . v a l (Fin . m o d N a t (2, 2, s))))), (0 : C))))) \cdot (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU)$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.renormS (✓ std3).

Commentary.

RenormS conjugates by the signed permutation and the two-site basis change, pinches equal sector labels, and sums the four-dimensional multiplicity index, matching the source’s S channel (main.tex l. 3149–3164). Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.6 (The two-to-four renormalization channel).

$\forall (y : Matrix (Fin (4), Fin (4), C)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . re n or m T (y) = ((Matrix . co nj T r an s p ose (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz x V)) \cdot (Matrix . o f (λ (r : Fin (16)) \mapsto (λ (s : Fin (16)) \mapsto (ite (Fin . d i v N a t (2, 8, r) = Fin . d i v N a t (2, 8, s), (((\frac{D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . n u}{D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . m u} : C)) \cdot ((1 : Matrix (Fin (4), Fin (4), C)) (Function . co m p (Fin . d i v N a t (4, 2), Fin . m o d N a t (2, 8), r), Function . co m p (Fin . d i v N a t (4, 2), Fin . m o d N a t (2, 8), s)))) \cdot ((((D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU) \cdot (y)) \cdot (Matrix . co nj T r an s p ose (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU))) (Fin . mk (((2) \cdot (Fin . v a l (Fin . d i v N a t (2, 8, r)))) + (Fin . v a l (Fin . m o d N a t (8, 2, r)))), Fin . mk (((2) \cdot (Fin . v a l (Fin . d i v N a t (2, 8, s)))) + (Fin . v a l (Fin . m o d N a t (8, 2, s)))))), (0 : C))))))) \cdot (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz x V)$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.renormT (✓ std3).

Commentary.

RenormT conjugates by the signed permutation, inserts the normalized multiplicity identity with scalar nu divided by mu, and restores the source tensor order, matching the source’s T channel (main.tex l. 3132–3147). The source multiplicity trace satisfies m_lambda = mu_lambda, so the common weight mu is used directly. Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.7 (The four-site channel).

$\forall (x : Matrix (Fin (16), Fin (16), C)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . l oc a lC hann e l (x) = D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . re n or m T (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . re n or m S (x))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.localChannel (✓ std3).

Commentary.

The local channel applies the four-to-two channel S, then the two-to-four channel T, as in the source’s E = T composed with S (main.tex l. 4951–4952).

Definition 1.8 (Cyclic site displacement).

$\forall (n : N), \forall (i : Fin (n)), \forall (k : N), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, k) = Fin . mk (Nat . m o d ((Fin . v a l (i)) + (k), n))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site (✓ std3).

Commentary.

Site i k is the cyclic displacement of i by the natural offset k. The result is represented by the residue modulo n. Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.9 (The four-bit window code).

$\forall (n : N), \forall (i : Fin (n)), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC o d e (i, x) = Fin . mk (((((8) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 0))))) + ((4) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 1)))))) + ((2) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 2)))))) + (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 3)))))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowCode (✓ std3).

Commentary.

WindowCode reads four consecutive cyclic bits, with the first site as the most significant bit, and packs them into Fin 16. Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.10 (Writing a window word).

$\forall (n : N), \forall (i : Fin (n)), \forall (x : (Fin (n)) \to (Fin (2))), \forall (p : Fin (16)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o w U p d a t e (i, x, p) = Function . u p d a t e (Function . u p d a t e (Function . u p d a t e (Function . u p d a t e (x, D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 0), Fin . mk (Nat . m o d (Nat . d i v (Fin . v a l (p), (2)^{3}), 2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 1), Fin . mk (Nat . m o d (Nat . d i v (Fin . v a l (p), (2)^{2}), 2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 2), Fin . mk (Nat . m o d (Nat . d i v (Fin . v a l (p), (2)^{1}), 2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 3), Fin . mk (Nat . m o d (Nat . d i v (Fin . v a l (p), (2)^{0}), 2)))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowUpdate (✓ std3).

Commentary.

WindowUpdate replaces the four cyclic window coordinates by the four binary digits of p, in most-significant-first order, and leaves all other coordinates unchanged. Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.11 (The translated local channel).

$\forall (n : N), \forall (i : Fin (n)), \forall (a : Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C)), \forall (x : (Fin (n)) \to (Fin (2))), \forall (y : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n) (i) (a, x, y) = p : Fin (16) \sum q : Fin (16) \sum (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . l oc a lC hann e l (Matrix . s in g l e (p, q, (1 : C))) (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC o d e (i, x), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC o d e (i, y))) \cdot (a (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o w U p d a t e (i, x, p), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o w U p d a t e (i, y, q)))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowChannel (✓ std3).

Commentary.

WindowChannel inserts the four-site local channel into a cyclic n-site matrix by summing over the input and output window words and updating the two matrix indices accordingly.

Definition 1.12 (The matrix of a window channel).

$\forall (n : N), \forall (i : Fin (n)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wS u p ero p er a t or (n) (i) = λ (x : (((Fin (n)) \to (Fin (2))) \times ((Fin (n)) \to (Fin (2))))) \mapsto (λ (y : (((Fin (n)) \to (Fin (2))) \times ((Fin (n)) \to (Fin (2))))) \mapsto (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, i, Matrix . s in g l e (Prod . f s t (y), Prod . s n d (y), (1 : C)), Prod . f s t (x), Prod . s n d (x))))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowSuperoperator (✓ std3).

Commentary.

WindowSuperoperator is the matrix-unit representation of a translated window channel on pairs of binary configurations.

Definition 1.13 (The parent Lindbladian).

$\forall (n : N), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . p a re n t L in d b l a d ian (n) = i \in Finset . f i lt er (λ (i : Fin (n)) \mapsto (Nat . m o d (Fin . v a l (i), 2) = 0), Finset . u ni v (Fin (n))) \sum ((D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wS u p ero p er a t or (n, i)) - ((1 : Matrix ((((Fin (n)) \to (Fin (2))) \times ((Fin (n)) \to (Fin (2)))), (((Fin (n)) \to (Fin (2))) \times ((Fin (n)) \to (Fin (2)))), C))))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.parentLindbladian (✓ std3).

Commentary.

The parent Lindbladian is the sum of the translated channel minus the identity over zero-based even starting sites, corresponding to the source’s odd-window sum after reindexing (main.tex l. 4951–4952). Nat.div denotes natural-number floor division and Nat.mod the remainder; Fin.divNat a b p and Fin.modNat a b p have values p.val / b and p.val % b, respectively.

Definition 1.14 (The tensor product of bit flips).

$\forall (n : N), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . t e n sor X (n) = λ (x : (Fin (n)) \to (Fin (2))) \mapsto (λ (y : (Fin (n)) \to (Fin (2))) \mapsto (ite (x = λ (j : Fin (n)) \mapsto ((y (j)) + (1)), (1 : C), (0 : C))))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.tensorX (✓ std3).

Commentary.

TensorX has one at the entry taking y to the configuration obtained by adding one in Fin 2 at every site, and zero elsewhere.

Definition 1.15 (The ring controlled-Z operator).

$\forall (n : N), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz (n) = Matrix . d ia g o na l (λ (x : (Fin (n)) \to (Fin (2))) \mapsto ((- (1 : C))^{\sum_{j : Fin (n)} (Fin . v a l (x (j))) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (j, 1))))}))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.cz (✓ std3).

Commentary.

Cz is diagonal, with phase minus one raised to the number of adjacent pairs of occupied bits around the cyclic ring.

Definition 1.16 (The CZX unitary).

$\forall (n : N), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz xU ni t a ry (n) = (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . cz (n)) \cdot (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . t e n sor X (n))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxUnitary (✓ std3).

Commentary.

The CZX unitary is the controlled-Z operator followed by the tensor product of bit flips, in the source order.

Definition 1.17 (Evolution under the parent generator).

$\forall (n : N), \forall (t : R), \forall (a : Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C)), \forall (x : (Fin (n)) \to (Fin (2))), \forall (y : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . e v o l u t i o n (n, t, a, x, y) = Matrix . m u l V ec (NormedSpace . e x p (((t : C)) \cdot (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . p a re n t L in d b l a d ian (n))), λ (p : (((Fin (n)) \to (Fin (2))) \times ((Fin (n)) \to (Fin (2))))) \mapsto (a (Prod . f s t (p), Prod . s n d (p)))) ((x, y))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.evolution (✓ std3).

Commentary.

Evolution applies the matrix exponential of t times the parent Lindbladian to the vector of matrix entries and evaluates it at a pair of configurations.

Definition 1.18 (The constant-sector gauge phase).

$\forall (n : N), \forall (e : Fin (2)), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e (n, e, x) = (- (1 : C))^{(Fin . v a l (e)) \cdot (\sum_{j : Fin (n)} (Fin . v a l (x (j))) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (j, 1)))))}$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gauge (✓ std3).

Source. Repository-derived.

Acknowledgement. Yuhan Liu; Alberto Ruiz-de-Alarcón; Georgios Styliaris; Xiao-Qi Sun; David Pérez-García; J. Ignacio Cirac (2026). Parent Lindbladians for matrix product density operators. DOI: 10.1103/1qyd-59z7. URL: https://arxiv.org/abs/2501.10552v2.

Commentary.

Gauge assigns to a bit e and configuration x the phase minus one raised to e times the cyclic nearest-neighbour occupation sum.

Theorem 1.19 (Distinct sites in a four-site window).

$\forall (n : N), (4 \leq n) \Rightarrow (\forall (i : Fin (n)), \forall (k : Fin (4)), \forall (l : Fin (4)), (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, Fin . v a l (k)) = D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, Fin . v a l (l))) \Leftrightarrow (k = l))$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

When n is at least four, the four cyclic positions from a fixed starting site are pairwise distinct. The proof cancels the common cyclic displacement modulo n.

Definition 1.20 (The window channel as a linear map).

$\forall (n : N), \forall (i : Fin (n)), \forall (a : Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o w L M (n, i) (a) = D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, i, a)$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowLM (✓ std3).

Source. Repository-derived.

Commentary.

WindowLM is the complex-linear endomorphism whose action on every matrix is windowChannel.

Definition 1.21 (A constant gauge window).

$\forall (n : N), \forall (i : Fin (n)), \forall (Δ : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g oo d Win d o w (i, Δ) = \forall (k : Fin (4)), Δ (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, Fin . v a l (k))) = Δ (i)$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.goodWindow (✓ std3).

Source. Repository-derived.

Commentary.

GoodWindow holds when the gauge difference is constant on the four sites of the window.

Definition 1.22 (The sector gauge phase).

$\forall (n : N), \forall (Δ : (Fin (n)) \to (Fin (2))), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . sec t or G a ug e (n, Δ, x) = (- (1 : C))^{\sum_{j : Fin (n)} ((Fin . v a l (Δ (j))) \cdot (Fin . v a l (x (j)))) \cdot (Fin . v a l (x (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (j, 1))))}$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge (✓ std3).

Source. Repository-derived.

Commentary.

SectorGauge is the product phase obtained by weighting every ring edge by the gauge difference at its source site.

Definition 1.23 (A gauged matrix unit).

$\forall (n : N), \forall (Δ : (Fin (n)) \to (Fin (2))), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e d U ni t (n, Δ, x) = (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . sec t or G a ug e (n, Δ, x)) \cdot (Matrix . s in g l e ((x) + (Δ), x, (1 : C)))$

Formalization. D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gaugedUnit (✓ std3).

Source. Repository-derived.

Commentary.

GaugedUnit is the sector phase times the matrix unit from x to x plus delta.

Theorem 1.24 (Constant sectors recover the gauge).

$\forall (n : N), \forall (e : Fin (2)), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . sec t or G a ug e (n, Function . co n s t (Fin (n), e), x) = D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e (n, e, x)$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge_const (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a constant difference, distributing the constant over the finite sum identifies sectorGauge with gauge.

Theorem 1.25 (The gauge phase is self-inverse).

$\forall (n : N), \forall (Δ : (Fin (n)) \to (Fin (2))), \forall (x : (Fin (n)) \to (Fin (2))), (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . sec t or G a ug e (n, Δ, x)) \cdot (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . sec t or G a ug e (n, Δ, x)) = (1 : C)$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge_mul_self (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every sector gauge phase squares to one because its exponent is an integer and the sign square identity applies.

Theorem 1.26 (The successor site map is injective).

$\forall (n : N), Function . I nj ec t i v e (λ (i : Fin (n)) \mapsto (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 1)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site_succ_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cyclic successor map is injective for every nonempty Fin n. The proof uses the additive inverse in Fin n after establishing n is nonzero from an index.

Theorem 1.27 (The gauged window action).

$\forall (n : N), (4 \leq n) \Rightarrow (\forall (i : Fin (n)), \forall (Δ : (Fin (n)) \to (Fin (2))), \forall (x : (Fin (n)) \to (Fin (2))), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, i, D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e d U ni t (n, Δ, x)) = ite D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g oo d Win d o w (i, Δ), (((4 : C))^{- 1}) \cdot (b : Fin (2) \sum c : Fin (2) \sum D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e d U ni t (n, Δ, Function . u p d a t e (Function . u p d a t e (x, D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 1), b), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . s i t e (i, 2), c))), (0 : Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gauged_window_sector (✓ std3). ∎

Source. Repository-derived.

Commentary.

On a good window, the gauge converts the local channel into the uniform average over the two middle bits; on a bad window the action is zero. The phase change on the three affected edges cancels using the self-inverse gauge phase.

Theorem 1.28 (Gauged units span the matrix space).

$\forall (n : N), \forall (f : Module . E n d (C, Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C))), \forall (g : Module . E n d (C, Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C))), (\forall (Δ : (Fin (n)) \to (Fin (2))), \forall (x : (Fin (n)) \to (Fin (2))), f (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e d U ni t (n, Δ, x)) = g (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . g a ug e d U ni t (n, Δ, x))) \Rightarrow (f = g)$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.matrix_linearMap_ext_gauged (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two complex-linear endomorphisms agreeing on every gauged unit agree everywhere. Each standard matrix unit is a self-product of a sector phase times one gauged unit, so the standard matrix basis extension applies.

Theorem 1.29 (Translated window channels commute).

$\forall (n : N), (4 \leq n) \Rightarrow (\forall (i : Fin (n)), \forall (j : Fin (n)), \forall (a : Matrix ((Fin (n)) \to (Fin (2)), (Fin (n)) \to (Fin (2)), C)), D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, i, D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, j, a)) = D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, j, D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wC hann e l (n, i, a)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_channels_commute (✓ std3). ∎

Source. Repository-derived.

Commentary.

The gauged-unit action identifies each good window channel with an average over its two middle coordinates. The coordinate averages commute, and the four cases of good or bad windows give equality for every matrix.

Theorem 1.30 (The window superoperator action).

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_superoperator_action (✓ std3). ∎

Source. Repository-derived.

Commentary.

Applying LinearMap.toMatrix_mulVec_repr to windowLM in Matrix.stdBasis identifies the matrix-vector action of windowSuperoperator with windowChannel entrywise.

Theorem 1.31 (Idempotence of a window superoperator).

$\forall (n : N), (4 \leq n) \Rightarrow (\forall (i : Fin (n)), IsIdempotentElem (D5 . S 3 . Q u an t u m . T e n sor N e tw or k s . CZXP a re n t L in d b l a d ianWin d o wC hann e l . w in d o wS u p ero p er a t or (n, i)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_idempotent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The local channel is idempotent on matrix units; the window channel therefore composes with itself to itself. The preceding action formula transfers this identity to the window superoperator.

References

Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.cz
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxU
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxUnitary
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.czxV
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.evolution
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gauge
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gaugedUnit
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.gauged_window_sector
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.goodWindow
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.localChannel
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.matrix_linearMap_ext_gauged
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.mu
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.nu
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.parentLindbladian
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.renormS
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.renormT
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge_const
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.sectorGauge_mul_self
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site_injective
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.site_succ_injective
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.tensorX
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowChannel
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowCode
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowLM
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowSuperoperator
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.windowUpdate
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_channels_commute
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_idempotent
Truth anchor: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianWindowChannel.window_superoperator_action
Dependency: D5/S3/Quantum/TensorNetworks/CZXParentLindbladianAveraging

Keyboard shortcuts

trureturing — Discovering truth

CZX parent-Lindbladian window channel

Abstract

References