All missions

Motivation

A Gittins index assigns a number to an uncertain arm in a discounted bandit problem. The index converts a sequential choice, where an agent may keep gathering information or retire, into a tax threshold for playing the arm. Computing it generally requires an optimal stopping calculation. A Bayesian upper confidence bound, by comparison, is a quantile of the posterior distribution and is directly available for a Gaussian posterior. Russo's note asks how closely these two quantities agree when the agent is patient and the discount factor approaches one. The answer is an asymptotic identity for a Gaussian arm, not a finite-discount formula. Russo, 2019, pp. 1–3.

The note places its result alongside work on computational approximations of Gittins indices and finite-horizon index policies, but aims at the conceptual relationship with Bayesian confidence bounds. It appeared as an arXiv preprint in 2019; this mission follows that version's theorem numbering and formulas. A later journal publication appeared in Operations Research in 2021, but its numbering is not used here.

Setting

One arm has an unknown quality $\theta$. The prior distribution is Gaussian, $\theta\sim N(\mu,\sigma^2)$, where $\mu\in\mathbb R$ and $\sigma^2>0$. Playing the arm at time $t$ yields $R_t=\theta+W_t$, where the observation noises $W_t$ are independent Gaussian variables of mean zero and variance $\sigma_W^2>0$. After observing $R_0,\ldots,R_{t-1}$, the posterior is $N(\mu_t,\sigma_t^2)$. Its mean and variance follow the Gaussian update (1) of Russo, p. 2. In particular, $\sigma_t^2=(1/\sigma^2+t/\sigma_W^2)^{-1}$.

For each play, the agent pays a tax $\lambda\in\mathbb R$. The agent may retire, receiving zero thereafter. At discount factor $0<\gamma<1$, an admissible retirement time $\tau\ge1$ uses only the rewards observed through the current time. Its discounted payoff includes the play at $\tau$: $\sum_{t=0}^{\tau}\gamma^t(\theta-\lambda)$. The value $V^\lambda_\gamma(\mu,\sigma^2;\sigma_W^2)$ is the supremum of the expected payoff over these retirement times. The Gittins index $\lambda_\gamma(\mu,\sigma^2;\sigma_W^2)$ is the supremum of taxes for which the value is nonnegative. These are the stopping-time value and fair-tax definition in equations (2)–(3) of Russo, p. 2.

Write $\Phi$ and $\phi$ for the distribution function and density of $N(0,1)$, and $\Phi^{-1}(\gamma)=\inf\{z:\Phi(z)\ge\gamma\}$. Thus $\mu+\sigma\Phi^{-1}(\gamma)$ is the prior's upper $\gamma$-quantile, with $\sigma=\sqrt{\sigma^2}$.

Formalization targets

Gaussian Gittins index asymptotic

The goal is Theorem 1, p. 3, for each fixed prior mean, positive prior variance, and positive observation-noise variance:

$$\lambda_\gamma(\mu,\sigma^2;\sigma_W^2) =\mu+\sigma\Phi^{-1}(\gamma)+o(1) \qquad(\gamma\uparrow1).$$

The remainder is an additive quantity tending to zero; the claim does not assert equality at any fixed discount factor. The paper reduces the general prior to a standardized one. Its intermediate targets are the normal-quantile asymptotic, explicit bounds on $\mathbb E[(X-\lambda)^+]$, an upper bound obtained from noiseless information, and a matching lower bound from an admissible exploration policy. They appear as the mission's milestones, along with the posterior identities the lower bound uses. Russo, pp. 3–6.

Significance

The theorem identifies the limiting tax threshold with a familiar statistical quantile. It explains why a Bayesian upper confidence bound can approximate the Gittins priority of an arm when the effective horizon is large. It does not state that a quantile policy is exactly optimal at a fixed horizon or discount factor, and the paper's limitations section notes that significant observation noise relative to the horizon can make exploration costly. Russo, pp. 3, 7.

For a formal development, the reusable pieces are a Gaussian stopping-time model, the fair-tax index, the normal tail and positive-part estimates, and posterior update identities. The asymptotic theorem is proved in the source paper but has no machine-checked proof in this mission. Its local Lean statement is a target with sorry; the same applies to the milestone theorems. The definitions and a small sanity lemma compile in the pinned environment. Contributions that establish the source's stated bounds, their probabilistic prerequisites, or the final asymptotic reduction are relevant.

Difficulty

The direct idea of replacing the index by a posterior quantile at each fixed $\gamma$ does not establish the theorem. The index optimizes over retirement times that adapt to noisy observations. A decision maker who sees $\theta$ without noise has a larger value, so the resulting expression supplies an upper bound, but it does not give a lower bound for the original information structure. The paper's matching lower estimate uses an actual reward-adapted policy and tracks both the cost of initial sampling and the benefit of later commitment. The two estimates must agree to an additive $o(1)$, not merely at their leading order. Russo, §§3.3–3.4, pp. 4–7.

Formalization scope

Lean uses the canonical probability space $\Omega=\mathbb R\times(\mathbb N\to\mathbb R)$: the first coordinate is $\theta$, and the second is the independent noise sequence. The model measure is the Gaussian prior times an infinite product of Gaussian noise laws. The reward history at time $t$ generates $\mathcal F_t=\sigma(R_0,\ldots,R_t)$. An admissible $\mathbb N_\infty$-valued stopping time has $\tau\ge1$; $\tau=\infty$ means never retire. The stopped reward is a countable sum. The index is the supremum of the nonnegative-value tax set. Only the discount domain $0<\gamma<1$ is used in fixed-discount statements; limits approach one from below. Variances are nonnegative reals at the Mathlib Gaussian interface, with strict positivity assumed in the theorem statements. The paper suppresses $\sigma_W^2$ in the index notation; Lean keeps it explicit and arbitrary.

The value is defined from the stopping problem and the index from the fair-tax set. Retirement decisions depend on observed rewards only; giving them access to $\theta$ would change the target. The posterior variance uses $t/\sigma_W^2$ in its closed form, correcting a printed error in (1). Lemma 3's limit is $\gamma\uparrow1$, and Lemma 7 uses $\log(1/(1-\gamma))$ in its little-o scale; their printed versions are inconsistent with the surrounding derivations. The natural-language item notes identify these corrections. Russo, pp. 2, 4, 6, 9.

Selected references

• Daniel Russo, A Note on the Equivalence of Upper Confidence Bounds and Gittins Indices for Patient Agents, arXiv:1904.04732v1, 2019. Preprint.
• J. C. Gittins, K. D. Glazebrook, and R. Weber, Multi-Armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. DOI.

Motivation

Measurements of long quantum spin chains can have outcomes far from their typical values. A large-deviation principle quantifies how quickly the probability of such outcomes decreases with the number of sites. In a classical lattice system this is a standard way to describe rare macroscopic fluctuations; in a quantum chain, observables on overlapping sets of sites generally fail to commute, which makes the corresponding probability laws harder to analyze. Ogata's 2008 paper establishes a full principle for the energy density of any translation-invariant finite-range interaction in a $C^*$-finitely correlated state. Its introduction explains that earlier spin-chain results covered upper bounds or more restricted observables and states, while the lower bound for general observables remained the substantial issue. Ogata, pp. 2–4

The finitely correlated class includes local states generated from finite auxiliary memory. It is large enough to include mixtures and periodic behavior, so a theorem restricted to a primitive transfer map would miss part of Ogata's statement. This mission targets the printed Theorem 1.2 in its full scope. Ogata, p. 4

Setting

At each site let $M_d(\mathbb C)$ be the algebra of complex $d\times d$ matrices. On sites $1,\ldots,n$, the local algebra is the $n$-fold tensor product, represented as matrices whose rows and columns are spin configurations. A finite-range translation-invariant interaction $\Phi$ assigns a Hermitian operator $\Phi(X)$ to each finite set of sites $X\subset\mathbb Z$, with the same term on translated sets and with $\Phi(X)=0$ when the diameter of $X$ exceeds a fixed range. Its finite-volume Hamiltonian is

$$H_\Phi([1,n])=\sum_{X\subseteq[1,n]}\Phi(X).$$

The sum includes the scalar term associated with the empty set. The interaction need not be nearest-neighbor and may have a term on any finite pattern within its range. Ogata, pp. 2–3

A $C^*$-finitely correlated state is specified by a finite-dimensional auxiliary algebra $\mathcal B$, a unital completely positive map $\mathcal E:M_d(\mathbb C)\otimes\mathcal B\to\mathcal B$, and a faithful stationary state $\rho$ on $\mathcal B$. Iterating $\mathcal E$ gives a compatible local state $\omega_n$ on $n$ sites. The probability measure $\mu_{n,\Phi}$ is the spectral distribution of $H_\Phi([1,n])/n$ in $\omega_n$: for a Borel set $B\subseteq\mathbb R$, it assigns the state weight of the spectral projection corresponding to $B$. These local restrictions determine the distributions used in the theorem. Ogata, pp. 3–4

Formalization targets

Full large-deviation principle

The goal is a good rate function $I:\mathbb R\to[0,\infty]$: $I$ is lower semicontinuous and each set $\{x:I(x)\le a\}$ is compact for finite $a\ge0$. For every closed $C$ and open $O$ in $\mathbb R$, Theorem 1.2 asserts

$$\limsup_{n\to\infty}\frac1n\log\mu_{n,\Phi}(C)\le-\inf_{x\in C}I(x),$$ $$\liminf_{n\to\infty}\frac1n\log\mu_{n,\Phi}(O)\ge-\inf_{x\in O}I(x).$$

One rate function serves both inequalities and every eligible set. The statement asserts existence, without imposing a formula for $I$ or a primitivity condition on the auxiliary map. Ogata, pp. 3–4

Supporting targets

The milestone list includes the paper's Gärtner–Ellis theorem, the spectral-law exponential-moment identity behind equation (1), the two-sided order estimate (15) for a gapped auxiliary map, the regrouping of $l$ consecutive sites into one site, under which the same state is generated by the $l$-th iterate $\mathcal E^{(l)}$ of the transfer map and $\widehat{\mathcal E^{(l)}}_1=(\widehat{\mathcal E}_1)^l$, and the differentiable limiting pressure under condition (14). In the last target, the pressure is the limit of $n^{-1}\log\omega_n(e^{\alpha H_\Phi([1,n])})$ for every real $\alpha$. These are narrower claims with separate hypotheses; none replaces the full goal. Ogata, pp. 4–5, 12–15

Significance

The theorem gives an exponential-scale description of the energy-density distribution for all translation-invariant finite-range interactions in this state class. The upper bound controls probability on closed sets; the lower bound supplies the matching guarantee for open sets. Compact sublevel sets prevent low-rate mass from escaping to infinity. The result is already proved in Ogata's paper; the remaining work here is a machine-checked development of the statement and its supporting mathematics. Ogata, Theorem 1.2

Formalizing the finite-dimensional transfer construction, its spectral measures, and an extended-valued LDP vocabulary would also make these objects available for later spin-chain results. The goal itself is not currently accompanied by a machine-checked proof in this mission. The Gärtner–Ellis and auxiliary-map statements are likewise proof targets, not asserted as solved Lean facts.

Difficulty

The exponential of a sum of overlapping local interaction terms cannot generally be factored into independent one-site contributions. Even when an auxiliary transfer map has a spectral gap and yields a differentiable limiting pressure, that argument does not directly cover every finitely correlated state. A mixture can have a limiting log moment generating function with a corner; the resulting rate function can be nonconvex. Ogata's printed Lemma 4.1 reduces to special components but omits the separate mixture step needed to recover the unrestricted theorem. The goal retains the theorem's printed hypotheses, while the condition-(14) milestone records precisely the restricted pressure claim. Ogata, pp. 12–15

Formalization scope

The Lean model uses finite matrices for local algebras. A nonempty finite site basis represents $M_d(\mathbb C)$, with site 1 indexed by 0. An interaction stores one Hermitian term for each support anchored at its least site; all translates that fit in $[1,n]$ appear in the Hamiltonian. The scalar empty-set term is retained. The auxiliary algebra is represented by a full matrix algebra $M_k(\mathbb C)$; finite-dimensional $C^*$-algebra data have an equivalent full-matrix representation for the generated local states. Stationarity is written in the primal trace form. The recursive local state places the first site's matrix in the outermost application of $\mathcal E$.

The spectral law is formed from the eigenvalues and spectral weights of the actual Hamiltonian. It is not supplied as an arbitrary sequence of measures. The theorem uses no ergodicity, spectral-gap, or condition-(14) binder, and both LDP bounds range over every closed or open subset of $\mathbb R$. Logarithms of probabilities take values in the extended reals, with $\log0=-\infty$; sequence limits are at $n\to\infty$, so the placeholder value at $n=0$ is immaterial. Nonnegative lower integrals represent exponential moments. In the restricted pressure milestone, the real logarithm applies to a positive state expectation. These choices also rule out a vacuous proof based on a zero measure, a moment represented by a non-integrable Bochner integral, or a rate function unrelated to the spectral law.

Reusable contributions include finite-dimensional spectral-law lemmas, positivity and stationarity facts for completely positive maps, good-rate-function and LDP lemmas on $\mathbb R$, and the Gärtner–Ellis result. The full theorem additionally needs a treatment of non-ergodic finite mixtures and periodic components that preserves both large-deviation bounds.

Selected references

• Yoshiko Ogata, Large Deviations in Quantum Spin Chain, arXiv preprint, 2008. arXiv:0803.0113v1.

Motivation

Optical quantum communication commonly encodes information in continuous variables such as the position and momentum quadratures of a light mode. Gaussian states and Gaussian operations are attractive in this setting because phase shifters, squeezers, beam splitters, and homodyne measurements are standard optical tools. Transmission through a lossy or noisy line can also be modeled by a Gaussian channel. The practical question is whether adding vacuum modes and Gaussian encoding and decoding can protect a signal against such a channel. Niset, Fiurášek, and Cerf (2008) give a negative answer for the code class defined in their Fig. 1.

The result sits after the early impossibility results for distilling Gaussian entanglement with Gaussian operations, including Giedke and Cirac (2002). Those results concern shared states and allowed local operations. The 2008 paper asks the channel-coding question directly: whether a finite Gaussian code can make a fixed single-mode Gaussian channel less damaging to entanglement. It introduces a scalar, entanglement degradation, to state the answer for every single-mode Gaussian channel in one inequality.

Setting

A single optical mode has two real quadratures, $x$ and $p$. For $n$ modes, the order is $(x_1,p_1,\ldots,x_n,p_n)$. A state has a real covariance matrix $\gamma$ recording its second moments in this order. The vacuum covariance matrix is the identity $I$. A Gaussian channel $T$ on one mode is described at the covariance level by two real $2\times2$ matrices $M$ and $N$:

$$\gamma\longmapsto M\gamma M^{\mathsf T}+N.$$

Here $N$ is the added noise. Complete positivity imposes symmetry and a matrix positivity condition on $N$; in particular, it gives $\det N\ge(\det M-1)^2$. A Gaussian unitary changes covariances by a symplectic matrix $S$, satisfying $SJS^{\mathsf T}=J$ for the canonical symplectic form $J$. Displacements affect first moments only and therefore play no role in these covariance formulas.

The code $G(n,E,D)$ uses a positive integer $n$. The input occupies mode zero in the formalization; the other $n-1$ modes are vacuum ancillas. A Gaussian encoding unitary $E$ acts on all modes, then the same channel $T$ acts independently once on each mode, and a Gaussian decoding unitary $D$ acts on all modes. Only the first output mode is retained. This defines an effective single-mode channel $T_{GC}$ with matrices $M_{GC},N_{GC}$. The ancillas contribute noise to $N_{GC}$ even before the $n$ channel uses are counted.

For a channel $T=(M,N)$, the paper defines its degradation by

$$D[T]=\min\left\{\frac{\det N}{(1+\det M)^2},1\right\}.$$

