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

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 F.6.1Matched weights, tensors, and repeated gauges

The matched flattened data are the functions $\widetilde\mu $, $\widetilde P$, and $(k,q)\mapsto X_k$ defined above on the flattened copy coordinates of $Q$.

LaTeX

Lean

MPSTensor.matched_p_weight
MPSTensor.matched_p_basis
MPSTensor.matched_block_gauge

Definition F.7.1Invertible permutation gauge

For a permutation $\rho $ of a finite bond-index set, let $\Pi _\rho $ be its permutation matrix. The corresponding element of the general linear group is denoted $G_\rho $.

LaTeX Lean

Definition F.6.3Sector and bond-coordinate equivalences

The sector bijection, copy bijections, and bond-dimension equalities induce an equivalence of the dependent triples $(j,q,a)$ and $(k,q',a')$. After flattening the dependent bond coordinate, this gives an equivalence of the standard total bond-index sets.

LaTeX

Lean

MPSTensor.SectorDecomposition.sectorFlatSigmaEquiv
MPSTensor.SectorDecomposition.sectorFlatDimEquiv

Definition 2.3.1Gauge equivalence

Two tensors $A$ and $B$ of the same bond dimension $D$ are gauge equivalent if there exists an invertible matrix $X \in \mathrm{GL}_D(\mathbb {C})$ such that, for every $i \in \{ 0,\ldots ,d{-}1\} $,

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

In tensor-network notation, (5) is represented by

$\begin{tenkz}[boundary=open] \tn[skin=ring]{X} & \tn[ports={90:physical:$i$}]{A} & \tn[skin=ring]{X^{-1}} \end{tenkz}$

where the black node denotes the tensor $A$, the upper leg is the physical index $i$, and the two red side nodes denote the gauge matrices acting on the virtual legs.

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 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

Definition F.4.1Invertible matrix associated to a unitary

A unitary matrix $U$ determines an invertible matrix whose inverse is $U^\dagger $.

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 F.7.2Matrix and inverse identities for a permutation gauge

The matrix of $G_\rho $ is $\Pi _\rho $, and the matrix of its inverse is $\Pi _{\rho ^{-1}}$.

LaTeX

Lean

MPSTensor.permGL_val
MPSTensor.permGL_inv_val

Lemma F.7.3Permutation conjugation reindexes both coordinates

For a permutation $\rho $ and a square matrix $M$, conjugation by the permutation matrix reindexes both coordinates by $\rho $:

\begin{align} \Pi _\rho M\Pi _{\rho ^{-1}} & =\bigl(M_{\rho (i),\rho (j)}\bigr)_{i,j}. \label{eq:app_ft_perm_conjugation} \end{align}

Equivalently, the right-hand side is the submatrix of $M$ along $\rho \times \rho $.

LaTeX Lean

Lemma F.6.2Equality of the matched total bond dimensions

If matched sectors have equal bond dimensions and matched copy sets are bijective, then $P$ and $Q$ have the same total bond dimension.

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 E.2.1.3Bijection from matches in both directions

Suppose every sector of $Q$ has an equal-dimensional, gauge-phase-equivalent partner in $P$ with non-decaying overlap, and the converse holds from $P$ to $Q$. Then the forward partners may be chosen as a bijection between the two finite sector sets, preserving all three properties.

LaTeX Lean

Lemma F.2.1Full-basis coefficient identity from matched sectors

Let $P$ and $Q$ be BNT canonical forms with the same MPV family at every positive length, matched by a bijection $\beta :J(Q)\simeq J(P)$ with bond-dimension equalities and a gauge-phase equivalence between $Q_k$ and $P_{\beta (k)}$ for every $k$. Then each sector carries a unit-modulus phase $\zeta _k$, and eventually

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

This is the equal-MPV coefficient comparison of [ CPGSV16 , Appendix MPV proof, lines 1187–1188 ] .

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 F.3.1Proportional matched-phase coefficient identity, scalar-threaded

Let $P$ be a BNT canonical form and $Q$ a sector decomposition whose total tensors generate eventually nonzero proportional MPV families. Suppose a bijection $\beta :J(Q)\simeq J(P)$ and scalars $\zeta _k$ satisfy the matched MPV phase identities (2) for every sector $k$. Then there is a single eventually-nonzero scalar sequence $c_N$ and a threshold $N_0$ such that, for all $N{\gt}N_0$ and every $k\in J(Q)$,

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

The scalar $c_N$ is the same for every sector $k$: it is the single global proportionality scalar of [ CPGSV16 , Theorem thm1, lines 1167–1170 ] at length $N$.

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 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

Lemma F.4.2Unitary block-diagonal gauges

If every block gauge $U_k$ is unitary, then the flattened block-diagonal gauge $U=\bigoplus _k U_k$ is unitary.

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 F.6.4Equal-MPV gauge with all matched witnesses

Under the hypotheses of the equal-MPV theorem, one may choose simultaneously the sector bijection, bond-dimension equalities, copy bijections, phases, block gauges, total-dimension equality, and the flattened global gauge. They satisfy the matched block and weight identities of Theorem 10.3.4, together with the conjugation of $Q$ by the matched-coordinate $P$-tensor.

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 E.2.1.2Full-basis matching under eventual proportionality

Under the same hypotheses, every sector of $Q$ has an equal-dimensional, gauge-phase-equivalent partner in $P$ with non-decaying cross-overlap.

LaTeX Lean

Theorem F.5.2Additional proportional global gauge under coefficient identities

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, 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 every sector $k$ and physical index $i$. If one additionally assumes that these same phases satisfy the matched-sector coefficient identities $c_N^{(\beta (k))}(P)=\zeta _k^N\, c_N^{(k)}(Q)$ for all sufficiently large $N$, then they determine a copy-weight matching and hence 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)$.

LaTeX Lean

Theorem F.5.1Additional proportional global gauge under copy-weight matching

Let $P$ and $Q$ be BNT canonical forms whose total tensors generate eventually nonzero proportional MPV families. Then the proportional sector-matching theorem gives $\beta $, the bond-dimension equalities, the unit phases $\zeta _k$, and the block gauges $X_k$. If one additionally assumes a copy-weight matching for these same phases, 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)$.

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