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?
Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).
The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.
Time is discrete and counted backward: is the number of periods to go and period is the last. Each order must be delivered at most periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack means the order must leave now.
Shipping a package that must arrive within periods costs , the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on . In each period new orders arrive with probability .
With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack among pending orders. The state is therefore , or when nothing is pending. The cost-to-go functions and satisfy the recursion (2)–(3): for and ,
with and . Holding is infeasible at . Shipping is optimal at when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.
For every period there is an integer such that, for every slack ,
The threshold may depend on , and no formula for it is asserted.
Theorem 1 reduces the policy of a -period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.
The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for , and the case is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.
The natural first idea is to argue that the cost-to-go inherits convexity in from and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of and the slope of (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference can a priori be larger or smaller than , because the optimal shipping periods for slacks and may differ. The recursion couples two indices, period and slack, through the no-order value , and its boundary cases (, where shipping is forced, and , the last period) behave differently from the interior. The paper's own argument covers only ; the regime , in which the horizon ends before the most urgent order's deadline, is left to the reader.
valuePair F α d t returning . The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; stands for the smallest slack among pending orders. All objects are deterministic; enters only through (3).Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.Autonomous vehicles (AVs) can drive closer to one another than human drivers, because they react faster and can coordinate in platoons. Transport agencies and industry groups have therefore proposed reserving a designated lane for AVs on highways, so that AVs can exploit short headways without mixing with human-driven vehicles (HVs). Whether such a lane helps depends on a trade-off that is familiar from queueing theory: splitting a highway into two separate lanes loses the efficiency of pooled capacity, while a lane reserved for AVs moves faster when it is busy.
Mirzaeian, Cho and Scheller-Wolf (Management Science, 2021; manuscript SSRN 3278330) model a highway segment as a state-dependent loss queue and compare a no-AV benchmark with the designated-lane policy (the D policy). Their headline finding is that the D policy reduces mean travel time only when the highway is heavily loaded and AVs make up a large enough share of traffic. This mission formalizes that finding.
The queueing model is the state-dependent queue of Cheah and Smith (1994), developed for pedestrian flows, which Jain and Smith (1997) applied to vehicular traffic; its stationary law, display (12) below, is due to Cheah and Smith.
A highway segment has length and lanes, each holding at most vehicles. Vehicles arrive as a Poisson process of rate ; a vehicle that finds the segment full is turned away. When vehicles are on a segment of capacity , each travels at mean speed , for , with . This is the queue. Its stationary law is (display (12) of the paper)
its throughput is , and its mean travel time is, by Little's law, (display (13)).
The benchmark pools all lanes into one queue of capacity with speeds ; its mean travel time is . Under the D policy, a fraction of arrivals are AVs and must use the designated lane, so there are two independent queues: the AV queue (capacity , speeds , arrival rate ) and the HV queue (capacity , speeds , arrival rate ). The overall mean travel time is
The jam speeds , , are the speeds of full queues. The paper assumes throughout, and the AV lane is faster when full than the HV lanes, . The threshold is
For every with there is such that
The goal makes precise the paper's main policy conclusion: under heavy load a designated AV lane lowers mean travel time relative to the benchmark exactly when the AV share exceeds a threshold that depends only on the three jam speeds. Below the threshold, the loss of pooling dominates. This is the basis for the paper's caution against designating lanes for AVs while AV penetration is low, and the same heavy-traffic argument underlies its comparisons with the integrated policy (Propositions 2 and 3).
The printed Proposition 1(a) is not correct as stated, and the formal statement records the repair. Its heavy-load clause asserts a single valid for every ; the travel-time gap behaves like with affine and vanishing at , so no single threshold works for AV shares arbitrarily close to , and at the equivalence can fail for all . Its light-load clause (" for when is small") fails at whenever the AV lane is as fast as the benchmark at low occupancy and faster at higher occupancy, which includes the paper's calibrated model. The mission therefore poses the heavy-load clause pointwise in , excluding , which is what the paper's proof establishes. None of these results has a machine-checked proof; the queueing layer (the stationary law, travel time and their heavy-traffic limits) is new on the platform.
The heavy-traffic limits are the core. The obvious route, letting in the definition , gives the indeterminate form : the blocking probability and tends to the jam throughput. The limit has to be read off a rearranged expression, the closed form (16), whose leading terms in cancel to . Lemma 1 is a genuine monotonicity statement about a ratio of polynomials in whose coefficients depend on an arbitrary nonincreasing speed sequence; it cannot be checked degree by degree. The goal then needs strict separation of the two limits away from , together with an eventually-in- argument, and care at , where one of the two D-policy queues receives no traffic.
The queue is represented by its closed-form stationary law (12), exactly as in the paper; no continuous-time Markov chain is constructed. Speeds are arbitrary real sequences , read at ; the platooning model of §3.1.2 (a Markovian arrival process that generates the speeds) is out of scope, and Proposition 1 is stated in terms of the speeds only. "Decreasing" speeds are read as nonincreasing (AntitoneOn on ), and "increasing" in Lemma 1 as weakly increasing. Capacity is per lane. The arrival rate is real, and the limit is in . Lean's assigns at , where the throughput vanishes; Lemma 1 and (16) are therefore stated for , and the goal's is positive. At or the idle queue's junk value carries weight zero. The strict inequality (the proof writes ) keeps the threshold's denominator nonzero, and it is necessary for the equivalence. The goal is not trivialized by vacuous hypotheses: the instance , , , , satisfies all of them, with strictly inside . A statement that drops the exclusion , uses one for all , or feeds the full rate to both D-policy queues would not be this result.
A complete development needs finite sums and products, factorials, polynomial-ratio limits at infinity, and a monotonicity argument for ratios of power series truncations. The loss-queue layer (stationary law, throughput, travel time, its closed form, monotonicity and heavy-traffic limit) is reusable for any model, including the paper's integrated policy. Contributions to any milestone, and alternative proofs of Lemma 1, are welcome.
Many shared assets deteriorate unless someone pays to maintain them: a public infrastructure stock, a jointly used ecosystem, a joint venture's capital, a common research base. When several parties benefit from the same stock and each pays for its own contributions, every party is tempted to wait for the others to pay. Kwon (arXiv:1904.00500, published in Operations Research, 2022) models this as a two-player stochastic differential game in continuous time, in which each player may raise the stock at any rate, and studies the Markov perfect equilibria of the game.
The single-player version is a classical monotone follower problem of singular stochastic control (Alvarez 2001; Øksendal and Sulem 2005; Lon and Zervos 2011): the optimal policy reflects the stock upward at a threshold. In the game, a natural first guess is that free riding lowers that threshold, or that the players take turns reflecting. The paper shows instead that, in the symmetric game, there is an equilibrium in which both players contribute gradually, at a finite rate, below the same threshold as the single decision maker. The equilibrium is a continuous-state analogue of the mixed-strategy delay equilibrium of the war of attrition.
The stock lives in an interval ( or allowed) and satisfies
on a filtered probability space satisfying the usual conditions, where is a Wiener process, (the stock deteriorates) and . Player 's control is any adapted, nondecreasing, right-continuous process: its cumulative contribution. A control may jump, including at time . Player 's payoff from the initial stock is
where is an increasing, bounded-above flow profit, the unit cost and the discount rate. In the symmetric game both players have the same and .
The analysis uses:
Assumptions 1–3 of the paper require Lipschitz coefficients with linear growth, a uniform integrability condition on , integrability of , and boundary behaviour of and at and ; in particular increases below a point and decreases above it.
The single decision maker's value is
for a threshold and a coefficient that make twice continuously differentiable (Lemma 1). The candidate equilibrium rate is
If of (6) is Lipschitz on with linear growth, then the profile in which both players contribute at the regular rate is a Markov perfect equilibrium, and
The equilibrium is against all adapted deviations, from every initial state, with the opponent keeping its feedback rule .
Theorem 2 says that the free-rider problem in this game does not shift the threshold below which the stock is maintained; it changes how the stock is maintained, from instantaneous reflection by one party to gradual, rate-limited contribution by both. The equilibrium value equals the single decision maker's value, so the players lose nothing relative to a single owner who pays for everything, although each pays only part. This contrasts with the asymmetric case, where the paper's Theorem 3 rules out a regular-control equilibrium with smooth payoffs. The result is one of the few explicit equilibria of a nonzero-sum singular-control game with linear costs.
The paper's proofs are on paper only. A formalization requires machine-checked versions of a verification theorem for one-dimensional singular control (the optimality condition), of the analysis of the free-boundary point through the fundamental solutions, and of the passage from best response within a restricted class to best response among all adapted controls. The verification steps for a controlled diffusion with jumps, Itô's formula for semimartingales with a nondecreasing part, and the comparison with the uncontrolled process are reusable for other singular-control and monotone-follower problems on the platform.
The obvious route, Itô's formula applied to along an arbitrary deviation, requires the transversality limit and uniform integrability of the localised terms. is unbounded below when , and the deviation is arbitrary, so this needs the comparison of every controlled state with the uncontrolled process and Assumption 1(ii). The proof also passes through a best-response theorem for the restricted class (Theorem 1), whose conclusion is weaker than a Nash equilibrium; the upgrade to all of is a separate argument. Finally, the identification of uses the boundary behaviour of , and the scale density at the ends of , which Mathlib does not provide for general diffusions.
Time is . The probabilistic data (measure, filtration, Wiener process, the uncontrolled family , , ) form one structure, and the standing assumptions of §2.1 together with Assumptions 1–3 form one predicate, a hypothesis of every theorem. The Itô integral of the state equation is the published relation EthierKurtz.HasBrownianItoIntegral; Mathlib supplies Brownian motion, stopping times, uniform integrability and Stieltjes measures.
Conventions the formalization commits to:
The threshold and coefficient are not chosen by the formalization: the goal holds for every pair making twice continuously differentiable on , and smoothness at determines the pair. The rate is computed from through the generator, not supplied as a free function, and its nonnegativity is part of the conclusion. A payoff is never a Bochner integral of a non-integrable function, so no junk value can enter an equilibrium comparison.
Contributions welcome: proofs of the milestones, and reusable infrastructure for Itô's formula with nondecreasing càdlàg integrators, comparison theorems for one-dimensional SDEs, and the boundary classification of one-dimensional diffusions.
The apparel industry is a large source of carbon emissions, water use and landfill waste, and much of that footprint comes from garments being discarded early. Fast-fashion retailers such as Zara and H&M combine two operational choices: they offer a very large number of styles each season, and they replenish the styles that turn out to be popular through quick response, i.e. production during the selling season at a higher unit cost. Their garments are also widely reported to be of low quality, which shortens their useful life and reduces the chance of reuse.
X. Long and J. Nasiry, Sustainability in the Fast Fashion Industry (SSRN 3486502; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2021.1054), give an operational explanation of low quality: it is driven by the firm's incentive to offer variety. The paper's headline (abstract, and the first sentence of its conclusion) is that when variety is chosen by the firm, quality falls as consumers become more sensitive to fashion or as introducing new styles gets cheaper. This mission formalizes that result and the chain of propositions leading to it.
A firm sells one season of a fashion product. Before the season it chooses a number of styles (design cost ), a common quality , and an inventory per style produced at unit cost . Styles are points on a circle of unit circumference (Salop's circular city). During the season, a trend uniform on the circle and a market size are realised. All consumers buy the style closest to the trend at their valuation
where is the arc distance, is a base value, and and measure the sensitivity to quality and to fashion. Demand above is met by quick response at unit cost with ; unsold units of the other styles are wasted.
The paper shows that equally spaced styles are optimal (Lemma 1), computes the expected price and the expected quick-response volume , and arrives at the firm's problem (1):
An optimal solution is a feasible triple with the largest expected profit. The parameters satisfy and ; is any real number.
For admissible parameters, problem (1) has an optimal solution, and
where each comparison changes one parameter, keeps the others fixed, and holds between every optimal solution before the change and every optimal solution after it. Monotonicity is weak: on part of the parameter space the optimal quality does not move.
In attack order:
The result separates two channels by which fashion sensitivity could affect quality. For a fixed number of styles, the optimal quality does not depend on , or at all (p. 17). All of the effect therefore runs through variety: more styles mean more leftover inventory or more reliance on expensive quick response, and the firm cuts quality to lower the unit cost. Policy conclusions in the paper rest on this mechanism. The disposal-cost and production-tax analyses of §5 ask whether a regulator can reverse the quality decline, and the environmental-impact comparison (Corollary 3) compares fast fashion with a single-style firm.
The paper proves the result with Karush–Kuhn–Tucker conditions on a non-concave reduced problem, split into four regions of and several cases in . No machine-checked proof of any of its statements exists. A formal development would certify the region analysis, which the paper itself states with thresholds that are easy to mistype. It would also supply a reusable treatment of monotone comparative statics for every selection of a non-unique optimum. Two printed slips are already corrected in the statements: the expectation "" on p. 11 should read , and the optimal-inventory display on p. 14 needs .
The reduced profit is not concave in : on its second derivative changes sign, and the optimum can jump between , an interior critical point , and the region-III value . Differentiating an optimality condition, the implicit-function argument the paper uses for , says nothing about these jumps or about ties. The goal is stated for every optimal solution, including the parameter values where two values of are optimal, so a proof needs an argument valid across jumps.
Everything is real-valued. Parameters form a record with an admissibility predicate. Problem (1) is one explicit real function, and the feasible set is , , , with the number of styles a real number as in the paper's analysis. "Optimal" means a feasible maximiser over this set. "The optimal " is read as the -component of every optimal solution; "increases/decreases" are weak; parameter changes are strict and vary one record field ({ P with γ := γ₂ }). Ties at the thresholds of Proposition 3 are handled by asserting uniqueness of only off the thresholds. The circle is AddCircle (1 : ℝ), whose metric is the arc distance and whose Haar measure is the uniform probability; the uniform market size is an interval integral divided by . Lemma 1 is stated in the reduced form its proof uses: equal spacing minimises the expected nearest-style distance. The paper's standing assumption that the base value is high enough to make quick response always worth using does not enter (1) and is not a hypothesis.
The goal is a statement about every joint maximiser of the expected profit (1) over , , . It compares parameter values that differ in one coordinate only, and it asserts that an optimum exists. For a fixed number of styles the optimal quality does not depend on , or , so a formalization about the per- optimum would be trivially true; the content lies entirely in how the optimal variety responds.
A proof needs only real analysis: one-variable optimisation of quadratics, existence of a maximiser of a continuous coercive function, and an increasing-differences (Topkis-type) monotonicity argument. A proved abstract version of the latter is on the platform, Supermodularity.Monotonicity.argmax_mono_of_strictly_increasing_differences. Lemma 1 needs integration on AddCircle and a convexity inequality over arc lengths. Contributions of alternative proofs of Proposition 3, and of reusable lemmas on comparative statics of argmax sets, are welcome.
A two-sided platform (a ride-hailing service, a marketplace, a payment network) earns money only when its two sides transact, so its value depends on the stock of participants on both sides. A young platform has to decide not only how fast to grow but also which side to grow, and it does so through the prices it sets on each side. Whether to subsidize drivers or riders, sellers or buyers, is a recurring operational decision, and the economics literature on two-sided markets (Rochet and Tirole, 2003; Armstrong, 2006) studies it mostly in static models.
Lian and van Ryzin (SSRN 3310559, later published in Management Science, 2021, doi:10.1287/mnsc.2020.3832) pose the question dynamically: supply and demand stocks grow with the surplus each side receives and decay at their own attrition rates, and the platform chooses prices over time to maximize discounted profit. Their first main result, Theorem 1, says that the optimal mix of the two sides at any moment depends only on the current size of the market, and it describes exactly how that mix moves as the market grows. This mission formalizes Theorem 1 and the lemmas its proof rests on.
A supply stock and a demand stock generate transactions per unit time, where the output function is homogeneous of degree : for . The returns to scale are decreasing if and increasing if . Buyers value a transaction at , sellers incur cost . Supply and demand decay at attrition rates and grow with adoption coefficients ; the platform discounts at rate .
When prices are unconstrained, the two stocks reduce to one market size and a balance , the share of the size held by supply. With the output is , and the size evolves by
where is the platform's per-transaction margin. The platform maximizes over balance and margin paths (problem (13)). The net welfare rate is
The paper assumes (Assumptions 1–4) that is twice differentiable and positive on , nonnegative at and , strictly concave (), that has a unique zero , the output-maximizing balance, and, when , that .
In Lean the primitives are the fields of TwoSidedGrowth.Balance.Model (with ASCII names bs0 bd0 bs1 bd1 for the four 's), the assumptions are the structure Model.Standing, and h, out, G, kappa, IsBalance, Admissible, profit are the objects above.
Write . For every market size the optimal balance is
in the sense that exactly one balance satisfies (14); it is the unique maximizer of on ; and along any size path the balance path yields at least the discounted profit of every other admissible balance path on every finite horizon. Moreover, as grows from to , moves monotonically:
The balances and are the durability-maximizing balances: all of the market on the side that attrites more slowly.
Theorem 1 separates the two controls of the growth problem: the balance is chosen myopically from the current size, and only the margin, which determines how fast the size moves, remains a dynamic decision. Every later result of the paper (the stationary size of Theorem 2, the subsidy and growth policies of §4) analyses a one-dimensional problem in because of this reduction. The table also has a direct managerial reading: a small market with decreasing returns should be balanced for output, a large one for durability, and with increasing returns the order is reversed.
The result is proved in the paper, partly in prose ("the other three cases can be checked similarly"). No machine-checked version of it is known. The formal development adds a precise reading of (14) when is unbounded at the ends (as it is for the paper's own Cobb–Douglas example, where the printed claim that is bounded by and fails), explicit monotonicity and limit statements for all four cases, and a machine-checked version of the profit identity that underlies the reduction.
The identity of Lemma 5 is an integration by parts, and the argmax of a strictly concave function is unique. The work lies elsewhere. The first obstacle is that need not be bounded on , so has to be read as an extended inverse with three regimes, and the argmax characterization must handle the boundary cases where is monotone on and its maximum sits at an endpoint where has no derivative. The second is the monotonicity: the naive argument differentiates everywhere, but is constant at or on whole intervals of sizes when is bounded at an end, and it is not differentiable where it reaches the boundary; monotonicity has to be proved for the clamped function directly, and the derivative formula (34) only on the open set of interior balances, through the inverse function theorem. The limits require continuity of the extended inverse at and the divergence of at the other end of the size range.
TwoSidedGrowth.Balance; the single definition file Setting holds the model and all derived objects.IsBalance: an interior root of , or when on , or when on . It is not defined as an argmax of , and the profit of (13) is the integral of , not the right-hand side of Lemma 5; either shortcut would make the main conjuncts definitional and is ruled out.Personalized decisions in medicine, marketing and public policy are increasingly learned from observational data: records of who received which treatment and how it turned out. Standard policy-learning methods assume unconfoundedness, that treatment assignment depends only on observed covariates. When an unobserved factor influences both the treatment and the outcome, these methods can return a policy that is worse than the status quo, and nothing in the data reveals it.
Kallus and Zhou (arXiv:1805.08593, published in Management Science 2021 as Minimax-Optimal Policy Learning Under Unobserved Confounding) take the robust route. They fix a bound on how far the unobserved confounding may distort the propensity scores, in the marginal sensitivity model of Tan (2006), and learn the policy that minimizes the worst-case regret against a baseline policy over every distortion the model allows. The paper proves two guarantees for this policy: it never does worse than the baseline up to vanishing terms (Theorem 2), and it is asymptotically minimax-optimal (Corollary 7). This mission is about the second.
Data are iid triples : covariates , one of treatments , and a real outcome , read as a loss. The nominal propensity is . A policy assigns to each a probability vector over treatments; is a class of policies and a baseline.
Inverse propensity weights are unknown under confounding. The marginal sensitivity model with parameter confines them to the weight box
The set of such weight functions is , and its restriction to a sample of size is the box .
For weights , the Hájek regret of against is with
and is the same expression with replaced by the sample average . The worst-case regrets are
The learned policy minimizes over ; the population minimax regret is .
The complexity of is measured by its VC-major dimension (Definition 1): the largest such that some points have all subsets cut out by superlevel sets , , . The standing assumptions are bounded outcomes (Assumption 1), overlap with constant (Assumption 2), and VC-major dimension of at most (Assumption 3).
There is a constant depending only on such that, with probability at least ,
The result. Corollary 7 says that the confounding-robust policy loses at most against the best possible worst-case guarantee in its class. The worst-case regret cannot be identified from data. It is the regret the decision maker must budget for when the confounding is only known to lie within . With Theorem 2, it makes the procedure both safe and asymptotically optimal among safe procedures, for randomized and multi-treatment policy classes of finite VC-major dimension.
Formalizing it. The paper's proof of the dimension-only dependence of is incomplete. Its Proposition 5, which states that the monotone weight class has finite VC-major dimension under Assumption 3, is false as printed. A class of monotone policies on with VC-major dimension at most gives a that shatters arbitrarily large grids. The printed proof of Theorem 6 runs through Proposition 5 and Lemma 4, so Theorem 6 and Corollary 7 are believed true but are not established by the paper. A formal proof would settle the claim. None of the statements has a machine-checked proof.
The worst case over is a supremum over an essentially arbitrary bounded function class, which is far too large for a uniform law of large numbers. Proposition 3 reduces it to monotone transformations of the score . This is a linear-fractional program whose population version lives in a function space. The natural next step is to apply a uniform law over the pairs . That step needs a complexity bound on the composition in terms of the dimension of alone, and this is exactly where the printed argument fails. A different route is needed. One candidate exploits the Lipschitz dependence of the worst-case Hájek value on the scores. The Hájek ratios also need denominators bounded away from zero uniformly. The paper's decomposition (p. 42) uses , which holds for the true weights only.
All statements live in the namespace ConfoundRobust.Minimax, with one definitions file Setting.
𝒳 × Fin m × ℝ, with treatments 0-indexed as on the page. The population is a probability measure μ, and a sample is ω : Fin n → Obs 𝒳 m under Measure.pi. is .π : 𝒳 → Fin m → ℝ, with π x t , measurable and simplex-valued. The nominal propensity is a measurable version of , given by its defining integral identity, with .sSup/sInf; the weight sets are nonempty (they contain ) and the regrets are bounded, so these are true extrema. An empty treatment group gives a Hájek ratio .∀ v, ∃ K, ∀ (everything else). Letting depend on , , or would trivialize the bound and is ruled out.A complete development needs: linear-fractional optimization over function boxes; Dudley-type entropy bounds for VC-major and VC-hull classes; the Dvoretzky–Kiefer–Wolfowitz inequality with Massart's constant (posed separately on the platform as MassartDKW.Tight.corollary_1); and a uniform bound for Hájek ratios. The empirical-process pieces (VC-major classes, monotone classes) are reusable well beyond this mission. Contributions to any milestone, and alternative routes to Theorem 6 that avoid Proposition 5, are welcome.
Characterizing the state of an -qubit device is a basic task in quantum computing and simulation. Full quantum state tomography reconstructs completely, but it needs a number of measurements exponential in (Haah et al., 2017; O'Donnell–Wright, 2016). In practice one usually wants only a list of properties, such as the expectation values of observables (fidelities with target states, entanglement witnesses, local energies). Aaronson's shadow tomography (Aaronson, 2018) showed that such properties can be learned from a number of copies polylogarithmic in , but with collective measurements across many copies that are far beyond present hardware.
Huang, Kueng and Preskill (arXiv:2002.08953, Nature Physics 16, 2020) gave a procedure that uses only single-copy randomized measurements: rotate by a random unitary from a fixed ensemble, measure in the computational basis, and store the outcome classically. From these records, called classical shadows, a median-of-means estimator predicts all properties at once. Their Theorem 1 bounds the number of measurements by times a state-independent norm of the observables. The method has since become a standard tool for benchmarking and for estimating many observables in experiments.
Fix qubits. Computational-basis labels are bit strings , and operators are complex matrices. A state is a positive semidefinite matrix of trace one.
A measurement primitive (Definition 1) is a finite ensemble of unitaries drawn with probabilities . One snapshot of draws with probability , applies , and measures, obtaining with probability (S1). The primitive is tomographically complete if any two distinct states give different outcome probabilities for some and some of positive weight.
The measurement channel (S2) is the linear map
and the classical shadow of the outcome is (S3). For an observable the single-shadow prediction is . The shadow norm (S7) is
and is the traceless part of .
The median-of-means prediction (S12) takes independent snapshots, splits them into batches of , averages within each batch, and outputs the median of the batch means.
For Hermitian , and integers
the median-of-means predictions from independent classical shadows satisfy
The constants , and are the paper's own. Remark 1 of the paper says they are chosen for simplicity, not tightness.
Theorem 1 gives a sample complexity . It grows only logarithmically in the number of properties and does not depend on the dimension except through the shadow norm. For random global Clifford measurements the shadow norm is at most . For random single-qubit Pauli measurements it is at most for an observable acting on qubits (Propositions 1–3 of the paper). These instantiations are what make the protocol useful for fidelity estimation and for local observables. The theorem also separates two independent ingredients, a state-independent variance bound and a generic median-of-means concentration bound, and each is reusable.
The result is proved in the paper. As far as the platform's corpus shows, it has not been machine-checked. This mission produces a formal statement of the protocol and its guarantee, and its definitions (measurement channel, classical shadow, shadow norm) can be reused for the Clifford and Pauli instantiations and for the paper's quadratic-function estimator (Theorem 4).
The linear-algebra layer is elementary but has to be set up carefully. The channel must be shown invertible from completeness on states alone. Its inverse must be shown trace-preserving and self-adjoint, and the variance has to be rewritten as an expectation of squared diagonal entries.
The probabilistic layer is where the naive argument fails. Chebyshev's inequality on a single empirical mean gives a sample size proportional to , not . Applying Hoeffding's inequality to the number of failing batches gives exponent . That is weaker than , so it does not reach the stated constant . The bound needs the relative-entropy form of the Chernoff bound for a binomial tail, which Mathlib does not provide in this form. The median also has to be related to a count of deviating batch means without sign or tie errors.
Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ. States are the published WildeQIT.IsDensityOperator.WildeQIT.FinDist of weights and a family in Matrix.unitaryGroup. The paper's ensemble is general, but both of its examples are finite with uniform weights. "" in completeness means positive weight.Ring.inverse of it. Every statement using assumes tomographic completeness.Theorem 1 must not be restated about an abstract estimator with a variance bound; that is milestone 6. The goal is about the median of means of classical shadows of a concrete primitive, with the shadow norm of (S7). Tomographic completeness is satisfiable non-trivially: the three single-qubit Pauli bases form a complete primitive, so the goal's hypotheses are not vacuous.
Needed infrastructure: elementary facts about the trace pairing and diagonal entries of ; finite product measures, or direct finite-sum manipulations; Chebyshev's inequality; a binomial Chernoff bound in relative-entropy form; and order-statistic facts about the median. The binomial tail bound and the median-of-means lemma are independent of quantum information and reusable elsewhere. Contributions to any milestone are welcome. The Clifford and Pauli shadow-norm computations are natural follow-up work on top of these definitions.
Retailers that sell both through physical stores and online increasingly offer buy-online-pickup-at-store (BOPS): a customer reserves an item online against the store's inventory and collects it in the store. Whether this helps the retailer is not obvious. BOPS changes which customers draw on the store inventory, and therefore how much stock the store should carry and how often a visiting customer finds the item. Gao and Su (Management Science, 2017) modelled BOPS with customers who respond to store inventory availability and found that it need not be profitable for every product; Hu, Xu, Xue and Yang (Management Science 68(2), 2022; accepted manuscript SSRN 3214047) ask when it helps, through the inventory side. They identify two opposing effects: demand pooling, where BOPS moves online demand onto the store inventory, and demand depooling, where BOPS splits off customers who used to buy in the store. This mission formalizes their first effect, Proposition 3: in a stated region of costs, BOPS benefits the retailer.
A retailer owns one brick-and-mortar store and an online channel fulfilled from a distribution centre. On a probability space there are two customer segments with random market sizes: store-only customers, who buy only in the store, and omni-customers, who may buy in the store or online. The store sells at price with unit cost ; the online channel sells at with unit cost . A store visit costs a customer , waiting for an online delivery costs . The base surpluses are online and in the store, and Assumption (U) holds throughout.
The retailer chooses a store order quantity before demand is realized. A customer who visits the store finds the item with probability equal to the store's fill rate , where is the demand facing the store (Deneckere and Peck). Customers decide on the basis of a belief about the fill rate; the retailer orders on the basis of beliefs about the fractions of each segment that shop in the store.
A rational-expectations (RE) equilibrium is a profile in which customers' choices are optimal for the believed fill rate, the order quantity is optimal for the believed choices, and both beliefs are correct. When several exist, the paper selects the Pareto-dominant one. The optimal order quantities , (BASE, with only store-only customers, respectively both segments, in the store) and (BOPS, store-only customers in the store) define fill rates .
If
then Pareto-dominant RE equilibria exist under BASE and under BOPS, and at any such pair the retailer's expected profits satisfy
Proposition 3 is one half of the paper's comparison of BOPS with independent channels (Figure 3 of the paper): together with the depooling effect (Proposition 4) it partitions the cost region below the diagonal into areas where BOPS helps, hurts, or is neutral. It isolates a mechanism that does not appear in models with exogenous store demand: the fill rate, and hence customers' channel choices, respond to the inventory decision.
The paper's proof is short once the equilibria are characterized, but it is a proof in the paper's normal-demand model, where the statement does not hold (see below). The mission produces a corrected, machine-checked version: an explicit equilibrium model with rational expectations and Pareto selection, the characterization of the equilibria that the comparison needs, and the comparison itself. None of these results has a machine-checked proof.
The comparison of profits is easy once one knows which equilibrium each strategy selects; the work lies in the equilibrium analysis. Equilibria are fixed points of a map that couples a newsvendor problem with a discrete choice through the fill rate, and the fill rate is a ratio of expectations of the optimizer. Showing that a candidate profile is consistent, that the remaining profiles are not, and that the selected one Pareto-dominates every other, requires comparing optimal values of different newsvendor objectives and monotonicity of optimizers between them (Lemma 2), without closed forms. The obvious shortcut, reading off the equilibria from the paper's case tables, is not available: the tables are the theorems to be proved.
All objects live in the namespace OmniPool.BOPS; a single definitions file encodes the profits (2) and (4) term by term, the fill rates, the choice rules in utility form, and the RE equilibria of Definitions A1 and A2 as fixed points.
The goal asserts existence of Pareto-dominant equilibria under both strategies; without these conjuncts the universally quantified comparison could hold vacuously. Defining by the paper's region tables instead of through equilibria would make the goal a tautology and is ruled out.
Infrastructure needed: integrability of truncated demands, monotone comparative statics for maximizers of functions with increasing differences, and pointwise identities between the profit expressions. The equilibrium definitions are reusable for the paper's other results (Propositions 4 and 5) and for RE models of omnichannel retail. Proofs of the milestones, and formalizations of Propositions 1(i) and 2(ii)–(iii), are welcome.
Mean-variance analysis, the trade-off between the expected value and the variance of a portfolio's outcome, is the most widely used criterion for portfolio choice in practice. In continuous time it has two well-known defects when applied to terminal wealth: the criterion is time-inconsistent (a strategy that is optimal today is no longer optimal tomorrow), and the resulting equilibrium strategies of Basak and Chabakauri (2010) and Björk, Murgoci and Zhou (2014) prescribe a dollar amount in the stock that does not scale with wealth, which is at odds with how investors and advisers think in terms of portfolio fractions.
Dai, Jin, Kou and Xu apply the mean-variance criterion to the log-return of the portfolio instead of to wealth. They show that, in the classical complete market with constant coefficients, the resulting equilibrium strategy is a constant fraction of wealth, that it coincides with the classical optimal strategy of Merton (1969) for a CRRA investor with relative risk aversion , and that the investor's preference parameter is in one-to-one correspondence with a target annual return. The last fact is what the paper uses to elicit from an investor's stated target return.
A bond pays the constant interest rate . One stock has price with constant drift , volatility , and a standard Brownian motion on a probability space. An investor with horizon holds the fraction of wealth in the stock. A feedback strategy is a function of time and current log-wealth . The log-wealth then solves the stochastic differential equation (6)
For a time and a log-wealth , the investor evaluates a strategy through the reward function
the mean minus times the variance of terminal log-wealth for the process started at . Here is a constant (Assumption A). A strategy is admissible if .
Because is time-inconsistent, optimality is replaced by an equilibrium, following Björk, Khapko and Murgoci (2017). For and , the perturbation holds the constant fraction on and follows afterwards. An admissible is an equilibrium strategy (Definition 1) if, at every , every and every ,
With the market price of risk, the mission's two named quantities are
In Lean these are piHat M and aHat M for a market M : Market with fields μ r σ γ T; the SDE is IsLogReturn, admissibility Admissible, the reward J, the perturbation spike and Definition 1 IsEquilibrium.
A supporting item (not a milestone) states the reward of an admissible deterministic policy, (p. O–10); another states that and all its perturbations are admissible.
Part (i) shows that the dynamic mean-variance criterion on log-returns and CRRA expected utility of terminal wealth share the same optimal strategy in a complete market, although the first is time-inconsistent and the second is not. Part (ii) gives a closed-form, strictly increasing link between the target annual return and , which is the basis of the paper's procedure for eliciting the risk parameter (Corollary 1) and of its comparisons with terminal-wealth mean-variance strategies.
The result is proved on paper; nothing in it has a machine-checked proof. Formalizing it requires a working account of the Itô integral of deterministic integrands against Brownian motion (Gaussianity of the integral, its mean and variance, and uniqueness of solutions of an SDE with deterministic coefficients) in the form of the published step-sum relation EthierKurtz.HasBrownianItoIntegral. That account is reusable by any mission that computes moments of linear SDEs.
The paper's proof is three displays long because it takes the moment formulas for granted. Mathlib has Brownian motion (IsBrownianReal) but no Itô integral, no Itô isometry and no existence theory for SDEs, so each of the following is real work:
The equilibrium inequality itself is pointwise algebra once the reward is known.
EthierKurtz.HasBrownianItoIntegral, in elapsed time from , with the integrand set to after the horizon.Classical.epsilon); under admissibility the choice is immaterial.Market.Standing. The coordinates of are assumed measurable.Trivializing encodings are ruled out: is defined from the SDE and never by the closed form of Appendix C.2, and the goal's conclusion (not its hypotheses) asserts admissibility of and of every perturbation, so the equilibrium claim cannot hold vacuously. The moment milestone concludes , because Lean's integral and variance are on non-integrable inputs.
Welcome contributions: the Gaussian law of for deterministic under the step-sum relation; existence and uniqueness for (6) with deterministic coefficients; and the algebraic milestones, which are independent of the stochastic layer.
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.
NLTS Hamiltonians from good quantum codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix positive clustering constants , a bound on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant bounding the total number of checks by . There exist and an integer , uniform over the code, state, energy density and preparing circuit, with the following property.
For , let and be check matrices with , sparsity at most , and . Put and , and assume the CSS condition . Write for the encoded dimension, and assume . Assume Property 1: for every and every , implies or , and the same implication holds with interchanged. Here , and is Hamming weight. Define the unnormalized check Hamiltonian , counting all supplied rows.
Define
The corrected permitted cutoff is
For every density matrix and every ,
for every preparing circuit . A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on qubits, for any , starts in , and has reduced output on the first qubits after discarding the other qubits. Depth is its number of layers; is the natural logarithm.
Moreover, for every fixed , there exist and , uniform over all code instances, such that whenever , and , one has
Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at already implies linear distance.
This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.
Source correction. The paper prints only . Its proof uses Property 1 at with , so we also require . This is exactly the missing domain condition; it is automatic if . No normalization is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.
Correction to the printed source.
Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.
Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.
Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.
Fix positive clustering constants , a bound on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant bounding the total number of checks by . There exist and an integer , uniform over the code, state, energy density and preparing circuit, with the following property.
For , let and be check matrices with , sparsity at most , and . Put and , and assume the CSS condition . Write for the encoded dimension, and assume . Assume Property 1: for every and every , implies or , and the same implication holds with interchanged. Here , and is Hamming weight. Define the unnormalized check Hamiltonian , counting all supplied rows.
Define
The corrected permitted cutoff is
For every density matrix and every ,
for every preparing circuit . A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on qubits, for any , starts in , and has reduced output on the first qubits after discarding the other qubits. Depth is its number of layers; is the natural logarithm.
Moreover, for every fixed , there exist and , uniform over all code instances, such that whenever , and , one has
Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at already implies linear distance.
This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.
Source correction. The paper prints only . Its proof uses Property 1 at with , so we also require . This is exactly the missing domain condition; it is automatic if . No normalization is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.
Correction to the printed source.
Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.
Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.
Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.
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.
There is a deterministically explicit family of binary CSS check descriptions on qubits, and constants , a locality bound , and a threshold , all independent of . Explicit means that a deterministic polynomial-time function on unary outputs the actual row counts and both binary check matrices. For every , both check matrices have row and column weights at most , their total row count satisfies , and their associated projector terms or act on at most qubits, commute, and annihilate a common unit vector. Let be this unnormalized Hamiltonian. Every circuit of parallel one- and two-qubit unitaries on disjoint wires, starting from zero qubits and allowing arbitrary clean ancillas and discarded qubits, has an output density operator satisfying, for ,
This is the existence of an NLTS Hamiltonian family. Quantifying over every preparation circuit gives the lower bound for mixed as well as pure low-energy states.
Formalization Note The deterministic interpretation of explicit and the CSS witness implementation are recorded for independent moderation; the theorem does not assume an NLTS guarantee on its family.
Let be a binary CSS check presentation with , and let be any density operator with , where and is the sum of the actual check projectors. Write for its standard- and product-Hadamard-basis distributions and for the words violating at most a fraction of the actual checks on side . For every ,
If , both and have probability one. If , choosing gives both masses at least .
These bounds place low-energy measurement outcomes in the approximate classical codes. The energy identity and probability bounds are conclusions of the source argument, not hypotheses of the formal statement.
Let and be a binary CSS pair satisfying Property 1 with positive constants . Assume , , and . On define when , with the corresponding definition on modulo . Here . For either basis this is an equivalence relation. Its distinct computed classes are nonempty, pairwise disjoint, and cover the corresponding approximate code. Distinct classes satisfy
This constructs the separated clusters needed for the depth argument.
Formalization Note The strict domain follows Property 1 on page 2; the page-4 prose writes a non-strict endpoint. The classes are computed from the relation rather than supplied with a separation guarantee.
Correction to the printed source.
Printed: Page 4 says 'assuming 2 epsilon1 <= delta0', but Property 1 on page 2 is stated only for delta < delta0.
Corrected: Use 0 <= epsilon1 and the strict inequality 2 epsilon1 < delta0 in the clustering regime.
Reason: The proof invokes Property 1 at delta = 2 epsilon1; the strict domain is necessary. This is a standing-domain clarification pending independent moderation.
Consider a binary CSS presentation with and logical dimension , satisfying Property 1 with . Let be any density operator. Assume , , , and
For the computed clusters in the preceding result, either every standard-basis cluster has -mass strictly less than , or every Hadamard-basis cluster has -mass strictly less than .
This uncertainty consequence selects a basis in which no single cluster captures almost all probability. It requires no low-energy hypothesis once the clusters are defined.
Formalization Note The subtraction takes place in the reals. The positive- reading comes from the section's positive-rate setting and is flagged for independent moderation.
Correction to the printed source.
Printed: The displayed finite lemma does not explicitly say k>=1, while Section 2 is introduced for constant-rate code families.
Corrected: State the finite lemma for k>=1 and n,mx,mz>0, keeping ((k-1)/(4n))^2 with real subtraction.
Reason: The proof uses a positive logical dimension; at k=0 the zero-radius clusters can concentrate in both bases. The finite positive-rate reading requires independent moderation.
Let be any -qubit density operator, and let be its standard- and product-Hadamard-basis measurement distributions. For all sets ,
This bounds concentration in conjugate bases and applies to mixed states. No positive-mass hypothesis on is required; empty sets and are allowed.
Let a binary CSS presentation on qubits satisfy Property 1 with , and assume , , and . Fix either basis and any density operator . Suppose its measurement distribution gives the approximate-code set mass at least , while each computed class has mass less than . Then there are disjoint subcollections of the computed classes whose unions are disjoint and satisfy
This extracts two positive-mass separated sets in whichever basis Lemma 2 selects. Both probability constants and the cross-union separation are retained.
Let be a circuit of depth consisting of layers of disjoint one- and two-qubit unitaries, starting in the all-zero product state. Allow any number of clean ancillas and measure only its output qubits in the standard basis, giving distribution . Let , and suppose . For any such that every has Hamming distance at least ,
For positive set distance this is equivalently .
This is the quantitative circuit-depth obstruction for well-spread output distributions. The exponential formulation also covers overlapping sets without taking the logarithm of zero; the original circuit's workspace is unrestricted.
Let and . Let and . Suppose every with satisfies . Then
This transfers small-set expansion to the clustering dichotomy. Both the size cutoff and syndrome cutoff use the number of columns , even for rectangular matrices.
Formalization Note Positivity is taken from the proof and the paragraph immediately following Lemma 8; the unsupported zero- extension is excluded.
Correction to the printed source.
Printed: The displayed Lemma 8 omits its parameter domain; its proof uses delta>0 and mu>0 and the following paragraph takes mu<nu.
Corrected: State Lemma 8 on the meaningful positive regime delta>0 and 0<mu<nu, as pinned by the plan and proof.
Reason: For delta=0, an expansion hypothesis with beta=0 supplies no information and the claimed nontrivial dichotomy can fail. Independent moderation must confirm the intended domain.
Let be a family of binary CSS check presentations. Fix positive and . For all , suppose . For every , define as the words in of minimum Hamming weight within their coset modulo , and define analogously modulo . Assume is -expanding on and is -expanding on . Then there are constants , independent of , such that for all and ,
and the same dichotomy holds on the side modulo .
This derives Property 1 from uniform expansion of minimal representatives, without assuming the desired dichotomy. The check-density factors converting to a threshold relative to are retained.
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.
Classical statistical mechanics describes a particle by a probability density on phase space; quantum mechanics replaces this by a wavefunction, and the uncertainty principle forbids any honest probability interpretation of simultaneous position and momentum. In 1932, Eugene Wigner introduced the transform that has become the standard way of placing quantum states on classical phase space anyway: a quasiprobability distribution , defined by an explicit integral formula, whose marginals reproduce the Born position and momentum distributions of the wavefunction (Wigner 1932). Unlike a probability density, generally takes negative values, and this negativity is the standard marker of genuinely quantum behavior — of interference — in quantum optics, quantum information, and the study of the quantum-to-classical transition.
The central question about the probabilistic character of is: which quantum states have an everywhere nonnegative Wigner function? Hudson's theorem (1974) gives the complete answer in one dimension: only Gaussian wave packets (Hudson 1974). This mission formalizes the definition, the basic properties, and the positivity characterization of the Wigner function, following the source text, the Wikipedia article Wigner quasiprobability distribution (oldid 1376057304).
Timeline of the key results:
A wavefunction is a function , and denotes the reduced Planck constant. The Wigner function of at the phase-space point is
a Lebesgue (Bochner) integral over . The Lean development factors this into three definitions mirroring the formula: the integrand (Wigner.wignerIntegrand), the integral (Wigner.wignerIntegral), and the Wigner function itself (Wigner.wigner), defined as the real part of the integral divided by ; that the discarded imaginary part vanishes is itself milestone 1. The Fock states of the harmonic oscillator enter through the physicists' Hermite polynomials and the ordinary Laguerre polynomials , defined by their standard three-term recurrences, and the normalized -th Hermite function
This is exactly the source's statement of Hudson's theorem; nothing is left unfixed. The mission is complete when the goal is proved.
The milestone list is the source's property list, ordered as the attack path: (1) reality of the defining integral; (2) the position marginal ; (3) the total integral ; (4) Groenewold's closed formula for the Fock states; (5) a concrete negativity witness, the first excited Fock state at the origin; (6) the pointwise bound ; (7) the converse of Hudson's theorem, that Gaussian pure states have nonnegative Wigner function.
The result itself. Hudson's theorem draws the exact boundary between the classical and the quantum in phase space: Gaussian states — coherent and squeezed states — are precisely the pure states that can be described by an honest phase-space probability density. This is used in quantum optics as a nonclassicality criterion, in tomography and state-reconstruction theory, and in the study of the quantum-to-classical transition: negativity of is shielded by the uncertainty principle (negative regions cannot extend beyond a few ) and disappears in the classical limit, as the source emphasizes.
What formalizing it adds. The Wigner transform and this circle of ideas are absent from current Mathlib, so the mission builds the foundations itself: the integral transform and its basic identities (reality, marginals, normalization, boundedness), the Hermite/Laguerre recurrences and Groenewold's Fock-state formula, and finally Hudson's theorem with its converse. All of these are reusable well beyond the mission — for quantum optics, for the Wigner–Ville time–frequency distribution used in signal analysis, and for the wider phase-space formulation of quantum mechanics (Moyal brackets, star products). These are known results: this is formalization of known mathematics, not new mathematics, and no machine-checked proof of Hudson's theorem exists in Mathlib today.
The naive approach to Hudson's theorem is doomed from the start, and solvers should know it: since the Husimi function (a Gaussian smoothing of ) is positive for every quantum state, no smoothing or positivity-of-convolution argument can extract any information from . The known route (Soto–Claverie) is: everywhere forces the Husimi function strictly positive everywhere; the Husimi function is the squared modulus of the Segal–Bargmann transform of , so is a zero-free entire function; hence for some entire , and square-integrability of against a Gaussian measure forces to have at most quadratic growth, hence to be a quadratic polynomial; inverting the Segal–Bargmann transform then exhibits as a Gaussian. The hard Lean steps are the growth-to-polynomial (Liouville-type) step, the inversion of the transform, and, for the milestone properties, the Fubini and Fourier-inversion machinery. Mathlib contains the raw harmonic analysis (Fourier inversion for Schwartz functions) but none of the assembled phase-space layer.
Infrastructure contributed and reusable beyond this mission: hermiteP, laguerreL, fockState, wignerIntegrand, wignerIntegral, wigner. Welcome additional contributions: the momentum marginal, the state-overlap formula (Property 6), Galilei covariance (Property 4), and harmonic-oscillator time evolution, as further theorems in the same namespace.
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.
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.