Unnumbered main construction: RAGE contains MPS and weighted-graph/product-superposition states

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.rage_contains_mps_wgs_products

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

prove2quantum

Let $N,D\ge1$ . For site matrices $A_{k,b}\in\mathbb C^{D\times D}$ , let $M(A)$ have amplitudes $\operatorname{tr}(A_{1,b_1}\cdots A_{N,b_N})$ . Let $W_\Phi$ apply $\operatorname{diag}(1,1,1,e^{i\Phi_{jk}})$ once per unordered pair, where $\Phi$ is symmetric, has zero diagonal, and has entries in $[0,2\pi)$ . Let $V=\bigotimes_k V_k$ , $V_k\in U(2)$ , and set $R(A,\Phi,V)=VW_\Phi M(A)$ . Then

R(A,0,I)=M(A),\qquad R(A(r),\Phi,V)=VW_\Phi\bigotimes_k|+\rangle.

Here the second equality uses bond-one tensors with both local amplitudes $1/\sqrt2$ . More generally, for $m\ge1$ , arbitrary coefficients $c_t$ , and arbitrary product factors $r_{t,k}(b)$ , the diagonal tensors $B_{k,b}(t,t)=r_{t,k}(b)$ , with an additional factor $c_t$ at the first site, satisfy

R(B,\Phi,V)=VW_\Phi\sum_{t=1}^m c_t\bigotimes_k r_{t,k}.

These are exact raw-vector containments, with one common graph and rotation family. Physical states are obtained by normalizing nonzero vectors. In Eq.(3), the factors $\eta(d)$ have amplitudes $(1,e^d)$ ; the conflicting first-line exponent is not asserted.

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 pp.1–2, Eqs.(1)–(3): exact raw-vector containments, including finite
superpositions under one common graph and common rotations. Only the unambiguous second
line of Eq.(3) is used; its conflicting first-line quadratic exponent is deferred. -/
theorem rage_contains_mps_wgs_products {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ) :
    rage A (emptyPhaseGraph N) (fun _ => 1) = traceMPS A ∧
    rage (productTensors (plusFactors N)) G V =
      enhance G V (productVec (plusFactors N)) ∧
    (∀ (m : ℕ), 1 ≤ m → ∀ (c : Fin m → ℂ)
      (r : Fin m → Fin N → Bool → ℂ),
      rage (diagonalTensors c r) G V = enhance G V (∑ t, c t • productVec (r t))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 1, Unnumbered main construction: RAGE contains MPS and weighted-graph/product-superposition states

Read-back

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

For all natural numbers $N,D$ satisfying $1\le N$ and $1\le D$ , every family $A_{k,b}$ of complex $D\times D$ matrices indexed by sites $k<N$ and Booleans $b$ , every real weight function $w_{jk}$ satisfying $w_{jk}=w_{kj}$ , $w_{jj}=0$ , and $0\le w_{jk}<2\pi$ , and every family of unitary $2\times2$ complex matrices $V_k$ with Boolean row and column indices, the following three statements hold jointly. For a bit string $a\in\{\mathrm{false},\mathrm{true}\}^N$ , write

M_A(a)=\operatorname{tr}\!\left(A_{0,a_0}A_{1,a_1}\cdots A_{N-1,a_{N-1}}\right), \qquad E_{w,V}(v)(b)= \sum_{a\in\{\mathrm{false},\mathrm{true}\}^N} \left(\prod_{k=0}^{N-1}(V_k)_{b_k,a_k}\right) \exp\!\left(i\!\sum_{\substack{j<k\\a_j=a_k=\mathrm{true}}}w_{jk}\right)v(a);

thus the vector denoted by $\operatorname{rage}(A,G,V)$ is $E_{w,V}(M_A)$ . First, using all-zero weights and identity matrices at every site gives $E_{0,I}(M_A)=M_A$ . Second, if every site matrix is the $1\times1$ matrix with entry $(\sqrt2)^{-1}$ , then its resulting vector is $E_{w,V}(v_+)$ , where $v_+(a)=\prod_{k=0}^{N-1}(\sqrt2)^{-1}$ . Third, for every natural number $m\ge1$ , every $c:\{0,\ldots,m-1\}\to\mathbb C$ , and every complex family $r(t,k,b)$ , form diagonal $m\times m$ site matrices $B_{k,b}$ with diagonal entry $c_t r(t,k,b)$ at $k=0$ and $r(t,k,b)$ at $k\ne0$ ; then

E_{w,V}(M_B)= E_{w,V}\!\left(a\longmapsto \sum_{t=0}^{m-1}c_t\prod_{k=0}^{N-1}r(t,k,a_k)\right).

The matrices $A$ , the coefficients $c$ , the factors $r$ , and the vectors in these equalities need not be normalized; the hypotheses exclude $N=0$ , $D=0$ , and, in the third statement, $m=0$ .

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