All missions

Motivation

Noncommutative $L_p$-spaces built from a von Neumann algebra $M$ come in two kinds. When $M$ carries a normal faithful trace, $L_p(M)$ is a space of (unbounded) operators affiliated with $M$, and much of classical analysis — martingale inequalities, square functions, maximal inequalities, interpolation — has been carried over to this tracial setting. Algebras of type III, which occur naturally in quantum field theory and quantum statistical mechanics, have no such trace; their $L_p$-spaces are Haagerup's, defined through a crossed product and the dual weight.

Haagerup, Junge and Xu (arXiv:0806.3635, Trans. AMS 362 (2010)) give a general method for transferring tracial results to type III algebras. Its engine is a reduction theorem, due to Haagerup and circulated as an unpublished manuscript since the late 1970s: after enlarging $M$ to a crossed product, the algebra is approximated by an increasing sequence of finite von Neumann algebras, in a way that respects the state and its modular group. This mission formalizes that theorem, §2 of the paper.

Timeline. Haagerup constructs his $L_p$-spaces in 1979 (Colloq. Internat. CNRS 274) and proves the reduction in the manuscript [H3]. Junge and Xu use it for noncommutative Burkholder–Rosenthal inequalities (Ann. Probab. 2003) and maximal ergodic theorems (J. AMS 2007). The 2008 preprint, revised in 2009, gives the first published proof together with its applications to $L_p$ approximation, extension of maps to crossed products, and martingale and maximal inequalities.

Setting

$M$ is a von Neumann algebra on a Hilbert space $H$ with a normal faithful state $\varphi$. Up to spatial isomorphism $M$ is in standard form: there is a unit vector $\xi$, cyclic and separating for $M$, with $\varphi(x) = \langle x\xi,\xi\rangle$. Tomita–Takesaki theory supplies the modular operator $\Delta$ and the modular automorphism group $\sigma^\varphi_t(x) = \Delta^{it}x\Delta^{-it}$.

$G = \bigcup_{n\ge1}2^{-n}\mathbb Z$ is the group of dyadic rationals with the discrete topology. On $\ell^2(G,H)$ define

$$(\pi(x)\eta)(h) = \sigma^\varphi_{-h}(x)\,\eta(h),\qquad (\lambda(g)\eta)(h) = \eta(h-g),$$

for $x\in M$, $g,h\in G$. The crossed product $\mathcal R = M\rtimes_{\sigma^\varphi}G$ is the von Neumann algebra generated by $\pi(M)$ and $\lambda(G)$. With $\hat\xi = \delta_0\otimes\xi$, the dual state is $\hat\varphi(y) = \langle y\hat\xi,\hat\xi\rangle$; on generators $\hat\varphi(\lambda(g)\pi(x))$ equals $\varphi(x)$ for $g = 0$ and $0$ otherwise. Its modular group is $\sigma^{\hat\varphi}$, and $\|y\|_{\hat\varphi} = \hat\varphi(y^*y)^{1/2}$.

For a bounded functional $\psi$ on an algebra $A$, the centralizer is $A_\psi = \{x\in A:\psi(xy) = \psi(yx)\ \forall y\in A\}$. With $b_n = -i\,\mathrm{Log}\,\lambda(2^{-n})$ (branch $0\le\operatorname{Im}\mathrm{Log}<2\pi$), $a_n = 2^nb_n$ and $\varphi_n(x) = \hat\varphi(e^{-a_n}x)$, the subalgebras are $\mathcal R_n = \mathcal R_{\varphi_n}$. A von Neumann algebra is finite if every isometry in it is unitary. A conditional expectation from $\mathcal R$ onto a subalgebra $A$ is a positive linear $A$-bimodular map onto $A$ fixing $A$.

Formalization targets

Goal: Theorem 2.1 (p. 6)

There is an increasing sequence $(\mathcal R_n)$ of von Neumann subalgebras of $\mathcal R$ such that each $\mathcal R_n$ is finite, $\bigcup_n\mathcal R_n$ is w*-dense in $\mathcal R$, and for each $n$ there is a normal faithful conditional expectation $\Phi_n:\mathcal R\to\mathcal R_n$ with

$$\hat\varphi\circ\Phi_n = \hat\varphi,\qquad \sigma^{\hat\varphi}_t\circ\Phi_n = \Phi_n\circ\sigma^{\hat\varphi}_t\quad(t\in\mathbb R).$$

The goal asserts existence only, as printed; the construction $\mathcal R_n = \mathcal R_{\varphi_n}$ is the content of the milestones.

Milestones

1. Dual modular data (p. 6, (1.7) p. 4): $\hat\xi$ is cyclic and separating for $\mathcal R$, so $\hat\varphi$ has modular data; $\sigma^{\hat\varphi}_t(\pi(x)) = \pi(\sigma^\varphi_t(x))$ and $\sigma^{\hat\varphi}_t(\lambda(g)) = \lambda(g)$.
2. Lemma 2.2: $\hat\varphi(f(\lambda(t))) = \int_{\mathbb T}f\,dm$ for $t\in G\setminus\{0\}$.
3. Lemma 2.3: $\lambda(t)\in Z(\mathcal R_{\hat\varphi})$; $b_n$ is the unique element of $Z(\mathcal R_{\hat\varphi})$ with $0\le b_n\le2\pi$ and $e^{ib_n} = \lambda(2^{-n})$.
4. Lemma 2.4: $\sigma^{\varphi_n}$ is $2^{-n}$-periodic; there is a unique $\hat\varphi$-preserving, $\sigma^{\hat\varphi}$-commuting normal faithful conditional expectation onto $\mathcal R_n$; $\mathcal R_n\subseteq\mathcal R_{n+1}$.
5. Lemma 2.5: for a normal faithful state $\psi$, analytic $x$ gives $x\psi x^*\le c\psi$, and $x$ in the centralizer gives $x\psi x^*\le\|x\|^2\psi$.
6. Lemma 2.6: $\|[b_n,x]\|_{\hat\varphi}\to0$, $\sup_{|t|\le1}\|[e^{itb_n},x]\|_{\hat\varphi}\to0$, and $\sup_t\|\sigma^{\hat\varphi}_t(x)-e^{ia_nt}xe^{-ia_nt}\|_{\hat\varphi}\to0$.
7. Lemma 2.7: $\Phi_n(x)\to x$ σ-strongly, so $\bigcup_n\mathcal R_n$ is σ-strongly dense.

Significance

The reduction theorem lets a statement about Haagerup $L_p(M)$ be proved by checking it on the finite algebras $\mathcal R_n$, where traces exist, and passing to the limit: the expectations $\Phi_n$ extend to contractive projections on $L_p$ and their ranges exhaust $L_p(\mathcal R)$, which contains $L_p(M)$ complementably. The paper uses this to obtain noncommutative Burkholder–Gundy, Stein, Burkholder–Rosenthal and Doob inequalities, and maximal ergodic inequalities, for type III algebras; for some of these no other proof is known. The theorem has since become a standard tool in noncommutative probability and harmonic analysis.

The theorem is proved (in the cited paper, with details on pp. 7–11). It has not been formalized: Mathlib has von Neumann algebras as double commutants but no crossed products, conditional expectations, modular theory or Haagerup $L_p$-spaces. This mission produces a formal statement of the reduction theorem and of each lemma of its proof, built on the published standard-form encoding of Tomita–Takesaki data, and invites solvers to formalize the known proof.

Difficulty

The modular group of a type III algebra is outer and aperiodic, so no centralizer is large enough to be finite and dense at once. The proof works around this by perturbing $\hat\varphi$ to states $\varphi_n$ whose modular groups are periodic, and the delicate step is density: showing that the centralizers $\mathcal R_{\varphi_n}$ eventually see every element of $\mathcal R$. This rests on uniform estimates in the $\hat\varphi$-norm (Lemma 2.6) that need the distribution of $\lambda(t)$ under $\hat\varphi$ (Lemma 2.2), analytic elements (Lemma 2.5), and an $L_2$ approximation of the logarithm by trigonometric polynomials. Norm density of $\bigcup_n\mathcal R_n$ is false in general; only weak*-type density holds. For finite $M$ the statement is easy ($\mathcal R$ is already finite); the content is the type III case.

Formalization scope

