All missions

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

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

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

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

The search and discovery problem

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

The formalization commits to the following readings:

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

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

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

A complete development needs:

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

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

Selected references

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

Motivation

Traffic and packet networks are congested over time, not only on average. The fluid queuing model (Vickrey's bottleneck model on a network) captures this: every arc of a network is a bottleneck queue followed by a link of fixed length. Users entering at a source choose routes so as to arrive at the destination as early as possible, given the queues that the other users create. The resulting dynamic equilibrium (also called a Nash flow over time) is the dynamic analogue of a Wardrop equilibrium and a standard object in dynamic traffic assignment.

A basic question about any such dynamics is its long-run behaviour. When a constant inflow enters forever, do queues grow without bound, oscillate, or settle down? Cominetti, Correa and Olver (arXiv:2112.10412, Operations Research 70(1), 2022) answer this: if the inflow rate does not exceed the minimum cut capacity of the network, every dynamic equilibrium reaches a steady state after finite time, in which all queues are constant.

Timeline.

• Koch and Skutella (2011, Theory Comput. Syst.) characterized Nash flows over time through the derivatives of the earliest arrival labels ("thin flows with resetting") for piecewise constant inflows.
• Cominetti, Correa and Larré (2015, Oper. Res.) established existence of dynamic equilibria and the thin-flow characterization of their derivatives, the results the paper recalls in its §2.
• Before Cominetti, Correa and Olver it was not known whether a steady state is reached, or even whether queue lengths stay bounded, when $u_0\le\bar\nu$ (arXiv:2112.10412v1, p. 4). The paper introduces a potential function that increases along any dynamic equilibrium, derives the finite-time steady state under the min-cut condition, and gives a pseudopolynomial bound on the convergence time for rational data.

Setting

A fluid queuing network is a finite directed multigraph $G=(V,E)$ with a source $s$ and a terminal $t\neq s$. Each arc $e=vw$ has a capacity $\nu_e>0$ and a delay $\tau_e\ge 0$. A constant inflow rate $u_0>0$ enters at $s$. Every node is assumed reachable from $s$.

A flow over time consists of measurable, locally integrable inflow rates $f^+_e\ge 0$ and queue lengths $z_e$ with $z_e(0)=0$, governed by the queue dynamics

$$\dot z_e(\theta)=\begin{cases} f^+_e(\theta)-\nu_e & z_e(\theta)>0,\\ [f^+_e(\theta)-\nu_e]_+ & z_e(\theta)=0.\end{cases}$$

The queue releases flow at rate $\nu_e$ while it is nonempty, and the released flow leaves the arc $\tau_e$ time units later. Flow is conserved at every node other than $t$, with external inflow $u_0$ at $s$.

A particle entering arc $e$ at time $\theta$ leaves it at $T_e(\theta)=\theta+z_e(\theta)/\nu_e+\tau_e$. The earliest arrival label $\ell_v(\theta)$ is the minimum over $s$–$v$ paths $p=e_1\cdots e_k$ of $T_{e_k}\circ\cdots\circ T_{e_1}(\theta)$. An arc $e=vw$ is active at $\theta$ if $\ell_w(\theta)=T_e(\ell_v(\theta))$, i.e. it lies on a currently fastest route. A flow over time is a dynamic equilibrium if, for almost every time $\xi$, flow enters an arc $e=vw$ at time $\xi$ only if $\xi=\ell_v(\theta)$ for some $\theta\ge 0$ at which $e$ is active. It attains a steady state if there is $\theta_0$ with $z_e(\theta)=z_e(\theta_0)$ for every arc and every $\theta\ge\theta_0$.

The potential of the paper is

$$\Phi(\theta)=u_0\bigl(\ell_t(\theta)-\ell_s(\theta)\bigr)-\sum_{e=vw\in E}z_e(\ell_v(\theta)).$$

Formalization targets

Goal: Theorem 3

$$u_0\le\sum_{e\in\delta^+(S)}\nu_e\ \text{ for all } S\ni s,\ S\not\ni t\quad\Longrightarrow\quad\exists\,\theta_0\ \forall e\ \forall\theta\ge\theta_0:\ z_e(\theta)=z_e(\theta_0),$$

for every dynamic equilibrium. No bound on $\theta_0$ is asserted.

Milestones

1. Labels and static flows $x_e(\theta)=\int_0^{\ell_v(\theta)}f^+_e$ are nondecreasing and absolutely continuous (§2.3).
2. Almost everywhere, the derivatives $(\ell',x')$ form a normalized thin flow with resetting on the active and queuing arcs (§2.3, (10)–(13)).
3. The queue identity $z_e(\ell_v(\theta))=\nu_e[\ell_w(\theta)-\ell_v(\theta)-\tau_e]_+$ (proof of Theorem 2).
4. Lemma 1: a steady state is attained iff all $\ell'_v$ are eventually $1$.
5. Theorem 2: $\Phi'\ge 0$ wherever $\Phi$ is differentiable, and almost everywhere $\Phi'=0$ exactly when all $\ell'_v=1$.
6. A uniform $\kappa>0$ with $\Phi'\in\{0\}\cup[\kappa,\infty)$ almost everywhere (proof of Theorem 3).
7. The min-cut condition makes the min-cost flow program (P) feasible (proof of Theorem 3).
8. Labels and queues give a feasible point of the dual (D), so $\Phi(\theta)$ is bounded by the cost of every feasible point of (P) (proof of Theorem 3).

Significance

The result. Theorem 3 shows that, under the min-cut condition, the equilibrium dynamics settles. Queues freeze, so travel times become constant. The limit regime is described by the linear program (P), a min-cost flow, and its dual (D). Without the theorem it would be unknown whether congestion can oscillate forever in a network with enough capacity. The condition is sharp: if $u_0$ exceeds the minimum cut capacity $\bar\nu$, the arcs of a minimum cut grow unbounded queues (p. 4). The result is a prerequisite for the paper's convergence-time bounds and for its constructions of long transient phases.

Formalizing it. The result is proved on paper; to our knowledge, no part of the theory of flows over time with queues has been formalized. The mission produces a Lean model of fluid queuing networks and dynamic equilibria for general measurable inflows. Its definitions (queue dynamics, earliest arrival labels, active arcs, thin flows with resetting) can be reused for the other results of this literature (existence of equilibria, the price of anarchy over time, convergence-time bounds). The paper's own proofs of the §2.3 facts cite earlier work, so a complete development also formalizes parts of Koch–Skutella (2011) and Cominetti–Correa–Larré (2015).

Difficulty

The potential argument is short once its ingredients exist, but each ingredient is analytic. The labels are minima of compositions of exit-time functions that depend on the queues. The queues depend on the inflows, and the inflows are constrained by the labels. Absolute continuity and almost-everywhere differentiability of the labels, and the identification of their derivatives with a thin flow, need the regularity theory of this fixed point.

The step "there are only finitely many possible derivatives, hence a uniform $\kappa$" is the delicate point. It relies on the thin-flow system determining $\ell'$ from the pair (active arcs, queuing arcs). As printed ("for all subsets $E^*\subseteq E'\subseteq E$"), that uniqueness fails when $E'$ contains a cycle of zero-delay arcs carrying no flow. A proof must therefore use the structure of the active-arc sets that actually occur. The bound $\Phi\le\alpha$ needs max-flow/min-cut and LP weak duality in the network's own encoding.

Formalization scope

Everything lives in the namespace NashFlowLT.SteadyState. The network is a structure with tail, head : E → V over finite types, so parallel arcs are allowed, as in the paper's Example 1. Its data are nu, tau, u0, s, t.

The standing assumptions $\nu>0$, $\tau\ge 0$, $u_0>0$, $s\neq t$ and reachability of every node from $s$ form Network.Standing. The last two are added to the page: $s\neq t$ is implicit in a source–sink pair, and reachability is needed so the minimum defining $\ell_v$ is over a nonempty set.

Flows over time carry the inflows fin and the queues z as data. The queue equation is imposed in integrated form from $z_e(0)=0$, inflows are measurable, nonnegative and integrable on bounded intervals (an added hypothesis), and conservation holds almost everywhere. All functions of time are real-valued on $\mathbb R$, and only $\theta\ge 0$ matters.

Labels are minima over simple paths (lists of arcs visiting distinct nodes), never solutions of the Bellman equations. With zero-delay cycles those equations admit spurious solutions.

The min-cut hypothesis is stated as "$u_0$ is at most the capacity of every $s$–$t$ cut". The bound $\Phi\le\alpha$ is stated against every feasible point of (P), so no infimum is defined. The equality case of Theorem 2 and the thin-flow characterization are posed for almost every $\theta$; the nonnegativity of $\Phi'$ holds at every point of differentiability.

The goal quantifies over all dynamic equilibria. It must not be replaced by a statement about one constructed equilibrium, by the label condition of Lemma 1, or by a hypothesis that $\Phi$ is bounded or that there are finitely many phases. A sanity file exhibits a one-arc instance that satisfies every hypothesis and is a dynamic equilibrium.

Contributions welcome: proofs of the milestones, a proof of the thin-flow characterization, a max-flow/min-cut bridge to the platform's existing LinearOptimization.max_flow_min_cut, and the uniqueness of $\ell'$ for the active-arc sets that occur in equilibria.

Selected references

• R. Cominetti, J. Correa, N. Olver, Long term behavior of dynamic equilibria in fluid queuing networks, Operations Research 70(1), 2022; arXiv:2112.10412v1. https://arxiv.org/abs/2112.10412
• R. Koch, M. Skutella, Nash equilibria and the price of anarchy for flows over time, Theory of Computing Systems 49(1), 2011. https://doi.org/10.1007/s00224-010-9299-y
• R. Cominetti, J. Correa, O. Larré, Dynamic equilibria in fluid queueing networks, Operations Research 63(1), 2015. https://doi.org/10.1287/opre.2015.1348
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2), 1969. https://www.jstor.org/stable/1823678

Motivation

Lie 2-algebras allow a Lie bracket to satisfy its laws up to a specified higher operation. They arise when an ordinary Lie algebra extension has a cocycle in degree three rather than degree two. Baez, Crans, Stevenson, and Schreiber use this language to relate a finite-dimensional model attached to a compact simple Lie group to an infinite-dimensional construction made from paths and loops. Their paper also constructs a Lie 2-group at integral levels; the algebraic comparison is Theorem 5.1 of the pinned preprint, the target of this mission.

The comparison matters because the two descriptions expose different features. The finite-dimensional algebra $\mathfrak g_k$ displays its degree-three cocycle directly. The path algebra $\mathcal P_k\mathfrak g$ comes with a central term built from an integral over the path interval. Showing that these models are equivalent makes it possible to use the smaller skeletal description while retaining the structure carried by based loops. The main result states more than a loose correspondence: it puts both models in a strictly exact sequence of Lie 2-algebras.

Setting

Let $\mathfrak g$ be a finite-dimensional simple real Lie algebra with an invariant positive-definite inner product $\langle\cdot,\cdot\rangle$. Fix $k\in\mathbb R$. Write $P_0\mathfrak g$ for the smooth functions $p:[0,2\pi]\to\mathfrak g$ with $p(0)=0$, and $\Omega\mathfrak g$ for those also satisfying $p(2\pi)=0$. Their brackets are pointwise. A prime denotes differentiation with respect to the interval coordinate, with one-sided derivatives at the endpoints.

A 2-term $L_\infty$-algebra has vector spaces $V_0,V_1$, a linear map $d:V_1\to V_0$, binary brackets $l_2$ in degrees $(0,0)$ and $(0,1)$, and a ternary bracket $l_3:V_0^3\to V_1$. A homomorphism has components $(f_0,f_1,f_2)$: a chain map in degrees zero and one and a skew bilinear correction $f_2$. The correction obeys the three compatibility equations of Definition 2.7. A 2-homomorphism is a linear chain homotopy with the extra bracket equation of Definition 2.8. Two algebras are equivalent when there are homomorphisms in both directions whose composites are 2-isomorphic to the identities.

The skeletal algebra $\mathfrak g_k$ has $V_0=\mathfrak g$, $V_1=\mathbb R$, zero differential, the ordinary bracket on $\mathfrak g$, trivial action on $\mathbb R$, and

$$l_3(x,y,z)=k\langle x,[y,z]\rangle.$$

The path algebra $\mathcal P_k\mathfrak g$ has $V_0=P_0\mathfrak g$, $V_1=\Omega\mathfrak g\oplus\mathbb R$, and $d(\ell,c)=\ell$. Its degree-zero bracket is pointwise, $l_3=0$, and its action on degree one is

$$l_2(p,(\ell,c))=\left([p,\ell],\;2k\int_0^{2\pi}\langle\ell(\theta),p'(\theta)\rangle\,d\theta\right).$$

Finally, $E\Omega\mathfrak g$ has $\Omega\mathfrak g$ in both degrees, identity differential, its pointwise bracket in both binary slots, and zero ternary bracket. These are the formulas of Example 2.15, Proposition 4.2, and Lemma 5.2.

Formalization targets

The main target is the strictly exact sequence of Theorem 5.1:

$$0\longrightarrow E\Omega\mathfrak g\xrightarrow{\lambda}\mathcal P_k\mathfrak g\xrightarrow{\phi}\mathfrak g_k\longrightarrow 0,$$ $$E\Omega\mathfrak g\simeq 0,\qquad \phi\text{ is an equivalence.}$$

Strict exactness means that $\lambda$ is injective, its image is the kernel of $\phi$, and $\phi$ is surjective on both the object and morphism vector spaces. The composite $\phi\circ\lambda$ is the zero homomorphism, including its bilinear component. This is a statement for every real $k$; no integrality condition is attached to the Lie-algebra result.

The five milestone targets are the paper's numbered Lemmas 5.3, 5.4, 5.5, 5.7, and 5.8. They state, in order, that $EL$ is equivalent to zero, that the endpoint and integral formulas define $\phi$, that $E\Omega\mathfrak g$ is its strict kernel via $\lambda$, that any smooth endpoint interpolation defines a reverse homomorphism $\psi$, and that $\phi\psi$ is the identity while $\psi\phi$ is 2-isomorphic to the identity. Their exact formulas are in the theorem items and milestone statements.

Significance

The theorem identifies the skeletal degree-three cocycle with the path model's integral central term at the level of Lie 2-algebra equivalence. It also locates the based-loop algebra within a strict exact sequence, so the comparison retains information about kernels and morphisms as well as objects. The paper uses this algebraic result alongside a separate group-level construction whose integral-level conditions have a different role; the conclusion of §6 distinguishes the two.

The paper proves the result on paper. This mission asks for machine-checked proofs of the displayed homomorphism and 2-homomorphism equations and of strict exactness. A completed development would also leave reusable definitions for smooth based paths, central loop integrals, and the component presentation of 2-term $L_\infty$ homomorphisms. The paper's Fréchet Lie 2-group construction and its topological realization are outside this mission.

Difficulty

The endpoint map alone does not define a homomorphism of the relevant 2-term algebras. Its bilinear component must account for the central integral in $\mathcal P_k\mathfrak g$ and for the nonzero ternary bracket in $\mathfrak g_k$. The integral formula contains a boundary term for general paths, so treating it as the loop cocycle without that term changes the statement. The reverse homomorphism depends on a smooth interpolation $f$, and equivalence requires its composites to match the identity at all three component levels, together with the 2-homomorphism equation. Smoothness, endpoint behavior, and the signs in the graded brackets all affect these equalities.

Formalization scope

Lean represents a path by a function on $\mathbb R$ that is smooth on $[0,2\pi]$ and constant outside it, fixed by clamping to the interval. This removes irrelevant differences between extensions of the same interval path. The underlying Lie algebra has a continuous bilinear bracket, Jacobi identity, invariance of the inner product, and simplicity. The continuous-bracket requirement is automatic in finite dimension. The inner product can be any invariant positive-definite form; the normalization by the basic form divided by $4\pi$ used for the group construction is not imposed. All levels $k\in\mathbb R$ are included.

The formal object called a Lie 2-algebra is its 2-term $L_\infty$ presentation. Theorem 2.10's equivalence with the categorical presentation is used as the paper's interpretation and is not re-proved. The record stores the operations, while the homomorphism records explicitly enforce the chain map and equations (3)–(5), and 2-homomorphisms enforce both chain-homotopy equations and equation (7). It does not separately store the HDA6 coherence equations. Composition is recorded by the paper's component formula (6). The data for $\mathcal P_k\mathfrak g$ are defined directly from Proposition 4.2, without building the Fréchet Lie 2-group first. The source's exact integral coefficients, real summand, and nonzero ternary bracket are fixed in the definitions; removing any one of them changes the target.

Contributions to the analytic closure of smooth paths under pointwise brackets, the interval integration identities, and the homomorphism equations are useful beyond the final theorem. Proofs of the five stated lemmas and of the final exactness and equivalence claims are the intended contributions.

Selected references

• J. C. Baez, A. S. Crans, D. Stevenson, and U. Schreiber, From Loop Groups to 2-Groups, arXiv:math/0504123v3, 2023 revision of the preprint dated 2007. arXiv.

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

Inventory control when stock is seen only at zero

In many retail settings, recorded inventory is not reliable. Shrinkage, misplacement and recording errors mean the shelf count is unknown, but a stock-out is visible. Bai, Chen and Stolyar (SSRN 3865728; Operations Research Technical Note, 2022, doi:10.1287/opre.2022.2305) study the extreme version of this: a single-item lost-sales system whose inventory level is observed only when it is zero.

For the discounted cost criterion, Bensoussan, Çakanyıldırım and Sethi (2007) showed that optimal feedback policies exist for this model. Whether a stationary policy minimizes the long-run average cost was left open. Average-cost problems for partially observable systems are harder because of the vanishing-discount argument they rely on. It needs a uniform bound on relative value functions, and on a space of beliefs such bounds are not automatic. The paper settles the question for this model.

Setting

In each period $t$ the inventory level is $x_t\in\mathbb R_+$. The decision maker orders $a_t\in\mathbb A=[0,K]$, with $K>0$. The order arrives at once and ordering costs nothing. Then an i.i.d. demand $D_t\sim D$ is realized, and unmet demand is lost:

$$x_{t+1}=(x_t+a_t-D_t)^+ .$$

The period cost is the holding and lost-sales cost $h^+(x_t+a_t-D_t)^+ + h^-(x_t+a_t-D_t)^-$, with $h^+,h^->0$. Its expectation given $(x,a)$ is $c(x,a)$. The demand $D$ is nonnegative, has a density $f$ with distribution function $F$, a finite positive mean and a positive variance.

Only the signal $y_t=\mathbf 1\{x_t>0\}$ is observed. The decision maker therefore acts on a belief $z$, the conditional distribution of the current inventory level. After ordering $a$ from belief $z$, the next belief is $\delta_0$ if $y=0$. If $y=1$ it is the posterior $H(z,a,1)$, the law of $(x+a-D)^+$ (with $x\sim z$) conditioned on being positive. The probability of $y=1$ is $R(1\mid z,a)$.

This yields a completely observable MDP (COMDP). Its states are beliefs with finite second moment, $\int x^2\,z(dx)<\infty$ (Assumption 1), taken with the topology of weak convergence. Its cost is $\bar c(z,a)=\int c(x,a)\,z(dx)$ and its transition kernel is

$$q(\cdot\mid z,a)=R(0\mid z,a)\,\delta_{\delta_0}+R(1\mid z,a)\,\delta_{H(z,a,1)}.$$

For a policy $\pi$, $v^\pi_\alpha$ is its $\alpha$-discounted cost and $w^\pi$ its average cost per period (a $\limsup$). The optima are $v_\alpha=\inf_\pi v^\pi_\alpha$ and $w=\inf_\pi w^\pi$ over all history-dependent randomized policies. Write $m_\alpha=\inf_z v_\alpha(z)$, $u_\alpha=v_\alpha-m_\alpha$ and $w^*=\inf_z w(z)$.

Formalization targets

Goal: Theorem 1 (p. 9)

There are a sequence $\alpha_n\uparrow 1$ and a measurable stationary policy $\varphi$ that is average-cost optimal among all policies. With $w^*$ finite and

$$u(z)=\liminf_{n\to\infty,\ s\to z}u_{\alpha_n}(s)$$

finite, $\varphi$ satisfies the average cost optimality inequality (ACOI)

$$w^*+u(z)\ \ge\ \bar c(z,\varphi(z))+\int u(s)\,q(ds\mid z,\varphi(z))\qquad\text{for every belief }z .$$

Milestones, in attack order

1. §3.1, p. 10. $q$ is a measurable stochastic kernel, so the COMDP exists.
2. Lemma 3, p. 12. Assumption B(i): $w^*<\infty$.
3. §3.2, p. 12. Assumption (W*): $\bar c$ is $\mathbb K$-inf-compact and $q$ is weakly continuous.
4. Lemma 2, p. 12 (Feinberg 2016, for a general MDP on Borel spaces). Under (W*) and (B), $w^*=\lim_{\alpha\uparrow1}(1-\alpha)v_\alpha$, and a stationary average-cost optimal policy satisfies the ACOI.
5. Lemma 4, p. 14. For two inventory paths started at $x'\ge x\ge 0$, sharing demands and an arbitrary control rule $\zeta$: $V^\zeta_\alpha(x)-V^\zeta_\alpha(x')\le h^-(x'-x)-\mathbf 1\{x'-x\ge C\}h'(x'-x)\le h^-C$, with $C,\alpha_*,h'>h^-$ uniform.
6. Display (12), corrected, pp. 13–14. $v_\alpha(\delta_0)-v^\pi_\alpha(z')\le\bar C$, uniformly in $\alpha\in[\alpha_*,1)$, in beliefs $z'$ and in stationary $\pi$. The paper prints $v^\pi_\alpha(\delta_0)$ as the first term. Its proof bounds the cost of a different policy (the "pursuing" policy) started at $\delta_0$, and the derivation of (11) uses the optimal value. The printed form, with the same $\pi$ at $\delta_0$, is not what the proof establishes.
7. Display (11), p. 13. $\sup_{\alpha\in[\alpha_*,1)}u_\alpha(\delta_0)<\infty$.
8. Theorem 2, p. 13. Assumption B(ii): $\sup_{\alpha\in[\alpha_*,1)}u_\alpha(z)<\infty$ for every belief $z$.

Significance

Theorem 1 gives existence of a stationary average-cost optimal policy for a partially observed inventory system with lost sales. In that setting the belief space is infinite-dimensional and the state is never fully revealed except at zero. The ACOI also supplies the structure needed to study such a policy. The paper leaves open whether the ACOE (the equality form) holds.

The reduction is reusable. Feinberg's general conditions, (W*) and (B), apply to many belief MDPs. The problem-specific work is the uniform bound B(ii), obtained here through a coupling estimate (Lemma 4) for lost-sales paths under arbitrary, even anticipating, controls.

The paper proves Theorem 1, Theorem 2, Lemma 3 and Lemma 4. Lemma 2 and the (W*) claim are cited from Feinberg (2016) and Feinberg, Kasyanov and Zgurovsky (2016) and are not proved in the paper. As far as is known, none of these results has a machine-checked proof; the general vanishing-discount theory for MDPs on Borel spaces is itself not yet formalized.

Difficulty

The obvious route to B(ii) compares $v_\alpha(z)$ with $v_\alpha(\delta_0)$ by running from $z$ the policy that is optimal from $\delta_0$. This fails: a policy is a function of the belief, and the beliefs generated from $z$ and from $\delta_0$ differ, so the same policy produces different orders. The paper goes the other way and bounds $v_\alpha(\delta_0)$ above by $v^\pi_\alpha(z')+\bar C$. This needs a policy started from $\delta_0$ that mimics $\pi$'s orders while the two systems have not yet merged. The constant must be uniform in $\alpha$ close to $1$, so per-period estimates that grow like $1/(1-\alpha)$ are useless.

The (W*) claim has its own difficulty. The observation kernel $\mathbf 1\{x>0\}$ is discontinuous at $0$, so the known criterion for weak continuity of belief kernels, which needs observations continuous in total variation, does not apply. Continuity has to come from the density of $D$.

Formalization scope

The Lean development lives in the namespace PartialLostSales.ACOI. It reuses the published FeinbergLiang.ACOE layer: MDP, history-dependent randomized Policy, vDisc, vOpt, avgCost, wOpt, IsAvgOptimal, uRel, uTilde, IsDiscountSeq, KInfCompact and AssumptionWStar. All costs and values lie in $[0,\infty]$. Its conventions are:

• Spaces. Inventory lives in ℝ≥0 with the Euclidean topology, and actions in the subtype $[0,K]$.
• Beliefs. Beliefs form the subtype of ProbabilityMeasure ℝ≥0 with finite second moment. They carry the weak topology and Mathlib's (Giry) σ-algebra, which is the Borel σ-algebra here.
• COMDP. "The COMDP" is any MDP satisfying IsCOMDP, which pins the lower bound $0$, the cost $\bar c$ and the kernel $q$ pointwise; milestone 1 shows one exists.
• Assumption (B). It is the paper's version, with $\sup$ over $[\alpha_*,1)$.
• Policies. "Stationary" means a measurable map from beliefs to actions.

The paper states that COMDP and POMDP policies correspond with equal values (Feinberg, Kasyanov and Zgurovsky 2016). The goal is stated in the COMDP, and that equivalence is not formalized.

Added hypotheses. Demand is nonnegative. Lemma 4's control rule is measurable, but adaptedness is not required.

Totality devices. The posterior when $R(1\mid z,a)=0$, and the map of a posterior back into the belief subtype, have else branches that are never used.

Indexing. Lemma 4 indexes periods from $0$ with weight $\alpha^t$. Its costs are realized costs, since controls may anticipate.

Trivializing formalizations. Several encodings would make statements trivial, and none is used. The kernel and cost of the MDP are never left free. The ACOI carries explicit finiteness of $w^*$ and $u$, so it is not an $[0,\infty]$ inequality that holds when $u=\infty$. Optimality is over all policies, not only stationary ones. The ACOI uses $w^*$, not $\limsup(1-\alpha)m_\alpha$ or a free constant.

Not formalized.

• Lemma 1, already open on the platform as FKZAvg.WStar.theorem_2 (v).
• Theorem 3, p. 20, and the pursuing-policy construction of §4.1.
• The POMDP–COMDP equivalence.
• The extensions of §5.

Contributions of general value include Feinberg's average-cost theory on Borel spaces (Lemma 2) and weak continuity of belief kernels with discontinuous observations.

Selected references

• X. Bai, X. Chen, A. L. Stolyar, Average Cost Optimality in Partially Observed Lost-Sales Inventory Systems, SSRN preprint 3865728; Operations Research Technical Note, 2022. https://ssrn.com/abstract=3865728, https://doi.org/10.1287/opre.2022.2305
• E. A. Feinberg, Optimality conditions for inventory control, in Optimization Challenges in Complex, Networked and Risky Systems (INFORMS TutORials in Operations Research), 14–45, 2016. https://doi.org/10.1287/educ.2016.0145
• E. A. Feinberg, P. O. Kasyanov, M. Z. Zgurovsky, Partially observable total-cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 41(2), 2016. https://doi.org/10.1287/moor.2015.0746
• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 2012. https://doi.org/10.1287/moor.1120.0555
• A. Bensoussan, M. Çakanyıldırım, S. P. Sethi, Partially observed inventory systems: the case of zero-balance walk, SIAM Journal on Control and Optimization 46(1), 2007. https://doi.org/10.1137/040620321