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?
The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, Existence and smoothness of the Navier–Stokes equation (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on (statement (A)) or on the torus (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.
Timeline.
Fix a dimension and write for Euclidean -space with its Euclidean norm ; in Lean this is NavierStokes.Vec n. A velocity field assigns to each time and point a vector ; in Lean is the field at time and is Fefferman's . A pressure is a real function . The viscosity is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).
For a vector field the divergence is
in Lean NavierStokes.div, computed from the Fréchet derivative as . The Laplacian acts componentwise (Mathlib's Laplacian on inner product spaces). The gradient is Mathlib's gradient. The convective term is the derivative of at in the direction . Finally is NavierStokes.gradNormSq.
Admissible initial data (Fefferman's condition (4), NavierStokes.IsInitialData): a , divergence-free vector field that decays together with all its derivatives faster than any power,
In Lean the bound is on the -th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.
A physically reasonable solution on a set of times (NavierStokes.IsSolutionOn; for NavierStokes.IsSolution) is a pair such that
Take and . For every admissible initial datum there exist a velocity field and a pressure forming a physically reasonable solution on :
This is NavierStokes.existence_and_smoothness_R3. It is open; a proof would settle the Millennium Prize Problem in the affirmative.
NavierStokes.local_existence_R3): for and every admissible there are and a physically reasonable solution on . Fefferman: "(A) and (B) hold ... if the time interval is replaced by a small time interval , with depending on the initial data."NavierStokes.small_data_global_existence_R3): there is an absolute constant such that, for , (A) holds for every admissible withFefferman: "(A) and (B) hold provided the initial velocity satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of , so Kato's theorem also applies.
3. The two-dimensional case (NavierStokes.existence_and_smoothness_R2): statement (A) with . Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."
A bridging lemma, NavierStokes.isInitialData_iff_schwartz, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.
The result itself. Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."
Formalizing it. None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on , the pressure equation or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.
The energy identity controls in and in , but in three dimensions this control is supercritical: under the scaling that preserves the equations, the energy of shrinks as , so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for , gives , which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.
The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of and recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on nor the heat semigroup in usable form.
EuclideanSpace ℝ (Fin n) with Lebesgue measure; the dimension is a parameter, the goal fixes and the 2D milestone .ContDiffOn of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to . The momentum equation is imposed at interior times with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "".fderiv, deriv, iteratedFDeriv, gradient, Laplacian) with junk value at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.No trivializing formalization. The zero field solves the equations only for ; for any other admissible the initial condition, smoothness, the equation on and bounded energy must all hold.
Infrastructure needed and welcome contributions. The heat kernel on with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the NavierStokes namespace, decompositions of the milestones, and Mathlib lemmas about ContDiffOn on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations () are out of scope.
Quantum circuits built from Clifford gates alone are classically simulable in polynomial time. Universality is recovered by adding copies of a magic state, and the fastest known classical simulators of such circuits work by writing the magic-state input as a short linear combination of stabilizer states. The length of the shortest such combination -- the stabilizer rank -- is therefore the exponent governing classical simulation of quantum computation in this model, and lower bounds on it are among the very few unconditional obstructions to classical simulation available at all.
A timeline of what is established for the standard magic state :
Between the linear unconditional lower bound and the upper bound lies the open problem this mission targets.
Index the computational basis of an -qubit system by bit strings , so a state is a vector with coordinates .
The Pauli operators are for , acting by , where counts the coordinates on which both are and is bitwise addition; the Pauli group is the set of operators . A unitary is a Clifford unitary when lies in the Pauli group for every Pauli group element , and a stabilizer state is a vector for some Clifford . There are of them up to phase -- six for a single qubit.
The stabilizer rank is the least admitting coefficients and stabilizer states with .
The magic state is , and its -fold tensor power, with coordinates where is the Hamming weight of .
The goal is a super-polynomial lower bound: for every exponent and constant there exists with
equivalently, is not for any fixed .
Stronger statements are expected but are deliberately not the goal. An exponential bound is believed and follows from hardness assumptions, but a goal naming a specific growth rate would be superseded by the next improvement; super-polynomiality is the weakest statement that settles the question of principle.
The result itself. A super-polynomial lower bound would unconditionally rule out efficient classical simulation of Clifford-plus-magic-state circuits by stabilizer decomposition, currently the leading such technique. The converse direction shows how much is at stake: a polynomial upper bound on would imply , and via postselection . There is also a purely classical payoff -- improving the known bound even to super-linear would produce a Boolean function computable in polynomial time requiring a super-linear number of summands in any decomposition into exponentials of quadratic forms over , resolving a separate open question.
Formalizing it. The goal is open, so no known proof is being transcribed. What the mission produces is a machine-checked statement of the problem together with formalizations of the established bounds, none of which has a machine-checked proof anywhere. It also produces the first Pauli/Clifford/stabilizer layer in Lean: no existing Lean library contains the -qubit Pauli group, the Clifford group, or stabilizer states, and that layer is reusable for stabilizer error correction, magic monotones, and Clifford simulation generally.
Counting settles the problem for random states: the stabilizer states are too few for short combinations to cover a generic state, so almost every state has exponential stabilizer rank. This says nothing about , which is a single explicit, highly structured vector, and the entire difficulty is that lower bounds must be proved for that specific state rather than for a typical one. Every newcomer proposes the counting argument; it does not apply.
The known techniques reduce the question to statements about decompositions of explicit Boolean functions into quadratic-form exponentials, and the barrier is quantitative: the available arguments lose a factor that caps them at linear bounds. The source of the current record documents explicitly why its method cannot pass super-linear, and the fact that going beyond linear would resolve an independent open problem in Boolean function complexity indicates the obstruction is not merely technical.
State vectors are functions and are not required to be normalised; normalisation does not affect the rank, and stabilizer states are unit vectors automatically as Clifford images of . The Pauli group is given by the explicit parametrisation rather than an abstract presentation, and the Clifford group is characterised as its unitary normaliser, equivalent to the usual generated-by- description. Because normalises the Pauli group whenever does, the stabilizer states are closed under global phase; this is harmless, as the coefficients are arbitrary complex numbers.
One trivialising reading must be excluded. The rank is defined as an infimum over a set of natural numbers, and Lean gives the empty infimum the value ; if no decomposition existed the rank would be for every state and the goal would be false rather than merely unproved. The milestone is what certifies the set is nonempty, making the rank a genuine minimum, and it should be proved first. Separately, the goal quantifies over all reals including negative values, for which the inequality is trivially satisfiable; the content lies in large positive .
A complete development needs, beyond the published definitions, the correspondence between stabilizer states and affine subspaces carrying quadratic phase functions, on which all known lower-bound arguments rest. Contributions of any milestone are welcome, as are function-level reformulations of the rank and the equivalent characterisation of stabilizer states via maximal abelian Pauli subgroups.
A smooth manifold is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The strong Whitney embedding theorem supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by LeanEval v1, rather than a substitute formulation.
The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of . The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature (source and attribution).
Let be a natural number satisfying . Let carry a topology and a smooth atlas modeled on , with the usual model having no boundary. The topology is Hausdorff: distinct points admit disjoint neighborhoods. It is second countable: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the Lean statement.
A topological embedding is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An immersion has an injective differential at every point. For a smooth map , write for the induced linear map on tangent spaces at . These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.
For every and every with the structures and hypotheses just stated, establish
The codomain has dimension exactly . The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding, with the binders and conclusion preserved from the benchmark source.
The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the benchmark's explanation.
A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.
The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition (benchmark discussion).
All positive dimensions remain in scope, including and . Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.
The source model is EuclideanSpace ℝ (Fin n), and the target is EuclideanSpace ℝ (Fin (2 * n)). Smoothness is expressed by ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e; the other two conjuncts are IsEmbedding e and pointwise Function.Injective of mfderiv. The type remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion (exact declaration).
Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak alternative.
Every even integer greater than is the sum of two primes. Christian Goldbach posed it in a 1742 letter to Euler, and it has resisted proof for nearly three centuries while being verified computationally up to — making it one of the oldest and most famous open problems in all of mathematics. Its ternary sibling, the weak Goldbach conjecture, was settled by Helfgott in 2013, but the strong form stated here remains wide open: the circle method controls three-prime sums yet loses control at two. This headline mission hosts the conjecture as a machine-checked target for partial results, reductions between its variants, and any future attack.
A retailer that sells substitutable products must decide, for each arriving customer, which subset of products to display. Customer preferences are unknown at the start and have to be learned from purchases, while every suboptimal display costs revenue. This is dynamic assortment planning, a standard problem of revenue management in e-commerce and online advertising, and its learning version is a bandit problem whose arms are the subsets of products.
Under the multinomial logit (MNL) choice model the problem has been studied through the regret of a policy over customers (Chen, Wang and Zhou, §2 and Table 1):
In the capacitated model the regret must grow with . Chen, Wang and Zhou (arXiv:1805.04785v2, Mathematics of Operations Research 2021) show that without a capacity constraint it need not: a trisection policy achieves regret with a universal constant, and is a lower bound. This mission formalizes the upper bound.
There are items with known revenues and unknown utilities ; the no-purchase option has utility . In each period the retailer offers an assortment , and the customer buys with probability or buys nothing with probability , independently of the past. The expected revenue of is
and the regret of a policy is , where maximizes over all subsets.
The policy rests on two objects. The level set collects the items whose revenue is at least . The revenue potential is a piecewise-constant function of one real variable. Its maximum is , its right limit is , and denotes the fixed point .
The adaptive-confidence trisection policy keeps an interval , starting from . In epoch it forms the points and , at distance , and runs inner iterations. Each inner iteration does two things:
At the end of the epoch the policy sets if , and otherwise. The policy knows and but never .
There is a universal constant such that for every , every horizon , all and all , the adaptive-confidence trisection policy satisfies
No gap condition and no bound on is assumed. The constant is left unspecified, as in the paper.
Theorem 3, together with the lower bound of Theorem 4, settles the minimax regret of uncapacitated MNL assortment learning at , independent of the number of products. The policy uses no estimate of the individual utilities, and its cost per period is one level-set offer, so it applies to catalogues where is large compared with . The structural lemmas on the revenue potential (Lemmas 1–4) are standard tools for MNL assortment problems and are reusable by other missions on static and dynamic assortment optimization. Lemma 8 is a MOSS-style concentration inequality whose confidence level grows with the sample size; it is the device that removes the factor of the paper's baseline bound (Theorem 2).
The result is proved in the paper and is not presented as open; no machine-checked proof of any part of it is known. The platform has the MNL model, the UCB policy of Agrawal et al. (whose bound depends on ) and Hoeffding's inequality, but no level-set or trisection analysis. A formal proof would also check the paper's argument, whose printed slips are recorded in the scope section.
The regret concerns a stateful algorithm whose epochs end at random times: an inner iteration takes two periods while exploration is active and one afterwards, and the policy's internal state must be recomputed from the purchase history alone. The obvious argument fixes a confidence level , bounds each epoch's regret on the event that all confidence intervals hold, and sums a geometric series. That argument loses a factor, and it is the paper's own Theorem 2. Removing the factor needs confidence levels that weaken as data accumulate. A failure is then no longer rare enough to be ignored, so the analysis has to track its cost. This is done by a recursion on conditional expected regrets across three cases (interval to the right of, containing, or to the left of ), in which a wrong decision in one epoch passes to another case with controlled probability. Within an epoch, the purchases made while exploring a level set must be shown to behave like i.i.d. samples with mean , although the number of explorations is itself random.
MNLBandit.UCB.Setting with every subset admissible: histories are sequences of choices in Option (Fin N) (none = no purchase), policies are deterministic functions of the past choices, and expectations are finite sums over histories. Items and periods are 0-based in Lean; epochs and inner iterations are as on the page.Function.rightLim.An object is hidden in one of boxes. Each search of box costs time , and if the object is there it is found with probability , independently of all earlier searches. When the searcher knows the probabilities with which the object was placed, the problem has a classical index solution. Norris (1962), Bram (1963), Blackwell (reported by Matula, 1964), Black (1965) and Ross (1983) showed that it is optimal to search, at every step, a box maximizing the current Gittins index , where is the number of failed searches of box so far. Ross also showed the converse: only such sequences are optimal.
The adversarial version replaces the known prior by a hider who chooses the box to maximize the expected time to detection, while the searcher minimizes it. Because overlook is possible, a pure search strategy must be an infinite sequence of boxes. This zero-sum search game goes back to Bram (1963) for unit search times, and it belongs to the search games against an evader in a stationary search space surveyed in Book 1 of Alpern and Gal (2003).
Timeline.
There are boxes with search times and detection probabilities .
Pure strategies. A pure strategy of the hider is a box. A pure strategy of the searcher is a search sequence . If the hider is in box , the expected time to detection is
where is the number of searches of box among the first .
Mixed strategies. A hiding strategy is a probability vector in the simplex . A search strategy is a probability mass function on , and . Against a sequence , a hiding strategy earns the hider .
Value and optimal strategies. The value is
A hiding strategy is optimal if it attains . A search strategy is optimal if for every box .
Gittins search sequences. , the set of Gittins search sequences against , consists of the sequences that always search a box of maximal Gittins index.
Tie-breaking by one ordering. A permutation lists the boxes in order of preference. is the Gittins search sequence against that, whenever several boxes have maximal index, searches the one lists first. Then
has at most elements, whereas can be uncountable.
For every optimal hiding strategy there is a search strategy with
The goal fixes no constants. It asserts that an optimal search strategy exists, and that one can be found among mixtures of at most elements of .
The result. In the searcher's pure strategy space is uncountable, so the existence of an optimal search strategy is not automatic. The standard theory of semi-finite games gives only -optimal strategies. Theorem 6 settles existence for general search times. Theorem 10 reduces the search for an optimal strategy to the finite set .
The paper's computational section builds on this reduction. For interior , optimality of in is equivalent to optimality in the finite matrix game, which a linear program solves (Proposition 11). This is also the basis of the paper's bounding algorithm. Theorem 10 extends Gittins' two-box, unit-time Proposition 8.5 to any number of boxes and arbitrary search times.
Formalizing it. The results are proved on paper. To our knowledge none is machine-checked. The Blackwell–Ross index theorem is the only ingredient already proved on the platform. This mission formalizes:
The obvious route to existence is the -game argument of Blackwell and Girshick: if the set of payoff vectors is closed, the infimum over its convex hull is attained, and Carathéodory gives a mixture of at most points. For general search times no such closedness argument is available for itself: its payoff vectors are unbounded, and a sequence that neglects a box has an infinite coordinate. The paper therefore restricts to Gittins sequences against hiding strategies bounded away from the boundary, and adds pseudo-strategies that dominate everything near the boundary. Closedness of the resulting set rests on the continuity of . This map is discontinuous at tie points in general and is continuous only along the cones (Lemma 17).
For Theorem 10, the natural idea is that every Gittins sequence is a mixture of the . That is false pathwise. Lemma 9 replaces it with a statement about extreme points of .
Representation.
Fin n and searches are 0-indexed (ξ : ℕ → Fin n).stdSimplex ℝ (Fin n), boundary included.PMF (ℕ → Fin n).ℝ≥0∞).AllocationIndices search-problem definitions, with cost . Blackwell's theorem is the published AllocationIndices.search_index_optimal.Tie-breaking.
[NeZero n], which is implied by the simplex being nonempty.Real vectors. , and are real vectors, obtained via toReal. They are used only for interior , where every coordinate is finite.
Trivializing readings, all excluded. None of the following is used:
Infrastructure and contributions. A complete development needs:
convexHull_eq_union) and Krein–Milman (Mathlib closure_convexHull_extremePoints);The -game theorem and the semi-finite minimax theorem are reusable well beyond search games. Proofs of any milestone, and of these general tools as separate lemmas, are welcome.
A retailer who sets a price for a product with limited inventory usually learns about demand from past sales. When the shelf runs empty, sales record the inventory level rather than the demand. Demand above the stock is lost and never observed. This demand censoring is pervasive in retail and inventory data, and it biases naive estimators of demand curves (Besbes and Muharremoglu, Management Science 2013; Ban, Operations Research 2020). Bu, Simchi-Levi and Wang (SSRN 3619625; Management Science, doi:10.1287/mnsc.2022.4382) ask a basic question about offline (historical) data. The retailer has censored sales at a few past prices and must choose a single new price. When can it, with enough data, guarantee near-optimal revenue no matter what the unobserved part of the demand distribution looks like? The paper answers this exactly, and gives an algorithm that achieves the guarantee whenever it is achievable.
The retailer has units of inventory and chooses a price in a known interval . Demand is linear: , where the base demand is random with c.d.f. , and the price sensitivity lies in a known interval . Demand is nonnegative almost surely at every feasible price. Sales are , and under a c.d.f. of the expected revenue is .
Offline data. different historical prices were used with inventories . At pair there are independent censored sales . The data size is . A value of is observable only below the observable boundary . Write , which is assumed positive. Assumption 1 asks that, below , is either discrete with finitely many atoms or has a density, with a slope or density lower bound .
Ambiguity set. No amount of censored data reveals on . The set of distributions consistent with the data is . The optimistic and pessimistic revenues are and . Their largest maximizers on are the optimistic price and the pessimistic price . With the largest maximizer of , the worst-case revenue loss of a price is .
Identifiability. A data-driven algorithm maps the censored data and the public inputs (, the two intervals, the pairs ) to a feasible price . The problem is identifiable (Definition 1) if some algorithm satisfies for every .
The problem is identifiable if and only if
The Lean goal states this in three parts, for every instance satisfying the standing assumptions:
Theorem 1 separates censored-data pricing problems into two classes. In identifiable ones, more data eventually yields near-optimal prices. In the others, a positive loss persists however large the sample, and the right benchmark is the minimax loss . The criterion is checkable in terms of two robust optimization problems, the maximax and the maximin. The constructive half comes with an algorithm that uses only observable data and has sample complexity , matching data-driven newsvendor results without censoring (Levi, Perakis and Uichanco, Operations Research 2015).
The results are proved in the paper. None of them, and none of the model, is formalized. The mission formalizes the model, the ambiguity set, the algorithm and the full chain of the proof. It includes two concentration inequalities not yet available in Lean in the needed form: DKW with Massart's constant for distributions with atoms, and a uniform bound over monotone function classes.
The algorithm sees only the censored data. A proof that silently uses or to pick the price does not establish the theorem. The obvious estimator of , least squares on observed sales, is biased by censoring. D2ACD instead regresses empirical quantiles at the level , below which the data are uncensored. Its analysis needs a lower bound on the slope of the c.d.f. (Assumption 1), and a uniform-in-price comparison of piecewise empirical revenues whose breakpoint is itself random. On the other side, the lower bound requires the exact extremal distributions in . The optimistic one sends the unobserved mass beyond every relevant demand level. The pessimistic one puts it at the boundary .
Representation. c.d.f.s are probability measures on . means agreement with on every half-line , , so an atom at is allowed. , , the worst-case loss and are defined as suprema and infima. Their attainment is part of the milestones, so no statement is true through a junk value. "" is the supremum of the set of maximizers. The data are base-demand samples under the product law, mapped to censored sales. An algorithm is a function of the sample sizes and the censored sales for fixed public inputs. Failure probabilities are outer measures. The limit is over all sample-size vectors with .
Standing assumptions and disclosed choices. The data equation is ; the page drops once. The continuous branch of Assumption 1 bounds the density on , with a lower bound of the support. The printed contradicts nonnegative demand together with . The historical prices are pairwise different, as the text says. The finite-sample statements (Lemmas 1, 2, Theorem 2) are made on the data assumption for all , as on p. 10; the goal is not. In D2ACD, is the clamp of the least-squares slope to , which is the arg min of line 9. Ties go to the largest price and the least index. The output is when some sample is empty.
Trivializing readings ruled out. Definition 1 fixes the instance before asking for an algorithm, so a constant algorithm returning witnesses the bare equivalence. For that reason the goal names D2ACD, a definition taking only the public inputs and the censored sales, and states the quantitative lower bound for the other direction. Two sanity instances, one discrete and one uniform, satisfy every standing assumption, so the hypotheses are not vacuous.
Contributions welcome. Proofs of any milestone. The concentration lemmas A.2 and A.3 are reusable well beyond this mission. Propositions 1–3, 6 and 7 are deterministic convex-analysis arguments about the two robust revenue curves and are a natural starting point.
Models of Bayesian social learning describe agents in a network who each receive a private signal about an unknown state of the world, observe the actions of their neighbours over time, and act optimally given everything they have seen. They are used in economics, operations research and the study of collective decision making to ask whether groups aggregate dispersed information, and they presuppose that every agent can carry out the Bayesian update. Hązła, Jadbabaie, Mossel and Rahimian (arXiv:1705.04770, Operations Research 2021) show that this presupposition fails in general: already at the second round of interaction, computing a Bayesian agent's action is NP-hard (their Theorem 1). The proof is a reduction from approximate VERTEX-COVER. This mission formalizes the mathematical core of that reduction: in the network built from a graph, the belief of one designated agent at time two is pushed to opposite extremes by graphs with small vertex covers and by graphs whose vertex covers are all large.
A finite set of agents is given, and every agent has a neighbourhood of agents whose actions she observes, with . The state is , drawn from the uniform prior . Agent receives a private signal with law ; conditionally on the signals are independent, so a signal profile has probability .
At every time agent knows her own signal and the actions of all at times . Her information set is the set of profiles that agree with in and in all those actions. Her belief is the posterior (4)
and in the binary action model (utility ) her action is the more likely state, with ties broken towards . Actions at time depend on information sets at time , which depend on actions at earlier times, so all of these are defined together by recursion on . The log-belief ratio is .
The reduction network for a simple graph with vertices and edges has agents: a vertex agent for each vertex, observing only herself, with and ; an edge agent for each edge , observing , and herself, with an uninformative signal; an agent observing only herself; and the agent , with an uninformative signal, observing and all edge agents. With , and , agent 's signal is chosen so that
Agent 's observed history is: every edge agent announces , and announces .
There are and such that for every , every graph on vertices, every admissible signal structure of , and every signal profile producing the observed history:
The constant is not fixed: the paper writes .
Theorem 6 is the step that turns a statement about vertex covers into a statement about beliefs. Together with the NP-hardness of distinguishing graphs with a vertex cover of size from graphs with no vertex cover smaller than (Theorem 5, from Khot, Minzer and Safra's proof of the 2-to-2 games theorem), it shows that no polynomial-time algorithm computes the time-two action of a Bayesian agent unless P = NP, and that even approximating the belief is hard, since the two cases differ by exponentially small versus exponentially close to one. This sets a limit on rational-agent models of social learning as descriptions of behaviour and motivates bounded-rationality alternatives.
The result is proved in the paper; to the best of current knowledge it has not been formalized. The mission produces a machine-checked model of Bayesian group decision making on a network, with information sets defined by recursion on time, reusable for other results about Bayesian learning on graphs, and a finite Chernoff bound in Kullback–Leibler form. The NP-hardness itself is not part of the mission: it needs a model of computation and inherits its hardness from a cited theorem.
The model's information sets are defined by a recursion in which every agent simulates what every neighbour could have seen. The first obstacle is to compute the time-two information set of agent in closed form: one must check that the actions of agent and at earlier times, and of the edge agents at time zero, carry no additional information, and that the edge agents' time-one actions reveal exactly whether the vertex signals form a vertex cover. Then the posterior becomes a ratio of two weighted counts of vertex covers. A naive bound comparing the two sums term by term does not separate the YES and NO cases, because the sums are dominated by different covers; in the YES case the large covers must be discarded using a tail bound whose exponent beats the likelihood of a single small cover, which is where the constants enter.
States, signals and actions are Bool (false = 0). A network is BinNet (neighbourhoods with , and ); post, mapAct, infoSet, act, logBelief are (4), the MAP action with ties to , , and . Information sets contain the conjunct from the history of (1). The reduction network is vcNet G k₀ k₁ for G : SimpleGraph (Fin n), on the agent type Agent n G (vertex agents, edge agents indexed by G.edgeSet, iAg, kap), with quantified over all pairs in with . Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Decimals are exact rationals; , , are compared as real numbers. Probabilities of events on the vertex signals are written as finite sums of over subsets . is the published bernoulliRelativeEntropy. is the number of graph vertices, not of agents.
The goal is about the model's own posterior on the model's own information set, for every profile on which the model's actions produce the history; it is not stated about a hand-written ratio of sums, which would skip the model. The constants and are quantified before the graph and before 's parameters, so they cannot depend on the instance. The complexity clauses of Theorem 6 (a polynomial-time reduction, the bounds (9)) and Theorem 1's NP-hardness are not formalized.
Contributions welcome: closed-form computations of early information sets in the model, the finite Chernoff bound (Theorem 7; the published Proved MassartDKW.Binom.comment_3 is the strict-tail Cramér–Chernoff bound for binomial n p), and the numerical inequalities of (16) and (17).
Mixed-integer programs often contain general integer variables . A standard modelling device replaces such a variable by binary variables linked to through a polytope, a binarization. Examples are the unary encoding, the "full" encoding with one indicator per value, and the logarithmic encoding . Binarizations let cutting-plane and branching techniques built for 0/1 variables, such as lift-and-project and sequential convexification, act on general integer programs. Computational experience with such encodings is mixed. A logarithmic encoding uses the fewest variables, but it is not obvious that it should help or hurt the strength of the relaxation. Dash, Günlük and Hildebrand (Mathematical Programming 170, 2018) studied split cuts in binary extended formulations. Aprile, Conforti and Di Summa (arXiv:2106.00354, Mathematics of Operations Research, 2024) introduced a rank that measures how many convexification steps on the binary variables are needed to remove fractional values of , and compared binarizations by it.
The underlying operation is Balas's sequential convexification (Balas, Discrete Applied Mathematics 89, 1998; doi:10.1016/S0166-218X(98)00136-X): for a polytope , replacing by for in turn yields the convex hull of the mixed 0/1 points.
A point is written . A polytope is the convex hull of finitely many points; is its vertex set and two vertices are adjacent when the segment joining them is a face of . The skeleton is the resulting graph.
For a polytope with some coordinates restricted to , write . The lift-and-project rank is the least such that some indices satisfy .
A polytope is a binarization of in the range , , if the -values of its points with are exactly . For a number let . Given integers and points , the rank of is
with the lift-and-project rank taken with respect to . It counts the -convexifications needed to cut off every point of whose -value lies strictly between and for some .
is a -hypercube binarization if its vertices project onto in the -space and onto in the -space, so that the vertices of correspond one-to-one to those of the -cube, each with its own integer -value. The logarithmic binarization is
For every -hypercube binarization and all ,
The milestones follow the paper's development:
where counts coordinate directions in which no edge of crosses any level .
The theorem gives a precise sense in which the logarithmic encoding is the best among all encodings of an integer variable whose binarization has the combinatorics of a cube. It is not only the most compact one: it also requires the fewest sequential convexification steps on the binary variables to remove any prescribed family of fractional -intervals. Combined with Corollaries 4.19 and 4.22, it yields the explicit formula . In particular, for every even . By Theorem 4.23 this extends to every hypercube binarization a result of Owen and Mehrotra (Operations Research 50, 2002) on the logarithmic encoding: convexifying all but one of the -variables of does not ensure integrality of .
The result is proved in the paper. No machine-checked version exists. The mission formalizes the vertex-and-edge view of sequential convexification that the paper's proofs rest on: Balas's theorem for V-polytopes, lift-and-project rank as a hitting set, and the hypercube graph of a binarization with its cut structure. Mathlib has convex hulls, extreme points and extreme subsets, but no face lattice of polytopes, no skeleton graph and no hypercube graph. Platform results on Balas's theorem exist only for H-polyhedra with explicit bound rows.
The comparison is between an arbitrary hypercube binarization and a specific one. Direct computation of for an arbitrary is not possible, because the polytope depends on the whole edge structure of , and the skeleton of a hypercube binarization need not be the cube graph: it can contain extra edges. The step that has to be bridged is from the lift-and-project rank of a polytope to a statement about cuts in the hypercube graph . That requires the vertex description of sequential convexification, the location of vertices of fractional slices on edges of , and the reduction from the skeleton to the subgraph . A natural first idea, comparing the polytopes and through an affine map, fails: a general hypercube binarization is not affine, and by Lemma 4.16 of the paper is, up to symmetry, the only affine one.
The Lean development fixes the following conventions.
p : Fin (d+1) → ℝ, with = p 0 and = p i.succ. Coordinates of are indexed from , so the weight of is 2 ^ (i : ℕ).Set.extremePoints, and edges are the published Hirsch.Adj.Disjunctive.HigherDim.SplitConvexify and IteratedSplit.lpr Q H is defined for any set H of 0/1 coordinates, with repetitions allowed in the sequence of convexified variables, as an sInf that Theorem 2.1 shows is attained.rk B xbar takes the fractional points as an argument. Every statement about it quantifies over all admissible choices, and in the goal the choices for and are independent.A formalization in which the rank of is a junk value (an empty set under sInf, or convexification over the wrong coordinates) would make the goal trivial. The definitions were checked against this: a sorry-free verification file proves and that is a -hypercube binarization.
A complete development needs:
The polytope and edge results, including the vertex form of Balas's theorem, are reusable well beyond this paper. Contributions proving any milestone, or general lemmas on vertices of hyperplane sections and on projections of polytopes, are welcome.
Selecting a valuable subset subject to several simultaneous restrictions is a common combinatorial optimization problem. A facility may contribute less after nearby facilities have already been selected; a collection of observations may provide overlapping information. Such diminishing returns are captured by submodular objectives. Matroid constraints describe families of admissible selections that are closed under deletion and satisfy an exchange rule. Requiring a selection to satisfy several matroids permits overlapping restrictions on the same elements.
Lee, Sviridenko and Vondrák study this model with access to objective values and independence tests through oracles. Their main monotone guarantee is a polynomial approximation factor of for any fixed number of matroids and fixed . The source compares this with the earlier greedy guarantee. This mission formalizes the published monotone result and its supporting exchange statements, with the constants and algorithmic quantifiers intact (Introduction and Theorem 3.1).
The ground set is a finite set of elements. A submodular function assigns a real number to every subset and satisfies
All objective values in the faithful source statements are nonnegative. For the headline theorem the function is also nondecreasing: implies . The empty set need not have value zero.
A matroid on is a family of independent sets containing the empty set, closed under taking subsets, and satisfying augmentation: a smaller independent set can gain an element from a larger independent set while remaining independent. There are such matroids, all on the same ground set. A set is common independent, or feasible, when it is independent in every one of them. The quantity is the maximum of over feasible subsets. This maximum exists even when is empty, since there are finitely many subsets and the empty set is feasible.
An algorithm receives a value oracle for and one independence oracle for each matroid. A value query specifies a subset and returns its value; an independence query specifies a matroid and a subset and returns a yes-or-no answer. Real arithmetic and comparisons use the unit-cost oracle convention. No table of all objective values is supplied (Introduction, p. 795).
The goal is the first sentence of Theorem 3.1. For each fixed and , there must exist one finite oracle program and polynomial constants, depending only on those fixed parameters, such that on every instance it halts and returns a feasible set with
The time bound includes initialization, oracle queries, subset processing, unsuccessful searches, and output. It is not merely a bound on the number of improving moves (Theorem 3.1, p. 803).
The eleven supporting milestones follow the source's numbered statements. They cover perfect matching for equal-size independent sets; irreducible cycle covers; the independence consequence of a unique perfect matching; feasibility of irreducible cycles; feasible path and cycle covers; exact-cover addition; generalized Rota exchange; bounded-multiplicity exchange for independent sets; exact-cover removal; and exact and approximate local-search inequalities. The order follows the dependencies identified in §§1–3. The exact local-search bound is
with a factor on the left in the approximate version. Here is an integer, is any feasible set, and the objective may be nonmonotone (Lemmas 3.1–3.2).
The approximation theorem gives a quantitative guarantee for general matroid intersections with a submodular objective. Restricting the constraints to partition matroids, or proving that a good set exists without a polynomial computation, would lose part of the result. The supporting exchange statements also describe how independent sets can be related when individual exchanges cannot simply be combined across constraints (§§2–3).
The mathematics is a published result; this mission asks for machine-checked proofs of its formal statements. The submodularity predicate is reused from an existing published definition. Lemma 2.1 is anchored to an existing Open bijective exchange theorem through a contraction and graph interpretation, rather than posed again. Open means that its proof remains a target. The remaining statements and the operational oracle model are local drafts, and compiling their statements does not prove them.
A chain of individually feasible swaps need not give a feasible simultaneous exchange. The source's distinction between an arbitrary directed cycle and an irreducible one therefore matters. Feasibility of a path or cycle also includes every eligible subpath, not just the whole vertex-set swap. Losing either distinction changes the supporting exchange results (Definitions 2.1–2.2).
Polynomial computation is a separate obligation from local-optimum quality. Literal Figure 1 admits infeasible singleton initialization when loops are present and nontermination at zero value under its non-strict update test. These issues are recorded as findings about the displayed routine, while the existential headline retains all inputs. Two further findings identify missing witness properties and an invalid intermediate path-count estimate in the printed analysis; they do not establish falsity of the numbered local-search inequalities. Proofs must resolve those obligations without importing them as assumptions (pp. 802–803).
Lean represents by Fin n, subsets by finite sets, objective values by real numbers, and matroids by Mathlib matroids with ground set equal to the whole finite type. Indexed families preserve repeated sets and repeated paths or cycles. Paths may consist of one vertex, cycles may have two vertices, and the cover multiplicity is , including . There is no looplessness, normalization, positive-optimum, or equal-cardinality restriction on the headline inputs.
The algorithmic goal uses a finite register-machine language whose only input-dependent operations are the two types of oracle queries. An explicit halt and a bound on the full execution cost are conclusions. Definitions contain neither an approximation guarantee nor an assumed polynomial stopping bound. The terminal predicate for Figure 1 uses strict inequality because the printed update uses greater-than-or-equal. Empty and zero-value inputs belong to the headline theorem even though the literal terminal predicate need not describe them.
The stronger linear-objective sentence of Theorem 3.1, the nonmonotone algorithm of Theorem 4.1, and the tightness examples in §5 are outside this mission. No optional variants are posed. Contributions needed here include the source theorem proofs, the exchange adapter, and the operational algorithm witness and its accounting.
A system of users sharing resources may have no stable configuration: whenever the users settle on their choices, somebody may prefer to change. Weighted congestion games describe this question when different users place different demands on the resources they choose. Routing and scheduling provide examples, but the mathematical question here does not impose a particular network or scheduling structure. It asks which resource cost functions guarantee stability regardless of the finite population, its demands, and its feasible choices. Harks and Klimm give a classification of such functions in their 2012 paper, Theorem 5.1.
There are two distinct requirements. A stable configuration may exist even when some sequences of individually profitable moves cycle forever. Guaranteeing that every sequence terminates is generally stronger. The result identifies the continuous function classes for which these two universal guarantees coincide. The word “universal” matters: the assertion concerns all games generated by a class of costs, rather than the behavior of one specified game.
A weighted congestion game has a nonempty finite set of players and a nonempty finite set of facilities . Each player has a positive real demand and a nonempty finite collection of available strategies. A strategy is a subset of facilities; it may itself be empty. A profile chooses one strategy for every player. Facility has a real-valued cost function defined on the nonnegative half-line. Its load and a player's private cost are
Costs can have either sign, and the game model imposes no monotonicity. A pure Nash equilibrium is a profile satisfying for every feasible unilateral change . A strict improvement lowers the deviating player's cost. The finite improvement property, or FIP, excludes improvement cycles, equivalently infinite improvement paths in this finite profile space. These conventions follow §2 and Definition 2.1.
For any set of cost functions, write for all such games with at every facility. The class is consistent if every game in has a pure equilibrium, and FIP-consistent if every such game has the FIP. The class can be infinite or empty. In the results below, continuity always includes the endpoint zero. “Monotonic” means nondecreasing or nonincreasing, with the direction allowed to differ between functions.
The goal is Theorem 5.1, p.427. For a set of continuous functions, the following are equivalent:
The exponential rate is shared by the entire class. No coefficient or rate is subject to a sign or nonzero restriction. The disjunction is inclusive, as printed in the theorem: classes of constant functions satisfy both alternatives.
Six source milestones support this target. Lemma 3.1 characterizes monotonicity by local right-hand comparisons with . Lemma 3.2 supplies positive loads with either or the reversed inequalities. Lemma 3.4 asserts monotonicity of the integer hull with offsets
under unrestricted consistency. Proposition 5.1 uses consistency for exactly three players to obtain monotonicity of both restricted hulls
Lemma 4.1 equates monotonicity of every integer combination of two continuous monotonic nonconstant functions with affine dependence between them. Lemma 5.1 equates monotonicity of the translated-function hull with each function being affine or exponential; its rate may depend on the function. The source locations are pp.422–427, §§3–5.
The classification separates structural guarantees from favorable individual instances. A class that fails the displayed alternatives cannot guarantee a pure equilibrium for every admissible game. Conversely, either alternative guarantees termination of strict improvement paths as well as equilibrium existence. This gives a precise answer to the unrestricted consistency question posed by Harks and Klimm, without imposing nonnegative or increasing costs.
The mathematical results are published results, not new conjectures. The remaining task is their machine-checked proof. This draft supplies compiled definitions and theorem statements; the seven theorem bodies remain proof targets. Its reusable components include the finite weighted game model, universal class predicates, and three different integer hulls. Published pure-equilibrium and improvement-path definitions are reused through their existing interfaces.
Monotonicity of individual resource costs does not settle the unrestricted problem. The selected statements impose conditions on combinations of functions, and those conditions distinguish the allowed class-wide structure. In particular, separate exponential representations for every member do not establish the common-rate alternative. Another logical obstacle is that an improvement cycle alone need not rule out an equilibrium elsewhere in a game's profile space. The source's nonexistence arguments must exclude every feasible equilibrium, not just exhibit cycling behavior. These distinctions are visible in §§3–5.
The findings accompanying this mission record local issues in printed proofs separately from their theorem statements. Such issues do not authorize stronger hypotheses or weaker conclusions in the faithful targets.
Players and facilities are indexed by finite initial segments with strictly positive sizes. Strategies are finite subsets, and feasible strategies are subtypes of the specified nonempty families. This represents every finite game up to relabeling. Demands are strictly positive nonnegative reals, loads are finite sums, and private costs are ordinary reals. Payoff-maximizing published definitions receive the negative of the private cost. Finite profile spaces justify the equivalence of the published infinite-path FIP convention and the paper's cycle convention.
Consistency is defined by quantification over all admissible games; neither potentials nor the classification are included in admissibility. The hulls are constructed from integer coefficients and the stated translates, without selecting only their monotonic members. Continuity is imposed on the whole nonnegative domain. These choices exclude vacuous proxy models and restricted strategy classes. The empty class and constant functions remain included. No asymptotic estimates or extracted constants occur.
The twelve new definition items precede the seven theorem items, and the six numbered source milestones retain their provenance. No optional variant is posed. The independent two-player characterization and the network and singleton results are outside the mission. In particular, the correction notice on p.436 concerning finite rather than polynomial termination does not introduce an algorithmic target here. Contributions should complete the faithful statements and their needed supporting theory while preserving these conventions.
An accepted call earns revenue but occupies circuits that could serve later calls. In a network, those consequences extend beyond the links used by the original call: a change in blocking on one link changes the traffic reaching other links. Network planning therefore needs a marginal value that accounts for these indirect effects. Chapter 4 of Kelly and Yudovina's Stochastic Networks develops such values for the Erlang fixed-point approximation. The relevant question is how revenue changes when offered traffic or installed capacity changes, with the network allowed to settle to its new fixed point.
The mission concerns this sensitivity calculation. It complements the scalar Erlang formula and fixed-point uniqueness results, which already have published formalizations. It does not claim that the approximation equals the exact stationary performance of the underlying stochastic loss network.
A loss network has finitely many links and routes. Link has a positive integer number of circuits. A call of route requires circuits at link , where the matrix entries are nonnegative integers. Its offered traffic is , and carrying it earns a real value . Every link in the stated system is used by at least one route.
The Erlang fixed point assigns a blocking probability to each link. In the independent-link approximation, the acceptance probability and carried traffic of route are
Write for carried circuit load and for reduced offered load. The defining equations are , where is Erlang's scalar blocking formula. Revenue is .
The capacity derivative requires an additional convention. The scalar Erlang formula is extended by linear interpolation between successive integer capacities, and the network fixed point is then recomputed using that extension. At the original integer capacities, capacity sensitivity means the derivative from the left. Interpolating the final network revenue would define a different function. These conventions are specified on printed page 102 of the supplied source.
The goal is Theorem 4.6, printed page 103. Define the improvement quantity
There is a unique route-surplus vector and link-cost vector satisfying
The goal asserts existence of the derivatives and their values:
Uniqueness concerns all solutions of the local cost equations, independently of whether they also satisfy a derivative identity.
Three source milestones support this target. Exercise 1.8 gives the scalar Erlang traffic derivative. Theorem 3.20 supplies existence and uniqueness of the integer-capacity fixed point. Both are reused as published references. Exercise 4.9 supplies the matrix characterization. With and , it states
The symmetric matrix is positive definite and invertible, and the unique costs are
These are the claims of Exercise 4.9, printed pages 106–107, including both the equivalence and the explicit solution.
An implied cost assigns the marginal revenue effect of capacity to an individual link. A route's surplus compares its direct value with the total implied cost of the circuits it uses. The theorem thus relates local quantities to derivatives of a network-wide objective. As explained in Remark 4.7, the link costs are also shadow prices for capacity. Their interpretation includes the effect on later traffic, rather than just the revenue of the currently admitted call.
The formal contribution is the precise connection between the actual fixed-point revenue function, one-sided capacity sensitivity, and the unique local linear system. The published scalar derivative and fixed-point theorem remain references, not duplicate problems. The new definition layer and matrix characterization provide reusable objects for later formal work on routing and capacity sensitivity. The submitted theorem statements are proof obligations; successful compilation does not supply their proofs.
Differentiating revenue while holding the blocking vector fixed misses the indirect effects that the theorem measures. Blocking is itself an implicit function of all offered traffics and capacities. Moreover, the scalar interpolation has corners at integer capacities, so ordinary two-sided capacity differentiability is not the required statement. The formal obligations include existence of the appropriate derivatives; merely evaluating a total derivative operator would not establish that existence.
The printed proof explicitly treats a – incidence matrix, whereas the surrounding fixed-point model allows arbitrary nonnegative integer circuit requirements. Finding F2 records this proof-scope gap. The goal retains the general integer statement. Exercise 4.9 also requires legitimate denominators and an invertible matrix; these properties must be established from the network data rather than supplied as assumed conclusions.
Links and routes use finite, zero-based index types. Values, traffic, and blocking coordinates are real. The base capacities are positive integers, offered traffic is positive, and each link is used. The last condition states the domain of the printed weighted-average quotient: an isolated link would make its denominator zero. No injectivity or rank condition on the incidence matrix is imposed. Empty link sets are allowed; in that case every route has acceptance one and revenue is linear in offered traffic.
The scalar Erlang formula and integer fixed-point relation reuse the series' published definitions. The new physical fixed-point selector is constructed from the interpolated equations, with a total fallback outside the existence domain. Its definition assumes no differentiability or cost identity. The goal additionally verifies the selected integer-capacity vector against the published fixed-point relation. A formalization that assumes the sensitivity identities, or replaces revenue by an arbitrary function constrained to satisfy them, would trivialize the target and is excluded here.
No asymptotic notation or unspecified constants occur in these targets. Exercise 4.8's marker-route reduction is left as a proof resource rather than a separate milestone. The queueing-cost strict-convexity assertion in Exercise 4.7 is outside this loss-network mission; its counterexample remains recorded as F1. Finding F3 records why the displayed improvement formula cannot simply be extended to noninteger base capacities: at unit load and capacity , a single-link example gives actual capacity derivative but cost formula . No variant item is posed.
Communication connections can demand bandwidth at rates that fluctuate over time. Reserving every connection's peak rate can leave substantial capacity unused, while reserving only its mean rate allows temporary overloads and queueing delays. Effective bandwidth provides a way to express the statistical cost of a source in terms that can be used in admission decisions. Chapter 6 of Kelly and Yudovina's Stochastic Networks develops this question first for an instantaneous aggregate load and then for a resource with a buffer.
The buffered model distinguishes the number of connections from the number of connection classes. The number of classes stays fixed while capacity, buffer size, and the number of connections all grow together. The object of interest is the exponential rate of the probability that the workload exceeds the buffer level. This rate measures rare overloads on a scale where ordinary convergence of probabilities to zero loses the relevant information.
A source increment is the work arriving during an interval from connection of class . The classes form a finite set . A source supplies nonnegative, additive increments, with no work on an interval of length zero. Each interval workload is a measurable real random variable. Different source processes are independent, copies within one class have the same process law, and increments have stationary distributions: the law of an interval's workload depends only on its duration. Independence between increments of one source is not required.
Let be the natural number of class- sources in a base system. At positive integer scale , there are copies. The aggregate arrival is
A server of capacity , where , processes this work. Its infinite-past workload at time zero is the random variable
This is the construction in equation (6.4), not an independently chosen stationary queue size. It can be infinite. With a positive base buffer , the overflow probability is .
The logarithmic moment generating function of a class- increment is
Exponential moments are assumed finite locally around zero for each finite duration, following the chapter's MGF convention; a larger tilt may have infinite expectation. The quantity is the nonsingular expression for the product in the book's effective-bandwidth formula.
The goal is Theorem 6.10, printed page 145 of the supplied Lecture Notes PDF:
The supremum over duration remains outside the infimum over tilt. Both the continuous time domain and the infinite horizon are part of the target.
Three source milestones accompany the goal. Equation (6.1) asserts, for a measurable real random variable and ,
including infinite exponential expectations. Theorem 6.2 asserts the exact logarithmic rate for an iid sum exceeding . Its assumptions include a mean below , a positive probability of exceeding , local MGF finiteness, and an optimizing tilt in the interior of the finite-MGF domain. Exercise 6.9 gives both the two-sequence and finite-sum largest-term principles, with finite real rates and positive sequences. It makes no assertion about a countable sum.
The goal relates the statistical characteristics of individual connections to the overload behavior of a large system. It retains duration as a variable, allowing temporal dependence within a connection to affect the rate. A fixed-time tail probability alone does not describe the workload accumulated from an unlimited past. This distinction is central to the buffered model in Chapter 6.
The formal deliverable specifies the source family, its scaling, the workload construction, and the variational expression in one consistent setting. It also separates extended expectations from finite real expectations, so the meaning of a rare event does not change when its probability is zero. These definitions can support later work on queueing large deviations without requiring a finite-state Markov model.
The local theorem files are declarations to be proved, not completed proofs. A published proved Chernoff bound is retained as a reference for the integrable exponential case. The separately published open Cramér theorem assumes finiteness at every real tilt and a closed tail event; it is not substituted for the chapter's local-MGF, strict-tail statement.
The source explicitly gives only a sketch for Theorem 6.10. Fixed-time exponential limits do not by themselves determine the exponential rate of a sum over infinitely many times. Exercise 6.9 establishes a finite-sum result, so it cannot close this gap. The continuous-time workload also raises a measurability and time-discretization issue. Finding F1 records the missing justification with an explicit array of exponentially small terms whose count grows exponentially.
Finding F4 gives an explicit counterexample to the printed goal, even with positive buffer and mean load below capacity. Independent sources have uniformly random phases of a periodic arrival rate taking values 0, 1, and 2. Each source contributes at most one unit of net input over any interval, so with the strict overflow probability is zero at every scale. At duration 2, however, the maximum input 3 has probability , giving a finite variational value . The faithful goal is retained as printed and is expected to be disproved; no corrected variant is proposed. This is a failure of the fixed-time application of Cramér’s theorem at a support endpoint, separate from F1’s infinite-time gap.
Finding F2 concerns a different finite-sample step in the proof of Cramér's theorem: convergence of a tilted-window probability to one half does not ensure it is at least one half for a given sample size. The limiting theorem is retained. Neither finding is converted into an extra hypothesis or a variant. The goal carries no uniform temporal decay estimate, mixing assumption, or fixed-time large-deviation conclusion as an assumption.
The formalization uses Mathlib probability measures, independence and equality-in-distribution predicates, nonnegative Lebesgue integrals, and extended-real order topology. Whole source paths are independent; this is stronger information than independence of one chosen interval's workloads. Natural multiplicities provide exactly copies without rounding. Source indices begin at zero, and the asymptotic scale is represented as to avoid a zero denominator.
The queue supremum is over all nonnegative real times and takes values in EReal. Zero overflow probability has logarithm ; infinite exponential expectation has logarithm . The rate subtracts only finite linear terms. Zero multiplicities contribute zero, including when an unused source has an infinite MGF. At zero time or zero tilt, the log MGF is zero under the source assumptions. No division by is introduced.
Nonnegative additive increments use the usual half-open interval convention for endpoint arrivals. Measurability of the constructed workload is explicit, as required for the source's random-variable language. The model API also requires a probability measure and the relevant measurability when forming an overflow probability or exponential rate. Capacity and buffer are positive; F3 records a deterministic counterexample to extending the goal to zero buffer. Empty class sets and zero source counts remain permitted and give no overflow. For Exercise 6.9, positivity and a nonempty finite index set prevent default logarithms or maxima.
The goal must not be replaced by a finite-horizon queue, a deterministic drift inequality, or a hypothesis already asserting the desired asymptotic. No selected result uses an unspecified asymptotic constant, so there is no constant to instantiate. No variant is posed. The model module supplies real definition bodies; theorem statements expand the relevant formulas so standalone blind read-backs can inspect their meaning without resolving unpublished imports.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.A network of queues records both how many customers occupy each location and how they move between locations. These are different kinds of information. A simple distribution for the occupancies at one time need not make the arrival streams simple, or make the queues independent over time. Open migration processes provide a setting in which the distinction can be studied precisely: customers can move through a finite network, enter from outside, and eventually leave. Chapter 2 of Kelly and Yudovina, Stochastic Networks develops their equilibrium structure.
The target concerns what an observer sees when a stationary network is run backwards. It says that the reversed random process belongs to the same class of models, even when its rates differ from those of the original process. This structural result is the setting for the source's subsequent conclusion about Poisson exit streams. The mission treats the process statement itself, keeping the distinction between an equilibrium rate calculation and a statement about a random trajectory.
There are a finite positive number of colonies. The state is , where counts individuals at colony . There is no upper bound on an occupancy or on the total population. A transition can transfer an individual from colony to a different colony , remove one from the system at colony , or introduce one at colony .
The corresponding rates are , , and . The coefficients are nonnegative, , and the service factors satisfy and when . A departure requires an individual to be present. Immigration rates do not depend on the occupancy. These are the rates in Section 2.4 of the supplied source, printed pages 30–31.
A Markov process here consists of measurable random variables on one probability space, indexed by real time. Its conditional future distributions depend on the most recent state, through a time-homogeneous transition function. Transition rates are its right-hand infinitesimal transition probabilities. The standing assumptions from Section 1.1 are explicit: the process is irreducible, every state has a strictly positive finite exit rate, and sample paths have only finitely many jumps on each bounded interval. A stationary law is a positive normalized mass function giving the distribution at every time.
The goal is Theorem 2.9, printed page 32 of the supplied PDF:
Three milestones support this target. The partial-balance equations (2.3) and (2.4) are grouped as one milestone because one published theorem supplies both identities. They express equilibrium flux balance for transitions associated with a colony and with the outside world. Theorem 2.8 gives the normalized product-form distribution. With positive traffic parameters satisfying
and finite normalizing sums , that distribution is
The third milestone, Proposition 1.1, concerns a stationary process on a countable state space. Its reversed process has the same stationary law and rates
All three source statements are in Kelly and Yudovina, printed pages 16–17 and 31. The goal does not assume the product form, a reverse-process Markov property, or any of the reverse-rate identities.
The result identifies a class of stochastic networks that remains closed under reversal of stationary time. It does not assert detailed balance or equality of the original and reversed rates. It also does not infer independence of colony trajectories from independence of occupancies at one time; the source expressly distinguishes these statements on printed page 32. This separation is needed when interpreting the Poisson exit-stream consequence on printed page 33 of the source.
Published formal results already supply partial balance, normalized full balance, and the algebraic reversed migration rates. They are included as references rather than repeated as new theorem statements. The remaining formal targets concern the actual countable-state random processes: the Markov property of the reversal and preservation of the open-migration class. The new definition layer also provides finite-cylinder and nonexplosive-path specifications that can be reused for other countable-state stationary models.
A formula for a reversed rate matrix alone does not establish a theorem about the reversed process. The latter has finite-dimensional distributions, measurable coordinates, and nonexplosive paths. These must all be connected to the rates. The occupancy space is countably infinite even though the number of colonies is finite, so finite-state reversal theorems do not directly cover the goal. Similarly, assuming the candidate product distribution as part of the meaning of a stationary migration process would omit part of the source's claim. The definition deliberately leaves the stationary law unspecified.
Colonies are represented by with ; states are unrestricted functions from this type to natural numbers. The zero-based colony labels differ only typographically from the source's labels . The exact published migration operators and rate functions are reused. Their natural-number subtraction is protected by vanishing service factors at zero and a zero routing diagonal. Empty products equal one. Normalizing sums in the referenced product-form result use HasSum, so divergent real sums cannot acquire a default value and masquerade as finite normalizers.
The process definitions use probability measures, measurable coordinates, stochastic transition functions, finite-cylinder identities, and locally finite jump paths. Cylinder identities avoid conditioning by division at null events. The state space is countable with measurable singletons, and rate rows are explicitly summable. Positivity of the stationary mass function prevents a zero denominator in the reversal formula. Paths may take either adjacent value at a jump, accommodating the reversal of the right-continuous endpoint convention; isolated zero-duration spikes are excluded.
The goal must establish migration dynamics for the actual map ; an algebraic rate identity or independence at a single time is not a substitute. No asymptotic constants or failure probabilities occur in these targets. The infinite-colony extension, Poisson departure processes, Little's law, Bartlett's theorem, and renewal-reward variants are outside this mission. The findings register preserves observations about out-of-scope source displays, but no variant theorem is proposed. Contributions to the countable-state stochastic foundations and proofs of the two draft theorem statements are within scope.
ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.A semidefinite constraint asks whether a symmetric matrix is positive semidefinite: every vector must have a nonnegative quadratic form under that matrix. In optimization, its entries can depend on a decision and on uncertain inputs. Requiring the constraint for every possible input can be restrictive, especially when rare inputs have very large magnitude. A chance constraint instead requires the matrix inequality to hold with a specified probability. Chapter 10 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops safe approximations for such constraints, including conic quadratic constraints represented through symmetric matrices.
The question here is how a known probability of a moderate matrix perturbation can imply a much higher probability at a larger threshold. The chapter gives explicit answers for bounded independent perturbations and for independent standard normal perturbations. The goal is its Corollary 10.1.3, including both distributional cases and the possibility that the reference matrix is singular.
Let be deterministic symmetric real matrices, with . The random perturbation is
The Loewner order means that is positive semidefinite. Thus the event controls the perturbation simultaneously in every vector direction. For normalized matrices, denotes the operator norm for Euclidean vectors, rather than a maximum entry or a row-sum norm.
The random coordinates are measurable and independent on a probability space. Under assumption A.I they have zero means and satisfy almost surely. Under A.II each has the standard normal law . The deterministic variance certificate is
This is precisely system (10.1.13) in the source. A separate premise supplies the base probability
where and . Neither this probability premise nor the certificate contains the amplified probability conclusion.
Write for , and for its inverse upper-tail quantile. The book writes these functions as Erf and ErfInv. Its Erf is a one-sided upper Gaussian tail; substituting the common analytic error function would change every Gaussian bound.
The goal, Corollary 10.1.3, asserts that under A.I, for every ,
Under A.II and the additional condition , it asserts
Both conclusions retain the constants and strict threshold of equations (10.1.15)–(10.1.16).
Three source-numbered milestones support this goal. Theorem 10.1.1 concerns symmetric with and defines . Its bounded-case conclusion is
Theorem B.5.1 concerns a closed convex set with standard Gaussian mass at least . It asserts that contains the centered ball of radius . If it contains a centered ball of radius , then for ,
Its further conclusion covers centered Gaussians with arbitrary positive semidefinite covariance: an outside probability at most becomes at most after dilation. This clause includes degenerate covariance matrices.
Theorem 10.1.2 is the normalized Gaussian matrix milestone. With the same variance normalization and exact base mass , it states, now for ,
The chapter’s bounds connect a matrix certificate and a base confidence level to explicit larger-threshold confidence guarantees. They preserve information about the reference matrix, including its null directions. A statement requiring positive definiteness would exclude part of this conclusion.
These are established textbook results whose Lean proofs remain the targets of this mission. The draft supplies concrete definitions and open theorem statements, not completed proofs. Mathlib already provides probability measures, normal distributions, matrix positivity, and a semidefinite Schur-complement equivalence. The published theorem PinningSync.Tree.lemma_2_13 supplies the positive-definite Schur-complement branch as a reference; it is not presented as a substitute for the full semidefinite lemma.
The target combines probabilistic concentration with inequalities that must hold in every matrix direction. Entrywise bounds do not state the same event. Likewise, an invertible reference matrix is a restricted case of the goal. The Gaussian branch also requires exact control of inverse-tail conventions and dilation probabilities for general closed convex sets. The source’s proof of Theorem B.5.1(i) has inconsistent tail arguments in its separating-halfspace paragraph, recorded as a proof warning; the theorem statement retains the printed .
All matrices are real, finite, and explicitly symmetric in the theorems. Matrix and perturbation dimensions are positive; indexing by Fin changes only the origin of the indices. The setup uses Mathlib’s positive-semidefinite predicate directly. The two matrix inequalities are defined by their positive-semidefinite differences, and the variance certificate is an existential block-matrix condition. The Gaussian geometric theorem uses the concrete standard and multivariate Gaussian measures on Euclidean space, with a positive-semidefinite covariance premise.
Formalization Note. Equation (2.3.22) specifies the inverse tail on , while the later statements allow base mass one and failure probability zero. The draft retains those cases by using the extended-real inverse quantile, with , , and the limiting exponential envelope zero at infinity. An infinite-radius centered ball is the whole space. All displayed formulas agree with the source on finite quantile arguments. This endpoint interpretation is recorded in the findings for review, rather than imposing an unprinted restriction.
The reusable components are the matrix perturbation, the two-sided order event, the block certificate, and the Gaussian tail conventions. Proof contributions must establish the full statements with their constants and endpoints. No variants are posed in this mission.
Permutation operators encode the symmetries of many identical quantum systems. When one tensor factor is transposed, the resulting operators occur in questions about the commutant of mixed tensor representations and about partially transposed quantum states. The usual symmetric-group algebra no longer describes their multiplication: a product can acquire a factor equal to the local dimension . Mozrzymas, Horodecki, and Studziński determined the full algebraic structure of their span in their 2014 paper. Their description identifies its simple components even when a small local dimension makes the natural spanning family linearly dependent.
Let and . On tensor factors of , the permutation operator moves the computational-basis tensor indexed by to the tensor indexed by . Write for matrix transposition on the last tensor factor only. The object of this mission is the complex operator algebra
The subspace is spanned by those for which . Its complement in the result is an ideal that annihilates on both sides. The permutations of the first positions act on . For each irreducible representation of that occurs in this action, write . Definition 40 constructs operators from their matrix coefficients, the permutation operators, and partial transposition. Their span is .
Definition 29 assigns to a block matrix indexed by and , where and . Its block is , so every diagonal block is times the identity. Finally, a partition of labels an irreducible representation of ; counts the rows of its Young diagram.
Theorem 30 asserts that splits into mutually annihilating ideals, and that those ideals split further into full matrix algebras:
When , the summand has order . The goal also includes the multiplication law for the operators, with coefficient as in equation (6) of Proposition 44. This identity specifies how their natural generators multiply even when is singular. The two cases for printed in Theorem 30, and , give the same uniform restriction because every partition of has at most rows.
The theorem identifies the simple ideals and their sizes from representation data of two smaller symmetric groups. It separates the dimension-dependent part , where the rank of may drop, from the part controlled by partitions with fewer than rows. Consequently, it determines the irreducible representations of this concrete operator algebra and explains why its decomposition changes with .
The result is proved in the cited paper; this mission asks for a machine-checked proof of its precise statement. The published operator model and tensor-permutation definition already fix the underlying matrices. A completed development would add reusable facts about partial transposition, ideals of represented group algebras, matrix units arising from singular coefficient matrices, and occurrence of symmetric-group representations. The read side of this mission is an open theorem, not a claim that Theorem 30 has already been formalized.
The natural spanning elements are not a basis when , and the can also be dependent. Counting generators therefore cannot establish the orders of the matrix ideals. The matrix records those dependencies; its rank, not its number of rows, governs the summand. The complementary ideal requires tracking which representations of survive after the component is removed. A dimension count alone would identify neither the actual ideals nor their matrix-unit multiplication laws.
Operators are matrices indexed by functions Fin n → Fin d, a coordinate model of . The last-factor transpose is the published ptLast; and are the published complex spans algA and algM. The paper's labels become Fin (m+1), and its last label becomes Fin.last (m+1). Permutations multiply right to left. The irreducible family is represented by real orthogonal matrices, hence by unitary complex matrices after casting; the explicit completeness condition ensures that every irreducible of is present in the family.
Occurrence means that a nonzero intertwiner embeds an irreducible into the action on exactly . An ideal is a complex subspace of closed under multiplication on both sides. An assertion requires linearly independent matrix units spanning and obeying the matrix-unit law; it cannot be discharged by a dimension count. For this requires . The order is represented by the number of standard Young tableaux of shape , using the classical symmetric-group dimension formula. The goal permits and requires .
Theorem 30's displayed coefficient conflicts with Proposition 44's equation (6), ; the latter agrees with the matrix-index contraction and is used here. Contributions toward the listed source results, the partition occurrence criterion, and the singular-matrix algebra reduction are useful. An arbitrary family of subspaces with the right dimensions does not meet the target: the statements fix , , , , and the matrix-unit structure of each component.
A quantum circuit may create a state whose full list of amplitudes is far too large for a classical computer to store. That fact alone does not show that every observable feature of its output is hard to estimate. In Simulating quantum computers with probabilistic methods, Van den Nest asks when classical sampling can reproduce the accuracy of a quantum experiment that estimates an observable's expectation. The paper's Theorem 1 identifies a condition on the input state and on the observable after it is pulled back through the circuit, rather than requiring the circuit itself to have a sparse matrix. This separates the cost of describing a whole output state from the cost of estimating the particular quantity measured at the end. Van den Nest, §§1–3
The paper distinguishes weak simulation, which achieves the accuracy available from polynomially many experimental runs, from strong simulation, which asks for much finer numerical precision. This mission addresses the sampling estimate behind the former. The source's 2010 preprint proves an efficient classical algorithm under computational assumptions; the formal target below states its finite probability guarantee for the particular estimator in that proof. Van den Nest, pp. 2, 6–7
An -qubit computational basis has labels . A state has complex coefficient at each label, with . Measurement in this basis yields with Born probability . A state is computationally tractable (CT) in the paper when these probabilities can be sampled, and individual coefficients can be evaluated, in polynomial time. The finite development below represents the resulting sample and coefficient access directly. Van den Nest, Definition 1, p. 8
For a matrix , the entry is its transition from basis label to label . The operator is -sparse if each row and each column has at most nonzero entries. Its column data consist of coefficients and row labels for , with . Nonzero coefficients in a column occupy distinct rows. The paper calls such an operator efficiently computable sparse (ECS) when the nonzero entries can also be found efficiently. Van den Nest, §4.3, pp. 10–11
For two normalized states , write . The paper defines bounded complex functions and from the column data, separating each contribution according to whether . The estimator is the sum over of a sample mean of under and a sample mean of under . The same independent draws from each law are used for every in this formalization. Its target is the matrix element . Van den Nest, Eqs. (5)–(8), pp. 12–13
The main result concerns a unitary , a Hermitian observable with spectral norm at most one, and the pulled-back operator . When is -sparse and has the stated column data, the estimator targets the output expectation . For samples of each kind and , the target is
The paper states Theorem 1 as an efficient simulation claim. The displayed explicit tail is obtained from its Theorem 3, the pointwise bounds on and , and Appendix A's Chernoff–Hoeffding estimate. Its exact constants are a commitment of this finite accuracy target, not a constant printed in Theorem 1. Van den Nest, Theorem 1, p. 2; Theorem 3, p. 11; Eq. (18), p. 23
The milestones follow the paper's supporting statements: the real and complex sampling bounds, the sparse matrix-element decomposition, the two expectation identities, the bound on , the row-preimage count, the bound on , and the general matrix-element estimate of Theorem 3. Theorem 3 permits two different normalized states and a sparse operator that need not be unitary. Its specialization with and gives the target above. Van den Nest, pp. 11–13, 23
The theorem gives a concrete error probability for recovering an output observable's expectation from classical samples of the input state. The condition concerns ; it allows the circuit matrix itself to be dense. Thus it applies to circuit and observable pairs for which output-state enumeration is a poor guide to the cost of this particular expectation estimate. The paper develops consequences for local observables and other circuit families after Theorem 3. Van den Nest, Theorem 1 and §5
A formal development would make the finite probability claim, the sample-access model, and the spectral-norm assumptions independently checkable. The paper's theorem is proved mathematically, but this mission's Lean theorems are open statements awaiting proofs. In particular, machine-checking the explicit estimator's accuracy is separate from representing a polynomial-time classical machine, which this mission does not undertake.
Sparse columns make a sum of terms indexed by , but they do not by themselves give a bounded random variable when a term is sampled from . Dividing by a small may create a large weight. Sampling from has the analogous problem in the opposite direction, and the row labels need not be injective as functions of . The paper's two functions split those regimes; its row-sparsity condition controls the number of terms that can contribute to one . The proof must also keep the complex modulus, the strict failure event, and the shared sample sets consistent with the finite probability law. Van den Nest, proof of Theorem 3, pp. 12–13
Lean represents basis labels as functions Fin n → Bool, states as finite complex coefficient vectors, and operators as complex matrices. The operator bound uses the published spectral norm QAlgorithms.specNorm. Theorem 1 assumes a unit vector, a unitary matrix, and a Hermitian observable of norm at most one. The general Theorem 3 uses any finite basis and two normalized coefficient vectors. Column data can enumerate nonzero entries in any order; the proof needs their values and distinctness, while the paper fixes top-to-bottom order. All expectations and event probabilities are finite sums. No measurable-space conventions or Bochner-integral defaults enter.
The estimator is fixed by the definitions of , , and their two sample means. It reads sampled labels, state coefficients, and sparse column data. It cannot read the target matrix element, enumerate all basis labels to output the answer, or inspect and outside the supplied column data. The model asserts the accuracy that these accesses support; it does not certify that sampling, coefficient evaluation, column enumeration, or the circuit family run in polynomial time. This is the precise part of the paper's classical simulation statement represented here.
Positive avoids the undefined statistical meaning of an empty sample mean. The split assigns equality to . A zero Born probability has zero sampling mass; the corresponding totalized quotient is set to zero. For , the sparse matrix and estimator are zero, and the theorem's failure bound is zero. The displayed bound is the one derived from the paper's inequalities; the complex-valued intermediate constant is likewise derived from Eq. (18). Reusable contributions include the finite product-sampling concentration theorem, the column-data representation, and the matrix-element decomposition. Van den Nest, pp. 10–13, 23
Quantum devices rarely prepare the state they are asked for. A procedure meant to output a pure state on levels often outputs a mixed state , the result of noise during preparation. If the procedure can be run times, the copies can be processed jointly into a single output closer to . This task is quantum purity amplification (QPA), also called purification. It appears as a primitive in error mitigation, in state preparation on near-term hardware, and in the theory of quantum state estimation and cloning.
For qubits and depolarizing noise, Cirac, Ekert and Macchiavello found the optimal protocol in 1999 (Phys. Rev. Lett. 82, 4344), and Keyl and Werner determined the rate of optimal purification procedures (Ann. Henri Poincaré 2, 2001), with the minimum fidelity as figure of merit. For qudits () the optimal protocol remained open. Childs, Fu, Leung, Li, Ozols and Vyas gave a streaming protocol (arXiv:2309.16387), and Grinko and Ozols reduced unitary-equivariant SDPs of this type to linear programs (arXiv:2207.05713) without solving this one in closed form. Li, Fu, Isogawa, Silva and Chuang (arXiv:2409.18167, version 4 of 25 Dec 2025) solve the qudit case exactly: they give the Choi matrix of the optimal channel in closed form (Theorem II.1).
Let . An unknown pure state is corrupted by the depolarizing channel of strength :
A QPA protocol is a quantum channel from (the input registers) to (the output register). Its quality at is the fidelity , and the figure of merit is the minimum fidelity .
A channel is described by its Choi matrix , an operator on with and ; the channel is . Averaging the fidelity over a Haar-random gives the semidefinite program (SDP)
with , , and the Haar probability measure on .
The answer is phrased with Young diagrams. A Young diagram with boxes and at most rows labels an irreducible representation of of dimension , and denotes the projector onto the -isotypic part of (weak Schur sampling). The protocol must be covariant under the mixed representation . Inside the -sector this representation splits as , where removes the last box of row of (padded with zeros to rows). Row is feasible if it is the last row or . Let be the smallest feasible row; is with the bottom box of its last column removed. is the projector onto the -isotypic component of .
is feasible and optimal for the SDP. Its channel is a quantum channel. For every channel , . The statement asserts optimality, not uniqueness, and holds for every , , .
The theorem gives the exact optimal purification channel for every , and depolarizing strength, and the channel does not depend on . It has an operational form, worked out in the paper's Sec. II C: Schur sampling, a correction inside each sector, and a partial trace. From it the paper derives the optimal sample complexity for output infidelity (Theorem II.2) and an efficient circuit implementation (Algorithm 1). Both rest on Theorem II.1.
The result is proved on paper but not formalized anywhere. A formal proof would check a chain that mixes semidefinite programming, Haar integration, the Schur–Weyl duality of the mixed representation , and a combinatorial inequality for normalized Schur polynomials (Sra's theorem, European J. Combin. 51, 2016), which is cited and not proved in the paper. Several of these components are general results: the block decomposition of covariant operators, the cost-matrix projection argument for SDPs with a partial-trace constraint, and the dominance ordering of normalized Schur polynomials.
Symmetry reduces the SDP to a linear program in one coefficient per block, but the coefficients of the original cost matrix are hard to evaluate directly. The proof replaces by , whose block coefficients are characters of rational representations evaluated at the spectrum of , and shows that the replacement leaves the optimizer unchanged. The remaining step compares these characters across blocks. That comparison is the Cuttler–Greene–Skandera inequality for normalized Schur polynomials, a nontrivial combinatorial theorem. One natural guess fails: keeping the block of the largest feasible row instead of the smallest gives a channel that is not optimal in general. The optimal block removes the bottom box of the last column, which is generally a different row.
Operators are complex matrices indexed by , output register first. Partial traces are the published WildeQIT.partialTraceLeft/Right. The Haar measure is the published probability Haar measure QAlgorithms.Schur.unitaryHaar d on , and Haar integrals of matrices are taken entrywise. Young diagrams, Schur polynomials, dimensions (semistandard tableau counts), Schur modules with their polynomial representations, and the weak Schur sampling projector come from the published QAlgorithms.Schur layer; channels are QAlgorithms.IsChannel (finite Kraus families). Rows are 0-based in Lean.
The irreps of the mixed representation (Nguyen, arXiv:2310.01613) are rational: when has fewer than rows, has last row . They are encoded by the determinant shift , a Young diagram with boxes, with . The isotypic projector is the character integral .
Disclosed choices:
Trivializing formalizations are ruled out. is the explicit operator above, computed from and alone, never an argmax or a hypothesis. The cost matrix is the actual Haar integral, not a closed form. The competitors are all feasible and all channels , with no symmetry assumed.
Welcome contributions: the tracing and Pieri-type decomposition of ; Haar orthogonality of characters on ; the equivalence of Choi feasibility and Kraus channels; Sra's inequality. Each is reusable beyond this mission.
Light carries information in electromagnetic field modes. At optical frequencies, photon statistics affect the capacities of thermal-noise and broadcast communication channels. Bounds on these capacities depend on identifying the smallest entropy that a beam splitter can produce under specified input conditions. Guha, Erkmen, and Shapiro explain why two such minimum output entropy claims matter: their first supports the proposed thermal-noise channel capacity, and their second supports the proposed bosonic broadcast capacity region. The paper states both as conjectures and shows that they follow from its Entropy Photon-Number Inequality (EPnI).
The authors model the EPnI on the classical entropy power inequality, but its quantum version concerns density operators rather than probability densities. Their 2007 paper does not prove the EPnI. A later platform theorem, sourced from an OpenAI mathematics preprint codebase, is marked Proved for finite-energy inputs. It supplies this mission's referenced first milestone. The statements here express the paper's two consequences in that same model; their Lean proofs are still open in this proposal.
A bosonic mode has number states indexed by . An -mode state is a positive density operator on the full Fock space indexed by , with trace one. Its von Neumann entropy is . All logarithms are natural. A thermal state with average photon number per mode has weights in the number basis; for modes the state is the product of these single-mode distributions. At this is the vacuum, with zero photons in every mode. A pure state is a projector onto a unit Fock vector. A state has zero mean field when the expectation of the annihilation operator is zero for each mode.
Two independent input states and enter a lossless beam splitter with transmissivity . For each mode its retained output has annihilation operator ; the other output is discarded. The retained density operator is . Independence means that the joint input is ; correlations among modes inside either input are allowed. The thermal entropy per mode is
with the continuous convention at . The entropy photon-number of an -mode state is . Eq. (13) of the paper asserts that the output entropy photon-number is at least times that of the first input plus times that of the second. The source paper gives the definitions in §II.B, p. 2.
The first target fixes the second input to a thermal product state of mean , while the first ranges over zero-mean-field pure states. The second fixes the first input to the vacuum, while the second ranges over states with entropy . For each class, the claimed lower bound and attained minimum are
For the first class the vacuum first input attains equality. For the second, the product thermal second input attains equality. The goal states both claims together, including the existence of an attaining input and output. The shared attack path contains the EPnI, Eq. (13), the scalar properties of and its inverse, thermal state existence and entropy, zero entropy of pure states, the beam splitter's thermal output for vacuum and thermal inputs, and the inequalities of Eqs. (16)–(17). Each milestone uses the statement on pp. 2–3 of the paper.
An attained minimum gives the precise noise floor for the two input classes. In the paper's capacity arguments, the first class concerns the thermal-noise channel and the second the bosonic broadcast channel. The mission records the exact optimizer and the output entropy, including the endpoints and . Without the optimizer's output value, a lower bound alone would not identify the minimum.
The referenced EPnI is marked Proved on Prove2Me under finite-energy assumptions. This mission's thermal-state, pure-state, and beam-splitter statements are draft targets and have no machine-checked proofs here. Closing them would connect the platform's general inequality to the two applications explicitly worked through by Guha, Erkmen, and Shapiro. The thermal-state and entropy facts can also serve other bosonic-channel formalizations using the same Fock-space interface.
The EPnI supplies an entropy photon-number bound, but converting it into an attained output-entropy minimum requires more than substituting a pure input. One must justify that the inverse thermal entropy behaves as expected on nonnegative entropies, that thermal product states really exist in the chosen infinite-dimensional state space, and that vacuum mixed with thermal noise produces the specified thermal output. The last claim is a statement about the full beam-splitter matrix and its partial trace, not just a scalar entropy comparison. Infinite sums also demand care: a formal expression that defaults to zero when it diverges would give a spurious entropy value.
The development reuses OAI.EntropyPhotonNumber.State n, its number-basis matrix entries, real-valued entropy, , the infimum definition of , and the beam-splitter output relation. The new definitions express thermal, vacuum, pure, and zero-mean-field states on that same carrier. The thermal state uses Eq. (10)'s number-basis formula; Eq. (9)'s coherent-state integral is outside this mission. The beam splitter uses the sign convention in the published definition, which yields the paper's retained output . The zero-mean-field condition includes convergence of each annihilation expectation.
There is at least one mode, , since Eq. (11) divides entropy by . Inputs to which the EPnI is applied have finite energy. This assumption is additional to the paper's phrasing: it is required by the referenced platform theorem and prevents the real-valued infinite-series entropy from taking a default zero on a divergent input. The first optimized input is therefore a finite-energy pure state; the second is a finite-energy state of entropy . The thermal and vacuum witnesses themselves have finite energy. These conditions are disclosed in the theorem statements and are not assertions that the unrestricted conjectures have been settled here.
The goal quantifies over every feasible input and corresponding output, states equality for every output from the named optimizer, and asserts that the optimizer and an output exist. This rules out a vacuous result from an empty thermal-state class or a bound that omits attainment. Contributions to the scalar lemmas, thermal-state construction, pure-state entropy, and the beam-splitter output calculation are all within scope. Infrastructure for summable Fock-space matrix entries and operator entropy should remain reusable beyond this mission.
The cyclotomic Birman–Wenzl–Murakami algebra is an algebra of braids and contractions equipped with an additional cyclotomic relation. It connects diagram algebras, representation theory, and knot theoretic constructions. For calculations over a coefficient ring, one needs to know whether the diagrammatic spanning elements remain independent after parameters are specialized. The freeness theorem of Goodman and Hauschild Mosley answers that question for admissible integral ground rings: the algebra has a basis of the size predicted by labeled Brauer diagrams. The paper also identifies the algebra with a cyclotomic Kauffman tangle algebra. This mission targets the algebra's freeness and rank assertion.
The cited paper builds on admissibility relations developed with Wilcox and Yu. Its earlier definitions and preliminary statements already appear in Prove2Me mission 92e1197e-907f-4ab8-92be-01ea44f6cfef. The present mission reuses that published layer and poses the deferred freeness theorem and the intermediate results that support it. The distinction matters because two algebras with similar names but different generators or parameter conventions need not have the same rank statement.
A ground ring is a commutative unital ring with a positive integer and parameters . The parameters are units, and they satisfy
The algebra is generated over by invertible braids , contractions , and an invertible affine generator . It obeys the affine BMW relations of Definition 2.1 and the cyclotomic relation of Definition 2.8. The shared published presentation uses indices for and , corresponding to the paper's and . At there are no generators.
The parameters are admissible when is nonzero and not a zero divisor, weak admissibility holds for every integer shift of the relations, and are -linearly independent in . These are the conditions of Definition 3.3, expressed using condition (1) of Theorem 3.2. A morphism of ground rings preserves all and and permits exactly the four paired sign actions on and in Definition 2.13. Consequently, base change includes the sign twists allowed by the paper.
For the generic case, is the rational function field in algebraically independent variables. Put , set for odd and for even , and define , where is the rational expression in equation (3.6). A shape in is an -tuple of Young diagrams whose total number of boxes is at most and congruent to modulo two. An up–down tableau of shape is a path from the empty tuple to , adding or removing one box at each step. Its set is .
The central target is the freeness half of Theorem 6.1. For every admissible integral ground ring and every ,
Here , so the asserted rank at is one. A basis indexed by a finite type of that cardinality states both freeness and rank.
The milestone path includes the paper's admissibility equivalences, generic parameter construction, universal admissible integral domain, base change, the spanning family of elements, the relevant Jones ideal and Hecke quotient results, and the generic structure results. At the generic field, Theorem 4.8 supplies split matrix blocks indexed by , with block size . The count in the proof of Theorem 5.2 is
which agrees with the generic dimension asserted by Theorem 5.2. The final theorem applies over an admissible integral domain, rather than only over .
The result supplies an exact finite basis for throughout the admissible integral-domain regime. It fixes the module rank independently of a choice of specialization and gives a numerical benchmark for presentations and representations of these algebras. The generic matrix decomposition also records the simple-block labels and their sizes; the tableau identity explains how those dimensions total the same rank.
Goodman and Hauschild Mosley proved these results. This mission asks for machine-checked proofs of the statements already known in the paper. Its reusable output includes ground-ring morphisms with sign twists, the generic parameter model, and finite tableau types. The published preliminary layer in mission 92e1197e-907f-4ab8-92be-01ea44f6cfef contains two proved and four open results among the six referenced milestones; none of the eight new theorem statements is presented here as already machine proved.
A spanning family alone does not show a basis: specializations can introduce linear dependence, and an equality of dimensions over one field does not itself establish independence over every integral ground ring. The argument also has to maintain the exact admissibility conditions when moving between coefficient rings. Over the generic field, identifying the right semisimple blocks requires the branching shapes and tableau sizes, while the final statement concerns arbitrary admissible integral domains. These are distinct algebraic regimes, and the same presentation and parameter conventions must be kept through each one.
Lean uses the published GroundParameters, BMW, BMWAdmissible, UAdmissible, and equation (3.6) gamma expression from QAlgorithms.Papers.Independent.Support21.P14. The algebra is the quotient of a free algebra by the source's relations, with zero-based generator indices. The new definition layer records all four sign cases of Definition 2.13, the generic field as a fraction ring of a multivariate polynomial ring over , and shapes and tableaux as finite-indexed Young diagrams. A generic ground-parameter value is asserted to exist as a theorem because the required unit and compatibility proofs are substantive.
The universal-ring milestone states all five parts of Theorem 3.19 for and ; part (5) is read inside , where the universal -admissible ring is the subring generated by , , and . The base-change statement uses for the source's . Theorem 4.8 is expressed as a product of full matrix algebras with tableau-sized blocks, combining its split and labeling clauses with the block dimensions stated elsewhere in §4. Theorem 6.1's Kauffman-tangle isomorphism is not posed because a corresponding tangle algebra has not been provided here. The cited spanning set is expressed as an indexed family, which remains meaningful when a degenerate coefficient ring identifies elements.
The goal requires an actual basis of cardinality over an admissible integral domain. A mere dimension equality or spanning claim does not satisfy it. Contributions toward the missing generic decomposition, tableau count, base-change isomorphism, and passage to arbitrary admissible domains are all within scope. The ground-parameter and quotient-presentation definitions are reusable independently of this mission.
In this paper, we introduce the notion of a normal form of one qubit quantum circuits over the basis , where , and denote the Hadamard, Phase and gates, respectively. This basis is known as the {\it standard set} and its universality has been shown by Boykin et al. [FOCS '99]. Our normal form has several nice properties: (i) Every circuit over this basis can easily be transformed into a normal form, and (ii) Every two normal form circuits compute same unitary matrix if and only if both circuits are identical. We also show that the number of unitary operations that can be represented by a circuit over this basis that contains at most -gates is exactly .
This mission is the statement-level formalization of Representation of Quantum Circuits with Clifford and Gates (arXiv:0806.3834v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed paper result): unique exact normal form (Theorem 1 (seed paper result): unique exact normal form, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Matsumoto and Amano (2008) showed that every single-qubit Clifford+T operator can be uniquely written of a particular form, which we call the Matsumoto-Amano normal form. In this mostly expository paper, we give a detailed and streamlined presentation of Matsumoto and Amano's results, simplifying some proofs along the way. We also point out some corollaries to Matsumoto and Amano's work, including an intrinsic characterization of the Clifford+T subgroup of SO(3), which also yields an efficient T-optimal exact single-qubit synthesis algorithm. Interestingly, this also gives an alternative proof of Kliuchnikov, Maslov, and Mosca's exact synthesis result for the Clifford+T subgroup of U(2).
This mission is the statement-level formalization of Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators (arXiv:1312.6584v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §1 main result: MA existence, uniqueness, optimality and effective normalization (§1 main result: MA existence, uniqueness, optimality and effective normalization, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum Max Cut assigns a qubit to each vertex of a weighted graph and a two-qubit energy term to each edge. It asks for a quantum state with high total energy. The problem is a quantum analogue of graph Max Cut, but states can be entangled and edge terms act on a Hilbert space whose dimension grows exponentially with the number of vertices. Approximation algorithms therefore need a compact way to reason about the best quantum state without describing that state explicitly. Gharibian and Parekh's 2019 algorithm used product-state rounding for a quantum Max Cut relaxation; Parekh and Thompson's level-2 work showed why stronger quantum relaxations matter. The present paper combines a level-2 relaxation with a different treatment of highly valued edges to obtain a one-half guarantee.
The target is a known result from the pinned version arXiv:2206.08342v2, not an open conjecture. This mission isolates its Quantum Max Cut theorem. The paper also treats other positive 2-local Hamiltonians and a separate guarantee for graphs of prescribed minimum degree; neither is part of this target.
Let be a finite undirected graph with a nonnegative weight on each edge, and put one qubit at each vertex. Write for the three Pauli operators acting on qubit . The edge Hamiltonian and total Quantum Max Cut Hamiltonian are
Every undirected edge appears once. A density matrix is positive semidefinite with trace one. Its energy is , and is the largest energy attainable by any density matrix, including an entangled one.
A Pauli polynomial is a real linear combination of tensor products of . A monomial's degree counts its nonidentity factors. A -positive pseudo-density is Hermitian, has trace one, and satisfies for every Pauli polynomial of degree at most . The level-2 quantum Lasserre relaxation maximizes over all such pseudo-densities. It is an upper bound on the unrestricted quantum optimum, even though itself need not be positive semidefinite. These definitions are from pp. 6–8 of the paper.
For an edge, its relaxed value is . The rescaled value is defined by . Algorithm 4 chooses a threshold , puts every edge with in , and calls vertices incident to no edge in the set . It assigns the two-qubit mixed state to each edge in . Vertices in receive single-qubit states obtained by normalizing three independent Gaussian projections of the relaxation's rounding vectors. The output is the product of those factors, as in equation (5), p. 14. The large edges form a matching at the selected threshold, so those factors occupy disjoint qubits. The Gaussian draw is the algorithm's only randomness.
The goal is the paper's Theorem 3, p. 17. A single threshold must work for every graph and every nonnegative edge weighting:
The level-2 solution used by Algorithm 4 is optimal for the given . The goal also says that the matrix output is a density matrix for every Gaussian outcome. Its threshold is existential because the theorem does not fix a decimal constant; the paper subsequently selects for its analysis.
The fourteen milestones follow the order in which the proof of Theorem 3 uses them.
Equation (7) (p. 17): Gaussian product-state rounding earns in expectation on edge . Lemma 6 (p. 18) reduces to two checks at ; Definition 13 (p. 19) asserts that passes them; Fact 1 (p. 16) is the resulting factor on edges with both ends in . 3. Monogamy. The SWAP Gram matrix of three qubits is positive semidefinite (p. 20). Lemma 8 (p. 22): and imply . Fact 2 (p. 16): if then . Remark 3 (p. 19): the large edges form a matching. 4. Edges touching . Equation (12) (p. 19): earns on a large edge. The last display of the proof of Theorem 3 (p. 19): an edge adjacent to earns exactly .
The theorem guarantees half of the optimum over all quantum states while returning a state built from one- and two-qubit product factors. This is stronger than a guarantee relative only to the best product state: the benchmark permits entanglement. It also explains why a level-2 relaxation has algorithmic value for this problem. The comparison and the claimed approximation factor are established in the paper; formalizing them would leave a reusable verified interface for finite-qubit Pauli polynomials, pseudo-densities, and Gaussian product-state rounding.
The formal work still needed is a machine-checked proof of the known theorem and its milestones. The published register, Pauli, density-matrix and standard-Gaussian-vector definitions can be reused. The source's separate results for other positive 2-local Hamiltonians would need additional models and theorems, beyond this mission.
Level-1 Gaussian product-state rounding alone does not reach one half uniformly: the paper identifies an edge range where its ratio falls below . Large edge values cannot be handled by the same rounding estimate. A level-2 pseudo-density supplies stronger constraints between adjacent edges, but it is not itself a physical state, so ordinary positivity of is unavailable. The source's SWAP matrix and threshold analysis express the needed restrictions. The paper's printed dual certificate for Lemma 8 has a coordinate-order erratum; the lemma's statement remains the target.
Qubits are indexed by Fin n (the paper uses ), with basis Fin n → Bool. Operators are complex matrices. The real part of a trace represents the expectation of a Hermitian expression. The maximum eigenvalue is stated through comparison with every density matrix; for Hermitian , this is equivalent to comparing with its largest eigenvalue. Expected energy is a Bochner integral over a probability measure carrying independent standard Gaussian coordinates. A zero Gaussian projection is assigned Bloch vector zero, giving the maximally mixed one-qubit state at that outcome.
The rounding vectors are given with unit norms and exactly the Gram matrix obtained from the level-2 solution. The output state is computed as the matrix product in equation (5); energy is traced against that matrix. Positivity is required for every real degree-2 Pauli polynomial, and the pseudo-density is required to be optimal. These choices exclude vacuous variants based on degree-1 positivity, free Bloch vectors, or edge energies supplied as assumptions. The finite operator model also covers an empty graph; the approximation inequality there is .
The statement formalizes the approximation guarantee and state validity. The polynomial running-time clause of the paper's general approximation definition is outside this Lean statement. Reusable contributions include the Pauli-polynomial interface, matrix and moment identities for pseudo-densities, integrability and measurability facts for the Gaussian rounding, and the SWAP semidefinite bound.
Gelfand duality identifies compact Hausdorff spaces with commutative unital C*-algebras: a space corresponds to the algebra of continuous complex functions, and continuous maps correspond contravariantly to unital *-homomorphisms (Gelfand 1941; in categorical form, Negrepontis 1971). Measure theory has an analogous expectation. A measurable space with a σ-ideal of negligible sets yields the commutative von Neumann algebra of bounded measurable functions modulo equality almost everywhere, and every commutative von Neumann algebra should arise in this way. Making that expectation precise as an equivalence of categories requires deciding which measurable spaces to allow and which maps between them to identify.
Timeline. Stone (1936–1937) established the duality between Boolean algebras and Stone spaces, and between complete Boolean algebras and extremally disconnected ones. Segal (1951) introduced localizable measure spaces. Dixmier (1951) characterized the Gelfand spectra of commutative von Neumann algebras as the hyperstonean spaces. Loomis (1947) and Sikorski (1948) represented σ-complete Boolean algebras as measurable sets modulo meager sets on their Stone spaces. Von Neumann (1932), Maharam (1958), Ionescu Tulcea (1965), Vesterstrøm–Wils (1969), Edgar (1976) and Graf (1980) gave criteria for lifting homomorphisms of measure algebras to point maps. Pavlov (arXiv:2005.05284, J. Pure Appl. Algebra) assembled these ingredients into one equivalence of categories. That equivalence is the subject of this mission.
An enhanced measurable space is a set , a σ-algebra of subsets of , and a σ-ideal of the power set , the negligible sets. A premap is a map defined on a conegligible subset of with and . Two premaps are weakly equal almost everywhere, , when for every . The space is compact if some compact class (a family with the finite intersection property for all subfamilies) has a non-negligible member inside every non-negligible measurable set. It is strictly localizable if it is isomorphic, through premaps, to a coproduct of a small family of spaces carrying faithful finite measures. CSLEMS is the category of compact strictly localizable spaces with -classes of premaps.
A frame is a complete lattice in which finite meets distribute over arbitrary joins; the category of locales is the opposite of the category of frames. A complete Boolean algebra is localizable if is the supremum of the elements for which carries a finite faithful continuous valuation. MLoc, the category of measurable locales, is the full subcategory of locales on the localizable Boolean algebras. A hyperstonean locale is a Stonean locale (coherent, regular, ) in which every nonzero open has a positive normal valuation not vanishing on it. A hyperstonean space is a sober space whose locale of opens is hyperstonean. HStoneanLoc and HStonean take open maps as morphisms. CVNA is the category of commutative von Neumann algebras (C*-algebras with a predual) and normal unital *-homomorphisms.
The goal is the existence of the four equivalences. It does not fix the functors.
The supporting milestones, in proof order:
The result. Theorem 1.1 replaces commutative von Neumann algebras, a class of operator algebras, by measurable locales, which are pointless spaces. It also gives a point-set model, CSLEMS, in which morphisms are measurable maps modulo a null relation. With it, constructions on commutative von Neumann algebras can be carried out measure-theoretically and transported back: products, pushforwards of measures, and the identification of the predual with valuations. It also explains why the obvious choices fail. With localizable instead of strictly localizable spaces, with equality almost everywhere instead of weak equality, or without compactness, the measure-theoretic category is not dual to CVNA (Remarks 4.23 and 5.18).
Formalization. The theorem is proved in the paper. None of the five categories, and none of the equivalences, has a machine-checked form in Mathlib or on the platform. Mathlib has W*-algebras (WStarAlgebra), locales, Stonean spaces and Baire-measurable sets, but no normal homomorphisms, measure algebras or lifting theorems. The published module QAlgorithms_Papers_Independent_Support21_P20 formalizes this paper's valuations, enhanced measurable spaces and premaps, and poses several lemmas, three of which are milestones here. Completing the mission means formalizing Stone and Stonean duality for locales, the spectral theory of commutative von Neumann algebras through projections, and the von Neumann–Maharam lifting theorem for strictly localizable spaces.
The equivalences in §2 restrict classical dualities and are mostly bookkeeping once those dualities are available. Even so, Mathlib's Stone duality is not stated for locales with open maps. The central difficulty is Proposition 5.16. An object of CSLEMS must be isomorphic, through point maps, to the Stone spectrum of its own measure algebra. In one direction this needs a lifting that is a Boolean homomorphism, and that uses strict localizability through the von Neumann–Maharam theorem. In the other direction it needs a point map from the spectrum back to , constructed from the compact class. The natural first idea, choosing representatives class by class, does not give a homomorphism: liftings exist only through a transfinite construction. A second difficulty is Lemma 5.11. A Boolean homomorphism induced by a measurable map preserves countable suprema, but in general it does not preserve arbitrary ones (Remark 5.12). Compactness and the measurable image of Proposition 4.65 are what rule this out.
All five categories live in one universe, with objects in Type u. The encoding commits to these conventions:
X → Option Y) modulo weak equality almost everywhere. Theorem 1.1's bullet speaks of maps of sets, but with total maps the theorem is false: has no map to (Remarks 4.9, 4.15). Strict localizability uses a small index family and isomorphism in PreEMS; the faithful finite measures of its σ-finite pieces are countably additive maps with absolutely convergent sums (Remark 4.29), because Definition 4.28's saturation clause alone would also admit merely finitely additive ones. Compactness quantifies over arbitrary subfamilies, not countable ones.Locale on localizable Boolean algebras.CStarAlgebras with WStarAlgebra. Normality is stated as "pulls normal functionals back to normal functionals", which is equivalent to Definition 3.3 by Sakai's uniqueness of the predual.The equivalence milestones assert an equivalence together with a description of its functor. They never take a functor as a hypothesis, so none of the statements reduces to rfl or to an instance argument.
Reusable parts:
Contributions are welcome at every level: proofs of the milestones, Stone and Stonean duality for locales, and a lifting theorem.
In quantum mechanics, a system that interacts with an environment is described by a density matrix: a positive semidefinite complex matrix of trace one. When nothing is known about the joint state of the system and its environment, a natural model is to take that joint state to be a uniformly random pure state and to trace out the environment. The resulting law on density matrices, the induced measure of Życzkowski and Sommers (Życzkowski–Sommers 2001), is a standard model of a "typical" mixed state. It is used in quantum information to study the typical entanglement of bipartite pure states, as in Page's conjecture on average entropy (Page 1993).
Nechita (arXiv:quant-ph/0702154v3, Ann. Henri Poincaré 2007) studies the asymptotics of this ensemble. In the regime where the system dimension and the environment dimension grow proportionally, the spectrum of the random density matrix, magnified by , has the same almost sure limit as the spectrum of a Wishart matrix: the Marchenko–Pastur law (Marchenko–Pastur 1967). The mission formalizes this result (Theorem 5) together with the chain of statements the paper uses to derive it.
Throughout, denotes the law of where are independent real Gaussians of mean and variance , so that .
is the induced measure on density matrices. Here is the partial trace over the environment.
Let , let be integers with , and let have law for every . Then, almost surely,
The result. Theorem 5 says that the reduced state of a large random bipartite pure state has a deterministic spectral profile at scale . When , the environment is smaller than the system, and an atom of mass at records that has rank . When , the spectrum fills the interval . The result transfers the classical Wishart limit to the induced measure, and with it quantitative information on the typical entanglement spectrum of bipartite pure states.
Formalizing it. The theorem is proved on paper, and none of it is machine-checked. The mission produces the induced-measure layer in Lean: complex Gaussian matrices, the invariant law on pure states, the partial-trace construction of , and the Marchenko–Pastur law with its atom. Lemma 1 and eq. (12) connect these objects to Wishart matrices. The step that needs the most new library is Theorem 2, the Marchenko–Pastur theorem itself, which the paper quotes without proof. The perturbation step is posed as a statement about weak convergence. The paper argues it through convergence of moments, and in that argument weak convergence of is used as if it gave convergence of moments. The statement posed here is true as stated and needs no moment control.
The reduction from Theorem 5 to Theorem 2 is short on paper. The work lies elsewhere.
The naive route of "taking moments" in the perturbation step fails: weak convergence does not give convergence of moments, so (52)–(53) cannot be compared without extra tightness or moment bounds.
IsPureDensity: Hermitian, idempotent, trace one). A law on is a probability measure on complex matrices carried by that set. Unitary invariance is invariance under (IsPureStateLaw).HasInducedLaw: the law of is the image under the partial trace of some unitarily invariant law on pure states of . Proposition 1 makes this law unique.Fin n × Fin k with the environment on the right. The partial trace is the published WildeQIT.partialTraceRight. is the published SpikedWishart.SoftEdge.stdComplexGaussian, with variance per real coordinate.Solvers are welcome to contribute in four places: