Unnumbered transfer-operator formula for the reduced density matrix

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.reduced_state_transfer

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

prove2quantum

Let $N,D\ge1$ , let $A,\Phi,V$ be admissible RAGE data, and assume the raw MPS $M(A)$ is nonzero. Let $S$ be any subset of sites, including the empty or full set, and let $a,b$ be bit strings on $S$ . Set $E_{k,u,v}=A_{k,u}\otimes\overline{A_{k,v}}$ and define

T_k(a,b)=\begin{cases}E_{k,a_k,b_k},&k\in S,\\ \sum_{t=0}^1 e^{it\sum_{j\in S}\Phi_{jk}(a_j-b_j)}E_{k,t,t},&k\notin S.\end{cases}

Let $\nu_{a,b}=\operatorname{tr}(T_1(a,b)\cdots T_N(a,b))$ , let $G_S$ be the product of graph gates entirely within $S$ , let $V_S=\bigotimes_{k\in S}V_k$ , and let $Z=\|M(A)\|^2>0$ . The reduced density matrix of the normalized RAGE vector is

\rho_S=\frac{V_S G_S\nu G_S^\dagger V_S^\dagger}{Z}.

This identity gives every marginal entry. The partial trace uses equal outside bra and ket bits. The summed physical bit in each outside transfer operator fixes the printed index omission; internal phases and rotations suppressed in the source are restored.

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.2–3, reduced-state displays: full normalized identity with suppressed internal
phases and V restored. Printed/changed/why: the second double sum omits equality of traced
bra/ket bits; joinBits restores it as required by the preceding partial trace. The printed
B_l phase has an unbound outside label; transferT uses the summed t as required by gate action.
These are disclosed source corrections, requiring independent moderation. -/
theorem reduced_state_transfer {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ)
    (hv : traceMPS A ≠ 0) (S : Finset (Fin N)) :
    0 < ‖traceMPS A‖ ^ 2 ∧ IsDensityMatrix (rageMarginal (rage A G V) S) ∧
    rageMarginal (rage A G V) S =
      (((‖traceMPS A‖ ^ 2 : ℝ) : ℂ)⁻¹) •
        (retainedOp G V S * crossMarginal A G S * (retainedOp G V S).conjTranspose) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Unnumbered transfer-operator formula for the reduced density matrix

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$ , let $A_i(t)$ be arbitrary complex $D\times D$ matrices for each site $i\in\{0,\ldots,N-1\}$ and Boolean value $t$ ; let $w_{ij}$ be real weights satisfying $w_{ij}=w_{ji}$ , $w_{ii}=0$ , and $0\le w_{ij}<2\pi$ ; and let each $V_i$ be a unitary complex $2\times2$ matrix. For a Boolean assignment $b$ on all sites, put

m_b=\operatorname{tr}\!\left(A_0(b_0)\cdots A_{N-1}(b_{N-1})\right), \qquad v_b=\sum_c \left(\prod_i(V_i)_{b_i c_i}\right) e^{\,\mathrm i\sum_{i<j}w_{ij}c_i c_j}m_c,

where $c$ ranges over all Boolean assignments. Assume that the vector $m$ is nonzero, and let $S$ be any subset of the sites. For assignments $a,b:S\to\{0,1\}$ , define

\rho_{ab} = \frac{1}{\|v\|^2} \sum_{e:S^{\mathrm c}\to\{0,1\}} v_{a\cup e}\,\overline{v_{b\cup e}}, \qquad R_{ab} = \left(\prod_{i\in S}(V_i)_{a_i b_i}\right) e^{\,\mathrm i\sum_{\substack{i,j\in S\\i<j}}w_{ij}b_i b_j},

where $a\cup e$ denotes the assignment agreeing with $a$ on $S$ and with $e$ outside $S$ . To define another matrix $C$ , put $E_i(s,t)=A_i(s)\otimes\overline{A_i(t)}$ , where the bar conjugates every matrix entry, and set

T_i(a,b)= \begin{cases} E_i(a_i,b_i),&i\in S,\\[2mm] \displaystyle\sum_{t\in\{0,1\}} e^{\,\mathrm i t\sum_{j\in S}w_{ji}(a_j-b_j)}E_i(t,t),&i\notin S, \end{cases} \qquad C_{ab}=\operatorname{tr}\!\left(T_0(a,b)\cdots T_{N-1}(a,b)\right).

The theorem asserts simultaneously that $Z=\|m\|^2>0$ , that $\rho$ is positive semidefinite with trace $1$ , and that

\rho=Z^{-1}RCR^\dagger.

Here all norms of vectors are Euclidean, and the scalar inverse used in defining $\rho$ is the total inverse, taking value $0$ at $0$ . The subset $S$ may be empty or contain every site; assignments on an empty set form a singleton, empty sums are $0$ , and empty products are identities.

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