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?
Two-stage stochastic linear optimization is the standard model for decisions taken before uncertainty is revealed and corrected after it: capacity before demand, inventory before transport capacities, generation commitments before load. In practice the probability distribution of the uncertainty is unknown and only historical samples are available, so the stochastic problem has to be replaced by a data-driven one. The sample average approximation (SAA) is consistent but can overfit badly on small samples; distributionally robust formulations hedge against this, but for two-stage problems they are typically intractable.
Bertsimas, Shtern and Sturt (arXiv:1907.07142v4, published as a Technical Note in Operations Research, 2022) study sample robust optimization (SRO): each sample is perturbed adversarially within a small ball intersected with a known support polyhedron. SRO is equivalent to two-stage distributionally robust optimization over a type-∞ Wasserstein ball (Bertsimas, Shtern, Sturt 2018, Proposition 3, as cited on p. 7), and evaluating its objective is NP-hard even for one sample. The paper proposes a tractable multi-policy approximation (MP), with one linear decision rule per sample, and proves that it recovers the optimal value and the optimal decisions of the underlying stochastic problem as the data grow, without assuming relatively complete recourse.
The data are , , , and an affine right-hand side . The second-stage cost of a first-stage decision under the realization is
equal to when no recourse is feasible. With a random vector of law , the stochastic problem is
The support of lies in a known polyhedron . Given i.i.d. samples , a radius and an -norm, the uncertainty sets are and
A linear decision rule is a policy ; the set of them is . The multi-policy approximation chooses, besides , one rule per sample, feasible on its own set:
The single-policy approximation (SP) uses one shared rule for all .
Assume [A1] ; [A2] is finite and ; [A3] the optimal set of (OPT) is nonempty and bounded; [A4] there are and such that around every some linear decision rule is feasible on . Then
and almost surely every accumulation point of optimal first-stage decisions of (SRO) or (MP) is optimal for (OPT).
Theorem 2 says that a linear or second-order cone program with variables and constraints (Proposition 1) is a consistent estimator of the optimal value and decisions of a two-stage stochastic linear program, under assumptions comparable to those for SAA, for unbounded and without relatively complete recourse. Theorem 1 adds that (MP) is always a valid upper approximation of (SRO), so the same limit holds for the intractable SRO problem.
The result is proved in the paper; nothing here is open. No part of it has been machine-checked. A complete development would give a verified model of two-stage linear programs with extended-valued recourse, a verified sample-robust and multi-policy layer, and the polyhedral lemmas on balls intersected with polyhedra (Lemmas 5, 9 and display (3)), which are reusable for other robust and distributionally robust convergence results. The two cited consistency statements (milestones 1 and 7) would be the first formal consistency results for SAA with extended-valued convex integrands.
The upper bound cannot be obtained by plugging an optimal into (MP): need not admit any linear decision rule feasible on a neighbourhood of a sample, and without relatively complete recourse a sample near the boundary of the feasible region may admit none at all. The proof perturbs towards the point given by [A4], which requires the uniform radius of display (3), obtained from an induction over the faces of in Appendix C. Lemma 1's direction [A4] [A6] is a second induction over face dimension (Appendix B).
The lower bound reduces to SAA, but the SAA consistency it needs is for an extended-valued, merely lower semicontinuous convex integrand (King and Wets 1991), for which Mathlib has no epi-convergence theory and no law of large numbers for random lower semicontinuous functions. A uniform law of large numbers on a compact set does not apply: the feasible region need not be bounded and is off a polyhedron.
Vectors are Fin k → ℝ; the -norm is that of PiLp p for an arbitrary p : ℝ≥0∞ with 1 ≤ p, the dual norm is , and the same p is used on in Lemma 3. Every optimal value (, , , the SAA, SRO, SP and MP values, , , ) is an infimum or supremum in EReal: "min" and "max" are read as inf and sup, attainment is never assumed, infeasibility gives , and the factor is the real . The expectation is the platform definition DupacovaWets.Consistency.expect ( when , else ), which agrees with the usual expectation whenever is finite. Samples are ξ 0, ξ 1, …, independent with law and ; the paper's are the first . The radii are deterministic. (MP) is stated as printed with policies. Faces of are nonempty sets , and the relative interior is intrinsicInterior.
Trivializing encodings are ruled out: is not real-valued with a junk value for infeasibility, the expectation is not a Bochner integral of a real truncation, optimal values are not real sInfs, [A4] is the printed local condition and not the global single-rule condition of Proposition 2, and the accumulation-point clauses quantify over sequences that are optimal for all large (requiring optimality at would make them vacuous).
Disclosed readings: the accumulation-point clauses of Theorem 2 hold on one almost-sure event for every eventually-optimal sequence; Lemmas 2 and 3 and display (3) carry §4.2's standing [A2]–[A3], the support condition, and optimality of ; Lemmas 5 and 9 assume the appendix's normalization but not minimality of the representation; display (3)'s set-builder, which omits its bound variable, is read as in Theorem 3; Lemma 2 is stated as printed with , although its proof derives the equivalent form with and swapped.
Contributions welcome: proofs of any milestone, in particular LP strong duality in this inequality form for Lemma 3, the polyhedral Lemmas 5 and 9, and the SAA consistency results, which are reusable beyond this mission.
In the first weeks of the COVID-19 pandemic, diagnostic testing capacity in many countries was a small fraction of the population, and policy discussion centred on waiting for more accurate tests before deploying them widely. Drakopoulos and Randhawa (SSRN 3565245; Management Science, 2021, doi:10.1287/mnsc.2021.4029) treat a test as an information product: an agent's decision to request a test depends on how much the test's result could change that agent's own action. When tests are rationed among those who ask, the accuracy of a test therefore determines not only what is learned from each test but also who asks for one. The paper shows that, under scarcity and uniformly random rationing, a planner can strictly prefer a slightly imperfect test to a perfect one. The result speaks to operations managers and public-health planners who allocate scarce diagnostic capacity, and to the literature on pricing and allocating information goods.
A unit mass of agents has private priors of being infected, distributed with density on and distribution function ; write . An agent who acts (seeks treatment, self-isolates) earns , where is a normalized cost; an untested agent acts iff , with expected utility .
A -test has false positive rate and true positive rate , with ; the -test is the perfect test. The value of the test to an agent is , where is the expected utility of acting optimally after observing the result. Two critical values
split the agents into low-likelihood (, never act), medium-likelihood (, follow the test) and high-likelihood (, always act). Only medium-likelihood agents request a test, so the demand is .
A mass of kits is scarce and is allocated uniformly at random among requesting agents, so each requester is tested with probability . The planner gains for every infected agent who acts and loses for every uninfected one; its objective is the expected net gain over the population (display (9) of the paper with ). Finally
Assume a perfect test is available, , and . Then , and
In the order of the paper's argument:
The result. Proposition 2 gives explicit sufficient conditions, in terms of the density of priors at the extremes, under which accuracy and social value come apart: when many agents have priors near (respectively near ), lowering the specificity (respectively the sensitivity) of the test discourages those agents from requesting it and frees kits for agents whose actions depend on the result. It is the paper's main formal argument against waiting for a perfect test under scarcity, and it isolates the mechanism — demand that responds to test quality — that the paper's later examples and observations build on.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formalization fixes the model unambiguously (who requests, how kits are rationed, what the planner counts) and checks the proof's calculus, including one-sided derivatives at the boundary of the set of tests and a derivative of a parametric integral whose limits and integrand both move. Formalizing the proof also checks the printed derivative , whose middle term is printed as although the condition the paper derives from it, and the corrected computation, give ; milestone 12 states the corrected value.
The planner's objective is defined agent by agent from behaviour, so the first obstacle is to show that the set of requesting agents is exactly the interval (Lemma 1) and to turn into the three-integral closed form; only then is a function of through , and . The second is the derivative at the perfect test. At the thresholds sit at the endpoints and of the prior's support, so the derivatives exist only from one side, the integrand is evaluated at an endpoint where a density is not determined pointwise, and the availability moves with the thresholds. The naive argument "a more accurate test always helps" holds when tests are plentiful (Proposition 1 of the paper, where ); under scarcity the congestion term is what can reverse the sign, and it has to be tracked exactly.
All objects live in the namespace ScarceTesting.PerfectTest, in one definitions file Setting. Conventions:
f with IsPriorDensity f: nonnegative on , interval-integrable on , total mass ; cdf f x is . Values , are read with ContinuousWithinAt f (Icc 0 1) at the endpoint, a disclosed reading of "density with value ".if D ≤ κ then 1 else κ / D, so that zero demand gives .S integrates each agent's expected contribution against ; it is not defined by the paper's simplified formula, which is a milestone.A complete development needs Lebesgue and interval integrals with variable limits, the fundamental theorem of calculus at an endpoint of continuity, and one-sided derivatives of parametric integrals. The Bayesian value-of-a-test layer (Lemma 1, display (6)) is reusable for other models of testing and information products. Proofs of any milestone are welcome independently.
Data have become an input to innovation: firms use consumer data, together with research labor, to develop new products. Data differ from labor and capital in two ways. They are a by-product of consumption, so their supply is endogenous, and selling them costs consumers privacy. Cong, Xie and Zhang (arXiv:2109.10028, published in Management Science) put both features into a continuous-time semi-endogenous growth model in the tradition of Romer (1990) and Jones (1995). They then ask whether a decentralized market economy with data trading grows at the rate a social planner would choose.
The paper's headline has two halves. The first, which this mission formalizes, is analytical: on the balanced growth path the decentralized economy and the social planner grow at the same rates (Proposition 3). The second, that the market economy underemploys R&D labor and overuses data, is shown only numerically (§3.3, Figure 1) and is not part of the mission.
Time is continuous. The population is with . Parameters: discount rate ; inverse elasticity of intertemporal substitution , ; privacy-disutility curvature ; labor elasticity ; marginal cost of intermediate goods; innovation efficiency ; data share ; knowledge spillover .
Varieties of intermediate goods accumulate through the innovation possibility frontier
where is the data each consumer sells and , are the labor shares of R&D and final-good production.
The decentralized economy (§2). Per-capita consumption obeys the Euler equation . The data price obeys . Data are bounded by consumption: . Monopolistic intermediate producers earn the profit and pay the wage . A patent is worth the present value
Free entry equates the marginal value of data and of labor in R&D with their prices: and .
The social planner (§3.2) maximizes the consumer's utility subject to the frontier, the resource constraint with , and . The paper solves this problem through the necessary conditions of the current-value Hamiltonian, with shadow prices and ((A.7)–(A.10)).
A balanced growth path (BGP) is a path on which every variable grows at a constant rate of its own, and the interest rate is a constant . With , write
With , for a balanced growth path of the decentralized economy and one of the planner's system with the same parameters,
and the planner's per-capita output grows at . The goal states equality of rates, not their closed form.
The result. The equilibrium is inefficient: monopoly pricing and the knowledge spillover drive a wedge between private and social returns to R&D. Proposition 3 says that this wedge acts on levels (the R&D labor share and data intensity), not on long-run growth rates. Those rates are pinned by population growth, preferences and the frontier's returns to scale, and are free of scale effects. This puts the paper in the semi-endogenous growth family and isolates where data policy can matter. Privacy regulation and data ownership change allocations, not the long-run growth rate.
Formalizing it. The proofs in the paper are short and use growth-form identities freely. The mission makes the model precise: what a balanced growth path is, which equations hold in levels, and where integrability and positivity enter. The definition layer (constant-growth paths, present values of profit streams, Hamiltonian necessary-condition systems for growth models) does not exist on the platform and is reusable for other continuous-time growth models. None of these results has been machine-checked before.
The individual steps are short, but each has a gap the paper leaves open:
The tempting shortcut is to work with the growth rates directly. That skips the content: the rates of a balanced growth path are not given numbers, they are derived from the level equations.
Real.rpow and of the Bochner integral are excluded. Both BGP notions were checked to be inhabited at the paper's Table 2 calibration.A financial position can have many possible outcomes, and a risk measure assigns a number to the cash needed to make that position acceptable. A risk manager who uses expected disutility must choose a loss function to describe how strongly different losses matter. That choice is often uncertain: several functions can fit the available preference comparisons. Delage, Guo and Xu study how to measure risk when the loss function belongs to a set rather than being known exactly. Their model keeps one common probability law and makes the preference uncertainty explicit. This matters when an optimization problem uses risk as its objective or as a constraint, because the chosen loss function can change the resulting decision. The paper develops this model and later studies preference information, discrete optimization reformulations, and sample approximation (Delage, Guo and Xu, §§1, 3–5).
Fix a probability space . A position is a real random variable with finite th moment, where . Positive represents a gain, so the loss after adding cash is . A loss function transforms that loss before expectation. The paper's class consists of convex, nondecreasing functions that are strictly increasing on for some (Definition 2.1). This excludes a loss function that remains flat around zero and fixes the normalized benchmark .
The individual shortfall risk is the least cash amount for which expected loss is no greater than the benchmark:
If is a set of plausible loss functions, the preference robust shortfall risk requires the same cash amount to satisfy every member of :
The normalization belongs to each function separately. The paper also defines the worst risk of a set of risk measures as ; these are (1.2)–(1.4) of the dated preprint (Delage, Guo and Xu, pp. 2–3 of the April 25, 2018 preprint).
The goal is all three claims of Theorem 2.1. First, for every and every admissible ,
Second, with , the same value is . Third, if is a set of normalized convex utility-based shortfall risk measures and , then
The supporting targets follow the statements used on pp. 5–7: divergence of each at (Lemma 2.1(ii)); the extended Jensen inequality and its supremum form (2.11); divergence of the robust gap as cash tends to (2.12); the inequality (2.13); feasibility of the finite worst individual risk; and the infinite-value case. These targets retain the source's separate finite and infinite regimes (Delage, Guo and Xu, Theorem 2.1 and proof).
The identity gives two ways to use preference uncertainty. A decision problem may impose one common expected-loss constraint across all plausible preferences, or it may evaluate the worst individual shortfall risk. Theorem 2.1 says these produce the same risk for the admissible position. The paper uses this connection before characterizing loss-function sets from preference information and deriving optimization formulations. It also clarifies that robust shortfall risk need not itself equal the shortfall risk of one fixed loss function: the worst function can depend on the position (Proposition 2.2, Delage, Guo and Xu).
The theorem is proved in the cited paper. The remaining work here is a machine-checked proof of the exact extended-value statement and its supporting steps. The proposal contains compiled Lean statements with proof placeholders; no new machine-checked proof of Theorem 2.1 is claimed. A completed development would also provide reusable definitions for loss classes, extended shortfall risks, and worst-risk operators.
The tempting interchange of an infimum over cash with a supremum over loss functions is not valid for arbitrary constraint families. Here each loss function belongs to , and the proof must account for the behavior of its expected loss as cash varies. The expected loss can be infinite even when has a finite th moment, and the common feasible set can be empty. At the other boundary, an empty loss set makes every cash amount feasible. The proof therefore has to establish the finite case and handle the two extended endpoints without silently replacing them by ordinary real values. The page's finite-case argument also uses feasibility at an individual infimum; this requires a continuity fact that is implicit in its displayed calculation.
The Lean model represents by a real function with MemLp Z p P, , on a probability measure. It represents by convexity, monotonicity, and strict increase from a negative threshold. It imports the published DupacovaWets.Consistency.expect for extended expectation, which returns when the positive part has infinite integral. Risk values live in EReal. An infimum over cash is taken after embedding its feasible real cash amounts into EReal; this preserves for an empty feasible set and for one unbounded below. The supremum over an empty is , as in the extended-real convention.
The definition of uses the paper's single supremum constraint, with subtracted inside that supremum. It is not defined through the theorem's proposed right-hand side. Individual risk maps are total on real functions, while the goal evaluates them only for positions in . The converse describes the members of as maps for some , using the characterization in Proposition 2.1 without formalizing that proposition. The divergence target (2.12) requires nonempty; the source's displayed limit fails for an empty set, although the main theorem includes that case. Supporting statements use Integrable Z P, a consequence of the source's condition on a probability space. Contributions proving the extended Jensen step, endpoint behavior, and the representation are within scope; the paper's later numerical and sample-approximation results are separate work.
An assortment decision determines which products a customer can buy, but its expected revenue depends on the probability that the customer chooses each offered product. A distribution over complete rankings gives a direct model: sample a customer's ranking, then take the highest-ranked product in the assortment. The resulting choice probabilities are easy to define and expensive to evaluate by direct enumeration, because a universe of products has rankings. Désir, Goyal, Jagabathula and Segev study this issue for distributions built from Mallows models and use the resulting probabilities in assortment optimization and a case study (manuscript, §§2–5). This mission isolates their exact dynamic program for a single Mallows model, Theorem 1 of the manuscript.
Let the product universe be , with . A ranking assigns each product a distinct position from to ; a smaller position means higher preference. The modal ranking is , meaning that has position . This choice follows the manuscript's relabelling of the products in §4.1. It fixes a reference order without restricting which ranking a customer may draw.
The Kendall–Tau distance counts pairs of products whose order in disagrees with their order in . For a concentration parameter , the Mallows distribution assigns probability
The normalizer sums over all rankings. At they are equally likely; larger gives less weight to rankings with more pairwise disagreements. Every summand in is positive, so the distribution is well-defined (manuscript, §2.1, p. 7).
An offer set is a subset of the products. For an offered product , its choice probability is the Mallows weight of rankings that place before every other member of :
This is equation (1) of the manuscript for one Mallows component (§2.2, p. 8). The formula is an exact definition, but its sum ranges over every ranking.
Algorithm 1 is the repeated insertion method. It starts with and inserts each next product at a position with probability
Write . After step , let denote the probability that is first among the offered products inserted so far and occupies position . The manuscript's Algorithm 2 computes a separate table, , by its initial condition and recursions (3)–(4), without enumerating rankings (§4.1, pp. 16–18).
For , the mission's goal is Theorem 1: Algorithm 2 returns the Mallows choice probability of each offered product.
The table also returns zero for every product outside . The milestone list follows the source's intermediate claims: the repeated insertion law is Mallows; choice probability decomposes by final position; and the probabilities obey the two cases of the insertion transition (Lemma 1 and §4.1, pp. 17–18).
The result replaces an -term probability sum with the manuscript's dynamic program for all offered products at once. Those probabilities are inputs to its later assortment optimization model and permit computations on product universes where direct ranking enumeration is impractical (manuscript, pp. 16, 18–21). This mission targets the exact identity, not a numerical approximation or the later mixed-integer formulation.
The result is already proved in the cited manuscript; the goal here is a machine-checked Lean proof. A completed development would provide reusable finite-ranking definitions, a formal repeated insertion law, and verified transitions between a probabilistic model and an explicit recurrence. The definitions and theorem statements in this proposal compile locally; the theorem proofs remain open.
At a single insertion, the chosen offered product can keep its position, move down one position, or be displaced by the new product. Which outcome matters depends on whether the newly inserted product is offered and on where the previous best offered product stood. A naive table recording only each product's total choice probability loses the position information needed for the next insertion. Algorithm 2 retains that information in , so a proof must connect its state and boundary values to the distribution over complete rankings (manuscript, §4.1, pp. 17–18).
Products and ranks are represented by Fin n and rankings by permutations of Fin n, interpreted as product-to-rank maps. Lean's indices begin at zero; the paper's , insertion position , and table indices begin at one. The modal ranking is identity after the paper's relabelling. Offer sets are finite subsets of Fin n, and wherever is named. The concentration parameter satisfies . The Mallows normalizer is the finite sum displayed above, rather than the manuscript's printed product formula.
Algorithm 2 says “without loss of generality” that . The printed recurrence actually needs that condition, so the goal and the new-product transition state it explicitly. Equation (1), read literally for , can be positive because its indicator does not test membership. The main equality is therefore about ; the table's zero output for unoffered products is stated separately. Outside the paper's index ranges, , the probabilistic , and the dynamic-program table have explicit zero values. In particular, and settle the boundary in recursion (3).
The left side of the goal is the weighted sum over every ranking; the right side is the table computed from recursions (3)–(4) and never examines a ranking. A proof needs finite permutation reasoning, normalization of the insertion probabilities, and a link between the insertion law and the table's meaning. Lemmas about these pieces, as well as proofs of the listed milestones, are welcome contributions.
Industrial buyers rarely negotiate with suppliers from scratch. A common practice is to issue a request for proposal/quotation (RFx): suppliers first submit quotations, and the buyer then negotiates contracts with them one after another, possibly using the quotations as fallback options. Chu, Rong and Zheng (SSRN 3200030; Operations Research, doi:10.1287/opre.2019.1964) ask whether this extra stage helps the buyer when the actual terms are settled by bilateral bargaining anyway. Their answer is that it does: the buyer's equilibrium profit with an iterative tendering stage is at least her profit at the most favorable outcome of bargaining without one. The paper builds on the literature of bilateral bargaining in supply chains with competing suppliers, where the buyer's outside options are endogenous and the order of negotiations matters.
A monopoly buyer (player 0) procures from two suppliers (players 1 and 2) of substitutable products. Write and . The model is described by the following scalars:
The paper's Assumptions 1–2 (a unique interior maximizer of the chain profit, and submodularity) imply and . Each bilateral negotiation is an asymmetric Nash bargaining problem: maximize , where and are the supplier's and the buyer's profits and , their reservation utilities.
Without an RFx (simultaneous bargaining). Supplier 's dual-sourcing profit maximizes subject to and . Here is the buyer's profit when she sources from alone, and is 's profit as exclusive supplier. The most favorable bargaining outcome is the unique solution of
With an RFx. Suppliers quote offers , the profits they demand. The buyer then negotiates with a leader , accepting or rejecting his offer, and afterwards with the follower . Accepting an offer turns it into a reservation utility, so the leader's program [RFx-i] maximizes
over and the buyer's single-sourcing profit . The reservation utilities , are given explicitly on p. 18 for each accept/reject choice. The buyer accepts both offers when no choice of leader, accept/reject decision or negotiated solution gives her more than .
For every pair of nonnegative offers at which the buyer accepts both offers,
and the right-hand side also dominates the buyer's profit at every dual-sourcing equilibrium of simultaneous bargaining.
Theorem 5 is a robustness statement for an everyday procurement practice. Without an RFx, simultaneous bargaining has many equilibria, and is the best of them for the buyer. The theorem says the tendering stage secures at least this best case, whatever the bargaining powers and the substitutability of the suppliers. In the paper's Appendix A instance (, , , ) the gain is strict: the most favorable outcome gives the buyer , the RFx equilibrium . Lemmas 2, 4 and 5 describe how a buyer responds to quotations in a Nash bargaining framework, and that description is reusable for other sequential-negotiation models.
The paper's results are proved in its e-companion. As far as is known, none of them has a machine-checked proof. Formalizing them checks a case analysis over Nash bargaining programs with piecewise-linear reservation utilities and zero-surplus corner cases, which is where informal arguments are easiest to get wrong.
The obvious argument works offer by offer: compute the follower's split, plug it into the leader's program and compare closed forms. It breaks down in two places. First, the buyer's profit in [RFx-i] contains , so the leader's objective is neither concave nor smooth, and its maximizers move between regimes with the offers. Second, accepting an offer can leave zero bargaining surplus. Then every feasible point maximizes the Nash product, and the accept-both characterization has to hold for all of them, not for a convenient one. Comparing with needs a separate argument as well: is defined by a fixed-point system with positive parts, and [Q] has to be shown to have it as its unique optimum.
Fin 2 and offers are nonnegative reals.Real.geom_mean_le_arith_mean2_weighted) for the Nash split, and a case analysis over piecewise-linear constraints. Contributions are welcome in both. A general lemma on asymmetric Nash splits, on , would be reusable beyond this mission.Firms that sell large catalogues of digital goods (streaming titles, cable channels, software features) rarely price every subset of products separately: with products there are bundles. A common simplification is bundle-size pricing (BSP), where the price depends only on how many items the customer takes and the customer picks which items go into the bundle. BSP sits between pure bundling (one price for everything) and full mixed bundling, and its menu has only prices.
Bakos and Brynjolfsson (Management Science, 1999) showed that for many products a pure bundle extracts almost all surplus under suitable concentration. Armstrong (Review of Economic Studies, 1999) showed that a cost-based two-part tariff asymptotically achieves the perfect-price-discrimination profit. Chu, Leslie and Sorensen (American Economic Review, 2011) computed optimal BSP menus numerically for up to five goods. Abdallah, Asadpour and Reed (Operations Research, 2021) develop an asymptotic theory of BSP as . This mission formalizes their homogeneous-cost result: with identical marginal costs, optimal BSP asymptotically earns the perfect-price-discrimination profit.
A firm sells products to one customer with valuations , additive over bundles. Let be the order statistics. A bundle of size is worth to the customer, the sum of her largest valuations, with . The firm incurs a marginal cost for item , so a bundle of size costs , where lists the items by valuation and ties go to the lowest index.
A BSP menu is with , where means size is not offered. The customer buys a size , with the free no-purchase option. The firm's profit is , and the BSP problem is . The benchmark is perfect price discrimination, , the most any selling mechanism can earn.
The large-offering regime describes the valuations as one random sequence :
The normalized curves are and for . The quantile function is .
With identical costs , for every ,
The size fraction maximizes over , and when is a continuity point of . If ,
Theorem 1 is the general principle behind the goal. Suppose and pointwise, with nondecreasing continuous limits, and . Offer the single size at price , where grows faster than but is . Then
The milestones follow the appendix proofs in order:
Theorem 2 says that, with identical marginal costs and enough statistical concentration across products, a menu of size prices earns, to first order, everything a seller who knew each valuation could earn. Theorem 1 says more: one well-chosen bundle size, sold at a price slightly below its fluid value, is asymptotically as good as the optimal BSP menu. The paper's later results on heterogeneous costs (Theorems 3–4), clustered BSP and unknown budgets reuse this framework: Theorem 1 reduces each of them to computing the limit curves and .
The results are proved in the paper and have no machine-checked version. This mission formalizes them under a weak-convergence hypothesis on the empirical distribution, with no independence assumption. The formal statements also fix points the page leaves implicit: the tie-breaking rules, the value of the BSP problem as a supremum, and the case , where the goal's ratio degenerates.
The obvious route to Theorem 2 goes through Theorem 1, as the paper does. That needs a dominating the fluctuation of , and Assumptions 1–2 give no second moments. A proof of the goal must therefore avoid Theorem 1's condition or replace it with a weaker device.
The convergence is a statement about sums of top order statistics of a dependent sequence. Pointwise convergence of the empirical cdf does not by itself control the upper tail, which carries the mass of . The weak law and uniform integrability have to supply that control.
The upper bound (A1) requires exchanging a supremum over with a limit in probability, which uses monotonicity of in and continuity of the limits. The step " for " holds only at grid points , so the off-grid error must be bounded separately.
Everything lives in the namespace LargeBSP.Homog. Items are 0-indexed: coordinate n < N is the paper's item . The valuations are one sequence X : ℕ → Ω → ℝ on a probability space, measurable and nonnegative; the -product model uses its first terms. is cdf ν for a probability measure ν on with and finite mean. "" toward a constant is convergence in probability (TendstoInMeasure); deterministic sequences use Tendsto.
Menus are ℕ → WithTop ℝ, with ⊤ meaning "not offered". Within a bundle size, items are ranked by valuation with ties to the lowest index, as on the page. Among sizes, the customer picks the smallest maximizer of surplus, a disclosed tie-break, so an indifferent customer does not buy. is the real supremum of the expected profit over all menus with prices in . It is bounded by , so it is never the junk value of an unbounded supremum.
The quantile is . Its set is empty only outside , where Lean returns ; every use is at or inside an integral. The set defining is taken over .
Disclosed readings:
The tail condition (6) of the paper is not assumed: neither proof uses it.
The goal cannot be satisfied trivially. is the value of the BSP problem over all menus, not a chosen menu. PPD is the sum of the per-item expectations. The instance , satisfies every hypothesis with , and . So the ratio is neither nor fixed by a degenerate menu.
Needed infrastructure: order statistics of a finite family through a rank function, empirical distribution and quantile functions, the identity "mean = integral of the quantile function", convergence of quantiles under weak convergence (van der Vaart, Lemma 21.2), and uniform integrability of averages. These parts are reusable well beyond pricing. Contributions are welcome on any milestone, and on proofs of the goal that bypass Theorem 1's second-moment condition.
Philosophers of physics use category theory to decide when a formulation of a theory carries excess structure. Weatherall (2016) represents each formulation of electromagnetism as a category of models and the passage from potentials to field strengths as the functor . A functor that is not full forgets structure, one that is not essentially surjective forgets properties, and one that is not faithful forgets stuff. Weatherall's §4 argues on Minkowski space that the potential formulation with gauge transformations as arrows is related to the field-strength formulation by a functor that is full and essentially surjective. His footnote 9 sets topology aside, and the erratum to his Proposition 2 (arXiv v2, p. 15) records that the gauge-theoretic functor is not faithful, because constant gauge transformations act trivially on fields.
On a contractible spacetime these facts all rest on one theorem: the Poincaré lemma, which says closed differential forms are exact. A companion mission (Weatherall 2016: Potentials vs. Field Strengths on a Finite 2-Complex) proves the discrete version, in which fullness, faithfulness and essential surjectivity are equivalent to the vanishing of , and of a cell complex. This mission is the continuum version on a vector space, built on Mathlib's exterior derivative.
Timeline. The explicit radial homotopy operator proof of the Poincaré lemma is standard in textbooks; it is the proof of Theorem 4-11 in Spivak's Calculus on Manifolds (1965). Antiexact forms and the same operator are studied in Kycia (2020). Mathlib has the exterior derivative extDeriv with . In 2025 Kudryashov proved the degree-1 case for convex sets, stated for 1-forms written as E → E →L F with a symmetric derivative. Mathlib has no Poincaré lemma in higher degree, no de Rham cohomology and no Hodge star.
Let be a real normed space, for example , and a real Banach space of field values. A differential -form is a map that assigns to each point a continuous alternating -linear map. Smooth means (ContDiff ℝ ∞). The exterior derivative is Mathlib's extDeriv:
A function is a 0-form, and is its derivative viewed as a 1-form (grad). The radial homotopy operator sends a -form to the -form
Field equations enter through an arbitrary predicate on 2-forms. For example once a metric is chosen, and in vacuum. The categories are:
Fld P (Weatherall's EM1): smooth closed 2-forms with , with only identity arrows.Pot P (EM2 with gauge arrows, fn. 15): smooth 1-forms with . An arrow is a smooth with , and arrows compose by adding gauge functions.fieldStrength P : Pot P ⥤ Fld P: the functor , which sends every gauge arrow to an identity.The cohomology conditions are elementary Props:
For every that admits at least one potential:
So the potential description with gauge arrows forgets only stuff, namely the constant gauge transformations, and nothing else on a vector space.
Four supporting statements isolate the reusable ingredients of Milestone 2:
alternatizeUncurryFin.The result. The goal makes precise, on and with any field equation, the claim behind Weatherall's §4: up to the constants , potentials modulo gauge carry no more information than field strengths. With the discrete mission, it shows that the three ways of forgetting information correspond to , and in both settings. The continuum version is metric-free. Maxwell's equations, sources or any other field equation enter only through , so the classification holds for all of them at once.
Formalizing it. The homotopy formula and the Poincaré lemma for Mathlib's extDeriv in arbitrary degree are not in Mathlib. They are prerequisites for de Rham cohomology of manifolds, for the homotopy invariance of de Rham cohomology, and for any formal treatment of gauge potentials, Chern–Simons terms or Hamiltonian mechanics that uses local primitives. The classical proof is a textbook argument; the remaining work is to formalize it against Mathlib's alternating-map API. Machine-checked versions exist elsewhere only in other representations: Mathlib proves degree 1 for 1-forms written as E → E →L F on convex sets, and this platform's Rudin chapter 10 mission has proved Poincaré's lemma (Rudin, Theorem 10.39) as Rudin.ch10_poincare_lemma and Rudin.ch10_primitive_of_closed, for its own coefficient-style KForm on convex open subsets of . A bridge from those statements to Mathlib's extDeriv would be a welcome contribution.
The obstacle is the homotopy formula in general degree. Each side involves the alternatization alternatizeUncurryFin of a derivative, the insertion curryLeft of the position vector as the first argument, and Fin.removeNth reindexing. Matching the two sides requires the signs from moving an argument to the front to cancel exactly against those of . The degree-1 shortcut through Mathlib's existing curve-integral Poincaré lemma does not generalize, because it uses a different representation of 1-forms and has no analogue in degree 2, which the essential-surjectivity clause needs. A second, routine obstacle is smoothness of : need not be finite-dimensional, so differentiating under the integral needs bounds that are uniform in near each point.
E → E [⋀^Fin k]→L[ℝ] F and the exterior derivative is extDeriv. "Smooth" is ContDiff ℝ ∞, where ∞ means , not analytic. is any real normed space, not necessarily finite-dimensional or complete, and is a real Banach space (CompleteSpace F), so the integral defining is the Bochner integral.Fld P is a Mathlib Discrete category. Pot P has a hand-written Category instance whose arrows are the structure GaugeHom. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.[Nonempty (Pot P)], meaning the field equation has a solution. Without it Pot P is empty and faithfulness and fullness hold vacuously. The cohomology conditions are explicit statements about extDeriv and grad, not definitions that make a target hold by construction. The goal fixes nothing about .extDeriv, in the form used here, and the gauge invariance . The homotopy operator, the homotopy formula and the Poincaré lemma are stated for arbitrary degree and are intended for reuse in de Rham and gauge-theory missions. Contributions toward a Mathlib-quality homotopy-operator API are welcome.MeasureTheory/Integral/CurveIntegral/Poincare.lean (Poincaré lemma for 1-forms on convex sets), mathlib4 PR #24019.A computable measure of entanglement establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be positive integers, and fix an orthonormal product basis of . For a matrix on this space, let denote its partial transpose on the first subsystem, so that . Write and . Let be any finite family of Hermitian matrices on this space, and let be nonnegative real numbers with . Then
This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives outside the state domain.
Let be positive integers, and fix an orthonormal product basis of . For a matrix on this space, let denote its partial transpose on the first subsystem, so that . Write and . Let be any finite family of Hermitian matrices on this space, and let be nonnegative real numbers with . Then
This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives outside the state domain.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let be a Hermitian matrix on a positive finite-dimensional space. There exist density matrices and such that
Their coefficient sum is no larger than that of any other such decomposition. Eigenvalues are counted with multiplicity. This is an attained variational characterization, valid also for .
Let and be bipartite density matrices. Regroup their product as , and define . Then
All four local spaces are finite and nonempty. This additivity concerns logarithmic negativity.
There exist two density matrices and on two qubits for which
Thus logarithmic negativity is not convex. This states only the nonconvexity clause; the source's subsequent inference about LOCC increase is deferred separately.
Fix a finite adaptive LOCC protocol before a bipartite density matrix is supplied. Local instruments may change finite dimensions, add ancillas, discard systems, and choose later operations from prior outcomes. After any fixed classical coarse-graining, let be its subnormalized outputs, , and for . Then
Zero-probability outcomes contribute zero. This is the selective entanglement-monotone inequality.
Let be a compact convex set of Hermitian trace-one matrices whose real span is the full Hermitian space. Define and as the infima of and over , where and . These sets are nonempty and bounded below. The first functional is a norm on Hermitian matrices; is convex and nonnegative. Moreover,
Members of need not be positive. The statement includes definiteness, the triangle inequality, and absolute homogeneity of the norm.
For a density matrix on positive finite local spaces, let and use the variational base construction with separable states and PPT states, respectively. Then
Furthermore, exactly when is separable; and each hold exactly when . These zero sets distinguish the measures. The phrase “in general” is not a universal strictness condition.
Fix a finite adaptive LOCC protocol with arbitrary positive finite input and output dimensions, including a fixed final classical recording map. For input density matrix , write and for its probabilities and normalized positive-probability conditional outputs. Then both
The two robustness measures are defined by their actual separable and PPT bases. This retains selective, rather than only deterministic, monotonicity.
For any finite deterministic LOCC protocol and any bipartite density matrix ,
Here sums all subnormalized leaves after forgetting the transcript; input and output local dimensions may differ. This is the deterministic monotonicity asserted in the introduction and supported by §II.
Let and let be a state on . Let be its standard maximally entangled state, and let be the infimum of over deterministic LOCC protocols . Then
The trace norm is unhalved. No optimal protocol is assumed to exist.
Let and let be an bipartite density matrix. For a deterministic LOCC teleportation protocol , let map Alice's unknown input state to Bob's output. Define by taking the infimum over of the Haar average of . Then
The protocol is fixed before the unknown input. This optimized equality is the numbered result adapted from reference [27].
Let be a finite bipartite density matrix and . Define achievable nonnegative rates using the source's universal condition on diverging integer sequences: counts input copies, output Bell pairs, and requires . The supremum is taken in the extended nonnegative reals. Then
The case is included. The input/output letter interchange near Eq. (41) is resolved by Eq. (43) and the proof.
Let be a Schmidt expansion, where the two vector families are orthonormal, , and . For ,
Coefficients are amplitudes, not squared eigenvalues; zero padding and rectangular local spaces are allowed. The robustness identification retains the source's attribution to [18].
For normalized Schmidt data , with , write and . Its entropy in bits satisfies
Zero coefficients contribute zero. Equality holds if and only if every pair of nonzero coefficients is equal. This includes rank-one product states and maximal entanglement on a proper Schmidt support.
Let , let swap the two -dimensional factors, and let be the maximally entangled projector. Choose real so that is a density matrix. Set and . Then
This computes the measure on the actual family (51), including .
For a density matrix as in Eq. (51), put and . Then
Both robustness quantities retain their variational definitions. The background coincidence of PPT and separability is specific to this family and is attributed by the source to [22].
Let be a positive definite physical two-mode covariance matrix, so are real symmetric matrices and . Use with , and let reverse Alice's momentum. Then
The polynomial's plus sign is retained; its roots occur as imaginary symplectic pairs.
Correction to the printed source.
Printed: PDF p.9 prints the standard block [[0,1],[1,0]] and describes the roots near Eq.(64) as real pairs.
Corrected: Use J=[[0,1],[-1,0]], explicitly in symplecticTwo and the covariance hypothesis; preserve every coefficient of Eq.(64).
Reason: Eq.(54) explicitly requires an antisymmetric symplectic form; the preceding normal-mode paragraph gives imaginary eigenvalue pairs. At the physical vacuum gamma=I/2 the characteristic polynomial is (X^2+1/4)^2. The symmetric printed block would give (X^2-1/4)^2. This is the minimal sign repair consistent with the source's commutation convention.
For a tripartite density matrix, let , , and . For every finite adaptive LOCC protocol acting on the three separated parties, with normalized positive-probability outputs and probabilities , all three grouped negativities obey
All regroupings are computed from the same state. Local dimensions may change, and a fixed final coarse-graining is allowed. The other three functions in threePartyMeasures are reduced-state negativities defined by the source for a noncooperating discarded party; this theorem makes no monotonicity assertion about them under three-party LOCC.
For a four-party density matrix , form and . Then
and the same two inequalities hold for . These compare the measures and hence their distillation upper bounds. They do not compare actual optimal rates of different distillation tasks.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Practical Quantum Error Mitigation for Near-Future Applications.
Let be an -qubit density matrix and a Hermitian observable. Let be finite Kraus maps, with no trace-preservation requirement, applied in chronological order. Write , , and , in the order on each wire. Then
Traces in these coordinates are real. The empty circuit has identity transfer matrix. These identities connect the physical experiments to real linear algebra.
Consider a fixed finite mitigation design on qubits. Its slots comprise a product preparation, an ordered list of inverse or compensation stages, and an observable measurement; every slot is used exactly once. At slot , let be real coefficients, let , and set . Assume the ideal density matrix, ideal Hermitian observable and each ideal stage map equal the corresponding signed sums of their physical realizations, on every input operator. In an inverse stage the native map precedes the correction; compensation chooses either the native map or a basis branch.
Sample each choice with weight , run the resulting physical circuit, and multiply the readout by the sign of the product of selected coefficients. A rejected postselection returns zero and remains a trial. If is this effective outcome and is the ideal circuit expectation, then
Here are independent complete trials. If a slot has zero coefficient mass, the defined trial is a zero-scoring dummy; the decomposition then has zero target expectation. This states conditional factorization, rather than existence of a complete calibrated design.
Correction to the printed source.
Printed: PDF p.4 prints the preparation and output sampling probabilities as q/C, without absolute values.
Corrected: Use |q|/C for preparations and readouts as well as gate choices; negative coefficients remain encoded in the estimator sign.
Reason: The same paper's §IV p.4 and Appendix I.3 p.19 explicitly prescribe absolute weights. Signed q/C can be negative and is not a probability. Independent moderation is required.
Let take values with probabilities , where . Let , and . For independent trials , with integers , let . Then
If , equality of this variance with the ideal binary-sampling variance holds exactly when
The model has no postselection zeros. The formula distinguishes the exact overhead ratio from the usual approximation; any desired positive standard deviation can be met using the displayed upper bound.
Use the sixteen matrices in Table I, in their printed order, and the superoperators . Let be the corresponding printed word with , and . Words are matrix products, so their rightmost factor acts first. For every ,
The phase convention for is irrelevant at the superoperator level. The three primitive letters are ; postselection denotes the accepted branch, without renormalization. These equalities give physical words for the library. Linear independence is stated in the separate completeness item.
Let be the real Pauli transfer matrices of Table I. Form the matrix whose columns are their column vectorizations. Then is invertible. For every and every real matrix on the -wire Pauli coordinate space, there is exactly one real coefficient array such that
For this is the scalar basis. The span concerns signed maps, including trace-decreasing branches, rather than only channels. It supplies the algebraic completeness needed for cancellation.
Let and as in Table I. Write . Then, on every qubit operator,
Here implements up to global phase. This is an expectation-estimation decomposition, not deterministic synthesis with the corresponding time cost.
Let be the Table I matrices, let , and put the control in the first tensor factor. Then
The twelve coefficients have absolute sum . The identity holds on every operator; projective branches are unnormalized. It exhibits how local signed operations represent an entangling gate.
Let and let be real matrices. Define , with eigenvalues counted with multiplicity. All norms below are Euclidean vector norms or their induced operator norms. If , then
The strict inequality makes the denominator positive and the lower bound strictly positive for nonzero . This is the symbolic robustness argument used for operation and SPAM completeness.
For wire , let () be real basis matrices and let be the square matrix with columns . Assume each invertible. For a real -wire map , vectorize by interleaving each wire's column and row indices, using the column-first convention of Eq. (2), correcting the reversed local pairs in (D3), and define
The tensor synthesis matrix is invertible and
every coefficient array representing equals this computed . Empty tensors have scalar value one. This pins the construction rather than quantifying over unrelated coefficients.
Correction to the printed source.
Printed: Eq. (2), PDF p.5, stacks each basis matrix by columns. D3, PDF p.13, instead starts with E_{I...I,I...I}, E_{I...I,I...X}, varying the column index before the row index.
Corrected: Use column-then-row local index pairs, evaluating E(row,column), in both the tensor synthesis matrix and the interleaved target vector. This swaps the local row/column order printed in D3; all tensor factors and basis-operation labels retain their order.
Reason: D1 and the inverse-coordinate construction use the synthesis matrices defined by Eq. (2). Their target vector must use the same ordering. Correcting only D3 makes those formulas consistent; it changes neither the represented operation nor any coefficient-mass bound. Independent moderation must verify this source correction.
Use reference preparations and reference observables . Let have entries , and let have entries , in Pauli order. For physical density preparations and Hermitian observables , form with the same formulas. The reference frames are invertible. With denoting largest absolute entry,
Whenever is invertible, every column has unique coordinates . Whenever is invertible, every row has unique coordinates . Multiplication by the respective frame reconstructs the target exactly. These statements include all complete frames, not only nearby ones.
Let be ideal and native real Pauli transfer matrices on wires. On each wire let be a complete real operation basis with invertible synthesis matrix . Fix any real . Define by applying the inverse tensor synthesis matrix to the interleaved coordinates of . Then
and this coefficient array is unique for the chosen . No inverse of is required. This is the algebraic compensation witness; physical sampling is conditional on the branch realizations.
Correction to the printed source.
Printed: Eq. (2), PDF p.5, stacks each basis matrix by columns. D3, PDF p.13, instead starts with E_{I...I,I...I}, E_{I...I,I...X}, varying the column index before the row index.
Corrected: Use column-then-row local index pairs, evaluating E(row,column), in both the tensor synthesis matrix and the interleaved target vector. This swaps the local row/column order printed in D3; all tensor factors and basis-operation labels retain their order.
Reason: D1 and the inverse-coordinate construction use the synthesis matrices defined by Eq. (2). Their target vector must use the same ordering. Correcting only D3 makes those formulas consistent; it changes neither the represented operation nor any coefficient-mass bound. Independent moderation must verify this source correction.
Let be invertible ideal and native real operation matrices. Let the local bases have invertible synthesis matrices, and define . Then and . The computed tensor coordinates of are the unique representation of , and
Thus the physical order is the native operation followed by its sampled correction. Both inverses have explicit hypotheses; the inverse noise need not itself be a channel.
Correction to the printed source.
Printed: Eq. (2), PDF p.5, stacks each basis matrix by columns. D3, PDF p.13, instead starts with E_{I...I,I...I}, E_{I...I,I...X}, varying the column index before the row index.
Corrected: Use column-then-row local index pairs, evaluating E(row,column), in both the tensor synthesis matrix and the interleaved target vector. This swaps the local row/column order printed in D3; all tensor factors and basis-operation labels retain their order.
Reason: D1 and the inverse-coordinate construction use the synthesis matrices defined by Eq. (2). Their target vector must use the same ordering. Correcting only D3 makes those formulas consistent; it changes neither the represented operation nor any coefficient-mass bound. Independent moderation must verify this source correction.
Let be ideal and native real operation matrices, let , and let the local operation bases be complete. For fixed real , set and compute the tensor coordinates of . Then
with a unique coefficient array for this . The statement asserts a signed linear decomposition. It does not assert nonnegative coefficients or complete positivity of ; the favorable Pauli boosting example is a separate model-specific observation.
Correction to the printed source.
Printed: Eq. (2), PDF p.5, stacks each basis matrix by columns. D3, PDF p.13, instead starts with E_{I...I,I...I}, E_{I...I,I...X}, varying the column index before the row index.
Corrected: Use column-then-row local index pairs, evaluating E(row,column), in both the tensor synthesis matrix and the interleaved target vector. This swaps the local row/column order printed in D3; all tensor factors and basis-operation labels retain their order.
Reason: D1 and the inverse-coordinate construction use the synthesis matrices defined by Eq. (2). Their target vector must use the same ordering. Correcting only D3 makes those formulas consistent; it changes neither the represented operation nor any coefficient-mass bound. Independent moderation must verify this source correction.
Fix an -qubit physical tomographic frame of density preparations and observable measurements, with invertible input and output matrices . Let be an invertible real gauge, fixed for all operations, and let be finite Kraus maps in chronological order. Form the exact measured matrices and . Then is invertible and
For every input and readout label , including an empty operation sequence,
This establishes prediction invariance using computed exact calibration data; estimated coordinates need not be physical states.
Let be invertible real local tomography frames on wires. Use the reference matrices computed from the Appendix D preparations and observables. Let and . For the choice , the estimated input frame is exactly , so its error is zero. The estimated output frames are and satisfy
The empty-wire maxima are zero. This keeps the valid symbolic bound separate from the printed numerical norm evaluations.
Let be local real input-frame matrices, the computed reference input matrix, , , and . Let be real operation matrices and put , and . Assume . Then is invertible and
For the computed GST estimate ,
The empty tensor case has and identity gauge. This states the source proof's small-error domain, not a bound with a nonpositive denominator.
Correction to the printed source.
Printed: F14 and its use in F7 display an inverse norm bound without an explicit small-error inequality at that point.
Corrected: Require e_n<s_min(Min0)^n before applying the displayed reciprocal bound; keep all symbolic norms and the printed F7 formula.
Reason: The proof invokes F10 and C3, whose strict smallness condition makes the denominator positive. Invertibility alone is insufficient; this proof-domain clarification requires independent moderation.
Let be real local library maps, let be their synthesis matrices, and let be the synthesis matrix computed from Table I. Put and . Let be target and native -wire real operation matrices, with . If , compute by inverse tensor synthesis of . Then
The denominator is positive. This is a bound on the constructed witness, without an assumed inverse-norm conclusion or any claim of optimality.
Correction to the printed source.
Printed: Eq. (2), PDF p.5, stacks each basis matrix by columns. D3, PDF p.13, instead starts with E_{I...I,I...I}, E_{I...I,I...X}, varying the column index before the row index.
Corrected: Use column-then-row local index pairs, evaluating E(row,column), in both the tensor synthesis matrix and the interleaved target vector. This swaps the local row/column order printed in D3; all tensor factors and basis-operation labels retain their order.
Reason: D1 and the inverse-coordinate construction use the synthesis matrices defined by Eq. (2). Their target vector must use the same ordering. Correcting only D3 makes those formulas consistent; it changes neither the represented operation nor any coefficient-mass bound. Independent moderation must verify this source correction.
Assume the exact model with and decay rate . Let and . Its two positive model values recover the zero-error value exactly:
The positivity assumptions specify real powers. This is conditional on exponential decay to zero and exact model points; it makes no unbiasedness assertion about ratios of noisy empirical measurements and no universal decay claim for Markovian errors.
Let be an ideal -qubit unitary and let be any channel in finite normalized Kraus form. Set and , where . Then
This constructs the before/after noise model explicitly. The required inverse is the ideal unitary channel; invertibility of the noisy channel is unnecessary.
Let sum to one and let . Set and . Then
The component is independent of because the ratios are fixed. The identities hold on all input operators and avoid division by zero.
Let , and . For , define and
For every qubit operator ,
Moreover as and on the punctured positive neighborhood of zero, with uniform constants on that neighborhood. This describes slow variation of a trace-decreasing model's component, not exact exponential decay of all expectations.
Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.
Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.
A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.
An input consists of two bit strings of the same positive length , separated by . The strings are read most significant bit first, with leading zeros permitted. If denotes the represented natural number, the required output is exactly the -bit binary representation of , padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define .
The full target is
This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants and such that every pair of -bit inputs, for and , halts within
steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger gives a stronger asymptotic saving because .
Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.
A proof for any positive value would give a strict asymptotic improvement over . Such an improvement would contradict the proposed lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.
Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.
A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.
The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.
The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.
A full Lean proof of this bound is already on the platform: NLogN.KFTop.kappa_bound (theorem f904f4ef), which also proved IntMul.Kappa.openai_theorem_1. It formalizes the OpenAI manuscript's construction (Prop 7/8 networks, τ = 1−2^-50, crude assembly) on top of a verified multitape-machine compiler and the Harvey–van der Hoeven O(n log n) machine. It uses only the standard axioms.
Quantum mechanics prescribes two incompatible evolutions: the unitary Schrödinger evolution of an isolated system, and the discontinuous state reduction that a measurement appears to trigger. The measurement problem is to explain when and why reduction takes over. Penrose's answer, set out in the 1996 paper this mission formalizes, is that gravity drives the transition: a superposition of two distinct mass distributions carries two distinct space-time geometries; the time-translation needed to call such a superposition stationary is inherently ill-defined; and the resulting energy fuzziness destabilizes the superposition, with a characteristic lifetime of order , where is the gravitational self-energy of the difference between the two mass distributions (Penrose 1996). The idea is an objective-collapse proposal in which observers play no special role; it descends from Károlyházy's 1966 considerations through Diósi's 1989 model (doi:10.1103/PhysRevA.40.1165) and its energy-conserving modification by Ghirardi, Grassi and Rimini (doi:10.1103/PhysRevA.42.1057), and it is testable in principle through the mirror-superposition experiment of Marshall, Simon, Penrose and Bouwmeester (doi:10.1103/PhysRevLett.91.130401). A survey of the physical picture is the Wikipedia article on the Penrose interpretation (https://en.wikipedia.org/wiki/Penrose_interpretation).
The physical criterion is a conjecture about nature, not a theorem, and this mission does not ask for its proof. What is a theorem is the mathematical backbone by which Penrose computes the quantity — the measure of incompatibility of the two superposed space-time geometries in the Newtonian limit — and identifies it, up to an explicit constant, with the gravitational self-energy of the difference of the two mass distributions. Establishing that chain in Lean 4 is this mission's goal.
Fix a real gravitational constant . A mass distribution is a smooth, rapidly decreasing (Schwartz) function : smooth enough that the potential below is twice differentiable and all integrals converge, and decaying so that boundary terms in the whole-space integration by parts vanish. In Lean these are elements of Mathlib's SchwartzMap over three-dimensional Euclidean space.
The Newtonian potential of is
the gravitational field is , and the Laplacian is the trace of the second derivative: the sum of second directional derivatives along the standard orthonormal basis. Penrose's measure of incompatibility of two mass distributions is
the squared norm of the difference of the two field gradients (Penrose 1996, Section 6). Two further quantities from the paper: the gravitational self-energy of a distribution ,
and the interaction energy between two distributions, .
Sign conventions. The displayed formulas of Section 6 of the paper mix conventions: the paper's Poisson display is inconsistent with its displayed potential formula . This mission fixes the convention under which the paper's chain of identities holds as written: , with the potential formula above. Under this convention the first three identities of the displayed chain hold verbatim; the final displayed formula of the paper carries a sign and constant slip and is corrected here to . The physical reading always takes , but no item needs that hypothesis.
The goal is the paper's central identification: the incompatibility measure is the gravitational self-energy of the difference of the two mass distributions, up to the explicit constant ,
The supporting chain, each step a milestone, from Section 6 of the paper:
Two structural facts complete the mission: the self-energy is invariant under translation of the distribution (the two locations of Penrose's displaced lump have equal individual self-energies), and under that equal-self-energy hypothesis is determined by the interaction energy and the common self-energy,
which is the precise sense of the paper's remark that, apart from the factor , it does not make any difference which expression is used.
The result itself. The chain turns a space-time consideration — the failure of a consistent time-translation for the superposed geometry — into a computable Newtonian quantity, and identifies that quantity with a classical binding-energy functional. It is the quantitative core of the Diósi–Penrose collapse criterion: every numerical prediction of the model (collapse rates for dust specks, electrons, mirrors) is extracted from the self-energy of the difference distribution.
Formalizing it. None of this chain is formalized anywhere to our knowledge, and Mathlib has no Newtonian-potential layer at all: no potential, no Poisson equation, no gravitational energy functionals. The mission therefore builds reusable infrastructure — Schwartz densities over Euclidean space, the Newtonian potential with its gradient and Laplacian, and the energy functionals — which serves any later Newtonian-gravity formalization (the Schrödinger–Newton equation, Diósi–Penrose dynamics). The proofs exist in the classical potential-theory literature (elliptic regularity for Poisson's equation; change of variables for translation invariance): the mission asks solvers to formalize known mathematics, not to prove new physics.
The naive attack on Poisson's equation — differentiate twice under the integral sign — fails at the singularity , where the kernel is not even once differentiable. That the potential is nonetheless twice differentiable with at every point is a genuine elliptic-regularity theorem; solvers will need either a distributional argument with cutoffs and a limiting step, or a direct construction of the second directional derivatives with explicit remainder estimates. The whole-space integration by parts needs decay control: the difference potential decays only like when the difference distribution has nonzero total mass, so the boundary term over large balls must be estimated rather than assumed zero. The translation-invariance milestone is a change of variables in a double integral whose kernel is singular on the diagonal — routine, but integrability demands care.
The Lean representation: mass densities are SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ; integrals are Bochner integrals with respect to Mathlib's volume on Euclidean space; the Laplacian is the trace of the second Fréchet derivative, the sum of second directional derivatives along the standard basis vectors. The gravitational constant is an unconstrained real parameter: every identity in the chain is algebraic in , and the physical reading is recorded here only. Degenerate inputs: for Schwartz densities every integral appearing in the items converges; nevertheless, Lean's integral returns for a non-integrable integrand, so establishing the relevant integrability is part of each proof — the identities are stated between the honest (convergent) quantities. No item carries an unsatisfiable hypothesis, and no statement is specialized to positive densities: the paper's derivation nowhere uses positivity, so the items quantify over all Schwartz . A trivializing formalization is ruled out: is defined independently of the self-energy (an norm of a field difference versus a double integral of densities), and the goal asserts their equality.
A physical law is a claim about what happens whenever a preparation is repeated, not about a single run. The objects of the law are therefore ensembles: the statistical outputs of a preparation procedure. Classical probability distributions and quantum density operators are two realizations of that idea, and they share a convex structure coming from statistical mixing. Gabriele Carcassi and Christine A. Aidala isolate that structure in the draft chapter Ensemble spaces (12 October 2026), as part of the Assumptions of Physics project (assumptionsofphysics.org).
The convex fragment already separates a classical behaviour from a non-classical one. In a classical ensemble space, an ensemble that is separate from two ensembles is separate from every mixture of them. In a quantum ensemble space it need not be: the equal mixture of two orthogonal pure states is not separate from a pure state in their span. The draft turns this distinction into a theorem that uses only mixing. Monodecomposability — every decomposable ensemble has no two decompositions in which one summand is separate from both summands of the other — holds if and only if mixtures preserve separateness (Proposition 1.35).
This mission formalizes that equivalence and the lemmas of §§1.2–1.3 that it depends on. Entropy, affine embedding, and the open problems of the same draft are later developments and are not assumed here.
An ensemble space is a nonempty topological space that is and second countable, together with a continuous mixing operation
Mixing is the identity , idempotent (), commutative (), and associative in the following sense. If , and , then
In the formalization the operation is mix p a b, equal to . Binary mixing records only the first coefficient.
A finite mixture , for with , is the nested mixture (1.11) of the pairs with , in the given order. Reordering the pairs does not change the ensemble (Corollary 1.12).
An ensemble is a component of when for some ensemble and some . Two ensembles are separate, written , when they have no common component. An extreme point has no component other than itself. An internal point admits every ensemble as a component. A boundary point is a point that is not internal.
A set is bounded around when every open neighbourhood of admits some with .
An ensemble is decomposable when it is a mixture with and ; separately decomposable when the two summands may be taken separate; and multidecomposable when it admits two such decompositions
with and . It is monodecomposable when it is not multidecomposable. The space is monodecomposable when every decomposable ensemble is. Mixtures preserve separateness when and imply for every .
For an ensemble space ,
The two sides are exactly Definitions 1.33 and 1.28. No entropy, orthogonality, or finite-dimensionality hypothesis is added, and none is removed.
For with and any permutation ,
and the common value exists as an ensemble.
A set is bounded around if and only if whenever in and .
The set of internal points is convex: it is closed under mixing.
Components and separateness satisfy the six properties listed in the draft: every ensemble is a component of itself; a component yields a common component, so the two ensembles are not separate; separateness is irreflexive and symmetric; distinct extreme points are separate; an internal point is not separate from any ensemble; separate ensembles are boundary points.
If is separate from for some , then is separate from for every .
An ensemble is extreme if and only if it is not decomposable.
Proposition 1.35 is the convex form of the draft's classicality test. One direction says that if mixing can create a common component where none existed, then some ensemble has two genuinely different separate decompositions. The other says that if mixing never does this, then no decomposable ensemble is multidecomposable. The quantum Bloch ball is the draft's witness that the property can fail; the classical simplex is the witness that it can hold. Those two model statements (Proposition 1.34 and Propositions 1.29–1.30) are not part of this mission, but the interface they would plug into is.
The same interface is what the later sections of the draft extend: entropy is defined on a space that already mixes, and affine combinations are built from that mixing. A machine-checked Proposition 1.35 is a base those extensions can import without taking the entropy axiom as a hypothesis they do not use.
The argument in the draft is a proof, not an open problem. It had not been formalized against this 12 October 2026 text. An earlier formalization on this platform records Axioms 4.4, 4.7 and 4.55 of the 31 December 2025 book, in which entropy is part of the same structure. That package is a different source. Importing it here would add the entropy axiom to theorems proved in the draft before entropy is introduced, and would weaken them.
The equivalence is not a rephrasing of the definitions. One direction needs Proposition 1.27, whose proof places an auxiliary ensemble on a segment and rewrites coefficients so that a common component of and one mixture becomes a common component of and another. The arithmetic is sensitive to which endpoint is which, and to the restriction rather than .
Corollary 1.12 is an induction on a bracketed expression, not on an unordered convex combination. Definition 1.10 deletes zero coefficients before bracketing. An encoding that feeds a zero coefficient to binary mixing denotes the same point only after the mixture axioms are applied; the draft's definition does not do that. The statement below follows the draft and deletes zeros first.
Proposition 1.17 is a topological fact about a continuous binary operation on a space that need not be a topological vector space. There is no scalar multiplication to rescale a neighbourhood, so the argument has to manufacture the shrink from mixing alone. Boundedness around is not the same as metric boundedness, and the draft does not assume a metric.
The carrier is a type with a topological-space instance. An EnsembleSpace packages nonemptiness, the and second-countability axioms, and the mixing operation. Coefficients of the operation are elements of the unit interval. In the associativity axiom, each real expression is shown to lie in and is then used as that element; it is not replaced by a projection.
Finite mixtures are partial. Zero coefficients are removed, order preserved, and the rest is folded by binary mixing as in (1.11). The fold returns no value if every coefficient was zero or a tail sum vanishes. On inputs with nonnegative coefficients at most that sum to , Corollary 1.12 asserts that a value exists. Real coefficients that arise while rescaling a tail are passed through the projection onto , which is the identity for data obeying those hypotheses. The empty index set cannot occur under the sum hypothesis: the sum of no coefficients is .
Separateness, components, extreme and internal points, decomposability and monodecomposability are propositions on this structure. A component uses a coefficient in . A decomposition uses a coefficient in and two distinct ensembles. Multidecomposability asks for two such decompositions, with one summand of the first separate from both summands of the second.
Entropy, orthogonality, affine combinations, vector-space embeddings, metrics, and the classical and quantum models are out of scope. In particular the goal must not be restated as “every Choquet simplex is a simplex”, and separateness must not be replaced by disjointness of supports. Adding the entropy axiom, or cancellativity, is a different theorem. Contributions that build the missing model statements on top of these definitions, without changing them, are the natural continuation; changes to the definitions are not.
Quantifying Coherence establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix an orthonormal reference basis in a finite-dimensional Hilbert space of dimension . For a density matrix , define its -norm of coherence in this basis by , where the absolute value is the complex modulus and both ordered off-diagonal entries are counted. Let be any finite family of density matrices on this same space, and let be real numbers with and . Then
This is condition (C3) for the coherence functional of Eq. (9): mixing quantum states cannot increase coherence above the weighted average of the component coherences.
Fix an orthonormal reference basis in a finite-dimensional Hilbert space of dimension . For a density matrix , define its -norm of coherence in this basis by , where the absolute value is the complex modulus and both ordered off-diagonal entries are counted. Let be any finite family of density matrices on this same space, and let be real numbers with and . Then
This is condition (C3) for the coherence functional of Eq. (9): mixing quantum states cannot increase coherence above the weighted average of the component coherences.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Fix and . This is a unit vector. For each unit vector , define . These matrices preserve diagonal positive operators and satisfy , with
Every density matrix has a finite ensemble , with nonnegative weights summing to one and unit vectors . The named matrices form a complete incoherent Kraus family and
Thus the resource prepares any target; outcomes are forgotten for mixed targets.
Let be a unitary on a qubit. For define
These matrices are chosen from before the unknown input. They preserve diagonal positive matrices, obey , and for every unit input ,
Both outcomes implement the desired gate, consuming one coherent resource qubit.
Let be a nonnegative real functional on density matrices for every finite dimension . Suppose it is convex on finite ensembles and satisfies selective monotonicity for every complete incoherent Kraus family, allowing different positive output dimensions per branch. Zero-probability branches contribute zero. Then for every incoherent family with a common output dimension,
This implication requires no faithfulness hypothesis.
Let be nonnegative on pairs of density matrices in each positive finite dimension, zero exactly on equal arguments. Suppose its minimum over incoherent density matrices is attained for every state. Define by the infimum of these distances. It is an actual attained minimum: a minimizing incoherent exists, , and this value is no larger than for any incoherent . Moreover,
The attainment premise makes the source's minimum domain explicit without imposing continuity.
Let be a dimension-indexed nonnegative distance on density matrices whose incoherent-state minima are attained. Assume for every completely positive trace-preserving map, including changes of finite positive dimension. For any complete incoherent Kraus family of common output dimension,
This gives axiom (C2a) for the induced candidate.
Let be nonnegative and jointly convex on density-matrix pairs in every positive finite dimension, with attained incoherent-state minima. For any finite ensemble , there are minimizing incoherent states , and
Thus is convex. No contractivity assumption is needed.
In each positive finite dimension choose any genuine norm on the complex vector space of matrices. It need not be unitarily invariant or contractive. For every density matrix the minimum over diagonal density matrices is attained, and the resulting candidate satisfies
The norm is specified by nonnegativity, definiteness, the triangle inequality and complex absolute homogeneity.
Let be a density matrix of dimension , and let delete its off-diagonal entries. Use natural-log entropy . The matrix is an incoherent density matrix, and
Here is Umegaki relative entropy, infinite when the support condition fails, with . The statement includes singular states and proves the diagonal minimizer's optimality.
In every positive finite dimension let , with natural logarithms. It is nonnegative, vanishes exactly on diagonal states, is convex, and is monotone under all complete incoherent operations. In particular, for selective operations with positive branch output dimensions,
It also satisfies when the output dimension is common. These clauses establish all the proper-coherence requirements; null branches are allowed.
For every density matrix in dimension , natural-log entropy gives
The vector is normalized and satisfies . This identifies an attaining witness without a uniqueness claim. Dimension one yields zero.
For any density matrix in dimension , is incoherent and minimizes the entrywise absolute-sum distance:
This value is nonnegative and is zero exactly when is diagonal. This is the entrywise norm, counting both ordered positions, with no factor one half.
Let . For every complete incoherent Kraus family on a positive-dimensional input, allowing different positive output dimensions, and every input density matrix,
When the output dimension is common, as well. Incoherence is required separately of each branch; no individual-outcome decrease is asserted.
For a density matrix in any dimension , the diagonal density matrix attains
The theorem includes the minimizing value and its comparison with every incoherent density matrix. This is the squared Hilbert–Schmidt distance, not the operator norm; it does not assert coherence monotonicity.
Let be a density matrix and let be a complete incoherent Kraus family with common positive output dimension . Put the flag first in its classical basis and define the unnormalized-block sum
Then is a density matrix, and . The product basis is flattened consistently to dimension . Zero-probability blocks contribute zero without division.
Let obey and . Define
The matrix is a density matrix and these matrices form a complete incoherent instrument. For ,
The endpoint is allowed; for this particular input both branch probabilities are . This disproves selective monotonicity.
Let . In every positive finite dimension the minimum
is attained. This candidate is nonnegative, vanishes exactly on diagonal states, is monotone under nonselective incoherent operations and is convex on finite ensembles. This establishes (C1'), (C2a), (C3); no selective monotonicity is claimed.
In every positive finite dimension,
has an attained minimum. It is nonnegative, zero exactly on diagonal density matrices, monotone under nonselective incoherent operations and convex on finite ensembles. Here is the full trace norm, without a factor one half. This supplies (C1'), (C2a), (C3) and makes no (C2b) claim.
There exist a positive finite dimension , a density matrix and an incoherent density matrix such that
Thus dephasing need not yield a closest incoherent state for the full trace norm. Since dephasing itself is feasible, this is equivalent to the source's existential failure of equality with the minimum.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
General Entanglement Breaking Channels establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and be integers. Fix density matrices and positive semidefinite matrices , and define the complex-linear Holevo map on all matrices by
For every positive finite reference dimension and every density matrix on ,
Here the cone consists of finite sums with nonnegative real coefficients and includes zero. If, in addition, is a POVM, meaning , then is completely positive and trace-preserving, and every such joint output is a separable density matrix: it is a finite convex combination of product density matrices.
This is precisely the measure-and-prepare implication of Theorem 4 and its printed channel specialization. It applies to entangled inputs without purity, orthogonality, or independence restrictions on the prepared states.
Formalization Note The general part uses the frozen separable-positive-cone predicate because unrestricted positive effects need not preserve trace. The channel part uses normalized separability. The identity always acts on the reference factor.
Let and be integers. Fix density matrices and positive semidefinite matrices , and define the complex-linear Holevo map on all matrices by
For every positive finite reference dimension and every density matrix on ,
Here the cone consists of finite sums with nonnegative real coefficients and includes zero. If, in addition, is a POVM, meaning , then is completely positive and trace-preserving, and every such joint output is a separable density matrix: it is a finite convex combination of product density matrices.
This is precisely the measure-and-prepare implication of Theorem 4 and its printed channel specialization. It applies to entangled inputs without purity, orthogonality, or independence restrictions on the prepared states.
Formalization Note The general part uses the frozen separable-positive-cone predicate because unrestricted positive effects need not preserve trace. The channel part uses normalized separability. The identity always acts on the reference factor.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let and let be complex-linear. A finite Holevo representation with density matrices and positive semidefinite effects exists if and only if breaks entanglement in the separable-positive-cone sense.
For every supplied such representation, trace preservation is equivalent to being a POVM. For every supplied representation (2) with unit output vectors , it is equivalent to ; the input vectors need not be unit or nonzero.
This identifies measure-and-prepare maps without presupposing complete positivity or trace preservation.
For , let be the set of complex-linear entanglement-breaking, trace-preserving maps on . Then
Thus is EBT for any two EBT maps and any . Convexity refers to maps on all operators and supports the paper's study of extreme channels.
Let and let be a unitary matrix on . Then
This records that unitary dynamics preserves some entanglement. The dimension restriction corrects the printed sentence: at unitary conjugation is EBT. The correction requires independent source moderation.
Correction to the printed source.
Printed: Conjugation with a unitary matrix is not EBT, without any stated dimension exception.
Corrected: Restrict the unitary-channel assertion to d at least two.
Reason: At d=1 every joint state is separable across the one-dimensional acted-on system; the identity channel is EBT.
Let and let be a density matrix on . Define the replacement map on all operators. Then
Here pure means for a unit vector . Both ambient convex sets are recorded, as supported by the point-channel paragraph and Theorem 5(A),(B).
Let , let be density matrices, and let be positive semidefinite. For arbitrary orthonormal bases and , set . Then, on every operator ,
If the effects form a POVM the Kraus family is normalized. In the CQ case , the reduced family is , and is normalized. In the QC case , it is , normalized when is a POVM. For pure-output CQ maps it further reduces to , with unit .
These are explicit operator-sum witnesses; square roots are the positive matrix square roots.
Let and let be complex-linear. Write . The following six conditions are equivalent:
If preserves trace, the corresponding six-way equivalence holds with a POVM in A, EBT in B, normalized separable density in C, in D, and trace-preserving positivity tests in E,F. Empty general representations are allowed for the zero map. This supplies all the theorem's characterizations, including its continuation on page 5.
Let and let be an extreme CQ map in the source's terminology: for an orthonormal basis and unit vectors ,
Then is an extreme point of the convex set of EBT maps. The vectors may coincide or be dependent. The source-defined class is therefore distinguished from convex extremality itself.
Let , let be an orthonormal basis of , and let be arbitrary unit vectors. For the supplied representation ,
No orthogonality or independence assumption on outputs is imposed. This characterizes which pure-output CQ maps remain extreme in the larger channel set.
Let . If is EBT and is an extreme point of the set of CPT maps, then
Explicitly, an orthonormal input basis and unit output vectors realizing Eq.(8) exist. Neither Choi rank nor a -term Kraus representation is assumed: those are proof conclusions. This identifies the overlap of EBT with the extreme points of CPT.
The two dimension regimes for extreme EBT maps are:
whereas, for every integer , there exists an extreme EBT endomap of that is not CQ.
The qubit proof is attributed by the paper on page 8 to Ruskai [18], quant-ph/0302032. The paper supplies the higher-dimensional counterexamples, including the qutrit example. The result separates EBT extremality from pure-output CQ structure in higher dimensions.
Let and be orthonormal bases of . Put and set
These effects form a POVM, and the computed map is an extreme EBT map which is QC and is not CQ.
The third displayed effect corrects the source's repeated to , as forced by the word trine, normalization, and the proof. Independent source moderation is required. This is a concrete witness rather than a free existential channel.
Correction to the printed source.
Printed: The third effect is printed as (2/3)|g_+><g_+|, duplicating the second.
Corrected: Replace only that third effect by (2/3)|g_-><g_-|.
Reason: The narrative calls this a trine POVM and its proof uses that POVM. The changed effect cancels the off-diagonal entries; the printed effects do not sum to I.
Let and let be a von Neumann measurement: mutually orthogonal Hermitian projections summing to . If some has rank greater than one, then
The actual computed pinching map is used. A rank-two block can retain entanglement, distinguishing such block projections from rank-one dephasing.
Let and let satisfy . If , then the channel with this actual Kraus list satisfies
The empty normalized list is impossible for . The result gives a lower bound on the size of every Kraus representation of an EBT map; its cited ingredients are [11], or [8] with [2].
Let , let be CPT, and let for the unit maximally entangled vector . If , then
where is matrix transpose, a complex-linear map. The exact rank and TP hypotheses are retained; the low-rank separability ingredient is attributed to [10].
Let be a separable density matrix on , with . Suppose both and its first marginal have rank . Then there exist , nonnegative weights summing to one, and unit vectors , such that
The rank is independent of the ambient dimensions. First proved in [10], the lemma receives a new proof here and bounds the length of separable decompositions under a matching marginal-rank assumption.
Fix an orthonormal basis of . Let , , , and . The computed channel
is extreme in EBT, is not CQ, and is not extreme in CPT. Its distinct rays have overlap , and the only Hermitian projections commuting with all four pure densities are , ruling out an orthogonal block split.
Its positive rank-one Holevo form is essentially unique: in any finite representation with strictly positive weights , unit output vectors , and unit input vectors , each pair of pure densities equals for some . The sum of weights belonging to each ray is . This permits splitting and merging weights and arbitrary vector phases; it makes no assertion about arbitrary mixed-output or zero-effect presentations.
For each i, the plane reflection U_i=I-2|v_i⟩⟨v_i| is unitary, and on every operator X the final page-12 construction is explicitly realized by Phi(X)=(1/4)X+(3/16) sum_(i=0)^3 U_i X U_i†. The five nonnegative coefficients sum to one.
Let and let be a real Hilbert–Schmidt orthonormal basis of Hermitian matrices, with and the remaining matrices traceless. For a density matrix , put , which is real. Then
The printed is corrected to its reciprocal, as forced by trace normalization. This coordinate description is used in the map factorization; independent source moderation of the correction remains required.
Correction to the printed source.
Printed: The source prints w_0=d^(1/2) with G_0=d^(-1/2)I and trace rho=1.
Corrected: State w_0=d^(-1/2); all other displayed coefficient formulas are retained.
Reason: Directly Tr(rho G_0)=Tr(rho)/sqrt(d)=1/sqrt(d); rho=I/2 is a concrete counterexample to the printed exponent.
In the preceding Hermitian basis, let be density matrices and positive semidefinite effects, . Define , and for the computed Holevo map. Then
Moreover, is a POVM if and only if the first row of is . Both factors have rows and columns. The product corrects the printed according to those dimensions and the unchanged entrywise formula. Independent moderation of this correction is required.
Correction to the printed source.
Printed: The source prints T=W^T U although W and U are d^2 by N.
Corrected: Use T=W U^T and retain the source's unchanged entrywise sum t_jn=sum_k w_jk u_nk.
Reason: W^T U has shape N by N, while W U^T has the required d^2 by d^2 shape and exactly the printed entries.
Let , let be the Hermitian coordinate basis above, and let be CQ or QC. Let be its full -by- coordinate matrix and the density matrices. Then
The second dimension is affine in the trace-one hyperplane, following the separation of the identity coordinate on page 12. A linear-dimension interpretation would fail at . This bounds the geometry of the output-state set.
Correction to the printed source.
Printed: The source calls the density image a subspace of dimension at most d-1.
Corrected: Interpret this as an affine span over the real numbers within the trace-one hyperplane.
Reason: Equation (23) fixes the identity coordinate; the convex hull of d density outputs has affine dimension at most d-1. Linear dimension zero already fails for the d=1 state.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Separability Criterion for Density Matrices establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let and index orthonormal bases of two nonempty finite-dimensional complex Hilbert spaces, with no requirement that their dimensions agree. Let be a density matrix on their tensor product, so is positive semidefinite and . Suppose it is separable: for some finite ensemble of density matrices on the first subsystem and on the second, and real weights summing to one, . Define its first-subsystem partial transpose by . Then
Equivalently, all eigenvalues of the Hermitian matrix are nonnegative. This is a necessary condition for separability, with no assertion of a converse.
Formalization Note The unspecified ensemble in Eq. (1) is represented by an arbitrary finite ensemble in the paper's finite-dimensional setting. Allowing zero weights is equivalent to the printed positive-weight convention after deleting zero-weight terms; normalization excludes an empty ensemble.
Let and index orthonormal bases of two nonempty finite-dimensional complex Hilbert spaces, with no requirement that their dimensions agree. Let be a density matrix on their tensor product, so is positive semidefinite and . Suppose it is separable: for some finite ensemble of density matrices on the first subsystem and on the second, and real weights summing to one, . Define its first-subsystem partial transpose by . Then
Equivalently, all eigenvalues of the Hermitian matrix are nonnegative. This is a necessary condition for separability, with no assertion of a converse.
Formalization Note The unspecified ensemble in Eq. (1) is represented by an arbitrary finite ensemble in the paper's finite-dimensional setting. Allowing zero weights is equivalent to the printed positive-weight convention after deleting zero-weight terms; normalization excludes an empty ensemble.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let be a density matrix on two nonempty finite subsystem spaces with basis sets and . Define , transposing only the first subsystem. Then
The assertion holds for arbitrary subsystem dimensions and requires no separable decomposition. It makes the eigenvalue test a test on a Hermitian matrix.
Let be a density matrix on , with nonempty finite basis sets. Let and be arbitrary complex unitaries on the respective subsystem spaces, and set . Writing for transposition of the first subsystem only, one has
as polynomials in . Hence the two partial transposes have the same eigenvalues with algebraic multiplicities. This expresses the criterion's independence of local basis choices.
For two qubits, let , , and , where . Let . Its characteristic polynomial is
In particular, if , then is positive definite and satisfies the necessary separability criterion. The calculation identifies the effect of white noise, whose random fraction includes all four Bell components equally.
Let satisfy , and let . Set and . If , then, for ,
The negative eigenvalue obstructs separability. Both the determinant and spectral conclusions are retained.
Let be the two-qubit singlet density matrix and let . Define and . Then
Thus even an arbitrarily small positive singlet fraction in this family produces entanglement. The zero-fraction endpoint is excluded by the source's positivity condition.
Let be a density matrix on two nonempty finite subsystem spaces and , and let . Group the copies so that the first observer holds all registers and the second holds all registers. In these coordinates let denote the product with entries , and put . Then
The last implication holds independently of separability. This is the finite-copy stability that prevents strengthening this algebraic test by taking identical copies.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Reversing quantum dynamics with near-optimal quantum and classical fidelity (Barnum, Knill) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be an ensemble of density matrices on a finite-dimensional Hilbert space, indexed by a finite label set , with probabilities , . Write and , and let be the generalized inverse square root (non-zero eigenvalues inverted, zero eigenvalues kept). The pretty good measurement (PGM) has effects . For density matrices let be the Bures–Uhlmann fidelity.
Then the success probability of the PGM, and therefore the optimal success probability over all measurements (POVMs with one outcome per label), satisfy
the sums running over ordered pairs of distinct labels.
This bound expresses the error of state discrimination through pairwise overlaps only; it is the tool behind the polynomial query complexity of the hidden subgroup problem (Childs, Theorem 10.1).
Formalization Note The paper writes the left side of (39) as and opens (38) with , which is reversed relative to its own Corollary 4 and false in general (two equiprobable pure states with overlap 0.9). Its proof establishes the bound for the PGM success probability and then for the optimal ; that is what is stated. The reversal map of Eq. (35)–(36) is not formalized: for of form (35), classical fidelities of reversal are exactly measurement success probabilities on the ensemble.
Let be an ensemble of density matrices on a finite-dimensional Hilbert space, indexed by a finite label set , with probabilities , . Write and , and let be the generalized inverse square root (non-zero eigenvalues inverted, zero eigenvalues kept). The pretty good measurement (PGM) has effects . For density matrices let be the Bures–Uhlmann fidelity.
Then the success probability of the PGM, and therefore the optimal success probability over all measurements (POVMs with one outcome per label), satisfy
the sums running over ordered pairs of distinct labels.
This bound expresses the error of state discrimination through pairwise overlaps only; it is the tool behind the polynomial query complexity of the hidden subgroup problem (Childs, Theorem 10.1).
Formalization Note The paper writes the left side of (39) as and opens (38) with , which is reversed relative to its own Corollary 4 and false in general (two equiprobable pure states with overlap 0.9). Its proof establishes the bound for the PGM success probability and then for the optimal ; that is what is stated. The reversal map of Eq. (35)–(36) is not formalized: for of form (35), classical fidelities of reversal are exactly measurement success probabilities on the ensemble.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Potential-Function Proofs for First-Order Methods (Bansal, Gupta) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the regret bound of online mirror descent with a constant step size.
Let be a finite-dimensional real vector space with an arbitrary norm , and let be the dual norm of a linear functional . Let be a convex body (closed, convex, with nonempty interior). Let be differentiable functions that are convex over . Let be differentiable and -strongly convex with respect to for some , i.e. for all , and let be its Bregman divergence. Fix a step size and a starting point . Mirror descent produces and, for , where ; here minimizes over . Then for every such run and every ,
With the Euclidean norm and it recovers the regret bound of projected online gradient descent; with negative entropy on the simplex it gives the Hedge bound.
Formalization Note The source prints the second sum as ; is a typo for and is corrected. Gradients are Fréchet derivatives, whose operator norm is the dual norm. The first iterate is the Bregman projection of (equal to when ).
This is the regret bound of online mirror descent with a constant step size.
Let be a finite-dimensional real vector space with an arbitrary norm , and let be the dual norm of a linear functional . Let be a convex body (closed, convex, with nonempty interior). Let be differentiable functions that are convex over . Let be differentiable and -strongly convex with respect to for some , i.e. for all , and let be its Bregman divergence. Fix a step size and a starting point . Mirror descent produces and, for , where ; here minimizes over . Then for every such run and every ,
With the Euclidean norm and it recovers the regret bound of projected online gradient descent; with negative entropy on the simplex it gives the Hedge bound.
Formalization Note The source prints the second sum as ; is a typo for and is corrected. Gradients are Fréchet derivatives, whose operator norm is the dual norm. The first iterate is the Bregman projection of (equal to when ).
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum Amplitude Amplification and Estimation (Brassard, Høyer, Mosca, Tapp) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the overlap identity for Fourier phase states (Brassard, Høyer, Mosca, Tapp, Lemma 10), which yields the outcome distribution of Fourier-transform phase estimation.
Let be an integer. For a real number , the phase state on the -dimensional register with orthonormal basis is
For reals , let be the distance on the circle . Let , , and . Then:
The inner product is conjugate-linear in its first argument. Taking gives the probability of outcome when is measured, which is the paper's Theorem 11 and the lecture notes' Proposition 3.11.
Formalization Note The phase state is the shared definition bhmtPhaseState M ω on EuclideanSpace ℂ (Fin M), and is circDist ω0 ω1 = |(ω0 − ω1) − round(ω0 − ω1)|, which equals the minimum in Definition 9.
This is the overlap identity for Fourier phase states (Brassard, Høyer, Mosca, Tapp, Lemma 10), which yields the outcome distribution of Fourier-transform phase estimation.
Let be an integer. For a real number , the phase state on the -dimensional register with orthonormal basis is
For reals , let be the distance on the circle . Let , , and . Then:
The inner product is conjugate-linear in its first argument. Taking gives the probability of outcome when is measured, which is the paper's Theorem 11 and the lecture notes' Proposition 3.11.
Formalization Note The phase state is the shared definition bhmtPhaseState M ω on EuclideanSpace ℂ (Fin M), and is circDist ω0 ω1 = |(ω0 − ω1) − round(ω0 − ω1)|, which equals the minimum in Definition 9.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
In a Proof-of-Stake (PoS) cryptocurrency, new coins are not mined with computing power: before each date the protocol picks one coin holder at random, with probability equal to the fraction of coins she holds, and pays her a reward of new coins. A common claim in the cryptocurrency press is that this makes the rich richer: larger holders are selected more often, so their holdings should grow faster. Roşu and Saleh (Management Science 67(2), 2021) test this claim in a model that is, for a buy-and-hold investor, a generalized Pólya urn whose number of added balls varies with time.
Their first result (Proposition 1) is that an investor's share is a martingale with an almost-sure limit whose mean is the initial share, which the paper itself calls standard for Pólya urns. The sharper question is whether shares are stable in the strict sense: does the limiting share concentrate at the initial share when the economy starts with many coins? The answer depends on how fast the reward grows with the coin supply, and Proposition 4 locates the threshold exactly.
Time is discrete, . Fix a probability space with a filtration . Initially coins are outstanding, and the tracked investor (investor 1) holds of them. At each date the protocol pays a deterministic reward , so the coin supply is
Let , -measurable, indicate that investor 1 is selected at . She never trades, so her coins follow , and her share is . The PoS selection rule is
The other investors enter only through . The power reward is for , with constants .
The variance sequence is , , the paper's (A12). Proposition 1 gives an almost-sure limit . For the goal, the initial share is fixed and the initial supply varies: model has and .
For and ,
The statement fixes no constant and no rate. It is the full equivalence, as printed.
The result. Proposition 4 separates two regimes of PoS reward schedules that grow with the supply. For sublinear growth () a large economy keeps every holder's share near its starting value: the protocol does not redistribute wealth. For linear or faster growth () the limiting share has the maximal variance whatever the initial supply. The share then ends near or with probability bounded away from zero, even though its mean is unchanged. Proposition 3 of the same paper covers non-increasing rewards. Together they say which PoS implementations give stable shares.
Formalizing it. The paper's proofs are short and informal. This mission produces a machine-checked version of the model and of the equivalence, and a reusable Lean treatment of a time-inhomogeneous two-colour Pólya urn: the martingale property, the closed-form variance recursion, and the variance of the limit. None of these results has a machine-checked proof on Prove2Me or in Mathlib.
The "if" direction combines Lemma 5 with Chebyshev's inequality. Lemma 5 needs a Riemann-sum comparison: the sum is bounded by . This uses that is increasing and is decreasing, and the details matter at the first index. The step from the variances of to the variance of the limit needs dominated convergence for squares.
The "only if" direction is where the printed argument is loose. The page lets inside a statement about . What is true and needed is that for each fixed the ratio stays bounded below in , so . The tail bound (A31) must then be derived from the exact variance alone, uniformly in . Neither Doob's convergence theorem nor Chebyshev's inequality gives this lower bound directly.
All objects are defined in the namespace PoSShares.Stability. A Model Ω carries the filtration, , , and the indicators . coinSupply, coins, share, IsPoS and IsPowerReward are its supply, coins (5), share (1), selection rule and power reward. aSeq and alphaSeq are (A12) and (A16), both started at index with value . Committed conventions:
μ.real.Trivializing formalizations are ruled out:
IsPoS is satisfiable for every , and , and the power reward rule has a solution for all .limUnder default.A complete development needs Mathlib's conditional expectation and conditional variance, the martingale convergence theorem for bounded martingales, the law of total variance, Chebyshev's inequality, and integral comparison for monotone functions. The urn lemmas (milestones 1–5 and 8) apply to any deterministic reward schedule and are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 5.
An online allocator must commit to an action after each arrival, although later arrivals can change which actions would have been best. Revenue management and online resource allocation use regret to measure the expected reward lost against a benchmark. If the benchmark sees too much future information, this gap can grow with the horizon even when the online controller behaves optimally. Vera, Banerjee, and Gurvich use a benchmark whose extra information can be chosen for the application, and relate regret to two quantities that can be studied separately: how often the online action disagrees with an informed action, and how accurately a proposed value function satisfies a Bellman equation (Vera–Banerjee–Gurvich, 2020, §§2–3).
The paper proves constant-regret application results for online probing, dynamic pricing, and learning by combining this framework with estimates particular to each model. This mission isolates the framework's Theorem 5 and the displayed statements leading to it. Its result is known on paper; the work here is to give the model, the conditional expectations, and the regret bound machine-checkable statements.
There are decision periods, indexed by time to go . At the start of period the controller is in state and observes an input . It selects an action from a nonempty feasible set , collects real reward , and moves to . The initial state is the fixed state .
The observed filtration is generated by the arrivals . A non-anticipative policy chooses an -measurable action from the current state. Offline has the augmented filtration , where is a fixed sigma-algebra carrying extra information. Offline's value is the feasible-action maximum in the conditional Bellman equation (2), with . Its expected initial value is the benchmark for the online policy's expected reward. Regret is their difference.
A relaxed value and a Bellman loss obey the Bellman inequalities if initially bounds the conditional Offline value, ends at zero, and at each state is at most one feasible action's immediate reward plus its expected relaxed continuation and . An action meeting this inequality is satisfying. A maximum-loss bound controls the shortfall of every feasible action. For a policy with action on its actual trajectory, is the event that is not satisfying under this same and .
Proposition 1 concerns a feasible -adapted policy that always takes satisfying actions. It bounds its shortfall from Offline by the expected accumulated Bellman loss:
The proposal also states the one-step displayed inequality from its proof, where a conditional continuation at a fixed state and action becomes the conditional continuation of the policy's random trajectory.
Theorem 5 concerns a feasible non-anticipative policy. It states the pathwise-compensation expectation bound and, when is nonnegative, the paper's two-term bound:
The milestones include the paper's maximum-loss, compensated one-step, and iterated displays on the route to this target. The first inequality is also stated for signed ; only the second requires .
The theorem turns a regret analysis into two concrete estimates. An application can count or bound the periods when the online action fails the informed satisfying-action test, and can separately quantify the error in its chosen relaxed value. Neither quantity alone certifies small regret; the theorem supplies the inequality connecting both to the benchmark's actual reward gap. The paper's constant-regret claims use application-specific bounds on these terms (Vera–Banerjee–Gurvich, 2020, §§4–6).
A complete formalization would establish the conditional-expectation and measurability infrastructure needed to apply this template to other finite-horizon allocation models. The paper gives a proof of Theorem 5, but the theorem and its applications have no machine-checked proofs in this mission. The proposal records the open Lean statements and a statement-only non-vacuity check for the exact Bellman value with zero loss.
Definition 5 describes a satisfying action for a fixed state and action, while Theorem 5 evaluates it at a random state and a policy's random action. The conditional expectation in that definition cannot simply be substituted syntactically for the conditional expectation of the ensuing trajectory. Countable states and finite actions make the substitution meaningful, but measurability of the selected state and action still has to be established. The same issue appears in the maximum-loss display. Time runs backward, so the information at contains the information at ; a forward-indexed filtration would change the conditional expectation in the paper's formulas.
The second displayed inequality presents a separate statement issue: removing from is valid only for nonnegative . The paper allows signed Bellman losses elsewhere, so nonnegativity is attached to that inequality rather than to the definition of Bellman inequalities.
The Lean model uses a countable state type, a finite nonempty action type, real rewards, and an explicit nonempty feasible-action set. The probability space carries a probability measure, measurable arrivals, and an auxiliary sub-sigma-algebra . The observed and augmented information families are plain sigma-algebra families because their order decreases with time to go. The index is terminal; decision sums and hypotheses use exactly . Offline's value is defined by the feasible-action Bellman recursion and is never a free benchmark variable.
The source bounds the maximum reward above. This formalization additionally bounds feasible rewards, , and in absolute value over the finite horizon, and requires measurable reward, transition, and feasibility data. These assumptions ensure the real integrals and conditional expectations have their intended values. Definition 4 is an almost-sure real upper bound rather than a supremum that could take a default value. The feasible-action maximum in the Bellman inequality is represented by a feasible witness. The source's family is represented by the single sigma-algebra it generates, .
The goal covers every feasible -adapted state-feedback policy; RABBI is in this class. Proposition 1 retains its distinct -adapted policy class. The disagreement event uses the same as the Bellman inequalities. The maximum-loss display follows Definition 4's parentheses and sign, correcting a printed slip on p. 14. The nonnegative-loss condition corrects the second inequality of the printed Theorem 5. A complete development needs reusable lemmas on finite feasible maxima, measurable state-feedback trajectories, conditional expectations under decreasing information, and integration of finite sums. Contributions to those lemmas and to the five stated milestones are in scope.
Public buyers of medicines, school meals, computers and similar goods often run a framework agreement. A central agency selects an assortment of products through an auction and fixes their unit prices. Public offices then buy from that menu as needed, each choosing what suits it. The European Union awarded €80 billion through framework agreements in 2010, 17% of all public procurement by value. Chile's ChileCompra bought US$3 billion this way in 2018, 22% of the country's public procurement (figures as cited in the paper's introduction). Two decisions are bundled in such a mechanism: which differentiated products to put in the assortment, and at what prices. A larger assortment serves heterogeneous users better; a smaller one lets the buyer extract lower prices from the suppliers, whose costs are private.
Saban and Weintraub (Operations Research, 2021; author version SSRN 3453144) model this trade-off as a mechanism-design problem and ask a structural question: how much does the buyer lose by being restricted to linear prices, where users pick quantities from the posted menu and every supplier is paid its unit price times the quantity sold, compared with a centralized planner who could dictate allocations and arbitrary transfers? Their answer for the Hotelling model of horizontal differentiation, Theorem 4.1, is the goal of this mission.
There are suppliers . Supplier has a private unit cost in a finite set of positive reals, drawn independently with probability mass function and cdf . A profile is .
A unit mass of consumers sits uniformly on ; supplier is located at , with . A consumer at buying from at price has utility , with transportation cost . Allocations (no outside option) give gross consumer surplus , minus times the total transportation cost, and consumer surplus . The demand for an assortment and prices is a maximizer of over with for .
The virtual cost of type is
where is the predecessor of in (itself for the lowest type). Virtual costs are assumed strictly increasing (Assumption 3.1).
In a direct mechanism with allocation and transfers , supplier of type reporting gets interim utility . The two problems are:
denotes the optimal value. Every DecLin mechanism is a Cent mechanism with the same value, so always.
Let . If (1) some profile has for all , and (2) every and consecutive virtual costs differ by at most , then
The proof runs through the following statements, in attack order:
The theorem identifies a regime where linear pricing, the format actually used in framework agreements, loses nothing relative to the best mechanism with arbitrary transfers. In general it does lose: the paper's Example 4.1 has (values and ). The conditions say that virtual costs are close relative to the transportation cost, so that every supplier is in the optimal assortment for some profile and costs can be moved one supplier at a time without leaving the assortment. This gives a design guideline: when products are differentiated enough relative to cost uncertainty, posting unit prices suffices. The companion result for two-part tariffs (Proposition 4.1) and the affine-demand analogue (Theorem 4.2) are outside this mission.
The theorem has a complete proof in the paper (Appendix F and the electronic companion), but no machine-checked version exists. A formal proof would check the discrete-type envelope argument (Proposition 3.1), the explicit Hotelling demand as an optimal-transport maximizer, and the linear-algebraic consistency argument, which has gaps at ties (see Formalization scope). Each of these is reusable: the discrete Myerson characterization applies to any procurement or auction model with finite type spaces, and the Hotelling demand result applies to any model of spatial competition on a segment.
The obvious argument is: solve Cent by Proposition 3.1, then pick prices equal to virtual costs, which induce the right demand. This fails because prices must do two jobs at once. They must reproduce the centralized allocation through consumer choice, which pins down price differences among active suppliers profile by profile, and they must reproduce the interim transfers (11), which pins down averages of across profiles. Prices equal to virtual costs satisfy the first and generally violate the second. The question becomes whether one linear system in all prices of all profiles is consistent.
Lemma F.1 converts consistency into the statement that every dependency among the rows is also a dependency of the right-hand side. Proving that requires showing that the coefficients on transfer rows vanish (Step 1), and this is where Theorem 4.1's conditions enter: Lemma F.2's all-active box and connecting paths propagate from one profile to its neighbours. Without such connectivity the profiles split into classes whose transfer constraints conflict, which is exactly what happens in Example 4.1.
The Lean development lives in the namespace ProcureAssort.Hotelling, with one definition item (Setting) and eleven theorem items. Conventions:
Fin n, 0-indexed, ordered by location; is assumed because needs two suppliers. Types are a Finset ℝ per supplier; "consecutive types" means no element strictly between. Profiles are dependent functions; all expectations are finite sums.The goal cannot be satisfied trivially. DecLin ranges only over mechanisms whose allocation is consumer-optimal for the posted assortment and prices, and whose payments are price times quantity. DecLin therefore cannot choose allocations freely or pay lump sums, and an equality with OPT(Cent) is a substantive claim. The hypotheses are satisfiable, for example with two suppliers at and , and uniform.
A complete development needs: finite-type mechanism-design bookkeeping (interim sums, the envelope formula), the Hotelling demand as a maximizer (a one-dimensional transport argument), finite-dimensional linear algebra for Lemma F.1, and the combinatorics of Lemma F.2. Contributions to any milestone are welcome, as are proofs of the Fredholm alternative and of the discrete Myerson lemma in general form.
Misinformation campaigns target specific people in a social network and rely on the network to spread what they plant. Whether such a campaign can succeed depends on how people combine what they see themselves with what their neighbours believe. Mostagir, Ozdaglar and Siderius (SSRN 3474643; Management Science, 2022, doi:10.1287/mnsc.2021.4265) model a network in which a strategic principal injects slanted news into chosen agents. Some agents are Bayesian and know the truth; the rest are DeGroot agents who average their own news-based opinion with their neighbours' beliefs.
The paper asks when society as a whole can be manipulated. Every later result in it — which agents the principal targets, which networks resist manipulation, how the answer depends on the network's density — is a statement about the agents' long-run beliefs. Its Theorem 2 supplies those beliefs in closed form, and that closed form is the subject of this mission.
DeGroot updating (DeGroot, 1974) and its combination with personal Bayesian updates (Jadbabaie, Molavi, Sandroni and Tahbaz-Salehi, 2012) are standard models of non-Bayesian social learning. Stubborn agents in averaging dynamics were studied by Acemoglu, Como, Fagnani and Ozdaglar (2013). The present model adds a principal who corrupts the signals of targeted agents.
There are agents and a binary state with prior . Agent has a signal quality . At each time agent receives a signal :
Agent 's signals are independent over time. Its personal experience is the posterior it would compute taking every signal at face value. With the numbers of and signals among ,
and .
A set of agents is Bayesian. A Bayesian agent knows and always believes it. Each DeGroot agent has weights and with . For a state , its belief follows the DeGroot update
The influence matrix has zero rows for Bayesian agents and row for DeGroot agents. The vector has entry on Bayesians. The unweighted graph has a link when listens to ; for a DeGroot agent this means .
Assumption 1 (pp. 10–11):
Under Assumption 1, for every principal action , each DeGroot agent's personal experience converges almost surely to a constant , and
where the Bayesian entries of the vector are the correct belief. The goal does not fix the constants: the paper computes them only later (display (2), p. 12).
Theorem 2 reduces the paper's manipulation question to linear algebra. A DeGroot agent ends up believing the wrong state exactly when the corresponding entry of crosses a threshold. The principal's targeting problem then becomes a combinatorial problem over in which the network enters only through . The paper's DeGroot centrality (Proposition 2) and its results on dense and sparse networks all start from this formula.
On formalization: the paper proves Theorem 2, but no machine-checked version exists. The mission's statements also record two places where the written argument needs repair. The text attributes the almost-sure convergence of to the martingale convergence theorem, but is a face-value posterior and not a martingale under the corrupted signal law. The proof's step from small increments of to convergence of is also not valid as written. Both claims are true under Assumption 1, and a complete development supplies correct arguments. The supporting results — spectral radius below one for a substochastic matrix with leakage reachable from every row, and convergence of linear recursions with convergent input — are reusable beyond this paper.
Two steps resist the obvious arguments.
First, is a function of the drift of a random walk. Its limit exists only if the walk is transient or . For a targeted agent the walk's step law mixes the principal's message with organic news. For one boundary value of the step has mean zero, the walk is recurrent and oscillates forever. Assumption 1(i) excludes exactly that value. A proof must use it; a martingale argument does not apply.
Second, is substochastic but not strictly so: a DeGroot row sums to , which equals whenever . A row-sum bound alone gives , not . Strict inequality needs every DeGroot agent to reach, in the weighted graph, an agent that leaks weight — a Bayesian or a DeGroot agent with . This uses the interaction of Assumption 1 (ii), (iii) and (iv), with Bayesian agents' outgoing links playing no role in .
Agents are Fin n and the Bayesian set is a Finset. Time is discrete, and the history at time is the signals at times . The state space is a two-element inductive type. The signals are random variables on a probability space . Each agent's sequence is independent over time with the law above; signals of different agents may be dependent. This is deliberate: in the paper all targeted agents receive the same principal stream, so cross-agent independence would exclude the paper's own model. The principal's action is pure (), as §3.2 allows without loss of generality. The DeGroot initial belief can be any value in , and the conclusion holds for every such initial belief on one almost-sure event. "Spectral radius" is Mathlib's spectralRadius ℂ of the complexified matrix. is Mathlib's matrix inverse; no invertibility hypothesis is added, because Assumption 1 implies it. In the graph , a DeGroot agent's links are exactly its positive weights; Bayesian agents' links are free.
The personal experience is the explicit face-value posterior of the given signal process, and the conclusion of the goal includes its almost-sure convergence to the constants used in the limit. The goal therefore cannot be met by an abstract learning rule or a free limit vector.
A complete development needs:
Contributions of any of these, as standalone lemmas, are welcome.
Online marketplaces such as lodging, ride-hailing and freelancing platforms test changes to their product (a new ranking, a new fee display, a new photo layout) with randomized experiments. In a two-sided marketplace these experiments are subject to interference: treated and control units compete for the same scarce supply or demand, so the outcome of one unit depends on the treatment of others, and the stable-unit assumption behind the textbook difference-in-means estimator fails. The resulting bias can be as large as the effect being measured, and platforms routinely choose between randomizing customers (customer-side randomization, CR) and randomizing listings (listing-side randomization, LR) without a principled guide.
Johari, Li, Liskovich and Weintraub (arXiv:2002.05670, Management Science 2022) introduced a tractable model in which this question can be answered. Their analysis shows that which side to randomize depends on market balance, the ratio of the rate of demand to the rate at which supply is replenished. This mission formalizes the demand-constrained half of that answer.
There are finitely many listing types and customer types . Listings of type form a mass , with . Customers arrive at total rate , a share of them of type (). A state records the mass of available listings of each type, and lies in .
An arriving type- customer includes each available type- listing in its consideration set with probability , has utility for it and an outside option of value , and books by multinomial logit. In the mean-field limit the probability that it books a type- listing is
A booked type- listing stays occupied for an exponential time of rate , with and . A steady state is a state balancing the flows:
A two-sided randomization (TSR) design treats a fraction of customers and a fraction of listings. The intervention replaces by , both positive, only when a treated customer meets a treated listing. The experimental system is the same mean-field model on the types and , (0 = control, 1 = treatment), with , , and . The mass vector is written . At its steady state , the rate at which condition- customers book condition- listings is
The global treatment effect is . The naive estimators are
Fix every parameter except and , and consider sequences with (a demand-constrained market). Then for every
and for every and Lebesgue-almost every treatment utility in the positive orthant, there is such that along every such sequence
Theorem 3, together with its supply-constrained mirror (Theorem 4 of the paper, not part of this mission), is the paper's main structural finding. Each naive design is unbiased in one extreme of market balance and biased in the other. When demand is scarce, customers do not compete for listings, so randomizing customers creates no interference, while randomizing listings makes treated and control listings compete for the same customers. This finding motivates the paper's TSR designs, which interpolate between CR and LR according to market balance.
The result is proved in the paper; nothing here is open. To the best of the curators' knowledge, no part of it has a machine-checked proof. The mission produces a formal account of the mean-field model and its steady state, which other models of matching markets with MNL choice and occupancy can reuse. It also makes the informal "generically biased" claim precise: the paper argues it only by saying that the limit "in general" differs from the GTE.
The central step is Theorem 1. The steady-state equation is a nonlinear fixed point, and the objective whose minimizer it is fails to be convex in . Existence and uniqueness therefore need a change of variables under which becomes strictly convex and coercive, followed by a boundary argument. The limit statements then follow from a quantitative bound on and the continuity of the choice probability, but they must hold at boundary designs ( or ), where some types have zero mass.
The LR half carries a second difficulty. Showing that the LR estimator is biased for one parameter value is easy; the claim is that the bias vanishes only on a Lebesgue-null set of treatment utilities. That requires the zero set of a nonzero rational function on an open orthant to be null, a fact Mathlib does not state in ready form.
Everything lives in the namespace TwoSidedExp.DemandLimit. Types are Fintype; treatment conditions are Fin 2. A mean-field system MFSystem Γ Θ carries (eps) and . A Model adds , and Model.expt aC aL is the experimental system. and are arguments, and a sequence of systems is a pair of positive real sequences with .
Conventions the formalization commits to:
Real.log 0 = 0. In (10) the printed is read inside the sums, as in (30).Trivializing formalizations are ruled out explicitly. is never evaluated at instead of the steady state. GTE is built from the experimental system's and , not from a separate formula. The LR half is an almost-everywhere statement with a sequence-independent , not an existential.
Infrastructure that is reusable beyond this mission: strict convexity and coercivity of log-sum-exp-type objectives, and the Lebesgue-nullity of zero sets of nonzero polynomials on . Proofs of any milestone are welcome. So are alternative routes to Theorem 1, for example via a monotone fixed-point argument.
Distributionally robust optimization (DRO) guards a data-driven decision against misspecification of the model that generated the data. In its penalized form, the decision maker replaces the sample-average problem , where is the empirical distribution of the data , by
where is a -divergence and controls how far an adversary may move the distribution. Such models are used in operations research, statistics and machine learning (Ben-Tal et al. 2013; Lam 2016; Duchi and Namkoong 2019), and a practitioner must choose . Gotoh, Kim and Lim (arXiv:1711.06565, Operations Research 2021) study this calibration problem. Their first contribution, on which the rest of the paper builds, is an exact description of what the robust model penalizes for small : the worst-case loss of expected reward is, to first order, the variance of the reward divided by the curvature of the divergence. This mission formalizes that theorem (Theorem 2.2) together with its proof chain in Appendix F.
A decision is fixed throughout, so the data enter only through the reward vector with . The nominal distribution is a probability vector with every ; the empirical distribution of distinct data points is . Write
The divergence generator is a function satisfying Assumption 2.1: is closed (lower semicontinuous) and convex, for , for , and is twice continuously differentiable on a neighbourhood of with . Kullback–Leibler (), modified () and Burg () generators all qualify.
For , the worst-case measures of (2.7) are the minimizers, over probability vectors , of
and . The worst-case sensitivity (2.8) of the expected reward is
The proof uses the convex conjugate (F.5) and a Lagrange multiplier for the constraint .
For every satisfying Assumption 2.1, every with positive weights and every , worst-case measures exist for each , and for every choice of them
Theorem 2.2 identifies penalized DRO, for small , with a mean–variance trade-off: the robust objective is (by the expansion (2.6), which the paper cites) , and the theorem gives the derivative of the worst-case mean that underlies that expansion. The paper's calibration method (§§4–6) rests on this: since in-sample robustness acts by penalizing variance, is chosen by trading an out-of-sample reduction in variance against a loss in mean.
The result is proved in the paper; to the best of current searches it has no machine-checked proof. The mission produces a complete formal proof of Theorem 2.2 under the paper's own assumption, a formal treatment of the conjugate duality for penalized -divergence problems on finite supports, and corrected versions of three steps of the printed argument (see Formalization scope).
The theorem is a first-order expansion of an argmin, and the obvious route is to differentiate the optimality conditions at by the implicit function theorem. That step fails under Assumption 2.1: the system defining the multiplier involves evaluated at , and its partial derivative in at requires a third derivative of , which is not assumed. For the multiplier satisfies , so it is not differentiable at , although Theorem 2.2 still holds. A proof therefore has to extract the first-order behaviour of from continuity of at alone. Further work lies in showing that the minimizer is interior and unique for small when is only locally smooth, and in handling extended-real values of and .
ℝ → EReal satisfying Assumption21: lower semicontinuity, pointwise convexity on (with ), for , , for , finiteness and smoothness of the real part on an open interval around , and . Assumption 2.1 is the only hypothesis on : no third derivative, no finiteness on , and no separate (it follows from the assumption).EReal.toReal); every statement that differentiates also asserts or implies finiteness where it differentiates.Fin n. The weights are general, and ; the paper's empirical distribution is , and its variance is the special case. The paper's (2.4) also allows zero weights; these are excluded.stdSimplex. The goal asserts that minimizers exist for every and that the limit holds for every selection of minimizers; it is not a statement about an arbitrary function constrained by hypotheses, and the existence clause rules out a vacuous reading.EReal, LowerSemicontinuous, stdSimplex, deriv, ContDiffOn, HasDerivAt, Filter.Tendsto. A reusable by-product is the local theory of the convex conjugate of a convex function near a point of positive curvature. Contributions of proofs of any milestone are welcome.