$(M,\varphi)$ is given by the published OAI.BoundedRecovery.StandardModularData H: a von Neumann algebra on $H$, a unit cyclic separating vector $\xi$, $\log\Delta$ as a nondegenerate functional calculus, and $J$, tied together by the closed Tomita relation; $\sigma^\varphi_t$ is its sigma. Every σ-finite von Neumann algebra with a normal faithful state is spatially isomorphic to such data, and every statement is invariant under spatial isomorphism.

The crossed product is built on lp (fun _ : dyadic => H) 2, as the double commutant of $\pi(M)\cup\lambda(G)$ and their adjoints. $\pi(x)$, $\lambda(g)$ and $b_n$ are the bounded operators characterized by their pointwise formulas; $b_n$ is the Laurent operator of $\theta\mapsto\theta$ on $[0,2\pi)$ in the shift $\lambda(2^{-n})$, which is $-i\,\mathrm{Log}\,\lambda(2^{-n})$ (Mathlib has no Borel functional calculus). Centralizers use the commutation form for bounded functionals. Finiteness is the published OAI.FiniteFactor.IsFiniteAlgebra (every isometry is unitary). W*-density is equality of the double commutant with $\mathcal R$; σ-strong convergence of bounded sequences is strong convergence. Order on operators is the Loewner order. Lemma 2.2 is stated for continuous $f$, which already determines the distribution.

Hypothesized modular data. The platform has no Tomita–Takesaki existence theorem, so the modular data of $\hat\varphi$ (and of $\varphi_n$ in Lemma 2.4 (i)) enter as hypotheses $\hat S$ with $\hat S.M = \mathcal R$ and $\hat S.\xi = \hat\xi$; the first milestone proves such $\hat S$ exists, so the goal is not vacuous. The formalization does not restrict to finite, finite-dimensional or tracial $M$ (where the goal is empty); $\sigma^{\hat\varphi}$ is never defined by a formula; finite means "every isometry is unitary", not finite-dimensional; and density is never norm density.

Reusable beyond this mission: the dyadic crossed product and dual state, conditional expectations, the commutation-form centralizer, and Lemma 2.5 for arbitrary standard-form data. Welcome contributions include the existence of modular data for crossed products, the shift and Laurent operators on $\ell^2$ of a discrete group, and the averaging construction of conditional expectations from periodic modular groups.

Selected references

• U. Haagerup, M. Junge, Q. Xu, A reduction method for noncommutative $L_p$-spaces and applications, Trans. Amer. Math. Soc. 362 (2010), 2125–2165; arXiv:0806.3635v2. https://arxiv.org/abs/0806.3635
• U. Haagerup, $L^p$-spaces associated with an arbitrary von Neumann algebra, Algèbres d'opérateurs et leurs applications en physique mathématique, Colloq. Internat. CNRS 274 (1979), 175–184.
• Ş. Strătilă, Modular Theory in Operator Algebras, Editura Academiei / Abacus Press, 1981 (dual weights, §19).
• M. Takesaki, Theory of Operator Algebras II, Encyclopaedia Math. Sci. 125, Springer, 2003. https://doi.org/10.1007/978-3-662-10451-4
• M. Junge, Q. Xu, Noncommutative maximal ergodic theorems, J. Amer. Math. Soc. 20 (2007), 385–439. https://doi.org/10.1090/S0894-0347-06-00533-9

Why random gate sets matter

Quantum information protocols often require a finite collection of unitary gates whose averages reproduce those of the full unitary group. A unitary design gives a precise finite-moment version of that requirement. When gates are sampled from an exact design, a practitioner needs to know how many independent draws make the empirical collection a reliable approximation. Dulian and Sawicki give an explicit probability bound for that question in Theorem 1 of their paper. The bound depends on the sample count, the desired accuracy, and the dimensions of the irreducible representations visible at the chosen moment order.

The result joins two subjects. Matrix concentration controls the norm of a sum of random operators. Representation theory identifies which operator blocks occur in the moment being estimated and supplies their dimensions. Neither ingredient alone gives the numerical bound stated by the paper. This mission formalizes their combination for independent gates drawn from any exact $t$-design, including Haar-distributed gates.

Unitary moments and sampled gates

Fix integers $d,t\ge0$. Write $U(d)$ for the group of complex $d\times d$ unitary matrices and $\mu$ for its Haar probability measure. For a gate $U\in U(d)$, its mixed tensor representation is

$$U^{t,t}=U^{\otimes t}\otimes\overline U^{\otimes t},$$

where the bar conjugates every matrix entry. For a probability measure $\nu$ on $U(d)$, the moment operator is $T_{\nu,t}=\int U^{t,t}\,d\nu(U)$. An exact $t$-design is a probability measure $\nu$ satisfying $T_{\nu,t}=T_{\mu,t}$. The design distance is $\delta(\nu,t)=\|T_{\nu,t}-T_{\mu,t}\|$, using the spectral operator norm.

Draw $S$ independent gates $U_1,\ldots,U_S$ from an exact $t$-design $\nu$, with $S\ge1$. Their empirical measure $\nu_S$ counts every draw, including repetitions, with weight $1/S$. Thus $T_{\nu_S,t}=S^{-1}\sum_{k=1}^S U_k^{t,t}$. This convention implements the sum used in the paper's concentration argument and remains meaningful when the sampling distribution has atoms.

The moment representation splits into a trivial part and nontrivial irreducible blocks indexed by $\Lambda_t$. An index $\lambda=(\lambda_1,\ldots,\lambda_d)$ is a nonzero weakly decreasing integer tuple with $\sum_i\lambda_i=0$ and $\sum_i\max(\lambda_i,0)\le t$. Its block dimension is the Weyl dimension

$$d_\lambda=\prod_{1\le i<j\le d}\frac{\lambda_i-\lambda_j+j-i}{j-i}.$$

This explicit index set and dimension formula come from equations (20), (22), and (23) of the source. The zero- and one-dimensional cases are included in the formal statement; their nontrivial index set can be empty.

Formalization targets

The goal is the corrected positive-threshold form of Theorem 1, for $S\ge1$ and $0<\delta<1$:

$$\Pr\bigl(\delta(\nu_S,t)\ge\delta\bigr)\le \frac{2e^{-\delta S\operatorname{artanh}(\delta)}}{(1-\delta^2)^{S/2}} \sum_{\lambda\in\Lambda_t}d_\lambda.$$

The paper prints “any $\delta<1$.” Its formula fails for some nonpositive $\delta$: a negative threshold makes the event certain while the displayed expression can decrease below one as $S$ grows. At $\delta=0$, an empty $\Lambda_t$ also gives a zero right-hand side for a certain event. The positive-threshold range is the meaningful form of its result.

The milestone list follows the paper's numbered claims. Fact 2 provides a master concentration bound for independent complex matrices through Hermitian dilation. Theorem 18 specializes it to one irreducible block, with its two equivalent closed forms of the tail factor. Lemma 16 and equation (24) connect the full design distance to the norms of those blocks and state the resulting union bound. Fact 9 supplies the decomposition indexed by $\Lambda_t$ and the Weyl dimensions needed to turn the block sum into Theorem 1's explicit sum.

What the result provides

The bound gives a finite-sample guarantee for the mixed tensor moment of random gates. It exposes how an accuracy threshold and a representation-theoretic dimension sum determine the chance that the empirical moment differs from Haar averaging. A reader can evaluate the right-hand side once $d$, $t$, $S$, and $\delta$ are fixed. The bound also covers Haar random gates because Haar measure itself is an exact design at every order, as the paper observes in Section 6.

The mathematical result was proved by Dulian and Sawicki; the machine-checked development requested here remains to be built. Existing published Prove2Me modules already provide a spectral matrix norm, a Hermitian dilation, and a general matrix master bound. The new formalization must establish the paper's mixed tensor representation model, its irreducible decomposition and weight dimensions, the one-block estimate, and their assembly into the displayed inequality. These components can serve later results on random unitary designs and matrix concentration.

Main difficulty

The operator $U^{t,t}$ acts on a space of dimension $d^{2t}$, so applying a single matrix tail bound directly to it leaves a prefactor governed by that large ambient dimension. The paper's sharper expression depends on separating the nontrivial irreducible blocks, removing the Haar-invariant part, and identifying the dimensions of exactly the blocks that occur. The critical representation-theoretic step is the complete, multiplicity-aware decomposition in Fact 9. A bound for an arbitrary collection of block matrices would not identify the paper's $\Lambda_t$ or its Weyl dimension sum.

