Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Corollary 10.4.2.2Canonical Form II unitary refinement in the equal case

Let $P$ and $Q$ be BNT canonical forms whose total tensors generate the same MPV family at every positive length. Assume every listed sector has a positive number of copies and every copy weight is nonzero, as in Definition 9.6.1.13. Their total bond dimensions agree; writing the common value as $D$, there is a unitary matrix $U\in \mathrm{U}(D)$ such that, for every physical index $i$,

\begin{align} Q_{\mathrm{tot}}^i & = U P_{\mathrm{tot}}^i U^\dagger . \notag \end{align}

LaTeX Lean

Corollary 10.4.1.3Canonical Form II unitary refinement of proportional matching

Under the hypotheses of Theorem 10.4.1, there exist a bijection $\beta :J(Q)\simeq J(P)$, unitary matrices $U_k\in \mathrm{U}(\dim Q_k)$, and phases $\zeta _k\in \mathbb {C}$ with $|\zeta _k|=1$, such that $\dim P_{\beta (k)}=\dim Q_k$ and, for every $k$ and every physical index $i$,

\begin{align} Q_k^i & =\zeta _k\, U_k\, P_{\beta (k)}^i\, U_k^\dagger . \notag \end{align}

This is the proportional part of [ CPGSV16 , Corollary A.6, lines 1197–1199 ] .

LaTeX Lean

Definition 2.5.7Block-diagonal tensor from blocks

Given $r$ blocks with bond dimensions $(D_k)_{k=1}^r$, per-block tensors $\{ A_k^i\} $, and scaling factors $(\mu _k)_{k=1}^r$, the associated block-diagonal tensor is the tensor of total bond dimension $D = \sum _{k=1}^r D_k$ defined by

\begin{align} A^i & = \bigoplus _{k=1}^{r} \mu _k A_k^i. \notag \end{align}

LaTeX Lean

Definition 2.3.12Gauge-phase equivalence

Two tensors $A$ and $B$ are gauge-phase equivalent if there exist $X \in \mathrm{GL}_D(\mathbb {C})$ and $\zeta \in \mathbb {C}\setminus \{ 0\} $ such that, for every physical index $i$,

\begin{align} B^i & = \zeta X A^i X^{-1}. \label{eq:mps_gauge_phase_equiv} \end{align}

LaTeX

Lean

MPSTensor.GaugePhaseEquiv
MPSTensor.GaugeEquiv.toGaugePhaseEquiv

Definition 10.3.1Flattened block-diagonal gauge

Given per-block gauges $X_k \in \mathrm{GL}_{D_k}(\mathbb {C})$, form the block-diagonal element $\bigoplus _k X_k$ and then reindex the dependent block-coordinate space with the standard bond index $\{ 0,\ldots ,\sum _k D_k-1\} $ of the assembled tensor. The result is an element of $\mathrm{GL}_{\sum _k D_k}(\mathbb {C})$.

LaTeX

Lean

MPSTensor.blockDiagonalGL
MPSTensor.globalGaugeOfBlocks

Definition 8.1.1.1Irreducible tensor

An MPS tensor $A$ is irreducible if it has no nontrivial invariant projection.

LaTeX Lean

Definition 5.4.1Left-canonical normalization

An MPS tensor $A=(A^i)_i$ is left-canonical when

\begin{align} \sum _i (A^i)^\dagger A^i & =\mathbb {1}. \notag \end{align}

Equivalently, its Kraus map is trace-preserving.

LaTeX Lean

Definition 2.3.4Positive-length same MPV - different bond dimensions

For tensors $A$ and $B$ of possibly different bond dimensions, we write $\mathcal{V}^+(A) = \mathcal{V}^+(B)$ if $|V^{(N)}(A)\rangle = |V^{(N)}(B)\rangle $ for every $N {\gt} 0$.

LaTeX Lean

Definition 9.6.1.13BNT canonical form

Given a sector decomposition $P$, these conditions define the normalized, left-canonical, aperiodic BNT surface used below. This is stronger than the abstract BNT of Definition 9.1.1 and the literal coefficient-form BNT of Definition 9.1.2: besides spanning and eventual linear independence, it fixes irreducible left-canonical representatives, their self-overlap normalization, gauge-phase separation, and the canonical-form weight normalization. It imposes no equal-modulus factorization or strict ordering on the raw weights. Explicitly, each basis block has positive bond dimension, is irreducible, and is left-canonical; the normalized self-overlap of every basis block converges to $1$; the basis MPV family is eventually linearly independent; distinct same-dimension basis blocks are not gauge-phase equivalent after identifying equal bond dimensions; and the [ CPGSV16 , Section 2.3 ] canonical-form normalization holds,

\begin{align} \forall (j,q),\quad & |\mu _{j,q}| \le 1, \notag \\ \exists \, (j_*,q_*),\quad & |\mu _{j_*,q_*}| = 1. \notag \end{align}

The MPV expansion takes the raw two-layer form

\begin{align} V^{(N)}(P)_\sigma & = \sum _{j=1}^{g} \left(\sum _{q=1}^{r_j} \mu _{j,q}^N\right) V^{(N)}(P_j)_\sigma , \label{eq:bnt_sector_raw_expansion} \end{align}

matching [ CPGSV16 , Section 2.3 ] and [ CPGSV21 , Definition IV.2 ] . The canonical-form normalization admits every example of the source paper (in particular $C \oplus D$, $C \oplus (-C)$, $C \oplus (1/2) C$, and $C \oplus (-C) \oplus (1/2) C$) and is not derivable from the per-block normality hypotheses alone.

LaTeX Lean

Definition 10.2.3Copy-weight matching for matched BNT sectors

Let the sectors of two decompositions $P$ and $Q$ be matched by $\beta :J(Q)\simeq J(P)$, with sector phases $\zeta _k$. A copy-weight matching consists of copy permutations $\tau _k$ such that, for all sectors $k$ and copies $q$, $\nu _{k,q}=\zeta _k^{-1}\mu _{\beta (k),\tau _k(q)}$. This is the copy-level conclusion of [ CPGSV16 , Appendix MPV proof, line 1188 ] .

LaTeX Lean

Definition 10.2.4Copy-weight matching from matched-sector coefficient identities

The construction takes as input a sector matching $\beta :J(Q)\simeq J(P)$, nonzero sector phases $\zeta _k$, and the eventual matched-sector coefficient identities

\begin{align} c_N^{(\beta (k))}(P) & = \zeta _k^N\, c_N^{(k)}(Q). \label{eq:ft_sector_coeff_identity_hyp} \end{align}

It returns the copy-weight matching obtained by choosing, in every sector, a copy permutation $\tau _k$ satisfying $\nu _{k,q}=\zeta _k^{-1}\mu _{\beta (k),\tau _k(q)}$. This is the sectorwise construction in [ CPGSV16 , Appendix MPV proof, line 1188 ] .

LaTeX Lean

Lemma E.1.11Eventual coefficient extraction from linear independence

If a finite family of vectors is linearly independent for all sufficiently large $N$, and two finite linear combinations of that family are equal for all sufficiently large $N$, then the corresponding coefficients are equal for all sufficiently large $N$.

LaTeX Lean

Lemma 10.4.1.1Phase normalization for an irreducible gauge

Let $A$ and $B$ be left-canonical tensors of common positive bond dimension, with $B$ irreducible. If $X$ is invertible, $\zeta \ne 0$, and $B^i=\zeta XA^iX^{-1}$ for every $i$, then $|\zeta |=1$.

LaTeX Lean

Lemma 10.4.1.2Unitary replacement with the same phase

Let $A$ and $B$ be left-canonical irreducible tensors of common positive bond dimension satisfying $B^i=\zeta XA^iX^{-1}$ for an invertible $X$ and a nonzero scalar $\zeta $. There is a unitary matrix $U$, with the same scalar $\zeta $, such that $|\zeta |=1$ and $B^i=\zeta UA^iU^\dagger $ for every $i$.

