Missions · Prove2Me

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models: The Adaptive-Confidence Trisection Policy Has N-Independent Regret at Most C√TResearch Paper

Learning which products to offer

A retailer that sells $N$ substitutable products must decide, for each arriving customer, which subset of products to display. Customer preferences are unknown at the start and have to be learned from purchases, while every suboptimal display costs revenue. This is dynamic assortment planning, a standard problem of revenue management in e-commerce and online advertising, and its learning version is a bandit problem whose arms are the $2^N$ subsets of products.

Under the multinomial logit (MNL) choice model the problem has been studied through the regret of a policy over $T$ customers (Chen, Wang and Zhou, §2 and Table 1):

Rusmevichientong, Shen and Shmoys (2010) analysed the same revenue potential as this paper with a golden-ratio search; their bound involves $\log N$ and needs a separability (gap) assumption between candidate assortments.
Sauré and Zeevi (2013) also cast MNL assortment learning as regret minimization.
Agrawal, Avadhanula, Goyal and Zeevi gave UCB and Thompson-sampling policies with regret $\tilde O(\sqrt{NT} + N)$ for assortments of capacity $K$ .
Chen and Wang (2018) proved an $\Omega(\sqrt{NT})$ lower bound in the capacitated model when $K \le N/4$ .

In the capacitated model the regret must grow with $N$ . Chen, Wang and Zhou (arXiv:1805.04785v2, Mathematics of Operations Research 2021) show that without a capacity constraint it need not: a trisection policy achieves regret $C_1\sqrt T$ with a universal constant, and $\sqrt T/384$ is a lower bound. This mission formalizes the upper bound.

Setting

There are $N$ items with known revenues $r_1,\dots,r_N \in [0,1]$ and unknown utilities $v_1,\dots,v_N \ge 0$ ; the no-purchase option has utility $v_0 = 1$ . In each period $t = 1,\dots,T$ the retailer offers an assortment $S_t \subseteq [N]$ , and the customer buys $j \in S_t$ with probability $v_j/(1+\sum_{i\in S_t} v_i)$ or buys nothing with probability $1/(1+\sum_{i\in S_t} v_i)$ , independently of the past. The expected revenue of $S$ is

R(S) = \frac{\sum_{j\in S} r_j v_j}{1 + \sum_{j\in S} v_j},

and the regret of a policy is $\mathrm{Regret} = \mathbb E\sum_{t=1}^T R(S^*) - R(S_t)$ , where $S^*$ maximizes $R$ over all $2^N$ subsets.

The policy rests on two objects. The level set $\mathcal L_\theta = \{i : r_i \ge \theta\}$ collects the items whose revenue is at least $\theta$ . The revenue potential $F(\theta) = R(\mathcal L_\theta)$ is a piecewise-constant function of one real variable. Its maximum is $F^* = \sup_{\theta \ge 0} F(\theta)$ , its right limit is $F(\theta^+)$ , and $\theta^*$ denotes the fixed point $\theta^* = F(\theta^*) = F^*$ .

The adaptive-confidence trisection policy keeps an interval $[a_\tau, b_\tau]$ , starting from $[0,1]$ . In epoch $\tau$ it forms the points $x_\tau = \tfrac23 a_\tau + \tfrac13 b_\tau$ and $y_\tau = \tfrac13 a_\tau + \tfrac23 b_\tau$ , at distance $\varepsilon_\tau = y_\tau - x_\tau = \tfrac13(\tfrac23)^\tau$ , and runs $n_\tau = 8\lceil\varepsilon_\tau^{-2}\ln(8T\varepsilon_\tau^2)\rceil$ inner iterations. Each inner iteration does two things:

while $y_\tau$ lies inside the current confidence interval $[\ell, u]$ for $F(y_\tau)$ , it explores: it offers $\mathcal L_{y_\tau}$ , adds the revenue to the running sum $\rho_t$ , and sets $[\ell_t, u_t] = \rho_t/t \pm \sqrt{2\ln(8T/t)/t}$ ;
it then exploits by offering $\mathcal L_{a_\tau}$ .

At the end of the epoch the policy sets $b_{\tau+1} = y_\tau$ if $u < y_\tau$ , and $a_{\tau+1} = x_\tau$ otherwise. The policy knows $r$ and $T$ but never $v$ .

Formalization targets

Goal: Theorem 3

There is a universal constant $C_1 > 0$ such that for every $N$ , every horizon $T$ , all $v_i \ge 0$ and all $r_i \in [0,1]$ , the adaptive-confidence trisection policy satisfies

\mathbb E\sum_{t=1}^T R(S^*) - R(S_t) \le C_1\sqrt T.

No gap condition and no bound on $v$ is assumed. The constant is left unspecified, as in the paper.

Milestones

Structure of $F$ . Lemma 1 (revenue-ordered optimality), Corollary 1 ( $F^* = R(S^*)$ ), Lemma 2 (the fixed point, under $F^* > 0$ ), the jump identity (S4)/(S8), and Lemmas 3–4 ( $F$ is below the diagonal to the right of $\theta^*$ and above it to the left).
Concentration. Hoeffding's inequality (Lemma 15, already proved on the platform), the uniform inequality with growing confidence levels (Lemma 8, (11)), and the two tail bounds (S32) and (S33) used in the proof of Lemma 10.
Recursion. With $\psi^\omega_\tau(\alpha,\beta)$ the expected regret of epochs $\tau,\dots,\tau_0$ conditioned on the relative position of $a_\tau$ , $b_\tau$ and $\theta^*$ ((14)): Lemma 11 (Case 3, $\psi^3_\tau \le \alpha T$ ), Lemma 9 (Case 1) and Lemma 10 (Case 2).

Significance

Theorem 3, together with the lower bound of Theorem 4, settles the minimax regret of uncapacitated MNL assortment learning at $\Theta(\sqrt T)$ , independent of the number of products. The policy uses no estimate of the individual utilities, and its cost per period is one level-set offer, so it applies to catalogues where $N$ is large compared with $T$ . The structural lemmas on the revenue potential (Lemmas 1–4) are standard tools for MNL assortment problems and are reusable by other missions on static and dynamic assortment optimization. Lemma 8 is a MOSS-style concentration inequality whose confidence level grows with the sample size; it is the device that removes the $\sqrt{\log T}$ factor of the paper's baseline bound (Theorem 2).

The result is proved in the paper and is not presented as open; no machine-checked proof of any part of it is known. The platform has the MNL model, the UCB policy of Agrawal et al. (whose bound depends on $N$ ) and Hoeffding's inequality, but no level-set or trisection analysis. A formal proof would also check the paper's argument, whose printed slips are recorded in the scope section.

Difficulty

The regret concerns a stateful algorithm whose epochs end at random times: an inner iteration takes two periods while exploration is active and one afterwards, and the policy's internal state must be recomputed from the purchase history alone. The obvious argument fixes a confidence level $1/T^2$ , bounds each epoch's regret on the event that all confidence intervals hold, and sums a geometric series. That argument loses a $\sqrt{\log T}$ factor, and it is the paper's own Theorem 2. Removing the factor needs confidence levels that weaken as data accumulate. A failure is then no longer rare enough to be ignored, so the analysis has to track its cost. This is done by a recursion on conditional expected regrets across three cases (interval to the right of, containing, or to the left of $\theta^*$ ), in which a wrong decision in one epoch passes to another case with controlled probability. Within an epoch, the purchases made while exploring a level set must be shown to behave like i.i.d. samples with mean $F(y_\tau)$ , although the number of explorations is itself random.

Formalization scope

Model. The model is the published MNLBandit.UCB.Setting with every subset admissible: histories are sequences of choices in Option (Fin N) (none = no purchase), policies are deterministic functions of the past choices, and expectations are finite sums over histories. Items and periods are 0-based in Lean; epochs and inner iterations are as on the page.
Policy. The policy is defined exactly. Confidence radius $\sqrt{2\ln(8T/t)/t}$ (δ = 1/T in (12)); $n_\tau = \max(1, 8\lceil(y_\tau-x_\tau)^{-2}\ln(8T(y_\tau-x_\tau)^2)\rceil)$ ; trisection weights $2/3, 1/3$ ; the update $b \leftarrow y_\tau$ if and only if $u < y_\tau$ ; exploitation of $\mathcal L_{a_\tau}$ in every inner iteration; exploration only while $\ell \le y_\tau \le u$ .
Conventions.
- The $\max(1,\cdot)$ matters only for tiny $T$ , where the printed $n_\tau$ is $0$ .
- The empty assortment is allowed (§3 asks $S_t \neq \varnothing$ ; $R(\varnothing) = 0$ ).
- §3's $r_i > 0$ is relaxed to Theorem 3's $r_i \in [0,1]$ .
- $F$ is defined on all of $\mathbb R$ , and $F(\theta^+)$ is Mathlib's Function.rightLim.
- $\theta^*$ is defined as $F^*$ .
- $\psi$ is a ratio of finite sums and is $0$ on a conditioning event of probability $0$ .
- Every $O(\cdot)$ and $\lesssim$ is an existential constant chosen before all other quantities.
Added hypotheses. Lemma 2 assumes $F^* > 0$ , which its proof uses. Lemmas 9 and 10 and (S33) assume $T \ge 25$ and that epoch $\tau$ can start ( $\sum_{\tau'<\tau} n_{\tau'} < T$ ); without these, $\log(T\varepsilon^2)$ can be negative.
Repairs. Two printed statements are repaired.
- (S32) is stated with $\exp\{-n_\tau\Delta^2/2\}$ , which its printed justification gives; the printed $\exp\{-n_\tau\Delta^2\}$ fails on an explicit instance.
- Lemma 9 sums from $\tau' = \tau$ , as its proof does, with exponent $n_{\tau'}$ and the deterministic last epoch $\bar\tau(T)$ as upper limit.
Ruled out. Three formalizations would make the goal trivial, and none is admissible: a policy that receives $v$ (it could offer $S^*$ in every period); a constant $C_1$ that depends on $T$ , $N$ or the instance (the regret is at most $T$ ); and an abstract "trisection oracle" with assumed guarantees in place of the algorithm above.
Not included. Theorem 4 (the $\sqrt T/384$ lower bound) and its Lemmas 12–14 are not part of the mission, and neither are Theorem 2 and its Lemmas 5–7 (the baseline policy) or Proposition 1.
Contributions welcome. Lemmas 1–4 need only finite sums; Lemma 8 and (S32)/(S33) need Hoeffding's inequality and a union bound over sample sizes; the reduction of exploration purchases to i.i.d. samples is reusable for other level-set policies.

Selected references

X. Chen, Y. Wang, Y. Zhou, An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models, arXiv:1805.04785v2, 2019; Mathematics of Operations Research 46(4), 2021. https://arxiv.org/abs/1805.04785
S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5), 2019. https://arxiv.org/abs/1706.03880
X. Chen, Y. Wang, A note on tight lower bound for MNL-bandit assortment selection models, Operations Research Letters 46(5), 534–537, 2018.
P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic Assortment Optimization with a Multinomial Logit Choice Model and Capacity Constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
D. Sauré, A. Zeevi, Optimal Dynamic Assortment Planning with Demand Learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.2013.0429
K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
J.-Y. Audibert, S. Bubeck, Minimax Policies for Adversarial and Stochastic Bandits, COLT 2009.

17 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

A Classical Search Game in Discrete Locations: for any optimal hiding strategy, the searcher has an optimal strategy mixing at most n Gittins search sequences that each break all ties by one orderResearch Paper

Motivation

An object is hidden in one of $n$ boxes. Each search of box $i$ costs time $t_i$ , and if the object is there it is found with probability $q_i$ , independently of all earlier searches. When the searcher knows the probabilities $p_i$ with which the object was placed, the problem has a classical index solution. Norris (1962), Bram (1963), Blackwell (reported by Matula, 1964), Black (1965) and Ross (1983) showed that it is optimal to search, at every step, a box maximizing the current Gittins index $p_i(1-q_i)^{m_i}q_i/t_i$ , where $m_i$ is the number of failed searches of box $i$ so far. Ross also showed the converse: only such sequences are optimal.

The adversarial version replaces the known prior by a hider who chooses the box to maximize the expected time to detection, while the searcher minimizes it. Because overlook is possible, a pure search strategy must be an infinite sequence of boxes. This zero-sum search game goes back to Bram (1963) for unit search times, and it belongs to the search games against an evader in a stationary search space surveyed in Book 1 of Alpern and Gal (2003).

Timeline.

Bram (1963): for unit search times $t_i=1$ , an optimal search strategy exists, and optimal hiding strategies put positive probability on every box.
Roberts and Gittins (1978): for $n=2$ and unit search times, an optimal hiding strategy under certain conditions.
Gittins (1989), Proposition 8.5: for $n=2$ and $t_1=t_2=1$ , there is an optimal search strategy that randomizes between just two simple search sequences. The argument does not extend directly to $n\ge3$ .
Clarkson, Lin and Glazebrook (arXiv 2021; Mathematics of Operations Research, 2023): for arbitrary $n$ $n$ and arbitrary search times $t_i>0$ $t_{i} > 0$ :
- an optimal search strategy exists;
- for every optimal hiding strategy $p^*$ , some optimal search strategy mixes at most $n$ Gittins search sequences against $p^*$ , each of which breaks every tie by one and the same ordering.

Setting

There are $n$ boxes with search times $t_i>0$ and detection probabilities $q_i\in(0,1)$ .

Pure strategies. A pure strategy of the hider is a box. A pure strategy of the searcher is a search sequence $\xi=(\xi_0,\xi_1,\dots)\in\mathcal C=\{1,\dots,n\}^\infty$ . If the hider is in box $i$ , the expected time to detection is

V_i(\xi)=\sum_{m\ge0}t_{\xi_m}(1-q_i)^{N_i(m)}\in[0,\infty],

where $N_i(m)$ is the number of searches of box $i$ among the first $m$ .

Mixed strategies. A hiding strategy is a probability vector $p$ in the simplex $\mathcal P$ . A search strategy is a probability mass function $\eta$ on $\mathcal C$ , and $V_i(\eta)=\sum_\xi\eta(\xi)V_i(\xi)$ . Against a sequence $\xi$ , a hiding strategy $p$ earns the hider $\sum_ip_iV_i(\xi)$ .

Value and optimal strategies. The value is

v^*=\sup_{p\in\mathcal P}\ \inf_{\xi\in\mathcal C}\ \sum_{i=1}^np_iV_i(\xi).

A hiding strategy is optimal if it attains $v^*$ . A search strategy $\eta$ is optimal if $V_i(\eta)\le v^*$ for every box $i$ .

Gittins search sequences. $\mathcal C_p$ , the set of Gittins search sequences against $p$ , consists of the sequences that always search a box of maximal Gittins index.

Tie-breaking by one ordering. A permutation $\sigma\in S_n$ lists the boxes in order of preference. $\xi_{\sigma,p}$ is the Gittins search sequence against $p$ that, whenever several boxes have maximal index, searches the one $\sigma$ lists first. Then

\widehat{\mathcal C}_p=\{\xi_{\sigma,p}:\sigma\in S_n\}

has at most $n!$ elements, whereas $\mathcal C_p$ can be uncountable.

Formalization targets

Goal: Theorem 10 (p. 20)

For every optimal hiding strategy $p^*$ there is a search strategy $\eta^*$ with

V_i(\eta^*)\le v^*\quad(i=1,\dots,n),\qquad \operatorname{supp}\eta^*\subseteq F\subseteq\widehat{\mathcal C}_{p^*},\quad |F|\le n.

The goal fixes no constants. It asserts that an optimal search strategy exists, and that one can be found among mixtures of at most $n$ elements of $\widehat{\mathcal C}_{p^*}$ .

Milestones, in attack order

The Blackwell–Ross index theorem (§3.1, p. 6): $\mathcal C_p$ is exactly the set of pure strategies that optimally counter $p$ . This is already proved on the platform and is reused.
Proposition 2 (p. 7): optimal search strategies mix only sequences in $\bigcap_{p\in\mathcal P^*}\mathcal C_p$ .
Proposition 3 [1.] (p. 7): optimal hiding strategies are interior.
Lemma 15 (p. 41): $\mathcal S_p=\{V(\xi):\xi\in\mathcal C_p\}$ is closed for interior $p$ .
Lemmas 16 and 17 (pp. 42, 44): continuity of $x\mapsto V(\xi(r,x))$ at non-tie and at tie points.
Closedness of $\bar S(\epsilon)$ (Appendix A, pp. 40, 46–49).
Lemmas 4 and 5 (p. 10), on the perturbed game $G(\epsilon)$ .
Theorem 6 (p. 11): the goal with $\mathcal C_{p^*}$ in place of $\widehat{\mathcal C}_{p^*}$ .
Lemma 9 (p. 15): for interior $p$ , $\operatorname{Conv}(\mathcal S_p)=\operatorname{Conv}(\widehat{\mathcal S}_p)$ .

Significance

The result. In $G$ the searcher's pure strategy space is uncountable, so the existence of an optimal search strategy is not automatic. The standard theory of semi-finite games gives only $\epsilon$ -optimal strategies. Theorem 6 settles existence for general search times. Theorem 10 reduces the search for an optimal strategy to the finite set $\widehat{\mathcal C}_{p^*}$ .

The paper's computational section builds on this reduction. For interior $p$ , optimality of $p$ in $G$ is equivalent to optimality in the finite $n\times|\widehat{\mathcal C}_p|$ matrix game, which a linear program solves (Proposition 11). This is also the basis of the paper's bounding algorithm. Theorem 10 extends Gittins' two-box, unit-time Proposition 8.5 to any number of boxes and arbitrary search times.

Formalizing it. The results are proved on paper. To our knowledge none is machine-checked. The Blackwell–Ross index theorem is the only ingredient already proved on the platform. This mission formalizes:

the model, with payoffs that may be infinite;
the passage to the perturbed game $G(\epsilon)$ ;
the closedness of the payoff sets, which the paper proves by a delicate continuity analysis at tie points;
the convex-hull reduction from $\mathcal C_p$ to $\widehat{\mathcal C}_p$ .

Difficulty

The obvious route to existence is the $\mathcal S$ -game argument of Blackwell and Girshick: if the set of payoff vectors $\{V(\xi)\}$ is closed, the infimum over its convex hull is attained, and Carathéodory gives a mixture of at most $n$ points. For general search times no such closedness argument is available for $G$ itself: its payoff vectors are unbounded, and a sequence that neglects a box has an infinite coordinate. The paper therefore restricts to Gittins sequences against hiding strategies bounded away from the boundary, and adds pseudo-strategies that dominate everything near the boundary. Closedness of the resulting set rests on the continuity of $x\mapsto V(\xi(r,x))$ . This map is discontinuous at tie points in general and is continuous only along the cones $\mathcal P(p,\Sigma)$ (Lemma 17).

For Theorem 10, the natural idea is that every Gittins sequence is a mixture of the $\xi_{\sigma,p}$ . That is false pathwise. Lemma 9 replaces it with a statement about extreme points of $\operatorname{Conv}(\mathcal S_p)$ .

Formalization scope

Representation.

Boxes are Fin n and searches are 0-indexed (ξ : ℕ → Fin n).
Hiding strategies range over the whole stdSimplex ℝ (Fin n), boundary included.
Mixed search strategies are PMF (ℕ → Fin n).
Every payoff lives in $[0,\infty]$ (ℝ≥0∞).
The value is the hider's max-inf (1). Searcher optimality means $V_i(\eta)\le v^*$ for all $i$ , so Theorems 6 and 10 include the minimax equality the paper takes from Ferguson.
$\mathcal C_p$ and the hider's payoff reuse the published AllocationIndices search-problem definitions, with cost $t$ . Blackwell's theorem is the published AllocationIndices.search_index_optimal.

Tie-breaking.

A permutation is read as position ↦ box.
A tie-breaking rule $r\in\mathcal R$ is a sequence of permutations, and $r_k$ is used at search $k$ . The paper indexes $r$ by encountered tie instead. Both rule spaces generate exactly $\mathcal C_p$ , and constant rules give $\xi_{\sigma,p}$ in both.
Constructing $\xi_{\sigma,p}$ needs [NeZero n], which is implied by the simplex being nonempty.

Real vectors. $\mathcal S_p$ , $\widehat{\mathcal S}_p$ and $\bar S(\epsilon)$ are real vectors, obtained via toReal. They are used only for interior $p$ , where every coordinate is finite.

Trivializing readings, all excluded. None of the following is used:

real-valued payoffs, under which neglecting a box would cost $0$ ;
a hider optimality that does not attain the value;
a searcher optimality measured against the searcher's own infimum;
a $\widehat{\mathcal C}_p$ not built from the index rule (3);
a "mixture" with unbounded support (the support lies in a finite set of at most $n$ sequences);
a $G(\epsilon)$ without the pseudo-strategies $\zeta_i(\epsilon)$ paying $M_i(\epsilon)$ .

Infrastructure and contributions. A complete development needs:

Blackwell–Girshick's $\mathcal S$ -game theorem for closed payoff sets;
Carathéodory's theorem (Mathlib convexHull_eq_union) and Krein–Milman (Mathlib closure_convexHull_extremePoints);
compactness of $\mathcal R$ as a product of finite sets;
tail estimates for $V$ along Gittins sequences.

The $\mathcal S$ -game theorem and the semi-finite minimax theorem are reusable well beyond search games. Proofs of any milestone, and of these general tools as separate lemmas, are welcome.

Selected references

J. Clarkson, K. Y. Lin, K. D. Glazebrook, A Classical Search Game in Discrete Locations, Mathematics of Operations Research, 2023; preprint arXiv:2103.09310v1, 2021. https://arxiv.org/abs/2103.09310
D. Blackwell, M. A. Girshick, Theory of Games and Statistical Decisions, Wiley, 1954.
J. Bram, A 2-player N-region search game, IRM-31, Operations Evaluation Group, Center for Naval Analyses, 1963.
S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, 1983.
J. C. Gittins, Multi-armed Bandit Allocation Indices, Wiley, 1989.
D. M. Roberts, J. C. Gittins, The search for an intelligent evader: strategies for searcher and evader in the two-region problem, Naval Research Logistics Quarterly 25(1):95–106, 1978.
S. Alpern, S. Gal, The Theory of Search Games and Rendezvous, Kluwer, 2003.
T. S. Ferguson, A Course in Game Theory, World Scientific, 2020.
J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

14 thms3 active usersReviewed

Operations Research Optimization Statistics·Captain: mikedeng1

Offline Pricing and Demand Learning with Censored Data: a data-driven pricing problem is identifiable if and only if the optimistic and pessimistic prices coincideResearch Paper

Pricing from censored sales data

A retailer who sets a price for a product with limited inventory usually learns about demand from past sales. When the shelf runs empty, sales record the inventory level rather than the demand. Demand above the stock is lost and never observed. This demand censoring is pervasive in retail and inventory data, and it biases naive estimators of demand curves (Besbes and Muharremoglu, Management Science 2013; Ban, Operations Research 2020). Bu, Simchi-Levi and Wang (SSRN 3619625; Management Science, doi:10.1287/mnsc.2022.4382) ask a basic question about offline (historical) data. The retailer has censored sales at a few past prices and must choose a single new price. When can it, with enough data, guarantee near-optimal revenue no matter what the unobserved part of the demand distribution looks like? The paper answers this exactly, and gives an algorithm that achieves the guarantee whenever it is achievable.

Setting

The retailer has $y \ge 0$ units of inventory and chooses a price $p$ in a known interval $[\underline p, \bar p] \subset (0,\infty)$ . Demand is linear: $D(p) = \xi - bp$ , where the base demand $\xi$ is random with c.d.f. $F_\xi$ , and the price sensitivity $b$ lies in a known interval $[\underline b, \bar b] \subset (0,\infty)$ . Demand is nonnegative almost surely at every feasible price. Sales are $\min\{D(p), y\}$ , and under a c.d.f. $F$ of $\xi$ the expected revenue is $R_F(p) = p\,\mathbb E_F[\min\{\xi - bp, y\}]$ .

Offline data. $K \ge 2$ different historical prices $p_i \in [\underline p, \bar p]$ were used with inventories $y_i$ . At pair $i$ there are $N_i$ independent censored sales $S^j_i = \min\{\xi^j_i - bp_i,\ y_i\}$ . The data size is $N = \min_i N_i$ . A value of $\xi$ is observable only below the observable boundary $\lambda = \max_i\{y_i + bp_i\}$ . Write $\gamma = \mathbb P[\xi < \lambda]$ , which is assumed positive. Assumption 1 asks that, below $\lambda$ , $\xi$ is either discrete with finitely many atoms or has a density, with a slope or density lower bound $\underline g > 0$ .

Ambiguity set. No amount of censored data reveals $F_\xi$ on $[\lambda,\infty)$ . The set of distributions consistent with the data is $\mathcal F = \{F : F(x) = F_\xi(x)\ \forall x < \lambda\}$ . The optimistic and pessimistic revenues are $R_{\max}(p) = \max_{F\in\mathcal F} R_F(p)$ and $R_{\min}(p) = \min_{F\in\mathcal F} R_F(p)$ . Their largest maximizers on $[\underline p,\bar p]$ are the optimistic price $p^*_{\max}$ and the pessimistic price $p^*_{\min}$ . With $p^*_F$ the largest maximizer of $R_F$ , the worst-case revenue loss of a price $p$ is $\max_{F\in\mathcal F}\{R_F(p^*_F) - R_F(p)\}$ .

Identifiability. A data-driven algorithm maps the censored data and the public inputs ( $y$ , the two intervals, the pairs $(p_i, y_i)$ ) to a feasible price $p^{\mathcal A}$ . The problem is identifiable (Definition 1) if some algorithm satisfies $\lim_{N\to\infty}\mathbb P[\max_{F\in\mathcal F}\{R_F(p^*_F) - R_F(p^{\mathcal A})\} < \varepsilon] = 1$ for every $\varepsilon > 0$ .

Formalization targets

Goal: Theorem 1

The problem is identifiable if and only if

p^*_{\max} = p^*_{\min}.

The Lean goal states this in three parts, for every instance satisfying the standing assumptions:

the paper's algorithm D2ACD (Algorithm 1) always prices in $[\underline p,\bar p]$ , and if $p^*_{\max} = p^*_{\min}$ it satisfies the near-optimality limit;
if $p^*_{\max} \ne p^*_{\min}$ , every feasible price has worst-case loss at least

\frac{\gamma b}{(\sqrt\gamma+1)^2}\,(p^*_{\max} - p^*_{\min})^2 > 0;

identifiable $\iff p^*_{\max} = p^*_{\min}$ .

Milestones

Structure of the robust revenues. Concavity and projection (Proposition 1); closed forms of $R_{\max}$ , $R_{\min}$ with the extremal distributions (Proposition 2); $p^*_{\min} \le p^*_F \le p^*_{\max}$ (Proposition 3); the worst-case loss equals $\max\{R_{\max}(p^*_{\max}) - R_{\max}(p),\ R_{\min}(p^*_{\min}) - R_{\min}(p)\}$ (Proposition 7); the lower bound on the minimax loss $\Delta$ (Proposition 6).
Concentration. Hoeffding (Lemma A.1, already proved on the platform), Dvoretzky–Kiefer–Wolfowitz for an arbitrary c.d.f. (Lemma A.2), and a uniform deviation bound for bounded monotone functions (Lemma A.3).
Analysis of D2ACD. Consistency of the sensitivity estimate $\hat b$ (Lemma 1), of the empirical revenue (Lemma D.1) and of the empirical uncensored fraction (Lemma D.2). Uniform convergence of the empirical robust revenues (Lemma 2). The sample-complexity bound $N(\varepsilon,\delta) = C\varepsilon^{-2}\log(8K/\delta)$ with the paper's explicit constant $C$ (Theorem 2).

Significance

Theorem 1 separates censored-data pricing problems into two classes. In identifiable ones, more data eventually yields near-optimal prices. In the others, a positive loss persists however large the sample, and the right benchmark is the minimax loss $\Delta$ . The criterion is checkable in terms of two robust optimization problems, the maximax and the maximin. The constructive half comes with an algorithm that uses only observable data and has sample complexity $O(\varepsilon^{-2}\log(1/\delta))$ , matching data-driven newsvendor results without censoring (Levi, Perakis and Uichanco, Operations Research 2015).

The results are proved in the paper. None of them, and none of the model, is formalized. The mission formalizes the model, the ambiguity set, the algorithm and the full chain of the proof. It includes two concentration inequalities not yet available in Lean in the needed form: DKW with Massart's constant for distributions with atoms, and a uniform bound over monotone function classes.

Difficulty

The algorithm sees only the censored data. A proof that silently uses $b$ or $F_\xi$ to pick the price does not establish the theorem. The obvious estimator of $b$ , least squares on observed sales, is biased by censoring. D2ACD instead regresses empirical quantiles at the level $\hat\gamma_{\min}$ , below which the data are uncensored. Its analysis needs a lower bound on the slope of the c.d.f. (Assumption 1), and a uniform-in-price comparison of piecewise empirical revenues whose breakpoint $\hat{\tilde p}$ is itself random. On the other side, the lower bound requires the exact extremal distributions in $\mathcal F$ . The optimistic one sends the unobserved mass beyond every relevant demand level. The pessimistic one puts it at the boundary $\lambda$ .

Formalization scope

Representation. c.d.f.s are probability measures on $\mathbb R$ . $F \in \mathcal F$ means agreement with $F_\xi$ on every half-line $(-\infty, x]$ , $x < \lambda$ , so an atom at $\lambda$ is allowed. $R_{\max}$ , $R_{\min}$ , the worst-case loss and $\Delta$ are defined as suprema and infima. Their attainment is part of the milestones, so no statement is true through a junk value. " $\max\{\arg\max\}$ " is the supremum of the set of maximizers. The data are base-demand samples $\xi^j_i$ under the product law, mapped to censored sales. An algorithm is a function of the sample sizes and the censored sales for fixed public inputs. Failure probabilities are outer measures. The limit $N \to \infty$ is over all sample-size vectors with $\min_i N_i \to \infty$ .

Standing assumptions and disclosed choices. The data equation is $S^j_i = \min\{\xi^j_i - bp_i, y_i\}$ ; the page drops $b$ once. The continuous branch of Assumption 1 bounds the density on $[\ell, \lambda)$ , with $\ell$ a lower bound of the support. The printed $[0,\lambda)$ contradicts nonnegative demand together with $\gamma > 0$ . The historical prices are pairwise different, as the text says. The finite-sample statements (Lemmas 1, 2, Theorem 2) are made on the data assumption $\hat\gamma_i > 0$ for all $i$ , as on p. 10; the goal is not. In D2ACD, $\hat b$ is the clamp of the least-squares slope to $[\underline b, \bar b]$ , which is the arg min of line 9. Ties go to the largest price and the least index. The output is $\underline p$ when some sample is empty.

Trivializing readings ruled out. Definition 1 fixes the instance before asking for an algorithm, so a constant algorithm returning $p^*_{\max}$ witnesses the bare equivalence. For that reason the goal names D2ACD, a definition taking only the public inputs and the censored sales, and states the quantitative lower bound for the other direction. Two sanity instances, one discrete and one uniform, satisfy every standing assumption, so the hypotheses are not vacuous.

Contributions welcome. Proofs of any milestone. The concentration lemmas A.2 and A.3 are reusable well beyond this mission. Propositions 1–3, 6 and 7 are deterministic convex-analysis arguments about the two robust revenue curves and are a natural starting point.

Selected references

J. Bu, D. Simchi-Levi, L. Wang, Offline Pricing and Demand Learning with Censored Data, Management Science, 2022 (SSRN 3619625, PDF of 2021-08-23). https://ssrn.com/abstract=3619625, https://doi.org/10.1287/mnsc.2022.4382
P. Massart, The tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, Annals of Probability 18(3), 1990. https://doi.org/10.1214/aop/1176990746
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
O. Besbes, A. Muharremoglu, On implications of demand censoring in the newsvendor problem, Management Science 59(6), 1407–1424, 2013.
G.-Y. Ban, Confidence intervals for data-driven inventory policies with demand censoring, Operations Research 68(2), 309–326, 2020.
R. Levi, G. Perakis, J. Uichanco, The data-driven newsvendor problem: new bounds and insights, Operations Research 63(6), 2015.

17 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

The Circlet Inequalities: A New, Circulant-Based, Facet-Defining Inequality for the TSP: The Circlet Inequality Is Valid and Facet-Defining for the Symmetric TSP Polytope When 4 Divides nResearch Paper

Motivation

The symmetric traveling salesman polytope $STSP(n)$ is the convex hull of the incidence vectors of all Hamiltonian cycles of the complete graph $K_n$ . Minimizing a linear cost over it is the traveling salesman problem, and polyhedral methods for the TSP (cutting planes, branch and cut, LP relaxations and their integrality gaps) depend on linear inequalities that are valid for $STSP(n)$ and, ideally, define its facets. Known facet classes include the comb, clique-tree, path and crown inequalities; Naddef's survey (Naddef 2007) collects them.

Circulant TSP instances are those whose edge costs depend only on the edge's length around a circle of $n$ equally spaced cities. Gutekunst and Williamson (SIAM J. Discrete Math. 2019) showed that the subtour LP has integrality gap exactly $2$ on circulant instances; the witnessing family of LP solutions is cut off by several known facets, but not robustly under small modifications. They conjectured an inequality, now called the circlet inequality, that would cut off the whole family. The paper of this mission (arXiv:2012.12363v1) proves that conjecture and shows the inequality is facet defining when $4\mid n$ . Its coefficients are themselves circulant, a property shared among classical facets only by the crown inequalities of Naddef and Rinaldi (Math. Oper. Res. 1992).

Timeline. 2019: Gutekunst and Williamson characterize the subtour LP gap on circulant instances and conjecture Inequality (2). 2020: Gutekunst and Williamson prove validity (Theorem 3.1) and the facet property (Theorem 5.1) for $4\mid n$ , and compute the inequality's strength.

Setting

Fix $n$ cities $1,\dots,n$ , edges $E$ of $K_n$ , and $d=n/2$ . The length of the edge $\{i,j\}$ is

\ell_{i,j}=\min\{|i-j|,\ n-|i-j|\},

an integer in $\{1,\dots,d\}$ . For a vector $x\in\mathbb R^E$ and $1\le i\le d$ , $t_i=\sum_{\{s,t\}\in E:\ \ell_{s,t}=i}x_{s,t}$ is the total weight on edges of length $i$ . A Hamiltonian cycle $H$ visits every city once and returns; its incidence vector $\chi_H\in\{0,1\}^E$ marks its $n$ edges, and

STSP(n)=\operatorname{conv}\{\chi_H:\ H\text{ a Hamiltonian cycle on }K_n\}.

For $4\mid n$ the circlet coefficients are $c_i=i$ for odd $i$ and $c_i=d-i$ for even $i$ (for $n=12$ : $1,4,3,2,5,0$ ), and the circlet inequality is

\sum_{i=1}^{d} c_i t_i\ \ge\ n-2. \tag{2}

An inequality is valid for $STSP(n)$ if every point of $STSP(n)$ satisfies it, and facet defining if moreover the face $F=\{x\in STSP(n):\ \sum_i c_it_i(x)=n-2\}$ has $\dim F=\dim STSP(n)-1$ .

In the Lean development, cities are Fin n, a Hamiltonian cycle is an ordering π : Equiv.Perm (Fin n), its incidence vector is MetricTSP.tourVec π, STSP n is the convex hull of these vectors, lenCount n i x is $t_i$ , coeff n i is $c_i$ and circletForm n x is $\sum_{i=1}^{d}c_it_i$ .

Formalization targets

Goal: Theorem 5.1

For every positive $n$ with $4\mid n$ :

\forall x\in STSP(n):\ \sum_{i=1}^{d}c_it_i(x)\ge n-2,\qquad\text{and}\qquad STSP(n)\cap\Big\{\textstyle\sum_{i=1}^{d}c_it_i=n-2\Big\}\ \text{is a facet of } STSP(n).

Validity: Theorem 3.1

Every Hamiltonian cycle on $n$ cities, $4\mid n$ , satisfies (2). The proof is by minimal counterexample and runs through the milestones Claim 3.2 (the base case $n=4$ ), Lemma 3.3 (a violating cycle has $t_1+2t_d>n+2$ ), Lemma 3.4 (a minimal violating cycle contains none of three local edge patterns), and the window count $t_1+2t_d=T_1+\dots+T_d$ with $T_u\le 2$ .

The technical lemma: contraction

Lemma 3.4 is proved by contracting four vertices of a cycle containing one of the patterns and showing the cost drops by at least $4$ : Claims 4.1 and 4.2 (symmetries), Proposition 4.3 (surviving edges never get more expensive), Propositions 4.4 and 4.5 (the five contracted edges), and the resulting contraction step.

The facet property

The dimension $\dim STSP(n)=n(n-3)/2$ (cited on p. 19 from Naddef and Rinaldi, Theorem 3.7), and a family of $n(n-3)/2$ tight Hamiltonian cycles with linearly independent incidence vectors.

Significance

The circlet inequality is a facet of $STSP(n)$ whose coefficients depend only on edge length, so it is invariant under rotation of the city labels. It resolves the circulant TSP conjecture of Gutekunst and Williamson and removes from the subtour LP every member of the canonical family of solutions that witnesses the integrality gap $2$ on circulant instances, a class of TSP instances for which relatively little is known. Since any relabelling of the cities gives another valid inequality, it supplies on the order of $n!$ facets of $STSP(n)$ . The validity proof also gives a self-contained example of a minimal-counterexample argument by vertex contraction, a technique common in polyhedral combinatorics.

The result is proved in the paper; it has not been formalized. This mission produces machine-checked statements of the validity theorem, the facet theorem, and every intermediate result their proofs use, together with a reusable formal model of $STSP(n)$ , edge lengths on a cycle, and facets of polytopes built from tour incidence vectors. The dimension of $STSP(n)$ is a classical cited result that, to the best of current knowledge, has no formal proof either; it is included as a target in its own right.

Difficulty

Validity is not a local statement. A Hamiltonian cycle may use edges of any length, and the coefficients alternate between $i$ and $d-i$ with parity, so no edge-by-edge or degree-by-degree bound works: the inequality is tight on cycles that mix lengths $1$ , $d$ and one other length. The paper's argument needs the global structure of the cycle twice, once to rule out the patterns of Figure 4 in a minimal counterexample (where a parity argument on a four-group quotient graph handles the hardest equality case of Proposition 4.5) and once to count windows. The contraction step requires checking that the contracted object is again a Hamiltonian cycle and tracking costs on two different vertex sets with different moduli $n$ and $n-4$ .

For the facet half, exhibiting the tight tours is explicit, but proving the linear independence of $n(n-3)/2$ incidence vectors for all $n$ and proving the dimension of $STSP(n)$ are substantial linear-algebra arguments. The paper's own justification of independence for the first family is inaccurate (a length- $d$ edge is shared by two rotations), so a correct argument has to be supplied.

Formalization scope

Cities are Fin n with 0-based labels; lengths and costs depend only on label differences, so the shift from $1,\dots,n$ changes nothing. The contraction results (Propositions 4.3–4.5, the contraction step) use the paper's 1-based labels in ℕ, with integer lengths and costs, and refer to a cycle's edges through the label of each vertex ( $v\mapsto v+1$ ).
$STSP(n)$ lives in Fin n → Fin n → ℝ (ordered pairs); the incidence vector is symmetric with zero diagonal, and affine dimension is the same as in $\mathbb R^E$ . $t_i$ counts each unordered edge once.
"Facet" is the published Disjunctive.Polarity.IsFacet (extreme, nonempty, dimension one less), and the goal conjoins validity, since a face of codimension one is also cut out by the reversed inequality.
Added hypotheses: $0<n$ throughout (for $n=0$ the polytope is a point and the facet claim fails); $n\ge 8$ in the contraction step and in $T_u\le 2$ , where the paper derives it from Claim 3.2. "Feasible TSP input" in Theorem 3.1 is a Hamiltonian cycle; validity on all of $STSP(n)$ is part of the goal. Claims 4.1 and 4.2, which the paper states about counterexamples, are stated in the stronger form their proofs give (a relabelled cycle with the same circlet value).
The goal cannot be trivialized: validity is asserted on the whole polytope, the face is required nonempty, and its dimension is compared with that of $STSP(n)$ , which is itself pinned down by a separate milestone. Lemmas 3.3 and 3.4 have hypotheses that no cycle satisfies once Theorem 3.1 holds; they are stated as printed, and the contraction step carries their non-vacuous content for an explicit contracted vector.
Infrastructure needed: incidence vectors of Hamiltonian cycles and relabellings of them, contraction of a cycle, affine dimension of convex hulls of finite point sets. The model of $STSP(n)$ and the dimension result are reusable for any facet result on the TSP polytope. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

S. C. Gutekunst, D. P. Williamson, The Circlet Inequalities: A New, Circulant-Based, Facet-Defining Inequality for the TSP, arXiv:2012.12363v1, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2012.12363
S. C. Gutekunst, D. P. Williamson, Characterizing the integrality gap of the subtour LP for the circulant traveling salesman problem, SIAM Journal on Discrete Mathematics 33(4) (2019) 2452–2478. https://doi.org/10.1137/18M1167784
D. Naddef, G. Rinaldi, The crown inequalities for the symmetric traveling salesman polytope, Mathematics of Operations Research 17(2) (1992) 308–326. https://doi.org/10.1287/moor.17.2.308
D. Naddef, Polyhedral theory and branch-and-cut algorithms for the symmetric TSP, in: G. Gutin, A. P. Punnen (eds.), The Traveling Salesman Problem and its Variations, Springer, 2007, 29–116. https://doi.org/10.1007/0-306-48213-4_2

19 thms3 active usersReviewed

Completed

Group Theory Quantum Information Theoretical Computer Science·Captain: mikedeng1

The Solovay-Kitaev algorithm: every gate in SU(d) is ε-approximated by a sequence of O(log^{ln 5/ln(3/2)}(1/ε)) gates from any instruction setResearch Paper

Motivation

A quantum computer executes a fixed, finite instruction set of gates, while quantum algorithms are written with arbitrary gates. Every algorithm must therefore be compiled: each gate $U$ is replaced by a sequence of available instructions whose product approximates $U$ . If an accuracy $\delta$ required sequences of length $O(1/\delta)$ , compiling an $m$ -gate algorithm to overall accuracy $\epsilon$ would cost $O(m^2/\epsilon)$ instructions, which would erase quadratic speed-ups such as Grover's search. The Solovay-Kitaev theorem says the cost is only polylogarithmic in $1/\epsilon$ , for every instruction set, and the Solovay-Kitaev algorithm finds the sequences efficiently. It is the standard justification for treating the choice of a universal gate set as immaterial in quantum complexity theory.

Timeline. Solovay announced the theorem for $SU(2)$ in 1995 on an email list, without a subsequent paper. Kitaev outlined a proof for $SU(d)$ in 1997 (Kitaev 1997), with an algorithm. Nielsen and Chuang's textbook (2000, Appendix 3) gave a detailed proof, and Kitaev, Shen and Vyalyi (2002) gave two algorithmic variants, one with sequence length $O(\log^{3+\delta}(1/\epsilon))$ . Dawson and Nielsen (2005, arXiv:quant-ph/0505030) gave the self-contained pedagogical account of the theorem and algorithm, for qubits and qudits, which this mission formalizes; their algorithm yields length $O(\log^{\ln 5/\ln(3/2)}(1/\epsilon)) \approx O(\log^{3.97}(1/\epsilon))$ .

Setting

Fix a dimension $d$ . $SU(d)$ is the group of $d \times d$ complex unitary matrices of determinant $1$ , and $U^\dagger = U^{-1}$ is the adjoint. The distance between gates is the operator norm of their difference,

d(U, V) = \|U - V\| = \sup_{\|\psi\| = 1} \|(U - V)\psi\| .

A sequence $S = g_1, \dots, g_m$ of gates also denotes the unitary $g_1 g_2 \cdots g_m$ , and $|S| = m$ is its length; $S$ is an $\epsilon$ -approximation to $U$ when $d(U, S) < \epsilon$ .

An instruction set for $SU(d)$ (Definition 1) is a finite set $\mathcal G \subseteq SU(d)$ such that

$g^\dagger \in \mathcal G$ for every $g \in \mathcal G$ , and
$\mathcal G$ is universal: for every $U \in SU(d)$ and every $\epsilon > 0$ some sequence of gates from $\mathcal G$ is an $\epsilon$ -approximation to $U$ .

The Solovay-Kitaev algorithm $\mathrm{SK}(U, n)$ is a recursion of depth $n$ . At depth $0$ it returns a stored basic approximation of bounded length $l_0$ . At depth $n$ it computes $U_{n-1} = \mathrm{SK}(U, n-1)$ , decomposes $\Delta = U U_{n-1}^\dagger$ approximately as a balanced group commutator $VWV^\dagger W^\dagger$ with $V, W$ close to the identity, and returns the concatenation $V_{n-1} W_{n-1} V_{n-1}^\dagger W_{n-1}^\dagger U_{n-1}$ of five sequences computed at depth $n - 1$ . The accuracies satisfy $\epsilon_n = c\,\epsilon_{n-1}^{3/2}$ and the lengths $l_n = 5\, l_{n-1}$ .

Formalization targets

Goal: Theorem 1 with the exponent of Eq. (8)

For every instruction set $\mathcal G$ for $SU(d)$ there is $C > 0$ such that for every $\epsilon > 0$ and every $U \in SU(d)$ some sequence $S$ of gates from $\mathcal G$ satisfies

|S| \le C \ln\!\Big(2 + \frac1\epsilon\Big)^{\ln 5/\ln(3/2)} \quad\text{and}\quad d(U, S) < \epsilon .

Theorem 1 of the paper asserts length $O(\log^c(1/\epsilon))$ for some $c$ ; the goal fixes $c = \ln 5/\ln(3/2)$ , the exponent the paper's algorithm attains (Eq. (8), and §5.1 for qudits). $C$ is left unspecified, as in the paper.

Milestones

In attack order: the inverse-sequence fact (p. 3); $d(I, e^{iH}) \le \|H\|$ (p. 3); the base case, bounded-length $\epsilon_0$ -approximations (p. 5); Lemma 1, the error of an approximated group commutator (Eq. (14)); Lemma 2, a traceless Hermitian $H$ is a commutator $[F, G] = iH$ with $\|F\|, \|G\| \le d^{1/4}((d-1)/2)^{1/2}\sqrt{\|H\|}$ ; Lemma 3, $d(e^{iF}e^{iG}e^{-iF}e^{-iG}, e^{i \cdot i[F,G]}) \le c_1\delta^3$ ; the logarithm of a gate near the identity (p. 12); the balanced approximate commutator in $SU(d)$ , Eq. (33); the recursion invariant of the algorithm (Eqs. (1)–(2), (15), (21)–(22)); the closed form of $\epsilon_n$ (Eq. (4)); and the depth/length trade-off (Eqs. (7)–(8)).

Significance

The result. Theorem 1 makes universality quantitative. Any two universal instruction sets simulate each other with polylogarithmic overhead, so the class of efficiently computable quantum functions does not depend on the gate set, and fault-tolerant architectures may restrict themselves to a small set of protected gates. The algorithm turns the existence statement into a compiler with polylogarithmic running time.

Formalizing it. The theorem is proved, and the paper's argument is complete apart from constants it declares "tedious … easy to supply". The paper is not machine-checked, and the platform has no $SU(d)$ version: an open goal from Childs's lecture notes (QAlgorithms.Childs.solovayKitaev) concerns circuits of one- and two-qubit gates up to global phase with an unspecified exponent, and proved items cover $SU(2)$ commutator estimates only. This mission produces the qudit statement with the explicit exponent $\ln 5/\ln(3/2)$ , the commutator estimates of Lemmas 1–3 in arbitrary dimension, and an explicit model of the recursion. The paper's constants are only approximate ( $c_1 \approx 4$ , $c_{\mathrm{approx}} \approx 8c_{gc''}$ ); rigorous values are a welcome by-product.

Difficulty

The obvious argument, approximating $U$ with ever longer sequences from a dense subgroup, gives no rate at all: density says nothing about how long sequences must be. The rate comes from an error-cancellation effect: if $V, W$ are at distance $O(\sqrt\epsilon)$ from the identity and are approximated to accuracy $\epsilon$ , their group commutator is approximated to accuracy $O(\epsilon^{3/2})$ , better than the inputs (Lemma 1). Making this work needs (i) a decomposition of every gate close to the identity as an approximate balanced commutator in $SU(d)$ , which requires a matrix logarithm, the commutator representation of traceless Hermitian matrices (Lemma 2), and a third-order Baker-Campbell-Hausdorff estimate (Lemma 3); and (ii) a uniform base case, which needs compactness of $SU(d)$ to turn pointwise universality into a single length bound $l_0$ . The paper's derivation of Eq. (33) also contains a sign slip: with $[F, G] = iH$ the commutator approximates $U^\dagger$ instead of $U$ , which a formal proof must repair.

Formalization scope

Gates are elements of Matrix.specialUnitaryGroup (Fin d) ℂ; Lemma 1 is about matrices in the unitary group. The distance is the $\ell^2$ operator norm QAlgorithms.specNorm from the published definition QAlgorithms_Defs_Basic, never Mathlib's entrywise matrix norm. Sequences are lists, their unitary is the list product $g_1 \cdots g_m$ , and the inverse sequence is the reversed list of inverses. Instruction sets are Finsets closed under inverses; universality is the paper's own gloss of Definition 1, part 3 ("for every $U$ and $\epsilon > 0$ a product of gates from $\mathcal G$ is an $\epsilon$ -approximation"). The exponential is NormedSpace.exp on complex matrices. The algorithm is a Lean function of two routines: a lookup basic and a decomposition gc, indexed by the recursion level because GC-Approx-Decompose's guarantee is relative to the current accuracy.

Conventions and additions, all disclosed in the items: $\log(1/\epsilon)$ becomes $\ln(2 + 1/\epsilon)$ so that bounds are meaningful for every $\epsilon > 0$ (same $O$ -class); the paper's approximate constants ( $c_1$ , $c_{gc'}$ , $c_{gc''}$ , $c_{\mathrm{approx}}$ ) are existential and chosen before $\epsilon$ and $U$ ; the logarithm milestone adds $\operatorname{tr} H = 0$ (needed by Lemma 2) and $\|H\| < \pi$ (the proviso of p. 3); the identity $d(I, e^{iH}) = \max_E 2\sin(|E|/2)$ is not stated, since as printed it fails for $|E| > \pi$ .

Trivializing formalizations are ruled out: $\mathcal G$ must be closed under $\dagger$ and $S$ must consist of gates from $\mathcal G$ ; the constant $C$ is quantified before $\epsilon$ and $U$ , so it cannot depend on them; in the recursion invariant the base routine has a fixed length bound $l_0$ and the decomposition routine is constrained by the accuracy bounds, not assumed to be exact.

Running time (Eqs. (3), (6), (9), $O(\log^{2.71}(1/\epsilon))$ ) is out of scope: there is no machine model. Needed infrastructure: compactness of $SU(d)$ (Mathlib has no instance at this revision), a principal logarithm near the identity, operator-norm estimates for products and exponentials, and spectral facts about Hermitian matrices. The commutator and exponential estimates are reusable beyond this mission. Proofs of any milestone, and sharper constants, are welcome.

Selected references

C. M. Dawson and M. A. Nielsen, The Solovay-Kitaev algorithm, Quantum Information and Computation 6(1), 2006; arXiv:quant-ph/0505030v2, 2005. https://arxiv.org/abs/quant-ph/0505030
A. Yu. Kitaev, Quantum computations: algorithms and error correction, Russian Mathematical Surveys 52(6), 1997. https://doi.org/10.1070/RM1997v052n06ABEH002155
A. Yu. Kitaev, A. H. Shen and M. N. Vyalyi, Classical and Quantum Computation, AMS Graduate Studies in Mathematics 47, 2002. https://doi.org/10.1090/gsm/047
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Appendix 3. https://doi.org/10.1017/CBO9780511976667
A. M. Childs, Lecture Notes on Quantum Algorithms, University of Maryland, Chapter 2. https://www.cs.umd.edu/~amchilds/qa/

14 thms3 active usersReviewed

Completed

Combinatorics Discrete Geometry Linear Optimization+2·Captain: mikedeng1

Binary Extended Formulations and Sequential Convexification: Among All d-Hypercube Binarizations, the Logarithmic Binarization Has Minimum RankResearch Paper

Motivation

Mixed-integer programs often contain general integer variables $x \in \{0, \dots, k\}$ . A standard modelling device replaces such a variable by $d$ binary variables $y \in \{0,1\}^d$ linked to $x$ through a polytope, a binarization. Examples are the unary encoding, the "full" encoding with one indicator per value, and the logarithmic encoding $x = \sum_i 2^{i-1} y_i$ . Binarizations let cutting-plane and branching techniques built for 0/1 variables, such as lift-and-project and sequential convexification, act on general integer programs. Computational experience with such encodings is mixed. A logarithmic encoding uses the fewest variables, but it is not obvious that it should help or hurt the strength of the relaxation. Dash, Günlük and Hildebrand (Mathematical Programming 170, 2018) studied split cuts in binary extended formulations. Aprile, Conforti and Di Summa (arXiv:2106.00354, Mathematics of Operations Research, 2024) introduced a rank that measures how many convexification steps on the binary variables are needed to remove fractional values of $x$ , and compared binarizations by it.

The underlying operation is Balas's sequential convexification (Balas, Discrete Applied Mathematics 89, 1998; doi:10.1016/S0166-218X(98)00136-X): for a polytope $Q \subseteq [0,1]^h \times \mathbb R^{n-h}$ , replacing $Q$ by $\operatorname{conv}(\{x \in Q : x_i = 0\} \cup \{x \in Q : x_i = 1\})$ for $i = 1, \dots, h$ in turn yields the convex hull of the mixed 0/1 points.

Setting

A point is written $(x, y) \in \mathbb R \times \mathbb R^d$ . A polytope is the convex hull of finitely many points; $V(P)$ is its vertex set and two vertices are adjacent when the segment joining them is a face of $P$ . The skeleton $\operatorname{sk}(P)$ is the resulting graph.

For a polytope $Q$ with some coordinates $H$ restricted to $[0,1]$ , write $Q_{x_i} = \operatorname{conv}(\{x \in Q : x_i = 0\} \cup \{x \in Q : x_i = 1\})$ . The lift-and-project rank $\operatorname{lpr}(Q)$ is the least $k$ such that some indices $i_1, \dots, i_k \in H$ satisfy $((Q_{x_{i_1}})\dots)_{x_{i_k}} = \operatorname{conv}\{x \in Q : x_i \in \{0,1\}\ \forall i \in H\}$ .

A polytope $B \subseteq \mathbb R \times [0,1]^d$ is a binarization of $x$ in the range $\{0, \dots, k\}$ , $k \ge 1$ , if the $x$ -values of its points with $y \in \{0,1\}^d$ are exactly $\{0, \dots, k\}$ . For a number $f$ let $B(f) = \{(x,y) \in B : x = f\}$ . Given integers $\alpha_1, \dots, \alpha_\ell$ and points $\alpha_j < \bar x^j < \alpha_j + 1$ , the rank of $B$ is

\operatorname{rk}_B(\alpha_1, \dots, \alpha_\ell) = \operatorname{lpr}\Big(\operatorname{conv}\Big(\bigcup_{j} B(\bar x^j)\Big)\Big),

with the lift-and-project rank taken with respect to $y_1, \dots, y_d$ . It counts the $y$ -convexifications needed to cut off every point of $B$ whose $x$ -value lies strictly between $\alpha_j$ and $\alpha_j + 1$ for some $j$ .

$B$ is a $d$ -hypercube binarization if its vertices project onto $\{0,1\}^d$ in the $y$ -space and onto $\{0, \dots, 2^d - 1\}$ in the $x$ -space, so that the vertices of $B$ correspond one-to-one to those of the $d$ -cube, each with its own integer $x$ -value. The logarithmic binarization is

B^L(d) = \Big\{(x,y) \in \mathbb R \times [0,1]^d : x = \sum_{i=1}^d 2^{i-1} y_i\Big\}.

Formalization targets

Goal: Theorem 4.23

For every $d$ -hypercube binarization $B$ and all $\alpha_1, \dots, \alpha_\ell \in \{0, \dots, 2^d - 2\}$ ,

\operatorname{rk}_B(\alpha_1, \dots, \alpha_\ell) \ \ge\ \operatorname{rk}_{B^L}(\alpha_1, \dots, \alpha_\ell).

Milestones

The milestones follow the paper's development:

Balas's theorem (Theorem 2.1) and the set covering form of $\operatorname{lpr}$ (Observation 2.2).
The basic facts on binarizations: binary points are vertices (Observation 2.3), and the vertices of a fractional slice lie on edges crossing the slice (Lemma 4.3).
The set covering form of $\operatorname{rk}_B$ over the $\alpha_j$ -edges of $\operatorname{sk}(B)$ (Observation 4.8), and the comparison of $\operatorname{sk}(B)$ with $\operatorname{sk}(\pi_y(B))$ (Corollary 4.15).
For hypercube binarizations, the hypercube graph $G(B)$ and its cuts give

\operatorname{rk}_B(\alpha_1,\dots,\alpha_\ell) = d - f_B(\alpha_1,\dots,\alpha_\ell)\quad\text{(Lemma 4.18, Corollary 4.19)},

where $f_B$ counts coordinate directions in which no edge of $G(B)$ crosses any level $\alpha_j$ .

The arithmetic bound $2^{f_B(\alpha_1,\dots,\alpha_\ell)} \mid \alpha_j + 1$ (Lemma 4.20).
The exact value $f_{B^L}(\alpha_1,\dots,\alpha_\ell) = \max\{t : 2^t \mid \alpha_j + 1\ \forall j\}$ (Lemma 4.21, Corollary 4.22).

Significance

The theorem gives a precise sense in which the logarithmic encoding is the best among all encodings of an integer variable whose binarization has the combinatorics of a cube. It is not only the most compact one: it also requires the fewest sequential convexification steps on the binary variables to remove any prescribed family of fractional $x$ -intervals. Combined with Corollaries 4.19 and 4.22, it yields the explicit formula $\operatorname{rk}_{B^L}(\alpha_1,\dots,\alpha_\ell) = d - \max\{t : 2^t \mid \alpha_j + 1\ \forall j\}$ . In particular, $\operatorname{rk}_{B^L}(\alpha) = d$ for every even $\alpha$ . By Theorem 4.23 this extends to every hypercube binarization a result of Owen and Mehrotra (Operations Research 50, 2002) on the logarithmic encoding: convexifying all but one of the $y$ -variables of $B^L(d)$ does not ensure integrality of $x$ .

The result is proved in the paper. No machine-checked version exists. The mission formalizes the vertex-and-edge view of sequential convexification that the paper's proofs rest on: Balas's theorem for V-polytopes, lift-and-project rank as a hitting set, and the hypercube graph of a binarization with its cut structure. Mathlib has convex hulls, extreme points and extreme subsets, but no face lattice of polytopes, no skeleton graph and no hypercube graph. Platform results on Balas's theorem exist only for H-polyhedra with explicit bound rows.

Difficulty

The comparison is between an arbitrary hypercube binarization and a specific one. Direct computation of $\operatorname{lpr}$ for an arbitrary $B$ is not possible, because the polytope $\operatorname{conv}(\bigcup_j B(\bar x^j))$ depends on the whole edge structure of $B$ , and the skeleton of a hypercube binarization need not be the cube graph: it can contain extra edges. The step that has to be bridged is from the lift-and-project rank of a polytope to a statement about cuts in the hypercube graph $G(B)$ . That requires the vertex description of sequential convexification, the location of vertices of fractional slices on edges of $B$ , and the reduction from the skeleton $\operatorname{sk}(B)$ to the subgraph $G(B)$ . A natural first idea, comparing the polytopes $B$ and $B^L$ through an affine map, fails: a general hypercube binarization is not affine, and by Lemma 4.16 of the paper $B^L$ is, up to symmetry, the only affine one.

Formalization scope

The Lean development fixes the following conventions.

A point $(x, y)$ is p : Fin (d+1) → ℝ, with $x$ = p 0 and $y_i$ = p i.succ. Coordinates of $y$ are indexed from $0$ , so the weight $2^{i-1}$ of $B^L(d)$ is 2 ^ (i : ℕ).
Polytopes are convex hulls of finite sets, vertices are Set.extremePoints, and edges are the published Hirsch.Adj.
One convexification step and its iteration are the published Disjunctive.HigherDim.SplitConvexify and IteratedSplit.
lpr Q H is defined for any set H of 0/1 coordinates, with repetitions allowed in the sequence of convexified variables, as an sInf that Theorem 2.1 shows is attained.
The rank rk B xbar takes the fractional points $\bar x^j$ as an argument. Every statement about it quantifies over all admissible choices, and in the goal the choices for $B$ and $B^L$ are independent.
The range $\{0, \dots, 2^d - 2\}$ is written $\alpha_j + 2 \le 2^d$ , avoiding natural-number subtraction.
The cut condition $\delta(V^i_0) \cap \bigcup_j \delta(V_{\alpha_j}) \ne \emptyset$ is expressed through pairs of vertices of $B$ whose $y$ -parts differ exactly in component $i$ .
Corollary 4.22 adds $\ell \ge 1$ , since for $\ell = 0$ the maximum it names does not exist.
Only the second sentence of Observation 4.8 is formalized.

A formalization in which the rank of $B^L$ is a junk value $0$ (an empty set under sInf, or convexification over the wrong coordinates) would make the goal trivial. The definitions were checked against this: a sorry-free verification file proves $\operatorname{rk}_{B^L(1)}(0) = 1$ and that $B^L(1)$ is a $1$ -hypercube binarization.

A complete development needs:

the vertex description of $Q_{x_i}$ for V-polytopes;
faces and edges of polytopes, and the intersection of a polytope with a hyperplane;
the hypercube graph and its perfect matchings;
binary expansions and $2$ -adic valuations.

The polytope and edge results, including the vertex form of Balas's theorem, are reusable well beyond this paper. Contributions proving any milestone, or general lemmas on vertices of hyperplane sections and on projections of polytopes, are welcome.

Selected references

M. Aprile, M. Conforti, M. Di Summa, Binary extended formulations and sequential convexification, Mathematics of Operations Research, 2024; preprint arXiv:2106.00354v1. https://arxiv.org/abs/2106.00354
E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89, 3–44, 1998. https://doi.org/10.1016/S0166-218X(98)00136-X
S. Dash, O. Günlük, R. Hildebrand, Binary extended formulations of polyhedral mixed-integer sets, Mathematical Programming 170(1), 207–236, 2018.
J. H. Owen, S. Mehrotra, On the value of binary expansions for general mixed-integer linear programs, Operations Research 50(5), 810–819, 2002.
M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0

15 thms3 active usersReviewed

Combinatorics Operations Research Optimization·Captain: Shuze Chen

Submodular Maximization over Multiple Matroids via Generalized Exchange Properties: Polynomial approximation for monotone submodular maximizationResearch Paper

Motivation

Selecting a valuable subset subject to several simultaneous restrictions is a common combinatorial optimization problem. A facility may contribute less after nearby facilities have already been selected; a collection of observations may provide overlapping information. Such diminishing returns are captured by submodular objectives. Matroid constraints describe families of admissible selections that are closed under deletion and satisfy an exchange rule. Requiring a selection to satisfy several matroids permits overlapping restrictions on the same elements.

Lee, Sviridenko and Vondrák study this model with access to objective values and independence tests through oracles. Their main monotone guarantee is a polynomial approximation factor of $1/(k+\delta)$ for any fixed number $k\ge2$ of matroids and fixed $\delta>0$ . The source compares this with the earlier $1/(k+1)$ greedy guarantee. This mission formalizes the published monotone result and its supporting exchange statements, with the constants and algorithmic quantifiers intact (Introduction and Theorem 3.1).

Setting

The ground set is a finite set $N$ of $n$ elements. A submodular function assigns a real number $f(S)$ to every subset $S\subseteq N$ and satisfies

f(A\cup B)+f(A\cap B)\le f(A)+f(B).

All objective values in the faithful source statements are nonnegative. For the headline theorem the function is also nondecreasing: $A\subseteq B$ implies $f(A)\le f(B)$ . The empty set need not have value zero.

A matroid on $N$ is a family of independent sets containing the empty set, closed under taking subsets, and satisfying augmentation: a smaller independent set can gain an element from a larger independent set while remaining independent. There are $k$ such matroids, all on the same ground set. A set is common independent, or feasible, when it is independent in every one of them. The quantity $\mathrm{OPT}$ is the maximum of $f$ over feasible subsets. This maximum exists even when $N$ is empty, since there are finitely many subsets and the empty set is feasible.

An algorithm receives a value oracle for $f$ and one independence oracle for each matroid. A value query specifies a subset and returns its value; an independence query specifies a matroid and a subset and returns a yes-or-no answer. Real arithmetic and comparisons use the unit-cost oracle convention. No table of all objective values is supplied (Introduction, p. 795).

Formalization targets

The goal is the first sentence of Theorem 3.1. For each fixed $k\ge2$ and $\delta>0$ , there must exist one finite oracle program and polynomial constants, depending only on those fixed parameters, such that on every instance it halts and returns a feasible set $S$ with

f(S)\ge\frac{\mathrm{OPT}}{k+\delta}.

The time bound includes initialization, oracle queries, subset processing, unsuccessful searches, and output. It is not merely a bound on the number of improving moves (Theorem 3.1, p. 803).

The eleven supporting milestones follow the source's numbered statements. They cover perfect matching for equal-size independent sets; irreducible cycle covers; the independence consequence of a unique perfect matching; feasibility of irreducible cycles; feasible path and cycle covers; exact-cover addition; generalized Rota exchange; bounded-multiplicity exchange for independent sets; exact-cover removal; and exact and approximate local-search inequalities. The order follows the dependencies identified in §§1–3. The exact local-search bound is

\left(k+\frac1p\right)f(S)\ge f(S\cup C)+\left(k-1+\frac1p\right)f(S\cap C),

with a factor $1+\varepsilon$ on the left in the approximate version. Here $p\ge1$ is an integer, $C$ is any feasible set, and the objective may be nonmonotone (Lemmas 3.1–3.2).

Significance

The approximation theorem gives a quantitative guarantee for general matroid intersections with a submodular objective. Restricting the constraints to partition matroids, or proving that a good set exists without a polynomial computation, would lose part of the result. The supporting exchange statements also describe how independent sets can be related when individual exchanges cannot simply be combined across constraints (§§2–3).

The mathematics is a published result; this mission asks for machine-checked proofs of its formal statements. The submodularity predicate is reused from an existing published definition. Lemma 2.1 is anchored to an existing Open bijective exchange theorem through a contraction and graph interpretation, rather than posed again. Open means that its proof remains a target. The remaining statements and the operational oracle model are local drafts, and compiling their statements does not prove them.

Difficulty

A chain of individually feasible swaps need not give a feasible simultaneous exchange. The source's distinction between an arbitrary directed cycle and an irreducible one therefore matters. Feasibility of a path or cycle also includes every eligible subpath, not just the whole vertex-set swap. Losing either distinction changes the supporting exchange results (Definitions 2.1–2.2).

Polynomial computation is a separate obligation from local-optimum quality. Literal Figure 1 admits infeasible singleton initialization when loops are present and nontermination at zero value under its non-strict update test. These issues are recorded as findings about the displayed routine, while the existential headline retains all inputs. Two further findings identify missing witness properties and an invalid intermediate path-count estimate in the printed analysis; they do not establish falsity of the numbered local-search inequalities. Proofs must resolve those obligations without importing them as assumptions (pp. 802–803).

Formalization scope

Lean represents $N$ by Fin n, subsets by finite sets, objective values by real numbers, and matroids by Mathlib matroids with ground set equal to the whole finite type. Indexed families preserve repeated sets and repeated paths or cycles. Paths may consist of one vertex, cycles may have two vertices, and the cover multiplicity is $2^s$ , including $s=0$ . There is no looplessness, normalization, positive-optimum, or equal-cardinality restriction on the headline inputs.

The algorithmic goal uses a finite register-machine language whose only input-dependent operations are the two types of oracle queries. An explicit halt and a bound on the full execution cost are conclusions. Definitions contain neither an approximation guarantee nor an assumed polynomial stopping bound. The terminal predicate for Figure 1 uses strict inequality because the printed update uses greater-than-or-equal. Empty and zero-value inputs belong to the headline theorem even though the literal terminal predicate need not describe them.

The stronger linear-objective sentence of Theorem 3.1, the nonmonotone algorithm of Theorem 4.1, and the tightness examples in §5 are outside this mission. No optional variants are posed. Contributions needed here include the source theorem proofs, the exchange adapter, and the operational algorithm witness and its accounting.

Selected references

Jon Lee, Maxim Sviridenko and Jan Vondrák, Submodular Maximization over Multiple Matroids via Generalized Exchange Properties, Mathematics of Operations Research 35(4), 795–806, 2010. Published journal article. All result numbering and page references use this artifact; PDF pages 1–12 correspond to printed pages 795–806.

16 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: Shuze Chen

On the Existence of Pure Nash Equilibria in Weighted Congestion Games: Characterizing universal pure equilibrium existenceResearch Paper

Motivation

A system of users sharing resources may have no stable configuration: whenever the users settle on their choices, somebody may prefer to change. Weighted congestion games describe this question when different users place different demands on the resources they choose. Routing and scheduling provide examples, but the mathematical question here does not impose a particular network or scheduling structure. It asks which resource cost functions guarantee stability regardless of the finite population, its demands, and its feasible choices. Harks and Klimm give a classification of such functions in their 2012 paper, Theorem 5.1.

There are two distinct requirements. A stable configuration may exist even when some sequences of individually profitable moves cycle forever. Guaranteeing that every sequence terminates is generally stronger. The result identifies the continuous function classes for which these two universal guarantees coincide. The word “universal” matters: the assertion concerns all games generated by a class of costs, rather than the behavior of one specified game.

Setting

A weighted congestion game has a nonempty finite set of players $N$ and a nonempty finite set of facilities $F$ . Each player $i$ has a positive real demand $d_i$ and a nonempty finite collection $S_i$ of available strategies. A strategy is a subset of facilities; it may itself be empty. A profile $s$ chooses one strategy $s_i\in S_i$ for every player. Facility $f$ has a real-valued cost function $c_f$ defined on the nonnegative half-line. Its load and a player's private cost are

\ell_f(s)=\sum_{j:\,f\in s_j}d_j, \qquad \pi_i(s)=\sum_{f\in s_i}d_i c_f(\ell_f(s)).

Costs can have either sign, and the game model imposes no monotonicity. A pure Nash equilibrium is a profile $s$ satisfying $\pi_i(s)\le\pi_i(t_i,s_{-i})$ for every feasible unilateral change $t_i$ . A strict improvement lowers the deviating player's cost. The finite improvement property, or FIP, excludes improvement cycles, equivalently infinite improvement paths in this finite profile space. These conventions follow §2 and Definition 2.1.

For any set $C$ of cost functions, write $\mathcal G(C)$ for all such games with $c_f\in C$ at every facility. The class is consistent if every game in $\mathcal G(C)$ has a pure equilibrium, and FIP-consistent if every such game has the FIP. The class can be infinite or empty. In the results below, continuity always includes the endpoint zero. “Monotonic” means nondecreasing or nonincreasing, with the direction allowed to differ between functions.

Formalization targets

The goal is Theorem 5.1, p.427. For a set $C$ of continuous functions, the following are equivalent:

C\text{ is consistent};\qquad C\text{ is FIP-consistent};

\left[\forall c\in C\ \exists a_c,b_c\in\mathbb R\ \forall x\ge0,\ c(x)=a_cx+b_c\right] \quad\text{or}\quad \left[\exists\varphi\in\mathbb R\ \forall c\in C\ \exists a_c,b_c\in\mathbb R\ \forall x\ge0,\ c(x)=a_ce^{\varphi x}+b_c\right].

The exponential rate is shared by the entire class. No coefficient or rate is subject to a sign or nonzero restriction. The disjunction is inclusive, as printed in the theorem: classes of constant functions satisfy both alternatives.

Six source milestones support this target. Lemma 3.1 characterizes monotonicity by local right-hand comparisons with $c(0)$ . Lemma 3.2 supplies positive loads $0<x<y$ with either $c(y-x)<c(y)<c(x)$ or the reversed inequalities. Lemma 3.4 asserts monotonicity of the integer hull with offsets

\mathcal L_{\mathbb Z}(C)=\left\{x\mapsto\sum_{k=1}^{K}a_kc_k(x+b_k):a_k\in\mathbb Z,\ b_k\ge0,\ c_k\in C\right\}

under unrestricted consistency. Proposition 5.1 uses consistency for exactly three players to obtain monotonicity of both restricted hulls

\mathcal L_{\mathbb Z}^2(C)=\{a_1c_1+a_2c_2:a_1,a_2\in\mathbb Z,\ c_1,c_2\in C\},

\mathcal L_{\mathbb Z}^3(C)=\{x\mapsto a_1c(x)+a_2c(x+\delta):a_1,a_2\in\mathbb Z,\ c\in C,\ \delta>0\}.

Lemma 4.1 equates monotonicity of every integer combination of two continuous monotonic nonconstant functions with affine dependence between them. Lemma 5.1 equates monotonicity of the translated-function hull with each function being affine or exponential; its rate may depend on the function. The source locations are pp.422–427, §§3–5.

Significance

The classification separates structural guarantees from favorable individual instances. A class that fails the displayed alternatives cannot guarantee a pure equilibrium for every admissible game. Conversely, either alternative guarantees termination of strict improvement paths as well as equilibrium existence. This gives a precise answer to the unrestricted consistency question posed by Harks and Klimm, without imposing nonnegative or increasing costs.

