All missions

Decision making with uncertain transitions

A routing decision can have a known immediate cost while its consequences depend on uncertain weather. A controller observes the current state, chooses an action, and then faces a random next state. A policy optimized for one estimated transition model may perform poorly when those estimates change. Chapter 13 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization studies this issue through finite-state control problems and illustrates it with aircraft routing. The mathematical target here is the finite-horizon theorem that evaluates and optimizes policies against admissible changes in transition probabilities.

The uncertainty model matters. Requiring nature to use one fixed transition matrix throughout the horizon couples its choices across time. Allowing each time, state and action to have its own admissible probability row gives a different problem. The latter is the setting of this mission and of the chapter's robust Bellman recursion. No assertion of exact solution of the stationary-uncertainty problem is included.

Finite states, actions, and independent uncertainty rows

Let the state space be a finite nonempty set $X$, and let the action space be a finite nonempty set $A$, available in every state. The decision times are $T=\{0,\ldots,N-1\}$, with terminal time $N$. A deterministic Markov policy $u$ assigns an action $u_t(i)$ to every time $t$ and state $i$. The stage cost $c_t(i,a)$ and terminal cost $c_N(i)$ are real numbers; they need not be nonnegative. The initial state has a given probability distribution $q_0$.

A transition row $p_{ti}^a$ gives the probabilities of the next state, conditional on time $t$, current state $i$, and action $a$. For fixed policies, distributions evolve according to

$$q_{t+1}(j)=\sum_{i\in X}q_t(i)p_{ti}^{u_t(i)}(j).$$

The expected total cost is defined from these forward distributions:

$$C_N(u,p)=\sum_{t=0}^{N-1}\sum_{i\in X}q_t(i)c_t(i,u_t(i))+\sum_{i\in X}q_N(i)c_N(i).$$

For robust control, every row belongs to a nonempty closed set $P_{ti}^a$ in the probability simplex. Rectangular uncertainty means that nature's admissible policies are the entire product of these sets: choices at different times, states and actions are independent constraints. The sets themselves may depend on time and need not be convex. These are the standing assumptions of Sections 13.2–13.3 of the book.

Formalization targets

The first supporting target is Theorem 13.1.2. For a fixed controller and fixed transition rows, the expected cost equals the attained maximum of the linear program with terminal vector $v_N=c_N$ and inequalities

$$v_t(i)\le c_t(i,u_t(i))+\sum_jp_{ti}^{u_t(i)}(j)v_{t+1}(j),$$

whose objective is $q_0^Tv_0$. The second target, Theorem 13.1.4, is the nominal Bellman theorem: the recursion that minimizes the corresponding one-step expression over actions gives the optimal remaining cost at every time and state, and greedy policies for its values are optimal.

The goal is the full Theorem 13.3.1. With $v_N=c_N$, define

$$v_t(i)=\min_{a\in A}\left[c_t(i,a)+\max_{p\in P_{ti}^a}\sum_jp(j)v_{t+1}(j)\right].$$

Then $v_t(i)$ is the minimum worst-case remaining expected cost starting at state $i$ at time $t$, and

$$\min_u\max_p C_N(u,p)=q_0^Tv_0.$$

The target includes existence of controller policies choosing the displayed minimizing actions and nature policies choosing maximizing rows. Every such controller is optimal, and corresponding maximizing rows realize its worst cost. For any fixed controller $u$, the separate evaluation recursion

$$v_N^u=c_N,\qquad v_t^u(i)=c_t(i,u_t(i))+\max_{p\in P_{ti}^{u_t(i)}}p^Tv_{t+1}^u$$

must give its attained worst expected remaining cost, including the total value $q_0^Tv_0^u$.

What the results establish

These statements connect three different objects: a forward stochastic evolution, optimization over complete policies, and backward value calculations. The robust theorem supplies both an optimal decision rule and an evaluation of uncertainty for a prescribed rule. Keeping the initial distribution arbitrary retains the distinction between statewise values and the value of the original control problem.

The results are established mathematics in the source; the work requested is their formal verification. A related proved robust-DP theorem uses time-independent uncertainty sets, nonnegative stage costs and a fixed initial state. This mission preserves the book's different data and attainment conclusions. Its local statements are open proof targets, not completed Lean proofs.

Difficulty

The central issue is relating the independent forward cost to the policy optimization and preserving all attainments. Choosing an individually favorable action does not by itself establish optimality over complete policies. Likewise, replacing a maximum by a real supremum leaves the existence of a maximizing nature policy unresolved. Closedness of the row sets and their probability constraints are substantive assumptions here. The fixed-policy and optimizing recursions must also be distinguished: nature's worst choices for an arbitrary controller need not be the rows selected from the optimal value function.

Formalization scope

States, actions and decision times use finite index types, with nonempty state and action spaces. All costs and probabilities are real. Probability vectors have nonnegative coordinates summing to one. The model retains arbitrary initial distributions, time-dependent uncertainty sets and terminal costs. A zero horizon has no decisions and yields terminal expected cost.

The definition bundle includes forward distributions, expected costs, both Bellman recursions, the independent worst-cost function, and the policy-selection predicates. The theorems compare these independently defined quantities, rather than defining expected cost to be the desired Bellman value. Extrema use attained order predicates, with internal suprema restricted to the admissible nature policies. Full-horizon policies encode suffix policies by ignoring coordinates before the starting time.

Formalization Note Each theorem carries its needed concrete definitions in a separate namespace so it compiles without importing unpublished drafts. The definition item records the common reusable interface. Equation (13.1.3) supplies the forward-distribution definition rather than a tautological milestone. The nominal LP Theorem 13.1.3 is not a dependency in this selected route; its printed index and arbitrary-optimizer issues are recorded locally. No corrected or strengthened variant is posed.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009, Chapter 13, especially Theorems 13.1.2, 13.1.4 and 13.3.1, printed pp. 345–346 and 350. DOI.

Motivation

A quantum circuit normally applies a sequence of gates to a prepared state. Verstraete, Wolf and Cirac proposed a different physical route: couple a quantum system to a memoryless environment so that dissipation drives it toward a state recording the circuit's computation. Their dissipative quantum computation construction places a clock beside the computational qubits and makes the circuit history a stationary state of a time independent master equation. A useful process must have a well identified stationary state and a rate of relaxation that does not collapse with the number of qubits or with the chosen gates. The paper argues for these properties in its DQC section and its efficiency appendix (Verstraete, Wolf and Cirac, 2008, pp. 1–2, 4–5).

The printed spectral gap formula and part of its supporting clock block do not describe the slowest decay of the stated generator. Direct finite dimensional calculations reveal a slower coherence sector. This mission therefore targets the stated stationary state and a corrected, explicitly ranged version of the paper's lower bound. The discrepancies and boundary cases are recorded in the formalization scope so that the target is a mathematical claim about the displayed Lindblad operators rather than an unchecked transcription.

Setting

Fix $N\geq 0$ qubits and $T\geq 0$ circuit steps. A computational basis string is a function from the $N$ qubit positions to $\{0,1\}$. The clock register has basis $|t\rangle$ for $t=0,\ldots,T$. A family of unitary gates $U_1,\ldots,U_T$ acts on the qubit register. Its history vectors are $|\psi_0\rangle=|0\cdots0\rangle$ and $|\psi_t\rangle=U_t\cdots U_1|0\cdots0\rangle$.

A jump operator resets qubit $i$ only when the clock is at zero: $L_i=|0\rangle_i\langle1|\otimes|0\rangle\langle0|$. For each neighboring clock pair, another jump operator moves in both directions, applying the relevant gate on the forward move and its adjoint on the reverse move. The Lindblad generator is the linear map on matrices

$$\mathcal L(\rho)=\sum_k\left(L_k\rho L_k^\dagger-\frac12(L_k^\dagger L_k\rho+\rho L_k^\dagger L_k)\right).$$

There is no Hamiltonian term. The proposed history state is the normalized density matrix

$$\rho_0=\frac1{T+1}\sum_{t=0}^{T}|\psi_t\rangle\langle\psi_t|\otimes|t\rangle\langle t|.$$