LaTeX Lean

Lemma F.8.1Unitary gauge for left-canonical irreducible tensors

Let $A$ and $B$ be left-canonical irreducible tensors of common positive bond dimension that are gauge-phase equivalent. Then the gauge can be taken unitary: there are a unitary matrix $U$ and a scalar $\zeta $ with $|\zeta |=1$ such that, for every physical index $i$,

\begin{align} B^i & =\zeta \, UA^iU^\dagger . \notag \end{align}

LaTeX Lean

Lemma 10.2.2Full-basis coefficient identity from matched phases

Let $P$ be a BNT canonical form, let $Q$ be a sector decomposition, and assume $P_{\mathrm{tot}}$ and $Q_{\mathrm{tot}}$ have the same MPV family at every positive length. Suppose that there is a bijection $\beta :J(Q)\simeq J(P)$ and scalars $\zeta _k \in \mathbb {C}$ such that, for every $k \in J(Q)$, every positive length $N$, and every spin configuration $\sigma $ of length $N$,

\begin{align} V^{(N)}(Q_k)_\sigma & = \zeta _k^N\, V^{(N)}(P_{\beta (k)})_\sigma . \label{eq:ft_phase_relation_hyp} \end{align}

Then for every $k \in J(Q)$ there is $N_0$ such that, for all $N{\gt}N_0$, $c_N^{(\beta (k))}(P)=\zeta _k^N\, c_N^{(k)}(Q)$. This is the coefficient-comparison step of [ CPGSV16 , Appendix MPV proof, lines 1187–1188 ] in full-basis form.

LaTeX Lean

Lemma 10.3.3Equal-MPV matched copy-weight witnesses

Let $P$ and $Q$ be BNT canonical forms whose total tensors have the same MPV family at every positive length. Then there are a bijection $\beta :J(Q)\simeq J(P)$, bond-dimension equalities, unit-modulus phases $\zeta _k$, and block gauges $X_k$ such that $Q_k^i=\zeta _k X_kP_{\beta (k)}^iX_k^{-1}$. For the same phases there is a copy-weight matching: after a permutation of the copies inside each matched sector, $\nu _{k,q}=\zeta _k^{-1}\mu _{\beta (k),\tau _k(q)}$.

LaTeX Lean

Lemma F.8.2Unitary gauge in matched sector coordinates

Let $P$ and $Q$ be BNT canonical forms whose total tensors generate the same MPV family at every positive length. There are a sector bijection $\beta $, copy bijections $\tau _k$, phases $\zeta _k$, sector unitaries $U_k$, and a unitary block-diagonal matrix $X$ such that

\begin{align} Q_k^i & = \zeta _k U_kP_{\beta (k)}^iU_k^\dagger , \notag \\ \nu _{k,q} & = \zeta _k^{-1}\mu _{\beta (k),\tau _k(q)}, \notag \\ |\zeta _k| & = 1. \notag \end{align}

The matched sectors and copies have equal bond dimensions and multiplicities. If $P_{\mathrm{match}}$ denotes the corresponding reordered block assembly, then $Q_{\mathrm{flat}}^i=XP_{\mathrm{match}}^iX^{-1}$.

LaTeX Lean

Lemma 9.7.1.2Matched-sector weight-permutation extractor

Under the hypotheses of Lemma 9.7.1.1, the per-sector multiplicities agree and there is a permutation $\tau $ of the per-copy index set identifying the individual weights up to the gauge phase: for every $q$, $\nu _{\tilde k_0, \tau (q)} = \zeta ^{-1} \cdot \mu _{j_0, q}$. This is the per-copy realisation of [ CPGSV16 , Appendix A ] : the multiset equality from Lemma 9.7.1.1 is upgraded to a concrete indexing between the matched $P$- and $Q$-copies.

LaTeX Lean