The mathematical results are published results, not new conjectures. The remaining task is their machine-checked proof. This draft supplies compiled definitions and theorem statements; the seven theorem bodies remain proof targets. Its reusable components include the finite weighted game model, universal class predicates, and three different integer hulls. Published pure-equilibrium and improvement-path definitions are reused through their existing interfaces.

Difficulty

Monotonicity of individual resource costs does not settle the unrestricted problem. The selected statements impose conditions on combinations of functions, and those conditions distinguish the allowed class-wide structure. In particular, separate exponential representations for every member do not establish the common-rate alternative. Another logical obstacle is that an improvement cycle alone need not rule out an equilibrium elsewhere in a game's profile space. The source's nonexistence arguments must exclude every feasible equilibrium, not just exhibit cycling behavior. These distinctions are visible in §§3–5.

The findings accompanying this mission record local issues in printed proofs separately from their theorem statements. Such issues do not authorize stronger hypotheses or weaker conclusions in the faithful targets.

Formalization scope

Players and facilities are indexed by finite initial segments with strictly positive sizes. Strategies are finite subsets, and feasible strategies are subtypes of the specified nonempty families. This represents every finite game up to relabeling. Demands are strictly positive nonnegative reals, loads are finite sums, and private costs are ordinary reals. Payoff-maximizing published definitions receive the negative of the private cost. Finite profile spaces justify the equivalence of the published infinite-path FIP convention and the paper's cycle convention.

Consistency is defined by quantification over all admissible games; neither potentials nor the classification are included in admissibility. The hulls are constructed from integer coefficients and the stated translates, without selecting only their monotonic members. Continuity is imposed on the whole nonnegative domain. These choices exclude vacuous proxy models and restricted strategy classes. The empty class and constant functions remain included. No asymptotic estimates or extracted constants occur.

The twelve new definition items precede the seven theorem items, and the six numbered source milestones retain their provenance. No optional variant is posed. The independent two-player characterization and the network and singleton results are outside the mission. In particular, the correction notice on p.436 concerning finite rather than polynomial termination does not introduce an algorithmic target here. Contributions should complete the faithful statements and their needed supporting theory while preserving these conventions.

Selected references

Tobias Harks and Max Klimm, On the Existence of Pure Nash Equilibria in Weighted Congestion Games, Mathematics of Operations Research 37(3), 419–436, 2012. Published article and correction notice. All theorem numbering and quotations use this published artifact.

22 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: Shuze Chen

Stochastic Networks XIV: Large Deviations for Queues with Many SourcesTextbook

Motivation

Communication connections can demand bandwidth at rates that fluctuate over time. Reserving every connection's peak rate can leave substantial capacity unused, while reserving only its mean rate allows temporary overloads and queueing delays. Effective bandwidth provides a way to express the statistical cost of a source in terms that can be used in admission decisions. Chapter 6 of Kelly and Yudovina's Stochastic Networks develops this question first for an instantaneous aggregate load and then for a resource with a buffer.

The buffered model distinguishes the number of connections from the number of connection classes. The number of classes stays fixed while capacity, buffer size, and the number of connections all grow together. The object of interest is the exponential rate of the probability that the workload exceeds the buffer level. This rate measures rare overloads on a scale where ordinary convergence of probabilities to zero loses the relevant information.

Setting

A source increment $X_{ji}[a,b]$ is the work arriving during an interval from connection $i$ of class $j$ . The classes form a finite set $J$ . A source supplies nonnegative, additive increments, with no work on an interval of length zero. Each interval workload is a measurable real random variable. Different source processes are independent, copies within one class have the same process law, and increments have stationary distributions: the law of an interval's workload depends only on its duration. Independence between increments of one source is not required.

Let $n_j$ be the natural number of class- $j$ sources in a base system. At positive integer scale $N$ , there are $n_jN$ copies. The aggregate arrival is

S^N[a,b]=\sum_{j\in J}\sum_{i=1}^{n_jN}X_{ji}[a,b].

A server of capacity $CN$ , where $C>0$ , processes this work. Its infinite-past workload at time zero is the random variable

Q^N(0)=\sup_{t\ge0}\{S^N[-t,0]-CNt\}.

This is the construction in equation (6.4), not an independently chosen stationary queue size. It can be infinite. With a positive base buffer $B$ , the overflow probability is $L_N=P(Q^N(0)>BN)$ .

The logarithmic moment generating function of a class- $j$ increment is

M_j(s,t)=\log\mathbb E\exp(sX_{j1}[0,t]).

Exponential moments are assumed finite locally around zero for each finite duration, following the chapter's MGF convention; a larger tilt may have infinite expectation. The quantity $M_j(s,t)$ is the nonsingular expression for the product $st\alpha_j(s,t)$ in the book's effective-bandwidth formula.

Formalization targets

The goal is Theorem 6.10, printed page 145 of the supplied Lecture Notes PDF:

\lim_{N\to\infty}\frac1N\log L_N =\sup_{t\ge0}\inf_{s\ge0} \left[\sum_{j\in J}n_jM_j(s,t)-s(B+Ct)\right].

The supremum over duration remains outside the infimum over tilt. Both the continuous time domain and the infinite horizon are part of the target.

Three source milestones accompany the goal. Equation (6.1) asserts, for a measurable real random variable $Y$ and $s\ge0$ ,

P(Y>0)=\mathbb E\mathbf1_{\{Y>0\}}\le\mathbb E e^{sY},

including infinite exponential expectations. Theorem 6.2 asserts the exact logarithmic rate for an iid sum exceeding $nc$ . Its assumptions include a mean below $c$ , a positive probability of exceeding $c$ , local MGF finiteness, and an optimizing tilt in the interior of the finite-MGF domain. Exercise 6.9 gives both the two-sequence and finite-sum largest-term principles, with finite real rates and positive sequences. It makes no assertion about a countable sum.

Significance

The goal relates the statistical characteristics of individual connections to the overload behavior of a large system. It retains duration as a variable, allowing temporal dependence within a connection to affect the rate. A fixed-time tail probability alone does not describe the workload accumulated from an unlimited past. This distinction is central to the buffered model in Chapter 6.

The formal deliverable specifies the source family, its scaling, the workload construction, and the variational expression in one consistent setting. It also separates extended expectations from finite real expectations, so the meaning of a rare event does not change when its probability is zero. These definitions can support later work on queueing large deviations without requiring a finite-state Markov model.

The local theorem files are declarations to be proved, not completed proofs. A published proved Chernoff bound is retained as a reference for the integrable exponential case. The separately published open Cramér theorem assumes finiteness at every real tilt and a closed tail event; it is not substituted for the chapter's local-MGF, strict-tail statement.

Difficulty

The source explicitly gives only a sketch for Theorem 6.10. Fixed-time exponential limits do not by themselves determine the exponential rate of a sum over infinitely many times. Exercise 6.9 establishes a finite-sum result, so it cannot close this gap. The continuous-time workload also raises a measurability and time-discretization issue. Finding F1 records the missing justification with an explicit array of exponentially small terms whose count grows exponentially.

Finding F4 gives an explicit counterexample to the printed goal, even with positive buffer and mean load below capacity. Independent sources have uniformly random phases of a periodic arrival rate taking values 0, 1, and 2. Each source contributes at most one unit of net input over any interval, so with $B=C=1$ the strict overflow probability is zero at every scale. At duration 2, however, the maximum input 3 has probability $1/5$ , giving a finite variational value $-\log 5$ . The faithful goal is retained as printed and is expected to be disproved; no corrected variant is proposed. This is a failure of the fixed-time application of Cramér’s theorem at a support endpoint, separate from F1’s infinite-time gap.

Finding F2 concerns a different finite-sample step in the proof of Cramér's theorem: convergence of a tilted-window probability to one half does not ensure it is at least one half for a given sample size. The limiting theorem is retained. Neither finding is converted into an extra hypothesis or a variant. The goal carries no uniform temporal decay estimate, mixing assumption, or fixed-time large-deviation conclusion as an assumption.

Formalization scope

The formalization uses Mathlib probability measures, independence and equality-in-distribution predicates, nonnegative Lebesgue integrals, and extended-real order topology. Whole source paths are independent; this is stronger information than independence of one chosen interval's workloads. Natural multiplicities provide exactly $n_jN$ copies without rounding. Source indices begin at zero, and the asymptotic scale is represented as $N+1$ to avoid a zero denominator.

The queue supremum is over all nonnegative real times and takes values in EReal. Zero overflow probability has logarithm $-\infty$ ; infinite exponential expectation has logarithm $+\infty$ . The rate subtracts only finite linear terms. Zero multiplicities contribute zero, including when an unused source has an infinite MGF. At zero time or zero tilt, the log MGF is zero under the source assumptions. No division by $st$ is introduced.

Nonnegative additive increments use the usual half-open interval convention for endpoint arrivals. Measurability of the constructed workload is explicit, as required for the source's random-variable language. The model API also requires a probability measure and the relevant measurability when forming an overflow probability or exponential rate. Capacity and buffer are positive; F3 records a deterministic counterexample to extending the goal to zero buffer. Empty class sets and zero source counts remain permitted and give no overflow. For Exercise 6.9, positivity and a nonempty finite index set prevent default logarithms or maxima.

The goal must not be replaced by a finite-horizon queue, a deterministic drift inequality, or a hypothesis already asserting the desired asymptotic. No selected result uses an unspecified asymptotic constant, so there is no $O(\cdot)$ constant to instantiate. No variant is posed. The model module supplies real definition bodies; theorem statements expand the relevant formulas so standalone blind read-backs can inspect their meaning without resolving unpublished imports.

Selected references

F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. The pinned supplied artifact is titled Lecture Notes on Stochastic Networks: Chapter 6, printed pages 133–148, PDF pages 141–156. Correspondence with a particular published printing is not asserted. PDF SHA-256: ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.

6 thms3 active usersReviewed

Markov Chain Operations Research Probability+1·Captain: Shuze Chen

Stochastic Networks X: Stationary Open Migration Processes Under Time ReversalTextbook

Motivation

A network of queues records both how many customers occupy each location and how they move between locations. These are different kinds of information. A simple distribution for the occupancies at one time need not make the arrival streams simple, or make the queues independent over time. Open migration processes provide a setting in which the distinction can be studied precisely: customers can move through a finite network, enter from outside, and eventually leave. Chapter 2 of Kelly and Yudovina, Stochastic Networks develops their equilibrium structure.

The target concerns what an observer sees when a stationary network is run backwards. It says that the reversed random process belongs to the same class of models, even when its rates differ from those of the original process. This structural result is the setting for the source's subsequent conclusion about Poisson exit streams. The mission treats the process statement itself, keeping the distinction between an equilibrium rate calculation and a statement about a random trajectory.

Setting

There are a finite positive number $J$ of colonies. The state is $n=(n_1,\ldots,n_J)\in\mathbb N^J$ , where $n_j$ counts individuals at colony $j$ . There is no upper bound on an occupancy or on the total population. A transition can transfer an individual from colony $j$ to a different colony $k$ , remove one from the system at colony $j$ , or introduce one at colony $k$ .

The corresponding rates are $\lambda_{jk}\varphi_j(n_j)$ , $\mu_j\varphi_j(n_j)$ , and $\nu_k$ . The coefficients are nonnegative, $\lambda_{jj}=0$ , and the service factors satisfy $\varphi_j(0)=0$ and $\varphi_j(r)>0$ when $r\ge1$ . A departure requires an individual to be present. Immigration rates do not depend on the occupancy. These are the rates in Section 2.4 of the supplied source, printed pages 30–31.

A Markov process here consists of measurable random variables on one probability space, indexed by real time. Its conditional future distributions depend on the most recent state, through a time-homogeneous transition function. Transition rates are its right-hand infinitesimal transition probabilities. The standing assumptions from Section 1.1 are explicit: the process is irreducible, every state has a strictly positive finite exit rate, and sample paths have only finitely many jumps on each bounded interval. A stationary law is a positive normalized mass function $\pi$ giving the distribution at every time.

Formalization targets

The goal is Theorem 2.9, printed page 32 of the supplied PDF:

(n(t))_{t\in\mathbb R}\text{ stationary open migration} \quad\Longrightarrow\quad (n(-t))_{t\in\mathbb R}\text{ stationary open migration}.

Three milestones support this target. The partial-balance equations (2.3) and (2.4) are grouped as one milestone because one published theorem supplies both identities. They express equilibrium flux balance for transitions associated with a colony and with the outside world. Theorem 2.8 gives the normalized product-form distribution. With positive traffic parameters $\alpha_j$ satisfying

\alpha_j\left(\mu_j+\sum_k\lambda_{jk}\right) =\nu_j+\sum_k\alpha_k\lambda_{kj},

and finite normalizing sums $g_j$ , that distribution is

g_j=\sum_{m=0}^{\infty}\frac{\alpha_j^m}{\prod_{r=1}^m\varphi_j(r)}, \qquad \pi(n)=\prod_j g_j^{-1}\frac{\alpha_j^{n_j}}{\prod_{r=1}^{n_j}\varphi_j(r)}.

The third milestone, Proposition 1.1, concerns a stationary process on a countable state space. Its reversed process has the same stationary law and rates

q'(i,j)=\frac{\pi(j)q(j,i)}{\pi(i)}.

All three source statements are in Kelly and Yudovina, printed pages 16–17 and 31. The goal does not assume the product form, a reverse-process Markov property, or any of the reverse-rate identities.

Significance

The result identifies a class of stochastic networks that remains closed under reversal of stationary time. It does not assert detailed balance or equality of the original and reversed rates. It also does not infer independence of colony trajectories from independence of occupancies at one time; the source expressly distinguishes these statements on printed page 32. This separation is needed when interpreting the Poisson exit-stream consequence on printed page 33 of the source.

Published formal results already supply partial balance, normalized full balance, and the algebraic reversed migration rates. They are included as references rather than repeated as new theorem statements. The remaining formal targets concern the actual countable-state random processes: the Markov property of the reversal and preservation of the open-migration class. The new definition layer also provides finite-cylinder and nonexplosive-path specifications that can be reused for other countable-state stationary models.

Difficulty

A formula for a reversed rate matrix alone does not establish a theorem about the reversed process. The latter has finite-dimensional distributions, measurable coordinates, and nonexplosive paths. These must all be connected to the rates. The occupancy space is countably infinite even though the number of colonies is finite, so finite-state reversal theorems do not directly cover the goal. Similarly, assuming the candidate product distribution as part of the meaning of a stationary migration process would omit part of the source's claim. The definition deliberately leaves the stationary law unspecified.

Formalization scope

Colonies are represented by $\mathrm{Fin}\,J$ with $J>0$ ; states are unrestricted functions from this type to natural numbers. The zero-based colony labels differ only typographically from the source's labels $1,\ldots,J$ . The exact published migration operators and rate functions are reused. Their natural-number subtraction is protected by vanishing service factors at zero and a zero routing diagonal. Empty products equal one. Normalizing sums in the referenced product-form result use HasSum, so divergent real sums cannot acquire a default value and masquerade as finite normalizers.

The process definitions use probability measures, measurable coordinates, stochastic transition functions, finite-cylinder identities, and locally finite jump paths. Cylinder identities avoid conditioning by division at null events. The state space is countable with measurable singletons, and rate rows are explicitly summable. Positivity of the stationary mass function prevents a zero denominator in the reversal formula. Paths may take either adjacent value at a jump, accommodating the reversal of the right-continuous endpoint convention; isolated zero-duration spikes are excluded.

The goal must establish migration dynamics for the actual map $t\mapsto n(-t)$ ; an algebraic rate identity or independence at a single time is not a substitute. No asymptotic constants or failure probabilities occur in these targets. The infinite-colony extension, Poisson departure processes, Little's law, Bartlett's theorem, and renewal-reward variants are outside this mission. The findings register preserves observations about out-of-scope source displays, but no variant theorem is proposed. Contributions to the countable-state stochastic foundations and proofs of the two draft theorem statements are within scope.

Selected references

F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. The pinned supplied artifact is titled Lecture Notes on Stochastic Networks: Section 1.1 and Proposition 1.1, printed pages 13–17 (PDF 21–25); Section 2.4, equations (2.2)–(2.4), Theorems 2.8–2.9, printed pages 30–33 (PDF 38–41). Equivalence to a particular published printing is unverified. PDF SHA-256: ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.

9 thms3 active usersReviewed

Convex Optimization Operations Research Optimization+1·Captain: Shuze Chen

Robust Optimization IX: Safe Matrix Chance ConstraintsTextbook

Matrix inequalities under random perturbations

A semidefinite constraint asks whether a symmetric matrix is positive semidefinite: every vector must have a nonnegative quadratic form under that matrix. In optimization, its entries can depend on a decision and on uncertain inputs. Requiring the constraint for every possible input can be restrictive, especially when rare inputs have very large magnitude. A chance constraint instead requires the matrix inequality to hold with a specified probability. Chapter 10 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops safe approximations for such constraints, including conic quadratic constraints represented through symmetric matrices.

The question here is how a known probability of a moderate matrix perturbation can imply a much higher probability at a larger threshold. The chapter gives explicit answers for bounded independent perturbations and for independent standard normal perturbations. The goal is its Corollary 10.1.3, including both distributional cases and the possibility that the reference matrix is singular.

Symmetric matrices, probability, and the variance certificate

Let $A,B_1,\ldots,B_L$ be deterministic symmetric real $m\times m$ matrices, with $m,L\ge1$ . The random perturbation is

S=\sum_{\ell=1}^L\zeta_\ell B_\ell.

The Loewner order $C\preceq D$ means that $D-C$ is positive semidefinite. Thus the event $-tA\preceq S\preceq tA$ controls the perturbation simultaneously in every vector direction. For normalized matrices, $\|S\|$ denotes the operator norm for Euclidean vectors, rather than a maximum entry or a row-sum norm.

The random coordinates are measurable and independent on a probability space. Under assumption A.I they have zero means and satisfy $|\zeta_\ell|\le1$ almost surely. Under A.II each has the standard normal law $N(0,1)$ . The deterministic variance certificate is

\exists Y_1,\ldots,Y_L:\quad \begin{pmatrix}Y_\ell&B_\ell\\B_\ell&A\end{pmatrix}\succeq0 \quad(1\le\ell\le L),\qquad \sum_\ell Y_\ell\preceq A.

This is precisely system (10.1.13) in the source. A separate premise supplies the base probability

\Pr\{-\Upsilon A\preceq S\preceq\Upsilon A\}\ge\chi,

where $\Upsilon>0$ and $\chi>0$ . Neither this probability premise nor the certificate contains the amplified probability conclusion.

Write $T(t)=\Pr\{G>t\}$ for $G\sim N(0,1)$ , and $q$ for its inverse upper-tail quantile. The book writes these functions as Erf and ErfInv. Its Erf is a one-sided upper Gaussian tail; substituting the common analytic error function would change every Gaussian bound.

Formalization targets

The goal, Corollary 10.1.3, asserts that under A.I, for every $\Omega>\Upsilon$ ,

\Pr\{-\Omega A\preceq S\preceq\Omega A\} \ge1-\frac1\chi\exp\left(-\frac{(\Omega-\Upsilon)^2}{16}\right).

Under A.II and the additional condition $\chi>1/2$ , it asserts

\Pr\{-\Omega A\preceq S\preceq\Omega A\} \ge1-T\left(q(1-\chi)+(\Omega-\Upsilon) \max\{1,q(1-\chi)/\Upsilon\}\right).

Both conclusions retain the constants and strict threshold of equations (10.1.15)–(10.1.16).

Three source-numbered milestones support this goal. Theorem 10.1.1 concerns symmetric $B_\ell$ with $\sum B_\ell^2\preceq I$ and defines $\chi=\Pr\{\|S\|\le\Upsilon\}>0$ . Its bounded-case conclusion is

\Pr\{\|S\|>\Omega\}\le\chi^{-1}e^{-(\Omega-\Upsilon)^2/16},\qquad \Omega>\Upsilon.

Theorem B.5.1 concerns a closed convex set $Q\subseteq\mathbb R^m$ with standard Gaussian mass at least $\chi>1/2$ . It asserts that $Q$ contains the centered ball of radius $q(1-\chi)>0$ . If it contains a centered ball of radius $r\ge q(1-\chi)$ , then for $\alpha\ge1$ ,

\Pr\{G\notin\alpha Q\}\le T(q(1-\chi)+(\alpha-1)r) \le T(\alpha q(1-\chi))\le\tfrac12e^{-\alpha^2q(1-\chi)^2/2}.

Its further conclusion covers centered Gaussians with arbitrary positive semidefinite covariance: an outside probability at most $\delta<1/2$ becomes at most $T(\alpha q(\delta))\le\tfrac12e^{-\alpha^2q(\delta)^2/2}$ after dilation. This clause includes degenerate covariance matrices.

Theorem 10.1.2 is the normalized Gaussian matrix milestone. With the same variance normalization and exact base mass $\chi>1/2$ , it states, now for $\Omega\ge\Upsilon$ ,

\Pr\{\|S\|>\Omega\}\le T\left(q(1-\chi)+(\Omega-\Upsilon)\max\{1,\Upsilon^{-1}q(1-\chi)\}\right) \le e^{-\Omega^2\Upsilon^{-2}q(1-\chi)^2/2}.

What a formal development supplies

The chapter’s bounds connect a matrix certificate and a base confidence level to explicit larger-threshold confidence guarantees. They preserve information about the reference matrix, including its null directions. A statement requiring positive definiteness would exclude part of this conclusion.

These are established textbook results whose Lean proofs remain the targets of this mission. The draft supplies concrete definitions and open theorem statements, not completed proofs. Mathlib already provides probability measures, normal distributions, matrix positivity, and a semidefinite Schur-complement equivalence. The published theorem PinningSync.Tree.lemma_2_13 supplies the positive-definite Schur-complement branch as a reference; it is not presented as a substitute for the full semidefinite lemma.

Difficulty

The target combines probabilistic concentration with inequalities that must hold in every matrix direction. Entrywise bounds do not state the same event. Likewise, an invertible reference matrix is a restricted case of the goal. The Gaussian branch also requires exact control of inverse-tail conventions and dilation probabilities for general closed convex sets. The source’s proof of Theorem B.5.1(i) has inconsistent tail arguments in its separating-halfspace paragraph, recorded as a proof warning; the theorem statement retains the printed $q(1-\chi)$ .

Formalization scope

All matrices are real, finite, and explicitly symmetric in the theorems. Matrix and perturbation dimensions are positive; indexing by Fin changes only the origin of the indices. The setup uses Mathlib’s positive-semidefinite predicate directly. The two matrix inequalities are defined by their positive-semidefinite differences, and the variance certificate is an existential block-matrix condition. The Gaussian geometric theorem uses the concrete standard and multivariate Gaussian measures on Euclidean space, with a positive-semidefinite covariance premise.

Formalization Note. Equation (2.3.22) specifies the inverse tail on $(0,1)$ , while the later statements allow base mass one and failure probability zero. The draft retains those cases by using the extended-real inverse quantile, with $q(0)=+\infty$ , $T(+\infty)=0$ , and the limiting exponential envelope zero at infinity. An infinite-radius centered ball is the whole space. All displayed formulas agree with the source on finite quantile arguments. This endpoint interpretation is recorded in the findings for review, rather than imposing an unprinted $\chi<1$ restriction.

The reusable components are the matrix perturbation, the two-sided order event, the block certificate, and the Gaussian tail conventions. Proof contributions must establish the full statements with their constants and endpoints. No variants are posed in this mission.

Selected references

A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. DOI. Chapter 10, printed pp. 237–241; Appendix B.5, printed p. 508; equation (2.3.22), printed p. 39.

6 thms3 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: Shuze Chen

Robust Optimization I: Conic Representations of Robust Linear ConstraintsTextbook

Reliable linear constraints under uncertain data

A production or allocation decision can satisfy a linear constraint for nominal data and violate it when those data change. Robust optimization asks for a decision that satisfies the constraint for every realization in a prescribed uncertainty set. The uncertainty set is part of the model: the requirement does not attach probabilities to its elements, and it does not permit a small violation at an unfavorable realization. Chapter 1 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops this interpretation for linear optimization.

This requirement initially gives infinitely many inequalities, even when the decision vector has only a few coordinates. The chapter's representation results identify uncertainty descriptions for which those inequalities can be replaced exactly by finite systems. The replacement matters to applications because it preserves the set of admissible decisions while expressing it in the language of linear, conic quadratic, or semidefinite optimization.

Affine uncertainty and lifted descriptions

Let $x\in\mathbb R^n$ be the decision vector and $z\in\mathbb R^L$ the perturbation. The nominal coefficients are $a^0\in\mathbb R^n$ and $b^0\in\mathbb R$ , with shifts $a^\ell,b^\ell$ for each perturbation coordinate. The robust linear constraint is

(a^0)^Tx+\sum_{\ell=1}^Lz_\ell(a^\ell)^Tx \le b^0+\sum_{\ell=1}^Lz_\ell b^\ell \qquad\text{for every }z\in Z.

A lifted conic description specifies the perturbation set by

Z=\{z\in\mathbb R^L:\exists v\in\mathbb R^u,\ Pz+Qv+p\in K\}.

Here $P,Q$ are linear coefficient arrays, $p$ is an offset, and $K$ is a cone. The variable $v$ describes the uncertainty set; it is not a decision made after uncertainty is observed. The general theorem assumes that $K$ is closed, convex and pointed, with nonempty interior. The perturbation set is nonempty. For a nonpolyhedral cone, the description must have a point strictly inside the cone.

An equivalent representation has additional variables but projects to precisely the original feasible set. The interpretation is existential: a feasible decision $x$ must admit a certificate, and every feasible pair must project to a robust feasible $x$ . This is Definition 1.3.1 of the source, not a sufficient-condition approximation.

Formalization targets

The goal is Corollary 1.3.5, printed page 21. If the description uses a nonnegative orthant, a product of Lorentz cones, or a positive semidefinite cone, the robust constraint has an explicit LP, SOCP, or SDP representation, respectively. Strict feasibility is required for the latter two cases. With auxiliary variable $y$ , the system is

p^Ty+(a^0)^Tx\le b^0,\qquad Q^Ty=0,

(P^Ty)_\ell+(a^\ell)^Tx=b^\ell\quad(1\le\ell\le L),\qquad y\in K.

The goal includes the polynomial size of this representation and the explicit dependence of its coefficients on the input data. It also records preservation of the set of feasible objective values for an objective depending only on $x$ .

Theorem 1.3.4 is the general supporting target. It gives the same system with $y\in K^*$ , where $K^*=\{y:y^Tz\ge0\text{ for every }z\in K\}$ , and allows either a polyhedral cone or a strictly feasible description. The two introductory examples give concrete representation targets:

(a^0)^Tx+\sum_\ell|(a^\ell)^Tx-b^\ell|\le b^0 \quad\text{for }Z=[-1,1]^L,

(a^0)^Tx+\Omega\sqrt{\sum_\ell((a^\ell)^Tx-b^\ell)^2}\le b^0 \quad\text{for }Z=\{z:\|z\|_2\le\Omega\}.

The box target includes its further representation by finitely many linear inequalities with auxiliary upper bounds on the absolute values. These are Examples 1.3.2 and 1.3.3, not additional general duality assumptions.

What the representation provides

The result identifies the finite certificate system appropriate to each uncertainty model. It distinguishes an exact reformulation from a conservative replacement that could exclude valid decisions. Because the original decision variables remain present, an objective can be retained without interpreting the auxiliary certificate as an additional physical decision.

The mathematical results are established textbook results. The work requested here is their formal proof against explicit Lean statements. The resulting definitions expose affine uncertainty, lifted perturbation sets and finite certificate systems for reuse. Published good-cone and dual-cone definitions are already available and are imported; the theorem statements in this mission remain open proof targets.

Difficulty and boundary behavior

The equivalence requires existence of a finite certificate, not merely a sequence approaching a limiting objective value. Nonpolyhedral descriptions can fail to admit the asserted certificate without strict feasibility. In contrast, the polyhedral case does not need a strictly feasible point, so imposing that condition uniformly would lose part of the source result.

There is also a distinction between a finite worst-case value and a perturbation attaining it. The proof on printed page 20 writes a maximization problem and then discusses its optimal value; this does not require primal attainment. The formal target uses universal feasibility directly. The local findings record an explicit nonattainment example, without establishing a gap in the duality argument.

Formalization scope

All coordinates are real and finite. Nominal coefficients are stored separately from perturbation shifts. Lorentz blocks contain a distinguished scalar coordinate and a finite vector part; their Euclidean norm is the square root of a sum of squares. PSD coefficients are symmetric matrices, and pairings sum all matrix entries, giving the trace pairing for symmetric inputs. Strict feasibility in that case means positive definiteness in the symmetric ambient space.

The representation is built from the coefficient arrays themselves. Robust feasibility is defined independently by universal quantification over perturbations; it is never defined as certificate existence. No rank condition is imposed on $P$ or $Q$ . Nonnegative ball radii include zero, and zero-dimensional coordinate lists retain their ordinary empty-sum interpretation.

Formalization Note The explicit system has one scalar inequality, $u+L$ scalar equalities, and one standard cone block. If $N$ is its number of auxiliary scalar coordinates and $q$ its structural cone description length, the chosen dense counts are

I=1+n+L+u+N+(L+1)(n+1)+(L+u+1)N+q,

O=n+N+(u+L+1)(n+N+1)+q.

The size target is $O\le4I^2$ , an explicit witness to the book's polynomial-size assertion. The constant is encoding bookkeeping, not a numerical complexity constant quoted from the book. PSD storage uses $k^2$ coordinates, including symmetric duplicates. These counts concern the finite representation, not bit complexity or the time needed to solve it.

Selected references

Aharon Ben-Tal, Laurent El Ghaoui and Arkadi Nemirovski, Robust Optimization, Princeton University Press, 2009, Chapter 1, Definition 1.3.1, Examples 1.3.2–1.3.3, Theorem 1.3.4 and Corollary 1.3.5, printed pages 17–21. DOI.

7 thms3 active usersReviewed

Information Theory Quantum Information·Captain: mikedeng1

Entropy and Optimal Decompositions of States Relative to a Maximal Commutative Subalgebra: Equivalent Characterizations of a Symmetric Optimal Pair for Transposition-Invariant Rank-Two StatesResearch Paper

Motivation

In finite dimensional quantum information, a state of a full matrix algebra can be restricted to a smaller algebra of observables. The resulting entropy depends on which observables are retained. For a maximal commutative subalgebra, the retained observables are equivalent to measurements in a fixed orthonormal basis. The restriction has an ordinary probability distribution, but the state before restriction can still contain coherence between basis vectors. Uhlmann studies how the entropy of this restricted state compares with the least average entropy obtainable from pure states whose mixture is the original state. This comparison is an instance of the entropy of a subalgebra introduced by Narnhofer and Thirring and developed in the setting of matrix algebras Uhlmann, pp. 2–4.

Symmetry can make that minimization more concrete. A unitary that swaps two basis projections acts on states and their decompositions. Uhlmann's Lemma 6 asks when a rank two state fixed by this swap has a distinguished two-state optimal decomposition, and relates that event to the geometry of a set on which the entropy roof is affine Uhlmann, pp. 8–11. The result is a specific connection between a physical symmetry, an optimization problem over pure states, and the extreme points of a convex set.

Setting

Let $\mathcal H=\mathbb C^d$ with its standard basis $|j\rangle$ , and let $\mathcal C$ be the diagonal algebra. Its minimal projections are $P_j=|j\rangle\langle j|$ . A state is represented by a positive semidefinite matrix $D$ of trace one. A pure state has density matrix $|\psi\rangle\langle\psi|$ for a unit vector $\psi$ . The state of $\mathcal C$ obtained by restricting $D$ records the diagonal probabilities $D_{jj}$ Uhlmann, p. 4, equations (1)–(3).

Write $s(x)=-x\ln x$ , with $s(0)=0$ . The diagonal entropy is $\widetilde S(D)=\sum_j s(D_{jj})$ . The convex roof $R(D)$ is the infimum of $\sum_k p_k\widetilde S(\rho_k)$ over finite decompositions $D=\sum_k p_k\rho_k$ into pure states with positive weights $p_k$ summing to one. A decomposition attaining the infimum is optimal. Uhlmann's entropy of $\mathcal C$ at $D$ is $H_D=\widetilde S(D)-R(D)$ Uhlmann, pp. 4–5, equations (4)–(7).

An affine functional $l$ supports $R$ if $l\le R$ on all states and equality holds at some state. Its contact set is $\Omega(l)=\{\nu:R(\nu)=l(\nu)\}$ . Given $D$ , define $\Omega_D$ as the intersection of all contact sets whose support functional touches $R$ at $D$ . This intersection is compact and convex, contains every pure state used by an optimal decomposition of $D$ , and is a region on which $R$ is affine Uhlmann, pp. 6–7, Lemma 3 and equation (10). A transposition $U$ swaps two $P_j$ and fixes the remaining minimal projections. It transforms a density matrix as $D\mapsto U^*DU$ Uhlmann, p. 8.

Formalization targets

Goal: equivalent rank two conditions

For a rank two state $D$ fixed by a transposition $U$ , Uhlmann's Lemma 6 asserts equivalence of three statements:

\begin{aligned} \text{(a)}\;&D\text{ is the only }U\text{-invariant state in }\Omega_D;\\ \text{(b)}\;&D\text{ has an optimal decomposition into two different pure states,}\ &\text{and some member of }\Omega_D\text{ does not commute with }U;\\ \text{(c)}\;&\operatorname{Ext}(\Omega_D)=\{\rho,U^*\rho U\}\text{ for two distinct states.} \end{aligned}

The milestone list follows the paper's supporting results: finite optimal decompositions with rank bounds (Lemma 1), comparison on an $R$ -set (Lemma 2), compact supporting contact sets and their covering (Lemma 3), the intersection properties of $\Omega_D$ (the Corollary at equation (10)), zero entropy implying purity (Lemma 4), and the rank two support projection formula (equation (13)) Uhlmann, pp. 5–9. The goal preserves all three clauses of the printed equivalence.

Significance

When the equivalent conditions hold, the rank two state has an optimal decomposition using just two pure states, while the entire supporting contact set has only the two swapped extreme points. Thus the statement identifies circumstances under which the symmetry of a matrix state controls both the optimizer and the geometry of the convex roof. Uhlmann subsequently gives an explicit expression for $R(D)$ under these conditions in equation (27), which is outside the present goal Uhlmann, pp. 10–12.

The result is proved in the cited paper; the remaining task here is a machine checked development of the definitions, supporting results, and equivalence. The local Lean files state the targets and compile with proof placeholders; they do not constitute machine checked proofs of the milestones or goal. A completed development would also supply reusable finite dimensional infrastructure for pure state roofs, supporting contact sets, and optimal decompositions of density matrices.

Difficulty

An optimal pair alone does not immediately determine every extreme point of $\Omega_D$ . That set is an intersection of all contact sets, and may be larger than the convex hull of the pure states seen in one decomposition. The paper itself says equality with that smaller convex hull remains a conjecture in general Uhlmann, p. 7, Remark and footnote 3. Its printed discussion of the implication from the optimal pair to the two extreme points does not resolve this general distinction. The equivalence is therefore retained exactly as printed and the gap is recorded for review.

Formalization scope

Matrices are indexed by Fin d, so the paper's indices $1,\ldots,d$ become $0,\ldots,d-1$ . The state predicate reuses the published QAlgorithms.IsDensityMatrix. Pure states are unit-vector outer products. Finite decompositions use strictly positive real weights and complex matrix mixtures. Real.negMulLog supplies natural logarithms and $s(0)=0$ . The real infimum defining $R$ is applied only to states; there the decomposition set is nonempty and its costs are bounded below. Off the state space, Lean's real infimum can return a default value that has no meaning in the paper.

Supporting affine functionals are represented by Hermitian matrices via $l_A(\nu)=\operatorname{Re}\operatorname{Tr}(\nu A)$ , as in the paper's equation (9). The set $\Omega_D$ is the full intersection in equation (10), and its extreme points are taken in the ambient real matrix space. The transposition in the goal is explicitly self-adjoint, $U^*=U$ , matching the identity used in the printed proof. The rank is matrix rank. “Length two” means two distinct pure states with positive weights whose cost attains $R(D)$ . No optimal pair is assumed as a hypothesis.

The needed contributions are proofs of the six stated milestones, the finite dimensional properties of the model definitions they use, and the three implications of Lemma 6. The model's pure state decomposition and supporting set definitions are reusable for other convex roof problems on finite density matrices.

Selected references

Armin Uhlmann, Entropy and optimal decompositions of states relative to a maximal commutative subalgebra, preprint arXiv:quant-ph/9704017v2, 1998. arXiv

9 thms3 active usersReviewed

Algebra Quantum Information Representation Theory·Captain: mikedeng1

Structure and Properties of the Algebra of Partially Transposed Permutation Operators: A = M ⊕ S, M = ⊕ U(α) with U(α) ≅ M(rank Q(α), ℂ), and S ≅ ⊕_{h(ν)<d} M(dim ψ^ν, ℂ)Research Paper

Motivation

Permutation operators encode the symmetries of many identical quantum systems. When one tensor factor is transposed, the resulting operators occur in questions about the commutant of mixed tensor representations and about partially transposed quantum states. The usual symmetric-group algebra no longer describes their multiplication: a product can acquire a factor equal to the local dimension $d$ . Mozrzymas, Horodecki, and Studziński determined the full algebraic structure of their span in their 2014 paper. Their description identifies its simple components even when a small local dimension makes the natural spanning family linearly dependent.

Setting

Let $d\ge1$ and $n=m+2\ge2$ . On $n$ tensor factors of $\mathbb C^d$ , the permutation operator $V(\sigma)$ moves the computational-basis tensor indexed by $(i_1,\ldots,i_n)$ to the tensor indexed by $(i_{\sigma^{-1}(1)},\ldots,i_{\sigma^{-1}(n)})$ . Write $t_n$ for matrix transposition on the last tensor factor only. The object of this mission is the complex operator algebra

A=A_n^{t_n}(d)=\operatorname{span}_{\mathbb C}\{V(\sigma)^{t_n}:\sigma\in S(n)\}.

The subspace $M$ is spanned by those $V(\sigma)^{t_n}$ for which $\sigma(n)\ne n$ . Its complement $S$ in the result is an ideal that annihilates $M$ on both sides. The permutations of the first $n-2$ positions act on $(\mathbb C^d)^{\otimes(n-2)}$ . For each irreducible representation $\varphi^\alpha$ of $S(n-2)$ that occurs in this action, write $w^\alpha=\dim\varphi^\alpha$ . Definition 40 constructs operators $u^{ab}_{ij}(\alpha)$ from their matrix coefficients, the permutation operators, and partial transposition. Their span is $U(\alpha)$ .

Definition 29 assigns to $\alpha$ a block matrix $Q(\alpha)$ indexed by $(a,i)$ and $(b,j)$ , where $1\le a,b\le n-1$ and $1\le i,j\le w^\alpha$ . Its $(a,b)$ block is $d^{\delta_{ab}}\varphi^\alpha((a\ n-1)(ab)(b\ n-1))$ , so every diagonal block is $d$ times the identity. Finally, a partition $\nu$ of $n-1$ labels an irreducible representation $\psi^\nu$ of $S(n-1)$ ; $h(\nu)$ counts the rows of its Young diagram.

Formalization targets

Structure theorem

Theorem 30 asserts that $A$ splits into mutually annihilating ideals, and that those ideals split further into full matrix algebras:

A=M\oplus S,\qquad M=\bigoplus_{\varphi^\alpha\subseteq V_d[S(n-2)]}U(\alpha),\qquad U(\alpha)\cong M_{\operatorname{rank}Q(\alpha)}(\mathbb C),\qquad S\cong\bigoplus_{\substack{\nu\vdash n-1\\h(\nu)<d}}M_{\dim\psi^\nu}(\mathbb C).

When $\det Q(\alpha)\ne0$ , the $U(\alpha)$ summand has order $(n-1)w^\alpha$ . The goal also includes the multiplication law for the $u$ operators, with coefficient $Q^{bp}_{jk}(\alpha)$ as in equation (6) of Proposition 44. This identity specifies how their natural generators multiply even when $Q(\alpha)$ is singular. The two cases for $S$ printed in Theorem 30, $d\ge n$ and $d<n$ , give the same uniform restriction $h(\nu)<d$ because every partition of $n-1$ has at most $n-1$ rows.

Significance

The theorem identifies the simple ideals and their sizes from representation data of two smaller symmetric groups. It separates the dimension-dependent part $M$ , where the rank of $Q(\alpha)$ may drop, from the part $S$ controlled by partitions with fewer than $d$ rows. Consequently, it determines the irreducible representations of this concrete operator algebra and explains why its decomposition changes with $d$ .

The result is proved in the cited paper; this mission asks for a machine-checked proof of its precise statement. The published operator model and tensor-permutation definition already fix the underlying matrices. A completed development would add reusable facts about partial transposition, ideals of represented group algebras, matrix units arising from singular coefficient matrices, and occurrence of symmetric-group representations. The read side of this mission is an open theorem, not a claim that Theorem 30 has already been formalized.

Difficulty

The natural spanning elements $V(\sigma)^{t_n}$ are not a basis when $d<n$ , and the $u^{ab}_{ij}(\alpha)$ can also be dependent. Counting generators therefore cannot establish the orders of the matrix ideals. The matrix $Q(\alpha)$ records those dependencies; its rank, not its number of rows, governs the $U(\alpha)$ summand. The complementary ideal $S$ requires tracking which representations of $S(n-1)$ survive after the $M$ component is removed. A dimension count alone would identify neither the actual ideals nor their matrix-unit multiplication laws.

Formalization scope

Operators are matrices indexed by functions Fin n → Fin d, a coordinate model of $(\mathbb C^d)^{\otimes n}$ . The last-factor transpose is the published ptLast; $A$ and $M$ are the published complex spans algA and algM. The paper's labels $1,\ldots,n-1$ become Fin (m+1), and its last label becomes Fin.last (m+1). Permutations multiply right to left. The irreducible family is represented by real orthogonal matrices, hence by unitary complex matrices after casting; the explicit completeness condition $\sum_\alpha(w^\alpha)^2=(n-2)!$ ensures that every irreducible of $S(n-2)$ is present in the family.

Occurrence means that a nonzero intertwiner embeds an irreducible into the action on exactly $(\mathbb C^d)^{\otimes(n-2)}$ . An ideal is a complex subspace of $A$ closed under multiplication on both sides. An assertion $I\cong M_r(\mathbb C)$ requires $r^2$ linearly independent matrix units spanning $I$ and obeying the matrix-unit law; it cannot be discharged by a dimension count. For $r=0$ this requires $I=0$ . The order $\dim\psi^\nu$ is represented by the number of standard Young tableaux of shape $\nu$ , using the classical symmetric-group dimension formula. The goal permits $n=2$ and requires $d\ge1$ .

Theorem 30's displayed coefficient $Q^{bp}_{ik}$ conflicts with Proposition 44's equation (6), $Q^{bp}_{jk}$ ; the latter agrees with the matrix-index contraction and is used here. Contributions toward the listed source results, the partition occurrence criterion, and the singular-matrix algebra reduction are useful. An arbitrary family of subspaces with the right dimensions does not meet the target: the statements fix $A$ , $M$ , $U(\alpha)$ , $Q(\alpha)$ , and the matrix-unit structure of each component.

Selected references

M. Mozrzymas, M. Horodecki, M. Studziński, Structure and properties of the algebra of partially transposed permutation operators, Journal of Mathematical Physics 55, 032202 (2014), arXiv:1308.2653v3. The cited version supplies the page and result numbers used in this mission.
M. Studziński, M. Horodecki, M. Mozrzymas, Commutant structure of U⊗(n−1)⊗U transformations*, arXiv:1305.6183v2. Its published operator model supplies the shared Lean definitions.

10 thms3 active usersReviewed

Combinatorics Quantum Information Representation Theory·Captain: mikedeng1

Optimal Quantum Purity Amplification: Removing the Bottom Box of the Last Column of Each Schur-Sampled Young Diagram Gives the Optimal Choi Matrix for Purifying n Depolarized QuditsResearch Paper

Motivation

Quantum devices rarely prepare the state they are asked for. A procedure meant to output a pure state $|\psi\rangle$ on $d$ levels often outputs a mixed state $\rho$ , the result of noise during preparation. If the procedure can be run $n$ times, the copies $\rho^{\otimes n}$ can be processed jointly into a single output closer to $|\psi\rangle$ . This task is quantum purity amplification (QPA), also called purification. It appears as a primitive in error mitigation, in state preparation on near-term hardware, and in the theory of quantum state estimation and cloning.

For qubits and depolarizing noise, Cirac, Ekert and Macchiavello found the optimal protocol in 1999 (Phys. Rev. Lett. 82, 4344), and Keyl and Werner determined the rate of optimal purification procedures (Ann. Henri Poincaré 2, 2001), with the minimum fidelity as figure of merit. For qudits ( $d>2$ ) the optimal protocol remained open. Childs, Fu, Leung, Li, Ozols and Vyas gave a streaming protocol (arXiv:2309.16387), and Grinko and Ozols reduced unitary-equivariant SDPs of this type to linear programs (arXiv:2207.05713) without solving this one in closed form. Li, Fu, Isogawa, Silva and Chuang (arXiv:2409.18167, version 4 of 25 Dec 2025) solve the qudit case exactly: they give the Choi matrix of the optimal channel in closed form (Theorem II.1).

Setting

Let $W=\mathbb C^d$ . An unknown pure state $\sigma=|\psi\rangle\langle\psi|$ is corrupted by the depolarizing channel of strength $\lambda\in(0,1)$ :

\rho=\mathcal D_\lambda(\sigma)=(1-\lambda)\,\sigma+\lambda\,\frac{\mathbb I_d}{d}.

A QPA protocol is a quantum channel $\Phi$ from $W^{\otimes n}$ (the input registers) to $W$ (the output register). Its quality at $\psi$ is the fidelity $F_\Phi(\psi)=\langle\psi|\Phi(\rho^{\otimes n})|\psi\rangle$ , and the figure of merit is the minimum fidelity $\min_{\|\psi\|=1}F_\Phi(\psi)$ .

A channel is described by its Choi matrix $T$ , an operator on $\mathrm{out}\otimes\mathrm{in}$ with $T\succeq0$ and $\mathrm{tr}_{\mathrm{out}}T=\mathbb I_{\mathrm{in}}$ ; the channel is $\Phi_T(X)=\mathrm{tr}_{\mathrm{in}}(T(\mathbb I\otimes X^\top))$ . Averaging the fidelity over a Haar-random $\psi$ gives the semidefinite program (SDP)

\max\ \mathrm{tr}(C^\top T)\quad\text{s.t.}\quad \mathrm{tr}_{\mathrm{out}}T=\mathbb I_{\mathrm{in}},\ T\succeq0,\qquad C=\int\sigma_U^\top\otimes\rho_U^{\otimes n}\,dU,

with $\sigma_U=U|0\rangle\langle0|U^\dagger$ , $\rho_U=\mathcal D_\lambda(\sigma_U)$ , and $dU$ the Haar probability measure on $U(d)$ .

The answer is phrased with Young diagrams. A Young diagram $\varsigma$ with $n$ boxes and at most $d$ rows labels an irreducible representation $W^{[\varsigma]}$ of $U(d)$ of dimension $d^{[\varsigma]}$ , and $\Pi_\varsigma$ denotes the projector onto the $\varsigma$ -isotypic part of $W^{\otimes n}$ (weak Schur sampling). The protocol must be covariant under the mixed representation $R(U)=\bar U\otimes U^{\otimes n}$ . Inside the $\varsigma$ -sector this representation splits as $\bigoplus_i W^{[\mu_i]}$ , where $[\mu_i]=\varsigma-e_i$ removes the last box of row $i$ of $\varsigma$ (padded with zeros to $d$ rows). Row $i$ is feasible if it is the last row or $\varsigma_i>\varsigma_{i+1}$ . Let $i^*$ be the smallest feasible row; $[\mu_{i^*}]$ is $\varsigma$ with the bottom box of its last column removed. $P_\mu$ is the projector onto the $[\mu]$ -isotypic component of $R$ .

Formalization targets

Goal: Theorem II.1

T^*=\sum_{\varsigma}\frac{d^{[\varsigma]}}{d^{[\mu_{i^*}]}}\;P_{\mu_{i^*}}\big(\mathbb I_{\mathrm{out}}\otimes\Pi_\varsigma\big)

is feasible and optimal for the SDP. Its channel $\Phi_{T^*}$ is a quantum channel. For every channel $\Phi$ , $\min_\psi F_\Phi(\psi)\le\min_{\psi'}F_{\Phi_{T^*}}(\psi')$ . The statement asserts optimality, not uniqueness, and holds for every $d\ge1$ , $n\ge0$ , $0<\lambda<1$ .

Milestones (in the order the proof uses them)

Proposition S2.1. An operator commuting with $\bar U\otimes U^{\otimes n}$ ( $U\in SU(d)$ ) and with input permutations is a scalar $m_i$ on each block $[\mu_i]$ of every sector.
Eq. (S23). $|\psi\rangle\langle\psi|=A(-\rho^{-1})+B\,\mathbb I_d/d$ with $A=\frac{\lambda(d(1-\lambda)+\lambda)}{d^2(1-\lambda)}$ , $B=d+\frac{\lambda}{1-\lambda}$ .
Lemma S2.3. $P=\mathrm{Id}-\frac{\mathbb I}{d}\otimes\mathrm{tr}_{\mathrm{out}}$ is an orthogonal projector.
Lemma S2.4. If $P(C_1)=AP(C_2)$ with $A>0$ , the two SDPs have the same optimal solutions.
Eq. (S25). $P(C)=AP(C')$ with $C'=-\int(\rho_U^\top)^{-1}\otimes\rho_U^{\otimes n}\,dU$ .
Eq. (S26). $C'$ acts on the block $[\mu_i]$ as $c'_i=-S^{[\mu_i]}(a,\dots,a,b)$ , $a=\lambda/d$ , $b=1-\frac{d-1}{d}\lambda$ , where $S^{[\mu]}=s^{[\mu]}/d^{[\mu]}$ is the normalized Schur polynomial.
Eqs. (S27)–(S28). $S^{[\mu]}\le S^{[\lambda]}$ on $(0,\infty)^d$ iff $[\mu]\preceq[\lambda]$ in dominance order.
p. 21. $[\mu_i]\preceq[\mu_j]$ whenever $i\le j$ .

Significance

The theorem gives the exact optimal purification channel for every $d$ , $n$ and depolarizing strength, and the channel does not depend on $\lambda$ . It has an operational form, worked out in the paper's Sec. II C: Schur sampling, a correction inside each sector, and a partial trace. From it the paper derives the optimal sample complexity $n\approx\frac1\delta(1-\frac1d)\frac{\lambda}{(1-\lambda)^2}$ for output infidelity $\delta$ (Theorem II.2) and an efficient circuit implementation (Algorithm 1). Both rest on Theorem II.1.

The result is proved on paper but not formalized anywhere. A formal proof would check a chain that mixes semidefinite programming, Haar integration, the Schur–Weyl duality of the mixed representation $\bar U\otimes U^{\otimes n}$ , and a combinatorial inequality for normalized Schur polynomials (Sra's theorem, European J. Combin. 51, 2016), which is cited and not proved in the paper. Several of these components are general results: the block decomposition of covariant operators, the cost-matrix projection argument for SDPs with a partial-trace constraint, and the dominance ordering of normalized Schur polynomials.

Difficulty

Symmetry reduces the SDP to a linear program in one coefficient $t_i$ per block, but the coefficients $c_i$ of the original cost matrix $C$ are hard to evaluate directly. The proof replaces $C$ by $C'$ , whose block coefficients are characters of rational representations evaluated at the spectrum of $\rho$ , and shows that the replacement leaves the optimizer unchanged. The remaining step compares these characters across blocks. That comparison is the Cuttler–Greene–Skandera inequality for normalized Schur polynomials, a nontrivial combinatorial theorem. One natural guess fails: keeping the block of the largest feasible row instead of the smallest gives a channel that is not optimal in general. The optimal block removes the bottom box of the last column, which is generally a different row.

Formalization scope

Operators are complex matrices indexed by $\mathrm{Fin}\,d\times(\mathrm{Fin}\,n\to\mathrm{Fin}\,d)$ , output register first. Partial traces are the published WildeQIT.partialTraceLeft/Right. The Haar measure is the published probability Haar measure QAlgorithms.Schur.unitaryHaar d on $U(d)$ , and Haar integrals of matrices are taken entrywise. Young diagrams, Schur polynomials, dimensions $d^{[\nu]}$ (semistandard tableau counts), Schur modules with their polynomial representations, and the weak Schur sampling projector $\Pi_\varsigma$ come from the published QAlgorithms.Schur layer; channels are QAlgorithms.IsChannel (finite Kraus families). Rows are 0-based in Lean.

The irreps $[\mu_i]$ of the mixed representation (Nguyen, arXiv:2310.01613) are rational: when $\varsigma$ has fewer than $d$ rows, $\mu_d$ has last row $-1$ . They are encoded by the determinant shift $\nu_i=\varsigma+(1^d)-e_i$ , a Young diagram with $n+d-1$ boxes, with $[\mu_i]=[\nu_i]\otimes\det^{-1}$ . The isotypic projector is the character integral $P_\mu=d^{[\nu]}\int\overline{\chi_\nu(U)}\det U\,R(U)\,dU$ .

Disclosed choices:

Proposition S2.1 is stated on the full space with an added permutation-invariance hypothesis, which replaces the paper's restriction to one irrep block. Without it the full-space statement is false.
Lemma S2.4 uses $\mathrm{Re}\,\mathrm{tr}(CT)$ without the transpose, as printed, and the constraint $\mathrm{tr}_{\mathrm{out}}T=\mathbb I$ .
Eq. (S28) makes the quantifier over positive arguments explicit.
The goal's minimum-fidelity clause is stated without infima: there is a $\psi$ whose fidelity under $\Phi$ is at most the fidelity of $\Phi_{T^*}$ at every $\psi'$ .

Trivializing formalizations are ruled out. $T^*$ is the explicit operator above, computed from $d$ and $n$ alone, never an argmax or a hypothesis. The cost matrix is the actual Haar integral, not a closed form. The competitors are all feasible $T$ and all channels $\Phi$ , with no symmetry assumed.

Welcome contributions: the tracing and Pieri-type decomposition of $\bar U\otimes U^{\otimes n}$ ; Haar orthogonality of characters on $U(d)$ ; the equivalence of Choi feasibility and Kraus channels; Sra's inequality. Each is reusable beyond this mission.

Selected references

Z. Li, H. Fu, T. Isogawa, C. Silva, I. Chuang, Optimal Quantum Purity Amplification, arXiv:2409.18167v4, 2025. https://arxiv.org/abs/2409.18167
J. I. Cirac, A. K. Ekert, C. Macchiavello, Optimal purification of single qubits, Phys. Rev. Lett. 82, 4344, 1999. https://doi.org/10.1103/PhysRevLett.82.4344
M. Keyl, R. F. Werner, The rate of optimal purification procedures, Annales Henri Poincaré 2, 1–26, 2001.
A. M. Childs, H. Fu, D. Leung, Z. Li, M. Ozols, V. Vyas, Streaming quantum state purification, arXiv:2309.16387, 2023. https://arxiv.org/abs/2309.16387
D. Grinko, M. Ozols, Linear programming with unitary-equivariant constraints, arXiv:2207.05713, 2023. https://arxiv.org/abs/2207.05713
Q. T. Nguyen, The mixed Schur transform: efficient quantum circuit and applications, arXiv:2310.01613, 2023. https://arxiv.org/abs/2310.01613
S. Sra, On inequalities for normalized Schur functions, European Journal of Combinatorics 51, 492, 2016.

15 thms3 active usersReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

A (Slightly) Improved Approximation Algorithm for Metric TSP: Max-Entropy Spanning Tree Plus Odd-Vertex Matching Costs at Most (3/2 − ε)·OPT in Expectation, ε > 10⁻³⁶Research Paper

Motivation

The metric traveling salesperson problem asks for the cheapest tour through a finite set of cities whose pairwise costs are symmetric and satisfy the triangle inequality. The classical Christofides–Serdyukov algorithm combines a spanning tree with a matching on its odd-degree vertices and has a worst-case guarantee of $3/2$ times the optimal tour cost. Karlin, Klein, and Oveis Gharan showed that a randomized choice of spanning tree can improve that factor by an absolute amount, however small. Their Theorem 1.1 gives an $\varepsilon>10^{-36}$ for which the expected cost is at most $(3/2-\varepsilon)\operatorname{OPT}$ Karlin–Klein–Oveis Gharan, §1.

The paper was circulated as a preprint before its 2024 Operations Research publication. This mission uses the pinned arXiv version 6, whose theorem numbers and page references appear throughout. The authors explicitly distinguish their algorithmic guarantee from an improvement to the Held–Karp integrality gap; the former does not itself establish the latter Karlin–Klein–Oveis Gharan, p. 1. Their separate work studies that integrality-gap question Karlin–Klein–Oveis Gharan, 2022.

Setting

Let $V$ be a set of $n\ge3$ cities and let $c(u,v)$ be a metric cost. A tour visits every city once and returns to its start; $\operatorname{OPT}(c)$ is the least tour cost. A Held–Karp vector $x^0$ assigns a nonnegative fractional value to every undirected edge, has degree two at every city, and crosses every nontrivial vertex cut with total value at least two. Its objective is $c(x^0)=\tfrac12\sum_{u,v}c(u,v)x^0_{uv}$ . We take $x^0$ to attain the minimum Held–Karp objective. These objects reuse the published MetricTSP model.

The paper chooses any city $u$ and splits it into $u_0$ and $v_0$ . Each edge incident to $u$ gives half its LP value to each copy. A new edge $e_0=\{u_0,v_0\}$ has LP value one and cost zero. Let $E$ be the positive support of the split LP vector after removing $e_0$ , and let $x$ denote its values on $E$ . A spanning-tree law $\mu$ gives probabilities to the spanning trees contained in $E$ and has marginal $\Pr_{T\sim\mu}[e\in T]=x_e$ for each $e\in E$ .

Among all such laws, a maximum-entropy law maximizes $H(\mu)=-\sum_T\mu(T)\log\mu(T)$ , taking $0\log0=0$ . A sampled tree $T$ has an even number of odd-degree vertices. Let $M_T$ be a minimum-cost perfect matching of those vertices in the complete metric graph. The cost studied here is $\operatorname{algCost}(c,\mu)=\mathbb E_{T\sim\mu}[c(T)+c(M_T)]$ . The tree and matching make a connected Eulerian multigraph; metric shortcutting gives a tour with no larger cost Karlin–Klein–Oveis Gharan, pp. 1–3.

Formalization targets

The goal is a single absolute constant, chosen before the size, costs, LP optimum, split city, or tree law:

\exists\varepsilon>10^{-36}\quad\forall(n,c,x^0,u,\mu),\qquad \operatorname{algCost}(c',\mu) \le\left(\frac32-\varepsilon\right)\operatorname{OPT}(c).

Here $c'$ is the split cost, $x^0$ is any Held–Karp optimum, and $\mu$ is any maximum-entropy law with exact marginals of the split LP vector. The maximum-entropy existence milestone ensures this class of laws is nonempty. The attack path records the node split, membership in the spanning-tree polytope, existence of the exact law, the tree-cost identity, the $O$ -join characterization, Theorem 3.1's payment bounds, and the final expected matching-cost bound Karlin–Klein–Oveis Gharan, pp. 2, 6, 18–19.

The proof of Theorem 1.1 uses $\varepsilon_P=3.12\cdot10^{-16}$ , $\eta=\varepsilon_P/1308$ , and $\beta=\eta/4.1$ . Its matching analysis gives the sharper intermediate target $\mathbb E[c(M_T)]\le(1/2-\varepsilon_P\beta/6)\operatorname{OPT}$ . With the expected tree cost at most $\operatorname{OPT}$ , this yields an improvement greater than $10^{-36}$ Karlin–Klein–Oveis Gharan, proof of Theorem 1.1.

Significance

The result supplies a strict improvement over the $3/2$ guarantee for general metric TSP using a specified random-tree and parity-correction algorithm. It also isolates a useful probabilistic statement: a maximum-entropy spanning-tree law with fixed LP marginals admits a cheaper expected odd-vertex matching than the standard half-of-OPT bound. The constant is tiny; the claim is a worst-case theoretical guarantee rather than a prediction of practical performance Karlin–Klein–Oveis Gharan, §1.

The paper theorem is proved, but the statements in this mission have no machine-checked proofs yet. A completed formalization would connect existing Lean definitions for tours, Held–Karp feasibility, graph cost, tour incidence vectors, and $T$ -joins to reusable definitions for finite spanning-tree distributions, entropy, rooted near-minimum cuts, and the $O$ -join cut relaxation. The mission also keeps the quantitative constants and the uniform order of quantifiers visible to later developments.

Difficulty

The marginal constraints make the expected tree cost straightforward, but they do not determine the parity of a tree cut. A matching on the odd-degree vertices must simultaneously satisfy every relevant parity cut, while its total expected cost must fall strictly below half of the optimal tour. Near-minimum cuts can overlap and cross, so a bound on any one cut does not automatically coexist with bounds on all the others. Theorem 3.1 captures the required simultaneous payment statement, including a negative expected payment on LP edges and a controlled positive payment on optimal-tour edges Karlin–Klein–Oveis Gharan, §3.

Formalization scope

Cities are Fin n with $n\ge3$ ; edges are unordered pairs, and LP vectors remain symmetric functions on ordered city pairs as in the published Held–Karp model. Cut sums count each crossing edge once. A tree is a finite edge set that spans the split vertex type Fin (n+1). Distributions and expectations are finite sums, with probabilities zero away from spanning trees of $E$ . The distinguished edge has split cost zero and LP value one. Matchings use an involution on the vertices, fixed on even-degree vertices; the matching cost is half the sum over matched vertices. The real infimum defining that cost is over a finite, nonempty set.

The paper's printed spanning-tree inequality for $S=\varnothing$ has the impossible bound $0\le-1$ , so Fact 2.1 uses nonempty $S$ . Theorem 3.1 explicitly assumes $0\le\eta\le10^{-12}$ : without nonnegativity, its bound on a nonnegative random vector can be negative. Every near-minimum cut is nonempty and excludes both endpoints of $e_0$ , matching the paper's rooted-cut convention. The optimal tour in Theorem 3.1 is any optimal Hamiltonian cycle through $e_0$ . The O-join bound uses $y_{e_0}=1$ in place of the proof's infinite placeholder; the edge has zero cost.

The goal uses the exact maximum-entropy law. An arbitrary tree distribution would not state the paper's improvement, and an existential over unspecified tour-producing procedures would be satisfied by always returning an optimal tour. The polynomial-time construction of an approximately marginal-preserving $\lambda$ -uniform sampler, and therefore the runtime guarantee of the algorithm as implemented in the paper, are outside this formalization. The path version, Theorem 1.2, is also outside this mission Karlin–Klein–Oveis Gharan, §1.1 and proof of Theorem 1.1.

Selected references

A. R. Karlin, N. Klein, and S. Oveis Gharan, A (Slightly) Improved Approximation Algorithm for Metric TSP, Operations Research, 2024; arXiv:2007.01409v6.
A. R. Karlin, N. Klein, and S. Oveis Gharan, A (Slightly) Improved Bound on the Integrality Gap of the Subtour LP for TSP, FOCS, 2022; arXiv:2105.10043.

16 thms3 active usersReviewed

Optimization Quantum Information Theoretical Computer Science·Captain: mikedeng1

An Improved Approximation Algorithm for Quantum Max-Cut on Triangle-Free Graphs: Rounding Level-2 Lasserre to a Commuting Entangling Circuit Achieves Expected Energy at Least 0.582·‖H‖Research Paper

Motivation

Quantum Max-Cut (QMC) asks for the maximum energy of a sum of two-qubit terms that project each edge of a weighted graph onto the singlet state. Its maximum-energy state is the ground state of the antiferromagnetic Heisenberg model, a standard model of magnetism, and computing that energy is QMA-hard (Piddock–Montanaro 2017, Cubitt–Montanaro 2016). QMC has become the test case for approximation algorithms for local Hamiltonians, playing the role Max-Cut plays for classical constraint satisfaction.

No product-state algorithm (one that outputs a state without entanglement) can guarantee more than half of the optimum on every instance: on a single edge the best product state has energy $1$ while the singlet has energy $2$ . Beating this worst-case $1/2$ barrier therefore requires producing entangled states, and the obstacle is monogamy of entanglement: a qubit cannot be maximally entangled with all of its neighbours at once.

Timeline. Gharibian–Parekh (2019) rounded the level-1 Lasserre relaxation to a product state with ratio $0.498$ . Anshu–Gosset–Morenz (2020) showed that product states with commuting entangling gates beat product states, with ratio $0.531$ . Parekh–Thompson (2021) introduced the level-2 Lasserre relaxation for QMC, showed that it encodes monogamy, and obtained $0.533$ . In 2022 two simultaneous works rounded a level-2 solution to a commuting entangling circuit: Lee obtained $0.562$ on all graphs, and King (published 2023) obtained $0.582$ on triangle-free graphs, with an algorithm that uses the level-2 solution twice: once to round to a product state, once to choose the entangling angles.

Setting

The graph has vertex set $V=\{0,\dots,n-1\}$ , one qubit per vertex, and symmetric weights $w_{ij}\ge0$ normalised so that $\sum_{i<j}w_{ij}=1$ ; the neighbours of $i$ are the vertices $k\ne i$ with $w_{ik}\ne0$ , and the graph is triangle-free if no three vertices are pairwise neighbours. The edge term is

h_{ij}=\tfrac12\bigl(1-X_iX_j-Y_iY_j-Z_iZ_j\bigr)=2\,|\psi^-\rangle\langle\psi^-|_{ij},\qquad H=\sum_{i<j}w_{ij}h_{ij},

and the quantity to approximate is $\|H\|=\max_{\|\psi\|=1}\langle\psi|H|\psi\rangle$ .

The level-2 Lasserre relaxation $\mathrm{Lasserre}_2(H)$ is a semidefinite program over real matrices $M$ indexed by Pauli strings of weight at most $2$ : $M\succeq0$ , $M(A,B)$ depends only on the operator $A^\dagger B$ (with a sign flip when $A^\dagger B$ changes sign, and $M(A,B)=0$ when $A^\dagger B$ is not Hermitian), $M(A,A)=1$ , and the objective is $\tfrac12\sum_{i<j}w_{ij}(1-M(X_i,X_j)-M(Y_i,Y_j)-M(Z_i,Z_j))$ . From a solution the algorithm reads the edge values $x_{ij}=-\tfrac12(1+M(1,X_iX_j)+M(1,Y_iY_j)+M(1,Z_iZ_j))\in[-1,1]$ .

Algorithm 17 of the paper, written out:

Solve $\mathrm{Lasserre}_2(H)$ , obtaining $M$ .
GP rounding: take Gram vectors $W_{k\sigma}$ of the single-site block of $M$ , draw a Gaussian matrix $Z$ , and set the Bloch vectors $\vec v_k=Zu_k/\|Zu_k\|$ , $u_k=(W_{kX},W_{kY},W_{kZ})$ .
Set $\theta_{ij}=\tfrac12\arcsin(\beta x_{ij})$ when $x_{ij}\ge0$ and $\theta_{ij}=0$ otherwise.
For each vertex draw $\vec n_k$ uniformly on the circle of unit vectors orthogonal to $\vec v_k$ , and put $P_k=\vec n_k\cdot\vec\sigma$ .
Choose signs $\varepsilon_{ij}=\pm1$ by the argument of $\langle v_i|P_j|v_j\rangle\langle v_j|P_i|v_i\rangle$ (rule (10)).
Output $\prod_{ij}\exp(i\varepsilon_{ij}\theta_{ij}P_i\otimes P_j)\bigotimes_k|v_k\rangle$ .

Its expected energy $E$ is the expectation of $\langle H\rangle$ in the output state over all of the algorithm's randomness. The parameter $\beta$ is chosen as $\beta^*=\arg\max_\beta\min_xF(\beta;x)/(1+x)\approx0.390$ , where $F(\beta;x)=f(x)\bigl(\tfrac12+\tfrac12(1-\beta^2(1-x)^2)+\tfrac2\pi\beta x(\sqrt{1-\beta^2}+(1-\sqrt{1-\beta^2})x)\bigr)$ and $f$ is the hypergeometric function (12) describing GP rounding.

Formalization targets

Goal: Theorems 3 and 19

For every triangle-free normalised weighted graph, every solution $M$ of $\mathrm{Lasserre}_2(H)$ , every Gram factorisation used by the rounding, and every $\beta\in[0,1]$ with $F(\beta;x)\ge0.582(1+x)$ on $[-1,1]$ ,

0.582\cdot\|H\|\ \le\ E\ \le\ \|H\| .

The hypothesis on $\beta$ is exactly how the proof uses $\beta^*$ ; it is satisfied by $\beta=0.39$ .

Milestones, in attack order

Lemma 10: $\operatorname{Tr}(h_{ij}\,\rho_{\text{prod}})=\tfrac12(1-\vec v_i\cdot\vec v_j)=:E_{ij}$ .
Lemma 11: $\langle v_k|P_k|v_k\rangle=0$ , $P_k$ reverses the Bloch vector, and the phase $\gamma_{ij}$ is uniform.
Lemma 12: on a triangle-free graph, averaged over the $P_k$ ,

\langle h_{ij}\rangle\ge E_{ij}\Bigl(\tfrac12+\tfrac12\prod_{j\ne k\sim i}\cos2\theta_{ik}\prod_{i\ne l\sim j}\cos2\theta_{lj}+\tfrac1\pi\sin2\theta_{ij}\Bigl(\prod_{j\ne k\sim i}\cos2\theta_{ik}+\prod_{i\ne l\sim j}\cos2\theta_{lj}\Bigr)\Bigr).

Lemma 7 (monogamy): $\sum_{j\in S}x_{ij}\le1$ for every set $S$ of neighbours of $i$ .
Lemma 22 and Corollary 8: the products $\prod\sqrt{1-\beta^2x_{ik}^2}$ over neighbours with $x_{ik}\ge0$ are at least $\sqrt{1-\beta^2}$ , and at least $\sqrt{1-\beta^2(1-x_{ij})^2}$ when $j$ is excluded.
Lemma 18: $\langle h_{ij}\rangle\ge E_{ij}\bigl(\tfrac12+\tfrac12(1-\beta^2(1-x_{ij})^2)+\tfrac2\pi\beta x_{ij}(\sqrt{1-\beta^2}+(1-\sqrt{1-\beta^2})x_{ij})\bigr)$ .
Lemma 13: $\mathbb E_Z[E_{ij}]\ge f(x_{ij})$ .
Display after Lemma 18: $F(0.39;x)\ge0.582(1+x)$ for $x\in[-1,1]$ .
Theorem 6: $\mathrm{Lasserre}_2(H)\ge\|H\|$ .

Significance

The result shows that a semidefinite relaxation can do more than produce a product state: the same solution that fixes the product state also tells the algorithm which edges to entangle and by how much, and the level-2 constraints are what make this choice respect monogamy. The algorithm is rotation-invariant and uses no preferred single-qubit basis. The ratio $0.582$ exceeds every earlier guarantee for QMC, on triangle-free graphs; the paper suspects the same ratio holds on all graphs.

The result is proved on paper, by a chain of explicit calculations. Its statements are drafted here, while their Lean proofs remain open. A complete development would give a verified Pauli-string and Lasserre layer for two-local Hamiltonians, a verified analysis of Gaussian projection rounding in three dimensions, and a verified analysis of commuting Pauli-product circuits; each is reused by the other QMC approximation algorithms in the timeline above.

Difficulty

The obvious argument evaluates each edge's energy separately, but the gates on neighbouring edges do not act trivially on $h_{ij}$ : expanding the circuit produces cross terms indexed by pairs of neighbour subsets, and on graphs with triangles those cross terms do not cancel. Lemma 12 is where triangle-freeness enters, and its expectation over the random equatorial Paulis must be computed exactly, including the uniform law of the relative phase that produces the factor $2/\pi$ . The second difficulty is analytic: Lemma 13 is an identity for Gaussian projections expressed through ${}_2F_1$ , and the final inequality $F(0.39;x)\ge0.582(1+x)$ holds with a margin of about $0.001$ , so it requires certified numerical bounds on a hypergeometric series rather than a plot.

Formalization scope

Qubit registers are Fin n → Bool. Pauli strings are Fin n → Fin 4 (0 = identity), with operators from the published QMCProduct_HalfApprox_Basic layer. Edges are unordered pairs $i<j$ with $w_{ij}\ne0$ , counted once in $H$ and in the objective.
$\|H\|$ is the supremum of $\operatorname{Re}\langle\psi|H|\psi\rangle$ over unit amplitude vectors.
A solution of $\mathrm{Lasserre}_2(H)$ is a feasible matrix whose objective is at least that of every feasible matrix. The goal quantifies over every such solution.
GP rounding is defined in the paper only by citation. It is formalized as the Gaussian projection $\vec v_k=Zu_k/\|Zu_k\|$ above, for any Gram factorisation of the single-site block. This reproduces the paper's formula (12) exactly; Lemma 13 is stated in expectation over $Z$ , because the printed pointwise inequality is false for a single draw.
The equator draw $\vec n_k$ is the normalisation of $g_k-(g_k\cdot\vec v_k)\vec v_k$ , with $g_k$ an independent standard Gaussian vector. The signs use the principal argument in $(-\pi,\pi]$ , which agrees with rule (10). Each gate is written $\cos\theta\,1+i\varepsilon\sin\theta\,P_iP_j$ , equal to $\exp(i\varepsilon\theta P_i\otimes P_j)$ , and gates are applied in lexicographic order (they commute).
$E$ is a Bochner integral of $\operatorname{Tr}(H\rho_{\text{out}})$ over the product of the Gaussian laws of $Z$ and $(g_k)$ . The integrand is bounded and measurable, so the integral does not take its junk value.
The goal fixes the algorithm completely. An existential over output states or over algorithms would be witnessed by the top eigenvector, and such a statement is not the theorem. The hypothesis on $\beta$ is satisfiable, so the goal is not vacuous.
Out of scope: "efficient" and "classical description" in Theorem 3, the EPR Hamiltonian results (Theorems 4 and 16), and the $y$ -parts of Lemma 7 and Corollary 8.
Contributions are welcome on any milestone. Lemma 22, the display inequality and Lemmas 10–11 are self-contained, while Lemma 7 needs the Parekh–Thompson monogamy argument for $\mathrm{Lasserre}_2$ .

Selected references

R. King, An Improved Approximation Algorithm for Quantum Max-Cut on Triangle-Free Graphs, accepted in Quantum (2023); arXiv:2209.02589v3. https://arxiv.org/abs/2209.02589
S. Gharibian, O. Parekh, Almost optimal classical approximation algorithms for a quantum generalization of Max-Cut, APPROX/RANDOM 2019. https://arxiv.org/abs/1909.08846
J. Briët, F. M. de Oliveira Filho, F. Vallentin, Grothendieck inequalities for semidefinite programs with rank constraint, Theory of Computing 10 (2014). https://arxiv.org/abs/1011.1754
A. Anshu, D. Gosset, K. Morenz, Beyond product state approximations for a quantum analogue of Max Cut, TQC 2020. https://arxiv.org/abs/2003.14394
O. Parekh, K. Thompson, Application of the level-2 quantum Lasserre hierarchy in quantum approximation algorithms, ICALP 2021. https://arxiv.org/abs/2105.05698
E. Lee, Optimizing quantum circuit parameters via SDP, ISAAC 2022. https://arxiv.org/abs/2209.00789
S. Piddock, A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Inf. Comput. 17 (2017). https://arxiv.org/abs/1506.04014
T. Cubitt, A. Montanaro, Complexity classification of local Hamiltonian problems, SIAM J. Comput. 45 (2016). https://arxiv.org/abs/1311.3161

17 thms3 active usersReviewed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

Asymptotically Optimal Approximation of Single Qubit Unitaries by Clifford and T Circuits Using a Constant Number of Ancillary Qubits: O(log(1/ε)) Gates Approximate Every Single-Qubit UnitaryResearch Paper

Motivation

A fault-tolerant quantum computer executes only a discrete set of gates. The standard choice is the Clifford and T library: the Hadamard gate $H$ , the phase gate $S$ , CNOT, and the gate $T = \mathrm{diag}(1, e^{i\pi/4})$ , which together are universal and are well suited to error-corrected implementation. Every other gate, in particular every single-qubit rotation that appears in quantum simulation or the quantum Fourier transform, has to be approximated by a circuit over this library, and the number of gates spent per rotation multiplies the cost of the whole computation. The question is therefore how many library gates are needed to approximate a single-qubit unitary to precision $\varepsilon$ .

A short history of the question:

Solovay–Kitaev (Kitaev 1997; Dawson–Nielsen 2005, arXiv:quant-ph/0505030): any universal library approximates any single-qubit unitary with $O(\log^{3+\delta}(1/\varepsilon))$ gates, without ancillas.
Lower bound (Harrow–Recht–Chuang 2002, arXiv:quant-ph/0111031): a volume count shows that $\Omega(\log(1/\varepsilon))$ gates are necessary in general.
Phase kickback: a special resource state on $O(\log(1/\varepsilon))$ ancilla qubits gives $O(\log(1/\varepsilon))$ gates, but the resource state itself costs $O(\log^2(1/\varepsilon)\log\log(1/\varepsilon))$ gates and $O(\log^2(1/\varepsilon))$ ancillas.
Exact synthesis (Kliuchnikov–Maslov–Mosca 2012, arXiv:1206.5236; Giles–Selinger 2012, arXiv:1212.0506): a unitary is a Clifford and T circuit, on the same qubits plus at most one ancilla, exactly when its entries lie in the ring $\mathbb Z[i, 1/\sqrt2]$ , with gate count linear in the denominator exponent.
This paper (Kliuchnikov–Maslov–Mosca, December 2012, arXiv:1212.0822): with two ancillas initialized to $|0\rangle$ , $O(\log(1/\varepsilon))$ Clifford and T gates suffice, matching the lower bound up to a constant factor.
Ancilla-free optimal synthesis followed shortly after (Selinger 2012, arXiv:1212.6253; Ross–Selinger 2014, arXiv:1403.2975), using number-theoretic rounding in $\mathbb Z[i,1/\sqrt2]$ directly.

Setting

A register of $n$ qubits has computational basis $\{|z\rangle : z \in \{0,1\}^n\}$ . The circuits of this mission act on three wires: the data qubit (wire 0) and two ancillas (wires 1 and 2), which start in $|0\rangle$ . A circuit is a finite list of gates, each being $H$ or $T$ on one wire or CNOT on an ordered pair of distinct wires; it is applied in list order, and its size $\#C$ is the number of gates.

The quality of a circuit $C$ as an implementation of a one-qubit unitary $U$ is measured on the input–output map with the ancillas initialized: compare the linear maps from one qubit to three qubits

\mathcal C : \psi \mapsto C(\psi\otimes|00\rangle), \qquad \mathcal U : \psi \mapsto (U\psi)\otimes|00\rangle ,

by the Frobenius norm $\|\mathcal C - \mathcal U\|_F$ . This is sensitive to the global phase of $U$ , and it charges any amplitude the circuit leaves on the ancillas.

The paper's central gate is the phase gate $\Lambda(e^{i\varphi}) = \mathrm{diag}(1, e^{i\varphi})$ . For $k\in\mathbb N$ it uses the roundings $\lfloor 2^k\cos\varphi\rfloor$ , $\lfloor 2^k\sin\varphi\rfloor$ , the Gaussian rational

\gamma = \frac{\lfloor 2^k\cos\varphi\rfloor + i\lfloor 2^k\sin\varphi\rfloor}{2^k},

and the two-qubit vector $|v\rangle = \frac{1}{2^k}(\lfloor 2^k\cos\varphi\rfloor + i\lfloor 2^k\sin\varphi\rfloor, 0, a+ib, c+id) = \gamma|00\rangle + |1\rangle\otimes|g\rangle$ , where the integers $a,b,c,d$ solve $a^2+b^2+c^2+d^2 = 4^k - \lfloor 2^k\cos\varphi\rfloor^2 - \lfloor 2^k\sin\varphi\rfloor^2$ .

Formalization targets

Goal: every single-qubit unitary with $O(\log(1/\varepsilon))$ gates and two ancillas

\exists A>0\ \ \forall U\in U(2)\ \ \forall \varepsilon\in(0,1]\ \ \exists C:\quad \|\mathcal C - \mathcal U\|_F \le \varepsilon \ \text{ and }\ \#C \le A\Big(\log_2\tfrac1\varepsilon + 1\Big).

The constant $A$ is absolute. The goal asserts only the shape of the bound, so a sharper constant does not invalidate it.

Milestones

Every $U\in U(2)$ is a fixed-length product of $H$ and phase gates $\Lambda(e^{i\theta})$ (§2, p. 2).
$\Lambda(e^{i\varphi}) = T^m\Lambda(e^{i\varphi'})$ with $m<8$ and $0\le\varphi'\le\pi/4$ (§2.1, p. 3).
For $0\le\varphi\le\pi/4$ the four-square equation is solvable and every solution makes $|v\rangle$ a unit vector (§2.1, p. 3).
$|\gamma - e^{i\varphi}| \le \sqrt2/2^k$ (§2.2, p. 3).
$\||g\rangle\|^2 = 1-|\gamma|^2 \le 2\sqrt2/2^k$ (§2.2, p. 3).
Any controlled preparation of $|v\rangle$ is within $\sqrt{2/4^k + 2\sqrt2/2^k}$ of $\Lambda(e^{i\varphi})\otimes|00\rangle$ (§2.2, p. 3).
$|v\rangle$ is prepared, controlled on the data qubit, by $O(k)$ gates with no further ancilla (§2.2, p. 3; §2.3, p. 4).
$\Lambda(e^{i\varphi})$ is approximated within $\sqrt{2/4^k + 2\sqrt2/2^k}$ by $O(k)$ gates (§2.2, p. 3).
Errors add when approximating circuits are composed (§2, p. 2).

Significance

The result. The theorem shows that the logarithmic lower bound on the gate count can be attained constructively with the Clifford and T library, at the price of two clean ancillas and with a classical compilation cost dominated by solving one four-square equation. Before it, the best constructive count for this library was the polylogarithmic one of Solovay–Kitaev. The construction also separates the problem into a number-theoretic rounding step and an exact-synthesis step, which is the structure later ancilla-free algorithms refine.

Formalizing it. The result is proved on paper but, to our knowledge, no part of it is machine-checked. A complete development formalizes: the reduction of single-qubit unitaries to phase gates; the rounding and four-square estimates; the controlled exact synthesis of a two-qubit state over $\mathbb Z[i]/2^k$ with linear gate count; and the error bookkeeping on initialized maps. The $n$ -qubit generalization from Kliuchnikov's later paper (arXiv:1306.3200) is posed on the platform as an open goal (QAlgorithms.Papers.Independent.Renew46.P12.approximateSynthesis), using the same error measure; this mission is its single-qubit, exactly-two-ancilla case, with its own proof route.

Difficulty

The estimates of §2.1–§2.2 are elementary. The weight sits in milestone 7, which the paper cites rather than proves: a two-qubit unit vector with entries in $\mathbb Z[i]/2^k$ must be prepared from $|00\rangle$ by $O(k)$ gates (the Giles–Selinger column lemma, a reduction by two-level unitaries of types $iX$ , $T^{-m}(iH)T^m$ and $W$ ), and the resulting circuit must be made controlled on the data qubit without introducing a third ancilla. The naive route, controlling each gate of a generic exact-synthesis circuit, ordinarily consumes an extra ancilla (the paper itself notes that a straightforward count gives three), and ancilla-free exact synthesis is not available for arbitrary operators: circuits over $\{H,T,\mathrm{CNOT}\}$ on three qubits realize only a restricted set of determinants. Keeping the gate count linear in $k$ through both steps requires the count of two-level operators to be linear in the denominator exponent, which is the substance of the column lemma.

Formalization scope

Registers are Qubits n = Fin n → Bool; wire 0 is the data qubit and wires 1, 2 are the ancillas, appended after the data wire.
The gate set is the published $\{H, T, \mathrm{CNOT}\}$ (htcxGateSet); $S = T^2$ and $X = HT^4H$ , so gate counts against the full Clifford and T library differ by a constant factor. Circuits and their unitaries are the published Circuit, Circuit.unitary, Circuit.size.
The error is frobNorm (initializedMap c.unitary - idealMap U 2): the Frobenius norm of the rectangular map above. It dominates the per-state distance of §2.2 and the paper's "larger system" remark.
Every $O(\cdot)$ of the page is pinned: $2\sqrt2/2^k$ for $1-|\gamma|^2$ , $\sqrt{2/4^k + 2\sqrt2/2^k}$ for the distance, $A(k+1)$ and $A(\log_2(1/\varepsilon)+1)$ for gate counts, with $A$ quantified before every other variable. The printed bound $\sqrt2/2^k$ is kept as is.
"Up to two ancillary qubits" is formalized as exactly two ancilla wires; an unused one stays idle. The ancillas need not be returned clean, since leakage is charged by the error.
The hypothesis $0\le\varphi\le\pi/4$ of §2.1 is kept wherever the page uses it; milestone 2 removes it.
The page prints the transformed state as $\alpha|000\rangle + \beta\gamma|100\rangle + \beta|01\rangle\otimes|g\rangle$ ; by its own definition of $|v\rangle$ the last term is $\beta|11\rangle\otimes|g\rangle$ , and the formalization uses the latter.

Trivializing readings are excluded: dropping the ancillas makes the goal false (with no ancillas and a phase-sensitive error, unitaries whose determinant is not a power of $e^{i\pi/4}$ cannot be approximated), quotienting by the global phase or allowing arbitrary one-qubit gates would make it a different and weaker statement, and a constant $A$ depending on $U$ or $\varepsilon$ would make it vacuous.

Not formalized here: Lemma 1 (the $\Omega(\log(1/\varepsilon))$ lower bound with ancillas, p. 4), the average classical runtime $O(\log^2(1/\varepsilon)\log\log(1/\varepsilon))$ of the randomized four-square solver, and the auxiliary bound $4^k - \lfloor 2^k\cos\varphi\rfloor^2 - \lfloor 2^k\sin\varphi\rfloor^2 \le 4\cdot2^k + \mathrm{Const}$ that serves only that runtime.

Reusable beyond this mission: the controlled exact-preparation lemma (milestone 7) and the composition lemma for initialized maps (milestone 9) apply to any ancilla-based synthesis result. Proofs of individual milestones, Mathlib-style lemmas on embedOp and circuit unitarity, and a formal treatment of two-level unitaries over $\mathbb Z[i,1/\sqrt2]$ are all welcome.

Selected references

V. Kliuchnikov, D. Maslov, M. Mosca, Asymptotically optimal approximation of single qubit unitaries by Clifford and T circuits using a constant number of ancillary qubits, arXiv:1212.0822v2, 2012 (Phys. Rev. Lett. 110, 190502, 2013). http://arxiv.org/abs/1212.0822
B. Giles, P. Selinger, Exact synthesis of multiqubit Clifford+T circuits, Phys. Rev. A 87, 032332, 2013. http://arxiv.org/abs/1212.0506
V. Kliuchnikov, D. Maslov, M. Mosca, Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates, Quantum Inf. Comput. 13, 2013. http://arxiv.org/abs/1206.5236
M. Amy, D. Maslov, M. Mosca, M. Roetteler, A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits, IEEE Trans. CAD 32, 2013. http://arxiv.org/abs/1206.0758
C. M. Dawson, M. A. Nielsen, The Solovay–Kitaev algorithm, Quantum Inf. Comput. 6, 2006. http://arxiv.org/abs/quant-ph/0505030
A. W. Harrow, B. Recht, I. L. Chuang, Efficient discrete approximations of quantum gates, J. Math. Phys. 43, 2002. http://arxiv.org/abs/quant-ph/0111031
A. Y. Kitaev, A. H. Shen, M. N. Vyalyi, Classical and Quantum Computation, Graduate Studies in Mathematics 47, AMS, 2002.
M. O. Rabin, J. O. Shallit, Randomized algorithms in number theory, Comm. Pure Appl. Math. 39, 1986.
V. Kliuchnikov, Synthesis of unitaries with Clifford+T circuits, 2013. http://arxiv.org/abs/1306.3200
P. Selinger, Efficient Clifford+T approximation of single-qubit operators, 2012. http://arxiv.org/abs/1212.6253
N. J. Ross, P. Selinger, Optimal ancilla-free Clifford+T approximation of z-rotations, 2014. http://arxiv.org/abs/1403.2975

17 thms3 active usersReviewed

Control Theory Mathematical Physics Quantum Information·Captain: mikedeng1

Stabilizing qubit coherence via tracking-control: Under Pure Dephasing, Coherence Can Be Held Constant Exactly Until t_b = v_z(0)²/(2γc), Where the Control Fields DivergeResearch Paper

Motivation

A qubit coupled to an environment loses the phase relation between its basis states $|0\rangle$ and $|1\rangle$ : the off-diagonal entries of its density matrix decay. This decoherence is the main obstacle to storing quantum information, and a large body of work tries to counter it with external control fields. Lidar and Schneider (arXiv:quant-ph/0410048, Quantum Information and Computation 2005) ask a sharp question in the simplest nontrivial setting: if the controller may observe the state and choose the Hamiltonian at every instant (tracking control), can it keep the coherence of a dephasing qubit exactly constant, and for how long?

Their answer, stated in the abstract, is that "it is possible to maintain coherence for finite time durations, until the control field diverges." It was known that Hamiltonian control cannot hold the purity $\operatorname{Tr}\rho^2$ of a Markovian open system at its initial value (Ketterle and Pritchard, Phys. Rev. A 46, 4051 (1992), and Tannor and Bartana, J. Phys. Chem. A 103, 10359 (1999), refs. [25, 26] of the paper), and the paper's §II.A shows that under a unital Lindbladian the purity decreases whatever the Hamiltonian; the present result locates exactly how much of the coherence, as opposed to the purity, control can protect.

Setting

A qubit state is a complex $2\times2$ matrix $\rho$ with $\operatorname{Tr}\rho=1$ , $\rho_{10}=\rho_{01}^*$ and $\operatorname{Tr}(\rho^2)\le1$ . With the Pauli matrices $\sigma_x,\sigma_y,\sigma_z$ , its Bloch vector is $\vec v=(v_x,v_y,v_z)$ , $v_\alpha=\operatorname{Tr}(\rho\sigma_\alpha)$ , so that $\rho=\tfrac12(I+\vec v\cdot\vec\sigma)$ (eq. (9)). The coherence is the squared radius of $\vec v$ in the $x$ – $y$ plane,

c=v_x^2+v_y^2=4|\rho_{01}|^2 \quad\text{(eq. (11))}.

The controller applies the Hamiltonian $H(t)=\tfrac{\hbar}{2}\bigl(\omega_0(t)\sigma_z+\omega_1(t)\sigma_x-\omega_2(t)\sigma_y\bigr)$ (eq. (13)) with three real fields $\omega_0,\omega_1,\omega_2$ , and the qubit undergoes pure dephasing at rate $\gamma>0$ :

\frac{\partial\rho}{\partial t}=-\frac{i}{\hbar}[H,\rho]+\frac{\gamma}{2}(\sigma_z\rho\sigma_z-\rho)\quad\text{(eq. (32))}.

Equivalently the Bloch vector obeys $\dot{\vec v}=M(t)\vec v$ with

M(t)=\begin{pmatrix}-\gamma&-\omega_0&-\omega_2\\ \omega_0&-\gamma&-\omega_1\\ \omega_2&\omega_1&0\end{pmatrix}\quad\text{(eq. (30))}.

Without control the coherence decays as $e^{-2\gamma t}c$ . The breakdown time of an initial state with coherence $c>0$ is

t_b=\frac{v_z(0)^2}{2\gamma c}\quad\text{(eq. (38))}.

The tracking fields are, with $s=\operatorname{sign}v_z(0)$ , an arbitrary $\omega_0$ , and $R(t)=v_z(0)^2-2\gamma ct$ ,

\omega_2(t)=s\,\frac{-\gamma v_x(0)-\omega_0(t)v_y(0)}{\sqrt{R(t)}},\qquad \omega_1(t)=s\,\frac{-\gamma v_y(0)+\omega_0(t)v_x(0)}{\sqrt{R(t)}}\quad\text{(eqs. (41)–(42))},

and the tracked state is $\tfrac12(I+\vec v(t)\cdot\vec\sigma)$ with $\vec v(t)=(v_x(0),v_y(0),s\sqrt{R(t)})$ .

Formalization targets

Goal: coherence can be held exactly on $[0,t_b)$ , and no longer

For $\hbar>0$ , $\gamma>0$ and a qubit state $\rho_0$ with coherence $c>0$ :

No-go. For all controls and every solution $\rho(t)$ of (32) on $[0,T)$ with $\rho(0)=\rho_0$ and constant coherence $c$ ,

v_z(t)^2=v_z(0)^2-2\gamma c\,t\quad(t\in[0,T)),\qquad T\le t_b .

Achievability. If $v_z(0)\ne0$ , then for every $\omega_0$ the tracked state starts at $\rho_0$ , is a qubit state, keeps $v_x,v_y$ fixed, and solves (32) at every $t\in[0,t_b)$ with the tracking fields.
Divergence. If $v_z(0)\ne0$ , then $\omega_1(t)^2+\omega_2(t)^2\to+\infty$ as $t\to t_b^-$ , whatever $\omega_0$ is.

Milestones

The milestones follow the paper's derivation: the Bloch parametrization (§II.B, p. 3); the equivalence of (32) and (30) (§III.B, p. 5); eq. (36), $\dot v_z=-\gamma c/v_z$ under constant coherence (p. 6); eqs. (37)–(38), $v_z(t)=(\pm)\sqrt{v_z(0)^2-2\gamma ct}$ and $T\le t_b$ (p. 6); eqs. (41)–(42), the tracking fields solve (30) and are forced once $v_x,v_y$ are frozen (p. 6); and the field-strength identity of §III.C (p. 8),

\omega_1(t)^2+\omega_2(t)^2=\frac{(\gamma^2+\omega_0(t)^2)\,c}{v_z(0)^2-2\gamma ct}.

Significance

The result gives an exact, state-dependent budget for coherence protection under dephasing. The time $t_b$ is inversely proportional to the coherence to be maintained and proportional to $v_z(0)^2=p(0)-c$ , where $p=|\vec v|^2$ is the purity: the more coherent the initial state, the shorter the protection, and a state of maximal coherence for its purity ( $v_z(0)=0$ ) cannot be protected at all. The no-go part holds for every control law, so it bounds any tracking strategy, not only the linearized one the paper constructs. The divergence of the fields is the physical cost: protection up to $t_b$ requires unbounded control amplitude, which any bounded actuator cuts short.

The paper proves these statements by direct calculation. As far as is known, none of them has a machine-checked proof. The mission turns a physics derivation, in which "the solution is" and "does not stay real" carry the logical weight, into precise statements about solutions of an ODE on a half-open interval, with the sign choice, the degenerate case $v_z(0)=0$ and the domain of the square roots made explicit.

Difficulty

The calculations are elementary, but the no-go statement quantifies over arbitrary, possibly discontinuous control fields and arbitrary solutions of the matrix equation. Nothing is assumed about the controls beyond being real functions of time, nothing about the solution beyond continuity on $[0,T)$ and the equation on $(0,T)$ , and the conclusion constrains only the $z$ -component while the hypothesis constrains only the $x$ – $y$ components. The tempting shortcut, assuming that $v_x$ and $v_y$ are frozen as in the paper's explicit construction, proves a strictly weaker statement and is not the goal. On the achievability side, the square root is not differentiable where its argument vanishes, so differentiability has to be established on $[0,t_b)$ , including the endpoint $t=0$ , and the sign $\operatorname{sign}v_z(0)$ has to be carried through the derivative.

Formalization scope

Operators are Matrix (Fin 2) (Fin 2) ℂ in the basis $|0\rangle,|1\rangle$ ; the Pauli matrices are the published MIPRE.LCS.Pauli.X/Y/Z. Bloch vectors and controls are Fin 3 → ℝ: Bloch components in the order $x,y,z$ , control components in the order $\omega_0,\omega_1,\omega_2$ (with $\omega_0$ multiplying $\sigma_z$ , as in (13)). The Bloch vector is $v_\alpha=\operatorname{Re}\operatorname{Tr}(\rho\sigma_\alpha)$ , following eq. (9); eq. (8) prints an extra factor $\tfrac12$ , which contradicts (9) and is treated as a misprint. A trajectory solves (32) or (30) on $[0,T)$ if it is continuous on $[0,T)$ and has the prescribed derivative at every $t\in(0,T)$ . Controls are arbitrary functions $\mathbb R\to\mathbb R$ . The hypotheses $\gamma>0$ and $c>0$ are added, because $t_b$ divides by $2\gamma c$ ; $\hbar>0$ is a parameter. The sign $(\pm)$ of (37), (41), (42) is $\operatorname{sign}v_z(0)$ .

Statements about $t_b$ , the tracked state and the fields are restricted to $[0,t_b)$ , because Lean's square root and division are total ( $\sqrt{x}=0$ for $x<0$ , $x/0=0$ ); a statement that only asserts that the closed-form curve solves the ODE would be the achievability half alone, and the goal requires the no-go half over all controls as well.

A complete development needs the Bloch dictionary for $2\times2$ matrices, the passage from (32) to (30), and one-variable real analysis on half-open intervals. The Bloch dictionary and the reduction of a Lindblad equation to Bloch form are reusable for other qubit control problems. Proofs of any milestone, and sorry-free lemmas on the Pauli algebra, are welcome.

Selected references

D. A. Lidar and S. Schneider, Stabilizing qubit coherence via tracking-control, Quantum Information and Computation (2005); arXiv:quant-ph/0410048v1, 2004. https://arxiv.org/abs/quant-ph/0410048
W. Ketterle and D. E. Pritchard, Atom cooling by time-dependent potentials, Physical Review A 46, 4051 (1992). https://doi.org/10.1103/PhysRevA.46.4051

9 thms3 active usersReviewed

Algebra Representation Theory·Captain: mikedeng1

Cyclotomic Birman–Wenzl–Murakami Algebras, II: Admissibility Relations and Freeness: Over an Admissible Integral Domain S, W_{n,S,r} Is a Free S-Module of Rank r^n(2n−1)!!Research Paper

Motivation

The cyclotomic Birman–Wenzl–Murakami algebra is an algebra of braids and contractions equipped with an additional cyclotomic relation. It connects diagram algebras, representation theory, and knot theoretic constructions. For calculations over a coefficient ring, one needs to know whether the diagrammatic spanning elements remain independent after parameters are specialized. The freeness theorem of Goodman and Hauschild Mosley answers that question for admissible integral ground rings: the algebra has a basis of the size predicted by labeled Brauer diagrams. The paper also identifies the algebra with a cyclotomic Kauffman tangle algebra. This mission targets the algebra's freeness and rank assertion.

The cited paper builds on admissibility relations developed with Wilcox and Yu. Its earlier definitions and preliminary statements already appear in Prove2Me mission 92e1197e-907f-4ab8-92be-01ea44f6cfef. The present mission reuses that published layer and poses the deferred freeness theorem and the intermediate results that support it. The distinction matters because two algebras with similar names but different generators or parameter conventions need not have the same rank statement.

Setting

A ground ring $S$ is a commutative unital ring with a positive integer $r$ and parameters $\rho,q,\delta_0,\delta_1,\ldots,u_1,\ldots,u_r$ . The parameters $\rho,q,\delta_0,u_1,\ldots,u_r$ are units, and they satisfy

\rho^{-1}-\rho=(q^{-1}-q)(\delta_0-1).

The algebra $W_{n,S,r}$ is generated over $S$ by invertible braids $g_i$ , contractions $e_i$ , and an invertible affine generator $y_1$ . It obeys the affine BMW relations of Definition 2.1 and the cyclotomic relation $\prod_{j=1}^r(y_1-u_j)=0$ of Definition 2.8. The shared published presentation uses indices $i=0,\ldots,n-2$ for $g_i$ and $e_i$ , corresponding to the paper's $g_{i+1}$ and $e_{i+1}$ . At $n=0$ there are no generators.

The parameters are admissible when $q-q^{-1}$ is nonzero and not a zero divisor, weak admissibility holds for every integer shift of the $\delta$ relations, and $e_1,y_1e_1,\ldots,y_1^{r-1}e_1$ are $S$ -linearly independent in $W_{2,S,r}$ . These are the conditions of Definition 3.3, expressed using condition (1) of Theorem 3.2. A morphism of ground rings preserves all $\delta_j$ and $u_i$ and permits exactly the four paired sign actions on $\rho$ and $q$ in Definition 2.13. Consequently, base change includes the sign twists allowed by the paper.

For the generic case, $F=\mathbb Q(q,u_1,\ldots,u_r)$ is the rational function field in algebraically independent variables. Put $p=\prod_j u_j$ , set $\rho=p$ for odd $r$ and $\rho=q^{-1}p$ for even $r$ , and define $\delta_a=\sum_j\gamma_j u_j^a$ , where $\gamma_j$ is the rational expression in equation (3.6). A shape in $\Gamma_n$ is an $r$ -tuple of Young diagrams whose total number of boxes is at most $n$ and congruent to $n$ modulo two. An up–down tableau of shape $\lambda$ is a path from the empty tuple to $\lambda$ , adding or removing one box at each step. Its set is $T(n,\lambda)$ .

Formalization targets

The central target is the freeness half of Theorem 6.1. For every admissible integral ground ring $S$ and every $n\ge0$ ,

W_{n,S,r}\cong_S S^{\,r^n(2n-1)!!}.

Here $(-1)!!=1$ , so the asserted rank at $n=0$ is one. A basis indexed by a finite type of that cardinality states both freeness and rank.

The milestone path includes the paper's admissibility equivalences, generic parameter construction, universal admissible integral domain, base change, the spanning family of $r^n(2n-1)!!$ elements, the relevant Jones ideal and Hecke quotient results, and the generic structure results. At the generic field, Theorem 4.8 supplies split matrix blocks indexed by $\Gamma_n$ , with block size $|T(n,\lambda)|$ . The count in the proof of Theorem 5.2 is

\sum_{\lambda\in\Gamma_n}|T(n,\lambda)|^2=r^n(2n-1)!!,

which agrees with the generic dimension asserted by Theorem 5.2. The final theorem applies over an admissible integral domain, rather than only over $F$ .

Significance

The result supplies an exact finite basis for $W_{n,S,r}$ throughout the admissible integral-domain regime. It fixes the module rank independently of a choice of specialization and gives a numerical benchmark for presentations and representations of these algebras. The generic matrix decomposition also records the simple-block labels and their sizes; the tableau identity explains how those dimensions total the same rank.

Goodman and Hauschild Mosley proved these results. This mission asks for machine-checked proofs of the statements already known in the paper. Its reusable output includes ground-ring morphisms with sign twists, the generic parameter model, and finite tableau types. The published preliminary layer in mission 92e1197e-907f-4ab8-92be-01ea44f6cfef contains two proved and four open results among the six referenced milestones; none of the eight new theorem statements is presented here as already machine proved.

Difficulty

A spanning family alone does not show a basis: specializations can introduce linear dependence, and an equality of dimensions over one field does not itself establish independence over every integral ground ring. The argument also has to maintain the exact admissibility conditions when moving between coefficient rings. Over the generic field, identifying the right semisimple blocks requires the branching shapes and tableau sizes, while the final statement concerns arbitrary admissible integral domains. These are distinct algebraic regimes, and the same presentation and parameter conventions must be kept through each one.

Formalization scope

Lean uses the published GroundParameters, BMW, BMWAdmissible, UAdmissible, and equation (3.6) gamma expression from QAlgorithms.Papers.Independent.Support21.P14. The algebra is the quotient of a free algebra by the source's relations, with zero-based generator indices. The new definition layer records all four sign cases of Definition 2.13, the generic field as a fraction ring of a multivariate polynomial ring over $\mathbb Q$ , and shapes and tableaux as finite-indexed Young diagrams. A generic ground-parameter value is asserted to exist as a theorem because the required unit and compatibility proofs are substantive.

The universal-ring milestone states all five parts of Theorem 3.19 for $\overline R_0$ and $\overline R_+$ ; part (5) is read inside $F$ , where the universal $u$ -admissible ring is the subring generated by $q^{\pm1}$ , $(q^{-1}-q)^{-1}$ , $\delta_0^{-1}$ and $u_i^{\pm1}$ . The base-change statement uses $S'\otimes_S W$ for the source's $W\otimes_S S'$ . Theorem 4.8 is expressed as a product of full matrix algebras with tableau-sized blocks, combining its split and labeling clauses with the block dimensions stated elsewhere in §4. Theorem 6.1's Kauffman-tangle isomorphism is not posed because a corresponding tangle algebra has not been provided here. The cited spanning set is expressed as an indexed family, which remains meaningful when a degenerate coefficient ring identifies elements.

The goal requires an actual basis of cardinality $r^n(2n-1)!!$ over an admissible integral domain. A mere dimension equality or spanning claim does not satisfy it. Contributions toward the missing generic decomposition, tableau count, base-change isomorphism, and passage to arbitrary admissible domains are all within scope. The ground-parameter and quotient-presentation definitions are reusable independently of this mission.

Selected references

F. M. Goodman and H. Hauschild Mosley, Cyclotomic Birman–Wenzl–Murakami algebras, II: Admissibility Relations and Freeness, 2008, arXiv:math/0612065v5.

16 thms3 active usersReviewed

Dynamical Systems Mathematical Physics Quantum Information·Captain: mikedeng1

Highly Efficient Energy Excitation Transfer in Light-Harvesting Complexes: The Fundamental Role of Noise-Assisted Transport: Sink Population 1/(N−1) Without Noise, 1 Under DephasingResearch Paper

Motivation

Photosynthetic light-harvesting complexes move an electronic excitation from the pigment that absorbed a photon to a reaction centre, where its energy is stored chemically. In the Fenna–Matthews–Olson (FMO) complex this transfer is close to lossless, and two-dimensional spectroscopy showed long-lived quantum coherence during it (Engel et al. 2007). This raised a concrete question in open-system quantum dynamics: does the environment, whose noise destroys coherence, hinder transport, or can it help?

Numerical studies of FMO models found that local dephasing raises transfer efficiency compared with purely coherent evolution (Mohseni et al. 2008; Plenio and Huelga 2008; Rebentrost et al. 2009). Caruso, Chin, Datta, Huelga and Plenio (arXiv:0901.4454, J. Chem. Phys. 2009) isolated a mechanism behind this in a model that can be solved exactly: the fully connected network (FCN). There, coherent evolution traps most of the excitation by destructive interference, and any amount of uniform dephasing removes the trap. This mission formalizes that exact result.

Setting

\mathcal D_{r,c}(\rho) = r\,\bigl[2c\rho c^\dagger - \{c^\dagger c, \rho\}\bigr].

The state $\rho(t)$ , a complex $(N+2)\times(N+2)$ matrix, obeys the Lindblad master equation $\dot\rho = \mathcal L(\rho)$ with

\mathcal L(\rho) = -i[H,\rho] + \sum_{j=1}^N \mathcal D_{\Gamma_j,\,\sigma_j^-}(\rho) + \sum_{j=1}^N \mathcal D_{\gamma_j,\,|j\rangle\langle j|}(\rho) + \mathcal D_{\Gamma_{N+1},\,|N+1\rangle\langle k|}(\rho).

The terms are coherent hopping, dissipation to the environment at rates $\Gamma_j$ , pure dephasing at rates $\gamma_j$ , and irreversible decay into the sink from a chosen site $k$ at rate $\Gamma_{N+1}$ . So $\rho(t) = e^{t\mathcal L}\rho(0)$ . The initial state is $\rho(0) = |1\rangle\langle 1|$ , and transport is measured by the sink population

p_{\rm sink}(t) = 2\Gamma_{N+1}\int_0^t \rho_{kk}(t')\,dt'.

The goal concerns the FCN of §II.A: $\omega_j = 0$ , $\Gamma_j = 0$ , the sink attached at $k = N$ , and a uniform dephasing rate $\gamma_j = \gamma \ge 0$ .

Formalization targets

Goal: noise-free and dephased limits

For $N \ge 2$ , $J \ne 0$ and $\Gamma_{N+1} > 0$ :

\gamma = 0:\quad \lim_{t\to\infty} p_{\rm sink}(t) = \frac{1}{N-1}, \qquad\qquad \gamma > 0:\quad \lim_{t\to\infty} p_{\rm sink}(t) = 1.

The first limit is Eq. (5) of the paper. The second is the claim of §II.C, confirmed for uniform dephasing in Appendix A.3, Eq. (A30). The coupling $J$ , the sink rate and the dephasing rate are left free; neither limit depends on them.

Milestones

(A7) Population sum rule: $1 = \sum_{j=1}^N \rho_{jj}(t) + \rho_{00}(t) + p_{\rm sink}(t)$ for all $t$ .
§II.A spectrum. $|\phi\rangle = N^{-1/2}\sum_j |j\rangle$ has energy $J(N-1)$ . The states $|\psi_j\rangle = |1\rangle - |j\rangle$ , $j = 2,\dots,N$ , have energy $-J$ , and together with $|\phi\rangle$ they span the site space.
Eq. (8). $|1\rangle = \frac{1}{N-1}\bigl[\sum_{j=2}^{N-1}|\psi_j\rangle + \sqrt N|\phi\rangle - |N\rangle\bigr]$ .
Invariant states. In the noiseless FCN, an eigenstate of $H$ with no overlap with site $N$ does not evolve, and $p_{\rm sink} \equiv 0$ .
Eqs. (6)–(7). For $N \ge 3$ , $\rho(t) \to \frac{N-2}{N-1}|\Psi\rangle\langle\Psi| + \frac1{N-1}|N+1\rangle\langle N+1|$ .
(A14). The closed form of $\rho_{NN}(t)$ for the noiseless FCN, $N \ge 3$ .
Appendix A.1. The closed linear system of six equations for $\Lambda = \sum_{i,j}\rho_{ij}$ , $X + iY = \sum_j \rho_{Nj}$ , $\rho_{NN}$ , $\rho_{00}$ and $p_{\rm sink}$ under uniform $\omega$ , $\Gamma$ , $\gamma$ .

Significance

The result. The noise-free limit $1/(N-1)$ shows that a perfectly coherent, fully symmetric network is a poor transporter: for $N = 10$ only $1/9$ of the excitation reaches the sink, whereas a classical random walk on the same graph delivers all of it. The dephased limit $1$ shows that arbitrarily weak local noise restores complete transfer. Together they are the cleanest exactly solvable instance of dephasing-assisted transport. The invariant-subspace argument behind them (milestones 2–5) also predicts which states are protected from a sink, a mechanism related to coherent population trapping in quantum optics and condensed-matter systems.

Formalizing it. The paper derives these limits from Laplace-domain calculations and residue computations, some of them only sketched. A machine-checked proof would settle the exact constants, the hypotheses under which each limit holds (the necessity of $J \ne 0$ and $\Gamma_{N+1} > 0$ , and the case $N = 2$ ), and the passage from the matrix exponential to the collective variables. As far as is known, none of these results has been formalized. The development also produces reusable pieces: the Lindblad generator of a single-excitation network with a sink, the trace identity (A7), and the spectrum of the complete-graph hopping Hamiltonian.

Difficulty

The obvious route is to compute $e^{t\mathcal L}$ , but $\mathcal L$ acts on an $(N+2)^2$ -dimensional space for arbitrary $N$ , so no fixed-size computation applies. The noise-free limit hinges on an exact cancellation: $\frac{N-2}{N-1}$ of the weight lies in an $H$ -eigenspace that is invisible to the sink, and the remainder must be shown to drain completely, which is a statement about the spectrum of a non-normal generator on the complementary subspace. Under dephasing that invariant subspace no longer exists, but the reduced six-variable system still has to be shown to have $p_{\rm sink} = 1$ as its only attracting steady state, for every $\gamma > 0$ and every $N$ . In the paper this is done through a final-value theorem applied to a fifth-order characteristic polynomial (A26), which is misprinted. A proof that the limit exists, and not only what it equals, is part of the task.

Formalization scope

Basis and operators. The basis is Fin (N + 2) in the paper's numbering (0 = zero-exciton state, 1…N = sites, N + 1 = sink), with natural-number indices cast into it. Operators are Matrix (Fin (N + 2)) (Fin (N + 2)) ℂ.
Hopping and rates. The hopping is normalized as $\langle i|H|j\rangle = J$ , which matches (A1), (A34) and the spectrum on p. 4. The rates multiply $2c\rho c^\dagger - \{c^\dagger c,\rho\}$ with no factor ½, as in Eqs. (2)–(4).
Evolution. $\rho(t)$ is semigroupEvolution of the published definition P16, that is, NormedSpace.exp of $t\mathcal L$ , applied to $|1\rangle\langle 1|$ .
Sink population. $p_{\rm sink}$ is the interval integral of the real part of $\rho_{kk}$ , as defined on p. 3. It is not the sink entry $\rho_{N+1,N+1}$ ; that the two agree is part of milestone 1.
Added hypotheses. The goal assumes $N \ge 2$ , $J \ne 0$ and $\Gamma_{N+1} > 0$ ; without any one of them the limits fail. Milestones 5 and 6 assume $N \ge 3$ , where $|\Psi\rangle$ and the closed form are defined.
Uniform dephasing. The dephased clause is stated only for a uniform rate $\gamma_j = \gamma$ , which is the case the paper solves. It is quantified over every $\gamma > 0$ .

A trivializing formalization is ruled out by construction: $N$ and $\gamma$ are free, $p_{\rm sink}$ unfolds to an integral of an entry of the matrix exponential of the literal generator, and none of the limits is built into a definition.

Needed infrastructure includes calculus for $t \mapsto e^{tL}X$ (derivatives, HasDerivAt of entries, the fundamental theorem of calculus for $p_{\rm sink}$ ), invariant-subspace arguments for linear ODEs, and asymptotics of linear systems with a stable matrix. Contributions of general lemmas about Lindblad semigroups (trace preservation, Hermiticity preservation, stationary states) are welcome and reusable beyond this mission.

Not formalized here: Eq. (9) (static disorder), Eq. (10) (dissipation), §II.D–§V, the Laplace-domain route (A9)–(A13) and (A25)–(A29), the two-level system (A32), and the general networks of (A39)–(A40).

Selected references

F. Caruso, A. W. Chin, A. Datta, S. F. Huelga, M. B. Plenio, Highly efficient energy excitation transfer in light-harvesting complexes: The fundamental role of noise-assisted transport, J. Chem. Phys. 131, 105106 (2009). https://arxiv.org/abs/0901.4454v2 — https://doi.org/10.1063/1.3223548
G. S. Engel et al., Evidence for wavelike energy transfer through quantum coherence in photosynthetic systems, Nature 446, 782 (2007). https://doi.org/10.1038/nature05678
M. Mohseni, P. Rebentrost, S. Lloyd, A. Aspuru-Guzik, Environment-assisted quantum walks in photosynthetic energy transfer, J. Chem. Phys. 129, 174106 (2008). https://doi.org/10.1063/1.3002335
M. B. Plenio, S. F. Huelga, Dephasing-assisted transport: quantum networks and biomolecules, New J. Phys. 10, 113019 (2008). https://doi.org/10.1088/1367-2630/10/11/113019
P. Rebentrost, M. Mohseni, I. Kassal, S. Lloyd, A. Aspuru-Guzik, Environment-assisted quantum transport, New J. Phys. 11, 033003 (2009). https://doi.org/10.1088/1367-2630/11/3/033003
G. Lindblad, On the generators of quantum dynamical semigroups, Commun. Math. Phys. 48, 119 (1976). https://doi.org/10.1007/BF01608499

10 thms3 active usersReviewed

Quantum Information·Captain: Goku

Entanglement-Assisted Classical Capacity of Noisy Quantum ChannelsResearch Paper

Motivation

Prior entanglement between sender and receiver, which exactly doubles the classical capacity of a noiseless quantum channel, can increase the classical capacity of some noisy quantum channels by an arbitrarily large constant factor depending on the channel, relative to the best known classical capacity achievable without entanglement. The enhancement factor is greatest for very noisy channels, with positive classical capacity but zero quantum capacity. Although such quantum channels can be simulated classically, no violation of causality is implied, because the simulation requires at least as much forward classical communication as the entanglement-assisted classical capacity of the channel being simulated. We obtain exact expressions for the entanglement-assisted capacity of depolarizing and erasure channels in d dimensions.

This mission is the statement-level formalization of Entanglement-Assisted Classical Capacity of Noisy Quantum Channels (arXiv:quant-ph/9904023v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main result / equation (3): depolarizing assisted capacity (Abstract main result / equation (3): depolarizing assisted capacity, PDF p. 3). 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

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

Unnumbered C <= CE <= FCCC: A resource-counted finite adaptive bipartite channel-simulation model with arbitrary local ancillas, message-independent prior pure entanglement, free backward classical communication, an actual forward classical arm, and asymptotically faithful reference-preserving simulation. (hard)
Erasure flags simulate depolarization and all corresponding capacity inequalities: Source-compatible Q2 from counted noisy-channel calls interleaved with adaptive finite LOCC, initially with no shared entanglement. (hard)
Again the difference between the bounds approaches H2(x): A source-pinned noise regime for the asserted limit of the signed quantum-bound gap. (source-ambiguity)
Author note [9]: A transpose/label convention or restriction making the three induced classical transition matrices literally identical. (source-ambiguity)

Selected references

Entanglement-Assisted Classical Capacity of Noisy Quantum Channels, arXiv:quant-ph/9904023v5, https://arxiv.org/abs/quant-ph/9904023v5

30 thms3 active usersReviewed

Quantum Information·Captain: Goku

The operational meaning of quantum conditional informationResearch Paper

Motivation

How correlated are two quantum systems from the perspective of a third? We answer this by providing an optimal quantum state redistribution protocol for multipartite product sources. Specifically, given an arbitrary quantum state of three systems, where Alice holds two and Bob holds one, we identify the cost, in terms of quantum communication and entanglement, for Alice to give one of her parts to Bob. The communication cost gives the first known operational interpretation to quantum conditional mutual information. The optimal procedure is self-dual under time reversal and is perfectly composable. This generalizes known protocols such as the state merging and fully quantum Slepian-Wolf protocols, from which almost every known protocol in quantum Shannon theory can be derived.

This mission is the statement-level formalization of The operational meaning of quantum conditional information (arXiv:quant-ph/0612050v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact state-redistribution rate region and optimal corner (Main result: exact state-redistribution rate region and corner, Eqs. (1)–(2), PDF p. 2). 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

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

w-state: Independently moderated correction of the printed W-state numerical communication cost (source-ambiguity)
zero-communication-entanglement: Independently moderated correction of the printed flagged-state entanglement-cost sign (source-ambiguity)

Selected references

The operational meaning of quantum conditional information, arXiv:quant-ph/0612050v2, https://arxiv.org/abs/quant-ph/0612050v2

14 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with MathematicaResearch Paper

Motivation

We present in this paper a set of routines constructed to compute the rank of a matrix Lie algebra and also to determine a Cartan subalgebra from a given list of elements

This mission is the statement-level formalization of Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica (arXiv:math/0205235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is so(n): BSo ordered basis (so(n): BSo ordered basis, PDF p. 5). 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

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

Abstract and introduction: rank/Cartan extension algorithm: A valid and fully specified exact Cartan-extension routine on the advertised real semisimple matrix embeddings, including guards and symbolic branch/parameter selection. (source-ambiguity)
Introduction, unnumbered Teorema: claimed Cartan characterization: A valid Cartan characterization with the original quantification over all real semisimple matrix embeddings and all their Cartan subalgebras. (source-ambiguity)

Selected references

Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica, arXiv:math/0205235v1, https://arxiv.org/abs/math/0205235v1

17 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Representation of Quantum Circuits with Clifford and $π/8$ GatesResearch Paper

Motivation

In this paper, we introduce the notion of a normal form of one qubit quantum circuits over the basis $\{H, P, T\}$ , where $H$ , $P$ and $T$ denote the Hadamard, Phase and $π/8$ gates, respectively. This basis is known as the {\it standard set} and its universality has been shown by Boykin et al. [FOCS '99]. Our normal form has several nice properties: (i) Every circuit over this basis can easily be transformed into a normal form, and (ii) Every two normal form circuits compute same unitary matrix if and only if both circuits are identical. We also show that the number of unitary operations that can be represented by a circuit over this basis that contains at most $n$ $T$ -gates is exactly $192 \cdot (3 \cdot 2^n - 2)$ .

This mission is the statement-level formalization of Representation of Quantum Circuits with Clifford and $π/8$ Gates (arXiv:0806.3834v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed paper result): unique exact normal form (Theorem 1 (seed paper result): unique exact normal form, PDF p. 6). 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.

Selected references

Representation of Quantum Circuits with Clifford and $π/8$ Gates, arXiv:0806.3834v1, https://arxiv.org/abs/0806.3834v1

27 thms3 active usersReviewed

All missions

An Optimal Policy for Dynamic Assortment Planning Under Uncapacitated Multinomial Logit Models: The Adaptive-Confidence Trisection Policy Has N-Independent Regret at Most C√TResearch Paper

Learning which products to offer

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Classical Search Game in Discrete Locations: for any optimal hiding strategy, the searcher has an optimal strategy mixing at most n Gittins search sequences that each break all ties by one orderResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 10 (p. 20)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Offline Pricing and Demand Learning with Censored Data: a data-driven pricing problem is identifiable if and only if the optimistic and pessimistic prices coincideResearch Paper

Pricing from censored sales data

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Circlet Inequalities: A New, Circulant-Based, Facet-Defining Inequality for the TSP: The Circlet Inequality Is Valid and Facet-Defining for the Symmetric TSP Polytope When 4 Divides nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Validity: Theorem 3.1

The technical lemma: contraction

The facet property

Significance

Difficulty

Formalization scope

Selected references

The Solovay-Kitaev algorithm: every gate in SU(d) is ε-approximated by a sequence of O(log^{ln 5/ln(3/2)}(1/ε)) gates from any instruction setResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 with the exponent of Eq. (8)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Binary Extended Formulations and Sequential Convexification: Among All d-Hypercube Binarizations, the Logarithmic Binarization Has Minimum RankResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.23

Milestones

Significance

Difficulty

Formalization scope

Selected references

Submodular Maximization over Multiple Matroids via Generalized Exchange Properties: Polynomial approximation for monotone submodular maximizationResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

On the Existence of Pure Nash Equilibria in Weighted Congestion Games: Characterizing universal pure equilibrium existenceResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Stochastic Networks XIV: Large Deviations for Queues with Many SourcesTextbook