All missions

This problem asks for a formal proof of the complete conditional geometric K24 change-of-slice result, including its regularity obstruction. The source gives informal analytic arguments; this publication does not claim a new proof or a new unsolved conjecture for the standard perturbation lemma. It does not assert existence of the still-missing geometric organizer in the four-dimensional Einstein research program.

Let $M$ be a closed smooth real four-manifold with an actual common smooth circle action. Write $\Pi_0$ for its normalized Haar average on the relevant tensor, covector, or vector bundle and $\Pi_\perp=I-\Pi_0$. Let the positive metrics $\widehat g$ and $z$ be invariant under that same action; the actual nearby positive metric $g$ need not be invariant. The scalar $\lambda$ is arbitrary. Define

$$E(q)=\operatorname{Ric}_q-\lambda q,\qquad \Psi_{\widehat g}(q)=E(q)+\delta_q^*\Pi_\perp\beta_{\widehat g}(q-\widehat g),$$

where $\beta_h u=-\operatorname{div}_h u+\tfrac12d\operatorname{tr}_h u$, $\delta_h^*$ is the symmetrized covariant derivative with factor $1/2$, and $\mathcal K_hY=\mathcal L_Yh$. These are actual geometric differential operators, not freely supplied linear maps.

Fix the numerical data for a uniformly bounded local finite-cover system, metric ellipticity and coefficient bounds, $0<\alpha<1$, and a uniform pullback bound $H\ge1$ for the common action. These bounds are fixed before the conclusion constants are chosen. Covering degree is not globally bounded, and the downstairs overlap count is kept separate from the internal coordinate atlas on each covering manifold. The proposition requires all of the following.

1. Exact tensor identities and genuine differentiation. Prove the full product rule

$$D\Psi_{\widehat g}(z)u=DE(z)u+(D\delta^*)_z[u]\,\Pi_\perp\beta_{\widehat g}(z-\widehat g)+\delta_z^*\Pi_\perp\beta_{\widehat g}u.$$

Invariance makes the middle term vanish. On the genuine zero-Haar-mean tensor sector, identify the difference of the fixed-reference and re-anchored derivatives as

$$R_{\widehat g,z}u=\delta_z^*(\beta_{\widehat g}-\beta_z)u.$$

The target also includes the actual connection/Bianchi coefficient expansions, principal-symbol identification by a quadratic-jet test and its intrinsic norm bound, sector preservation and equivariance. It requires the displayed variation to be the Fréchet derivative in the specified section norms on a positive-radius metric neighborhood, not just a pointwise or directional derivative.

2. Uniform tensor estimates in both scales. For one uniform $C_T$,

$$\|R_{\widehat g,z}u\|_{C^{0,\alpha}_{\rm cov}} \le C_T\|\widehat g-z\|_{C^{2,\alpha}_{\rm cov}}\|u\|_{C^{2,\alpha}_{\rm cov}}.$$

For every real $s>4$, with the corresponding fixed local Sobolev coefficient/atlas bounds, require a uniform $C_S$ with

$$\|R_{\widehat g,z}u\|_{H^{s-2}_{\rm cov}} \le C_S\|\widehat g-z\|_{H^s_{\rm cov}}\|u\|_{H^s_{\rm cov}}.$$

The Sobolev clause is not restricted to integer order and does not impose higher Hölder regularity on the metric. It uses local real-order metric and inverse-metric bounds; it does not impose a fixed global bound on the degree-dependent norm of the whole metric.

3. Both vector errors and the correct regularity. For the actual projected operator $B_{\widehat g,g}Y=\Pi_\perp\beta_{\widehat g}\mathcal L_Yg$, retain both terms:

$$B_{\widehat g,g}-B_{z,z}=\Pi_\perp\big[(\beta_{\widehat g}-\beta_z)\mathcal K_z+ \beta_{\widehat g}\mathcal L_{(\cdot)}(g-z)\big].$$

Prove the natural $C^{2,\alpha}\to C^{0,\alpha}$ estimate by a uniform constant times $(\|\widehat g-z\|_{C^{2,\alpha}}+\|g-z\|_{C^{2,\alpha}})\|Y\|_{C^{2,\alpha}}$. For the shifted $C^{3,\alpha}\to C^{1,\alpha}$ pair, both metric differences must instead be controlled in $C^{3,\alpha}$. The actual Bianchi–Killing/rough-Laplacian identity is also included.

4. Geometric inverse transfer. In each stated pair of actual zero-mean section spaces, suppose the re-anchored projected operator is a bounded linear isomorphism with inverse bound $C_A$ (or $C_B$). If that bound times the norm of the actual difference operator is strictly below $1/2$, prove that the fixed-reference operator is an isomorphism with inverse bound at most $2C_A$ (respectively $2C_B$), including surjectivity and the corresponding Banach-dual gap. Mere absence of kernel is not substituted for the initial isomorphism. Norm, completeness, Haar integrability/boundedness and projection facts needed for this argument are requested conclusions about the concrete spaces; they are not assumed copies of the desired theorem.

5. Actual flat-torus sharpness. On the genuine four-torus with coordinates of period $2\pi$, use the flat metric, the circle translation in $x_2$, $V=\sin(x_2)\partial_{x_1}$ and

$$f_n=n^{-(3+\alpha)}\sin(nx_1)(dx_1\otimes dx_2+dx_2\otimes dx_1).$$

Require positivity of $g_n=g_0+f_n$ for $n\ge2$, finite norms, $\|f_n\|_{C^{2,\alpha}}\to0$, bounded $C^{3,\alpha}$ norms, and a lower bound $\pi^{-\alpha}$ for the $C^{1,\alpha}$ norm of the projected actual vector-operator difference tested on $V$. Consequently no uniform shifted estimate using only the $C^{2,\alpha}$ metric difference can hold. This is a statement about genuine torus tensors and operators, not an abstract sequence of scalar exponents.

Norm and formalization choices. The definition packages specify full big Hölder norms from actual iterated derivatives and top-order Hölder seminorms, hierarchical local finite covers, and real-order Bessel–Sobolev norms with explicit partitions. Sobolev carriers use the continuous/C² representatives justified by the requested ranges; their completeness and norm properties remain to be proved. The adapted Sobolev norm is an explicit upstairs sum and is not identified with downstairs $L^2$ independently of covering degree. Haar averaging is pointwise in finite-dimensional fibers, avoiding an unsupported assumption of norm-continuous action on big Hölder space. The projection bounds are $H$ and $1+H$; $1$ and $2$ apply only in the isometric case. Raw inverse, derivative and integral definitions are totalized in Lean, while positivity, regularity, integrability and the analytic properties are enforced by the full statement's hypotheses or required conclusions. Definitions have no admissions or new axioms. There is exactly one intentional unproved theorem placeholder.

Remaining application boundary. K24 does not construct the common marked action, the required same-window $C^2$/$C^3$ closeness, or the adapted re-anchored inverse from an arbitrary Einstein degeneration. Those organizer inputs remain open. The nonlinear diffeomorphism-chart and quadratic-remainder applications in K16/K21 are separate supporting questions; they require their own loss-aware regularity hypotheses/proofs. Neither those applications nor the original Einstein conjecture is claimed proved by this publication.

Motivation

The 3SUM problem — does an integer array contain three values, at three distinct positions, that sum to zero — is a canonical benchmark of fine-grained complexity. Hundreds of reductions sit beneath it in the 3SUM-hardness lattice, so its worst-case exponent governs the reported complexity of convex-hull degeneracies, motion planning, and many computational-geometry tasks. On the real-RAM side the best known bounds are barely subquadratic; on the integer side, Alman and Vassilevska Williams opened a line of subquadratic deterministic word-RAM exponents built on truly subquadratic triangle detection in lopsided graphs.

A recent development is that the entire algorithmic pipeline — data structure, compiled word-RAM program, and runtime certificate — has been written down in Lean 4 and machine-checked, turning a numerical-exponent claim into a verified theorem. Along the way a refinement ladder formed, each step exported as a theorem EndStatement.ThreeSum.SolvedInTime r against the same benchmark specification:

• 2026-10: full deterministic formalization at $1.962$ (c0ldzy17/three-sum-lean), refining earlier $1.999x$ entries already formalized on this platform;
• 2026-10: platform-side $1.960614$ (the ThreeSum1960614 tree here);
• 2026-10: margin refinement to $1.921$ and then $1.9203$ (fringewidth/three-sum-lean);
• 2026-10: tightened logarithm and entropy intervals to $4800699/2500000 = 1.9202796$ (JoshuaQFEX/3sum-bound), the source of this mission.

Setting

The benchmark model is the source word RAM of the Alman–Vassilevska Williams formalization (EndStatement, already on the platform in TrulySubcubicAPSP_SourceSpecification): a deterministic machine over signed words of width $W$ with arithmetic, memory, and conditional-jump instructions. One says SolvedInTime r when for every magnitude exponent $\kappa$ there is a single finite program $P$, a width bound $b$, and a time function $T$ with $T(n)^{r.\mathrm{den}} \le K\, n^{r.\mathrm{num}}$ for some $K$ — the rational-power encoding of $O(n^r)$ — such that $P$, run at every width $W \ge b(\lfloor\log_2 n\rfloor + 1)$, decides 3SUM on every instance of $n$ integers of absolute value at most $n^\kappa$ within $T(n)$ steps. Instances are functions Fin n → Int; yes requires the three summands at three distinct indices.

Formalization targets

Goal

$$\texttt{EndStatement.ThreeSum.SolvedInTime}\;((4800699 : \mathbb Q)/2500000)$$

i.e. deterministic 3SUM in $O(n^{1.9202796})$ word-RAM steps. The constant is hard-coded: this mission certifies this exact exponent, the sharpest point of the current chain.

Chain of margins (milestones)

The proof is the ternary-radix refinement of the $1.962$ construction: the same color-coding data structure reorganized around base-3 digits, banks, and queries, compiled to an explicit machine program, with the runtime charged combinatorially stage by stage. The milestone list follows the costing chain of the source: radix-3 machinery and the ternary data structure, the principal-cost certificate ($< 1.92027946$, the bank term $156432807976/81463563795$), the finite-block certificate ($1.92027957$), the frontend budget ($1.92027958$), the executed colored solver ($1.92027959$), and the exported benchmark target ($1.92027960$).

Significance

The result is, at the time of writing, the best formalized deterministic 3SUM exponent available anywhere: previous formalized entries on this platform bottom out at $1.960614$. Once proved end to end here it becomes the platform's record value for this benchmark, and every lemma of the ternary layer becomes reusable platform infrastructure — falsifiable, importable, and improvable by others, since a cheaper stage immediately yields a better SolvedInTime value by the same costing bridge.

Formalizing it also stress-tests something beyond the number: an end-to-end compiled program execution with a certified asymptotic runtime, not just an abstract algorithm. The runtime margins are certified against strict gaps ($10^{-7}$ at the largest scale), so the verification is quantitative, not just qualitative.

Difficulty

The difficulty is not one deep lemma but a long, load-bearing chain: thousands of small Meets-specifications about program fragments, the radix-3 generalization of the binary machinery, entropy and logarithm interval arithmetic for the exponent, and the assembly of a single compiled program whose correctness and runtime must both hold simultaneously. A tempting shortcut is to postulate the data-structure spec and prove only the runtime analysis — but the benchmark statement is about one concrete word-RAM program, so nothing may be assumed about the implementation: the compiler, the machine semantics, and the runtime ledger are all part of the statement's content.

Formalization scope

This mission is a transplant of an existing, checked Lean 4 development (Apache-2.0) pinned to this platform's default environment (Lean 4.33.1, Mathlib 0df444a…). Statements keep the source's model and names; the benchmark Problem/SolvedInTime layer is reused from the platform's existing TrulySubcubicAPSP_SourceSpecification and the preceding 3SUM trees, and only the new ternary layer is added. No sorry, no assumed oracle, no weakening of SolvedInTime to a per-instance or per-width reading is admissible.

Selected references

• J. Alman and V. Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs. Source paper of the benchmark and the original exponent.
• c0ldzy17, three-sum-lean: full Lean formalization of deterministic $O(n^{1.962})$ integer 3SUM. https://github.com/c0ldzy17/three-sum-lean
• fringewidth (H. S. Bojnal), three-sum-lean: exponent-margin refinement to $1.9203$. https://github.com/proof-factory/three-sum-lean
• J. Wharton (QFEX), A sharper exponent for deterministic integer 3SUM, note and Lean sources. https://github.com/JoshuaQFEX/3sum-bound

Motivation

Conglomerates and stand-alone firms finance projects differently. A multi-divisional firm runs an internal capital market: headquarters raises funds externally and then decides which division gets them. A stand-alone firm must raise capital project by project. A long line of work in corporate finance asks when the internal market is more efficient: Stein (1997) argues that headquarters can "pick winners", while managers with empire-building motives may over-invest.

Hwang (Management Science, 2025) adds voluntary disclosure to this comparison. Managers may disclose a project's profitability to investors at a cost, and investors set their financing terms from what is disclosed and what is withheld. Withholding information becomes a strategic choice, and the organizational form changes what a manager gains by disclosing. The paper's main result says exactly when a founder should prefer a single multi-divisional firm to two stand-alone firms.

Setting

A founder owns two projects $i \in \{1,2\}$. Each needs one unit of capital and pays $\theta_i X$, where $X > 1$ and $\theta_i \in \{0,1\}$. The types are independent, with $\Pr(\theta_i = 1) = p \in (0,1)$.

• Disclosure. A manager who knows $\theta_i$ chooses $d_i \in \{D, ND\}$. Disclosure is truthful and raises the capital required for project $i$ by $c > 0$. Write $\#D$ for the number of disclosures.
• Investors are competitive. After observing the disclosures they hold a belief about the undisclosed types: a probability vector on type profiles that agrees with every disclosed value, given by Bayes' rule whenever the message is sent in equilibrium. They fund $k$ projects in exchange for a share $\alpha \in [0,1]$ of cash flows that lets them break even. In the multi-divisional firm ($o = m$) one manager sees $(\theta_1,\theta_2)$. Investors choose $k = 2$ if some $\alpha \in [0,1]$ solves

$$(E[\theta_1] + E[\theta_2])\,\alpha X = 2 + c\,\#D,$$

otherwise $k = 1$ if some $\alpha$ solves $E[\theta_\lambda]\,\alpha X = 1 + c\,\#D$, otherwise $k = 0$. With one unit the manager implements the better project ($\lambda = 1$ iff $\theta_1 \ge \theta_2$). This choice is the internal capital allocation.

• Payoffs. The manager receives $q(1-\alpha)X$ from each profitable implemented project, with $q \in (0,1)$, plus an empire-building benefit $\beta$ per implemented project, where $\beta > qX$.
• Stand-alone firms ($o = s$). Each firm has its own manager, who sees only $\theta_i$. Investors fund firm $i$ iff some $\alpha_i \in [0,1]$ solves $E[\theta_i]\,\alpha_i X = 1 + c\,I(d_i)$.

An equilibrium is a pure-strategy perfect Bayesian equilibrium. The disclosure strategy is a best response for every type. Investors act on admissible, Bayes-consistent beliefs. Ties are broken toward silence: a disclosure is made only if withholding it would strictly lower the manager's payoff. A structure's investment efficiency is the expected net cash flow of the implemented projects. Following the paper, each structure is evaluated at its equilibrium with the highest efficiency. These values are $V_m$ and $V_s$. The founder chooses the structure with the larger value.

Formalization targets

Goal: Proposition 3, the founder's choice (corrected on one line)

Assume $X \ge 1 + c$. Then $V_m$ and $V_s$ exist and:

$$\tfrac{1-p}{2p} < c < \tfrac{1-p^2}{2p^2},\ X < \min\{2+c, \tfrac{1+p}{p}\} \ \Longrightarrow\ V_s < V_m,$$ $$c < \tfrac{1-p}{p},\ X \ge 2 + c \ \Longrightarrow\ V_m < V_s,$$

