All missions

Motivation

Qubits that sit close together, closer than the wavelength of the environment modes they couple to, are disturbed by that environment in the same way. The resulting noise is collective decoherence: its error operators are the collective spin operators $S_\alpha=\sum_i\tfrac12\sigma_\alpha^{(i)}$ rather than independent errors on each qubit. Chapter 8 of D. M. Bacon's thesis (Decoherence, Control, and Symmetry in Quantum Computers, arXiv:quant-ph/0305025v1, §8.4–§8.7, pp.113–121) derives this regime from spin-boson and amplitude-damping models and then works out the decoherence-free subspaces and subsystems (DFSs) it admits, which is where quantum information can be stored with no active correction at all.

Timeline. Duan and Guo (1997) and Zanardi and Rasetti (1997) observed that collectively coupled qubits support noiseless states (doi:10.1103/PhysRevLett.79.1953, arXiv:quant-ph/9705044). Lidar, Chuang and Whaley (1998) named and characterized decoherence-free subspaces (arXiv:quant-ph/9807004). Knill, Laflamme and Viola (2000) generalized them to noiseless subsystems through the representation theory of the error algebra (arXiv:quant-ph/9908066). Kempe, Bacon, Lidar and Whaley (2001) worked out the collective decoherence case in full, together with universal computation on it (arXiv:quant-ph/0004064); Chapter 8 of the thesis is its exposition.

Setting

The register is $n$ qubits, with Hilbert space $\mathbb C^{2^n}$ and computational basis $|x\rangle=|x_1\cdots x_n\rangle$, $x\in\{0,1\}^n$. The Pauli matrices $\sigma_x,\sigma_y,\sigma_z$ act on a single qubit, and $\sigma^{(i)}_\alpha$ (Lean: onQubit i (BBPSSW.Distill.pauli α)) is $\sigma_\alpha$ on qubit $i$ tensored with the identity elsewhere. The collective operators are

$$S^{[n]}_\alpha=\sum_{i=1}^n\tfrac12\sigma^{(i)}_\alpha\quad(\alpha=x,y,z),\qquad S_\pm=S_x\pm iS_y,$$

(Lean: collS n α, collPlus n, collMinus n), and the total angular momentum is $(S^{[n]})^2=S_x^2+S_y^2+S_z^2$ (totalS2 n). The exchange operator $E_{ij}$ (exchange i j) swaps qubits $i$ and $j$.

Under weak collective decoherence the only error is $S_z$. The Hamming weight $H(x)$ (hammingWeight x) counts the $1$'s of $x$, and $\mathrm{DFS}_n(h)$ (dfsWeak n h) is the span of the basis states of Hamming weight $h$.

Under strong collective decoherence the errors generate the complex algebra $\mathcal A$ spanned by products of $I,S_x,S_y,S_z$. The total angular momentum $J$ of $n$ spin-$\tfrac12$ particles runs over $n/2,\,n/2-1,\dots$, down to $0$ or $\tfrac12$. The matrices $S_\alpha(2J+1)$ (spinRep (2J) α) form the standard spin-$J$ representation of $\mathfrak{su}(2)$, with $S_z$ diagonal and $S_-|m\rangle=\sqrt{(J+m)(J-m+1)}\,|m-1\rangle$. For multiplicities $n_J$, $\bigoplus_J I_{n_J}\otimes X_J$ (blockOp n m X) is the block operator acting as $X_J$ on the irrep factor and trivially on the degeneracy factor.

Formalization targets

Goal: (8.41)–(8.43)

There are multiplicities $n_J$ and a unitary $W:\mathbb C^{2^n}\to\bigoplus_J\mathbb C^{n_J}\otimes\mathbb C^{2J+1}$ with

$$W S_\alpha W^\dagger=\bigoplus_J I_{n_J}\otimes S_\alpha(2J+1),\qquad n_J=\frac{(2J+1)\,n!}{(n/2+J+1)!\,(n/2-J)!},\qquad W\mathcal A W^\dagger=\bigoplus_J I_{n_J}\otimes M_{2J+1}.$$

All three clauses are part of the goal: the form of the generators, the multiplicity formula, and the fact that the collective algebra is the whole block algebra (both inclusions).

Milestones

• (8.32): $[S_\alpha,S_\beta]=i\varepsilon_{\alpha\beta\gamma}S_\gamma$.
• (8.34): $S_z|x\rangle=\tfrac12(n-2H(x))|x\rangle$.
• (8.35): $\dim\mathrm{DFS}_n(h)=\binom nh$, and $\mathrm{DFS}_n(h)$ is the $S_z$-eigenspace for $\tfrac12(n-2h)$.
• (C.8): $(S^{[n]})^2=n(1-\tfrac n4)I+\tfrac12\sum_{i\neq j}E_{ij}$.
• (8.50): in every basis of the form (8.43), $S_-|J,\lambda,m\rangle=\sqrt{(J+m)(J-m+1)}\,|J,\lambda,m-1\rangle$ and $S_+S_-|J,\lambda,m\rangle=(J+m)(J-m+1)|J,\lambda,m\rangle$.

Significance

The decomposition is the structure theorem of collective decoherence. Since every error acts as $I_{n_J}\otimes X_J$, a state written into the degeneracy factor $\mathbb C^{n_J}$ for one fixed $J$ is untouched by every error: this is the strong collective decoherence DF subsystem $\mathrm{DFS}_n(J)$, of dimension $n_J$ (Definition 8.6.1). The multiplicity formula says how much protected information $n$ qubits hold. Three qubits already carry one protected qubit ($n_{1/2}=2$), and $n_J$ grows like $2^n$ up to a polynomial factor, so the encoding rate tends to one. Chapters 9 and 11 build universal exchange-only computation on these subsystems, and their proofs (Appendix C) induct on exactly this decomposition and on (C.8). (8.50) gives the collective amplitude damping DF subspaces of §8.7.

The facts are textbook angular momentum addition, and the thesis cites (8.42) to Mandel and Wolf rather than proving it. No machine-checked version is known to exist: the platform holds Schur-transform encodings, and nothing proves the multiplicity formula or the algebra decomposition for qubits. The mission yields a reusable Lean account of the collective spin representation on $(\mathbb C^2)^{\otimes n}$.

Difficulty

The commutation relations and the action of $S_z$ are finite computations, and the dimension count $\sum_J n_J(2J+1)=2^n$ is elementary. The goal asks for more than either. Clause (8.43) requires a single change of basis that brings all three non-commuting generators at once to the standard real spin-$J$ matrices, with matching phases in every copy of every irrep. A dimension count fixes the sizes of the blocks but not the basis. Clause (8.42) asks for the exact number of copies of each irrep, a statement about the whole $2^n$-dimensional representation that no small case settles. Clause (8.41) is an equality of algebras: the products of $S_x,S_y,S_z$ must reach every operator of the form $\bigoplus_J I_{n_J}\otimes X_J$, with the blocks for different $J$ chosen independently. The obvious inclusion $\mathcal A\subseteq\bigoplus_J I_{n_J}\otimes M_{2J+1}$ follows from (8.43); the reverse inclusion is where the content lies.

Formalization scope

Qubits are Fin n → Fin 2. Operators are Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ, and $|0\rangle$ is index $0$, with $m=+\tfrac12$. The labels $x,y,z$ and the Pauli matrices are the published BBPSSW.Distill.Axis and BBPSSW.Distill.pauli, imported as references. Half-integers are avoided: $J=n/2-r$ with r : Fin (n/2+1), the irrep factor is Fin (n - 2r + 1), and the basis index $k$ stands for $m=J-k$. The multiplicity formula is stated in $\mathbb Q$ (degeneracy n r), so no truncating division hides a failure of divisibility. The unitary is a rectangular matrix $W$ between the two index sets with $W^\dagger W=I$ and $WW^\dagger=I$. The algebra is Algebra.adjoin ℂ (Set.range (collS n)), which contains $I$. All statements also hold, and are stated, for $n=0$.

The goal cannot be satisfied by a degenerate witness. The multiplicities are pinned by the formula, $W$ must be unitary, and clause (8.41) is an "if and only if", so an empty block or a zero map cannot meet it. Proved sanity checks confirm $n_1=n_0=1$ for $n=2$, $n_{3/2}=1$, $n_{1/2}=2$ for $n=3$, the row $n=8$ of Table 8.2, and $\sum_J n_J(2J+1)=2^n$ for $n\le6$. They also check that for $n=1$ an explicit unitary meets (8.43).

Useful infrastructure: computational-basis lemmas for onQubit, the spin-$J$ representation and its irreducibility, a Casimir argument, and a Burnside or double-commutant theorem for matrix algebras. These parts are reusable by Missions VIII and IX of this series and by any permutation-symmetric quantum information result. Contributions toward the milestones, toward the explicit highest-weight construction, and toward the binomial identity behind (8.42) are welcome.

Selected references