The intended value is $1$ when the denominator vanishes: the quotient is then interpreted as infinite and is saturated by the minimum. This quantity is related to the entanglement remaining when $T$ acts on one half of a two-mode squeezed vacuum as the squeezing grows. The paper measures that entanglement through the smallest symplectic eigenvalue $\nu_-$ after partial transpose and the logarithmic negativity $E_N=\max\{0,-\log\nu_-\}$.

Formalization targets

Main no-go theorem

The mission goal is the theorem on page 3, equation (11): for every completely positive single-mode Gaussian channel and every finite code of the stated form,

$$D[T]\le D[T_{GC}].$$

This is the assertion that the code cannot lower the channel's entanglement degradation. It includes $n=1$, singular channels, and channels with negative determinant $M$. No numerical performance constant or bound on the number of modes is fixed.

Supporting results

The milestones record the paper's channel-noise constraint (2), the fact that the code produces a Gaussian channel, the local matrix normal forms used in Lemma 2, the asymptotic calculations (8) and (10), the entanglement-breaking case, and Lemma 2 itself. Lemma 2 characterizes the degradation through the limiting squared eigenvalue and, when finite, gives $E_N=-\tfrac12\log D[T]$. The milestones retain the paper's distinction between positive, negative, and zero determinant regimes.

Significance

The theorem rules out a specific and broad way of improving Gaussian transmission: adding any finite number of vacuum ancillas and using Gaussian unitaries before and after independent uses of a fixed channel cannot improve this intrinsic entanglement measure. The paper applies this conclusion to attenuation, amplification, and classical-noise channels, showing how an apparent reduction in one channel parameter can be offset by increased noise. It also relates degradation to an upper bound on quantum capacity, though that further bound is outside this mission. Niset, Fiurášek, and Cerf (2008)

The paper's theorem is proved in the mathematical literature; the goal here is a machine-checked statement and, eventually, a proof in the covariance-matrix representation. The published covariance layer already supplies symplectic forms, two-mode squeezed covariances, partial transpose, and an intrinsic $\nu_-$; this mission adds the channel and code definitions required to state the no-go theorem. Those definitions can be reused for other single-mode Gaussian-channel questions. A complete proof still needs substantial results connecting codes, Gaussian operations, and entanglement behavior; a compiled sorry statement alone does not establish the theorem.

Difficulty

One might try to compare $\det N$ before and after the code. That scalar does not track the code: encoding mixes signal and vacuum modes, each copy of the channel adds noise, decoding mixes the modes again, and discarding modes changes both $M_{GC}$ and $N_{GC}$. Neither determinant separately gives the desired inequality. The boundary $\det M=-1$ also defeats a direct real-valued transcription of the printed quotient. The asymptotic entanglement formulas cross several determinant regimes, with different normal forms and a separate entanglement-breaking case. The central challenge is to retain the physical meaning of all these cases in one theorem over arbitrary finite codes.

Formalization scope

Lean uses real matrices indexed by interleaved mode and quadrature coordinates. The published QAlgorithms_Papers_Independent_Frontier30_P13 layer provides ModeQuadrature, phaseJ, squeezedCM, partial transpose, and the intrinsic smallest symplectic eigenvalue lambdaMin; QAlgorithms_Papers_Independent_Dependency50_P10 provides entrywise complexification. A channel is required to satisfy the Gaussian complete-positivity matrix inequality. Encoders and decoders satisfy $SJS^{\mathsf T}=J$. The code uses the same $(M,N)$ on every one of its $n$ modes, with $n\ge1$, and includes the vacuum covariance on every ancillary mode. Gaussian unitaries enter through their symplectic matrices; their displacement parts do not affect covariances.

The definition of $D$ explicitly saturates at $1$ when $1+\det M=0$, avoiding Lean's zero value for division by zero. The squeezed input uses $\cosh(2r)$ and $\sinh(2r)$. The eigenvalue $\nu_-$ is the intrinsic lambdaMin, not an unguarded square-root expression. Logarithmic negativity uses the natural logarithm; its finite limit statement assumes $\det N>0$, while the degradation statement still covers $\det N=0$. The infinite-squeezing output is represented by limits of finite-$r$ covariances and entanglement quantities.

The code's vacuum term, all $n$ noise blocks, the symplectic equation, and the guarded degradation are essential to the target; dropping any of them would change the question. Lemma 1's teleportation equivalence and the external Gaussian no-distillation theorem are not formalized here. Their faithful treatment would require operational Gaussian states, measurements, and protocols beyond the covariance model. Contributions establishing those interfaces, proving the stated matrix milestones, or connecting the two layers are welcome.

Selected references

• J. Niset, J. Fiurášek, and N. J. Cerf, A No-Go Theorem for Gaussian Quantum Error Correction, Physical Review Letters 102, 120501, 2009; arXiv:0811.3128v1 (2008). The preprint is the citation basis for page and equation numbers here.
• G. Giedke and J. I. Cirac, Characterization of Gaussian operations and distillation of Gaussian states, Physical Review A 66, 032316, 2002; arXiv:quant-ph/0204085.

Motivation

Quantum circuits whose gates respect a global symmetry are a standard model for quantum simulation, for symmetry-protected quantum computing, and for the study of conserved quantities in quantum dynamics. For SU(d) symmetry on $n$ qudits, the unitaries that commute with every $U^{\otimes n}$ are, by Schur–Weyl duality, exactly the unitaries in the linear span of the qudit permutations. A natural question is whether every such unitary can be built from local symmetric gates, as happens without symmetry, where 2-qudit gates are universal.

Marvian, Liu and Hulse (arXiv:2105.12877) show that for $d \ge 3$ the answer is no, and that the obstruction appears as conservation laws. Unitaries generated by 2-local SU(d)-invariant gates conserve quantities that general SU(d)-invariant unitaries change. The paper gives two families of such laws. The first, Theorem 1 (the $f_{\mathrm{sgn}}$ law, from a $\mathbb Z_2$ symmetry of the swap Hamiltonians), is a separate result of the paper and is not part of this mission. The second, Theorem 2, is the target here. It comes from a correspondence between a subspace of the qudits and a system of free fermions.

Timeline: Marvian (Nature Physics 18, 283, 2022) showed that symmetry together with locality restricts the realizable unitaries in general, with examples for U(1) and SU(2) symmetry. For qubits with SU(2) symmetry, the constraints restrict only relative phases between sectors of inequivalent irreducible representations (p. 3 of the present paper). The present paper (arXiv:2105.12877, v2 January 2022) treats SU(d) with $d\ge 3$, where constraints beyond relative phases appear. The connection to Marin's 2007 description of the Lie algebra generated by transpositions (J. Algebra 310, 742) is discussed on p. 9.

Setting

Consider $n$ qudits with Hilbert space $(\mathbb C^d)^{\otimes n}$ and computational basis $|x_1\rangle\cdots|x_n\rangle$, $x_i\in\{0,\dots,d-1\}$.

• A unitary $V$ is SU(d)-invariant if $[V,U^{\otimes n}]=0$ for every $U\in\mathrm{SU}(d)$ (Eq. (1)).
• $V$ is 2-local on qudits $a,b$ if $V=W_{ab}\otimes\mathbb I_{\text{rest}}$.
• $\mathcal V_2$ is the group generated by finite products of 2-local SU(d)-invariant unitaries.
• $\mathbf P(\sigma)$ is the permutation operator of $\sigma\in S_n$, and $\mathbf P_{ab}$ is the swap of qudits $a,b$.

For $L\le\min\{n,d-1\}$, the vector $\big(\bigwedge_{m=1}^L|m\rangle\big)\otimes|0\rangle^{\otimes(n-L)}$ antisymmetrizes the levels $1,\dots,L$ over the first $L$ qudits with weight $1/\sqrt{L!}$ (Eq. (40)). The subspace $\mathcal H_{\mathrm{comp}}$ is the span of all permutations of these vectors (Eq. (42)), and $\Pi_{\mathrm{comp}}$ is the orthogonal projector onto it.