These are equations (1)–(4) of the paper, with the clock step index repaired as described below. The appendix introduces a gate removal unitary $W$, a connected clock path matrix $L_{00}$, and clock blocks with a penalty at time zero. Their spectra lead to the uniqueness and decay claims (paper, pp. 2, 4–5).

Formalization targets

Main goal

For every $N\geq0$, $T\geq2$, and family of unitary gates, prove that $\mathcal L(\rho_0)=0$, that $\rho_0$ is positive semidefinite with trace one, and that the full kernel of $\mathcal L$ consists of scalar multiples of $\rho_0$. For $T\geq5$, prove additionally that every nonzero eigenvalue $\mu$ satisfies

$$\operatorname{Re}(\mu)<-\frac1{T^2}.$$

The bound applies uniformly across the number of qubits and the circuit gates. It is the corrected form of the efficiency conclusion on p. 5. The goal does not assert the printed formula $\Delta=\pi^2/(2T+3)^2$, which is contradicted by the slowest coherence sector (paper, pp. 2, 5).

Supporting targets

The milestones first establish stationarity and removal of the circuit gates by $W$. They then target the one dimensional fixed space for identity gates, the first nonzero eigenvalue of the connected clock path, the penalized clock blocks, and the full generator's bound for identity gates. This follows the sequence of reductions described in the efficiency appendix while retaining the paper's exact clock constants where they are valid (paper, pp. 4–5).

Significance

The kernel statement identifies every stationary matrix, a stronger assertion than merely finding one stationary density matrix. The eigenvalue bound supplies a uniform spectral scale for the finite dimensional generator, independent of the circuit content. Together these make precise the part of dissipative computation that says the intended history is singled out and spectrally separated from other modes. A convergence time theorem would also have to control Jordan blocks or the operator semigroup and is outside this target; the paper itself notes this separate issue on p. 5 (paper, p. 5).

Formalizing the corrected claim creates a reusable finite matrix representation of a Lindblad generator and a circuit clock, plus independently usable path and boundary penalty spectral statements. The paper result is known in physics prose; these exact Lean statements are open proof goals in this proposal. The correction also prevents later arguments from importing a spectral equality that does not hold for the displayed process.

Difficulty

The gate operators couple the qubit register to the clock, so diagonalizing a clock matrix alone does not describe the generator. Even after the gates are removed, the Liouvillian acts on matrices, including coherences between two qubit states and two clock times. The decay of a one sided coherence at clock zero carries half the penalty of a population term. Reading every nonzero sector as if it had the population penalty produces the printed gap value and misses the slowest mode. The clock path also has to retain the first edge and its endpoint diagonal entries; omitting that edge changes the spectrum.

Formalization scope

Lean uses matrices indexed by $N$ bit strings paired with the finite clock $\{0,\ldots,T\}$, and a complex linear endomorphism on those matrices. Gates are quantified as unitary matrices; they may act on all qubits, whereas the paper starts with nearest neighbor gates. The appendix's spectral argument is independent of that locality, so this is a disclosed generalization. The model also permits $N=0$. Gates use zero based indexing: Lean's $U(t)$ is the paper's $U_{t+1}$ and acts on the step $t\to t+1$. This repairs equation (3), which otherwise calls for both an undefined $U_0$ and an out of range clock state $|T+1\rangle$.

Uniqueness is restricted to $T\geq2$: at $T=1$ an additional clock coherence is stationary. The strict $1/T^2$ bound is restricted to $T\geq5$: direct diagonalization shows it fails for $T=1,2,3,4$. The paper's printed corner coefficient $-2$ is correct for a population sector, but a one sided coherence has coefficient $-3/2$. A milestone states the valid printed matrix fact and the corrected bound for all clock zero penalties $a\geq1/2$. The connected path matrix follows the displayed spectral formula rather than the printed tridiagonal sum whose range omits the first edge.

The generator is defined from the jump operators by equation (1). It is not defined from the desired block decomposition or eigenvalues. The spectral assertion quantifies over actual nonzero complex eigenvalues and compares their real parts directly; no default valued infimum defines a gap. Work toward the mission may supply matrix identities, unitary covariance, tridiagonal spectra, or a direct finite dimensional analysis of the generator. The generic finite matrix Lindblad definition can be reused independently of this circuit model.

Selected references

• Frank Verstraete, Michael M. Wolf, and J. Ignacio Cirac, Quantum computation, quantum state engineering, and quantum phase transitions driven by dissipation, arXiv:0803.1447v2, 2008; later Nature Physics 5, 633–636 (2009). Pinned preprint.

Motivation

Many constructions in differential topology and infinite-dimensional Lie theory start from a continuous object and need a smooth one: a continuous section of a smooth bundle, a continuous map into a manifold, a continuous homotopy between smooth maps. Steenrod's approximation theorem (Steenrod 1951, §6.7) says that, for finite-dimensional bundles, a continuous section can be smoothed by a small homotopy through sections, without changing it where it is already smooth. Hirsch's textbook (Hirsch 1976, Ch. 2) gives the relative version for maps between finite-dimensional manifolds.

Gauge theory and the study of principal bundles whose structure group is an infinite-dimensional Lie group (current groups, diffeomorphism groups, gauge groups) need the same statement when the typical fibre is infinite-dimensional. C. Wockel (arXiv:math/0610252, 2006) proves it for a finite-dimensional base with corners and a fibre that is a manifold modelled on a locally convex space, combining Steenrod's argument with Neeb's approximation results for maps into locally convex spaces (Neeb 2002, App. A.3). The consequences in the paper are that smooth and continuous homotopy classes of sections, and of maps from a finite-dimensional manifold into a locally convex manifold, coincide; this is used in bundle theory for infinite-dimensional structure groups (Müller–Wockel 2006, cited as [MW06] in the paper).

Setting

A manifold with corners $M$ is a Hausdorff paracompact space with charts onto open subsets of the quadrant $\mathbb R^d_+ = \{x \in \mathbb R^d : x_i \ge 0\}$ and smooth coordinate changes. A locally convex manifold $N$ is a Hausdorff space with charts onto open subsets of a locally convex space and smooth coordinate changes, where smoothness of $f : U \to Y$ means that all iterated directional derivatives exist and are continuous (Definition 0.1 of the paper).

A map $\pi : E \to M$ is a locally trivial smooth bundle with typical fibre $N$ if every point of $M$ has an open neighbourhood $S$ and a diffeomorphism $\varphi : \pi^{-1}(S) \to S \times N$ with $\mathrm{pr}_1 \circ \varphi = \pi$. A section is a continuous map $\sigma : M \to E$ with $\pi \circ \sigma = \mathrm{id}_M$. A map is smooth on a neighbourhood of a set $s$ if it is smooth on some open set containing $s$.

For spaces $X, Y$, $C(X, Y)_{c.o.}$ is the space of continuous maps with the compact-open topology, generated by the sets $\lfloor C, W\rfloor = \{f : f(C) \subseteq W\}$ with $C$ compact and $W$ open.

Formalization targets

Goal: Theorem 0.11 (Generalised Steenrod Approximation Theorem)

Let $M$ be finite-dimensional and connected, $\pi : E \to M$ a locally trivial smooth bundle with typical fibre $N$, $\sigma$ a continuous section, $L \subseteq M$ closed, $U \subseteq M$ open, and $\sigma$ smooth on a neighbourhood of $L \setminus U$. Then for every open $O \supseteq \sigma(M)$ there are a section $\tau$ and a homotopy $H$ with

$$\tau(M) \subseteq O,\quad \tau \text{ smooth on a neighbourhood of } L,\quad \tau|_{M \setminus U} = \sigma|_{M \setminus U},$$ $$H : [0,1] \times M \to O,\quad H(0,\cdot) = \sigma,\ H(1, \cdot) = \tau,\quad \pi \circ H(t, \cdot) = \mathrm{id}_M,\quad H(t,x) = \sigma(x) \text{ for } x \notin U.$$

Milestones

1. Remark 0.4: a connected paracompact finite-dimensional manifold with corners is σ-compact.
2. Proposition 0.7: $C^\infty(M, Y)$ is dense in $C(M, Y)_{c.o.}$, with support control for compactly supported maps.
3. Corollary 0.8: $C^\infty(M, V)$ is dense in $C(M, V)_{c.o.}$ for $V \subseteq Y$ open.
4. Lemma 0.9: relative smoothing of $f : M \to W$, $W \subseteq Y$ open convex, within any compact-open neighbourhood, keeping $f$ off $U$.
5. Lemma 0.10: the same for maps into a subset $W \subseteq N$ diffeomorphic to an open convex subset of the model space.
6. Sections versus fibre maps (proof of Theorem 0.11, p. 5): over a smooth trivialisation $\varphi$, a section $\sigma'$ is smooth near $x$ if and only if $\mathrm{pr}_2 \circ \varphi \circ \sigma'$ is.

Significance

The result. The theorem turns continuous sections into smooth ones by homotopies that are small (they stay in any prescribed open set $O$ around the section) and relative (fixed where nothing needs changing). It yields that $C^\infty(M, N)$ is dense in $C(M, N)$ for the graph and compact-open topologies (Corollary 0.12), that every continuous section is homotopic to a smooth one and continuously homotopic smooth sections are smoothly homotopic (Proposition 0.13), and that smooth and continuous homotopy classes $[M, N]$ agree (Corollary 0.14). These are the statements needed to compare smooth and topological classification of bundles with infinite-dimensional structure groups.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. Mathlib has smooth partitions of unity on finite-dimensional manifolds with corners and local-to-global smoothing for maps into convex sets, but no density of $C^\infty(M, Y)$ in $C(M, Y)$ for the compact-open topology, no relative smoothing lemma, and no smoothing of sections of non-vector bundles. A formalization would supply these as reusable statements about Mathlib's ContMDiff, Bundle.Trivialization and C(M, Y).

Difficulty

The obvious argument glues local smoothings with a partition of unity, as for real-valued functions. This fails for sections of a non-linear bundle: convex combinations of points of $E$, or of $N$, are meaningless, so a partition-of-unity average of local smoothings is not a section, and the smoothing cannot be done in one global step. Any stepwise replacement must keep the section inside the prescribed open set $O$, must not destroy smoothness already achieved near earlier parts of $L$, and must avoid convergence arguments, since infinitely many steps are needed on a non-compact $M$. The homotopy has to be continuous at the end where infinitely many steps accumulate. Finally, an infinite-dimensional $N$ is not locally compact, so all compactness must come from $M$; this is why the base is finite-dimensional while the fibre is not.

Formalization scope

• Normed models. Mathlib's manifolds require a normed model space, so $N$ is modelled (without boundary) on a real normed space $F$, not necessarily complete or finite-dimensional, and the total space $E$ is a manifold with corners modelled on a real normed space; in Proposition 0.7, Corollary 0.8 and Lemma 0.9 the target $Y$ is a real normed space. On normed spaces the paper's smoothness coincides with Fréchet $C^\infty$, Mathlib's ContMDiff … ∞ (not the analytic ω). This is the one specialisation of the paper; non-normable locally convex fibres are out of scope.
• The base. $M$ carries any finite-dimensional Mathlib model with corners $I$ (which contains the quadrant $\mathbb R^d_+$), with [T2Space M], and [ParacompactSpace M] (Theorem 0.11, Remark 0.4, milestone 6) or [SigmaCompactSpace M] (Proposition 0.7, Corollary 0.8, Lemmas 0.9, 0.10), as Definition 0.3 and the statements require; Theorem 0.11 adds [ConnectedSpace M]. $N$ is [T2Space N].
• Conventions. "Smooth on a neighbourhood of $s$" is $C^\infty$ on an open set containing $s$ (SmoothNear), not smoothness on $s$ itself. Spaces $C(M, W)$ for $W \subseteq Y$ or $W \subseteq N$ are maps into the subtype with the compact-open topology, so neighbourhoods are taken in $C(M, W)$. A bundle is given by smooth Bundle.Trivializations covering $M$; "$W$ diffeomorphic to an open convex subset of $F$" is a partial diffeomorphism $N \to F$ with source $W$ and convex target. The homotopy is indexed by unitInterval and runs from $\sigma$ at $0$ to $\tau$ at $1$. "Support" is the closed support tsupport.
• No trivial reading. The goal must not be read with smoothness on $L$ only (which is weaker for closed $L$), with $O$ replaced by all of $E$, or with a trivial bundle or finite-dimensional fibre; a sanity file checks that the hypotheses are satisfiable on the product bundle $\mathbb R \times \mathbb R \to \mathbb R$.
• What a development needs. Smooth partitions of unity on $M$ (in Mathlib), local compactness and σ-compactness of $M$, the compact-open topology on $C(M, W)$ and continuity of the operations $\gamma \mapsto \lambda\gamma + (1-\lambda)f$ on it, and the gluing of sections along locally finite covers. Proofs of Proposition 0.7 and Lemma 0.9 are reusable beyond this mission; contributions proving any milestone, or the Mathlib-level density results, are welcome.

Selected references

• C. Wockel, A Generalisation of Steenrod's Approximation Theorem, preprint arXiv:math/0610252v1, 2006. https://arxiv.org/abs/math/0610252
• N. Steenrod, The Topology of Fibre Bundles, Princeton University Press, 1951, §6.7. https://doi.org/10.1515/9781400883875
• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer, 1976, Ch. 2. https://doi.org/10.1007/978-1-4684-9449-5
• K.-H. Neeb, Central extensions of infinite-dimensional Lie groups, Ann. Inst. Fourier 52 (2002), App. A.3 (cited as [Ne02]).
• C. Müller, C. Wockel, Equivalences of smooth and continuous principal bundles with infinite-dimensional structure group, preprint, 2006 (cited as [MW06]).
• J. Dugundji, Topology, Allyn and Bacon, 1966, Theorems XI.7.2–3.

Motivation

The Lie superalgebra $\widehat{\mathfrak{gl}}_{\infty|\infty}$, a central extension of the Lie superalgebra of infinite matrices of finite support, appears in the representation theory of the $W_{1+\infty}$ vertex algebra and in Howe-type dualities with $\mathfrak{gl}_n$ (Kac–Radul; Cheng–Lam). Its irreducible quasi-finite highest weight modules of positive integral level $n$ are indexed by generalized partitions $\lambda=(\lambda_1\ge\cdots\ge\lambda_n)\in\mathbb Z^n$, and their characters had been computed by Cheng and Lam in terms of hook Schur functions and Littlewood–Richardson coefficients.

J.-H. Kwon (arXiv:math/0605005) gave these characters a tableau model. He introduced A/B-semistandard tableaux, pairs of super-semistandard tableaux attached to a generalized partition, showed that their generating function $S^{\mathcal A/\mathcal B}_\lambda$ is the character in question (Theorem 5.2), and developed an insertion scheme that yields an RSK correspondence, a Littlewood–Richardson rule, and a Jacobi–Trudi type determinant formula (Theorem 4.5). The paper notes that this determinant formula for the characters of $\widehat{\mathfrak{gl}}_{\infty|\infty}$-modules had not been observed before. The combinatorics rests on Stembridge's rational semistandard tableaux (1987), which model the rational representations of $\mathfrak{gl}_n$, and on Berele–Regev's hook Schur functions (1987).

Setting

Let $\mathcal A$ and $\mathcal B$ be linearly ordered, at most countable sets, each split into even and odd letters, $\mathcal A=\mathcal A_0\sqcup\mathcal A_1$.

A filling $T$ of a skew Young diagram with letters of $\mathcal A$ is $\mathcal A$-semistandard if its entries weakly increase along rows and down columns, even letters strictly increase down columns, and odd letters strictly increase along rows. The weight of $T$ records how many times each letter occurs, and $x^T_{\mathcal A}=\prod_a x_a^{m_a}$.

A generalized partition of level $n\ge1$ is $\lambda\in\mathbb Z^n_+=\{\lambda_1\ge\cdots\ge\lambda_n\}$. It is drawn against a vertical line: row $k$ has $\lambda_k$ boxes to the right of the line if $\lambda_k\ge0$ and $|\lambda_k|$ boxes to the left if $\lambda_k<0$.

An A/B-semistandard tableau of shape $\lambda$ is a pair $(T^+,T^-)$ with $T^+\in SST_{\mathcal A}((\lambda+(d^n))/\mu)$ and $T^-\in SST_{\mathcal B}((d^n)/\mu)$ for some $d\ge0$ and partition $\mu\subset(d^n)$, $\mu\subset\lambda+(d^n)$. Both tableaux are drawn against the line of $\lambda$, so enlarging $d$ by one and $\mu$ by a full column gives the same pair. The character is

$$S^{\mathcal A/\mathcal B}_\lambda=\sum_{(T^+,T^-)\in SST_{\mathcal A/\mathcal B}(\lambda)}x^{T^+}_{\mathcal A}\big(x^{T^-}_{\mathcal B}\big)^{-1}\in\mathbb Z[[x_{\mathcal A},x_{\mathcal B}^{-1}]],$$

a power series in the symbols $x_a$ and $x_b^{-1}$. At level one, $S^{\mathcal A/\mathcal B}_k$ is defined for every $k\in\mathbb Z$, negative $k$ included.

A rational $[n]$-semistandard tableau of shape $\lambda$ fills the diagram of $\lambda$ with $1,\dots,n$ right of the line and $-n,\dots,-1$ left of it, rows weakly and columns strictly increasing, subject to Stembridge's compatibility condition between columns $1$ and $-1$. Its content $\nu$ has $\nu_k=m_k-m_{-k}$, and $K_{\lambda\mu}$ counts the tableaux of shape $\lambda$ and content $\mu$.

Formalization targets

Goal: Theorem 4.5

For infinite $\mathcal A$, $\mathcal B$ and every $\lambda\in\mathbb Z^n_+$, $n\ge1$,

$$S^{\mathcal A/\mathcal B}_\lambda=\det\Big(S^{\mathcal A/\mathcal B}_{\lambda_i-i+j}\Big)_{1\le i,j\le n}.$$

The entries are level-one A/B-characters, not complete symmetric functions. Unlike $h_k$, they do not vanish for $k<0$.

Milestones

1. Each coefficient of (3.14) counts finitely many tableaux.
2. Lemma 3.3: the map $\sigma: SST_{[n]}(\lambda)\to SST_{[n]}(\lambda+(1^n))$ is a bijection; it shifts content by $(1^n)$.
3. (4.3): $K_{\lambda\mu}=K_{\lambda+(d^n)\,\mu+(d^n)}$, and $K_{\lambda\mu}=0$ unless $\lambda\ge\mu$ lexicographically.
4. Corollary 4.4: a weight-preserving bijection $\prod_i SST_{\mathcal A/\mathcal B}(\nu_i)\cong\bigsqcup_\mu SST_{\mathcal A/\mathcal B}(\mu)\times SST_{[n]}(\mu)_\nu$.
5. The expansion $H^{\mathcal A/\mathcal B}_\mu=\prod_i S^{\mathcal A/\mathcal B}_{\mu_i}=\sum_{\langle\lambda\rangle=\langle\mu\rangle}K_{\lambda\mu}S^{\mathcal A/\mathcal B}_\lambda$ (proof of Theorem 4.5).
6. (4.5): $h_\mu=\sum_{\lambda\ge\mu}K_{\lambda\mu}s_\lambda$ and $s_\lambda=\det(h_{\lambda_i-i+j})$ in $n$ variables.
7. Lemma 3.17: the $S^{\mathcal A}_\lambda$, $\lambda\in\mathscr P_{\mathcal A}$, are linearly independent.
8. Remark 3.19: infinite combinations of $S_\lambda(x_{\mathcal A})S_\mu(x_{\mathcal B}^{-1})$ converge and have unique coefficients.
9. Proposition 3.20: $S_\lambda(x_{\mathcal A},x_{\mathcal B})=\sum_{\mu,\nu\in\mathscr P_n}c^\lambda_{\mu\nu^*}S_\mu(x_{\mathcal A})S_\nu(x_{\mathcal B}^{-1})$.
10. Corollary 3.23: infinite combinations $\sum_\lambda a_\lambda S^{\mathcal A/\mathcal B}_\lambda$ at a fixed level converge and have unique coefficients.

Significance

The result. Theorem 4.5 is the super, rational analogue of the Jacobi–Trudi identity. Through Theorem 5.2 it becomes a determinant formula for the characters of the irreducible quasi-finite $\widehat{\mathfrak{gl}}_{\infty|\infty}$-modules of positive level (Corollary 5.4). Specialising $\mathcal A$ and $\mathcal B$ recovers formulas for $\widehat{\mathfrak{gl}}_\infty$ and for the $(\mathfrak{gl}_{p|q},\mathfrak{gl}_n)$ Howe duality. Milestones 2–6 develop the rational Kostka theory along the way: its shift invariance, its triangularity, and its role in an RSK correspondence for A/B-tableaux.

Formalizing it. The theorem is proved in the paper; nothing in it has a machine-checked proof. Mathlib has semistandard Young tableaux and symmetric polynomials, but no Schur polynomials as tableau generating functions, no Kostka numbers, no RSK, and no classical Jacobi–Trudi identity. Milestone 6 is therefore new to formal mathematics in its own right, and it is a prerequisite for the goal's proof.

Difficulty

The obvious attack proves the classical Jacobi–Trudi identity once and then transfers it. That fails here for two reasons. The entries $S^{\mathcal A/\mathcal B}_k$ with $k<0$ are nonzero, so the classical vanishing $h_k=0$ that truncates the determinant is unavailable. And the expansion $H^{\mathcal A/\mathcal B}_\mu=\sum K_{\lambda\mu}S^{\mathcal A/\mathcal B}_\lambda$ is an infinite sum over generalized partitions, so the comparison with (4.5) leaves an error term supported on $\mathbb Z^n_+\setminus\mathscr P_n$. Killing it requires both the shift invariance of the rational Kostka numbers and the uniqueness of coefficients in infinite combinations (Corollary 3.23). The combinatorial input, Corollary 4.4, is a weight-preserving insertion bijection for pairs of super tableaux, built from row and column insertion, rectangular complements and Stroomer's theorem. Each of these is substantial to formalize.

Formalization scope

• Namespace and definitions. Everything is in SuperTableaux.JacobiTrudi, with one definitions item.
• Letters and grading. Letters are types with LinearOrder and Countable; the grading is a function odd : A → Bool, where true means odd.
• Characters. Characters live in MvPowerSeries (A ⊕ B) ℤ. The variable Sum.inl a is $x_a$ and Sum.inr b is the symbol $x_b^{-1}$, which is literally the ring $\mathbb Z[[x_{\mathcal A},x_{\mathcal B}^{-1}]]$. The coefficient at a monomial is Nat.card of the set of tableaux of that weight; milestone 1 proves that set finite.
• Cut coordinates. A/B-tableaux are stored in cut coordinates: the class of $(d,\mu)$ is the antitone vector $c=\mu-(d^n)$, so each pair of tableaux is counted once.
• Rows and order. Rows are $0$-based. The order on $\mathbb Z^n_+$ is Mathlib's lexicographic order toLex, which is the paper's "reverse lexicographic ordering" of p. 23.
• Infinite sums. These are HasSum/Summable in the coefficientwise topology, never tsum.
• Bijections. Lemma 3.3 is stated for the paper's map $\sigma$, written out as a definition; it also records the content shift of p. 23. Corollary 4.4 asserts a bijection preserving the A/B-weight (the weight clause of Corollary 4.3); the insertion map $\kappa_{\mathcal A/\mathcal B}$ itself is not written out.

A formalization that defines $S^{\mathcal A/\mathcal B}_\lambda$ by a determinant or product formula, sums over $(d,\mu)$ without the identification (every coefficient becomes Nat.card of an infinite set, i.e. $0$), or drops the parity conditions trivializes the goal; the definitions here are the tableau generating functions of (3.13)–(3.14).

A complete development needs Kostka numbers, Schur polynomials as tableau generating functions, the classical Jacobi–Trudi identity, RSK for super tableaux, and coefficientwise convergence in multivariate power series. All of these are reusable beyond this mission. Contributions are welcome on any milestone, and on intermediate lemmas such as the classical Jacobi–Trudi identity.

Selected references

• J.-H. Kwon, Rational semistandard tableaux and character formula for the Lie superalgebra $\widehat{\mathfrak{gl}}_{\infty|\infty}$, preprint, 2006. https://arxiv.org/abs/math/0605005
• J. R. Stembridge, Rational tableaux and the tensor algebra of $\mathfrak{gl}_n$, J. Combin. Theory Ser. A 46 (1987) 79–120. https://doi.org/10.1016/0097-3165(87)90077-X
• A. Berele, A. Regev, Hook Young diagrams with applications to combinatorics and to representations of Lie superalgebras, Adv. Math. 64 (1987) 118–175. https://doi.org/10.1016/0001-8708(87)90007-7
• S.-J. Cheng, N. Lam, Infinite-dimensional Lie superalgebras and hook Schur functions, Comm. Math. Phys. 238 (2003) 95–118.
• V. G. Kac, A. Radul, Representation theory of the vertex algebra $W_{1+\infty}$, Transform. Groups 1 (1996) 41–70. https://arxiv.org/abs/hep-th/9512150
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford University Press, 1995.

Motivation

We give an overview of relative tensor products (RTPs) for von Neumann algebra modules. For background, we start with the categorical definition and go on to examine its algebraic formulation, which is applied to Morita equivalence and index. Then we consider the analytic construction, with particular emphasis on explaining why the RTP is not generally defined for every pair of vectors. We also look at recent work justifying a representation of RTPs as composition of unbounded operators, noting that these ideas work equally well for L^p modules. Finally, we prove some new results characterizing preclosedness of the map (ξ, η) \mapsto ξ\otimes_φη.

