Static updates: explicitly computable energy gradient for global optimization

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.explicit_energy_gradient

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

prove2quantum

Let $N,D\ge1$ and fix admissible RAGE data giving a nonzero raw vector $v$ and a Hermitian Hamiltonian $H$ . Along any differentiable real parameter path through these data, let $\dot v$ be the explicit finite-product derivative: replace one site tensor or one local rotation at a time by its derivative and differentiate each graph phase as $\frac{d}{dt}e^{i\theta}=i\dot\theta e^{i\theta}$ . Write $f=\langle v,Hv\rangle$ and $g=\|v\|^2>0$ . Then

\frac{dE}{dt}=\frac{g\,2\operatorname{Re}\langle\dot v,Hv\rangle-f\,2\operatorname{Re}\langle\dot v,v\rangle}{g^2}.

The Lean statement specifies the finite sums for $\dot v$ and assumes differentiability only of the supplied scalar parameter entries. In particular the formula applies to real coordinates of the tensors and graph and to valid smooth charts of the unitary rotations. It supplies an explicit gradient without an optimization convergence claim.

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, final Static updates sentence: the gradient is explicitly computable.
For every differentiable real coordinate path, the raw derivative is the displayed finite
sum, and the energy derivative is the quotient rule with a positive norm denominator.
There is no optimizer convergence or global-optimality conclusion. -/
theorem explicit_energy_gradient {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ)
    (hv : rage A G V ≠ 0) (H : Matrix (Qubits N) (Qubits N) ℂ) (hH : H.IsHermitian)
    (t0 : ℝ) (Ap : ℝ → Tensors N D) (wp : ℝ → Fin N → Fin N → ℝ)
    (Vp : ℝ → Fin N → Matrix Bool Bool ℂ)
    (Adot : Tensors N D) (wdot : Fin N → Fin N → ℝ)
    (Vdot : Fin N → Matrix Bool Bool ℂ)
    (hA0 : Ap t0 = A) (hw0 : wp t0 = G.weight)
    (hV0 : Vp t0 = fun k => (V k : Matrix Bool Bool ℂ))
    (hAp : ∀ k b i j, HasDerivAt (fun t => Ap t k b i j) (Adot k b i j) t0)
    (hwp : ∀ i j, HasDerivAt (fun t => wp t i j) (wdot i j) t0)
    (hVp : ∀ k a b, HasDerivAt (fun t => Vp t k a b) (Vdot k a b) t0) :
    let v := rage A G V
    let vdot := rawTangent A Adot G.weight wdot (fun k => (V k : Matrix Bool Bool ℂ)) Vdot
    let path := fun t => act (productOp (Vp t)) (act (graphOp (wp t)) (traceMPS (Ap t)))
    let f := (inner ℂ v (act H v)).re
    let g := ‖v‖ ^ 2
    HasDerivAt path vdot t0 ∧
    HasDerivAt (fun t => rayleighEnergy H (path t))
      ((g * (2 * (inner ℂ vdot (act H v)).re) -
        f * (2 * (inner ℂ vdot v).re)) / g ^ 2) t0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 3, Static updates: explicitly computable energy gradient for global optimization

Read-back

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

Let $N,D$ be natural numbers with $N,D\ge1$ ; let $A$ assign a complex $D\times D$ matrix to each site and Boolean value; let $G$ have real weights $w_{ij}$ that are symmetric, zero on the diagonal, nonnegative, and strictly less than $2\pi$ ; and let each $V_k$ be a unitary complex $2\times2$ matrix. For bit strings $a,b\in\{0,1\}^N$ , put

T_A(b)=\operatorname{tr}\!\left(\prod_{l=0}^{N-1}A_l(b_l)\right),\qquad \Gamma_w(b)=\sum_{\substack{i<j\\b_i=b_j=1}}w_{ij},\qquad P(V)_{ab}=\prod_{l=0}^{N-1}(V_l)_{a_l b_l},

where the matrix product defining $T_A$ is in increasing site order, and define $v=P(V)(e^{i\Gamma_w(b)}T_A(b))_b$ . Assume $v\ne0$ , and let $H$ be any Hermitian complex matrix indexed by these bit strings. Fix $t_0\in\mathbb R$ , paths $A(t)$ of tensor families, $w(t)$ of real arrays, and $V(t)$ of complex $2\times2$ matrix families, together with families $\dot A,\dot w,\dot V$ . Assume $A(t_0)=A$ , $w(t_0)=w$ , and $V(t_0)=V$ , and assume that at $t_0$ every entry $A_k(b)_{ij}$ , for $k<N$ , Boolean $b$ , and $i,j<D$ , has derivative $(\dot A_k(b))_{ij}$ , every $w_{ij}(t)$ , for $i,j<N$ , has derivative $\dot w_{ij}$ , and every $(V_k(t))_{ab}$ , for $k<N$ and Boolean $a,b$ , has derivative $(\dot V_k)_{ab}$ . Define

\dot T_b=\sum_{k=0}^{N-1}\operatorname{tr}\!\left( \prod_{l=0}^{N-1} \begin{cases}\dot A_l(b_l),&l=k,\\A_l(b_l),&l\ne k,\end{cases}\right),\qquad \dot P_{ab}=\sum_{k=0}^{N-1}\prod_{l=0}^{N-1} \begin{cases}(\dot V_l)_{a_l b_l},&l=k,\$V_l)_{a_l b_l},&l\ne k,\end{cases}

and

\dot v_a=\sum_b e^{i\Gamma_w(b)} \left[\dot P_{ab}T_A(b)+P(V)_{ab} \bigl(\dot T_b+i\Gamma_{\dot w}(b)T_A(b)\bigr)\right].

Then the path (p(t)=P(V(t))(e^{i\Gamma_{w(t)}(b)}T_{A(t)}(b))_b $has derivative$ \dot v $at$ t_0 $. Furthermore, writing$ f=\operatorname{Re}\langle v,Hv\rangle $and$ g=|v|^2>0 $, the real function$ t\mapsto\operatorname{Re}\langle p(t),Hp(t)\rangle/|p(t)|^2$ has derivative

\frac{g\,2\operatorname{Re}\langle\dot v,Hv\rangle -f\,2\operatorname{Re}\langle\dot v,v\rangle}{g^2}

at $t_0$ , where the complex inner product is conjugate-linear in its first argument. Away from $t_0$ , no graph-weight conditions or unitarity conditions are imposed on the paths; the energy quotient uses the convention that division by zero equals zero.

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