All missions

Motivation

Music streaming platforms collect a subscription fee from each user and pay part of the revenue to the artists whose content was played. The industry standard is the pro-rata method: the revenue pool is divided in proportion to each artist's total number of streams across all users. A competing method, the user-centric method, divides each user's own payment among the artists that user played, in proportion to that user's streams. SoundCloud adopted it in 2021 and Deezer has campaigned for it; the debate between the two methods is documented in the literature the paper cites, among others Dimont (2017), Haampland et al. (2022), Page and Safir (2018) and Meyn et al. (2023), listed below.

Bergantiños and Moreno-Ternero (arXiv:2310.11861, published in Management Science, 2025) put the debate on an axiomatic footing. Their Theorem 1 identifies the two basic principles every reasonable method in a large family satisfies, and isolates pro-rata and user-centric inside that family by one further principle each. This mission formalizes that theorem and the steps of its proof.

Setting

There are $n$ artists $N$ and a finite set $M$ of users, $m=|M|$. A streaming problem $(N,M,t)$ records, for every artist $i$ and user $j$, the number $t_{ij}\in\mathbb N$ of times $j$ streamed content of $i$. Each user pays $1$, so the amount to share is $m$. Write

• $T_i=\sum_{j\in M}t_{ij}$, the streams of artist $i$;
• $T^j=\sum_{i\in N}t_{ij}$, the streams of user $j$;
• $L^j=\{i\in N : t_{ij}>0\}$, the artists user $j$ played, assumed nonempty for every user;
• $t_{\cdot j}=(t_{ij})_{i\in N}$, the profile of user $j$, and $t_{-j}$ the table without user $j$.

A popularity index $I$ assigns to every problem a vector $I(N,M,t)\in\mathbb R^N_{\ge 0}$ with positive sum, and artist $i$ is paid the reward

$$R^I_i(N,M,t)=\frac{I_i(N,M,t)}{\sum_{i'\in N}I_{i'}(N,M,t)}\,m .$$

Since $R^{cI}=R^I$ for every $c>0$, an index is identified with its positive multiples. The pro-rata index is $P_i=T_i$ and the user-centric index is $U_i=\sum_{j\in M}t_{ij}/T^j$. A weight system assigns a weight $\omega(j,x)>0$ to every user $j$ and every profile $x\in\mathbb N^N$; its weighted index is $I^\omega_i=\sum_{j\in M}\omega(j,t_{\cdot j})\,t_{ij}$. Pro-rata is $\omega\equiv 1$ and user-centric is $\omega(j,x)=1/\sum_i x_i$.

The axioms are:

• Homogeneity: if $t_{ij}=\lambda t_{i'j}$ for all $j\in M$, with $\lambda\ge 0$, then $I_i=\lambda I_{i'}$.
• Additivity: if $M$ splits into disjoint $M^1,M^2$, then $I(N,M,t)=I(N,M^1,t^1)+I(N,M^2,t^2)$.
• Equal individual impact of similar users: if $t_{ij}=t_{ij'}$, then $I_i(N,M\setminus\{j\},t_{-j})=I_i(N,M\setminus\{j'\},t_{-j'})$.
• Equal global impact of users: $\sum_i I_i(N,M\setminus\{j\},t_{-j})=\sum_i I_i(N,M\setminus\{j'\},t_{-j'})$ for all $j,j'\in M$.

Two further axioms of §3 compare the methods: reasonable lower bound (the artists played by a group $C$ of users receive at least $|C|$) and click-fraud-proofness (changing one user's streams moves no artist's reward by more than $1$).

Formalization targets

Goal: Theorem 1 (p. 12)

For every popularity index $I$:

$$\text{(a)}\quad I \text{ satisfies homogeneity and additivity} \iff \exists\,\omega>0:\ I=I^\omega ;$$ $$\text{(b)}\quad (n\ge 2)\quad \text{homogeneity, additivity, equal individual impact} \iff \exists\,c>0:\ I=c\,P ;$$ $$\text{(c)}\quad \text{homogeneity, additivity, equal global impact} \iff \exists\,c>0:\ I=c\,U .$$

Milestones (the proof, Appendix pp. 18–20)

1. Every weighted index satisfies homogeneity and additivity (p. 18).
2. An additive index decomposes as $I_i(N,M,t)=\sum_{j\in M}I_i(N,\{j\},t_{\cdot j})$ (p. 18).
3. On a one-user problem a homogeneous index is $I_i(N,\{j\},x)=\frac{\sum_{i'}I_{i'}(N,\{j\},x)}{T^j}\,x_i$ (pp. 18–19).
4. Theorem 1(a) as a statement on its own (p. 12).
5. Pro-rata satisfies the three axioms of (b) (p. 19).
6. Under the axioms of (b), any representing weight $\omega(j,x)$ is the same at every nonzero profile (pp. 19–20).
7. $\sum_i U_i(N,M\setminus\{j\},t_{-j})=m-1$, and user-centric satisfies the axioms of (c) (p. 20).
8. Under equal global impact, $\sum_i I_i(N,\{j\},x)$ is the same for every user and nonzero profile (p. 20).

Companions (§3, p. 13; Appendix, pp. 21–22): user-centric satisfies reasonable lower bound and click-fraud-proofness; with at least two artists, pro-rata satisfies neither.

Significance

Theorem 1 says that the choice between the two methods used in practice is a choice between two principles, and nothing else, once homogeneity and additivity are accepted: equal individual impact of similar users ("all streams count the same") gives pro-rata, and equal global impact of users ("all users count the same") gives user-centric. Part (a) describes the whole family of methods that respect the two basic axioms, which includes capped and hybrid schemes proposed in the industry (p. 10). The companion results show that the further axioms of §3 separate the two methods in favour of user-centric. The paper's further results, the core of the associated cooperative game (Theorem 2) and the core-selection characterization (Theorem 3), are separate missions of this series.

The result is proved in the paper; its proofs are in the appendix (pp. 18–22). No machine-checked version is known. A formalization fixes the model precisely, including the conventions the paper leaves implicit (the disjointness in additivity, nonempty user lists, the identification of indices up to a positive factor), and records exactly where two artists are needed.

Difficulty

The "if" directions are direct computations. The "only if" directions are a functional equation on indices: additivity reduces an index to its values on one-user problems, and homogeneity forces those values to be proportional to the profile, so the remaining freedom is one weight per user and profile. The work in (b) and (c) is to show that this weight is constant, using the extra axiom only on small auxiliary problems that contain users outside the given problem. The constant must be one number for all problems: a constant depending on the problem would make (b) and (c) much weaker, and is not what the paper proves.

Formalization scope

Artists are Fin n, indexed from $0$. Users are natural numbers, an infinite universe, and a problem is a finitely supported table ℕ →₀ (Fin n → ℕ) whose support is the user set $M$; every user of a problem therefore has a nonzero profile, which is the paper's standing assumption $L^j\neq\varnothing$, and an index can only read the columns of users in $M$. Streams are natural numbers. An index is a function from problems to Fin n → ℝ; it is a popularity index when it is nonnegative with positive sum on every problem with at least one user. The empty problem has nothing to share, and no positivity is demanded there; additivity forces the index to vanish on it. Additivity is stated for disjoint user sets: the printed axiom only says $M=M^1\cup M^2$, which with $M^1=M^2=M$ would force $I=2I$ and leave no index at all. "Is the pro-rata (user-centric) index" means "is a positive multiple of it, with one constant for all problems". Part (b) assumes at least two artists: with one artist the user-centric index satisfies its axioms and is not a multiple of pro-rata (every index then pays the whole $m$ to the single artist, so (b) holds at the level of rewards). Weights at the zero profile never enter a weighted index and are only required to be positive.

A formalization in which the positivity requirement applies to the empty problem, additivity allows overlapping user sets, or the constant in (b) or (c) depends on the problem is trivial or empty and is ruled out.

All objects are defined in one module, MusicStreaming.Axioms.Setting, on top of Mathlib's Finsupp and finite sums; nothing else is needed. Proofs of the milestones, alternative proofs of Theorem 1, and the verification that the definitions compute the paper's Example 1 are welcome.

Selected references

• G. Bergantiños and J. D. Moreno-Ternero, Revenue sharing at music streaming platforms, Management Science, 2025; preprint arXiv:2310.11861v1, 2023. https://arxiv.org/abs/2310.11861 (the source of every statement in this mission; Theorem 1 on p. 12, proofs on pp. 18–22).
• J. Meyn, M. Kandziora, S. Albers, M. Clement, Consequences of platforms' remuneration models for digital content: initial evidence and a research agenda for streaming services, Journal of the Academy of Marketing Science 51, 114–131, 2023 (reference [39] of the paper).
• J. Dimont, Royalty inequity: Why music streaming services should switch to a per-subscriber model, Hastings Law Journal 69, 675, 2017 (reference [22] of the paper).
• W. Page and D. Safir, Money in, money out: Lessons from CMOs in allocating and distributing licensing revenue, technical report, 2018 (reference [45] of the paper).
• O. Haampland, R. Johannessen, F. Moreau, P. Wikström, Fairness and royalty payment systems on music streaming platforms, mimeo, 2022 (reference [29] of the paper).

Motivation

Linear Cauchy–Riemann operators are the linearizations of the nonlinear Cauchy–Riemann equation for pseudoholomorphic curves. On the cylinder $\mathbb{R}\times S^1$ with the trivial bundle they take the form

$$D_S=\partial_s+J_0\,\partial_t+S(s,t):W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n}),$$

