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?
Generous return policies raise demand, but they also invite opportunistic returns: customers who buy a product intending to use it briefly and return it for a refund. Retail-industry surveys put the share of such "wardrobing" or renting customers near a tenth of all customers, and retailers answer with restocking fees, return windows, or analytics services that flag suspected renters. Altug, Aydinliyim and Jain (SSRN 3283334; Management Science, 2021, doi:10.1287/mnsc.2020.3777) compare three ways a retailer can set prices and refunds in this situation. Their model extends Su's newsvendor model of consumer returns (Su 2009), in which every customer is an honest returner who returns only after learning that the product does not suit him, and the optimal refund equals the salvage value. The question is whether a retailer who cannot tell renters from honest customers can still do as well as one who can.
A retailer stocks units at unit cost , sells at price , refunds per returned unit, and salvages leftover units at . Aggregate demand is random. A fraction of customers are renters, the rest are honest returners.
The fraction of customers who transact is . A decision with marginal net revenue earns
The three proposals are:
Write for the three optimal profits and for an optimal uniform refund. Without renters the optimal refund is the benchmark .
together with the existence of an optimal uniform decision. Hence . This is a corrected Proposition 6 (p. 17). As printed, part (b) is an equivalence and part (c) says when . That fails: in the setting of the paper's Figure 1 with , and , the uniform optimum has and prices renters out, while targeted refunds earn strictly more, and so does the menu.
In attack order: the closed form (5b) of the binding price; the first two claims of Lemma 1; the benchmark refund as a strict maximizer of the honest margin; the upper bounds ; Proposition 4's (10b)–(10c); the strict gain when ; Proposition 4's last sentence, ; the §7.1 claim that gives ; and Proposition 5's price-refund choice in (12b)–(12c), with its consequence for optimal profit.
The result says when screening by a price-refund menu is as good as identifying customers. A retailer that can segment customers only by paying an analytics firm learns that the payment buys nothing exactly when its optimal uniform refund is at least the salvage value, and that otherwise the menu degenerates to a single uniform policy. Figure 1 of the paper maps the regions in where each case occurs.
The proofs of Propositions 1 to 11 sit in an electronic companion that is not part of the working paper, and the printed Proposition 6 is false at the boundary . A machine-checked proof therefore settles the corrected statement independently of the missing appendix. No part of the paper has been formalized before.
Each program is a joint optimization over stock, price and refunds, with the stock entering through a newsvendor term whose coefficient depends on the refunds. The comparisons are between suprema of different programs, not between first-order conditions. The obvious approach, comparing the closed forms of Propositions 1, 4 and 5, does not work: Proposition 1 rests on the hypothesis that is decreasing, which no distribution with a density on satisfies, and its threshold is only asserted to exist. The case is the hard one: it requires showing that the menu's incentive constraints force it back to a uniform policy, which depends on the shape of the targeted profit in the rental fee and hence on the IGFR assumption.
LariviereIGFR.Char.IsIGFR). Demand is a probability law on with finite mean, and is SupplyChainTheory.expSales.Customer abandonment, or reneging, is a basic feature of service systems: call centres, emergency departments and online platforms all lose customers who give up waiting. The number of reneging customers is a natural performance measure, and in many-server and single-server models alike it is the quantity managers monitor and are penalised for. Typical (law-of-large-numbers) behaviour of reneging is well understood; the question here is how unlikely atypical amounts of reneging are, over long horizons.
R. Atar, A. Budhiraja, P. Dupuis and R. Wu (arXiv:1903.06870; Mathematics of Operations Research, 2022) answer this for the single-server queue with exponential patience, in the many-arrivals scaling. They prove a sample-path large deviation principle for the pair (queue length, cumulative reneging) and then solve the associated long-horizon variational problem in closed form. The answer has a counter-intuitive feature, which the authors call the reneging paradox: the exponential decay rate of the probability of observing reneging at an atypical long-run rate does not depend on the reneging rate . Customers who are very patient and customers who are very impatient produce, over long horizons, the same large-deviation cost for the same atypical reneging rate.
Fix rates (arrival, service, per-customer reneging), an initial queue length and a horizon . Throughout the mission (the paper's standing assumption from §2.2 on). The Skorohod map on is
and the local cost is for .
A path is a pair of continuous functions ; is the queue length and the cumulative number of reneged customers, both on the fluid scale. A control is a triple of measurable maps that perturb the arrival, service and reneging rates; it is admissible for , written , if for all
The rate function is
equal to when no control is admissible. The cost of seeing reneged customers by time is
with the one-sided versions (constraint ) and (constraint ). Finally
The limit depends on only; and appear in the hypotheses and inside , never in .
The milestones follow the paper's proof, in order:
The theorem gives the exact long-horizon decay rate of the probability of atypical reneging in the queue, in closed form, together with the explicit optimal path for . It shows that the patience parameter, which governs typical reneging, is invisible in the long-run large-deviation cost of atypical reneging. The paper treats the many-server analogue in its §7; that part is not in this mission.
The result is proved in the paper. None of it is formalized: Mathlib has no sample-path large deviations and no Skorohod problem, and the platform has no rate function for a reflected, state-dependent jump process. This mission formalizes the deterministic, variational half (§§4–6) of the paper; the probabilistic LDP itself (Theorem 2.1, proved in §3) is not a target.
The variational problem has a state-dependent cost () and a reflection constraint, so the obvious approach of guessing a constant-rate tilt and checking it fails: the optimal path is not linear, its constants solve the transcendental equation (5.9), and the minimizer must be shown to stay in the interior for large , which happens only beyond a horizon that genuinely grows with the data. The case , where the explicit candidate is not shown to be optimal, and , where the reflection at zero is active, need separate arguments (Propositions 6.3 and 6.4). The final passage from to the one-sided problems relies on the shape of (Lemma 6.1).
All declarations live in the namespace RenegingLD.MM1, in two definition files (Model for §2, Variational for §§4–6) and one theorem file per statement. The conventions are:
lam, mu stand for . The standing assumptions , , and are explicit hypotheses of every statement that needs them.deriv, the a.e. derivative on .A trivializing formalization is ruled out: the costs are lower integrals, so a non-integrable control cannot have cost zero; is off continuous paths; and the goal quantifies over every path through , and , not over the explicit candidate, for every and every in the paper's ranges.
A complete development needs absolutely continuous functions and the fundamental theorem of calculus for them (present in Mathlib), the one-dimensional Skorohod problem, convexity of perspective functions, and a first-variation argument for convex integral functionals. The Skorohod-map and perspective-convexity lemmas are reusable beyond this mission. Contributions of proofs of any milestone, including partial results such as the or cases of the goal, are welcome.
In a communication network, file transfers ("flows") share the capacity of the links on their routes, and the bandwidth-sharing policy decides how much rate each flow receives. The connection-level model of Massoulié and Roberts (2000) treats flows as customers that arrive at random, carry a random amount of data, and leave once it is transferred. Under weighted proportional fairness (Kelly 1997; Mo and Walrand 2000), the rates maximise subject to the link capacities. Its delay performance in steady state, measured by the expected numbers of flows on the routes, is the quantity a network operator cares about.
Most heavy-traffic results for this model are diffusion approximations: Kang, Kelly, Lee and Williams (2009) under a local-traffic assumption, Ye and Yao (2012) under a full-rank routing matrix, with interchange of limits by Shah, Tsitsiklis and Zhong (2014) and Ye and Yao (2016); all assume exponential file sizes. Vlasiou, Zhang and Zwart (2014) obtained the diffusion limit for phase-type sizes. Whether the stationary flow counts depend on the file-size distribution beyond its mean (insensitivity) is the central practical question, since real file sizes are far from exponential. Wang, Maguluri, Srikant and Ying (arXiv:1808.02120, 2021; Math. Oper. Res. 2022) answer it in heavy traffic with explicit bounds, using the Lyapunov drift method instead of diffusion limits.
There are links with capacities and routes ; the routing matrix has if link is on route and otherwise, has full row rank, and every route uses some link. Flows arrive on route as a Poisson process of rate . Their sizes are i.i.d. with a phase-type law in the class : the absorption time of a Markov chain whose transient phases form Erlang blocks with pairwise distinct rates , started with positive probability in the first phase of every block. With subgenerator and initial law , the mean size is and the route load is . The class is dense in the distributions on .
Given the numbers of flows on the routes, the weighted proportionally fair allocation with weights gives each flow on route the rate solving
The state counts the flows of route in phase ; it is a continuous-time Markov chain: arrivals into phase at rate , phase changes at rate , and completions from phase at rate .
Heavy traffic. Fix on the boundary of the capacity region: for all links, with equality exactly on the nonempty set of critically loaded links, . The -th system has arrival rates , , and denotes a random vector distributed as its stationary distribution, with route totals .
The leading constants depend only on the number of critical links and the weights, not on the file-size laws in .
The proof is organised around a new inner product on the phase-level state space (67). In attack order:
The result. The bound is linear in the number of critical links, not routes, and holds without the local-traffic assumption. With equal weights the two sides coincide and give the exact heavy-traffic limit for every file-size law in : proportional fairness is heavy-traffic insensitive. As a by-product, state-space collapse yields the interchange of limits for the diffusion approximation of Vlasiou, Zhang and Zwart (Theorem 5 of the paper, not part of this mission).
Formalizing it. The paper's results are proved on paper; no part of this argument is machine-checked. A formalization yields reusable pieces beyond this paper: the continuous-time Bertsimas–Gamarnik–Tsitsiklis tail bound (Lemma 10), steady-state "zero expected drift" arguments for countable-state chains, and the matrix analysis of phase-type laws (Lemmas 5, 6, 11). The paper's own proof of Lemma 6 contains an incorrect step (a hazard-rate claim that fails for Erlang blocks), so a checked proof of that lemma is itself a contribution.
The drift method needs a Lyapunov function whose drift is negative along the directions the process actually moves. For exponential sizes the diagonal inner product of (9) suffices. With phase-type sizes the natural Euclidean or diagonal inner products fail: the rotation by produced by phase changes can make negative, so (P2') breaks. The integral construction (67) of is what restores it, and checking that is positive definite requires a controllability (PBH) argument. On the probabilistic side, every step "in steady state the expected drift is zero" requires integrability of an unbounded Lyapunov function under the stationary law of a countable-state chain, which must first be established from the tail bounds; Mathlib has no ready theory for this.
All objects are in the namespace HTInsensBW.PhaseType. A class- law is a structure (PhaseTypeD) with blocks, lengths, distinct rates and an initial law; phases are pairs (block, position), 0-based. The network (BWNetwork) carries , , , and one law per route; the standing assumptions are explicit theorem hypotheses: 0/1 entries and full row rank of , every route uses a link, , , , (7)–(8) with . The allocation is a predicate on route totals, and theorems take an allocation function satisfying it (it exists and is unique by milestone (5)). The chain's rates are exactly (60) with zero diagonal; a stationary distribution is a nonnegative, total-mass-one solution of the global balance equations (the published KellyStochasticNetworks.FullBalance), and statements hold for every such solution. and are explicit – statements with constants chosen before , and every expectation carries a summability clause.
The goal's statement uses only the model layer; , , the cone distance and the projections live in a second definitions module used by the milestones. The goal cannot be satisfied trivially: the allocation exists (milestone (5)), stationary distributions exist for every (Lemma 7), the expectation must be finite, and none of the network, the weights or the file-size laws is specialised.
Paper slips handled in the statements: Lemma 7 is stated for (the page says "nonnegative"); Lemma 8 quantifies over all with , as its proof does; is stated for critical links only, which is what its derivation shows; Lemma 9 holds for every multiplier vector, since multipliers need not be unique; the closing brackets missing in (80) are restored.
Needed infrastructure: the matrix exponential of block-bidiagonal matrices and its integrals; positive definiteness through the PBH test; countable-state continuous-time Markov chains (irreducibility, stationarity, uniformisation, zero expected drift for integrable Lyapunov functions); finite-dimensional convex optimisation with KKT conditions. Contributions to any of these, and proofs of any milestone, are welcome.
A constrained optimization problem often has an objective of the form : a smooth map describes the model, while an extended-real function gives the cost and can assign to infeasible outputs. Such a description covers polyhedral constraints, quadratic penalties on pieces, and many nonsmooth composite objectives. Solvers need to know how the local first and second order behavior of depends on the two parts of the model. The usual chain rules in Rockafellar and Wets, Variational Analysis use qualification conditions stronger than an error bound at the point of interest. Mohammadi, Mordukhovich, and Sarabi develop chain rules under a metric subregularity qualification condition (MSQC), including the second order result targeted here.
The paper was circulated as arXiv:1905.08837v2 in 2019 and published in Mathematics of Operations Research in 2022. This mission follows the pinned arXiv version, whose theorem and page numbering is used throughout. The result is known in mathematics; the open task here is its formalization in Lean. The paper also derives optimality conditions and statements about KKT systems from its second order analysis, but those later applications are outside this mission's target. Source: §§1, 5, 6, 8.
Fix finite dimensional Euclidean spaces and . An extended-real function has finite domain . Assigning outside a feasible set lets an ordinary function and a constraint be treated together. A convex piecewise linear-quadratic function (PWLQ) has a finite collection of polyhedral convex pieces whose union is its domain. On each piece its value is , where is symmetric. The separate formulas must agree where pieces meet, because all describe the same function. Source: (2.9), p. 5.
A function is fully subamenable at when it agrees with on a neighborhood of , with twice differentiable at , convex PWLQ, and MSQC satisfied there. Write . MSQC says that for some and all near , . This controls how far a nearby point is from feasibility through its residual in the outer domain. It is the paper's condition (3.5), not metric regularity. Source: Definition 3.2 and (3.5), pp. 9–10; Definition 4.2, p. 16.
The subderivative is a lower limit of first order difference quotients as positive time tends to zero and the direction tends to . Given a limiting subgradient , the second subderivative uses the quotient after subtracting the linear term and dividing by . Proper twice epi-differentiability means these quotients epi-converge to a second subderivative that never equals and is finite somewhere. The paper gives an equivalent test using recovery directions for every positive null sequence; that test is used in Lean. Source: (2.11), (2.15), (2.16), pp. 6–7.
For every , a fully subamenable is properly twice epi-differentiable at for . With
its second subderivative satisfies, for every ,
The maximum is attained; a supremum alone is a weaker claim. This is Theorem 5.2 and (5.3), p. 22.
The milestones are the paper's equality rules for first order subderivatives and subgradients (Theorems 3.4 and 3.6), its identification of critical directions with the finite domain of the second subderivative (Theorem 4.4), the PWLQ outer-function formula (4.8), the lower bound (4.10), and the parabolic limit formula (Lemma 5.1). Each names a separate mathematical claim needed to connect the composite model to the goal. Source: §§3–5.
Theorem 5.2 gives a data-level way to evaluate the second order behavior of a nonsmooth composite: the outer function contributes its own second subderivative, the inner map contributes its Hessian, and multipliers connect the two. Its properness and epi-differentiability clauses make the formula suitable for the paper's later no-gap second order optimality conditions and parametric analysis. Without those clauses, an equality of extended-real expressions alone would not establish the stability of the difference quotients. Source: Theorem 5.2 and §6.
A formal development of this result would add reusable definitions and lemmas for extended-real difference quotients, second-order tangent geometry, PWLQ functions, and local composite error bounds. The present draft contains statements and definitions that compile; it does not yet contain proofs of the open theorem items. The published limiting-subdifferential definition is reused, while the paper-specific local representation and multiplier set are defined here.
A first order expansion of does not settle the second order claim. Near a polyhedral boundary, the direction may be tangent while a fixed straight path leaves the domain; the second-order correction and the outer function's active piece matter. MSQC controls distance to feasibility but does not itself identify a feasible second-order path or a maximizing multiplier. The source therefore needs separate results about critical directions, PWLQ second subderivatives, parabolic limits, and dual attainment before the full formula can be stated with a maximum. Source: §§4–5, especially pp. 17–23.
Lean uses EuclideanSpace ℝ (Fin n) and EReal. The paper's codomain excludes ; the relevant hypotheses enforce that exclusion, while the subderivatives themselves may take either infinite value. The finite domain is defined by exclusion of . A PWLQ representation records finite closed half-space intersections, symmetric operators, and the exact quadratic coefficient. Twice differentiability includes differentiability near the base point and differentiability of the derivative at the point. The composite identity holds on a neighborhood rather than globally. MSQC uses the paper's local distance estimate with . Positive null sequences represent ; a filter lower limit represents the varying direction. The second quotient retains the paper's denominator.
The subdifferentials are the published analytic regular and limiting subdifferentials. Their use matches the paper's geometric subdifferentials at the lower semicontinuous functions in these statements. The goal computes the second subderivative from the lower-limit definition, rather than defining it by (5.3). Full subamenability retains MSQC and a genuine PWLQ representation; it is neither an empty-domain case nor a stronger metric-regularity special case. Contributions toward proofs of the milestone theorems, their needed tangent-set geometry, and the goal are in scope.
Many proposed quantum optimization and machine-learning methods (variational quantum eigensolvers, QAOA, quantum classifiers) tune the real parameters of a circuit by gradient descent on an objective that is only accessible as a black box. Classically, a finite-difference estimate of costs on the order of evaluations of . Quantum algorithms can access coherently through a phase oracle , and the question is how many such queries are needed to learn to accuracy in the sup norm.
Timeline.
A point of is , with . The paper's is .
Grid and Jordan's algorithm. For qubits put . A bit string encoding the integer labels the grid point , and is the set of these points (Definition 17). Algorithm 2 prepares registers of qubits in uniform superposition over . It applies the phase oracle once, applies the inverse grid Fourier transform to each register, and measures the outcome .
Index sequences and analyticity. For , is the -th partial derivative along the coordinates , and (Definition 4). The function is analytic around if
(Definition 5, there at ).
Central differences. The central difference coefficients are
The degree- central difference of is , an approximation of (Definition 7).
Queries. A fractional query with counts as one query (Definitions 10–11). The algorithm of Theorem 25 has parameters and . It runs Algorithm 2 with qubits per register on the phase , where . It reads each outcome as , repeats times and outputs the coordinate-wise median. One run costs queries to .
There is an absolute constant such that for every , and some parameter choice, made before and , uses at most
queries. For every and every smooth that is analytic around with (), it outputs with with probability at least .
The result. Theorem 25 gives a quantum gradient algorithm whose query count grows like in the dimension and nearly linearly in . Jordan's original analysis gives , and classical finite differences need on the order of evaluations. Section 6 of the paper shows that cannot be beaten for a class of smooth functions, so Theorem 25 is optimal up to logarithmic factors. Section 5.5 shows that probability oracles built from parametrized circuits satisfy the derivative bound, so the theorem applies to gradient-based training of variational circuits.
Formalizing it. The theorems are proved in the paper; this mission is not aware of a machine-checked proof of any of them. A formal proof would check the explicit constants (1/1000, , , ) and the accounting of fractional queries, which are spread across the main text and Appendix A. It would also produce reusable libraries: exactness and coefficient bounds for central differences, concentration of random multilinear forms, and a phase-estimation-style analysis of Jordan's algorithm on the published Lean model.
Jordan's algorithm reads off a gradient only if the phase is almost exactly affine on the whole grid. A truncated Taylor expansion of makes the error of order- terms grow like on the cube, which destroys the scaling. The approximation is only good on most of the grid, not all of it. The guarantee therefore has to tolerate a small fraction of bad grid points inside the quantum algorithm (Lemma 20) and has to control random multilinear forms (Lemma 36). The analysis also has to keep explicit, -uniform control of the central difference coefficients, whose sizes enter both the approximation error and the query count.
Fin d → ℝ, whose norm is . is iteratedFDeriv along coordinate vectors, and functions are assumed (ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)). "Analytic" is the Taylor representation (5) at the relevant point (IsTaylorRep), not Mathlib's local AnalyticAt.QAlgorithms.gradientAlgState. Independent runs multiply.Contributions are welcome at every level. Most useful are general facts about central difference coefficients (moment identities, , the binomial ratio bounds), concentration of multilinear forms in independent symmetric variables, and the single-run analysis of gradientAlgState. These are reusable beyond this mission.
Stress testing and data-driven decision making often combine two samples: observations of the quantity of interest and additional scenarios (stress scenarios supplied by a regulator, or unlabeled data). Blanchet and Kang (arXiv:1605.01340v4, 2020; later in Operations Research, 2021) propose to measure how far the empirical distribution of the observations is from the set of distributions that live on the merged sample and satisfy a hypothesis about a parameter, such as "the mean is ". The distance is an optimal-transport (Wasserstein) cost, and the resulting statistic is the sample out-of-sample (SOS) profile function.
The construction is the transport analogue of empirical likelihood (Owen 1988), whose central result is a Wilks-type theorem (Wilks 1938): of the likelihood ratio at the true mean is asymptotically . Empirical likelihood can only reweight the observed points. The SOS function can also move mass to out-of-sample scenarios, which is what makes it usable for stress testing. Confidence regions require the asymptotic law of the statistic at the true parameter. That law is the subject of this mission: the paper's main theorem for means, Theorem 1 (pp. 15–16).
Let . Observations and scenarios are random vectors in , all mutually independent, with Lebesgue densities and . A ratio fixes the number of scenarios used with observations. The standing assumptions A1)–A4) (p. 14) are: the samples are i.i.d. with these densities; ; everywhere; and, if , are differentiable with bounded gradients.
The merged sample is . For the SOS function (Definition 1, in the linear-programming form (21)) is
It is the least squared transport cost from the empirical measure of the to a probability measure supported on with mean . The statistic of interest is at the true mean . Write and .
The limits involve a mixed exponential variable. With the rate , the variable satisfies . From one defines , , the solution of , and .
As ,
The goal is the paper's theorem in all three regimes. The case is stated with , a correction of the printed (see Formalization scope).
Theorem 1 calibrates the SOS method. Its quantiles define the radius of a confidence region for the mean, and through the paper's Theorems 2–3 for estimating equations and for stochastic programs whose uncertainty set must cover out-of-sample scenarios. Unlike empirical likelihood, the limit depends on the dimension and on the densities : more dispersed scenarios give smaller distances and smaller quantiles (§4.1.1). The theorem also shows that the scaling itself changes with , from for to for .
The result is proved in the paper; nothing here is an open problem. As far as we know, none of it has been formalized. A formal development adds:
The obvious approach is a Wilks-type expansion: take the dual of the LP, find the dual multiplier by a quadratic approximation, and read off a limit. This works only for . In higher dimensions the transport may only move mass to sample points, and the constraint for observation is controlled by the distance from to the nearest other sample point. That distance is of order , so it competes with at a dimension-dependent scale. The quadratic approximation therefore fails: the dual objective becomes, after rescaling, an average of over dependent first-arrival times, which share the same merged sample.
Three steps carry the weight. (a) The dependent array needs a uniform empirical-process bound (Lemma 1); i.i.d. tools such as the Dvoretzky–Kiefer–Wolfowitz inequality do not apply. (b) A quantitative Poisson approximation (Lemma 2) needs the bounded density gradients. (c) The random concave objective must converge to a deterministic one uniformly enough that its maximiser converges (argmax continuity). Step (c) also needs a multivariate central limit theorem for , which Mathlib does not yet provide.
Representation. Points live in EuclideanSpace ℝ (Fin l). The samples are infinite sequences on a probability space , jointly independent (iIndepFun over ), with laws volume.withDensity. The -th statistic uses the first observations and the first scenarios; is read as the floor, and is allowed. The SOS function is a real infimum over couplings of indexed families. Convergence in distribution is Mathlib's TendstoInDistribution, with limit the image of multivariateGaussian 0 Var(X) under an explicit map . The goal is a conjunction of three clauses, , , .
Conventions and disclosed readings.
Ruled out. The following are not acceptable formalizations: a feasibility hypothesis on every sample; a limit law left as a parameter or quantified existentially; , or given by closed forms rather than from the law of and the fixed-point property; the printed presented as proved; Lemma 2 with a constant uniform in ; Lemma 1 with a Bochner integral, which would be a default for a non-integrable supremum.
Infrastructure. A full proof needs: finite LP strong duality (Farkas), absent as a packaged theorem; binomial/Poisson estimates for small-ball counts; a pathwise Burkholder–Davis–Gundy inequality (Beiglböck and Siorpaes 2015) or another route to Lemma 1; dominated-convergence differentiation of ; a multivariate CLT; and argmax-continuity for random concave functions. The LP duality and the multivariate CLT are reusable well beyond this mission. Contributions to any milestone are welcome; milestones 1, 2, 6, 7 and 8 are deterministic and independent of the probabilistic core.
Digital platforms earn advertising revenue in proportion to the time users spend on them, and many of their design choices (infinite scroll, autoplay, notifications) raise engagement at the expense of the user's experience. Whether competition between platforms disciplines such addictive design or amplifies it is a question for competition policy and for the regulation of digital markets.
Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16, 2022; Management Science, 2023) model platforms that compete for a consumer's attention by choosing how addictive to make their services. Without costs of addictiveness they find that competition hurts the consumer when attention is scarce and helps her when it is abundant (a separate mission formalizes that comparison). Section 5 of the paper asks what changes when raising addictiveness is costly, for instance because it requires investment in technology. Its answer, Proposition 5, is that the comparison then depends on the size of that cost rather than on the scarcity of attention: for high costs competition leads to more addictiveness and lower consumer welfare than joint-profit maximization would, whatever the attention cap.
There are platforms and one consumer. Each platform chooses an addictiveness and pays , with . The consumer observes , joins a set of platforms and allocates attention to each , subject to the attention cap , where . Her payoff is if she joins nothing and otherwise
Platform earns the attention it receives, if and otherwise, minus its cost .
The utility has the form : addictiveness lowers the utility of any given amount of attention but raises its marginal value. The primitives satisfy the paper's Assumptions 1–3: is strictly increasing and concave, strictly decreasing, and strictly increasing in ; the attention cost is strictly increasing, convex and twice differentiable with ; the cost of addictiveness is increasing, strictly convex and differentiable with and ; and with the inverse of , the product is weakly decreasing.
Two outcomes are compared.
Consumer surplus , respectively , is the consumer's payoff at the equilibrium, respectively at the joint-profit maximizing outcome.
For every and the equilibrium is unique, with all platforms at the same positive addictiveness, and a joint-profit maximizing outcome exists. For every , including , there is a such that for every
The threshold may depend on the cap and the primitives but not on .
Proposition 5 separates two forces. When addictiveness is cheap, the consumer's participation constraint pins down the outcome under joint-profit maximization, and the platforms push her payoff to zero; competition then helps her because she can leave one platform. When addictiveness is expensive, each platform's marginal trade-off between attention and cost determines its choice, and competing platforms, which take attention from one another, choose more addictiveness than they would jointly. The result implies Corollary 1: for the platforms gain from a collective cap on addictiveness, which bears on the debate about industry self-regulation.
The result is proved in the paper; to our knowledge none of it has been formalized. A machine-checked proof would cover a game with a continuum of strategies for every player, a consumer best response defined at every profile, a fixed-point characterization of equilibrium, and a threshold argument in the cost parameter. Appendix D's proof is short and leaves steps to the reader, among them that is increasing in and that each , not only consumer surplus, is lower under joint-profit maximization. A formal proof has to supply these steps.
The obvious argument is to compute both outcomes from first-order conditions and compare. Three steps of that argument do not go through as written. First, the consumer's allocation (A.6) is derived from an unconstrained first-order condition and fails when a platform is so addictive that its formula gives negative attention, so a platform's payoff away from symmetric profiles is not given by the closed form (A.10). Ruling out profitable deviations into that region needs a separate argument. Second, uniqueness of the equilibrium is claimed among all profiles, not only symmetric ones. Third, the "if and only if" requires the set of costs where the joint-profit outcome is better to be an interval closed at its left end, which in turn needs monotonicity and continuity of both consumer payoffs in across the switch between the participation regime and the marginal regime.
Platforms are Fin K (the paper's platform 1 is index 0) and the cap is an extended nonnegative real ℝ≥0∞. Derivatives of , and on are one-sided. The consumer strategy is a choice at every profile, and the equilibrium requires optimality at every nonnegative profile. Without that requirement any profile could be supported by a consumer who punishes deviations. The joint-profit outcome uses its own restricted consumer problem ("join all or none") and the consumer-favourable tie-break among profit-maximizing profiles. Without the tie-break, profiles below the participation level would also count as outcomes. No value function is written as a supremum: equilibrium objects are characterized through maximizers. "Lower", "higher" and "decreasing" are read weakly. The proof yields only weak inequalities on both sides of , and at the two outcomes can coincide.
The statement adds the following disclosed hypotheses to the paper's assumptions:
Lemma D.1 also carries an interiority hypothesis, that every coordinate of (A.6) is nonnegative, without which it is false. The goal also asserts that a joint-profit maximizing outcome exists, so that its comparison cannot hold vacuously. ranges over ; the proof's use of as a cost-free benchmark is not part of any statement.
The hypotheses are satisfiable. A sanity check, not part of the mission, verifies all of them in Lean for every on the instance
A complete development needs Karush–Kuhn–Tucker conditions for a concave program over a simplex-like set, implicit differentiation for , a monotone fixed-point argument for the best response, and continuity of maximizers in a parameter. These parts are reusable beyond this mission. Proofs of the milestones, partial results under the closed-form allocation, and checks of the statements on concrete instances are all welcome. The goal is Proposition 5. Propositions 1–4, 6 and 7, Corollary 1 and the side claims of Appendices E–F are not posed here.
Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.
Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost . The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.
Demands are i.i.d. copies of a non-negative random variable with and distribution function . The product lives periods. At the start of period the state is , where is the stock with remaining lifetime at most . The firm orders , raising the total stock to (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity outdates, and the state evolves by
The system starts empty. The period cost is
with holding cost , lost-sales penalty and outdating cost .
A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is , and is the infimum of over admissible policies. The base-stock policy orders , and is its long-run average cost. The heuristic level is any minimizer over of
The lower support of demand is .
for every selection of minimizers, with , , and the demand law fixed. The statement holds for every demand law, whether is zero or positive.
The goal's proof also uses inequality (21), . That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.
Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level fails in this regime.
The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of , the identity , and continuity of the newsvendor cost. Each of these becomes an explicit statement.
The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than grows. That needs uniform control of as . The level must eventually fall into , where no stock survives periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of " decreases in " holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.
PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with ) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.Fin (m - 1) → ℝ≥0 of cumulative levels, with . When the state is empty and everything left over outdates. Levels range over .atTop there. The goal asserts that is finite and that the difference of real values tends to , so no convention enters.Large platforms that also sell their own products (Amazon, JD.com, app stores) hold detailed data on consumers and sometimes share part of it with the independent sellers they compete with. The usual view in the personalized-pricing literature is that information is a competitive weapon: a firm that knows more about consumers can price discriminate and capture more surplus, so giving that knowledge to a rival should only hurt. Thisse and Vives (American Economic Review, 1988) showed that when both firms on a Hotelling line can price every consumer individually, competition intensifies and the profits of the informed firm fall.
Choe, Cong and Wang (Monash Discussion Paper 2021-10, revised October 20, 2022; published in Management Science, 2024, doi:10.1287/mnsc.2023.4689) show that this is not the whole picture: an informed firm can strictly gain by sharing data on a well-chosen segment of consumers with an uninformed rival, and the rival gains too. This mission formalizes that result, Proposition 1 of the paper, together with the steps its proof is built from.
Consumers are located on the interval . A consumer's location has cumulative distribution function with density , continuous on , and the hazard rate
is strictly increasing on (the monotone hazard rate condition). Firm 1 sits at and knows every consumer's location; firm 2 sits at and knows none. A consumer at who buys from firm at price pays plus a transport cost equal to her distance to firm ; production is costless and the market is fully covered.
Benchmark. Without data sharing, firm 2 sets one uniform price and firm 1 undercuts it consumer by consumer, so firm 2 serves with and earns . The first-order condition gives the benchmark marginal consumer and price :
The benchmark profits are and .
Data sharing on . Firm 1 gives firm 2 the locations of the consumers in . Firm 2 then chooses a uniform price for the consumers it does not know and personalized prices on . Its uniform price either serves only , at price and profit , or serves for some , with best profit
When firm 2 chooses the first option, the profits are
Firm 2's incentive constraint (IC) is .
For every distribution satisfying the conditions above:
and there exists with
so sharing data on satisfies firm 2's incentive constraint and makes both firms strictly better off than without sharing.
The result reverses the standard intuition that a firm's informational advantage should be guarded. Firm 1 shares data only on firm 2's own customer base , which it could not win anyway, and keeps the data on the most loyal consumers private. Firm 2 then prefers to extract surplus from those loyal consumers with a high uniform price , and firm 1 raises its personalized prices accordingly. Competition is softened without firm 1 conceding market share. The statement holds for every monotone-hazard-rate distribution, not for a parametric family, which is what makes it a structural claim rather than a numerical example. It underlies the paper's analysis of optimal data sharing (Section 3.3) and its welfare conclusion that consumer surplus falls (Proposition 3), and it is the benchmark against which the paper's extensions (sales fees, data sale, entry) are compared.
The paper's proof is complete for the first part. For the existence of , the written argument infers a negative derivative of at from a strict inequality, which does not follow as written and presupposes differentiability of a maximum value function; the statement itself is true. A machine-checked proof closes that step. To the best of current knowledge none of these results has been formalized.
The two profit comparisons in the first part are integral identities and estimates that only need the fundamental theorem of calculus and . The existence of is the hard part. Both and start from the same value at , and has zero derivative there, so the comparison is decided at first order by how fast decreases. But is a maximum over whose maximizer moves with and need not be unique, so is not known to be differentiable, and the strict decrease of milestone 7 alone does not give a linear rate. A proof has to bound from above by minus a term proportional to , uniformly over the possible maximizers, and compare it with the second-order behaviour of near its maximum. Existence of similarly needs the hazard rate to blow up at , which uses and .
All objects are real-valued functions on with hypotheses only on . The distribution is the structure MHRDist F f: , , has derivative within at every point of , is continuous and strictly positive on , and is strictly increasing on . The paper's "smooth" is read as continuously differentiable, a weaker assumption, so the formal theorems are at least as strong as the paper's. Every integral is an interval integral of the integrand times , always with increasing bounds. enters as a number zN with the hypothesis IsZN F f zN ( and ); milestone 1 shows exactly one such number exists, so no statement is vacuous. is defined as the supremum of the profit over (a maximum, since the set is compact and the function continuous), never through the first-order condition (5); the incentive inequality in the goal is strict, as in the paper's proof.
A trivializing formalization is ruled out: is the actual maximum, not a free parameter or the value at a stationary point, and is pinned by Eq. (1), whose solution is shown to exist.
A complete development needs the fundamental theorem of calculus for interval integrals, compactness and the intermediate value theorem on , and a uniform first-order estimate on a parametric maximum. The lemmas on hazard rates and on the maximizer of are reusable for other Hotelling and pricing models with monotone-hazard-rate demand. Contributions are welcome on any milestone, and alternative proofs of the existence of are of particular interest.
A seller who customizes products for buyers must learn what each buyer wants, and buyers have private information about how much they value quality. Liang Guo's paper The Voice of Customers in Customization (Management Science, doi:10.1287/mnsc.2021.04025; author copy SSRN 3994319) compares two ways of learning those preferences. Under A-Learning ("asking") the buyer sends an unverifiable, costless message about its type and the seller then designs the product. Under O-Learning ("observing") the buyer itself proposes the quality it wants, and the seller accepts or rejects the proposal. In both, the price is set afterwards by bargaining in which the seller makes the take-it-or-leave-it offer with probability .
Customization works only if buyer types are revealed in equilibrium. The paper shows that each approach admits a separating equilibrium exactly when the buyers are heterogeneous enough: the ratio of the two types' quality preferences must exceed a critical value, under A-Learning (Proposition 1) and under O-Learning (Proposition 3). Which approach makes customization easier to sustain is then a comparison of two explicit numbers. Proposition 7 answers it, and its answer depends only on the seller's bargaining power and the two cost coefficients. This is the question a manager choosing between surveys and interviews (asking) and design-it-yourself tools (observing) faces in the model.
A model is a tuple of real numbers :
The paper's standing assumptions (§2, pp. 5–6) are
The A-Learning thresholds (Proposition 1, p. 12, and p. 13) are
is the ratio above which the high type does not gain by claiming to be low, and the ratio above which the low type does not gain by claiming to be high.
The O-Learning thresholds (Proposition 3, p. 17) are
and are the high type's thresholds in the two regimes (seller acceptance binds) and (it does not); is the low type's.
for every model satisfying the standing assumptions. The paper phrases this as "the critical value of to sustain the separating equilibrium is larger under the A-Learning customization than under the O-Learning customization (i.e., )"; the parenthetical fixes the statement as a comparison of the two printed thresholds.
The result. Proposition 7 says that neither learning approach dominates the other. When the seller's bargaining power is low, A-Learning requires more heterogeneous buyers than O-Learning, so empowering buyers to design their own products sustains customization over a larger range of markets; when the seller is powerful, the order reverses. Milestones 1–3 carry the paper's economic reading: the low type's incentive to reveal itself is weaker under A-Learning (), the high type's is stronger (), and the comparison is decided by which effect dominates. The cutoff on is explicit in and , which is what makes the comparison usable for comparative statics.
Formalizing it. The result is proved in the paper, in a short Appendix argument (p. 29); it has not been machine-checked. A formal proof pins down that the reduction is correct for every parameter value allowed by the standing assumptions, including the boundary cases (where ) and the case where the two candidate cutoffs coincide. Together with the companion missions of this series, which formalize Propositions 1 and 3 as statements about the equilibria of the two games, it gives a fully checked version of the paper's comparison of the two approaches.
Both critical values are nested maxima and minima of rational functions of , and which term attains each maximum or minimum changes across the parameter space, in particular at , where and exchange order. A direct case split on the attaining terms therefore produces many cases, several of which turn on sign conditions that hold only under the standing assumptions. The cutoff on the right-hand side is a maximum of two expressions of different kinds, one rational and one involving , and neither of them dominates the other for all , so neither can be dropped. Strictness must be tracked throughout, since both sides of the equivalence are strict and the boundary is attained.
All objects live in the namespace CustomerVoice.Thresholds. A structure Model holds the six real primitives, Model.Standing is the conjunction of the standing assumptions, and Model.DeltaH, DeltaL, Delta, LambdaH1, LambdaH2, LambdaL, Lambda are the printed closed-form expressions, with and on and the square root as Real.sqrt. Every theorem takes a model and the hypothesis M.Standing; no other hypothesis is added. Only , and enter the thresholds; , and are carried so that the model is the paper's. Under the standing assumptions all denominators are positive, so Lean's convention is never used.
The thresholds are defined as the paper prints them. Defining or as the least type ratio at which an equilibrium exists, replacing them by simplified forms that hold only in a regime (for instance when ), replacing the right-hand side of Proposition 7 by an equivalent condition the paper does not print, or proving only one direction of the equivalence, would each be a different statement and is ruled out.
The two games and the equilibrium characterizations behind and (Propositions 1 and 3) are not part of this mission; they are the goals of missions I and II of this series, and the model is defined again here because draft missions cannot import each other. No library beyond Mathlib's ordered-field and square-root API is needed. Contributions welcome: proofs of the four milestones and the goal, and helper lemmas solving the two quadratic inequalities and in .
The source is the SSRN author copy of the paper (version of 2023-11-29); all page numbers are its printed pages, and the proof the milestones come from is in its Appendix.
Production in agriculture, semiconductors, pharmaceuticals and many other industries suffers from random yield: only a random fraction of a planned production run turns out usable. When a retailer buys from such a supplier, someone in the chain bears the risk that less arrives than was ordered. Geng, Guo, Xiao and Yang (SSRN 3546872; Manufacturing & Service Operations Management 25(3), 2023, doi:10.1287/msom.2022.0198) study two levers a retailer can pull to push that risk away from itself. Payment postponement means paying only for what is delivered rather than for what was ordered. Pricing postponement means fixing the retail price after the delivery is known rather than committing to it in advance. Both are common in practice, and their effect on the other members of the chain, the supplier and the end consumers, is not obvious: shifting risk changes the supplier's wholesale price and production, and so everyone's payoff.
This mission formalizes the paper's answer for pricing postponement (its Proposition 5): when does moving from ex ante to responsive pricing make the supplier, the retailer and the consumers all better off, and when does it hurt the supplier?
A supplier sells one product to a retailer, who sells it in a market with linear demand , , and inverse demand . The supplier plans a production quantity at unit cost , but only is realized, where the yield factor equals with probability and with probability , for . Write for the mean yield. The retailer orders and receives .
There are four scenarios. Under pay-by-order (O) the retailer pays ; the supplier then produces exactly . Under pay-by-delivery (D) it pays , and the supplier may inflate production above . Under ex ante pricing (A) the retailer commits to a price when it orders; under responsive pricing (R) it sets after observing , maximizing . In each of OA, OR, DA, DR the supplier first sets the wholesale price , the retailer then orders (and, ex ante, prices), the supplier chooses , the yield is drawn, and under responsive pricing the price is set last. Both firms are risk-neutral. Admissible actions are , , , and (pay-by-order) or (pay-by-delivery); costs range over .
The solution concept is subgame-perfect equilibrium. Its outcome is the triple of the retailer's and supplier's expected profits and the expected consumer surplus , with
The paper derives each scenario's equilibrium in closed form, piecewise in , with thresholds such as (its Lemmas 1–4 and Appendix B).
(O) Pay-by-order, any . Comparing equilibria of OA and OR:
an increasing function such that implies and the same triple of increases on ; and, if ,
(D) Pay-by-delivery, . Comparing equilibria of DA and DR: all three quantities strictly increase for , and all three are unchanged for .
The equilibrium of each scenario (Lemmas 1–4, with existence and uniqueness of the outcome on each open piece of ), the two last-stage responses (production (4) and the ex post price (5)), Lemma 2(i) (when ), the threshold claim behind (O)(ii) ( and ), and the ordering for .
The result. Proposition 5 shows that pricing postponement can be a Pareto improvement for the entire chain, consumers included, and identifies where: at high or intermediate production cost under pay-by-order, and above under pay-by-delivery. It also identifies the one place where it is not: under pay-by-order, low cost, and severe and likely yield loss, the retailer gains at the supplier's expense, because it orders a large quantity at a low wholesale price. Under pay-by-delivery and low cost, pricing postponement changes nothing, since the supplier already absorbs the yield risk by inflating production. These statements feed the paper's managerial conclusions on when a retailer facing unreliable supply should adopt flexible pricing and how this affects its supplier.
Formalizing it. The paper proves its lemmas by "the results in Appendix B" and its propositions as "straightforward comparisons". A machine-checked development would make the backward induction itself explicit: four three-stage games, each with kinks in the production and order responses and boundary optima of the wholesale price. Drafting this mission already turned up four printed slips: a consumer-surplus denominator in Appendix B.1 ( for ), a consumer-surplus value in Appendix B.4 that no single equilibrium produces, a production tie rule under which scenario DR has no equilibrium on an interval of costs, and swapped labels in display (2). None of them changes Proposition 5. To our knowledge, none of the paper's results has been formalized.
Once Lemmas 1–4 are known, each comparison in Proposition 5 is algebra between explicit pieces. The work is in Lemmas 1–4. The obvious approach, maximizing each stage's closed-form objective, does not suffice. The equilibrium must be optimal in every subgame, including order quantities and wholesale prices never played. The objectives are only piecewise smooth, so the maximizer often sits at a kink: at in scenario OA, the retailer is indifferent between inflating its order and not; at in scenario DR, the supplier is indifferent between inflating production and not, and the supplier's value is discontinuous there. Existence of an equilibrium in DR on depends on how that tie is resolved. On top of this come inequalities between thresholds involving nested square roots, e.g. under , and the monotonicity of .
Everything is finite-dimensional real arithmetic: , with no measure theory. The cost is a separate argument, and every threshold depends on only. The standing assumptions are , and , the paper's (1) and (3). Strategies are functions of everything observed before the move. Optimality is required at every node. Under pay-by-order , as the model prescribes. Conventions committed to, all disclosed in the items:
The profits are the outcomes of equilibria of the game, not the closed forms of Appendix B. The goal also asserts that equilibria exist for every admissible cost, so it cannot hold vacuously through an unsatisfiable equilibrium predicate.
Contributions welcome: the last-stage lemmas (4) and (5), the threshold inequalities, the scenario equilibria (Lemmas 1–4), and the goal. The equilibrium framework is shared with the three sibling missions on Propositions 2, 3 and 4 of the same paper.
A quantum LDPC code is a CSS code whose two check matrices and have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.
Timeline.
Let be a finite bipartite graph, , , with , and write for adjacency. is -biregular if every vertex of has neighbours and every vertex of has . For let be its neighbourhood. is -left-expanding if for every with ; right expansion is the same on the side, and left-right expanding means both. denotes the unique neighbours of , adjacent to exactly one vertex of .
Let be the binary biadjacency matrix of . The quantum code has qubits, indexed by (written and ), and check matrices
with rows indexed by and . The row of has support the Z-generator . An error is , its syndrome is , and is the space of sums of Z-generators. The weight of a quantum error counts the qubits where or is nonzero.
The decoder. On a syndrome , one iteration picks a vector whose support lies in some generator , such that has and the ratio is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum of the flipped vectors. The decoder is the same with and exchanged.
Assume is -biregular and -left-right expanding with
and let be a quantum error with
Then on every run, the decoder on input never outputs a failure and its output satisfies . The decoder on behaves symmetrically, with .
In the paper's order of proof:
The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order . The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).
Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:
The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to rather than the distance.
adj : A → B → Prop on finite types, and = bipMatrix adj : Matrix B A (ZMod 2).TillichZemor.HGP.Setting is reused. The paper's is TillichZemor.HGP.hz H H and its is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.(A × A) ⊕ (B × B), weights are hammingNorm, and is CodingTheory.dualCode of ker H_Z.Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in .Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.Additions and omissions.
Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses = hz H H, not the swapped matrix.
Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.
Best subset selection fits a linear model using at most of candidate predictors. When the noise level is high relative to the signal, it overfits. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add a shrinkage penalty , , to the best-subsets problem and prove oracle inequalities for the resulting estimators. Their main error bounds (Theorems 2–5) are proved in the same way: a deterministic argument shows the bound holds whenever the noise vector lies in one of four explicit sets, and a separate probabilistic result shows that each set has probability close to one. This mission formalizes that probabilistic result, Theorem 1 of the paper (p. 13, proof in Supplement B.1, pp. 38–39).
The four events combine several tools of high-dimensional statistics. The event controls the noise through a sorted- (SLOPE-type) norm; its probability bound is Theorem 4.1 of Bellec, Lecué and Tsybakov, Slope meets Lasso (Ann. Statist. 2018). The event is a sparse version of a deviation bound, adapted from Lemma 8 of Raskutti, Wainwright and Yu (IEEE Trans. Inf. Theory 2011). The event is the classical Gaussian maximal inequality behind Lasso and Dantzig-selector analyses.
Observations follow the model
in . The mean is deterministic and unknown. The noise has independent coordinates, with . The design is deterministic, and its columns have unit Euclidean norm.
For , is the Euclidean norm, the norm, the largest absolute coordinate, and the number of non-zero coordinates. For an integer , . The non-increasing rearrangement lists in non-increasing order. Logarithms are natural, and is a confidence parameter.
The four events (p. 13) are sets of noise vectors:
For and :
where is with in place of under the root. Each event is also asserted to be measurable.
The printed claim is false. Take and . Then with , and , which exceeds once . The corrected constant is what the argument the paper cites actually gives. Downstream, the paper uses only inside inequalities that hold up to universal constants, so the correction does not affect its other results.
The proof in B.1 is followed step by step:
The result. Theorem 1 is the only probabilistic input to the paper's statistical theory. Theorem 2 ( shrinkage) is proved on , and . Theorem 3 ( shrinkage) uses as well. The lower bound for best subsets (Theorem 4) and the BIC-type choice of (Theorem 5) also rely on . Every high-probability bound and every expected-error bound in §3 is obtained by combining a deterministic inequality with this theorem. The event is also of independent use: it gives the sorted- control of Gaussian noise used in SLOPE and Lasso analyses.
Formalizing it. All four bounds are known results; the mission formalizes them. The deterministic reduction is elementary. The three probability bounds need Gaussian machinery: a sorted- deviation bound (the hardest part), a tail bound with a union over supports, and a Gaussian maximal inequality. None of these has a machine-checked proof in Mathlib for this setting. The formal statement of the bound with its corrected constant is a contribution of its own, because the printed form is false.
The and parts are routine once the Gaussian tools exist. The part is a uniform statement over all supports at once, and the explicit constants and leave no room for a lossy tail bound: a generic sub-Gaussian estimate does not reach them.
The part is the hardest. It is uniform over all of , not over a sparse set. A union bound over the coordinates of gives the flat weight on every coordinate, not the decreasing weights , and it does not produce the explicit constant . The bound of Bellec, Lecué and Tsybakov has to be formalized in full, under this paper's normalization (unit columns rather than columns of norm ).
Fin n → ℝ, and is Matrix (Fin n) (Fin p) ℝ with unit columns (). Mathlib's default norm on Fin m → ℝ is the sup norm, so the Euclidean, , and norms are explicit definitions. Indices are 0-based: j : Fin p stands for the paper's .The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum possible total cost. It quantifies how much selfish routing loses compared with central coordination, and it has been studied intensively since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), mostly through worst-case bounds over classes of cost functions.
Worst-case bounds say nothing about how the PoA of one particular network behaves when its data change. In transport applications both the cost functions (capacities, tolls, travel-time models) and the demands are estimated, so the PoA is only useful if small errors in the data cause small errors in the PoA. Wu and Möhring (arXiv:2007.13979, published in Mathematics of Operations Research, 2023) study this sensitivity question in a setting where cost functions and demands change simultaneously. Earlier sensitivity results changed only the demands, with the cost functions fixed: Englert, Franke and Olbrich (2010) bounded the growth of the PoA of a single-O/D network with polynomial costs of degree at most by a factor when the demand grows by a factor ; Takalloo and Kwon (2020) extended this to several O/D pairs whose demands are scaled together; and Cominetti, Dose and Scarsini (arXiv:1907.10101) studied differentiability of the PoA as a function of the demand of a single O/D pair. The main theorem of the paper, Theorem 9, is the subject of this mission.
A network consists of a finite set of arcs, a finite non-empty set of origin–destination (O/D) pairs, and for every a non-empty set of paths; each path is a non-empty set of arcs. From §3.1 onward the paper also assumes every arc lies on some path and every has at least two paths (Condition 1).
A game on the network consists of cost functions , one per arc, that are continuous and non-decreasing, and demands , one per O/D pair. The total demand is . The game space consists of the games with and for all .
A flow assigns a non-negative amount to every path, with . Its arc flows are , its path costs , and its total cost
A Wardrop equilibrium (WE) is a flow in which every used path of a pair is a cheapest path of that pair. The SO cost is the minimum total cost over all flows, the WE cost is the total cost of a WE flow (all WE flows have the same cost), and
Games are compared by the distance
for and . It compares cost functions only on the range of flow values both games can produce, plus the values at the respective total demands. A function is Lipschitz continuous on with constant if for all .
Let be a game of the game space whose cost functions are Lipschitz continuous on . Then there are and , depending only on , such that
The goal fixes the exponent and leaves the radius and the constant existential, which is the form the paper claims.
for an -approximate WE flow and a WE flow when all costs are -Lipschitz on . 2. Lemma 10a)–d) (p. 27): on a demand slice (games with a common demand vector ), is Lipschitz, WE flows of one game are -approximate WE flows of the other, and and are Hölder with exponent with explicit constants. 3. Lemma 11a)–c) (p. 31): on a cost slice (games with a common cost vector and ), explicit Hölder bounds of exponent for and and a Lipschitz bound for .
Theorem 9 is the first pointwise Hölder continuity result for the PoA on the whole game space, with demands and costs perturbed together. Its hypothesis is mild (Lipschitz costs on a compact interval, which covers polynomial, BPR-type and piecewise linear costs), and such games are dense in the game space. Together with Theorem 8 of the same paper, which shows that no uniform Hölder bound exists, it describes exactly what kind of stability the PoA has: local, with a constant depending on the game, and exponent in general. The explicit constants of Lemmas 10 and 11 give computable error bounds for the PoA of a network whose data are known only approximately.
The result is proved in the paper; no machine-checked proof exists. This mission formalizes the statement and the explicit slice estimates the proof rests on. Lemma 1 is a self-contained statement about approximate Wardrop equilibria that is useful well beyond this paper, for instance for analysing iterative traffic-assignment algorithms, which only ever produce approximate equilibria.
The obvious approach compares an equilibrium of with an equilibrium of directly. This fails because the two games have different demand vectors, so their flows live in different polytopes: an equilibrium of one game is not even a flow of the other. The paper separates the perturbation into a change of costs at fixed demand and a change of demand at fixed costs, through an auxiliary game, and each half needs its own argument. On a demand slice an equilibrium of one game is only an approximate equilibrium of the other, and the passage from an approximate equilibrium to its cost loses a square root (Lemma 1c), which is tight by Example 2). On a cost slice the demand has to be removed path by path from an equilibrium while keeping it an equilibrium of a shifted game. Finally, the constants of the slice estimates depend on the auxiliary game, and they must be controlled uniformly near .
The Lean development fixes the following conventions.
KellyStochasticNetworks_Wardrop. -approximate WE flows follow (2.7) in arc form. The total cost uses the arc form, which equals the path form for 0/1 incidence.A complete development needs: existence of Wardrop equilibria and uniqueness of their cost on the game space, existence of social optima, the integral inequality (2.9) for monotone costs, positivity of on the game space, and the path-by-path demand-reduction construction of Lemma 11. The existence and uniqueness results and Lemma 1 are reusable in any formalization of selfish routing. Proofs of any milestone are welcome, as are the supporting lemmas above.
The source is the arXiv preprint arXiv:2007.13979v3 (23 Aug 2021); all page and theorem numbers refer to it, not to the published version.
The price of anarchy (PoA) of a nonatomic congestion game is the ratio between the total travel cost at a Wardrop equilibrium, where every traveller uses a cheapest route, and the minimum total cost a central planner could achieve. Worst-case bounds on the PoA are classical (Roughgarden and Tardos, 2002), but traffic studies observe that the empirical PoA is close to both in light and in heavy traffic (Youn, Gastner and Jeong, 2008; O'Hare, Connors and Watling, 2016). This raises the question of how the PoA of a fixed network with fixed cost functions behaves as the demand varies.
For decreasing demand the literature had one convergence result: for polynomial costs, Colini-Baldeschi, Cominetti, Mertikopoulos and Scarsini (2020) show when the total demand tends to with fixed demand proportions, at rate . Wu and Möhring (2021) obtain a rate for arbitrary cost functions that are strictly positive and Lipschitz near , with no condition on the demand proportions, as a corollary of their sensitivity analysis of the PoA. This mission formalizes that corollary, Corollary 5.1 of arXiv:2007.13979v3.
A structure consists of a finite set of arcs, a finite nonempty set of origin–destination (O/D) pairs, and for every pair a set of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game is a vector of arc cost functions , continuous and non-decreasing, together with demands of total . The game space consists of the games with and on .
A flow routes over with . Arc flows are and the total cost is . A flow is a Wardrop equilibrium if every used path is a cheapest path of its pair. With the minimum total cost and the cost of a Wardrop equilibrium (all equilibria have the same cost),
Games are compared by the distance (3.3),
and the demand normalization , with , rescales a game to a different total demand. The cost slice of is the set of games whose costs agree with on .
Let the costs be strictly positive on and Lipschitz on with constant , and let . There is such that for every demand vector with ,
The corollary gives a rate of convergence of the PoA to in light traffic for every cost vector that is strictly positive at and Lipschitz near , with an explicit constant depending only on the number of arcs, the number of O/D pairs, the Lipschitz constant and the free-flow costs . It removes the fixed-proportion condition on the demands needed in the earlier polynomial result, and it combines with the heavy-traffic results for regularly varying costs to show that the PoA is bounded on whole cost slices (p. 43).
The result is proved in the paper, in a few lines on top of the local Lipschitz estimate (4.33) of Theorem 12a). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean model of nonatomic congestion games with demand normalizations and the metric (3.3), together with the comparison between a game of total demand and the constant-cost game at the same demand, which is reusable for other light-traffic statements.
A direct bound cannot simply be read off as : the costs and both tend to with the demand, so their ratio is a quotient of two vanishing quantities, and an additive estimate on each cost says nothing about the ratio. The difficulty is to obtain a bound in which neither the threshold on nor the constant depends on the demand vector , including the proportions , which may vary arbitrarily, and some of which may vanish. Any argument whose constants depend on the particular game near which it works (as a pointwise Hölder constant does) gives only a pointwise statement, not the uniform one asserted here.
The Lean development lives in the namespace SensitivityPoA.SmallDemand and builds on the published definition KellyStochasticNetworks_Wardrop (flows, arc flows, Wardrop's first principle). Conventions:
A trivializing formalization is ruled out: the threshold is chosen before (choosing it after makes the statement vacuous), is required (at Lean's would make ), every game considered lies in the game space, and the bounds use , which holds at equality cases.
Contributions welcome: proofs of the milestones, the comparison of WE costs under pointwise cost perturbation (the variational inequality of Wardrop equilibria), and existence of Wardrop equilibria for costs that are continuous and monotone only on . The source is the arXiv preprint v3; the published version in Mathematics of Operations Research is not the cited artifact.
The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) prepares a parametrized quantum state whose measurement yields a candidate solution of a combinatorial optimization problem. Its level-one version alternates a single phase operator and a single mixing operator and is simple enough to analyse by hand. In arXiv:1412.6062 the same authors applied it to Max E3LIN2 with bounded occurrence: given linear equations mod 2, each on exactly three bits, with every bit in at most equations, satisfy as many equations as possible. A uniformly random string satisfies half of them in expectation; the question is by how much an algorithm can beat .
Without the occurrence bound no efficient algorithm achieves unless P = NP (Håstad, J. ACM 2001). With every bit in at most equations the history, as recounted on pp. 2–3 of the paper, is:
Section III, formalized here, studies the typical case: it fixes the triples and draws the right-hand sides at random, and shows that the QAOA then reaches an advantage of order , the order of the classical algorithm, on all but a vanishing fraction of the instances.
An instance on bits with equations is a list of triples with , no triple repeated, together with right-hand sides ; equation is . The instance has occurrence at most if every bit lies in at most triples. Write and ; equation is satisfied by exactly when .
Let be the number of equations satisfied by , viewed as a diagonal operator on the -dimensional space spanned by , let , and let be the uniform superposition. For angles the level-one QAOA state is
Measuring it in the computational basis gives a string; is the expected number of satisfied equations.
In Section III the triples are fixed and the instance is drawn uniformly from the choices of right-hand sides; and denote the mean and variance over this choice. The mixing angle is and the state analysed is , following the paper's sign convention.
For an equation with bits , the polynomial collects the equations that share exactly the bit with it, and is its number of terms.
For every E3LIN2 family of triples with occurrence at most , every and every ,
With and fixed, all but a fraction of the instances reach . This is the paper's closing sentence of Section III with an explicit failure probability.
The result shows that on random-sign instances with any fixed bounded-occurrence structure, a single layer of QAOA beats a random assignment by , the same order as the best known classical guarantee and better than the paper's own worst-case bound by a logarithmic factor. It was one of the first concrete performance statements for the QAOA on a problem where its advantage over random guessing could be compared with the best classical guarantee. The average-case technique, an exact single-clause formula followed by an average over independent signs and a dependency count, applies to other local constraint problems.
The statements are proved in the paper by hand; none of them, and no QAOA performance bound, has a machine-checked proof on the platform. The mission produces a verified link from the quantum state to a classical average (25), a finite second-moment method over sign vectors, and an explicit Chebyshev form of the concentration claim.
The central step is (25): turning the expectation of in the state into a classical average over bits. It requires conjugating three Pauli operators through the mixer at , expanding the phase operator around the three bits, and showing that equations sharing two bits with the clause cancel. A direct computation in the -dimensional space does not scale with and does not give a closed form.
For the variance, the naive bound by pairs gives nothing. The argument needs exact independence of clause terms whose sign dependencies are disjoint, which rests on (25) showing that each term depends only on its own sign and on the signs of the equations sharing exactly one bit with it, and then a combinatorial count of linked pairs.
Bit strings are Fin n → Bool with true the bit ; the quantum layer reuses the published QAlgorithms definitions (Qubits, act, prob, uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary). The phase operator is the full count of satisfied equations, which differs from the paper's of (6) by the constant ; the resulting states differ by a global phase and all probabilities agree. Triples are strictly increasing and pairwise distinct, which encodes "exactly three variables" and . is a natural number. is the uniform average over all right-hand-side vectors, over all strings.
Two pins are disclosed. The angle range is added to (50) and the goal, since the lower bound needs . The goal's threshold is (50)'s exact lower bound, not the paper's (54): is the large- limit and is false at every finite , so (51)–(53) are stated as a limit instead. The goal is about the expected satisfied count of the measured state; the sampling procedure, circuit size and the search over are out of scope.
A trivializing reading is excluded: the probability is over the instances on the fixed triples, not over a single instance, and the bound is about the quantum expectation at (at the mean has the opposite sign and the statement would be false).
A complete development needs finite averages over with independence of coordinates, the single-clause formula (25) in the -dimensional Hilbert space, and Chebyshev's inequality on a finite uniform space. The (25) computation and the second-moment count are reusable for other QAOA analyses. Contributions to any milestone are welcome, in any order.
In the classical secretary problem, candidates arrive one at a time in uniformly random order, and a decision maker must accept or reject each one irrevocably. The decision maker sees exact scores, or at least a total ranking of the candidates seen so far. In hiring, admissions and procurement the observed scores are often biased: evaluations of candidates from different groups, or produced by different evaluators, cannot be compared reliably, even when comparisons inside a group can. Salem and Gupta (SSRN 3444283; Management Science, 2023, doi:10.1287/mnsc.2023.4926) model this by giving the algorithm only the comparisons it can trust. These form a partial order on the candidates, and the true scores remain hidden.
The question is how much is lost when only partial ordinal information is available. The paper's answer is governed by the width of the partial order, the largest number of mutually incomparable candidates. Width 1 is the classical totally ordered problem. Width means that no comparison is available at all. This mission formalizes the paper's first positive result with explicit constants: an algorithm, ProxyLabel, whose competitive ratio grows linearly in a known estimate of the width.
A finite set of elements carries a partial order . Each element has a hidden true score . The scores are pairwise distinct and consistent with the order: implies . The width of is the largest size of an antichain, a set of pairwise incomparable elements.
The elements arrive in a uniformly random order. The algorithm knows and a selection capacity . At each time it sees the comparisons of among the elements that have arrived. It may select at most elements, and every decision is irrevocable. The offline optimum is the largest total score of at most elements. An algorithm is -competitive if, on every instance,
where is the total score of the selected elements and the expectation is over the arrival order and the algorithm's randomness.
ProxyLabel (Algorithm 1 of the paper) takes a width estimate . It works as follows.
Each label class therefore contributes at most one element: the first non-sampled one that beats everything of its label seen before.
If for some , then ProxyLabel has competitive ratio at most
with the convention . That is, .
With the exact width , the ratio is at most , and it is for .
Proposition 5.2 shows that partial ordinal information costs at most a factor linear in the width, provided a width estimate within a constant factor is available. Proposition 5.1 of the same paper shows that no algorithm beats ratio , so the bound is order-optimal. ProxyLabel is also the building block of the paper's width-free algorithm PosetLabel (§5.4), which estimates the width from a first sample and then runs ProxyLabel's selection phase.
The result is proved in the paper and has not been machine-checked. A complete development would give a formal model of online selection on a poset under random arrival, with an explicit selection rule and exact finite averages for probabilities. It would also contain a formal use of Dilworth's theorem inside a probabilistic argument, and the elementary inequalities and in the form the proof needs.
The events of the algorithm are tangled. The sample is a prefix of a random order with a random length. Whether an element is selected depends on everything that arrived before it, on the labels, and on whether an earlier element of the same label was already selected. The bound must be proved for every finite poset and every consistent scoring, with exact constants, on the finite probability space of arrival orders, labellings and sample sizes. The width enters only through the structure of a single label class, a subposet whose width is at most , so the argument has to pass from the global width to an arbitrary random subposet.
A tempting simplification lets every passing unsampled element be selected. That algorithm can select several elements of one label, so its expected score is larger and the bound becomes easier. It is not ProxyLabel.
α with a PartialOrder, so is Fintype.card α. The width is the published definition AppliedComb.Posets.width α, the maximum size of an antichain. Dilworth's theorem is the published, proved theorem AppliedComb.Posets.dilworth.α ≃ Fin N, and labellings are functions α → Fin k. Labels are independent of the order, which is the same distribution as assigning labels on arrival.OPT is the maximum of over sets with , so it is the total score when .Contributions are welcome on every milestone. The prefix-of-a-random-order lemma (a binomially sized prefix is an i.i.d. Bernoulli sample) is reusable well beyond this mission.
A firm that sells a network good (a platform, a communication service, a standard) faces consumers whose benefit from buying grows with the number of other buyers. When these network effects are strong, the buying decisions form a coordination game: everybody buying and nobody buying can both be equilibria at the same price and quality. The firm's choice of quality then depends on which equilibrium it expects consumers to play.
The classical answer, going back to Spence's analysis of monopoly quality (Spence 1975), is that a monopolist sets quality for the marginal consumer. Under the usual equilibrium-selection criteria (Pareto dominance, focality) the network-good monopolist inherits this logic. L. T. Chan, Quality Strategies in Network Markets (Management Science, 2023; SSRN copy 4203818), asks what happens when the firm instead anticipates potential maximization, a generalization of risk dominance to many players introduced through the potential games of Monderer and Shapley (1996). The answer is a different first-order condition for quality, in which every consumer's valuation and every possible number of buyers matter. This mission formalizes that condition, Proposition 5 of the paper, together with the chain of results in §3 that leads to it.
There are consumers . Consumer has a valuation , labelled so that . The benefit of the good when consumers buy at quality is weakly increasing in and, in , weakly increasing and differentiable. The firm's cost of quality is weakly increasing and differentiable.
In stage 1 the firm chooses a price and a quality . In stage 2 consumers simultaneously decide whether to buy. If is the set of buyers, consumer receives the payoff (7)
and the firm earns . A buyer set is a Nash equilibrium of stage 2 if no buyer gains by leaving and no non-buyer gains by joining. The market has strong network effects at when is strictly increasing in .
The potential (10) of a buyer set is
A potential maximizer is a buyer set maximizing over all subsets of . A firm that anticipates potential maximization earns when all consumers buying is a potential maximizer, and otherwise. In Lean these objects are Market, Market.Standing, Market.StrongNE, Market.u, Market.IsNash, Market.pot, Market.IsPotMax and Market.profitPM in the namespace NetworkQuality.PotentialMax.
Assume the standing assumptions and strong network effects at every . If maximizes over , and , then
The statement is the necessary first-order condition. It fixes no functional form for or .
The result. Proposition 5 replaces the Spence condition (Proposition 4 of the paper) by one in which the marginal consumer's valuation is replaced by the harmonic mean of all valuations, and the equilibrium benefit by its uniform average over the number of buyers. Comparing it with the social optimum (Proposition 3, arithmetic mean of valuations) shows that a firm worried about miscoordination underprovides quality relative to the planner, increasingly so as valuations become more dispersed, and that it tends to undersupply (oversupply) quality when the number of buyers and quality are complements (substitutes) in the benefit (p. 15).
Formalizing it. The paper's arguments are in the main text (§3.2 and §3.5) and are short; some steps are only sketched: Proposition 1's proof treats only buyer sets of the form , and (12) is derived only in the price range with two equilibria. A machine-checked development makes these steps complete, fixes the tie-breaking convention of the selection, and isolates exactly which assumptions the first-order condition uses (none of the convexity the paper assumes). No part of this result has a machine-checked proof at the time of writing.
The objects are finite and the algebra is elementary, so the difficulty lies in bookkeeping that the paper leaves implicit. The obvious reading of Proposition 1, "consumers to buy", is not forced when valuations tie; excluding an arbitrary buyer set of intermediate size needs a comparison between its weakest buyer and its strongest non-buyer, using the ordering of valuations and nonnegativity of . The characterization (12) is a statement about maximizers over all buyer sets, not just about the two candidates the text compares, so it rests on the reduction "potential maximizer ⇒ Nash equilibrium ⇒ or ". Finally the firm optimizes jointly over price and quality against a discontinuous profit function; the first-order condition only appears after the price has been optimized out at each quality, and it needs differentiability at an interior optimum.
Consumers are Fin n; the paper's consumer is Lean index , while the first argument of is a number of buyers in ℕ, so is ∑ i : Fin n, M.f (i.val + 1) q. and are M.v ⟨0, _⟩ and M.v ⟨n - 1, _⟩. and are total functions on ℝ.
The standing assumptions (Market.Standing, pp. 4 and 9) are: ; and antitone; for and , , weakly increasing in and in on , differentiable on ; on , weakly increasing there and differentiable on . Statements about a single quality add , the paper's domain.
Added hypotheses, each disclosed in the items: equilibria are pure (buyer sets); the goal assumes an interior quality and strong network effects at every ; the "sufficiently convex" cost of p. 4 is dropped, so the goal is the necessary condition only. The profit under potential maximization selects "all buy" at the tie , as the paper's "if and only if " does.
The profit is defined through the selection (IsPotMax over all buyer sets), not as the reduced formula (14), and the goal's optimality hypothesis ranges over price and quality jointly; defining the profit by (14), or restricting maximizers to , would trivialize the mission and is ruled out. Derivatives are deriv, and the standing assumptions guarantee they are genuine at .
Everything needed beyond Mathlib (Finset, deriv, IsLocalMax) is in the single definition file. Proofs of the milestones in any order are welcome, as are proofs of the goal that use the milestones as stepping stones.
Firms that serve several customers from shared capacity, such as a warehouse supplying several retailers, a flexible production line building several products, or an assemble-to-order system, often sign contracts that guarantee each customer an individual service level. Typical targets are the probability of filling a customer's whole demand (Type-I), the expected fraction of demand filled (Type-II or Type-III), each required to be at least a target . Once demand is realized, the firm must decide how to ration the pooled resources among customers. Jiang, Wang and Zhang (SSRN 3385089, published in Operations Research, doi:10.1287/opre.2022.2386) ask how much capacity suffices and which rationing policy meets all targets at least cost. The exact optimal policy is an infinite-dimensional program over randomized policies, (11). This mission formalizes the paper's answer to the second question: a simple, learnable policy is asymptotically optimal.
There are customers and resources. The capacity vector is fixed. The demand is random with law . After observing a demand vector , the firm chooses a solution from a compact set . Here is the demand of customer that is fulfilled and is the amount of resource given to customer . The solution costs , with linear, and customer receives service .
It then adopts at a uniformly drawn iterate .
The Lean development uses the same letters: detService, detCost, IsFeasible, obj11, mwsObjective, mwsIter, stepSize, G, Gstar, Lterm.
Under Assumptions 1 and 3, if is feasible and , then almost surely
Here is a fresh copy of the demand, so each expectation is taken with the iterate fixed. The statement holds for every tie-breaking rule in (16).
Theorem 3 replaces an optimization over probability measures on a space of functions by a sequence of finite-dimensional problems (16) and a one-line dual update. Problem (16) is often solved greedily: under a polymatroid structure the paper's Theorem 4 turns it into an index rule. The result therefore justifies a practical rationing heuristic with a guarantee: a firm that runs Algorithm 1 on historical demand gets a policy whose average cost is asymptotically no worse than the optimum of (11), and whose service levels asymptotically meet every individual target.
On the formal side, the statement and its milestones combine a projected stochastic subgradient method, a triangular array of bounded martingale differences, and the weak duality of a semi-infinite program. The paper proves the result; none of it has been machine-checked. A formal proof must also repair the paper's argument for (28): the stochastic-dominance induction on p. 54 does not establish an almost-sure limit.
The obvious argument treats the iterates as a standard online gradient method with a fixed step. That handles the expected regret but not the almost-sure claim. The noise terms depend on the horizon , both through and through every earlier iterate, so they form a triangular array, not a single martingale. Classical stochastic-approximation theorems with decreasing steps do not apply. Feasibility of enters only through the dual bound . The expectations are over a fresh copy with the random iterate held fixed, and that must be kept separate from the sample the iterate itself uses. The service half (28) needs a bound on the growth of the dual weights (Lemma 6), and that bound itself needs the cost to be bounded on feasible allocations.
Fin n and Fin m. The Lean iterate at index is the page's , and becomes a sum over .Fin n → ℝ is the sup norm.Two formalizations would make (27) trivial, and both are ruled out. is the infimum of the cost over feasible mixtures; it is neither defined from the algorithm nor identified with . Feasibility and keep that infimum from being Lean's junk value . The selection depends on alone, not on or on the sample path.
The development needs Bochner integrals, independence (iIndepFun), conditional expectation and the referenced Azuma and Borel–Cantelli results. The triangular-array strong law for bounded martingale differences with summable exponential tails is reusable beyond this mission. Contributions toward any milestone, or a repaired proof of (28), are welcome.
Many recent quantum algorithms for linear algebra and optimization take their input as a block-encoding: a unitary circuit whose top-left block, after projecting a set of ancilla qubits onto , approximates the matrix of interest. The quantum semidefinite-programming solver of van Apeldoorn and Gilyén (arXiv:1804.05058) introduces the quantum operator model, in which every constraint matrix of the SDP is given this way (Definition 2, p. 4). Block-encodings are also the input format of quantum singular value transformation and of Hamiltonian simulation by qubitization (Low and Chuang, arXiv:1610.06546).
A natural question is where block-encodings come from in applications. In §4.1, on shadow tomography, the constraint matrices are the elements of two-outcome measurements, and what a user can do is perform those measurements, not write down their matrices. The closing remark of §4.1 (pp. 24–25) answers the question for that setting: if a two-outcome measurement can be implemented on a quantum computer with small bias, then a block-encoding of its measurement operator can be built from the same circuit with one extra qubit and one CNOT gate. The remark is credited to the same observation by Low and Chuang (arXiv:1707.05391).
A two-outcome POVM on a finite-dimensional system is a pair of operators with and positive semidefinite. A mixed state (density matrix) is a positive semidefinite operator with ; outcome occurs with probability .
An implementation of the measurement on a quantum computer, as the paper fixes it, takes the input , attaches ancilla qubits in the state , applies a unitary to system and ancillas, measures in the computational basis, and accepts when the last qubit reads :
The implementation has bias at most if, for every state ,
Write , an operator on the system. A unitary on ancilla qubits and the system is an -block-encoding of (Definition 2) if in the operator norm. Finally adds one fresh qubit, and is a CNOT gate whose control is the measured qubit and whose target is the fresh qubit.
The subnormalization is , the ancilla count is and the error is the same as the bias; none of these is weakened.
The result. It converts an operational primitive, performing a measurement, into the input format that block-encoding algorithms consume, with an additive error equal to the measurement's bias and at the cost of one qubit and one CNOT. In the paper it is what makes the shadow-tomography application of §4.1 meaningful: the cost of the SDP solver is stated in terms of block-encodings of the , and this remark lets one replace that by the cost of controlled implementations of the measurements. More generally it shows that the quantum operator model is no stronger than the ability to measure.
Formalizing it. The paper proves the remark in a few displayed lines, one of which ("it is easy to see") is left to the reader and whose CNOT direction is not printed. No machine-checked version exists. A formal proof fixes the register conventions, makes the direction of the CNOT explicit, and contributes a reusable fact about matrices: for a Hermitian , over density matrices. The block-encoding predicate itself is already published on the platform and is reused.
The algebra of milestones 1 and 3 is bookkeeping over tensor-product index sets, and the main cost there is choosing representations that make the registers line up.
The one step with mathematical content is the direction "" of milestone 2. The bias condition controls only for density matrices , that is, it bounds the numerical radius of , while a block-encoding needs the operator norm. For a general matrix these differ by up to a factor of two, so the step needs to be Hermitian: is Hermitian as a POVM element, and is Hermitian because it is a compression of the projector . A formal proof must use both facts and exhibit a state that attains the norm.
The Lean development lives in the namespace QuantumSDP18.MeasureBE. Its conventions are:
QAlgorithms.specNorm.Qubits c × Bool, so and the Bool factor is the last, measured qubit. The basis state of any register is its all-false index.PosSemidef with trace ), and its absolute value is the modulus of a complex trace.QAlgorithms.cnot (control first), placed on the measured qubit (control) and the fresh qubit (target). With the opposite direction the block is and the goal is false; the chosen direction is the only reading under which the page's identity holds.QAlgorithms.IsBlockEncoding, which puts the ancilla register first, as Definition 2 does; the circuit, written system-first as on p. 25, is reindexed to match.The goal keeps both POVM hypotheses ( and ), and the bias condition quantifies over all states rather than one fixed state, under which the conclusion would be false. A formalization in which (14) ranges over arbitrary matrices, or which drops the CNOT and states only , is a different theorem.
Needed infrastructure: Kronecker products and reindexing of matrices, the unitarity of permutation matrices and of Kronecker products, and the variational characterization of the operator norm of a Hermitian matrix through its eigenvectors. The last is reusable beyond this mission. Proofs of the three milestones are welcome independently.
Many quantum algorithms end in a measurement that succeeds only with some probability . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate with error of order after applications of , where classical sampling needs order samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.
Timeline:
Let be a finite-dimensional Hilbert space with computational basis and a distinguished zero state . A quantum algorithm without measurements is a unitary matrix on , and a Boolean function calls a basis state good when . Write for the splitting into the projections onto the good and the bad subspaces. The initial success probability is , the probability that measuring gives a good state, and is the angle with .
The operator flips the sign of the amplitudes of good states, flips the sign of the amplitude of , and the amplification operator is
For an integer , the quantum Fourier transform is , and the controlled power is . The phase state is , and is the circular distance. The algorithm applies to , measures the first register to obtain , and outputs .
For every positive integer , the event
has probability at least when , and greater than when . If then with certainty. If and is even, then with certainty.
Further statements from the same development are included as companion targets: the success probability after rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized ), Theorem 13 (counting) and Corollary 14.
Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as in the number of applications of , and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for make the estimator usable as a zero-error test for the existence of a good state.
All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: , the strict tail bound , and the additive term . It also covers every modulus , not only powers of two, and arbitrary and , not only uniform search. Related statements are posed on the platform but unproved:
QAlgorithms.Nannicini.amplitudeEstimation_error is the special case , , with a bit-string presentation of the algorithm.QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the half of Theorem 2.The Grover theorems already proved on the platform treat a single marked item with a uniform start.
The obvious argument has two parts: rotates a plane by , and phase estimation reads off . Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of , and that holds only for . The goal does not assume this: the degenerate cases , where do not exist, must be handled separately.
On the phase-estimation side, the tail bound for must be strict and must hold for every . The bound for relies on a minimization over that needs , while the goal has no such hypothesis, so the small cases need their own argument. Finally, the second eigenphase appears as , and the matching outcome wraps to at .
States are vectors over a finite type (the paper writes ), operators are matrices, and is Bool. is assumed unitary and is written . The second register is Fin M with ; is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), is its conjugate transpose, and is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. is computed from , and , and . The goal assumes neither nor , and it keeps the strict inequality for . The step "after step 2, ignoring global phase" is stated with its phase written out.
A formalization that takes or as a free parameter, assumes the mixture form of the outcome law, or reasons about without deriving them from and would make the goal trivial. The statements here do none of these: every quantity is computed from , , and . The clauses "uses exactly evaluations of " (Theorem 12) and "requires exactly evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending to the uniform superposition, which includes , as the paper allows on p. 20.
A complete development needs:
The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.
In inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.
The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.
Costs lie on the unit sphere of , . In period nature presents a feasible set , compact, nonempty and of diameter at most , and a -Lipschitz context . The forward problem with cost has solution set . The decision-maker plays some , nature reveals an expert action for the true cost , and the regret over periods is
The knowledge set is the set of costs in the initial set under which every expert action seen so far was optimal.
The angle between nonzero vectors is , and the uncertainty angle of a set is ; a minimizing is a circumcenter. The initial set is pointed when .
For a positive diagonal and an orthonormal , the ellipsoidal cone is
a cone with axis and elliptical cross-section. The effective difference of period is (and if the difference vanishes).
EllipsoidalCones with parameter starts from the circular cone , a circumcenter of , and plays the axis as proxy cost. With it keeps the cone if
and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.
With there is an absolute constant such that for every , , closed pointed with , , admissible instances and run,
The constant is left unfixed: the shape is the claim, and the proof's explicit constant rests on a step that fails at .
The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.
The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the case of Lemma B-1.
Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.
Costs live in EuclideanSpace ℝ (Fin (m+1)) with , actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. is stored as its diagonal , as a real orthogonal matrix, and is written . Lean periods are -based: Lean period is the paper's period . This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.
Standing assumptions carried by the statements: , , feasible sets nonempty, compact and of diameter at most , contexts -Lipschitz, a closed subset of , . Pinned and disclosed choices:
The run predicate is satisfiable: a circumcenter of a closed nonempty exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of is nonzero. A formalization in which no run exists, or in which may depend on or , does not state Theorem 3.
A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.
Digital markets with strong network effects (messaging, social networks, app stores) tend to concentrate: a platform with more users is worth more to each user. Interoperability, the ability of a platform's users to interact with the users of rival platforms, is a central remedy in current competition policy; the EU Digital Markets Act (2022) mandates it for messaging services offered by designated gatekeepers. Whether interoperability actually reduces the market share of a dominant platform is a question about equilibria of a pricing game.
Ekmekci, White and Wu (Management Science, 2025) answer it in a model of platform competition built on net fees. Their Proposition 6 shows, for a Logit duopoly, that lowering interoperability always admits an equilibrium with an even larger dominant platform; equivalently, interoperability may mitigate dominance. This mission formalizes that result and the steps of its proof.
There are two platforms and one side of users. Platform chooses a net fee : the price a user pays, net of the interaction value the platform extracts once the user has joined. With Logit demand and no outside option, platform 's market share at the fee profile is
Both platforms have marginal cost , and each user values each other user of the same platform at , the network externality. The degree of interoperability lets a user of platform also enjoy per user of the rival platform (the paper's (19)), and the platform extracts this value too. Platform 's profit is
A fee profile is a Nash equilibrium in net fees under if no platform can raise its profit by changing its own fee to any other real number. In an equilibrium with , platform is the dominant platform.
The Lean development (namespace NetFeePlatform.InteropDominance) writes as demand 0 t j (the 0 is the weight of the absent outside option), as profit 0 c γ lam t j, and equilibrium as IsEquilibrium 0 c γ lam t, with t : Fin 2 → ℝ.
Let , and . If is an equilibrium under and , then there is an equilibrium under with
The equilibrium is not unique in general, and the statement does not say which one; it asserts existence, exactly as the paper does.
The result. Proposition 6 is the paper's argument that interoperability mandates can reduce concentration without any change in the platforms' cost or quality: at a fixed network externality, every equilibrium with a dominant platform under a higher degree of interoperability is outsized by an equilibrium under a lower degree, so the largest dominant share an equilibrium can sustain does not increase as interoperability rises. The proof rests on the equivalence of item 4, under which interoperability acts as a reduction of the effective network externality from to ; Figure 2 of the paper plots the resulting largest equilibrium share as varies at .
Formalizing it. The paper's proof is three paragraphs, and it identifies equilibria with zeros of . A formal proof has to supply what the text takes for granted: that the first-order condition is necessary at a global Nash equilibrium, that it is sufficient in the stated range, and that a zero of can be turned back into a fee profile. No part of the result has been machine-checked before. A complete development also gives a reusable treatment of Logit demand and of best responses in one-variable concave games.
The algebra of and the intermediate value step are short. The work lies in the equilibrium notion. A Nash equilibrium is a global condition over every unilateral deviation , and profit is not concave in the platform's own fee. Measured against the platform's own share , profit has second derivative ; it is concave exactly when does not exceed the minimum of . Outside that range the first-order condition is not sufficient, and a zero of need not be an equilibrium; the paper does not treat that case.
Fin 2, Logit demand with no outside option (outside weight , literally), common and , interoperability written lam. The Setting file states the general -platform objects (demand with an outside-option weight , profit with the interoperability term , equilibrium, the diversion ratio of (32)); this mission uses them at , .demand 0 t j at a fee profile, never free variables. Profit keeps the interoperability term; without it would not enter the model at all.Markets organized by platforms (social networks, marketplaces, messaging services) exhibit network effects: a user values a platform more when more users join it. A standing concern in competition policy is that such markets "tip" towards one dominant platform, and the usual remedy proposed is to foster entry. Ekmekci, White and Wu (Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025) develop a tractable model of platform oligopoly in which platforms compete in net fees, the price a user pays net of the interaction value the platform delivers, and use it to examine policy interventions. Their Proposition 4 shows that the intuition "more platforms, less dominance" can fail: with strong network effects, adding a third platform to a duopoly can produce an equilibrium whose leader is larger than any platform of any duopoly equilibrium.
The net-fee approach is the authors' alternative to the "insulated equilibrium" of White and Weyl (2016); the paper's §5 specializes it to Logit demand, where pricing formulas are explicit.
There are platforms and one side of users. Platform charges a net fee ; write . Demand has the Logit form (13): with outside-option weight ,
and in this mission there is no outside option, , so the shares sum to one. Platforms are ex ante identical: common marginal cost and common interaction value . Platform 's profit ((8) with one side) is
the net fee plus the interaction value the platform extracts per user, less cost, times its share. A net-fee equilibrium is a pure-strategy Nash equilibrium: no platform can raise by changing its own net fee to any . Duopoly is , triopoly .
At an equilibrium, each net fee satisfies the Logit pricing formula (14), . For equilibria with one dominant platform of share and equal small platforms of share , the paper reduces the equilibrium conditions to a zero of the characterization function
For : duopoly has an equilibrium, and there exist a triopoly equilibrium and a platform with
The comparison is against every duopoly equilibrium and every platform in it, not against one selected equilibrium.
The result. Proposition 4 is a counterexample to a policy presumption: entry need not reduce concentration in markets with network effects. With a third platform, the two small platforms can split the fringe so thinly that the leader's share rises above anything sustainable in a duopoly. The result identifies an explicit parameter window; together with the companion results on interoperability (Propositions 6 and 7 of the same paper), it frames which interventions reduce dominance in this model.
Formalizing it. The proposition is proved in the paper partly by a numerical check ("we can verify", p. 50), and its printed interval is slightly too wide at the bottom: at the symmetric duopoly equilibrium the paper's own criterion requires . A machine-checked proof would settle the corrected statement, replace the numerical step by an argument, and make the equilibrium characterization through (including the step from first-order conditions to global Nash equilibrium) available for the other results of the series. None of these statements is formalized anywhere to our knowledge.
Three steps resist the obvious argument.
NetFeePlatform.Competition. The definitions file Setting declares the Logit demand demand w t j, the profit profit w c γ lam t j (with an interoperability term , set to throughout this mission), the global Nash predicate IsEquilibrium, and the diversion ratio; GChar declares . Platforms are indexed by Fin J.Affirmative action policies are usually designed reductively: one adjustment for women, another for a racial minority, a third for applicants from low-income families. An applicant who belongs to several categories gets the combined adjustments. A long literature in sociology and law, beginning with Crenshaw's account of intersectionality (1989), argues that people at the intersection of several disadvantaged categories (for instance Black women) can stay underrepresented even when every single category is proportionally represented. Carvalho, Pradelski and Williams, Intersectionality: Affirmative Action with Multidimensional Identities (Management Science, 2025), give this debate a decision-theoretic model. They ask whether any policy that treats identity dimensions independently can achieve proportional representation of every intersectional group.
Their first main result answers that question for a general class of score adjustments and for generic score distributions. This mission formalizes that result, Theorem 1, together with the lemmas its proof uses.
A decision maker admits a share of a unit-mass pool of applicants. Each applicant has a score in an interval and an identity , with . Category is the set of identities with . Write and for the vectors of zeros and ones and for the -th basis vector. The identity equals when the sum is computed coordinatewise in the integers.
The population is a probability measure on , with marginal masses . The space consists of those whose conditional score laws are continuous (atomless) and have full support on . carries the relative weak topology, the topology of weak convergence of probability measures.
A policy family is a set of strictly increasing bijections that is rich (for all some has ) and commutative (). Additive shifts on are an example. A policy assigns to each identity a map . Given a threshold , an applicant of group is accepted when , subject to the capacity constraint
The accepted share of is , the fraction of the accepted who belong to . The outcome is representative if for every (Definition 2). A policy is nonintersectional if implies , and intersectional otherwise (Definition 1). Nonintersectional policies are the reductive ones: is the composition of the maps over the categories that belongs to.
A property is generic in if it holds on a dense open subset of . Theorem 1 states: there is a dense open such that for every ,
"Yields a representative outcome" means that some threshold satisfies the capacity constraint at level and gives for every . Nothing about is fixed beyond richness and commutativity, and nothing about beyond membership in .
The result. Theorem 1 separates two classes of policy. The reductive class, which covers the way most affirmative action programmes are written, cannot generically deliver proportional representation of intersectional groups, however its category-wise adjustments are tuned. A policy that adjusts each intersectional group separately can. The negative part holds for every rich commutative family, not only for additive or multiplicative adjustments, so the impossibility does not come from a particular functional form. The later results of the paper build on this one. They measure how badly reductive policies fail, give the nongeneric conditions under which they succeed (Proposition 3, which is the subject of the companion mission), and treat imperfectly intersectional policies.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization has to make several things precise:
The paper's proof of Lemma 2 also concludes with a formula valid only for the additive family (p. 23), so a complete formal proof would supply the missing argument for a general .
Part (b) and the necessary conditions behind part (a) follow from the definitions. The hard step is genericity (Lemma 2). Openness requires the quantiles to depend continuously on in the weak topology. It also requires the map to be continuous, where each is itself determined by and . The obvious argument writes this map as an explicit formula, , and that formula holds only for additive shifts. For a general rich commutative family, continuity of the transport map must come from the structure of as a group of homeomorphisms of an interval acting freely and transitively. Density requires perturbing the law of group while keeping the perturbation inside . This is where enters: for , and there is nothing to perturb independently.
The Lean development fixes the following conventions.
Fin n → Bool, and is checked coordinatewise on Bool.toNat.ProbabilityMeasures on , whose Mathlib topology is that of weak convergence. is the subtype of measures for which every group of positive mass has no atoms and positive mass on every nonempty open subinterval of .Several trivializing formalizations are ruled out:
A complete development needs:
The first two are reusable well beyond this mission. Contributions to any milestone are welcome, and proofs of the quantile-continuity facts as standalone lemmas are especially useful.