Formalization scope

Lean represents $U(d)$ as Matrix.unitaryGroup (Fin d) ℂ with the measurable space induced from the published Borel structure on complex matrices. The mixed tensor basis is indexed by a pair of functions from Fin t to Fin d; ordinary factors come first, conjugate factors second. The measure $\mu$ is required to be a left- and right-invariant probability measure. An exact design is a probability measure with equality of the full mixed $t$th moment, not merely a first moment or a one-sided tensor power. Independent samples use the product measure, and the empirical moment is their average with multiplicity.

The norm is the published $L^2$ operator norm on matrices. The set $\Lambda_t$ is a finite set of integer tuples; bounds $-t\le\lambda_i\le t$ follow from its defining constraints. The Weyl product uses zero-based Fin d indices, which preserve every difference $j-i$. All real exponents are real powers, with positive bases in the stated threshold range. The supremum over zero nontrivial blocks is defined to be zero, matching the zero design distance in that case.

The representation structure requires positive dimensions and multiplicities, irreducibility, pairwise inequivalence, orthogonal isometric embeddings, completeness, and intertwining with the concrete mixed tensor action. Those requirements prevent a vacuous or incomplete block family from making the goal automatic. Contributions are welcome on the representation decomposition, the Haar projection onto the trivial part, the non-Hermitian matrix bound, and the probability-to-block reduction. The source's highest-weight labels are kept: the block indexed by $\lambda\in\Lambda_t$ has $\lambda$ as its highest weight, expressed through weights of the diagonal torus and the dominance order of the simple roots $L_i-L_{i+1}$, and its dimension is the Weyl product $d_\lambda$.

Selected references

• C. Dulian and A. Sawicki, Matrix concentration inequalities and efficiency of random universal sets of quantum gates, arXiv preprint (2023), arXiv:2202.05371v3.
• J. A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning, 2015, doi:10.1561/2200000048.

Consumer search when the set of options is not known in advance

In the standard model of costly sequential search, a consumer knows from the start which products exist and pays to learn how much each is worth. Weitzman (Econometrica 1979) solved this problem with a single number per product, the reservation value: inspect in decreasing order of reservation values, and stop as soon as the best product found is worth more than every remaining reservation value. This rule underlies most structural models of online search in marketing and industrial organization.

In many markets, though, consumers do not know every option at the start. On a retail platform they scroll through results a page at a time, and each page shows only partial information (price, picture, rating) about the products it reveals. Learning the full value of a product requires clicking on it. The consumer therefore chooses among three kinds of action: buy, inspect a product already seen, or discover more products. R. P. Greminger, Optimal Search and Discovery (Management Science, 2022), shows that this richer problem is still solved by comparing reservation values, now three kinds of them.

Timeline. Weitzman (1979) treats inspection with a known set of products. Keller and Oldale (JET 2003) prove that a Gittins index policy is optimal for branching bandits, in which taking an action creates new actions. Choi, Dai and Kim (Econometrica 2018) give the eventual purchase theorem for Weitzman's problem. Greminger (arXiv 2019, journal 2022) adds the discovery action and characterizes the optimal policy.

The search and discovery problem

A risk-neutral consumer gets utility $u(x_j,y_j)=x_j+y_j$ from buying product $j$. The partial valuation $x_j$ is visible as soon as the product is discovered. The rest of the value, $y_j$, is revealed only by inspection. The pairs $(x_j,y_j)$ are independent draws of $(X,Y)$, where $X\sim G$ and $Y\mid X=x\sim F_{Y\mid X=x}$.

In period $t$ the consumer has a consideration set $C_t$ of inspected products (valuation $x_j+y_j$ known), which also contains an outside option worth $u_0$, and an awareness set $S_t$ of discovered products for which only $x_j$ is known. The available actions are:

1. buy any product of $C_t$, which ends search;
2. inspect a product of $S_t$ at cost $c_s>0$, which moves it to $C_t$;
3. discover $n_d$ more products at cost $c_d>0$, which adds them to $S_t$.

With probability $q\in[0,1]$, the consumer believes, a discovery is the last one. Recall is free, payoffs are not discounted, and the objective is the expected purchase value minus the total costs paid.

The three reservation values are defined against a hypothetical outside option $z$. The search value $z^s_j$ is the root of

$$Q_s(x_j,c_s,z)=\mathbb E_Y\big[\max\{0,x_j+Y-z\}\big]-c_s .$$

The purchase value is $z^b_j=x_j+y_j$. The discovery value $z^d$ is the root of

$$Q_d(c_d,c_s,z)=\mathbb E_{\boldsymbol X}\big[V(\text{outside option }z,\ n_d\text{ new products, no discovery})\big]-z-c_d ,$$

where $V$ is the optimal value of the reduced problem whose only products are the outside option and the $n_d$ newly discovered ones.

Formalization targets

Goal: Theorem 1

Let $\tilde z^b(t)=\max_{k\in C_t}z^b_k$ and $\tilde z^s(t)=\max_{k\in S_t}z^s_k$. Every policy that obeys

$$\text{buy } j \text{ only if } z^b_j=\tilde z^b(t)\ge\max\{\tilde z^s(t),z^d\},\qquad \text{inspect } j \text{ only if } z^s_j=\tilde z^s(t)\ge\max\{\tilde z^b(t),z^d\},$$ $$\text{discover only if } z^d\ge\max\{\tilde z^b(t),\tilde z^s(t)\}$$

is feasible and attains the largest expected payoff among all feasible policies, from every initial state.

Milestones

1. Equation (6) has a unique solution, and $Q_s$ is a tail integral of $F_{Y\mid X=x}$ (Appendix B).
2. The search value is the Gittins index of inspection: an outside option $w$ is optimal against one product $x$ if and only if $w\ge z^s(x)$.
3. $Q_d(z)=\mathbb E[\max\{z,\max_k\tilde W_k\}]-z-c_d=\int_z^\infty(1-H(w))\,\mathrm dw-c_d$, with $\tilde W_k=\min\{z^s_k,z^b_k\}$ (Appendix B).
4. Proposition 7: equation (10) has a unique solution.
5. The discovery value is the Gittins index of discovery: against an outside option $w$, discovering helps if and only if $w<z^d$.

Significance

The theorem turns a dynamic program over an infinite state space into comparisons of three reservation values. The discovery value still requires optimizing inspection among the products in one newly discovered batch. The paper builds on the result in several directions. Its second main result, an eventual purchase theorem under limited awareness (Theorem 2), is derived from Theorem 1. So are its closed-form expected payoff, its comparisons with random and directed search, and the claim that the discovery value, and hence the optimal policy, does not depend on the belief $q$.

Formalizing it gives the first machine-checked statement of a Weitzman-type optimality theorem with an outside option, partial information and a branching action. As far as a search of the Prove2Me catalog shows, Weitzman's rule itself is not formalized for undiscounted search with an outside option, so the milestones on the search value and on the closed form of $Q_d$ are new formalizations in their own right. The paper's proof relies on two external results, Keller and Oldale's branching bandit theorem and Choi, Dai and Kim's Corollary 1. A complete formal development either proves these or replaces them with a direct argument.

Difficulty

The obvious argument is to treat the problem as a multi-armed bandit and apply the Gittins index theorem. It does not apply as stated. Discovery creates new arms, the problem is undiscounted and ends at a purchase, and the number of future discoveries is random. The branching bandit theory that covers creating arms is stated for discounted rewards and in a derivative form, $\Theta=b-\int\prod_a\partial\Theta_a/\partial w$, which needs almost-everywhere differentiability of value functions in the outside option. The step specific to this paper is to show that the index of discovery does not depend on whether later discoveries are possible. That needs the index to be non-increasing along search, which the paper derives from stationarity. Finally, the rule policy must be shown to stop almost surely with an integrable payoff even when infinitely many products can be discovered ($q=0$).

Formalization scope

All objects live in the namespace SearchDiscovery.Reservation. A model SDModel carries $G$, the kernel κ ($F_{Y\mid X}$), cs, cd, nd and $q\in[0,1]$. Its standing assumptions are $c_s,c_d>0$, $n_d\ge1$, finite second moments of $G$ and of each κ x, and a finite unconditional mean of $Y$ (footnote 36). An information state lists the purchase values of $C_t$ (the outside option is one entry), the partial valuations of $S_t$, and whether discovery is available. A run is driven by an explicit probability space: the hidden $y$ of each initial awareness product, and for each discovery $n_d$ i.i.d. pairs together with an independent Bernoulli($q$) flag saying whether the discovery was the last.

The formalization commits to the following readings:

• Policies are deterministic functions of the information state.
• A feasible policy takes available actions and buys after finitely many periods almost surely, and has an integrable payoff.
• $\tilde z^s=-\infty$ when $S_t$ is empty.
• $z^d$ enters the buy and inspect rules only while discovery is available.
• $z^s$ and $z^d$ are hypotheses satisfying (6) and (10), not definitions.
• Theorem 1 is read as sufficiency: every rule-obeying policy, with any tie-break, is optimal. The policy's payoff is assumed measurable.

Several shortcuts would make the statements trivial, and the formalization rules them out:

• the rule predicate is satisfiable at every state, and FollowsRules is not vacuous;
• feasibility of the rule policy is a conclusion, not a hypothesis;
• maxima over empty sets are never given a junk value of 0;
• $Q_d$ is defined from the optimal value of the reduced problem, not from its closed form.

A complete development needs:

• path-wise runs of history-dependent searches over infinite product measures;
• an undiscounted optimal stopping and index theory with an outside option;
• the layer-cake identities for $Q_s$ and $Q_d$.

The Weitzman/Pandora layer (search values, the closed form of the reduced problem) is reusable well beyond this paper. Contributions to any milestone are welcome, as are alternative proofs that avoid the derivative form of the branching bandit theorem.

Selected references

• R. P. Greminger, Optimal Search and Discovery, Management Science, 2022, https://doi.org/10.1287/mnsc.2021.4085; preprint arXiv:1911.07773v5 (cited version), https://arxiv.org/abs/1911.07773
• M. L. Weitzman, Optimal Search for the Best Alternative, Econometrica 47(3), 641–654, 1979. https://doi.org/10.2307/1910412
• G. Keller and A. Oldale, Branching Bandits: A Sequential Search Process with Correlated Pay-offs, Journal of Economic Theory 113(2), 302–315, 2003. https://doi.org/10.1016/S0022-0531(03)00004-0
• M. Choi, A. Y. Dai and K. Kim, Consumer Search and Price Competition, Econometrica 86(4), 1257–1281, 2018. https://doi.org/10.3982/ECTA13803
• K. Adam, Learning While Searching for the Best Alternative, Journal of Economic Theory 101(1), 252–280, 2001. https://doi.org/10.1006/jeth.2000.2724

Motivation

Positive maps give tests for entanglement in bipartite quantum states. A density matrix can pass one positive-map test and fail another, so the choice of map changes which states can be detected. Maps that behave predictably under unitary changes of basis are particularly structured, but that symmetry can appear restrictive. Bardet, Collins, and Sapra ask whether requiring unitary equivariance loses the ability to detect states that a given positive map detects. Their Theorem 5.1 says that it does not, provided one permits a sequence of larger output matrix algebras. Bardet, Collins, and Sapra, §5

The question sits between two familiar perspectives. The positive-map criterion tests a state by applying a map to one subsystem; unitary equivariance controls how that map reacts when the subsystem is rotated. The paper's result shows that a specified detector can be recovered, in the limit of a nested family, within this symmetric class. It addresses a fixed input map and a fixed ancillary dimension. The paper separately states a more uniform corollary about Schmidt number, but that corollary is outside this mission. Bardet, Collins, and Sapra, Theorem 5.1 and Corollary 5.4

Setting

Write $M_n(\mathbb C)$ for complex $n\times n$ matrices and $U_n$ for their unitary group. A complex linear map $\phi:M_n(\mathbb C)\to M_N(\mathbb C)$ is $t$-positive if $\mathrm{id}_t\otimes\phi$ sends every positive semidefinite matrix on $\mathbb C^t\otimes\mathbb C^n$ to a positive semidefinite matrix. It is completely positive if it is $r$-positive for every natural number $r$. A map $\Phi:M_n(\mathbb C)\to M_D(\mathbb C)$ is unitarily equivariant if, for each $U\in U_n$, there is one unitary $V\in U_D$ satisfying $\Phi(UXU^*)=V\Phi(X)V^*$ for every $X\in M_n(\mathbb C)$. The choice of $V$ may depend on $U$ and $\Phi$, while the equality must hold for all $X$. Bardet, Collins, and Sapra, Definition 2.1

A density matrix on $\mathbb C^m\otimes\mathbb C^n$ is positive semidefinite and has trace one. The detection set of $\phi$ at ancillary dimension $m$ is

$$S_m(\phi)=\{\rho:\rho\geq0,\ \operatorname{Tr}\rho=1,\ (\mathrm{id}_m\otimes\phi)(\rho)\geq0\}.$$

Here $\phi$ acts on the second tensor factor. A state outside $S_m(\phi)$ is detected by $\phi$: applying $\mathrm{id}_m\otimes\phi$ produces an operator that is not positive semidefinite. No trace preservation or unitality is required of $\phi$. Bardet, Collins, and Sapra, equation (17)

Formalization targets

Main theorem

Fix $m,n,N,t$ with $1\leq t\leq\min\{m,n\}$ and a $t$-positive map $\phi:M_n(\mathbb C)\to M_N(\mathbb C)$ that is not completely positive. The target is one family $\Phi_a:M_n(\mathbb C)\to M_{N_a}(\mathbb C)$, chosen before any state $\rho$, for which each member is unitarily equivariant and $t$-positive, $N_a\to\infty$, and

$$S_m(\Phi_{a+1})\subseteq S_m(\Phi_a),\qquad \bigcap_{a\geq1}S_m(\Phi_a)\subseteq S_m(\phi).$$

Thus the family eventually detects every state detected by $\phi$, and detection persists at later indices. The ancillary dimension $m$ is fixed before the family is chosen. Bardet, Collins, and Sapra, Theorem 5.1

Intermediate targets

The milestone statements cover the infinite dimensional lift of a linear map to $H=L^2(U_n,\mathbb C^N)$, its inclusion $S_m(\Phi)\subseteq S_m(\phi)$, the finite dimensional invariant subspaces supplied by the Peter–Weyl decomposition, and the compression of the lift to such a subspace, which is a unitarily equivariant $t$-positive matrix map $\Psi$ with $S_m(\Phi)\subseteq S_m(\Psi)$. These are the source's Lemma 5.3, Theorem 5.2 for its explicit witness, the consequence of equations (24)–(25) used in §5.2, and the compression step of the proof of Theorem 5.1 on pp. 14–15. The milestone for Theorem 5.2 names the particular fibrewise lift constructed in the paper as its witness and asserts its equivariance, its $t$-positivity and the inclusion of detection sets. Bardet, Collins, and Sapra, §5.1–5.2

Significance

The theorem shows that symmetry alone does not prevent a positive map from detecting the states detected by a specified input map. It turns a single detector into a nested family with growing finite output dimensions, while keeping the same positivity order. The conclusion is pointwise in states but uses one sequence uniformly across all density matrices at the fixed ancillary dimension: each state outside $S_m(\phi)$ is excluded from every sufficiently late $S_m(\Phi_a)$. The result does not assert that any one finite output dimension suffices for every state. Bardet, Collins, and Sapra, Theorem 5.1

The paper proves this mathematical result. This mission records its statements in Lean, leaving proofs of the drafted goal and milestones to formalization work. The finite matrix definitions and the infinite dimensional $L^2$ interface can be reused for other questions about positive maps, regular representations, and finite dimensional compression. The published tensor superoperator and complete positivity definitions are shared with other quantum information developments rather than redefined here.

Difficulty

The immediate detector $\phi$ need not be unitarily equivariant. Replacing it by a single symmetric finite matrix map therefore gives no direct reason to preserve all of its detected states. The source passes through a fibrewise map indexed by every input unitary, so the intermediate output space is infinite dimensional. The remaining difficulty is to return to finite matrix outputs while retaining both equivariance and $t$-positivity, and to choose the outputs so their detection sets are nested. A finite dimensional truncation without invariance under the regular action would not establish the claimed symmetry. Bardet, Collins, and Sapra, §5.1–5.2

Formalization scope

Finite matrices are Matrix (Fin n) (Fin n) ℂ; positive semidefiniteness is Matrix.PosSemidef. The ancillary factor is first in Fin m × Fin n, and the existing QAlgorithms.idTensorSuperop applies the map to the second factor. Complete positivity is the published QAlgorithms.Entanglement.IsCompletelyPositive. The paper's indices $a\geq1$ become Lean natural numbers starting at zero. The density matrix test includes both positivity and trace one. The output dimensions form an actual function tending to infinity, and the maps form a dependent family whose codomain uses that function. The goal keeps the printed “not completely positive” hypothesis and all five stated conclusions. In particular, choosing detectors separately for each state would not meet it.

For the intermediate result, $H$ is a complex $L^2$ space over a Borel measure on $U_n$. The lift is encoded by its sesquilinear form, whose kernel at $U$ is $\phi(U^*XU)$; positivity on $\mathbb C^t\otimes H$ is tested by all block quadratic forms. A finite measure and two $L^2$ vectors make these integrals integrable because the matrix kernel is bounded. The regular action uses left invariance; the detection inclusion uses positivity of nonempty open sets; the Peter–Weyl milestone uses Haar probability measure. These are properties of the paper's Haar measure. The source's standing convention that linear maps preserve adjoints is already implied by $t$-positivity for the goal and is not a separate assumption there. The general linear map in the lift milestones is stated exactly where the source permits it.

The development needs the shared matrix-map definitions, the $L^2$ and measure interfaces, and finite dimensional unitary representation theory. Work on the bounded-operator interpretation of the form, invariant truncations, and compression can be reused beyond this mission. The paper's inconsistent phrase “Schmidt number smaller than $t$” is not encoded, because the target uses only detection sets. Bardet, Collins, and Sapra, pp. 12–15

Selected references

• I. Bardet, B. Collins, and G. Sapra, Characterization of equivariant maps and application to entanglement detection, arXiv preprint, 2019, arXiv:1811.08193v3.

Motivation

Quantum mechanics is usually written in linear-algebraic terms: states are vectors of a complex Hilbert space, observables are Hermitian operators, and expectation values pair the two. Classical mechanics is written geometrically: states form a symplectic manifold, observables are functions on it, and dynamics is a Hamiltonian flow. A line of work starting with Kibble (1979) and continued by Cirelli, Lanzavecchia, Heslot, Ashtekar–Schilling (arXiv:gr-qc/9706069) and Brody–Hughston (arXiv:quant-ph/9906086) recasts quantum mechanics in the classical language: the Hilbert space, seen as a real manifold, carries a Kähler structure (a symplectic form, a Euclidean metric and a compatible complex structure), and observables become real quadratic functions on it.

Cariñena, Clemente-Gallardo and Marmo (arXiv:math-ph/0701053v2) organise this correspondence around one map, the momentum map of the unitary group acting on Hilbert space. The algebra of observables carries two products, a Lie product (the commutator) and a Jordan product (the anticommutator). The paper's Proposition 5 states that the momentum map carries both products, read as tensors on the dual of the unitary Lie algebra, to the symplectic and Euclidean parts of the Kähler structure of Hilbert space. This mission formalizes that statement in finite dimension.

Setting

Fix $n\in\mathbb N$ and let $\mathcal H=\mathbb C^n$, with $\langle\psi|\phi\rangle=\sum_k\overline{\psi_k}\phi_k$. The space of observables $\mathcal O$ is the real vector space of Hermitian $n\times n$ complex matrices. On it the paper defines:

• the isomorphism $\alpha(A)=iA$ onto the Lie algebra $\mathfrak u(n)$ of anti-Hermitian matrices, eq. (2);
• the Lie product $[A,B]_-=\alpha^{-1}(\alpha(A)\alpha(B)-\alpha(B)\alpha(A))=i(AB-BA)$, eq. (3);
• the scalar product $\langle A,B\rangle=\tfrac12\operatorname{Tr}(AB)$, eq. (4);
• the Jordan product $A\circ B=\tfrac12(AB+BA)$, eq. (6).

Through (4), the dual $\mathfrak u^*(n)$ is identified with Hermitian matrices $\xi$. Each observable $A$ gives a linear function $\widehat A(\xi)=\tfrac12\operatorname{Tr}(\xi A)$. On $\mathfrak u^*(n)$ the paper defines the Lie–Poisson tensor (11), $\Lambda(d\widehat A,d\widehat B)(\xi)=\tfrac i2\operatorname{Tr}\,\xi(\alpha(A)\alpha(B)-\alpha(B)\alpha(A))$, and the Jordan tensor (12), $\mathcal R(\xi)(d\widehat A,d\widehat B)=\tfrac12\operatorname{Tr}\,\xi(AB+BA)$.

On the Hilbert space side, use real coordinates $z_k=q_k+ip_k$. Every complex matrix $A$ defines the quadratic function $f_A(\psi)=\tfrac12\langle\psi|A\psi\rangle$. The canonical Poisson bracket is $\{f,g\}=\sum_k(\partial_{q_k}f\,\partial_{p_k}g-\partial_{p_k}f\,\partial_{q_k}g)$, and the contravariant Euclidean structure is $G=\sum_k(\partial_{q_k}\otimes\partial_{q_k}+\partial_{p_k}\otimes\partial_{p_k})$. The momentum map is

$$\mu:\mathbb C^n\to\mathfrak u^*(n),\qquad \mu(\psi)=\rho_\psi=|\psi\rangle\langle\psi| .$$

Formalization targets

Goal: Proposition 5 (p. 12)

For Hermitian $A,B$ and every $\psi\in\mathbb C^n$:

$$\widehat A(\mu(\psi))=f_A(\psi),\qquad \{f_A,f_B\}(\psi)=\Lambda(d\widehat A,d\widehat B)(\mu(\psi)),\qquad G(df_A,df_B)(\psi)=\mathcal R(\mu(\psi))(d\widehat A,d\widehat B).$$

In the paper's notation: $\mu^*(\widehat A)=f_A$, $\mu^*(\{\widehat A,\widehat B\})=\{f_A,f_B\}$ and $\mu^*(\mathcal R(d\widehat A,d\widehat B))=G(\mu^*(d\widehat A),\mu^*(d\widehat B))$.

Milestones

In attack order:

1. Lemma 5 (p. 12): $f_A$ is real-valued for all $\psi$ if and only if $A$ is Hermitian.
2. Lemma 1 (p. 4), in two parts:
   • $[\cdot,\cdot]_-$ makes $\mathcal O$ a real Lie algebra, isomorphic to $\mathfrak u(n)$ through $\alpha$;
   • $\tfrac12\operatorname{Tr}(AB)$ is a real, symmetric, positive definite scalar product, invariant under $A\mapsto UAU^\dagger$.
3. Lemma 2 (p. 5): $(\mathcal O,\circ)$ is a Jordan algebra.
4. Proposition 1 (p. 5): the scalar product is invariant for both products (7), and $\mathrm{ad}_-$ is a derivation of $\circ$ (8).
5. Lemma 3 (p. 5): $\mathcal O$ is a Jordan–Lie algebra. This means the Lie and Jordan algebra axioms hold, (8) holds together with the associator identity (9), $(A\circ B)\circ C-A\circ(B\circ C)=\tfrac14\hbar[[A,C]_-,B]_-$, here with $\hbar=1$.
6. Equivariance (§3.1.1, p. 11): $\mu$ takes values in $\mathfrak u^*(n)$ and $\mu(U\psi)=U\mu(\psi)U^\dagger$ for unitary $U$.

Significance

Proposition 5 says that the algebra of observables can be read off Hilbert space geometrically:

• commutators of observables become Poisson brackets of their expectation-value functions;
• anticommutators become the metric pairing of their gradients.

This is the dictionary behind geometric treatments of the Schrödinger equation as a Hamiltonian flow. It also underlies variance and uncertainty relations written through the metric, and the reduction to projective space and density states that the paper discusses in §§2.5 and 4. The paper presents it as an alternative to the GNS construction for pure states.

The paper's proof is "Direct verification", and Lemmas 1–3 and Proposition 1 are classical facts about Hermitian matrices. No step is open. What the mission adds is a machine-checked version with every normalisation pinned, as listed in Formalization scope:

• the factors ½ in (4), (6) and $f_A$;
• the factor $i/2$ in (11);
• $\hbar=1$ in (9).

The paper uses both the Hermitian picture (3), (4), (6) and the anti-Hermitian picture (5), (11). The formal statement fixes the signs and factors needed to read their relation precisely. The prior-art search for this mission found no published Prove2Me statement with the same finite-dimensional objects and conclusion.