Lemma F.1.2Unit phase from matched normalized BNT blocks

Let $P$ and $Q$ be BNT canonical forms. If, for every positive length $N$ and word $\sigma $, a sector $P_j$ and a sector $Q_k$ have MPV families related by

\begin{align} V^{(N)}(Q_k)_\sigma & = \zeta ^N V^{(N)}(P_j)_\sigma , \label{eq:ft_matched_mpv_phase_norm} \end{align}

then $|\zeta |=1$.

LaTeX Lean

Lemma F.4.3Direct-sum conjugation by the flattened gauge

If, for every block $k$ and physical index $i$, $B_k^i=X_kA_k^iX_k^{-1}$, then the weighted direct sums satisfy

\begin{align} \bigoplus _k \mu _k B_k^i & = X\left(\bigoplus _k \mu _k A_k^i\right)X^{-1}, \notag \end{align}

where $X$ is the flattened block-diagonal gauge from Definition 10.3.1. Hence the two assembled tensors are gauge equivalent.

LaTeX

Lean

MPSTensor.toTensorFromBlocks_eq_globalGaugeOfBlocks_conj
MPSTensor.gaugeEquiv_toTensorFromBlocks_of_blockConj

Theorem 10.4.2.1Equal BNT canonical forms are globally conjugate

Let $P$ and $Q$ be BNT canonical forms (Definition 9.6.1.13) whose total tensors $P_{\mathrm{tot}}$, $Q_{\mathrm{tot}}$ generate the same MPV family for every positive system size $N$. Every listed sector has a positive number of copies and every copy weight is nonzero. Then their total bond dimensions coincide; writing the common value as $D$, there is one invertible matrix $X\in \mathrm{GL}_D(\mathbb {C})$ such that, for every physical index $i$,

\begin{align} Q_{\mathrm{tot}}^i & =X\, P_{\mathrm{tot}}^i\, X^{-1}. \notag \end{align}

LaTeX Lean

Theorem 10.4.1Multi-block fundamental theorem for normal tensors

Let $P$ and $Q$ be BNT canonical forms (Definition 9.6.1.13), with bases of normal tensors $(P_j)_{j=1}^{g_a}$ and $(Q_k)_{k=1}^{g_b}$. Every listed sector has a positive number of copies, and every copy weight is nonzero. If the total tensors $P_{\mathrm{tot}}$, $Q_{\mathrm{tot}}$ generate eventually nonzero proportional MPV families — for all sufficiently large $N$ there is a nonzero scalar $c_N$ with $V^{(N)}(P_{\mathrm{tot}})=c_NV^{(N)}(Q_{\mathrm{tot}})$ — then $g_a=g_b$. After relabelling the basis of normal tensors of $P$ by a bijection $\beta :J(Q)\simeq J(P)$, there are scalars $\zeta _k\in \mathbb {C}$ with $|\zeta _k|=1$ and invertible matrices $Y_k$ such that, for every $k$ and every physical index $i$,

\begin{align} Q_k^i & =\zeta _k\, Y_k\, P_{\beta (k)}^i\, Y_k^{-1}. \notag \end{align}

Thus the paired normal tensors have the same bond dimension ($\dim P_{\beta (k)}=\dim Q_k$) and the same gauge-phase class.

LaTeX Lean

Theorem 10.2.5Equal-case sector and copy matching with differing bond dimensions

Let $P$ and $Q$ be BNT canonical forms, possibly with different sector counts and different bond dimensions before matching. If their total tensors generate the same MPV family at every positive length, then there is a bijection $\beta :J(Q)\simeq J(P)$ such that each matched basis pair has equal bond dimension and is gauge-phase equivalent. The matched copy multiplicities agree, and there are unit phases $\zeta _k$ and copy bijections $\tau _k$ satisfying

\begin{align} Q_k^i & =\zeta _kX_kP_{\beta (k)}^iX_k^{-1}, \notag \\ \nu _{k,q} & =\zeta _k^{-1}\mu _{\beta (k),\tau _k(q)}. \notag \end{align}

Only the global weight normalization in Definition 9.6.1.13 is assumed; no unit-modulus copy is required in each sector. This is the sector-data form of [ CPGSV16 , Corollary 2.11 and Appendix A, lines 1182–1188 ] .

LaTeX Lean

Theorem 10.1.1Paired component maps for products of matrix algebras

For a ring equivalence between products of full matrix algebras, the map induced between each pair of matched components is bijective.

LaTeX

Lean

MPSTensor.ringEquiv_maps_single_support
MPSTensor.componentMap_surjective
MPSTensor.componentMap_bijective

Theorem 10.1.2Dimension preservation for matched matrix summands

An algebra automorphism of a product of full matrix algebras preserves the dimension of every pair of summands matched by its induced permutation.

LaTeX Lean

Theorem 5.2.1Irreducible fixed-point uniqueness

Let $A$ be an MPS tensor whose transfer map is irreducible. If $\rho ,\sigma \geq 0$ are fixed points of $\mathcal{E}_A$ and $\rho \neq 0$, then $\sigma =c\rho $ for some $c\in \mathbb {C}$.

LaTeX Lean

Theorem 9.8.1.1Bijective matching by symmetry

Let $P, Q$ be two BNT canonical forms with the same MPV family at every positive length. Then there is a bijection $\beta : J(Q) \simeq J(P)$ such that for every $k \in J(Q)$ the bond dimensions match, the basis tensors $P_{\beta (k)}$ and $Q_k$ are gauge-phase equivalent after identifying the matched bond dimensions, and the basis cross-overlap does not tend to zero.

LaTeX Lean

Theorem 10.3.4Full-basis global gauge in matched coordinates

Let $P$ and $Q$ be BNT canonical forms whose total tensors have the same MPV family at every positive length. Then there exist:

a bijection $\beta :J(Q)\simeq J(P)$,
bond-dimension equalities $\dim P_{\beta (k)}=\dim Q_k$,
copy-number equalities $r_{\beta (k)}(P)=r_k(Q)$ and copy permutations $\tau _k$,
unit-modulus phases $\zeta _k$ with $|\zeta _k|=1$ and block gauges $X_k$,

such that, for every sector $k$, copy $q$, and physical index $i$,

\begin{align} Q_k^i & = \zeta _k\, X_k P_{\beta (k)}^i X_k^{-1}, \notag \\ \nu _{k,q} & = \zeta _k^{-1} \mu _{\beta (k),\tau _k(q)}. \notag \end{align}

Moreover, if $X=\bigoplus _k (\mathbf{1}_{r_k}\otimes X_k)$ is the flattened block-diagonal gauge, then, for every physical index $i$, the flattened $Q$-coordinates satisfy

\begin{align} Q_{\mathrm{flat}}^i & = X\, P_{\mathrm{matched}}^i\, X^{-1}. \notag \end{align}

This is the explicit direct-sum gauge construction of [ CPGSV16 , Appendix MPV proof, lines 1189–1192 ] .

LaTeX Lean

Theorem 10.3.5Literal equal-MPV gauge after sector-coordinate permutation

Let $P$ and $Q$ be BNT canonical forms whose total tensors have the same MPV family at every positive length. Then the total bond dimensions agree; write their common value as $D$. There is

\begin{align} Y & \in \mathrm{GL}_D(\mathbb {C}) \label{eq:ft_literal_gauge_Y} \end{align}

such that, for every physical index $i$,

\begin{align} Q_{\mathrm{tot}}^i & = Y\, P_{\mathrm{tot}}^i\, Y^{-1}, \notag \end{align}

where $P_{\mathrm{tot}}^i$ and $Q_{\mathrm{tot}}^i$ are both regarded as matrices in $M_{D}(\mathbb {C})$ using the total bond-dimension equality. This is the BNT form of [ CPGSV16 , Corollary 2.11 and Appendix A, lines 1189–1192 ] .

