All missions

Why the sign of the recourse matrix matters

A two-stage adjustable robust linear program chooses a first-stage decision $x$ before an uncertain right-hand side $h$ is revealed, and a second-stage (recourse) decision $y(h)$ afterwards, minimising the worst case over an uncertainty set $\mathcal U$ of the total cost. Computing the optimal value $z_{AR}(\mathcal U)$ is hard in general (Feige et al., 2007), and the standard tractable restriction is to affine policies $y(h)=Ph+q$ (Ben-Tal et al., 2004), whose optimal value $z_{Aff}(\mathcal U)$ is computed by a single linear program.

El Housni and Goyal (arXiv:1807.00163v2) show that, when the recourse matrix $B$ is non-negative and $\mathcal U$ is a budget of uncertainty set, $z_{Aff}$ is within a factor $O(\log n/\log\log n)$ of $z_{AR}$. Their Section 7 asks whether the non-negativity of $B$ is needed, and answers with a family of two-stage lot-sizing instances whose recourse matrix is a network matrix with entries in $\{-1,0,1\}$. On this family the adjustable problem has value $0$ while every affine policy costs at least $m/2-1$. Lot-sizing and transportation recourse are among the most common uses of two-stage robust optimisation (see Bertsimas and de Ruiter, 2016), so the instance is a natural one, not an artefact.

Lower bounds on the gap between affine and adjustable policies were known before (Bertsimas and Goyal, 2012); the point of the present family is that the adjustable value is exactly $0$, so the ratio $z_{Aff}/z_{AR}$ is infinite and the difference $z_{Aff}-z_{AR}$ grows linearly in $m$.

Setting

The lot-sizing problem (7.1). There are $m$ nodes. Node $i$ stores inventory $x_i$ at cost $c_i$ per unit, up to a capacity $K_i$, and faces an uncertain demand $h_i$. After $h$ is revealed, inventory may be shipped from node $i$ to node $j$ in amount $y_{ij}(h)\ge0$ at cost $d_{ij}$ per unit. A solution $(x,y)$ is feasible when $0\le x_i\le K_i$ and, for every $h\in\mathcal U$,

$$x_i+\sum_{j}y_{ji}(h)-\sum_j y_{ij}(h)\ \ge\ h_i\qquad(i\in[m]).$$

The objective is the first-stage cost $\sum_ic_ix_i$ plus the worst case over $h\in\mathcal U$ of the transportation cost $\sum_{ij}d_{ij}y_{ij}(h)$. The optimum over all rules $h\mapsto y(h)$ is $z_{AR}(\mathcal U)$, and the optimum over affine rules $y(h)=Ph+q$ (one row of $P$ per arc, one column per node) is $z_{Aff}(\mathcal U)$.

The family (7.2). Let $m=2k$, and split the nodes into $J_1$ and $J_2$ with $|J_1|=|J_2|=k$. Set $c_i=0$ on $J_1$ and $c_i=1$ on $J_2$, $K_i=1$ everywhere, $d_{ij}=0$ for $i\in J_1$, $j\in J_2$, and $d_{ij}=\infty$ otherwise. The uncertainty set is

$$\mathcal U=\Big\{h\in[0,1]^m\ \Big|\ \sum_{i=1}^m h_i\le m/2\Big\}.$$

Inventory can thus move only from $J_1$ to $J_2$, at no cost; stocking $J_1$ is free and stocking $J_2$ costs one per unit.

In the Lean development the general problem is the structure LotSizing N E (nodes N, usable arcs E with tail src, head tgt, distances d), with the predicate Feasible, the cost cost, and the sets adjustableValues, affineValues of objective values. The family is lotSizingFamily k, on nodes Fin k ⊕ Fin k and arcs Fin k × Fin k.

Formalization targets

Goal: Lemma 7.1

For every $k\ge1$,

$$z_{AR}(\mathcal U)=0\qquad\text{and}\qquad z_{Aff}(\mathcal U)=\frac m2-1=k-1,$$

each stated as IsLeast of the corresponding set of objective values, which asserts that the value is attained and is the minimum. The unboundedness of the gap, $z_{Aff}-z_{AR}=k-1\to\infty$, is immediate.

Milestones (Appendix D, in proof order)

1. The first-stage decision $x=\mathbb 1_{J_1}$ admits a second-stage policy with cost $0$ in every scenario (p. 35).
2. (D.3), for $k\ge2$: every feasible affine solution has $x_i=1$ on $J_1$, and its flow on arc $(i,j)$ depends on $h_i$ only, with $P_{(i,j),i}+q_{ij}=0$ (p. 36).
3. For $k\ge2$, every feasible affine solution satisfies $x_j+q_{\ell j}\ge1$ for $\ell\in J_1$, $j\in J_2$ (pp. 36–37).
4. Every feasible affine solution has $\sum_{j\in J_2}x_j\ge m/2-1$, hence $z_{Aff}\ge m/2-1$ (p. 37).
5. The explicit affine solution $x=\mathbb 1-e_m$, $y_{im}(h)=1-h_i$, is feasible and costs $m/2-1$ (p. 37).

Significance

The result. The approximation guarantees of the paper ($O(\log n/\log\log n)$ for budget sets, $O(\log^2 n/\log\log n)$ for disjoint constrained budgets) assume $B\ge0$. Lemma 7.1 shows that this assumption is not a convenience of the proof: with a network recourse matrix no bound on $z_{Aff}/z_{AR}$ of any form holds, even for a budget set and a bipartite network. Any extension of the guarantees to transportation or flow recourse must therefore change the policy class or add structure, which is the open direction the paper states after the lemma.

Formalizing it. The lemma is proved in the paper; it has not been machine-checked. The mission produces a reusable definition of the two-stage robust lot-sizing problem with arc-based recourse, the precise instance family, and checked versions of the five steps of Appendix D. Two of those steps hold only for $m\ge4$ and one is printed with its indices swapped (see the scope section); the formal statements make those boundaries explicit.

Difficulty

The adjustable half is a transportation argument, and the affine upper bound is a direct verification of one explicit solution. The substance is the affine lower bound, which must hold for every feasible affine solution, not for a particular one. Comparing an affine policy with the adjustable optimum on a few extreme scenarios gives nothing: on any single scenario an affine policy can match the adjustable cost. What fails for affine policies is simultaneous feasibility over the whole of $\mathcal U$, and the lower bound has to extract a cost from that requirement alone. It is also sensitive to the size of the instance: two of the intermediate steps of Appendix D are false for $m=2$, so a formal proof has to treat small $m$ separately.

Formalization scope

