Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Repeated games model long-run relationships: the same players meet stage after stage, observe what was played, and can condition today's behavior on the past. The folk theorem describes what such relationships can sustain. When players are patient, every payoff vector that is feasible and gives each player at least what the others can force on them is the payoff of an equilibrium, and the equilibrium can be chosen subgame perfect, so that every threatened punishment is itself credible. Economics, operations research and computer science use the result to explain cooperation and collusion and to reason about long-term contracts and repeated auctions.
The classical statement assumes stationary discounting: a payoff at stage is worth of a payoff today, and "patient" means . Experimental and behavioral evidence points instead to discount rates that change over time (hyperbolic and quasi-hyperbolic discounting), and planning problems with a finite or decaying horizon have weights that are not geometric at all. X. Li (later with D. Kim) asks whether the perfect folk theorem survives when the weight of stage is an arbitrary decreasing sequence, and gives a patience condition under which it does.
Timeline.
A finite set of players plays a stage game repeatedly. Player has a finite action set , , and gives the stage payoffs. At each stage every player observes the past actions and chooses an action, possibly at random. A behavior strategy assigns a mixed action to every finite history, and a profile determines a distribution over infinite plays.
An evaluation is a sequence in that is decreasing and sums to one; the payoff of is
Stationary discounting is . After a history of stages the remaining game is evaluated by the continuation evaluation ; unlike the stationary case, depends on . A profile is a subgame perfect equilibrium of if, after every history , the induced profile is a Nash equilibrium of the subgame . is the set of subgame perfect equilibrium payoffs.
The minmax level of player is
the lowest payoff the others can hold to by mixing independently. is the set of feasible payoffs and the set of feasible and individually rational payoffs.
A sequence of evaluations is patient if as , uniformly in .
If and is patient, then
The goal fixes no rate and no constants; it asserts only the limit.
The result. The theorem says that the set of credible long-run outcomes is the same under any patient time-dependent discounting as under stationary discounting with . Quasi-hyperbolic preferences with and discount factors that vary by stage are special cases. Patience is stated through ratios of consecutive weights. The paper notes that this condition does not cover -stage averages with , where the folk theorem is known to need extra assumptions. The equilibria use pure paths, with no public randomization.
Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission builds a reusable Lean model of discounted repeated games with perfect monitoring: behavior strategies, the induced distribution over finite histories, continuation games, subgame perfection, minmax levels and the feasible and individually rational set. It then states the theorem and the lemmas of its proof. The one-shot deviation principle under general discounting and the pure-path decomposition (Proposition 4.3) are standard tools that the literature usually cites without proof, and both are useful well beyond this paper.
The stationary proof relies on the fact that every subgame looks like the original game: . Under time-dependent discounting the continuation evaluation changes with the starting stage. A punishment phase of fixed length therefore carries a different weight depending on when it starts, and the number of stages needed to deter a deviation depends on the stage. Two consequences make the obvious adaptation fail. First, a deviation during a punishment starts a new punishment whose length differs from the remaining length of the old one, so the incentive check splits into cases (Lemma 5.2). Second, the pure paths that deliver the reward payoffs have to work for every continuation evaluation at once, which needs the uniformity statements of Lemma 4.2 and the perturbed decomposition of Lemma 4.4. Replacing each continuation evaluation by a geometric one does not work, because nothing forces the weights of a patient sequence to be close to geometric.
All declarations live in the namespace TimeDepFolk.Asymptotic. Stages are 0-based: Lean stage is the paper's , a history of played stages is Fin n → (∀ i, A i), and cont θ n is the paper's , which is when the tail sum vanishes. Mixed actions are lotteries (AGT.IsLottery) and the minmax level uses AGT.expectedPayoff from the published definition agt_games, with independent mixing by the others. Action sets are finite, so expectations are finite sums over histories and the payoff is the series ; no measure theory is needed. Payoff vectors live in I → ℝ with the sup norm. Subgame perfection quantifies over all histories, the empty history included, and over all behavior-strategy deviations; the one-shot reduction is a milestone to prove, not part of the definition. The player set and every action set are finite and nonempty. " nonempty and fully dimensional" is (interior (F g)).Nonempty.
The goal uses the extended-valued Hausdorff distance Metric.hausdorffEDist. The real-valued Metric.hausdorffDist is when one set is empty, so a goal stated with it would hold vacuously for every at which no equilibrium is known; the extended version makes nonemptiness of part of the claim. Stating the goal for a single payoff, with Nash instead of subgame perfect equilibrium, or with Theorem 3.2's discount factors in place of evaluations would each prove a different and weaker theorem.
A complete development needs the probability of finite histories under behavior strategies, the decomposition of the payoff into the first stage and the continuation, the one-shot deviation principle, Carathéodory's theorem (in Mathlib), and the barycentric sensitivity of Claim 7.1. The repeated-game layer and the one-shot deviation principle can be reused for any discounted repeated game with perfect monitoring. Contributions to any milestone, and alternative proofs of the decomposition results, are welcome.
Congestion pricing charges road users for the delay they impose on others. The classical theory, going back to Beckmann, McGuire and Winsten (1956), assumes a single benevolent authority that sets every toll: charging each link its marginal toll makes the selfish (Wardrop) traffic pattern socially optimal. Many real networks are different. Roads, bridges and tunnels built under build-operate-transfer schemes are run by private operators who set their own prices to maximize their own revenue. When operators compete, an equilibrium of the pricing game need not exist, need not be unique, and can be far from optimal (Acemoglu and Ozdaglar 2007; Hayrapetyan, Tardos and Wexler 2007).
Correa, Guzmán, Lianeas, Nikolova and Schröder (2021) ask whether a regulator who can only impose price caps — an upper bound on the toll of each link — can steer competing operators to the optimal flow. Their main result, Theorem 1, answers yes: optimal tolls bounded by the marginal tolls, used as caps, are the unique equilibrium of the capped game, even against coalitions of operators. This mission formalizes that theorem and the two monotonicity lemmas it rests on.
A network has links and commodities ; each commodity has a finite set of routes, each route being a set of links. Commodity has a maximum demand and a nonincreasing, continuous, nonnegative utility function on ; its aggregate utility is . Each link has a latency function on , nonnegative, nondecreasing, convex and smooth.
A flow assigns to each route so that ; is the set of flows and is the flow on link . Under a toll vector , users settle in a Wardrop equilibrium, which is a maximizer over of the potential
The paper restricts to instances where this maximizer is unique (linkwise) for every , and writes for it.
The social welfare of a flow is ; an optimal flow maximizes it over . The marginal tolls are , and a toll vector is optimal if is the optimal flow.
Each link is run by a separate operator, whose profit is . Given caps , operator chooses . A profile is a Nash equilibrium of the capped game if no operator gains by a unilateral change within its cap, and a strong Nash equilibrium if no nonempty coalition has a joint change, within the caps and confined to , that strictly raises the profit of every member. By Definition 1, is a (strong) cap equilibrium if itself is the unique (strong) Nash equilibrium of the game with caps .
If is an optimal toll vector with
then is both a cap equilibrium and a strong cap equilibrium.
Theorem 1 resolves, for capped games, the problems of existence, uniqueness and inefficiency that the literature on competing link operators identified: the regulator needs only to know the optimal flow and its marginal tolls, and then no operator, and no coalition of operators, has a reason to move away from the optimal tolls. The paper's consumer-surplus comparison (Theorem 2) is a comparison among such great tolls, and its extensions with operating costs, multi-link operators and complementary links (Theorems 3–6) follow the same pattern. The two lemmas are general facts about Wardrop flows under elastic demand — monotonicity in the tolls and a first-order bound at a profit maximum — that are reusable for any toll-setting or pricing question in nonatomic routing.
The result is proved in the paper; none of it is formalized. The mission produces a machine-checked version of the full argument, including the steps the paper states without proof.
The equilibrium flow is defined only implicitly, as the maximizer of a concave potential that depends on the tolls, so every statement about operators' profits is a statement about a parametric optimization problem. Lemma 1 needs first-order optimality conditions of (1) on a polytope of route flows with elastic demand, and continuity needs a maximum-theorem argument in which only the link flows, not the route flows, are unique. Lemma 2 cannot simply differentiate : need not be differentiable in , so the argument must work with one-sided difference quotients. The coalition part of Theorem 1 cannot be reduced to unilateral deviations; a deviation by many operators at once moves the flow on every link of the network simultaneously.
All declarations live in the namespace NetworkPricing.Caps. Links, routes and commodities are Fin J, Fin R, Fin Sd; link flows are KellyStochasticNetworks.linkFlow of the published definition KellyStochasticNetworks_Wardrop. The model commits to the following conventions:
flow with flow t a maximizer of (1) for each , together with the paper's uniqueness assumption on link flows.Formalizations that make the goal trivial are ruled out: must maximize the potential (1), not be an arbitrary function of ; uniqueness of the equilibrium is part of the conclusion, not just that is an equilibrium; and the strong notion quantifies over all coalition deviations, not single-player ones.
A complete development needs first-order optimality conditions for concave maximization over polytopes, a version of Berge's maximum theorem, and convexity facts about differentiable functions. All of these are reusable well beyond this mission. Contributions are welcome on each milestone independently, and on general lemmas about parametric Wardrop flows.
In a multiplayer multi-armed bandit, several agents repeatedly choose among the same finite set of arms, and two agents that choose the same arm collide and receive nothing. The model comes from cognitive radio and wireless networks: users share channels, a channel used by two users at once carries neither transmission, and the quality of a channel differs from user to user. Each user must learn the channel qualities from her own rewards while avoiding the others, and in a large network the users can neither exchange messages nor observe each other's choices.
When all players share the same arm means, the problem reduces to finding the best arms and spreading the players over them; algorithms such as Musical Chairs (Rosenski, Shamir and Szlak, 2016) do this. When each player has her own means , the target is an optimal solution of an assignment problem, which couples the players. Bistritz and Leshem (arXiv:1810.11162, NeurIPS 2018; a journal version appeared in Mathematics of Operations Research) gave the first algorithm for this heterogeneous case that uses no communication at all and has near-logarithmic expected regret. This mission formalizes the main theorem of the preprint arXiv:1810.11162v7.
There are players and arms. At every turn each player picks an arm . The non-collision indicator is if more than one player chose arm in the profile and otherwise. Player receives : the reward of her arm, or after a collision.
The rewards satisfy Definition II.1: for each the sequence is i.i.d. with a continuous law, mean , variance and Bernstein's moment condition with parameter , and the sequences are independent. Because the law is continuous, a zero reward reveals a collision almost surely; this is the only feedback a player gets. The horizon is unknown to the players.
Write . The benchmark is an optimal assignment , assumed unique, and the total regret is
The Game of Thrones (GoT) algorithm (Algorithm 1) runs in epochs , each with three phases: an exploration phase of turns, where players sample arms uniformly and average their collision-free rewards into estimates ; a GoT phase of turns, where players run a perturbed content/discontent dynamic with perturbation and exponent on the game ; and an exploitation phase of turns, where each player plays the arm with which she was most often content during the last GoT phases. The GoT dynamics form a Markov chain on the states (baseline arm and mood of every player), with optimal state .
With , , integers , and , there is such that for all large enough
The theorem shows that full decentralization costs at most a factor in regret: the lower bound of Proposition II.3 holds already with full information, and GoT reaches with no messages, no knowledge of , and no observation of the other players. It is a learning-in-games result as much as a bandit result: the players reach the welfare-maximizing assignment of a game that is not interdependent, which the content/discontent dynamics of Marden, Young and Pao (2014) require, and the requirement on the exponent is instead of .
The result is proved on paper and has no machine-checked proof; nothing in this mission is formalized yet. A formal proof would also settle points the paper leaves implicit, recorded in the formalization notes: one must serve every epoch although the stationary threshold of Theorem V.6 depends on the epoch's estimated utilities, and the GoT chain has transient states, so the tree formula of Lemma V.5 and the norm must be applied to its closed class.
Each phase is analysed separately, and the work lies in the parts that are not standard. The exploration bound needs a concentration inequality for averages over a random number of collision-free samples. The GoT phase needs a lower bound on a stationary probability of a perturbed chain on states, obtained by comparing the resistances of trees in the sense of Freidlin and Wentzell (Appendix A, pp. 15–18). It then needs a Chernoff bound for Markov chains (Chung, Lam, Liu and Mitzenmacher, 2012) in terms of the mixing time. Finally, the epochs interact: the estimates of epoch determine the chain of epoch , the GoT phase starts from the end of an earlier GoT phase, and the exploitation phase votes over dependent phases.
The natural first idea, to treat each epoch's GoT run as a fixed ergodic chain and apply a stationary-mass bound, fails twice. The chain is random through the estimates, so the threshold on must hold uniformly over a neighbourhood of the true means. The chain is also not irreducible: a state where a colliding player is content can never be entered.
Players, arms and turns are 0-based (Fin N, Fin M, t : ℕ), and epochs are 1-based. The collision indicator is noColl, because also names the slack in Theorem V.6 and Lemmas V.7–V.8. The rewards live on a probability space as r n i t. The players' randomization is a family of private uniform seeds, jointly independent of the rewards, and every random choice of Algorithm 1 is realized from a seed with exactly the prescribed law. Each player's action and update read only her own memory, her own seeds and her own received reward; the means, , and the other players' actions never enter a rule. Collisions are read off a zero reward, as in Algorithm 1. The regret is Eq. (3) with the realized comparison rewards. The GoT chain is an explicit matrix on Fin N → Fin M × Mood. Stationarity and the mixing time (worst start, total variation) come from the published MarkovMixing definitions.
Conventions and disclosed additions:
A formalization in which a player's rule sees the instance would make the goal trivial (play from the start), and a policy class in place of Algorithm 1 would change the theorem. Neither is used. Irreducibility of the GoT chain is false, and no statement assumes it.
Needed infrastructure that Mathlib lacks: Bernstein's inequality for sums over random index sets, the Markov-chain tree theorem (already posed on the platform as YoungConventions.Perturbed.markov_chain_tree_formula), and a Chernoff bound for finite Markov chains. The last two are reusable well beyond this mission, and contributions of them as separate theorems are welcome.
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 is replaced by a sequence of available instructions whose product approximates . If an accuracy required sequences of length , compiling an -gate algorithm to overall accuracy would cost instructions, which would erase quadratic speed-ups such as Grover's search. The Solovay-Kitaev theorem says the cost is only polylogarithmic in , 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 in 1995 on an email list, without a subsequent paper. Kitaev outlined a proof for 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 . 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 .
Fix a dimension . is the group of complex unitary matrices of determinant , and is the adjoint. The distance between gates is the operator norm of their difference,
A sequence of gates also denotes the unitary , and is its length; is an -approximation to when .
An instruction set for (Definition 1) is a finite set such that
The Solovay-Kitaev algorithm is a recursion of depth . At depth it returns a stored basic approximation of bounded length . At depth it computes , decomposes approximately as a balanced group commutator with close to the identity, and returns the concatenation of five sequences computed at depth . The accuracies satisfy and the lengths .
For every instruction set for there is such that for every and every some sequence of gates from satisfies
Theorem 1 of the paper asserts length for some ; the goal fixes , the exponent the paper's algorithm attains (Eq. (8), and §5.1 for qudits). is left unspecified, as in the paper.
In attack order: the inverse-sequence fact (p. 3); (p. 3); the base case, bounded-length -approximations (p. 5); Lemma 1, the error of an approximated group commutator (Eq. (14)); Lemma 2, a traceless Hermitian is a commutator with ; Lemma 3, ; the logarithm of a gate near the identity (p. 12); the balanced approximate commutator in , Eq. (33); the recursion invariant of the algorithm (Eqs. (1)–(2), (15), (21)–(22)); the closed form of (Eq. (4)); and the depth/length trade-off (Eqs. (7)–(8)).
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 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 commutator estimates only. This mission produces the qudit statement with the explicit exponent , the commutator estimates of Lemmas 1–3 in arbitrary dimension, and an explicit model of the recursion. The paper's constants are only approximate (, ); rigorous values are a welcome by-product.
The obvious argument, approximating 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 are at distance from the identity and are approximated to accuracy , their group commutator is approximated to accuracy , 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 , 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 to turn pointwise universality into a single length bound . The paper's derivation of Eq. (33) also contains a sign slip: with the commutator approximates instead of , which a formal proof must repair.
Gates are elements of Matrix.specialUnitaryGroup (Fin d) ℂ; Lemma 1 is about matrices in the unitary group. The distance is the 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 , 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 and a product of gates from is an -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: becomes so that bounds are meaningful for every (same -class); the paper's approximate constants (, , , ) are existential and chosen before and ; the logarithm milestone adds (needed by Lemma 2) and (the proviso of p. 3); the identity is not stated, since as printed it fails for .
Trivializing formalizations are ruled out: must be closed under and must consist of gates from ; the constant is quantified before and , so it cannot depend on them; in the recursion invariant the base routine has a fixed length bound and the decomposition routine is constrained by the accuracy bounds, not assumed to be exact.
Running time (Eqs. (3), (6), (9), ) is out of scope: there is no machine model. Needed infrastructure: compactness of (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.
Risk measures enter optimization models as objectives or constraints, and the models that use them most, multi-stage stochastic programs, are solved as large linear programs. A risk functional is only usable there if it can itself be written as the value of a linear program. Eichhorn and Römisch introduced polyhedral risk measures for this purpose (doi:10.1137/040605217). They are risk functionals defined as the optimal value of a linear stochastic program whose right-hand side is the random income being evaluated. The average value-at-risk of Rockafellar and Uryasev (doi:10.21314/JOR.2000.038) is the basic example. Sums and nestings of average values-at-risk over several periods are further examples.
Sections 2.4.4 and 3.3.5 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific, 2007, doi:10.1142/6478) develop this class in the book's profit convention (larger is better). They prove that, under two finite-dimensional conditions on the program's data, the functional is finite, concave and continuous, and that it has a dual representation over an explicitly polyhedral set of densities. The book then reads off from that dual set which axioms of multi-period acceptability functionals the functional satisfies. This mission formalizes those results.
Let be a probability space, , and a filtration in with trivial . Fix and with . Income processes live in , densities in . Random variables equal almost surely are identified.
A set is polyhedral if it is a finite intersection of closed half-spaces, and a polyhedral cone if all of those half-spaces pass through the origin. Its polar cone is , which is the negative of the usual dual cone.
The data of a polyhedral functional are dimensions , vectors and non-empty polyhedral sets for , together with coefficients . The functional is
The first decision is deterministic. The functional depends on the filtration only through the measurability of the decisions. The two standing conditions are:
The dual set is
The single-period case with is the book's Definition 2.66.
Under (i) and (ii), is finite, positively homogeneous, concave and continuous on . It is information monotone (MA0): enlarging the filtration does not decrease it. For every ,
Theorem 3.38 turns a linear multi-stage program into a risk functional with known structure. The functional is concave and continuous, and it is the lower envelope of linear functionals over a dual set cut out by finitely many linear conditions on conditional expectations. Theorem 3.39 makes that dual set into a design tool. Which translation equivariance a polyhedral functional has can be read off from finitely many vector conditions, without evaluating the functional. The multi-period average value-at-risk and sums of single-period average values-at-risk are obtained this way. These are the risk functionals that can be embedded in large-scale stochastic programming models without leaving linear programming.
The results are proved in the book and in Eichhorn–Römisch (2005). As far as is known, no part of them has a machine-checked proof. The platform has no polyhedral risk functional. It has finite-dimensional linear programming duality and a loss-side, upper-tail average value-at-risk on , which uses a different convention and so is not a substitute.
The theorem is linear programming duality, but in an infinite-dimensional space of adapted processes. Finite-dimensional LP duality does not apply directly, for three reasons:
Finiteness needs feasible decisions with a uniform bound, which is a measurable-selection question for a polyhedral set-valued map. The duality step needs conjugacy on a product of spaces. It also needs to exchange an infimum over random decisions with an expectation, and that exchange is a theorem about normal integrands, not a formality. Little of this exists in Mathlib.
The two inclusions of Theorem 3.39 that use complete recourse alone cannot simply be combined with the goal: a non-empty dual set is an extra hypothesis there (see below).
Lean namespace RiskFunctionals.Polyhedral.
Fin k → ℝ with the dot product ⬝ᵥ. Polyhedral sets and cones
are explicit finite systems of inequalities, never general closed convex cones. The polar cone
uses the book's sign.MemLp hypotheses and an -measurable
representative. Constraints hold almost surely, and conditional expectations are Mathlib's.W t (t-τ), indexed by the period of the decision it multiplies, so that its type matches.EReal, so empty
or unbounded programs give instead of a junk value. Finiteness is always a conclusion
and never a hypothesis. The other properties are stated for the real value only alongside
finiteness. The dual set is the printed polyhedral set, not an existential family.sSup over the feasible set, or a dual set given
only by its existence, would make the goal trivially true. Both are ruled out by the EReal
values and by the explicit dual set.Beyond the paper. There are two corrected variants, each stated next to the faithful item.
Two sign slips in Example 2.70 (a printed and ) are corrected in the faithful item itself.
The development needs measurable selections of polyhedral multifunctions, Fenchel–Moreau conjugacy on products, and interchange of infimum and integral. All three are reusable well beyond risk measures. Contributions of any of them, of the single-period case, or of the multi-period average value-at-risk as an instance are welcome.
Risk that unfolds over several periods is measured in two common ways. One adds up one-period measurements of each payment, each made with the information available one step earlier. The other composes one-period conditional measurements backwards in time, the way dynamic programming evaluates a policy. The second way is the one used in multistage stochastic programming with risk-averse objectives, because it is time-consistent by construction: a plan that is optimal today stays optimal when re-evaluated tomorrow. Ruszczyński and Shapiro (Conditional risk mappings, Math. Oper. Res. 2006) built the general theory of such compositions. Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) studied the matching dynamic-programming (Bellman) principle for coherent multiperiod risk-adjusted values.
The most widely used one-period building block is the average value-at-risk. When it is applied conditionally at every stage, the composition is the nested average value-at-risk. Section 3.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007), treats both constructions. It builds the nested functional, shows that it depends only on the total payoff, gives its dual representation as an infimum over bounded-growth martingale densities, and compares it with the additive (multi-period) average value-at-risk. This mission formalizes that section's statements.
Let be a probability space with a filtration . Random variables that agree almost surely are identified, and all (in)equalities between them hold almost surely. The book uses profit variables, where larger is better. Fix and put . An income process is with .
A conditional acceptability mapping has three properties:
A family defines the nested functional and the compositions
Since is trivial, both are constants.
For and a sub--field , the conditional average value-at-risk of is defined implicitly by
With trivial this is the lower-tail average of the quantile function. The nested average value-at-risk is
The multi-period average value-at-risk is . Below it is used with all and .
For and , the nested average value-at-risk is well defined, and
Here is -measurable. The feasible are nonnegative martingales whose one-step growth is at most .
The representation (3.49) shows that the nested average value-at-risk is a coherent functional of the total payoff. Its dual set consists of martingale densities with a multiplicative growth bound. Proposition 3.36 builds on this description to compare the nested and additive constructions. The same description underlies cutting-plane methods for risk-averse multistage programs: there the nested value is evaluated stage by stage, and each stage contributes one factor . Proposition 3.33 is the general mechanism behind this: predictable translation-equivariance collapses a nested definition into a cumulative one.
All of these results are proved in the book, some only in outline. None is machine-checked. The platform has loss-side, upper-tail conditional value-at-risk results in other conventions and a nested risk-adjusted cost in an SDDP setting. It has no statement of the nested average value-at-risk or of (3.49). Formalizing this section yields a reusable treatment of conditional average values-at-risk defined by duality, together with their compositions along a filtration.
The conditional average value-at-risk is not given by a formula. It is defined through a family of infima indexed by the sets , so composing two of them requires knowing what the first one does when paired with a general bounded weight rather than an indicator. Merging the infima of successive stages into one infimum over processes needs measurable selection of near-optimal densities, conditional on the earlier stages, and the martingale constraint must be preserved. The printed proof treats in a few lines and asserts that the general case "follows by induction". Its last display also carries a misprint, for (FINDINGS F5).
Random variables are functions Ω → ℝ. The filtration is Mathlib's Filtration ℕ, and only indices matter. IsStandardFiltration records that is trivial and . The conditional average value-at-risk is the predicate IsConditionalAVaR, a literal transcription of the defining relation, with the infimum computed in EReal. The nested and multi-period values are predicates that are existential over versions of the conditional average values-at-risk. The goal therefore asserts existence and the identity separately. A version of the goal that only assumed some value exists, or that took a bare real infimum, would be vacuous or junk-valued, and the formal statement rules out both. The expectation of the -measurable output is the functional's real value. The dual set requires to be -measurable, which the page leaves implicit.
Beyond the paper. Two corrected variants are posed beside the faithful statements:
The faithful statements stay as printed and are expected to be disproved.
Contributions that would be reused beyond this mission:
A deviation functional measures how far a random profit spreads around its mean: the variance, the standard deviation, the mean absolute deviation from the median, and the average value-at-risk deviation are the standard examples in portfolio selection and in risk-averse stochastic programming. Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), §2.5, organize many of them under one construction, the minimal loss functional: the smallest expected loss incurred when is predicted by a constant under a convex loss . Optimization over portfolios with such a functional as the risk term relies on writing it as a supremum of linear functionals of — a dual representation — because a supremum of linear functions can be handled by linear and conic programming and by subgradient methods.
The best known instance is the representation of the average value-at-risk as a minimum over a scalar , due to Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002), stated in the loss convention. The general convex-analytic tool behind such representations is Rockafellar's conjugacy theorem for integral functionals (Pacific J. Math. 1968). This mission formalizes the book's Theorem 2.75, which combines the two for every minimal loss functional, together with the results its special cases rest on.
Let be a probability space, , and the conjugate exponent, . Random variables are profits (larger is better) in ; dual variables are in , so that is finite.
Let be non-negative, convex, with . The minimal loss functional of is
defined for such that exists. The Fenchel conjugate of is
For example gives and ; gives the mean absolute deviation from the median and equal to on and outside.
The distribution function of is , its quantile function the left-continuous inverse , . For the average value-at-risk is the lower-tail average
and the average value-at-risk deviation is . Write and .
For every as above and every with finite,
and, for every and ,
The constants , and are exactly the book's; the last minimum is attained.
Two further items state Eq. (2.89) (p. 97), , and Eq. (2.101) (p. 102) as printed, .
The result. Theorem 2.75 gives every minimal loss functional an explicit dual set: the centered , penalized by . For piecewise linear the penalty is the indicator of a box, so is a supremum of linear functionals over a polyhedral set, and the acceptability functional is an infimum over mean-one dual variables; (2.114) and the last display recover the dual representation (2.20) of the average value-at-risk from this general principle. For quadratic the theorem returns the variance representation (2.89). The same dual sets feed the book's later results on the monotonicity of with respect to stochastic orders and on conditional versions (2.116)–(2.117).
Formalizing it. No platform item states Theorem 2.75, the integral conjugacy of Proposition B.3, or the dual representations of the variance and standard deviation. Related platform results use other conventions — the loss-side, upper-tail CVaR minimization formula (RUCVaR.MinFormula), a minimal weighted mean absolute deviation in Ogryczak–Ruszczyński normalization (DualSSD.MeanRisk.hDiam_eq_min), finite-dimensional Fenchel–Young and biconjugation (ConvexOptimization.fenchel_young, ConvexOptimization.fenchel_biconjugate_eq_self). The mission produces the profit-side, statements of the book.
The weak inequality in (2.113) is the Fenchel–Young inequality integrated; equality is the content. The printed proof treats piecewise linear by choosing, from alone, a partition on which one affine piece of is maximal, and claims for every ; that identity holds only at , and the conclusion does not follow (for and uniform on the chosen is ). The statement itself is correct in that example, but a complete argument has to choose the dual variable at a minimizing , which need not exist, and has to pass from piecewise linear to general by a limiting argument the book does not give. On the side, an optimal such as need not lie in when grows faster than , so the supremum is in general not attained and must be approached. Proposition B.3 requires a measurable selection of subgradients and handles the case .
Lean represents random variables as measurable functions with MemLp hypotheses (, , p.HolderConjugate q, ) on a probability space; constraints on hold almost surely. is an extended-real supremum (EReal), so it is where the book's supremum is unbounded. The suprema and infima of the dual representations are taken in EReal over the for which (resp. ) is finite — almost surely finite and integrable — which does not change the book's value. is defined as the infimum in of : the book's "min" presupposes attainment, which fails for and unbounded above, and attainment is not claimed. The standing assumption of §2.5.5 that exists is a hypothesis of the parts on general . is the book's lower-tail average of the left-continuous quantile function, not the loss-side upper-tail CVaR; variance is Mathlib's ProbabilityTheory.variance and .
A trivializing formalization is ruled out: no supremum or infimum is a bare real sSup/sInf whose junk value on an empty or unbounded set could make an identity hold, the dual sets are nonempty ( resp. is admissible), is an infimum in rather than a real sInf, and the minimum for is stated with attainment (IsLeast).
Beyond the paper. Two variants are posed beside the faithful items. A corrected Proposition 2.74 adds the hypothesis that is finite: at and exponentially distributed, for every while , so the printed minimum does not exist. A corrected (2.101) replaces the constraint by : for the left side is but every with gives ; the book's own rule (2.79) gives mean-one dual variables.
Definitions needed: the quantile function and , the Fenchel conjugate, the expectation of and the minimal loss functional; all are reusable by any formalization of law-invariant deviation measures. Welcome contributions include a measurable-selection lemma for subgradients of a convex function of one variable, Rockafellar's integral conjugacy on (of which Proposition B.3 is a case), and the variant statements.
A risk measure that returns a single number answers the question "how acceptable is this random profit, seen from today?". Multi-period decision problems — portfolio rebalancing, insurance reserves, stochastic programs on scenario trees — need the same question asked at every later date, given the information available then. The answer is no longer a number but a random variable measurable with respect to the information available at that date. Section 2.3 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific, 2007, doi:10.1142/6478), sets up these conditional acceptability mappings axiomatically and gives them a dual representation modelled on the defining relation of the conditional expectation. The conditional average value-at-risk defined there is the building block of the nested risk measures used in multi-stage stochastic optimization (Chapter 3 of the same book), and of the time-consistent risk measures of Ruszczyński and Shapiro (doi:10.1287/moor.1060.0204) and Detlefsen and Scandolo (doi:10.1007/s00780-005-0159-6).
Let be a probability space and a sub--field, the observable information. Fix and let be its conjugate exponent, . Put and , the subspace of classes with an -measurable version. Random variables equal almost surely are identified, and every (in)equality between them holds almost surely. Variables are profits: larger is better.
A map is a conditional acceptability mapping if for all
It is positively homogeneous if for , and upper semicontinuous if, for every , the real functional is upper semicontinuous on . For and the dual function is
For and , the conditional average value-at-risk is a class in such that, for every ,
When is trivial it reduces to the lower-tail average of the left-continuous quantile function of .
For an upper semicontinuous conditional acceptability mapping , every and every ,
and if is positively homogeneous then takes only the values (on ) and (off ), and
Further items of the section, stated faithfully but not milestones:
Theorem 2.51 says that a conditional acceptability mapping is determined by the family of real concave functionals , and that each of these is an infimum of expectations under densities whose conditional expectation is . It turns the axioms (CA1)–(CA3) into a computable object: a dual set, one per observable event, which is what stochastic programs with conditional risk constraints actually optimize over. The converse direction (Theorem 2.52 and Example 2.53) is how the book manufactures conditional versions of the average value-at-risk and of other dual-representable functionals, and Proposition 2.57 lists the properties used later when these mappings are nested over a tree.
None of these results is formalized. Mathlib has conditional expectation, spaces, Hölder
duality and the Hahn–Banach separation theorem, but no Fenchel–Moreau theorem on and no
conditional risk mappings. Prove2Me poses, as an open problem, Ruszczyński and Shapiro's
representation of lower semicontinuous conditional risk mappings
(CondRiskMap.Repr.theorem_1); it is stated pointwise in on abstract paired spaces with
loss variables, not in the integrated form over events used here. Two of the printed statements are false as stated, and the mission
records this: see Beyond the paper below.
The obvious route to (2.45) applies the Fenchel–Moreau theorem to and then shows that the dual function is off the constraint set. The first step needs the biconjugation theorem for concave upper semicontinuous real functionals on , with the dual identified as , for every including where the dual is ; none of this is in Mathlib. The second step must handle the constraint as an equality of conditional expectations, not of expectations. For Theorem 2.52 the natural argument builds a measure on from the infimum and takes its Radon–Nikodym derivative; the additivity of that set function is exactly what fails for general .
is Lp ℝ p P with 1 ≤ p, p ≠ ∞, and is Mathlib's subspace
lpMeas ℝ ℝ m p P of classes a.e. equal to an m-measurable function, where m ≤ mΩ is
; the dual exponent is given by p.HolderConjugate q. Pointwise axioms are almost
sure. is Mathlib's P[Z|m]. Every infimum, and the dual function
, is computed in EReal, so an empty constraint set gives , an unbounded one
, and no infimum has a junk value; the difference always has a
real first term. Upper semicontinuity is that of the real functionals indexed by ,
as the book defines it — reading it as upper semicontinuity of the map into , or
replacing the infimum by an unconstrained one over all of , would change the theorem. The
conditional is a predicate on classes in , never a construction:
its existence is a stated result, not an assumption. Profits, not losses: the lower tail is
averaged. Version-independence (Definition 2.55, used in Proposition 2.57(i)) is stated
pointwise: the conditional is almost surely one fixed function of the
conditional distribution function of (2.56), for every .
Needed infrastructure: the Fenchel–Moreau theorem on , the – duality pairing, and Radon–Nikodym on a sub--field. All three are reusable well beyond this mission.
Beyond the paper. Two corrected variants are posed beside the faithful statements. Theorem 2.52, corrected (findings F1, F2) adds that is bounded in and closed under pasting along ; without pasting, on makes the right side of (2.50) non-additive in , and without boundedness with makes it . Proposition 2.57, corrected (finding F3) replaces the second inequality of (2.58), , which fails on two equally likely points with , trivial, full and , by . Disproofs of the faithful Theorem 2.52 and of the faithful Proposition 2.57 are welcome contributions, as are proofs of the variants.
Risk functionals assign a number to an uncertain profit and are used as objectives and constraints in portfolio selection, insurance and energy planning. Since the axiomatization of coherent risk measures by Artzner, Delbaen, Eber and Heath (Math. Finance 1999), the standard way to understand such a functional is through a dual representation: the functional is written as a worst case of expectations under a family of probability densities, penalized by a convex or concave function of the density. Föllmer and Schied (Finance Stoch. 2002) and Ruszczyński and Shapiro (Math. Oper. Res. 2006) established this representation for convex risk measures on and on paired spaces. Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007), develop the same theory on the profit side, for acceptability functionals (larger is better) and deviation risk functionals, on spaces. Section 2.2 of their book recognizes these functionals by their dual representations. This mission formalizes that section and the conjugate duality of Appendix B it rests on.
Let be a non-atomic probability space: no measurable with has every measurable subset of probability or (the book assumes this throughout). Fix and with . Write and , paired by
A functional is a map ; constants are constant random variables. An acceptability functional satisfies
Positive homogeneity (A4) is for , and strictness (A5) is . A deviation risk functional satisfies (D1) , (D2) convexity, and (D3) . The acceptance set of is , and a set defines .
The concave conjugate and the convex conjugate are
and . A convex-type is proper if everywhere and somewhere; a concave-type is proper if is.
A proper upper semicontinuous acceptability functional satisfies, for every ,
and conversely, a functional represented in this form by any proper functional in place of is upper semicontinuous and satisfies (A1)–(A3). Up to semicontinuity, acceptability functionals are exactly the penalized infima of expectations under probability densities.
Further items, not milestones: the first sentence of Theorem B.1 ( is the largest l.s.c. convex minorant of a proper ) and the deviation half of Corollary 2.32, representation (2.12), each stated as printed.
The corollary is the profit-side, form of the dual representation of convex risk measures. It turns a property of a functional into a constraint on its dual domain. Translation equivariance becomes the requirement that the densities have mean one, and monotonicity becomes the requirement that they be nonnegative. This is how later chapters of the book compute with the average value-at-risk, distortion functionals and multi-period functionals: each is specified by its supergradient set. A machine-checked version gives these computations a common, verified foundation.
The results are classical and proved on paper; none is formalized in this form. The platform holds a loss-side analogue on abstract paired spaces with signed-measure duals (ConvexRiskFn.Dual.theorem_2_2) and a Fenchel–Moreau theorem in the same setting (ConvexRiskFn.Dual.theorem_2_1). Neither states the /, profit-side, density-constrained representation (2.11). Formalizing the chapter also checks its statements: three printed statements are false as written, and the mission poses a corrected form beside each faithful one.
Representation (2.11) needs the Fenchel–Moreau theorem in infinite dimension, for an extended-real concave functional, on with dual . That requires Hahn–Banach separation of a closed convex hypograph and the identification of the dual of , and Mathlib provides only parts of the latter. Upper semicontinuity in the norm topology must be converted to weak semicontinuity, and the value must be handled throughout. Example 2.28 of the book shows that dropping upper semicontinuity breaks the representation, so the hypothesis cannot be avoided. The restriction of the infimum to densities with , is a separate step: one must show that every other has . The first sentence of Theorem B.1 fails as printed when has no continuous affine minorant, so the natural "largest l.s.c. convex minorant" route to the biconjugate needs care.
Functionals are EReal-valued maps on Mathlib's Lp ℝ p P, with p ≠ ⊤, [Fact (1 ≤ p)] and [p.HolderConjugate q]. The pairing is the Bochner integral of , integrable by Hölder's inequality. Conjugates are EReal suprema and infima over the whole space, so they are never a junk default. (A2), (D2) and (A4) are written as the book's inequalities in EReal, where . Non-atomicity is the book's atom definition, which is stronger than Mathlib's NoAtoms. Semicontinuity is for the norm topology. "Proper" follows the concave or convex notion of Appendix B. The book's abstract dual pair is instantiated as with , the example it gives itself.
A trivializing formalization would take the infimum in (2.11) over all of (Fenchel–Moreau alone), or replace by a real-valued function and so discard the values that encode the constraints. The goal does neither: the infimum ranges over the densities, and is the EReal conjugate.
Beyond the paper. There are three variants, each a corrected statement beside its faithful one:
deviation_representation_corrected (F1): (2.12) prints where is meant. For and , , but gives .fenchel_moreau_largest_corrected (F2): Theorem B.1's first sentence needs . For on , is not the largest l.s.c. convex minorant.acceptabilityOfSet_properties_corrected (F3): Proposition 2.27(i) needs a monotone (a closed set built from line segments gives but ), and (v) holds only for ().A complete development needs Fenchel–Moreau for extended-real functionals on , the duality for , and coupling constructions on non-atomic spaces for version independence. All of these are reusable well beyond risk theory. Contributions of any of these pieces, or proofs of the corrected variants, are welcome.
A switch or wireless network can have several queues ready for service while its hardware permits only certain combinations to be served together. A scheduler must choose a feasible combination repeatedly as new packets arrive. The question is whether this local sequence of decisions keeps the queue process stable whenever the arrival rates fit within the network's service capacity. Kelly and Yudovina formulate this question for finite service schedules and independent Poisson arrivals in §7.8 of Stochastic Networks.
MaxWeight scheduling gives larger queues greater influence over the choice of schedule. An exponent controls how strongly queue length affects priority. The chapter's target is a stability guarantee for every positive exponent, rather than a guarantee confined to the familiar linear weighting. The supplied Lecture Notes PDF states this as Theorem 7.13, printed page 180, and develops supporting analytic questions in Appendix D.
Let be a finite nonempty set of queues. A schedule is a vector describing how many packets each queue can serve in one time slot. The feasible schedule family is finite and nonempty. It is downward closed: reducing any schedule coordinate leaves a feasible schedule. This includes the possibility of unused service when a selected queue has fewer packets than the schedule permits.
The admissible region is
It describes arrival rates dominated by an average of feasible schedules. The interior used here is the ordinary interior in .
Fix . At queue vector , a schedule is drawn from a fixed probability distribution supported on the maximizers of . New arrivals in the slot are independent Poisson variables of means , independent of the scheduling randomization and the past. The next queue vector is
These laws specify a homogeneous Markov chain on the countable state space . They follow the general model in §7.8 and the explicit empty-queue convention in Example D.4, printed page 213.
The goal is Theorem 7.13: for , the MaxWeight- queue chain is positive recurrent. In return-time notation,
This retains every positive value of and the full queue process.
Three supporting targets are selected from the same supplied source. Proposition D.1 states the Foster–Lyapunov criterion for an irreducible countable chain and an arbitrary finite exception set. A nonnegative function with drift at most outside that set and at most inside it yields finite expected return to the set from every starting state and positive recurrence.
Exercise 7.18 concerns the weighted drift
It asks for constants and finite such that
Exercise D.1(3) asks for finite moments of , where is a finite service bound and is Poisson, and for the tail term
to tend to zero as for fixed . The source locations are printed pages 210–211, 182, and 214–215 respectively.
The recurrence conclusion concerns repeated operation over an unlimited number of slots. It asserts a finite mean return time to each queue state under the specified policy. It does not require an explicit formula for the stationary distribution, nor does it prescribe a numerical delay guarantee. The result therefore identifies a capacity regime in which this queue-based scheduling rule is stable, while leaving performance within that regime as a separate question.
The formalization contribution is the connection between a concrete random scheduling transition law and recurrence on an infinite state space. Its reusable components include the capacity region of finite schedules, capped-service queue transitions, extended return expectations, and the Poisson envelope estimates. The textbook presents the theorem as an established result with a proof sketch. The theorem items here are statements awaiting proofs; compilation verifies their Lean syntax and types, not their mathematical proofs.
Negative drift by itself is insufficient for the recurrence conclusion. The distinctions between negative drift, drift bounded away from zero, and control of upward increments matter in the chapter's discussion, printed pages 180–181. Arbitrary positive real exponents also require attention at empty queues and to unbounded Poisson arrivals.
The sketch's equality between actual departures and a chosen schedule fails when a positive queue is shorter than the proposed service. This is a proof gap, not a counterexample to the stability theorem. Appendix D additionally switches between conditioning on the full vector and conditioning on one coordinate in (D.5). Those conditional expectations need not agree for coupled schedules. The selected statements retain actual capped departures and avoid relying on that ambiguous display. Completing the analytic link to the goal remains part of the proof task.
Queue and schedule coordinates are natural numbers, rates are nonnegative real numbers, and the exponent is an arbitrary positive real. The schedule family is a finite set of vectors. Random tie rules are stationary probability kernels supported on the maximizing schedules; the source specifies no particular distribution among ties. The norm in Exercise 7.18 is made Euclidean explicitly. Constants there are chosen before the queue vector is quantified, so they cannot depend on the current state or time.
Return times are represented by extended nonnegative sums of survival probabilities. Consequently, an event of never returning has infinite expected cost. Real drift sums have explicit absolute-integrability conditions. In the queue drift and Poisson moment items, integrability is a conclusion, not an assumed substitute for analysis. The Poisson tail term is an unconditional tail integral, including when its conditioning event would have probability zero.
No selected statement contains an unspecified term or a high-probability claim; there are therefore no numerical asymptotic constants to instantiate. Exercise D.1 is included only through its explicitly numbered part (3). The remaining parts, (D.5), congestion-control optimization results, and the switch-specific matching example are outside this mission's theorem list. No variants are posed.
Stability is not defined as negative drift, and the goal is not restricted to or a finite truncation of the queue space. Mathlib supplies probability mass functions, product measures, Poisson laws, real powers, and topology. The local definitions supply the scheduling and recurrence interfaces needed to state the targets.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a; correspondence with a particular published printing has not been verified.Food delivery platforms such as Uber Eats, DoorDash and Meituan let a restaurant serve customers who never enter it, but they also charge those customers a delivery fee and share the restaurant's kitchen with its walk-in trade. Whether the platform helps or hurts the restaurant is a question restaurant owners, platforms and regulators all ask. Chen, Hu and Wang (Management Science, 2022) answer it in a stylized game: a restaurant whose kitchen is a queue, a platform that sets a fee, and two kinds of customers who decide where to eat by comparing expected waiting costs. Their first main result, Proposition 1, describes how the equilibrium changes as more customers become able to order through the platform: below a critical mass nothing changes for the restaurant, and at the critical mass the restaurant abruptly turns into a delivery-only kitchen. The analysis builds on the unobservable-queue joining games of Edelson and Hilderbrand (1975) and Hassin and Haviv (2003).
A kitchen serves meals at rate . At total joining rate the expected wait for food is . A meal is worth to a customer. Walk-in customers pay the food price and incur waiting cost rate ; food-delivery customers pay plus the delivery fee and incur the smaller waiting cost rate . Their expected utilities are
and balking gives . Tech-savvy customers arrive at rate and may walk in, use delivery or balk; traditional customers arrive at rate and may walk in or balk. The delivery-worker pool is unlimited and costless.
A customers' equilibrium under is a profile of joining rates with in which every option used by a positive rate is a best reply at , and an arrival stream that does not fully join is no better off joining. Ties between delivery and walking in at go to delivery. The game has three stages. The restaurant sets . The platform then sets to maximize . Finally customers play an equilibrium. The restaurant maximizes , where . A subgame-perfect equilibrium (SPE) combines a customers' equilibrium after every , a best-response fee after every , and an optimal price . Its outcome is , , , , , and the social welfare , the total surplus of all stakeholders.
Assume , , , . There is such that for every there are and an SPE for every whose outcome, viewed as a function of , satisfies the following. With if and otherwise:
The thresholds are existential, as printed. The milestones pin them to the values the proof constructs: is the root of in , , is the smallest root of , and has a closed form (Online Appendix p. 23).
The paper's own chain (Online Appendix C.1): Lemma C.2 (customers' equilibrium), Proposition C.3 (platform's best response), Corollary C.2 (restaurant's profit curve), Lemmas C.6–C.8 (the three profit curves, their maxima and intersections), Proposition C.4 (restaurant's optimal price), and Corollaries C.3–C.4 (platform profit and welfare in equilibrium). "We have Proposition 1 from Proposition C.4, Corollary C.3 and Corollary C.4."
The result separates two regimes. In the delivery-irrelevant regime, more tech-savvy customers only change who eats at the restaurant; the price and the throughput are fixed while the platform's profit and welfare grow. Past the critical mass , the restaurant raises its price and serves only delivery customers, and the platform's profit and social welfare drop. This is the basis of the paper's answer to "friend or foe" and of its later analysis of revenue-sharing contracts that restore coordination (Proposition 2, not part of this mission).
The paper's proof is a long chain of case analyses over piecewise-defined profit functions, spread over 22 pages of appendix. A machine-checked version settles every boundary case. Reading the proof closely has already turned up several (findings F1–F9): ties in the restaurant's optimum at and at ; table rows that are wrong outside their derived price range; an implicit hypothesis ; the degenerate case ; a tie rule that needs a precise reading; and a boundary error in Lemma C.7(3). The definitions of the queue-joining equilibrium and the three-stage Stackelberg game can be reused for other platform and queueing games. None of this has been formalized before.
The equilibrium is defined by optimality conditions, so each stage needs an existence-and-characterization argument, not a formula check. The customers' stage has mixed strategies with three utility comparisons and a tie rule. The platform's profit is piecewise in , with branches that switch depending on and on whether . The restaurant's profit is the upper envelope of three curves whose maxima must be compared through the cubic defining and a quartic-type equation defining . The obvious approach, substituting the tables, fails at the boundaries. At and at the restaurant has two optimal prices with different platform profits, so "the" equilibrium price is not unique. The jump statements are therefore about a particular equilibrium selection and about one-sided limits.
All objects live in FoodDeliv.Decentral, with one definitions file, FoodDeliv_Decentral_Model. Conventions:
Beyond the paper. No variant items are posed. The findings file records the evidence for each deviation above.
Contributions welcome: proofs of the milestones in any order; existence of customers' equilibria for every under the tie rule; reusable lemmas on unimodal functions, cubic roots and one-sided limits of piecewise functions.
Unitary representations turn symmetries into operators on Hilbert spaces. For ordinary locally compact groups, the associated group -algebra lets one study these operators through a single algebraic object. A Lie supergroup adds odd infinitesimal symmetries to an ordinary Lie group. Its unitary representations must respect both the group action and those odd operators. Neeb and Salmasian construct a -algebra that captures this combined structure Neeb–Salmasian 2015. The representation correspondence is the point at which their construction becomes useful: a representation of retains precisely the data of a unitary supergroup representation.
The paper subsequently uses this bridge to discuss direct integral decompositions through the -algebra. This mission concerns the bridge itself, Theorem 6.4. Its input is not a special connected or nilpotent group: the paper works with an arbitrary finite-dimensional Lie supergroup. The later CCR results in §7 add hypotheses and are outside this mission.
A finite-dimensional Lie supergroup is a pair . Here is a real Lie group and is a real Lie superalgebra. Its even part is the Lie algebra of . The group acts smoothly on the superalgebra by an adjoint action whose even restriction is the derivative of conjugation; differentiation of the action recovers the superbracket. These are the conditions of Definition 2.1, including the finite-dimensional convention stated just after it.
A unitary representation consists of a graded complex Hilbert space , a strongly continuous unitary action of preserving that grading, and a real-linear superalgebra action on the space of smooth orbit vectors. On even elements, equals the derived group action. On odd elements, is symmetric, and the odd action transforms under through the adjoint action. This is Definition 2.3, including its parity and bracket requirements.
The paper adjoins a parity element and writes . A test function on this group is a pair of smooth, compactly supported complex functions on . Using the complex universal enveloping algebra, the authors form an algebraic crossed product . A word and a test function act in each unitary representation by the bounded operator . The norm of an algebraic element is the supremum of the norms of these represented operators; completion after quotienting its zero seminorm gives the non-unital -algebra §§3–4.
A star representation of on is nondegenerate when the span of its image applied to is dense. A morphism between two unitary supergroup representations is a bounded, even, complex-linear operator intertwining both their -actions and their -actions on smooth vectors. A morphism between -algebra representations intertwines every element of .
The first targets are the uniform bound of Proposition 3.2 and the smoothness statement of Proposition 5.1. For each word and test pair , the same constant works for every unitary representation:
The left multiplier orbit is smooth for every . The construction from a nondegenerate representation also identifies its smooth vectors with the represented algebraic core, as in Lemma 6.2. These are the analytic steps named in the milestone list.
The goal is Theorem 6.4. Propositions 6.1 and 6.3 give mutually inverse assignments on objects, and Theorem 6.4 retains the same intertwiners:
Thus each unitary representation yields exactly one nondegenerate representation agreeing on every generator, each nondegenerate representation comes from exactly one unitary supergroup representation, and a bounded operator intertwines one pair exactly when it intertwines the other. The goal includes all three clauses.
The result lets questions about unitary Lie supergroup representations be transferred to a -algebra without losing the odd infinitesimal action or the morphisms. In the paper, this is the foundation for the later direct integral discussion and CCR criteria. Without the equivalence, properties of would have no stated connection to decomposition of unitary supergroup representations §7.
The mathematical result is proved in the cited paper; the local Lean declarations are open statements. A complete formal development would add machine-checked proofs for the uniform operator bounds, the algebra and multiplier facts, reconstruction of the odd action, and the categorical equivalence. The reusable parts include smooth-vector actions, integrated test-function operators, and a universal bounded family of representations.
The odd infinitesimal operators are defined on , not automatically as bounded operators on all of . Integrating against a test function supplies smooth vectors, but it does not by itself give a bound for an arbitrary word in the odd and even operators that is uniform over every representation. That uniformity is needed to construct one -norm. In the reverse direction, a nondegenerate representation of first gives bounded operators; recovering the derived action on precisely the smooth core requires the multiplier and smoothness statements. An object-level bijection alone would still miss the paper's assertion about intertwiners.
Lean models as a finite-dimensional smooth real Lie group, with its Mathlib group Lie algebra and a finite-dimensional real normed space. The superbracket and odd adjoint action are fields of a Harish–Chandra pair. Smoothness uses , not analyticity. The group is neither assumed connected nor second countable. A left Haar measure is fixed. The Hilbert spaces quantified in the mission belong to Type; the index of all such unitary representations belongs to Type 1.
The test space is encoded as pairs of functions, and the enveloping-algebra elements needed here as finite words. is the closed non-unital star subalgebra of the bounded product of operator algebras generated by their representation families. This uses all Type-small unitary representations; the paper takes unitary-equivalence classes of cyclic ones, which yield the same norm through its Remark 2.5. The algebra depends only on and Haar measure, and acts on itself. This rules out a choice of algebra or an off-domain operator value that would make the correspondence automatic.
The published smooth-orbit and vector-integral definitions from van Dijk–Neeb–Salmasian–Zellner are reused. Completing this mission calls for the Dixmier–Malliavin factorization, Gårding smoothing, bounded operator estimates, non-unital -algebra representations and multiplier actions. Contributions proving those general tools or the source-labelled milestones are within scope. The generator family is represented through vectors rather than an operator-norm Bochner integral, whose measurability is unavailable for a merely strongly continuous representation.
The relative entropy of entanglement measures how distinguishable a multipartite quantum state is from all fully separable states. In finite dimensions it is a standard entanglement measure, but infinite-dimensional systems raise a basic analytical problem: the measure may take the value , and finite-rank approximations do not automatically control its behavior at a limit state. Shirokov's analysis identifies a broad class of states at which the direct relative entropy of entanglement is finite and lower semicontinuous. The result applies when all but possibly one marginal state satisfy the FA-property, a spectral condition that includes useful finite-entropy states without requiring finite-dimensional Hilbert spaces.
The paper relates the direct measure to a universal extension formed from local finite-rank compressions. This mission isolates the part of Theorem 2 A) and the source results needed to reach it. A later paper by Lami and Shirokov addresses more general global lower semicontinuity questions using a different operator model and hypotheses; its statements are related work, not imports into this mission. Shirokov, §4.3; Lami–Shirokov.
There are parties , with separable Hilbert spaces . A state is a positive trace-class operator with trace one on their joint system. Its marginal is obtained by tracing out every party except . A product state is a tensor product of one state per party. The set of fully separable states is the trace-norm closed convex hull of product states. Closure matters in infinite dimension: restricting to finite convex combinations would change the infimum below. Shirokov, pp. 10–11, (26).
Write for Lindblad's quantum relative entropy, including the trace correction for unnormalized positive operators and the value on support failure. The direct relative entropy of entanglement is
The von Neumann entropy and are extended nonnegative real quantities in natural-logarithm units. A state has the FA-property when its eigenvalues admit nonnegative numbers with and . In particular, the FA-property implies finite entropy. The set consists of joint states with the FA-property on at least marginals. Shirokov, pp. 2, 4, 14, (1), (34).
For each party, a finite-rank orthogonal projector compresses the joint state. The universal extension takes the supremum of the homogeneous values of all such local compressions. A compressed positive operator with trace is valued as ; the zero operator has value zero. Local spectral projectors built from the marginals define the approximation used in Theorem 1. Shirokov, pp. 7, 12–13, (17), (31).
For , . For every sequence of states in trace norm,
The sequence itself may lie anywhere in the full state space. This is the sequential lower semicontinuity assertion (35), together with finiteness, in Theorem 2 A).
The milestones, in attack order, are: the FA entropy consequence (p. 4); the pure-state separable comparison of Lemma 3; the -convexity of (first sentence of Theorem 2 E)); the upper bound (28) by any marginal entropies,
the concavity-defect bound (27), ; membership of in ; the -class assertion of Theorem 1; the relative-entropy inequality of Lemma 1 for positive maps with trace-preserving sum; the comparison ; lower semicontinuity of ; and the equality on (Theorem 2 B)). These are claims made in the paper, with the portions outside the route explicitly scoped in the item descriptions. Shirokov, pp. 4, 8, 11, 13–15, 20, 25.
The theorem gives a stable finite value of at every state in : approximating sequences cannot converge there while hiding a smaller limiting value. This matters when infinite-dimensional states are approximated by finite-rank or energy-constrained states, because pointwise convergence of operators alone does not control an extended-valued entanglement measure. The equality with also identifies the direct measure with a globally lower semicontinuous construction on the stated domain. Shirokov, Theorem 2 and discussion in §4.3.
The mathematical result is proved in the source paper. The formalization work is to express its spectral FA condition, multipartite partial traces, trace-norm separability, finite-rank compression, homogeneous extension, and extended-real inequalities in Lean, then prove the milestones and goal. The published P01 definition already supplies von Neumann entropy and Lindblad relative entropy; the propositions in this mission are open Lean statements, not machine-checked proofs. This shared infrastructure can support other infinite-dimensional quantum information results involving separability and marginal entropies.
A direct argument from the infimum defining cannot simply exchange that infimum with a state limit: the separable comparison state that nearly minimizes at one point need not remain useful along a convergent sequence. Infinite values also make real-valued continuity bounds insufficient. The paper's theorem therefore has to coordinate a finite-entropy estimate on marginals with control of local finite-rank approximations and a lower semicontinuous extension. The approximation estimate is uniform over a class of functions, with the rank threshold and error sequence chosen before the function. Shirokov, Theorem 1 and proof of Theorem 2 A).
Each is represented as for a countable basis index type. Parties are indexed by , and the joint basis uses their dependent Cartesian product. The state topology is the trace-norm topology of the published P33 state structure. Entropy, relative entropy, and take values in ; no real-valued surrogate replaces an infinite value. The FA-property requires an actual orthonormal eigenbasis tied to the state's coefficients. Its partition sum is computed in , so divergence cannot default to zero. The definition of says at least FA marginals and does not impose FA on the sequence in the goal.
The class is represented with a finite set of FA parties in place of the first parties, reflecting the paper's relabeling symmetry. Within that class, is converted to a real number only on the finite-entropy domain. The universal extension uses all finite orthonormal local families and the homogeneous convention for compressed positive operators. The setting also defines countable separable decompositions, finite-rank projectors, the spectral approximation relation, binary entropy in nats, and positive linear maps on the trace class. The proviso of (27) that "all the involved quantities are finite" (p. 11) is stated as finiteness of at the two mixed states. These definitions and the cited P01/P33 libraries are the reusable work. A definition of FA that every state satisfies, a separable set without trace closure, or a real that discards would trivialize or alter the target.
The paper also states a regularized case. It is outside this mission: its proof in version 2 invokes propositions by broken “??” references that are absent from the source. The hatted-class and -class portions of Theorem 1, the regularized equality in Theorem 2 B), and the entanglement-monotone part of the universal-extension bullet are likewise outside these milestones. Contributions proving the stated Lean milestones, improving the common operator definitions, and then proving the goal are welcome.
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.
Let with its standard basis , and let be the diagonal algebra. Its minimal projections are . A state is represented by a positive semidefinite matrix of trace one. A pure state has density matrix for a unit vector . The state of obtained by restricting records the diagonal probabilities Uhlmann, p. 4, equations (1)–(3).
Write , with . The diagonal entropy is . The convex roof is the infimum of over finite decompositions into pure states with positive weights summing to one. A decomposition attaining the infimum is optimal. Uhlmann's entropy of at is Uhlmann, pp. 4–5, equations (4)–(7).
An affine functional supports if on all states and equality holds at some state. Its contact set is . Given , define as the intersection of all contact sets whose support functional touches at . This intersection is compact and convex, contains every pure state used by an optimal decomposition of , and is a region on which is affine Uhlmann, pp. 6–7, Lemma 3 and equation (10). A transposition swaps two and fixes the remaining minimal projections. It transforms a density matrix as Uhlmann, p. 8.
For a rank two state fixed by a transposition , Uhlmann's Lemma 6 asserts equivalence of three statements:
The milestone list follows the paper's supporting results: finite optimal decompositions with rank bounds (Lemma 1), comparison on an -set (Lemma 2), compact supporting contact sets and their covering (Lemma 3), the intersection properties of (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.
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 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.
An optimal pair alone does not immediately determine every extreme point of . 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.
Matrices are indexed by Fin d, so the paper's indices become . 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 . The real infimum defining 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 , as in the paper's equation (9). The set 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, , 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 . 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.
A quantum repeater is judged by how much it beats direct transmission over a point-to-point link. The natural yardsticks are the two-way assisted capacities of the link's channel : the quantum capacity and the secret-key capacity , the best rates of entanglement and key that two parties can obtain over many uses of when unlimited two-way classical communication and local operations are free. Computing them exactly for a given channel is rare, because it requires a lower and an upper bound that meet.
Pirandola and Laurenza (arXiv:1512.04945v2, 2016) obtain such matching bounds for a family of channels. The lower bound is the coherent information of the channel (with its reverse version), which is achievable by the hashing protocol. The upper bound is the entanglement flux , the relative entropy of entanglement of the channel's Choi matrix, which bounds for channels that can be simulated by teleportation. For the qudit dephasing channel the two bounds coincide, which gives (Eqs. (20) and (95)). This mission formalizes that coincidence.
Fix a dimension and the computational basis of a qudit. Let and let be the generalized phase operator, . For a dephasing probability define the binomial weights
and the qudit dephasing channel, given by its Kraus operators,
Write and (with ) for its Shannon entropy.
The Choi matrix of a map on matrices is , where . The first tensor factor is the reference , the second the channel output . With the von Neumann entropy :
The paper's candidate separable state is .
For every and :
The lower and the upper bound on the two-way capacities therefore meet. The statement keeps and free and asserts exact values, not numerical constants.
The result. The coincidence of the two bounds pins down and of the qudit dephasing channel for every and , which gives the repeaterless benchmark for any qudit link dominated by dephasing. At it recovers the qubit dephasing benchmark of the same paper (Eq. (75), with , which the binary entropy does not see). Combined with the operational facts the paper imports (the hashing inequality and the bound of by the flux for teleportation-covariant channels), it yields the capacity formula (95).
Formalizing it. The paper's computation is complete but terse. The formalization makes three implicit points explicit: the support of the Choi matrix lies inside the support of the rank- state (so is taken on its support); the claim of " non-zero eigenvalues" in (91) fails at , while the entropy identity does not; and (45) needs trace preservation as well as unitality. The results are proved in the paper and, as far as the platform's catalogue shows, formalized nowhere. Eq. (68) and Eq. (45) are reusable lemmas about arbitrary states and unital channels.
The calculation on the page is short; the difficulty lies in what it leaves to the reader. The entropy identity (91) asks for the spectrum of a matrix that is not diagonal in the computational basis, while the von Neumann entropy is defined through the matrix functional calculus, so "diagonalizing" has to be made precise. The state has rank in dimension : the relative entropy against it is finite only because of a support inclusion the paper does not mention, and a computation that ignores the kernel of does not establish the value. The upper bound needs to be separable in the sense of the infimum, a finite convex combination of product density matrices, not merely diagonal. Finally, the coherent information is a difference of entropies of a partial trace and of the full Choi matrix; equating it to requires both that the output marginal is maximally mixed and the entropy identity (91).
Qudit indices are Fin d, with (and [NeZero d] where an instance needs it); is real with . is a matrix power, , and the channel is the published QAlgorithms.krausApply of the Kraus family . The Choi matrix is the published QAlgorithms.idTensorSuperop applied to maximallyEntangledProjector d (entries on ), the reference being the first factor of Fin d × Fin d. Entropies are in bits with : QAlgorithms.vnEntropy for states and a local Shannon entropy for the weights. The partial traces are QAlgorithms.traceLeft (over the reference) and QAlgorithms.traceRight (over the output). The relative entropy and are the published relativeEntropyBits and relativeEntanglement (Umegaki entropy divided by , off support, infimum over IsSeparableDensity, values in ). The real bound is embedded with ENNReal.ofReal; since , nothing is lost.
None of the defined quantities is given by its closed form: the Choi matrix is computed from the channel, is the infimum over all separable states (not or an infimum over diagonal states), and is defined from partial traces, not as . This rules out the trivializing formalization in which a milestone or the goal holds by definition. The bound alone holds for every state; the goal's bound is .
The operational capacities and of Eq. (95) are not formalized. They are defined over adaptive LOCC protocols with private-state targets, which have no substrate on the platform. The paper also does not prove the two bridges from them to the bounds: it imports (Eq. (2), from Pirandola et al.) and the hashing inequality (from Devetak and Winter). For the same reason, the reverse inequality is not stated, since the paper obtains it only through the hashing bound. Teleportation stretching, convexity of the flux, the bosonic Gaussian channels and the erasure channel are outside this mission.
Contributions are welcome at every level: the spectrum of circulant blocks, the support calculus of the Umegaki entropy, and the separable decomposition of diagonal states are all reusable beyond this mission.
A Gittins index assigns a number to an uncertain arm in a discounted bandit problem. The index converts a sequential choice, where an agent may keep gathering information or retire, into a tax threshold for playing the arm. Computing it generally requires an optimal stopping calculation. A Bayesian upper confidence bound, by comparison, is a quantile of the posterior distribution and is directly available for a Gaussian posterior. Russo's note asks how closely these two quantities agree when the agent is patient and the discount factor approaches one. The answer is an asymptotic identity for a Gaussian arm, not a finite-discount formula. Russo, 2019, pp. 1–3.
The note places its result alongside work on computational approximations of Gittins indices and finite-horizon index policies, but aims at the conceptual relationship with Bayesian confidence bounds. It appeared as an arXiv preprint in 2019; this mission follows that version's theorem numbering and formulas. A later journal publication appeared in Operations Research in 2021, but its numbering is not used here.
One arm has an unknown quality . The prior distribution is Gaussian, , where and . Playing the arm at time yields , where the observation noises are independent Gaussian variables of mean zero and variance . After observing , the posterior is . Its mean and variance follow the Gaussian update (1) of Russo, p. 2. In particular, .
For each play, the agent pays a tax . The agent may retire, receiving zero thereafter. At discount factor , an admissible retirement time uses only the rewards observed through the current time. Its discounted payoff includes the play at : . The value is the supremum of the expected payoff over these retirement times. The Gittins index is the supremum of taxes for which the value is nonnegative. These are the stopping-time value and fair-tax definition in equations (2)–(3) of Russo, p. 2.
Write and for the distribution function and density of , and . Thus is the prior's upper -quantile, with .
The goal is Theorem 1, p. 3, for each fixed prior mean, positive prior variance, and positive observation-noise variance:
The remainder is an additive quantity tending to zero; the claim does not assert equality at any fixed discount factor. The paper reduces the general prior to a standardized one. Its intermediate targets are the normal-quantile asymptotic, explicit bounds on , an upper bound obtained from noiseless information, and a matching lower bound from an admissible exploration policy. They appear as the mission's milestones, along with the posterior identities the lower bound uses. Russo, pp. 3–6.
The theorem identifies the limiting tax threshold with a familiar statistical quantile. It explains why a Bayesian upper confidence bound can approximate the Gittins priority of an arm when the effective horizon is large. It does not state that a quantile policy is exactly optimal at a fixed horizon or discount factor, and the paper's limitations section notes that significant observation noise relative to the horizon can make exploration costly. Russo, pp. 3, 7.
For a formal development, the reusable pieces are a Gaussian stopping-time model, the fair-tax index, the normal tail and positive-part estimates, and posterior update identities. The asymptotic theorem is proved in the source paper but has no machine-checked proof in this mission. Its local Lean statement is a target with sorry; the same applies to the milestone theorems. The definitions and a small sanity lemma compile in the pinned environment. Contributions that establish the source's stated bounds, their probabilistic prerequisites, or the final asymptotic reduction are relevant.
The direct idea of replacing the index by a posterior quantile at each fixed does not establish the theorem. The index optimizes over retirement times that adapt to noisy observations. A decision maker who sees without noise has a larger value, so the resulting expression supplies an upper bound, but it does not give a lower bound for the original information structure. The paper's matching lower estimate uses an actual reward-adapted policy and tracks both the cost of initial sampling and the benefit of later commitment. The two estimates must agree to an additive , not merely at their leading order. Russo, §§3.3–3.4, pp. 4–7.
Lean uses the canonical probability space : the first coordinate is , and the second is the independent noise sequence. The model measure is the Gaussian prior times an infinite product of Gaussian noise laws. The reward history at time generates . An admissible -valued stopping time has ; means never retire. The stopped reward is a countable sum. The index is the supremum of the nonnegative-value tax set. Only the discount domain is used in fixed-discount statements; limits approach one from below. Variances are nonnegative reals at the Mathlib Gaussian interface, with strict positivity assumed in the theorem statements. The paper suppresses in the index notation; Lean keeps it explicit and arbitrary.
The value is defined from the stopping problem and the index from the fair-tax set. Retirement decisions depend on observed rewards only; giving them access to would change the target. The posterior variance uses in its closed form, correcting a printed error in (1). Lemma 3's limit is , and Lemma 7 uses in its little-o scale; their printed versions are inconsistent with the surrounding derivations. The natural-language item notes identify these corrections. Russo, pp. 2, 4, 6, 9.
Measurements of long quantum spin chains can have outcomes far from their typical values. A large-deviation principle quantifies how quickly the probability of such outcomes decreases with the number of sites. In a classical lattice system this is a standard way to describe rare macroscopic fluctuations; in a quantum chain, observables on overlapping sets of sites generally fail to commute, which makes the corresponding probability laws harder to analyze. Ogata's 2008 paper establishes a full principle for the energy density of any translation-invariant finite-range interaction in a -finitely correlated state. Its introduction explains that earlier spin-chain results covered upper bounds or more restricted observables and states, while the lower bound for general observables remained the substantial issue. Ogata, pp. 2–4
The finitely correlated class includes local states generated from finite auxiliary memory. It is large enough to include mixtures and periodic behavior, so a theorem restricted to a primitive transfer map would miss part of Ogata's statement. This mission targets the printed Theorem 1.2 in its full scope. Ogata, p. 4
At each site let be the algebra of complex matrices. On sites , the local algebra is the -fold tensor product, represented as matrices whose rows and columns are spin configurations. A finite-range translation-invariant interaction assigns a Hermitian operator to each finite set of sites , with the same term on translated sets and with when the diameter of exceeds a fixed range. Its finite-volume Hamiltonian is
The sum includes the scalar term associated with the empty set. The interaction need not be nearest-neighbor and may have a term on any finite pattern within its range. Ogata, pp. 2–3
A -finitely correlated state is specified by a finite-dimensional auxiliary algebra , a unital completely positive map , and a faithful stationary state on . Iterating gives a compatible local state on sites. The probability measure is the spectral distribution of in : for a Borel set , it assigns the state weight of the spectral projection corresponding to . These local restrictions determine the distributions used in the theorem. Ogata, pp. 3–4
The goal is a good rate function : is lower semicontinuous and each set is compact for finite . For every closed and open in , Theorem 1.2 asserts
One rate function serves both inequalities and every eligible set. The statement asserts existence, without imposing a formula for or a primitivity condition on the auxiliary map. Ogata, pp. 3–4
The milestone list includes the paper's Gärtner–Ellis theorem, the spectral-law exponential-moment identity behind equation (1), the two-sided order estimate (15) for a gapped auxiliary map, the regrouping of consecutive sites into one site, under which the same state is generated by the -th iterate of the transfer map and , and the differentiable limiting pressure under condition (14). In the last target, the pressure is the limit of for every real . These are narrower claims with separate hypotheses; none replaces the full goal. Ogata, pp. 4–5, 12–15
The theorem gives an exponential-scale description of the energy-density distribution for all translation-invariant finite-range interactions in this state class. The upper bound controls probability on closed sets; the lower bound supplies the matching guarantee for open sets. Compact sublevel sets prevent low-rate mass from escaping to infinity. The result is already proved in Ogata's paper; the remaining work here is a machine-checked development of the statement and its supporting mathematics. Ogata, Theorem 1.2
Formalizing the finite-dimensional transfer construction, its spectral measures, and an extended-valued LDP vocabulary would also make these objects available for later spin-chain results. The goal itself is not currently accompanied by a machine-checked proof in this mission. The Gärtner–Ellis and auxiliary-map statements are likewise proof targets, not asserted as solved Lean facts.
The exponential of a sum of overlapping local interaction terms cannot generally be factored into independent one-site contributions. Even when an auxiliary transfer map has a spectral gap and yields a differentiable limiting pressure, that argument does not directly cover every finitely correlated state. A mixture can have a limiting log moment generating function with a corner; the resulting rate function can be nonconvex. Ogata's printed Lemma 4.1 reduces to special components but omits the separate mixture step needed to recover the unrestricted theorem. The goal retains the theorem's printed hypotheses, while the condition-(14) milestone records precisely the restricted pressure claim. Ogata, pp. 12–15
The Lean model uses finite matrices for local algebras. A nonempty finite site basis represents , with site 1 indexed by 0. An interaction stores one Hermitian term for each support anchored at its least site; all translates that fit in appear in the Hamiltonian. The scalar empty-set term is retained. The auxiliary algebra is represented by a full matrix algebra ; finite-dimensional -algebra data have an equivalent full-matrix representation for the generated local states. Stationarity is written in the primal trace form. The recursive local state places the first site's matrix in the outermost application of .
The spectral law is formed from the eigenvalues and spectral weights of the actual Hamiltonian. It is not supplied as an arbitrary sequence of measures. The theorem uses no ergodicity, spectral-gap, or condition-(14) binder, and both LDP bounds range over every closed or open subset of . Logarithms of probabilities take values in the extended reals, with ; sequence limits are at , so the placeholder value at is immaterial. Nonnegative lower integrals represent exponential moments. In the restricted pressure milestone, the real logarithm applies to a positive state expectation. These choices also rule out a vacuous proof based on a zero measure, a moment represented by a non-integrable Bochner integral, or a rate function unrelated to the spectral law.
Reusable contributions include finite-dimensional spectral-law lemmas, positivity and stationarity facts for completely positive maps, good-rate-function and LDP lemmas on , and the Gärtner–Ellis result. The full theorem additionally needs a treatment of non-ergodic finite mixtures and periodic components that preserves both large-deviation bounds.
Optical quantum communication commonly encodes information in continuous variables such as the position and momentum quadratures of a light mode. Gaussian states and Gaussian operations are attractive in this setting because phase shifters, squeezers, beam splitters, and homodyne measurements are standard optical tools. Transmission through a lossy or noisy line can also be modeled by a Gaussian channel. The practical question is whether adding vacuum modes and Gaussian encoding and decoding can protect a signal against such a channel. Niset, Fiurášek, and Cerf (2008) give a negative answer for the code class defined in their Fig. 1.
The result sits after the early impossibility results for distilling Gaussian entanglement with Gaussian operations, including Giedke and Cirac (2002). Those results concern shared states and allowed local operations. The 2008 paper asks the channel-coding question directly: whether a finite Gaussian code can make a fixed single-mode Gaussian channel less damaging to entanglement. It introduces a scalar, entanglement degradation, to state the answer for every single-mode Gaussian channel in one inequality.
A single optical mode has two real quadratures, and . For modes, the order is . A state has a real covariance matrix recording its second moments in this order. The vacuum covariance matrix is the identity . A Gaussian channel on one mode is described at the covariance level by two real matrices and :
Here is the added noise. Complete positivity imposes symmetry and a matrix positivity condition on ; in particular, it gives . A Gaussian unitary changes covariances by a symplectic matrix , satisfying for the canonical symplectic form . Displacements affect first moments only and therefore play no role in these covariance formulas.
The code uses a positive integer . The input occupies mode zero in the formalization; the other modes are vacuum ancillas. A Gaussian encoding unitary acts on all modes, then the same channel acts independently once on each mode, and a Gaussian decoding unitary acts on all modes. Only the first output mode is retained. This defines an effective single-mode channel with matrices . The ancillas contribute noise to even before the channel uses are counted.
For a channel , the paper defines its degradation by
The intended value is when the denominator vanishes: the quotient is then interpreted as infinite and is saturated by the minimum. This quantity is related to the entanglement remaining when acts on one half of a two-mode squeezed vacuum as the squeezing grows. The paper measures that entanglement through the smallest symplectic eigenvalue after partial transpose and the logarithmic negativity .
The mission goal is the theorem on page 3, equation (11): for every completely positive single-mode Gaussian channel and every finite code of the stated form,
This is the assertion that the code cannot lower the channel's entanglement degradation. It includes , singular channels, and channels with negative determinant . No numerical performance constant or bound on the number of modes is fixed.
The milestones record the paper's channel-noise constraint (2), the fact that the code produces a Gaussian channel, the local matrix normal forms used in Lemma 2, the asymptotic calculations (8) and (10), the entanglement-breaking case, and Lemma 2 itself. Lemma 2 characterizes the degradation through the limiting squared eigenvalue and, when finite, gives . The milestones retain the paper's distinction between positive, negative, and zero determinant regimes.
The theorem rules out a specific and broad way of improving Gaussian transmission: adding any finite number of vacuum ancillas and using Gaussian unitaries before and after independent uses of a fixed channel cannot improve this intrinsic entanglement measure. The paper applies this conclusion to attenuation, amplification, and classical-noise channels, showing how an apparent reduction in one channel parameter can be offset by increased noise. It also relates degradation to an upper bound on quantum capacity, though that further bound is outside this mission. Niset, Fiurášek, and Cerf (2008)
The paper's theorem is proved in the mathematical literature; the goal here is a machine-checked statement and, eventually, a proof in the covariance-matrix representation. The published covariance layer already supplies symplectic forms, two-mode squeezed covariances, partial transpose, and an intrinsic ; this mission adds the channel and code definitions required to state the no-go theorem. Those definitions can be reused for other single-mode Gaussian-channel questions. A complete proof still needs substantial results connecting codes, Gaussian operations, and entanglement behavior; a compiled sorry statement alone does not establish the theorem.
One might try to compare before and after the code. That scalar does not track the code: encoding mixes signal and vacuum modes, each copy of the channel adds noise, decoding mixes the modes again, and discarding modes changes both and . Neither determinant separately gives the desired inequality. The boundary also defeats a direct real-valued transcription of the printed quotient. The asymptotic entanglement formulas cross several determinant regimes, with different normal forms and a separate entanglement-breaking case. The central challenge is to retain the physical meaning of all these cases in one theorem over arbitrary finite codes.
Lean uses real matrices indexed by interleaved mode and quadrature coordinates. The published QAlgorithms_Papers_Independent_Frontier30_P13 layer provides ModeQuadrature, phaseJ, squeezedCM, partial transpose, and the intrinsic smallest symplectic eigenvalue lambdaMin; QAlgorithms_Papers_Independent_Dependency50_P10 provides entrywise complexification. A channel is required to satisfy the Gaussian complete-positivity matrix inequality. Encoders and decoders satisfy . The code uses the same on every one of its modes, with , and includes the vacuum covariance on every ancillary mode. Gaussian unitaries enter through their symplectic matrices; their displacement parts do not affect covariances.
The definition of explicitly saturates at when , avoiding Lean's zero value for division by zero. The squeezed input uses and . The eigenvalue is the intrinsic lambdaMin, not an unguarded square-root expression. Logarithmic negativity uses the natural logarithm; its finite limit statement assumes , while the degradation statement still covers . The infinite-squeezing output is represented by limits of finite- covariances and entanglement quantities.
The code's vacuum term, all noise blocks, the symplectic equation, and the guarded degradation are essential to the target; dropping any of them would change the question. Lemma 1's teleportation equivalence and the external Gaussian no-distillation theorem are not formalized here. Their faithful treatment would require operational Gaussian states, measurements, and protocols beyond the covariance model. Contributions establishing those interfaces, proving the stated matrix milestones, or connecting the two layers are welcome.
Quantum circuits whose gates respect a global symmetry are a standard model for quantum simulation, for symmetry-protected quantum computing, and for the study of conserved quantities in quantum dynamics. For SU(d) symmetry on qudits, the unitaries that commute with every are, by Schur–Weyl duality, exactly the unitaries in the linear span of the qudit permutations. A natural question is whether every such unitary can be built from local symmetric gates, as happens without symmetry, where 2-qudit gates are universal.
Marvian, Liu and Hulse (arXiv:2105.12877) show that for the answer is no, and that the obstruction appears as conservation laws. Unitaries generated by 2-local SU(d)-invariant gates conserve quantities that general SU(d)-invariant unitaries change. The paper gives two families of such laws. The first, Theorem 1 (the law, from a symmetry of the swap Hamiltonians), is a separate result of the paper and is not part of this mission. The second, Theorem 2, is the target here. It comes from a correspondence between a subspace of the qudits and a system of free fermions.
Timeline: Marvian (Nature Physics 18, 283, 2022) showed that symmetry together with locality restricts the realizable unitaries in general, with examples for U(1) and SU(2) symmetry. For qubits with SU(2) symmetry, the constraints restrict only relative phases between sectors of inequivalent irreducible representations (p. 3 of the present paper). The present paper (arXiv:2105.12877, v2 January 2022) treats SU(d) with , where constraints beyond relative phases appear. The connection to Marin's 2007 description of the Lie algebra generated by transpositions (J. Algebra 310, 742) is discussed on p. 9.
Consider qudits with Hilbert space and computational basis , .
For , the vector antisymmetrizes the levels over the first qudits with weight (Eq. (40)). The subspace is the span of all permutations of these vectors (Eq. (42)), and is the orthogonal projector onto it.
For an operator on one qudit, is acting on qudit . Let . The map sends an operator on the qudits to the matrix
(Eqs. (49), (51)). On the fermionic side there are sites, creation operators , the vacuum , and the fermionic swap (Eq. (28)). Its single-particle counterpart is on (Eq. (33)). The map sends to (Eq. (41)).
For every , every density operator on qudits and every positive integer ,
The statement holds for all and . Its content is the case : the case holds for every SU(d)-invariant unitary (Eq. (55)).
Theorem 2 gives an infinite family of polynomial invariants of the state, for . Together these fix the spectrum of , so every Rényi entropy of the single-particle density operator is conserved. Already for the law is violated by SU(d)-invariant Hamiltonians with 3-local terms (p. 11 and §IV D). This shows that, for , 2-local SU(d)-invariant gates are not universal among SU(d)-invariant unitaries, even up to relative phases, and that 3-local interactions can be detected from the dynamics of . For the laws hold for all SU(2)-invariant unitaries.
The result is proved in the paper. As far as a search of the platform shows, it has not been formalized. A formalization adds machine-checked versions of the qudit–fermion correspondence of §IV B, including the isometry and the intertwining relation (44), and of the free-fermion form of the swap dynamics. These are statements about finite-dimensional matrices, so the whole development stays inside Mathlib's linear algebra.
The obvious route is to show that each generator acts on by conjugation with an unitary, and then to induct over products. The difficulty is the generator step. The definition (51) of involves the projector onto a span of antisymmetrized vectors, and nothing in (51) shows directly why conjugating by should conjugate by . The covariance becomes visible only after is identified with fermionic Fock sectors, where the swap becomes a quadratic, particle-number-preserving Hamiltonian. That identification needs care with the signs of the fermionic creation operators and with the ordering of products. A second obstacle is the characterization of the generators (Eq. (5)). It rests on the commutant of being spanned by and the swap, a Schur–Weyl statement for two qudits that Mathlib does not provide.
Operators on the qudits are matrices indexed by Fin n → Fin d, with sites and levels 0-based and [NeZero d] assumed so that exists. Fock-space operators are matrices indexed by Finset (Fin n), the set of occupied sites. The creation operator uses the Jordan–Wigner sign , the encoding of the public definition QAlgorithms_Papers_Independent_Next46_P23, copied rather than imported.
The following conventions are fixed:
EuclideanSpace ℂ (Fin n → Fin d).QAlgorithms.Entanglement.IsCompletelyPositive.The following trivializing formalizations are ruled out:
A complete development needs:
Finset Fock space;The Fock-space and permutation-operator lemmas can be reused for other qudit–fermion and Schur–Weyl statements. Contributions welcome: proofs of any milestone, and lemma-level infrastructure on the Fock space.
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 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 for which the expected cost is at most 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.
Let be a set of cities and let be a metric cost. A tour visits every city once and returns to its start; is the least tour cost. A Held–Karp vector 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 . We take to attain the minimum Held–Karp objective. These objects reuse the published MetricTSP model.
The paper chooses any city and splits it into and . Each edge incident to gives half its LP value to each copy. A new edge has LP value one and cost zero. Let be the positive support of the split LP vector after removing , and let denote its values on . A spanning-tree law gives probabilities to the spanning trees contained in and has marginal for each .
Among all such laws, a maximum-entropy law maximizes , taking . A sampled tree has an even number of odd-degree vertices. Let be a minimum-cost perfect matching of those vertices in the complete metric graph. The cost studied here is . 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.
The goal is a single absolute constant, chosen before the size, costs, LP optimum, split city, or tree law:
Here is the split cost, is any Held–Karp optimum, and 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 -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 , , and . Its matching analysis gives the sharper intermediate target . With the expected tree cost at most , this yields an improvement greater than Karlin–Klein–Oveis Gharan, proof of Theorem 1.1.
The result supplies a strict improvement over the 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 -joins to reusable definitions for finite spanning-tree distributions, entropy, rooted near-minimum cuts, and the -join cut relaxation. The mission also keeps the quantitative constants and the uniform order of quantifiers visible to later developments.
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.
Cities are Fin n with ; 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 . 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 has the impossible bound , so Fact 2.1 uses nonempty . Theorem 3.1 explicitly assumes : without nonnegativity, its bound on a nonnegative random vector can be negative. Every near-minimum cut is nonempty and excludes both endpoints of , matching the paper's rooted-cut convention. The optimal tour in Theorem 3.1 is any optimal Hamiltonian cycle through . The O-join bound uses 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 -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.
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 while the singlet has energy . Beating this worst-case 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 . Anshu–Gosset–Morenz (2020) showed that product states with commuting entangling gates beat product states, with ratio . Parekh–Thompson (2021) introduced the level-2 Lasserre relaxation for QMC, showed that it encodes monogamy, and obtained . In 2022 two simultaneous works rounded a level-2 solution to a commuting entangling circuit: Lee obtained on all graphs, and King (published 2023) obtained 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.
The graph has vertex set , one qubit per vertex, and symmetric weights normalised so that ; the neighbours of are the vertices with , and the graph is triangle-free if no three vertices are pairwise neighbours. The edge term is
and the quantity to approximate is .
The level-2 Lasserre relaxation is a semidefinite program over real matrices indexed by Pauli strings of weight at most : , depends only on the operator (with a sign flip when changes sign, and when is not Hermitian), , and the objective is . From a solution the algorithm reads the edge values .
Algorithm 17 of the paper, written out:
Its expected energy is the expectation of in the output state over all of the algorithm's randomness. The parameter is chosen as , where and is the hypergeometric function (12) describing GP rounding.
For every triangle-free normalised weighted graph, every solution of , every Gram factorisation used by the rounding, and every with on ,
The hypothesis on is exactly how the proof uses ; it is satisfied by .
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 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.
The obvious argument evaluates each edge's energy separately, but the gates on neighbouring edges do not act trivially on : 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 . The second difficulty is analytic: Lemma 13 is an identity for Gaussian projections expressed through , and the final inequality holds with a margin of about , so it requires certified numerical bounds on a hypergeometric series rather than a plot.
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 with , counted once in and in the objective.A fault-tolerant quantum computer executes only a discrete set of gates. The standard choice is the Clifford and T library: the Hadamard gate , the phase gate , CNOT, and the gate , 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 .
A short history of the question:
A register of qubits has computational basis . The circuits of this mission act on three wires: the data qubit (wire 0) and two ancillas (wires 1 and 2), which start in . A circuit is a finite list of gates, each being or on one wire or CNOT on an ordered pair of distinct wires; it is applied in list order, and its size is the number of gates.
The quality of a circuit as an implementation of a one-qubit unitary is measured on the input–output map with the ancillas initialized: compare the linear maps from one qubit to three qubits
by the Frobenius norm . This is sensitive to the global phase of , and it charges any amplitude the circuit leaves on the ancillas.
The paper's central gate is the phase gate . For it uses the roundings , , the Gaussian rational
and the two-qubit vector , where the integers solve .
The constant is absolute. The goal asserts only the shape of the bound, so a sharper constant does not invalidate it.
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 with linear gate count; and the error bookkeeping on initialized maps. The -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.
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 must be prepared from by gates (the Giles–Selinger column lemma, a reduction by two-level unitaries of types , and ), 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 on three qubits realize only a restricted set of determinants. Keeping the gate count linear in 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.
Qubits n = Fin n → Bool; wire 0 is the data qubit and wires 1, 2 are the ancillas, appended after the data wire.htcxGateSet); and , 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.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.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 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 depending on or would make it vacuous.
Not formalized here: Lemma 1 (the lower bound with ancillas, p. 4), the average classical runtime of the randomized four-square solver, and the auxiliary bound 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 are all welcome.
A qubit coupled to an environment loses the phase relation between its basis states and : 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 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.
A qubit state is a complex matrix with , and . With the Pauli matrices , its Bloch vector is , , so that (eq. (9)). The coherence is the squared radius of in the – plane,
The controller applies the Hamiltonian (eq. (13)) with three real fields , and the qubit undergoes pure dephasing at rate :
Equivalently the Bloch vector obeys with
Without control the coherence decays as . The breakdown time of an initial state with coherence is
The tracking fields are, with , an arbitrary , and ,
and the tracked state is with .
For , and a qubit state with coherence :
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), under constant coherence (p. 6); eqs. (37)–(38), and (p. 6); eqs. (41)–(42), the tracking fields solve (30) and are forced once are frozen (p. 6); and the field-strength identity of §III.C (p. 8),
The result gives an exact, state-dependent budget for coherence protection under dephasing. The time is inversely proportional to the coherence to be maintained and proportional to , where is the purity: the more coherent the initial state, the shorter the protection, and a state of maximal coherence for its purity () 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 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 and the domain of the square roots made explicit.
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 and the equation on , and the conclusion constrains only the -component while the hypothesis constrains only the – components. The tempting shortcut, assuming that and 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 , including the endpoint , and the sign has to be carried through the derivative.
Operators are Matrix (Fin 2) (Fin 2) ℂ in the basis ; the Pauli matrices are the published MIPRE.LCS.Pauli.X/Y/Z. Bloch vectors and controls are Fin 3 → ℝ: Bloch components in the order , control components in the order (with multiplying , as in (13)). The Bloch vector is , following eq. (9); eq. (8) prints an extra factor , which contradicts (9) and is treated as a misprint. A trajectory solves (32) or (30) on if it is continuous on and has the prescribed derivative at every . Controls are arbitrary functions . The hypotheses and are added, because divides by ; is a parameter. The sign of (37), (41), (42) is .
Statements about , the tracked state and the fields are restricted to , because Lean's square root and division are total ( for , ); 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 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.
The walled Brauer algebra is the centralizer algebra of mixed Schur–Weyl duality: for it acts on the mixed tensor space of and commutes with , and for it plays the same role for the general linear supergroup . Its representation theory has been studied through cellular structures and blocks (Cox–De Visscher–Doty–Martin 2008), Khovanov arc algebras (Brundan–Stroppel 2012) and cyclotomic quotients (Sartori–Stroppel 2015).
For the group algebra of the symmetric group there is a classical description of the center: it consists of the symmetric polynomials in the Jucys–Murphy elements (Jucys 1974, Murphy 1983). Jung and Kim (arXiv:1508.06469v2) prove the walled analogue: when is semisimple, its center is generated by the supersymmetric polynomials in its Jucys–Murphy elements. This mission formalizes that theorem and the chain of results leading to it.
Timeline. Jucys (1974) and Murphy (1981, 1983) describe the center of through Jucys–Murphy elements. Stembridge (1985) characterizes supersymmetric polynomials and shows that the power sums generate them. Cox, De Visscher, Doty and Martin (2008) give the cellular structure of , its blocks in characteristic zero and a semisimplicity criterion. Brundan and Stroppel (2012) prove that the central element (essentially ) acts on cell modules by a content sum. Jung and Kim (2015, revised 2017) prove the generation theorem for all supersymmetric polynomials.
Fix integers and . An -walled Brauer diagram is a pairing of vertices, on top and on the bottom, with a wall between positions and , such that vertical edges do not cross the wall and horizontal edges do. is the complex vector space with these diagrams as basis; two diagrams are multiplied by stacking them and replacing each closed loop by a factor .
For vertices on the same side of the wall, is the diagram of the transposition of and . For , is the diagram with a top arc and a bottom arc joining and and all other vertices joined straight down. The Jucys–Murphy elements (Definition 2.1) are
A polynomial is supersymmetric (Definition 2.8) if it is symmetric in the and in the separately, and the substitution produces a polynomial independent of . Examples are the power sums . Write for the supersymmetric polynomials and for the substitution , .
The cell modules are indexed by bipartitions with , , ; this set is . The set equals except when and , where is removed; it indexes the simple modules. The content vector lists the contents of , then zeros, then the contents of shifted by .
Both inclusions are asserted. The goal fixes no constants; the hypothesis holds for all but finitely many (Proposition 1.1).
The theorem gives an explicit generating set for the center of a semisimple walled Brauer algebra, parallel to the symmetric-group case. Its consequences in the paper include a description of the Gelfand–Zetlin subalgebra and formulas for primitive idempotents (§4), an alternative proof of the block classification of Cox et al. (§5), and, via the same method, the center of the quantized walled Brauer algebra (§6). Corollary 2.9 alone, valid for every , provides a supply of central elements whose action on each cell module is computed by Corollary 3.3.
The theorem is proved in the paper; no part of it is formalized. A formalization would supply machine-checked Jucys–Murphy relations for a diagram algebra built on a published, generic encoding of walled Brauer diagrams, a Lean development of supersymmetric polynomials (including Stembridge's theorem, absent from Mathlib), and a reusable dimension count for centers of semisimple algebras in terms of simple modules.
The inclusion of the supersymmetric polynomials in the center (Corollary 2.9) reduces to diagram relations plus Stembridge's theorem; the latter is a nontrivial statement about polynomial rings, with no counterpart in Mathlib. The reverse inclusion is the harder half. A central element is not visibly a polynomial in the : the argument must show that enough linearly independent central elements of the form exist, which requires computing their scalars on every cell module (an explicit cellular computation involving the arc elements ), separating all content vectors (where semisimplicity enters through the criterion of Cox et al.), and comparing with , which needs Wedderburn–Artin together with the classification of simple modules. Separation genuinely fails outside the semisimple range, so no argument independent of can work.
The algebra, diagrams, cell modules , the index sets (CellIndex) and (Label) and contents are the published definitions WalledBrauer_Blocks_{Diagram, Algebra, ModuleTheory, Partitions, CellModules}, used as references. New definitions are in WalledBrauer.Center.Setting. Conventions:
Fin (r + s)); the paper's is jm δ ⟨k-1, _⟩.MvPolynomial (Fin r ⊕ Fin s) ℂ. The evaluation is defined monomial by monomial in increasing vertex order, without assuming that the commute; it is never routed through a commutative subalgebra.IsSemisimpleRing, the center is Subalgebra.center ℂ, "generate" is Algebra.adjoin ℂ. In Proposition 1.1, is real.Supersymmetry is defined intrinsically on polynomials, never through the algebra, so neither inclusion of the goal holds by definition; stating only or only as the goal is excluded.
Proofs of any milestone are welcome, as are reusable developments of supersymmetric polynomials (Stembridge's theorem, elementary supersymmetric polynomials) and of the center of a split semisimple algebra.
Noncommutative -spaces built from a von Neumann algebra come in two kinds. When carries a normal faithful trace, is a space of (unbounded) operators affiliated with , and much of classical analysis — martingale inequalities, square functions, maximal inequalities, interpolation — has been carried over to this tracial setting. Algebras of type III, which occur naturally in quantum field theory and quantum statistical mechanics, have no such trace; their -spaces are Haagerup's, defined through a crossed product and the dual weight.
Haagerup, Junge and Xu (arXiv:0806.3635, Trans. AMS 362 (2010)) give a general method for transferring tracial results to type III algebras. Its engine is a reduction theorem, due to Haagerup and circulated as an unpublished manuscript since the late 1970s: after enlarging to a crossed product, the algebra is approximated by an increasing sequence of finite von Neumann algebras, in a way that respects the state and its modular group. This mission formalizes that theorem, §2 of the paper.
Timeline. Haagerup constructs his -spaces in 1979 (Colloq. Internat. CNRS 274) and proves the reduction in the manuscript [H3]. Junge and Xu use it for noncommutative Burkholder–Rosenthal inequalities (Ann. Probab. 2003) and maximal ergodic theorems (J. AMS 2007). The 2008 preprint, revised in 2009, gives the first published proof together with its applications to approximation, extension of maps to crossed products, and martingale and maximal inequalities.
is a von Neumann algebra on a Hilbert space with a normal faithful state . Up to spatial isomorphism is in standard form: there is a unit vector , cyclic and separating for , with . Tomita–Takesaki theory supplies the modular operator and the modular automorphism group .
is the group of dyadic rationals with the discrete topology. On define
for , . The crossed product is the von Neumann algebra generated by and . With , the dual state is ; on generators equals for and otherwise. Its modular group is , and .
For a bounded functional on an algebra , the centralizer is . With (branch ), and , the subalgebras are . A von Neumann algebra is finite if every isometry in it is unitary. A conditional expectation from onto a subalgebra is a positive linear -bimodular map onto fixing .
There is an increasing sequence of von Neumann subalgebras of such that each is finite, is w*-dense in , and for each there is a normal faithful conditional expectation with
The goal asserts existence only, as printed; the construction is the content of the milestones.
The reduction theorem lets a statement about Haagerup be proved by checking it on the finite algebras , where traces exist, and passing to the limit: the expectations extend to contractive projections on and their ranges exhaust , which contains complementably. The paper uses this to obtain noncommutative Burkholder–Gundy, Stein, Burkholder–Rosenthal and Doob inequalities, and maximal ergodic inequalities, for type III algebras; for some of these no other proof is known. The theorem has since become a standard tool in noncommutative probability and harmonic analysis.
The theorem is proved (in the cited paper, with details on pp. 7–11). It has not been formalized: Mathlib has von Neumann algebras as double commutants but no crossed products, conditional expectations, modular theory or Haagerup -spaces. This mission produces a formal statement of the reduction theorem and of each lemma of its proof, built on the published standard-form encoding of Tomita–Takesaki data, and invites solvers to formalize the known proof.
The modular group of a type III algebra is outer and aperiodic, so no centralizer is large enough to be finite and dense at once. The proof works around this by perturbing to states whose modular groups are periodic, and the delicate step is density: showing that the centralizers eventually see every element of . This rests on uniform estimates in the -norm (Lemma 2.6) that need the distribution of under (Lemma 2.2), analytic elements (Lemma 2.5), and an approximation of the logarithm by trigonometric polynomials. Norm density of is false in general; only weak*-type density holds. For finite the statement is easy ( is already finite); the content is the type III case.
is given by the published OAI.BoundedRecovery.StandardModularData H: a von Neumann algebra on , a unit cyclic separating vector , as a nondegenerate functional calculus, and , tied together by the closed Tomita relation; is its sigma. Every σ-finite von Neumann algebra with a normal faithful state is spatially isomorphic to such data, and every statement is invariant under spatial isomorphism.
The crossed product is built on lp (fun _ : dyadic => H) 2, as the double commutant of and their adjoints. , and are the bounded operators characterized by their pointwise formulas; is the Laurent operator of on in the shift , which is (Mathlib has no Borel functional calculus). Centralizers use the commutation form for bounded functionals. Finiteness is the published OAI.FiniteFactor.IsFiniteAlgebra (every isometry is unitary). W*-density is equality of the double commutant with ; σ-strong convergence of bounded sequences is strong convergence. Order on operators is the Loewner order. Lemma 2.2 is stated for continuous , which already determines the distribution.
Hypothesized modular data. The platform has no Tomita–Takesaki existence theorem, so the modular data of (and of in Lemma 2.4 (i)) enter as hypotheses with and ; the first milestone proves such exists, so the goal is not vacuous. The formalization does not restrict to finite, finite-dimensional or tracial (where the goal is empty); is never defined by a formula; finite means "every isometry is unitary", not finite-dimensional; and density is never norm density.
Reusable beyond this mission: the dyadic crossed product and dual state, conditional expectations, the commutation-form centralizer, and Lemma 2.5 for arbitrary standard-form data. Welcome contributions include the existence of modular data for crossed products, the shift and Laurent operators on of a discrete group, and the averaging construction of conditional expectations from periodic modular groups.