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?
Retail chains increasingly let a customer who visits one store buy a product that only another store carries, delivered from that store or picked up later. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) study how a seller operating several stores should choose assortments when customers can substitute across stores at a utility cost, and compare two ways of presenting the other stores' products: simultaneous recommendation (SMR), where they are shown together with the visited store's assortment, and sequential recommendation (SQR), where they are shown only after the customer declines everything in the visited store.
For fixed prices, the paper shows that under SMR the best a chain can do is to offer the single-store optimal assortment everywhere (its Theorem 1). Section 8 asks whether this survives when the seller also sets prices, store by store. This mission formalizes the answer, Theorem 6: under SMR with joint pricing, offering every product in every store at the classical single-store constant adjusted markup prices is optimal. It also formalizes the paper's Proposition 9, which transfers this solution to SQR with a factor-½ revenue guarantee.
The single-store ingredient is older. For the multinomial logit (MNL) model with product-specific price sensitivities, the optimal prices share a common markup adjusted by the reciprocal sensitivity; this goes back to work on MNL multi-product pricing such as Li and Huh (2011) and is stated in this form by Wang (2012), whom the paper cites.
There are stores and products . A fraction of customers visits store , with . The seller chooses an assortment profile with , writes , and chooses real prices , the price of product in store ; production costs are zero.
A customer visiting store who buys product in store at that store's price has utility plus an independent standard Gumbel term, where is the intrinsic utility, the price sensitivity, and the utility discount for buying from another store, with . Write . For , the customer buys from a store that offers and maximizes over the stores offering ; then and . The no-purchase option has weight .
The SMR joint problem (13) maximizes
and the SQR joint problem (15) maximizes
The single-store problem (14) maximizes over and real . Finally is the unique solution of
No uniqueness is claimed.
Theorem 6 says that, under simultaneous recommendation, cross-store substitution creates no value that a coordinated price-and-assortment policy can extract: the multistore problem decouples into independent single-store pricing problems, each solved by offering everything at a constant adjusted markup. Together with Theorem 1 it places SMR as a clean benchmark against which SQR is compared, and Proposition 9 turns the benchmark into a guaranteed policy for SQR, where the joint problem has no known closed-form solution.
None of these results has a machine-checked proof. The mission's main new formal content is the single-store MNL pricing theorem with heterogeneous price sensitivities (milestone 2), which is cited, not proved, in the paper and is not on the platform; it is reusable for any MNL pricing model. Formalizing the store-wise reduction also makes explicit what the printed argument leaves implicit: the bound holds for every tie-breaking in the best-store rule, and for arbitrary real prices.
The multistore objective (13) is not a sum of independent store problems: store 's prices enter store 's revenue through and , and the selection is itself an that changes with the prices, so the objective is discontinuous in . Direct first-order analysis of (13) is therefore not available. The single-store problem (14) is not concave in the prices either, so its optimum cannot be read off from a stationarity condition alone: one needs a global bound valid for every real price vector and every assortment, including negative prices and empty assortments.
Stores are Fin m, products Fin n (the paper's product is index ), assortments Finset (Fin n), prices real-valued functions. is the finite union of the . The best-store rule is a function Fin m → Fin n → Fin m constrained by a predicate (it must offer and maximize the customer's utility among the stores offering ); every statement holds for every such , and the right-hand side at the full profile, where , does not depend on its rule. enters as a hypothesis "θ solves the markup equation", never as a chosen term; its existence and uniqueness is milestone 1.
Standing assumptions carried as explicit hypotheses: , , and (the page's ), , . Prices range over all of . Optimality is a universal upper bound over all profiles, prices and tie-breaking rules, never a supremum or an . Proposition 9's "optimal solution to problem (13)" is the solution constructed in Theorem 6.
The choice model (13)–(15) is taken as given; the derivation of the MNL probabilities from Gumbel utilities is not formalized. A formalization in which the selection is unconstrained, in which uses store 's price sensitivity instead of the customer's, or in which the optimum is a supremum of a possibly unbounded set would change the theorem and is ruled out by the definitions.
A complete development needs only Mathlib's real analysis (exponential, logarithm, finite sums); no new library is required. The single-store pricing optimum (milestone 2) is reusable for any MNL pricing model, and contributions of a general MNL pricing library are welcome.
A retailer with several physical stores often carries a different selection in each one. A customer who walks into a store and finds nothing she likes may still buy a product stocked elsewhere in the chain, paying in delivery cost or waiting time for it. Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing those other products. Under simultaneous recommendation (SMR) the customer sees the store's own assortment and the rest of the chain's products at once. Under sequential recommendation (SQR) she first sees only the store's assortment and is shown the other stores' products only after declining all of them.
The paper shows that sequential recommendation earns more than simultaneous recommendation, but that choosing the best SQR assortments is NP-hard. A natural first heuristic ignores the cross-store interaction: each store simply carries the assortment that would be optimal if it were alone. This mission formalizes the paper's guarantee for that heuristic: it earns at least half the optimal sequential revenue, and half is the best possible constant. The guarantee is proved in the heterogeneous case of the paper's §7.1, where a product may be valued differently in different stores (a flagship store downtown and an outlet store, for example).
There are stores and products. A fraction of the customers first visits store , with . Product earns revenue , and the products are numbered so that . In store , product has attraction value , where is its mean utility; not buying has attraction value . A customer who first visits store but buys product from store suffers a utility discount , with .
A decision is a profile of assortments ; write . A product reaches a store- customer through the cheapest store that offers it, with discount . Under the multinomial logit model with sequential recommendation, a customer who first visits store buys product with probability
and the seller's expected revenue is
Its maximum over all profiles is .
The single-store problem of store is
An assortment is revenue-ordered if it is for some . Some revenue-ordered assortment is optimal for the single-store problem; denotes the smallest such one. The heuristic offers in store for every , and its revenue is , cross-selling between stores included.
and the factor is tight: for every there is an instance with two stores and two products on which .
The guarantee says that the simplest decentralized policy, in which every store optimizes as if alone, cannot lose more than half of what the best sequential recommendation earns, whatever the store-specific valuations and the cross-store discounts. Read from the other side, the same bound with its tight instance says that sequential cross-selling can at most double the revenue of operating the stores separately, and that a doubling is approached. Since the exact SQR problem is NP-hard (the paper's Proposition 3), a constant-factor guarantee for a policy computable store by store is the kind of statement a practitioner can act on; the paper's numerical study (its Appendix G) finds the heuristic much closer to optimal on synthetic data than the worst case.
Proposition 7 is proved in the paper; nothing in it has been machine-checked. The mission formalizes the model, the proposition with both parts, and the three steps of its proof. Lemma D.1, the monotonicity of the optimal MNL revenue in the attraction values, is a standard fact of assortment optimization that is stated here for a single MNL model and is reusable beyond this mission.
The heuristic profile and the optimal profile are unrelated: the optimal one may stock in store products that store 's own optimum omits, precisely to sell them to other stores' customers in the second stage. A comparison store by store therefore fails, because the optimum's revenue in store depends on every other store's assortment through and the discounts . The second-stage revenue is a product of two MNL fractions over different assortments with discounted attraction values, and it has to be bounded by the single-store optimum with undiscounted values; this is where Lemma D.1 is needed, and the lemma itself does not follow from comparing a fixed assortment, since the optimal assortment changes with the attraction values. For the tightness part, the answer depends on the tie rule that defines : in the instance, store 2 has two optimal single-store assortments, and only the smallest one makes the bound tight.
Lean 4 with Mathlib. Products are Fin n (the paper's product is index ) and stores are Fin m; assortments are Finset (Fin n) and profiles are Fin m → Finset (Fin n). Attraction values are the primitive data, not utilities. The discount factor is the largest over the offering stores, and when no store offers (the paper's ). The single-store revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1 S. The model is the choice probabilities (10) and the objective (SQR-heter), taken as given; the paper's derivation of (10) from Gumbel utilities is not formalized.
The standing assumptions , , , , and are explicit hypotheses of every theorem. One hypothesis is pinned beyond the page: . The paper's revenues are prices and its proof drops a second-stage revenue term that is nonnegative only for nonnegative revenues, but the sign is never stated. The paper's tightness claim ("an instance where the equality holds") is realized only in the limit , so the goal states it in the form "for every , some instance has ".
"Optimal" means a maximizer over all assortments or profiles, ties allowed, and is never formed as a term: the bound is stated as for every profile . is a predicate (revenue-ordered, optimal, and of least cardinality among the revenue-ordered optima). An encoding in which can never exist would make the bound vacuous, so the tightness part asserts that exists on its instance. The tightness part also must use the paper's tie rule, not an arbitrary single-store optimum, since with the other optimum the instance is not tight.
Welcome contributions: proofs of Lemma D.1 and of the two halves of the bound, the exact evaluation of the tightness instance, and a general Lean library for single-store MNL assortment optimization (existence of revenue-ordered optima, monotonicity in attraction values) that the other missions of this series can reuse.
Lambda Value-at-Risk (VaR), introduced by Frittelli, Maggis and Peri (Mathematical Finance 24(3), 2014), generalizes the Value-at-Risk used in banking and insurance regulation: instead of one fixed confidence level, the level may depend on the size of the loss. It has since been studied for its properties, representation and characterization (Bellini and Peri, SIAM J. Financial Math. 13(1), 2022; Han et al. 2025; see the references of arXiv:2511.00717v1).
Regulators and risk managers rarely know the loss distribution exactly. A standard way to account for this ambiguity is to evaluate the risk measure under every model in a neighbourhood of a reference model and report the worst case. Neighbourhoods defined by a -divergence (Kullback–Leibler, chi-squared, -divergences) are the most common choice in distributionally robust optimization (Ben-Tal et al. 2013). P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv:2511.00717v1 (2025), define VaR with respect to a capacity. They show that for increasing the worst case over a -divergence ball is again a VaR, under an explicitly distorted reference probability. This mission formalizes that result.
Let be a measurable space. A capacity is a set function that is increasing () with and ; every probability measure is one. Let be the set of increasing functions . For a capacity and a random variable ,
with and . A constant gives the Choquet quantile . For a class of capacities, and are its setwise envelopes; for a class of probability measures they are written and .
Fix a probability measure and a convex with and . For a probability measure , , and for the -divergence ball is . The distortion is , and
For , , and every random variable ,
If moreover is finite, strictly convex and , then
The theorem reduces a supremum over an infinite-dimensional set of models to a single VaR under the reference model with a transformed level function . Robust VaR therefore inherits the computational and statistical tools available for VaR, and the worst-case VaR at level is the ordinary VaR at the explicit level . The limit statement shows an asymmetry: as the ambiguity vanishes, the robust value converges to the upper version , not to ; the two differ when the distribution function of has a flat piece where it meets .
The result is proved in the paper (2025) and, to our knowledge, nothing of it is machine-checked. The platform has no capacity, no Choquet quantile, no VaR, and no -divergence over general (non-discrete) probability spaces; the mission supplies all of these, and the formula for the upper probability of a -divergence ball (Proposition 5) is a reusable fact about divergence balls in its own right.
Proposition 2 is an order-theoretic exchange of a supremum with an infimum; it fails for decreasing (Example 1 of the paper), so monotonicity of must be used at the right place, and the values have to be handled. Proposition 5 asks for the exact value of a supremum over an infinite-dimensional ball of measures, for a that may take the value and may be negative; the upper bound must hold for every density in the ball, not only for the simple ones, and the integrability conventions of matter. The second part of Proposition 5 is real analysis of the perspective function , and continuity of at the endpoints and does not follow from continuity of alone. In the limit the natural guess is wrong: the limit is , so any argument that treats the robust value as a perturbation of fails at flat pieces of the distribution function.
All definitions live in the namespace LambdaVaRAmb.Robust. A random variable is a measurable function ; statements quantify over all of them, which covers every domain the paper allows. Set functions are Set Ω → ℝ and the capacity axioms are imposed on measurable sets. VaR, VaR, the suprema over the ball and the limits as are taken in EReal, so are genuine values. is ℝ → EReal (only its values on matter); convexity uses . is the integral of the positive part of minus that of the negative part; members of the ball are probability measures. is defined as , which is the inverse of on under the hypotheses where the paper uses it.
Implicit hypotheses made explicit: the classes and in Proposition 2 and Corollary 1 are nonempty; "" in the second parts is the hypothesis that is finite on ; " being the solution" is posed as existence and uniqueness.
The trivializing readings are ruled out: suprema over the ball and VaR values are never real sSup/sInf (which would collapse to on empty or unbounded sets); the envelopes are real suprema only over nonempty classes of values in ; the ball always contains , so it is not empty; is the paper's supremum, not a closed form for a particular .
Needed infrastructure, all reusable beyond this mission: capacities and Choquet-type quantiles; -divergences for general measures via Radon–Nikodym derivatives; conditional Jensen for extended-valued convex functions; perspective functions. Contributions of any of these, and proofs of the milestones in any order, are welcome.
Small third-party sellers on e-commerce marketplaces (Amazon, JD.com, Alibaba) typically have little capital and limited credit history, so they finance procurement through short-term credit. The traditional source is trade credit: the supplier ships the goods and is paid after the sales. Since about 2011 the platforms themselves lend to their sellers (the Amazon Lending Program, Ant Group's micro-loans, JD Small Loan), a form of finance called platform financing. The usual argument for platform loans is that platforms have cheap capital and rich data. Huang, Lai, Wang and Xiao (SSRN 4014045; published in Management Science, 2024, doi:10.1287/mnsc.2022.00201) remove both advantages: supplier and platform have the same capital cost and the same information. They ask whether a platform loan can still help the seller and the supplier, and at which interest rates.
The paper builds on the literature comparing supply-chain finance with bank finance, for example Buzacott and Zhang (2004) on asset-based financing and Kouvelis and Zhao (2012) on supplier versus bank financing of a newsvendor. The new feature is a third lender, the platform, which also collects a share of the revenue.
A supplier produces at unit cost . A seller with no capital procures units and sells all of them on a platform at the market-clearing price . The market size is uniform on , where measures uncertainty. The platform keeps the share of revenue, and the seller receives . Supplier and platform both have capital cost equal to the risk-free rate . The paper assumes , so selling is profitable in expectation, and that the smallest market size keeps the price positive.
The seller has limited liability: if her revenue falls short of what she owes, she hands over all of it. If she owes per unit, her expected profit is
Each scheme is a two-stage Stackelberg game: the supplier chooses , then the seller, having observed , chooses . Its subgame-perfect equilibrium gives the profits (seller and supplier under trade credit) and (under platform financing).
The paper defines two piecewise threshold functions of . They are built from the thresholds and the rates , all explicit in :
The goal states that and that, for every pair of equilibria of the two games,
The theorem says that a platform loan never benefits the seller while hurting the supplier. The outcome "win for the seller, loss for the supplier" does not occur. Whenever the platform's rate is low enough to help the seller, it also helps the supplier. Combined with Proposition 3, it identifies the mechanisms that make a platform loan attractive even without a cost-of-capital or information advantage: an interest subsidy at low uncertainty, risk mitigation at moderate uncertainty, and risk isolation at high uncertainty, where exceeds . The thresholds are explicit, so the result tells a platform the range of rates at which its lending creates value for both supply-chain parties.
The paper's proofs are long case analyses on closed-form radicals. Several displayed formulas in the manuscript contain printing errors (listed below), and some comparisons are justified as "it can be verified". A machine-checked development would certify the closed forms and the threshold algebra and settle the boundary cases. None of these results is formalized in Mathlib or in the Prove2Me library as of October 2026.
The equilibrium is not given by first-order conditions alone. Under limited liability the seller's objective is not concave in : it has a no-default regime and a default regime, and the maximizer jumps between them at . The supplier's problem under trade credit is therefore a comparison of two local optima: one quadratic, one a cubic in with a radical maximizer. The winner switches at , which involves . The comparisons of Propositions 3–6 then require sign analyses of differences of nested radicals across up to five regimes, ordered by and over .
Equating first-order conditions is not enough: equilibrium uniqueness requires excluding the off-path behaviour of the seller and handling the supplier's indifference at and .
Expectation. over is the normalized interval integral . All integrands are continuous.
Equilibrium. A strategy profile is a price together with an order rule defined at every price. A subgame-perfect equilibrium requires two things:
Two tie-breaks are part of the definition, both the paper's own conventions:
Goals quantify over equilibria. The closed forms enter only through the milestones. A statement taking the closed forms as hypotheses, or proving only , is not this theorem.
Standing assumptions.
Corrected slips, each disclosed in its item:
Boundary. Propositions 3–4 exclude the rate from their "otherwise" clause only for , where makes and the paper's statement and proof disagree; for other the boundary rate is kept, as on the page.
A complete development needs the following:
The best-response analysis under limited liability is reusable for other newsvendor-type financing models. Contributions of any milestone, of lemmas on the threshold order, and of alternative proofs are welcome.
Consumers judge a price against a reference price, an internal benchmark formed from the prices they have seen before. A price below the reference is perceived as a gain and raises demand; a price above it is perceived as a loss and lowers demand. Because today's price moves tomorrow's reference price, a seller who maximises the revenue of each period separately ignores how it erodes or builds future demand. This makes pricing a dynamic program, studied for a single product with linear demand by Popescu and Wu (Operations Research 2007) and Chen, Hu and Hu (Management Science 2017), among others.
Guo, Jiang and Shen (SSRN 4189049, published in Manufacturing & Service Operations Management, 2025) treat several substitutable products under multinomial-logit (MNL) demand. The dynamic program then has a continuous state of dimension , and computing the optimal policy is impractical even for moderate . The myopic policy, which maximises the current period's revenue only, is easy to compute. This mission formalizes the paper's bound on how much revenue the myopic policy can lose (Proposition 2).
There are products . Product has intrinsic utility , price sensitivity , and reference-price sensitivities (to gains) and (to losses). At price vector and reference vector , the utility of product is
the market share is , and the single-period revenue is .
Prices and reference prices lie in the admissible box with a price ceiling . The reference price follows exponential smoothing with memory : . Revenue is discounted by .
With , for every and every myopic policy,
The bound is uniform in the initial reference price and has an explicit constant. It vanishes in three regimes: (the reference price never moves), (only the present counts) and (no reference effect). It quantifies how much the intertemporal structure costs a seller who ignores it. The myopic policy is computable by a one-dimensional root search (Theorem 1 of the paper), while the optimal policy suffers from the curse of dimensionality, so the bound is what makes the myopic policy a usable benchmark.
The paper proves Proposition 2 in its online supplement (Appendix C.1), which is not part of the source file used for this mission. To our knowledge, none of these results has a machine-checked proof. Formalizing them yields a verified Bellman equation for a deterministic dynamic program with a continuous multidimensional state and a nonsmooth, nonconcave reward.
The left inequality only uses the fact that the myopic price sequence is admissible. The right inequality is the content. Comparing the two value functions period by period fails: in a given period the optimal policy may earn less than the myopic one, and its later advantage comes from having moved the reference price. The two policies also generate different reference paths, so their revenues are evaluated at different states, and the sensitivity of the revenue to the reference price enters only through the constant . The revenue is not concave in prices or in reference prices, and the kinks at make it nonsmooth. The Bellman equation itself needs the optimal value to be well behaved enough in for the one-step maximum to be attained.
Products are indexed by Fin n (product is Lean index ), and vectors are Fin n → ℝ. The shares are defined directly by the logit formula; the Gumbel random-utility derivation is motivation only. The standing assumptions , , , and are hypotheses of every theorem. The goal also assumes the ceiling condition , as a standing assumption of §2.4. That condition is stated as the existence of a root of (9) at most . The Bellman equation omits the ceiling condition (it holds without it). Proposition 1.1 varies , so it does not take the condition.
optValue, the supremum over all admissible price sequences, built as an instance of the published deterministic dynamic program KarlinDP.Deterministic.optimalReturn (Karlin 1955). The paper writes as a maximum over stationary policies and uses it through (6); milestone 1 is the theorem that connects the two.⨆ i, which is when (then ).Lean's real supremum is on an unbounded family and its tsum is on a non-summable series. Neither default is reached here: with and the family is nonempty and bounded by , and every series is summable. So the goal cannot hold vacuously through a junk value. In particular, may not be replaced by an arbitrary solution of (6), and the constant may not be weakened, for example by replacing with .
Needed infrastructure: continuity of the MNL revenue, the Bellman equation for a discounted deterministic program on a compact action set, and bounds on the myopic value as a function of . The first two are reusable beyond this mission. Contributions toward any milestone are welcome.
Financial networks are webs of liabilities: firm owes firm an amount , and every firm holds some external assets. When firms cannot pay in full, how much money actually moves through the network depends on how each firm splits its available funds among its creditors. The classical clearing model of Eisenberg and Noe (2001) fixes this split by a proportional rule. Flow allocation games, introduced by Bertschinger, Hoefer and Schmand (arXiv:1908.01714, Mathematics of Operations Research, 2025), make it strategic: every firm chooses how to allocate whatever it receives, and the resulting payments are the clearing state of the chosen strategies.
Because money that circulates comes back, the total amount of flow in such a network is driven by cycles, and cycles require several firms to cooperate. The natural solution concept is therefore the strong equilibrium, which is stable against joint deviations of coalitions. The paper shows that in unit-ranking games a strong equilibrium maximizing total flow always exists (Theorem 9, price of stability ). This mission concerns the other side: how much total flow can the worst strong equilibrium lose, and which structural parameter of the network controls the loss.
A flow allocation game consists of a finite directed graph (parallel edges allowed), a fixed supply at each node and a capacity on each edge. Every node is a player. and denote the outgoing and incoming edges of , and .
In a unit-ranking game, player chooses for each edge a non-decreasing function with and : given a total supply , it forwards all of it until its outgoing edges are full, one unit at a time according to a ranking of unit capacities. A flow is feasible for a profile if with . The clearing state is the coordinatewise largest feasible flow; player 's utility is , and the total flow is
A profile is a strong equilibrium if no non-empty coalition can jointly switch to other unit-ranking strategies so that every member of strictly gains.
The circulation network adds an auxiliary node with edges of unbounded capacity and of capacity for every . An optimal circulation of maximizes . A decomposition of into cycles of unit flow is a list of simple directed cycles of that uses each edge exactly as often as has units on it. The parameter of this mission is
the smallest possible size of the longest cycle, over all decompositions of all optimal circulations; sizes count auxiliary edges.
In unit-ranking games, the price of anarchy for strong equilibria in terms of Flow is at most : for every strong equilibrium and every unit-ranking profile ,
The statement fixes no constant beyond the structural parameter and holds for all capacities and supplies.
The bound identifies the length of the circulating cycles as the quantity that governs the efficiency of coalition-stable payment behaviour. In networks whose optimal circulation decomposes into short cycles, such as bilateral or triangular netting of liabilities, every strong equilibrium clears at least a fraction of the optimal total payments; Proposition 17 shows that long cycles genuinely cost efficiency, so the bound is tight up to one. For pure Nash equilibria no such bound exists (Proposition 15, the price of anarchy is unbounded), so the result separates coalitional from unilateral stability.
The results are proved on paper; none of them is machine-checked. A formalization adds a precise account of the model (clearing state as a supremum of feasible flows, unit-ranking strategies as functions on , cycle decompositions of the circulation network) and checks a proof whose last step, as printed, needs repair. The printed last display, , does not hold for cycles passing through the auxiliary node : with a single node , and no outgoing edges, but . The theorem itself is not contradicted by this example, and the printed argument is complete for games without fixed supplies. The cycles through the auxiliary node need a separate count, which is part of the work this mission asks for.
The upper bound compares an arbitrary strong equilibrium with an optimum that may look nothing like it. The obvious approach, counting the units of each optimal cycle that also carry equilibrium flow, fails: the clearing state is a fixed point of all strategies at once, so whether a unit reaches an edge depends on decisions all around the network, and the equilibrium may route its flow along entirely different cycles. A single player cannot complete a cycle on its own, which is why the Nash price of anarchy is unbounded; any argument has to use coalitional deviations, and a deviation changes the clearing state globally, so its effect on each member's utility must be controlled through the fixed point.
The second difficulty is the auxiliary node. A cycle of the optimal decomposition that passes through contains a node that is not a player, so no coalition of players can claim it, and the unit of flow it represents may sit on an auxiliary edge that does not count. These cycles are exactly where the printed argument stops short.
Supplies, capacities, strategies and flows are natural numbers, as the paper prescribes for unit-ranking games. The graph is a finite type of nodes and a finite type of edges with tail and head maps, so parallel edges and loops are allowed. The clearing state is the coordinatewise sSup of the feasible flows. Coalitions are non-empty, and deviations range over unit-ranking profiles. Optimal circulations are optimal among integral circulations. Cycles of are lists of edges with pairwise distinct start nodes, and decompositions are lists of cycles counted with multiplicity. Nodes of are Option V, with none the node .
The price of anarchy is stated multiplicatively, , with no division, so a zero-flow equilibrium cannot satisfy the goal vacuously through a junk quotient. The parameter enters as a hypothesis, "some decomposition of some optimal circulation has all cycles of size at most ", which is equivalent to the bound for the min-max and avoids an infimum that would be on an empty set. In Proposition 17 the strong equilibrium is required to have positive flow, since otherwise the lower bound would hold trivially.
Not formalized: the complexity results of the paper, the bounds for other quality measures (Proposition 18) and for Nash equilibria (Proposition 15). A complete development needs the integral version of the lattice theorem for feasible flows (Theorem 2), the existence of a Flow-optimal profile from the proof of Theorem 9, and integral cycle decomposition of circulations; the last two are reusable beyond this mission. Contributions are welcome on each milestone, on a separate count for cycles through , and on the explicit construction of Proposition 17.
Global sensitivity analysis asks how much the uncertainty in an output of a model or a data set is explained by an input . A large family of indices has the form "expected discrepancy between the marginal law of and its conditional law given ": the variance-based index of Sobol' and Wagner, the density-based index, Kuiper and Cramér–von Mises indices. Borgonovo, Figalli, Plischke and Savaré (Management Science 2025, doi:10.1287/mnsc.2023.01796) take the discrepancy to be an optimal-transport cost. The resulting indices apply to multivariate outputs, need no density, and include as special cases the numerator of Wiesel's Wasserstein correlation coefficient (Wiesel 2022, arXiv:2207.14079).
A sensitivity index is meant to measure information: how much knowing , or a coarsening of , tells about . Two properties make this reading legitimate. Coarser information must never be worth more than finer information, and an index computed from increasingly fine observations of must approach the value for the limiting information. This mission formalizes both properties for the optimal-transport indices, Theorems 8 and 9 of the paper. Theorem 9 is also the last step of the paper's consistency proof for its partition estimator (Theorem 21).
Let be a probability space, and Polish spaces with Borel σ-algebras , , and , measurable maps. Write and for the laws of and .
A cost is a continuous function with exactly when . The optimal-transport cost between probability measures on is
where is the set of probability measures on with marginals and .
For a σ-algebra , representing partial information on , a version of the conditional distribution of given is a family of probability measures on with -measurable and
The OT-based sensitivity measure (Definition 1) is
written when . For a Borel map into a Polish space, is a new random variable and is defined in the same way on ; is the σ-algebra generated by .
For an increasing sequence of sub-σ-algebras of with join ,
The results. Theorem 8 is the formal statement that the OT indices value information monotonically: a transformation of an input, such as a discretization or an aggregation of features, can only lose explanatory power, and loses none when is injective. Theorem 9 makes the indices continuous in the information: refining a partition of the input space, as an estimator does when the sample grows, recovers the index of the limiting σ-algebra. The paper relies on Theorem 9 to prove that its given-data estimator is consistent, and on Theorem 8 to justify its interpretation of the indices as values of information.
The formalization. The proofs are on pp. 35–36 of the authors' manuscript. As far as we know, none of these statements has been machine-checked. Formalizing them requires conditional distributions relative to arbitrary sub-σ-algebras, the convexity of optimal-transport costs under mixtures, and their lower semicontinuity under weak convergence, which are general facts of optimal transport that the platform does not yet have.
The monotonicity in Theorem 8 is a Jensen inequality, but it is applied to a function of a measure, , along a mixture indexed by a disintegration, so the step needs a measurable choice of near-optimal couplings. Without such a choice the averaged coupling is not defined.
For Theorem 9, the inequality follows from monotonicity, and is the substance. The natural first idea, Lévy's upward theorem applied to , gives convergence for one test function at a time and outside a null set that depends on . Weak convergence of the conditional laws for almost every is a statement about all test functions at once. Even with it, is only lower semicontinuous, not continuous, and the cost may be unbounded and take the value . No integrability hypothesis is available: the theorem holds without assuming , including when the limit is .
ℝ≥0∞); integrals are lower Lebesgue integrals.RWPI.SqrtLasso.transportCost. Its first argument is the marginal and its second the conditional law.IsCondDistrib), never constructed. Every statement holds for every version, and versions for different need not be compatible.⨆ n, Fs n), and the sequence is indexed from .The goal is a Tendsto in , not a one-sided bound. In particular, a proof of only (monotonicity) or of the statement under a finiteness hypothesis on does not close it. uses the conditional distribution of given the random variable on , not that given ; their equality is part of (24).
Two readings are disclosed corrections. Theorem 9's "sub-σ-algebras in " is read as sub-σ-algebras of . The comparison of two sub-σ-algebras , used in the proof of Theorem 9 but stated in Theorem 8 only for , is posed as its own milestone.
Reusable infrastructure includes the following, and contributions of any of them are welcome:
Optimal auction theory in the tradition of Myerson (1981) assumes that the seller knows the distribution of the buyers' valuations. In practice that distribution is estimated, misspecified, or simply unknown. Prior-independent mechanism design asks for a mechanism that performs well across a whole class of distributions, without being tuned to any one of them. A natural yardstick is regret: the gap between the revenue the seller would extract if she knew the valuations, namely the highest valuation, and the revenue her mechanism actually collects. The seller chooses a mechanism to minimize the worst case of this gap over all distributions Nature may pick.
For a single buyer, Bergemann and Schlag (2008) showed that the minimax regret over valuations supported on is , attained by a posted price drawn at random with CDF on . Whether a comparably explicit answer exists for buyers, and whether the familiar second-price auction remains optimal among all dominant-strategy mechanisms, was open. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) answer both questions for i.i.d. valuations. This mission formalizes that answer: their Theorem 1.
A seller has one indivisible item and buyers with valuations . A mechanism assigns to every valuation profile allocation probabilities and expected payments . It is dominant-strategy incentive compatible (DSIC), written , if for all , all and every misreport :
For a joint distribution of , the regret is
and the minimax regret over a class of distributions is . Here is the class of product laws whose marginal is supported on .
A second-price auction with random reserve draws a reserve price from a distribution . The highest bidder wins if her bid is at least and pays , where are the two highest valuations. Otherwise nothing is sold.
Two explicit functions enter the answer. For , let
and, for ,
with below and above . The isorevenue marginal on , , is the law under which every posted price in earns the same revenue .
Let be the root of in ; it is the only root in . A reserve distribution on with CDF exists. The auction is DSIC and minimax-regret optimal, and
The Lean goal states the location and uniqueness of the root, the existence of the reserve law, the DSIC property, the upper bound for against every i.i.d. law, the matching lower bound for every DSIC mechanism, and the literal identity for .
A companion item states Corollary 1 (p. 14): for , , on , and the minimax regret is .
The theorem gives, for every number of buyers, a closed-form description of the minimax-regret optimal mechanism among all DSIC mechanisms, together with its value. The optimum is a familiar format, a second-price auction, but its reserve price must be randomized. The same saddle point is the starting point for the paper's results on affiliated and arbitrary joint valuations, which are separate missions of this series.
The result is proved on paper. To our knowledge none of it has been formalized. A complete development would supply machine-checked versions of several tools that recur in robust mechanism design: DSIC mechanisms with randomized allocations, the regret functional, order-statistic CDFs of product measures, Myerson-type revenue characterizations under distributions with atoms, and saddle-point arguments for inf–sup problems over mechanisms and distributions.
The upper bound (Step 1) is a pointwise optimization once the regret of is written through the CDFs of the order statistics. Writing it that way already requires integration by parts against arbitrary distributions on , which may have atoms.
The lower bound (Step 2) is the hard direction. One must show that no DSIC mechanism beats against the isorevenue law. The standard route through Myerson's virtual values does not apply directly: the isorevenue law is a mixture of a density and a point mass at , so the revenue of a general DSIC mechanism has to be characterized from first principles. That characterization starts from the payment identity for dominant-strategy mechanisms. The closed forms also involve a transcendental root and a logarithmic ODE solution, so the monotonicity and boundary facts about (it is a CDF, ) need real analysis rather than numerics.
Buyers are indexed by Fin n, valuations are functions Fin n → ℝ, and distributions are measures on that space. (IR), (IC) and (AC) are imposed for valuations in , which is all the seller considers. Two conditions are added to DSIC so that the expectation in the regret is meaningful: the allocation and payment rules are measurable, and payments are bounded on the cube. The second-price auction breaks ties in favour of the lowest index; the revenue does not depend on the rule. A reserve law or an isorevenue law is described by a hypothesis on its CDF. is defined piecewise, so its closed form is never evaluated at the singular point , and "" is stated as a one-sided limit. The minimax regret is a real infimum over the nonempty class of DSIC mechanisms of real suprema of bounded families. Uniqueness of is stated on , which is what the paper's proof establishes.
Trivializing formalizations are ruled out explicitly. The regret is not a Bochner integral of a possibly non-integrable payment, which Lean would set to . The mechanism class is not restricted to second-price auctions. The value is the explicit integral, not a sSup. The root's location in is part of the claim.
Contributions are welcome at every level. These include the DSIC property of , order-statistic CDFs of product measures, Lemma B-1 and Proposition 1, the analytic facts about and , the payment identity for DSIC mechanisms with randomized allocations, and the revenue bound of Step 2. The analytic and mechanism-design infrastructure is reusable beyond this paper.
Social media influencers earn money by endorsing products to their followers. An influencer who endorses only products that fit her organic content keeps her audience; one who accepts every sponsorship offer earns more per follower today but loses part of her audience and grows more slowly. Practitioners describe this as the choice between growing and monetizing, and the marketing literature documents both sides of it: followers unsubscribe after poorly fitting sponsored posts (Cheng and Zhang 2022), and small influencers have deeper engagement than large ones (Bentley et al., J. Global Marketing 34(3), 2021, cited in the paper).
Nistor, Selove and Villas-Boas (Management Science, Articles in Advance 2024) turn this trade-off into a deterministic continuous-time control problem. Awareness of the influencer spreads by word of mouth as in the Bass (1969) diffusion model, and the influencer's authenticity is the control. The paper's first main result, Proposition 1, characterizes the optimal policy completely: depending on two explicit conditions, the influencer is always authentic, always inauthentic, or authentic until her awareness reaches a threshold and inauthentic forever after. This mission formalizes Proposition 1 and the lemmas of §3.3 that lead to it.
Time is and the mass of potential followers is one. The influencer's awareness is the fraction of potential followers who know her, starting from . At each time she is authentic or inauthentic. Following Table 1 of the paper, with parameters and (the reduced-form parameters of §3.1, which aggregate the offer arrival rate, the share of good-fit offers and the followers' tolerance of bad-fit posts):
Awareness grows according to the equation of motion (1),
so it grows at rate when she is authentic and when she is inauthentic. With discount rate the influencer maximizes the discounted profit (2),
and is the value of starting at awareness and following the optimal policy.
Two closed-form objects enter the main result. The value of always being inauthentic from awareness is (Lemma 3)
and its derivative is (3)
Condition 1 (with footnote 4) holds if or .
For , , , :
and for all sufficiently small the policy "authentic while , inauthentic once " is optimal.
In the paper's order: Lemma 1 (corrected) bounds the growth of above awareness ; Lemma 2 (corrected) shows that permanent inauthenticity is optimal at large awareness; Lemma 3 gives in closed form; (3) identifies as its derivative; (4) computes the limit of at zero awareness,
which is where Condition 1 comes from.
Proposition 1 is the benchmark of the paper: each of the six model extensions of §4 (celebrities, follower turnover, partial authenticity, viral content, two segments, commitment) is read against it. Its third clause explains an observed pattern in influencer marketing, that small influencers post fitting content and large ones accept most sponsorships, as an optimal policy rather than a change in preferences, and Condition 1 makes explicit when growth potential outweighs current profits; the paper notes it always holds when . The numerical example of §3.5 (Table 2) places the switch at about 73% awareness.
The proofs are in an online appendix and have not been machine-checked. Formalizing them requires an optimality argument against every measurable switching pattern, not only threshold policies. The mission also records two corrections: Lemma 1 and Lemma 2 are false as printed when (explicit counterexamples are in the milestone statements), and they are stated here with the constant that the paper's own argument gives.
The natural argument compares, at each instant, the extra profit from inauthenticity, , with the value of the extra growth from authenticity, . This requires knowing the value function , its differentiability, and the Bellman equation it satisfies, none of which is given; replacing by is only justified along the part of the trajectory after the switch. The comparison must also hold against every measurable switching pattern, under which awareness solves (1) only almost everywhere. Clause 3 additionally needs the threshold equation to have a single crossing and the optimal trajectory to cross it exactly once. Optimality of a constant policy cannot be read off from instantaneous profits alone when : the instantaneously better choice (inauthenticity) can be the wrong one for a small influencer.
A trivializing formalization is ruled out: optimality is never assumed, the competitor class contains the constant policies' logistic paths, the threshold must solve the equation of (3) inside , and measurability of policies keeps every profit integral meaningful. The microfoundations of §3.1 (, , , , ) do not enter any statement.
The development needs Carathéodory solutions of a scalar ODE with a measurable switching coefficient, comparison and uniqueness for such solutions, differentiation under an improper integral, and a verification argument for a one-dimensional deterministic control problem with bang-bang control. The last two are reusable for other continuous-time marketing and diffusion models. Proofs of any milestone are welcome, as are proofs of the logistic closed form underlying Lemma 3.
A portfolio manager who observes today's value of a covariate (a market signal, a macroeconomic indicator) wants to choose a portfolio that performs well conditionally on that observation: the relevant risk is of the asset return , not its unconditional mean. With finitely many historical pairs , the empirical conditional distribution at a new is usually empty or rests on one or two samples, so estimating it directly is unreliable. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research 2025) hedge it with distributionally robust optimization: they take the worst case of the conditional expectation over all joint laws of within an optimal-transport ball around the empirical measure that still put a prescribed amount of mass on the conditioning event.
The objective is a ratio of two linear functionals of the law, so the standard strong-duality theorems for Wasserstein distributionally robust optimization (Mohajerin Esfahani and Kuhn, 2018; Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) do not apply directly. This mission formalizes the paper's answer in the singular case where the conditioning event is the single point and the event must keep mass at least .
Let (covariates) and (returns) be spaces with ground costs , , combined into the separable cost . The data are samples , , with empirical measure .
For a loss at a fixed decision, the object of study is the worst-case conditional expected loss
For and ,
The loss is arbitrary (measurable, real-valued), and both sides may be .
Theorem 3.2 reduces an infinite-dimensional, fractional worst-case problem to a two-multiplier convex program whose only infinite-dimensional pieces are suprema over . For piecewise-linear losses and norm costs the paper turns this into the conic programs of Propositions 3.3–3.4, which are what make the robust conditional portfolio model solvable in practice. It also compares the formulation with the trimming approach of Esteban-Pérez and Morales (Mathematical Programming, 2022), whose adversary may only pick laws with fiber mass exactly ; Proposition A.5 shows that, at , the more powerful adversary allowed attains the same value.
The result is proved in the paper; nothing here is open mathematics. None of it is formalized. A complete development would add to the platform a first conditional (fractional) distributionally robust duality, a decomposition of optimal-transport balls around empirical measures (milestone 1, reusable by every finite-sample Wasserstein result), and a moment-problem duality with one budget constraint (milestone 5).
The ratio objective is the obstacle: neither the numerator nor the denominator alone determines the worst case, and a law that is optimal for the numerator may violate the mass constraint. The step "fix the fiber mass at " (Proposition A.5) is where the obvious argument fails: an optimal law may put more than on , and reducing that mass requires moving sample points off at vanishing transport cost, which needs points of arbitrarily close to . Milestone 1 needs the existence of optimal couplings, which Mathlib lacks. Milestone 5 is an infinite-dimensional Lagrangian duality whose Slater point degenerates on the boundary of the weight set, so the final interchange of supremum and infimum must avoid that boundary.
and are Polish spaces with their Borel σ-algebras; samples are indexed by Fin N with , repeats allowed. The optimal transport cost is the published RWPI.SqrtLasso.transportCost (an infimum of lower integrals of the -valued cost; attainment is not built in), and every expectation of the loss is the published ModelRiskOT.Duality.extIntegral, in . Worst-case values and duals are EReal suprema and infima. The loss is a measurable L : Y → ℝ standing for at an arbitrary decision.
Hypotheses beyond the page, all disclosed in the statements:
NotIsolated: for every there is with . This is Assumption 2.4(iii) at read with the ambient boundary of , as the paper's remark on p. 11 does; with the topological frontier in , (iii) is vacuous at an isolated , and Theorem 3.2 is then false.Trivializing formalizations are ruled out: conditional expectations are only taken at laws with fiber mass at least (never at mass , where a real division would return ); expectations are never Bochner integrals, which would be for a non-integrable loss; the radius enters through ENNReal.ofReal ρ only where or forces ; and every supremum ranges over exactly the paper's feasible set.
Needed infrastructure: existence of optimal couplings on Polish spaces (Villani, Theorem 4.1), a Lagrangian duality for moment problems, and Mathlib's Sion minimax theorem for the interchange. Contributions to any of these, and proofs of the milestones in any order, are welcome.
Banks lend to each other. When one bank's investments fail, it may be unable to repay its interbank debt, and its creditors then receive less. Since Eisenberg and Noe (2001), the standard way to compute who pays whom after such losses has been a clearing vector: a fixed point of a system in which every bank pays the smaller of what it owes and what it has. Much of the later literature on systemic risk takes the banks' assets as given and asks how losses spread through this fixed point, for example Acemoglu, Ozdaglar and Tahbaz-Salehi (2015).
Chong Shu's paper Endogenous Risk Exposure and Systemic Instability (Management Science, doi:10.1287/mnsc.2022.01519) reverses the question: when banks know they are connected, how much risk do they choose? A successful bank pays its interbank debt in full while its failed counterparties do not, so success is partly taxed by the network. This cross-subsidy shrinks the reward for choosing a safe project. The paper's first main result, Proposition 1, says that in every network the banks' risk choices are strategic complements: when one bank takes more risk, every other bank wants to take more risk too. This mission formalizes Proposition 1.
A finite set of banks is given. For banks , is the face value of the debt that bank owes bank . Bank 's total interbank liability is , assumed positive, and is bank 's share of it. Bank also owes a deposit , which must be paid before its interbank debt.
Every bank picks a project from an interval . The project pays with probability and otherwise, independently across banks. Assumption 1: , is decreasing, and is concave. A standing assumption rules out systemic default: for every , so a bank whose project succeeds can always pay in full.
A state records which projects succeeded; bank 's cash flow is if and otherwise. A payment equilibrium solves
Bank 's profit is , and its expected profit is the sum over states weighted by . The best-response set is the set of maximizers of over , with the other banks' choices held fixed. The cross-subsidy is
bank 's expected net payment to the network when its own project succeeds.
For banks , profiles , and equal to except that :
This is the strong-set-order form of " is nondecreasing in ". It does not require the network to be regular or path-connected.
The regular-network step (I.3) (IA p. 7), that the maximizer of is increasing in , is also posed, as a theorem outside the milestone list.
Proposition 1 makes the risk-taking game supermodular. That property is what the rest of the paper relies on. It gives existence of equilibrium (Proposition 2) through Tarski's fixed-point theorem, it identifies least and greatest equilibria, and it lets the later comparative statics compare networks: complete against ring, size, central clearing, bailouts. Each of these results argues "the cross-subsidy rises, so equilibrium risk rises", and that step is Proposition 1 applied through Topkis's monotonicity theorem.
On the formal side, no clearing model is currently on the platform. This mission supplies one: the Eisenberg–Noe clearing system with a stochastic state, the greatest clearing vector, expected profits, and best responses. It also checks the paper's proof in the non-regular case. That proof splits on the states in which a bank survives its own failure, and one inequality in it is asserted without proof. The result is proved on paper; none of it has been machine-checked.
In a regular network a failed bank always defaults, and the argument reduces to two monotonicity facts: (I.3) and (I.4). In a non-regular network a failed bank can still earn a profit when enough of its debtors succeed. A riskier counterparty then has two opposite effects. It raises the cross-subsidy, which pushes toward risk, and it lowers the chance of being bailed out after one's own failure, which pushes away from risk. The proof must show that the first effect dominates in every network. It does so by partitioning the states according to whether bank survives its own failure, , and by showing that the states in that set contribute nothing to the cross-partial. This requires the clearing vector to be monotone in every bank's success and stable when a surviving bank's own state flips. It also needs an inequality, whenever , which the paper asserts without proof.
The naive route is to differentiate the first-order condition, as the paper does in (I.3). That route is not available: Assumption 1 gives neither differentiability of nor a unique maximizer.
Banks form a finite type, and states are Boolean vectors (true = success). All probabilities are finite products and all expectations are finite sums: no measure theory is involved. Sums over are written as sums over full states with fixed, weighted by the product over .
Conventions the Lean statements commit to:
AntitoneOn), which is the more general hypothesis.The goal is vacuous when a best-response set is empty. This is faithful, since presupposes a maximizer, and best responses exist whenever is continuous. A formalization that takes as an arbitrary solution under a uniqueness hypothesis, or as an sSup that could be junk, would trivialize the mission. The definition used here is shown, in a sorry-free check, to solve the clearing system.
Not posed: Lemma 1 (cited from Eisenberg–Noe), Proposition 2 and Corollary 1 (consequences of Proposition 1), and the later comparative statics (Propositions 3–9). Proposition 4, the comparison of complete and ring networks, is a separate mission of this series. Reusable contributions are welcome: monotonicity of greatest fixed points in a parameter, and a general Topkis-style argmax monotonicity on chains.
Reward-based crowdfunding and venture capital are two of the main sources of early-stage finance, and the empirical record on how they interact points both ways: some studies find that more crowdfunding activity is followed by more VC investment, others find the opposite. Hu, Jin and Keppo (SSRN 3512638; Management Science, 2024, doi:10.1287/mnsc.2022.00994) explain both signs with one firm-level model. A crowdfunding campaign has two roles: it raises a modest amount of money, and its outcome is a public signal about whether the product will succeed. Two VC firms with different priors compete for the deal, and the more optimistic one may prefer to wait for the campaign's outcome rather than invest at once.
The paper builds on earlier work on the informational value of crowdfunding for professional investors (Roma, Gal-Or and Chen, 2018; Babich, Marinesi and Tsoukalas, 2021) and on crowdfunding as a mechanism (Strausz, 2017). Its main result, Proposition 6, says exactly when the mere option of crowdfunding lowers the expected VC investment and when it raises it.
A startup needs at least to launch a project whose revenue is if it succeeds and if it fails, with ; each state has probability . It offers an investing VC firm an equity share . VC and VC believe the startup succeeds with probabilities , the startup itself with probability ; under a belief the expected revenue is , giving . A VC's valuation of the share is .
The investment level at which VC acquires the share is
where is the startup's negotiation power. VC never invests; it matters only as the startup's outside option.
Timeline. At VC may invest. If it does not, the startup runs a crowdfunding campaign with target , which produces a signal (success, collected) or (failure) with , where is the signal's accuracy. All parties update by Bayes' rule, with posteriors , and expected revenues , . At VC reconsiders: after the requirement is and the share is scaled to ; after both stay as they were. Assumption (I) requires .
VC compares its surplus from investing now, , with its expected surplus from waiting, ; the value of waiting is , and VC invests at when and . The paper shows that this happens exactly when , for an explicit threshold (Proposition 2). The startup chooses to maximize its expected payoff. Without crowdfunding it offers . With crowdfunding it offers or , according to the sign of its own value of waiting (Proposition 4). The expected VC investment level or is the level along VC's decisions, averaged over the signal under the unconditional belief .
Under the standing assumptions,
and if no share in draws an investment without crowdfunding, while .
Proposition 6 separates two populations of startups. For a startup that VC would fund anyway () and that prefers to induce a delay (), crowdfunding lowers expected investment: after success the requirement drops to , and after failure nobody invests. For a startup that VC would not fund on its prior (), crowdfunding creates investment that would otherwise not exist. If the startup prefers to keep the investment before the campaign (), the mere option of crowdfunding raises the level even though no campaign is run. Together these account for both signs of the empirical crowdfunding–VC relationship.
The paper's proofs are case analyses on closed forms. No part of this model has been machine-checked, and nothing on the platform models crowdfunding, VC competition or this signal structure. A formalization checks the seven-subcase comparison behind Proposition 2. It also pins down hypotheses the paper uses without stating them: nonnegative revenue, , , and . Each is needed, and each has an explicit counterexample without it.
The hard step is Proposition 2(i). Both and are piecewise linear in , with breakpoints where , , and cross their requirements. The claim that is a single up-ray needs the relative order of these breakpoints. Which closed form ( or ) is the threshold depends on where VC's post-signal valuation sits. The threshold is therefore not read off a single formula: each ordering of the breakpoints is a separate case, and the paper's proof runs through seven of them. Everything downstream, including the startup's optimum and the comparison of investment levels, needs the threshold to be exact.
Everything is elementary real arithmetic, with no measure theory. The parameters are a record of nine reals. "Expected" means the two-term average over and , with , the mixture implied by the signal accuracies (the paper does not print it). The posteriors, , , , , , and are the printed closed forms. VC's decisions, the startup's payoffs and the investment levels are defined from the surpluses and from . A VC that cannot meet the requirement after a signal gets surplus , as in the paper's proof (the printed would give it its valuation). VC's ties go to investing now and the startup's ties to . "Optimal" means a global maximizer over . "Raises" is weak where equality can occur (, ), and comparative statics in are weak.
Standing assumptions on every statement: , , , , , , . Added hypotheses:
Proposition 3(i)'s bound is stated as , because is allowed.
The goal compares investment levels computed from VC's decisions, not the paper's closed forms , , whose comparison is three lines of algebra. The threshold is not defined as the infimum of the shares at which VC invests, which would make Proposition 2(i) a tautology. The goal is stated at the paper's selected share , not at every maximizer.
Not formalized: Online Appendix A (the startup re-optimizes after the campaign), Appendix B (profitability for the startup and VC), and Appendix C (comparative statics in and ). Proofs of any milestone are welcome. The case analysis of Proposition 2(i), stated as lemmas about the piecewise-linear surpluses, would be reusable by every downstream item.
Antitrust authorities review horizontal mergers by asking whether the merged firm will raise prices. A prior question is which mergers firms will choose to form at all. When several firms can merge, the identity of the partner matters: a large firm may absorb a small rival, or two small rivals may combine to face the large one. Wang, Wu, Tang and Dai (Management Science, 2024) study this partner-selection question in a price-competition model with two frictions common in retail and service markets: limited capacity of the small firms, and loyal segments, buyers who only buy from their own firm. Their main result says exactly which merger, if any, arises in equilibrium. Every step of its proof is an explicit comparison of closed-form profits, which makes the result a natural target for complete machine verification.
Three firms , , sell a homogeneous product at zero marginal cost. A unit mass of buyers each demand one unit and value it at the reservation price . Each firm has loyal buyers, ; the remaining buyers are switchers who buy from the cheapest firm. Firm is unconstrained; the small firms and each have capacity , with . Unserved buyers are rationed at random and spill over to the next cheapest firm.
The firms may stay independent, ; firm may merge with one small firm, the mixed merger ; or the two small firms may merge, the small merger . A merged entity pools capacities and loyal buyers. In each structure the firms play a price game whose equilibrium is in mixed strategies. The paper's Table A1 lists, for each structure, the lower bound of price support , , and the equilibrium profits , , , , , , as piecewise functions of built from
the numbers of spilled-over switchers. In the small merger each small firm receives half: .
A structure is an equilibrium structure when no firm or coalition gains by deviating. For this is
for it is
and the status quo is the equilibrium structure when neither condition (1) nor condition (2) holds.
With ,
The statement is an exact characterization: in the interval the mixed merger is an equilibrium structure and the small merger is not; outside it neither merger is.
The result separates the two forces of the model. Loyal buyers make a merged entity less aggressive in price, which is why no merger is profitable when capacity is ample. Limited capacity creates spillover demand, which a large firm captures by merging with a small rival but which two small firms do not capture by merging with each other. Proposition 3 says the second force wins exactly on and that the small merger never forms. This answers one of the paper's opening questions, whether two capacity-constrained small firms merge to compete with a large one: in this model they do not.
The paper proves the result by hand, over eight regions of the parameter plane (its Figure A1). The comparisons involve rational functions whose denominators are positive only under the region's constraints, and threshold curves with square roots. A machine-checked proof certifies the region bookkeeping. No formalization of this result exists.
Each single comparison is elementary algebra; the difficulty is the case structure. Table A1 has four rows in whose boundaries (, , ) differ per column, and three of its cells are maxima whose active branch changes along the curves , , . Root-location facts such as and are needed to know which row a region lies in. One inclusion the proof uses is only shown in the paper's figure: on , where condition (2a) holds, one needs in order to conclude that (2b) fails. At the region boundaries and several of the proof's strict inequalities are equalities.
Everything is stated over the reals in the namespace EndogMerger.SymLoyal. All definitions take explicit parameters (α k r : ℝ). The standing assumptions , , , and or as each statement requires, are hypotheses of each theorem. Relative to the paper, replaces (every region of the analysis has ), and is made explicit. Firm 's capacity does not enter Table A1 and is not modelled. The split of between and is left unspecified, as in the paper.
Table A1 is the definition. The profits and lower bounds are defined by Table A1's piecewise expressions, row by row, with max where the table has a maximum. The paper's derivation of these values as equilibrium outcomes of a mixed-strategy price game with random rationing is not formalized; Section 6 of the paper itself obtains Proposition 3 from the Table A1 profits. The paper's PDF page numbers are cited throughout; the appendix restarts its printed numbering, so printed page numbers are not used.
Three trivializing formalizations are ruled out. The profits are not defined by the closed forms of Lemmas 3–5, which would make those lemmas definitional. The equilibrium predicate for requires that neither condition (1) nor condition (2) holds, so the goal includes the claim that the small merger is never an equilibrium. The thresholds and are not defined by the paper's equation , which Real.sqrt satisfies for every with a negative radicand. Instead , and is a parameter pinned as the root in of .
Where the paper's proof claims a strict inequality on a closed region whose boundary gives equality, the milestone states it on the open region, and its Formalization Note says so.
No library beyond Mathlib's real arithmetic and Real.sqrt is needed. Lemmas about the threshold curves, for example that lies in , are reusable across milestones. Contributions of intermediate lemmas, including the region inclusion , are welcome.
Ride-hailing platforms are expected to add autonomous vehicles (AVs) to fleets of human-driven vehicles (HVs). A common expectation is that AVs, by removing the driver's wage, will make rides cheaper. Lian and van Ryzin (SSRN 3716491; published in Management Science, 2025, DOI 10.1287/mnsc.2020.03112) show that the answer depends on the market configuration. Two forces act on the price. A labor-cost effect: AVs displace human drivers, and the remaining drivers need lower pay. A density effect: pickup times fall as more idle cars are close to riders, so a larger fleet on one dispatch platform is more efficient per ride. When AVs and HVs are dispatched by independent platforms, the HV platform becomes thinner and loses density, and the price can rise.
This mission formalizes Proposition 4 of the paper, the result that makes this precise: under an explicit upper bound on the slope of the HV labor supply curve, coexistence of AVs and HVs on independent platforms strictly raises the price above the pure human-driver market. The version used is the authors' SSRN working paper of 23 August 2023; all numbering refers to it.
A market has six parameters. Riders wait for a pickup for an expected time , where is the number of open cars (idle vehicles), , and is the ETA elasticity; means there is a density effect. A ride lasts . Rider values for a ride-hour are uniform on . In a demand scenario with potential demand mass , the inverse demand at a demand rate (ride-hours per hour) is
A fleet of human drivers participates only if each earns its reservation earnings per hour, with and ; means HV supply is finitely elastic.
By Little's law and an optimization over the number of open cars, the minimal fleet that can serve a demand rate is
and the fleet's on-trip utilization is .
Pure-HV market. Revenue is and the minimal labor cost is . A demand rate is an equilibrium when they are equal; it is stable when no small perturbation has cost above revenue below and revenue above cost above . The maximal stable equilibrium is the largest stable equilibrium. At the price equals , the labor cost per ride-hour.
Independent platform market. AVs serve on their own platform; HVs serve on theirs, with their own minimal fleet . The market price is , and HVs are in equilibrium when
Assume , and
Then every coexistence equilibrium of the independent platform market satisfies
Proposition 4 is the step that separates the two dispatch designs in the paper's main comparison (Proposition 3). On a common platform AVs always lower prices; on independent platforms, under (19), every scenario in which AVs and HVs coexist has a strictly higher price, for a monopoly AV supplier and for perfectly competitive AVs alike. The condition (19) is explicit in the primitives, so it says when fragmentation of dispatch harms riders: when the HV supply is elastic (small ) or the pure-HV demand is low.
The result is proved in the paper, in Appendix D.3. It has no machine-checked proof. The mission produces one, together with reusable facts about the square-root-law-type fleet function : its log-derivative bounds and the sign of the derivative of the labor cost per ride-hour.
The two steps are of different kinds. The comparison rests on the defining property of the maximal stable equilibrium: that revenue falls short of cost at every demand above . That property is not part of the definition of the maximal stable equilibrium. A first idea, comparing revenues pointwise at and , fails without it, because revenue minus cost need not be monotone.
The second step is a sign computation of the derivative of , involving real powers and . The paper's condition is pointwise, while Item 1 needs monotonicity on a whole interval.
All quantities are real numbers; fleet sizes and demand rates are continuous, as in the paper. Real powers are Mathlib's Real.rpow. Statements about the ratio are made only at , where it is differentiable; Lean's value at is a junk . Derivatives are Mathlib's deriv.
Standing assumptions: , (and where the page assumes a density effect), , , , (and where the page assumes finite elasticity). Pinned choices:
A coexistence equilibrium with , or a vacuous one with , is excluded explicitly; with the goal would be false, and dropping positivity of would make (48) trivially satisfiable.
Everything is defined locally in one definition file (the shared market model, repeated in each mission of this series, plus the ratio, the bound and coexistence). Contributions of general lemmas on derivatives of and on largest stable roots of continuous functions are reusable.
Data brokers sell two kinds of products to marketers. A marketing list supplies the contacts a marketer needs in order to act at all; a data append enriches a list the marketer already holds. In both cases the broker can also choose how informative its accompanying analytics are, and it can price a menu of plans of different informativeness to marketers whose costs of acting it cannot observe. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how such a seller should design this menu, and in particular when it should sell more or less information than would be efficient.
The paper first works with a two-point value distribution (Sections 2–3) and then, in Section 4, with a general information structure in which informativeness is ordered by the rotation order of the distribution of the posterior mean (Johnson and Myatt 2006). This mission formalizes the marketing-list result of Section 4.1: Proposition 4 (comparative statics of the efficient informativeness) and Proposition 5 (the optimal screening menu). It is the third mission of a four-mission series on the paper; the first two treat the two-point model, the fourth treats data appends under the rotation order.
A marketer's value from targeting a consumer is unknown. The seller supplies a signal of informativeness . The marketer's posterior mean has cumulative distribution function on a support , with a strictly positive density . Bayesian updating keeps the mean fixed: for every , where is the prior mean. The rotation order (9) requires a point such that
Raising moves probability mass from the middle of the distribution to its tails.
The seller incurs a selling cost , increasing, with . A marketer's targeting cost is with probability and with probability , with . A marketer with cost targets exactly when , so informativeness is worth
With observable costs (the benchmark), the seller sells to type the informativeness maximizing (12), ; a maximizer is an efficient level . With private costs, the seller offers a menu of plans , , with fees . A type- marketer choosing plan gets (13). The seller maximizes subject to individual rationality and incentive compatibility (problem (6)). Its solutions are written .
In general , and if (resp. ), then
The first identity says that the low-cost marketer, the "high type" of the screening problem, receives the efficient informativeness. The second says that the high-cost marketer's informativeness is distorted, upward when both costs lie below the rotation point and downward when both lie above it. Both are stated for every optimal menu and every efficient level.
Proposition 4 states that the value of information to a marketer is non-monotone in the cost of acting: it is largest for costs near the rotation point , where the targeting decision is hardest. Proposition 5 turns this into a pricing rule. In the two-point model the direction of the distortion depends only on the prior (Proposition 2, or ). Under the rotation order it depends on where the costs lie relative to , so a seller facing marketers with low costs over-supplies information to its less profitable segment, and one facing high costs under-supplies it. The comparison with the two-point model (pp. 17–18 of the manuscript) connects the two settings through the single-crossing point of the posterior-mean distributions.
The results are proved in the paper, through integration by parts, signs of derivatives and Topkis's monotonicity theorem. None of them is formalized. Formalizing them checks the reduction of the screening problem, which the paper performs by analogy with the two-point model, including the constraints it drops without comment. It also produces a reusable treatment of rotation-ordered distribution families on an interval. Topkis's Theorem 2.8.4 is already proved on the platform and is part of this mission as a reference.
The obvious argument has two gaps. The first is the reduction (14). The paper substitutes the binding and constraints and drops , and . That the dropped constraints hold at a solution of (14) is not shown in the paper. The second gap is strictness: Topkis's theorem compares maximizers weakly. The strict inequalities require showing that efficient levels are interior and that the first-order conditions differ there. This uses the footnote-5 behaviour of at the endpoints and the mean-preserving property (10), which follows from (9) and the constancy of the mean.
The model is one Lean structure, SellingData.ListsRotation.Model, with real parameters and its standing assumptions as fields. The committed conventions are:
Two further hypotheses are pinned, and only on the statements that need strictness or differentiation under the integral sign:
Optimal menus and efficient levels are sets of maximizers, not chosen maximizers, because need not be convex. "" is the equality of the set of low-cost plans of optimal menus with the set of efficient levels. The goal is stated for the screening problem (6) itself, with all four constraints and nonnegative fees. Defining the optimal menu through (14), or efficient levels through a first-order condition, would make half of the goal a restatement of a milestone, and is ruled out. As on the page, is stated with no condition on the position of the costs relative to ; only the comparison of with carries the two cost ranges. A sorry-free instance shows that the model's hypotheses are jointly satisfiable: , , .
Contributions are welcome on the integration-by-parts and differentiation-under-the-integral lemmas for families of distributions on an interval, which are reusable beyond this paper, and on any milestone in any order.
Many service systems do not receive random, memoryless traffic: customers are given appointments. Outpatient clinics, airport runways, container terminals and delivery slots all schedule arrivals on a regular grid, and the actual arrival deviates from the appointment by a random lateness or earliness. A queue fed by such scheduled traffic is a basic model for these systems, going back to Winsten (1959) and Mercer (1960, 1973), and Chen and Zhao (1997) used it with deterministic service times to model aircraft landings, proving stability under bounded perturbations.
Classical queueing theory says that a single-server queue fed by stationary traffic is stable when the mean work brought per unit time is below the service rate, and unstable when it is above (Loynes 1962). The boundary case, critical loading, is unstable for renewal traffic with non-degenerate interarrival times: the workload grows like . Araman and Glynn ask what happens at critical loading when the traffic is scheduled and every customer brings the same amount of work, and show that the answer depends only on the right tail of the arrival perturbations.
Timeline. Winsten (1959) and Mercer (1960, 1973) analysed queues with scheduled arrivals and obtained waiting-time distributions in implicit form. Loynes (1962) proved the stability dichotomy for stationary input. Kingman (1962) showed that the heavy-traffic limit of the S/G/1 queue coincides with that of D/G/1 when perturbations are positive with finite mean. Chen and Zhao (1997) studied the S/D/1 queue with bounded perturbations. Araman and Glynn (2012) obtained a fractional-Brownian functional limit for scheduled traffic with infinite-mean perturbations, and Araman, Chen, Glynn and Xia (2022) showed that S/D/1 queues with Pareto-like perturbations behave unlike D/D/1 and G/D/1 queues. The present note (arXiv 2022; Operations Research technical note, 2025) settles stability at critical loading.
Fix a probability space and a scheduling interval . Customer is scheduled at time . Its perturbation is a real random variable, and the are independent and identically distributed with . A uniform shift , uniform on and independent of , makes the arrival process stationary. Customer arrives at
and for the arrival count is , so .
A single server works at unit rate and every customer brings exactly units of work (the S/D/1 queue; "D" for deterministic service ). Since one customer is scheduled per time units, the queue is critically loaded. The system is empty at time , and the workload at time is
The proof runs in reversed time. With reversed arrival times , let
Write . " is a bounded random variable" means that almost surely for some constant .
The statement makes no assumption beyond the standing model. In particular the left tail of is arbitrary (only ).
Here count reversed arrivals in of customers and ; are the counts , , and .
The result. Theorem 1 shows that, unlike renewal traffic, scheduled traffic can keep a critically loaded queue stable, and it identifies exactly when: only late arrivals (the right tail of ) can destabilise the queue, while arbitrarily early arrivals cannot. For appointment systems this says that a server whose capacity exactly matches the schedule has a finite stationary backlog precisely when lateness is bounded, so tardiness, not earliness, determines whether waiting times stay bounded. It complements Corollary 1 of the same note, a diffusion limit for random service times at critical loading.
Formalizing it. The theorem is proved in the paper, but its proof contains several misprints: an identity that omits a term and has an infinite summand, a bound with a wrong constant, a sign error in , a false inequality , and a conditional Borel–Cantelli step applied to non-adapted events. The milestones of this mission state the corrected inequalities, each checked by hand on small instances. A machine-checked proof would settle the argument. No part of it is formalized anywhere at present.
The forward workload is not monotone in , so its convergence cannot be read off from its paths; the proof needs the time reversal to a monotone running maximum , and the reversal of a perturbed lattice requires its stationarity under the uniform shift. In the unstable direction the obvious first idea is to show that is large for a fixed large . That fails: for each fixed the overshoot is a tight random variable. Large values occur only along random times at which many customers just after are very late while few customers just before are very early, and producing infinitely many such times needs an ergodic or Borel–Cantelli argument over a dependent stationary sequence. Mathlib has no pointwise ergodic theorem and no conditional Borel–Cantelli lemma, so this step needs new infrastructure.
All declarations live in the namespace ScheduledQueue.Stability. The standing model is a bundle ScheduledInput P ξ U (measurable, i.i.d. via iIndepFun and IdentDistrib, Integrable (ξ 0), HasLaw U uniform on , and independence of U from the whole sequence). Customers are indexed by ℤ, time by ℝ, and is the atTop filter on ℝ. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is a probability measure on .
Conventions that differ from the printed page:
Every count used inside a pointwise inequality is an extended natural number (Set.encard), so that statements such as " a.s." are not satisfied by the junk value of an infinite Set.ncard. The goal's limit is a probability measure on , not on the extended reals, because there "" would also count as convergence. "Bounded" means bounded almost surely, not pointwise. Measurability of is part of the conclusion of the "if" direction, not a hypothesis.
A complete development needs the stationarity and time reversal of the perturbed lattice point process, tail-sum bounds , a pointwise ergodic theorem for i.i.d. shifts (or a Lévy-type Borel–Cantelli argument), and measurability of suprema over intervals. The ergodic theorem and the reversal lemma are reusable well beyond this mission. Proofs of individual milestones, in any order, are welcome.
Financial firms owe each other money. When some firms cannot meet their obligations, the payments that actually clear in the network are a fixed point: what a firm can pay depends on what it receives, which depends on what others can pay. Eisenberg and Noe (Management Science, 2001) introduced this clearing model under a fixed pro-rata payment rule. Later work asked what happens when firms choose how to pay their creditors, which turns the clearing problem into a game.
Bertschinger, Hoefer and Schmand (arXiv:1908.01714v3; Mathematics of Operations Research, 2025) study this game in an abstract form, the flow allocation game. Each node of a directed network receives a fixed external supply plus whatever flows in, and decides how to split its total supply among its outgoing edges, subject to edge capacities. Each node wants to maximize its own total outflow (its payments, which in the financial reading is what keeps it solvent). The paper's first main result is that, when strategies rank single units of flow, there is always a strong equilibrium, stable against every coalition, which is at the same time socially optimal for the total flow.
Timeline:
A flow allocation game consists of a finite directed multigraph , a fixed supply at each node and a capacity on each edge. and are the outgoing and incoming edges of , and .
Every node is a player. A strategy profile assigns to each edge an allocation function : when the tail of has total supply , it forwards units on . The profile is unit-ranking if for all , , : (1); (2); (no fraud, (3)); and each is non-decreasing (5). Equivalently, every node ranks the single units of its outgoing capacity.
A flow gives node the total supply , and is feasible for if on every edge (4). The clearing state of is the coordinatewise supremum of the feasible flows. Player 's utility is , and the total flow is .
A unit-ranking profile is a strong equilibrium if no non-empty coalition has a joint deviation such that is unit-ranking and for all .
The circulation network adds a node , an uncapacitated edge and an edge of capacity for every . An optimal circulation maximizes the total flow over all edges of .
For every flow-monotone (if then ) there is a strong equilibrium maximizing over all unit-ranking profiles.
Strong equilibria rarely exist in network games, and when they do they are usually not efficient. Theorem 9 gives both at once: every unit-ranking game has a strong equilibrium, and one of them maximizes the total flow, so the price of stability for is . Corollary 12 extends this to every flow-monotone welfare function, including egalitarian welfare, Nash social welfare and the number of solvent firms. In the financial reading, a coalition of firms cannot jointly reorder its payments to make every member better off, and the stable payment pattern can be chosen to clear the largest possible volume of debt.
The results are proved in the paper and, to our knowledge, have no machine-checked proof. Formalizing them yields a reusable Lean development of clearing states (the Knaster–Tarski structure of feasible flows), the circulation representation of feasible flows, and integral maximum circulations with a cycle-augmentation argument. The second mission of this series (strong price of anarchy, Theorem 16) builds on the same model.
The obvious argument fails at the deviation step. After a coalition deviates, the clearing state of the new profile is an implicit object: the greatest fixed point of a map that mixes the deviators' new strategies with everyone else's old ones. Nothing ties it pointwise to the optimal circulation, and comparing utilities alone gives no contradiction, because a deviator's gain can be paid for by flow that appears elsewhere in the network. The increase of flow has to be traced through deviators and non-deviators alike, and the two kinds of node obey different constraints.
A second difficulty is that the threshold profile built from an optimal circulation has clearing state exactly . The clearing state is a supremum over all feasible flows, so it is not enough that is feasible. The claim depends on optimality: for a circulation that is not optimal it is false, as a two-node cycle carrying one unit on edges of capacity two already shows.
All data are natural numbers: supplies, capacities, strategies and flows, as the paper prescribes for unit-ranking games (p. 13). The graph is a finite type of edges with tail and head maps, so multi-edges and self-loops are allowed. A profile is one function on edges. The clearing state is the coordinatewise sSup in ; the definition does not assume that the supremum is a feasible flow, which is milestone 1. Optimal circulations are optimal among integral circulations, which the paper justifies by integrality of capacities (p. 23). Natural-number subtraction is used only where it is the page's .
Coalitions are non-empty. With the condition "every member strictly gains" holds vacuously and no profile would be a strong equilibrium; the paper reads it the same way (Proposition 4, Proposition 17). Deviations must again be unit-ranking profiles; the broader deviations of Remark 10 are not formalized. The maximization in the goal ranges over all unit-ranking profiles, not over threshold-ranking ones. A goal maximizing only over threshold profiles, or one that drops the optimality conjunct, is a strictly weaker theorem and is ruled out.
Out of scope: the second sentence of Theorem 9 (polynomial-time computation and polynomial-space representation) and the polynomial-space sentence of Corollary 12. Both need a model of computation. The threshold representation behind them is milestone 4.
A complete development needs: Knaster–Tarski on a finite product of intervals (Mathlib's OrderHom fixed-point lattice), flow conservation bookkeeping on finite multigraphs, existence of integral optimal circulations, and extraction of a cycle from an infinite backward walk in a finite graph. The last two are reusable beyond this mission. Proofs of any milestone, and sorry-free lemmas about clearing states, are welcome.
Two-sided platforms (ride hailing, delivery, freelancing, logistics) collect demand and supply requests over a matching cycle and then clear them with an optimization problem. When such a platform runs an experiment, treated and control units compete for the same supply, so the outcome of one unit depends on the treatment of others. Interference bias of this kind is the subject of Bright, Delarue and Lobel, Reducing Marketplace Interference Bias Via Shadow Prices (arXiv:2205.02274v4; Management Science, 2025). Their analysis of estimators, including the shadow-price estimator built from linear-programming duals, is carried out in a deterministic fluid limit. Theorem 1 of the paper justifies that step: as the market becomes dense, the expected matching value per unit of density converges to the optimal value of a deterministic linear program with the arrival rates as inputs.
The same kind of statement, the expected value of a random linear program converging to the value of the program at the mean data, is also used in network revenue management and in stochastic matching, where fluid linear programs serve as benchmarks.
Network. There are demand types and supply types. A directed network has one demand node per demand type (a sink), one supply node per supply type (a source) and a finite set of intermediate nodes. Every arc carries a value and a capacity .
Matching program. For a density , demand vector and supply vector , is the maximum of over flows with inflow at most at , outflow at most at , flow balance at every intermediate node and (display (2), p. 7). Write . Without intermediate nodes this is a capacitated bipartite transportation problem.
Random counts. Demand units of type arrive at rate and supply units of type at rate . At density the numbers of units collected in one cycle are independent Poisson counts
Treatment effect. If a treatment changes the demand rates from to (with ), the global treatment effect at density is (Definition 1, p. 8).
for every network, every and every , along integer densities . No rate of convergence and no constant is fixed.
Theorem 1 is the bridge between the paper's stochastic model and its deterministic analysis. Corollary 1 follows from it and identifies the estimand . Every fluid-limit result of the paper is stated about this deterministic quantity: that the RCT estimator overestimates the treatment effect (Theorem 2), and that in a symmetric experiment the shadow-price estimator is no more biased than the RCT estimator (Theorem 4). Without Theorem 1 those results describe a linear program, not the experiment.
The result is proved in the paper (Appendix C.1, pp. 37–39). As far as a search of the Prove2Me catalogue shows, it has not been formalized: the catalogue has fluid limits of queueing networks and several Poisson concentration bounds, but no law of large numbers for the value of a random network-flow program. A formal development would provide a reusable definition of the capacitated network-flow program with supply and demand bounds, its scaling identity, and an integrability tool for suprema of scaled Poisson counts. The two other missions of this series, on the shadow-price estimator in the fluid limit and in finite samples, use the same network program.
The obvious argument is: and , is continuous, so the expectations converge. Each step needs care.
Representation.
Fin nd and supply types Fin ns; Lean index is the paper's type .E and intermediate-node type I. Each arc's tail is a supply or intermediate node and its head is a demand or intermediate node, which builds in the source/sink structure. Values are real and capacities nonnegative.Probability.
Ruled out. A trivializing formalization is excluded: the expectation is taken against the Poisson laws with means and , with the factor inside the expectation, not against point masses at the rates or in the rescaled form . No hypothesis beyond is imposed.
Not stated.
The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed in each item's Formalization Note.
Infrastructure needed.
The network-program definition and the Poisson tail bound are reusable beyond this mission. Contributions toward any of these are welcome.
Global sensitivity analysis asks how much of the uncertainty in the output of a model, a simulator or a learned predictor is attributable to an input . A standard way to answer is to compare the law of with its law after is revealed, and to average that discrepancy over . Variance-based indices (Sobol' 1993; Wagner 1995) compare conditional and unconditional means. Density-based and distribution-based indices compare whole distributions. Rényi's postulates for measures of dependence ask, among other things, that such an index vanish exactly under independence (zero-independence) and reach its maximum exactly when is a function of (max-functionality, Postulate E). Variance-based indices fail the first postulate, because the conditional mean can be constant while the conditional law moves.
Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose indices in which the discrepancy is an optimal transport cost. The squared 2-Wasserstein case is the numerator of the Wasserstein correlation coefficient of Wiesel (2022), whose Theorem 2.2 gives max-functionality for that coefficient. The paper extends max-functionality to general continuous costs, through a strict-convexity property of the transport cost on Dirac masses (Lemma 4). This mission formalizes that result, Theorem 5, together with the zero-independence property, Proposition 3.
Let be a probability space and , Polish spaces with their Borel -algebras. The input and the output are measurable, with laws and .
A cost is a continuous function with if and only if . It need not be symmetric, a metric, or finite. For probability measures on , a coupling is a probability measure on with marginals and , and the optimal transport cost is
For a sub--algebra of the Borel sets of , a version of the conditional distribution of given is a Markov kernel that is -measurable in and satisfies for and Borel . The OT-based sensitivity measure of Definition 1 is
written when is the full Borel -algebra. The candidate maximum is
with an independent copy of ; for it equals twice the total variance of .
If , then for every sub--algebra and every version of the conditional distribution,
and
The steps of the paper's proof, in order:
The result. Together, Proposition 3 and Theorem 5 place on a scale from (no information about in ) to (complete information), so the ratio is a normalized measure of association. This normalization is what lets practitioners rank inputs of a simulator or features of a model on a common scale. The result covers all continuous costs vanishing exactly on the diagonal, including the powers of a metric that give the Wasserstein indices, and arbitrary sub--algebras , which model partial information about (for example the information carried by a function ).
Formalizing it. The theorem is proved in the paper; the work here is to formalize the known proof. As far as is known, no machine-checked version of this result or of Wiesel's Wasserstein-correlation theorem exists. Along the way the development needs facts about optimal transport with extended-real costs that are not in Mathlib: the product-coupling bound, the transport cost to a Dirac mass, convexity and lower semicontinuity of , and cyclical monotonicity of optimal plans.
The inequality and the "functional dependence ⇒ equality" direction are direct computations with the product coupling and with Dirac conditional laws. The converse is the hard direction. Equality of the integrals gives only the pointwise equality (63) almost everywhere, and the step from there to " is a Dirac mass" needs strict convexity of . Strict convexity fails for general measures: is affine along many segments. It holds only between Dirac masses at distinct points of (Lemma 4), and even there it fails when the costs involved are infinite. A non-Dirac conditional law is not a two-point mixture, so the strict inequality must be carried over to general measures with an integrand that takes values in . The last step, building an -measurable from the conditional laws, is measure-theoretic bookkeeping that is easy to get wrong.
ℝ≥0∞), so is allowed as on the page, and integrals are lower Lebesgue integrals.RWPI.SqrtLasso.transportCost. Its first argument is the marginal , and the cost is evaluated as with .IsCondDistrib is admissible, and every theorem quantifies over all versions and over all sub--algebras .Thompson sampling (TS) is the standard randomized heuristic for the Bayesian multi-armed bandit: at each decision it samples a parameter vector from the current posterior and pulls the arm that would be best if the sample were true. It ignores the remaining horizon. Min, Maglaras and Moallemi (arXiv:1902.04251, Management Science, 2025) obtain horizon-aware generalizations of TS from the information relaxation duality of Brown, Smith and Sun (Oper. Res. 2010). Each penalty function yields an upper bound on the Bayes-optimal value and an IRS policy. Such a policy samples a whole future outcome and plays the first action of the penalized clairvoyant optimum. With the zero-information penalty it is exactly TS.
Two of these policies, IRS.FH and IRS.V-Zero, are designed to interpolate between TS and the myopic rule. When one period remains they pull the arm with the highest predictive mean (Remark 5 of the paper). This mission formalizes the other end, Proposition 1: when many periods remain, they randomize exactly as Thompson sampling does. The paper presents this as the sense in which IRS policies "behave like TS during the initial decision epochs" and shift smoothly from exploration to exploitation without a tuning parameter.
There are arms . Arm has an unknown parameter . Given , its rewards are i.i.d. with law . The prior of is , a member of a conjugate family indexed by a belief . A Bayesian update maps to the posterior belief after a reward . The arms are independent. Throughout, rewards are integrable: for every belief (display (3)).
At remaining horizon and belief , the three policies act as follows:
It then plays the arm to which the optimal allocation assigns the most pulls.
Each action is a random variable driven by the policy's own sample.
Assume almost surely under , for all . Then for every arm ,
This holds for every choice of the tie-breaking rules in the argmaxes and in the allocation problem.
Proposition 1 identifies the long-horizon behaviour of the two IRS policies with that of Thompson sampling. Together with Remark 5 it pins down both ends of the horizon. It explains why their simulated regret curves track TS early and the myopic policy late (§5 of the paper). It also shows that the design choice "play the arm with the largest allocation" in IRS.V-Zero is the one that recovers TS. Other selection rules, such as any arm with a positive allocation, need not.
The paper gives a complete proof in Appendix D.1–D.2. A machine-checked version adds three things. It fixes the probabilistic model of a conjugate Bayesian bandit with infinite reward sequences in Lean, which the companion missions on the same paper also need. It makes the role of tie-breaking explicit. And it repairs a step of the printed proof: the bound in §D.2 holds only for two arms, and the general case needs and a threshold growing with . No formalization of this result is known on Prove2Me or in Mathlib.
The IRS.FH half reduces to almost-sure convergence of posterior means, which is a martingale argument (Lévy's upward theorem). That argument needs to be measurable with respect to the limit -algebra of the reward sequence, a fact supplied by the strong law of large numbers. Building the outcome law, a mixture over of infinite product measures, and identifying the conjugate update with conditional expectation are where the measure theory lies.
The IRS.V-Zero half does not follow from convergence of the posterior means alone. The selected arm is a function of an optimal allocation of a combinatorial problem whose size grows with . The naive expectation that the arm with the best limit receives "most" pulls has to be proved by an exchange argument that handles the finitely many early terms, where the posterior means can still be badly ordered. The printed version of this argument is correct only for .
Fin K with NeZero K; the reward sequence of an arm is ℕ → ℝ, 0-based.The development needs Lévy's upward theorem (MeasureTheory.tendsto_ae_condExp in Mathlib) and the strong law of large numbers (ProbabilityTheory.strong_law_ae). It also needs a lemma identifying iterated conjugate updates with the posterior given finitely many rewards, and the measurability of . These last two are reusable for any Bayesian bandit or sequential-estimation development. Contributions of the two deterministic milestones are self-contained and welcome first.
Round-Robin is the simplest allocation rule for indivisible goods: agents take turns, in a fixed order, picking their favourite remaining good. When agents have additive valuations and report them truthfully, the outcome is envy-free up to one good (EF1) — every agent values its own bundle at least as much as any other bundle with one good removed, a notion going back to Lipton et al., 2004 and Budish (2011) — which makes Round-Robin a standard baseline in fair division (Markakis, 2017). The mechanism, however, only sees reported rankings, and agents can gain by misreporting; without monetary transfers no truthful mechanism has a meaningful fairness guarantee even for two additive agents. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) therefore study equilibrium fairness of Round-Robin when valuations go beyond additive. This mission concerns their fairness result for submodular valuations: strategic play does not destroy fairness, it only degrades it by a constant factor.
Timeline. Aziz, Goldberg and Walsh (ADT 2017) proved that Round-Robin always has a pure Nash equilibrium for additive valuations. Amanatidis et al. (WINE 2021) initiated the study of equilibrium fairness and showed that, for additive valuations, Round-Robin has equilibria and each of them yields an EF1 allocation with respect to the true valuations. The 2023 paper extends equilibrium existence to cancelable valuations (exact PNE) and submodular valuations (1/2-approximate PNE, with 1/2 tight), and proves that approximate equilibria are approximately EF1: factor for submodular and for subadditive cancelable valuations.
There are agents and a set of goods. Agent has a valuation that is normalized () and non-decreasing. The marginal value of a good with respect to a set is , and is submodular if whenever and .
Each agent reports a ranking , a total order on . Round-Robin runs steps; in step (counted from ) agent receives its -top good among those still unallocated. The result is an allocation . An allocation is -EF1 if for all agents with some satisfies . A profile is an -approximate pure Nash equilibrium (PNE) if no agent can, by reporting any other ranking , obtain a bundle worth more than times its current one:
In Lean the objects are marginal, IsValuation, IsSubmodular, IsRanking, roundRobin, IsApproxEF1 and IsApproxPNE in RoundRobinEq.SubmodularEF1.Setting; the step-to-agent map agentAt n t = t % n comes from the shared module RoundRobinEq.CancelableBluff.Setting.
For and submodular valuations, every -approximate PNE of Round-Robin yields an allocation that is -EF1 with respect to the true valuations:
Companions (not milestones): Lemma 4.1 (the greedy response is 1/2-EF1 from the deviator's perspective) and Theorem 4.2 (two agents: ).
The theorem says that fairness of Round-Robin is robust to strategic misreporting for a class far beyond additive valuations: whatever approximate equilibrium agents settle in, each agent's envy up to one good is bounded by . Combined with the existence of a 1/2-approximate PNE (Theorem 3.7 of the same paper), it gives an equilibrium that is 1/6-EF1. Lemmas 4.6 and 4.7 are statements about two runs of Round-Robin that differ in one agent's report; they involve no valuations and are reused verbatim for subadditive cancelable valuations (Theorem 4.5).
The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The mission builds a finite fair-division layer (Round-Robin as a step-by-step process, rankings, α-EF1, approximate PNE) that does not exist in Mathlib, and checks the combinatorial coupling of two runs, which is where the paper's argument carries its weight.
The obvious argument compares agent 's equilibrium bundle with its bundle after a good deviation (Algorithm 4's greedy response) and then compares that with agent 's bundle. With two agents everything not in or goes to , and this closes the argument. With agents the deviation reshuffles goods among all other agents, and there is no direct control on what ends up holding relative to the deviation run. The proof needs a global statement (Lemma 4.6) about how much two Round-Robin runs that differ in one report can diverge before each of 's turns, and then a careful indexing of by allocation time in the other run, so that a counting bound turns into the good-by-good inequality (2). The bookkeeping of steps, rounds and two simultaneous runs is the main work.
Fin n with , 0-based; goods a finite type M. The paper's standing simplification (p. 7) is a hypothesis Fintype.card M = k * n of every theorem; the paper's reduction to this case (dummy goods) is not formalized.allocBefore σ (r*n + i), and the paper's bounds for , , appear as for .Trivializing formalizations are excluded: deviations over arbitrary lists (which would strengthen the hypothesis), , EF1 computed on reported rankings instead of the true valuations, or the EF1 witness fixed in the goal statement would each change the theorem, and none is used.
Contributions welcome: proofs of Lemma 4.6 by induction on rounds (the reusable core), basic API for allocBefore/roundRobin (every good is allocated once, ), and Theorem 2.1.
Data brokers sell consumer data to firms that use it to decide whom to target, whom to lend to, or where to open a store. Two kinds of products are common: a marketing list, which supplies contact information without which the buyer cannot act at all, and a data append, which enriches information about consumers the buyer can already reach (Federal Trade Commission, Data Brokers, 2014). A seller who does not know a buyer's cost of acting must screen buyers with a menu of plans that differ in price and in how informative the data are.
Liang Guo's paper Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) characterizes the optimal menu, first for a binary-value model (§3) and then for a general information structure ordered by rotation (§4), following Johnson and Myatt (2006). This mission formalizes Proposition 7: data appends under the rotation order. It is the fourth mission of a series built from the same manuscript; the first three cover marketing lists and data appends in the binary model and marketing lists under the rotation order.
A marketer can take an action (target a consumer) at cost ; the action's value is uncertain with prior mean . A data service of informativeness produces a signal, and its information is summarized by the posterior mean . For each , has cumulative distribution function on a support , with a strictly positive density and mean for every . The family is rotation ordered: there is a point with
A more informative service spreads the posterior mean away from .
A service plan charges a fixed fee . Serving a marketer with informativeness costs the seller , with and increasing. A marketer targets exactly when , so a marketer with cost who buys earns
Costs are with probability and with probability , . A data-append buyer can act without the data, so its outside option is .
The seller offers a menu and maximizes subject to individual rationality and incentive compatibility for both types. Call any maximizer an optimal menu, with levels . The benchmark with observable costs is
and its maximizers are the efficient levels .
Assume . If , then
and if , then
Here means that the set of -levels of optimal menus equals the set of efficient levels, and each strict inequality holds for every optimal menu and every efficient level.
Proposition 7 is the general-distribution form of a "double reversal". With marketing lists the low-cost marketers are the high type: they get efficient information, and the high-cost marketers' information is distorted (Proposition 5 of the paper). With data appends and costs below the prior mean, the outside option makes the high-cost marketers value data more. The roles of the types swap, and the direction of the distortion flips with the position of the costs relative to the rotation point. The result tells a data seller which customers to under- or over-supply, and shows that the answer depends on whether its data enable an action or only refine it.
The paper proves the result on a few pages, partly by phrases such as "it can be readily verified". No machine-checked version exists. A formalization makes explicit what the printed argument leaves implicit: that the dropped constraints hold at the reduced optimum, which regularity of and the strict inequalities need, and that statements about "the" optimum hold for every optimum when maximizers are not unique.
The obvious approach substitutes the binding constraints and compares first-order conditions. Two steps of it fail as stated. First, the reduction to (15) drops and ; holds at a maximizer of (15) only when the two informativeness levels are ordered as the rotation order dictates. That ordering is available only when both costs lie on the same side of . Second, first-order conditions say nothing at a corner of . The strict comparison needs the efficient level to be interior, where the derivative of exists. That comes from the conditions of footnote 5 together with the mean-preserving property of the family. The selling cost need not be convex, so maximizers can be non-unique, and every comparison must hold for every pair of maximizers.
RotationFamily with a bounded support (the paper allows an unbounded one). is continuous on with , and derivative , continuous on the closed support. exists on the closed support. The rotation order (9) holds on the open support, and the mean is for every . Condition (10) is not assumed; it follows.Model extends it with , , and with both costs in (a pin: the integrals presume it). It also fixes with monotone on . is written as .3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the input-size exponent, rather than an experimental speedup, is the quantity being studied.
Alman and Vassilevska Williams (2026) give a deterministic truly subquadratic integer 3SUM algorithm through thin matrix products and reductions involving Exact Triangle. Xu's manuscript, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, dated 13 October 2026, refines the analysis of that framework. Its claimed bound is the formalization target here. The Hexagon link identifies the author's submission page, which may require authentication; it is not presented as a public article identifier or evidence of peer review.
An input of size is a function . For a fixed natural number , every entry obeys . Acceptance means that there are pairwise distinct indices with . Repeated values at different positions are allowed. This is a decision problem, so the algorithm need not return a witness triple.
The word-RAM specification is the campaign's existing EndStatement definition, imported from its foundation mission. For each fixed , one finite deterministic program, one word-width threshold constant, and one time-bound function must work for all input sizes and all word widths above that threshold. Words have finite signed interpretations; arithmetic, indirect memory access, branching, acceptance, and rejection are defined operationally. The result concerns this exact model.
For the supporting analysis, let , with endpoint values . All logarithms are natural. For an integer , a positive integer , and , set , , , and
The sharp preprocessing saving, query exponent, and encoding exponent are
These auxiliary definitions describe costs; they neither redefine 3SUM nor assume the existence of a fast algorithm.
The campaign goal is the exact fixed bound
The first supporting milestone is the two-sided binomial entropy estimate. The second is the manuscript's normalized tail bound
A further milestone establishes strict improvement over the earlier preprocessing saving at fixed parameters. The algorithmic milestone combines the manuscript's Propositions 4.1 and 5.1: admissible sharp-tail parameters must yield a program satisfying the shared 3SUM specification, not merely a numerical inequality.
The final supporting milestone certifies the exact choice
It includes the preprocessing, query, encoding, prime-selection, and instance-construction inequalities, together with
Every terminating decimal denotes an exact rational number. The target is the fixed big- exponent 1.999017; the smaller cutoff is accompanied by residual asymptotic losses in the manuscript and is not asserted as the same fixed bound.
A complete proof would certify the manuscript's improved integer 3SUM bound in the campaign's common machine model. The gain is an analysis refinement of the inherited algorithm and reductions. It does not claim a new algorithmic framework, optimal parameters, global optimality, or priority over all other work.
The manuscript also gives an auxiliary bound by retuning the previous estimate. That weaker result is background, not this mission's campaign value. The existing upstream formalization is prior work; it does not automatically certify either refinement. The supplied rational interval verifier checks the parameter inequalities, but those checks alone do not prove a word-RAM running-time theorem. The main goal and the newly drafted supporting statements remain open Lean proof obligations.
A better tail estimate is insufficient unless every other cost remains within the final budget. Shared encoding work, all queries, deterministic prime selection, witness scanning, and instance construction must be included. The word-size and address bounds must remain valid after changing parameters. Ceiling operations, restricting to powers of four, and bounded-size exceptions must also be handled.
The central formalization burden is the connection between the analytic estimates and an actual deterministic program. Assuming an oracle with the desired running time would remove that burden and would not establish the stated target. Likewise, checking a finite range of sizes or a floating-point optimizer's output cannot establish the universal algorithmic statement.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The foundation reference and the campaign goal's import are retained. Supporting definitions use real logarithms, real powers, natural binomial coefficients, finite sums, and a natural ceiling. Domain hypotheses exclude invalid entropy-tail regimes; endpoint binomial cases are included explicitly.
For , the shared time predicate means that there exists such that for every . Correctness and termination still cover every input size, including . The manuscript's convention must be extended to the campaign's case, and its word-size analysis must justify uniform correctness at every sufficiently large word width. Both are explicit interface obligations.
Reusable contributions include entropy and tail estimates, rigorous logarithm enclosures, and parameterized cost-to-program results. Existing compatible library results should be reused where available. The manuscript and metadata were prepared with AI assistance; this mission makes no claim of completed human review or completed formal verification of the improved bound.
EndStatement.lean supplies the shared specification, not a proof of this mission's new exponent.A two-stage adjustable robust linear program chooses a first-stage decision before an uncertain right-hand side is revealed, and a second-stage (recourse) decision afterwards, minimising the worst case over an uncertainty set of the total cost. Computing the optimal value is hard in general (Feige et al., 2007), and the standard tractable restriction is to affine policies (Ben-Tal et al., 2004), whose optimal value is computed by a single linear program.
El Housni and Goyal (arXiv:1807.00163v2) show that, when the recourse matrix is non-negative and is a budget of uncertainty set, is within a factor of . Their Section 7 asks whether the non-negativity of is needed, and answers with a family of two-stage lot-sizing instances whose recourse matrix is a network matrix with entries in . On this family the adjustable problem has value while every affine policy costs at least . Lot-sizing and transportation recourse are among the most common uses of two-stage robust optimisation (see Bertsimas and de Ruiter, 2016), so the instance is a natural one, not an artefact.
Lower bounds on the gap between affine and adjustable policies were known before (Bertsimas and Goyal, 2012); the point of the present family is that the adjustable value is exactly , so the ratio is infinite and the difference grows linearly in .
The lot-sizing problem (7.1). There are nodes. Node stores inventory at cost per unit, up to a capacity , and faces an uncertain demand . After is revealed, inventory may be shipped from node to node in amount at cost per unit. A solution is feasible when and, for every ,
The objective is the first-stage cost plus the worst case over of the transportation cost . The optimum over all rules is , and the optimum over affine rules (one row of per arc, one column per node) is .
The family (7.2). Let , and split the nodes into and with . Set on and on , everywhere, for , , and otherwise. The uncertainty set is
Inventory can thus move only from to , at no cost; stocking is free and stocking costs one per unit.
In the Lean development the general problem is the structure LotSizing N E (nodes N, usable arcs E with tail src, head tgt, distances d), with the predicate Feasible, the cost cost, and the sets adjustableValues, affineValues of objective values. The family is lotSizingFamily k, on nodes Fin k ⊕ Fin k and arcs Fin k × Fin k.
For every ,
each stated as IsLeast of the corresponding set of objective values, which asserts that the value is attained and is the minimum. The unboundedness of the gap, , is immediate.
The result. The approximation guarantees of the paper ( for budget sets, for disjoint constrained budgets) assume . Lemma 7.1 shows that this assumption is not a convenience of the proof: with a network recourse matrix no bound on of any form holds, even for a budget set and a bipartite network. Any extension of the guarantees to transportation or flow recourse must therefore change the policy class or add structure, which is the open direction the paper states after the lemma.
Formalizing it. The lemma is proved in the paper; it has not been machine-checked. The mission produces a reusable definition of the two-stage robust lot-sizing problem with arc-based recourse, the precise instance family, and checked versions of the five steps of Appendix D. Two of those steps hold only for and one is printed with its indices swapped (see the scope section); the formal statements make those boundaries explicit.
The adjustable half is a transportation argument, and the affine upper bound is a direct verification of one explicit solution. The substance is the affine lower bound, which must hold for every feasible affine solution, not for a particular one. Comparing an affine policy with the adjustable optimum on a few extreme scenarios gives nothing: on any single scenario an affine policy can match the adjustable cost. What fails for affine policies is simultaneous feasibility over the whole of , and the lower bound has to extract a cost from that requirement alone. It is also sensitive to the size of the instance: two of the intermediate steps of Appendix D are false for , so a formal proof has to treat small separately.
IsLeast. No real infimum is used, so "" cannot hold on an empty feasible set; feasibility includes , on all of , and the coverage constraint at every node, including the outflow constraint (D.2) at .LotSizing (any node set, any arc set, any uncertainty set) can host other two-stage lot-sizing and transportation results. Proofs of any milestone, and alternative arguments for the affine lower bound, are welcome.The source is arXiv:1807.00163v2; its printed page numbers equal the PDF's.
Superconducting circuits built from capacitors, inductors and Josephson junctions are the dominant platform for current quantum processors (Google, IBM, Rigetti, IQM and others). The source article — the Wikipedia entry Superconducting quantum computing — states two facts about the gate model on this hardware that this mission makes precise:
Statement 2 is a mathematical theorem, not an engineering claim: it says that every unitary operation on qubits can be written exactly as a finite product of the hardware's elementary gates. Its classical form with CNOT as the two-qubit gate is due to Barenco et al. (1995); the iSWAP version follows because CNOT can be built from two iSWAPs and single-qubit gates (Schuch–Siewert 2003).
Timeline.
An -qubit register has computational basis states labelled by bit strings ; its operations form the unitary group . For a unitary and a qubit , the single-qubit gate applies to qubit and leaves the others unchanged. For a matrix and an ordered pair of distinct qubits , applies to qubits (qubit is the first tensor factor). Write
The gates used are
in the basis , and the Toffoli gate . Time evolution under a Hamiltonian is , and the coupling Hamiltonian is . A two-level unitary acts as the identity outside the span of two basis vectors.
For every ,
The goal theorem is the formal justification for compiling arbitrary quantum algorithms to superconducting hardware whose native entangling interaction is of XY/iSWAP type: any target unitary, however large, has an exact decomposition into the hardware's elementary operations. Milestone 1 connects the abstract gate to the physical Hamiltonian; milestones 3–4 are the textbook universality theorem in the CNOT form, reusable for any other two-qubit gate that can synthesise CNOT; milestone 5 is the Toffoli construction mentioned in the source.
All results are classical and proved in the literature. To the best of the drafter's knowledge they are not yet available as machine-checked statements in Mathlib in this form; the mission's contribution is a complete formal development.
The naive route — "decompose into two-level unitaries, then implement each with gates" — hides real work: a two-level unitary on basis states with differing in many bits must be conjugated by a Gray-code sequence of controlled-NOT style gates into one acting on a single qubit, controlled on all others, and multiply-controlled single-qubit gates must then be reduced to single-qubit gates and CNOTs. Keeping indices, tensor embeddings and controls consistent over qubits is the main formal burden. Milestone 1 requires computing a matrix exponential exactly, which in Lean means handling NormedSpace.exp on a non-diagonal matrix.
Fin n → Fin 2; two-qubit operators are indexed by Fin 2 × Fin 2 with the Kronecker product ⊗ₖ, first factor = first qubit.Subgroup.closure) inside Matrix.unitaryGroup equals ⊤; no approximation or topological closure is involved, which is why the full continuous family of single-qubit gates is included.onQubit, onPair) and multiply-controlled gates are reusable for any quantum-circuit mission.