For an operator $A$ on one qudit, $A_i$ is $A$ acting on qudit $i$. Let $Q_{ij}=(\mathbb I_i-|0\rangle\langle0|_i)|0\rangle\langle0|_j$. The map $\Omega$ sends an operator $\rho$ on the qudits to the $n\times n$ matrix

$$\Omega[\rho]=\sum_{i,j=1}^n\Omega_{ij}[\rho]\,|i\rangle\langle j|,\qquad \Omega_{ij}[\rho]=\begin{cases}\mathrm{Tr}\big(\Pi_{\mathrm{comp}}\rho\Pi_{\mathrm{comp}}\,\mathbf P_{ij}Q_{ij}\big)& i\neq j,\\ \mathrm{Tr}\big(\Pi_{\mathrm{comp}}\rho\Pi_{\mathrm{comp}}\,(\mathbb I_i-|0\rangle\langle0|_i)\big)& i=j\end{cases}$$

(Eqs. (49), (51)). On the fermionic side there are $n$ sites, creation operators $c_j^\dagger$, the vacuum $|\mathrm{vac}\rangle$, and the fermionic swap $\mathbf P^f_{ab}=\mathbb I^f-(c_a^\dagger-c_b^\dagger)(c_a-c_b)$ (Eq. (28)). Its single-particle counterpart is $E_{ab}=\mathbb I-(|a\rangle-|b\rangle)(\langle a|-\langle b|)$ on $\mathbb C^n$ (Eq. (33)). The map $U^f$ sends $\mathbf P(\sigma)\big[\big(\bigwedge_{m}|m\rangle\big)\otimes|0\rangle^{\otimes(n-L)}\big]$ to $\prod_{i=1}^L c^\dagger_{\sigma(i)}|\mathrm{vac}\rangle$ (Eq. (41)).

Formalization targets

Goal: Theorem 2 (p. 11)

For every $V\in\mathcal V_2$, every density operator $\rho$ on $n$ qudits and every positive integer $l$,

$$\mathrm{Tr}\big(\Omega[V\rho V^\dagger]^l\big)=\mathrm{Tr}\big(\Omega[\rho]^l\big).$$

The statement holds for all $n$ and $d$. Its content is the case $l\ge 2$: the case $l=1$ holds for every SU(d)-invariant unitary (Eq. (55)).

Milestones (in attack order)

1. Eq. (5): up to a global phase, a 2-local SU(d)-invariant unitary on qudits $a,b$ equals $e^{i\theta\mathbf P_{ab}}=\cos\theta\,\mathbb I+i\sin\theta\,\mathbf P_{ab}$.
2. Eqs. (27)–(29): $\mathbf P^f_{ab}c_j^\dagger\mathbf P^{f\dagger}_{ab}=c^\dagger_{\sigma_{ab}(j)}$, $\mathbf P^f_{ab}|\mathrm{vac}\rangle=|\mathrm{vac}\rangle$, and $\mathbf P^f_{ab}$ is Hermitian and unitary.
3. Eq. (31): $e^{i\theta\mathbf P^f_{ab}}c_j^\dagger e^{-i\theta\mathbf P^f_{ab}}=e^{-i\theta}(\cos\theta\,c_j^\dagger+i\sin\theta\,c^\dagger_{\sigma_{ab}(j)})$.
4. Eq. (34): the same dynamics written through the single-particle unitary $e^{i\theta(E_{ab}-\mathbb I)}$.
5. p. 9: $\mathbf P(\sigma)\Pi_{\mathrm{comp}}=\Pi_{\mathrm{comp}}\mathbf P(\sigma)$.
6. Eq. (41) and App. C5: $U^f$ satisfies (41) and is an isometry on $\mathcal H_{\mathrm{comp}}$.
7. Eq. (44): $U^fe^{i\theta\mathbf P_{ab}}\Pi_{\mathrm{comp}}=e^{i\theta\mathbf P^f_{ab}}U^f\Pi_{\mathrm{comp}}$.
8. App. C7, (C42)–(C43): the qudit form (51) and the fermionic form (50) of $\Omega$ agree.
9. Lemma 3: $\Omega[e^{i\theta\mathbf P_{ab}}\rho e^{-i\theta\mathbf P_{ab}}]=e^{i\theta E_{ab}}\Omega[\rho]e^{-i\theta E_{ab}}$, and $\Omega$ is completely positive.

Significance

Theorem 2 gives an infinite family of polynomial invariants of the state, $\mathrm{Tr}(\Omega[\rho]^l)$ for $l=1,2,\dots$. Together these fix the spectrum of $\Omega[\rho]$, so every Rényi entropy of the single-particle density operator $\Omega[\rho]/\mathrm{Tr}\,\Omega[\rho]$ is conserved. Already for $l=2$ the law is violated by SU(d)-invariant Hamiltonians with 3-local terms (p. 11 and §IV D). This shows that, for $d\ge3$, 2-local SU(d)-invariant gates are not universal among SU(d)-invariant unitaries, even up to relative phases, and that 3-local interactions can be detected from the dynamics of $\Omega$. For $d=2$ the laws hold for all SU(2)-invariant unitaries.

The result is proved in the paper. As far as a search of the platform shows, it has not been formalized. A formalization adds machine-checked versions of the qudit–fermion correspondence of §IV B, including the isometry $U^f$ and the intertwining relation (44), and of the free-fermion form of the swap dynamics. These are statements about finite-dimensional matrices, so the whole development stays inside Mathlib's linear algebra.

Difficulty

The obvious route is to show that each generator acts on $\Omega[\rho]$ by conjugation with an $n\times n$ unitary, and then to induct over products. The difficulty is the generator step. The definition (51) of $\Omega$ involves the projector $\Pi_{\mathrm{comp}}$ onto a span of antisymmetrized vectors, and nothing in (51) shows directly why conjugating $\rho$ by $e^{i\theta\mathbf P_{ab}}$ should conjugate $\Omega[\rho]$ by $e^{i\theta E_{ab}}$. The covariance becomes visible only after $\mathcal H_{\mathrm{comp}}$ is identified with fermionic Fock sectors, where the swap becomes a quadratic, particle-number-preserving Hamiltonian. That identification needs care with the signs of the fermionic creation operators and with the ordering of products. A second obstacle is the characterization of the generators (Eq. (5)). It rests on the commutant of $\{U\otimes U : U\in\mathrm{SU}(d)\}$ being spanned by $\mathbb I$ and the swap, a Schur–Weyl statement for two qudits that Mathlib does not provide.

Formalization scope

Operators on the qudits are matrices indexed by Fin n → Fin d, with sites and levels 0-based and [NeZero d] assumed so that $|0\rangle$ exists. Fock-space operators are matrices indexed by Finset (Fin n), the set of occupied sites. The creation operator uses the Jordan–Wigner sign $(-1)^{|\{k\in T:k<j\}|}$, the encoding of the public definition QAlgorithms_Papers_Independent_Next46_P23, copied rather than imported.

The following conventions are fixed:

• $\mathbf P(\sigma)|y\rangle=|y\circ\sigma^{-1}\rangle$, the representation convention the paper uses in Eq. (30) and App. C5. Eq. (9) as printed describes $\mathbf P(\sigma^{-1})$, and under it the map of Eq. (41) is not well defined. All other objects coincide under the two conventions.
• Exponentials of involutions are written in the closed form $\cos\theta\,\mathbb I+i\sin\theta X$ of Eq. (5), and $\theta$ ranges over $[0,2\pi)$ as in the paper.
• $\Pi_{\mathrm{comp}}$ is the matrix of Mathlib's orthogonal projection onto $\mathcal H_{\mathrm{comp}}\subseteq$ EuclideanSpace ℂ (Fin n → Fin d).
• $U^f$ is an explicit linear map defined on the whole space. It sends the basis state with $|m\rangle$ on site $p(m)$, $m=1,\dots,L$, to $\frac1{\sqrt{L!}}c^\dagger_{p(1)}\cdots c^\dagger_{p(L)}|\mathrm{vac}\rangle$, and all other basis states to $0$.
• Complete positivity is the published QAlgorithms.Entanglement.IsCompletelyPositive.