LaTeX Lean

Theorem F.4.4Global gauge from a copy-weight matching

Suppose that the sectors of $P$ and $Q$ are matched, with bond-dimension equalities, nonzero phases, and block gauges satisfying $Q_k^i=\zeta _k X_kP_{\beta (k)}^iX_k^{-1}$. If the same phases also give a copy-weight matching, then the flattened $Q$-tensor is obtained from the matched-coordinate $P$-tensor by the direct-sum gauge $X=\bigoplus _k(\mathbf{1}_{r_k}\otimes X_k)$. This is only a reformulation of Theorem 10.3.2.

LaTeX Lean

Theorem 10.3.2Global gauge from matched sectors and copy weights

Suppose that the sectors of two sector decompositions $P$ and $Q$ are matched by a bijection $\beta :J(Q)\simeq J(P)$, with bond-dimension equalities, copy permutations $\tau _k$, nonzero phases $\zeta _k$, and block gauges $X_k$. If, for every sector $k$, copy $q$, and physical index $i$,

\begin{align} Q_k^i & = \zeta _k\, X_k P_{\beta (k)}^i X_k^{-1}, \notag \\ \nu _{k,q} & = \zeta _k^{-1} \mu _{\beta (k),\tau _k(q)}, \label{eq:ft_matched_weights_hypotheses} \end{align}

then, in the flattened $Q$-coordinates,

\begin{align} Q_{\mathrm{flat}}^i & = X\, P_{\mathrm{matched}}^i\, X^{-1}, \notag \\ X & = \bigoplus _k(\mathbf{1}_{r_k}\otimes X_k). \notag \end{align}

This is the direct-sum gauge construction of [ CPGSV16 , Appendix MPV proof, lines 1189–1192 ] , separated from the coefficient-comparison step that supplies the weight identities.

LaTeX Lean

Theorem F.1.1Bijective matching under eventual proportionality

Let $P$ and $Q$ be BNT canonical forms whose total MPV families are eventually nonzero and proportional. There is a bijection $\beta :J(Q)\simeq J(P)$ such that every $Q_k$ has an equal-dimensional, gauge-phase-equivalent partner $P_{\beta (k)}$ satisfying

\begin{align} O_{P_{\beta (k)}Q_k}(N) & \not\longrightarrow 0. \notag \end{align}

LaTeX Lean

Theorem 10.2.1Proportional sector matching with unit phases

Let $P$ and $Q$ be BNT canonical forms whose total tensors generate eventually nonzero proportional MPV families. Then there are a bijection $\beta :J(Q)\simeq J(P)$, bond-dimension equalities $\dim P_{\beta (k)}=\dim Q_k$, scalars $\zeta _k\in \mathbb {C}$, and block gauges $X_k$ such that $|\zeta _k|=1$ and, for every sector $k$ and physical index $i$,

\begin{align} Q_k^i & = \zeta _k X_k P_{\beta (k)}^i X_k^{-1}. \label{eq:ft_gauge_relation} \end{align}

Diagrammatically, the gauge relation (1) reads

$\begin{tenkz}[rows={wire}, cols=1, west=open, east=open] \tn[label pos=s, ports={90:physical:$i$}]{Q_k} \end{tenkz}$ $ = \zeta _k$ $\begin{tenkz}[rows={wire}, cols=3, west=open, east=open] \tn[skin=ring]{X_k} & \tn[label pos=s, ports={90:physical:$i$}]{P_{\beta(k)}} & \tn[skin=ring]{X_k^{-1}} \end{tenkz}$

with every open virtual end a matrix index. Equivalently, for every positive length $N$ and word $\sigma $,

\begin{align} V^{(N)}(Q_k)_\sigma & = \zeta _k^N V^{(N)}(P_{\beta (k)})_\sigma . \notag \end{align}

This is [ CPGSV16 , Appendix MPV theorem statement, lines 1167–1170, and proof line 1182 ] .

LaTeX Lean