Circuit simulation: local coordinate updates for the overlap objective

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.local_gate_variational_update

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

prove2quantum

Let $N,D\ge1$ . Normalize a nonzero initial RAGE vector with $V=I$ and apply a single-qubit unitary at site $q$ , giving the unit target $\chi$ . Fix admissible nonzero trial data with the same nonincident edges, and vary one trial site tensor pair. Let $L$ be its physical-state map, $G=L^\dagger L$ , and $b=L^\dagger\chi$ . The normal equations

Gx=b

have a solution. Every solution gives the orthogonal projection $Lx$ of $\chi$ onto $\operatorname{range}L$ . If $Lx\ne0$ , it maximizes $|\langle Ly,\chi\rangle|^2/\|Ly\|^2$ over all nonzero trial vectors; if $Lx=0$ , all such objectives equal zero. Singular $G$ is allowed.

With the trial tensors fixed, varying one edge incident on $q$ keeps the norm squared $Z$ constant and gives

\mathcal O(z)=\frac{c_0+2\operatorname{Re}(c_1z)}Z,\qquad |z|=1,

with coefficients explicitly obtained from the complementary edge components. A maximum on this circle is attained. These are coordinate optima in an alternating sweep, with all other edges frozen.

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 p.4, Eq.(5) and following paragraph: coordinate optima in an alternating sweep.
The singular normal equations and zero-projection case are retained. Nonincident edges are
frozen by edgeTrial. The statement makes no claim of global convergence of the sweep. -/
theorem local_gate_variational_update {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A Atr : Tensors N D) (G Gtr : PhaseGraph N) (hv : traceMPS A ≠ 0)
    (htrial : traceMPS Atr ≠ 0) (q : Fin N) (U : Matrix.unitaryGroup Bool ℂ)
    (hfixed : ∀ i j, i ≠ q → j ≠ q → Gtr.weight i j = G.weight i j) (k : Fin N) :
    let chi := act (localGate q U) (normalizeRageVector (rage A G (fun _ => 1)))
    let L := siteMap Atr Gtr (fun _ => 1) k
    let G := L.conjTranspose * L
    let b := L.conjTranspose.mulVec (WithLp.ofLp chi)
    (∃ x : SiteCoordinates D → ℂ, G.mulVec x = b) ∧
    (∀ x : SiteCoordinates D → ℂ, G.mulVec x = b →
      (∀ y : SiteCoordinates D → ℂ,
        inner ℂ (siteVector L y) (chi - siteVector L x) = 0) ∧
      (siteVector L x ≠ 0 → ∀ y : SiteCoordinates D → ℂ, siteVector L y ≠ 0 →
        overlapObjective (siteVector L y) chi ≤ overlapObjective (siteVector L x) chi) ∧
      (siteVector L x = 0 → ∀ y : SiteCoordinates D → ℂ, siteVector L y ≠ 0 →
        overlapObjective (siteVector L y) chi = 0)) ∧
    (∀ j : Fin N, j ≠ q →
      let c := overlapCoefficients Atr Gtr q j chi
      let Z := ‖traceMPS Atr‖ ^ 2
      (∀ z : ℂ, ‖z‖ = 1 →
        overlapObjective (edgeTrial Atr Gtr (fun _ => 1) q j z) chi =
          (c.1 + 2 * (c.2 * z).re) / Z) ∧
      (∃ z : ℂ, ‖z‖ = 1 ∧ ∀ w : ℂ, ‖w‖ = 1 →
        overlapObjective (edgeTrial Atr Gtr (fun _ => 1) q j w) chi ≤
          overlapObjective (edgeTrial Atr Gtr (fun _ => 1) q j z) chi)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 4, Circuit simulation: local coordinate updates for the overlap objective

Read-back

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

For all natural numbers $N,D$ with $1\le N$ and $1\le D$ , let $A_r^s$ and $A_{\mathrm{tr},r}^s$ be two collections of complex $D\times D$ matrices, and let $G,G_{\mathrm{tr}}$ be graphs whose respective real weights $w,w^{\mathrm{tr}}$ are symmetric, vanish on the diagonal, and lie in $[0,2\pi)$ . Assume both vectors

T(b)=\operatorname{tr}\!\left(\prod_{r=0}^{N-1}A_r^{b_r}\right), \qquad T_{\mathrm{tr}}(b)=\operatorname{tr}\!\left(\prod_{r=0}^{N-1}A_{\mathrm{tr},r}^{b_r}\right)

are nonzero, where products are in increasing site order. Choose sites $q,k<N$ and a unitary complex $2\times2$ matrix $U$ , and assume $w^{\mathrm{tr}}_{ij}=w_{ij}$ whenever $i\ne q$ and $j\ne q$ . Define $\Phi_G(b)=\sum_{r<s,\ b_r=b_s=1}w_{rs}$ , and define $\Phi_{\mathrm{tr}}$ using $w^{\mathrm{tr}}$ . Let $v_G(b)=e^{i\Phi_G(b)}T(b)$ , and let $\chi$ be obtained from $v_G/\|v_G\|$ by applying $U$ at site $q$ and the identity at all other sites; explicitly, $\chi(b)=\sum_{s\in\{0,1\}}U(b_q,s)v_G(b[q\leftarrow s])/\|v_G\|$ . Index site coordinates by $C=\{0,1\}\times\{0,\ldots,D-1\}\times\{0,\ldots,D-1\}$ . For $e\in C$ , replace the trial tensor at site $k$ by the matrices whose $(i,\ell)$ entry for bit $s$ is $1$ if $(s,i,\ell)=e$ , and $0$ otherwise, leaving all other trial tensors unchanged; call this collection $A_{\mathrm{tr}}^{[e]}$ . Define the matrix $L$ , with rows indexed by bit strings and columns by $C$ , by

L_{b,e}=e^{i\Phi_{\mathrm{tr}}(b)} \operatorname{tr}\!\left(\prod_{r=0}^{N-1}(A_{\mathrm{tr}}^{[e]})_r^{b_r}\right), \qquad M=L^\dagger L,\qquad \beta=L^\dagger\chi,

and write $F(\xi)=|\langle\xi,\chi\rangle|^2/\|\xi\|^2$ , taking $F(0)=0$ . The theorem asserts that $Mx=\beta$ has a solution $x:C\to\mathbb C$ , and that every solution satisfies

\begin{gathered} \forall y:C\to\mathbb C,\quad \langle Ly,\chi-Lx\rangle=0,\\ Lx\ne0\ \Longrightarrow\ \forall y:C\to\mathbb C,\quad Ly\ne0\ \Longrightarrow\ F(Ly)\le F(Lx),\\ Lx=0\ \Longrightarrow\ \forall y:C\to\mathbb C,\quad Ly\ne0\ \Longrightarrow\ F(Ly)=0. \end{gathered}

It also asserts the following for every site $j\ne q$ : set

B_j(b)=e^{i\Phi_{\mathrm{tr}}(b)-iw^{\mathrm{tr}}_{qj}\mathbf1_{\{b_q=b_j=1\}}}T_{\mathrm{tr}}(b),

let $u_j$ be $B_j$ restricted to strings whose selected bits are not both $1$ , extended by zero, and let $v_j$ be its restriction to strings whose selected bits are both $1$ , extended by zero. With

a_j=\langle u_j,\chi\rangle,\quad b_j=\langle v_j,\chi\rangle,\quad c_{0,j}=|a_j|^2+|b_j|^2,\quad c_{1,j}=a_j\overline{b_j},\quad Z=\|T_{\mathrm{tr}}\|^2,

one has

\forall z\in\mathbb C,\quad |z|=1\ \Longrightarrow\ F(u_j+zv_j)=\frac{c_{0,j}+2\operatorname{Re}(c_{1,j}z)}{Z},

and there exists $z\in\mathbb C$ with $|z|=1$ such that $F(u_j+wv_j)\le F(u_j+zv_j)$ for every $w\in\mathbb C$ with $|w|=1$ . The site $k$ need not differ from $q$ ; when $N=1$ , the final assertions quantified over $j\ne q$ are vacuous.

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