where $S(s,\cdot)$ converges to loops $S^\pm$ of symmetric matrices as $s\to\pm\infty$. These are the operators of Floer homology, of symplectic field theory and of contact homology. The dimension of their moduli spaces is the Fredholm index of $D_S$, and the Riemann–Roch formula with punctures computes it from the Conley–Zehnder indices of the asymptotic operators $A^\pm=-J_0\partial_t-S^\pm(t)$:

$$\operatorname{ind}D_S=\mu_{CZ}(A^+)-\mu_{CZ}(A^-).$$

This mission formalizes this formula, together with the Fredholm property of $D_S$, following C. Wendl, Lectures on Symplectic Field Theory, Lectures 3–5, in the case of the cylinder (the sphere with one positive and one negative puncture). Mathlib has the notion of a Fredholm operator but no Sobolev spaces on cylinders, no Cauchy–Riemann operators and no Conley–Zehnder index.

Setting

• Cylinder. $S^1=\mathbb{R}/\mathbb{Z}$. Maps on $\mathbb{R}\times S^1$ are maps $u(s,t)$ on $\mathbb{R}^2$ with $u(s,t+1)=u(s,t)$, and $L^p(\mathbb{R}\times S^1)$ is $L^p$ of the strip $\mathbb{R}\times[0,1)$ with Lebesgue measure. $\mathbb{R}^{2n}=\mathbb{C}^n$ with $J_0=\begin{pmatrix}0&-1\\1&0\end{pmatrix}$, multiplication by $i$.
• Sobolev space. $W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})$ is the closure of the smooth maps that vanish for large $|s|$ under the norm $\|u\|_p+\|\partial_su\|_p+\|\partial_tu\|_p$.
• Asymptotic operators. For a loop $S_\infty$ of symmetric matrices, $A=-J_0\partial_t-S_\infty(t)$. Its fundamental solution $\Psi$ solves $\Psi'=J_0S_\infty\Psi$, $\Psi(0)=\mathrm{Id}$. $A$ is nondegenerate if $1$ is not an eigenvalue of $\Psi(1)$, and $\mu_{CZ}(A)$ is the Conley–Zehnder index of the symplectic path $\Psi|_{[0,1]}$.
• Cauchy–Riemann operators. $S:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ is continuous and $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$. $D_S$ acts on $W^{1,p}$; its index is $\dim\ker D_S-\dim\operatorname{coker}D_S$.

Formalization targets

Goal: the index formula on the cylinder

If $1<p<\infty$ and the asymptotic operators $A^\pm$ are nondegenerate, then $D_S:W^{1,p}\to L^p$ is Fredholm and $\operatorname{ind}D_S=\mu_{CZ}(A^+)-\mu_{CZ}(A^-)$ (Wendl, Theorem 5.4 with Theorem 4.3, for the cylinder).

Milestones

1. Translation-invariant operators. For a nondegenerate loop $S_\infty$, $\partial_s+J_0\partial_t+S_\infty(t):W^{1,p}\to L^p$ is an isomorphism (Theorem 4.11).
2. Global regularity. An $L^p$ weak solution of $D_S\eta=f\in L^p$ lies in $W^{1,p}$ (Proposition 4.6).
3. Local estimate. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p+c\|\eta\|_p$ for $\eta$ supported in $[-R,R]\times S^1$ (Proposition 4.8).
4. Estimate on the ends. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p$ for $\eta$ supported far out in an end with nondegenerate asymptotic operator (Proposition 4.9).
5. An abstract estimate. If $\|x\|\le c\|Tx\|+c\|Kx\|$ with $K$ compact, then $\ker T$ is finite-dimensional and $T$ has closed range (Lemma 4.12).
6. Global estimate. $\|\eta\|_{W^{1,p}}\le c\|D_S\eta\|_p+c\|\eta\|_{L^p([-R,R]\times S^1)}$ (Lemma 4.13).
7. Compactness on finite cylinders. Bounded sequences in $W^{1,p}$ have subsequences converging in $L^p([-R,R]\times S^1)$ (Wendl, p. 74).
8. Semi-Fredholm property of $D_S$ (Corollary 4.14).
9. Cokernel and formal adjoint. $\dim\operatorname{coker}D_S$ is finite and equals the kernel dimension of the Cauchy–Riemann operator $D_{\bar S}$ on $W^{1,q}$, $\bar S=-CS^{\mathsf T}C$, $1/p+1/q=1$, with $C$ complex conjugation (Lemma 4.17, Proposition 4.18, Theorem 4.20).
10. Fredholm property of $D_S$ (Theorem 4.3).
11. Independence of $p$ of the kernel dimension and of the index (Theorem 4.3).
12. Classification of nondegenerate asymptotic operators. Two nondegenerate loops have the same Conley–Zehnder index if and only if they are joined by a path of nondegenerate loops (Theorem 3.34).
13. Conjugation. $\mu_{CZ}(-J_0\partial_t+CS_\infty C)=-\mu_{CZ}(-J_0\partial_t-S_\infty)$ (Lemma 5.8).
14. Model operators. $\eta\mapsto-J_0\dot\eta-\pi k\eta-\sigma e^{2\pi ikt}\bar\eta$ on loops in $\mathbb{C}$ is nondegenerate with Conley–Zehnder index $k$, for $k\in\mathbb{Z}$ and $\sigma>0$ (Lemma 5.29).
15. A plane equation without $L^2$ solutions. $\bar\partial f+\bar z\bar f=0$ has no nonzero smooth solution in $L^2(\mathbb{C})$ (Proposition 5.20).
16. A plane equation with Gaussian solutions. The smooth $L^2$ solutions of $\bar\partial f+z\bar f=0$ are the real multiples of $e^{-|z|^2/2}$ (Proposition 5.21).
17. Large antilinear perturbations. For a function $\beta$ on the cylinder with normalized zeros, $D_S+\sigma\beta\bar{\ \cdot\ }$ is onto with kernel of dimension $\#Z^+$ when all zeros are positive, and injective with cokernel of dimension $\#Z^-$ when all zeros are negative, for all large $\sigma$ (Proposition 5.27).
18. Antilinear deformations of asymptotic operators. If each asymptotic operator has the Conley–Zehnder index of an operator $-J_0\partial_t-S'^\pm$ whose deformations $-J_0\partial_t-S'^\pm-\sigma\beta_\pm\bar{\ \cdot\ }$, $\sigma\ge0$, are all nondegenerate, then $\operatorname{ind}D_S=\operatorname{wind}\beta_+-\operatorname{wind}\beta_-$ (Lemma 5.28).