• Model. Vectors are functions on finite types with the componentwise order; indices are 0-based. The second stage is a rule $y:\mathbb R^N\to\mathbb R^E$, which gives the same values as choosing $y(h)$ separately per scenario. The epigraph variable $z$ of (7.1) appears through the sets of objective values $t$ with $\sum_ic_ix_i+\sum_a d_a y_a(h)\le t$ for all $h\in\mathcal U$.
• Infinite distances. Arcs with $d_{ij}=\infty$ are omitted rather than given an extended-real cost: a finite-cost solution never uses them, so no optimal value changes, and App. D itself works with the reduced constraints (D.1)–(D.2) and with a matrix $P$ having "one row per edge". The kept arcs $J_1\times J_2$ have $d=0$, and the cost keeps the term $\sum_a d_a y_a(h)$ so that (7.1) is visible.
• Values as IsLeast. No real infimum is used, so "$z=0$" cannot hold on an empty feasible set; feasibility includes $0\le x\le K$, $Ph+q\ge0$ on all of $\mathcal U$, and the coverage constraint at every node, including the outflow constraint (D.2) at $J_1$.
• Sizes. The paper's "$m$ even" is $m=2k$. The goal assumes $k\ge1$; at $k=0$ the affine value would be $0\ne-1$.
• Corrections, disclosed in the items. (i) The paper builds the zero-cost adjustable policy only at extreme points of $\mathcal U$; the milestone quantifies over all of $\mathcal U$, as feasibility requires. (ii) (D.3) and the bound $x_j+q_{\ell j}\ge1$ are false for $m=2$ (explicit counterexamples are in the items' notes) and carry the hypothesis $k\ge2$. (iii) "for any $j\in J_1$ and for any $\ell\in J_2$" on p. 37 has the indices swapped and is stated with $\ell\in J_1$, $j\in J_2$.
• Not formalized. That (7.1) has a network recourse matrix with entries in $\{-1,0,1\}$ is descriptive and is not stated; total unimodularity is not needed.
• Reusable parts. LotSizing (any node set, any arc set, any uncertainty set) can host other two-stage lot-sizing and transportation results. Proofs of any milestone, and alternative arguments for the affine lower bound, are welcome.

The source is arXiv:1807.00163v2; its printed page numbers equal the PDF's.

Selected references

• O. El Housni, V. Goyal, On the Optimality of Affine Policies for Budgeted Uncertainty Sets, arXiv:1807.00163v2, 2019 (Mathematics of Operations Research 46(2), 2021). https://arxiv.org/abs/1807.00163v2
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99(2), 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Mathematical Programming 134(2), 2012. https://doi.org/10.1007/s10107-011-0444-4
• D. Bertsimas, F. de Ruiter, Duality in two-stage adaptive linear optimization: Faster computation and stronger bounds, INFORMS Journal on Computing 28(3), 2016. https://doi.org/10.1287/ijoc.2016.0689
• U. Feige, K. Jain, M. Mahdian, V. Mirrokni, Robust combinatorial optimization with exponential scenarios, IPCO 2007. https://doi.org/10.1007/978-3-540-72792-7_33

Motivation

Superconducting circuits built from capacitors, inductors and Josephson junctions are the dominant platform for current quantum processors (Google, IBM, Rigetti, IQM and others). The source article — the Wikipedia entry Superconducting quantum computing — states two facts about the gate model on this hardware that this mission makes precise:

1. two-qubit gates such as iSWAP "can be achieved through coherent exchange" between two coupled qubits, whose interaction is described by the coupling Hamiltonian $\hat H=\frac{\hbar J}{2}(\sigma_1^x\sigma_2^x+\sigma_1^y\sigma_2^y)$ (section Transmon);
2. "single-qubit gates combined with two-qubit gates form a universal gate set" (section Criteria for a viable quantum processor), and, for instance, a three-qubit Toffoli gate "is implemented using a combination of single and two-qubit gates" (section Quantum gates).

Statement 2 is a mathematical theorem, not an engineering claim: it says that every unitary operation on $n$ qubits can be written exactly as a finite product of the hardware's elementary gates. Its classical form with CNOT as the two-qubit gate is due to Barenco et al. (1995); the iSWAP version follows because CNOT can be built from two iSWAPs and single-qubit gates (Schuch–Siewert 2003).

Timeline.

• 1995 — DiVincenzo shows two-qubit gates are universal; Barenco et al. prove that single-qubit gates and CNOT generate all $n$-qubit unitaries exactly.
• 2003 — Schuch and Siewert analyse the XY (iSWAP-type) interaction and give a CNOT construction using two iSWAP gates.
• 2007 — the transmon is introduced; capacitively coupled transmons realise the XY interaction.
• 2012 — a Toffoli gate is demonstrated on three superconducting transmon qubits.

Setting

An $n$-qubit register has computational basis states $|x\rangle$ labelled by bit strings $x\in\{0,1\}^n$; its operations form the unitary group $U(2^n)$. For a $2\times2$ unitary $U$ and a qubit $k$, the single-qubit gate $U^{(k)}$ applies $U$ to qubit $k$ and leaves the others unchanged. For a $4\times4$ matrix $G$ and an ordered pair of distinct qubits $(i,j)$, $G^{(i,j)}$ applies $G$ to qubits $i,j$ (qubit $i$ is the first tensor factor). Write

$$\mathcal S_n=\{U^{(k)} : U\in U(2),\ k\text{ a qubit}\},\qquad \mathcal G_n(G)=\{G^{(i,j)} : i\neq j\}.$$

The gates used are

$$\mathrm{iSWAP}=\begin{pmatrix}1&0&0&0\\0&0&i&0\\0&i&0&0\\0&0&0&1\end{pmatrix},\qquad \mathrm{CNOT}=\begin{pmatrix}1&0&0&0\\0&1&0&0\\0&0&0&1\\0&0&1&0\end{pmatrix}$$

in the basis $|00\rangle,|01\rangle,|10\rangle,|11\rangle$, and the Toffoli gate $|a,b,c\rangle\mapsto|a,b,c\oplus ab\rangle$. Time evolution under a Hamiltonian $H$ is $U(t)=\exp(-itH/\hbar)$, and the coupling Hamiltonian is $H=\frac{\hbar J}{2}(\sigma^x\otimes\sigma^x+\sigma^y\otimes\sigma^y)$. A two-level unitary acts as the identity outside the span of two basis vectors.

Formalization targets

Goal — universality of single-qubit gates and iSWAP

For every $n\ge1$,

$$\big\langle\,\mathcal S_n\cup\mathcal G_n(\mathrm{iSWAP})\,\big\rangle=U(2^n).$$

Milestones

1. Coherent exchange: $\exp\!\big(-\tfrac{it}{\hbar}H\big)=\mathrm{iSWAP}^\dagger$ at $t=\pi/(2J)$, for $\hbar,J\ne0$.
2. $\mathrm{CNOT}=(A\otimes B)\,\mathrm{iSWAP}\,(C\otimes D)\,\mathrm{iSWAP}\,(E\otimes F)$ for some $A,\dots,F\in U(2)$.
3. Two-level unitaries generate $U(\mathbb C^\iota)$ for every finite $\iota$.
4. $\big\langle\,\mathcal S_n\cup\mathcal G_n(\mathrm{CNOT})\,\big\rangle=U(2^n)$ for $n\ge1$.
5. $\mathrm{Toffoli}\in\big\langle\,\mathcal S_3\cup\mathcal G_3(\mathrm{CNOT})\,\big\rangle$.

Significance

The goal theorem is the formal justification for compiling arbitrary quantum algorithms to superconducting hardware whose native entangling interaction is of XY/iSWAP type: any target unitary, however large, has an exact decomposition into the hardware's elementary operations. Milestone 1 connects the abstract gate to the physical Hamiltonian; milestones 3–4 are the textbook universality theorem in the CNOT form, reusable for any other two-qubit gate that can synthesise CNOT; milestone 5 is the Toffoli construction mentioned in the source.

All results are classical and proved in the literature. To the best of the drafter's knowledge they are not yet available as machine-checked statements in Mathlib in this form; the mission's contribution is a complete formal development.

Difficulty

The naive route — "decompose into two-level unitaries, then implement each with gates" — hides real work: a two-level unitary on basis states $|x\rangle,|y\rangle$ with $x,y$ differing in many bits must be conjugated by a Gray-code sequence of controlled-NOT style gates into one acting on a single qubit, controlled on all others, and multiply-controlled single-qubit gates must then be reduced to single-qubit gates and CNOTs. Keeping indices, tensor embeddings and controls consistent over $n$ qubits is the main formal burden. Milestone 1 requires computing a matrix exponential exactly, which in Lean means handling NormedSpace.exp on a non-diagonal matrix.

Formalization scope

• Basis states of $n$ qubits are functions Fin n → Fin 2; two-qubit operators are indexed by Fin 2 × Fin 2 with the Kronecker product ⊗ₖ, first factor = first qubit.
• Universality is exact: the subgroup generated (Subgroup.closure) inside Matrix.unitaryGroup equals ⊤; no approximation or topological closure is involved, which is why the full continuous family $U(2)$ of single-qubit gates is included.
• $n=0$ is excluded: with no qubits there are no generators, while $U(1)$ is nontrivial.
• The gate sets contain only the stated gates; a formalization that adds arbitrary two-qubit unitaries to the generators would make the goal trivially true and is not acceptable.
• Needed infrastructure: tensor embeddings of gates into $n$-qubit registers, controlled gates, Gray-code arguments, and exponentials of $2\times2$ / $4\times4$ matrices. Lemmas about embeddings (onQubit, onPair) and multiply-controlled gates are reusable for any quantum-circuit mission.

Selected references

• Wikipedia, Superconducting quantum computing (sections Quantum gates, Criteria for a viable quantum processor, Transmon). https://en.wikipedia.org/wiki/Superconducting_quantum_computing
• A. Barenco, C. H. Bennett, R. Cleve, D. P. DiVincenzo, N. Margolus, P. Shor, T. Sleator, J. Smolin, H. Weinfurter, Elementary gates for quantum computation, Phys. Rev. A 52, 3457 (1995). https://doi.org/10.1103/PhysRevA.52.3457
• N. Schuch, J. Siewert, Natural two-qubit gate for quantum computation using the XY interaction, Phys. Rev. A 67, 032301 (2003). https://doi.org/10.1103/PhysRevA.67.032301
• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press (2000), §4.5.

Motivation

Grover's algorithm is a quantum algorithm for unstructured search: given black-box access to a function $f\colon\{0,1,\dots,N-1\}\to\{0,1\}$ that takes the value $1$ at exactly one input $\omega$, it finds $\omega$ with high probability using $O(\sqrt N)$ evaluations of $f$. It was devised by Lov Grover in 1996 (Grover, STOC 1996). Classically the same task needs $\Theta(N)$ evaluations, since there is no better approach than trying the inputs one after the other. Bennett, Bernstein, Brassard and Vazirani showed that every quantum algorithm needs $\Omega(\sqrt N)$ evaluations (BBBV, SIAM J. Comput. 1997), so the quadratic speedup is optimal.

Because many problems contain exhaustive search as a subroutine, the algorithm and its generalization, amplitude amplification, speed up a broad class of algorithms: brute-force attacks on symmetric-key cryptography (a 128-bit key in roughly $2^{64}$ iterations), algorithms for NP-complete problems such as 3SAT, and black-box problems such as element distinctness and the collision problem.

This mission follows the presentation of the algorithm and of its analysis in the Wikipedia article Grover's algorithm (revision 1373498442), which gives two analyses of the same algorithm, a geometric proof and an algebraic proof, following Nielsen–Chuang 2010, Chapter 6.

Setting

Fix $N \ge 1$. The state space is $\mathcal H = \mathbb C^N$ with standard basis $|0\rangle,\dots,|N-1\rangle$ and inner product $\langle u|v\rangle = \sum_x \overline{u_x}v_x$. Let $f\colon\{0,\dots,N-1\}\to\{0,1\}$ have exactly one index $\omega$ with $f(\omega) = 1$.

• The oracle is the unitary $U_\omega|x\rangle = (-1)^{f(x)}|x\rangle$. The standard oracle acts on $\mathcal H\otimes\mathbb C^2$ (one extra ancillary qubit) by $U_f|x\rangle|y\rangle = |x\rangle|y\oplus f(x)\rangle$.
• The uniform superposition is $|s\rangle = \frac{1}{\sqrt N}\sum_{x=0}^{N-1}|x\rangle$, and the Grover diffusion operator is $U_s = 2|s\rangle\langle s| - I$.
• A Grover iteration applies $U_\omega$ and then $U_s$, i.e. the operator $U_sU_\omega$.

The algorithm. (1) Initialize the system to $|s\rangle$. (2) Perform the Grover iteration $r$ times. (3) Measure the resulting state $(U_sU_\omega)^r|s\rangle$ in the computational basis; by the Born rule the outcome is $\omega$ with probability $|\langle\omega|(U_sU_\omega)^r|s\rangle|^2$.

Two further objects appear in the analysis: the ket $|s'\rangle = \frac{1}{\sqrt{N-1}}\sum_{x\ne\omega}|x\rangle$ perpendicular to $|\omega\rangle$, and the angles $\theta = 2\arcsin\frac{1}{\sqrt N}$ (geometric proof) and $t = \arcsin\frac{1}{\sqrt N} = \theta/2$ (algebraic proof).

Formalization targets

Goal — success probability $1 - 1/N$ within $\lceil\frac\pi4\sqrt N\rceil$ iterations

$$\exists\, r \le \left\lceil\frac{\pi}{4}\sqrt N\right\rceil:\qquad \bigl|\langle\omega|(U_sU_\omega)^r|s\rangle\bigr|^2 \ge 1 - \frac1N .$$

This combines the article's headline claims: the algorithm outputs $\omega$ with probability at least $1/2$ (for $N \ge 2$) using $O(\sqrt N)$ applications of $U_\omega$, the success probability approaches $1$ for $N \gg 1$, and the number of iterations satisfies $r(N) \le \lceil\frac\pi4\sqrt N\rceil$. The goal does not fix $r$.

Milestones

Listed in the article's order.

1. Alternative oracle definition: $U_f\bigl(|x\rangle\otimes|-\rangle\bigr) = (U_\omega|x\rangle)\otimes|-\rangle$ with $|-\rangle = \frac{1}{\sqrt2}(|0\rangle - |1\rangle)$.
2. Unitarity: $U_\omega$ and $U_s$ are unitary.
3. Iteration count: $r(N) = \lfloor\pi/(4t)\rfloor \le \lceil\frac\pi4\sqrt N\rceil$.
4. Geometric proof: on $\mathrm{span}\{|s'\rangle,|\omega\rangle\}$, $U_\omega$ is the reflection across $|s'\rangle$; $U_\omega = I - 2|\omega\rangle\langle\omega|$ (Householder form); $U_s$ is the reflection through $|s\rangle$; $U_sU_\omega$ rotates the plane by $\theta$; $\langle s'|s\rangle = \sqrt{(N-1)/N}$; and the exact success probability is

$$\bigl|\langle\omega|(U_sU_\omega)^r|s\rangle\bigr|^2 = \sin^2\!\bigl((r+\tfrac12)\theta\bigr).$$

5. Algebraic proof: the action of $U_s$ and $U_\omega$ on $\mathrm{span}\{|\omega\rangle,|s\rangle\}$ by explicit $2\times 2$ matrices; the Jordan form $U_sU_\omega = M\,\mathrm{diag}(e^{2it},e^{-2it})\,M^{-1}$ and its $r$-th power; the success probability $\sin^2((2r+1)t)$ computed in coordinates; and, stopping at $r = \lfloor\pi/4t\rfloor$, error at most $1/N$.

Significance

The result. The goal says that unstructured search over $N$ items costs $O(\sqrt N)$ oracle queries on a quantum computer, with failure probability at most $1/N$ for a single run, and hence that the expected number of queries until $\omega$ is found is still $O(\sqrt N)$. It is the quantitative content behind the use of Grover's algorithm as a subroutine and behind its role in post-quantum key-length recommendations.

Formalizing it. The result is classical and fully proved on paper. The work here is to formalize the article's two proofs: the reflection/rotation picture and the algebraic diagonalization, together with the equivalence of the two oracle models and the explicit bound $\lceil\frac\pi4\sqrt N\rceil$ stated in the article. A separate platform mission, Grover's Algorithm, already contains machine-checked proofs of the amplitude formula $\sin((2k+1)\theta)$ and of a success guarantee with iteration bound $\lceil\pi/(4\arcsin(1/\sqrt N))\rceil$, in a model where the oracle is given by the marked index. This mission differs in that it derives the oracle from the function $f$, includes the ancilla-based standard oracle, the Householder and reflection statements, the algebraic Jordan-form analysis, and the bound $\lceil\frac\pi4\sqrt N\rceil$ in terms of $\sqrt N$. The lower bound of Bennett–Bernstein–Brassard–Vazirani (optimality) is out of scope.

Difficulty

None of the steps is deep; the difficulty lies in the bookkeeping. The plane $\mathrm{span}\{|\omega\rangle, |s\rangle\}$ is not spanned by an orthonormal pair, so the matrices of the algebraic proof are in a non-orthogonal spanning set, and the probability formula must be transported from that $2\times2$ picture back to the $N$-dimensional state. Passing from the exact formula $\sin^2((r+\frac12)\theta)$ to the bound $1 - 1/N$ requires choosing an integer $r$, controlling $(2r+1)t$ to within $t$ of $\pi/2$, and comparing $\arcsin(1/\sqrt N)$ with $1/\sqrt N$ to reach $\lceil\frac\pi4\sqrt N\rceil$. Edge cases matter: $N = 1$ (where $t = \pi/2$, $|s'\rangle$ is undefined and $M$ is singular) and the integer rounding of $r = \pi/4t$.

Formalization scope

All statements import one definitions file, GroverWiki_Defs, and live in the namespace GroverWiki.

• States are vectors Fin N → ℂ; operators are matrices Matrix (Fin N) (Fin N) ℂ acting by mulVec; the two-register space is indexed by Fin N × Fin 2. Bit values are Fin 2, so ⊕ is addition in Fin 2.
• The oracle is built from f : Fin N → Fin 2; uniqueness of the marked item is the hypothesis ∀ x, f x = 1 ↔ x = ω.
• The measurement probability of outcome x is ‖ψ x‖ ^ 2, applied to the state (U_s U_ω)^r |s⟩.
• Scalars such as $1/\sqrt N$ are real numbers cast to $\mathbb C$. For $N = 1$, Lean's conventions give $|s'\rangle = 0$; statements about $|s'\rangle$ or $M^{-1}$ assume $N \ge 2$, as the article implicitly does.
• The article's non-integer $r = \pi/4t$ is formalized as $\lfloor \pi/4t\rfloor$, and "error $O(1/N)$" as the explicit bound $1/N$.

The goal is not trivialized by the model: the state is the actual output of the algorithm, the iteration count is bounded explicitly, and the probability bound is the Born-rule probability of the marked index. Contributions of reusable lemmas on reflections and rotations in two-dimensional subspaces of $\mathbb C^N$ are welcome.

Selected references

• L. K. Grover, A fast quantum mechanical algorithm for database search, Proc. 28th ACM STOC, 1996. https://doi.org/10.1145/237814.237866 (arXiv: https://arxiv.org/abs/quant-ph/9605043)
• C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5), 1997. https://doi.org/10.1137/s0097539796300933
• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2010, pp. 276–305. https://doi.org/10.1017/CBO9780511976667
• Wikipedia, Grover's algorithm, revision 1373498442. https://en.wikipedia.org/w/index.php?title=Grover%27s_algorithm&oldid=1373498442

Motivation

A sequence of real numbers $(m_0, m_1, m_2, \dots)$ often arrives as a list of moments: averages $\mathbb E[X^n]$ of powers of a random variable, traces $\langle T^n e, e\rangle$ of powers of a self-adjoint operator, or coefficients of a continued fraction. The Hamburger moment problem, named after Hans Ludwig Hamburger (1920–21), asks when such a list really comes from a measure on the whole real line, and, when it does, whether the measure is determined by its moments. The question sits at the junction of probability (the method of moments, identification of limit laws), spectral theory of symmetric operators and Jacobi matrices, and the theory of orthogonal polynomials; standard monographs include Shohat–Tamarkin (1943) and Schmüdgen (2017).

Timeline (as summarized in the source article and its references):

1. 1894 — Stieltjes treats the analogous problem on $[0,+\infty)$ (the Stieltjes moment problem).
2. 1920–21 — Hamburger extends the theory to the whole real line: solvability is equivalent to positivity of the Hankel kernel $(m_{j+k})$.
3. 1920s — Carleman gives a growth condition on the moments guaranteeing uniqueness (Carleman's condition); the factorial growth bound $|m_n| \le C D^n n!$ is a special case (Reed–Simon 1975, p. 205).
4. Later — the operator-theoretic treatment through self-adjoint extensions of the shift operator and its spectral measure becomes standard (Reed–Simon 1975, p. 145).

Setting

Let $m = (m_n)_{n \ge 0}$ be a sequence of real numbers. A solution of the Hamburger moment problem for $m$ is a positive Borel measure $\mu$ on $\mathbb R$ such that every power $x^n$ is $\mu$-integrable and

$$m_n = \int_{-\infty}^{\infty} x^n \, d\mu(x) \qquad (n = 0, 1, 2, \dots).$$

The sequence $m$ is a moment sequence if at least one solution exists.

The Hankel kernel of $m$ is the infinite matrix $A = (m_{j+k})_{j,k \ge 0}$. It is positive definite (in the sense of the source) if

$$\sum_{j,k \ge 0} m_{j+k}\, c_j \overline{c_k} \;\ge\; 0$$

for every finitary complex sequence $(c_j)_{j \ge 0}$, i.e. $c_j = 0$ for all but finitely many $j$. Its finite sections are the $(n+1)\times(n+1)$ Hankel matrices

$$\Delta_n = (m_{i+j})_{0 \le i,j \le n}.$$

In the Lean development these objects are IsMomentMeasure m μ, IsMomentSequence m, hankelForm m c, HankelPosDef m and hankelMatrix m n, all in the namespace HamburgerMoment.

Formalization targets

Goal — Hamburger's characterization

$$m \text{ is a moment sequence} \iff \sum_{j,k \ge 0} m_{j+k} c_j \overline{c_k} \ge 0 \text{ for every finitary } (c_j) \subset \mathbb C.$$

Milestones

1. The identity $\sum_{j,k} m_{j+k} c_j \overline{c_k} = \int |\sum_j c_j x^j|^2 \, d\mu(x)$ for any solution $\mu$, and the resulting "only if" direction.
2. The "if" direction: a positive definite Hankel kernel is the kernel of a moment sequence.
3. The solution set is convex; hence a solvable problem has either a unique solution or infinitely many.
4. Positivity of $A$ gives $\det \Delta_n \ge 0$ for all $n$; if $\det \Delta_n = 0$ for some $n$, the solution is unique and finitely supported.
5. Uniqueness under the growth bound $|m_n| \le C D^n n!$.
6. Existence of moment sequences with more than one solution.
7. The real-polynomial identity $\int p^2 \, d\mu = \sum_{j,k} a_j a_k m_{j+k} \ge 0$, and the characterization of moment sequences by positive semidefiniteness of all real Hankel matrices $\Delta_n$.

Significance

The result. Hamburger's theorem turns an existence question about measures into a family of finite-dimensional positivity conditions that can be checked on the data. It is the basic tool behind the method of moments in probability (identifying a distribution from its moments, when the problem is determinate), behind the spectral theory of Jacobi matrices, and behind Gauss quadrature and orthogonal polynomials on the line. The uniqueness criteria decide when moments determine a law; the non-uniqueness examples (for instance the log-normal distribution) show that they do not always do so.

Formalizing it. All results here are classical and proved in the literature; to the best of the captain's knowledge none of them is currently available as a formal statement in Mathlib, which has neither moment problems nor Hankel kernels. The mission produces a reusable vocabulary (moment measures, Hankel forms and matrices) and machine-checked versions of the existence theorem, the uniqueness criteria and the non-uniqueness phenomenon.

Difficulty

The "only if" direction is a direct computation. The converse is the substance: from positivity of countably many finite quadratic forms one must produce a countably additive measure on a non-compact space with all moments matching. Compactness arguments on finite sections give measures whose low-order moments match, but mass can escape to infinity and higher moments need not converge; the source's route instead goes through the Hilbert space completion of finitary sequences, self-adjoint extensions of the (generally unbounded) shift operator and the spectral theorem for unbounded self-adjoint operators — machinery that is only partly present in Mathlib. An alternative route via positive linear functionals on polynomials (M. Riesz extension, Riesz–Markov–Kakutani) has to control the same escape of mass. The uniqueness criterion requires quasi-analyticity or Carleman-type estimates.

Formalization scope

1. Sequences are m : ℕ → ℝ; measures are Measure ℝ on the Borel σ-algebra of $\mathbb R$. A solution must have every power $x^n$ integrable, so in particular $\mu$ is finite with total mass $m_0$.
2. Finitary complex sequences are finitely supported functions ℕ →₀ ℂ, and the Hankel form is the finite double sum over the support. "$\ge 0$" is the order on $\mathbb C$ (the value is a nonnegative real number), matching the source.
3. $\Delta_n$ is the real matrix indexed by Fin (n + 1); positive semidefiniteness is Mathlib's Matrix.PosSemidef.
4. Uniqueness statements quantify over all solutions; finite support means the solution vanishes outside a finite set.

Needed infrastructure and welcome contributions: polynomial integrability under finite moments, positive linear functionals on $\mathbb R[x]$, a Riesz–Markov or spectral-measure construction on $\mathbb R$, Vandermonde arguments for finitely supported measures, and Carleman / quasi-analyticity estimates. The definitions of moment measures and Hankel kernels are reusable for the Stieltjes and Hausdorff moment problems.

Selected references

• Wikipedia, Hamburger moment problem, revision oldid=1356180072, https://en.wikipedia.org/w/index.php?title=Hamburger_moment_problem&oldid=1356180072
• H. Hamburger, Über eine Erweiterung des Stieltjesschen Momentenproblems, Math. Ann. 81 (1920), 235–319; 82 (1921), 120–164, 168–187.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, pp. 145, 205.
• T. S. Chihara, An Introduction to Orthogonal Polynomials, Gordon and Breach, 1978, pp. 56, 73.
• K. Schmüdgen, The Moment Problem, Graduate Texts in Mathematics 277, Springer, 2017. https://doi.org/10.1007/978-3-319-64546-9
• J. A. Shohat, J. D. Tamarkin, The Problem of Moments, AMS, 1943.

Motivation

Shor's algorithm is a quantum algorithm that finds a nontrivial factor of an integer $N$ in time polynomial in $\log N$, and its variants compute discrete logarithms in finite cyclic groups. It was developed by Peter Shor in 1994 (Shor, FOCS 1994; Shor, SIAM J. Comput. 1997). No classical polynomial-time factoring algorithm is known; the best classical method, the general number field sieve, runs in sub-exponential time. Because the security of RSA and of finite-field and elliptic-curve Diffie–Hellman rests on the hardness of factoring and of discrete logarithms, Shor's algorithm is the main reason these schemes are considered breakable by a large fault-tolerant quantum computer, and the main motivation for post-quantum cryptography.

This mission follows the presentation of the algorithm in the Wikipedia article Shor's algorithm (revision 1378862216), which describes the quantum part through quantum phase estimation, an approach due to Kitaev (Kitaev 1995) and standard in textbooks (Nielsen–Chuang 2010).

Setting

Let $1 < a < N$ be integers with $\gcd(a, N) = 1$. The order $r = \operatorname{ord}_N(a)$ is the smallest positive integer with $a^r \equiv 1 \pmod N$.

Classical reduction. If $r$ is even and $N \nmid a^{r/2}+1$, then $\gcd(N, a^{r/2}-1)$ is a nontrivial factor of $N$. Factoring therefore reduces to computing orders.

Quantum order finding. Let $n = \lceil\log_2 N\rceil$ and $Q = 2^{2n}$. A state of an $m$-qubit register is a vector in $\mathbb C^{2^m}$ with standard basis $|0\rangle, \dots, |2^m-1\rangle$. The modular-multiplication gate is the $n$-qubit gate

$$U|k\rangle = |ak \bmod N\rangle \ (0 \le k < N), \qquad U|k\rangle = |k\rangle \ (N \le k < 2^n).$$

With $\omega_r = e^{2\pi i/r}$, the states $|\psi_j\rangle = r^{-1/2}\sum_{k=0}^{r-1}\omega_r^{-kj}|a^k \bmod N\rangle$ are eigenvectors of $U$ with eigenvalues $\omega_r^j$. The order-finding circuit acts on a $2n$-qubit first register and the $n$-qubit second register: Hadamard gates $H^{\otimes 2n}$ on the first register, controlled gates $C\text{-}U^{2^i}$ for $i = 0, \dots, 2n-1$ (qubit $i$ of the first register controls $U^{2^i}$ on the second), and the inverse quantum Fourier transform $\mathrm{QFT}^{-1}_{2^{2n}}$ on the first register. It is applied to $|0\rangle^{\otimes 2n}|1\rangle$ and the first register is measured, producing an outcome $k \in \{0, \dots, Q-1\}$ with probability $P(k)$. Finally the continued fractions algorithm is run on $k/Q$.

Formalization targets

Goal: one run of the order-finding subroutine

For every $j \in \{0, \dots, r-1\}$,

$$\sum_{k\,:\,|k/2^{2n} - j/r| \le 2^{-(2n+1)}} P(k) \;\ge\; \frac{4}{\pi^2 r},$$

and for every such $k$ some continued fraction convergent of $k/2^{2n}$ equals $j/r$ in lowest terms, i.e. has numerator $j/\gcd(j,r)$ and denominator $r/\gcd(j,r)$. Summed over $j$, a single run yields with probability at least $4/\pi^2$ an outcome from which the continued fractions algorithm recovers some $j/r$ in lowest terms.

Milestones

1. Classical reduction (article section "Classical reduction"): $\gcd(a,N) \ne 1$ is a nontrivial factor; $N \mid (a^{r/2}-1)(a^{r/2}+1)$ for even $r$; $N \nmid a^{r/2}-1$; and $\gcd(N, a^{r/2} \mp 1)$ are nontrivial factors when $N \nmid a^{r/2}+1$.
2. Spectrum of $U$ (section "Quantum phase estimation"): $U^r = I$; every eigenvalue is some $\omega_r^k$; $U|\psi_j\rangle = \omega_r^j|\psi_j\rangle$; $\sum_{j}\omega_r^{jk} = 0$ for $1 \le k \le r-1$; $r^{-1/2}\sum_j|\psi_j\rangle = |1\rangle$.
3. Phase estimation: on $|0\rangle^{\otimes 2n}|\psi_j\rangle$ the circuit outputs $|\phi_j\rangle|\psi_j\rangle$ with $|\langle k|\phi_j\rangle|^2 \ge 4/\pi^2$ at every nearest integer $k$ to $2^{2n}j/r$; on $|0\rangle^{\otimes 2n}|1\rangle$ each $|\phi_j\rangle$ is found with probability $1/r$.
4. Continued fractions and register size (section "Choosing the size of the first register"): $|j/r - \varphi| < 1/(2r^2)$ implies $\varphi$ has $j/r$ in lowest terms as a convergent, and $2^{-(2n+1)} \le 1/(2N^2) \le 1/(2r^2)$.
5. Discrete logarithms (section "Shor's algorithm for discrete logarithms"): $f(a,b) = g^a x^{-b}$ on $\mathbb Z_p \times \mathbb Z_p$ is a homomorphism with kernel the multiples of $(r,1)$.

Significance

The goal is the quantitative statement behind the article's claim that phase estimation "gives as output a random integer of the form $\frac{j}{r}2^{2n}$" and that a $2n$-qubit first register suffices to recover $j/r$. Combined with the classical milestones, it is the correctness argument of Shor's factoring algorithm, minus the separate number-theoretic estimate of how often a random $a$ has even order with $a^{r/2} \not\equiv -1$, which the article does not state.

The results are classical and their proofs are published. The work this mission asks for is a machine-checked proof against an explicit gate-level model of the circuit — Hadamard tensor power, controlled modular-multiplication gates, inverse QFT — rather than against a closed-form output distribution assumed up front. Related missions on the platform formalize Shor's 1997 paper, which analyses the circuit by a direct Fourier-sum computation with $q \ge N^2$; this mission follows the phase-estimation route with the article's constants.

Difficulty

The spectral facts about $U$ and the classical reduction are short arguments. The main obstacle is the circuit: showing that the product of the $2n$ controlled gates $C\text{-}U^{2^i}$ acts on $|x\rangle|\psi_j\rangle$ as multiplication by $\omega_r^{jx}$ requires the binary expansion of $x$ and the commutation of the controlled gates, and the subsequent inverse QFT must be computed explicitly. The bound $4/\pi^2$ requires an estimate of $\left|\sum_{x<Q} e^{2\pi i x\delta}\right|$ for $|\delta| \le 1/(2Q)$ which is uniform in $Q$; a crude estimate gives a weaker constant. The measurement identity $P(k) = \frac1r\sum_j P_j(k)$ requires the orthonormality of the $|\psi_j\rangle$, which uses that $a^0, \dots, a^{r-1}$ are distinct modulo $N$.

Formalization scope

States are coordinate vectors Fin d → ℂ, gates are complex matrices acting by Matrix.mulVec, two-register operators are Kronecker products on Fin d₁ × Fin d₂, and measurement probabilities are sums of squared moduli. The order is orderOf (a : ZMod N) and $n$ is Nat.clog 2 N. Convergents are Mathlib's Real.convergent, the standard continued fraction expansion. The goal is a statement about the specific circuit defined in the mission's definition file, so it cannot be satisfied by choosing a convenient output distribution, and the recovery statement is quantified over a fixed $j$, so the trivial convergent $\lfloor k/Q\rfloor = 0$ (which equals $0/r$) does not discharge it for $j \ne 0$.

Reusable infrastructure welcome from this mission: the action of the Kronecker-product phase estimation circuit on eigenstates, the explicit inverse QFT computation, and the $4/\pi^2$ estimate for the Fejér-type kernel.

Selected references

• P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/sfcs.1994.365700
• P. W. Shor, Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer, SIAM J. Comput. 26(5), 1997. https://arxiv.org/abs/quant-ph/9508027
• A. Yu. Kitaev, Quantum measurements and the Abelian stabilizer problem, 1995. https://arxiv.org/abs/quant-ph/9511026
• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2010. https://doi.org/10.1017/CBO9780511976667
• Wikipedia, Shor's algorithm, revision 1378862216. https://en.wikipedia.org/w/index.php?title=Shor%27s_algorithm&oldid=1378862216

Motivation

Generalized complex geometry, introduced by N. Hitchin (Generalized Calabi–Yau manifolds, 2003) and developed by M. Gualtieri (thesis, 2004; Annals 2011), treats complex and symplectic structures as two special cases of one notion. It replaces the tangent bundle $T$ of a manifold by the generalized tangent bundle $T\oplus T^*$ and an almost complex structure on $T$ by an orthogonal almost complex structure on $T\oplus T^*$. The framework is used in string theory: supersymmetric flux compactifications require (possibly twisted) generalized complex structures (Graña 2006).

The pointwise theory is pure linear algebra, and the global statements of the subject rest on it: the equivalence between a generalized almost complex structure and its $\sqrt{-1}$-eigenbundle, Gualtieri's classification of maximal isotropic subspaces by pairs $(E,\varepsilon)$, the type invariant and its behaviour under B-field shifts, and the two model examples (complex and symplectic). This mission formalizes that linear-algebraic layer as presented in the Wikipedia article Generalized complex structure.

Setting

Fix $N\ge 0$. A fiber of the tangent bundle is $T=\mathbb R^N$; its dual $T^*$ is identified with $\mathbb R^N$ through the standard dual basis, so a one-form $\xi$ acts by $\xi(Y)=\sum_i\xi_iY_i$. The generalized tangent space is $T\oplus T^*$, whose elements are formal sums $X+\xi$, with the natural inner product of signature $(N,N)$

$$\langle X+\xi,\;Y+\eta\rangle=\tfrac12\bigl(\xi(Y)+\eta(X)\bigr).$$

The same formula defines a complex bilinear form on the complexification $(T\oplus T^*)\otimes\mathbb C=\mathbb C^N\oplus\mathbb C^N$, which carries the complex conjugation $v\mapsto\bar v$.

1. A generalized almost complex structure is a real linear map $\mathcal J:T\oplus T^*\to T\oplus T^*$ with $\mathcal J^2=-\mathrm{Id}$ and $\langle\mathcal J u,\mathcal J v\rangle=\langle u,v\rangle$.
2. Its $\sqrt{-1}$-eigenbundle is $L=\{v\in(T\oplus T^*)\otimes\mathbb C:\ \mathcal J v=\sqrt{-1}\,v\}$; $\bar L$ denotes the conjugate subspace.
3. A subspace $L$ is isotropic if $\langle\ell,\ell'\rangle=0$ for all $\ell,\ell'\in L$, and maximal isotropic if moreover $\dim L=N$.
4. For a subspace $E\subseteq T$ and a bilinear form $\varepsilon$ on $E$, $L(E,\varepsilon)=\{X+\xi:\ X\in E,\ \xi|_E=\varepsilon(X,\cdot)\}$.
5. The type of a complex subspace $L$ is $2N$ minus the real dimension of its projection $\pi_T(L)$ to $T\otimes\mathbb C$, i.e. $2\,(N-\dim_{\mathbb C}\pi_T(L))$; the real index is $r=\dim_{\mathbb C}(L\cap\bar L)$.
6. The B-field shift by a 2-form $B$ is $e^B(X+\xi)=X+\xi+i_XB$.
7. An almost complex structure $J_0$ on $T$ gives $\mathcal J_{J_0}(X+\xi)=-J_0X+\xi\circ J_0$; a nondegenerate 2-form $\omega$ gives $\mathcal J_\omega(X+\xi)=-(\omega^\flat)^{-1}\xi+\omega^\flat X$ with $\omega^\flat X=i_X\omega$.

Formalization targets

Goal: the eigenbundle correspondence

For every generalized almost complex structure $\mathcal J$, its eigenbundle $L$ satisfies

$$\text{(i)}\ L\cap\bar L=0,\qquad\text{(ii)}\ L\ \text{is maximal isotropic},$$

and conversely every complex subspace $L$ satisfying (i) and (ii) is the $\sqrt{-1}$-eigenbundle of a unique generalized almost complex structure. Hence (i), (ii) form an alternative definition of generalized almost complex structure.

Milestones

1. The eigenbundle of $\mathcal J$ satisfies (i) and (ii).
2. $\mathcal J$ is uniquely determined by its eigenbundle.
3. Every $L$ satisfying (i), (ii) is the eigenbundle of some $\mathcal J$.
4. $L(E,\varepsilon)$ is maximal isotropic whenever $\varepsilon$ is a 2-form (real or complex case).
5. Every maximal isotropic subspace has the form $L(E,\varepsilon)$ (Gualtieri).
6. The pair $(E,\varepsilon)$ is determined by $L(E,\varepsilon)$.
7. A generalized almost complex structure has type at most $N$.
8. B-field shifts are isometries of $T\oplus T^*$.
9. The type is invariant under B-field shifts.
10. A maximal isotropic $L$ is the eigenbundle of a generalized almost complex structure iff $r=0$.
11. Complex structures give generalized almost complex structures of type $N$.
12. Nondegenerate 2-forms give generalized almost complex structures of type $0$.
13. Up to a B-field shift, the symplectic ones are the only structures of type $0$.

Significance

The goal makes the two descriptions of a generalized almost complex structure interchangeable: integrability (closure of $L$ under the Courant bracket), the canonical pure-spinor line and the type are all phrased in terms of $L$, while the definition is phrased in terms of $\mathcal J$. The classification by $(E,\varepsilon)$ is the normal form behind the type, the local classification near regular points, and the identification of the complex and symplectic extremes. All of these results are classical and proved in the cited literature; the remaining work is their machine-checked formalization. A formal library of this linear algebra is a prerequisite for later missions on the manifold-level theory (Courant bracket, generalized Darboux theorem).

Difficulty

The goal mixes real and complex linear algebra. Recovering a real map $\mathcal J$ from a complex subspace $L$ requires knowing that $L\oplus\bar L$ is the whole complexification and that the map which is $\sqrt{-1}$ on $L$ and $-\sqrt{-1}$ on $\bar L$ commutes with conjugation and is orthogonal; each of these uses hypotheses (i) and (ii), and the dimension condition $\dim L=N$ cannot be dropped. The classification needs a dimension count for $L(E,\varepsilon)$ (functionals on $E$ versus the annihilator of $E$) and, in the converse direction, the extraction of $\varepsilon$ from an arbitrary maximal isotropic subspace. For the complex example, the type computation requires the dimension of the $-\sqrt{-1}$-eigenspace of a real complex structure, which is exactly $N/2$.

Formalization scope

Everything is fiberwise and in coordinates: $T=\mathbb R^N$ is Fin N → ℝ, $T\oplus T^*$ is GIdx N → ℝ with GIdx N = Fin N ⊕ Fin N (vector part on Sum.inl, one-form part on Sum.inr), endomorphisms are matrices over GIdx N, and the complexification is GIdx N → ℂ with the real matrix acting through $\mathbb R\to\mathbb C$. 2-forms on $T$ are skew matrices $B$ with $B(X,Y)=X^{\mathsf T}BY$; 2-forms on a subspace $E$ are skew bilinear forms on $E$. Nondegeneracy of $\omega$ is $\det\omega\neq0$ (the inverse used in $\mathcal J_\omega$ is the matrix inverse). The type uses the article's real-dimension convention, so it is twice Gualtieri's complex type. The classification milestones are stated over RCLike fields, i.e. for both $\mathbb R$ and $\mathbb C$, as in the article.

Out of scope for this mission: the Courant bracket and integrability, the canonical (pure spinor) bundle, upper semicontinuity of the type, the generalized Darboux theorem, local holomorphicity, and the $G$-structure description. These need manifold-level infrastructure (Lie derivatives and exterior derivatives of forms on manifolds) and are left for later missions.

Selected references

• N. Hitchin, Generalized Calabi–Yau manifolds, Q. J. Math. 54 (2003) 281–308. https://doi.org/10.1093/qmath/hag025
• M. Gualtieri, Generalized complex geometry, PhD thesis, Oxford, 2004. https://arxiv.org/abs/math.DG/0401221
• M. Gualtieri, Generalized complex geometry, Ann. of Math. 174 (2011) 75–123. https://arxiv.org/abs/0911.0993
• M. Graña, Flux compactifications in string theory: a comprehensive review, Phys. Rep. 423 (2006) 91–158. https://arxiv.org/abs/hep-th/0509003
• Wikipedia, Generalized complex structure (revision 1288019306). https://en.wikipedia.org/w/index.php?title=Generalized_complex_structure&oldid=1288019306

Motivation

The AdS/CFT correspondence (Maldacena 1997) relates quantum gravity on anti-de Sitter (AdS) space to a conformal field theory (CFT) living on its timelike boundary. Gubser–Klebanov–Polyakov and Witten gave the CFT-from-AdS direction of the dictionary: CFT correlators are computed from bulk Green functions. Giddings (PRL 83, 2707, 1999) supplies an entry in the reverse direction. Because AdS confines particles and has no ordinary asymptotic states, a flat-space S matrix does not exist; the paper defines a boundary S matrix from in/out states built out of wave packets incident from the boundary, derives an LSZ-type reduction formula (eq. 42), and concludes that the boundary S matrix equals the boundary CFT correlator (eqs. 44–45).

Every step of that argument rests on the classical theory of the free Klein–Gordon field on global AdS: the parameters $h_\pm,\nu$ (eq. 4), the discrete normalizable spectrum $\omega_{nl}=2h_++2n+l$ with modes behaving like $(\cos r)^{2h_+}$ at the boundary (eqs. 5–7), the non-normalizable modes behaving like $(\cos r)^{2h_-}$ (eqs. 8–9), and the boundary limit (eqs. 19–20) that fixes the normalization $2\nu$ of the bulk–boundary propagator.

Setting

Fix an integer $d\ge 2$, an AdS radius $R>0$ and a scalar mass $m\in\mathbb R$. Global $\mathrm{AdS}_{d+1}$ has metric (eq. 2)

$$ds^2=R^2\sec^2 r\,\bigl(-dt^2+dr^2+\sin^2 r\,d\Omega_{d-1}^2\bigr),\qquad 0\le r<\tfrac\pi2 .$$

Define (eq. 4)

$$\nu=\tfrac12\sqrt{d^2+4m^2R^2},\qquad 2h_\pm=\tfrac d2\pm\nu .$$

A mode $\phi=e^{-i\omega t}Y_{l\vec m}(\Omega)\chi(r)$, with $Y_{l\vec m}$ a spherical harmonic on $S^{d-1}$, solves the free equation $(\Box-m^2)\phi=0$ (eq. 3) exactly when the radial profile $\chi$ satisfies, on $0<r<\pi/2$,

$$\chi''+\frac{d-1}{\sin r\cos r}\chi'+\omega^2\chi-\frac{l(l+d-2)}{\sin^2 r}\chi-\frac{m^2R^2}{\cos^2 r}\chi=0 .$$

A normalizable mode is a nonzero $C^2$ solution that is bounded as $r\to0$ (regular at the centre of AdS) and has finite Klein–Gordon norm, i.e. $\int_0^{\pi/2}\tan^{d-1}r\,\chi(r)^2\,dr<\infty$. The explicit modes of eq. (5) are

$$\chi_{nl}(r)=\sin^l r\,(\cos r)^{2h_+}\,P_n^{(l+d/2-1,\;\nu)}(\cos 2r),$$

with $P_n^{(\alpha,\beta)}$ the Jacobi polynomial, and the eigenfrequencies of eq. (7) are $\omega_{nl}=2h_++2n+l$.

Formalization targets

Goal: the normalizable spectrum (eqs. 3–7)

For every $\omega\in\mathbb R$, $l\in\mathbb N$ and radial profile $\chi$,

$$\chi \text{ is a normalizable mode at }(\omega,l)\iff \exists n\in\mathbb N:\ |\omega|=\omega_{nl}\ \text{and}\ \chi=c\,\chi_{nl}\text{ on }(0,\tfrac\pi2)\text{ for some }c\neq0 .$$

Milestones

1. Eq. (4): $2h_\pm$ are the two roots of $\Delta(\Delta-d)=m^2R^2$, and $2h_+-2h_-=2\nu$.
2. Eqs. (5), (7): $\chi_{nl}$ solves the radial equation at $\omega=\omega_{nl}$.
3. Eq. (6): $\chi_{nl}(r)/(\cos r)^{2h_+}\to k_{nl}\neq0$ as $r\to\pi/2$.
4. Eq. (5): $\chi_{nl}$ is a normalizable mode at $(\omega_{nl},l)$.
5. Eqs. (8)–(9): for $|\omega|$ outside the spectrum there is a solution regular at $r=0$ with $\chi(r)/(\cos r)^{2h_-}\to1$.
6. Eqs. (19)–(20): $\displaystyle\lim_{r\to\pi/2}(\tan r)^{d-1}\bigl[(\cos r)^{2h_-}\overleftrightarrow{\partial_r}(\cos r)^{2h_+}\bigr]=-2\nu$.
7. Eqs. (12), (33): $\Delta_b>\Delta\Rightarrow(\cos r)^{\Delta_b-\Delta}\to0$.
8. Eqs. (23), (42)–(44): given Witten's formula (43), the LSZ expression (42) built from the wave packets (23) equals $\int\prod_a[db_a\,f_a(b_a)/Z_a]\,\langle T\prod_a\mathcal O(b_a)\rangle$.

Significance

The goal is the precise mathematical content behind the paper's statement that free solutions "exist at arbitrary frequency but are only normalizable for a discrete set of frequencies". This spectrum is what makes the boundary operators $a_{\omega l\vec m}$ of eq. (25) act as creation and annihilation operators (eqs. 27–29), and the boundary exponents $2h_\pm$ and the constant $2\nu$ determine the normalizations in eqs. (20), (21), (28) and (29). The physics derivation of eqs. (28)–(42) is not rigorous mathematics; milestone 8 isolates the final step from (42)–(43) to (44), which is an exact identity about integral kernels.

The radial results are classical (the paper attributes the explicit solutions to Balasubramanian–Kraus–Lawrence). This mission asks for machine-checked proofs of these results, together with the reusable Jacobi-polynomial and boundary-asymptotics infrastructure they require.

Difficulty

Verifying that $\chi_{nl}$ solves the equation is a computation. The goal's converse direction is the hard part: one must show that a solution regular at $r=0$ can have finite Klein–Gordon norm only when $|\omega|$ equals some $\omega_{nl}$, and that it is then unique up to a scalar. This requires controlling both regular singular points $r=0$ and $r=\pi/2$ of the radial equation, including the resonant cases where $2\nu$ or $l+d/2-1$ is an integer and logarithms appear. Since $d\ge2$ forces $\nu\ge1$, the $(\cos r)^{2h_-}$ branch is never square-integrable, so the second quantization available for $0<\nu<1$ does not arise.

Formalization scope

• $d$ is a natural number with $d\ge2$; $m,R$ are real with $R>0$; $l,n$ are natural numbers; $\omega$ is real and only $|\omega|$ matters.
• Radial profiles are real-valued functions $\mathbb R\to\mathbb R$; only their values on $(0,\pi/2)$ enter any definition. Complex modes reduce to their real and imaginary parts.
• Regularity at the origin is encoded as boundedness of $|\chi|$ on $(0,\pi/4]$. Finite Klein–Gordon norm is integrability of $\tan^{d-1}r\,\chi(r)^2$ on $(0,\pi/2)$.
• The Jacobi polynomial is defined by the explicit finite sum with generalized binomial coefficients. Powers of $\cos r$ with real exponents use Real.rpow; $\cos r>0$ on the relevant range.
• Nontriviality ($\chi\neq0$ somewhere) is part of the definition of a normalizable mode, so the zero function never counts.
• Milestone 8 takes the LSZ right-hand side (42) as the definition of the boundary S matrix and Witten's relation (43) as a hypothesis, with joint integrability of the integrand. In- and out-packets are listed together, and the plane-wave limit (45) is not formalized.

Selected references

• S. B. Giddings, Boundary S matrix and the anti–de Sitter space to conformal field theory dictionary, Phys. Rev. Lett. 83, 2707 (1999). https://doi.org/10.1103/PhysRevLett.83.2707
• V. Balasubramanian, P. Kraus, A. Lawrence, Bulk vs. boundary dynamics in anti-de Sitter spacetime, Phys. Rev. D 59, 046003 (1999). https://arxiv.org/abs/hep-th/9805171
• E. Witten, Anti de Sitter space and holography, Adv. Theor. Math. Phys. 2, 253 (1998). https://arxiv.org/abs/hep-th/9802150
• J. Maldacena, The large N limit of superconformal field theories and supergravity, Adv. Theor. Math. Phys. 2, 231 (1998). https://arxiv.org/abs/hep-th/9711200
• S. S. Gubser, I. Klebanov, A. Polyakov, Gauge theory correlators from non-critical string theory, Phys. Lett. B 428, 105 (1998). https://arxiv.org/abs/hep-th/9802109