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.
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 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.
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.
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.
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.
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.
A visible patroller gives an attacker information: the attacker can observe when a location is vacant and wait for a favorable moment. This changes the patrolling problem from choosing how often to visit each location to choosing a movement rule that remains effective against an adversary who chooses the attack time. The preprint The Uniformed Patroller Game studies this setting on a star network, where the patroller moves between a central base and the locations she protects. Its main result characterizes a robust attack delay and a robust patroller reflection rule for every attack duration, as well as exactly when those choices are unique. The source here is arXiv:1908.07366v2, by Alpern, Chleboun, and Katsikas; the later journal article has a different title and author list.
The network has a centre and end nodes. Each end node is a location to defend; the centre is a base and is not an attack location. A Markov patroller strategy is a pair . When at , the patroller goes to each specified end node with probability and stays at with probability . When at an end node, she returns to with probability and otherwise stays at that same end node. Thus , , and . The strategy does not depend on which node the attacker selects.
The attacker chooses an end node and an integer delay . After the patroller leaves , the attacker counts consecutive periods of her absence. If she returns before periods pass, the count resets. Otherwise the attack begins in the th period of absence. It lasts periods and is intercepted if the patroller visits during that interval. The paper requires because a one-period attack could always begin immediately after departure. This mission also takes , ensuring another end node exists and the conditional attack event has positive probability under the admissible strategies.
Let be the first positive step at which the patroller, having just left for , returns to . The starting state is already the first period of absence. The interception probability is the paper's equation (17):
The patroller maximizes and the attacker minimizes it. A saddle point is a pair of strategies for which neither can improve by changing alone, with comparisons over all admissible and all end-node-and-delay pairs . A strategy is called optimal if it occurs in a saddle point. The source analyzes pure strategies in these parametric sets; a pure saddle remains a saddle if independent randomization of these strategies is permitted.
Theorem 1 asserts that some optimal patroller strategy has and pairs with an attack at any end node with . It also asserts two exact uniqueness regimes:
The patroller's centre-to-end probability is selected optimally; it is not fixed in the main statement. The attack node is immaterial by symmetry, but it remains an explicit part of every attacker strategy. The theorem is posed over the full strategy sets, so its uniqueness assertions cannot be satisfied by restricting those sets to the displayed choices.
The milestone list follows the source's symmetry reduction, Lemmas 1–3, equations (3) and (15), and Propositions 1–2. For , Proposition 1 identifies and the value . It also identifies optimal reflection probabilities below one. For odd , Proposition 2 identifies the unique optimal patroller strategy , permits every attacker delay, and gives
For general even , the statement that an optimum has is recorded separately. It is needed to support the delay-uniqueness clause, while the paper illustrates this interior maximum numerically in Figure 2 rather than proving it as a numbered result.
The theorem reduces the strategic choices in this game: regardless of attack duration, delay two is an optimal response, and full reflection is compatible with an optimal patrol. The uniqueness clauses explain when alternatives are possible. With odd duration, the zero-holding random walk makes all delays equally good for the attacker. With duration two, a range of reflection probabilities below one remains optimal for the patroller. Those facts distinguish a recommendation that is optimal from one that is forced by the game.
The paper gives arguments for its numbered results, but this mission's Lean theorems are open statements awaiting machine-checked proofs. A completed development would provide a reusable finite-path model of conditional hitting probabilities and a formal game-theoretic treatment of the full delay set. The even-duration interior-maximizer milestone also calls for an analytic proof of a property that the preprint supports with plots. The finite-path and generic saddle-point definitions can be reused outside this particular star network.
The apparently direct comparison of attack delays fails because the patroller's state at attack start depends on surviving the entire waiting period without a return to . The conditional distribution at that start time changes with . Likewise, increasing reflection probability can change both the trajectory and the event on which the payoff is conditioned. A comparison of one-step transition probabilities alone does not establish a comparison of . Exact uniqueness is more delicate still: at the chain alternates between centre and end nodes, creating genuine ties between delays for odd durations. The even-duration argument needs an optimum away from this boundary.
Lean represents the original star as Option (Fin n), with none denoting and some i denoting end node . It builds finite-step taboo path probabilities and defines by the ratio above, rather than by a closed-form solution or by the three-state reduction. The two-player saddle predicate is a separate generic definition; the paper-specific model supplies its strategy types and payoff. The definitions use real probabilities. The conditions , , , , , and are explicit. They make the relevant conditioning event nonempty and ensure the natural-number indices and mean the intended periods.
Lemmas 1–2 count the attack start as and count interception by ; the model instead uses at departure and later transitions from the attack-start state. Lemma 3's printed claim that odd makes delay two uniquely optimal conflicts with Proposition 2 at . The milestone states a corrected strict claim under , for all , and records the discrepancy. Contributions to the model's finite-path identities, the three-state symmetry reduction, the numbered lemmas, the case propositions, and the even-duration interior maximum are all within scope.
Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.
Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.
Timeline:
Let be a finite set of actions. A discrete sequence is a tuple with and every ; for it is the empty sequence . Its length is , and denotes the set of all discrete sequences. The concatenation lists the elements of followed by those of . For the refinement is its prefix of length , with .
A sequence is dominated by , written , if can be obtained from by removing some of its elements while keeping the order of the remaining ones. Thus but .
A discrete sequence function is any . The marginal value of appending after is
The function is sequence-non-decreasing if whenever , and (display (10)). It is sequence-submodular if
(display (11)): appending the same sequence gains less after a longer history. Assumption 2 requires both properties.
The optimization problem (12) is, for a length budget ,
For , a sequence is -greedy if at every step its choice is within a factor of the best single-action marginal value (display (13)):
Under Assumption 2, for every , every -greedy of length and every sequence with ,
Applied to the optimum of (12), this is the paper's display (14), .
For sets, the bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.
Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.
The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is , and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of produces a factor , while the recursion needs the uniform factor ; the replacement relies on feasibility together with nonnegativity of , which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases , and that the printed argument passes over.
All declarations live in the namespace SeqSubmod.Discrete.
List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and is A.length.List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.marginal u B A := u (A ++ B) - u A is , with the arguments in the paper's order.H[i] is the paper's and H.take i is . The maximum over is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped , or an existentially quantified would each change the theorem, and none is used.
A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality , which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.
A defined benefit pension promises payments whose form depends on a member's employment and retirement status at death, and on the existence and later survival of a qualifying dependent. The same member can generate very different death benefits while employed, after leaving with preserved rights, or after retirement. A scheme may specify a salary-related lump sum before exit, a revalued preserved-rights benefit in deferment, a spouse's continuing pension after death, and instalments under a fixed pension guarantee. Coordination rules determine which payments coincide.
This mission formalises a finite-horizon actuarial contract in which the payable cash amounts and their dates follow explicit benefit switches, rather than being inferred from names such as “spouse's pension” or “death benefit”. The pension and multiple-state foundations are described by Dickson, Hardy and Waters (2020), Chapters 8–11, https://doi.org/10.1017/9781108784184. The contractual rules here are independently defined examples.
Scheme rules and governing documents determine legal entitlement and tax treatment. No salary multiple, spouse percentage, contribution refund or guarantee is universal.
Time is measured in integer anniversary ticks, numbered from valuation time zero. Let be a finite mortality horizon, the employment exit tick and the pension commencement tick. The coherent contract satisfies . A member death-year index means death occurs during and a death-related lump sum is paid at tick . The terminal index denotes no death within the observable horizon. A dependent's corresponding death index is , with the same convention. A same-tick death is treated as non-qualifying; within-year ordering needs a finer model.
The joint mortality law has masses summing to one. At member death , is the probability of a qualifying spouse, conditionally independent of the hypothetical dependent death index given . A spouse qualifies only when , then receives payments while . Eligibility is fixed at death; later mortality is checked at each due date.
An active death has , a deferred death has , and a retired death has . Define benefit amounts , and at settlement for these disjoint regimes. The active benefit can include an optional salary multiple, an accrued-service amount and a contractual refund. The deferred death lump uses preserved annual pension multiplied by revaluation and an explicit pension-to-capital factor measured in years; any contribution refund is a separate cash amount. The retired benefit is a distinct lump-sum rider if the scheme provides one. No component is automatically cumulative with another merely because both appear in the model.
Let be the original member pension payable at anniversary , conditional on the member surviving that date. Let , and be survivor pensions fixed from the death regime, with survivor indexation multiplier . The amounts can reflect salary or service to death, preserved rights, or a fraction of a retirement pension. The main survivor contract pays for ; a separate immediate alternative allows . Amounts are per instalment, with consistent monthly units when required.
A retirement guarantee of ticks covers pension due dates . After a retired member dies, remaining guaranteed member instalments continue to the contractual recipient. Under the parallel rule the surviving spouse also receives its separately payable pension. Under the replacement rule the survivor pension is suppressed while the guarantee remains payable, then resumes when eligible after its expiry. A separate commutation switch can replace all unpaid estate-guaranteed instalments with one lump sum at death settlement, priced using consistent forward discount factors. No guarantee or payment alternative is universal.
Existing joint-life mathematics provides basic survivor occupancy identities. This mission extends them to the three death regimes. For and :
The indicators are pairwise disjoint, preventing multiple death-regime claims.
The second family constructs the realised present value for a full benefit contract from the paid lump sum and the dated instalments. Write for the discount factor to time zero and for the sum of original member pension, qualifying survivor instalment and remaining guaranteed payment under replacement switch . Then
The death lump is zero for the censored member state. The instalment horizon obeys in the root: right-censored members and spouses remain alive at every priced tick. Extension beyond needs a new mortality model.
The principal target establishes an equality between mortality-event valuation and the payment-date component EPVs, together with a second equality accounting for guarantee coordination. With for expectation over the actual member and dependent death cells, for the separately priced death, member, spouse and guarantee payment streams, and for the qualifying retiree-survivor pension suppressed during the guarantee:
The overlap is separately priced using , survivor mortality, death regime and payment eligibility. It is not introduced as a residual defined by subtracting two values.
The event-based formulation follows member status and the amount payable at death. The payment-date formulation uses explicit mortality conditions at each cashflow date, as in the valuation models of Dickson, Hardy and Waters (2020), Chapter 11, https://doi.org/10.1017/9781108784184. Agreement provides an auditable reconciliation between those independently constructed views. Where the spouse receives income while guaranteed member payments continue to an estate, valuing the two promises separately is appropriate. Where a contract suppresses that survivor pension, the overlap term quantifies the adjustment required to prevent charging for both.
Supporting targets cover exit, retirement and guarantee endpoints, and frozen survivor entitlement. Further results mix dependent-age mortality scenarios and value child pensions with an explicit cessation age.
A death benefit calculated from salary or preserved rights at a member's death differs from a pension instalment conditional on living at a subsequent payment date. Moving from a double sum over member and dependent death times to a sum over payment dates must respect that distinction. In particular, multiplying an unconditional probability of marriage at every later instalment would introduce a new eligibility test absent from the contract. The overlap between an estate guarantee and a spouse pension creates a second risk of overvaluation when the intended rule replaces one stream with the other.
Boundary cases are sensitive to strict and weak inequalities. A guarantee ending at has no payment at that endpoint under the due-in-advance anniversary convention adopted here. Same-grid member and dependent death is not automatically resolved by a continuous-time assumption. The project therefore has to distinguish mathematical cashflow identities, genuine survival-law properties and scheme-specific premises throughout its theorem graph.
Lean 4 represents joint death-year cell masses and real-valued finite sums with targeted Mathlib imports. It supports arbitrary dependent-life mortality associations and user-supplied discount factors, salary schedules, preserved rights, revaluation multipliers and survivor indexation. Salary multiples, contribution refunds, deferred benefit valuations and retirement lump sums are switches or amounts supplied by a contract. The retirement guarantee has zero, parallel and replacement regimes. Payment streams may be represented on a finer integer grid to accommodate monthly schedules, but no mathematical identity in the annual kernel asserts exact continuous-payment equivalence.
The principal theorem assumes a normalised joint mortality law, , and . The event-to-payment equality follows from explicit realised payments, not a vacuous equality hypothesis, independence assumption or constant-rate restriction. It relies on genuine death-year and survivor eligibility indicators, rather than stipulating valuation equality in the hypotheses. Continuous-time integration and stochastic marital-history transitions remain future extensions. Finite spouse age-difference mixtures and age-limited child payments are included as separate supporting results. Statutory GMP/excess floors and pension tax rules are outside the contractual core until a scheme type and applicable legal basis are separately verified.
We develop a theory of exact transmission of finite-dimensional -algebras through quantum channels. These algebras describe hybrid classical-quantum information, allowing the dimension of the quantum system to depend on the classical message. Allowing arbitrary encodings and decodings yields a transmission set of algebra types, ordered by embedding, that unifies zero-error information theory with operator-algebraic error correction. We ask if this set admits a dominating algebra into which every transmittable algebra embeds. Our central finding is that domination can fail even in small dimensions. In its absence, several incomparable maximal algebras can describe different optimal uses of the same channel, forcing the user to select one depending on the operational task and the type of information to be preserved. We introduce hybrid capacities that reconstruct the only possible dominating algebra type and present a complete finite characterization of domination using minimal forbidden algebra types. We identify dominating algebras for channels whose operator systems are graph-isomorphic to -algebras, including highly divisible channels, and for channels with zero one-shot zero-error quantum capacity. Under tensor products, we prove that joint coding can produce new algebra types, giving an algebraic analogue of superadditivity from Shannon theory. Domination can fail for the joint use of two channels, even when both channels separately admit dominating algebras. Finally, we construct a channel whose -fold tensor powers have doubly exponentially many maximal algebra types, attaining the largest possible growth scaling for finite-dimensional channels. Consequently, new transmittable algebra types appear at arbitrarily large block-lengths for this channel, so its full transmission structure cannot be generated from any finite collection of bounded-block-length codes. △ Less
This mission is the statement-level formalization of Transmitting algebras through quantum channels (arXiv:2609.40054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main nonexistence result; Example 4.2 and (4.3) (Main nonexistence result; Example 4.2 and (4.3), PDF p. 30). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Firms that already buy a service from an incumbent supplier regularly re-source the contract: they invite new suppliers, the entrants, to compete in a descending open-bid auction. Entrants may be cheaper but are unproven: before the contract can be awarded to an entrant, the buyer must pay for qualification screening (visits to the supplier's facility, purchasing and testing sample products), and an entrant passes only with some probability. Industry practice splits into screening every entrant before the auction (pre-qualification) and screening only the winner after it (post-qualification). Zhang, Chen and Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6), 2021, compare the two formats in equilibrium.
In the post-qualification format (POST), the incumbent needs no screening, so he faces a genuine dynamic decision: as the clock price falls and entrants drop out, when should he quit? His drop-out price determines the buyer's procurement cost in POST, and Theorem 2 of the paper characterizes it completely. This mission formalizes that theorem.
Costs lie in an interval . The incumbent's cost is . There are entrants with i.i.d. costs of density and c.d.f. , supported on . Screening one entrant costs the buyer , and an entrant passes with probability . In POST, the clock descends from ; when the incumbent drops out at price , the price jumps down by the decrement , and the incumbent ends up with the contract at price only if all remaining entrants fail screening. The paper assumes and Assumption 1: is nondecreasing and convex.
Before the incumbent quits, an entrant with cost stays until the price reaches his effective cost . With entrants left at price , the highest remaining entrant cost therefore has c.d.f. and density . Writing , the incumbent's value solves the Bellman system (8)–(10):
Here is the planned drop-out price. The integral covers the event that an entrant drops out first, at price ; the second term covers the event that the incumbent quits at and all entrants then fail screening.
Theorem 2 introduces four objects. is the floor of the minimum over of . The compete threshold is the first price at which falls below . The switching price is the least price above at which quitting is worth as much as competing down to . The candidate drop-out rule is .
For all , and :
and . The goal also asserts that are well defined and satisfy . It asserts the monotonicity of part (i): and are nondecreasing in , is nonincreasing in , and is nonincreasing in and nondecreasing in . Finally, is nondecreasing in and and nonincreasing in .
The proof in the e-companion (pp. ec5–ec11) provides the milestones, in attack order:
The theorem turns an infinite-horizon-looking stopping problem into a compete-or-fold rule. Either the incumbent stays in until the price falls to the threshold , or he drops out immediately. The choice depends only on how many entrants remain and on whether the price is above the curve . With Lemma 2 and Theorem 1 (the entrants' strategies), this completes the equilibrium of POST. The paper's comparison of POST and pre-qualification, and its closed form for the buyer's expected cost, both rest on this equilibrium.
The result is proved in the paper; it has not been machine-checked. A formal proof would check a long argument with an intricate induction: Lemma EC.2 interleaves the strict monotonicity of with the monotonicity of in and . It would also check the treatment of the boundary case , where the proof appeals to the convexity in Assumption 1.
The obvious argument differentiates in and reads off the sign. That fails because the derivative involves , which is itself the value of an optimization. Its sign is controlled by the explicit function only after an induction on shows that has the form wherever it matters. The induction must carry the ordering of , and across different and (Claim EC.1) at the same time. Another difficulty is that must be evaluated beyond the current price: is defined at the reference price and may exceed .
All prices and costs are real numbers, and is a natural number with . The standing assumptions (including Assumption 1) are hypotheses of every statement. One hypothesis is added to the page: is positive and continuous on . The page's own formulas divide by and differentiate (9) in . is defined as , not taken as a parameter, and is the integral of .
The max in (8) is a real supremum over the compact feasible interval; that it is attained is part of the goal. The integral in (9) is a signed interval integral, so is given by (9) for as well. The minimum defining is read as an infimum over , because the ratio has a zero denominator at . The page's is taken over the reals. "Optimal drop-out price" means a maximizer in (8): at two maximizers exist, so uniqueness would be false. The derivative (EC.7) is stated away from the kink . Milestones use the open price domain the proof uses.
The game-theoretic layer is not modelled. The hypothesis "entrants follow Lemma 2 and Theorem 1" is how the page derives (8)–(10), and the statement is about (8)–(10). A formalization that states only the sign pattern of or the inductive hypothesis would be trivializing; the goal states optimality of in (8) for every , , , together with part (i).
A development needs differentiation under a parametrized integral (the fundamental theorem of calculus for ), continuity of in , and real-analysis facts about convex functions crossing a line. These are reusable for other auction and optimal-stopping models. Proofs of any milestone are welcome, as are proofs of the fold-only case independently of the compete case.
Restaurants, clinics and amusement venues that announce a waiting-time standard compete not only on price but on how unpleasant the wait feels. Waiting-area entertainment (a piano player, a television, a play area) lowers the perceived cost of waiting, and when several providers sit in one service cluster, a food court, a mall, a strip of restaurants, a single entertainment option can serve all of their customers at once. Yuan, Dai, Chen and Gavirneni (MSOM 2021) model this choice and ask when providers that compete on price but jointly fund entertainment, a form of co-opetition, do better than a single provider serving the market alone.
The model builds on the waiting-time-standard and volume-based capacity framework of Allon and Federgruen (Operations Research 2007) and on linear cost-allocation schemes of the yardstick type. Its central comparison concerns the even cost split: does sharing the entertainment bill outweigh the margin lost to price competition?
Customers arrive at a provider as a Poisson stream and the service time is exponential. With service fee and entertainment level , a local monopolist faces the arrival rate
where is the maximum demand rate, the price sensitivity, the waiting cost per unit time, the announced waiting-time standard and the effectiveness of entertainment. Entertainment costs with . To keep the expected wait at the provider buys service rate at marginal cost , so its profit is
The monopoly profit is the greatest value of over , .
Under co-opetition two symmetric providers share one entertainment level. Write , , margins , a price-competition intensity and . Provider 's arrival rate is . The cost is split by with cost-sharing factor , and provider earns
Providers first set margins simultaneously; then they jointly choose to maximize . A symmetric equilibrium has , jointly optimal at , and no deviation , followed by the joint optimum it induces, raises a provider's profit. The equilibrium profit is . Throughout, the parameters satisfy and .
With an even split () there is a threshold such that, for every and every symmetric equilibrium at ,
No value of is fixed: the goal asserts only the threshold shape of the comparison.
and . 2. Proposition 3(i) at . A symmetric equilibrium exists, and every one satisfies
The result separates two effects of clustering. Sharing one entertainment option halves each provider's cost, which supports a higher entertainment level and more demand; price competition erodes margins. Proposition 7(ii) says that, under an even split, the comparison with a local monopolist is decided by a single cut-off in the competition intensity, which is what lets the paper conclude that co-opetition can restore monopoly profit levels when competition is mild, and it is the reference point for the paper's analysis of unequal cost-sharing rules (Propositions 6 and 8) and of the design of cost allocation.
The paper's proofs sit in an online supplement; no machine-checked proof of any of these statements is known. Formalizing them produces a verified analysis of a two-stage game with a joint second stage, including the existence of the symmetric equilibrium, which the paper uses but which requires a global, not first-order, argument.
The co-opetition equilibrium is defined by a two-stage game: a price deviation changes the jointly chosen entertainment level, so a provider's payoff as a function of its own price is a composition with an argmax and need not be concave. Verifying that the first-order point of Proposition 3 is a global best response, and that every symmetric equilibrium satisfies the first-order conditions, is the step a direct first-order computation does not deliver. The threshold of Proposition 7(ii) then requires comparing an implicitly defined equilibrium profit, through its root equation in , with the implicitly defined monopoly optimum, and showing that the difference changes sign exactly once in ; monotonicity of alone does not give a sign change.
Everything is real-valued. Prices are encoded by margins , for the equilibrium and for every deviation, matching the page's domain . The joint entertainment stage maximizes over , and a deviation is evaluated at every joint optimum it induces. is any greatest element of the set of monopoly profits over , . The goal and milestones fix ; Proposition 3 for is out of scope.
Disclosed conventions: the capacity bound is the strict instead of the page's (at equality a degenerate profile with zero margins and no entertainment makes both profits equal to and falsifies the strict clause); the demand is read as , as in §3 and Proposition 3(ii), since the §4 display double-counts ; the cost share is read as , the first of the page's two inconsistent forms (they agree at ); "decrease" is strict; "the opposite holds" is the strict .
The goal is stated about genuine equilibria of the game and the genuine monopoly optimum. Replacing by the closed form of Proposition 3, or by the formula of Proposition 1, would turn the goal into a one-variable real-analysis fact and is not the paper's statement.
A complete development needs: the monopoly first-order analysis (joint concavity on , ); strict concavity of the joint second stage for positive total margin; the envelope argument for a provider's deviation; existence of a symmetric equilibrium; implicit-function comparative statics in . Lemmas on implicitly defined roots of type equations are reusable. Contributions of intermediate lemmas, including the existence of the equilibrium, are welcome.
Many financial assets (corporate and municipal bonds, swaps, asset-backed securities) trade over the counter (OTC): there is no central exchange, and a trade requires that a buyer and a seller find each other. Empirically, a large share of OTC volume passes through intermediation chains, in which an asset moves from the original seller to the final buyer through several dealers. Search-theoretic models explain how such chains form. Duffie, Gârleanu and Pedersen (2005) introduced continuous-time search and bargaining in OTC markets, and Hugonnier, Lester and Weill (2016) let investors' valuations take a continuum of values, so that dealers emerge endogenously as the investors with intermediate valuations.
Shen, Wei and Yan add a search cost: an investor who looks for a trading partner pays a flow cost . Investors with extreme valuations then prefer to stay out of the market, and participation becomes an equilibrium choice. The paper's Theorem 1 is the foundation of everything that follows in it: every proposition on chain length, trading volume, price dispersion and welfare is stated "in the equilibrium of Theorem 1".
Time is continuous. A continuum of investors of total mass trades an asset in supply , with ; each investor holds or unit, and the asset pays a coupon of per unit of time. An investor of type values the coupon at . Types are redrawn independently at intensity from a probability density on with c.d.f. . Everyone discounts at rate .
A non-owner either stays out or searches to buy; an owner either stays out or searches to sell. Searching costs per unit of time. Write for the densities over types of buyers, sellers, inactive non-owners and inactive holders, and , . A buyer meets sellers at rate and a seller meets buyers at rate , with .
Let be the values of the four activities, and . When a type- buyer meets a type- seller, the surplus is
they trade iff , and the buyer, with bargaining power , pays .
For cutoffs , , non-owners search to buy iff and owners search to sell iff . A steady-state intermediation equilibrium (Definition 1) consists of cutoffs , densities satisfying the flow balances (12)–(18) and market clearing (19), and value functions solving the Bellman system (8)–(11) under which these cutoff rules are optimal. Types in are the intermediaries: they search to buy when they hold nothing and search to sell as soon as they hold the asset.
There is an explicit threshold , built from the right-hand sides of the cutoff equations
with , the explicit functions (66), (64) of , , such that for
a steady-state intermediation equilibrium exists, and every such equilibrium has cutoffs equal to the unique roots of (20) and (21), densities (55)–(63), value functions (79)–(82), and the trade rule "trade iff " with prices (6).
The milestones follow the paper's proof. Step I solves the flow equations for given cutoffs: (55)–(57), (61)–(63), the populations (64) and (65)–(66), and the densities between the cutoffs (58)–(60), together with the existence of the steady state. Step II derives the slopes (77)–(78), the value functions (79)–(82), the trade rule (83)/(7), the cutoff equations (20), (21) with their unique roots, and the threshold (84). Step III shows that the cutoff rules are optimal for the closed-form values.
Theorem 1 gives a closed-form description of an OTC market with endogenous participation and an endogenous dealer sector. The search cost splits the population into three groups (passive low types, intermediaries, passive high types), and the length of intermediation chains, trading volumes and price dispersion are all computed from the explicit densities and value functions. Every comparative-statics result of the paper (for example, that a lower search cost lengthens chains) is a statement about the equilibrium this theorem constructs.
The result is proved in the paper, with gaps: the verification of the trade rule outside the dealer region is called "straightforward", Step III treats one of four cases, and uniqueness of the solution of the Bellman system is not argued. No part of it is machine-checked. The mission asks for a complete formal proof, and its definitions give a reusable Lean model of a continuous-time search-and-bargaining steady state with endogenous participation, which no existing formalization provides.
Step I is not just algebra. Between the cutoffs, the flow equation (18) couples each density with integrals of the others, and its solution comes from a Riccati-type equation for . As printed, the densities (59)–(60) do not solve it. Step II differentiates parametric integrals of the positive part of the surplus, which needs the monotonicity of before that monotonicity is proved. That uniqueness is the main gap: the paper takes it for granted. Monotonicity of the right-hand sides of (20)–(21) in the cutoff rests on decreasing and increasing, which is asserted, not shown. The obvious approach, plugging the closed forms into Definition 1, gives only existence; uniqueness requires showing that every solution of the flow equations and of the Bellman system is the closed-form one.
All quantities are real numbers; is written lam and is Δbar. The standing assumptions are , , , , and a probability density on (nonnegative, integrable, total mass ); and . The densities are required to be nonnegative and integrable, and the value functions bounded and measurable on , so that no integral takes Lean's default value .
The equilibrium predicate is Definition 1 itself: flow equations (12)–(19), Bellman system (8)–(11) multiplied through by , and optimality of the cutoff rules ( below , above, and likewise for owners). The closed forms are separate definitions, and is defined from (20)–(21) as the common value of their right-hand sides at the crossing point; it is never a parameter. A formalization that defined the equilibrium by its closed form, or took as a hypothesis, would make the goal trivial and is excluded.
Corrections and conventions, all disclosed in the items:
The definitions are split into a model module (parameters, steady state, Bellman system, optimality, equilibrium, prices) and a closed-form module (, , the cutoff equations, , densities, slopes, value functions). The model module is reusable for the paper's later results (trading volumes, chain length, comparative statics in , , , ) and for the non-intermediation equilibrium of its Theorem 2. Proofs of individual milestones, and lemmas on the monotonicity of , and of the cutoff equations, are welcome as separate contributions.