The following trivializing formalizations are ruled out:

• $\Omega$ is not identically zero: the normalization $1/\sqrt{L!}$ and the range $L\le\min\{n,d-1\}$ are as printed, and $\mathcal H_{\mathrm{comp}}\neq 0$ is checked.
• $\mathcal V_2$ is the group generated by all 2-local SU(d)-invariant unitaries, defined literally on p. 3. It is neither the generating set of Eq. (6) nor the group of all SU(d)-invariant unitaries, for which the statement is false when $d\ge3$.
• The goal uses the qudit form (51) of $\Omega$, not the fermionic form (50).

A complete development needs:

• the two-qudit commutant of $U\otimes U$;
• the CAR algebra on Finset Fock space;
• the orthonormality of the antisymmetrized vectors;
• the trace identity $\mathrm{Tr}((WXW^\dagger)^l)=\mathrm{Tr}(X^l)$.

The Fock-space and permutation-operator lemmas can be reused for other qudit–fermion and Schur–Weyl statements. Contributions welcome: proofs of any milestone, and lemma-level infrastructure on the Fock space.

Selected references

• I. Marvian, H. Liu, A. Hulse, Qudit circuits with SU(d) symmetry: Locality imposes additional conservation laws, arXiv:2105.12877v2, 2022. https://arxiv.org/abs/2105.12877
• I. Marvian, Restrictions on realizable unitary operations imposed by symmetry and locality, Nature Physics 18, 283–289, 2022. https://doi.org/10.1038/s41567-021-01464-0
• I. Marin, L'algèbre de Lie des transpositions, Journal of Algebra 310, 742–774, 2007. https://doi.org/10.1016/j.jalgebra.2006.08.018

Motivation

A qubit coupled to an environment loses the phase relation between its basis states $|0\rangle$ and $|1\rangle$: the off-diagonal entries of its density matrix decay. This decoherence is the main obstacle to storing quantum information, and a large body of work tries to counter it with external control fields. Lidar and Schneider (arXiv:quant-ph/0410048, Quantum Information and Computation 2005) ask a sharp question in the simplest nontrivial setting: if the controller may observe the state and choose the Hamiltonian at every instant (tracking control), can it keep the coherence of a dephasing qubit exactly constant, and for how long?

Their answer, stated in the abstract, is that "it is possible to maintain coherence for finite time durations, until the control field diverges." It was known that Hamiltonian control cannot hold the purity $\operatorname{Tr}\rho^2$ of a Markovian open system at its initial value (Ketterle and Pritchard, Phys. Rev. A 46, 4051 (1992), and Tannor and Bartana, J. Phys. Chem. A 103, 10359 (1999), refs. [25, 26] of the paper), and the paper's §II.A shows that under a unital Lindbladian the purity decreases whatever the Hamiltonian; the present result locates exactly how much of the coherence, as opposed to the purity, control can protect.

Setting

A qubit state is a complex $2\times2$ matrix $\rho$ with $\operatorname{Tr}\rho=1$, $\rho_{10}=\rho_{01}^*$ and $\operatorname{Tr}(\rho^2)\le1$. With the Pauli matrices $\sigma_x,\sigma_y,\sigma_z$, its Bloch vector is $\vec v=(v_x,v_y,v_z)$, $v_\alpha=\operatorname{Tr}(\rho\sigma_\alpha)$, so that $\rho=\tfrac12(I+\vec v\cdot\vec\sigma)$ (eq. (9)). The coherence is the squared radius of $\vec v$ in the $x$–$y$ plane,

$$c=v_x^2+v_y^2=4|\rho_{01}|^2 \quad\text{(eq. (11))}.$$

The controller applies the Hamiltonian $H(t)=\tfrac{\hbar}{2}\bigl(\omega_0(t)\sigma_z+\omega_1(t)\sigma_x-\omega_2(t)\sigma_y\bigr)$ (eq. (13)) with three real fields $\omega_0,\omega_1,\omega_2$, and the qubit undergoes pure dephasing at rate $\gamma>0$:

$$\frac{\partial\rho}{\partial t}=-\frac{i}{\hbar}[H,\rho]+\frac{\gamma}{2}(\sigma_z\rho\sigma_z-\rho)\quad\text{(eq. (32))}.$$

Equivalently the Bloch vector obeys $\dot{\vec v}=M(t)\vec v$ with

$$M(t)=\begin{pmatrix}-\gamma&-\omega_0&-\omega_2\\ \omega_0&-\gamma&-\omega_1\\ \omega_2&\omega_1&0\end{pmatrix}\quad\text{(eq. (30))}.$$

Without control the coherence decays as $e^{-2\gamma t}c$. The breakdown time of an initial state with coherence $c>0$ is

$$t_b=\frac{v_z(0)^2}{2\gamma c}\quad\text{(eq. (38))}.$$

The tracking fields are, with $s=\operatorname{sign}v_z(0)$, an arbitrary $\omega_0$, and $R(t)=v_z(0)^2-2\gamma ct$,

$$\omega_2(t)=s\,\frac{-\gamma v_x(0)-\omega_0(t)v_y(0)}{\sqrt{R(t)}},\qquad \omega_1(t)=s\,\frac{-\gamma v_y(0)+\omega_0(t)v_x(0)}{\sqrt{R(t)}}\quad\text{(eqs. (41)–(42))},$$

and the tracked state is $\tfrac12(I+\vec v(t)\cdot\vec\sigma)$ with $\vec v(t)=(v_x(0),v_y(0),s\sqrt{R(t)})$.

Formalization targets

Goal: coherence can be held exactly on $[0,t_b)$, and no longer

For $\hbar>0$, $\gamma>0$ and a qubit state $\rho_0$ with coherence $c>0$:

1. No-go. For all controls and every solution $\rho(t)$ of (32) on $[0,T)$ with $\rho(0)=\rho_0$ and constant coherence $c$,

$$v_z(t)^2=v_z(0)^2-2\gamma c\,t\quad(t\in[0,T)),\qquad T\le t_b .$$

2. Achievability. If $v_z(0)\ne0$, then for every $\omega_0$ the tracked state starts at $\rho_0$, is a qubit state, keeps $v_x,v_y$ fixed, and solves (32) at every $t\in[0,t_b)$ with the tracking fields.
3. Divergence. If $v_z(0)\ne0$, then $\omega_1(t)^2+\omega_2(t)^2\to+\infty$ as $t\to t_b^-$, whatever $\omega_0$ is.

Milestones

The milestones follow the paper's derivation: the Bloch parametrization (§II.B, p. 3); the equivalence of (32) and (30) (§III.B, p. 5); eq. (36), $\dot v_z=-\gamma c/v_z$ under constant coherence (p. 6); eqs. (37)–(38), $v_z(t)=(\pm)\sqrt{v_z(0)^2-2\gamma ct}$ and $T\le t_b$ (p. 6); eqs. (41)–(42), the tracking fields solve (30) and are forced once $v_x,v_y$ are frozen (p. 6); and the field-strength identity of §III.C (p. 8),

$$\omega_1(t)^2+\omega_2(t)^2=\frac{(\gamma^2+\omega_0(t)^2)\,c}{v_z(0)^2-2\gamma ct}.$$

Significance

The result gives an exact, state-dependent budget for coherence protection under dephasing. The time $t_b$ is inversely proportional to the coherence to be maintained and proportional to $v_z(0)^2=p(0)-c$, where $p=|\vec v|^2$ is the purity: the more coherent the initial state, the shorter the protection, and a state of maximal coherence for its purity ($v_z(0)=0$) cannot be protected at all. The no-go part holds for every control law, so it bounds any tracking strategy, not only the linearized one the paper constructs. The divergence of the fields is the physical cost: protection up to $t_b$ requires unbounded control amplitude, which any bounded actuator cuts short.

