Doubled amplitude QNTK is Hermitian and positive semidefinite

Proved

QAlgorithms.Papers.Independent.Intakenext100.P88.amplitude_kernel_psd

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Use the same ordered unitary circuit and normalized feature states, but output all complex amplitudes $z_{x,i}=\langle i|U\phi(x)\rangle$ , $i=1,\ldots,h$ . Duplicate each output as $\mathcal z_{x,0,i}=z_{x,i}$ and $\mathcal z_{x,1,i}=\overline{z_{x,i}}$ . The worldsheet index therefore records whether an amplitude is conjugated. For real parameters, write $\mathcal J_{\mu\ell}=\partial_{\theta_\ell}\mathcal z_\mu$ .

Define $\mathcal K_{\mu\nu}=\sum_\ell\mathcal J_{\mu\ell}\overline{\mathcal J_{\nu\ell}}$ . If $J$ is the undoubled amplitude Jacobian, its blocks are

\mathcal K=\begin{pmatrix}JJ^\dagger&JJ^T\\\overline J J^\dagger&\overline J J^T\end{pmatrix}.

This kernel is Hermitian, and every finite Gram submatrix is positive semidefinite for arbitrary complex test vectors. This extends kernel positivity to complex amplitude outputs without asserting invertibility.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P88

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P88

open scoped BigOperators ComplexConjugate Topology NNReal ComplexOrder

open MeasureTheory ProbabilityTheory Filter

/-- PDF p.29 SM Theorem 2, Eqs.(135),(141)-(142): the doubled complex kernel is Hermitian
and PSD on arbitrary finite submatrices, not just on conjugate-paired test vectors. -/
theorem amplitude_kernel_psd {D : Type*} {h L : ℕ}
    (M : AmplitudeModel D h L) (theta : Fin L → ℝ) :
    (∀ a b, star (amplitudeKernel M theta b a) = amplitudeKernel M theta a b) ∧
    ∀ (n : ℕ) (a : Fin n → D × Bool × Fin h),
      Matrix.PosSemidef (fun i j => amplitudeKernel M theta (a i) (a j)) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P88

end

Source

Representation Learning via Quantum Neural Tangent Kernels, arXiv:2111.04225v3, PDF p. 29, SM Theorem 2; Eqs.(135),(141)-(142)

Read-back

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

Let $D$ be any type, let $h,L$ be natural numbers, and let $M$ consist of $h>0$ , unitary complex $h\times h$ matrices $W_l$ , Hermitian complex $h\times h$ matrices $X_l$ , indexed by $0\le l<L$ , and a unit vector $\phi_x\in\mathbb C^h$ for every $x\in D$ . For $\theta\in\mathbb R^L$ , define $U(\theta)=\prod_{l=0}^{L-1}\bigl(W_l\exp(i\theta_lX_l)\bigr)$ , with factors written in increasing index order and the empty product equal to the identity. For $a=(x,\sigma,j)\in D\times\{\mathrm{false},\mathrm{true}\}\times\{0,\ldots,h-1\}$ , let $A_a(\theta)=(U(\theta)\phi_x)_j$ when $\sigma=\mathrm{false}$ , and let $A_a(\theta)=\overline{(U(\theta)\phi_x)_j}$ when $\sigma=\mathrm{true}$ . Write $\partial_l$ for differentiation with respect to the real coordinate $\theta_l$ , and set $K_\theta(a,b)=\sum_{l=0}^{L-1}\partial_lA_a(\theta)\,\overline{\partial_lA_b(\theta)}$ . Then $\overline{K_\theta(b,a)}=K_\theta(a,b)$ for all $a,b$ ; moreover, for every natural number $n$ and every list of sample indices $a_0,\ldots,a_{n-1}$ , allowing repetitions, the matrix $G_{ij}=K_\theta(a_i,a_j)$ is positive semidefinite: it is Hermitian and $\sum_{i,j=0}^{n-1}\overline{z_i}G_{ij}z_j$ is a nonnegative real number for every $z\in\mathbb C^n$ . This includes $n=0$ ; it also includes $L=0$ , when every kernel entry is zero.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph