All missions

Motivation

A chance constraint asks that a random inequality system hold with at least a prescribed probability $p$. Such constraints appear throughout engineering and energy optimization: reservoir and power-system management, network design, and any decision that must stay feasible against uncertain demand or inflow with high reliability. The function $x\mapsto\mathbb P(\text{constraint holds at }x)$ is called a probability function. It is in general neither convex nor smooth, even when the underlying random inequality is convex in the random vector, and this is what makes chance-constrained problems hard to solve with standard nonlinear-programming methods.

One remedy is to replace the probability function by a regular approximation and to solve a sequence of approximate problems. van Ackooij, Pérez-Aros, Soto and Vilches (arXiv:2301.09803, Mathematics of Operations Research, 2024) propose an inner regularization built from the Moreau envelope of a scalarized constraint function, for conic constraints in infinite-dimensional decision spaces. The approximate feasible sets contain the original one, and the approximate problems have smooth data. A regularization is useful only if solving the approximate problems recovers the original problem in the limit. This mission formalizes that consistency statement, Theorem 5.4 of the paper.

Setting

Let $\mathcal H$ be a separable real Hilbert space (the decision space), $\mathcal Y$ a real Banach space with dual $\mathcal Y^*$, and $\xi:\Omega\to\mathbb R^m$ a random vector on a probability space $(\Omega,\mathbb P)$ whose law has a density with respect to Lebesgue measure. A continuous map $\Phi:\mathcal H\times\mathbb R^m\to\mathcal Y$ and a nonempty closed convex cone $\mathcal K\subseteq\mathcal Y$ define the probability function

$$\varphi(x)=\mathbb P\big(\omega:\Phi(x,\xi(\omega))\in-\mathcal K\big).$$

The conic constraint is scalarized by a convex, weak$^*$-compact set $\mathcal C\subseteq\mathcal Y^*$ whose generated cone has weak$^*$ closure equal to the positive polar cone $\mathcal K^+=\{v^*:\langle v^*,v\rangle\ge0\ \forall v\in\mathcal K\}$. A convex, continuously differentiable $h:\mathcal H\to\mathbb R$ is assumed to make every scalarization $(x,z)\mapsto\langle v^*,\Phi(x,z)\rangle+h(x)$, $v^*\in\mathcal C$, jointly convex. The supremum function is $S^h_\Phi(x,z)=\sup_{v^*\in\mathcal C}\{\langle v^*,\Phi(x,z)\rangle+h(x)\}$.

For $\lambda>0$ and $\psi:\mathcal H\to\mathbb R\cup\{+\infty\}$, the Moreau envelope is $\mathrm e_\lambda\psi(x)=\inf_z\{\psi(z)+\frac1{2\lambda}\|x-z\|^2\}$. The inner regularization of $\varphi$ is

$$\varphi_\lambda(x)=\mathbb P\big(\omega:\mathrm e_\lambda S^h_\Phi(x,\xi(\omega))\le h(x)\big),$$

the envelope being taken on $\mathcal H\times\mathbb R^m$ with the Hilbert norm. For $p\in[0,1]$ put $M(p)=\{x:\varphi(x)\ge p\}$ and $M_\lambda(p)=\{x:\varphi_\lambda(x)\ge p\}$. Given a proper, convex, lower semicontinuous objective $\psi$, problem (P) minimizes $\psi$ over $M(p)$ and the regularized problem (Pλ) minimizes $\mathrm e_\lambda\psi$ over $M_\lambda(p)$, with optimal values $v(P)$ and $v(P_\lambda)$.

Formalization targets

Goal: Theorem 5.4 (p. 21)

If $\psi$ is moreover coercive and $M(p)\cap\operatorname{dom}\psi\neq\emptyset$, then

$$v(P),\ v(P_\lambda)\in\mathbb R\ \ (\lambda>0),\qquad v(P_\lambda)\xrightarrow[\lambda\to0^+]{}v(P),$$

and for $\lambda_k\to0^+$ and optimal solutions $x_k$ of $(P_{\lambda_k})$ with $x_k\rightharpoonup x_0$, the point $x_0$ is optimal for (P). If moreover $\operatorname{dom}\psi=\mathcal H$ and $\psi^*$ is Fréchet differentiable on $\operatorname{dom}\partial\psi^*$, then $x_k\to x_0$ in norm.

Milestones

1. Proposition 2.1 a), c) (p. 5): $\mathrm e_\lambda g\nearrow g$ as $\lambda\searrow0$, and $g(x)\le\liminf_k\mathrm e_{\lambda_k}g(x_k)$ for $x_k\rightharpoonup x$, $\lambda_k\searrow0$.
2. Proposition 2.6 (p. 8): $\varphi(x)=\mathbb P(S^h_\Phi(x,\xi)\le h(x))$.
3. Theorem 3.1 a), b), d) (p. 9): $\inf_{\lambda>0}\varphi_\lambda=\varphi$ monotonically; $\limsup_k\varphi_{\lambda_k}(x_k)\le\varphi(x)$; weak upper semicontinuity of $\varphi$ and $\varphi_\lambda$.
4. Proposition 5.1 (p. 19): $M_\lambda(p)\to M(p)$ in the Painlevé–Kuratowski sense, and in the Mosco sense when $h$ is sequentially weakly continuous.

Significance

Theorem 5.4 justifies the regularization as a solution method: optimal values converge, and weak limits of regularized optimal solutions solve the original problem, with strong convergence under a smoothness condition on $\psi^*$. Combined with the paper's differentiability results for $\varphi_\lambda$ (§4, not part of this mission), it reduces a nonsmooth chance-constrained problem to a sequence of problems with smooth data whose solutions approximate the true ones. The intermediate results (monotone convergence of $\varphi_\lambda$, the limsup estimate, convergence of feasible sets) are reusable for any analysis of envelope-based approximations of probability functions.

All statements are proved in the paper. None of them, and none of the general facts used (monotone and lower epi-convergence of Moreau envelopes in Hilbert space, Painlevé–Kuratowski and Mosco convergence), has a machine-checked proof on the platform at the time of writing. The mission produces a formal account of the conic scalarization, of the inner regularization, and of the consistency argument.

Difficulty

The obvious approach, "the regularized feasible sets converge, the regularized objectives converge, hence the minima converge", fails in two places. First, the decision space is infinite-dimensional, so bounded minimizing sequences only converge weakly, and the probability function must be controlled along weakly convergent sequences. This requires weak upper semicontinuity of $\varphi$ and a limsup estimate for $\varphi_{\lambda_k}(x_k)$ along weakly convergent $x_k$, which do not follow from continuity of $\Phi$. Second, convergence of values needs a liminf inequality for $\mathrm e_{\lambda_k}\psi(x_k)$ along weakly convergent sequences together with Mosco, not merely Painlevé–Kuratowski, convergence of the feasible sets. The probability function is not convex, so the usual convex-analytic route to Mosco convergence is unavailable.

Formalization scope

The Lean development uses H with [InnerProductSpace ℝ H] [CompleteSpace H] [SeparableSpace H], Y a real Banach space with dual StrongDual ℝ Y, and weak$^*$ notions through WeakDual ℝ Y. Extended-valued functions ($\psi$, $\mathrm e_\lambda\psi$, $S^h_\Phi$, $\psi^*$, $v(P)$, $v(P_\lambda)$) are EReal-valued, and infima and suprema are taken there, so no default value enters. Probabilities are ℝ≥0∞-valued. The product $\mathcal H\times\mathbb R^m$ carries the ℓ² norm (WithLp 2), as the paper requires. Weak convergence is defined through inner products. The limit $\lambda\to0^+$ is the filter of right neighbourhoods of $0$ for values and positive sequences for solutions and feasible sets.

The definitions file contains $\mathrm e_\lambda$, $\Gamma_0$, coercivity, conjugate, subdifferential, Fréchet differentiability of an extended-valued function, weak convergence, sequential weak continuity, Painlevé–Kuratowski and Mosco convergence, the conic setting (9)–(10), $S^h_\Phi$, $\varphi$, $\varphi_\lambda$, $M(p)$, $M_\lambda(p)$, $v(P)$, $v(P_\lambda)$ and optimality for (P) and (Pλ).

Two hypotheses are added to the printed statements, each used by the paper's own proofs: $\mathcal K$ is closed (the bipolar step of Proposition 2.6), and $h$ is sequentially weakly continuous in Theorem 3.1 d) and throughout Theorem 5.4. The second is automatic when $\mathcal H$ is finite-dimensional. Both are disclosed in the statements.

Trivializing readings are excluded: the feasible set meets $\operatorname{dom}\psi$; $\psi$ is proper; the envelope uses the Hilbert, not the sup, norm on the product; $S^h_\Phi$ is an extended-real supremum over a nonempty set, not a real supremum with a default value; every $\lambda$ is positive. Item b) of the goal is vacuous only when some regularized problem has no optimal solution, exactly as in the paper.

Contributions welcome: Moreau-envelope convergence in Hilbert space, the bipolar theorem for closed convex cones in Banach spaces, measure-theoretic continuity arguments for $\varphi_\lambda$, and the existence argument for optimal solutions of (P).

Selected references

• W. van Ackooij, P. Pérez-Aros, C. Soto, E. Vilches, Inner Moreau envelope of nonsmooth conic chance constrained optimization problems, Mathematics of Operations Research, 2024; arXiv:2301.09803v1, 2023. https://arxiv.org/abs/2301.09803
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Learning-augmented algorithms use a machine-learned prediction to perform better when the prediction is accurate, while keeping a worst-case guarantee when it is not. The two guarantees are called consistency (performance under a correct prediction) and robustness (performance under an arbitrary prediction). Agrawal, Balkanski, Gkatzelis, Ou and Tan (arXiv:2204.01120v1; Mathematics of Operations Research, 2024) brought this framework to mechanism design, where the input is reported by strategic agents and the designer must also keep reports truthful.

Their test case is facility location in the plane. Agents report preferred locations and a mechanism places one facility. Without predictions, the coordinatewise median achieves a $\sqrt2$-approximation for the average distance (Meir, 2019), which the paper reports as optimal among deterministic strategyproof mechanisms; the strategyproof mechanisms in the plane were characterized by Peters, van der Stel and Storcken (1993). A prediction of the optimal location can be used to beat $\sqrt2$, but only by giving up robustness. This mission targets the paper's exact description of that trade-off.

Timeline.

• 1993. Peters, van der Stel and Storcken characterize the strategyproof mechanisms in the plane; the deterministic, strategyproof, anonymous and unanimous ones are generalized coordinatewise medians.
• 2019. Meir shows the coordinatewise median is a $\sqrt2$-approximation for the average cost in $\mathbb R^2$.
• 2021. Goel and Hann-Caruthers analyze the worst-case approximation ratio of the coordinatewise median as a function of $n$ for odd $n$ (for even $n$ the tight bound $\sqrt2$ was known).
• 2022. Agrawal et al. introduce the Coordinatewise Median with Predictions (CMP) and prove Theorem 9 below.

Setting

There are $n\ge1$ agents. Agent $i$ has a preferred location $p_i\in\mathbb R^2$; the profile is $P=(p_1,\dots,p_n)$. The plane carries the Euclidean distance $d$. Placing the facility at $f$ costs

$$C^u(f,P)=\frac1n\sum_{i=1}^n d(f,p_i),$$

the utilitarian social cost. An optimal location $o(P)$ is any point minimizing $C^u(\cdot,P)$ (a geometric median of $P$).

The lower median of $m$ real numbers is the $\lceil m/2\rceil$-th smallest of them. The Coordinatewise Median with Predictions takes a prediction $\hat o\in\mathbb R^2$ and a confidence $c\in[0,1)$ such that $cn$ is an integer. It adds $cn$ copies of $\hat o$ to the agents' points and returns $f(P,\hat o,c)$, the point whose $x$-coordinate is the lower median of the $n+cn$ $x$-coordinates and whose $y$-coordinate is the lower median of the $n+cn$ $y$-coordinates. At $c=0$ this is the coordinatewise median.

A mechanism is $\alpha$-consistent if $C^u(f(P,o(P)),P)\le\alpha\,C^u(o(P),P)$ for every profile, and $\beta$-robust if $C^u(f(P,\hat o),P)\le\beta\,C^u(o(P),P)$ for every profile and every prediction $\hat o$. The approximation ratio of CMP on an instance is $r(P,\hat o,c)=C^u(f(P,\hat o,c),P)/C^u(o(P),P)$.

Formalization targets

Goal: Theorem 9

For every $c\in[0,1)$, every $n\ge1$ with $cn\in\mathbb Z$, every profile $P$, every optimal location $o$ of $P$ and every prediction $\hat o$,

$$C^u\big(f(P,o,c),P\big)\le\frac{\sqrt{2c^2+2}}{1+c}\,C^u(o,P),\qquad C^u\big(f(P,\hat o,c),P\big)\le\frac{\sqrt{2c^2+2}}{1-c}\,C^u(o,P).$$

The constants are exact: Lemma 8 shows both are attained, so no weaker goal would be the paper's theorem.

Milestones

The paper's proof reduces every instance to a one-parameter family. The milestones follow it:

• Lemmas 26, 27, 28 (pp. 23–24): moving a point along its ray from the optimum keeps the optimum; moving a point towards the optimum without changing CMP's output worsens a ratio above $1$; two points moving towards each other get closer in total to a third point, strictly when not collinear.
• Lemmas 15, 16 (p. 20): two conditions under which a strictly worse instance exists.
• Lemma 17 (p. 20): a bound valid on the Optimal-on-Axes (OA) and Clusters-on-Axes (CA) families holds everywhere.
• Lemmas 18, 24, 25 (pp. 20–22): OA and CA instances can be moved into the Clusters-and-Opt-on-Axes (COA) classes without improving the ratio.
• Lemma 7 (p. 13): a bound on the COA classes holds everywhere.
• Lemma 8 (p. 13): explicit COA instances attaining both constants.

The COA classes contain the instances with $o(P)=(0,1)$, CMP output $(0,0)$, and all points in $\{(0,1),(x,0),(-x,0)\}$ for one $x\ge0$.

Significance

The result. Theorem 9 gives a one-parameter menu of guarantees. At $c=0$ both bounds equal Meir's $\sqrt2$. As $c\to1$ consistency tends to $1$ while robustness grows without bound. The paper's Theorem 10 shows that no deterministic, strategyproof, anonymous mechanism improves on this menu (Pareto optimality), and its Theorem 12 refines the bound as a function of the prediction error, building on Theorem 9. It is one of the first exact consistency–robustness trade-offs for a mechanism design problem.

Formalizing it. The theorem is proved in the paper; nothing about it is machine-checked. A formal proof would check a reduction argument that runs over several pages and many cases (Lemmas 15–25, Appendix A). It would also check two delicate conventions on which the bounds rest: the lower median of $n+cn$ values, and the Euclidean metric. The model layer (Euclidean utilitarian cost, the geometric median as a minimizer, coordinatewise medians with phantom points) is reusable for other planar facility-location mechanisms.

Difficulty

The cost $C^u(f(P,\hat o,c),P)$ is not a convex or even continuous function of the profile, because the median jumps. So the worst case cannot be found by local optimization over the profile, and the geometric median $o(P)$ has no closed form. The paper instead transforms an arbitrary instance into a structured one step by step. Each step must keep three things under control at once: CMP's output, the optimal location (which can move when points move), and a ratio that may only increase. Several steps change the number of agents or regroup clusters (the four-fold copying after Lemma 7, the instances invoked in the proofs of Lemmas 21 and 22), so the argument is not an induction over a fixed $n$. The obvious approach, the triangle inequality $d(f,p_i)\le d(f,o)+d(o,p_i)$ agent by agent, needs a bound on $d(f,o)$ in terms of $C^u(o,P)$; but the median is controlled by counts of points, not by distances, and bridging the two is exactly what the reduction does.

Formalization scope

All declarations live in the namespace LearnAugFL.CMP, in one definitions module and one module per theorem.

• The plane is EuclideanSpace ℝ (Fin 2), with the Euclidean dist. Profiles are P : Fin n → Pt; CMP depends only on the multiset of points.
• CMP is cmp P ô k: each coordinate is the lower median of the agents' coordinates together with k copies of the prediction's. Admissible c n k states $n\ge1$ and $k=cn$, so the constants are functions of the same $c$ that fixes $k$.
• An optimal location is a hypothesis IsOpt P o (a minimizer of $C^u(\cdot,P)$), not a chosen function. Every statement quantifies over every optimal location; geometric medians of collinear profiles need not be unique.
• Bounds are cross-multiplied. Ratios ratio P ô o k appear only in the reduction lemmas. There, the families force a positive optimal cost, so no ratio is a junk $0/0$.
• "CMP is $\alpha$-consistent for $\alpha=\max$ over a family" (Lemmas 7 and 17) is stated as: every bound valid on the family is valid everywhere. This does not presuppose that the maximum is attained.
• "There exists an instance $Q$" allows $Q$ to have any number of agents, as in the paper's proofs.
• Lemma 8 assumes that some $n_0$ makes $cn_0$ an integer, the standing assumption without which no instance exists.
• Definition 13 (3) is read over points $p_i\ne o(P)$, and its clause (e) uses the $y$-clusters $(0,-y_1),(0,y_2)$. Both printed versions are slips.

Trivializing encodings are ruled out explicitly:

• ℝ × ℝ carries the sup metric, under which the bounds are a different statement.
• The upper median, or the median of the agents alone, is a different mechanism.
• Letting $k$ vary independently of $c$ decouples the constants from the mechanism.

Contributions welcome: proofs of the milestones in any order; facts about the lower median of a multiset under insertion of phantom values; and first-order optimality of the geometric median (a subgradient characterization), which Lemma 26 and the instances of Lemma 8 need and Mathlib does not have.

Selected references

• P. Agrawal, E. Balkanski, V. Gkatzelis, T. Ou, X. Tan, Learning-Augmented Mechanism Design: Leveraging Predictions for Facility Location, arXiv:2204.01120v1, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2204.01120v1
• S. Goel, W. Hann-Caruthers, Optimality of the coordinate-wise median mechanism for strategyproof facility location in two dimensions, 2021 (as cited in arXiv:2204.01120v1).
• R. Meir, Strategyproof facility location for three agents on a circle, International Symposium on Algorithmic Game Theory (SAGT), Springer, 2019, pp. 18–33.
• H. Peters, H. van der Stel, T. Storcken, Range convexity, continuity, and strategy-proofness of voting schemes, ZOR Methods and Models of Operations Research 38(2):213–229, 1993.

Motivation

The trade-off capacity region of a quantum channel characterizes the optimal net rates at which a sender can communicate classical, quantum, and entangled bits to a receiver by exploiting many independent uses of the channel, along with the help of the same resources. Similarly, one can consider a trade-off capacity region when the noiseless resources are public, private, and secret key bits. In [Phys. Rev. Lett. 108, 140501 (2012)], we identified these trade-off rate regions for the pure-loss bosonic channel and proved that they are optimal provided that a longstanding minimum output entropy conjecture is true. Additionally, we showed that the performance gains of a trade-off coding strategy when compared to a time-sharing strategy can be quite significant. In the present paper, we provide detailed derivations of the results announced there, and we extend the application of these ideas to thermalizing and amplifying bosonic channels. We also derive a "rule of thumb" for trade-off coding, which determines how to allocate photons in a coding strategy if a large mean photon number is available at the channel input. Our results on the amplifying bosonic channel also apply to the "Unruh channel" considered in the context of relativistic quantum information theory.

This mission is the statement-level formalization of Quantum trade-off coding for bosonic communication (arXiv:1105.0119v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal entropy: convergent power series (Lemma 4: thermal entropy power series, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 3 / (1), (28)–(30): pure-loss quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Proposition 1: regularized quantum dynamic formula (background reformulation): Canonical interpretation and full domain of unrestricted infinite-dimensional entropy differences (source-ambiguity)
• Proposition 2: degradable private dynamic formula (background reformulation): Canonical interpretation and full domain of unrestricted infinite-dimensional entropy differences (source-ambiguity)
• Theorem 7 / (2), (48)–(50): pure-loss private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• Theorem 8: unconditional entanglement-assisted quantum slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 9: thermal-noise quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 10: thermal-noise private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• Theorem 11: amplifier quantum dynamic achievability: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• Theorem 12: amplifier private dynamic achievability: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §III B, (40)–(41): pure-loss classical–quantum achievable slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III B, (42)–(43): pure-loss assisted/unassisted classical achievable slice: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III F, (58)–(59): public/private and public/key achievable slices: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §III G: conditional full quantum dynamic capacity: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III G.1: conditional CE and CQ capacity slices: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §III H, (77)–(79): conditional full private dynamic capacity: Full-Fock forward public/private/key consuming and generating block protocols, joint recovery/security, and independent asymptotic signed (R,P,S) region (hard)
• §IV A, (81)–(82) and CE display: thermal-noise achievable slices: Full-Fock energy-constrained signed (C,Q,E) block protocols and their independently defined asymptotic operational region (hard)
• §VI / Figure 7: mean-photon encoding versus single-excitation Unruh encoding: Physical two-use full-Fock vacuum amplifier precomposed with the dual-rail isometry, and both of its operational CQ/CE slices (hard)

Selected references

• Quantum trade-off coding for bosonic communication, arXiv:1105.0119v4, https://arxiv.org/abs/1105.0119v4

Motivation

We present an efficient family of quantum circuits for a fundamental primitive in quantum information theory, the Schur transform. The Schur transform on n d-dimensional quantum systems is a transform between a standard computational basis to a labelling related to the representation theory of the symmetric and unitary groups. If we desire to implement the Schur transform to an accuracy of epsilon, then our circuit construction uses a number of gates which is polynomial in n, d and log(1/epsilon). The important insights we use to perform this construction are the selection of the appropriate subgroup adapted basis and the Wigner-Eckart theorem. Our efficient circuit construction renders numerous protocols in quantum information theory computationally tractable and is an important new efficient quantum circuit family which goes significantly beyond the standard paradigm of the quantum Fourier transform.

This mission is the statement-level formalization of The Quantum Schur Transform: I. Efficient Qudit Circuits (arXiv:quant-ph/0601001v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite Gelfand–Zetlin labels fit in binary registers (III B: finite GZ labels and binary storage, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract/I/V C: efficient qudit Schur transform: A phase-compatible GZ/YY Schur analysis map and a clean, uniform qubit compiler with charged reversible classical work. (hard)
• III B, Eq.(29): reversible YY path compression: A bit-costed clean reversible rank/unrank program for valid one-box YY paths, implementing Eq.(29). (hard)
• IV B: coherent Schur cascade and composable cost: A constructed physical-space-to-GZ/YY cascade and row-label reversible schedule, tied to local CG maps. (hard)
• V opening: direct synthesis for fixed d: A fixed-d all-label GZ CG target with a uniform circuit-construction program and controlled-label synthesis costs. (hard)
• V B, Eqs.(46)–(54), Figs.4–5: dimension-reducing CG factorization: Compatible subgroup branching coordinates and total padded reduced-Wigner blocks controlled on the retained lower output. (hard)
• V C: efficient coherent reduced Wigner synthesis: An independently defined controlled reduced-Wigner target and an executable clean synthesis of it with numerical-error accounting. (hard)
• V C, Algorithm: Clebsch–Gordan transform: A source-compatible finite GZ one-box CG analysis map, clean recursive circuit interpreter and uniform d^3 polylog cost contract. (hard)
• III B: unfulfilled optimal-width GZ compression promise: A specified optimal-width GZ rank/inverse algorithm and a pinned meaning of efficient. (source-ambiguity)

Selected references

• The Quantum Schur Transform: I. Efficient Qudit Circuits, arXiv:quant-ph/0601001v1, https://arxiv.org/abs/quant-ph/0601001v1

Motivation

Online marketplaces (ride-sharing, delivery, freelance labour) set payments for their suppliers and want to know how a change in payment would change the platform's utility. The standard tool, a randomized A/B test, is biased in a marketplace: treated and control suppliers compete for the same demand, so a payment increase given to the treatment group draws business away from the control group. This interference violates the no-interference assumption of classical causal inference (Hudgens and Halloran, 2008), and it was documented on a large platform by Blake and Coey (2014). Global experimentation, changing the payment for everyone and comparing days, avoids interference but is slow and costly.

Wager and Xu (2021) propose local experimentation: give every supplier a small, symmetric, random payment perturbation, measure how participation responds to one's own perturbation, and correct for the equilibrium feedback using a model of how demand is matched to suppliers. The perturbations are symmetric, so they do not move the market equilibrium at first order. The paper shows that in a large market this recovers the gradient of the platform's equilibrium utility. This mission formalizes that result, Theorem 6 of the paper, together with the lemmas on which its proof rests.

Setting

Everything is conditional on a global state $A = a$ (weather, holidays), which is dropped from the notation. In the $n$-th system there are $n$ potential suppliers and a random demand $D \sim F^{(n)}$ on $[0,\infty)$ with $\mathbb E[D/n] = d > 0$, $\mathbb E[(D/n - d)^2] \to 0$ and $\mathbb P(D/n \notin [d/2, 2d]) = o(1/n)$.

Matching. If $t$ suppliers are active and demand is $d$, each active supplier serves on average $\Omega(d,t)$ units. $\Omega$ is non-decreasing in $d$, non-increasing in $t$, and $\Omega(d,t) = \omega(d/t) + l(d,t)$, where the error $l \ge 0$ is bounded and $o(1/\sqrt t + 1/\sqrt d)$, and $\omega$ is a regular allocation function: $\omega : \mathbb R_+ \to [0,1]$ is smooth, concave, non-decreasing, $\omega(0^+) = 0$, $\lim_{x\to\infty}\omega(x) \le 1$, $\omega'(0^+) \le 1$.

Choice. Supplier $i$ has a private feature $B_i \sim \beta$ and is paid $P_i$ per unit served. Given its expected revenue $x$, it becomes active ($Z_i = 1$) with probability $f_{B_i}(x)$, where each choice function $f_b$ is $[0,1]$-valued, non-decreasing and twice differentiable with uniformly bounded second derivative.

Equilibrium. With $X \sim \mathrm{Binomial}(n,\mu)$ independent of $D$, let $q^{(n)}(\mu) = \mathbb E[\Omega(D,X)]$. Under a payment law $\pi$, the equilibrium supply fraction $\mu^{(n)}(\pi)$ solves the balance equation

$$\mu = \mathbb E\bigl[f_{B}\bigl(P\,q^{(n)}(\mu)\bigr)\bigr],\qquad B \sim \beta,\ P \sim \pi.$$

At a fixed payment $p$, $\mu^{(n)}(p) = \mu^{(n)}(\delta_p)$. The mean-field supply $\mu(p)$ solves $\mu = \mathbb E[f_B(p\,\omega(d/\mu))]$, and the mean-field platform utility is

$$u(p) = \bigl(r(d/\mu(p)) - p\,\omega(d/\mu(p))\bigr)\,\mu(p),$$

with $r$ the limiting revenue per unit of supply. The marginal response is $\Delta(p) = \omega(d/\mu(p))\,\mathbb E[f_B'(p\,\omega(d/\mu(p)))]$, and $\Delta^{(n)}(p)$ is its pre-limit analogue.

The experiment. Payments are $P_i = p + \zeta_n\varepsilon_i$ with independent signs $\varepsilon_i = \pm 1$. From $\bar D = D/n$, $\bar Z = \frac1n\sum_i Z_i$ and the regression slope

$$\hat\Delta = \zeta_n^{-1}\,\frac{\sum_i (Z_i - \bar Z)(\varepsilon_i - \bar\varepsilon)}{\sum_i (\varepsilon_i - \bar\varepsilon)^2},$$

form $\hat\Upsilon = \hat\Delta / \bigl(1 + p\bar D\hat\Delta\,\omega'(\bar D/\bar Z)/(\bar Z^2\omega(\bar D/\bar Z))\bigr)$ and

$$\hat\Gamma = \hat\Upsilon\bigl[r(\bar D/\bar Z) - p\,\omega(\bar D/\bar Z) - (r'(\bar D/\bar Z) - p\,\omega'(\bar D/\bar Z))\,\bar D/\bar Z\bigr] - \omega(\bar D/\bar Z)\,\bar Z.$$

Formalization targets

Goal: Theorem 6

For $p > 0$ with $\mathbb E[f_B(p\,\bar\omega)] > 0$ ($\bar\omega = \sup\omega$), $\zeta > 0$ and perturbation sizes $\zeta_n = \zeta n^{-\alpha}$ with $0 < \alpha < 1/2$,

$$\lim_{n\to\infty}\mathbb P\Bigl[\bigl|\hat\Gamma - u'(p)\bigr| > \varepsilon\Bigr] = 0 \quad\text{for every } \varepsilon > 0.$$

Milestones, in the order of the proof

1. Lemma 1: the balance equation has a unique solution in $[0,1]$, and the active supply is $\mathrm{Binomial}(n, \mu^{(n)}(\pi))$.
2. Proposition 10: $\frac{d}{d\mu}q^{(n)}(\mu) \le 0$, and $\frac{d}{d\mu}q^{(n)}(\mu) \to -\omega'(d/\mu)\,d/\mu^2$.
3. Lemma 2 (3.13)–(3.14): $\mu^{(n)}(p) \to \mu(p)$ and $q^{(n)}(\mu) \to \omega(d/\mu)$.
4. Lemma 4: the implicit derivative of $\mu^{(n)}(p)$ in terms of $\Delta^{(n)}(p)$, and its mean-field limit $\mu'(p) = \Delta(p)/(1 + p\,d\,\Delta(p)\,\omega'(d/\mu)/(\mu^2\omega(d/\mu)))$.
5. Proposition 11: the perturbed equilibrium $\mu^{(n)}(p,\zeta)$ is flat at $\zeta = 0$ with second derivatives bounded uniformly in $n$.
6. Proposition 12 (second equality): the closed form of $u'(p)$.
7. (A.9): $|\zeta^{-1}\mathrm{Cov}_n[Z_i,\varepsilon_i] - \Delta^{(n)}(p)| \le \zeta C$, uniformly in $n$.
8. (A.7), corrected: $\bar D \to d$, $\bar Z \to \mu(p)$, $\hat\Delta \to \Delta(p)$ in $L_2$, and $\hat\Upsilon \to \mu'(p)$ in probability.

Significance

A platform can thus learn the payment sensitivity of its equilibrium utility from one period of data, with perturbations that vanish as the market grows. The gradient estimate is the input to the first-order payment-optimization scheme of §4.2 of the paper, and the decomposition of Lemma 4 separates the measurable marginal response $\Delta$ from an interference correction that depends only on the matching function $\omega$.

None of these results has been machine-checked. A complete formalization gives a verified mean-field limit for a fixed-point equilibrium with binomial supply, a binomial Stein-type identity (Proposition 10), and a consistency proof for a regression estimator under vanishing perturbations. The mission also records two corrections. The $L_2$ claim for $\hat\Upsilon$ in (A.7) is too strong as printed. Lemma 15 (Appendix B.3), used in Proposition 10's proof, omits a factor; Proposition 10 itself is not affected.

Difficulty

The obvious argument says that $\hat\Delta$ is a regression slope, so it converges by the law of large numbers. It does not apply directly, for two reasons. First, the $Z_i$ are not sampled at the unperturbed equilibrium: the perturbation itself moves the equilibrium, and the experiment runs at $\mu^{(n)}(p,\zeta_n)$. Showing that this shift is $O(\zeta_n^2)$ uniformly in $n$ (Proposition 11) needs the implicit-function structure of the balance equation and the symmetry of the perturbation. Second, the noise in $\hat\Delta$ has standard deviation of order $1/(\zeta_n\sqrt n)$, while its bias is of order $\zeta_n$. The rate restriction $\alpha < 1/2$ balances the two. Finally, the limit of $\frac{d}{d\mu}q^{(n)}$ is a derivative of an expectation over a binomial law in which the error term $l$ is multiplied by $n$; controlling it needs a Stein-type identity, not term-by-term convergence.

Formalization scope

All objects live in the namespace EquilibriumExperiment.Gradient. A Market B holds the primitives for one global state; Market.Standing bundles Definition 5, Assumptions 1–2, the part of Assumption 3 that concerns $r$, and the demand conditions (3.1)–(3.2). Conventions:

• One state. The statements are conditional on $A = a$. The state space is finite with a law independent of $n$, so the paper's unconditional probability is a finite mixture of conditional ones.
• Domains. Functions on $\mathbb R_+$ are functions on $\mathbb R$ whose hypotheses are stated on $[0,\infty)$; $\omega$ and $r$ are smooth on $(0,\infty)$. With Lean's $d/0 = 0$, the decomposition at $t = 0$ reads $\Omega(d,0) = l(d,0)$.
• Added hypotheses, disclosed. $d > 0$; measurability of $\Omega(\cdot,t)$, $(b,x)\mapsto f_b(x)$ and $f_b'(x)$; the joint reading of $o(1/\sqrt t + 1/\sqrt d)$ (for every $\varepsilon$ there is $K$ such that the bound holds when $d,t \ge K$); and the positivity condition $\mathbb E[f_B(p\,\bar\omega)] > 0$, which holds exactly when $\mu(p)$ exists.
• Equilibria. $q^{(n)}$ is the finite binomial sum. $\mu^{(n)}$ and $\mu(p)$ are defined as the solutions of their balance equations; Lemmas 1 and 2 prove that the solutions exist and are unique. Supplier decisions are realized as $Z_i = \mathbf 1\{U_i \le f_{B_i}(P_i\,q^{(n)}(\mu^{(n)}(\pi)))\}$ with independent uniforms $U_i$.
• Limits. Each $n$ has its own sample space, so convergence in probability is a limit of the probabilities of deviation events. $L_2$ convergence is eLpNorm … 2 → 0.
• Ranges. "$n \in \mathbb N$" is read as $n \ge 1$, and binomial parameters lie in $[0,1]$. Proposition 10's limit is stated for $\mu < 1$, and Proposition 11 for $\zeta \in (-p,p)$.

Ruled out: $Z_i$ independent of the perturbation, $\mu^{(n)}$ an arbitrary random variable rather than the solution of (A.2), hypotheses on all of $\mathbb R$, or $u'(p)$ as a deriv of a non-differentiable function (Proposition 12 proves differentiability).

Not in this mission. Theorem 7 (the $O(1/T)$ regret of the first-order method) is false as printed: with $\sigma = 1/2$, $\eta = 101/50$, $M = 101/100$, $I = [1,3]$, utilities $-(p-3)^2/4$ and $-(p-1)^2/4$ in two periods and $p_1 = 1$, the left side of (4.6) at $T = 2$, $p = 5/3$ equals $7/6 > \eta M^2/2$; step (A.10) drops a factor 2. Corollary 8, which rests on it, Theorem 9, Lemma 3 and (3.15), which concern the pre-limit utility, are also excluded. Lemma 15 is false as printed and is not an item.

Contributions are welcome at every milestone; the binomial Stein identity, the implicit-function argument for monotone fixed points and the triangular-array law of large numbers for the slope are reusable.

Selected references

• S. Wager and K. Xu, Experimenting in Equilibrium, Management Science 67(11), 2021; arXiv:1903.02124v5. https://arxiv.org/abs/1903.02124 (version of record: https://doi.org/10.1287/mnsc.2020.3844)
• M. G. Hudgens and M. E. Halloran, Toward causal inference with interference, Journal of the American Statistical Association 103(482), 2008. https://doi.org/10.1198/016214508000000292
• T. Blake and D. Coey, Why marketplace experimentation is harder than it seems: the role of test-control interference, ACM EC 2014. https://doi.org/10.1145/2600057.2602837

Motivation

School districts, public housing authorities and refugee resettlement agencies allocate scarce items (school seats, apartments, slots) without prices. Most such systems are priority-based: each applicant receives a priority, possibly depending on observable characteristics such as neighborhood or sibling status, and a mechanism such as deferred acceptance (DA), serial dictatorship or top trading cycles turns priorities and reported preferences into an assignment. The planner's design question is which priorities and quotas to choose. Shi (SSRN 3425348; Management Science 2022, doi:10.1287/mnsc.2020.3925) reduces this question, in a large-market model, to a linear program over budget set probabilities: the probability that an applicant of each segment can choose from each menu of items. That reduction is only useful if the optimal menus can actually be produced by a familiar mechanism. Theorem 1 a) of the paper says that, under a mild regularity condition, DA can produce any feasible menu distribution, and DA with a single tie-breaker (DA-STB) can produce exactly the nested ones.

The continuum approach to DA follows Azevedo and Leshno (JPE 2016), who describe stable matchings in large markets by cutoff vectors, and Abdulkadiroğlu, Che and Yasuda (AEJ: Micro 2015) on expanding choice in school choice.

Setting

There are $n$ items $j \in [n]$ and an outside option $0$, with $J = [n] \cup \{0\}$. A market $M = (m, n, \lambda, c, F)$ has $m$ segments of agents with masses $\lambda_t > 0$, capacities $c_j$ for the real items (the outside option is unlimited), and for each segment $t$ a probability distribution $F_t$ of utility vectors $u \in \mathbb{R}^J$ with pairwise distinct components (strict preferences). The choice probability is

$$P_t(j,S) = \mathbb{1}(j \in S)\,\mathbb{P}_{u \sim F_t}\big(u_j = \max_{j' \in S} u_{j'}\big).$$

A budget set probability matrix $y = (y_{tS})_{t \in [m],\, S \subseteq J}$ lists the probability that a segment-$t$ agent faces menu $S$. The feasible set $Y^M$ consists of those $y$ with $y_{tS} \ge 0$, $\sum_S y_{tS} = 1$, $y_{tS} = 0$ when $0 \notin S$, and the capacity constraint $\sum_{t,S} \lambda_t P_t(j,S) y_{tS} \le c_j$ for every $j \in [n]$.

In DA, each agent of segment $t$ draws a priority vector $\pi \in \Pi = [0,B]^n$ from a law $G_t$, independently of his utilities. Given a cutoff vector $z$, his budget set is $B_\pi = \{j \in J : j = 0 \text{ or } \pi_j \ge z_j\}$ and he receives his favourite item in it. The demand is $D_j(z) = \sum_t \lambda_t \mathbb{P}(j \text{ is the favourite in } B_\pi)$. For quotas $q \le c$, the DA operator raises each $z_j$ just enough to bring $D_j$ down to $q_j$, and the DA cutoff $z^{DA(M,G,q)}$ is its least fixed point in $[0,B]^n$. A mechanism implements $y$ if $\mathbb{P}_{\pi \sim G_t}(B_\pi = S) = y_{tS}$ for all $t$ and $S$. In DA-STB, $\pi_{ij} = b_{tj} + \delta_i$ for a deterministic boost matrix $b$ and one tie-breaker $\delta_i \sim \mathrm{Uniform}(0,1)$ per agent.

The market is regular if $\{0\} \subseteq S \subsetneq S'$ implies $P_t(0,S) > P_t(0,S')$ for all $t$: adding items to a menu strictly lowers the chance that the outside option is chosen. A matrix $y$ is nested within segment if any two menus used with positive probability by the same segment are ordered by inclusion.

Formalization targets

Goal: Theorem 1 a), p. 13

If $M$ is regular, then

$$\forall y \in Y^M,\ y \text{ is DA-implementable}, \qquad \forall y \in Y^M,\ \big(y \text{ is DA-STB-implementable} \iff y \text{ is nested within segment}\big).$$

Milestones

The milestones are the steps of the paper's own proof, in attack order:

1. the demand $D_j$ is decreasing in $z_j$ and increasing in $z_k$, $k \neq j$ (App. A.2, p. 34);
2. the DA operator is a monotone self-map of $[0,B]^n$, so the DA cutoff exists (App. A.2, p. 34);
3. under the priorities $\pi_{ij} = \mathbb{1}(j \in S_i) + \delta_i$ of (H.1) and quotas equal to the left-hand side of the capacity constraint, $D_j(\mathbf 1) = q_j$ and $\mathbf 1$ is a fixed point, eq. (H.2);
4. at cutoff $\mathbf 1$ these priorities yield menu $S$ with probability $y_{tS}$, eq. (H.3);
5. the DA cutoff respects the quotas;
6. in a regular market, a cutoff $z' \le \mathbf 1$ that changes the menu probabilities leaves strictly less mass on the outside option, eq. (H.4);
7. Proposition H.1: DA with (H.1) implements $y$ (p. 47);
8. Proposition H.2 a): DA-STB menus are always nested within segment (p. 48);
9. Proposition H.3: DA-STB with boosts $b_{tj} = \sum_{S \ni j} y_{tS}$ implements every nested-within-segment $y$ (p. 48).

Significance

Theorem 1 a) is what makes the paper's optimization approach operational. Once a planner solves the linear program over $Y^M$, part i) guarantees a DA mechanism with explicit priorities and quotas that realizes the solution, so for regular markets nothing is lost by restricting attention to DA. Part ii) characterizes the DA-STB-implementable matrices, which is what lets the paper compare single tie-breaking with DA and identify when the simpler mechanism suffices. The remaining results of the paper (optimal assortments under multinomial and nested logit, the Boston school choice application) are built on this reduction.

The theorem is proved in the paper; nothing here is open. To the best of the drafting search, none of it is formalized: Prove2Me has finite two-sided matching and Gale–Shapley items, but no continuum matching market, no DA cutoff, and no budget set implementation result. Formalizing it provides a machine-checked large-market DA model (demand, cutoff operator, least fixed point) that other market design papers using the Azevedo–Leshno framework can reuse.

Difficulty

The obvious argument shows that the all-ones cutoff vector reproduces $y$ and is a fixed point of the DA operator. That does not finish the proof: the DA mechanism uses the least fixed point, and in general there are smaller ones. Example H.1 of the paper (p. 50) gives a non-regular market with a feasible, nested matrix $y$ that no DA mechanism implements under any priorities or quotas, so regularity cannot simply be dropped. The work is in showing that, under regularity, no fixed point strictly below $\mathbf 1$ can change the menu probabilities. This mixes order theory (Knaster–Tarski on a box), measure theory (product measures of utilities and priorities, continuity of the demand under an atomless tie-breaker) and a strict comparison of outside-option masses.

Formalization scope

Items are Option (Fin n), with none the outside option; priorities and cutoffs are Fin n → ℝ; menus are Finset (Option (Fin n)), and sums over menus run over the whole power set of $J$. The utility laws $F_t$ are probability measures on Option (Fin n) → ℝ, concentrated on injective vectors (strict preferences). Capacities are assumed nonnegative. Probabilities are real numbers obtained as toReal of finite measures. The demand is computed under the product measure $F_t \otimes G_t$, which encodes independence of priorities and preferences.

The DA operator merges the two branches of Algorithm 2 into a single infimum over $[z_j, B]$, with $B$ added to the set so the operator maps $[0,B]^n$ to itself, as the paper asserts. The DA cutoff is characterized as the least element of the fixed points in $[0,B]^n$. DA-implementability quantifies over a priority box $[0,B]^n$ with $B > 0$, probability laws $G_t$ supported in it, quotas $0 \le q \le c$, and the DA cutoff. DA-STB-implementability quantifies over boosts with $0 \le b_{tj} \le B - 1$, so priorities stay in the box.

Implementability is never stated as quantification over menus directly: that would be the random assortment mechanism, which implements every $y$ by definition and would make part i) trivial. The cutoff is never "some fixed point": the all-ones vector is a fixed point by construction, and only the least fixed point carries the content of the theorem.

Theorem 1 b) (TTC and serial dictatorship) is not part of this mission: the TTC cutoffs are imported from Leshno and Lo as a black box. Contributions are welcome on the measure-theoretic lemmas (continuity of the demand, the menu law under (H.1) and under single tie-breaking) and on the Knaster–Tarski step, which can use Mathlib's OrderHom.lfp on a complete lattice of boxes.

Selected references

• P. Shi, Optimal Priority-Based Allocation Mechanisms, SSRN manuscript 3425348 (2020); Management Science 68(1), 2022. https://ssrn.com/abstract=3425348, https://doi.org/10.1287/mnsc.2020.3925
• E. M. Azevedo and J. D. Leshno, A Supply and Demand Framework for Two-Sided Matching Markets, Journal of Political Economy 124(5), 2016. https://doi.org/10.1086/687476
• A. Abdulkadiroğlu, Y.-K. Che and Y. Yasuda, Expanding "Choice" in School Choice, American Economic Journal: Microeconomics 7(1), 2015. https://doi.org/10.1257/mic.20120027
• J. D. Leshno and I. Lo, The Cutoff Structure of Top Trading Cycles in School Choice, Review of Economic Studies 88(4), 2021. https://doi.org/10.1093/restud/rdaa071

Motivation

Machine-learned models of molecular energies and properties are trained on the output of quantum-chemistry calculations, and a common way to make them data-efficient is to build the physical symmetries of the problem into the architecture. When the input is not a point cloud but a set of matrices expressed in an atomic-orbital basis (Fock, density, overlap and Hamiltonian matrices from a cheap mean-field calculation), the relevant symmetry is the freedom to rotate the orbital basis of each atom independently: a rotation of the molecule, or any other unitary change of the local frames, changes every matrix element but not the physics.