The paper proves these statements by direct calculation. As far as is known, none of them has a machine-checked proof. The mission turns a physics derivation, in which "the solution is" and "does not stay real" carry the logical weight, into precise statements about solutions of an ODE on a half-open interval, with the sign choice, the degenerate case $v_z(0)=0$ and the domain of the square roots made explicit.

Difficulty

The calculations are elementary, but the no-go statement quantifies over arbitrary, possibly discontinuous control fields and arbitrary solutions of the matrix equation. Nothing is assumed about the controls beyond being real functions of time, nothing about the solution beyond continuity on $[0,T)$ and the equation on $(0,T)$, and the conclusion constrains only the $z$-component while the hypothesis constrains only the $x$–$y$ components. The tempting shortcut, assuming that $v_x$ and $v_y$ are frozen as in the paper's explicit construction, proves a strictly weaker statement and is not the goal. On the achievability side, the square root is not differentiable where its argument vanishes, so differentiability has to be established on $[0,t_b)$, including the endpoint $t=0$, and the sign $\operatorname{sign}v_z(0)$ has to be carried through the derivative.

Formalization scope

Operators are Matrix (Fin 2) (Fin 2) ℂ in the basis $|0\rangle,|1\rangle$; the Pauli matrices are the published MIPRE.LCS.Pauli.X/Y/Z. Bloch vectors and controls are Fin 3 → ℝ: Bloch components in the order $x,y,z$, control components in the order $\omega_0,\omega_1,\omega_2$ (with $\omega_0$ multiplying $\sigma_z$, as in (13)). The Bloch vector is $v_\alpha=\operatorname{Re}\operatorname{Tr}(\rho\sigma_\alpha)$, following eq. (9); eq. (8) prints an extra factor $\tfrac12$, which contradicts (9) and is treated as a misprint. A trajectory solves (32) or (30) on $[0,T)$ if it is continuous on $[0,T)$ and has the prescribed derivative at every $t\in(0,T)$. Controls are arbitrary functions $\mathbb R\to\mathbb R$. The hypotheses $\gamma>0$ and $c>0$ are added, because $t_b$ divides by $2\gamma c$; $\hbar>0$ is a parameter. The sign $(\pm)$ of (37), (41), (42) is $\operatorname{sign}v_z(0)$.

Statements about $t_b$, the tracked state and the fields are restricted to $[0,t_b)$, because Lean's square root and division are total ($\sqrt{x}=0$ for $x<0$, $x/0=0$); a statement that only asserts that the closed-form curve solves the ODE would be the achievability half alone, and the goal requires the no-go half over all controls as well.

A complete development needs the Bloch dictionary for $2\times2$ matrices, the passage from (32) to (30), and one-variable real analysis on half-open intervals. The Bloch dictionary and the reduction of a Lindblad equation to Bloch form are reusable for other qubit control problems. Proofs of any milestone, and sorry-free lemmas on the Pauli algebra, are welcome.

Selected references

• D. A. Lidar and S. Schneider, Stabilizing qubit coherence via tracking-control, Quantum Information and Computation (2005); arXiv:quant-ph/0410048v1, 2004. https://arxiv.org/abs/quant-ph/0410048
• W. Ketterle and D. E. Pritchard, Atom cooling by time-dependent potentials, Physical Review A 46, 4051 (1992). https://doi.org/10.1103/PhysRevA.46.4051

Motivation

In the fluid queuing model (Vickrey's model) of flows over time, a continuum of infinitesimal particles travels from a source $s$ to a sink $t$ through a network whose arcs have capacities and transit times. Each particle picks a route that minimizes its own arrival time, and a dynamic equilibrium (a Nash flow over time) is a flow in which no particle can arrive earlier by deviating. Dynamic equilibria are a basic model of congestion in road traffic and communication networks.

Koch and Skutella (2011) showed that the derivatives of a dynamic equilibrium are normalized thin flows with resetting, and Cominetti, Correa and Larré (2015) proved that such thin flows always exist, which gives existence of equilibria. Computing a thin flow, however, was known to be efficient only in the two extreme cases where no arc or every arc is resetting. Kaiser (2022) casts thin flows as a linear complementarity problem, studies how they depend on the flow value, and shows that on two-terminal series-parallel networks the whole family of thin flows, for all flow values at once, can be computed in polynomial time. The key quantitative fact behind that algorithm is a bound on the number of breakpoints of the thin-flow labels as a function of the flow value. This mission formalizes that bound and the chain of results it rests on.

• 2011: Koch and Skutella characterize the derivatives of Nash flows over time by thin flows with resetting.
• 2015: Cominetti, Correa and Larré prove existence of normalized thin flows with resetting and of dynamic equilibria for $L^p$ inflow rates.
• 2020/2022: Kaiser gives the LCP formulation, the parametric analysis and the series-parallel algorithm.

Setting

A network is a finite directed multigraph with vertex set $V$, arc set $A'$ and two vertices $s \ne t$. It is a shortest path graph if $A'$ is acyclic and every vertex is reachable from $s$. Fix a set $A^* \subseteq A'$ of resetting arcs and capacities $\nu_a > 0$. A static $s$–$t$-flow of value $\nu'_0$ is a vector $x' \ge 0$ on the arcs that is conserved at every vertex other than $s, t$ and has net outflow $\nu'_0$ at $s$.

Along an arc $a = (v,w)$ a label is propagated by

$$\varrho^a(\ell'_v, x'_a) = \begin{cases}\max\{\ell'_v, x'_a/\nu_a\} & a \notin A^*,\\ x'_a/\nu_a & a \in A^*.\end{cases}$$

Labels $\ell' \in \mathbb R^V_{\ge 0}$ correspond to the flow $x'$ if $\ell'_w = \min_{a = (v,w)} \varrho^a(\ell'_v, x'_a)$ for every $w \ne s$ and $\ell'_w = \varrho^a(\ell'_v, x'_a)$ on every arc with $x'_a > 0$; such an $x'$ is a normalized thin flow with resetting (Definition 4).

The label function $\varrho^{G'}$ maps each flow value $\nu'_0 \ge 0$ to the corresponding labels, with label $1$ at $s$, of a normalized thin flow of value $\nu'_0$. A breakpoint of $\varrho^{G'}$ is a value $\nu'_0 > 0$ around which some component of $\varrho^{G'}$ is not affine.

A two-terminal series-parallel multigraph is built from single arcs $s \to t$ by series composition $G_1 * G_2$ (sink of $G_1$ glued to source of $G_2$) and parallel composition $G_1 \parallel G_2$ (sources glued, sinks glued).

Formalization targets

Goal: Theorem 31

For a two-terminal series-parallel multigraph $G' = (V, A')$, any $A^* \subseteq A'$ and any capacities $\nu > 0$: the label function $\varrho^{G'}$ exists, is continuous on $[0,\infty)$, has finitely many breakpoints, and

$$\#\{\text{breakpoints of } \varrho^{G'}\} \le 2|A'| - |A^*| - |V| + 1 .$$

Milestones

The milestones follow the paper's proof path.

• Theorem 6. Normalized thin flows are exactly the solutions of a linear complementarity problem (LCP) that also satisfy a normalization constraint.
• Lemma 7 and Corollary 8. A normalization map $\pi$ turns every LCP solution into a thin flow.
• Lemmas 11, 12 and 9. The LCP matrix has non-negative principal minors, via the factorization $L = BD(B^+)^\top$ of weighted Laplacians.
• Theorem 13 (existence). A thin flow exists for every flow value and every label at $s$.
• Theorem 14 and Corollary 15. Labels are monotone in the flow value and the label at $s$, and they are unique.
• Proposition 17. $\varrho^{G'}$ is continuous and piecewise linear.
• Lemma 18. Scaling and monotonicity of $\varrho^{G'}$.
• Lemmas 29 and 30. Series composition gives $n \le n_1 + n_2$ breakpoints, and parallel composition gives $n \le n_1 + n_2 + 1$.

Significance

The bound is what makes the recursive computation of $\varrho^{G'}$ along a series-parallel decomposition run in time polynomial in the size of the network. Each composition step is linear in the number of pieces, and Theorem 31 keeps the number of pieces linear in $|A'|$. Combined with the paper's §5, the result computes dynamic equilibria in series-parallel networks for piecewise constant, and more generally right-monotone, inflow rates. For general graphs the complexity of computing a thin flow with resetting is open: the problem lies in PPAD, and no polynomial algorithm is known. The bound is attained already for a single non-resetting arc, whose label at $t$ is $\max\{1, \nu'_0/\nu_a\}$.

The results are proved in the paper. None of them has been formalized: there is no machine-checked theory of flows over time, thin flows or directed series-parallel graphs. A formalization adds three things. It gives a checked LCP formulation of thin flows, which is reusable for any equilibrium computation in this model. It gives a checked parametric analysis (existence, uniqueness, monotonicity and piecewise linearity of the labels). And it gives a complete account of the counting argument for parallel composition, which the paper extends from the sink's label to the whole label vector only in outline ("Repeating the counting more carefully…").

Difficulty

Existence (Theorem 13) is not elementary. It combines a principal-minor computation for a block matrix with a theorem from LCP theory: a $P_0$-matrix whose LCP has only the trivial solution at zero data has a solution for every right-hand side. Mathlib has neither. Piecewise linearity (Proposition 17) likewise uses that solution sets of an LCP are finite unions of polyhedra.

The breakpoint count is subtle in the parallel case. Splitting the flow $\nu'_0 = \nu'_1 + \nu'_2$ between the two parts is generally not unique, so $\varrho^{G'}$ is not simply a composition of $\varrho^{G'_1}$ and $\varrho^{G'_2}$. The proof constructs a piecewise linear selection of the split and counts where its pieces can change. A tempting shortcut is to bound only the breakpoints of the sink's label $\varrho^{G'}_t$. That is weaker than what is claimed, which is a bound for the entire label vector.

Formalization scope

• Representation.
  • Networks are bundled finite multigraphs (Net) with arc types and tail/head maps, so parallel arcs are first-class.
  • $A^*$ is a Finset of arcs and capacities are real with $\nu > 0$.
  • The minimum in Definition 4 is IsLeast, never sInf.
  • The two-terminal series-parallel graphs are the graphs T.toNet of terms T : SPTerm built from arc, series and par. Every member of Definition 28's class is isomorphic to such a graph, and all quantities here are isomorphism-invariant.
• Label functions. Statements about $\varrho^{G'}$ are made about every function with its defining property: value $\nu'_0 \ge 0$, corresponding labels, label exactly $1$ at $s$. By Corollary 15 such a function is unique on $[0,\infty)$. The goal also asserts that one exists, so the bound cannot hold vacuously because no label function exists.
• Breakpoints. A breakpoint is a point $\nu'_0 > 0$ near which some component is not affine. They are counted for the whole vector, with Set.encard in Lemmas 29–30 and with Set.ncard plus finiteness in the goal.
• Arithmetic. The bound $2|A'| - |A^*| - |V| + 1$ is computed in $\mathbb Z$.
• The normalization $\pi$. It is computed by $|V|$ sweeps of its update rule, which equals the topological-order recursion on acyclic graphs.
• Additions relative to the page.
  • $s \ne t$ is added as a hypothesis in the flow statements of §4. It is the standing assumption of §2.
  • Lemma 11 assumes no self-loops, since the identity fails for a self-loop.
  • Lemma 18 (i) uses $\ell'_0 > 0$; at $\ell'_0 = 0$ the printed claim divides by zero and fails.
  • Lemma 18 adds the capacities, which the page omits.
  • In Lemmas 29–30 the parts inherit $A^*$ and $\nu$ by restriction.
• Not formalized. The second clause of Theorem 31, "can be computed in polynomial time", is not formalized, and neither is Corollary 32: Mathlib has no cost model for real-number algorithms. The dynamic model of §§2–3 and §5 (inflow rates, queues, Theorem 24) is outside this mission.

A complete development needs:

• an LCP theory for $P_0$-matrices (existence, and piecewise linearity of parametric solutions);
• Gershgorin-type bounds for diagonally dominant matrices;
• elementary combinatorics of acyclic multigraphs.

The LCP layer and the network and series-parallel layer are reusable beyond this mission. Contributions to either are welcome, as are proofs of the elementary milestones (Lemma 7, Lemma 11, Theorem 14, Corollary 15) independently of the rest.

Selected references

• M. Kaiser, Computation of Dynamic Equilibria in Series-Parallel Networks, Mathematics of Operations Research, 2022; preprint arXiv:2002.11428v2 (2020). https://arxiv.org/abs/2002.11428
• R. Koch and M. Skutella, Nash equilibria and the price of anarchy for flows over time, Theory of Computing Systems 49 (2011). https://doi.org/10.1007/s00224-010-9299-y
• R. Cominetti, J. Correa and O. Larré, Dynamic equilibria in fluid queueing networks, Operations Research 63 (2015). https://doi.org/10.1287/opre.2015.1348
• R. W. Cottle, J.-S. Pang and R. E. Stone, The Linear Complementarity Problem, SIAM Classics in Applied Mathematics, 2009. https://doi.org/10.1137/1.9780898719000

Motivation

The walled Brauer algebra $B_{r,s}(\delta)$ is the centralizer algebra of mixed Schur–Weyl duality: for $\delta=n$ it acts on the mixed tensor space $V^{\otimes r}\otimes (V^*)^{\otimes s}$ of $V=\mathbb C^n$ and commutes with $\mathfrak{gl}_n$, and for $\delta=m-n$ it plays the same role for the general linear supergroup $GL(m|n)$. Its representation theory has been studied through cellular structures and blocks (Cox–De Visscher–Doty–Martin 2008), Khovanov arc algebras (Brundan–Stroppel 2012) and cyclotomic quotients (Sartori–Stroppel 2015).

For the group algebra $\mathbb C\mathfrak S_n$ of the symmetric group there is a classical description of the center: it consists of the symmetric polynomials in the Jucys–Murphy elements $L_k=\sum_{j<k}(j,k)$ (Jucys 1974, Murphy 1983). Jung and Kim (arXiv:1508.06469v2) prove the walled analogue: when $B_{r,s}(\delta)$ is semisimple, its center is generated by the supersymmetric polynomials in its Jucys–Murphy elements. This mission formalizes that theorem and the chain of results leading to it.

Timeline. Jucys (1974) and Murphy (1981, 1983) describe the center of $\mathbb C\mathfrak S_n$ through Jucys–Murphy elements. Stembridge (1985) characterizes supersymmetric polynomials and shows that the power sums generate them. Cox, De Visscher, Doty and Martin (2008) give the cellular structure of $B_{r,s}(\delta)$, its blocks in characteristic zero and a semisimplicity criterion. Brundan and Stroppel (2012) prove that the central element $z_{r,s}$ (essentially $L_1+\dots+L_{r+s}$) acts on cell modules by a content sum. Jung and Kim (2015, revised 2017) prove the generation theorem for all supersymmetric polynomials.

Setting

Fix integers $r,s\ge0$ and $\delta\in\mathbb C$. An $(r,s)$-walled Brauer diagram is a pairing of $2(r+s)$ vertices, $r+s$ on top and $r+s$ on the bottom, with a wall between positions $r$ and $r+1$, such that vertical edges do not cross the wall and horizontal edges do. $B_{r,s}(\delta)$ is the complex vector space with these diagrams as basis; two diagrams are multiplied by stacking them and replacing each closed loop by a factor $\delta$.

For vertices $a\ne b$ on the same side of the wall, $(a,b)$ is the diagram of the transposition of $a$ and $b$. For $1\le j\le r<k\le r+s$, $e_{j,k}$ is the diagram with a top arc and a bottom arc joining $j$ and $k$ and all other vertices joined straight down. The Jucys–Murphy elements (Definition 2.1) are

$$L_k=\sum_{j=1}^{k-1}(j,k)\quad(1\le k\le r),\qquad L_k=-\sum_{j=1}^{r}e_{j,k}+\sum_{j=r+1}^{k-1}(j,k)+\delta\quad(r<k\le r+s).$$

A polynomial $p\in\mathbb C[x_1,\dots,x_r,y_1,\dots,y_s]$ is supersymmetric (Definition 2.8) if it is symmetric in the $x_i$ and in the $y_j$ separately, and the substitution $x_r=-y_1=t$ produces a polynomial independent of $t$. Examples are the power sums $p_k=\sum_i x_i^k+(-1)^{k+1}\sum_j y_j^k$. Write $S_{r,s}[x;y]$ for the supersymmetric polynomials and $p(L_1,\dots,L_{r+s})$ for the substitution $x_i\mapsto L_i$, $y_j\mapsto L_{r+j}$.

The cell modules $C_{r,s}(\lambda)$ are indexed by bipartitions $\lambda=(\lambda^L,\lambda^R)$ with $|\lambda^L|=r-t$, $|\lambda^R|=s-t$, $0\le t\le\min(r,s)$; this set is $\Lambda_{r,s}$. The set $\dot\Lambda_{r,s}$ equals $\Lambda_{r,s}$ except when $\delta=0$ and $r=s\ne0$, where $(\varnothing,\varnothing)$ is removed; it indexes the simple modules. The content vector $c(\lambda,\cdot)\in\mathbb C^{r+s}$ lists the contents of $\lambda^L$, then $2t$ zeros, then the contents of $\lambda^R$ shifted by $\delta$.

Formalization targets

Goal: Theorem 3.5

$$B_{r,s}(\delta)\ \text{semisimple}\ \Longrightarrow\ \mathbb C\bigl[p(L_1,\dots,L_{r+s}) : p\in S_{r,s}[x;y]\bigr]=Z\bigl(B_{r,s}(\delta)\bigr).$$

Both inclusions are asserted. The goal fixes no constants; the hypothesis holds for all but finitely many $\delta$ (Proposition 1.1).

Milestones

1. Relations among generators: Lemma 2.3 and Proposition 2.4.
2. The $L_k$ commute (Proposition 2.6); the power sums $p_k(L_1,\dots,L_{r+s})$ are central (Proposition 2.7).
3. Stembridge's theorem, $S_{r,s}[x;y]=\mathbb C[p_0,p_1,\dots]$, and its consequence, Corollary 2.9: every $p(L_1,\dots,L_{r+s})$ with $p$ supersymmetric is central, for every $\delta$.
4. Separation: Lemma 2.11 (generating functions), the semisimplicity criterion Proposition 1.1, and Lemma 2.12 (supersymmetric polynomials separate the content vectors).
5. Central characters: Lemma 3.2, Proposition 3.1 and Corollary 3.3, by which $f(L_1,\dots,L_{r+s})$ acts on $C_{r,s}(\lambda)$ as $f(c(\lambda,1),\dots,c(\lambda,r+s))$.
6. Counting: Lemma 3.4 (a nonsingular evaluation matrix) and $\dim Z(B_{r,s}(\delta))=|\dot\Lambda_{r,s}|$ in the semisimple case.

Significance

The theorem gives an explicit generating set for the center of a semisimple walled Brauer algebra, parallel to the symmetric-group case. Its consequences in the paper include a description of the Gelfand–Zetlin subalgebra and formulas for primitive idempotents (§4), an alternative proof of the block classification of Cox et al. (§5), and, via the same method, the center of the quantized walled Brauer algebra (§6). Corollary 2.9 alone, valid for every $\delta$, provides a supply of central elements whose action on each cell module is computed by Corollary 3.3.

The theorem is proved in the paper; no part of it is formalized. A formalization would supply machine-checked Jucys–Murphy relations for a diagram algebra built on a published, generic encoding of walled Brauer diagrams, a Lean development of supersymmetric polynomials (including Stembridge's theorem, absent from Mathlib), and a reusable dimension count for centers of semisimple algebras in terms of simple modules.

Difficulty

The inclusion of the supersymmetric polynomials in the center (Corollary 2.9) reduces to diagram relations plus Stembridge's theorem; the latter is a nontrivial statement about polynomial rings, with no counterpart in Mathlib. The reverse inclusion is the harder half. A central element is not visibly a polynomial in the $L_k$: the argument must show that enough linearly independent central elements of the form $p(L_1,\dots,L_{r+s})$ exist, which requires computing their scalars on every cell module (an explicit cellular computation involving the arc elements $\tau_t$), separating all content vectors (where semisimplicity enters through the criterion of Cox et al.), and comparing with $\dim Z$, which needs Wedderburn–Artin together with the classification of simple modules. Separation genuinely fails outside the semisimple range, so no argument independent of $\delta$ can work.

Formalization scope

The algebra, diagrams, cell modules $C_{r,s}(\lambda)$, the index sets $\Lambda_{r,s}$ (CellIndex) and $\dot\Lambda_{r,s}$ (Label) and contents are the published definitions WalledBrauer_Blocks_{Diagram, Algebra, ModuleTheory, Partitions, CellModules}, used as references. New definitions are in WalledBrauer.Center.Setting. Conventions:

• The base field is $\mathbb C$; $r,s$ are arbitrary natural numbers, including $0$; $\delta\in\mathbb C$ is arbitrary.
• Vertices are 0-based (Fin (r + s)); the paper's $L_k$ is jm δ ⟨k-1, _⟩.
• The published algebra multiplies diagrams with the left factor on top, the opposite of the paper's convention. One-sided relations are transcribed literally with the platform's product; each is the image of the paper's relation under the up–down flip, an anti-automorphism fixing every $(a,b)$, $e_{j,k}$, $L_k$ and $\tau_t$. The center, generated subalgebras, semisimplicity and central characters do not depend on the convention.
• Polynomials are MvPolynomial (Fin r ⊕ Fin s) ℂ. The evaluation $p(L_1,\dots,L_{r+s})$ is defined monomial by monomial in increasing vertex order, without assuming that the $L_k$ commute; it is never routed through a commutative subalgebra.
• The cancellation property is vacuous when $r=0$ or $s=0$. Semisimplicity is IsSemisimpleRing, the center is Subalgebra.center ℂ, "generate" is Algebra.adjoin ℂ. In Proposition 1.1, $r+s-2$ is real.
• Lemma 2.11's equality of rational functions is stated cross-multiplied in $\mathbb C[z]$.

Supersymmetry is defined intrinsically on polynomials, never through the algebra, so neither inclusion of the goal holds by definition; stating only $\subseteq$ or only $\supseteq$ as the goal is excluded.

Proofs of any milestone are welcome, as are reusable developments of supersymmetric polynomials (Stembridge's theorem, elementary supersymmetric polynomials) and of the center of a split semisimple algebra.

Selected references

• J. H. Jung and M. Kim, Supersymmetric polynomials and the center of the walled Brauer algebra, arXiv:1508.06469v2, 2017. https://arxiv.org/abs/1508.06469
• A. Cox, M. De Visscher, S. Doty and P. Martin, On the blocks of the walled Brauer algebra, J. Algebra 320 (2008), 169–212. https://arxiv.org/abs/0709.0851
• J. Brundan and C. Stroppel, Gradings on walled Brauer algebras and Khovanov's arc algebra, Adv. Math. 231 (2012), 709–773. https://arxiv.org/abs/1107.0999
• A. Sartori and C. Stroppel, Walled Brauer algebras as idempotent truncations of level 2 cyclotomic quotients, J. Algebra 440 (2015), 602–638. https://arxiv.org/abs/1411.2771
• J. R. Stembridge, A characterization of supersymmetric polynomials, J. Algebra 95 (1985), 439–444. https://mathscinet.ams.org/mathscinet-getitem?mr=801279
• Y. Li, Jucys–Murphy elements and centres of cellular algebras, Bull. Aust. Math. Soc. 85 (2012), 261–270. https://mathscinet.ams.org/mathscinet-getitem?mr=2891540
• G. E. Murphy, The idempotents of the symmetric group and Nakayama's conjecture, J. Algebra 81 (1983), 258–265. https://mathscinet.ams.org/mathscinet-getitem?mr=696137