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?
A one-warehouse, multi-retailer (OWMR) distribution system is the basic model of a supply chain in which a central warehouse buys from an outside supplier and ships to several retail locations. When every shipment carries a fixed cost and a positive lead time, the optimal policy of the stochastic system is unknown, and the classical approach is to search over a structured class of policies and bound its cost. Exact evaluation of even a simple policy is hard, because the warehouse can run out of stock and then the retailers' replenishments interact.
Zhu, Chen, Hu and Yang (SSRN 2921743; Operations Research, 2021, doi:10.1287/opre.2021.2101) study modified echelon policies for continuous-review OWMR systems with Poisson demand. Their central tool is an explicit upper bound on the long-run average cost of any such policy, written as the retailers' single-stage costs, a warehouse term that depends on the retailer policies, and a fixed-cost allowance. Their heuristic policy, its worst-case performance guarantee and its asymptotic optimality (Theorems 2–4 of the paper) are all built on this bound. The single-stage cost functions follow Zheng (1992) and the echelon cost accounting follows Chen and Zheng (1994).
There are retailers, indexed , and one warehouse, indexed . Retailer faces Poisson demand of rate , independent across retailers, so the warehouse sees Poisson demand of rate . Installation has a constant lead time , a fixed cost per shipment, and an echelon holding cost rate ; unmet retailer demand is backlogged at rate . Write .
A modified echelon policy has reorder levels and order quantities for every installation. When the echelon inventory position of installation is at or below and the upstream installation has stock on hand, a shipment raises as close as possible to .
With the lead-time demand of retailer , the single-stage holding-and-backlog rate and the single-stage cost are
With , and , the envelope of Lemma 3 at warehouse echelon level is
With , set , and
The long-run average system cost is (1) of the paper,
where is the expected cost rate of all retailers when the warehouse inventory position is .
It is stated for every policy, with no assumption on the parameters beyond .
The bound replaces the cost of an -installation stochastic system, which has no closed form, by computable retailer costs and a warehouse term. This is what makes the paper's heuristic policy computable and what its performance guarantees compare against: each retailer uses its single-stage optimal , and the warehouse minimizes the remaining term. Bounds of this decomposition type are a standard device in multi-echelon inventory theory, and Lemma 3's envelope, which charges each retailer at the lowest inventory position the others can leave it, is the step specific to the distribution setting.
The result is proved in the paper's online appendix. It has not been formalized. A formal development adds to the platform a single-stage cost with Poisson lead-time demand, the echelon envelope of Lemma 3 for general , and an explicit OWMR cost decomposition, all of which are reusable by later work on distribution systems, including the paper's own performance bounds.
The core is Lemma 3 for general . Bounding each retailer separately by its worst case fails, because a retailer below its reorder level can have a much larger cost rate ; the bound must use that the inventory positions are coupled through the warehouse echelon level. The printed proof is an induction on whose step needs convexity of a sum in which one term is only bounded by a convex function, so the order of bounding and convexity arguments matters. Convexity and continuity of (a Poisson mixture of piecewise-linear functions) must be established, and every expectation against the Poisson law needs an integrability argument, since the integrands grow linearly.
All declarations live in the namespace DistribRQ.UpperBound. Retailers are indexed by Fin N with [NeZero N]; the warehouse data are separate. The primitives are bundled in Primitives N (all rates and costs positive) and the policy in Policy N (real ; ), following the paper's continuous approximation (p. 7). Poisson expectations are Bochner integrals over against poissonMeasure, evaluated at real arguments . is the supremum of over , since the paper's need not be attained on a half-open interval.
The sample-path model (cycles, shipment intervals, the paper's Lemmas 1–2) has no substrate, so the system is encoded as the paper's proof uses it:
is never a free function bounded by , the feasible set keeps the clause for positive warehouse stock, and , , are computed from the Poisson law rather than taken as parameters; formalizations that relax any of these, or that rely on a junk value of sSup, an integral or a division, trivialize the statement and are not accepted.
Contributions welcome: convexity and continuity of , Poisson integrability lemmas, Lemma 3 for general , and the averaging steps of App. A (8)–(10).
In sequential multi-class diagnosis, a decision maker observes a system repeatedly, then chooses when to stop and which hidden class to report. Each new observation can improve the diagnosis, but waiting has a cost. A direct dynamic program uses the vector of posterior class probabilities as its state. With possible classes, that state lies in an -dimensional probability simplex. Wang's model asks when the observed sequence can instead be summarized by fewer coordinates, so that the same posterior can be recovered without retaining a full belief vector as an independent state Wang, §2–§3.
The paper considers class distributions related by exponential tilting. This relationship appears in common one-dimensional distribution families, including the normal, binomial, Poisson, and gamma examples collected in its Table 1 Wang, p. 8. The result targeted here is the belief reconstruction identity of Theorem 1. Later parts of the paper use the reduced statistic in optimality equations and study stopping regions; those results are outside this mission Wang, pp. 12–18.
The hidden class is . Before observing data, the decision maker has a prior belief : every component is nonnegative and their sum is one. Conditional on class , observations are independent and have the same density on the observation space . Class supplies a baseline density . The one-step Bayesian operator multiplies each current class weight by that class's likelihood at the new observation and divides by the sum of all weighted likelihoods. Starting at , the belief is obtained by applying once for each observation in arrival order Wang, pp. 6–7.
In the exponential tilting model, a transformed observation and a parameter describe each nonbaseline density:
Here . Place the in the rows of the diagnostic parameter matrix . Its rank decomposition is , where has rows and linearly independent columns, while has linearly independent rows and columns. Thus . The paper calls the reconstruction matrix and the projection matrix Wang, Definition 1, p. 8.
For , define the diagnostic statistic . For classes , the target identity is
The baseline coordinate is . The normalizer appearing in is evaluated from the row , as in equation (3), and the theorem identifies it with the model normalizer through . The target also identifies the set of posteriors reachable after exactly observations with , where is the set of attainable diagnostic statistics. These statements give a precise reading of the paper's claim that reachable beliefs admit an -coordinate representation Wang, Theorem 1, p. 9; Definition 2, p. 10.
The goal additionally states that the map is injective on when every prior component is positive. This is an explicit, qualified reading of the paper's phrase that the dimensionality is equal to . For discrete observations, the reachable set can be finite, so the phrase cannot always mean its geometric dimension is literally . The five milestones follow the source's Bayes operator and the displayed identities in its proof of Theorem 1 Wang, p. ec1.
The formula determines every posterior component from real coordinates, the prior, and the observation count. When is smaller than , this supplies the representation used by the paper to reformulate a diagnosis problem in a smaller state space. The paper's examples show cases with one or two diagnostic coordinates; Proposition 1 then rewrites its optimality equations using those coordinates Wang, pp. 9–12. This mission formalizes the reconstruction claim itself, including the exact reachable-set statement, while leaving the decision costs and Bellman equations for later work.
A completed development would provide reusable definitions for a finite-class Bayes update and its sequential iterate, an exponential-tilting model over densities, and a rank-factorized reconstruction map. The result is proved in the cited paper. The Lean declarations in this proposal compile as statements, but their sorry bodies are open proof obligations; this mission seeks machine-checked proofs of them.
The main verification burden is connecting several expressions for the same posterior without quietly replacing one definition by another. A sequential posterior is an iterated one-step update; the paper's closed form is a normalized product of likelihoods; and equation (3) is an exponential expression in a projected sum of transformed observations. Each form has its own denominator, so the positivity conditions that make division meaningful must be stated. The rank claim also requires full-rank assumptions on both factors of . For a prior with zero mass on a class, the posterior formula remains meaningful, but the injectivity assertion needs a separate full-support condition.
Lean represents classes by Fin (N + 1), with class zero as the baseline. Row i : Fin N of the diagnostic matrix is class i.succ. Observations form a List in arrival order; is its length, and the posterior is the list fold of . The observation space is a measurable type with a reference measure , covering continuous and discrete densities with one notation. This generalizes the paper's ; no order or arithmetic operation on observations is used by Theorem 1. Integrals are real-valued, and and are permitted. The reconstruction identity is stated for , matching the paper and avoiding the division by zero in .
The standing assumptions say that every is measurable, is positive at every admitted observation, its integral is one, and each tilted baseline density is integrable. These make the normalizers and the Bayesian denominators meaningful. Positivity, normalization, and integrability are explicit refinements of the paper's use of densities and normalizing constants. The prior lies in the standard simplex; need not be positive for reconstruction. The additional full-support condition appears only in the injectivity clause. The paper's conditional independence assumption is represented by multiplying class likelihoods along the list.
The generic Bayesian update and its reachable set are separate from the paper-specific model. In particular, the posterior is an actual fold of the one-step update, and the class densities are given data constrained by exponential tilting. Defining the posterior directly as equation (3), or defining the densities to make the tilting identity true by construction, would erase the result being formalized. A complete proof needs finite-sum identities, exponential and logarithm facts, integrability facts, matrix rank and row identities, and the algebra of probability normalization. The generic Bayes definitions and list-level likelihood identity are reusable beyond this paper; contributions that establish those interfaces or close any source-derived milestone are welcome.
Call centers, hospital wards and other service systems with many agents serve several customer classes, and customers who wait too long hang up or leave. The standard model is the multiclass many-server queue with reneging: identical servers, classes, class-dependent service-time and patience-time distributions, and a control policy that decides when an idle server takes a customer and from which class. Exact analysis is out of reach once service and patience times are not exponential, so performance is studied through fluid limits: the limit of the system scaled by as .
A. L. Puha and A. R. Ward (MOR 2022, doi:10.1287/moor.2021.1166) prove such a limit theorem for general service and patience distributions, batch arrivals and an arbitrary admissible head-of-the-line policy, including policies that idle or randomize. Earlier results covered one class without reneging (Kaspi and Ramanan, Ann. Appl. Probab. 2011), one class with reneging and unit arrivals (Kang and Ramanan, Ann. Appl. Probab. 2010), and static priority policies (Atar, Kaspi and Shimkin, Math. Oper. Res. 2014).
Fix classes. Class has a service-time distribution on with density , and a patience-time distribution on with density on , so a customer may never abandon. For a distribution with density , is the right edge of its support and on is its hazard function.
In the -th queue, class- customers arrive by a counting process that may jump by more than one. The state is : counts class- customers in system; is the age-in-service measure, a unit atom at the service age of each class- customer in service; and is the potential-queue measure, a unit atom at the time in system of each class- customer whose patience has not run out. The control enters only through the entry-into-service times. A head-of-the-line (HL) policy serves each class in order of arrival. It is admissible when the entry-into-service process is adapted to the filtration generated by the state history and the policy's own independent uniform random variables.
The fluid model works on the state space of finite measures with the weak topology. Given an arrival function (nondecreasing, rcll, ), a path defines the auxiliary functions , , , , , and the reneging function
A fluid model solution for satisfies the constraints (35)–(37), the monotonicity of , the balance law , and the transport equations (46)–(47) for and driven by and .
Under Assumptions 4 and 5, for every sequence of admissible HL policies:
and every distributional limit point is, almost surely, a continuous fluid model solution for started from , with continuous auxiliary functions and each charging no points. Assumptions 1–3 ask that the scaled arrivals and initial states converge. Assumption 4 asks that the hazards be bounded or lower semicontinuous near the right edges . Assumption 5 adds continuity of , an atomless , and control of by C-tightness or by inequality (55).
Theorem 1 characterizes fluid limits for every admissible HL policy at once. To get the fluid limit of a specific policy, one adds the equations that policy imposes and proves uniqueness for the resulting system; the paper does this for weighted random buffer selection (its Theorems 3–5). The reneging equation (40) is the main new feature: abandonment depends on the whole distribution of waiting times in queue, not only on the queue length. Allowing batch arrivals means the reneging count can only be sandwiched between two compensators, which is why Lemma 6 is needed.
The results are proved in the paper, with parts of the tightness argument delegated to Kang–Ramanan and Kaspi–Ramanan. None of them is formalized. The mission defines from scratch a measure-valued queue with abandonment, the Skorokhod space with convergence, and the fluid model of §3. These definitions are reusable for the single-class models of Kaspi–Ramanan and Kang–Ramanan, for the WRBS and static-priority policies, and for other measure-valued fluid limits.
Each milestone is a known argument, but the obvious route to the goal breaks at the reneging term. A naive limit passage in the prelimit reneging count fails: with batch arrivals, is not a functional of and alone, because customers with equal waiting times may be split between queue and service. Identifying the limit as the nonlinear function (40) requires bounds from above and below by marked point processes. It also requires showing that the compensators of these processes converge to a common limit, which uses that charges no points along the limit. The tightness part needs Kurtz–Jakubowski criteria for measure-valued processes on spaces whose right end may carry escaping mass. Lemma 6 is a pathwise identity for finite counting measures, and Lemma 7 is a pathwise bound.
Classes are Fin J with . Time is ℝ≥0. Customers are indexed by integers as in the paper. Event times are extended reals: a patience of keeps a customer in the potential queue forever, and an entry time of means the customer is never served. is FiniteMeasure on the subtype of ℝ≥0. convergence uses one time change for all coordinates, with the maximum of the sup-norm and Lévy–Prokhorov distances on . Convergence in distribution, distributional limit points, relative compactness and C-tightness are stated in coupling form; on the Polish space these are equivalent to the usual notions. Hazards take values in and are off . The integrals in (37), (40), (41), Lemma 6 and Lemma 7 are integrals of nonnegative functions. The derivative indicators that define the departure, reneging and marked processes are written as explicit counts.
Four readings are disclosed in the items. The goal's initial condition is stated through a coupling carrying jointly, because the limit point lives on its own probability space. in (46)–(47) are read as . In Lemma 8, the (K.2) branch of Assumption 2 is read as relative compactness of , because the printed (K.2) does not imply it. The goal encodes Assumption 2 as printed. The head-of-the-line order is the HL condition stated in words on pp. 8–9 rather than inequality (10) alone, which would let a policy skip a waiting customer for good and serve younger ones.
The statement admits trivializing formalizations, and they are excluded here. The HL predicate contains only the defining constraints of Definitions 1–3: entry no earlier than arrival and before abandonment (9), the head-of-the-line order (the HL condition of pp. 8–9, which contains (10): a customer can enter service only after every earlier customer of its class has entered or abandoned), the state constraints (S.1), (S.2), (15) and (16), and rcll paths. The identities (18)–(26) are not in it. All standing independence and distributional hypotheses and the adaptedness of are explicit. The auxiliary functions are computed from the path, never chosen. The policy is not specialized: idling and randomization are allowed.
Not posed: Lemmas 3–5, 9 and 10, Theorem 2, and Lemma 2 (ii) and (iv). Lemma 4 needs a server-assignment filtration, Lemma 5 needs predictable quadratic variations, and Theorem 2, Lemma 9 and Lemma 10 need measure-valued marked point processes on . Formalizing these, or a sorry-free construction of an admissible system satisfying Assumptions 1–5, is welcome.
In continuous-review inventory systems with backlogging, the classical constant base-stock (CBS) policy orders one unit whenever one unit of demand arrives, so that the inventory position (net inventory plus in-transit inventory) stays constant. Under CBS with Poisson demand of rate and i.i.d. lead times with mean , the in-transit inventory has a Poisson law with mean , and the steady-state net inventory level fluctuates on the scale : . Average holding and backlog costs therefore grow like .
Stolyar and Wang (arXiv:1801.02646, Operations Research 2022) observe that when lead times are random and orders may cross, an inventory manager can exploit the randomness: by ordering more aggressively when the inventory level is low and less when it is high, the variance of the inventory level can be reduced. Their generalized base-stock (GBS) policy implements this with a single gain parameter . The main theoretical result, Theorem 1, identifies the diffusion-scale steady-state law of the inventory level under GBS when lead times are exponential: it is normal with variance , a factor below the CBS variance. With (Corollary 2), the scaled average cost tends to , so GBS becomes infinitely better than CBS in the limit.
Demand units (customers) arrive as a Poisson process of rate . Supply units (items) are ordered by the policy and each arrives after an independent exponential lead time with mean . Let be the net inventory level (positive or negative, backlog allowed) and the number of items in transit. Write , , , .
The GBS policy has an integer gain , a truncation level and a centering . With it uses the target and the truncated target
At every arrival: a customer sets ; an item sets , . Then is recomputed and items are ordered, . Under exponential lead times is a continuous-time Markov chain on with customer rate and item rate .
The systems are indexed by , with satisfying
and arbitrary. A stationary distribution of a countable chain with rates and exit rates is a probability mass function with finite mean exit rate satisfying global balance .
For every some state is reachable from every state, for all large the chain has a unique stationary distribution, and for every choice of stationary distributions
In proof order: the stability part of Theorem 1; the conservation law (14); the mean bound for the reflected random walk that dominates the order gap (p. 16, EC.3); Lemma 4, ; the conservation law (19) and Lemma 5 for the artificial process, a birth–death chain that keeps exactly; Corollary 6; the stochastic comparison Lemma 8, and ; the target-gap bound (31); the transfer Lemma 9; and the reduction (36), . For §4 milestones the centering is , as in the paper (p. 12).
The result. Theorem 1 quantifies the value of random lead times: the GBS policy divides the asymptotic variance of the steady-state inventory level by , and the half-normal limits of give the asymptotic holding and backlog costs, which is what makes the cost comparison with CBS (bounds (12)–(13) and Corollary 2) possible. The artificial-process comparison and Lemma 9 form a reusable template for transferring a diffusion limit from a tractable one-dimensional chain to a higher-dimensional controlled chain.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission formalizes the GBS chain itself as explicit transition rates, so the theorem cannot be discharged by a model that only resembles the policy. The stability part is only sketched in the paper ("We omit further details of the stability proof", p. 13), so a complete formal proof also fills that gap. Lemma 5 is a stationary Halfin–Whitt-type limit for a birth–death chain with state-dependent up-rates, including uniform integrability of the scaled tails.
The two-dimensional chain has no product form, and its in-transit inventory does not track the target: after an item arrival rises by one while the target falls by , but only one item leaves transit, so overshoots its target and the gap is random. The natural argument, "the chain behaves like the birth–death chain with ", fails on two counts: the steady-state gap must be bounded uniformly in (Lemma 4), although the rates of the chain grow with and is unbounded on the state space, and the truncations of at and at produce error terms that must vanish after scaling (Corollary 6). Stochastic order alone gives only an inequality between the two laws; closing it needs the mean identity (36), which rests on the exact conservation laws (14) and (19).
All objects live in the namespace RandomLeadGBS.Diffusion. The state is ; the demand rate is real and along atTop. The parameters are , with , with and (10), and arbitrary . The policy is encoded literally: target (4), truncated target (5), order step applied after every arrival; the item rate is and the cap is (not ).
Conventions committed to:
gaussianReal 0 (1/(βγ));The goal concerns the two-dimensional GBS chain; stating it for the artificial chain, or only for an empty family of stationary laws, would trivialize it. The uniqueness clause and the existence clause of Lemma 5 rule out the vacuous reading.
A complete development needs a theory of stationary laws of countable continuous-time chains (existence via drift/Foster criteria, embedded-chain time change), birth–death stationary laws and their local normal asymptotics, and stochastic comparison of chains by coupling. The countable-chain stationarity layer and Lemma 9 are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome. Propositions 3 and 7 (generic comparison results used for Lemma 4 and Lemma 8) are not posed as milestones.
A seller that supplies several competing buyers may negotiate a wholesale price with each of them independently and simultaneously (simultaneous negotiation, SN), or may commit to charge all of them the same price (price-matching negotiation, PM). PM is the bargaining counterpart of the most-favoured-customer clause, a contractual guarantee that a customer receives the best price the vendor gives anyone. Retailers such as Walmart and Costco demand such clauses from common suppliers, and buyers command them expecting to obtain the same price as their rivals (Shang and Cai, §1). Shang and Cai (MSOM, 2021; SSRN 3021563) ask who benefits from PM relative to SN when wholesale prices are the outcome of Nash bargaining between the seller and each buyer, and show that with symmetric buyers PM benefits the seller and hurts both buyers.
The model builds on the bilateral-bargaining framework of Horn and Wolinsky (1988), in which a common supplier negotiates simultaneously with competing downstream firms, and on the analysis of negotiated wholesale contracts by O'Brien and Shaffer (2005, RAND Journal of Economics 36, 573–595) and Dukes, Gal-Or and Srinivasan (2006).
A seller supplies an intermediate good to Buyer 1 and Buyer 2, who each turn one unit of it into one unit of a substitutable end product. With demand base and substitutability , retail prices and quantities satisfy the reverse demand system , .
The game has two stages.
If a negotiation fails, the seller can sell to the other buyer alone. Then Buyer faces demand , and the seller earns the monopoly profit .
The two mechanisms are:
The Lean development uses this notation: pHat, xHat, piB (), piS (), piMb, piMs, IsNashBargain, IsSNEq, IsPMPrice.
With symmetric power , an SN equilibrium and a PM equilibrium price exist, and for every SN equilibrium and every PM price
The goal is stated about the equilibrium predicates, not about the closed-form prices, so that it asserts the comparison of the two mechanisms as the paper defines them.
Theorem 1 separates the effect of the negotiation mechanism from any asymmetry between buyers: under symmetric power the buyers are interchangeable, SN gives them the same price, and still the mechanism alone moves surplus from the buyers to the seller. The paper's explanation is that price matching lowers a buyer's incentive to negotiate the price down, so the matched wholesale price is higher (p. 10). The paper builds its asymmetric-power, side-payment and spot-market results (§§4–6) on this comparison.
The result is proved in the paper; nothing here is open. Neither the result nor its ingredients have been formalized. The mission produces a machine-checked account of a two-stage bargaining-over-competition model: the Bertrand stage, the Nash-bargaining stage with endogenous disagreement points, and the closed-form equilibria. Two steps the paper only asserts become formal obligations: uniqueness of the SN equilibrium, and the claim that the closed-form PM price is the global maximizer of the Nash product.
The comparison step is short once the closed forms are known: by milestones 6 and 7 the PM price is higher, the seller's diagonal profit increases, and the buyers' decreases. The work is in the equilibrium characterizations.
All quantities are real numbers. The standing assumptions are , and every bargaining power in . The sign is added; the paper never states it.
Real.rpow is the real power only on non-negative bases, and the individually rational set guarantees non-negative bases.Substituting the closed-form prices , into the profit comparison would turn Theorem 1 into the algebra of milestones 6–7. The goal is therefore stated for every equilibrium of each mechanism, together with existence of both equilibria, so neither the closed forms nor a vacuous equilibrium set can discharge it.
A complete development needs:
Contributions to any milestone, or to reusable lemmas on maximizing over an interval, are welcome.
Shared computing infrastructure — a data-centre cluster, a cloud platform's memory — is divided among users who arrive over time. Two requirements pull against each other. Proportional fairness asks that, when users are present, each holds at least a fraction of the resource. Limited disruption asks that the system not take resource away from running jobs at every arrival, because preemption and reallocation are costly; production cluster managers such as Google's Borg impose an explicit cap on the number of task disruptions an update may cause (Verma et al., 2015, as quoted in Vardi–Psomas–Friedman 2022, pp. 945–946). If reallocation were free, the resource could be re-split evenly at every arrival; if fairness did not matter, the first user could keep everything. The question is how much fairness survives a hard cap on disruptions.
Earlier work on dynamic fair division (Walsh 2011, online cake cutting; Kash, Procaccia and Shah 2014) did not allow reallocation at all. Friedman, Psomas and Vardi (EC 2017) introduced control vectors and gave non-optimal algorithms. Vardi, Psomas and Friedman (Mathematics of Operations Research, 2022) give an optimal algorithm for every control vector once the target ratio is known, and compute the optimal ratio exactly for uniform disruption budgets. This mission formalizes that exact computation.
One unit of a homogeneous, divisible resource is shared. Users arrive one at a time and never leave (the paper treats arrivals and departures separately; §§3–5, which this mission covers, are arrivals only). Users are labelled by arrival order, and is the share of the -th user when users are present.
A control vector of length fixes, for each arrival , a budget : when the -th user arrives, at most of the users already present may have their share strictly reduced (disrupted). Increasing a share is free. The -uniform control vector has for every , of any length, finite or infinite.
An allocation sequence for is feasible if at every time the shares are nonnegative, sum to at most , and respect the disruption budget. Its fairness ratio is
the smallest share relative to the proportional share , in the worst time step. The fairness ratio of the control vector, , is the supremum of this quantity over all feasible allocation sequences, and
The frugally fair algorithm takes a target ratio : when user arrives, it gives the newcomer and cuts the largest existing shares to . It may allocate more than one unit; denotes its total allocation at time .
For every integer ,
The goal states this in three parts: the infinite -uniform vector admits one feasible allocation sequence with ratio at least ; for every some finite -uniform vector admits no feasible allocation sequence with ratio ; and the infimum over all lengths of equals . For , .
The theorem gives a closed-form price of limited disruption: with reallocations per arrival, a system can guarantee every user of the resource forever, and no algorithm can guarantee more uniformly over all horizons. Since , a modest budget already recovers most of proportional fairness, which is the quantitative content a system designer needs to choose . Combined with Theorem 1, the value also turns FFA into a concrete optimal algorithm for the infinite -uniform vector, running online with no knowledge of the horizon.
The result is proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about control vectors, disruption-limited fair division or this constant is formalized there. The mission produces a machine-checked model of disruption-limited dynamic allocation, a formal optimality proof for a greedy online algorithm (Theorem 1) that is reusable for other control vectors (the paper's finite-vector algorithm and -gap bounds rest on the same theorem), and an explicit harmonic-sum asymptotic.
The impossibility half must rule out every algorithm, including ones that over-allocate early, raise shares opportunistically and choose whom to disrupt adaptively. The first idea, comparing total allocations time by time, fails: an arbitrary algorithm's allocation is not entrywise comparable with any fixed reference allocation, and a single well-chosen disruption can change which users are largest. The attainment half needs one allocation sequence for an unbounded horizon, so it cannot be obtained from finitely many feasibility checks; and the value is not the outcome of any finite computation but a limit of harmonic-number differences. The paper's own computation of the one-step change in total allocation contains a slip (a missing factor ; the sign is unaffected), so that step cannot be transcribed as printed.
Everything is real-valued and lives in DynFairDiv.Uniform. A control vector is ψ : ℕ → ℕ (index ) with a horizon n : ℕ∞, where ⊤ is the infinite vector; uniformCV d is the constant vector. Allocation sequences are X : ℕ → ℕ → ℝ with users labelled by arrival order, which is equivalent to the paper's sorted vectors because feasibility uses only sums, fairness only minima, and a disruption is a strict decrease of a given user's share; the newcomer is never counted as disrupted. Fairness at least is σ / t ≤ X t k for all and . is a real sSup, genuine for . FFA's state is a list of shares kept in nonincreasing order, so "the largest shares" is the front of the list. Departures (the paper's §6) are not modelled.
Added hypotheses, each disclosed in its item: throughout §5.1 (the paper's own assumption); for milestones 1, 2 and 6 (the paper's fairness ratios lie in ); in Lemma 1; a prefix of length at least in Proposition 2. Milestone 1 identifies the resulting sequence's shares with FFA's shares at each time.
A trivializing reading is ruled out: the impossibility half quantifies over every feasible allocation sequence, not only FFA-like or sorted ones, and the attainment half asks for a single sequence on the infinite horizon rather than one per finite length.
A complete development needs basic facts about FFA's list (length, order, scaling) and the harmonic asymptotics already in Mathlib (Real.tendsto_harmonic_sub_log). The FFA model and Theorem 1 apply to arbitrary control vectors and are reusable for the paper's finite-vector and -gap results; contributions of auxiliary lemmas about FFA (length, sortedness, scaling) are welcome.
An inventory system can replenish demand from several stages of a supply process. When an order is placed, the manager chooses where it enters; when work finishes at one stage, the manager may send it past intermediate stages to speed delivery. These choices change the future congestion of every stage. A stationary occupancy distribution is needed to calculate how often stock is available, how often demand waits, and how often expediting is used. Song, Xiao, Zhang, and Zipkin study such policies through a tandem network whose arrival and routing decisions depend on the current occupancies. They identify Policy-M as one family with a product-form stationary distribution, despite this state dependence (Song et al., SSRN 3702068, §§3–4).
The paper's Theorem 1 is the target here. Its formula permits the system's long-run inventory cost to be evaluated by summing over states with known product weights. The same paper develops a distinct Policy-E family, but its theorem has a different routing rule and is outside this mission (Song et al., Theorems 1–2).
There are service nodes in series, numbered . A state records the number of units at each node. The segment occupancy counts units between nodes and , inclusive. Demand arrives at positive rate . Node completes service at positive rate whenever . A completion at node leaves the supply system.
Policy parameters are thresholds for , with values in . For fixed origin , thresholds are nondecreasing as grows; for fixed destination , they are nonincreasing as grows. Every terminal threshold equals . An arriving demand places a new unit at node when no prefix reaches ; otherwise it places the unit at one node beyond the largest such . A service completion at node follows the analogous Policy-M rule using downstream segments and thresholds . An empty set of reached thresholds sends the unit to (Song et al., (5), (7), §4).
Assumption A imposes two inequalities on these thresholds: a triangle inequality for , and supermodularity for . The indices may include the demand source . The admissible state set consists of all occupancies whose segments obey for every (Song et al., Assumption A and (11)).
The first part of Theorem 1 identifies the states reachable from the empty system through positive-rate Policy-M transitions:
For and finite whenever , define and . The second part gives a normalized product law:
The mission also requires to have total mass one and to satisfy global balance for the rates generated by the stated routing rules. Its milestones are the closure claims (A-2) and (A-5), equality of the Appendix proof sets in (A-30), the indicator identity (A-25), and the local balance equations (A-12)–(A-15) (Song et al., Theorem 1 and Appendix A).
The formula describes the joint occupancy of all service nodes from rates and the policy thresholds. Once its normalizer is known, probabilities of stock levels and congestion events can be summed over , supplying the inputs to the paper's long-run cost calculation (9). The state-space result determines which occupancies contribute to those sums (Song et al., (9), Theorem 1).
Theorem 1 is proved in the paper. This mission asks for machine-checked proofs of its formal statements, not a new queueing result. A complete development would provide reusable finite-segment reasoning, routing-set identities, and countable-state balance calculations. The declarations staged here are open Lean statements, so they do not yet constitute machine-checked proofs.
With fixed routing, a proposed product weight can be compared across neighboring states using only the node rates. Here the route of a newly arriving or completed unit changes with several segment occupancies. An incoming transition to a state may have skipped nodes, and the condition that selected its destination must hold in the predecessor state. Checking only the product ratio therefore leaves out the routing indicators. The source's local equations (A-12)–(A-15) and its proof-set identity (A-25) make those indicators explicit. The paper also gives an example showing that state-dependent routing does not yield product form for every policy (Song et al., Example 1 and Appendix A).
Lean represents as a function from Fin K to natural numbers, while the functions occ and seg retain the paper's one-based node numbers. The threshold array takes values in extended natural numbers so is representable; a strict comparison with a threshold expresses the paper's “at most ” condition. Both routing rules specify the destination when no threshold is reached. A service transition is enabled only when its origin node is occupied. The theorem states , which is implicit in the paper's numbered-node model, along with positive arrival and service rates.
The source defines as the limiting law of a continuous-time Markov chain and invokes known ergodicity. This Lean development encodes its stationary claim by a summable, normalized product weight and the global balance equations for explicit Policy-M rates. It does not formalize the CTMC limit or uniqueness of that limit. The normalizer is a countable sum; the goal asserts summability and , so a default value for a divergent sum or division by zero cannot certify the claim. The state space is constructed from and proved reachable rather than supplied as a hypothesis. Empty-node departures are guarded to avoid natural-number subtraction at zero. The special case remains in the goal; the milestone combining four separate local equations assumes because its node-1 and node- formulas must refer to distinct nodes.
The staged definition supplies segments, thresholds, routing, transition rates, product weights, and the source's Appendix sets. Contributions may prove the listed milestones, build general lemmas about segment sums and reachability, or establish summability and the passage from local to global balance. These supporting tools can be reused for other countable-state queueing models.
Cloud platforms divide a shared physical resource, such as a pool of processors, among many users at once. Each user is promised a service level agreement (SLA): a fraction of the resource that it should effectively receive whenever it has work to do. The operator wants two things that pull against each other: to keep the resource busy (total work done should be large) and to honour every SLA. The difficulty is informational. The operator does not see future demand, and in the setting of Perez-Salazar, Menache, Singh and Toriello (arXiv:1809.02688) it does not even see current demand: at each step it only learns which users have a non-empty queue.
The paper answers with a multiplicative weight rule. Multiplicative weight methods go back to online learning (Freund and Schapire, 1997; survey: Arora, Hazan and Kale, 2012) and can be read as entropic mirror descent (Beck and Teboulle, 2003). Their classical guarantees compare an online learner with the best fixed decision in hindsight. This paper compares the algorithm with the best time-varying offline allocation instead, and proves the comparison directly, without the standard regret analysis.
There are users and discrete time steps . Each user has an SLA , with . Loads arrive online. User keeps a queue of unfinished work. At each step:
The total work of an allocation sequence up to time is .
Algorithm 1 has parameters and , and sets . It keeps in the truncated simplex , starting anywhere in . At step it assigns the gain to active users below their SLA (: ), to the other active users () and to inactive users. It then sets and takes , the KL projection: the minimizer over of .
Let for all and let be any run of Algorithm 1. For every offline allocation sequence and every time ,
and for every user , every comparator with and every ,
The result. Theorem 1 is a bicriteria guarantee against a dynamic benchmark. The work benchmark may change its allocation arbitrarily over time with full knowledge of all loads, and the algorithm, which sees only which queues are non-empty, loses only an additive amount that does not grow with time, at the price of a fraction of capacity. At the same time every user receives, up to a fixed delay, at least the work of a dedicated fraction of its SLA. The paper also shows (arXiv:1809.02688, Theorem 2) that against the unscaled offline optimum every deterministic online algorithm loses work on some load sequence, so some form of slack is unavoidable.
Formalizing it. The result is proved on paper; no machine-checked proof exists. A formalization would check the constant bookkeeping, where the printed text has slips (an versus in Theorem 1, a real block length used as an integer, an off-by-one in Claim 3.1). It would also produce a reusable deterministic queueing model and a verified closed form of the KL projection onto a truncated simplex.
The obvious first idea, the regret analysis of mirror descent, does not apply. Regret bounds compare with a fixed decision, but here the benchmark changes over time. The algorithm's gains also depend on its own past decisions through the queues, so they are not an exogenous sequence of losses. The paper notes (p. 10) that its guarantees do not follow from the standard analysis of mirror descent. A second obstacle is the feedback: a busy user is not the same as a user that uses its whole allocation. A user whose queue empties during a step completes less than its allocation, so utilization and work done can differ. Finally, the constants matter, because the goal states them explicitly. The printed derivation mixes and , uses the real number as a block length, and is off by one step when it identifies the work done with the arrived load.
A fork-join queue splits every incoming job into tasks, sends one task to each of parallel servers, and declares the job complete only when all tasks are done. The model describes assembly systems in which a manufacturer orders parts from suppliers and can only start production when every part has arrived, as well as parallel computing and storage systems in which a request is answered only after all sub-requests return. Because a job waits for its slowest task, the performance of the system is governed by the maximum queue length over the servers, and the question of interest is how this maximum behaves when is large and the system is heavily loaded.
Schol, Vlasiou and Zwart (arXiv:1912.11661, Mathematics of Operations Research 47(2), 2022) study this question in a nearly deterministic regime: arrivals and services happen in almost every time slot, and the traffic intensity of each server tends to at rate . Even in the empty-start case the queue lengths of different servers are dependent, because every server sees the same arrival process; the maximum of dependent random walks has to be analysed directly.
Timeline. Early work treats two service stations and obtains exact asymptotics (Flatto and Hahn, 1984; Baccelli, 1985; Wright, 1992). For more stations the literature turned to approximations and bounds: Nelson and Tantawi (1988) and Baccelli and Makowski (1989) bound the mean response time, and Ko and Serfozo (2004) approximate the response-time distribution in M/M/s fork-join queues. Heavy-traffic process limits for a fixed number of stations were obtained by Varma (1990) and Nguyen (1993, 1994), with reflected Brownian motion limits, and by Lu and Pang (2015–2017) for many-server stations. Sigman and Whitt (2011) analysed nearly deterministic G/G/1 and G/D/N queues. The paper of this mission gives a process-level (fluid) limit for the largest queue when the number of servers itself grows, in the nearly deterministic regime and with a non-zero initial condition.
Fix . For each the system runs in discrete time slots . In slot a task arrives at all servers with probability (indicator ), and server completes a task with probability (indicator ), all indicators being independent. The arrival process is and the service process of server is .
Server starts with tasks, where are i.i.d. random variables, the initial queue lengths are non-negative, and is a scaling sequence. By Lindley's recursion the maximum queue length at time is
The first term alone is the maximum queue length of the system started empty. The initial condition is assumed to satisfy in probability (Assumption 2.3), and either has a finite right endpoint (Assumption 2.4) or is continuous with as for all (Assumption 2.5, the Gumbel-domain case).
The fluid limit is
with under Assumption 2.4 and under Assumption 2.5. In Lean these are fluid, fluidEmpty, gFinite and gGumbel; the queue is maxQueue and the empty-start queue maxQueueEmpty.
For every and ,
under Assumptions 2.1–2.3 and either Assumption 2.4 or Assumption 2.5 (one conjunct per case).
The result. Theorem 2.1 identifies the scaling under which the maximum queue length of a large, heavily loaded fork-join system follows a deterministic curve: time of order and space of order . The limit separates the contribution of the empty-start dynamics, which saturate at the steady-state level after time , from the contribution of the initial backlog, which is governed by the extreme-value class of the initial condition. For instance, with and the system "starts and stays in steady state" on an initial interval (p. 12). The theorem gives the transient behaviour needed to judge how long a backlog at the slowest supplier persists.
Formalizing it. The result is proved in the paper; no part of it has a machine-checked proof. The mission produces a formal statement of the model and of the fluid limit, and the intermediate results of Section 4. The proof combines a non-uniform Berry–Esseen inequality, extreme-value theory for maxima of sums, Doob's maximal inequality and a tightness criterion; formalizing it would give reusable Lean versions of several of these tools.
The obvious argument treats the queues as independent reflected random walks and applies extreme-value theory to their maximum. It fails because all servers share the arrival process, so the queues are dependent. The paper handles this by splitting each queue into a common arrival term and an individual service term, but the individual terms are maxima of centred random walks evaluated at a time of order , and their Gaussian approximation must be accurate at the scale of the maximum: a uniform Berry–Esseen bound is too weak, and a non-uniform bound with the right rate in is needed (Lemma 4.2). Upgrading pointwise convergence to uniform convergence on requires a modulus-of-continuity estimate for a maximum of processes (Lemmas 4.11–4.12), where the number of processes grows with . The initial-condition term requires an extreme-value result for maxima of sums of two independent coordinates with different tails (Lemma B.1).
All objects are defined in one module, LargeForkJoin.FluidLimit.Model. Times are natural numbers, and is evaluated at , which is the paper's own convention . Servers are indexed . All variables live on one probability space; the Bernoulli laws are imposed for (for small , can be negative), and within each the arrival indicators, service indicators and initial-condition variables used by that system are mutually independent. The independence of from arrivals and services is an added assumption: the paper uses it in its proofs but does not state it. Initial queue lengths are non-negative almost surely. Assumption 2.5 adds for all , without which its ratio is undefined; "continuous" means "no atoms". Convergence in probability to a constant is written with -events, and as "some has ", the same event. Lemmas 4.4 and 4.9 speak of Gaussian variables outside the model; they are stated for the law of independent pairs (standard normal, law of ).
The goal is stated about the maximum queue length built from the Bernoulli indicators through (2.3), uniformly on . A statement about a Gaussian or reflected-Brownian surrogate (the heuristics of Sections 2.2–2.3), or a pointwise statement (Theorem 4.1), would not be Theorem 2.1.
Not included: Propositions 2.1–2.3 (other scalings and the steady state), the variant of Theorem 2.1 under Assumption 2.6, Theorem 4.2 (finite-dimensional distributions, a generic fact), and Lemma 4.7, whose statement includes the stationary case and needs a stationary-queue object. Contributions of general tools are welcome: a non-uniform Berry–Esseen inequality for Bernoulli sums, extreme-value results for maxima of i.i.d. sequences (relative stability, Gumbel-domain tails), and the tightness criterion of Billingsley's Theorem 7.3.
A central question of financial economics is how much of the information dispersed among traders ends up in market prices. The workhorse model is the noisy rational expectations equilibrium (REE): investors with private signals trade a risky asset, the price aggregates their information, and each investor learns from the price as well as from her own signal (Grossman and Stiglitz 1980; Hellwig 1980). In that tradition the price is a free public signal: every investor reads off from it exactly what it contains.
Vives and Yang (SSRN 2763813; published with Mondria as Mondria, Vives and Yang 2021) drop that assumption. Extracting information from a price takes effort, so each investor observes the price signal only through her own interpretation error, and can buy sophistication to reduce that error. The interpretation errors share a common component, and the paper's first result is that this common error re-enters the price. Even with no exogenous noise traders, costly interpretation makes the price noisy. This mission formalizes that first result: the existence, uniqueness and closed form of the linear financial-market equilibrium (Proposition 1, with the remark that follows it).
A risky asset pays , with independent (learnable) and (unlearnable). A continuum of investors have CARA utility with risk aversion . Investor observes:
All shocks are independent and centred, and all precisions and are positive. A linear price function is ; when it is equivalent to the signal with . Each investor demands , computed by Bayes' rule from the jointly Gaussian signals. A linear equilibrium is a pair , , such that aggregate demand is zero for every realization of .
The paper's closed forms use the precision of the combined price information,
and the cubic
There is exactly one linear equilibrium . In it
with evaluated at ; lies in , , and is the unique positive root of ; and .
Proposition 1 is the foundation of the rest of the paper. Every comparative static on price informativeness, volatility, return predictability, disagreement and trading volume (Propositions 2–3), and the analysis of the sophistication-acquisition game (Propositions 4–6), is computed from the closed forms of , and the root . The remark is the paper's mechanism: the common interpretation error is a source of price noise generated by the traders themselves, which vanishes only in the limit of full sophistication (Corollary 1).
The result is proved in the paper; nothing here is open. To our knowledge no part of it, nor any noisy-REE equilibrium with Bayesian price learning, has been machine-checked. The mission produces a formal account of the equilibrium construction of the noisy REE literature, from Gaussian conditioning to market clearing to a polynomial fixed point. The same pattern (conjecture a linear price, condition, match coefficients, solve for the fixed point) recurs throughout that literature.
Each step is elementary, but each is a large symbolic computation. Inverting the covariance matrix and simplifying to the printed fractions involves rational functions in seven variables. The discriminant of is a polynomial of degree ten with 25 terms, and its sign has to be established for all positive parameters.
The conceptual pitfall is uniqueness. Showing that has one positive root is not enough: a linear equilibrium may a priori have , so uniqueness among all linear equilibria needs to have one real root, which is what the discriminant gives. The fixed-point condition also needs at every candidate, which has to be proved rather than assumed.
All quantities are real. A parameter structure carries ; the standing assumption is that all seven are positive, and nothing else is assumed. The model is encoded in reduced form:
The equilibrium predicate is defined from Bayesian demands and market clearing only. Defining it by the closed forms of , , or as " is a root of (18)", would make Proposition 1 a statement about a cubic and is ruled out. Likewise the Bayes coefficients are , never the printed fractions.
A complete development needs matrix inversion over (Mathlib's Matrix.inv), rational-function simplification, Mathlib's Cubic and its discriminant, and the intermediate value theorem. A reusable lemma "a real cubic with negative discriminant has exactly one real root" would serve beyond this mission. Proofs of any milestone, and alternative proofs of uniqueness, are welcome.
A central planner holds a single pool of units of a product and must supply customers whose demands are random. Each customer asks to be fully served, i.e. to receive her entire demand, with probability at least a target . This Type-I service level (the persistency value of the stochastic knapsack) is the standard requirement in supply-chain allocation and in humanitarian logistics. The planner's question is how much capacity the targets require.
The answer depends on when the planner learns the demands. Lyu, Chou, Teo, Zheng and Zhong (SSRN 3674463, 2021) compare three information regimes:
Anticipative rules are the ones used in practice, because they are simple to announce and to audit. The paper's main result quantifies what they cost in capacity compared with adaptive rules.
Timeline. Alptekinoğlu et al. (2013) introduced capacity pooling with differentiated service probabilities under anticipative priority rules. Dean, Goemans and Vondrák (2008) bounded the adaptivity gap of the stochastic knapsack for revenue maximization by a constant factor. Zhong, Zheng, Chou and Teo (Management Science 64(4), 2018) treated the Type-II (fill-rate) version, in which partial service counts in proportion. They showed that its achievable region is a polymatroid and that anticipative policies are optimal there. Lyu et al. (2021) use this Type-II system to compare the Type-I classes.
Customers are . The demands are random variables on a probability space . An allocation run with capacity serves customers one at a time. A chosen customer is fully served if her demand does not exceed the remaining capacity, and her demand is then deducted. Otherwise she is not fully served, and the run stops.
The optimal Type-I capacities are
and is defined in the same way with anticipative policies. These are the optimal values of problem (CPP-A) of the paper.
On the Type-II side, is the set of with for every . is the least with . For a priority order , the greedy fill solves the fractional knapsack (CPP-F).
Standing assumptions (§3.3): the demands are independent and positive, and almost surely for a constant . The targets satisfy .
The bound is uniform in and in the joint law of the demands, subject only to the standing assumptions.
The result. Theorem 5 says that the information an adaptive planner gains costs at most two maximal demands of capacity, independently of the number of customers. Anticipative priority rules are therefore near-optimal for Type-I service whenever individual demands are small relative to the pool. This contrasts with the responsive regime: Example 1 of the paper shows that can exceed by an unbounded factor. In Theorems 3–4 the Type-II capacity serves as a common yardstick, so each policy class is compared with an explicitly computable polymatroid quantity.
Formalizing it. The theorem is proved on paper. To our knowledge none of it is machine-checked. A formal development has to make precise what the paper leaves informal: what a randomized adaptive policy is, why the event "customer is reached" is independent of , and why the infima defining the optimal capacities are over non-empty sets. The milestones on the greedy fill and the polymatroid can be reused for other fill-rate and persistency problems.
The obvious comparison fails because the two classes face different constraints. A Type-I requirement is an all-or-nothing event, so a deterministic priority order cannot hedge. With three identical unit-demand customers and targets , any fixed order needs , while . Randomization over orders is therefore essential on the anticipative side, and the link between a Type-I requirement and the Type-II region is not a statement about any single order. On the adaptive side, the decisions depend on revealed demands. Whether customer is fully served is correlated with , so a Type-I service probability does not translate directly into a bound on the expected demand served, which is what constrains. Conditioning arguments that ignore this correlation give false inequalities.
d : Fin N → Ω → ℝ on a probability space. Probabilities are μ.real, expectations are Bochner integrals. The standing assumptions are bundled in Standing μ d Δ α: measurable, iIndepFun, almost surely positive, almost surely ≤ Δ, 0 < Δ, and α i ∈ [0, 1].The infrastructure the proofs need: measurability of runs, independence of functions of disjoint coordinates, continuity of (so that is attained), and the greedy description of a polymatroid's base polytope. Proofs of any milestone are welcome. So are alternative proofs of milestone 1 that avoid the general polymatroid theorem.
A firm can return cash to shareholders by paying dividends, but a payment reduces the reserves available to survive future losses. If cash can be distributed only at scheduled dates while equity can be raised between those dates, the firm must coordinate a discrete dividend decision with a continuous-time financing decision. Keppo, Reppen and Soner study this combination for a firm whose cash flow is a Brownian motion with drift. Their preprint identifies the firm's optimal value through an operator that first solves the financing problem between dividend dates and then chooses the next dividend. The mission concerns that characterization, Theorem 3.4, together with the regularity results on which it depends.
Let be the initial reserve and let , where is a one-dimensional Brownian motion, is profitability, and is volatility. Dividends of amounts may be paid at dates , with . Equity issues have sizes and occur at stopping times ; the issue times are locally finite. A positive issue costs
while no issue costs zero. The cash reserve after actions at time is . The ruin time is the first strictly positive time that . A dividend cannot exceed the reserve immediately before its date, and no action is taken after ruin. These conditions define the admissible controls .
The firm's value function is the supremum, over admissible controls, of expected discounted dividends less expected discounted issue costs:
The first sum includes a possible dividend at time zero, following the displayed objective in §3.1 of the preprint. An issue at time belongs to the next period. Thus the one-period financing operator charges issues on and evaluates its continuation reward at the reserve immediately before . The dividend operator is
The continuation class consists of the continuous, nondecreasing functions that satisfy the issuance boundary condition of Definition 3.2, are bounded above by , and have nondecreasing and bounded in absolute value by . Its larger class omits the last condition. The intervention value in the boundary condition is .
The first target is the mapping statement in Theorem 3.3: for . With
the next targets are the one-period bound for , the classical one-period characterization of Theorem 3.6, and the remaining mapping and contraction assertions of Theorem 3.3. In particular, contracts the uniform distance between functions in by the factor .
The goal is Theorem 3.4:
This identifies the fixed point with the value defined from admissible controls. It also asserts that the value is finite at every nonnegative initial reserve.
Theorem 3.4 turns an infinite-horizon control problem into repeated one-period calculations. Since Theorem 3.3 makes a strict contraction on , iterating it determines the value in that class. The source connects this characterization to a numerical method when the one-period financing problem can be computed efficiently. A proof in Lean would also provide reusable statements about locally finite impulse controls, periodic actions, ruin, and discounted extended-real objectives. The preprint proves the mathematical results; this mission records their statements as open Lean theorems for machine-checked proofs.
The dividend operator is an elementary supremum over one payment, but the financing operator ranges over adapted impulses before ruin. Its regularity is central: the paper invokes Theorem 3.6 to show that is continuous and satisfies the issuance boundary condition. That theorem characterizes the arbitrary-maturity issuance value as the unique classical solution of a parabolic equation with a nonlocal boundary condition. The fixed-point conclusion alone would leave an additional gap: Theorem 3.4 must identify that fixed point with the original control supremum, including the limit over dividend periods and its terminal reward.
Lean represents nonnegative reserves by and the discount, costs and function values by real numbers. Control values and one-period rewards are suprema in extended real numbers, with dividends and issue costs integrated separately as nonnegative quantities. The bound proves the finiteness needed before converting to real values. An expression with both expected dividends and expected costs infinite takes the extended-real value and cannot improve a supremum with a finite admissible alternative.
The paper's cumulative processes are represented by nonnegative dividend amounts and a locally finite impulse sequence of nonnegative issues. This makes explicit that equity cannot be supplied by an uncharged continuous component. Simultaneous impulses are allowed; merging them cannot increase the cost. The Brownian cash flow uses the published AtaBarjesteh23.Workload.IsDriftBM definition. The model requires a probability measure, adaptation to a filtration, and positive . The filtration is right-continuous and its initial σ-algebra contains all subsets of ambient null measurable sets, as required by the usual conditions. A dividend at time zero follows the objective's sum. In , the continuation value uses , resolving the free-issue-at- ambiguity in the printed formula. The arbitrary-maturity problem retains its separately printed non-strict survival indicator.
The value is defined solely from admissible controls, never from or its iterates. Theorem 3.6 uses time to maturity and states smoothness only on the interior rectangle; uniqueness is restricted to the closed nonnegative time-state rectangle. Reusable work includes stopping-time measurability, impulse summation and parabolic regularity. Contributions proving the goal or the four listed milestones are within scope; §4's random-profitability model and §3.4's numerical experiments are outside this mission.
Many operational decisions are optimization problems whose cost vector is unknown when the decision is made but can be predicted from observed features: shortest paths under predicted travel times, portfolios under predicted returns, production plans under predicted prices. The common practice, predict-then-optimize, first fits a regression model mapping features to a cost estimate and then solves the optimization problem with in place of the true cost . What the decision maker cares about is not the prediction error but the optimality gap of the resulting decision under the true cost. Elmachtoub and Grigas (arXiv:1710.08005, Management Science 2022) introduced the SPO+ surrogate to train predictors against that gap directly, and established its Fisher consistency.
Ho-Nguyen and Kılınç-Karzan (arXiv:2012.15046, Management Science 2022) ask which surrogate losses give quantitative guarantees: when does a small excess surrogate risk force a small excess optimality-gap risk, uniformly over a class of data distributions? Their answer adapts the calibration theory of Steinwart (Constructive Approximation 26, 2007) to the end-to-end setting, and its most striking consequence concerns the ordinary squared loss.
Let be a non-empty convex compact set and a convex function, continuous on . For a cost vector the decision maker solves
An argmin selection is a fixed map with a minimizer of over for every . Using a prediction instead of the true cost incurs the true loss
Features and costs form a random pair with joint law . For a loss and a measurable predictor , the risk is and the Bayes risk is over measurable ; for these are written and . The squared loss is .
Given a set , the class consists of the laws for which every conditional law is concentrated on , is square integrable, and has mean . Assumption 2 asks that be bounded. The constants are , and .
A loss is -uniformly calibrated if for every there is such that, for every law in , every and every , a conditional excess -risk below forces a conditional excess true risk below . The largest such is the calibration function .
For every law with and every measurable predictor ,
The goal is stated with the constant and no other problem data: it is independent of , of beyond boundedness, and of the law of the data.
The corollary says that a predictor trained by ordinary least squares, without any information about or , has excess optimality-gap risk at most . Since the excess squared-loss risk separates over coordinates, coordinate-wise regression bounds suffice for end-to-end guarantees (Remark 7). Any learning-theoretic rate for least-squares regression therefore transfers to a rate for the decision problem, up to a square root. Theorem 3 gives the same transfer for any uniformly calibrated surrogate, and is the template for the paper's further results on separable symmetric losses.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires a measure-theoretic treatment of conditional risks through kernels, a Lean version of Steinwart's convexified calibration inequality in this setting, and the geometric bound of Lemma 5. Each milestone is a self-contained target.
The true loss is neither convex nor continuous in (Lemma 1): the decision jumps between faces of . A pointwise comparison between and fails, since a prediction close to can still select a far-away vertex when lies near a tie. The comparison only holds after conditioning on and averaging over , and it must hold uniformly over all conditional laws in , not for a fixed distribution. The step from conditional comparisons to the integrated risks is where the uniform bound on the conditional excess true risk and the convention at in matter; Bayes risks are infima over predictors, so this step also needs the conditional minimizers to assemble into a measurable predictor.
Vectors live in EuclideanSpace ℝ (Fin m). The standing setting (Standing X f) bundles convexity, compactness and non-emptiness of , convexity of on and continuity of on ; IsArgminSelection X f xstar is the selection property. A joint law is μ ⊗ₘ κ, with μ the law of and κ a Markov kernel giving ; is the Bochner integral against κ w. Risks are -valued lower integrals of ENNReal.ofReal of the non-negative losses, Bayes risks are infima over measurable predictors, and excess risks are truncated differences. The class is lsClass C, a set of conditional laws concentrated on \mathbb P \in \mathcal Pw \in WWB_X$ is Metric.diam X.
Added or pinned conventions:
xstar (the paper uses Lebesgue measurability, Lemma EC.4) and of predictors;The Bayes risks are genuine infima over measurable predictors and the conditional excess risks are defined generically. Neither is defined by the closed form that Lemma 2 or Lemma 6 establishes, so neither lemma holds by definition.
Needed infrastructure: lower integrals against μ ⊗ₘ κ and their disintegration, measurability of the conditional mean and of the optimal value , Jensen's inequality for real convex functions on a bounded interval, and the distance from a point to a half-space. The bias–variance decomposition for laws on and the half-space distance formula are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal that bypass Theorem 3.
Sensitivity analysis asks how the solution of an optimization problem changes when its data move. For linear optimization the answer has been known since the 1990s: as the objective is perturbed along a fixed direction, the optimal partition (which variables can be positive at an optimum and which slacks can) stays constant on open intervals and changes only at finitely many breakpoints, and the optimal value is piecewise linear with breakpoints exactly there (Adler and Monteiro, Algorithmica 8, 1992; Jansen, Roos and Terlaky, 1993). Semidefinite optimization (SDO) is used throughout control, combinatorial relaxations and polynomial optimization, and its parametric behaviour is less regular. The optimal partition can stay constant while the optimal sets move (a nonlinearity interval), and the optimal value need not be piecewise linear.
Mohammad-Nezhad and Terlaky (Optimization 69, 2020) defined invariancy intervals, nonlinearity intervals and transition points for parametric SDO. Hauenstein, Mohammad-Nezhad, Tang and Terlaky (arXiv:1908.10499v3; Mathematics of Operations Research, 2022) prove that there are only finitely many transition points (Theorem 1, p. 8) and then compute nonlinearity intervals with numerical algebraic geometry. Finiteness is what makes a computational description possible: without it, the interior of the domain need not decompose into finitely many intervals of each kind.
Timeline:
Let be the real symmetric matrices with . Data: and . For a real parameter consider
The primal feasible set does not depend on ; the dual one is . The optimal value function is the infimum of , its domain is , and the optimal sets are and .
Standing assumptions (p. 2): Assumption 1, the are linearly independent; Assumption 2, there are , with .
For , a maximally complementary optimal solution has and (Definition 1). A point is a transition point if every interval contains an with or (Definition 5).
The statement names no bound on the number of transition points; it asserts finiteness only.
The result. Theorem 1 implies that is a finite union of invariancy intervals, nonlinearity intervals and transition points (p. 8). This is the structural fact behind the paper's algorithm, which follows the optimal solution along a nonlinearity interval and detects its end points, and it extends to SDO the finite-breakpoint picture of parametric linear optimization. Without finiteness, a sensitivity report would have no finite description.
Formalizing it. The theorem is proved in the paper; nothing here is open. It has no machine-checked proof that we know of. A complete development would bring parametric conic duality into Lean (the interior point condition moving along a direction, strong duality with attainment, compactness of optimal sets), and it would connect convex analysis to semi-algebraic geometry: relative interiors, ranks of positive semidefinite matrices, and the one-dimensional case of Tarski–Seidenberg. Each of these is useful beyond this paper.
The obvious argument says that ranks are integers between and , so they can change only finitely often. That is false for arbitrary integer-valued functions on an interval: a rank pair could alternate on a sequence accumulating at a point, producing infinitely many transition points. Finiteness needs a structural reason why each level set is a finite union of points and intervals. That reason is semi-algebraicity. Proving it requires showing that the relative interior of the optimal set, and the parameter values where a rank is attained there, can be described by a first-order formula over the reals, and then eliminating the quantifiers. Mathlib has no Tarski–Seidenberg theorem, and the one-variable structure theorem for semi-algebraic sets (milestone 9) is itself missing.
A second difficulty is the parametric duality: strict feasibility is assumed only at , and propagating it to all of (Remark 1) uses a theorem of the alternative for SDO.
Matrices are Matrix (Fin n) (Fin n) ℝ; is PosSemidef (which includes symmetry) and is PosDef. Symmetry of , , is a hypothesis of every theorem, as are Assumptions 1–2. The optimal value is an EReal infimum over , so is represented faithfully and is not a junk set. compares with the primal value , as printed. The relative interior is Mathlib's intrinsicInterior. Definition 1 lets be any maximally complementary solution. The formalization removes this choice by taking the supremum of ranks over relative-interior points, and milestone 5 shows that every such point has that rank. uses the relative interior of the product, as printed. A subset of is semi-algebraic when its copy in is a finite union of sets with real polynomials.
Trivializing formalizations are excluded:
sInf (which would make an unbounded problem look finite with value );The paper also states that is closed. Under Assumptions 1–2 this is false: , , , , , gives . Milestone 2 omits closedness. The paper's proof of Theorem 1 does not use it.
Contributions welcome: proofs of any milestone; a semi-algebraic toolkit in Lean (closure under Boolean operations, projections from to , the one-dimensional structure theorem); conic duality for standard-form SDO.
Make-to-order manufacturers may use two substitutable raw materials to satisfy demand when production capacity and material deliveries are uncertain. A cheaper material may yield less finished product per unit, and the firm must decide how much of each material to preserve for later periods. A production rule based only on current unit costs can be wrong because using one material changes the inventory state from which future orders and production will be chosen. Chen, Duenyas, and Jasin study this coupled replenishment and production problem and characterize the form of an optimal production decision. Their result gives a state-dependent rule described by four curves, rather than requiring a separate optimization for every inventory state. This mission formalizes that production result from the 2016 working-paper version of their study.
There are periods and two substitutable materials. A unit of finished product requires units of type- material, with . Before production in period , the available material is a vector . Demand and production capacity are nonnegative random quantities with finite support. A unit of satisfied demand earns revenue ; a unit of lost demand incurs penalty . Holding costs are and material purchasing costs are . Ordered amounts are limited by random availabilities , whose finite supports may include .
The production decision is the remaining inventory after material use. The feasible set contains vectors satisfying , the demand limit, and the capacity limit:
The objective adds the current cost coefficients , where , to the next-period value . The value functions are determined backward from by the production and replenishment equations (1)–(5). Thus is an object computed from the model data and the dynamic program. These definitions follow §3 of the working paper.
The goal is Theorem 1, pp. 15–16. There are two nonincreasing switching curves and two balancing curves meeting at . Together they define the use-down-to and balancing (UB) rule of Definition 1. For every nonnegative and every , the prescribed decision is feasible and optimal:
The goal also includes the theorem's four minimization characterizations: minimizes on the whole nonnegative orthant; each minimizes a one-coordinate section; minimizes on ; and minimizes on , for every . The milestones retain Lemma 3(a), Lemma 3(d), the backward-induction claim for , Proposition 1 for the strictly convex perturbation, and Proposition 2 for the limiting policy.
The theorem identifies which material-use rule solves the production stage for any observed demand, capacity, and inventory. Its curves are independent of that period's realized and ; those realizations enter the region boundaries and the rule's arguments. This structure supports the paper's later ordering-policy and computational work without replacing the original dynamic program with an unrelated one. The same formal definitions of feasible production, finite-support expectations, and coordinatewise value-function structure can be reused in other two-resource inventory models.
The working paper proves the result mathematically; the requested machine-checked work is to prove the Lean statements. The present proposal supplies definitions and theorem targets with sorry proof bodies. It does not claim that Theorem 1 or its milestones already have Lean proofs. A completed development would connect the backward dynamic program to the curve characterization and then prove that the region-specific action is optimal.
The replenishment-stage objective is generally neither convex nor supermodular even when the subsequent value function has those properties, as the paper notes after Lemma 3. Consequently, taking a minimum in the replenishment recursion does not preserve the desired shape by an immediate standard argument. At the production stage, demand and capacity impose different coupled linear constraints on the two materials. Minimizing each material coordinate separately therefore does not produce a feasible or optimal decision in general. The source's region boundaries must account for which of these constraints binds and for their changes at and .
Lean uses with componentwise order for two-material vectors. Each random quantity is a finite support with nonnegative real weights summing to one; expectations are finite sums. The two availability laws are multiplied as independent laws at each period, and availability is represented by WithTop ℝ. The joint law of need not factor. The dynamic program has periods , and the terminal value is set at . Its minima are defined as infima of feasible objective images; attainment is content of the results, not part of the definitions. Lower-growth claims use eventual real inequalities for every positive error, with the other inventory coordinate fixed and nonnegative.
The paper describes revenues and costs as monetary amounts and uses sign conditions in its proof of Lemma 3. The Lean standing predicate makes explicit , , , and , in addition to the paper's and . These assumptions are disclosed because without them the stated coercivity and attainment claims may fail. The objective in the goal is precisely produced by the full backward recursion; allowing an arbitrary objective with assumed structural properties would omit the dynamic-programming content.
Definition 1 calls its six regions a partition. At , two printed regions can overlap; a concrete Lean check is included locally. The formal policy follows the page's displayed order when more than one region matches. Region coverage is asserted for all nonnegative , and pairwise disjointness is asserted only when . The first-match convention and corrected partition claim are documented with the counterexample for review. The piecewise formulas for , , and retain their source inequalities. Contributions establishing feasibility, curve existence, uniqueness for the perturbed problem, and the induction step are all useful to the mission.
Consensus halving asks for a division of a resource into two parts that every one of agents values equally, so that a group with heterogeneous preferences can agree that the two parts are of the same worth. The classical setting is a divisible interval (a cake or a necklace), where Simmons and Su (2003), building on Hobby and Rice (1965), showed that cuts always suffice. The question has a direct application to fair division: once a consensus halving is found, two parties can each take a part without either side of a group of stakeholders preferring the other part. Since Filos-Ratsikas and Goldberg (2018) proved that approximate consensus halving on an interval is PPA-complete, the problem has also become a central example in the complexity theory of total search problems.
Goldberg, Hollender, Igarashi, Manurangsi and Suksompong (arXiv:2007.06754, Mathematics of Operations Research, 2022) study the same question for a set of items with no spatial order: houses, children's custody days, or a portfolio of assets, where an item may be shared fractionally but each shared item is a cost. Their first result, for additive utilities, is the subject of this mission.
There is a set of agents and a set of items. Agent values item at , and §2 of the paper assumes .
Equivalently (display (1) of the paper), for all .
In the Lean development these are util, IsFractional, IsConsensusHalving, IsCut and numCuts in the namespace ConsHalving.Additive.
For agents with nonnegative additive utilities over items there is a consensus halving with at most cut items:
The paper states:
Theorem 2.2. For n agents with additive utilities, there exists a polynomial-time algorithm that computes a consensus halving with at most min{n, m} cuts.
The mission formalizes the existence of the algorithm's output. The polynomial-time clause is not formalized: the paper fixes no machine model, and its complexity argument is a reference to Gaussian elimination.
The milestones follow the steps of the paper's proof (p. 5), which runs an iterative procedure starting from :
The result. Splitting every item in half is always a consensus halving, but it cuts all items. Theorem 2.2 shows that, however many items there are, sharing at most as many items as there are agents is enough. This matches the -cut bound of Hobby–Rice and Simmons–Su for the interval, and the paper shows it is tight: Theorem 2.5 proves that when the utilities are drawn independently from non-atomic distributions, almost surely every consensus halving cuts at least items. The paper generalizes it to consensus -splitting (Theorem 5.3, at most cuts).
Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. The mission produces a checked consensus-halving model for additive utilities over unordered items and a checked proof of the bound, together with a reusable fact about linear systems: a system of equations in unknowns with a unique solution has .
The obvious approach is to note that the consensus halvings form a polytope in cut out by equations, and that a vertex of that polytope has at most fractional coordinates. The difficulty is to make "vertex" precise and nonempty in Lean: one must show that the polytope (nonempty, since it contains ) has a point where enough box constraints are tight, which needs either an extreme-point argument for compact convex sets or the paper's explicit procedure. The procedure in turn needs a termination argument: each pass freezes one new coordinate at or , and when no further move exists, a dimension count on the solution set of is required. The step coefficient may exceed , so the "convex combination" of the paper is an affine one, and the bound comes from the minimality of , not from convexity.
Fin n, items Fin m (the paper's , , indexed from ). The bounds are not assumed; every statement remains true for or .u : Fin n → Fin m → ℝ. Nonnegativity, a standing assumption of §2, is a hypothesis of the goal only; the milestones hold for real utilities of any sign, as the paper remarks on p. 6 for combinations of goods and chores.IsConsensusHalving includes . Without that bound every solution of (1) would count, and the cut count would be meaningless, so a formalization dropping it is ruled out.numCuts is the cardinality of the set of cut items.gamma x y j is the of Step 3(a). At it takes the junk value , and every statement using it quantifies over only and assumes , so the junk value never enters.The hypergraph k-cut problem asks for a least-cost way to split the vertices of a hypergraph into nonempty groups. An edge of a hypergraph may contain more than two vertices, so the graph version does not capture the behavior of every input. For fixed , randomized polynomial-time algorithms for hypergraph k-cut were known before the deterministic result of Chandrasekaran and Chekuri. Their paper identifies a structural property of optimal partitions that makes one of their deterministic approaches possible. This mission isolates that property as a mathematical theorem about finite hypergraphs.
The same paper explains why the distinction between hypergraph k-cut and partitioning by a general symmetric submodular set function matters. The hypergraph cut function is symmetric and submodular, but the cost of a k-partition counts each crossing hyperedge once; it is generally different from the sum of the cut values of the parts. The paper also gives a counterexample to a proposed extension of its uncrossing theorem to general submodular functions. The target here therefore uses the actual hyperedge crossing cost throughout. Chandrasekaran and Chekuri, §§1.1 and 3.
Let be a finite unit-cost hypergraph. A hyperedge is a subset of the vertex set , and may contain parallel copies. For a vertex set , its cut value is the number of edge copies meeting both and its complement . Thus empty edges, singleton edges, and edges lying entirely on one side contribute zero. This is the paper's convention after it reduces to unit costs in §1.1. Source, pp. 3 and 7.
An ordered k-partition has nonempty, pairwise disjoint parts whose union is . Its cost counts each hyperedge once if that edge meets at least two distinct parts. A minimum k-partition has least cost among all such ordered partitions. It is maximal minimum when there is no other minimum k-partition whose first part strictly contains . The order matters because the theorem singles out . Source, p. 4.
For disjoint vertex sets , an -terminal cut is a source set with . A minimum terminal cut has the smallest among these sets. The source-maximal minimum terminal cut is the minimum cut whose source set contains the source set of every other minimum -terminal cut. This condition identifies one set, even when several minimum cuts have the same value. Source, p. 3.
For , let be a maximal minimum k-partition with . For every that meets every with , the goal is
This is Theorem 1.2, p. 4. The size is an equality, and the set may depend on . Source maximality is part of the conclusion.
The milestone list includes symmetry and submodularity of , uniqueness of the source-maximal minimum terminal cut, the counting statements of §3 (Proposition 3.1, the identity ; Lemma 3.1, the one-step refinement bound on ; Lemma 3.2, the bound for uncrossed minimum terminal cuts; Lemma 3.3, the selection of parts), and the containment and extremal claims used in §4 (Lemma 4.1, Claims 4.1 and 4.2). The principal intermediate target is Theorem 3.1: under its specified family of minimum terminal cuts, it produces a k-partition whose last part strictly contains a given complement , and whose cost is at most half of every pair sum . These are separate theorem statements with the same finite hypergraph model.
Theorem 1.2 says that a part of a suitably chosen optimum partition can be specified by a bounded-size source set and a sink set meeting the other parts. It gives a finite certificate for recovering that part via a minimum terminal-cut problem. Unlike a statement about one specially chosen low-cut-value part, it applies to the first part of any maximal minimum k-partition that meets the size condition. The paper uses this theorem to derive its first deterministic polynomial-time algorithm. Chandrasekaran and Chekuri, Theorem 2.1 and §2.
This mission formalizes the known structural result, not a new conjecture. The Lean statements are compiled with proof placeholders; the mathematical proofs remain work for solvers. A complete development would produce reusable definitions and lemmas for hypergraph cut values, minimum terminal cuts, uncrossing, and counting edges crossing a partition. These objects are also useful for checking related claims about graph cuts and constrained partitions.
For a graph edge, crossing a partition has only two endpoints to track. A hyperedge may meet several parts at once, and the relationship between the sum of part cut values and the cost of the whole partition changes with that pattern. A direct submodularity argument does not control all the needed costs. Section 3 introduces an auxiliary count that distinguishes edge patterns, and Theorem 3.1 combines minimum terminal cuts with a partition cost bound. Section 4 then uses that bound to rule out a failed choice of the source set in Theorem 1.2. The paper explicitly shows that the corresponding uncrossing statement fails for arbitrary symmetric submodular functions. Source, §§3–4, especially Remark 3.2.
Vertices have a finite Lean type, vertex subsets are Finset V, and hyperedges form a Multiset (Finset V). The multiset preserves parallel copies under unit costs. Partitions are functions Fin k → Finset V; their parts are required to be nonempty, disjoint, and exhaustive, with P 0 representing . Complements are relative to all vertices. All counts are natural numbers. The theorem assumes , so is the ordinary nontruncated value. It counts a crossing edge when that edge meets at least two parts, following the explicit mathematical test in the paper's definition.
The source-maximal predicate requires both minimum cut value and containment of every other minimum terminal source set. Neither a merely minimum cut nor an arbitrary maximal minimum cut is accepted as the target. The cost and d functions count edge copies, including duplicate hyperedges, so replacing the multiset by a set would change the problem. The published predicates for symmetric and submodular real-valued set functions are reused after casting the cut counts to real numbers.
Theorem 1.1, the polynomial-time algorithm claim, is outside this mission. It would need a precise machine and running-time model; an unqualified existential algorithm claim would also be satisfied by exhaustive search. The algorithms and running-time theorems of §§2 and 6, and the distinct structural results of §§5–6, are not represented here. Contributions toward proofs of the source-maximal cut theorem, the §3 counting estimates, and the §4 containment argument are within scope.
Retailers that source apparel and other consumer goods from contract manufacturers in developing countries often work through a procurement service provider, an intermediary that solicits quotes, negotiates and manages production on the retailer's behalf. A documented problem in this industry is the hidden rebate: some manufacturers pay the intermediary a covert "referral commission" whenever they win an order. The intermediary then has a reason to favour those manufacturers, and, because the retailer sees quotes only through the intermediary, it can inflate the quotes of manufacturers that pay nothing. The retailer ends up buying from a more expensive source.
Fan, Chen and Tang (SSRN 3514358; Manufacturing & Service Operations Management, 2020) ask what a retailer can do about this with contracts alone, without audits or penalties, when it can verify a quote only with the manufacturer it finally selects. Their answer for the base model is an explicit contract: a selection rule that handicaps the rebate-paying manufacturer by the size of the rebate, together with a service fee equal to the rebate. The paper relates to the literature on middlemen and corruption in procurement (Burguet and Che 2004; Burguet and Perry 2007) and on mechanism design with partial verification, where Strausz (2016) showed that the revelation principle survives when only the selected party's report can be checked.
A retailer must buy one order from one of two manufacturers. Manufacturer is known to be ethical; manufacturer pays the intermediary a fixed hidden rebate if and only if wins. The manufacturers' prices are independent draws from a common distribution with density and survival function . Because builds the rebate into its quote, the true quotes are
The intermediary observes and reports to the retailer. A deterministic contract is a selection rule and a non-negative service fee . After choosing , the retailer checks the selected manufacturer's quote: if , the intermediary is paid and, if was selected, also collects from ; otherwise it receives nothing. Its ex post payoff (1) is
A contract is incentive compatible (13) when truthful reporting maximizes this payoff for every pair of true prices; ties are resolved in favour of truth-telling. Under truthful reporting the retailer pays , and its problem (14) is to minimize the expected value of this cost over incentive-compatible contracts.
The threshold of footnote 15 is
In the Lean development these objects are quote, payoff, IsIC, Feasible, cost, contractStar, Gbar and rbar, in the namespace HiddenRebate.Fixed.
Let be the contract (15):
If , then is incentive compatible, its expected cost is finite, and
for every admissible incentive-compatible deterministic contract .
Theorem 1 gives the retailer a contract that can be written down and implemented: it removes quote inflation entirely, selects the cheaper manufacturer in every state (no distortion), and lowers the retailer's expected cost from under "lowest quote wins" to (Corollaries 1 and 2 of the paper). The price of honesty is exactly the rebate, paid as a fee. The optimality half says that no other deterministic incentive-compatible contract does better as long as the rebate is below .
The paper's proof of Theorem 1, including the characterization of incentive-compatible contracts and the optimal contract for , is in an appendix that is not part of the preprint held for this mission. Formalizing the theorem therefore means reconstructing the optimality argument, not transcribing it. No machine-checked proof of this result, or of any result of the paper, is known.
Incentive compatibility of (15) is a short case check. The difficulty is optimality: the class of competitors is every pair of measurable maps on satisfying (13), and the obvious comparison with the first-best cost fails, because a competitor can pay less than in some states. One has to understand which contracts are incentive compatible under partial verification, where the intermediary can freely misreport the quote of the manufacturer that is not selected, and show that every such contract costs at least when . The threshold is an infimum over a two-parameter family, so the comparison must hold uniformly over that family.
Prices live in with ; is a probability measure absolutely continuous with respect to Lebesgue measure (the density ); the joint law of is . Reports range over all of , and (13) is required for every pair and every report, pointwise. A contract is a pair A : ℝ × ℝ → Supplier, F : ℝ × ℝ → ℝ with , measurable and measurable. The cost (14) is the Bochner integral over of at .
Conventions and additions relative to the page, all disclosed in the item statements:
The goal compares the cost of (15) with each competitor's cost directly; it is not stated with substituted for the left side, and it is not reduced to incentive compatibility alone, which is milestone 1. For iid Exp(1) prices , so the hypothesis is satisfiable; for prices with bounded support and the theorem is vacuous, as on the page.
Needed infrastructure: product measures and Bochner integrals on (in Mathlib), and a characterization of incentive-compatible contracts under partial verification, which would be reusable for other models in which only the selected agent is audited. Contributions of intermediate lemmas, such as lower bounds on the cost of incentive-compatible contracts, are welcome as linked theorems.
Ad-supported media and digital services (streaming music and video, news sites, social platforms) sell to two sides at once. Consumers value the content, advertisers value the consumers' attention, and consumers usually regard advertising as a nuisance whose cost differs from one person to the next. Many such platforms answer this with menu pricing: a free tier with ads next to a paid tier with few or no ads, so that consumers sort themselves by how much they mind advertising.
DeValve and Pekeč (SSRN 2715531; Operations Research 70(3), 2022, doi:10.1287/opre.2021.2230) characterize revenue-maximizing price/advertising menus when the platform does not observe a consumer's advertising disutility, first for a monopoly and then for a duopoly in which consumers decide endogenously whether to use one platform (single-homing), both (multi-homing) or neither. Earlier models of competing ad-supported platforms either fix homing behaviour through Hotelling competition (Anderson and Coate 2005; Armstrong 2006) or allow multi-homing with homogeneous ad disutility (Ambrus, Calvano and Reisinger 2016). This mission targets the paper's duopoly result, Proposition 3: the equilibrium with menus exists, is unique, and is symmetric, with both consumer types multi-homing.
A representative consumer has base value for content and is of type with advertising disutility , . Type occurs with probability ; write , . Two platforms each offer a menu of two items , a subscription price (negative prices allowed) and an advertising quantity ; the two items of a menu may coincide.
A consumer who single-homes on platform with item and consumes gets . A consumer who multi-homes with items , gets
where measures substitutability between the platforms. The utility of a choice is the supremum over nonnegative consumption; abstaining gives . Write for the cost of an item to type .
Advertisers pay a per-type market-clearing price , the sum over the platforms the consumer uses, and a platform used with item earns . Each platform maximizes its expected revenue over the two types.
An equilibrium is a menu profile with consumer choices such that: each type maximizes utility; on ties she multi-homes if multi-homing is optimal and participates if participating is optimal; and no platform can raise its expected revenue by switching to another admissible menu, when the consumers respond optimally under the same tie rules, the deviator may select the response most favourable to it, and a type that uses the rival platform before and after the deviation keeps her item there. The paper uses this concept in its proofs without naming it. The mission writes it out.
Let and .
With
the profile in which both platforms offer and each type multi-homes on is an equilibrium; the two items are distinct; in every equilibrium each menu is exactly these two items and each type multi-homes on her item; and each platform's expected revenue is
The proposition describes how competition shapes menus. With two platforms, consumers of both types use both platforms, the menus are symmetric, and the low-disutility type is given a price discount while the high-disutility type gets an advertising discount. When the menu is a "free use with ads / pay for no ads" menu. The paper builds on this characterization: Corollary 1 compares monopoly and duopoly prices by type, and Proposition 4 shows the value of offering a menu instead of a single item can exceed under competition.
No machine-checked version of these results exists. A formal proof checks a uniqueness argument that runs over every combination of homing behaviour and every admissible deviation, and it fixes an equilibrium concept that the paper uses without defining. The model file is reusable for the paper's other duopoly results (Lemma 3, Proposition 4, Corollary 1) and for related two-sided pricing models with quadratic utility.
The consumer has nine possible choices per type, and a platform's deviation changes which of them is optimal. A best response is therefore not one optimization problem but a family indexed by homing behaviour, and the ad price couples the two platforms through every type that multi-homes. Reducing the deviation problem to a single program requires showing that no deviation profitably moves a type from multi-homing to single-homing, which uses the rival's menu and the tie rules. The uniqueness part needs every non-multi-homing configuration ruled out separately (Lemma 8) and then a fixed-point argument for a piecewise-linear best-response map with a pooling regime. Tie-breaking matters: without the multi-homing tie rule or the status-quo rule on the rival platform, the stated profile is not an equilibrium.
Lean represents platforms and item slots by Fin 2 (the paper's platforms 1, 2 are 0, 1), menus by Fin 2 → ℝ × ℝ with entries (s, a), and all quantities in ℝ. A menu is admissible when every ad quantity is nonnegative; prices are unrestricted. Utilities are suprema over nonnegative consumption, which are finite because . They are not defined by the closed forms of Lemma 6. The equilibrium predicate IsEquilibrium encodes the four rules above: consumer optimality, multi-homing and participation on ties, arbitrary admissible deviations with the deviator's most favourable admissible response, and the status-quo rule on the rival platform. The strategy space is two-item menus, as in the paper after Lemma 7. Uniqueness is uniqueness of the chosen items and of each menu as a set, up to which slot holds which item.
Two hypotheses are added to the paper's standing assumptions and disclosed: , and , without which the stated is negative. The condition is not assumed; the case is part of the result.
The goal is not posed as "each menu solves the platform's program (21) given the other". That would assume the reduction from the game to the program, which is the content of Lemma 8 and of the platform-best-response step. The goal quantifies over all equilibria of the game itself. Existence is a conjunct of the goal, so the uniqueness and revenue clauses cannot hold vacuously.
Needed: the model file (provided), elementary calculus of concave quadratics for Lemma 6, and case analysis over finite choice sets. Welcome contributions are proofs of the Lemma 6 parts, the fixed-point algebra, the consumer-choice step, and the two platform best-response steps.
A partially observed array with three indices appears when data record relationships among triples of objects. If its entries have a low-rank structure, one can hope to recover the full array from far fewer than measurements. Cai, Li, Poor and Chen study this problem when the measurements are noisy and only a random subset of entries is seen. Their result gives a statistical error bound for a concrete two-stage method: spectral initialization followed by ordinary gradient descent on a nonconvex loss. It is a known theorem, proved in the pinned preprint, rather than an open conjecture.
The unknown symmetric order-three tensor is . It has a CP decomposition , where the nonzero columns form . Each unordered triple of coordinates is sampled independently with probability ; its six permutations share one sampling decision. On a sampled triple the observation is , with symmetric, centered, independent sub-Gaussian noise of variance at most . The observed tensor vanishes outside the sampled set .
For a candidate factor matrix , the objective is
Algorithm 2 obtains a leading -dimensional eigenspace from an off-diagonal Gram matrix of the mode-one unfolding of . Algorithm 3 uses Gaussian restarts, leading singular vectors, and greedy pruning to turn that subspace into a factor matrix . Algorithm 1 then applies the gradient step to . Eigenvalue ties, leading singular-vector choices, and pruning ties can produce several admissible executions; the result concerns every execution.
Incoherence measures how evenly the tensor and factors spread across coordinates and how nearly orthogonal distinct factors are. The condition number is the ratio of the largest to smallest factor norm. Write and . Distances , , and minimize their respective matrix norms over permutations of the columns.
The goal is Theorem 2.4, in the bounded-rank, bounded-incoherence, bounded-condition-number regime. Under its printed sampling, noise, restart, threshold and step-size conditions, for every it asserts, with probability at least ,
The rate is fixed to , consistent with the paper's local-convergence lemmas. Milestones formalize the gradient identity (36), local Hessian bounds (Lemma 5.1), spectral-subspace recovery (Lemma 5.7), factor retrieval (Theorem 5.9), and the paper's general-parameter recovery theorem (Theorem 2.8). The latter makes the dependence on and explicit.
The inequalities give two guarantees at once: geometric reduction of initialization error and an explicit noise floor. The bound controls the error in each coordinate row, which a Frobenius estimate alone does not supply. Together with the tensor-entry corollaries in the paper, they explain the accuracy of this practical nonconvex method under random subsampling. The authors also specify how the sample probability, noise level, rank and incoherence interact, so the result can be compared to other tensor-completion methods.
This mission asks for a machine-checked version of the known result. Its published ψ₂ norm definition is reused; the paper-specific tensor model, spectral initialization relations, loss and gradient iteration are new. The theorem statements compile with sorry, so none of their proofs is claimed as machine checked here. Proofs of the listed milestones, the main theorem, and faithful auxiliary concentration results are welcome; the paper's numerical experiments are outside this formalization.
The gradient loss is nonconvex, so global convexity cannot justify the iteration bound. The local Hessian estimate applies only near in both Frobenius and rowwise norm. A Frobenius estimate alone cannot establish the rowwise condition at every iteration. The spectral initializer must also select individual factors from a subspace despite nearly tied eigenvalues and noisy tensor contractions. These are the points where a direct appeal to standard smooth-gradient-descent theory stops short of the stated result.
Coordinates are Fin d and Fin r, with zero-based indexing; the PDF uses one-based indices. All logarithms are natural. Tensor and matrix norms are explicit finite-coordinate Euclidean norms. Minima over permutations range over all permutations of Fin r, and maxima in the incoherence parameters range over the indices specified by Definition 2.1. Sampling is on sorted triples, then extended by symmetry. The probability model is a single probability space carrying the sampling indicators, noise variables and Gaussian restarts, jointly independent; the paper leaves some cross-family independence implicit. Noise has mean zero, variance at most , and ψ₂ norm at most using the published extended-nonnegative norm. The last bound makes the paper's sub-Gaussian scale explicit.
The statements use , , nonzero true factor columns, , and . Theorems 2.8 and 5.9 use and round their real-valued restart count up to a natural number; this handles the boundary where . Theorem 2.4 places its claimed absolute error constants before the rank and incoherence bounds and all instance data. Probability is expressed as the outer measure of the bad event, since admissible-execution predicates quantify over choices and need not be measurable. Each good event explicitly asserts that an admissible execution exists before requiring the bounds for every execution; otherwise a failed pruning run would make a universal claim vacuous.
The remaining reusable infrastructure includes concentration for symmetric sampled tensors, finite-dimensional spectral perturbation with ties, and derivative estimates for the cubic factor map. The paper's leave-one-out iteration lemmas and their auxiliary estimators are not included in this initial milestone list; they remain natural contributions toward the full proof.
Banks hold claims on one another. When one bank cannot pay, its creditors receive less, which can push them into default in turn. Clearing models compute the payments and wealths that are consistent across the whole network. Regulators and researchers use them to measure systemic risk and to price interbank debt. The basic model is that of Eisenberg and Noe (2001), doi:10.1287/mnsc.47.2.236.9835. Rogers and Veraart (2013), doi:10.1287/mnsc.1120.1569, added bankruptcy costs: a defaulting bank recovers only part of its assets.
The value of a bank's debt or equity is an expectation over random endowments. For general endowments that expectation requires partitioning the endowment space into up to default regions (Gouriéroux, Héam and Monfort 2012), and with bankruptcy costs those regions need not be convex. Banerjee and Feinstein, Pricing of debt and equity in a financial network with comonotonic endowments (Operations Research 2022; arXiv:1810.01372), observe that when all endowments are driven by one factor (they are comonotonic), banks default in a fixed order as the factor falls. Default probabilities and the prices of debt and equity then have closed forms.
There are banks and an outside society node. Bank owes a total of ; the fraction of it is owed to bank (), and the fraction to society (Assumption 2.1). The matrix is the relative liabilities matrix. Banks start with endowments . A bank with negative wealth defaults and keeps a fraction of its external assets and of its interbank assets.
With componentwise, the clearing process is
and a variant , which replaces by its positive part, is used in the appendix. The greatest clearing wealth is the largest real solution of . Bank 's payment is and its equity is .
If the set of defaulting banks has indicator , the clearing equations are linear. With the diagonal 0–1 matrix of ,
Comonotonic endowments are for a nonnegative random factor and a nondecreasing map (Assumption 3.2). The solvency threshold of bank is (Definition 3.4). Banks are numbered so that , with and (Assumption 3.5). On exactly banks default; and are and at that default set, with and .
With , for every bank :
The goal is the theorem as printed, with one added hypothesis (see Formalization scope).
Theorem 3.6 turns the valuation of every bank's debt and equity in a network with bankruptcy costs into one-dimensional integrals of the factor, replacing the default regions of the general case. The default probabilities depend only on the thresholds , which in turn depend only on the map and not on the law of . The same formulas price debt and equity in the paper's numerical study of the European banking system, and they are the starting point for the comonotonic bounds of Lemma 4.1, which are not part of this mission.
The paper gives a one-sentence proof of Theorem 3.6 and proves its appendix results largely by citation (Tarski, Milgrom–Roberts, Rogers–Veraart, input–output theory). No part of it has been machine-checked. A formalization supplies the missing steps: the identification of the two clearing maps, the attainment of the thresholds, nonsingularity of the linear systems, and the decomposition of the expectations. It also produces, as a reusable by-product, the Rogers–Veraart clearing model with its greatest fixed point, which other financial-network results can build on.
The obvious argument is: banks default in order, on each interval of the wealth is affine in , so integrate piece by piece. Two steps of it fail as stated.
First, the threshold is an infimum, and the paper treats it as attained ("the minimal value such that firm is solvent"). With bankruptcy costs the wealth jumps when a bank defaults, even for continuous , so attainment needs an argument about the greatest fixed point under decreasing endowments. Without right-continuity of it is false.
Second, the greatest fixed point of is not reached by Tarski's theorem on , because is not monotone below . That every real fixed point lies above uses Assumption 2.1. Nonsingularity of also rests on Assumption 2.1. Matching the default set to the interval then combines monotonicity (Proposition A.6) with the ordering of Assumption 3.5.
Fin n; bank i is the paper's bank . The data are , , , (structure Network), with the standing assumptions bundled in Network.Standing. is the supremum of the real fixed points of in the lattice ; payments and equity follow Definition 2.2. Default sets are finite sets of banks. Inverses are Matrix.inv.i.When banks are hit by losses they sell assets to restore their leverage targets, and these fire sales depress prices for every other holder of the same assets. The resulting deviation of market capitalization from its fundamental value is a systemic externality: it depends not on any single bank's portfolio but on how the stock of each asset is distributed across banks. Awiszus, Capponi and Weber (arXiv:2003.10121, Operations Research 2022) ask which distribution of a fixed stock of assets among banks with fixed budgets minimizes this externality, as measured by the expected squared deviation of market capitalization from fundamentals. The question matters to macroprudential regulators, who can influence portfolio overlap among banks, and it connects to the literature on overlapping portfolios and price-mediated contagion (Greenwood, Landier and Thesmar, 2015; Capponi and Larsson, 2015).
The paper's answer is explicit: the optimal mean squared deviation has a closed form, the optimum is computed by a two-step "aggregate first, then allocate" procedure, and the optimal allocation is unique exactly when there are two banks.
There are assets and banks. A holding matrix records in entry the holding of asset by bank , so column is bank 's portfolio. Initial prices are normalized to .
Let . Then
the f-efficient holding matrix is unique if and only if , and in that case it equals
The result itself. Theorem 4.1 gives the smallest achievable mean squared deviation of market capitalization from fundamentals for a given asset supply, budget profile and systemic significance profile, as an explicit function of the shock moments. It is the benchmark against which the paper measures the inefficiency of observed and diversified holdings (Section 4.2 shows that full diversification is f-efficient only in a degenerate case) and drives the comparative statics of Section 5. Part b) says that with three or more banks efficiency leaves an affine family of optimal allocations of dimension , so a regulator has residual freedom to pursue other objectives at no cost in market efficiency.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The formal development delivers the theorem together with a reusable treatment of minimizing a positive definite quadratic form over a hyperplane, the existence part of the transportation-type linear system , , , and an exact rank computation for the structured matrix . The uniqueness characterization in part b) depends on that rank computation, which the paper carries out by Gaussian elimination on block matrices.
The minimization over is a -dimensional quadratic program whose objective is degenerate: it depends on only through the -vector . Strict convexity therefore cannot give uniqueness, since the objective is constant along every direction in which and the constraints do not change, and the obvious argument for part b) fails. Existence is not automatic either: is unbounded, and one must show that every point of the hyperplane is attained as by a feasible , which fails when is constant. The uniqueness statement is a dimension count: it needs the exact rank of the constraint matrix , whose rows carry exactly two linear dependencies under Assumption 3, so that the solution set has dimension , which is positive as soon as and .
Fin K, banks are Fin N, all quantities are real; holding matrices are Matrix (Fin K) (Fin N) ℝ. The paper's banks 1 and 2 are the indices 0 and 1.Matrix.inv, which returns on singular matrices. Every statement that mentions , or assumes for all (Assumption 2), and every statement that divides by assumes .Module.finrank of the kernel of .Fin.cast.The development needs the Sherman–Morrison identity for a diagonal-plus-rank-one matrix, the minimizer of a positive definite quadratic form under one linear constraint, explicit constructions in , and a rank computation. Contributions of reusable lemmas for these, and of proofs of the milestones in any order, are welcome.
A customer who is told that service will be delayed can use the announced wait to decide whether to stay, leave, or plan around the delay. A service operator needs to know whether a changing, customer-specific announcement actually predicts the eventual wait more accurately than a fixed announcement. Bassamboo and Ibrahim studied this question for the last-entered-service (LES) announcement, which reports the wait of the last customer to enter service, and for a static announcement based on the mean wait of delayed customers. Their empirical examples show that neither method wins uniformly across queueing regimes; the comparison depends on how the announcement and the eventual wait move together (Bassamboo and Ibrahim, 2021, §§3–4 of the submitted manuscript).
The mission isolates the paper's general comparison criterion. Its statement needs no particular arrival process, service discipline, or queue length. This makes the result a reusable mathematical test for predictors in other service systems as well as for LES. The paper itself notes that the criterion applies irrespective of the specific queueing model, subject to the moment conditions under which its mean-squared errors and correlations are defined (submitted manuscript, §4.2, p. 14).
Let be the real-valued waiting time of a delayed customer in steady state. Operationally, the paper takes the virtual waiting time and conditions on : has the conditional distribution of a positive wait. Let be a real-valued predictor issued to that customer. To compare a prediction with the outcome, the pair must be jointly distributed; their separate marginal distributions cannot determine the correlation. Both are represented as functions on one probability space in Lean.
The static announcement, denoted , always reports . A changing predictor can instead respond to the system's current state. The paper's mean-squared error of is the expectation of its squared discrepancy from the outcome:
Write and for variance and covariance. When both variances are positive, the Pearson correlation is . The coefficient of variation of the delay is . These are the quantities in §4.2 and equation (3) of the submitted manuscript (published article; mission citations use the submitted manuscript's page and equation numbers).
The first milestone establishes the error of the static predictor from its definition:
The next two milestones give the expanded error identity from the proof of Proposition 1 and its normalized form, equation (4). Suppose and with . Proposition 1 states
The goal is Corollary 1, equation (5). If has the same mean and variance as , it compares the two predictors at the exact threshold :
Both inequalities are non-strict. The corollary is stated for a general predictor ; applying it to LES requires a separate analysis of the LES wait and its correlation with the arriving customer's wait. The submitted manuscript supplies that model-specific analysis later in §5 (Bassamboo and Ibrahim, 2021).
Under the corollary's equal-mean and equal-variance assumptions, the comparison of two expected squared errors reduces to one correlation. A predictor with correlation at most offers no mean-squared-error improvement over the static announcement; a predictor above that threshold does. The equality case is included. Proposition 1 also records how a mean shift or a variance change modifies this comparison, which is useful when a proposed announcement is biased or more variable than the delay.
The paper proves these identities. This mission asks for machine-checked proofs of their statements in Lean; the draft theorems themselves are open proof obligations. A completed development would provide reusable definitions of predictor MSE, the constant mean announcement, Pearson correlation, and coefficient of variation, together with exact interfaces for later queueing results. It does not assert that the paper's LES limit theorems are already formalized.
The key mathematical work is passing from the expectation of a squared difference to the variance and covariance terms while keeping the two random variables on the same probability space. In Lean this requires the integrability consequences of square integrability, the relation between covariance and the centered product, and careful handling of the square-root normalization. Merely replacing MSE and correlation by unrelated real parameters would erase that work and yield an elementary numerical equivalence. The proposed definitions are therefore the expectations and covariance stated in the paper, and the goal quantifies over actual random variables.
The boundary also needs attention: the predictor has zero variance and ordinary Pearson correlation has a zero denominator. The term involving correlation is multiplied by , so the displayed identity still has a meaningful value under the Lean convention described below. Proposition 1's other denominator, , requires a positive delay mean and variance in the intended setting.
Lean uses an arbitrary measurable space with a probability measure and real-valued functions on that space. It does not construct the underlying queue; §4.2 makes the comparison at the level of the joint law of the delay and prediction. Each theorem explicitly assumes where both appear. This supplies finite second moments for the paper's variances and MSE and avoids Lean's default value for a nonintegrable real integral. The EA identity only needs .
Positive variance of is explicit in Proposition 1, its expansion, and the corollary. It gives the intended domain of correlation in the equal-variance corollary and prevents equation (4) from failing under division by zero. Proposition 1 additionally assumes , as expected for a positive conditional wait, so . No condition is imposed: at , Lean evaluates the zero-denominator correlation as zero and the entire correlation term vanishes. The error is defined with as in equation (3), although the proof writes the reversed difference. Contributions toward the integral identities, covariance normalization, and the final inequality are welcome; the four definitions may also serve other prediction-error formalizations.
In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.
Write for the set of all subsegments of with . An interval may be degenerate, meaning . A real-valued function on is continuous when its value varies continuously with the two endpoints. The required boundary condition is for every . No sign, monotonicity, or additivity condition is imposed. A partition into parts is a sequence , so its parts may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.
The intermediate setting is a nice multivalued function. Its graph is a compact subset of . The graph separates the bottom from the top inside the cylinder : those two sides lie in different connected components of . A representation of a nice graph is a continuous real function on that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.
For a prime , a segment , and a value , a zero partition is a sequence such that for each . The set contains exactly those pairs that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.
The goal is Theorem 1.1: for every positive integer and every continuous satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:
The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when , there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for . The milestone list includes the fixed-segment and continuous-family statements used to characterize , and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.
The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.
The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.
For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod- statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy , not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.
Lean represents by the endpoint pair with . The cylinder uses the closed value range ; a nice graph lies in its open interior . Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.
Every prime-step claim assumes prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes . The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.
Firms that serve several geographic markets must decide both how much to produce and where to sell it. A capacity limit couples those regional decisions: an extra unit sent to one region cannot also be sent to another. Different transport costs and demand curves make a collection of independent single-region Cournot models inadequate. Alsabah, Bernard, Capponi, Iyengar and Sethuraman study whether this coupled quantity game has a determinate outcome. Their 2020 author version proves a unique equilibrium allocation and characterizes it through firms' marginal profits. This mission concerns that result, Theorem 4.5 on p. 12 of that version.
There are firms and regions . Firm sells quantity in region . Its total output is , constrained by capacity . The total sales in region are . The inverse demand function gives the price when total sales are . Firm pays production cost per unit and transport cost per unit sent to region . Its profit at allocation is
A strategy for firm is any nonnegative regional allocation whose total is at most . A Nash equilibrium is a feasible profile at which no firm can gain by changing its entire regional allocation while the others hold theirs fixed. This is the feasible unilateral-deviation definition in the paper's Definition 3.1, p. 8.
The marginal profit in region is
For a vector of marginal-profit levels, condition (2) says and for every firm and region. Proposition 4.2 gives a unique nonnegative allocation satisfying these conditions, denoted , when lies in the box , where and . The reduced-form operator assigns firm zero marginal profit if its output at is below capacity. Otherwise it assigns the marginal-profit level at which its output under equals . This is the two-case definition on p. 11; it depends on the other firms' marginal-profit levels through .
Lemma 4.3 asserts that has exactly one fixed point in the marginal-profit box:
Theorem 4.5 identifies every equilibrium of the original quantity game with the allocation at that fixed point:
The goal includes existence of and the equivalence, so it asserts both existence and uniqueness of the equilibrium allocation. Its milestones follow the paper's supporting statements: existence of a pure equilibrium, marginal-profit conditions, existence and uniqueness of , continuity and comparative statics, fixed points of , and the link from an equilibrium to a fixed point. The Algorithm 4.1 computation clause of Proposition 4.2 and the iteration-convergence clause of Lemma C.5 are identified as partial milestones; their full printed text is retained in the milestone provenance.
The result establishes that capacities, regional demand, and unequal shipping costs still lead to a single predicted sales allocation under the paper's regularity conditions. It also gives a common language for comparing the original game with a smaller game in marginal-profit vectors. Subsequent results in the paper analyze changes in costs, capacities, prices, and consumer surplus relative to this equilibrium Alsabah et al., §§5–6; those later comparative-statics claims are outside this mission.
The mathematical result is proved in the cited paper. The goal here is a machine-checked Lean development of its model, its fixed-point characterization, and the existence and uniqueness theorem. The current proposal contains definitions and theorem statements, with proofs open. The pure-Nash relation is a published reusable definition; the market model, complementarity allocation, and operator are new interfaces that could also support later formalizations of the paper's comparative-statics results.
An equilibrium of the quantity game satisfies the marginal-profit conditions, but those conditions alone describe candidate allocations and do not replace feasible unilateral deviations. Conversely, a fixed point of does not become an equilibrium merely from the fixed-point equation: the capacity-constrained regional payoff problem still has to be connected to the allocation . Uniqueness also requires control of how all firms' regional sales respond when one marginal-profit coordinate changes. Lemma C.4 records weak and strict changes, including boundary cases where a firm stops selling in a region. The existence lemma invokes a general pure-strategy equilibrium argument; the statement is kept even though that infrastructure is substantial in Lean.
Lean uses Fin N and Fin R for zero-based firm and region indices. An allocation has type Fin N → Fin R → ℝ, with the firm coordinate first, the transpose of the matrix orientation in the paper. Finite sums give firm and region totals. The inverse demands are on , strictly decreasing and concave on nonnegative quantities; deriv is therefore the ordinary derivative at the quantities used here. The paper phrases Assumption 1 for direct demand on and then uses regularity of its inverse . The formal model makes that inverse-demand regularity an explicit assumption. It also states , as implicit in the interval , positive capacities, and nonnegative production and transport costs. Those sign assumptions are needed for the box and the two branches of to have the stated meaning. No positivity of prices at all quantities or finite choke quantity is assumed.
IsEquilibrium uses the published CarbonDoubleCount.Planner.IsPureNash relation, testing every feasible full strategy deviation. Qhat is chosen as the unique solution of condition (2), and Phi is computed from that allocation and the market capacities. On the stated box, the proposal's milestones establish that the selection and inverse branches denote the paper's objects. The intended theorem excludes encodings that choose an active set freely, pass or as arbitrary parameters, or substitute first-order conditions or coordinatewise deviations for Nash equilibrium. The definition layer and results on continuity, monotonicity, and fixed points are reusable parts of the development. Contributions that prove these stated targets or provide supporting analysis of the firm's concave payoff problem are within scope.