Significance

The result. The index formula is the dimension formula for moduli spaces of pseudoholomorphic cylinders: Floer trajectories in Hamiltonian Floer homology and holomorphic cylinders in symplectizations. It fixes the grading of these theories, and its sign conventions are those of the Conley–Zehnder index of the asymptotic orbits.

Formalizing it. The mission builds Sobolev spaces on the cylinder, the Fredholm theory of Cauchy–Riemann operators with cylindrical ends, and the Conley–Zehnder index of asymptotic operators. These are the analytic foundations of Floer theory and symplectic field theory and are reusable for transversality arguments and for the indices of other operators. Milestone 5 is a general statement about Banach spaces.

Difficulty

The operators act between infinite-dimensional spaces of functions on a non-compact domain, so finiteness of kernel and cokernel is a global statement that sees the behaviour at both ends. The Sobolev space is defined as a closure, and the operator acts on its elements through their weak derivatives. The Conley–Zehnder index is defined through a continuous argument of a normalized complex determinant along a path of symplectic matrices, extended to a normal form; the conventions (sign of $J_0$, orientation of the cylinder, which end is positive) all enter the final formula. Several milestones are uniform estimates in which the constant is chosen before the function.

Formalization scope

• Namespace CauchyRiemannIndex. The definition module CauchyRiemannIndex_Setting defines the cylinder measure, W1p, crKernel, crRange, crIndex, IsFredholmCR, asymptotic operators through IsFundamentalSolution, IsNondegenerate and asymptoticCZIndex, and the Conley–Zehnder index czIndex of a symplectic path. The mission is standalone; czIndex and its auxiliary definitions repeat those of the ConleyZehnder mission word for word.
• Spaces. $\mathbb{R}^{2n}$ is EuclideanSpace ℝ (Fin n ⊕ Fin n), matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ, and $J_0$ is Matrix.J. Maps on the cylinder are maps ℝ × ℝ → ℝ²ⁿ, periodic in the second variable, and $L^p$ is taken on the strip $\mathbb{R}\times[0,1)$. $W^{1,p}$ is a closed subspace of Lp × Lp × Lp, consisting of triples $(u,\partial_su,\partial_tu)$.
• Exponents. $p$ is in ℝ≥0∞ with $1<p$ and $p\ne\infty$. Norms of smooth maps are eLpNorm in ℝ≥0∞; constants are in ℝ≥0.
• Indices. The Fredholm index is finrank ker - finrank (Lp ⧸ range) in ℤ; statements that use it also assert that both are finite-dimensional.
• Smoothness. Smoothness is ContDiff ℝ ∞ ($C^\infty$, not analytic). The coefficient $S$ is only assumed continuous, with uniform convergence at the ends.

Contributions welcome: general lemmas on Sobolev spaces of periodic functions, on Fredholm operators between Banach spaces, and on the Conley–Zehnder index.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lectures 3–5. https://arxiv.org/abs/1612.01009
• J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932, arXiv:1307.7239. https://arxiv.org/abs/1307.7239
• D. Salamon, Lectures on Floer homology, in Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229.
• M. Schwarz, Cohomology operations from S¹-cobordisms in Floer homology, PhD thesis, ETH Zürich (1995).

Round-Robin as a game

Round-Robin is the simplest allocation procedure for indivisible goods: agents take turns, in a fixed order, and at each turn the active agent takes her favourite good among those still available. Run on truthful preferences with additive valuations it returns an allocation that is envy-free up to one good (EF1), which is why it is the default baseline of discrete fair division. The procedure, however, only asks each agent for a ranking of the goods, and an agent may gain by misreporting: taking a good that others want early, and a good nobody else wants later, can improve her bundle. Round-Robin is therefore a game whose strategies are rankings, and the natural questions are whether it has pure Nash equilibria and whether the allocations at equilibrium are still fair.

For additive valuations the answer to the first question is known: an exact equilibrium exists, given by a profile now called the bluff profile, with a proof fragmented over Aziz, Goldberg and Walsh (2017), Bouveret and Lemaître (2016) and Amanatidis et al. (2021), as recalled on p. 7 of the paper below. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) move beyond additive agents, to valuations for which the goods already held change the value of the remaining ones. This mission formalizes their first result: for cancelable valuations, the bluff profile is an exact pure Nash equilibrium.

Setting

There are $n \ge 1$ agents $N = [n]$ and a finite set $M$ of $m$ goods. Agent $i$ has a valuation function $v_i : 2^M \to \mathbb R$ that is normalized ($v_i(\emptyset) = 0$) and non-decreasing. A valuation $v$ is cancelable if for all $S, T \subseteq M$ and every good $g \notin S \cup T$,

$$v(S \cup \{g\}) > v(T \cup \{g\}) \;\Longrightarrow\; v(S) > v(T).$$

Cancelability says that adding a common good never reverses a strict comparison. Additive valuations are cancelable; the paper notes (p. 3) that cancelable functions also generalize budget-additive, unit-demand and multiplicative valuations, and (p. 5) that neither the cancelable nor the submodular class contains the other.

A ranking $\succ_i$ is a total order on $M$. Given a profile $\boldsymbol\succ = (\succ_1, \dots, \succ_n)$, Round-Robin (Mechanism 1) runs $m/n$ rounds; in each round agents $1, \dots, n$ in turn receive $\mathrm{top}(\succ_i, S)$, the $\succ_i$-largest good of the set $S$ of goods still available. The bundle of agent $i$ is $A_i(\boldsymbol\succ)$. The profile $\boldsymbol\succ$ is an exact pure Nash equilibrium (PNE) if for every agent $i$ and every ranking $\succ_i'$,