This mission is the statement-level formalization of Relative tensor products for modules over von Neumann algebras (arXiv:math/0301061v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Density of the intrinsic bounded-vector domain (§5, bounded-vector density, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 7.1 — preclosedness for two standard modules: Weight-GNS tensor map and trace-density measurable-operator calculus (hard)
• Proposition2.1: Countable standard row modules, amplification action and bounded intertwiner space (hard)
• RTPUniqueness: Canonical analytic RTP and enriched countable-sum-compatible module bifunctors (hard)
• Proposition3.2: Independent analytic Hilbert RTP and actual rectangular amplified standard L2 corner (hard)
• CorrespondencesAndSectors: Faithful normal correspondence realizations and partial-isometry sector quotient (hard)
• Proposition3.3: Entrywise normal amplification of a corner embedding and RTP composition (hard)
• Theorem4.1: Complex-linear Hilbert module categories, concrete RTP functor and unitary categorical equivalence (hard)
• Lemma4.3: Contragredient bimodule and analytic corner/standard-module identification (hard)
• Corollary4.4: Morita category, countable spatial amplification and full-support projection corners (hard)
• RTPAssociativity: Iterated analytic completion with external commuting actions (hard)
• IndexFactor: Independent factor index and dimension-monoid normalization (source-ambiguity)
• IndexGeneral: Specified normed linear domain and operator for the index spectral radius (source-ambiguity)
• BoundedVectorsIntrinsic: Coordinate bounded-strong-sum domain and transport through column-module representations (hard)
• AnalyticRTPRealizations: Positive tensor Gram form, null quotient completion and independent coordinate realization (hard)
• WeightIndependence: Analytic RTP for two faithful finite functionals and its natural unitary comparison (hard)
• OperatorComposition: True domains and closed-product convention for the density-corrected triple operator product (source-ambiguity)
• LpRTP: Complete canonical general Lp RTP construction, vector domains and topology (source-ambiguity)
• OperatorRecovery: Precise domain/closure convention for the schematic equation (7.4) (source-ambiguity)
• FiniteMeasurability: Actual closed affiliated densities, inverses and measurable closed-product algebra (hard)
• Theorem7.2: Hilbert tensor linearization and normalized atomic trace norm formula (hard)
• Proposition7.3: Central direct integral of factors and measurable fields of traces and density operators (hard)
• Proposition7.4: Weight bounded-vector domain, general analytic RTP and inverse-density criterion (hard)
• FalconeTheorem3.8: Original Falcone continuity and nondegeneracy hypotheses (source-ambiguity)

Selected references

• Relative tensor products for modules over von Neumann algebras, arXiv:math/0301061v1, https://arxiv.org/abs/math/0301061v1

Why this algebra comparison matters

The walled Brauer algebra organizes the linear operators that commute with a general linear group acting on a tensor product of vector spaces and their duals. Its diagrams mix crossings and contractions, with a wall distinguishing the two tensor factors. This makes it useful in mixed tensor representation theory, where the ordinary symmetric group algebra no longer records every commuting operator. Sartori and Stroppel compare this diagram algebra with a level-two cyclotomic quotient of a degenerate affine walled Brauer algebra. Their comparison identifies a concrete part of the larger algebra by an explicit change of generators Sartori–Stroppel, Theorem 6.2.

The paper's result is a proved theorem. This mission asks for a machine-checked proof of its algebraic statement. The source builds the cyclotomic quotient using parameters arising from parabolic category $\mathcal O$, but the target here is the resulting algebra isomorphism. The dimension comparison that the authors obtain through category $\mathcal O$ is included as a separate milestone, in the exact numerical form used in their injectivity argument Sartori–Stroppel, Theorem 5.2, Corollary 5.8, and Lemma 5.9.

The oriented generators and the cyclotomic quotient

Fix $r,t\in\mathbb N$. An orientation $a$ is a word of length $r+t$ containing exactly $r$ upward arrows and $t$ downward arrows. The walled Brauer algebra $\operatorname{Br}_{r,t}(d)$ is a complex algebra with an idempotent $1_a$ for each orientation. At an adjacent pair of positions $k,k+1$, equal arrows admit a crossing $s_k1_a$. Unequal arrows admit a changed-orientation crossing $\widehat s_k1_a$, an orientation-preserving contraction $e_k1_a$, and a changed-orientation contraction $\widehat e_k1_a$. The relations (Br1)–(Br6) specify orthogonal idempotents, sources and targets, quadratic and braid relations, and interactions among crossings and contractions Sartori–Stroppel, Definition 2.1.

The degenerate affine walled Brauer algebra adds commuting elements $y_1,\ldots,y_{r+t}$ and their relations with the oriented generators. Its level-two cyclotomic quotient imposes a quadratic relation on $y_1$ in each first-arrow component Sartori–Stroppel, Definitions 2.5 and 2.8. Write this quotient as $A$. It uses positive integers $m,n$ and an integer $\delta$, with

$$\begin{aligned} \beta_1^\uparrow&=-\delta+(m+n)/2,&\beta_2^\uparrow&=(n-m)/2,\\ \beta_1^\downarrow&=(m+n)/2,&\beta_2^\downarrow&=\delta+(m-n)/2,\\ \omega_0&=m+n,&\omega_1&=-\delta m+(m+n)^2/2. \end{aligned}$$

The later $\omega_j$ follow the quadratic recurrence determined by the upward cyclotomic polynomial; they are fixed by these parameters. These are the paper's parameters (5.4), with values in $\mathbb C$ Sartori–Stroppel, Definition 5.1 and Lemma 2.9.

For each position $k$ and orientation $a$, let $\eta_k1_a$ project away from the generalized eigenspace of $y_k1_a$ with eigenvalue $\beta_1^{a_k}$. The spectral truncation is $f1_a=\eta_1\cdots\eta_{r+t}1_a$, with $f=\sum_a f1_a$. The intermediate products are $f_k1_a=\eta_1\cdots\eta_k1_a$ and $f_0=1$. This gives the corner algebra $fAf$ Sartori–Stroppel, Definition 5.6. The elements $b_k,c_k$, polynomial square roots, and resulting images $\sigma_k,\widehat\sigma_k,\tau_k,\widehat\tau_k$ are defined by (6.1)–(6.4) Sartori–Stroppel, Definition 6.1.

Formalization targets

The goal is the full form of the paper's isomorphism theorem:

$$\Phi:\operatorname{Br}_{r,t}(-\delta)\xrightarrow{\ \sim\ }fAf, \qquad (1_a,s_k1_a,\widehat s_k1_a,e_k1_a,\widehat e_k1_a) \mapsto(f1_a,\sigma_k1_a,\widehat\sigma_k1_a,\tau_k1_a,\widehat\tau_k1_a).$$

Here $m,n>0$, $m,n\ge r+t$, and $\delta\in\mathbb Z$ satisfy Assumption 5.5: $|\beta_2^\uparrow|+r+t<\beta_1^\uparrow$ and $|\beta_2^\downarrow|+r+t<\beta_1^\downarrow$. The inequalities separate the relevant eigenvalues. The explicit $m,n\ge r+t$ condition is needed for Theorem 5.2 in the paper's dimension argument; Assumption 5.5 alone does not imply it Sartori–Stroppel, Assumption 5.5 and Theorem 5.2.

The milestone list records the finite-dimensional inverse and square-root result (Proposition 4.2), the inverse sandwich identity (Lemma 8.7), the changed contraction parameter (Lemma 8.4), the equal-orientation involution (Lemma 8.5), the Jucys–Murphy image identity (Lemma 6.6), and the dimension of the spectral corner (Corollary 5.8 with Lemma 5.9). The last two are stated in algebraic forms that avoid taking the sought map or category $\mathcal O$ as extra hypotheses.

What the result supplies

The theorem gives an explicit dictionary between diagram generators and operators in a cyclotomic quotient, including the change from the quotient's loop parameter $\omega_0=m+n$ to the source parameter $-\delta$ Sartori–Stroppel, Remark 6.3. It also identifies the whole corner, rather than merely producing a homomorphism into it. This lets properties of the larger algebra be transported to the diagram algebra when their hypotheses are met. The paper discusses graded cellular and Koszul consequences, and an oriented-category extension, separately Sartori–Stroppel, Remarks 6.4–6.5.

A formal development must establish that the presentations do not collapse, that every required oriented relation survives the generator assignment, and that the image fills precisely $fAf$. The milestone statements isolate several of the authors' central identities, while the final theorem retains injectivity and surjectivity. A proof would also create reusable infrastructure for quotient presentations with source and target idempotents and for inverses in idempotent corners.

The central difficulty

The formulas for the images involve inverses and square roots after a spectral truncation, and the quotient need not be semisimple. Substituting a scalar directly into a formal power-series identity does not justify the key contraction identity in that setting; the authors explicitly point out this obstruction Sartori–Stroppel, Remark 6.3. The oriented relations also contain dotted symbols that stand for several local choices, so a single equation between global sums does not fully state every relation. Finally, proving that the map exists is only one part of the theorem: its image and kernel require separate control.

Formalization scope

Lean represents both algebras as quotients of free complex algebras by the paper's generators and relations. An orientation is a Boolean sequence with exactly $r$ true entries; true denotes an upward arrow. Positions start at zero in Lean, so a paper index $k$ corresponds to Lean index $k-1$. Relations involving dotted generators are imposed for every composable choice with the same source and target. Invalid orientation choices are zero. The affine quotient uses $e_k^2=\omega_0e_k$; the source of the theorem uses $e_k^2=-\delta e_k$. The recurrence fixes every $\omega_j$ rather than leaving later parameters free.

The $\eta_k$, intermediate $f_k$, and $f$ are defined from the polynomial spectral-idempotent characterization, rather than supplied as arbitrary hypotheses. An inverse of $xu$ is selected by its two inverse equations in the corner $uAu$. Square roots are not unique in the source, so each theorem holds for every family $R_k$ of polynomial square roots satisfying $R_k^2=b_kf$; the factorized form $Q_k=R_{k+1}R_k^{-1}$ is used. A vacuous hypothesis, a collapsed or under-related presentation, a freely chosen $f$, or a merely linear map does not express this target. The conclusion requires multiplication, the specified generator values, injectivity, and range exactly $fAf$.

The category $\mathcal O$ construction and the paper's later applications are outside this mission. The needed reusable pieces are the finite-dimensional algebra lemma, oriented presentation machinery, polynomial spectral idempotents, and corner algebra operations. Contributions that strengthen the supporting algebraic library or close any of the stated milestones are within scope.

Selected references

• Antonio Sartori and Catharina Stroppel, Walled Brauer algebras as idempotent truncations of level 2 cyclotomic quotients, arXiv preprint, 2015. arXiv:1411.2771v2.

Motivation

The Birman–Murakami–Wenzl (BMW) algebras were introduced by Birman and Wenzl and by Murakami to study the Kauffman link polynomial; they are deformations of the Brauer algebras and act as centralizer algebras of quantum groups of orthogonal and symplectic type on tensor powers of the natural module. Their cyclotomic generalization was introduced by Häring-Oldenburg (J. Pure Appl. Algebra 161 (2001)) as the BMW analogue of the Ariki–Koike algebras, the cyclotomic Hecke algebras of type $G(r,1,n)$. Representation theorists care about when such an algebra is semisimple: in the semisimple case its representation theory is governed by a combinatorial index set (multipartitions with extra data), and outside it one needs decomposition numbers.

For the Ariki–Koike algebra the answer is Ariki's criterion (J. Algebra 169 (1994)). For the ordinary BMW algebra ($r = 1$) it is due to Rui and Si (J. Reine Angew. Math., [17] in the paper). Rui and Xu proved that the cyclotomic BMW algebra is free and cellular for odd $r$ under their u-admissibility conditions (arXiv:0801.0465), and Goodman and Hauschild Mosley (arXiv:math/0612064) and Yu (PhD thesis, Sydney, 2007) obtained freeness by other routes. Rui and Si (arXiv:0807.4149, 2008) extended cellularity to even $r$ and, by computing Gram determinants of cell modules, gave a semisimplicity criterion for all $r \ge 2$. That criterion is the goal of this mission.

Setting

Let $F$ be a field and $r, n$ positive integers. Fix non-zero $q, u_1, \dots, u_r \in F$ with $\delta = q - q^{-1} \ne 0$ and the $u_i$ pairwise distinct, and a sign $\varepsilon \in \{1, -1\}$. Put $\alpha = \varepsilon$ if $r$ is odd and $\alpha = \varepsilon q^{-\varepsilon}$ if $r$ is even, $\varrho^{-1} = \alpha\prod_\ell u_\ell$, $\gamma_r(x) = 1$ ($r$ odd), $-x$ ($r$ even), and

$$\gamma_i = \Big(\gamma_r(u_i) + \delta^{-1}\varrho(u_i^2-1)\prod_{j \ne i}u_j\Big)\prod_{j\ne i}\frac{u_iu_j - 1}{u_i - u_j},\qquad \omega_a = \sum_{j=1}^r u_j^a\gamma_j\quad(a\in\mathbb Z).$$

These are the u-admissible parameters of Assumption 2.2. The cyclotomic Birman–Wenzl algebra $\mathscr B_{r,n}$ is the unital associative $F$-algebra generated by $T_i, E_i$ ($1 \le i < n$) and $X_j^{\pm1}$ ($1 \le j \le n$) subject to the relations a)–k) of Definition 2.1: among them the Kauffman skein relation $T_i^2 - \delta T_i + \delta\varrho E_i = 1$, the braid relations, $E_i^2 = \omega_0E_i$, the skein relations between $T_i$ and $X_i, X_{i+1}$, the unwrapping relations $E_1X_1^aE_1 = \omega_aE_1$ for all $a \in \mathbb Z$, the tangle and untwisting relations, $E_iX_iX_{i+1} = E_i = X_iX_{i+1}E_i$, and the cyclotomic relation $(X_1 - u_1)\cdots(X_1 - u_r) = 0$. The Ariki–Koike algebra $\mathscr H_{r,n}$ is generated by $g_1, \dots, g_{n-1}, y_1, \dots, y_n$ with $(g_i - q)(g_i + q^{-1}) = 0$, the braid relations, $y_{i+1} = g_iy_ig_i$, commuting $y_j$ and $(y_1 - u_1)\cdots(y_1 - u_r) = 0$.