and $V_m = V_s$ everywhere else. The first region with $c = \frac{1-p}{2p}$ included gives $V_s \le V_m$. On that line the two values are equal, although the printed statement claims a strict preference there.

Milestones

1. Appendix B.1: no equilibrium of the multi-divisional firm discloses an unprofitable project.
2. Proposition 1: the stand-alone equilibria and their efficiencies $p(X-1-c)$ and $pX-1$.
3. Proposition 2 (ii), (iii): disclosure of exactly the profitable projects, with efficiencies $2p(X-1-c)$ and $2p(X+p-2-c)$.
4. Proposition 2 (i): the internal-capital-allocation equilibrium, with efficiency $p(2X - p(1+2c)) - 1$.
5. Proposition 2 (iv): no disclosure and full funding, with efficiency $2(pX-1)$.

Significance

The result. Proposition 3 splits the parameter space into three regions:

• Where disclosure costs are intermediate and cash flows low, the internal capital market strictly wins. The multi-divisional manager raises one unit without disclosing and directs it to a profitable project, which saves the disclosure cost a stand-alone firm must pay to be funded.
• Where disclosure is cheap and cash flows high, stand-alone firms strictly win. Disclosing one profitable project lets the empire-building manager fund an unprofitable one as well.
• Elsewhere the two structures are equally efficient.

The comparison is the paper's answer to when internal capital markets create value under voluntary disclosure. Its extensions (§6) are measured against this baseline.

Formalizing it. The result is proved in the paper by hand. It has no machine-checked proof. The proof's selection argument, "the equilibrium with the highest efficiency", ranges over every equilibrium with arbitrary off-path beliefs, and it is easy to get wrong at the boundaries. A check of the printed statements against an exact enumeration of equilibria found that the strict preference in part (i) fails on $c = \frac{1-p}{2p}$. The uniqueness claims of Propositions 1 (ii), 2 (i) and 2 (iv) also fail on tie lines. A formal proof settles the corrected statement. The model, a finite signaling game with verifiable costly disclosure and break-even investors, can be reused for other disclosure models.

Difficulty

The selected values are maxima over all pure-strategy equilibria. The off-path beliefs are any admissible beliefs. An upper bound on $V_m$ therefore needs a classification of every equilibrium:

• first rule out the disclosure of unprofitable projects, which depends on the tie-breaking rule, since a manager with two unprofitable projects is indifferent among many messages;
• then determine the region in which each remaining disclosure pattern is an equilibrium, and its efficiency.

Lower bounds need explicit belief systems that support the selected equilibrium off the path. Each step mixes a combinatorial case split over $4$ types and $4$ disclosure vectors with real inequalities in $(p, c, X)$. The regions of Proposition 2 meet along several curves. On each curve, every strict comparison must be checked again, because the corrections above sit exactly there. Comparing only the equilibria the paper names does not bound $V_m$: an equilibrium outside that list could have higher efficiency.

Formalization scope

Lean representation (namespace IntCapAlloc.OrgChoice):

• A type profile and a disclosure vector are Fin 2 → Bool. Project 1 is index 0. A message is Fin 2 → Option Bool.
• A belief is a function from messages to weights on profiles. It is admissible if it is a probability vector on the profiles consistent with the message. It must satisfy Bayes' rule only after messages that some type sends.
• Investors' $k$ uses the existential break-even rule of the paper. The share is the solution of the break-even equation.
• IsEquilibrium requires optimality against all four disclosure vectors and the tie rule per project. effSetM is the set of efficiencies of all equilibria. effSetS is the set of sums of two single-firm equilibrium efficiencies.
• Selected values are stated with IsGreatest, so existence is part of every claim.

Conventions:

• The standing assumptions $0<p<1$, $X>1$, $c>0$, $0<q<1$, $\beta > qX$ and the paper's focus $X \ge 1 + c$ are hypotheses. The goal fails without the focus.
• Footnote 7's "sufficiently high β" is not assumed. The game uses β only through $\beta > qX$, so the statements cover the footnote's case.
• The rule λ = 1 iff θ₁ ≥ θ₂ is the paper's (p. 11).
• Investors' $k$ in the milestones is the value after messages sent in equilibrium.
• Each milestone adds the efficiency its proof states, and posts the uniqueness clause only where it holds.

The goal is not trivial in any of the following ways:

• Off-path beliefs are not fixed, for example to "an undisclosed project is unprofitable".
• The equilibrium set is not limited to the paper's named equilibria.
• $V_m$ and $V_s$ are not defined by formulas.

Any of these would turn the goal into arithmetic.

Needed infrastructure: finite sums over Fin 2 → Bool, case analysis over messages, and real inequalities on the regions. Proofs of the milestones are welcome. So are general lemmas about the break-even rule (investment is monotone in the posterior mean) and about tie-breaking, which several milestones share.

Selected references

• H. Hwang, Internal Capital Allocation, Voluntary Disclosure, and Investment Efficiency, Management Science, 2025 (author manuscript, March 2025). https://doi.org/10.1287/mnsc.2022.01295
• J. C. Stein, Internal Capital Markets and the Competition for Corporate Resources, Journal of Finance 52(1), 1997. https://doi.org/10.1111/j.1540-6261.1997.tb04813.x
• R. A. Dye, Disclosure of Nonproprietary Information, Journal of Accounting Research 23(1), 1985. https://doi.org/10.2307/2490910
• R. E. Verrecchia, Discretionary Disclosure, Journal of Accounting and Economics 5, 1983. https://doi.org/10.1016/0165-4101(83)90011-3

Motivation

A retailer that learns customer preferences online, for example an e-commerce platform choosing which products to display, observes purchases that are not all generated by the population it is trying to learn. Some arrivals are bots, fraudulent accounts or atypical buyers, and their choices can be arbitrary or deliberately misleading. Standard learning algorithms for dynamic assortment optimization under the multinomial-logit (MNL) model assume every customer follows the same choice model. Chen, Krishnamurthy and Wang (arXiv:1910.04183v2, Operations Research 2024) study what can be guaranteed when an $\varepsilon$ fraction of customers are outliers controlled by an adaptive adversary.

The uncontaminated problem has an established regret theory. Agrawal, Avadhanula, Goyal and Zeevi (Operations Research 2019) proved an $\tilde O(\sqrt{NT})$ regret bound for an epoch-based UCB policy. Chen and Wang (Operations Research Letters 2018) gave a matching $\Omega(\sqrt{NT})$ lower bound. Robustness to adversarial corruption was first analysed for multi-armed bandits by Lykouris, Mirrokni and Paes Leme (STOC 2018). The present paper carries that question to MNL assortment optimization, where one observation reveals information about a whole offered set.

Setting

There are $N$ items. Item $i$ has a known revenue $r_i \in [0,1]$ and an unknown utility $v_i \in [0,1]$; the no-purchase option has utility $v_0 = 1$. In each of $T$ periods the retailer offers an assortment $S_t \subseteq [N]$ with $|S_t| \le K$. A typical customer buys item $i \in S_t$ with probability $v_i/(1 + \sum_{j\in S_t} v_j)$ and nothing with probability $1/(1+\sum_{j\in S_t}v_j)$. The expected revenue of $S$ under utilities $w$ is

$$R(S; w) = \frac{\sum_{i\in S} r_i w_i}{1 + \sum_{i\in S} w_i}.$$

An outlier customer chooses from $S_t \cup \{0\}$ according to an arbitrary distribution $Q_t$. An adaptive adversary decides, from the whole public past (types, assortments and purchases), whether the period-$t$ customer is an outlier and which $Q_t$ it uses, subject to sending at most $\varepsilon T$ outliers. Performance is measured by the TOTE regret (typically-optimal, typically-evaluated):

$$\mathrm{Regret}_{\mathrm{TOTE}}(T) = \mathbb E\Big[\sum_{t=1}^T R(S^*; v) - R(S_t; v)\Big],\qquad R(S^*;v) = \max_{|S|\le K} R(S;v).$$

Algorithm 1 (active elimination) receives an upper bound $\bar\varepsilon \ge \varepsilon$. It runs in doubling epochs $T_\tau = 2^\tau T_0$, $T_0 = 128(K+1)^2N\ln T$, and keeps an active item set $\mathcal A^{(\tau)}$ and estimates $\hat v^{(\tau)}$. In each epoch it computes, for every active item $i$, the best assortment $S_\tau^{(i)}$ containing $i$ under the current estimates. It eliminates items whose best assortment falls $2\hat\Delta_{\bar\varepsilon}(\tau)$ below the best, and then offers $S_\tau^{(i)}$ for a uniformly drawn active $i$. It re-estimates $v_i$ by the ratio of purchases of $i$ to no-purchases, and computes a new error bound $\hat\Delta_{\bar\varepsilon}(\tau+1)$.

Formalization targets

Goal: Theorem 1 (p. 12)

There are universal constants $C_0$ and $T_1$ such that the following holds for every $T \ge T_1$, $1 \le N \le T$, $K \ge 1$, $r, v \in [0,1]^N$ and $0 \le \varepsilon \le \bar\varepsilon$, every adaptive adversary with at most $\varepsilon T$ outliers and every tie-break in the argmax:

$$\mathrm{Regret}_{\mathrm{TOTE}}(T) \le C_0\Big(\bar\varepsilon K^2T\log T + \big(K^2\sqrt{\bar\varepsilon}+\sqrt K\big)\sqrt{NT\log^3T} + K^2N\log^2T\Big).$$

The second clause (6) states that if $\bar\varepsilon \le c_1/K^3$ and $K^3N\log T \le c_2T$, the regret is $O\big(\bar\varepsilon K^2T\log T + \sqrt{KNT\log^3T}\big)$.

Milestones

1. Lemma 1 (p. 13): with probability $1 - O(\tau_0N/T^2)$, the estimation error of every active item after a completed epoch is at most $\Delta^*_\varepsilon(i,\tau+1)$ of (7).
2. Lemma 2 (p. 14): $|R(S;\hat v) - R(S;v)| \le 2\sum_{i\in S}|\hat v_i - v_i|/(1+\sum_{i\in S}v_i)$.
3. Corollary 1 (p. 14, corrected): on Lemma 1's success events, the revenue error of every candidate assortment is at most the (corrected) computed bound.
4. Lemma 3 (p. 14): with high probability every optimal assortment survives elimination.
5. Lemma 4 (p. 14): with high probability every assortment offered in epoch $\tau$ loses at most $4\hat\Delta_{\bar\varepsilon}(\tau)$ against $S^*$.
6. (8)–(11) (pp. 14–15): the sum $\sum_{\tau\le\tau_0}4\hat\Delta_{\bar\varepsilon}(\tau)T_\tau$ obeys the bound of Theorem 1.

Significance

The theorem shows that a known contamination level costs an additive $\bar\varepsilon K^2T\log T$ and otherwise leaves the uncontaminated $\sqrt{NT}$ rate intact up to logarithms. Proposition 1 of the paper shows that a cost linear in $\varepsilon T$ is unavoidable. Theorem 1 is also the base case of the paper's algorithm for unknown $\varepsilon$ (Theorem 2), which runs copies of Algorithm 1 at geometrically spaced levels, and of its gap-dependent bound (Theorem 3).

The result is proved on paper, not formalized. The formalization would give the platform its first contaminated-bandit protocol with an adaptive adversary, and its first elimination policy for MNL assortment. During drafting, three printed statements were found to be false as stated (Corollary 1, clause (6), and line 14 of Algorithm 1); they are posed in corrected form. The printed proofs of Lemmas 3, 4 and Theorem 1 rely on the uncorrected Corollary 1. With the corrected Corollary 1, the printed argument gives Theorem 1 only with $\sqrt K$ replaced by roughly $K$ in the $\sqrt{NT\log^3T}$ term. No counterexample to Lemma 3, Lemma 4 or Theorem 1 is known. Completing their proofs at the printed strength is open work in this mission.

Difficulty

The estimator $n_i/n_0(i)$ is a ratio of two counts. An adaptive adversary can choose which periods to corrupt, and it does so after seeing the past and which assortment is about to be offered. The counts are therefore not sums of independent variables. Bounding them needs a martingale (Freedman-type) concentration argument combined with a perturbation bound for the ratio, and the variance depends on the assortment used to estimate each item.

The natural route to Lemmas 3 and 4 is to bound the revenue error of an arbitrary candidate assortment by summing per-item errors, which is what Corollary 1 does. This route breaks for large $K$. The per-item error $\Delta^*$ carries the utility mass of the assortment that estimated item $i$, not of the candidate assortment. Summing these errors therefore loses a factor $\sqrt K$. The page's argument therefore does not deliver the stated $\sqrt K$ dependence, and a sharper joint concentration of the revenue estimate is needed.

Formalization scope

• Types. Items are Fin N, outcomes Option (Fin N) (none is no purchase), periods $0,\dots,T-1$.
• Revenue. $R(S;w)$ is the published ChoiceCDLP.MNL.mnlObjective w r 1 S.
• Adversary. The adversary is deterministic, as in Definition 1, and reads the public past. Its outlier model $Q_t$ may depend on the offered assortment, which is a declared generalization. The budget (A1) holds on every public record of the $T$ periods.
• The run. A run is a record of (drawn item, customer type, purchase) per period. Its law is an explicit product of step probabilities, and expectations and probabilities are finite sums. No measure theory is used.
• Algorithm 1. It is encoded line by line, with the following conventions:
  • $T_0 = \lceil 128(K+1)^2N\ln T\rceil$, and the last epoch $\tau_0$ is truncated at $T$;
  • line 14 is read as $\hat v_i = \min\{1, n_i/n_0(i)\}$, with $\hat v_i = 1$ when $n_0(i)=0$ (correction: the printed $\max$ makes the algorithm eliminate the optimal item);
  • the argmax of line 5 is any routine sel satisfying IsArgmaxSel, and every theorem quantifies over all of them.
• Constants. "Universal constant" and "sufficiently large $T$" are existentials placed before every other quantifier. "With probability $1-O(\tau_0N/T^2)$" is a bound $C\tau_0N/T^2$ on the path-law mass of the bad event ($C(\tau_0+1)N/T^2$ in Lemma 1, counting all $\tau_0+1$ epochs).
• Corrections. Clause (6) carries the added hypothesis $K^3N\log T \le c_2T$, without which it is false. Corollary 1 multiplies the last term of $\hat\Delta$ by $\max\{1,\sqrt{K+1}/2\}$. Its second inequality bounds $|R(S;\hat v)-R(S;v)|$ by the bound at $\max\{\varepsilon,\bar\varepsilon\}$, because $\hat\Delta$ is not monotone in its parameter. Lemma 1 drops its unused condition on $\bar\varepsilon$.
• Ruling out trivializations. The regret is an expectation over the true law of the run against every adaptive adversary and every tie-break, so a fixed history, an oblivious adversary, a policy that knows $v$, or constants chosen after $N$ and $K$ do not satisfy the statement.

A complete development needs Freedman's martingale inequality for bounded increments with a predictable variance bound, which several Open platform items state. It also needs a perturbation analysis of ratio estimators and bookkeeping over doubling epochs. The concentration and summation lemmas are reusable for other elimination policies. Proofs of any milestone, and a corrected proof of Corollary 1's consequences at full strength, are welcome.

Selected references

• X. Chen, A. Krishnamurthy, Y. Wang, Robust Dynamic Assortment Optimization in the Presence of Outlier Customers, Operations Research, 2024; arXiv:1910.04183v2. https://arxiv.org/abs/1910.04183
• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://doi.org/10.1287/opre.2018.1832
• X. Chen, Y. Wang, A note on a tight lower bound for MNL-bandit assortment selection models, Operations Research Letters 46(5):534–537, 2018. https://arxiv.org/abs/1709.06109
• T. Lykouris, V. Mirrokni, R. Paes Leme, Stochastic Bandits Robust to Adversarial Corruptions, STOC 2018. https://arxiv.org/abs/1803.09353
• D. A. Freedman, On Tail Probabilities for Martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452

Motivation

Fault-tolerant quantum computers implement Clifford gates cheaply and the non-Clifford T gate expensively, because T gates are obtained by magic-state distillation (Fowler, Stephens and Groszkowski). Single-qubit rotations by small, arbitrary angles appear throughout quantum simulation and must be compiled into Clifford+T circuits, so the T-count of a small rotation is a standard cost measure. Selinger's ancilla-free method uses about $4\log_2(1/\theta)$ T gates for a $Z$-rotation by $\theta$ (arXiv:1212.6253), and the paper's own search puts optimal ancilla-free Clifford+T synthesis near $3\log_2(1/\theta)$ (Sec. VI).

Wiebe and Kliuchnikov (arXiv:1305.5528) proposed non-deterministic circuits with ancillas and measurement, the gearbox circuit and its recursive composed gearbox circuit, which, like the linear-combination-of-unitaries circuits of Childs and Wiebe, turn a coarse rotation into a much finer one and whose failures are undone by a Clifford gate, so they can be repeated until they succeed. The cost of such a repeat-until-success scheme is a random variable. Theorem 2 of the paper computes its mean exactly and bounds its variance; this mission formalizes that result together with the circuit identities it rests on.

Setting

A qubit has basis $|0\rangle,|1\rangle$; a gate is a $2\times2$ unitary $U$ with entry $U_{1,0}=\langle1|U|0\rangle$. Let $X=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ and $e^{-i\varphi X}=\cos\varphi\,\mathbb 1-i\sin\varphi\,X$.

Gearbox circuit $C^{(d)}(U^1,\dots,U^d)$. Prepare $d$ ancillas in $|0\rangle$ and a target in $|\psi\rangle$. Apply $U^1\otimes\cdots\otimes U^d$ to the ancillas, then a $d$-controlled $-iX$ on the target (active when every ancilla is $|1\rangle$), then $U^{1\dagger}\otimes\cdots\otimes U^{d\dagger}$, and measure the ancillas in the computational basis. Outcome $0\cdots0$ is success.

Composed gearbox circuit (Definition 1). $C^{\circ1}(U)$ is $C^{(1)}(U)$, and $C^{\circ d}(U)=C^{\circ1}(C^{\circ(d-1)}(U))$: the gate fed to the outer gearbox is the rotation the inner composed circuit enacts on success. Write $\theta_0\in[0,\pi/2]$ for the angle with $\sin^2\theta_0=|U_{1,0}|^2$ and, for $q\ge1$,

$$\varphi_q=\tan^{-1}\big(\tan^{2^{q-1}}\theta_0\big),\qquad P_q=\sin^4\varphi_q+\cos^4\varphi_q .$$

Cost. Level $q$ of $C^{\circ d}(U)$ is attempted until its measurement succeeds; the number of attempts $N_q$ is geometric on $\{1,2,\dots\}$. Each attempt at level $q\ge2$ needs one successful copy of $C^{\circ(q-1)}(U)$ and one of its inverse. With $x_d$ the number of applications of $C^{\circ1}(U)$ before $C^{\circ d}(U)$ succeeds, Appendix A's equation (A1) reads

$$x_1=N_1,\qquad x_d=\sum_{i=1}^{N_d}(\eta_i+\chi_i),$$

with $\eta_i,\chi_i$ distributed as $x_{d-1}$ and everything independent. Each $C^{\circ1}(U)$ uses one $U$ and one $U^\dagger$, so the number of applications of $U$ or $U^\dagger$ is $n_d=2x_d$.

Formalization targets

Goal: Theorem 2 (p. 6)

For every unitary $U$ and $d\ge1$,

$$\mathbb E(n_d)=\frac{2^d}{P_1\cdots P_d},$$

and, for $\theta_0<\pi/4$,

$$\mathbb V(n_d)\le\frac{2^{2d+1}(1-P_1)}{P_d^2\cdots P_1^2}\left(1+\frac{P_d\cdots P_1}{2^dP_1}\right).$$

Both clauses are stated as printed; the mean is exact for every $\theta_0\in[0,\pi/2]$.

Milestones

1. Theorem 1 (p. 2): on outcome $0$ the gearbox circuit leaves $\sqrt{\cos^4\theta+\sin^4\theta}\,e^{-iX\tan^{-1}(\tan^2\theta)}|\psi\rangle$, where $\sin^2\theta=\prod_\ell|U^\ell_{1,0}|^2$; this has probability $\cos^4\theta+\sin^4\theta$; every other outcome enacts $e^{i\pi X/4}$ up to a scalar.
2. Corollary 1 (p. 5): on success, $C^{\circ d}(U)=e^{-i\tan^{-1}(\tan^{2^d}\theta_0)X}$.
3. Appendix A, p. 14: the level-$q$ success probability is $P_q$; $\mathbb E(N_q)=1/P_q$ and $\mathbb V(N_q)=(1-P_q)/P_q^2$.
4. (A3): $\mathbb E(x_d)=2\,\mathbb E(N_d)\,\mathbb E(x_{d-1})$.
5. (A6): $\mathbb V(x_d)=2\,\mathbb V(x_{d-1})\,\mathbb E(N_d)+4\,\mathbb V(N_d)\,(\mathbb E(x_{d-1}))^2$.
6. Appendix A, p. 15: $P_q$ increases with $q$ when $\theta_0<\pi/4$.

Significance

The theorem shows that the composed gearbox reaches a rotation angle of order $\tan^{2^d}\theta_0$, doubly exponentially small in $d$, while using $\Theta(2^d)$ applications of $U$ in expectation, with a variance of the same squared order. Since $d\approx\log_2\log(1/\theta)$ levels give angle $\theta$, the gate cost scales like $\log(1/\theta)$ with a constant that depends on $U$ only through $P_1,P_2,\dots$; this is the basis of the paper's floating-point synthesis scheme, which combines a mantissa rotation with an exponent rotation produced this way (Sections IV–V).

The result has a complete written proof in Appendix A. As far as is known it has no machine-checked proof. The formalization adds three things: the circuit identities of Theorem 1 and Corollary 1 as exact matrix statements, including the boundary case $|U_{1,0}|=1$; the identification of the circuit's Born-rule success probabilities with the closed forms $P_q$; and the random-sum identities (A3), (A6) in a form where infinite moments cannot be hidden.

Difficulty

The computational parts are elementary but long. The real difficulty is that the theorem joins two models: a quantum circuit, whose success probabilities come from matrix entries of a post-selected block, and a nested random sum whose summands are themselves random sums. A naive approach postulates the success probabilities $P_q$ and proves a lemma about compound geometric sums. That approach proves nothing about the circuit: the content linking the two is milestone 3, which needs Theorem 1 at every level of the recursion and Corollary 1 to identify the gate fed to level $q$. On the probabilistic side, the variance identity for a random number of independent summands requires finiteness of all second moments, and the bound requires unfolding a recursion whose coefficients $1/P_q$ vary with the level, which is where the monotonicity of $P_q$ enters.

Formalization scope

States are vectors Fin 2 → ℂ; gates are Matrix (Fin 2) (Fin 2) ℂ, unitarity is membership in Matrix.unitaryGroup, and $|0\rangle,|1\rangle$ are indices 0, 1. The $d$ ancillas are Fin d → Fin 2, and the joint space is (Fin d → Fin 2) × Fin 2 with ancillas first; the controlled gate fires on the all-ones string. The rotation is the matrix $\cos\varphi\,\mathbb 1-i\sin\varphi\,X$, so $e^{i\pi X/4}$ is the rotation by $-\pi/4$. Because Lean's Real.tan returns $0$ at $\pi/2$, the angles $\tan^{-1}(\tan^2\theta)$ and $\tan^{-1}(\tan^{2^d}\theta_0)$ are defined to be $\pi/2$ when the cosine vanishes, the paper's value $\tan^{-1}(\infty)$; the case $|U_{1,0}|=1$ is not excluded. $C^{\circ d}(U)$ is the recursively defined success unitary: the outcome-$0$ block of the one-ancilla gearbox fed with $C^{\circ(d-1)}(U)$, normalized by the norm of its first column.

The number of applications of $U$ or $U^\dagger$ used to enact $C^{\circ d}(U)$ is modelled by Appendix A's recursion (A1): Theorem 2 speaks of "a given attempt", but its proof defines $x_d$ as the count until $C^{\circ d}(U)$ succeeds, and that is the quantity formalized. Laws are Mathlib PMF ℕ with independence built into bind; the geometric law is Mathlib's geometricMeasure shifted to $\{1,2,\dots\}$; means and variances are ℝ≥0∞-valued sums.

Three trivializing formalizations are ruled out. The law of $n_d$ uses the circuit's Born-rule success probabilities, never $P_q$ supplied as an input, so Theorem 1 and Corollary 1 are needed for the goal. Moments are in $[0,\infty]$, so a divergent variance is $\infty$, never the junk value $0$ that would make the bound trivially true. The angle convention above excludes the false reading $\tan(\pi/2)=0$ in Theorem 1 and Corollary 1.

Everything needed is in Mathlib: matrices, unitaryGroup, Real.arctan, PMF.bind/PMF.map, geometricMeasure. Reusable beyond this mission: the moments of the shifted geometric law and the mean and variance identities for a sum of a random number of i.i.d. summands, in ℝ≥0∞ form. Contributions to any milestone are welcome; the probabilistic milestones (3–6) do not depend on the circuit milestones except through part 1 of milestone 3.

Selected references

• N. Wiebe and V. Kliuchnikov, Floating point representations in quantum circuit synthesis, arXiv:1305.5528v3, 2013. https://arxiv.org/abs/1305.5528v3
• P. Selinger, Efficient Clifford+T approximation of single-qubit operators, Quantum Inf. Comput. 15, 2015. https://arxiv.org/abs/1212.6253
• A. M. Childs and N. Wiebe, Hamiltonian simulation using linear combinations of unitary operations, Quantum Inf. Comput. 12, 2012. https://arxiv.org/abs/1202.5822
• A. G. Fowler, A. M. Stephens and P. Groszkowski, High-threshold universal quantum computation on the surface code, Phys. Rev. A 80, 052312, 2009. https://arxiv.org/abs/0803.0272

Motivation

Firms and public agencies often roll a new product, feature or policy out gradually: a few markets first, more later, every market eventually. When the rollout is itself an experiment, its schedule determines how precisely the effect of the treatment can be estimated. A staggered rollout is the common design in which treatment, once switched on in a unit, stays on. Examples are a ride-sharing feature introduced city by city, a hospital protocol adopted ward by ward, or a stepped-wedge clinical trial. The effect of such a treatment often builds up over several periods, so the analyst wants the instantaneous effect and the lagged ones. The design question is then: in which period should each unit adopt?

Xiong, Athey, Bayati and Imbens (arXiv:1911.03764, Management Science 2024) answer this question in closed form for the trace criterion. Their non-adaptive result, Theorem 3.1, says that an optimal rollout has a treated fraction that follows a fixed S-shaped curve in time, and that each adoption cohort balances the observed and latent covariates.

Setting

There are $N$ units and $T$ periods. A design assigns to every unit $i$ an adoption time $A_i\in[T]\cup\{\infty\}$, where $\infty$ means never treated. The treatment indicator is coded $z_{it}=+1$ if $A_i\le t$ and $z_{it}=-1$ otherwise. The outcome model, (3.1) of the paper, is

$$Y_{it}=\alpha_i+\beta_t+X_i^\top\theta_t+\tau_0z_{it}+\tau_1z_{i,t-1}+\dots+\tau_\ell z_{i,t-\ell}+u_i^\top v_t+\varepsilon_{it}.$$

It has unit effects $\alpha_i$, time effects $\beta_t$, observed covariates $X_i\in\mathbb R^{d_x}$ with period-specific slopes $\theta_t$, and $\ell\ge0$ known lags. Latent covariates $u_i\in\mathbb R^{d_u}$ load on random factors $v_t$ with covariance $\Sigma_v$, and the noise $\varepsilon_{it}$ has variance $\sigma_\varepsilon^2$. The effects $\tau=(\tau_0,\dots,\tau_\ell)$ are estimated by generalized least squares on periods $\ell+1,\dots,T$. The per-period error covariance is $\Psi=U\Sigma_vU^\top+\sigma_\varepsilon^2I_N$, and the errors are uncorrelated across periods.

By the Gauss–Markov (Aitken) theorem, which is proved on Prove2Me as VectorSpaceOpt.gauss_markov, the covariance of the GLS estimator is $(W^\top\Sigma_e^{-1}W)^{-1}$ for the regressor matrix $W$. The precision $\operatorname{Prec}(\hat\tau;A)$ is therefore a deterministic matrix, (EC.2.1)–(EC.2.2): the Schur complement of the nuisance block. The T-optimal design problem (3.2) is

$$\max_{A\in([T]\cup\{\infty\})^N}\ \operatorname{tr}\operatorname{Prec}(\hat\tau;A).$$

With $h=\lfloor\ell/2\rfloor$, the paper defines a vector $a^{(\ell)}=(M^{(\ell)})^{-1}b^{(\ell)}$ of length $\ell-h$ from explicit $M^{(\ell)}$, $b^{(\ell)}$ ((EC.1.2)–(EC.1.3)). The S-shaped fraction $\omega^*_{\ell,t}$ of (3.4) has five stages: it is $-1$ for $t\le h$, equals $a^{(\ell)}_{t-h}$ for $h<t\le\ell$, is linear, $-1+(2t-(\ell+1))/(T-\ell)$, for $\ell<t\le T-\ell$, is antisymmetric in the fourth stage, and is $1$ at the end.

Formalization targets

Goal: Theorem 3.1

Assume $\sigma_\varepsilon^2>0$, $\Sigma_v=\sigma_\varepsilon^2I$, centred rows $\sum_iX_i=0$ and $\sum_iu_i=0$, $\sum_iX_iu_i^\top=0$, and, when $\ell>0$, $T>(\ell^3+13\ell^2+7\ell+3)/(8\ell)$. If

$$A\in\mathbb A_\ell\cap\mathbb A_X\cap\mathbb A_U,$$

then $\operatorname{tr}\operatorname{Prec}(\hat\tau;A')\le\operatorname{tr}\operatorname{Prec}(\hat\tau;A)$ for every design $A'$. Here $\mathbb A_\ell$ is the set of designs whose treated fraction at every $t$ is $(1+\omega^*_{\ell,t})/2$, and $\mathbb A_X$, $\mathbb A_U$ are the sets of designs whose adoption cohorts in periods $2,\dots,T$ have zero sum of $X_i$ (respectively $u_i$).

Milestones

1. Lemma EC.1.2 (corrected): $\operatorname{tr}\operatorname{Prec}(\hat\tau)=-\frac N{\sigma_\varepsilon^2}\sum_{j}\big(f_{j,1}+f_{j,X}+f_{j,U}\big)$. The first term depends only on the treated fractions, the second only on $X$, the third only on $U$.
2. The vector $a^{(\ell)}$ exists, and the resulting $\omega^*$ is feasible: nondecreasing, with values in $[-1,1]$, and the stage-2 values lie in $[-1,-1+(\ell+1)/(T-\ell)]$.
3. $\omega^*$ minimizes $f_1=\sum_jf_{j,1}$ over all nondecreasing paths in $[-1,1]^T$.
4. The covariate terms are nonnegative, and they vanish when $X^\top z_t$ and $U^\top z_t$ are constant in $t$.

Significance

The theorem turns a combinatorial design problem over $(T+1)^N$ schedules into explicit conditions. The fraction of treated units follows a universal curve that depends only on $(\ell,T)$, and the cohorts must balance the covariates. Two features are useful in practice. Without lags the optimal fraction grows linearly. With lags the optimal rollout starts and ends more slowly, which is what the extra stages capture. The paper uses these conditions to build practical designs (rounding the fractions to integers, stratifying on estimated latent factors) and an adaptive version.

The result is proved in the paper; this mission formalizes it. Formalizing it also repairs the record. Two statements in the printed proof are false as printed, and so is one display. The vector $b_\ell$ of Lemma EC.1.2 has an off-by-one, and its observed-covariate term is correct only when $X^\top X=N\,I$. The linear term of (EC.2.6) is summed over the wrong range. The mission states the corrected versions, each with a counterexample to the printed one. Theorem 3.1 itself is true as printed. Planning checked it by brute force on small instances, and checked the optimality of $\omega^*$ with an exact certificate for $\ell\le12$. As far as a search of Prove2Me shows, nothing about panel experimental design or GLS precision has been formalized there before.

Difficulty

The objective is a trace of a Schur complement, and the design enters through $\pm1$ entries in a large regression. Expanding that objective into the separable form of Lemma EC.1.2 requires exact control of the projection onto the two-way fixed effects and the period-specific covariate slopes. This is where the printed lemma goes wrong. The relaxed problem in $\omega$ is a convex quadratic program with monotonicity and box constraints. Its solution is not linear when $\ell>0$: the stage-2 values solve a linear system whose feasibility (bounds and monotonicity) holds only above a threshold in $T$. That is the role of the cubic threshold. A natural first idea is that "spread adoption evenly" is optimal. It is optimal only for $\ell=0$; for $\ell>0$ the KKT system forces nonlinear stages at both ends. A second step must also be checked: the $\pm1$ designs, whose fractions satisfy $\mathbb A_\ell$ and whose cohorts satisfy the balance conditions, minimize all three terms at once.

Formalization scope

• Units and periods are Fin N and Fin T, with periods 0-based. A design is Fin N → WithTop (Fin T), with ⊤ for never treated, and $z_{it}=\pm1$.
• The precision trace is $\sum_{j=0}^{\ell}\min_\gamma$ of the $\Psi^{-1}$-weighted residual sum of squares of the lag-$j$ column regressed on the nuisance columns. These are all $N$ unit dummies, a time dummy for each observed period, and a slope on $X_i$ for each observed period. This equals the trace of (EC.2.2) wherever that formula is defined. It is defined for every design and every $X$, with no matrix inverse of a possibly singular matrix.
• The random model enters only through $\Sigma_e=I\otimes\Psi$. Assumptions 2.1, 2.2 and 3.1 are encoded by the design type and this covariance; $\sigma_\varepsilon^2>0$ is a hypothesis.
• The threshold is read as "if $\ell>0$ then $T>\dots$", because the expression is undefined at $\ell=0$.
• Lemma EC.1.2 is stated with $b_{\ell,t}=(T_\ell+1-2t)/T_\ell$, and its $X$-term is $\frac1N z^\top(P\otimes H_X)z$, with $H_X$ the projector onto the column space of $X$, written without a pseudo-inverse.

The comparison design $A'$ ranges over all designs, never over $\mathbb A_\ell$ or relaxed fractions. The coding is $\pm1$, not $0/1$. The estimator uses only periods $\ell+1,\dots,T$. Coding with $0/1$ or dropping the period-specific slopes would change $\omega^*$ and the covariate term, and would be a different theorem. The set $\mathbb A_{\mathrm{opt}}$ can be empty for some $N$, in which case the goal holds vacuously, exactly as the paper's "if" allows. A sanity file exhibits nonempty instances, at $\ell=0$ with $d_x=d_u=1$ and at $\ell=1$, and reproduces a value of Example EC.1.4.

A complete development needs least-squares projections, Schur complements, centring matrices, and a KKT certificate for a monotone-constrained quadratic program. The first three are reusable well beyond this mission. Contributions to any milestone are welcome.

Selected references

• R. Xiong, S. Athey, M. Bayati, G. Imbens, Optimal Experimental Design for Staggered Rollouts, Management Science, 2024; arXiv:1911.03764v6. https://arxiv.org/abs/1911.03764
• A. C. Atkinson, V. V. Fedorov, The design of experiments for discriminating between two rival models, Biometrika 62(1), 1975. https://doi.org/10.1093/biomet/62.1.57
• J. Bai, Inferential theory for factor models of large dimensions, Econometrica 71(1), 2003. https://doi.org/10.1111/1468-0262.00392
• M. A. Hussey, J. P. Hughes, Design and analysis of stepped wedge cluster randomized trials, Contemporary Clinical Trials 28(2), 2007. https://doi.org/10.1016/j.cct.2006.05.007

Motivation

Ride-hailing, car-sharing and bike-sharing platforms, as well as scrip systems, move a fixed stock of reusable resources around a network. Each customer that is served relocates one unit, from a pick-up location to a drop-off location. The operator decides, customer by customer, whether to serve and with which unit. Supply can run dry at a location, which forbids serving from there. Demand also varies over the day, and the operator rarely knows the arrival rates.

Kanoria and Qian (arXiv:1903.02764v4; Management Science, 2024) propose Mirror Backpressure (MBP), a policy that uses only the current queue lengths and never estimates the rates. They prove that it is near-optimal against the best policy that knows the rates. Earlier guarantees for closed networks, such as Banerjee, Freund and Lykouris (arXiv:1608.06819), need exact knowledge of stationary rates and bound only the steady state. Classical backpressure (Tassiulas and Ephremides, 1992) and the drift-plus-penalty method (Neely, 2010) address open networks, where the no-underflow constraint is handled by idling, not by a fixed stock of units.

Setting

A closed network has a finite set $V$ of $m = |V| > 1$ nodes and $K$ identical supply units. The state is the vector of queue lengths $\mathbf q \in \Omega_K = \{\mathbf q \in \mathbb Z_+^m : \mathbf 1^\top \mathbf q = K\}$. In each period $t = 0, 1, \dots$ exactly one customer arrives. Her type $\tau$ lies in a finite set $\mathcal T$ and is drawn from a probability vector $\boldsymbol\phi^t$, independently of the past. Type $\tau$ has nonempty pick-up and drop-off neighborhoods $\mathcal P(\tau), \mathcal D(\tau) \subseteq V$.

After seeing $\tau$, the controller drops the customer or serves her with a pair $(j,k) \in \mathcal P(\tau) \times \mathcal D(\tau)$. Serving collects a payoff $w_{j\tau k}$, with $|w_{j\tau k}| \le 1$, and moves one unit from $j$ to $k$. Serving from $j$ requires $q_j > 0$: this is the no-underflow constraint. A feasible policy may randomize, depend on the whole history and the period, and know the rates.

Write $J^\pi_T(\mathbf q)$ for the expected payoff of $\pi$ in periods $0, \dots, T-1$ from $\mathbf q[0] = \mathbf q$. The benchmark is $W^*_T = \sup_\pi \max_{\mathbf q} J^\pi_T(\mathbf q)/T$, and a policy is evaluated from its worst initial state, $W^\pi_T = \min_{\mathbf q} J^\pi_T(\mathbf q)/T$. The loss is $L^\pi_T = W^*_T - W^\pi_T$.

The rates vary $\eta$-slowly if $\frac{1}{T-1}\sum_{t} \|\boldsymbol\phi^{t+1} - \boldsymbol\phi^t\|_1 \le \eta$. The connectedness

$$\alpha(\boldsymbol\phi) = \min_{\emptyset \ne S \subsetneq V} \sum_{\tau:\ \mathcal P(\tau) \cap S \ne \emptyset,\ \mathcal D(\tau) \setminus S \ne \emptyset} \phi_\tau$$

is the smallest rate of demand that can carry supply out of any proper node set. Condition 1 requires $\alpha(\boldsymbol\phi^t) > 0$ in every period, and $\alpha_{\min} = \min_t \alpha(\boldsymbol\phi^t)$.

MBP normalizes queue lengths as $\bar q_i = (q_i + \sqrt K)/\tilde K$ with $\tilde K = K + m\sqrt K$, and uses the congestion function $f(x) = -\sqrt m\, x^{-1/2}$. For a type-$\tau$ customer it picks $(j^*, k^*)$ maximizing the score $w_{j\tau k} + f(\bar q_j) - f(\bar q_k)$ over $\mathcal P(\tau) \times \mathcal D(\tau)$. It serves with that pair if the score is nonnegative and $q_{j^*} > 0$, and drops the customer otherwise.

Formalization targets

Goal: Theorem 1

There are a universal $C$ and $K_1 = \mathrm{poly}(m, 1/\alpha_{\min})$ such that for every instance and every $K \ge K_1$,

$$L^{\mathrm{MBP}}_T \le Cm\Big(\frac KT + \sqrt{\eta K}\Big) + \frac{Cm^2}{K}.$$

The constants are existential and fixed before the instance. A sharper constant is a stronger result that does not invalidate the goal.

Milestones

The milestones follow the paper's proof.

• Lemmas 4–6 and Proposition 1. Any policy's average payoff is at most the value of the static planning LP at the average rate $\bar{\boldsymbol\phi}$, with flow balance relaxed by $K/T$. The relaxation costs at most $mK/T$, so $W^*_T \le W^{\mathrm{SPP}}(\bar{\boldsymbol\phi}) + mK/T$.
• Strong duality for the partial dual $g(\mathbf y) = \sum_\tau \phi_\tau \max_{j,k}(w_{j\tau k} + y_j - y_k)^+$.
• Lemmas 1–3. A one-period decomposition of MBP's suboptimality into a potential drift $\mathcal V_1$, a stochastic term $\mathcal V_2$, a dual gap $\mathcal V_3$ and an underflow indicator $\mathcal V_4$. Then $\mathcal V_3 \le -\alpha(\boldsymbol\phi)[\max_j y_j - \min_j y_j - 2m]^+$ at $\mathbf y = \mathbf f(\bar{\mathbf q})$, and $\mathcal V_2 + \mathcal V_3 + \mathcal V_4 \le Cm^2/\tilde K$.
• Propositions 3, 4, 2. The policy gap $\frac1T\sum_t W^{\mathrm{SPP}}(\boldsymbol\phi^t) - W^{\mathrm{MBP}}_T \le CmK/T + Cm^2/K$. The variation gap $\frac1T\sum_t W^{\mathrm{SPP}}(\boldsymbol\phi^t) \ge W^{\mathrm{SPP}}(\bar{\boldsymbol\phi}) - m\eta T$. Batching them gives $L^{\mathrm{MBP}}_T \le CmK/\Delta_T + Cm^2/K + \Delta_T m\eta$ for every $0 < \Delta_T < T$.

Significance

Theorem 1 gives a finite-$K$, finite-horizon guarantee for a policy that is blind to the arrival rates. Its steady-state per-customer loss is $O(1/K)$ for stationary demand, the same order as rate-aware state-independent policies. Under imperfect rate estimates, any state-independent policy suffers a loss of order one (Banerjee, Kanoria and Qian, 2018, Proposition 4). The bound holds for arbitrary slowly varying demand. It does not degrade in the large-market regime where $K$ and the demand grow together.

The theorem is proved in the paper; nothing in it is formalized anywhere. This mission would give the platform its first controlled closed-network model: demand types with pick-up and drop-off sets, the no-underflow constraint, and history-dependent randomized policies over a finite horizon. It would also add a fully machine-checked drift-plus-penalty argument with an underflow term. One printed statement is corrected: Lemma 1 as printed has $\mathcal V_2$ with coefficient $1/(2\tilde K)$, which a two-node instance refutes. The milestone uses $1/\tilde K$, and Theorem 1 is unaffected.

Difficulty

The natural route is the backpressure argument: score each pair by payoff plus congestion difference and bound the Lyapunov drift. That argument assumes that serving from an empty queue is either impossible or harmless. Here the no-underflow constraint binds. The congestion-adjusted score can be positive at an empty queue, so the policy is forced to drop customers that the fluid solution would serve. Virtual-queue workarounds fail in a closed network because fake units never leave. Linear congestion costs, as in regular backpressure, can lose a constant per customer.

The proof needs three ingredients. First, a potential whose gradient is the steep congestion function. Second, the observation that the dual gap $\mathcal V_3$ is very negative exactly when some queue is short. Third, a growth estimate with the $\sqrt K$ offset showing that $\mathcal V_3$ absorbs $\mathcal V_2 + \mathcal V_4$ once $K \ge \mathrm{poly}(m, 1/\alpha)$. The finite-horizon benchmark separately requires a flow-decomposition argument and LP sensitivity in the rates.

Formalization scope

• Model. Nodes and types are Fintypes, with 1 < Fintype.card V. Decisions are Option (V × V). Periods are numbered from $0$, with rates phi : ℕ → Ty → ℝ.
• Policies and payoff. Policies are probability vectors on feasible decisions as a function of the period, the past (state, type, decision) triples, the current state and the current type. The history includes past decisions, so the class contains the paper's. The expected payoff is a finite recursion over types and decisions, with no measure theory.
• Loss. The loss is stated without a supremum: for every policy $\pi$ and initial states $\mathbf q, \mathbf q'$, $(J^\pi_T(\mathbf q) - J^{\mathrm{MBP}}_T(\mathbf q'))/T \le$ bound.
• Constants and tie-breaks. "Poly" is $c\,(m + 1/\alpha)^N$, with $C, c, N$ quantified before every type and instance. MBP is Algorithm 1 exactly, under every argmax tie-break. Payoffs satisfy $|w| \le 1$ rather than $\max|w| = 1$.
• Readings. Proposition 1's "$W^* \le W^{\mathrm{SPP}}(\bar{\boldsymbol\phi})$" is read as $W^* \le \limsup_T W^{\mathrm{SPP}}(\bar{\boldsymbol\phi}_T)$. The maximum of $|f'|$ in $\mathcal V_2$ is rendered as any upper bound $B$.

The statement has a trivializing formalization that is excluded. If $K_1$ or $C$ could depend on $T$, $\boldsymbol\phi$ or $\eta$, the choice $K_1 = T$ would make $CmK/T \ge 2 \ge L_T$ and the theorem empty. Likewise, a benchmark restricted to Markov or deterministic policies, or a supremum over an unconstrained set, would change what is proved.

The definitions of the closed network, the static planning LP with its relaxed flow balance, acyclic flows and the partial dual are reusable for other closed-network and ride-hailing results. Contributions are welcome on every milestone. The LP lemmas (4–6, strong duality, Lemma 2, Proposition 4) are independent of the policy and can be attacked first. Platform results LinearOptimization.lp_strong_duality and LinearOptimization.network_flow_decomposition_including_zero are available as tools.

Selected references

• Y. Kanoria, P. Qian, Blind Dynamic Resource Allocation in Closed Networks via Mirror Backpressure, arXiv:1903.02764v4, 2022; Management Science, 2024. https://arxiv.org/abs/1903.02764v4
• S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research, 2021. https://arxiv.org/abs/1608.06819
• S. Banerjee, Y. Kanoria, P. Qian, Dynamic Assignment Control of a Closed Queueing Network under Complete Resource Pooling, arXiv:1803.04959, 2018 (also ACM SIGMETRICS 2018). https://arxiv.org/abs/1803.04959
• M. J. Neely, Stochastic Network Optimization with Application to Communication and Queueing Systems, Morgan & Claypool, 2010. https://doi.org/10.2200/S00271ED1V01Y201006CNT007
• L. Tassiulas, A. Ephremides, Stability Properties of Constrained Queueing Systems and Scheduling Policies for Maximum Throughput in Multihop Radio Networks, IEEE Transactions on Automatic Control, 1992. https://doi.org/10.1109/9.182479
• A. Beck, M. Teboulle, Mirror Descent and Nonlinear Projected Subgradient Methods for Convex Optimization, Operations Research Letters, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6