$$v_i\big(A_i(\succ_i', \boldsymbol\succ_{-i})\big) \le v_i\big(A_i(\boldsymbol\succ)\big).$$

A strict truthful profile $\boldsymbol\succ^*$ has every agent rank the goods by non-increasing singleton value $v_i(\{g\})$, with ties broken in any fixed way. Let $h_1, \dots, h_m$ be the goods in the order Round-Robin$(\boldsymbol\succ^*)$ allocates them. The bluff profile $\boldsymbol\succ^{\mathrm b}$ has every agent report the same ranking $h_1 \succ h_2 \succ \cdots \succ h_m$.

Formalization targets

Goal: Theorem 3.2

For cancelable valuations and every strict truthful profile $\boldsymbol\succ^*$, the bluff profile is an exact PNE of Round-Robin:

$$\forall i \in N,\ \forall \succ_i' :\quad v_i\big(A_i(\succ_i', \boldsymbol\succ^{\mathrm b}_{-i})\big) \le v_i\big(A_i(\boldsymbol\succ^{\mathrm b})\big).$$

Milestones

1. Lemma 2.2. If $v$ is cancelable and $R \cap (S \cup T) = \emptyset$, then $v(S \cup R) > v(T \cup R) \Rightarrow v(S) > v(T)$, $v(S) \ge v(T) \Rightarrow v(S \cup R) \ge v(T \cup R)$, and $v(S) = v(T) \Rightarrow v(S \cup R) = v(T \cup R)$.
2. Lemma 3.3. For a cancelable valuation and $k$-element sets $X = \{x_1, \dots, x_k\}$, $Y = \{y_1, \dots, y_k\}$: if $v(\{x_j\}) \ge v(\{y_j\})$ for every $j$, then $v(X) \ge v(Y)$.
3. Fact 3.1. Round-Robin$(\boldsymbol\succ^{\mathrm b})$ and Round-Robin$(\boldsymbol\succ^*)$ return the same allocation.
4. The ordering $Y^*$ (proof of Theorem 3.2). If agent $i$ deviates to any ranking and receives $A_i$, then $A_i$ has an ordering $(y^*_1, \dots, y^*_k)$ with $v_i(\{y^*_r\}) \le v_i(\{h_{(r-1)n+i}\})$ for every round $r$.

A companion item, Proposition 2.5, states that Round-Robin$(\boldsymbol\succ^*)$ is EF1 for cancelable valuations; with Fact 3.1 and Theorem 3.2 it exhibits an exact PNE whose allocation is EF1.

Significance

The theorem gives an explicit equilibrium of Round-Robin, computable by one run of the mechanism on truthful singleton rankings, for a valuation class strictly larger than the additive one. Combined with Proposition 2.5 it shows that Round-Robin with cancelable agents always has an exact equilibrium that is EF1, so strategic behaviour need not cost fairness. The same paper shows that this fails for submodular valuations, where the best one can guarantee is a $1/2$-approximate equilibrium (the second mission of this series), and that every approximate equilibrium remains approximately EF1 (the third and fourth missions).

The result is proved in the paper; nothing about its truth is open. As far as is known, no part of it, and no part of the Round-Robin mechanism, the EF1 notion or the class of cancelable valuations, has been machine-checked. This mission formalizes the known proof and, on the way, builds a reusable model of Round-Robin as a function of reported rankings.

Difficulty

The proof compares two executions of Round-Robin: one in which everybody reports the bluff order, and one in which agent $i$ reports a different ranking. A deviation changes which goods are available at every later step, and so changes what every other agent takes; the obvious attempt, comparing agent $i$'s $r$-th good in the two runs directly, fails because her $r$-th good under the deviation may be a good that was already gone in round $r$ of the bluff run. The argument needs a reordering of the deviation bundle under which the round-by-round comparison holds, and then a set-level inequality that cancelable (not additive) valuations still support. In Lean, the main work is in the bookkeeping of the two executions: which goods are allocated before a given step, and how a change of one report propagates.

Formalization scope

Agents are Fin n with $n \ge 1$, numbered from $0$; goods form a finite type $M$ with decidable equality. Valuations are real-valued functions on Finset M, normalized and non-decreasing, hence nonnegative. A ranking is a list of all goods without repetition, most preferred first. Round-Robin is defined by recursion on steps: step $t$ (from $0$) belongs to agent $t \bmod n$, and agent $i$'s bundle collects the goods picked at her steps among the first $m$; the paper's step $(r-1)n + i$ is step $(r-1)n + (i-1)$. The bluff profile is computed from the strict truthful profile, and the theorem quantifies over every strict truthful profile, i.e. every tie-breaking. Deviations range over rankings only, as in Definition 2.4.

The paper assumes $m = kn$ "for simplicity", noting that dummy goods reduce the general case to it. Every statement that uses the round structure carries the hypothesis $|M| = kn$; the dummy-goods reduction is not formalized. Lemma 2.2 is stated for any real-valued cancelable function, which the page's proof covers. A bluff profile defined as an arbitrary equilibrium, deviations over arbitrary lists, or an EF1 computed from reports instead of true valuations would each trivialize or change the statement; none is used.

Definitions needed: valuations, cancelability, rankings and top, Round-Robin with its step bookkeeping, approximate PNE and EF1, strict truthful profiles and the bluff profile. All are in one definitions file, written to be shared with the other missions of the series. Proofs of the milestones, and lemmas about Round-Robin executions (one good per step, bundles of size $k$, the effect of changing one report), are welcome contributions.

Selected references

• G. Amanatidis, G. Birmpas, P. Lazos, S. Leonardi, R. Reiffenhäuser, Round-Robin Beyond Additive Agents: Existence and Fairness of Approximate Equilibria, arXiv:2301.13652v1, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2301.13652
• G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, WINE 2021, LNCS 13112, pp. 149–166.
• H. Aziz, P. Goldberg, T. Walsh, Equilibria in Sequential Allocation, ADT 2017, LNCS 10576, pp. 270–283.
• S. Bouveret, M. Lemaître, Characterizing Conflicts in Fair Division of Indivisible Goods Using a Scale of Criteria, Autonomous Agents and Multi-Agent Systems 30(2):259–290, 2016.
• R. J. Lipton, E. Markakis, E. Mossel, A. Saberi, On Approximately Fair Allocations of Indivisible Goods, EC 2004, pp. 125–131.

Why the price of borrowing a stock matters

To sell a stock short, an investor must first borrow it, and the owner who lends it charges a lending fee. Securities lending is a large market, and the fee varies across stocks: D'Avolio (2002) documents that shorting costs are positively related to the dispersion of investors' beliefs. Short-sale constraints have a long history in asset pricing (Miller 1977; Harrison and Kreps 1978; Jones and Lamont 2002), but most models either forbid short sales outright or take the fee as an exogenous parameter. Neither explains where the fee comes from, nor when a lending market is active at all.