• D. M. Bacon, Decoherence, Control, and Symmetry in Quantum Computers, PhD thesis, UC Berkeley, 2001; arXiv:quant-ph/0305025v1, 2003. arXiv:quant-ph/0305025
• J. Kempe, D. Bacon, D. A. Lidar, K. B. Whaley, Theory of decoherence-free fault-tolerant universal quantum computation, Phys. Rev. A 63, 042307, 2001. arXiv:quant-ph/0004064
• E. Knill, R. Laflamme, L. Viola, Theory of quantum error correction for general noise, Phys. Rev. Lett. 84, 2525, 2000. arXiv:quant-ph/9908066
• D. A. Lidar, I. L. Chuang, K. B. Whaley, Decoherence-free subspaces for quantum computation, Phys. Rev. Lett. 81, 2594, 1998. arXiv:quant-ph/9807004
• P. Zanardi, M. Rasetti, Noiseless quantum codes, Phys. Rev. Lett. 79, 3306, 1997. arXiv:quant-ph/9705044
• L.-M. Duan, G.-C. Guo, Preserving coherence in quantum computation by pairing quantum bits, Phys. Rev. Lett. 79, 1953, 1997. doi:10.1103/PhysRevLett.79.1953
• L. Mandel, E. Wolf, Optical Coherence and Quantum Optics, Cambridge University Press, 1995 (the thesis's reference [142] for (8.42)).

Pricing while reviews accumulate

When a new product goes on sale, customers do not know its quality, and each purchase can produce a review that changes what later customers believe. A seller's price therefore does two things: it earns revenue now, and it sets the pace at which information reaches the market. Whether this second effect justifies changing the price over time is a practical question for online marketplaces, where reviews are public and repricing is cheap. Learning from reviews has been studied by Besbes and Scarsini (2018) and Ifrach et al. (2019). Pricing with reviews has been studied with static and two-stage rules, for example by Crapis et al. (2017) and Papanastasiou and Savva (2017).

Shin, Vaccari and Zeevi compare dynamic pricing with the best fixed price in a single framework. Their theorem on critical time scales says when the comparison matters.

Setting

A seller offers one product over a horizon $T>0$. In the fluid model, the number of reviews $n(t)$ is a continuous function of time, and every purchase produces a review. The logit function is $\ell(\chi)=\exp(\chi)/(1+\exp(\chi))$. Customers share a normal prior with mean $\mu_0$, the true mean quality is $\mu$, and the learning rate is $\gamma>0$, the ratio of prior variance to rating variance. After $n$ reviews, whose average in the fluid model equals $\mu$, the posterior mean is

$$\mu(n)=\frac{1}{\gamma n+1}\,\mu_0+\frac{\gamma n}{\gamma n+1}\,\mu .$$

A price path $p$ on $[0,T]$ is piecewise continuous, and induces

$$\dot n(t)=\ell\bigl(\mu(n(t))-p(t)\bigr),\qquad n(0)=0 .$$

Its revenue is $\bar J^{\psi}_T=\int_0^T p(t)\,\ell(\mu(n(t))-p(t))\,dt$. The optimal revenue $\bar J^*_T$ is the maximum over all such paths, and $\bar J^{OFP}_T$ is the best revenue of a constant price in an allowed set $P$.

Formalization targets

The goal is Theorem 3 of the paper. If $\mu_0\ne\mu$, there is a function $\Delta:[0,\infty]\to\mathbb R$ such that

$$\frac{\bar J^{OFP}_T}{\bar J^*_T}\to\Delta(\kappa)\quad\text{as }\gamma T\to\kappa,\qquad \Delta(0)=\Delta(\infty)=1,\qquad \Delta(\kappa)<1\ \text{ for }\kappa\in(0,\infty).$$

The milestones, in order, are:

• the candidate path (13)–(14), with constant demand;
• the equivalent problem (EC.14) in demand coordinates;
• uniqueness of the root of (14) under condition (15);
• Theorem 1, the existence of an optimum and its uniqueness under (15);
• the closed-form value (16);
• the limits as $\gamma\to0$ and $\gamma\to\infty$;
• the dependence of $\bar J^*_T/T$ on $\gamma T$ alone, (EC.26);
• the sales equation for a fixed price, and the dependence of fixed-price revenue on $\gamma T$ alone, (EC.28);
• the strict loss of every fixed price when $\mu_0\ne\mu$.

Significance

The theorem sorts markets by one number. When $\gamma T$ is small, customers barely learn over the horizon, and a fixed price is nearly optimal. When $\gamma T$ is large, they learn almost at once, and a fixed price is again nearly optimal. Dynamic pricing has a value that persists in the limit only when $\gamma T$ is of order one. The sibling result for value-based reviews (Theorem 4 of the paper, not part of this mission) fails at $\kappa=\infty$, and this contrast is a main conclusion of the paper.

The formalization adds three things to the paper's result. First, the goal holds along every way that $(\gamma,T)$ approaches $\kappa$, not only with $T$ fixed. Second, it holds with no condition (15). The printed proof takes the root of (14) to be unique, which needs (15), so the mission's limit statements use a best root. Third, clause (c) has no argument in the printed proof, and here it is a stated milestone. The results are proved on paper, apart from the points just listed. A search of the platform found no formalization of them, so all are open as Lean theorems.

Difficulty

The obvious argument compares price paths pointwise. It fails at fast learning: the optimal price at $t=0$ does not converge to the limit of the price at later times, so the limit as $\gamma\to\infty$ is a statement about values and cannot be read off from (13). The second obstacle is multiplicity. Equation (14) can have three roots: for $\mu=29$, $\mu_0=-11$ and $\kappa=100$ the roots are near $-11.97$, $-6.42$ and $3.19$. An argument through a unique root covers only part of the parameter space. The third is the critical regime, where the proof must show a strict gap that survives the limit, and a fixed-price path has no closed form.

Formalization scope

Lean uses the normalization of the paper: the price sensitivity and intercept are $(\alpha,\beta)=(1,0)$, every buyer posts a review, and the horizon $T$ is real. Prices are real and may be negative, since the fluid problem drops the price constraint. Piecewise continuous means continuous on $[0,T]$ off a finite set, with finite one-sided limits. The state equation is stated in integral form, and $\bar J^*_T$ and $\bar J^{OFP}_T$ are suprema, with attainment of the former being part of Theorem 1. Limits as $\gamma T\to\kappa$ are over all pairs $\gamma,T>0$, and $\kappa$ lies in the extended nonnegative reals.

The allowed set $P$ is a parameter that must contain the static optima $p_0=\arg\max_p\{p\,\ell(\mu_0-p)\}$ and $p_\infty=\arg\max_p\{p\,\ell(\mu-p)\}$. The page's interval $[\underline p,\bar p]$ has no stated relation to these prices, and with $\mu=1$, $\mu_0=0$, $[\underline p,\bar p]=[10,11]$ the printed clauses (a) and (b) are false. Both $P=\mathbb R$ and any interval containing the two prices are instances. Uniqueness in Theorem 1 is up to a finite set of times, which is the only true form, since a path may be changed at one point. The function $\Delta$ is quantified before the limit, so that it cannot depend on $(\gamma,T)$.

A complete development needs existence and uniqueness of a scalar ODE with a piecewise continuous input, change of variables along the path, and Jensen's inequality in strict form. The logit and piecewise continuity vocabulary on an interval is reusable for other fluid models. Contributions to any milestone are welcome, and the milestones may be attacked in any order.

Selected references

• D. Shin, S. Vaccari, A. Zeevi, Dynamic Pricing with Online Reviews, SSRN working paper 3439836, version of Nov. 24, 2021. https://ssrn.com/abstract=3439836 . Published in Management Science. https://doi.org/10.1287/mnsc.2022.4387
• O. Besbes, M. Scarsini, On Information Distortions in Online Ratings, Operations Research, 2018. https://doi.org/10.1287/opre.2017.1676
• D. Crapis, B. Ifrach, C. Maglaras, M. Scarsini, Monopoly Pricing in the Presence of Social Learning, Management Science, 2017. https://doi.org/10.1287/mnsc.2016.2526
• B. Ifrach, C. Maglaras, M. Scarsini, A. Zseleva, Bayesian Social Learning from Consumer Reviews, Operations Research, 2019. https://doi.org/10.1287/opre.2019.1861
• Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science, 2017. https://doi.org/10.1287/mnsc.2015.2378

Why a static calendar

Revenue management usually assumes a firm can react: when inventory runs low it changes prices or drops products in real time. Many firms cannot. Promotions in consumer packaged goods are set on a calendar weeks ahead, and catalogue prices are printed. A static policy fixes in advance what is offered in each period and ignores how much has been sold. The question is how much revenue such a policy can guarantee against the standard upper bound, the choice-based deterministic LP.

The randomized policy that offers an assortment drawn from an LP solution was studied by Gallego, Iyengar, Phillips and Dubey (2004) and Liu and van Ryzin (2008), who found it effective and asymptotically optimal. Ma, Simchi-Levi and Zhao give the first non-asymptotic guarantee for it, with a tight dependence on the horizon and on the smallest inventory.

Setting

A firm sells $n$ items, item $i$ with inventory $b_i\in[1,T]$, over $T$ periods. Each item can be offered at prices $p_1,\dots,p_m>0$. A pair $(i,j)$ is a product and a set of products is an assortment. The feasible assortments form a downward-closed family $\mathcal S$ containing $\emptyset$.

When assortment $S$ is shown, the quantities demanded form a random vector $Q$ with a given joint law $D_S$. Quantities lie in $[0,1]$, products outside $S$ have quantity $0$, and two products of one item are never demanded together. Demand is stationary: the same laws apply in every period, independently across periods. Write $q(i,j,S)=\mathbb E_{D_S}[Q_{ij}]$.

Inventories are depleted under static substitution: a customer always sees all of $S$, so a product of a stocked-out item stays offered and its demand is lost. A product $(i,j)$ sells $\min\{B_i,Q_{ij}\}$ when $B_i$ units remain.

The LP CDLP-S maximizes $T\sum_{S}x(S)\sum_{(i,j)\in S}p_j\,q(i,j,S)$ over probability vectors $x$ on $\mathcal S$ with $T\sum_S x(S)\sum_{j:(i,j)\in S}q(i,j,S)\le b_i$ for each $i$. Its value is $\mathsf{OPT}_{\mathrm{LP}}$. Algorithm 1 solves it and, independently in every period, offers $S$ with probability $x(S)$.

For fractional demand the result needs Assumption 2: for $p_j>p_{j'}$ and $c\in[0,1]$, the fraction of untruncated demand sold when $c$ units remain, $\mathbb E[\min\{c,Q\}]/\mathbb E[Q]$, is at least as large at price $j$ (for any assortments) as at price $j'$. It holds automatically for $\{0,1\}$-valued demand.

Formalization targets

Goal: Theorem 1

Write $\underline b=\min_ib_i$ and $\Delta^{APX}(T,b)=\mathbb E[\min\{\mathrm{Bin}(T,b/T),b\}]/b$. Then

$$\mathbb E[\text{revenue of Algorithm 1}]\ \ge\ \Delta^{APX}(T,\underline b)\cdot\mathsf{OPT}_{\mathrm{LP}},$$ $$\Delta^{APX}(T,b)\ \ge\ 1-\frac{\lfloor b\rfloor^{\lfloor b\rfloor}}{\lfloor b\rfloor!}e^{-\lfloor b\rfloor},$$

and $\Delta^{APX}=1-O(1/\sqrt b)$ uniformly in $T$, non-decreasing in $b$, with $1-1/e\le\Delta^{APX}\le1$.

Milestones

In proof order:

1. $\{0,1\}$-demand satisfies Assumption 2.
2. Lemma EC.4, a mediant inequality, and (EC.5), a truncation inequality for each item.
3. Step 1: Algorithm 1 earns at least the virtual calendar, which offers each item at a single averaged price $p_{\mathsf C,i}$ with the mixture demand law.
4. Step 2: the virtual calendar's revenue is $\sum_ip_{\mathsf C,i}\mathbb E[\min\{\sum_tQ_i(\xi_t),b_i\}]$.
5. (EC.1) and Lemma EC.3: Bernoulli replacement in truncated sums.
6. Lemmas EC.7, EC.5 and EC.6: monotonicity of truncated binomials.
7. The chain closing Step 2.
8. Proposition EC.1 and its proof: $\Delta^{APX}$ is non-increasing in $T$, a finite-horizon bound, the limit, and the monotonicity of the limit term.

Significance

The bound is the guarantee of the simplest static policy for joint assortment and pricing, and the paper shows it is tight for every $T$ and $b$. It separates what commitment costs from what the LP gives: the loss is at most a factor $1-1/e$, and it vanishes at rate $1/\sqrt b$ with no dependence on $T$, $n$ or $m$. It covers multi-purchase and fractional demand, which the earlier literature did not treat.

Formalization adds three things. No static-policy guarantee in revenue management has a machine-checked proof on the platform, and this one involves an operational revenue with sequential truncation. The lemmas on $\mathbb E[\min\{c,\sum_tX_t\}]$ and on truncated binomials are general and recur in prophet inequalities and online resource allocation. The formal statement also records corrections to the paper: inequality (10) and the limit in Proposition EC.1 are false as printed for non-integral inventories, and are stated here at $\lfloor b\rfloor$. The theorem is proved in the paper and has no machine-checked proof on the platform.

Difficulty

The obvious argument treats each item separately and applies a concentration bound to the sales. Two things block it. Demand is correlated across items within a period and depends on the assortment drawn, and with several prices the revenue per unit of a truncated item depends on which price was lost. Bounding sales alone says nothing about revenue: low-price sales may survive and high-price sales may be cut. This is where Assumption 2 enters, and Proposition 1 of the paper shows the conclusion fails without static substitution.

A second obstacle is that the variables are not Bernoulli: a sharp constant needs a comparison valid for any law on $[0,1]$ with a given mean, not a tail bound. The third is the passage to finite $T$: the monotonicity of $\Delta^{APX}$ in $T$ is asserted in the paper without proof.

Formalization scope

Items are Fin n, prices Fin m, assortments Finset (Fin n × Fin m). DemandModel n m packages the prices, the family and the laws D S on Fin n × Fin m → ℝ, with the conditions above stated almost surely. Prices do not depend on the item, as in the paper. Inventories are real.

The run of Algorithm 1 is the product over Fin k of the one-period law period I x, and algRev is the expectation of the sequential revenue pathRev. $\Delta^{APX}$ is an explicit binomial sum with a real argument, so that it needs no binomial random variable. Assumption 2 is cross-multiplied, and (10) uses Nat.floor.

The goal quantifies over every feasible $x$ and every $b_0\in[1,\min_ib_i]$; an optimal $x$ and $b_0=\min_ib_i$ give the printed statement. The left side of (9) is the operational revenue, so a proof of the virtual-calendar bound alone does not close the goal. Assumption 1 and dynamic substitution are not part of this mission.

A complete development needs the Bernoulli-replacement and binomial-monotonicity lemmas, which are reusable, a limit for bounded functions of binomials, and Stirling's bound from Mathlib. Reasonable contributions include proofs of any milestone and a stand-alone convex-order library for sums of independent bounded variables.

Selected references

• W. Ma, D. Simchi-Levi, J. Zhao, Dynamic Pricing (and Assortment) under a Static Calendar, arXiv:1811.01077v5, 2020; Management Science, 2021. https://arxiv.org/abs/1811.01077v5
• G. Gallego, G. Iyengar, R. Phillips, A. Dubey, Managing Flexible Products on a Network, 2004 working paper, SSRN record 2020. https://doi.org/10.2139/ssrn.3567371
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2), 2008. https://doi.org/10.1287/msom.1070.0183
• W. Hoeffding, On the Distribution of the Number of Successes in Independent Trials, Annals of Mathematical Statistics 27(3), 1956. https://doi.org/10.1214/aoms/1177728178

Motivation

A weak measurement of a quantum system, or the amplification of a weak signal, always adds noise. The review of Clerk, Devoret, Girvin, Marquardt and Schoelkopf (arXiv:0810.4729, Rev. Mod. Phys. 82, 1155, 2010) derives the size of this unavoidable noise in a linear-response framework that assumes almost nothing about the detector: some stationary quantum system with an input port and an output port. The resulting standard quantum limit governs position measurements of nanomechanical resonators, qubit readout and the noise temperature of microwave amplifiers, and the review calls this part of the paper "the heart of the review".

Timeline. Haus and Mullen (1962) and Caves (1982, doi:10.1103/PhysRevD.26.1817) proved that a phase-preserving bosonic amplifier with large gain adds at least half a quantum of noise, for a scattering (mode-to-mode) model. Braginsky and Khalili (1996, doi:10.1103/RevModPhys.68.1, Eq. (6.36)) gave a related frequency-domain noise constraint. Averin (2003) and Clerk, Girvin and Stone (2003) stated the zero-frequency form for mesoscopic detectors. The review states the general inequality (4.11) at every frequency and derives the position-detector limit (5.62) from it.

Setting

A stationary quantum system is a unital $\ast$-algebra $\mathcal A$ of observables over $\mathbb C$, a one-parameter group $\tau_t$ of $\ast$-automorphisms (Heisenberg evolution, $x(t)=\tau_t x$), and a state $\rho_0$ (a positive normalized linear functional, written $\langle\cdot\rangle_0$) with $\rho_0\circ\tau_t=\rho_0$.

A detector on it is a pair of self-adjoint, centred observables: the input $\hat F$, which couples to the signal through $\hat H_{\rm int}=A\hat x\hat F$, and the output $\hat I$, which is read out. Its correlators $t\mapsto\langle a(t)b\rangle_0$, $a,b\in\{\hat I,\hat F\}$, are continuous and integrable. With the Fourier convention $f[\omega]=\int dt\,e^{i\omega t}f(t)$:

• the symmetrized noise $\bar S_{ab}[\omega]=\tfrac12\int dt\,e^{i\omega t}\langle\{a(t),b(0)\}\rangle_0$ (4.4) and the unsymmetrized $S_{ab}[\omega]$ (4.7);
• the Kubo gain $\chi_{ab}[\omega]=-\tfrac{i}{\hbar}\int_0^\infty dt\,e^{i\omega t}\langle[a(t),b(0)]\rangle_0$; $\chi_{IF}$ is the gain, $\chi_{FI}$ the reverse gain, and $\tilde\chi_{IF}=\chi_{IF}-\chi_{FI}^\ast$;
• $\Delta[z]=(|1+z^2|-(1+|z|^2))/2$, and the power gain $G_P=|\chi_{IF}|^2/(4\operatorname{Im}\chi_{FF}\operatorname{Im}\chi_{II})$ (5.52).

The detector measures an oscillator with susceptibility $\chi=\chi_{xx}[\omega]$, phase $\varphi=\arg\chi$. With coupling $A$, the added noise is (5.61)

$$\bar S_{xx,\rm add}[\omega]=\frac{\bar S_{II}}{|\chi_{IF}|^2A^2}+A^2|\chi|^2\bar S_{FF}+\sigma\frac{2\operatorname{Re}[\chi_{IF}^\ast\chi^\ast\bar S_{IF}]}{|\chi_{IF}|^2},\qquad\sigma=\pm1 .$$

Formalization targets

Quantum noise inequality (milestone, (4.11))

$$\bar S_{II}\bar S_{FF}-|\bar S_{IF}|^2\ \ge\ \Big|\frac{\hbar\tilde\chi_{IF}}2\Big|^2\Big(1+\Delta\Big[\frac{\bar S_{IF}}{\hbar\tilde\chi_{IF}/2}\Big]\Big),$$

for every detector and every frequency, with the milestones on the way: (4.8), the uncertainty relation (4.13), the long-time limits (4.15) and the phase-resolved bound (4.16).

Goal: the standard quantum limit ((5.62), corrected)

For a detector with $\chi_{FI}[\omega]=0$, $\chi_{IF}[\omega]\ne0$, $A\ne0$:

(a) if $\bar S_{IF}/\chi_{IF}$ is real, $\ \bar S_{xx,\rm add}[\omega]\ge\hbar|\operatorname{Im}\chi|$;

(b) the bound is attained under ideal noise (4.17), the optimal coupling (5.64), and $\bar S_{IF}/\chi_{IF}=-\sigma\frac\hbar2\cos\varphi/|\sin\varphi|$;

(c) for a detector with ideal noise and power gain $G$, with $s=|\sin\varphi|$, $c=|\cos\varphi|$, $1-s/\sqrt G>c$:

$$\bar S_{xx,\rm add}[\omega]\ \ge\ \hbar|\chi|\sqrt{s^2(1+1/G)-2s/\sqrt G}\ \xrightarrow[G\to\infty]{}\ \hbar|\operatorname{Im}\chi| .$$

The milestones (5.63), (5.65), (5.66), (5.67)–(5.68) are the steps of the page's derivation.

Significance

The limit says that a position detector with large power gain adds at least the zero-point noise of the oscillator it measures, independently of the detector's internal physics. Its relabelings give the noise-temperature limit $k_BT_N\ge\hbar\omega/2$ of voltage amplifiers (Sec. V.F) and its relatives in qubit readout ((3.35), (4.25)). The inequality (4.11) is the common source of these limits.

The printed derivation has a gap. Page 37 infers from "large power gain" that $\bar S_{IF}/\chi_{IF}$ is real. That holds for detectors with ideal noise (4.17), but not in general: passive spectra with no reverse gain and arbitrarily large power gain give added noise as small as $0.05\,\hbar|\operatorname{Im}\chi|$. The goal therefore states the bound under the exact phase hypothesis (a), and the large-gain statement for ideal detectors with an explicit finite-gain bound (c). The minimizer of (5.67) also needs $|\sin\varphi|$ in place of $\sin\varphi$. No part of the paper is machine-checked elsewhere; the platform has no item on linear-response noise or Kubo gains.

Difficulty

The uncertainty relation (4.13) is short, but the operators $\hat A,\hat B$ of (4.14) are time integrals of Heisenberg operators. They are not elements of an abstract $\ast$-algebra, so positivity has to be reached through double integrals of correlators and a $T\to\infty$ limit of Fejér type. The maximization over the phase $\delta$ in (4.16) must produce the $\Delta$ term exactly, not the weaker bound without it. Clause (c) cannot follow from (4.11) alone: the symmetrized inequality does not see the asymmetry between $+\omega$ and $-\omega$, and the finite-gain bound needs positivity of the noise matrix at each sign of the frequency separately. The obvious first idea is to take "large gain" as the hypothesis of (a); that is false, as noted above.

Formalization scope

The algebra is any unital $\ast$-algebra over $\mathbb C$, with no norm or C$^\ast$ axiom: a matrix algebra would make every integrable correlator vanish (finite dimensions give almost periodic correlators), and bounded operators would exclude the cavity detector of Sec. III.B. A proved check in the development builds a detector on bounded operators of $L^2(\mathbb R\sqcup\{\ast\})$ with $\chi_{FI}\equiv0$ and $\chi_{IF}[0]\ne0$, so the hypotheses of the goal are satisfiable. Correlators are assumed continuous and integrable; otherwise every integral would be Lean's junk value $0$. $\hbar>0$ is a parameter. $\bar S_{II},\bar S_{FF}$ are real and enter through their real parts. (5.61) is the definition of the added noise, and $\chi$ is an arbitrary complex number; the Langevin derivation is not formalized. The sign $\sigma$ is quantified because the paper's sign conventions for $\chi_{xx}$ disagree between (5.45) and (5.59). The phase is Complex.arg; $A\ne0$ and $\chi_{IF}\ne0$ exclude division by zero. The goal is about a detector; (4.11) is never a hypothesis.

Needed infrastructure: Fourier integrals of integrable correlators, Fejér-kernel limits, a Cauchy–Schwarz inequality for states, and elementary inequalities. The definitions of stationary systems, spectra and Kubo gains are reusable for fluctuation–dissipation and qubit-measurement results. Proofs of any milestone are welcome, as are proofs of the classical inequality (4.9) or of positivity of $\bar S_{II}$ as intermediate lemmas.

Selected references

• A. A. Clerk, M. H. Devoret, S. M. Girvin, F. Marquardt, R. J. Schoelkopf, Introduction to Quantum Noise, Measurement and Amplification, Rev. Mod. Phys. 82, 1155 (2010); arXiv:0810.4729v2. https://arxiv.org/abs/0810.4729
• C. M. Caves, Quantum limits on noise in linear amplifiers, Phys. Rev. D 26, 1817 (1982). https://doi.org/10.1103/PhysRevD.26.1817
• H. A. Haus, J. A. Mullen, Quantum noise in linear amplifiers, Phys. Rev. 128, 2407 (1962). https://doi.org/10.1103/PhysRev.128.2407
• A. A. Clerk, S. M. Girvin, A. D. Stone, Quantum-limited measurement and information in mesoscopic detectors, Phys. Rev. B 67, 165324 (2003). https://doi.org/10.1103/PhysRevB.67.165324
• D. V. Averin, Linear quantum measurements, in Quantum Noise in Mesoscopic Physics, ed. Yu. V. Nazarov, Kluwer (2003), pp. 205–228; arXiv:cond-mat/0301524. https://arxiv.org/abs/cond-mat/0301524
• V. B. Braginsky, F. Ya. Khalili, Quantum nondemolition measurements: the route from toys to tools, Rev. Mod. Phys. 68, 1 (1996). https://doi.org/10.1103/RevModPhys.68.1

Motivation

An online retailer stores each product in several distribution centers (DCs) and tries to ship every order from the DC next to the customer. When that DC has run out, the order can often be shipped from another DC, at a higher cost and with a longer delivery time, and some customers then walk away. Allowing such spillover is the fulfillment flexibility of the title. DeValve, Wei, Wu and Yuan study it with data from a large Chinese e-retailer (SSRN 3265838; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2021.0981). Flexibility is not free of risk: under a myopic rule that ships from the cheapest stocked DC, adding links can raise the total cost, because a DC spends inventory on distant orders that its local orders needed later.

The paper proposes spillover limit policies, which cap the amount each DC may ship on each link. The local fulfillment commitment of the retailer excludes the usual tools of the network revenue management literature, which may hold inventory back. According to the paper, no earlier work established asymptotic optimality of spillover limits under a general network with abandonment. This mission formalizes that result, Proposition 3 of the paper.

Setting

There are $N+1$ DCs, indexed by $0\le j\le N$, and a horizon of $T$ days. DC $j$ starts with inventory $r_j$. A set $A$ of ordered pairs of DCs gives the links: $(j,j')\in A$ means that DC $j$ may serve demand at DC $j'$. The unit cost of serving DC $j'$ from DC $j$ is $c_{jj'}$, and a lost sale at DC $j$ costs $p_j$. Each day a demand vector $(D^t_0,\dots,D^t_N)$ is drawn, independently across days, from a joint law with mean $\mu$. That day's arrivals are put in a uniformly random order.

An order at DC $j$ is filled locally if DC $j$ has stock: this is the local no-holdback requirement. Otherwise the customer abandons with probability $\alpha_j$. A remaining order is filled by the spillover limit policy with limits $\theta$: from the lowest cost DC $j'$ with $(j',j)\in A$ that has stock and has so far filled fewer than its limit $\theta_{j'j}$ of DC $j$ orders. If no such DC exists, the order is lost. Write $C^\theta(r,T)$ for the expected total fulfillment and lost sales cost.

The benchmark replaces demand by its mean and abandonment by a fraction. The deterministic linear program (DLP) has value $f(r)$:

$$\begin{aligned} f(r)=\min_{f,l\ge0}\ &\sum_j\Bigl(p_jl_j+\sum_{j'}c_{jj'}f_{jj'}\Bigr)\\ \text{s.t. }&l_j+\sum_{j'}f_{j'j}\ge T\mu_j,\qquad \sum_{j'\ne j}f_{j'j}\le(1-\alpha_j)(T\mu_j-f_{jj}),\\ &\sum_{j'}f_{jj'}\le r_j,\qquad f_{jj'}=0\ \text{ for }(j,j')\notin A. \end{aligned}$$

Assumption 1 says that $p_j\ge c_{jj}>0$, that $c_{j'j'}\le c_{jj'}\le p_{j'}$ on links, and that $p_{j'}+c_{jj}\le p_j+c_{jj'}$ on links. Assumption 2 says that the links are transitive and that $c_{jj''}+c_{j'j'}\le c_{jj'}+c_{j'j''}$ whenever $(j,j'),(j',j'')\in A$.

Formalization targets

Goal: Proposition 3

For base inventories $\mathbf b\ge0$ and daily demand with finite second moments, there is a constant $M$ such that for every $T\ge1$ some spillover limit policy satisfies

$$C^\theta(T\mathbf b,T)\le\Bigl(1+\frac{M}{\sqrt T}\Bigr)f(T\mathbf b).$$

The constant $M$ is chosen before $T$, and the limits $\theta$ may depend on $T$. The goal does not fix $M$, so a sharper constant does not invalidate it.

Milestones

In proof order:

1. Lemma 7: $\mathbb E[(\sum_{i\le T}X_i-T\mu)^+]\le\frac12\sqrt T\sigma$ for i.i.d. variables.
2. Lemma 8: an optimal DLP solution exists with $f^*_{jj'}>0$, $j'\ne j$, implying $f^*_{jj}=T\mu_j$.
3. The consequence of Lemma 8: one optimal solution also has $f^*_{jj}<T\mu_j\Rightarrow f^*_{jj}=r_j$.
4. Local and spillover fulfillment: under the policy with $\theta=f^*$, their expected amounts are at most $f^*$.
5. Lost sales: their expected amount at DC $j$ is at most $l^*_j+O(\sqrt T)$.
6. The additive bound: $C^\theta(T\mathbf b,T)\le f(T\mathbf b)+O(\sqrt T)$.
7. Linear scaling: $f$ at horizon $T$ is $T$ times $f$ at horizon $1$, and it is positive when some $\mu_j>0$.

Significance

The result shows that a class of simple, decentralized and easily adjusted rules loses only a vanishing fraction of the optimal cost. Combined with the paper's lower bounds $f(r)\le C^*(r)$ (Lemmas 1 and 2, not part of this mission), it gives the asymptotic tightness of the DLP bound, Corollary 1 of the paper. Assumption 2 cannot simply be dropped: the paper's Appendix B.4 gives a system violating it in which every local no-holdback policy fails to be asymptotically optimal.

The result is proved in the paper, and no machine-checked proof is known to this mission. Formalizing it produces a pathwise model of a fulfillment network with random sequencing and abandonment, which later work on fulfillment can reuse. It also pins down one correction: the printed statement has no moment assumption, while the proof needs finite variance, and the statement fails without it.

Difficulty

The obvious argument fixes $\theta=f^*$ for an optimal DLP solution and compares each amount with the DLP. It breaks in two places. First, an arbitrary optimal solution may ship out of a DC whose own demand is uncovered, and then the local no-holdback rule, which the DLP does not see, destroys the inventory the solution relies on. This is why the exchange argument of Lemma 8 is needed, and the printed repetition of that exchange still has to be shown to terminate.

Second, the lost sales cannot be bounded DC by DC, because the time at which one DC stocks out depends on the demand and the abandonment coins of the other DCs. The number of orders that stay at DC $j$ after its stockout is therefore a sum of coins over a random set of arrivals, not a binomial with a fixed number of trials as the printed proof calls it. The concentration has to go through this dependence.

Formalization scope

DCs are Fin (N + 1). The daily demand law is a PMF on DC N → ℕ, with no independence across DCs and with finite second moments assumed. The arrival sequence over $T$ days is a PMF on finite lists of pairs of a DC and a coin, and run is an explicit pathwise simulation. Inventories and limits are real; a DC has inventory when its stock is at least $1$, and a limit $\theta$ allows at most $\theta$ units. Cost ties go to the smallest index. Links contain the diagonal. Expectations are sums in $[0,\infty]$, and $f$ is a real infimum over the feasible set. The bound is stated as a product, not a ratio, so nothing divides by $f=0$.

No formalization is available in which the expected cost is a junk value: an infinite expectation is $\infty$, the policy cannot decline an eligible spillover, and $M$ precedes $T$.

A complete development needs the simulation invariants (pathwise bounds on the counts), the law of the per-DC arrival counts, a martingale or conditional second-moment bound for the coins, and an LP existence and exchange argument. The definitions of the network, of the DLP and of the arrival law are reusable for other fulfillment results. Contributions to any milestone are welcome, including a proof of Lemma 7 in general form.

Selected references

• L. DeValve, Y. Wei, D. Wu, R. Yuan, Understanding the Value of Fulfillment Flexibility in an Online Retailing Environment, SSRN 3265838, 2021. https://ssrn.com/abstract=3265838
• L. DeValve, Y. Wei, D. Wu, R. Yuan, same title, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2021.0981
• G. Gallego, G. van Ryzin, A multiproduct dynamic pricing problem and its applications to network yield management, Operations Research 45(1), 1997. https://doi.org/10.1287/opre.45.1.24
• J. Acimovic, S. Graves, Making better fulfillment decisions on the fly in an online retail environment, Manufacturing & Service Operations Management 17(1), 2015. https://doi.org/10.1287/msom.2014.0505

Mean-risk portfolio selection under a regulatory constraint

A risk measure condenses the risk of a financial position into one number, and regulators use such numbers to constrain what a financial agent may hold. Portfolio selection under a risk constraint goes back to the mean-variance problem of Markowitz (1952). Modern regulation works instead with monotone risk measures such as Value at Risk and Expected Shortfall.

A constraint of this kind can fail in a precise way. There may be portfolios whose expected excess return grows without bound while their measured risk stays nonpositive. The constraint is then void, and the mean-risk problem is ill posed. Herdegen and Khan call this $\rho$-arbitrage. Armstrong and Brigo (2019) and Armstrong and Brigo (2022) discuss its practical relevance. For $\rho$ the worst-case risk measure it is classical arbitrage of the first kind.

History, as far as it concerns this mission:

• 2002. Föllmer and Schied introduce convex risk measures, relaxing positive homogeneity on economic grounds.
• 2022. Herdegen and Khan study $\rho$-arbitrage for coherent (positively homogeneous and convex) risk measures.
• 2022. Castagnoli, Cattelan, Maccheroni, Tebaldi and Wang study star-shaped risk measures, in a setting with no underlying probability measure.
• 2024–2025. Herdegen and Khan (journal version) treat star-shaped risk functionals. This mission formalizes the preprint arXiv:2202.07610v3.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathbb P)$ and a Riesz space $L$ with $L^\infty\subset L\subset L^1$. A risk functional is a map $\rho:L\to(-\infty,\infty]$ that is monotone ($X_1\le X_2$ a.s. implies $\rho(X_1)\ge\rho(X_2)$), normalised ($\rho(0)=0$) and star-shaped ($\rho(\lambda X)\ge\lambda\rho(X)$ for $\lambda\ge1$). Neither convexity, nor cash-invariance, nor positive homogeneity is assumed.

The smallest positively homogeneous majorant of $\rho$ is

$$\rho^\infty(X):=\lim_{t\to\infty}\frac{\rho(tX)}{t}.$$

The market has a riskless asset with rate $r>-1$ and risky assets $S^1,\dots,S^d$ with $S^i_0>0$ and $S^i_1\in L$. It is nonredundant and nondegenerate. With returns $R^i=(S^i_1-S^i_0)/S^i_0$, a portfolio $\pi\in\mathbb R^d$ has excess return $X_\pi:=\pi\cdot(R-r\mathbf 1)$. Write $\mathcal X:=\{X_\pi:\pi\in\mathbb R^d\}$, $\Pi_\nu:=\{\pi:\mathbb E[X_\pi]=\nu\}$ and

$$\rho_\nu:=\inf\{\rho(X_\pi):\pi\in\Pi_\nu\}.$$

The market admits $\rho$-arbitrage if there are portfolios $(\pi_n)$ with $\mathbb E[X_{\pi_n}]\uparrow\infty$ and $\rho(X_{\pi_n})\le0$ for all $n$. The functional $\rho$ has the Fatou property on $\mathcal X$ if $\rho(X)\le\liminf_n\rho(X_n)$ for a.s. convergent sequences in $\mathcal X$ dominated in $L$. It is sensitive to large expected losses on $\mathcal X$ if every nonzero $X\in\mathcal X$ with $\mathbb E[X]\le0$ has $\rho(\lambda X)>0$ for some $\lambda>0$.

Formalization targets

Goal: Theorem 3.15

If $\rho$ has the Fatou property on $\mathcal X$ and is sensitive to large expected losses on $\mathcal X$, then

$$\rho^\infty_1>0\iff\text{no }\rho^\infty\text{-arbitrage}\iff\text{no }\rho\text{-arbitrage}.$$

Milestones, in the order of the paper's proof

1. Display (2.1): the limit defining $\rho^\infty$ exists, $\rho^\infty$ is a risk functional, and it is the smallest positively homogeneous majorant of $\rho$.
2. Proof of Theorem 3.15: the two axioms pass from $\rho$ to $\rho^\infty$ on $\mathcal X$.
3. Proposition C.1: an unbounded sequence of portfolios of bounded risk yields a nonzero $\pi$ with $\rho(\lambda X_\pi)$ bounded for all $\lambda>0$.
4. Theorem 3.8: for $\nu\ge0$ with $\rho_\nu<\infty$, the set of $\rho$-optimal portfolios is nonempty and compact.
5. Proposition 3.9: $\nu\mapsto\rho_\nu$ is star-shaped, and $\nu\mapsto\rho^\infty_\nu$ is a positively homogeneous majorant of it.
6. Proposition C.2: on a compact set, the minimum of the limit of a nondecreasing sequence of lower semi-continuous functions is the limit of the minima.
7. Proposition 3.10: $\nu\mapsto\rho^\infty_\nu$ is the smallest positively homogeneous majorant of $\nu\mapsto\rho_\nu$, $\rho^\infty_1>0$ if and only if $\nu^+<\infty$, and the three cases for $\nu_{\min}$ and $\rho_{\min}$.

Significance

Theorem 3.15 decides the absence of $\rho$-arbitrage by the sign of one number, computed from the positively homogeneous functional $\rho^\infty$. The paper calls the equivalence of $\rho$-arbitrage and $\rho^\infty$-arbitrage a key result, because it lets dual characterisations from the coherent case be lifted to convex risk measures (its Theorem 4.8). The well-posedness of the mean-$\rho$ problems (its Theorem 3.20) is a consequence as well. Remark 3.16 records, through Example A.2, that both axioms are needed for the implication from no $\rho^\infty$-arbitrage to no $\rho$-arbitrage.

These results are proved in the paper. None of them has a machine-checked proof on this platform at the time of writing. A complete development gives a Lean theory of possibly infinite-valued risk functionals on Riesz spaces, not restricted to bounded positions, and a compactness theorem for optimal portfolios.

Difficulty

The obvious argument for an optimal portfolio takes a minimising sequence and extracts a convergent subsequence, which requires boundedness. For a coherent risk measure, scaling transfers information between levels of expected return directly. A star-shaped $\rho$ has no such scaling identity: $\rho(\lambda X)$ is only bounded below by $\lambda\rho(X)$ for $\lambda\ge1$, and it can be $+\infty$.

Comparing $\rho_\nu$ with $\rho^\infty_\nu$ is similarly not formal. Proposition 3.9 gives one inequality for every risk functional, but Remark 3.11 records that minimality of $\nu\mapsto\rho^\infty_\nu$ fails without the two axioms, so the exchange of a limit in $t$ and an infimum over portfolios needs the axioms.

Formalization scope

$L$ is a Set (Ω → ℝ) of representatives satisfying IsRieszL P L. The risk functional is typed (Ω → ℝ) → EReal and constrained on $L$ only. Monotonicity uses a.s. inequality. "$X\ne0$" in the sensitivity axiom is $\neg(X=0$ a.s.$)$; a pointwise reading would make the axiom unsatisfiable, since $\rho$ vanishes on a.s. zero functions. The value $\rho^\infty(X)$ is defined as $\sup_{t\ge1}\rho(tX)/t$, and the first milestone states that this is the limit. The riskless asset is determined by $r$, and portfolios are vectors Fin M.d → ℝ. Infima of $\rho_\nu$ are in EReal, with $\inf\emptyset=+\infty$; $\nu^+$ and $\nu_{\min}$ are in ℝ≥0∞.

Nonredundancy is read for the price process, vanishing at time $0$ and a.s. at time $1$. This is the weaker of the two readings as an assumption, and it is equivalent to "$X_\pi=0$ a.s. implies $\pi=0$". Hypotheses are assumed on $\mathcal X$ only, never on all of $L$, and a statement assuming them on $L$ is not a solution.

All definitions are local to this mission. A development needs a working calculus of EReal-valued scaling and liminf, and lower semi-continuity on finite-dimensional portfolio spaces. That material, and Proposition C.2, are reusable outside this mission. Proofs of the milestones and auxiliary lemmas are welcome.

Selected references

• M. Herdegen and N. Khan, ρ-arbitrage and ρ-consistent pricing for star-shaped risk measures, arXiv:2202.07610v3, 2024. https://arxiv.org/abs/2202.07610v3 Published in Mathematics of Operations Research, 2025. https://doi.org/10.1287/moor.2023.0173
• M. Herdegen and N. Khan, Mean-ρ portfolio selection and ρ-arbitrage for coherent risk measures, Mathematical Finance 32 (2022), 226–272. https://doi.org/10.1111/mafi.12333
• E. Castagnoli, G. Cattelan, F. Maccheroni, C. Tebaldi and R. Wang, Star-shaped risk measures, Operations Research 70 (2022), 2637–2654. https://doi.org/10.1287/opre.2022.2303
• H. Föllmer and A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6 (2002), 429–447. https://doi.org/10.1007/s007800200072
• J. Armstrong and D. Brigo, Risk managing tail-risk seekers: VaR and expected shortfall vs S-shaped utility, Journal of Banking & Finance 101 (2019), 122–135. https://doi.org/10.1016/j.jbankfin.2019.01.010
• J. Armstrong and D. Brigo, Coherent risk measures alone are ineffective in constraining portfolio losses, Journal of Banking & Finance 140 (2022), 106315. https://doi.org/10.1016/j.jbankfin.2021.106315
• H. Markowitz, Portfolio selection, Journal of Finance 7 (1952), 77–91. https://doi.org/10.2307/2975974

Motivation

A decision-maker who cannot settle on one probability distribution often holds a set of plausible ones: disagreeing experts, or several models that all fit the data. Belief dominance compares options without weighting those distributions: an option is preferred when it is at least as good under every belief and strictly better under some belief. The resulting order is incomplete. It goes back to the incomplete preferences of Aumann (1962) and Bewley (2002), and it serves decision support by discarding dominated options instead of naming a single optimum.

When decisions unfold over time, one must ask whether a plan stays acceptable after information arrives. Dynamic inconsistency of non-expected-utility rules is classical (Machina 1989), and it is usually avoided by restricting the beliefs or by imposing a recursive formulation (Epstein and Schneider 2003). Ekholm and Baker (Management Science) observe that "dynamic inconsistency" covers two different failures, and they place belief dominance exactly between them.

Setting

A decision problem with multiple beliefs has first-period actions $x_1\in X_1$, a signal $y$ observed between the periods, and second-period actions in a set $X_{2,x_1,y}$. A strategy is $x=(x_1,x_2(Y))$, and $X$ is the set of all strategies. A utility $U(x_1,x_2,z)$ depends on the actions and on an outcome $z$. The set $\Phi$ holds discrete beliefs $f$ on pairs $(y,z)$, with marginal $f_Y$ and conditional $f_Z(z\mid y)$, and $\Phi_y$ is the subset with $f_Y(y)\neq 0$. The expected utilities are

$$V(x,f)=\sum_y\sum_z U(x_1,x_2(y),z)f(z,y),\qquad V_2(x_1,x_2,y,f)=\sum_z U(x_1,x_2,z)f_Z(z\mid y).$$

Strategy $x^*$ belief-dominates $x$ if $V(x^*,f)\ge V(x,f)$ for all $f\in\Phi$, strictly for some $f$. After $x_1$ and $y$, the action $x_2^*$ dominates $x_2$ if the same holds for $V_2$ over $\Phi_y$. A strategy is optimal if no strategy is strictly preferred to it, which gives the sets $X^*$ and $X^*_{2,x_1,y}$.

Fallacious inconsistency means that an optimal plan prescribes a second-period action that is not optimal in the second period. Fallible inconsistency means that a second-period action is optimal after an optimal first-period action, although every plan containing it was strictly dominated. Weak consistency means that a second-period preference between two actions extends to the two plans that differ only in that action.

Formalization targets

Goal

For every set $\Phi$ of discrete beliefs on arbitrary types and every problem whose sums exist,

$$\text{belief dominance is weakly consistent, and }\ x^*\in X^*\implies x_2^*(y)\in X^*_{2,x_1^*,y}\ \ \forall y,$$

while some such problem exhibits fallible inconsistency. The goal joins Theorem 5, its consequence through Theorem 3, and the clause of the abstract on fallible inconsistency, whose witness is the vaccine problem of §2.

Milestones

$$\succeq\text{ is a preorder};\qquad V(\tilde x,f)-V(x,f)=f_Y(y)\bigl(V_2(x_1,\tilde x_2(y),y,f)-V_2(x_1,x_2(y),y,f)\bigr);$$

Theorem 5; Theorem 3; the values of the vaccine problem of Appendix A, for example $V((\beta,\alpha,\beta),f_1)=0.8$; and the example of §2, with its seven nondominated strategies among 27.

Significance

The result says that belief dominance is safe in the sense that matters most: a decision-maker who follows a nondominated plan is never forced off it by new information, for any set of priors and with no recursive formulation. Non-expected-utility rules such as maxmin and minmax regret, whose solutions lie in the nondominated set, can still be fallaciously inconsistent, as the vaccine example shows. The price is fallible inconsistency: new options may appear acceptable that the original analysis had rejected.

The paper's theorems are proved, and no machine-checked version is known. This mission fixes the exact statement. It makes explicit which hypotheses the printed text leaves implicit, and it records the general notions of dynamic consistency on a preference relation in a form reusable for other decision rules.

Difficulty

The proofs are short, and the content of the mission is the precise statement. The natural first encoding fails: comparing second-period actions over all of $\Phi$ reads $f_Z(z\mid y)$ at beliefs where it is undefined, whereas the paper's relation lives on $\Phi_y$ while the first-period relation lives on $\Phi$. Passing between them requires handling beliefs that give the signal probability zero, which the paper's §3.4 introduces as excluded and its proof nevertheless treats. The hypothesis that the sums exist is implicit in print and has to be stated. The fallible clause is an existence statement, so it matters that it is carried by the paper's own example, which rests on exact arithmetic with the entries of Table 1.

Formalization scope

Types of actions, signals and outcomes are arbitrary. Beliefs are PMF (Y × Z). The result is for discrete beliefs: that restriction is the paper's (§3.4), and it is necessary, because with a density on $Y$ changing $x_2$ at one signal changes no value $V(x,f)$. $\Phi$ is an arbitrary set of any cardinality, not assumed convex and possibly empty. Signals of zero probability are allowed, and $\Phi_y$ may be empty, in which case all actions at $y$ are indifferent. WellPosed asserts the summability of the sum (1) for each $f\in\Phi$ and each strategy in $X$, because Lean's tsum returns $0$ otherwise, and it is required in both clauses of the goal. Dominance and indifference transcribe (3) and (4); they are not defined as parts of le. Lean's x / 0 = 0 makes $f_Z$ total, but the relations read $V_2$ only on $\Phi_y$, so a vacuous second-period comparison cannot occur by accident.

The development needs Mathlib's PMF, tsum and Summable, and nothing from the platform. The generic notions (DecisionSpace, WeaklyConsistent, ExhibitsFallacious, ExhibitsFallible) are reusable for other preference orderings. Contributions proving the theorems, and extensions covering Theorems 1, 2 and 4 of the paper, are welcome.

Selected references

• T. Ekholm, E. Baker, Multiple Beliefs, Dominance and Dynamic Consistency, Management Science, 2022 (Articles in Advance 2021). https://doi.org/10.1287/mnsc.2020.3908
• R. J. Aumann, Utility Theory without the Completeness Axiom, Econometrica 30(3), 1962. https://doi.org/10.2307/1909888
• T. F. Bewley, Knightian Decision Theory. Part I, Decisions in Economics and Finance 25, 2002. https://doi.org/10.1007/s102030200006
• L. G. Epstein, M. Schneider, Recursive Multiple-Priors, Journal of Economic Theory 113(1), 2003. https://doi.org/10.1016/S0022-0531(03)00097-8
• M. J. Machina, Dynamic Consistency and Non-Expected Utility Models of Choice under Uncertainty, Journal of Economic Literature 27(4), 1989. https://www.jstor.org/stable/2727025