Qiao, Christensen, Welborn, Manby, Anandkumar and Miller (arXiv:2105.14655v4, published in PNAS 2022) introduce UNiTE (Unitary N-body Tensor Equivariant network), the architecture behind OrbNet-Equi. They state as eq. (4), p. 3, that the network must satisfy $R\cdot F(T[\Psi_0])\equiv F(R\cdot T[\Psi_0])$ for every isometric basis rotation $R$, and prove this property in Appendix S2.6 (pp. 26–28) for a generalized version of the network: tensors of any order $N$, complex scalars, and an arbitrary unitary change of basis on each atom. The empirical results of the paper (QM9, MD17, GMTKN55) rest on this design principle, but the mathematical content of the paper is the equivariance proof.

Setting

There are $d$ atoms $u$. Atom $u$ carries a finite basis $\{e_{u;v}\}_{v\in\iota_u}$, and the concatenated basis is the set of pairs $(u,v)$. An N-body tensor of order $N=n+1$ is a function $T$ of $N$ concatenated indices; its sub-tensor $T_{\vec u}$ at $\vec u=(u_1,\dots,u_N)$ collects the entries whose $j$-th index lies in atom $u_j$.

A group $K$ (the paper's $\mathrm U(n)$; $\mathrm O(3)$ in the experiments) acts through unitary representations $\pi^1_u:K\to\mathrm U(\iota_u)$, and each atom has a subgroup $G_u\le K$. An element $g=(g_u)_u$ with $g_u\in G_u$ acts on tensors by the local action (S26):

$$g\cdot T_{\vec u}=(\pi^1(g_{u_1})\otimes\pi^1(g_{u_2})\otimes\cdots\otimes\pi^1(g_{u_N}))\,T_{\vec u}.$$

The network's hidden features $h_u$ assign to each label $L$ of a unitary representation $U^L:K\to\mathrm U(\mathbb V^L)$ and each channel $c$ a vector $h_{u,L,c}\in\mathbb V^L$; $g$ acts by $h_{u,L,c}\mapsto U^L_{g_u}h_{u,L,c}$. Matching matrices $(D_u)^{L,k,M}_v=\langle e_{u;v},\pi_{u;L,k,M}\rangle$ relate the atomic basis to a basis adapted to the decomposition $V_u\simeq\bigoplus_L(\mathbb V^L)^{\oplus K_L}$.

The UNiTE network $F$ (Methods 1.1; Appendix S2.5) consists of:

• a diagonal reduction $\psi_u$ turning the diagonal block $T_u$ into the initial features $h^0_u$;
• $t_1$ full steps, each made of a block convolution (S36), message passing (S37) with scalar attention weights $\alpha$, a reverse matching layer (S45) and a point-wise interaction $\phi$ (S40)–(S42) built from EvNorm (S39) and Clebsch–Gordan-type coefficients $C$;
• then $t_2$ point-wise interaction steps.

Formalization targets

Goal: G-equivariance of UNiTE (S2.6, p. 26)

Under the hypotheses the paper's proof uses — compatibility (S35) of the matching matrices, the Clebsch–Gordan property (S33) of $C$, equivariance (S32) of the diagonal reduction, invariance $g\cdot\alpha=\alpha$ of the attention weights, and positivity of the EvNorm constants — for every $g\in\prod_u G_u$, tensor $T$ and atom $u$,

$$F(g\cdot T)_u=U(g_u)\cdot F(T)_u .$$

Milestones

The proof in S2.6 rests on three results of S2.4 and four labelled sub-proofs:

• Theorem S1 (p. 24): a tensor product of irreducible unitary representations decomposes into irreducibles, with $\sum_L\mu(L)\dim\mathbb V^L=\prod_j\dim\mathbb V^{L_j}$ (S29)–(S30);
• Corollary S2 (p. 24): an invertible equivariant linear map $\psi:V_u^{\otimes N}\to\bigoplus_L(\mathbb V^L)^{\oplus\mu(L;V_u)}$;
• Corollary S3 (p. 24): an injective equivariant reduction $\psi(T)_{\nu,L,M}=\sum_{\vec v}T(\vec v)Q^{\vec v}_{\nu,L,M}$ with $\sum_Ln_L\le\dim(V_u)^N$;
• the four building-block equivariances of S2.6, for the block convolution, message passing, EvNorm and the point-wise interaction.

Significance

The theorem is what justifies feeding UNiTE features in arbitrary local frames: the predicted invariant quantities (energies) do not depend on the choice of atomic-orbital phases or orientations. The vector-valued outputs, such as dipole moments, then transform correctly. Without it, the model would have to learn the symmetry from data or from augmentation. The same argument applies to other architectures acting on matrices in local bases, for example models of Hamiltonian or density matrices.

The result is proved in the paper, with a proof written at the level of index manipulations. To our knowledge it has no machine-checked proof. Formalizing it pins down exactly which hypotheses each layer needs: (S35) on the matching matrices, the complex conjugate in (S36), the intertwining form of (S33), and invariance of the attention weights. It also yields a reusable library of statements about tensor-product and block-diagonal actions of unitary representations. Theorem S1 for an arbitrary group with a complete catalogue of irreducibles is a statement of independent interest: finite-dimensional unitary representations are completely reducible, which Mathlib does not yet provide outside finite groups.

Difficulty

No single step is deep; the difficulty is bookkeeping across dependent index types. The local action is block-diagonal over atoms, so cross-atom terms must be shown to vanish. Sub-tensor indices are dependent on the atom sequence $\vec u$. The block convolution's cancellation $\sum_v\pi^1_{vv'}\overline{\pi^1_{vv''}}=\delta_{v'v''}$ uses unitarity and the conjugate. The reverse matching layer needs the adjoint form of (S35), which uses that $G_u$ is a subgroup (closed under inverses). The point-wise block reindexes a double sum through a Kronecker product. The full network is a two-phase recursion whose attention weights depend on the current features, so the induction must carry the equivariance of every intermediate feature. Theorem S1 needs complete reducibility of a finite-dimensional unitary representation of an arbitrary group, together with the identification of each irreducible summand with a catalogue member.

A tempting shortcut, assuming each layer equivariant and composing, proves nothing about UNiTE: the content is that these specific layers are equivariant under these specific hypotheses.

Formalization scope

All scalars are complex; the paper's real (orthogonal) case is the special case of real unitary matrices. $\mathrm U(n)$ is replaced by an abstract group $K$ ([Group K]), representations are homomorphisms K →* Matrix.unitaryGroup ι ℂ, and the catalogue of irreducibles of $\mathrm U(n)$ is a family $U^L$ with the hypothesis CatalogComplete (every irreducible unitary representation is equivalent to some $U^L$), the formal reading of the paper's "we have abstracted the labelling details … into the index L". The subgroups $G_u$ are S u : Subgroup K, and every hypothesis is assumed only for $k\in G_u$.

Committed conventions:

• the tensor has order $N=n+1$ over the concatenated basis Σ u, ι u;
• every label has the same number $n_{\max}$ of channels, as (S41) requires;
• the matching weights use the main-text shapes (16) and (28), with a multiplicity index for the copies of $\mathbb V^L$ in $V_u$; they may depend on atom and step;
• the multilayer perceptrons are arbitrary functions of the invariant features, and the EvNorm statistics $\mu,\sigma$ are fixed parameters;
• (S33) is assumed in intertwining form $C(U^{L_1}\otimes U^{L_2})=U^LC$, which follows from the printed form for co-isometric $C$;
• the diagonal reduction $\psi_u$ is any linear map satisfying (S32), and the attention weights are any functions of the step's inputs satisfying $g\cdot\alpha=\alpha$; the paper's concrete attention (18)–(21) is not instantiated;
• only part (a) of the group $G$ of S2.2 (local unitaries) is formalized; permutations (b) and translations (c) leave the symmetric, translation-invariant input unchanged and are trivial.

Trivializing formalizations are ruled out. The layers are defined concretely, not replaced by maps assumed equivariant. The action is local, one unitary per atom, not one global unitary. The complex conjugate in (S36) is kept. Irreducibility of the catalogue and its completeness are both stated in Theorem S1 and the corollaries.

The development needs one definitions module (OrbNetEqui.Equivariance.Basic) and Mathlib's matrices, unitary groups, block-diagonal and Kronecker matrices. Contributions are welcome on every milestone; the building-block lemmas (block-diagonal and Kronecker actions of unitary matrices, unitary invariance of the regularized norm) and complete reducibility of finite-dimensional unitary representations are reusable beyond this mission.

Selected references

• Z. Qiao, A. S. Christensen, M. Welborn, F. R. Manby, A. Anandkumar, T. F. Miller III, Informing Geometric Deep Learning with Electronic Interactions to Accelerate Quantum Chemistry, Proc. Natl. Acad. Sci. USA 119 (2022); preprint arXiv:2105.14655v4. https://arxiv.org/abs/2105.14655
• Z. Qiao, M. Welborn, A. Anandkumar, F. R. Manby, T. F. Miller III, OrbNet: Deep learning for quantum chemistry using symmetry-adapted atomic-orbital features, J. Chem. Phys. 153, 124111 (2020). https://doi.org/10.1063/5.0021955
• N. Thomas et al., Tensor field networks: Rotation- and translation-equivariant neural networks for 3D point clouds, arXiv:1802.08219 (2018). https://arxiv.org/abs/1802.08219

Motivation

Forecast aggregation asks how to combine several experts' probability forecasts for the same event into one forecast. The two classical answers are linear pooling (average the probability vectors) and logarithmic pooling (average the log-probabilities and renormalize). Neither is justified by the way forecasts are usually evaluated: with a proper scoring rule, a payment rule under which reporting one's true belief maximizes expected reward. Neyman and Roughgarden (arXiv:2102.07081, Operations Research 2023) tie the aggregation method to the scoring rule. For each proper scoring rule $s$ they define quasi-arithmetic (QA) pooling with respect to $s$, which recovers linear pooling for the quadratic (Brier) score and logarithmic pooling for the log score, and they justify it in several ways. This mission formalizes the first justification, the paper's Theorem 4.1: QA pooling is the unique max-min optimal way for an agent paid by $s$ to aggregate the forecasts of experts it has sub-contracted.

The result places the paper in a line of work on scoring rules and convex analysis: the Savage representation of proper scoring rules as tangent planes of a convex function (Gneiting and Raftery, JASA 2007, Theorem 2), the link between entropy maximization and worst-case expected loss (Grünwald and Dawid, Annals of Statistics 2004), and the result of Chun and Shachter (UAI 2011) that, for $n=2$ outcomes, experts rewarded with the same scoring rule cannot be prevented from colluding profitably, by all reporting what Neyman and Roughgarden call the QA pool of their reports.

Setting

There are $n$ outcomes. A forecast is a point of the standard simplex $\Delta^n=\{p\in\mathbb R^n: p_j\ge 0,\ \sum_j p_j=1\}$, and $\delta_j$ is the vertex with a $1$ in coordinate $j$. A scoring rule is a function $s:\Delta^n\times[n]\to\mathbb R\cup\{-\infty\}$: an expert who reports $p$ receives $s(p;j)$ if outcome $j$ happens. The rule is proper if for every belief $p\in\Delta^n$ and every report $x\in\Delta^n$,

$$\sum_j p_j\,s(p;j)\ \ge\ \sum_j p_j\,s(x;j),$$

with equality only when $x=p$. It is regular if $s(p;j)$ is real except possibly $s(p;j)=-\infty$ when $p_j=0$. The forecast domain $\mathcal D$ is the set of $p$ at which every $s(p;j)$ is real, and the expected reward function is $G(p)=\sum_j p_j s(p;j)$. The paper assumes throughout that each $s(\cdot\,;j)$ and $G$ are continuous on $\Delta^n$.

An exposure function $g$ of $s$ satisfies the Savage representation

$$s(p;j)=G(p)+\langle g(p),\delta_j-p\rangle\qquad(p\in\mathcal D),$$

so $g(p)$ is a subgradient of $G$ at $p$. The Bregman divergence is $D_G(p\,\|\,q)=G(p)-G(q)-\langle g(q),p-q\rangle$.

Given forecasts $p_1,\dots,p_m\in\mathcal D$ and non-negative weights $w_1,\dots,w_m$ adding to $1$, the QA pool $p^*=\bigoplus_{\mathbf g}^{i=1..m}(p_i,w_i)$ is the unique $p^*\in\Delta^n$ at which $\sum_i w_i g(p_i)$ is a subgradient of $G$. An agent paid by $s$ who pays expert $i$ the amount $w_i s(p_i;j)$ and reports $q$ earns the profit

$$u(q;j)=s(q;j)-\sum_{i=1}^m w_i\,s(p_i;j).$$

Formalization targets

Goal: Theorem 4.1

For a regular, proper, continuous scoring rule $s$ with exposure function $g$, forecasts $p_i\in\mathcal D$ and weights $w_i\ge 0$ adding to $1$:

$$\min_j u(q;j)\ <\ \min_j u(p^*;j)\quad\text{for every } q\in\Delta^n,\ q\neq p^*;$$

the minimum $\min_j u(p^*;j)$ is attained at every $j$ with $p^*_j>0$; it is non-negative; and it is positive unless all reports with positive weight are equal. All four clauses are part of the goal.

Milestones

In the order the paper's proof uses them:

1. Proposition 3.1 (only-if direction, on $\mathcal D$): $G$ is convex on $\Delta^n$, $s(p;\cdot)$ is an exposure function, and every exposure function gives subgradients of $G$ on $\mathcal D$.
2. Proposition 3.4, first bullet: $D_G(x\,\|\,q)\ge 0$, with equality only when $x=q$, for $q\in\mathcal D$.
3. Well-definedness of the QA pool (§3.2): exactly one $p^*$ exists.
4. Claim 3.10: $p^*\in\mathcal D$.
5. KKT display in the proof of Theorem 4.1: $g(p^*)=\sum_i w_i g(p_i)+\lambda\mathbf 1_n+\mu$ with $\mu\ge 0$ and $\mu_j=0$ where $p^*_j>0$.
6. Profit identity: $u(p^*;j)=\sum_i w_i D_G(p^*\,\|\,p_i)+\mu_j$.

Significance

Theorem 4.1 says that an agent who sub-contracts experts and is paid by the same proper scoring rule can guarantee itself the largest worst-case profit, uniformly over outcomes, by reporting the QA pool, and that no other report achieves this guarantee. It gives an operational reason to aggregate with the method the scoring rule induces rather than a fixed one, and the strict positivity of the guarantee unless the weighted experts agree recovers, as a special case, the two-outcome collusion result of Chun and Shachter. The same objects (QA pools, exposure functions, Bregman divergences of expected rewards) carry the paper's later results on learning expert weights online and on axiomatizing QA pooling.

The theorem is proved in the paper; none of it is machine-checked. The mission produces a Lean statement and proof of Theorem 4.1 in full generality, including boundary pools where some outcome has probability zero, together with reusable statements about proper scoring rules on the simplex that are not in Mathlib: the Savage representation, non-negativity of the expected-reward Bregman divergence, existence and uniqueness of QA pools, and first-order optimality conditions on the simplex.

Difficulty

When $p^*$ lies in the interior of $\Delta^n$ and $G$ is differentiable, first-order optimality gives $g(p^*)=\sum_i w_i g(p_i)+\lambda\mathbf 1_n$ directly, and the rest is algebra. The difficulty is the boundary. The QA pool can have $p^*_j=0$ for some $j$; $G$ need not be differentiable there; and for rules such as the logarithmic score $s(p;j)=-\infty$ at points with $p_j=0$, so $G$'s subgradients may blow up near the boundary of $\Delta^n$. Showing that the pool avoids the points where $s$ is $-\infty$ (Claim 3.10) and that the multipliers $\lambda,\mu$ exist with the right sign there requires the continuity of $s$ into the extended reals, not just convexity of $G$. Uniqueness of the maximizer also needs the strictness built into properness.

Formalization scope

Forecasts are functions Fin n → ℝ, and $\Delta^n$ is Mathlib's stdSimplex ℝ (Fin n). The scoring rule takes values in EReal; only its values on $\Delta^n$ matter, the expected score uses $0\cdot(-\infty)=0$, and inner products are finite sums. Properness is strict, belief first and report second. $G$ is the real part of the expected score and is only evaluated on $\Delta^n$. Subgradients are taken relative to $\Delta^n$, the domain of $G$. The exposure function is real-valued and constrained by the Savage representation on $\mathcal D$ only; on $\mathcal D$ it is determined up to a multiple of $\mathbf 1_n$, and no statement depends on that choice. The Bregman divergence uses the exposure function in place of a gradient, since $G$ need not be differentiable at boundary forecasts. Continuity of $s(\cdot\,;j)$ is in the order topology of the extended reals. The QA pool is a predicate (a point of $\Delta^n$ with the subgradient property), and its existence and uniqueness is a separate milestone. The profit is $-\infty$ when the agent's report scores $-\infty$, and $\min_j$ is an infimum over the outcomes.

A trivial formalization is ruled out: the QA-pool hypothesis of the goal is satisfiable (milestone 3), exposure functions exist (milestone 1), and the continuity assumptions of the paper are kept as hypotheses rather than dropped.

Not formalized: the paper's results on learning expert weights (Theorems 5.1, 5.3), its axiomatizations (Theorems 6.6, C.7), which rules have convex exposure (Appendix D), the "if" direction of Proposition 3.1, and the second bullet of Proposition 3.4. Contributions of general lemmas on convex functions on the simplex (one-sided directional derivatives, first-order conditions at boundary minimizers) are welcome alongside the milestones.

Selected references

• E. Neyman and T. Roughgarden, From Proper Scoring Rules to Max-Min Optimal Forecast Aggregation, Operations Research, 2023; arXiv:2102.07081v2. https://arxiv.org/abs/2102.07081
• T. Gneiting and A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 2007. https://doi.org/10.1198/016214506000001437
• P. D. Grünwald and A. P. Dawid, Game Theory, Maximum Entropy, Minimum Discrepancy and Robust Bayesian Decision Theory, Annals of Statistics 32(4), 2004. https://doi.org/10.1214/009053604000000553
• S. Chun and R. D. Shachter, Strictly Proper Mechanisms with Cooperating Players, UAI 2011, pp. 125–134. https://dslpitt.org/uai/displayArticleDetails.jsp?mmnu=1&smnu=2&article_id=2168&proceeding_id=27
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, §5.5.3. https://doi.org/10.1017/CBO9780511804441