Evgeniou, Hugonnier and Prieto build a dynamic general equilibrium model in which the fee is endogenous: two investors with logarithmic utility disagree about the expected return of a risky asset, and a lending agent, acting for the asset owners, sets the fee charged to short sellers to maximize the owners' fee revenue. Their §3 derives the equilibrium shorting cost in closed form at every state of the economy. This mission formalizes that derivation.

Setting

The economy has a riskless asset and two risky assets with strictly positive volatilities $\sigma_1,\sigma_2$. Asset 1 can be shorted at a cost; asset 2 cannot be shorted at all. There are two investors, an optimist $o$ and a pessimist $p$, with wealths $W^{(o)},W^{(p)}>0$. Each investor $a$ perceives market prices of risk (Sharpe ratios) $\theta^{(a)}_1,\theta^{(a)}_2$, and the optimist is more optimistic about asset 1: $\theta^{(p)}_1\le\theta^{(o)}_1$, the disagreement $\Delta\ge0$.

A short position in asset 1 pays a shorting cost $\Phi$ per dollar shorted, and a long position earns a lending yield $\Gamma$. Both are measured per unit of volatility of asset 1: $\phi=\Phi/\sigma_1$ and $\gamma=\Gamma/\sigma_1$. A position $m$ in asset 1 earns fees at the rate

$$\Lambda(m;\Phi,\Gamma)=m^+\Gamma-m^-\Phi ,$$

with $m^+=\max\{m,0\}$ and $m^-=\max\{-m,0\}$. Investor $a$ chooses wealth fractions $p=(p_1,p_2)$ with $p_2\ge0$ to solve the mean-variance problem

$$\max_{p\in\mathbb R\times\mathbb R_+}\Big\{\Lambda(p_1;\Phi,\Gamma)+p_1\sigma_1\theta^{(a)}_1+p_2\sigma_2\theta^{(a)}_2-\tfrac12(p_1\sigma_1+p_2\sigma_2)^2\Big\},$$

which is what logarithmic utility reduces to at each instant. The lending agent's revenue per unit of volatility at fee $y$ is

$$R(y)=\sum_a y\,\big(\theta^{(a)}_1+y\big)^-\,W^{(a)} .$$

An equilibrium at a state consists of these quantities such that: the no-dominance condition $\theta^{(a)}_2=\theta^{(a)}_1+\gamma$ holds for both investors (equation (7)); each investor's portfolio is optimal; asset 1, in positive supply $S_1>0$, clears; the lending market clears (fees paid by short sellers equal fees received by long holders); and $\phi$ is the least maximizer of $R$ over $y\ge\gamma$. The inactive set is $\mathcal L=\{\gamma=0\}$ and the active set $\mathcal S$ is its complement.

Formalization targets

Goal: equations (15)–(17)

At every equilibrium state,

$$\gamma=0\iff\theta^{(p)}_2\ge0,\qquad \phi=-\tfrac12\,\theta^{(p)}_1\,\mathbb 1_{\{\theta^{(p)}_2<0\}} .$$

Lending is active exactly where the pessimist perceives a strictly negative net Sharpe ratio on long positions, and there the lending agent charges half the Sharpe ratio $-\theta^{(p)}_1$ the pessimist could earn by shorting absent frictions.

Milestones, in attack order

1. Proposition 1 (p. 17): the optimal portfolios of the mean-variance problem under (7) and $\phi\ge\gamma$.
2. (11) (p. 18): the optimist is long, $\theta^{(o)}_2=\theta^{(o)}_1+\gamma>0$.
3. (14) (p. 18): $\gamma\sigma_1S_1=(\phi-\gamma)(\theta^{(p)}_1+\phi)^-W^{(p)}$.
4. (12)–(13) (p. 18): the maximizers of the revenue over $y\ge\gamma$, and their least element $\max\{\gamma,-\tfrac12\theta^{(p)}_1\}$.

Two companion statements are also included: (18) (p. 20), that the pessimist is strictly short on $\mathcal S$, and the fee flow $(\pi^{(p)}_1)^-\Phi=\tfrac14(\theta^{(p)}_1)^2W^{(p)}\mathbb 1_{\mathcal S}$ (p. 19).

Significance

The goal is the paper's description of the short market. It identifies the active set by a condition on one observable-in-principle quantity, the pessimist's net Sharpe ratio, and it gives the fee as a fixed fraction of the pessimist's frictionless Sharpe ratio. The rest of the paper rests on it: the one-asset closed forms of §4.1, the trading regions of §3.3, and the pricing results of Proposition 2 all start from (15)–(16). The fee-flow identity shows that the optimist captures a quarter of the pessimist's frictionless excess return, which is the upper bound Remark 1 attributes to any alternative fee-setting mechanism.

The result is proved in the paper, partly in the text and partly in Appendix A. Some steps are argued informally: (11) rests on the sentence "agents cannot be short simultaneously in equilibrium", and (14) on "substituting the optimal portfolios of Proposition 1 into the market clearing conditions". As far as is known, none of it has been machine-checked. A formalization makes each step explicit, including the degenerate states the text passes over. In checking the statements against each other, three printed slips were found and are corrected here (see Formalization scope).

Difficulty

The goal combines optimality, clearing and revenue maximization, and the obvious argument fails at its degenerate edge. On the inactive set the shorting cost equals the lending yield ($\phi=\gamma=0$). There Proposition 1's characterization of optimal portfolios no longer holds: portfolios that short asset 1 to buy asset 2 are also optimal. So the step "substitute the optimal portfolios" is not available, and (14) must be obtained from the clearing conditions directly in that case. Similarly the revenue maximizer is not unique on the inactive set; the shorting cost is pinned down only by the paper's selection of the least maximizer, and (16) is false for any other selection. Finally, (11) requires an argument that the two investors cannot both be short while asset 1 is in positive supply. This uses optimality of both portfolios, not just of one.

Formalization scope

Everything is stated at one state $(\omega,t)$ of the paper's continuous-time economy, about real numbers. The continuous-time economy of §2 (Brownian filtrations, consumption streams, the dynamics of wealth) is the paper's motivation and is not formalized; the formalized statements are its instantaneous equilibrium conditions. The time index is dropped throughout, and the paper's "arbitrary process $x_t$" in Proposition 1 becomes an arbitrary real number.

Conventions:

• Rates are per unit of volatility; the dollar rates are $\Phi=\phi\sigma_1$ and $\Gamma=\gamma\sigma_1$, never obtained by division.
• $m^+$ and $m^-$ are written as $\max\{m,0\}$ and $\max\{-m,0\}$; indicators are if … then … else 0.
• Dollar positions are $\pi^{(a)}_1=W^{(a)}p^{(a)}_1$.
• The standing assumptions are hypotheses of every equilibrium statement: $\sigma_1,\sigma_2>0$ (the standing assumption of §3), $S_1>0$, $W^{(o)},W^{(p)}>0$, and $\theta^{(p)}_1\le\theta^{(o)}_1$.
• The shorting-cost condition (4) is stated in its per-volatility form (10), over $y\ge\gamma$, with the least maximizer selected as in (13). A single lending agent is built in.
• Consumption clearing and asset-2 clearing are not part of the equilibrium predicate; no statement uses them, so leaving them out makes every statement more general.