Write $o(q^2) > n$ for "$q^{2k} \ne 1$ for $1 \le k \le n$", and set

$$Q_{r,\varrho} = \begin{cases}\{-\varepsilon q, \varepsilon q^{-1}\}, & 2 \nmid r,\\ \{-q^\varepsilon, q^\varepsilon\}, & 2 \mid r,\end{cases}\qquad S_{r,\varrho} = \begin{cases}\bigcup_{k=3}^n\{\pm q^{3-k}, \pm q^{k-3}, \varepsilon q^{3-2k}, -\varepsilon q^{2k-3}\}, & 2 \nmid r,\\ \bigcup_{k=3}^n\{\pm q^{3-k}, \pm q^{k-3}, \pm q^{(2k-3)\varepsilon}\}, & 2 \mid r.\end{cases}$$

Formalization targets

Goal: Theorem 6.8

For $n \ge 2$ and $r \ge 2$:

(a) if $u_iu_j = 1$ for some $i \ne j$, or $u_i \in Q_{r,\varrho}$ for some $i$, then $\mathscr B_{r,n}$ is not semisimple;

(b) if $u_iu_j \ne 1$ for all $i \ne j$ and no $u_i$ lies in $Q_{r,\varrho}$, then

$$\mathscr B_{r,2}\ \text{semisimple} \iff o(q^2) > 2 \ \text{and}\ \big(u_iu_j^{-1} = q^{2d},\ i<j \Rightarrow |d| \ge 2\big),$$

and for $n \ge 4$, $\mathscr B_{r,n}$ is semisimple if and only if (a) $o(q^2) > n$; (b) $|d| \ge n$ whenever $u_iu_j^{-1} = q^{2d}$, $i < j$; (c) $u_i \notin S_{r,\varrho}$ for all $i$; (d) $u_iu_j \notin \bigcup_{k=3}^n\{q^{4-2k}, q^{2k-4}\}$ for all $i \ne j$. For $n = 3$ the goal states that semisimplicity implies (a)–(d).

The page states (b)(2) as an equivalence for all $n \ge 3$. The goal keeps only necessity at $n = 3$: Proposition 6.2 and Lemma 6.3 describe the same cell module of $\mathscr B_{r,3}$ and list different exclusions ($\varepsilon q$ against $-\varepsilon q^{-1}$ for odd $r$), and $S_{r,\varrho}$ at $n = 3$ contains neither.

Milestones

The rank $\dim_F\mathscr B_{r,n} = r^n(2n-1)!!$ (Theorem 2.14); the corner identities $E_{n-1}\mathscr B_{r,n}E_{n-1} = E_{n-1}\mathscr B_{r,n-2}$ (Lemma 3.1) and $E_{f,n}\mathscr B_{r,n}E_{f,n} = \mathscr B_{r,n-2f}E_{f,n}$ (Corollary 3.2), corrected at the two-strand boundary by requiring some $\omega_a\ne0$; Proposition 6.1, which says that $\det G_{1,\emptyset} = \det(\omega_{a+b})_{a,b\in N_r}$ is non-zero exactly when $u_iu_j \ne 1$ ($i \ne j$) and no $u_i$ lies in $Q_{r,\varrho}$; Proposition 6.5(b), non-semisimplicity when that determinant vanishes; and the reduction "$\mathscr H_{r,n}$ not semisimple $\Rightarrow \mathscr B_{r,n}$ not semisimple" from the proof of Theorem 6.8.

Significance

The criterion gives a closed list of parameter values at which the cyclotomic BMW algebra fails to be semisimple, and so, by Graham–Lehrer theory, the parameters at which all cell modules are simple and pairwise non-isomorphic. Outside that list the algebra's simple modules, their dimensions and the decomposition of tensor-type modules are given by the combinatorics of up-down tableaux; inside it, the list says which Gram determinants vanish and where decomposition numbers begin. For $r = 1$ it specializes to the semisimplicity criterion for BMW algebras, and its conditions (a)–(b) are Ariki's conditions for $\mathscr H_{r,n}$.

As far as is known, none of this is machine-checked: Mathlib has no BMW, Brauer, Ariki–Koike or Iwahori–Hecke algebras and no cellular algebras. The mission formalizes the statements of the paper on a presentation of $\mathscr B_{r,n}$ by generators and relations; a solver must supply a basis (or at least a dimension count), the cellular structure and the Gram-determinant computations. The paper leaves several of its proofs to the reader ("by arguments in the proof of [19, 5.41]"), so the formal proofs would also close gaps in the published argument.

Difficulty

Non-semisimplicity in part (a) needs only one degenerate bilinear form on a non-zero cell module, but showing that the module is non-zero, or that $\mathscr B_{r,n}$ does not collapse, already needs a lower bound on the dimension of a presented algebra, which no rewriting argument provides: the rank $r^n(2n-1)!!$ is proved in the literature through seminormal representations. Sufficiency in part (b) requires the Gram determinants of all cell modules $\Delta(f,\lambda)$, which the paper obtains by a recursion over up-down tableaux; vanishing of a single factor must be traced through branching and Morita-type functors between levels $n-2$, $n-1$ and $n$. Ariki's criterion for $\mathscr H_{r,n}$ is itself an external input.

Formalization scope

$\mathscr B_{r,n}$ and $\mathscr H_{r,n}$ are RingQuot quotients of FreeAlgebra F on finite generator types; indices are 0-based (the Lean T i is the paper's $T_{i+1}$), and $X_j^{-1}$ is a separate generator tied to $X_j$ by relation a). The sign $\varepsilon \in \mathbb Z^\times$ is the free parameter and $\alpha, \varrho, \gamma_i, \omega_a$ are computed from $(q, u, \varepsilon)$, so the parameters are u-admissible by construction. The $u_i$ are pairwise distinct (Assumption 2.2(1) divides by $u_i - u_j$; the paper extends 2.2 to coincident $u_i$ through [19, 3.11]). "Semisimple" is Mathlib's IsSemisimpleRing. The condition $o(q^2) > n$ is written as $q^{2k} \ne 1$ for $1 \le k \le n$, not through orderOf, which is $0$ for elements of infinite order. Relations d) and g) both use $\omega_0 = \sum_j\gamma_j$, which equals the paper's $1 - \delta^{-1}(\varrho - \varrho^{-1})$ for these parameters; were they different, the presentation would collapse. The corrected corner milestones require $n\ge3$ or some $\omega_a\ne0$ in Lemma 3.1, and $2f<n$ or some $\omega_a\ne0$ in Corollary 3.2. At $n=2$, $r=2$, $q=3$, $u=(2,\tfrac12)$, and $\varepsilon=1$, every $\omega_a$ vanishes, exposing the missing condition. $\det G_{1,\emptyset}$ is expressed as the Hankel determinant of the $\omega_a$, and $\mathscr B_{r,m} \subseteq \mathscr B_{r,n}$ is the subalgebra generated by the first generators.

A presentation that collapses to the zero algebra would make the goal false in part (a) but trivially true elsewhere; the rank milestone rules this out. Replacing semisimplicity by non-vanishing of Gram determinants would turn the goal into a different theorem and is not acceptable.

A complete development needs a basis theorem for $\mathscr B_{r,n}$, cellular algebras and Graham–Lehrer's semisimplicity criterion, the Ariki–Koike algebra and Ariki's criterion, and Gram-determinant computations. The cellular-algebra layer and the Ariki–Koike algebra are reusable beyond this mission; contributions of any of these, or of the milestones on their own, are welcome.

