All missions

Motivation

It is not a problem to complement a classical bit, i.e. to change the value of a bit, a 0 to a 1 and vice versa. This is accomplished by a NOT gate. Complementing a qubit in an unknown state, however, is another matter. We show that this operation cannot be done perfectly. We define the Universal-NOT (U-NOT) gate which out of N identically prepared pure input qubits generates M output qubits in a state which is as close as possible to the perfect complement. This gate can be realized by classical estimation and subsequent re-preparation of complements of the estimated state. Its fidelity is therefore equal to the fidelity F= (N+1)/(N+2) of optimal estimation, and does not depend on the required number of outputs. We also show that when some additional a priori information about the state of input qubit is available, than the fidelity of the quantum NOT gate can be much better than the fidelity of estimation.

This mission is the statement-level formalization of Optimal Manipulations with Qubits: Universal NOT Gate (arXiv:quant-ph/9901053v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal universal NOT error (Theorem (unnumbered), PDF p.3: optimal universal NOT error, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Optimal Manipulations with Qubits: Universal NOT Gate, arXiv:quant-ph/9901053v1, https://arxiv.org/abs/quant-ph/9901053v1

Motivation

Given a completely positive (CP) map $T$, there is a theorem of the Radon-Nikodym type [W.B. Arveson, Acta Math. {\bf 123}, 141 (1969); V.P. Belavkin and P. Staszewski, Rep. Math. Phys. {\bf 24}, 49 (1986)] that completely characterizes all CP maps $S$ such that $T-S$ is also a CP map. This theorem is reviewed, and several alternative formulations are given along the way. We then use the Radon-Nikodym formalism to study the structure of order intervals of quantum operations, as well as a certain one-to-one correspondence between CP maps and positive operators, already fruitfully exploited in many quantum information-theoretic treatments. We also comment on how the Radon-Nikodym theorem can be used to derive norm estimates for differences of CP maps in general, and of quantum operations in particular.

This mission is the statement-level formalization of Radon-Nikodym derivatives of quantum operations (arXiv:math-ph/0303056v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stinespring Radon–Nikodym theorem (Theorem 3.1: Stinespring Radon–Nikodym theorem (seed resolved from abstract), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

6 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 2.1 (Haagerup–Paulsen–Wittstock): A valid scope for the unrestricted spatial HPW factorization (source-ambiguity)
• §2.3, unnumbered: CB norm and predual diamond norm: Compatible Banach trace-class predual, finite amplifications, trace pairing, spatial factorization cost set and attainment (hard)
• Theorem 3.5: diagonal Kraus form as printed: A justified pure-point spectral assumption for the canonical RN derivative (source-ambiguity)
• Theorem 5.1: uniform m^2-domination as printed: A consistent normalization for the uniform m^2 domination assertion (source-ambiguity)
• §5.3, unnumbered: unit domination of T_omega as printed: A normalization or scale factor for the unit-domination assertion (source-ambiguity)
• §5.3, unnumbered: regularized faithful-state reconstruction: Normal tensor amplification of CP superoperators and construction of the infinite weighted Choi operator (hard)

Selected references

• Radon-Nikodym derivatives of quantum operations, arXiv:math-ph/0303056v3, https://arxiv.org/abs/math-ph/0303056v3

Motivation

We construct the unique optimal quantum device for turning a finite number of d-level quantum systems in the same unknown pure state σinto M systems of the same kind, in an approximation of the M-fold tensor product of the state σ.

This mission is the statement-level formalization of Optimal Cloning of Pure States (arXiv:quant-ph/9804001v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The unique optimal pure-state cloner (§4, unnumbered Theorem: unique optimal pure-state cloner, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Section 2: same-optimum sentence: A precisely scoped nonvacuous common-optimizer statement for the named p-norm losses and relative entropy in its printed argument order. (source-ambiguity)

Selected references

• Optimal Cloning of Pure States, arXiv:quant-ph/9804001v1, https://arxiv.org/abs/quant-ph/9804001v1

Motivation

We study some structural aspects of the subspaces of the non-commutative (Haagerup) L_p-spaces associated with a general (non necessarily semi-finite) von Neumann algebra A. If a subspace X of L_p(A) contains uniformly the spaces \ell_p^n, n>= 1, it contains an almost isometric, almost 1-complemented copy of \ell_p. If X contains uniformly the finite dimensional Schatten classes S_p^n, it contains their \ell_p-direct sum too. We obtain a version of the classical Kadec-Pel czynski dichotomy theorem for L_p-spaces, p>= 2. We also give operator space versions of these results. The proofs are based on previous structural results on the ultrapowers of L_p(A), together with a careful analysis of the elements of an ultrapower [L_p(A)]_U which are disjoint from the subspace L_p(A). These techniques permit to recover a recent result of N. Randrianantoanina concerning a Subsequence Splitting Lemma for the general non-commutative L_p spaces. Various notions of p-equiintegrability are studied (one of which is equivalent to Randrianantoanina's one) and some results obtained by Haagerup, Rosenthal and Sukochev for L_p -spaces based on finite von Neumann algebras concerning subspaces of L_p(A) containing \ell_p are extended to the general case.

This mission is the statement-level formalization of On subspaces of non-commutative L_p-spaces (arXiv:math/0307169v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Block-diagonal Schatten embedding and contractive pinching (Unnumbered block-diagonal Schatten embedding, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

50 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 0.1 (seed: Schatten block-sum embedding): Haagerup Lp quasi-norm, countable Schatten p-sum Kp and actual ambient complemented embeddings (hard)
• Theorem 0.2: Actual arbitrary-algebra Haagerup Lp and its Hilbert/complemented subspaces (hard)
• Fact 1.2: Nelson measurable operators, unbounded positive powers, strong product and actual support projections (hard)
• Fact 1.3: Haagerup quasi-norm and left/right support disjointness (hard)
• Fact 1.4: Canonical Haagerup corner identifications across the graded Lp scale (hard)
• Proposition 2.1: Canonical normal predual ultrapower, Groh/Raynaud algebra A and canonical algebra-ultrapower inclusion (hard)
• Corollary 2.2: Positive order and compression in the actual Groh/Raynaud algebra and inclusion of a_U (hard)
• Theorem 2.3: Groh/Raynaud projection lattice and canonical inclusion of projection families (hard)
• Corollary 2.4: Banach/p-Banach ultrapower quotient with canonical Raynaud Lp(A) identification and support operations (hard)
• Lemma 2.5: Canonical ultrapower supports and diagonal Haagerup embedding (hard)
• Lemma 2.6: Separable Haagerup ultrapower subsets and strong two-sided projection actions (hard)
• Theorem 2.7: Actual Haagerup ultrapower and almost-disjoint approximation topology (hard)
• Remarks 2.8 (i)–(ii): One-sided Haagerup supports, almost-disjoint approximations and canonical ultrapower (hard)
• Proposition 2.9: Unresolved source qualification or domain convention (source-ambiguity)
• Lemma 2.10: Ordinary sequence-defined disjoint type on the actual Haagerup space (hard)
• Proposition 2.11: Unresolved source qualification or domain convention (source-ambiguity)
• Unnumbered remark after Proposition 2.11 (p=2): Unresolved source qualification or domain convention (source-ambiguity)
• Theorem 3.1: Haagerup subspaces, countable quasi-Banach p-sums and almost-disjoint subspace compression (hard)
• Lemma 3.3: Varying-subspace p-Banach ultraproduct and canonical Lp(A) supports (hard)
• Remark 4.2: Actual Haagerup bounded-algebra actions and ultraweak topology (hard)
• Lemma 4.3: Canonical normal predual, sigma-finite projection supports and ultraweak topology (hard)
• Proposition 4.4: Haagerup compression equiintegrability for arbitrary ultraweakly null nets (hard)
• Remark 4.5: Positive bounded ultraweakly null algebra nets acting on Haagerup Lp (hard)
• Theorem 4.6: Computed diagonal support s_e in the canonical Raynaud algebra and actual equiintegrable quotient representatives (hard)
• Unnumbered properties of the diagonal support: Actual complete projection lattice and canonical diagonal Haagerup supports across p (hard)
• Lemma 4.7: Actual Haagerup left/right actions, support projections and quasi-norm closures (hard)
• Unnumbered remark after Theorem 4.6 proof: Canonical quotient, computed s_e and Haagerup equiintegrability (hard)
• Corollary 4.8: Haagerup subsequence compression and genuine net-based equiintegrability (hard)
• Corollary 4.9: Canonical ultraweak projection limits and Haagerup uniform compression conditions (hard)
• Unnumbered one-sided equiintegrability observations: One-sided Haagerup equiintegrability, star and measurable absolute-value images (hard)
• Proposition 4.11: Canonical Raynaud corner actions and existential one-sided equiintegrable representatives (hard)
• Corollary 4.12: Four Haagerup corners, one-sided equiintegrability and disjoint supports (hard)
• Unnumbered one-sided extension of Corollary 4.9: One-sided net equiintegrability and canonical normal state controls (hard)
• Unnumbered finite-algebra equiintegrability coincidence: Finite von Neumann algebra predicate with Haagerup one-sided actions and diagonal-support centrality (hard)
• Proposition 4.13: Actual Haagerup bounded-algebra orbits and net-based equiintegrability (hard)
• Theorem 4.14: Canonical normal predual and its L1 Haagerup equiintegrability identification (hard)
• Theorem 4.15: Canonical normal predual and super-reflexivity of its actual Banach subspaces (hard)
• Unnumbered control functional for ultrapowers: Predual Banach ultrapower, Raynaud algebra and computed diagonal control functional (hard)
• Theorem 5.1: Actual Haagerup graded multiplier, countable ell_p subspaces and equiintegrability (hard)
• Lemma 5.2: Haagerup equiintegrable range and finite Rademacher averages in its quasi-norm (hard)
• Proposition 5.3: Haagerup bounded sequences, equiintegrability and actual ell_p basis equivalence (hard)
• Proposition 5.4: Unresolved source qualification or domain convention (source-ambiguity)
• Unnumbered Banach-Saks results: Actual Haagerup Lp with weak topology, equiintegrability and HRS sequence-rate predicates (hard)
• Lemma 6.1: Arbitrary operator spaces and the actual vector-valued S_p^n[E] interpolation norm at every n (hard)
• Theorem 6.2: Unresolved source qualification or domain convention (source-ambiguity)
• Corollary 6.3: Haagerup interpolation operator-space hierarchy and complete complemented ell_p copies (hard)
• Theorem 6.4: Natural operator-space p-direct sums and Haagerup matrix amplification norms (hard)
• Corollary 6.5: Countable operator-space Schatten p-sum Kp and complete ambient embeddings (hard)
• Theorem A1: Actual Haagerup quasi-norm and both unbounded support projections (hard)
• Proposition A2: Positive Haagerup measurable powers and L1 trace Tr (hard)

Selected references

• On subspaces of non-commutative L_p-spaces, arXiv:math/0307169v1, https://arxiv.org/abs/math/0307169v1

Motivation

An action of an affine algebraic group $G$ on an affine variety $X$ is observable when invariant regular functions see every nonzero $G$-stable ideal of the coordinate ring: if $I\subseteq k[X]$ is a nonzero $G$-stable ideal, then $I^G\neq(0)$. The notion goes back to Grosshans' theory of observable subgroups (F. D. Grosshans, Observable groups and Hilbert's fourteenth problem, Amer. J. Math. 95, 1973): a closed subgroup $H\le G$ is observable exactly when the action of $H$ on $G$ by left translations is observable (p. 2 of the paper), and observable subgroups are the ones for which $G/H$ is quasi-affine.

L. Renner and A. Rittatore (arXiv:0902.0137) characterise observability geometrically. Their Theorem 3.10 states that an action on an irreducible affine variety is observable if and only if (1) every invariant rational function is a quotient of invariant regular functions, and (2) the set of closed orbits of maximal dimension contains a nonempty open set. Section 4 of the paper specialises this to reductive groups, where the answer becomes a single condition on closed orbits, and identifies a canonical closed subvariety, the socle, on which the action is observable. This mission formalizes that section.

Timeline:

• 1970, V. L. Popov: for a reductive group acting on an affine variety, if some closed orbit has maximal dimension then the closed orbits of maximal dimension form an open set (cited by the paper as Proposition 4.4, from Popov's stability criterion paper, Theorem 4).
• 1973, F. D. Grosshans: observable subgroups and Hilbert's fourteenth problem.
• 2009, Renner–Rittatore: Theorem 3.10 for arbitrary affine groups; Theorems 4.6 and 4.7 for reductive groups.

Setting

Let $k$ be an algebraically closed field. An affine algebraic group $G$ is given by its coordinate ring $k[G]$, a reduced, finitely generated, smooth $k$-algebra whose $k$-points $G(k)$ form a group with regular multiplication and inversion. An affine variety $X$ is given by its coordinate ring $k[X]$, a reduced finitely generated $k$-algebra; its points are the $k$-algebra maps $k[X]\to k$. A regular action is a group homomorphism $\rho:G(k)\to\operatorname{Aut}_k(k[X])$ whose evaluation is a regular function of $(g,x)$; points move by $g\cdot x=x\circ\rho(g^{-1})$.

• The orbit of $x$ is $\mathcal O(x)=G\cdot x$; its dimension is the Krull dimension of the coordinate ring of its closure.
• $X_{\max}$ is the set of points whose orbit has maximal dimension, and $\Omega(X)\subseteq X_{\max}$ is the subset of points whose orbit is also closed.
• The categorical quotient $\pi:X\to X/\!\!/G$ sends a point to its restriction to the invariant algebra $k[X]^G$.
• The socle is the Zariski closure of the union of the closed orbits:

$$X_{\mathrm{soc}}=\overline{\bigcup_{\overline{\mathcal O(x)}=\mathcal O(x)}\mathcal O(x)}.$$

• For a closed $G$-stable subset $Z$ with ideal $\mathcal I(Z)$, the restricted action is the action on $k[Z]=k[X]/\mathcal I(Z)$ induced through the quotient map.
• A point $g\in G(k)$ is unipotent when right translation by $g$ on $k[G]$ is locally unipotent. $G$ is reductive when every closed, connected, normal subgroup of $G$ consisting of unipotent elements is trivial.

Formalization targets

Goal: Theorem 4.7

For $G$ reductive acting on an irreducible affine variety $X$:

$$\text{the action is observable}\iff\Omega(X)\neq\emptyset,$$

and $X_{\mathrm{soc}}$ is the maximum $G$-stable closed subset $Z\subseteq X$ such that the restricted action $G\times Z\to Z$ is observable.

Milestones

1. Theorem 3.10 (referenced, already posed on the platform): observable $\iff$ $[k[X]^G]=[k[X]]^G$ and $\Omega(X)$ contains a nonempty open subset.
2. Lemma 4.3: $\Omega(X)=\pi^{-1}\bigl((X/\!\!/G)\setminus\pi(X\setminus X_{\max})\bigr)$; in particular $\Omega(X)$ is a $G$-stable open subset.
3. Proposition 4.4 (Popov): if $\Omega(X)\neq\emptyset$ then $\Omega(X)$ is open.
4. Lemma 4.5: $\pi|_{X\setminus X_{\max}}$ is dominant $\iff$ it is surjective $\iff$ $X_{\max}$ contains no closed orbit $\iff$ $\Omega(X)=\emptyset$.
5. Theorem 4.6, "Moreover" sentence: if $Z$ is $G$-stable, closed and $\pi|_Z$ is dominant, then $X_{\mathrm{soc}}\subseteq Z$, $X_{\mathrm{soc}}$ is irreducible, and $\Omega(X_{\mathrm{soc}})\neq\emptyset$.
6. Theorem 4.7, first sentence: observable $\iff\Omega(X)\neq\emptyset$.
7. Lemma 3.1 (referenced, already posed on the platform): for connected $G$, the action is observable if and only if the restricted action on each irreducible component is.

Significance

The result. For reductive groups observability is decided by one closed orbit of maximal dimension, with no condition on invariant rational functions. This simplification fails for general groups: a Borel subgroup acting on a semisimple group by left translation has every orbit closed of maximal dimension, yet the action is not observable (Example 3.11 of the paper). The second sentence gives every reductive action a canonical observable piece, the socle, computed from the closed orbits alone, and Proposition 4.8 of the paper then identifies its ideal as the largest $G$-stable ideal without nonzero invariants.

Formalizing it. The results are proved in the paper (Proposition 4.4 is Popov's theorem, cited there). None of them is machine-checked. Theorem 3.10 and Lemma 3.1 are open goals of an existing public mission on the same paper, which covers §§2–3 and defers §4; this mission states §4 on the same definitions, so a proof of either referenced statement serves both. A complete development needs the basic geometric invariant theory of reductive groups: finite generation of invariants, separation of closed $G$-stable sets by invariants, the existence of a unique closed orbit in each orbit closure, and semicontinuity of orbit dimension. None of this is in Mathlib.

Difficulty

The direction "observable $\Rightarrow\Omega(X)\neq\emptyset$" follows from Theorem 3.10. The converse is where reductivity enters: given a nonzero $G$-stable ideal, one must produce a nonzero invariant in it, and the natural route is to separate the closed orbits in $\Omega(X)$ from the zero set of the ideal by invariant functions. That separation is a theorem about reductive groups (closed disjoint $G$-stable sets are separated by invariants), not available for arbitrary groups, and it must be combined with the openness of $\Omega(X)$. For the maximality of the socle, the paper reduces to irreducible components through Lemma 3.1, which assumes $G$ connected; Theorem 4.7 makes no such assumption, so a disconnected $G$ needs a reduction to the stabiliser of a component.

Formalization scope

All statements are built on the public definitions module QAlgorithms_Papers_Independent_Support21_P10 for this paper: points are $k$-algebra maps, $G$ is a coordinate ring H with a group structure on its points (IsAffineAlgebraicGroup), $X$ is a coordinate ring A (IsAffineVariety, finite type and reduced), the action is rho : Point k H →* (A ≃ₐ[k] A) with IsRegularAction. Closure is the Zariski closure $V(\mathcal I(S))$ on $k$-points (classicalClosure), and $X/\!\!/G$ is the set of $k$-points of $k[X]^G$ with $\pi$ the restriction map (quotientPoint). No finite generation of $k[X]^G$ is assumed.

Conventions committed to:

• Irreducibility. $X$ is irreducible (IsDomain A) in Theorems 4.6 and 4.7, the paper's standing assumption for §4 (p. 2). Without it the first sentence of 4.7 is false. Lemmas 4.3, 4.5 and Proposition 4.4 are stated for arbitrary affine $X$, as printed.
• No connectedness of $G$. Theorem 4.7 is stated as printed, for possibly disconnected $G$.
• Reductive is a hypothesis IsReductiveGroup k H: every Zariski-closed normal subgroup of $G(k)$ with prime vanishing ideal and consisting of unipotent points is trivial. Unipotence is local unipotence of right translation on $k[G]$.
• Socle: classicalClosure {x | IsClosedOrbit rho x}.
• Restricted actions: an action rhoZ on A ⧸ coordinateVanishingIdeal Z compatible with the quotient map (IsRestrictionOf). For the socle its existence is part of the conclusion; for a competitor $Z$, compatibility is a hypothesis. No statement quantifies over an uncoupled action.
• $\Omega(X)\neq\emptyset$ is (omegaLocus rho).Nonempty. This is strictly weaker than Theorem 3.10's condition that $\Omega(X)$ contain a nonempty open set.

A trivializing reading is excluded: the socle is computed from the closed orbits and is never defined as "the largest closed set with observable restricted action", which would make the maximality claim a tautology.

Welcome contributions: proofs of the milestones, and reusable infrastructure for reductive group actions (finite generation of invariants, separation of closed invariant sets, orbit-closure structure).

Selected references

• L. Renner, A. Rittatore, Observable actions of algebraic groups, preprint, arXiv:0902.0137v2 [math.AG], 2009. https://arxiv.org/abs/0902.0137v2
• V. L. Popov, Stability criterion for the action of a semisimple group on a factorial manifold, Math. USSR Izv. 4 (3) (1970), 527–535 (reference [14] of the paper).
• F. D. Grosshans, Observable groups and Hilbert's fourteenth problem, Amer. J. Math. 95 (1973), 229–253 (reference [12] of the paper).
• W. Ferrer Santos, A. Rittatore, Actions and Invariants of Algebraic Groups, Pure and Applied Math. 268, Dekker/CRC Press, 2005 (reference [10] of the paper; Theorem 13.3.13 is Proposition 4.4).
• V. L. Popov, E. B. Vinberg, Invariant theory, in Algebraic Geometry IV, Encyclopaedia of Mathematical Sciences 55, Springer, 1994 (reference [15] of the paper).

Motivation

Quantum Max Cut asks for the highest energy of a two-qubit interaction Hamiltonian placed on the edges of a weighted graph. It is a quantum analogue of Max Cut: a classical cut assigns one of two labels to each vertex, while a quantum state can use correlations and entanglement across the qubits. Lee studies an approximation algorithm that first solves a semidefinite program and then uses its vectors to choose both a bit string and the angles of a quantum circuit. The result applies to arbitrary nonnegatively weighted simple graphs, without a degree or regularity restriction. The guarantee is an approximation ratio of $0.562$ for the energy of the algorithm's random output in expectation Lee, 2022, pp. 9–13.

The paper places this algorithm alongside earlier approaches that round a level-one or level-two quantum Lasserre program. Its distinguishing object is a circuit with one parameter per graph edge, computed from the SDP vectors rather than optimized over circuit angles after rounding. The parameter rule makes a global approximation guarantee possible even when neighboring edge gates interfere Lee, 2022, pp. 3–5, 9.

Setting

Let $G=(V,E,w)$ be a finite simple graph with nonnegative weights $w_{ij}$. Associate one qubit with each vertex. On qubit $i$, let $X_i,Y_i,Z_i$ be the standard Pauli operators, and let $I$ be the identity. Each edge contributes

$$H_{ij}=\frac14(I-X_iX_j-Y_iY_j-Z_iZ_j),\qquad H=\sum_{(i,j)\in E}w_{ij}H_{ij}.$$

For a unit state $|\psi\rangle$, its energy is $\langle\psi|H|\psi\rangle$. The Quantum Max Cut optimum is the largest eigenvalue of $H$, equivalently the largest energy over all unit states Lee, 2022, Definition 2, p. 2.

The paper's canonical Lasserre program at level $k$ uses a real positive semidefinite matrix $M$ indexed by Pauli strings of weight at most $k$. Its constraints make matrix entries consistent with products of Pauli strings. At level two, its objective has one term for each of $X_iX_j$, $Y_iY_j$, and $Z_iZ_j$ on every edge. Lemma 1 places all quantum-state energies below feasible Lasserre objectives. The paper then introduces a vector semidefinite program (S). It uses a unit vector $v_0$, vectors $v_{i,a}$ for vertices and $a\in\{1,2,3\}$, and vectors $v_{ij,a}$ for pairs of distinct vertices. Relations (1)–(8) fix their norms and inner products. Writing $v_{ij}=\sum_a v_{ij,a}$, its objective is

$$S(G;v)=\sum_{(i,j)\in E}\frac{w_{ij}}4(v_0-v_{ij})\cdot v_0.$$

Lemma 2 shows that (S) relaxes the level-two Lasserre program Lee, 2022, Definitions 3–5 and Lemmas 1–2, pp. 3–6.

Algorithm 1 takes an optimal feasible solution of (S). It picks $a\in\{1,2,3\}$ uniformly, chooses a random direction $r$, and sets bit $z_i$ by the sign of $v_{i,a}\cdot r$. For each edge it computes the normalized correlation

$$\gamma_{ij}=-\frac{(v_0+v_{ij})\cdot v_0}{\|v_0+v_{ij}\|\|v_0\|},\qquad \theta_{ij}=\frac12\arccos\bigl(\exp[-0.041\max(\gamma_{ij},0)]\bigr).$$

It starts in the computational basis state $|z\rangle$ and applies the commuting edge gates $\exp(i\theta_{ij}P(i)P(j))$, with $P(i)=X_i$ when $z_i=1$ and $P(i)=Y_i$ when $z_i=0$. The result is a random state $|\phi(\theta)\rangle$ Lee, 2022, Algorithm 1, p. 9.

Formalization targets

The goal is the expectation form of Theorem 1. For every nonnegatively weighted graph, every globally optimal feasible SDP solution $v$, and every unit quantum state $|\psi\rangle$,

$$\mathbb E\,\langle\phi(\theta)|H|\phi(\theta)\rangle \ge 0.562\,\langle\psi|H|\psi\rangle.$$

The goal also states that the random energy is integrable. Because the inequality holds for every unit $|\psi\rangle$, it is exactly the comparison with $0.562$ times the maximum eigenvalue. The printed theorem omits the expectation sign, while its proof explicitly averages the rounded output Lee, 2022, Theorem 1 and proof, pp. 10–11.

The milestones are the source's relaxation lemmas, the feasible-vector identities, the star monogamy bound, the hyperplane cut-probability bound, the circuit's edge-energy bound, equations (19) and (21)–(24), the final scalar minimum, and the per-solution expected-energy bound. Their order moves from the Hamiltonian and SDP model to the output of Algorithm 1. The coefficient $0.562$ and the parameter $0.041$ are the paper's values, not tunable placeholders.

Significance

Together, the two relaxation lemmas connect the quantum optimum to the objective optimized by (S). The rounding results then connect a feasible SDP value to a physically represented output state. The theorem certifies a constant approximation ratio for arbitrary weighted graphs in the model of the paper. The star monogamy inequality and edge-energy lemma also isolate claims useful for analyzing related rounding circuits Lee, 2022, Lemmas 1–6, pp. 4–10.

This result is proved in the cited paper. The mission asks for machine-checked proofs of its statements and for the model that makes those statements precise. Its definitions of Pauli strings, the quantum Hamiltonian, canonical Lasserre feasibility, the vector SDP, and the rounded circuit can support later comparisons of SDP-based quantum approximation algorithms. The draft statements compile, but a compiling sorry is not a proof; the theorem and milestones remain open formalization targets.

Difficulty

Bounding the probability that a rounded bit string cuts an edge is only one part of the argument. Its circuit gate acts on the same qubits as gates at neighboring edges. Consequently, a good cut probability alone does not determine the energy on that edge. The monogamy bound limits how much SDP value can be concentrated around a vertex, while the edge-energy statement accounts for the neighboring gate parameters. A formal proof must also connect matrix feasibility, vector feasibility, Gaussian rounding, and complex matrix expectations without losing the edge weights or the factor $1/4$ Lee, 2022, pp. 7–13.

Formalization scope

Vertices are Fin n, computational basis labels are bit strings Fin n → Fin 2, and Pauli strings are maps Fin n → Fin 4. The graph is simple; each edge occurs once, with its smaller endpoint first. Only that orientation's weight is read. The vector SDP uses Fin N → ℝ, and its feasibility predicate states relations (1)–(8) with distinct-index conditions. The ordered-pair implementation of $v_{ij,a}$ includes symmetry, making the paper's undirected edge indexing explicit. Optimality in the goal compares feasible solutions across every finite dimension, so a solution optimal only in a small dimension cannot satisfy the intended premise.

The random direction is a standard Gaussian vector. Its signs have the same distribution as the signs from a direction uniform on the sphere; a zero projection gives bit zero. The circuit uses the cosine-sine form of each Pauli-product exponential and a lexicographic edge order. Its gates commute, so the chosen order represents the paper's product. The expectation averages the three choices of $a$ and integrates over the Gaussian vector. The goal includes integrability, and its universal unit-state comparison avoids a supremum with a default value on a bad domain.

Three source boundaries are stated explicitly. The Lasserre objective requires $k\ge2$ because it indexes two-qubit Pauli strings. Lemma 6 requires $0\le\theta_{ij}\le\pi/4$ on edges; the printed nonnegative-angle condition is too broad, while Algorithm 1 always gives angles in that interval. Definition 4's repeated $Z_iZ_j$ objective term is read as $Y_iY_j$, as required by the Hamiltonian and its appendix calculation. The Goemans–Williamson quotient uses $[-1,1)$ since the printed closed endpoint $t=1$ gives $0/0$. A single arbitrary feasible SDP solution cannot replace the globally optimal one in the final comparison with the quantum optimum, and a deterministic bound for every random outcome is not asserted.

Contributions that establish the two relaxation maps, the vector identities, the Gaussian cut bound, the circuit's local energy bound, and the final expected-energy comparison all belong to this mission. Proofs of the paper's polynomial running-time claim and cited hardness results are outside the formal statements here.

Selected references

• Eunou Lee, Optimizing quantum circuit parameters via SDP, arXiv preprint, 2022, arXiv:2209.00789v1.

Motivation

Many manufacturing processes deliver only a random fraction of what they start: semiconductor wafers, biologics, agricultural produce and recycled materials all suffer random yield. A firm facing yield risk has two classical levers. It can inflate production to hedge against low yield, and it can postpone pricing until the yield is observed, so that the price clears whatever was actually produced. The operations literature has long studied both levers for a risk-neutral firm, starting from the price-setting newsvendor (Petruzzi and Dada, 1999).

Real firms, and especially small producers exposed to a single bad harvest or batch, care about low-profit outcomes more than about the mean. Kouvelis, Xiao and Yang (Management Science, 2021) model this with the conditional value-at-risk (CVaR) of profit, the criterion introduced by Rockafellar and Uryasev (2000) and used for newsvendor problems by Chen, Xu and Zhang (2009). Their first finding is that a sufficiently risk-averse firm does not produce at all, and that the risk level at which production stops is the same whether or not the firm can postpone its price. This mission formalizes that finding.

Setting

A monopoly firm sells one product to a market with deterministic demand $d(p)$, continuous and strictly decreasing in the price $p\in[0,p_0]$, where $p_0>0$ is the maximal allowable price, $d(p_0)=0$. The inverse demand $p(x)$ satisfies $p(d(p))=p$ and $d(p(x))=x$ for $x\in[0,d(0)]$. Assumption 2 of the paper requires the revenue $x\mapsto p(x)\,x$ to be concave on $[0,d(0)]$.

Producing $q$ units of input costs $cq$ and yields $q\xi$ sellable units. The yield factor $\xi$ is a continuous random variable with law $\nu$, support $[l,u]$ with $0\le l<u\le1$, c.d.f. $G$ and mean $\mu$. The cost satisfies $0\le c\le p_0\mu$, so that production is not hopeless. Write $G^{-1}(\eta)=\inf\{x:G(x)\ge\eta\}$ for the lower quantile and

$$g(\eta)=\frac1\eta\int_l^{G^{-1}(\eta)}\xi\,dG(\xi),\qquad \eta\in(0,1],$$

for the mean of the lowest $\eta$-fraction of yields.

For a random profit $\pi$ and a risk level $\eta\in(0,1]$,

$$\mathrm{CVaR}_\eta(\pi)=\max_{v\in\mathbb R}\Big\{v+\frac1\eta\,\mathbb E\min\{\pi-v,0\}\Big\},$$

the average profit over the worst $\eta$-fraction of outcomes; $\eta=1$ is risk neutrality and smaller $\eta$ means more risk aversion.

Under ex ante pricing the firm picks $p_a\in[0,p_0]$ and $q_a\ge0$ before the yield realizes and maximizes $\Pi_a(p_a,q_a)=\mathrm{CVaR}_\eta\big(p_a\min\{d(p_a),q_a\xi\}-cq_a\big)$. Under responsive pricing it picks $q_r\ge0$, observes $\xi$, then picks the revenue-maximizing price, and maximizes

$$\Pi_r(q_r)=\mathrm{CVaR}_\eta\Big(\max_{p_r\in[0,p_0]}p_r\min\{d(p_r),q_r\xi\}-cq_r\Big).$$

Since $q=0$ gives CVaR $0$, the firm produces under a scheme when some decision has strictly positive CVaR, and otherwise not producing is optimal.

Formalization targets

Goal: one threshold for both schemes (Proposition 4(i))

There is a single $\eta^*\in[0,1]$, either $\eta^*=0$ or a solution of $p_0\,g(\eta^*)=c$, such that for every $\eta\in(0,1]$

$$\text{ex ante firm produces}\iff\eta>\eta^*\iff\text{responsive firm produces}.$$

This is the paper's $\eta_a^*(p_0,c)=\eta_r^*(p_0,c)$, with the boundary case $\eta=\eta^*$ stated correctly (there the optimal CVaR is $0$, so the firm is indifferent and "produces" in the strict sense fails).

Milestones

1. Property 1: for a continuously distributed profit, the maximization formula equals the tail mean $\mathbb E[\pi\mid\pi\le\mathrm{VaR}_\eta(\pi)]$, attained at $v=\mathrm{VaR}_\eta(\pi)$.
2. Property 2: the CVaR of a profit concave in the decision is concave in the decision.
3. Proposition 1: at a fixed price $p_a$, the optimal ex ante quantity is $d(p_a)/\delta$ above a threshold price $\tilde p$ and $0$ below it.
4. The tail mean $g$: strictly increasing and continuous on $(0,1]$, with $g(1)=\mu$ and $g(0^+)=l$.
5. Proposition 2: the ex ante threshold $\eta_a^*$.
6. Lemma 1: the responsive firm's second-stage price is $p(\min\{q_r\xi,d^*\})$, where $d^*$ maximizes revenue.
7. Proposition 3: $\Pi_r$ is concave and the responsive threshold $\eta_r^*$ exists.

Significance

The result says that price postponement, although it raises the profit of a firm that does produce, does not enlarge the set of risk-averse firms willing to produce. The threshold is explicit: $\eta^*=0$ when $p_0l>c$, and otherwise $\eta^*$ solves $g(\eta)=c/p_0$. Because $g$ depends only on the yield law, the threshold separates cost and price power ($c/p_0$) from yield risk ($g$), which is what the paper's comparative statics in $c$, $p_0$ and the yield distribution (Proposition 4(ii)–(iv)) build on.

The mission states the paper's threshold results and its two CVaR properties in Lean. None of them is machine-checked anywhere. Proofs of the milestones would also provide a reusable CVaR toolkit on a general probability space: the identification of the maximization formula with the lower-tail mean, and concavity of CVaR in a decision parameter.

Difficulty

The paper's argument uses densities and derivatives throughout: $g'(\eta)>0$, a first-order condition at $q=0$, L'Hospital's rule for $g(0^+)$. The model here assumes only an atomless law with full support, so every such step has to be replaced by a measure-theoretic one. CVaR is a supremum of integrals over an unbounded index, so comparisons between the two schemes cannot be read off a closed form. The responsive profit is itself a maximum over prices inside an expectation inside a supremum. Finally, the two schemes have different optimal decisions everywhere except in the limit of vanishing production, so an argument that compares optimal values fails: the content is in comparing whether positive CVaR is attainable at all.

Formalization scope

• The yield is its law ν : Measure ℝ: a probability measure without atoms (NullSingletonClass), with ν [l,u]ᶜ = 0 and positive mass on every open subinterval of [l,u]. The paper's density is not assumed. Expectations are Bochner integrals against ν.
• $p_0$ is a finite positive real (the paper also allows $p_0=\infty$). Demand d and inverse demand P are two functions with both inverse identities on their intervals.
• CVaR (RiskPostpone.Threshold.cvar) is the real supremum over $v\in\mathbb R$ of the bracket. The model's profits are bounded on the support, so the supremum is genuine there; the general CVaR properties assume integrability. VaR and the yield quantile use the published MultistageStochastic.valueAtRisk.
• The responsive maximum is the sSup of the image of $[0,p_0]$, which is nonempty and bounded.
• "Produces" is strict: some decision has CVaR $>0$. With $\ge$ the statement would be trivially true at $q=0$; with a CVaR supremum that could be junk $0$, or with two separate thresholds for the two schemes, the goal would lose its content. All three formalizations are ruled out.
• Assumption 1 of the paper (an IGFR-type condition and increasing price elasticity) is used only for the uniqueness of the optimal ex ante price and is not assumed. Assumption 2 is stated without "twice differentiable". In Lemma 1, $d^*$ is any maximizer of revenue on $[0,d(0)]$ rather than the root of the first-order condition. Proposition 1 excludes the degenerate case $c=0=l$ (there the optimal quantity does not exist). Property 1 assumes the profit is integrable, essentially bounded above and atomless.
• Not formalized: the first-order conditions of Propositions 2(ii) and 3(ii), Proposition 4(ii)–(iv), Corollaries 1–4, the linear-demand comparisons of §5.2–§5.4, and the extensions of §7.

Contributions welcome: proofs of the milestones, especially the general CVaR facts (Properties 1 and 2) and the measure-theoretic properties of $g$, which are reusable beyond this model.

Selected references

• P. Kouvelis, G. Xiao, N. Yang, Role of Risk Aversion in Price Postponement under Supply Random Yield, Management Science 67(8), 4826–4844, 2021. https://doi.org/10.1287/mnsc.2020.3755 (formalized from the accepted manuscript MS-OPM-18-01273.R2)
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3), 21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• R. T. Rockafellar, S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7), 1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
• Y. Chen, M. Xu, Z. G. Zhang, A risk-averse newsvendor model under the CVaR criterion, Operations Research 57(4), 1040–1044, 2009. https://doi.org/10.1287/opre.1080.0603
• N. C. Petruzzi, M. Dada, Pricing and the newsvendor problem: a review with extensions, Operations Research 47(2), 183–194, 1999. https://doi.org/10.1287/opre.47.2.183

Motivation

The generalized Stieltjes transform of order $\alpha>0$ of a non-negative measure $\mu$ on $[0,\infty)$ is the function $z\mapsto\int_{[0,\infty)}\mu(du)/(u+z)^\alpha$. For $\alpha=1$ this is the classical Stieltjes transform, whose functions (Stieltjes functions) appear in moment problems, in the theory of completely monotone and Bernstein functions, in the spectral theory of positive operators, and in the functional calculus of sectorial operators. The classes of order $\alpha\ne1$ were studied by Widder, Hirschman and Widder, Sokal, and Schwarz, among others, and appear in work on functional calculi of sectorial operators (Batty, Gomilko and Tomilov, arXiv:1309.0318).

D. Karp and E. Prilepkina, Generalized Stieltjes transforms: basic aspects (arXiv:1111.4271), collect and prove the basic real- and complex-variable properties of these classes. One elementary but structural fact is that the classes are nested: a function of order $\alpha$ is also of every larger order $\beta$. This raises a natural question that the paper answers: given $f$ in the class of order $\beta$, is $\beta$ the smallest order available, or can it be lowered? The paper introduces the exact Stieltjes order and gives a criterion of exactness phrased purely in terms of the representing measure of $f$. This mission formalizes that criterion (Theorem 16) together with the results its proof relies on.

Setting

For $\alpha>0$, write $\mathcal M_\alpha$ for the set of non-negative Borel measures $\mu$ on $[0,\infty)$ with

$$\int_{[0,\infty)}\frac{\mu(dt)}{(1+t)^\alpha}<\infty. \tag{2}$$

The generalized Stieltjes class $S_\alpha$ consists of the functions $f:(0,\infty)\to\mathbb R$ of the form

$$f(z)=\mu_\infty+\int_{[0,\infty)}\frac{\mu_\alpha(du)}{(u+z)^\alpha},\qquad z>0,$$

with a constant $\mu_\infty\ge0$ and $\mu_\alpha\in\mathcal M_\alpha$. The paper writes the atom of $\mu_\alpha$ at $0$ separately as a term $\mu_0/z^\alpha$ (its formula (1)); here it is part of $\mu_\alpha$. The pair $(\mu_\infty,\mu_\alpha)$ is a representation of $f$ in $S_\alpha$, and $\mu_\alpha$ is its representing measure. Write $S_\infty=\bigcup_{\alpha>0}S_\alpha$.

For a measure $\mu$ on $[0,\infty)$, its left-continuous distribution function is $F_\mu(y)=\mu([0,y))$, so $F_\mu(0)=0$. For $\eta>0$, the left-sided Riemann–Liouville fractional integral $I^+_\eta\mu$ (Definition A1) is the measure on $[0,\infty)$ with Lebesgue density

$$y\longmapsto\frac{1}{\Gamma(\eta)}\int_{[0,y)}\frac{\mu(du)}{(y-u)^{1-\eta}}\qquad(y>0).$$

The exact Stieltjes order of $f\in S_\infty$ is

$$\alpha^*[f]=\inf\{\alpha>0:\ f\in S_\alpha\}. \tag{24}$$

Finally, for $f\in S_\beta$ with representing measure $\mu_\beta$ and a parameter $\varepsilon$, set

$$\Phi(y)=\int_{[0,y)}\frac{\mu_\beta(du)}{(y-u)^{\varepsilon}},\qquad y\ge0. \tag{25}$$

Formalization targets

Goal: Theorem 16 (criterion of exactness)

For $\beta>0$ and $f\in S_\beta$ with representing measure $\mu_\beta$,

$$\beta>\alpha^*[f]\iff \Phi\ \text{is non-decreasing on }(0,\infty)\ \text{for some}\ \varepsilon\in(0,\min\{\beta,1\}).$$

The order $\beta$ is exact precisely when no admissible $\varepsilon$ makes $\Phi$ monotone.

Milestones

1. Formula (12). For $0<\alpha<\beta$, $z>0$, $u\ge0$:

$$\frac{1}{(u+z)^\alpha}=\frac{\Gamma(\beta)}{\Gamma(\alpha)\Gamma(\beta-\alpha)}\int_{(0,\infty)}\frac{t^{\beta-\alpha-1}\,dt}{(z+u+t)^\beta}.$$

2. Theorem 3, first part. For $0<\alpha<\beta$, $S_\alpha\subset S_\beta$; explicitly, $f\in S_\alpha$ is represented in $S_\beta$ with the same $\mu_\infty$ and

$$\mu_\beta(dy)=\frac{\Gamma(\beta)\,dy}{\Gamma(\alpha)\Gamma(\beta-\alpha)}\int_{[0,y)}\frac{\mu_\alpha(du)}{(y-u)^{\alpha+1-\beta}}. \tag{10}$$

3. Theorem A1, first part. $I^+_\eta$ maps $\mathcal M_\alpha$ into $\mathcal M_{\alpha+\eta}$.
4. Theorem A1, inversion (29), case $0<\eta<1$. $F_\mu(y)=\frac{1}{\Gamma(1-\eta)}\int_{[0,y)}\frac{(I^+_\eta\mu)(du)}{(y-u)^{\eta}}$ for all $y\ge0$.
5. Theorem 3, inversion (11), case $0<\beta-\alpha<1$. If $f\in S_\alpha$ has representing measure $\mu_\alpha$ and any representation $(\mu'_\infty,\mu_\beta)$ in $S_\beta$, then $\mu'_\infty=\mu_\infty$ and

$$F_{\mu_\alpha}(y)=\frac{\Gamma(\alpha)}{\Gamma(\beta)\Gamma(\alpha-\beta+1)}\int_{[0,y)}\frac{\mu_\beta(du)}{(y-u)^{\beta-\alpha}}.$$

6. Claim (26). If $\Phi=F_\nu$ and $\int_{[0,\infty)}\Phi(y)\,dy/(1+y)^{\alpha+1}<\infty$, then $\int_{[0,\infty)}d\Phi(y)/(1+y)^\alpha<\infty$ and $\Phi(t)(1+t)^{-\alpha}\to0$.

Significance

The result. Theorem 16 reduces the question "is the order of $f$ optimal?" to a monotonicity test on a single function built from the representing measure. The paper derives two practical corollaries from it: if $\Phi(2y)/\Phi(y)$ has a limit below $1$, then $\beta$ is exact (Corollary 1), and if $\mu_\beta$ has compact support, then $\beta$ is exact (Corollary 2). Both are immediate once Theorem 16 is available and are natural follow-up targets. The milestones are of independent use: Theorem 3 is the nesting of the classes with an explicit formula for the new representing measure, and Theorem A1 is the integrability and inversion theory of fractional integrals of measures, which the paper's appendix develops because the authors found no reference treating measures rather than functions.

Formalizing it. The results are proved in the paper; none is formalized. The platform has the generalized Stieltjes class itself (a published definition from the Batty–Gomilko–Tomilov formalization) and the half-line Beta integral, but no fractional integrals of measures, no inversion formula, and nothing on the exact order. A complete development provides a reusable Riemann–Liouville calculus for measures on the half-line and the uniqueness of the representing measure in $S_\beta$, which milestone 5 contains.

Difficulty

The forward direction of Theorem 16 looks like a computation: pass from $\beta$ to a smaller order and read off the measure. The obstacle is that one must know that the representing measure in $S_\beta$ is unique, since $\Phi$ is built from the representing measure and the inversion formula (11) must apply to it; milestone 5 states the inversion for an arbitrary representing measure for this reason. The converse direction must produce a measure from a function: a non-decreasing $\Phi$ is a distribution function, and one must show the resulting measure satisfies (2) at the lower order, which is claim (26) and needs a careful tail estimate rather than a direct comparison. Throughout, interchanges of integration are carried out for measures with atoms (including an atom at $0$), where the naive differentiation formula of (11) and (29) for higher $n$ breaks down at jumps.

Formalization scope

Functions are real-valued on $(0,\infty)$ (PositiveReal), and the classes and representations are the published StieltjesClass and StieltjesRepresentation (QAlgorithms_Papers_Independent_Renew46_P11), reused unchanged. Representing measures are measures on ℝ≥0; the paper's atom at $+\infty$ is the constant $\mu_\infty$. All orders $\alpha,\beta,\eta$ are positive. All kernel integrals and the functions $F_\mu$ and $\Phi$ take values in $[0,\infty]$ (lower Lebesgue integrals), so a divergent integral is $+\infty$, not $0$; "non-decreasing" is monotonicity in $[0,\infty]$. The exact order is the real infimum of $\{\alpha>0: f\in S_\alpha\}$, which is nonempty and bounded below whenever $f\in S_\beta$. Densities are with respect to Lebesgue measure on $(0,\infty)$ pushed to ℝ≥0.

Corrected readings, each disclosed in the item: (25) is taken over $[0,y)$, while the paper prints $(0,y)$; with $(0,y)$ the theorem fails for $f(z)=z^{-\beta}$, whose representing measure is the unit mass at $0$. Formulas (11) and (29) are stated only for $n=0$, the case Theorem 16 uses; as printed for $n\ge1$ they differentiate a function at its jumps. Claim (26) is stated for the distribution function of an arbitrary measure, the generality its proof gives.

A trivializing formalization is ruled out: $\Phi$ must be built from the representing measure of the given $f$ (not from an arbitrary measure), over $[0,y)$ (over $(0,y)$ an atom at $0$ makes $\Phi$ identically $0$), and in $[0,\infty]$ (a real-valued Bochner $\Phi$ would be $0$ wherever the integral diverges).

Contributions welcome: proofs of any milestone, a reusable Riemann–Liouville integral of measures on ℝ≥0 with its Tonelli computations, uniqueness of generalized Stieltjes representations, and the corollaries of Theorem 16.

Selected references

• D. Karp, E. Prilepkina, Generalized Stieltjes transforms: basic aspects, arXiv:1111.4271v2, 2012. https://arxiv.org/abs/1111.4271
• C. Batty, A. Gomilko, Yu. Tomilov, Product formulas in functional calculi for sectorial operators, arXiv:1309.0318. https://arxiv.org/abs/1309.0318
• A. D. Sokal, Real-variables characterization of generalized Stieltjes functions, Expositiones Mathematicae 28 (2010), 179–185.
• J. H. Schwarz, The generalized Stieltjes transform and its inverse, J. Math. Phys. 46, 013501 (2005).
• D. V. Widder, The Stieltjes transform, Trans. Amer. Math. Soc. 43 (1938), 7–60.
• S. G. Samko, A. A. Kilbas, O. I. Marichev, Fractional Integrals and Derivatives: Theory and Applications, Gordon and Breach, 1993.

Motivation

In quantum field theory the vacuum is entangled between any two regions of space, and the amount of entanglement between nearby regions is infinite: the algebras of observables of regions that touch admit no normal separable state at all. For regions at a positive distance the question becomes quantitative. How much entanglement does the vacuum carry between a region and a second region at distance $\delta$, and how does it depend on $\delta$ and on the field content of the theory? Questions of this type underlie area laws for entanglement entropy, the thermodynamics of black holes, and the information-theoretic approach to quantum field theory.

S. Hollands and K. Sanders, Entanglement measures and their properties in quantum field theory (arXiv:1702.04924, SpringerBriefs in Mathematical Physics, 2018), define entanglement measures directly on the von Neumann algebras of local observables, without assuming a tensor product structure, and prove upper and lower bounds for them in several classes of theories. For conformal field theories in $d+1$ dimensions, $d>1$, they bound the relative entanglement entropy of the vacuum between a ball of radius $r$ and the outside of a concentric ball of radius $R>r$ by the partition function of the conformal Hamiltonian (Theorem 13, p. 79).

Setting

Let $\mathcal H$ be a Hilbert space and $\mathfrak A_A,\mathfrak A_B\subseteq B(\mathcal H)$ commuting von Neumann algebras, with join $\mathfrak A_A\vee\mathfrak A_B=(\mathfrak A_A\cup\mathfrak A_B)''$. A normal state $\sigma$ on the join is separable if $\sigma(ab)=\sum_j\varphi_j(a)\psi_j(b)$ for $a\in\mathfrak A_A$, $b\in\mathfrak A_B$, with positive normal functionals $\varphi_j,\psi_j$ and $\sum_j\varphi_j(1)\psi_j(1)<\infty$. Araki's relative entropy $H(\omega,\sigma)\in(-\infty,\infty]$ of two positive normal functionals generalizes $\operatorname{Tr}\rho(\ln\rho-\ln\rho')$. The relative entanglement entropy of a normal state $\omega$ is

$$E_R(\omega)=\inf\{H(\omega,\sigma):\sigma\text{ a separable state}\},$$

equal to $+\infty$ when there is no separable state. Two auxiliary measures enter: the logarithmic dominance $E_N(\omega)=\inf\{\ln\sigma(1):\sigma\geqslant\omega,\ \sigma\text{ separable}\}$, and the modular entanglement measure $E_M(\omega)=\ln\min(\|\Psi^A\|_1,\|\Psi^B\|_1)$, where $\Psi^A(a)=\Delta^{1/4}a\Omega$, $\Delta$ is the modular operator of $\mathfrak A_B'$ at the vector $\Omega$ of $\omega$, and $\|\cdot\|_1$ is the 1-nuclear norm.

A conformal field theory in $d+1$ dimensions is given, in its vacuum representation, by a net $O\mapsto\mathfrak A(O)$ of von Neumann algebras on a Hilbert space $\mathcal H_0$ indexed by causal diamonds $O$ of Minkowski space $\mathbb R^{d,1}$, a unitary representation $U$ of a covering group $\tilde G$ of the conformal group $SO_+(d+1,2)/\mathbb Z_2$ that acts covariantly on the net, and an invariant vacuum vector $|0\rangle$ with vacuum state $\omega_0$. The conformal Hamiltonian $\tfrac12(P^0+K^0)$ is the generator of the rotation $M_{0(d+2)}$ of $\mathfrak{so}(d+1,2)$, the sum of the energy $P^0\geq0$ and the generator $K^0$ of special conformal transformations in the time direction; $D$ generates dilations. For $R>r>0$, $\mathfrak A_A$ is the algebra of the double cone over the ball of radius $r$ about the origin, and $\mathfrak A_B$ that of the domain of dependence of the complement of the ball of radius $R$.

Formalization targets

Goal: Theorem 13

$$E_R(\omega_0)\leqslant\ln\operatorname{Tr}\Big(\frac rR\Big)^{\frac12(P^0+K^0)}\qquad(210)$$

for every conformal field theory satisfying the axioms, every $d\ge2$ and every $0<r<R$. The right side is $+\infty$ when the trace diverges.

Milestones

1. Theorem 3: $E_R(\omega)\le E_N(\omega)$.
2. Lemma 3: if $\|\Psi^A\|_1<\infty$, then $\omega(ab)=\sum_j\varphi_j(a)\psi_j(b)$ with normal $\varphi_j,\psi_j$ and $\sum_j\|\varphi_j\|\|\psi_j\|<\|\Psi^A\|_1+\varepsilon$.
3. Lemma 4: such a decomposition yields a separable $\sigma\geqslant\omega$ with $\|\sigma\|=\sum_j\|\varphi_j\|\|\psi_j\|$.
4. Theorem 4: $E_N(\omega)\le E_M(\omega)$.
5. $\|\Psi^A\|_1\le\|\Phi^A\|_1$, with $\Phi^A(a)=\Delta_{B'}^{1/4}a|0\rangle$ for the larger algebra $\mathfrak A_{B'}\subseteq\mathfrak A_B'$ (p. 56).
6. $\|\Delta^{1/4}a\Omega\|\le\|a\|$ for any von Neumann algebra with cyclic and separating $\Omega$ (proof of Theorem 13, p. 80).
7. Lemma 13: $\Delta_{B'}^{it}e^{isD}\Delta_{B'}^{-it}=\exp[-\tfrac{is}2\sinh(2\pi t)(P^0+K^0)+is\cosh(2\pi t)D]$.
8. (219): $\Delta_A=e^{-i(\ln r)D}\Delta_{B'}e^{i(\ln r)D}$.
9. (212): $\Delta_{B'}^{1/4}\Delta_A^{-1/4}=r^{\frac12(P^0+K^0)}r^{iD}$.

Significance

Theorem 13 bounds the vacuum entanglement of two regions by a quantity of the theory's spectrum alone. Combined with the paper's identification of $\operatorname{Tr}r^{\frac12(P^0+K^0)}$ with $\sum_{O}r^{d_O}$ over the spectrum of operator dimensions (Theorem 14, p. 83), it shows that for $R\gg r$ the entanglement decays like $(r/R)^{d_O}$ with $d_O$ the smallest non-zero dimension, and for $r\to R$ it diverges at most like $(\ln(R/r))^{-d}$. The general results on the way, $E_R\le E_N\le E_M$ and the nuclearity estimates, apply to any pair of commuting von Neumann algebras and underlie all upper bounds of the paper, including those for free and integrable models.

The results are proved in the paper, at the level of rigour of mathematical physics, with some steps cited (the Hislop–Longo theorem, the Heinz–Löwner inequality for unbounded operators, the edge-of-the-wedge theorem, the Reeh–Schlieder theorem). None of them is machine-checked. A formal proof would also make precise which axioms each step uses, for instance where statistical independence of $\mathfrak A_A$ and $\mathfrak A_B$, which is not an axiom here, enters.

Difficulty

The obvious route, comparing the vacuum with product states through a tensor product decomposition $\mathcal H_0=\mathcal H_A\otimes\mathcal H_B$, is not available: the local algebras are type III factors and there is no such decomposition. Every step must work with modular operators of the local algebras and normal functionals on their join. The analytic core is the operator identity (212): $\Delta_{B'}^{1/4}$ and $\Delta_A^{-1/4}$ are unbounded, Lemma 13 holds for real $t$ only, and reaching $t=-i/4$ requires analytic continuation in a strip, domain control through the Heinz–Löwner inequality, and the edge-of-the-wedge theorem. Separately, $E_N\le E_M$ needs that products of normal functionals on $\mathfrak A_A$ and $\mathfrak A_B$ are normal on the join, which in the conformal setting follows from modular nuclearity rather than from an axiom.

Formalization scope

The general layer (Definitions 5, 7, 10–13) is stated for von Neumann algebras $\mathfrak A_A,\mathfrak A_B\subseteq B(\mathcal H)$ in Mathlib's VonNeumannAlgebra, with functionals as maps $B(\mathcal H)\to\mathbb C$ of which only the values on the relevant algebra matter. Normal functionals are given by vector sums $\sum_n\langle\xi_n,a\eta_n\rangle$. The relative entropy is Araki's, in Kosaki's variational form, which is defined for all pairs of positive normal functionals. $H$, $E_R$, $E_N$, $E_M$ take values in EReal and norms in ℝ≥0∞, so empty infima are $+\infty$, as Definitions 5, 12 and 13 require. Separability is defined on the join, as in Theorem 2 c); no split property is assumed in the goal. Lemma 4 and Theorem 4 carry the §3 standing assumption of statistical independence, in the form that products of positive normal functionals are normal on the join. Modular operators are the published StandardModularData of BoundedRecovery; $\Delta^{1/4}$ is the limit of spectral cut-offs.

The conformal layer is a structure CFTVacuum d H₀: the net with isotony and locality (the algebra of a region such as $O_B$ contains those of the double cones inside it and commutes with those spacelike to it, without an additivity assumption the paper does not make) and weak additivity; a covering group of $SO_+(d+1,2)$ presented by a covering homomorphism with discrete kernel and an exponential map; a strongly continuous unitary representation with local covariance a3′); a unique invariant vacuum vector, cyclic for the quasi-local algebra (the GNS representation of a4′)); the generators $P^0\ge0$, $\tfrac12(P^0+K^0)$ and $D$ as spectral calculi; and the Hislop–Longo theorem for the unit double cone as a disclosed field. The projective representation of the paper is taken as a true representation of the cover (Bargmann). Generator signs are fixed so that $P^0$ generates forward time translations and $e^{isD}$ shrinks regions, consistent with (217), (219) and p. 84. $(r/R)^{\frac12(P^0+K^0)}$ is the bounded function $u\mapsto(r/R)^{\max(u,0)}$ of the conformal Hamiltonian, whose spectrum is non-negative (footnote 42), and the trace is taken in $[0,\infty]$. The goal assumes $d\ge2$ (§4.4, p. 78).

No conclusion of the paper is a field of the structure: not modular nuclearity a5′), not the split property, not (212) or (219), so the goal is not a restatement of its hypotheses. Theorem 14 (the field-content form $\ln\sum_{O\in\Phi}(r/R)^{d_O}$) is not stated: a faithful encoding of the operator-valued fields, their conformal transformation law (224) and descendants is left for a later mission.

Reusable beyond this mission: the entanglement measures on general von Neumann algebras, the 1-nuclear norm, $\Delta^{1/4}$, and the conformal structure. Contributions are welcome on the Kosaki formula (scaling, monotonicity, $H(\omega,\omega)=0$), on Heinz–Löwner for unbounded operators, and on the analytic continuation of modular groups.

Selected references

• S. Hollands, K. Sanders, Entanglement measures and their properties in quantum field theory, SpringerBriefs in Mathematical Physics, 2018. arXiv:1702.04924v3
• H. Araki, Relative entropy of states of von Neumann algebras, Publ. RIMS 11 (1976). doi:10.2977/prims/1195191148
• H. Kosaki, Relative entropy of states: a variational expression, J. Operator Theory 16 (1986). jot
• P. D. Hislop, R. Longo, Modular structure of the local algebras associated with the free massless scalar field theory, Comm. Math. Phys. 84 (1982). doi:10.1007/BF01208373
• R. Brunetti, D. Guido, R. Longo, Modular structure and duality in conformal quantum field theory, Comm. Math. Phys. 156 (1993). doi:10.1007/BF02096738
• D. Buchholz, C. D'Antoni, R. Longo, Nuclear maps and modular structures I, J. Funct. Anal. 88 (1990). doi:10.1016/0022-1236(90)90104-S

Motivation

A Hilbert space has an orthonormal basis, so every Hilbert space is isometric to some $\ell^2(I)$. Hilbert C$^*$-modules, the analogue of Hilbert spaces in which the inner product takes values in an operator algebra, have no such basis in general. Over a von Neumann algebra $\mathcal M$, Paschke showed that the self-dual Hilbert C$^*$-modules are exactly the "ultraweak direct sums" of corners $q_\alpha\mathcal M$ cut by projections $q_\alpha\in\mathcal M$ (Paschke, Trans. AMS 182, 1973).

Junge and Sherman (arXiv:math/0301044v2, 2003, revised 2004) carried this picture to the noncommutative $L^p$ spaces $L^p(\mathcal M)$, $0<p\le\infty$. They introduced $L^p$ modules, whose inner product takes values in $L^{p/2}(\mathcal M)$, and proved that every $L^p$ module is a column sum of corners $q_\alpha L^p(\mathcal M)$. The result organizes the study of module maps between noncommutative $L^p$ spaces (the paper's §5–§6 on commutants and $L^p$ bimodules build on it), and it is the $L^p$ form of the orthonormal-basis theorem. Earlier, Junge had proved a version for a special class of $L^p$ modules ([J1, Prop. 2.8]).

Setting

Let $n\in\mathbb N$ and let $\mathcal M$ be a unital $*$-subalgebra of the matrix algebra $M_n(\mathbb C)$; these are exactly the finite-dimensional von Neumann algebras. For real $0<p<\infty$, $L^p(\mathcal M)$ is $\mathcal M$ with the tracial (quasi)norm

$$\|a\|_p=\big(\mathrm{Tr}\,(a^*a)^{p/2}\big)^{1/p}.$$

In the Lean files this is lpNorm p a, the published Schatten norm schattenNorm.

Let $\mathfrak X$ be a complex vector space with a right action $(\xi,x)\mapsto\xi x$ of $\mathcal M$ (act). An $L^{p/2}$-valued inner product (Definition 2.1) is a map $\langle\cdot,\cdot\rangle:\mathfrak X\times\mathfrak X\to\mathcal M$ (ip). It is conjugate linear in the first variable and linear in the second, and satisfies

$$\langle\xi,\eta x\rangle=\langle\xi,\eta\rangle x,\qquad\langle\xi,\eta\rangle=\langle\eta,\xi\rangle^*,\qquad\langle\xi,\xi\rangle\ge0,\quad\langle\xi,\xi\rangle=0\iff\xi=0.$$

It induces

$$\|\xi\|=\big\|\langle\xi,\xi\rangle^{1/2}\big\|_p=\big(\mathrm{Tr}\,\langle\xi,\xi\rangle^{p/2}\big)^{1/p}$$

(gauge p ip ξ). By Proposition 2.2 this is a norm for $p\ge2$ and a $p/2$-norm for $p\le2$. A right $L^p$ $\mathcal M$-module (Definition 2.3) is such an $\mathfrak X$ that is complete in $\|\cdot\|$.

Given projections $(q_\alpha)_{\alpha\in I}$ of $\mathcal M$, the column sum (2.4) is

$$\textstyle\bigoplus_c q_\alpha L^p=\Big\{(\xi_\alpha)_{\alpha\in I}:\ \xi_\alpha\in q_\alpha L^p,\ \sum_\alpha\xi_\alpha^*\xi_\alpha\ \text{converges}\Big\},\qquad\langle(\xi_\alpha),(\eta_\alpha)\rangle=\sum_\alpha\xi_\alpha^*\eta_\alpha.$$

In Lean this is columnSumSet M q with colIp. The paper calls these modules principal.

Formalization targets

Goal: Theorem 2.5

For every right $L^p$ $\mathcal M$-module $\mathfrak X$ there are an index set $I$, projections $(q_\alpha)$ of $\mathcal M$ and a map $T:\mathfrak X\to\bigoplus_c q_\alpha L^p$ with the following properties: $T$ is bijective, complex linear and a module map, and

$$\Big\|\Big(\sum_\alpha T(\xi)_\alpha^*T(\xi)_\alpha\Big)^{1/2}\Big\|_p=\big\|\langle\xi,\xi\rangle^{1/2}\big\|_p\qquad(\xi\in\mathfrak X).$$

This is the paper's statement as printed: "isometrically isomorphic, as a module". The index set and the projections are not fixed; they are part of the conclusion.

Milestones

1. Lemma 1.2: $\overline{\mathcal M\varphi^{1/p}}=L^ps(\varphi)$ and $\overline{\varphi^{1/p}\mathcal M}=s(\varphi)L^p$.
2. Lemma 1.4: a bounded compatible net $\xi_\alpha=\xi_\alpha p_\alpha$, $\xi_\beta p_\alpha=\xi_\alpha$ $(\alpha<\beta)$ in $L^r$, $r<\infty$, converges in norm.
3. Proposition 2.2: $\langle\xi,\eta\rangle=\langle\xi,\xi\rangle^{1/2}T\langle\eta,\eta\rangle^{1/2}$ with $\|T\|\le1$; $\|\langle\xi,\eta\rangle\|_{p/2}\le\|\xi\|\|\eta\|$; and $\|\cdot\|$ is a norm ($p\ge2$) or a $p/2$-norm ($p\le2$).
4. (2.4): the column sum is a right $L^p$ module.
5. The cyclic case: $\overline{\xi\mathcal M}\cong s(\langle\xi,\xi\rangle^{1/2})L^p$.
6. Case 2 ($p>2$): the closed span of an orthogonal family is isomorphic to a column sum, and a vector with $0$ as best approximant from that span is orthogonal to the family.

Significance

Theorem 2.5 reduces questions about arbitrary $L^p$ modules to columns of corners of $L^p(\mathcal M)$. Two consequences follow. Module maps between $L^p$ modules become matrices of maps between corners, and the paper identifies the commutant of the right action and describes $L^p$ bimodules in this way. For $p=2$ the theorem is the orthonormal-basis theorem with $\mathcal M$-valued inner products; for $p=\infty$ it is Paschke's theorem. In between, there is no Hilbert-space structure to fall back on.

The result is proved in the paper for every von Neumann algebra and every $0<p\le\infty$. No part of it has been formalized. Mathlib has Hilbert C$^*$-modules with the C$^*$-norm and the Hermitian functional calculus for matrices, but no noncommutative $L^p$ spaces, no $L^p$ modules and no column sums. This mission produces the finite-dimensional theory: the definitions, the Cauchy–Schwarz inequality (2.1)–(2.2) for $L^{p/2}$-valued inner products, the column-sum construction and the structure theorem.

Difficulty

Even when $\mathcal M$ is finite-dimensional, $\mathfrak X$ need not be. An $L^p$ module may be an infinite column of corners, and the theorem must produce the decomposition without any basis to start from. The obvious idea is to copy Gram–Schmidt and Zorn: take a maximal orthogonal family $\{\xi_\alpha\}$ and show that its closed span $\mathfrak X_0$ is everything. For $p\ne2$ this step fails as stated. Without an inner product on $\mathfrak X$ there is no orthogonal projection onto $\mathfrak X_0$. A best approximation from $\mathfrak X_0$ exists only for $p>2$ (where $\mathfrak X$ is a Banach space and $\mathfrak X_0$ is reflexive), and turning "$0$ is a best approximant of $\zeta$" into the algebraic identity $\langle\zeta,\xi_\lambda\rangle=0$ needs smoothness of the $L^p$ norm together with the factorization (2.1). The case $p<2$ is reached by a different route through tensor products with $L^q(\mathcal M)$. A second difficulty is that $\|\cdot\|$ is the trace norm of $\langle\xi,\xi\rangle^{1/2}$: it depends on $p$ and is not the C$^*$-module norm, so Mathlib's C$^*$-module results do not apply.

Formalization scope

• Finite-dimensional algebra. $\mathcal M$ is a StarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ). $L^p(\mathcal M)$ is $\mathcal M$ with the Schatten (quasi)norm of the trace, which is isometric to Haagerup's $L^p(\mathcal M)$. This restriction is forced: Haagerup $L^p$ spaces of a general von Neumann algebra exist neither in Mathlib nor on the platform. Because $L^{p/2}(\mathcal M)=\mathcal M$ as a set, the inner-product axioms do not depend on $p$; the norm does.
• Exponents. Every item assumes $0<p<\infty$, and Case 2 items assume $p>2$ as in the paper. $p=\infty$ is out of scope.
• The module. $\mathfrak X$ is any complex vector space, of any dimension. The action is a function act with the right-module axioms for elements of $\mathcal M$, and the inner product is the structure LpInnerProduct. Completeness is sequential completeness for $\|\cdot\|$ (GaugeComplete), since $\|\cdot\|$ is only a quasi-norm for $p<2$.
• Column sums. A column sum is a set of families $I\to M_n(\mathbb C)$. Convergence of $\sum_\alpha\xi_\alpha^*\xi_\alpha$ is unconditional summability. In the goal, $I$ lives in the universe of $\mathfrak X$.
• Closures. In Lemma 1.2 and in the cyclic case the closures on the page are of finite-dimensional subspaces and are dropped. The closed span $\mathfrak X_0$ of Case 2 keeps its closure.
• No trivialization. Several formalizations would make the theorem empty or a different theorem, and none is admissible: measuring $\mathfrak X$ in the C$^*$-norm $\|\langle\xi,\xi\rangle\|^{1/2}$ (which makes the statement the $p=\infty$ theorem), assuming $\mathfrak X$ finite-dimensional or given with a basis, or asking only for a non-bijective or non-linear $T$.
• Infrastructure. The development needs the Hermitian functional calculus on matrices (square roots, powers, support projections), Hölder's inequality and the $p/2$-triangle inequality for Schatten quasinorms, and summability of positive matrix families. These pieces are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of Theorem 2.5 by routes other than the paper's.

Selected references

• M. Junge and D. Sherman, Noncommutative $L^p$ modules, preprint arXiv:math/0301044v2, 2003, revised 14 Sep 2004. arXiv:math/0301044v2
• W. L. Paschke, Inner product modules over B$^*$-algebras, Trans. Amer. Math. Soc. 182 (1973), 443–468 (reference [Pa] of the paper; cited as [P] on p. 10).
• H. Kosaki, Applications of the complex interpolation method to a von Neumann algebra: noncommutative $L^p$-spaces, J. Funct. Anal. 56 (1984), 29–78 (reference [K1] of the paper).
• U. Haagerup, $L^p$-spaces associated with an arbitrary von Neumann algebra, Algèbres d’opérateurs et leurs applications en physique mathématique, CNRS 15 (1979), 175–184 (reference [H] of the paper).