Corrected slips of the page, each disclosed in the item concerned:

1. Proposition 1's "the optimal portfolio satisfies (9)" fails when $\phi=\gamma$; the converse direction is stated under $\phi>\gamma$, and the constraint $0\le x\le\theta_2$ only where $\theta_2\ge0$.
2. The indicator in (12) should be $\mathbb 1_{\{\theta^{(p)}_1+\gamma\ge0\}}$, not $\mathbb 1_{\{\theta^{(p)}_1\ge0\}}$; the least maximizer (13) is unaffected.
3. (18) prints "$\neq\emptyset$"; its proof shows the set is empty, which is what is stated.

The results (11), (13) and (14) are not built into the equilibrium predicate. With them assumed, the goal would reduce to a four-line computation; they are separate items to be proved. The definitions are short and self-contained, needing only real arithmetic from Mathlib. Proofs of the milestones, and proofs of the goal that use the milestones, are welcome.

Selected references

• T. Evgeniou, J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Swiss Finance Institute Research Paper N°22-21, version of September 22, 2022 — the source of this mission. Published as J. Hugonnier, R. Prieto, Asset Pricing with Costly Short Sales, Management Science (2024), https://doi.org/10.1287/mnsc.2023.01887, whose numbering is not used here.
• G. D'Avolio, The market for borrowing stock, Journal of Financial Economics 66 (2002), 271–306.
• C. Jones, O. Lamont, Short-sale constraints and stock returns, Journal of Financial Economics 66 (2002).
• R. Radner, Existence of equilibrium of plans, prices and price expectations in a sequence of markets, Econometrica 40 (2) (1972), 289–303.

Why bound the order-up-to level of a perishable product

Food, blood products, pharmaceuticals and many retail goods are perishable: a unit is usable for a fixed number of periods and is then discarded. A seller of such a product decides every period how much to order, what price to charge, and how much stock to deplete or dispose of. Because units of different ages coexist, the state of the system is a vector of inventory levels by remaining lifetime, and the exact dynamic program suffers from the curse of dimensionality in that vector. Nahmias's survey (Nahmias 1982) records this obstacle for the pure ordering problem; adding pricing makes it worse.