Selected references

• H. Rui and M. Si, The representation theory of cyclotomic BMW algebras (printed title The representations of cyclotomic BMW algebras, II), preprint, 2008. https://arxiv.org/abs/0807.4149
• H. Rui and J. Xu, The representations of cyclotomic BMW algebras, preprint, 2007. https://arxiv.org/abs/0801.0465
• R. Häring-Oldenburg, Cyclotomic Birman–Murakami–Wenzl algebras, J. Pure Appl. Algebra 161 (2001), 113–144. https://doi.org/10.1016/S0022-4049(00)00100-6
• S. Ariki, On the semi-simplicity of the Hecke algebra of $(\mathbb Z/r\mathbb Z)\wr\mathfrak S_n$, J. Algebra 169 (1994), 216–225. https://doi.org/10.1006/jabr.1994.1280
• J. J. Graham and G. I. Lehrer, Cellular algebras, Invent. Math. 123 (1996), 1–34. https://doi.org/10.1007/BF01232365
• J. S. Birman and H. Wenzl, Braids, link polynomials and a new algebra, Trans. Amer. Math. Soc. 313 (1989), 249–273. https://doi.org/10.1090/S0002-9947-1989-0992598-X

Motivation

Sending classical messages through a quantum device requires choosing input states that remain distinguishable after noise. The one-shot classical capacity measures the best information rate when each channel use is signaled with a separate input state. For many channels the optimization is difficult because it ranges over all ensembles of quantum states. Fermionic systems provide a finite-dimensional setting in which the noise has a direct description on elementary operators, but the optimal signaling states still need not be obvious. Bravyi's 2005 paper isolates a family of fermionic product channels, computes the best rate from Gaussian input states for any number of qubits, and proves that this restricted rate is the full one-shot rate for one or two qubits.

Setting

The system has $n$ qubits, with computational basis indexed by bit strings $x\in\{0,1\}^n$. The Jordan–Wigner Majorana operators $c_1,\ldots,c_{2n}$ are tensor products of Pauli matrices: $c_{2j-1}$ has $Z$ on qubits before $j$, $X$ on qubit $j$, and identity afterwards; $c_{2j}$ replaces $X$ with $Y$. Their ordered monomials $c(x)=c_1^{x_1}\cdots c_{2n}^{x_{2n}}$, $x\in\{0,1\}^{2n}$, form a basis of all operators on the qubits. The paper gives these operators and their monomials in Eq. (3).

A fermionic product channel $\Phi_b$ is determined by attenuation coefficients $b_p\in[0,1]$. On each monomial it acts by $\Phi_b(c(x))=(\prod_{p:x_p=1}b_p)c(x)$, and linearity defines it on every operator. A state is a positive semidefinite matrix of trace one. For a finite ensemble of output states $\{(p_a,\rho_a)\}$, with nonnegative weights summing to one, its Holevo quantity in bits is

$$\chi= S\!\left(\sum_a p_a\rho_a\right)-\sum_a p_aS(\rho_a), \qquad S(\rho)=-\operatorname{Tr}(\rho\log_2\rho).$$

The supremum of $\chi$ over all finite ensembles of outputs of $\Phi_b$ is $C_1(\Phi_b)$. A Gaussian state has the specific form $U\rho_\lambda U^\dagger$ of Definition 1: $\rho_\lambda=2^{-n}\prod_j(I+\lambda_j Z_j)$, each $\lambda_j\in[-1,1]$, and $U=\exp(iH_2+iH_1)$ for Hermitian quadratic and linear combinations of Majorana operators. Requiring Gaussian input states gives $C_1^g(\Phi_b)$. Setting $H_1=0$ gives an even Gaussian state. These are separate classes; the even class supplies an intermediate entropy minimum. Definition 1 and Eq. (13) are on page 4.

Formalization targets

Gaussian capacity

Write $b_1^\downarrow\ge\cdots\ge b_{2n}^\downarrow$ for the coefficients in decreasing order, and let $H(t)=-t\log_2t-(1-t)\log_2(1-t)$. The main formula, Theorem 1 and Eq. (6), is

$$C_1^g(\Phi_b)=n-H\!\left(\frac{1+b_1^\downarrow}{2}\right) -\sum_{j=1}^{n-1}H\!\left(\frac{1+b_{2j}^\downarrow b_{2j+1}^\downarrow}{2}\right).$$

It holds for every $n\ge1$ and every unsorted $b\in[0,1]^{2n}$. The milestones identify the covariance and Gaussian-preservation facts, the exact even and general Gaussian minimum-output entropies, and an ensemble attaining the capacity.

Full one-shot capacity for at most two qubits

The second clause of Theorem 1 states

$$C_1(\Phi_b)=C_1^g(\Phi_b)\qquad(n\le2).$$

Thus restricting the input ensemble to Gaussian states loses no one-shot capacity in these dimensions. The paper does not prove this equality for arbitrary $n$.

Significance

The formula replaces an optimization over arbitrary finite Gaussian ensembles with binary entropies of sorted attenuation coefficients. In the one- and two-qubit cases it also settles the unrestricted one-shot optimization for this channel family. The intermediate result $C_1=n-S_{\min}$ relates signaling directly to minimum output entropy; the even-Gaussian and Gaussian minima make the distinction between the two state classes explicit. These relationships are established in Sections II–IV of the paper.

The mathematical results are proved in the 2005 paper. This mission asks for machine-checked proofs of their exact finite-dimensional statements. The definitions of bit-valued von Neumann entropy, finite output ensembles, ordered Majorana monomials, Gaussian-state predicates, and covariance matrices can support later work on fermionic channels. The submitted goal and milestones are presently proof obligations rather than claims of existing Lean proofs.

Difficulty

The channel is simple on each Majorana monomial, but the entropy of a general output state is not determined by its one- and two-point correlations. Even within the Gaussian class, optimizing only the even Gaussian states gives a different formula from optimizing all Gaussian states: linear Majorana terms change the optimum. A direct search over density matrices therefore does not expose the closed expression in Theorem 1. For the unrestricted two-qubit clause, one must also relate arbitrary states to the Gaussian class; the paper invokes a three-qubit parity result for that step. The distinctions and parity result appear in Sections III–IV.

Formalization scope

Lean represents qubit basis vectors by Fin n → Fin 2 and operators by complex matrices on that finite type. Majorana indices start at zero in Lean, so the paper's $c_{2j-1},c_{2j}$ correspond to consecutive indices $2j-2,2j-1$. The Jordan–Wigner tensor factor at coordinate $j$ acts on qubit $j$; the monomial product follows increasing Majorana index. The channel is defined on all matrices by the trace-orthogonal monomial expansion of Eq. (4), not merely on covariance matrices. Attenuations may equal zero or one. Entropies use logarithms to base two, with $0\log_2 0=0$.

Every capacity uses a real supremum over all finite normalized ensembles, with arbitrary ensemble size. The inputs are density matrices, and their channel outputs must be density matrices. The Gaussian capacity requires every input to satisfy Definition 1; Lemma 2 ensures these outputs are Gaussian too. The minimum-output quantities are real infima over their stated input classes, and the corresponding milestone theorems assert attainment. For the actual channels the relevant sets are nonempty and bounded: the maximally mixed state supplies an output state, while every Holevo quantity lies between zero and $n$. This representation rules out restricting the Gaussian ensemble to the displayed optimizing family, assuming the goal's coefficients are initially sorted, or replacing bit entropy with natural-log entropy.

The development needs finite-matrix functional calculus, positivity, matrix exponentials, permutation and singular-value reasoning, and finite ensemble entropy bounds. Contributions to those reusable layers and to the paper's covariance, Gaussian-preservation, and minimum-output results are within scope. Lemma 3 is stated in its even-Gaussian form, which its proof establishes; the displayed lemma says only “Gaussian.”

Selected references

• Sergey Bravyi, Classical capacity of fermionic product channels, arXiv preprint quant-ph/0507282v1, 2005. arXiv