Ω(1/k²) spectral gap of the adiabatic clock Hamiltonian on the computational subspace

Proved

QAlgorithms.Childs.clockPathMatrix_gap

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

childslecture-notesquantum-information

Let $k \ge 0$ be the number of gates of a quantum circuit and let $s \in [0,1]$ . In the adiabatic simulation of the circuit, the interpolated Hamiltonian $H(s) = (1-s)H_B + sH_C$ leaves invariant the $(k+1)$ -dimensional computational subspace spanned by the history states $|\psi_0\rangle, \dots, |\psi_k\rangle$ , and on it acts, by $\langle\psi_j|H_B|\psi_{j'}\rangle = -\delta_{j,j'}\delta_{j,0}$ and $\langle\psi_j|H_C|\psi_{j'}\rangle = -(\delta_{j,j'+1}+\delta_{j,j'-1})$ , as the real symmetric $(k+1)\times(k+1)$ matrix

A_k(s) = \begin{pmatrix} s-1 & -s & 0 & \cdots & 0 \\ -s & 0 & -s & \ddots & \vdots \\ 0 & -s & 0 & \ddots & 0 \\ \vdots & \ddots & \ddots & \ddots & -s \\ 0 & \cdots & 0 & -s & 0 \end{pmatrix},

whose $(0,0)$ entry is $s-1$ , whose first off-diagonal entries are $-s$ , and whose other entries vanish. Let $\lambda_0(s) \le \lambda_1(s) \le \cdots \le \lambda_k(s)$ be its eigenvalues, counted with multiplicity, and $\Delta_k(s) = \lambda_1(s) - \lambda_0(s)$ the gap between the smallest and the second smallest.

Lemma. The gap is $\Omega(1/k^2)$ uniformly in $s \in [0,1]$ : there are a constant $c > 0$ and a threshold $k_0$ such that

\Delta_k(s) \ge \frac{c}{k^2} \qquad \text{for all } k \ge k_0 \text{ and all } s \in [0,1].

This bound on the minimum gap along the whole interpolation path is what makes an adiabatic evolution time $T = \mathrm{poly}(k)$ sufficient, and hence shows that adiabatic quantum computation can efficiently simulate the circuit model.

Formalization Note The matrix is the shared definition clockPathMatrix k s on $\mathrm{Fin}(k+1)$ ; the gap is spectralGap, the second smallest minus the smallest eigenvalue of the Hermitian matrix with multiplicity (so a degenerate ground level would give gap $0$ ). The constants $c$ and $k_0$ are quantified before $k$ and $s$ .

Preamble

import Definitions.Def_QAlgorithms_Defs_Hamiltonian
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Childs

/-- Childs, Lemma 33.1 (PDF p. 182; matrix (33.16) on PDF p. 181): the gap between the smallest
and second smallest eigenvalues of the matrix (33.16) for `s ∈ [0, 1]` is `Ω(1/k²)`. The
constant `c > 0` and the threshold `k₀` are chosen before `k` and are uniform over
`s ∈ [0, 1]`. -/
theorem clockPathMatrix_gap :
    ∃ c : ℝ, 0 < c ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ s ∈ Set.Icc (0 : ℝ) 1,
      c / (k : ℝ) ^ 2 ≤ spectralGap (clockPathMatrix k s) := by
  sorry

end QAlgorithms.Childs

Source

Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025, PDF p. 182, Lemma 33.1. https://www.cs.umd.edu/~amchilds/qa/qa.pdf

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The statement asserts that there exist a real constant $c > 0$ and a natural number $k_0$ such that for every natural number $k \ge k_0$ and every real $s \in [0,1]$ ,

\frac{c}{k^2} \;\le\; \Delta\big(M_k(s)\big).

The matrix $M_k(s)$ . This is the real $(k+1)\times(k+1)$ matrix with rows and columns indexed by $0,1,\dots,k$ , with entries:

$(M_k(s))_{00} = s - 1$ ;
otherwise, $(M_k(s))_{ij} = -s$ whenever $|i-j| = 1$ ;
all other entries are $0$ .

So it is $-s$ times the adjacency matrix of the path on $k+1$ vertices, plus $s-1$ in the top-left corner. For example, $M_k(0) = \operatorname{diag}(-1,0,\dots,0)$ . The matrix is symmetric for every $k$ and $s$ .

The gap $\Delta$ . For a real square matrix $A$ of size $m$ :

If $m \ge 2$ , $\Delta(A) = \lambda_2 - \lambda_1$ , where $\lambda_1 \le \lambda_2 \le \dots \le \lambda_m$ are the eigenvalues of $A$ counted with multiplicity and sorted increasingly.
If $m < 2$ , then $\Delta(A) = 0$ .
If $A$ is not symmetric (Hermitian), all "eigenvalues" are taken to be $0$ by convention. This case does not arise here, since $M_k(s)$ is symmetric.

So for $k \ge 1$ , $\Delta(M_k(s))$ is the difference between the two smallest eigenvalues of $M_k(s)$ . It is zero if the smallest eigenvalue is repeated.

Edge cases.

For $k = 0$ the matrix is $1\times 1$ , so $\Delta = 0$ . The left side $c/0^2$ is evaluated with the convention that division by zero yields $0$ , so the inequality reads $0 \le 0$ .
Because $k_0$ is existentially chosen, the claim only concerns all sufficiently large $k$ . No explicit value of $c$ or $k_0$ is asserted.
The bound must hold uniformly in $s$ over the closed interval, including both endpoints $s = 0$ and $s = 1$ .

Human review

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

View graph