Chen, Pang and Pan (Operations Research 62(2), 2014) analyse the joint ordering, pricing and disposal problem with the tools of L♮-concavity (Murota's discrete convex analysis, extended to real vectors). Their §4 shows that the optimal profit-to-go is L♮-concave, which yields monotone policies with bounded sensitivity. Their §6.1 then shows that two one-dimensional, myopic problems bracket the optimal order-up-to level, which is the starting point of the heuristics of §6.2. This mission formalizes the backlogging case of that bracketing result, Theorem 3.

Setting

A single product has lifetime $l\ge 2$ periods; the replenishment lead time is zero, and unmet demand is backlogged. The unit costs are $c$ (ordering), $h^+$ (holding), $h^-$ (backlogging) and $\theta$ (disposal); $\gamma$ is the discount factor. The seller chooses the expected demand $d$ in an interval $\mathcal D=[\underline d,\bar d]$, which is equivalent to choosing the price $P(d)$, where $P$ is strictly decreasing. The expected revenue $P(d)\,d$ is continuous and concave on $\mathcal D$ (Assumption 1). Realized demand is $d_t=d+\varepsilon_t$, with independent, identically distributed, zero-mean noise supported in $[A,B]$, $A\le 0\le B$, and $\underline d+A\ge 0$.

The state $s=(s_1,\dots,s_{l-1})$ lies in $\mathcal S=\{s_1\le\dots\le s_{l-1}\}$: $s_i$ is the inventory with residual lifetime at most $i$ periods (negative values are backorders), and $s_{l-1}$ is the inventory position. Each period the seller picks an order-up-to level $s_l\ge s_{l-1}$, the demand level $d$, and, after demand is realized, a depletion $a$ with $s_1\vee d_t\le a\le s_l\vee d_t$. The next state is $\tilde s=(s_2-a,\dots,s_l-a)$. The one-period objective is

$$\varphi_t(s,s_l,d,a\mid\varepsilon_t)=\gamma c\,\tilde s_{l-1}-cs_l-\theta(a-d_t)-h^+(s_l-a)^+-h^-(a-s_l)^++\gamma f_{t+1}(\tilde s),$$

$g_t$ maximizes it over $a$, $G_t(s,s_l,d)=P(d)d+\mathbb E[g_t]$, and the profit-to-go is $f_t(s)=\max_{s_l\ge s_{l-1},\,d\in\mathcal D}G_t(s,s_l,d)$ with $f_{T+1}=0$.

Under $\theta\ge h^+/(1-\gamma)$ only expiring stock is disposed of (Proposition 1). With $\tilde\theta=\theta+\gamma c-h^+$ and $v_t(s_l,d_t)=-(1-\gamma)cs_l-\gamma cd_t-h^+(s_l-d_t)^+-h^-(d_t-s_l)^+$, the two myopic objectives are

$$\Pi_t(s_l,d)=P(d)d+\mathbb E[v_t(s_l,d_t)],\qquad \tilde\Pi_t(s_l,d)=\Pi_t(s_l,d)-\gamma cs_l-K\,\mathbb E[(s_l-d_t)^+],$$

with $K=\gamma h^++\dots+\gamma^{l-2}h^++\gamma^{l-1}\tilde\theta$. $\bar S_t(d)$ and $\underline S_t(d)$ are their largest maximizers over $s_l\ge0$.

Formalization targets

Goal: Theorem 3 (Bounds), backlogging case

For every period, every state $s\in\mathcal S$ and every $d\in\mathcal D$, the largest optimal order-up-to level $s_{lt}(s,d)$ satisfies

$$\underline S_t(d)\vee s_{l-1}\ \le\ s_{lt}(s,d)\ \le\ \bar S_t(d)\vee s_{l-1}.$$

Milestones, in attack order

1. Lemma 6 (p. 290): $f_t$ is nonincreasing in each coordinate of the state.
2. Proposition 1 (p. 292): if $\theta\ge h^+/(1-\gamma)$, depleting $d_t\vee s_1$ is optimal.
3. The p. 294 decomposition: $\varphi_t$ at $a=d_t\vee s_1$ equals $v_t(s_l,d_t)-\tilde\theta(s_1-d_t)^++\gamma f_{t+1}(\tilde s)$.
4. Theorem 1, first sentence (p. 291), at zero lead time: $f_t$, $g_t$, $\varphi_t$ are L♮-concave.
5. Concavity in $s_l$ (p. 295): $\Pi_t(\cdot,d)$ and $G_t(s,\cdot,d)$ are concave.
6. Upper step (p. 295): $G_t(s,s'_l,d)-G_t(s,s_l,d)\le\Pi_t(s'_l,d)-\Pi_t(s_l,d)$ for $s'_l>s_l\ge s_{l-1}$.

The proof's lower-bound display (p. 295) is not a milestone: as printed, for arbitrary $s'_l>s_l\ge s_{l-1}$, it is false when $h^+>\gamma c$ (see Formalization scope).

Significance

The result. The bounds reduce an $(l-1)$-dimensional optimization to two scalar newsvendor-type problems whose solutions do not depend on the period (Remark 6), and they give interpretable brackets: $\bar S_t(d)$ ignores the future cost of excess stock, while $\underline S_t(d)$ charges every excess unit holding until expiry and then disposal. They justify the one-dimensional heuristics of §6.2 and give a check on any computed policy.

Formalizing it. The paper's proof is short but compresses three steps that need care: the structural results of §4 at zero lead time, the minimal-disposal property, and a coupling argument for the lower bound whose printed display is not correct as stated (see below). A machine-checked development would make the whole chain from the recursion to the bounds explicit, including the existence conventions for optimal decisions. To the knowledge of this mission, none of these results has been formalized in any proof assistant.

Difficulty

The central obstacle is the concavity of $G_t(s,\cdot,d)$ in the order-up-to level. It is not visible from the one-period terms: it rests on L♮-concavity of the whole recursion (Theorem 1), and the depletion constraint $s_1\vee d_t\le a\le s_l\vee d_t$ is not an L♮-convex set, so the standard preservation lemma does not apply to (5) as written.

The lower bound needs a quantitative estimate of how much an extra unit of fresh stock can cost in the future. The printed estimate charges the expiring unit $\tilde\theta$ where an unused unit actually costs $\theta$, so it cannot hold for every pair of order-up-to levels; the lower bound must use that the comparison is only needed below $\underline S_t(d)$, where excess stock is not pushed past the next period's optimal order-up-to level.

Formalization scope

The Lean development lives in the namespace PerishablePricing.Bounds. Its conventions are:

• Carrier $\mathbb R$. The paper treats real and integer vectors at once; only the real case is formalized. L♮-convexity is defined on an explicit domain with real values, the paper's convention for "L♮-convex on a set".
• Indices. States are Fin L → ℝ with $L=l-1\ge1$, 0-based.
• Time. Time counts periods to go: f 0 = 0 is $f_{T+1}$, and $G_t$, $g_t$, $\varphi_t$ use the continuation f n.
• Maxima and expectations. The maxima in the recursion are suprema over nonempty sets whose values are bounded above, and expectations are Bochner integrals against the noise law.
• Optimal decisions. Every optimal decision is a largest maximizer, taken as a hypothesis at the points where it is used. With an arbitrary maximizer the upper bound fails when $\Pi_t(\cdot,d)$ is flat.

The standing assumptions are the hypotheses of every statement:

• nonnegative unit costs and $0\le\gamma\le1$;
• the noise conditions and the strictly decreasing inverse demand;
• Assumption 1;
• $(1-\gamma)c\le h^-$, the §4 assumption $c\le h^-/(1-\gamma)$;
• $h^+\le(1-\gamma)\theta$ with $\gamma<1$, the §6.1 assumption $\theta\ge h^+/(1-\gamma)$, which divides by $1-\gamma$.

Deviations from the page, all disclosed in the items:

• Only the backlogging case of Theorem 3 is stated. The lost-sales case rests on Theorem 2, which is not posed.
• The hypothesis "the starting inventory level of the planning horizon is zero" constrains no object of the statement, and the conclusion is stated for every state.
• $\tilde\Pi_t$'s printed term $-\gamma c\,\tilde s_{l-1}$ depends on the state and the noise. It is read as $-\gamma c\,s_l$, which leaves the maximizers unchanged.
• The objective missing from the printed definition of $\bar S_t(d)$ is $\Pi_t$.
• The upper step's "$G_t=\Pi_t+\gamma\mathbb E[f_{t+1}]$" omits a term constant in $s_l$.
• The lower-bound display of the proof of Theorem 3 is not stated. Its exponents $t+l-3$, $t+l-2$ should read $l-3$, $l-2$, and even then, for arbitrary $s'_l>s_l\ge s_{l-1}$, it fails when $h^+>\gamma c$. Example: $l=2$, deterministic demand, $c=1$, $\gamma=\tfrac12$, $h^+=h^-=1$, $\theta=2$, one period after the current one, $s_1=0$, $d=\tfrac12$, $s_l=100$, $s'_l=101$: the left side is $-3$ and the right side is $-2.75$. In that case an unused unit is disposed of at cost $\theta$, not $\tilde\theta$. Theorem 3 itself is stated as printed, with $\underline S_t(d)$ defined through $\tilde\Pi_t$.

The goal must not be trivialized. Its continuation, the concavity of $G_t$ and the monotonicity of $f_{t+1}$ are properties of the model's own recursion, never hypotheses on abstract functions. Likewise $s_{lt}(s,d)$ is defined through $G_t$, never through $\Pi_t$ or $\tilde\Pi_t$.

A complete development needs:

• L♮-concavity preservation under partial maximization over an L♮-convex set and under expectation;
• concavity of expectations of piecewise-linear functions of the noise;
• measurability and integrability of the stage value $g_t$ in the noise;
• the coupling arguments for Proposition 1 and the lower bound.

The L♮ preservation lemmas are reusable for other discrete-convexity models in inventory theory. Contributions toward any milestone, or toward that infrastructure, are welcome.

The source is the published Operations Research article. In the held scan, printed page = PDF page + 282.

Selected references

• X. Chen, Z. Pang, L. Pan, Coordinating Inventory Control and Pricing Strategies for Perishable Products, Operations Research 62(2):284–300, 2014. https://doi.org/10.1287/opre.2014.1261
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4):937–944, 2008. https://doi.org/10.1287/opre.1070.0482
• S. Nahmias, Perishable Inventory Theory: A Review, Operations Research 30(4):680–708, 1982. https://doi.org/10.1287/opre.30.4.680

The Hlawka inequality for Schatten $p$-norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge62$, also holds for every real $p\ge50$. This is an open problem: no proof is known, and the technique that reached 62 cannot go further. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-62 mission already covers every $p\ge62$, the new work is the range from 50 to 62.

The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at $p=61$, every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

• K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
• Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
• Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

• The accepted sharp diagonal bound for every real p ≥ 62.
• The accepted real coordinate bound for every real p ≥ 62.
• The accepted diagonal Schatten norm identity.

Motivation

Quantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space $\mathcal H$ and its observables by self-adjoint operators on $\mathcal H$. The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of $\mathcal H$, and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.

This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on $L^2(\mathbb R)$.

Setting

Let $\mathcal H$ be a complex Hilbert space. A (partially defined) linear operator $A$ has a domain $D(A)\subseteq\mathcal H$; it is bounded if there is $k\in\mathbb R$ with $\|A\psi\|\le k\|\psi\|$ for all $\psi\in D(A)$, and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, $A=A^*$, which includes $D(A)=D(A^*)$.

On $\mathcal H=L^2(\mathbb R)$:

1. The position operator acts by $(Q\psi)(x)=x\,\psi(x)$ on

$$D(Q)=\Big\{\psi\in L^2(\mathbb R): \int_{\mathbb R}x^2|\psi(x)|^2\,dx<\infty\Big\}\qquad\text{(eq. (3))}.$$

2. The momentum operator $P\psi=\hbar i^{-1}\,d\psi/dx$ has, in the paper's description, domain $D(P)$ consisting of the absolutely continuous functions in $L^2(\mathbb R)$.
3. Heathcote's wave function (eq. (4)) is