Difficulty

The algebraic milestones are short computations once the definitions are unfolded. The work concentrates in the goal, whose two sides live in different worlds.

The left side is built from real partial derivatives of real-valued functions on $\mathbb C^n$, viewed as $\mathbb R^{2n}$. Its derivatives must be computed in the directions $e_k$ and $ie_k$ and then recombined into complex inner products.

The right side is a trace of a product of matrices with the rank-one matrix $|\psi\rangle\langle\psi|$.

The difficulty is that the derivative formulas use real coordinates while the tensor formulas use complex matrix products and traces. Their normalizations and sign conventions must agree at the level of the full identity, including the $i$ in $\alpha(A)$ and the factors of $\tfrac12$ in the quadratic functions.

Replacing the derivative-defined brackets by their closed forms would make the goal trivial and is not permitted, see below.

Formalization scope

All objects are defined in one definitions module in the namespace GeomQM.MomentumMap, over Mathlib's Matrix (Fin n) (Fin n) ℂ and vectors Fin n → ℂ.

Committed conventions.

• Observables carry an explicit IsHermitian hypothesis. Lemma 5 is about an arbitrary complex matrix, and equivariance needs no hypothesis. $n=0$ is allowed, since every statement then holds trivially, as in the paper.
• $\partial/\partial q_k$ and $\partial/\partial p_k$ are fderiv ℝ applied to Pi.single k 1 and Pi.single k I. This is the paper's $z_k=q_k+ip_k$.
• $f_A$ is defined as the complex number $\tfrac12\langle\psi|A\psi\rangle$, and the real function used in the goal is its real part. Lemma 5 is stated on the complex value, so that it is not vacuous.
• $\mathfrak u^*(n)$ is the space of Hermitian matrices. $\widehat A$ uses the pairing (4), $\tfrac12\operatorname{Tr}(\xi A)$, not the pairing (5), which differs by a factor $i$ on $\alpha(A)$ and would change the sign.
• $\Lambda$ is (11) applied literally to $\alpha(A),\alpha(B)$. The shortcut $\widehat{[A,B]_-}$ has the opposite sign.
• $\mathcal R$ is the right-most expression of (12).
• The real-valued tensors take the real part of trace expressions that are real for Hermitian arguments.
• The second bracket $\{f_1,f_2\}_+$ displayed on p. 12 is not used, because Proposition 5 names $G$.

Ruled out. The brackets on $\mathbb C^n$ are defined through real derivatives of arbitrary functions, never as $f_{-i[A,B]}$ or $f_{AB+BA}$. The tensors on $\mathfrak u^*(n)$ are trace formulas, never rewritten as quadratic functions of $\psi$. Either shortcut would make bullets 2 and 3 hold by definition.

Not in scope. The following are not formalized:

• Propositions 2–4: the Poisson structure on all of $\mathcal O^*$, Lie derivatives of $\mathcal R$, and generalized distributions;
• Lemma 4: linear dynamics preserving both products;
• the Rayleigh-quotient statements of §3.4;
• the projective-space material of §4.

Welcome contributions. Proofs of the milestones and of the goal, and general lemmas that would be reusable beyond this mission:

• derivative formulas for real quadratic forms on Fin n → ℂ;
• the identity $\operatorname{Tr}(|\psi\rangle\langle\psi|M)=\langle\psi|M\psi\rangle$.

Selected references

• J. F. Cariñena, J. Clemente-Gallardo, G. Marmo, Geometrization of Quantum Mechanics, arXiv preprint, 2007 (v2). https://arxiv.org/abs/math-ph/0701053v2
• T. W. B. Kibble, Geometrization of quantum mechanics, Communications in Mathematical Physics 65, 189–201, 1979. https://doi.org/10.1007/BF01225149
• A. Ashtekar, T. A. Schilling, Geometrical formulation of quantum mechanics, in On Einstein's Path, Springer, 1998. https://arxiv.org/abs/gr-qc/9706069
• D. C. Brody, L. P. Hughston, Geometric quantum mechanics, Journal of Geometry and Physics 38, 19–53, 2001. https://arxiv.org/abs/quant-ph/9906086
• J. Grabowski, M. Kuś, G. Marmo, Geometry of quantum systems: density states and entanglement, Journal of Physics A 38, 10217–10244, 2005. https://arxiv.org/abs/math-ph/0507045
• N. P. Landsman, Mathematical Topics Between Classical and Quantum Mechanics, Springer Monographs in Mathematics, 1998. https://doi.org/10.1007/978-1-4612-1680-3

Motivation

Integrable spin chains with a Lie superalgebra symmetry $\mathfrak{gl}(M|N)$ are lattice regularizations of two-dimensional field theories with target-space supersymmetry, such as the $\mathfrak{gl}(M|N)$ Gross–Neveu models and sigma models on superspaces, which appear in the study of disordered systems, polymers and the AdS/CFT correspondence. Their spectra are described by the nested Bethe ansatz: each eigenvalue of the transfer matrix corresponds to a family of complex numbers, the Bethe roots, solving a system of algebraic equations, the Bethe ansatz equations (BAE). The nested algebraic Bethe ansatz for general closed $\mathfrak{gl}(M|N)$ chains was carried out by Belliard and Ragoucy (arXiv:0804.2822).

C. Candu, Continuum Limit of gl(M|N) Spin Chains (arXiv:1012.0050), studies the antiferromagnetic chain $(V\otimes V^*)^{\otimes L}$ of alternating fundamental and dual representations. Its §4 shows that a class of solutions of the $\mathfrak{gl}(M|N)$ BAE is fully characterized by solutions of the $\mathfrak{gl}(M-1|N-1)$ BAE, which embeds the $\mathfrak{gl}(M-1|N-1)$ spectrum into the $\mathfrak{gl}(M|N)$ spectrum. This is the algebraic counterpart of cohomological reduction (Candu–Creutzig–Mitev–Schomerus, arXiv:1001.1344), in which the $\mathfrak{gl}(M-1|N-1)$ chain is the cohomology of an odd nilpotent element acting on the $\mathfrak{gl}(M|N)$ chain. The paper uses this relation to compare all $\mathfrak{gl}(n+N|N)$ chains with $n$ fixed, and concludes that their continuum limits share the $\mathfrak{gl}(n)$ Gross–Neveu-like particle content.

This mission formalizes that restriction and lift of Bethe ansatz equations.

Setting

Let $d = M+N$ and $r = d-1$. A grading assigns to each position $i\in\{1,\dots,d\}$ a parity $|i|\in\{0,1\}$ and a sign $\sigma_i = (-1)^{|i|}$; $M$ counts the even and $N$ the odd positions. The loop weight is $n=\sum_{i=1}^d\sigma_i = M-N$. The simple roots are $\alpha_k = \epsilon_k-\epsilon_{k+1}$, $k=1,\dots,r$; $\alpha_k$ is odd when $\sigma_k\sigma_{k+1}=-1$.

For a chain of length $L$ the source terms are

$$\Lambda_1(u)=(u+\sigma_1)^L(u+\tfrac n2)^L,\qquad \Lambda_i(u)=u^L(u+\tfrac n2)^L\ (2\le i\le r),\qquad \Lambda_d(u)=u^L(u+\tfrac n2-\sigma_d)^L .$$

For each type $k=1,\dots,r$ let $\{u^{(k)}_j\}_{j=1}^{\nu^{(k)}}$ be a finite set of pairwise distinct complex numbers and $Q_k(u)=\prod_j(u-u^{(k)}_j)$, with $Q_0=Q_d=1$. The BAE (2.9) state that for every $k$ and every root $u=u^{(k)}_j$,

$$\frac{\Lambda_k(u)}{\Lambda_{k+1}(u)}=-\sigma_k\sigma_{k+1}\,\frac{Q_{k-1}(u)\,Q_k(u+\sigma_{k+1})\,Q_{k+1}(u-\sigma_{k+1})}{Q_{k-1}(u+\sigma_k)\,Q_k(u-\sigma_k)\,Q_{k+1}(u)} .$$

With $x^{(k)}_j = i\,u^{(k)}_j+\tfrac i2\sum_{l\le k}\sigma_l$ (2.11), the energy (2.18) of a solution is

$$E=-\sum_{j}\frac{\sigma_1}{(x^{(1)}_j)^2+1/4}-\sum_{j}\frac{\sigma_d}{(x^{(r)}_j)^2+1/4} .$$

The paper works throughout under $n = M-N>0$.

Fix $k$ with A1 ($\alpha_k$ odd) and A2 ($\alpha_k$ has no source term, $k\neq 1,r$). R1 identifies the roots of types $k-1$ and $k+1$. The reduced system deletes grading positions $k,k+1$ and root types $k,k+1$: it is the BAE of a $\mathfrak{gl}(M-1|N-1)$ chain with simple roots $\{\alpha_1,\dots,\alpha_{k-2},\epsilon_{k-1}-\epsilon_{k+2},\alpha_{k+2},\dots,\alpha_r\}$.

Formalization targets

Goal: restriction and lift (§4.1–4.2)

Under A1, A2, R1 and non-degeneracy of the roots,

$$\text{BAE}_{\mathfrak{gl}(M|N)}(\{u^{(l)}\}_{l=1}^r)\iff \text{BAE}_{\mathfrak{gl}(M-1|N-1)}(\{u^{(l)}\}_{l\neq k,k+1})\ \wedge\ (2.9)_{k-1}\text{ at the roots of type }k-1,$$

and $E_{\mathfrak{gl}(M|N)} = E_{\mathfrak{gl}(M-1|N-1)}$. The forward direction is the restriction R1–R2; the backward direction is the reduction of the lift to "a solution … to either eq. (4.2) or eq. (4.4)".

Milestones

1. Under A1–A2 the equations of types $k-1$, $k$, $k+1$ take the printed forms (4.2), (4.3), (4.4) (p. 17).
2. Under R1, (4.3) holds automatically (p. 18).
3. R2: (4.2) and (4.4) at a common root give (4.6), in which the type-$k$ roots no longer appear (p. 18).
4. The restricted equations are exactly the $\mathfrak{gl}(M-1|N-1)$ BAE for the reduced simple root system, with the same loop weight $n$ (p. 18).
5. Given a reduced solution and R1, (4.2) and (4.4) are equivalent (p. 19).

Significance

The restriction gives an explicit map from $\mathfrak{gl}(M-1|N-1)$ Bethe solutions to $\mathfrak{gl}(M|N)$ Bethe solutions that preserves the energy. Iterated, it relates every $\mathfrak{gl}(n+N|N)$ chain to the $\mathfrak{gl}(n)$ chain, which is how the paper identifies the vacuum and the massive excitations of the $\mathfrak{gl}(n+N|N)$ chains in the continuum limit (§5–§6). It is also a concrete, equation-level check of cohomological reduction.

The result is proved in the paper by direct algebra. The result is not formalized anywhere on Prove2Me, which has no Bethe ansatz equations of any kind. This mission produces a precise statement of the nested BAE with their grading-dependent signs, shifts and boundary conventions, and a verified version of the restriction, including the bookkeeping that the paper leaves implicit: the reindexing of types, the change of the source terms of the reduced chain, and the invariance of the energy.

Difficulty

Each step is elementary algebra; the difficulty is bookkeeping. The sign $-\sigma_k\sigma_{k+1}$, the shifts $\pm\sigma_k$, $\pm\sigma_{k+1}$ and the boundary cases $Q_0=Q_d=1$ differ between the original and the reduced system: after deletion, the neighbour of type $k+2$ is type $k-1$, and the last source term $\Lambda_d$ and the partial sums $\sum_{l\le k}\sigma_l$ in (2.11) are those of a different grading. A naive argument that matches equations by position, or that treats the reduced system with the original source terms, misses these shifts. The backward direction needs non-degeneracy, because recovering (4.4) from (4.6) and (4.2) requires dividing by the two sides of (4.2).

Formalization scope

Everything is in the namespace SuperBAE.Restriction and works over $\mathbb{C}$. Positions $1,\dots,d$ and types $1,\dots,d-1$ are natural numbers, and a grading is a Boolean function (true = odd), with $\sigma_i\in\{\pm1\}$. Root sets are Finset ℂ, which encodes the paper's requirement that no two roots of the same type coincide. $Q_k$ equals $1$ outside $1\le k\le d-1$. Only the homogeneous chain is modelled. The BAE are in division form, so every theorem carries a regularity hypothesis: at each root $u$ of type $k$, the values $\Lambda_k(u)$, $\Lambda_{k+1}(u)$, $Q_{k-1}(u+\sigma_k)$, $Q_k(u-\sigma_k)$ and $Q_{k+1}(u)$ are nonzero. This is the non-degeneracy the division form presupposes; it is imposed on the original system only. The standing assumption $n>0$ is kept as $N<M$, although the algebra of §4 does not use it. A1 is the Boolean condition $|k|\neq|k+1|$, and A2 is $2\le k$, $k+2\le d$.

The reduced system is the same BAE predicate applied to the deleted grading on $d-2$ positions and the reindexed roots, with its own source terms and its own loop weight. A formalization that writes the reduced equations by hand, or passes $n$ to the reduced chain as a parameter, is trivializing and is ruled out. Without the regularity hypothesis, Lean's convention $x/0=0$ would make degenerate configurations satisfy (2.9) vacuously; regularity excludes this, and a verification file checks that the hypotheses of the goal are jointly satisfiable and that regularity is not vacuous.

Out of scope: the Yang–Baxter and Yangian structure, the walled Brauer algebra, the weight constraints (4.1) and (4.8), existence and uniqueness of lifted type-$k$ roots, inhomogeneous chains, the boundary case $k=1,r$ of §4.3, and the thermodynamic limit. Proofs of the milestones are welcome, as are lemmas that put the finite-product manipulations of $Q$-polynomials into a reusable form.

Selected references

• C. Candu, Continuum Limit of gl(M|N) Spin Chains, arXiv preprint (v1, 2010), JHEP 2011. https://arxiv.org/abs/1012.0050
• S. Belliard and E. Ragoucy, Nested Bethe ansatz for 'all' closed spin chains, J. Phys. A 41, 295202 (2008). https://arxiv.org/abs/0804.2822
• C. Candu, T. Creutzig, V. Mitev and V. Schomerus, Cohomological Reduction of Sigma Models, JHEP 05, 047 (2010). https://arxiv.org/abs/1001.1344
• F. H. L. Eßler, H. Frahm and H. Saleur, Continuum Limit of the Integrable sl(2|1) 3–3̄ Superspin Chain, Nucl. Phys. B 712, 513 (2005). https://arxiv.org/abs/cond-mat/0501197
• E. Ogievetsky and P. Wiegmann, Factorized S-Matrix and the Bethe Ansatz for Simple Lie Groups, Phys. Lett. B 168, 360 (1986).

Motivation

Measuring a quantum system disturbs it. The information–disturbance tradeoff asks how little a measurement that yields a given amount of information about an unknown state must change that state. The question underlies the security analysis of quantum key distribution, where an eavesdropper's information gain is paid for in detectable disturbance, and the design of measurements that must leave a system usable afterwards, as in sequential or weak measurement schemes.

A measurement has two separate parts: the POVM, which fixes the outcome statistics, and the instrument, which fixes the post-measurement state for each outcome. Many instruments realize the same POVM. The natural candidate for the least disturbing one is the square-root (Lüders) dynamics, which maps a state $\rho$ to $F_b^{1/2}\rho F_b^{1/2}$ on outcome $b$. Whether this candidate is in fact optimal depends on how disturbance is averaged. H. Barnum (2002) showed that it is optimal when the average is over the uniform ensemble of pure states, and computed the resulting minimal disturbance for every POVM (arXiv:quant-ph/0205155). For general ensembles the same paper leaves optimality open (its "Possibility 4").

Setting

Fix a dimension $d\ge1$ and the Hilbert space $\mathbb C^d$ with standard basis $\{|i\rangle\}$.

• A POVM is a finite family $\{F_b\}_{b\in B}$ of positive semidefinite operators with $\sum_bF_b=I$. Outcome $b$ occurs on state $\rho$ with probability $\operatorname{tr}\rho F_b$.
• An instrument compatible with $\{F_b\}$ is a finite family of operators $\{A_{bi}\}$ (Hellwig–Kraus, or HK, operators) with

$$\sum_iA_{bi}^\dagger A_{bi}=F_b\quad\text{for every }b .$$

The unnormalized post-measurement state on outcome $b$ is $\mathcal A_b(\rho)=\sum_iA_{bi}\rho A_{bi}^\dagger$, and the overall operation is $\mathcal A(\rho)=\sum_{b,i}A_{bi}\rho A_{bi}^\dagger$.

• The square-root operation of the POVM is $\mathcal S(\rho)=\sum_bF_b^{1/2}\rho F_b^{1/2}$, the instrument with the single HK operator $F_b^{1/2}$ per outcome. An instrument with one HK operator per outcome has one-term conditional dynamics.
• The uniform ensemble $\Omega$ is the unitarily invariant probability measure on unit vectors of $\mathbb C^d$, the law of $U|0\rangle$ for a Haar-random unitary $U$.
• For a pure state the fidelity with an operator $\sigma$ is $\langle\psi|\sigma|\psi\rangle$. The average fidelity of an operation $\mathcal E$ is $\overline F(\mathcal E)=\int d\Omega_\psi\,\langle\psi|\mathcal E(|\psi\rangle\langle\psi|)|\psi\rangle$, and its average disturbance is

$$D(\mathcal E)=1-\overline F(\mathcal E)=1-\int d\Omega_\psi\sum_{b,i}|\langle\psi|A_{bi}|\psi\rangle|^2\qquad(\mathcal E=\mathcal A).$$

• The second moment of the ensemble is $\Pi=\int d\Omega_\psi\,|\psi\rangle\langle\psi|\otimes|\psi\rangle\langle\psi|$.

Formalization targets

The goal and the numbered milestones below are from Barnum, pp. 9–13, arXiv:quant-ph/0205155v1.

Goal: Theorem 5

For every POVM $\{F_b\}$ and every finite instrument $\{A_{bi}\}$ compatible with it,

$$D(\mathcal S)\;\le\;D(\mathcal A).$$

The instrument may have several HK operators per outcome; this is what distinguishes Theorem 5 from Theorem 8.

Milestones

1. Eq. (31) (Jones): for unit vectors $a,b$, $\int d\Omega_\psi|\langle\psi|a\rangle|^2|\langle\psi|b\rangle|^2=\dfrac{1+|\langle a|b\rangle|^2}{d(d+1)}$.
2. Lemma 9: $\Pi=\dfrac{1}{d(d+1)}\sum_{i,j}\big(|i\rangle\langle i|\otimes|j\rangle\langle j|+|i\rangle\langle j|\otimes|j\rangle\langle i|\big)$.
3. Eq. (32): $\int d\Omega_\psi\langle\psi|A|\psi\rangle\langle\psi|B|\psi\rangle=\operatorname{tr}\Pi(A\otimes B)=\frac{1}{d(d+1)}\sum_{ij}\big(\langle i|A|i\rangle\langle j|B|j\rangle+\langle i|A|j\rangle\langle j|B|i\rangle\big)$.
4. Eq. (33): $\overline F\big(\rho\mapsto\sum_kA_k\rho A_k^\dagger\big)=\frac{1}{d(d+1)}\sum_k\big(|\operatorname{tr}A_k|^2+\operatorname{tr}A_kA_k^\dagger\big)$.
5. Trace bound (p. 13, cited from von Neumann): for $A\ge0$, $\max_{V\text{ unitary}}|\operatorname{tr}VA|$ is attained where $VA=\sqrt{A^\dagger A}$.
6. Theorem 8: for one-term instruments, $\sum_b\overline F_b\le\frac{1}{d(d+1)}\big(d+\sum_b(\operatorname{tr}F_b^{1/2})^2\big)$, with equality for the square-root dynamics.
7. Theorem 7 (Ando): $(A,B)\mapsto A^t\otimes B^{1-t}$ is jointly concave for $0\le t\le1$.
8. Proposition 6: $\langle\psi|P_1|\psi\rangle^2+\langle\psi|P_2|\psi\rangle^2\le\langle\psi|\sqrt{P_1^2+P_2^2}|\psi\rangle^2$ for positive $P_1,P_2$.
9. Coarse-graining (p. 10): $\sum_j\langle\psi|P_j|\psi\rangle^2\le\langle\psi|\sqrt{\sum_jP_j^2}|\psi\rangle^2$.

Significance

Theorem 5 together with Theorem 8 gives a closed form for the minimal disturbance on the uniform ensemble of every POVM: $\overline D_{\min}=1-\frac{1}{d(d+1)}\big(d+\sum_b(\operatorname{tr}F_b^{1/2})^2\big)$ (Eqs. (34)–(35)). For rank-one POVMs this is $(d-1)/(d+1)$, one endpoint of the information–disturbance frontier that the rest of the paper studies. The result also shows that on this ensemble, extra Kraus operators per outcome never reduce disturbance, so the frontier may be computed over square-root instruments alone.

The milestones are of independent use. Lemma 9 and Eq. (32) are the standard second-moment formula for Haar-random pure states (the 2-design property). Eq. (33) is the Kraus-operator form of the average fidelity that appears throughout quantum channel benchmarking. Ando's concavity theorem is equivalent to Lieb's concavity theorem.

The results are proved in the paper (2002). This mission formalizes them; to the extent known, none of the paper's statements has a machine-checked proof. The platform already has the uniform ensemble and the average fidelity as published definitions, and Nielsen's formula relating average and entanglement fidelity, which is a different statement.

Difficulty

The polar-decomposition step suggests a pointwise argument: write $A_{bi}=U_{bi}P_{bi}$ and replace $U_{bi}$ by $I$. That fails. For a fixed $\psi$, $|\langle\psi|UP|\psi\rangle|^2$ can exceed $\langle\psi|P|\psi\rangle^2$ (take $d=2$, $P=|0\rangle\langle0|$, $\psi=(|0\rangle+|1\rangle)/\sqrt2$, $U|0\rangle=\psi$). The replacement is valid only after averaging over $\Omega$, through the explicit fourth-moment computation of Lemma 9. The second obstacle is merging several HK operators of one outcome into one, which needs Proposition 6. Proposition 6 is an inequality between non-commuting operators. The commuting case is elementary, but the general case rests on Ando's joint concavity, an operator-concavity theorem of Lieb's type that is not in Mathlib.

Formalization scope

Operators are Matrix (Fin d) (Fin d) ℂ and vectors EuclideanSpace ℂ (Fin d), with 0 < d. The uniform ensemble is the published QAlgorithms.QuditFidelity.haarPureStateLaw d hd, the image of normalized Haar measure on the unitary group under $U\mapsto U|0\rangle$. The average fidelity is the published averageFidelity d hd, whose integrand is $\operatorname{Re}\operatorname{tr}\big(|\psi\rangle\langle\psi|\,\mathcal E(|\psi\rangle\langle\psi|)\big)$. Disturbance is 1 - averageFidelity. POVMs are QAlgorithms.IsPOVM on a finite outcome type. An instrument is A : B → I → Matrix with one finite Kraus index type I for every outcome. Outcomes with fewer operators are padded with zeros, which changes neither the compatibility condition nor the operation. The square root is cfc Real.sqrt. Real powers in Theorem 7 use cfc of Real.rpow, so $X^0=I$. Real-valued quadratic forms and traces of positive operators are taken as real parts. $\Pi$ is defined entrywise.

The goal must not be read with I = Unit. That would be Theorem 8's one-term case, and the goal quantifies over every finite I. The ensemble is the Haar image itself, not a measure assumed to have the second moment of Lemma 9.

The wrapper disturbance accepts a raw superoperator, for which an integral need not exist. Every theorem here applies it only to a finite Kraus map, whose integrand is continuous and integrable on the Haar ensemble. A complete development needs Haar moment integrals on the unitary group (reusable for any unitary-design argument), the polar decomposition and the trace inequality for matrices, and an operator-concavity theorem (Ando/Lieb). Contributions of any of these, or of the commuting-case proof of Proposition 6 as a stepping stone, are welcome.

Selected references

• H. Barnum, Information-disturbance tradeoff in quantum measurement on the uniform ensemble, preprint, 2002. arXiv:quant-ph/0205155
• T. Ando, Concavity of certain maps on positive definite matrices and applications to Hadamard products, Linear Algebra Appl. 26 (1979) 203–241. doi:10.1016/0024-3795(79)90179-4
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. doi:10.1016/0001-8708(73)90011-X
• M. A. Nielsen, A simple formula for the average gate fidelity of a quantum dynamical operation, Phys. Lett. A 303 (2002) 249–252. arXiv:quant-ph/0205035