Static updates: the one-site energy minimization is a generalized Rayleigh problem

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.one_site_energy_minimum

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

prove2quantum

Fix $N,D\ge1$ , a valid nonzero RAGE vector, a site $k$ , and a Hermitian finite-qubit Hamiltonian $H$ . Freeze all data except the two site tensors at $k$ . Let $x\in\mathbb C^{2D^2}$ contain their entries, let $L$ be the resulting physical-state linear map, and set $F=L^\dagger HL$ , $G=L^\dagger L$ . Then the updated raw vector is $Lx$ and, whenever $x^\dagger Gx>0$ ,

E(x)=\frac{x^\dagger Fx}{x^\dagger Gx}.

There exist $x_*$ with $x_*^\dagger Gx_*>0$ and a real $\lambda$ such that

Fx_*=\lambda Gx_*,\qquad E(x_*)=\lambda\le E(y)\quad(y^\dagger Gy>0).

The norm matrix may be singular; only vectors with nonzero physical image are admissible. The minimum is an attained one-site optimum.

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.3, Static updates: the generalized Rayleigh reduction and an attained local
minimum. G may have a kernel. Eigenvectors are required to have positive G norm, preventing
common-kernel vectors from making arbitrary real numbers generalized eigenvalues. -/
theorem one_site_energy_minimum {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (Gph : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ)
    (hv : rage A Gph V ≠ 0) (k : Fin N)
    (H : Matrix (Qubits N) (Qubits N) ℂ) (hH : H.IsHermitian) :
    let L := siteMap A Gph V k
    let F := L.conjTranspose * H * L
    let G := L.conjTranspose * L
    (∀ x : SiteCoordinates D → ℂ,
      rage (replaceSite A k x) Gph V = siteVector L x) ∧
    (∀ x : SiteCoordinates D → ℂ, 0 < (rageSiteQuadratic G x).re →
      rayleighEnergy H (rage (replaceSite A k x) Gph V) =
        (rageSiteQuadratic F x).re / (rageSiteQuadratic G x).re) ∧
    (∃ (x : SiteCoordinates D → ℂ) (lam : ℝ),
      0 < (rageSiteQuadratic G x).re ∧ F.mulVec x = (lam : ℂ) • G.mulVec x ∧
      (rageSiteQuadratic F x).re / (rageSiteQuadratic G x).re = lam ∧
      (∀ y : SiteCoordinates D → ℂ, 0 < (rageSiteQuadratic G y).re →
        lam ≤ (rageSiteQuadratic F y).re / (rageSiteQuadratic G y).re)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 3, Static updates: the one-site energy minimization is a generalized Rayleigh problem

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_i(t)$ be arbitrary complex $D\times D$ matrices indexed by sites and Boolean values, let real weights $w_{ij}$ satisfy $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 any such tensor family $B$ , define a vector

v(B)_b = \sum_{a:\{0,\ldots,N-1\}\to\{0,1\}} \left(\prod_i(V_i)_{b_i a_i}\right) e^{\,\mathrm i\sum_{i<j}w_{ij}a_i a_j} \operatorname{tr}\!\left(B_0(a_0)\cdots B_{N-1}(a_{N-1})\right).

Assume $v(A)\ne0$ , choose a site $k$ , and let $H$ be any Hermitian complex matrix indexed by Boolean assignments on all sites. Write $C_D=\{0,1\}\times\{0,\ldots,D-1\}\times\{0,\ldots,D-1\}$ . For each $x:C_D\to\mathbb C$ , let $A[x]$ retain all matrices away from site $k$ and have entries $A[x]_k(t)_{ij}=x(t,i,j)$ . For $c\in C_D$ , let $e_c$ be $1$ at $c$ and $0$ elsewhere, and define

L_{bc}=v(A[e_c])_b,\qquad F=L^\dagger HL,\qquad G=L^\dagger L,\qquad q_M(x)=\sum_{c,d\in C_D}\overline{x_c}M_{cd}x_d.

The theorem asserts that $v(A[x])=Lx$ for every $x$ ; that whenever $\operatorname{Re}q_G(x)>0$ ,

\frac{\operatorname{Re}\langle v(A[x]),H v(A[x])\rangle}{\|v(A[x])\|^2} = \frac{\operatorname{Re}q_F(x)}{\operatorname{Re}q_G(x)};

and that there exist $x:C_D\to\mathbb C$ and a real number $\lambda$ such that

\operatorname{Re}q_G(x)>0,\qquad Fx=\lambda Gx,\qquad \frac{\operatorname{Re}q_F(x)}{\operatorname{Re}q_G(x)}=\lambda,

with

\lambda\le \frac{\operatorname{Re}q_F(y)}{\operatorname{Re}q_G(y)} \quad\text{for every }y:C_D\to\mathbb C \text{ satisfying }\operatorname{Re}q_G(y)>0.

The identity $v(A[x])=Lx$ includes choices yielding the zero vector; the quotient identity and the minimizing comparison are restricted to strictly positive denominators. No invertibility of $G$ or uniqueness of $x$ or $\lambda$ is assumed or asserted.

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