$$\psi(x)=\begin{cases}x^{-1}, & x\ge 1,\\ 0, & x<1.\end{cases}$$

Formalization targets

Goal

There is a unit vector of $L^2(\mathbb R)$, namely the class of $\psi$, lying in neither domain:

$$\exists\,\varphi\in L^2(\mathbb R):\quad \varphi=\psi\ \text{a.e.},\qquad \|\varphi\|=1,\qquad \varphi\notin D(Q),\qquad \varphi\notin D(P).$$

Milestones

1. Hellinger–Toeplitz (p. 2, footnote 1): a symmetric operator defined on all of a Hilbert space is bounded (an existing platform theorem).
2. Unbounded self-adjoint operators (p. 2, footnote 2): if $A=A^*$ is unbounded then $D(A)$ is dense and $D(A)\neq\mathcal H$.
3. Normalization (p. 5): $\psi\in L^2(\mathbb R)$ and $\int|\psi|^2=\int_1^\infty x^{-2}dx=1$.
4. Not in $D(Q)$ (p. 5): $\int x^2|\psi(x)|^2dx=\infty$.
5. Not in $D(P)$ (pp. 5–6): no a.e.-representative of $\psi$ is absolutely continuous on every compact interval.
6. Infinite position expectation (p. 9): $\int|x|\,|\psi(x)|^2dx=\int_1^\infty x^{-1}dx=\infty$.

Significance

The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of $\psi\in D(Q)$ is not explained by $\psi$ being "sharp in momentum", because $\psi$ is not even in $D(P)$. Milestone 6 records the physical reading: the mean position of this normalized state is infinite.

Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual $L^2$ space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.

Difficulty

The calculus is easy; the subtleties are in the bookkeeping. Elements of $L^2(\mathbb R)$ are almost-everywhere classes, so "$\psi$ is discontinuous at $1$" does not by itself show $\psi\notin D(P)$: one must rule out every a.e.-modification of $\psi$ being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives $D(A)\neq\mathcal H$ but not density, which comes from the adjoint being a genuine operator.

Formalization scope

• Operators are Mathlib's partially defined linear maps H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.
• $L^2(\mathbb R)$ is Lp ℂ 2 volume on ℝ; $D(Q)$ and $D(P)$ are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in $[0,\infty]$, so "$=\infty$" is literal and not a junk value.
• $D(P)$ follows the paper (absolutely continuous elements, i.e. having a representative absolutely continuous on every $[a,b]$) and omits the standard requirement $\psi'\in L^2$. This set contains the standard domain, so non-membership is a stronger statement.
• The paper's further claim that $\psi\notin D(H)$ for a Hamiltonian $H=P^2/2m+V$ is stated there without proof and for an unspecified potential $V$, and is not included.
• Trivialization is excluded: the goal pins $\varphi$ to the explicit function $\psi$ and requires $\|\varphi\|=1$.

Selected references

• A. Heathcote, Unbounded Operators and the Incompleteness of Quantum Mechanics, Philosophy of Science 57 (1990), 523–534.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, revised ed., Academic Press, 1980.

Motivation

This mission develops Chapter 7 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

For a matrix $M\in\mathbb F_2^{n\times k}$ of rank $k$ (the generator matrix of an $[n,k,d]_2$ linear code) and $x\in\{0,1\}^k$ define the codeword state

$$|\psi_x\rangle=\frac{1}{\sqrt n}\sum_{i\in[n]}|i,(Mx)_i\rangle .$$

For every rate $c_1>0$ there is a constant $c_0>0$ such that the following holds for all $n,k$ and all rank-$k$ matrices $M\in\mathbb F_2^{n\times k}$ with $k\ge c_1 n$: if a measurement (POVM $\{N_y\}_{y\in\{0,1\}^k}$) on $T$ copies identifies $x$ from $|\psi_x\rangle^{\otimes T}$, for $x$ drawn uniformly from $\{0,1\}^k$, with average success probability

$$\frac{1}{2^k}\sum_{x\in\{0,1\}^k}\operatorname{Tr}\!\big(N_x\,|\psi_x\rangle\langle\psi_x|^{\otimes T}\big)\ \ge\ \frac45,$$

then $T\ge c_0\,k$.

This improves the Holevo-type bound $\Omega(k/\log n)$ to the optimal $\Omega(k)$ for constant-rate codes, showing that codeword fingerprint states cannot be identified from few copies.

Formalization Note "$k=\Omega(n)$" is read as a fixed rate $k\ge c_1 n$, and the constant of $\Omega(k)$ may depend on $c_1$ only. Identifying the state means outputting $x$, which is equivalent since $x\mapsto Mx$ is injective for rank $k$. The code distance $d$ plays no role and is not a hypothesis.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 7.3.1: Barnum–Knill: the pretty good measurement is at most quadratically worse than optimal.
• Claim 7.3.5: Fourier coefficients of f composed with a linear map over F2.
• Claim 7.3.6: The maximum of (c/√t)^t on [1, c²] is e^{c²/(2e)} (for c ≥ √e).
• Fact 7.3.7: Binary entropy: H(ε) = O(ε log 1/ε) and 1 − H(1/2+ε) ≤ 2ε²/ln 2 + O(ε⁴).
• Fact 7.3.8: Binomial coefficients and their partial sums are at most 2^{nH(·/n)}.
• Fact 7.3.9: Helstrom bound for guessing a uniform bit from |ψ_b⟩, and its corollary.
• Fact 7.3.10: Subadditivity of von Neumann entropy.
• Lemma 7.4.1: Quantum PAC learners of a non-trivial class need Ω(log(1/δ)/ε) examples.
• Lemma 7.4.2: Quantum agnostic learners of a non-trivial class need Ω(log(1/δ)/ε²) examples.
• Theorem 7.4.3: Classical PAC sample complexity is Ω(d/ε + log(1/δ)/ε).
• Theorem 7.4.4: Classical agnostic sample complexity is Ω(d/ε² + log(1/δ)/ε²).
• Theorem 7.4.5: ε-average agnostic learners need (d/ε²)(1/62 − log(2d+2)/(4d)) samples.
• Theorem 7.4.6: Quantum PAC sample complexity lower bound (information-theoretic).
• Theorem 7.4.7: Quantum agnostic sample complexity lower bound (information-theoretic).
• Claim 7.5.2: Eigenvalues of an XOR-convolution matrix are scaled Fourier coefficients.
• Claim 7.5.3: Diagonal of √A in terms of Fourier coefficients of f.
• Lemma 7.5.4: Fourier coefficients of (1 − β|z|/m)^T are nonnegative and small.
• Claim 7.5.5: Counting index sequences whose basis vectors sum to S.
• Theorem 7.5.6: Optimal quantum PAC sample complexity lower bound.
• Lemma 7.5.7: PGM success bound for the PAC hard ensemble.
• Theorem 7.5.8: Optimal quantum agnostic sample complexity lower bound.
• Lemma 7.5.9: PGM success bound for the agnostic hard ensemble.
• Theorem 7.6.1: Quantum PAC lower bound under random classification noise.
• Theorem 7.6.2: Identifying a codeword state needs Ω(k) copies.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam.