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?
The minimum bisection problem partitions an even-sized graph into two equally large groups while cutting as few edges as possible. In community detection, a graph may have been generated around an unknown, balanced pair of groups. The statistical question is whether an optimizer can identify that planted partition from the edges. Before studying random graph models or relaxations, it is useful to know which properties of a single observed graph suffice for recovery and whether those properties can be weakened.
Del Pia, Khajavirad and Kunisky express a deterministic sufficient condition through two vertex-degree parameters. Their Theorem 1 says that minimum bisection recovers the planted partition when the smallest within-community degree exceeds the largest cross-community degree by more than . Theorem 2 supplies graphs at or below that boundary where recovery fails. Thus the degree difference has a sharp worst-case boundary within the theorem's stated size and degree ranges. This mission formalizes that second, tightness result.
Let be a simple undirected graph with vertices. A bisection is a partition of with . Its cut cost is the number of edges with one endpoint in each side. The planted bisection is a designated partition regarded as the answer the optimizer should recover. Since exchanging and leaves the partition unchanged, uniqueness is always understood up to this exchange.
For each vertex , count its neighbors on its own side of the planted bisection and its neighbors on the opposite side. Write and for these counts. The two parameters of the planted graph are
Minimum bisection recovers the planted partition if every bisection with cost at most that of the planted one is the planted partition, up to swapping its sides. This formulation requires both optimality and uniqueness. If the planted bisection costs more than a competitor, recovery fails; it also fails when a distinct bisection ties it. These definitions follow §2 of the pinned preprint.
Lemma 1 supplies two finite-graph existence statements. For positive even , a simple -regular bipartite graph exists on vertices with vertices per side whenever . For the same , a simple -regular graph exists whenever . The bipartite part includes the edgeless graph at and the complete bipartite graph at . The second part includes the edgeless and complete graphs at its own endpoints.
The mission's goal is Theorem 2. For every positive multiple of eight and every pair of nonnegative integers satisfying
there exist a graph on vertices and a planted bisection with those exact parameters for which minimum bisection does not recover the planted partition. The inequalities delimit the claimed family; the goal does not assert failure for every graph with those degrees. The word “exact” matters because a construction with merely smaller within-side degrees or larger cross-side degrees would not establish tightness for the requested parameter pair.
Together with the paper's Theorem 1, the goal locates the worst-case threshold for recovery by minimum bisection: a strictly larger degree difference guarantees recovery, while every admissible parameter pair at or below the boundary occurs in a counterexample. This separates a guarantee about all graphs with given degree extrema from a claim about a particular graph. It also gives a deterministic baseline for comparing the behavior of the paper's linear programming relaxation and stochastic block model, whose recovery guarantees concern different optimization procedures and graph distributions.
The theorem is proved in the cited paper; the task here is to state its graph model, parameter extrema, and recovery conclusion in Lean with the same quantifiers and boundary cases, then obtain a machine-checked proof. The regular-graph existence lemma is independently reusable for other finite graph constructions. The definition layer can also support later exact-recovery statements for the same paper after the series' graph conventions are consolidated.
A strict threshold being sufficient does not itself show that it is necessary. At equality, an inequality used in a recovery guarantee no longer forces a unique optimum, but that leaves open whether a graph with the prescribed degree extrema actually has a competing bisection. Every requested pair must be realized by a genuine simple graph, including the degree endpoints, and the competing partition must be balanced and distinct even after sides are exchanged. The proof therefore needs graph existence and degree bookkeeping as well as a comparison of cut costs. The page states one numbered supporting lemma, Lemma 1; its two clauses are the mission's milestone.
Vertices are represented by Fin n, indexed from zero rather than the paper's . A side of a bisection is a Finset; its complement represents the other side. Graphs are Mathlib SimpleGraph values, and cut cost counts each undirected crossing edge once by ordering its endpoints. The within and across degrees are filtered neighbor counts. Their minimum and maximum range over all vertices, matching the paper. An empty vertex type receives a conventional zero degree extremum, while Theorem 2 requires .
The bounds involving and are compared in the reals, so natural-number subtraction cannot truncate a negative difference. The hypothesis makes an integer in the theorem's actual domain. Lemma 1 uses positive even , with Mathlib's regular-degree predicate and a bisection set witnessing equal bipartition sizes. Its bound is safe in natural numbers because .
The formal goal requires a witness graph whose minimum within-side degree equals the requested and whose maximum across-side degree equals the requested . It also requires an actual planted bisection and failure of uniqueness up to complement. Replacing either equality with a loose degree bound, or allowing a non-bisection witness, would make the claim easier and lose the paper's result. Contributions toward finite regular graph constructions, exact degree calculations, and cut-cost comparisons are within scope.
Value iteration (VI) is the standard method for computing the optimal value function of a discounted Markov decision process (MDP). It applies the Bellman operator repeatedly, and because that operator is a -contraction in the sup norm, the error after steps is at most times the initial error. When the discount factor is close to , as in long-horizon planning, this rate is slow.
Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read value iteration as a gradient-type method and transfer momentum schemes from convex optimization (Nesterov acceleration, heavy-ball momentum) to the Bellman operator. On reversible policy chains these accelerated schemes provably converge faster than VI. On general MDPs, however, the accelerated iterates need not converge at all: the paper exhibits instances on which Accelerated Value Iteration (A-VI) oscillates or diverges. Section 7 of the paper resolves this tension with Safe Accelerated Value Iteration (S-AVI, Algorithm 1), which tries an accelerated step at every period and keeps it only when it makes enough progress on the Bellman equation . This mission formalizes the convergence guarantee of S-AVI, Theorem 7.1.
Let be a finite set of states and a nonempty finite set of actions. A discounted MDP is given by a transition kernel , with the probability of moving from state to state under action and ; a reward for each state-action pair; and a discount factor . The Bellman operator is
The sup norm is . The optimal value function is the unique fixed point of . For a vector , the quantity is its Bellman residual.
S-AVI (Algorithm 1) takes a scalar , step sizes and any starting vector . It sets , and at each period forms
If , the accelerated candidate is accepted, ; otherwise the algorithm takes a value-iteration step, . In the Lean development the MDP is AccelVI.SafeAVI.MDP with validity predicate MDP.Valid, the operator is bellman M, and the iterates are savi M lam' α γ v0 : ℕ → (S → ℝ).
For a valid MDP, any , any and any , the S-AVI iterates converge to , and
that is, there is a constant with for every . The constant is left unspecified, as in the paper.
The result. Theorem 7.1 says that the safeguard costs nothing in the worst case: S-AVI converges on every MDP at rate , and with it matches the rate of value iteration, which Theorem 6.3 of the same paper shows cannot be beaten by any first-order method uniformly over MDPs. At the same time it accepts accelerated steps whenever they reduce the residual fast enough, so it keeps the empirical speed-ups of A-VI. Remark 7.2 of the paper describes the role of : values closer to admit more accelerated steps. The guarantee also gives a computable stopping rule, since the residual bounds the distance to .
Formalizing it. The result is proved in the paper; to our knowledge it has not been machine-checked. This mission produces a Lean statement of the finite discounted MDP layer, the Bellman operator and Algorithm 1 itself (including its two-step recursion and its data-dependent branch), and a formal proof that the safeguarded iteration converges. The contraction property of and the residual-to-error bound are reusable for any later value-iteration development on the platform. Three sibling missions of this series pose the paper's other main results: the rate of Accelerated Value Computation on reversible chains (Theorem 5.1), the rate of Momentum Value Computation (Theorem 5.5), and the first-order lower bound (Theorem 6.3).
The accelerated candidate is built from two past iterates through a momentum step, and on a general MDP nothing controls it: A-VI is not a descent method, and its iterates may diverge. The natural first attempt, proving that A-VI steps contract the error, therefore fails. The difficulty in the formal setting lies elsewhere: the iterates are defined by a two-step recursion with a branch on a real inequality, so any argument must handle both branches at every period and keep the paper's indexing straight (the threshold at period is and it compares with the residual of , not of ). Existence and uniqueness of and the contraction property of a max of affine maps also need to be established for the specific operator, from the stochasticity of .
States and actions are finite types, [Fintype S], [Fintype A], and [Nonempty A] so that the maximum in exists. Vectors are functions S → ℝ with Mathlib's sup norm, which is . Rewards are arbitrary reals. The discount factor is M.lam with inside MDP.Valid; the initial distribution of the paper's tuple is omitted because no statement uses it. The optimal value function enters each statement as a vector vstar with bellman M vstar = vstar; this is not vacuous, since a valid MDP has exactly one such vector. The scalar ranges over the closed interval , and as in Algorithm 1, although the convergence argument does not need the step sizes to be positive. The sequence savi is indexed as the paper's : its recursive case s + 2 is the paper's period , with threshold lam' ^ (s + 2). " for all " is encoded as a single constant valid for every , which is stronger than an eventual big-O.
A formalization that replaced the test by the per-step condition (7.2) of Remark 7.3, used the residual of instead of , fell back to , or allowed would be a different theorem; none of these is posed. Remark 7.4's extension to arbitrary contractions is not posed either.
The development needs the contraction property of , the Banach fixed-point bound relating error and residual, and an induction over the iterates. Proofs of the milestones as separate lemmas are welcome, as are general statements about safeguarded fixed-point iterations for -contractions that specialize to this one.
When a contract breach propagates along a supply chain, one failure triggers the next: a supplier delivers late, the manufacturer misses its own delivery, the distributor misses its, and so on. Each link suffers a loss caused by its predecessor, and the question is who should be liable for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) study this as an axiomatic cost-sharing problem, with the aim of rules simple enough to be executed automatically by a smart contract.
Their first main result characterizes a one-parameter family, the fixed-fraction rules , , by four axioms. The axioms do not single out a member of the family. Section 4 of the paper gives two normative arguments for the midpoint . This mission formalizes the first of them, Theorem 2: for loss chains with equal losses, is the allocation at equal Euclidean distance from every agent's "ideal" allocation. The construction follows the tradition of ideal points in bankruptcy, taxation and bargaining (Yu 1973; Chun 1988), with one ideal allocation per agent instead of a single ideal point.
There are agents in a chain. Agent causes a loss to agent ; a loss problem is , with total loss .
An allocation of is a vector of liabilities with , with for (no initial segment of the chain pays less than the losses it caused), and with . The set of allocations is , and the ordered allocations are .
The fixed-fraction rule with parameter (Definition 1) is
Each agent pays the fraction of the loss it caused directly, and the initiator also pays the residual .
For the ideal allocation charges the first agents equally and the rest nothing:
When , is the allocation agent 2 would prefer among the ordered allocations, is the one agent would prefer, and is agent 1's. Distances are Euclidean: .
For every and with ,
Theorem 2 is one of the two arguments the paper gives for recommending among the fixed-fraction rules; the other is that is the Shapley value and the nucleolus of the associated liability game (Theorem 3, a separate mission of this series). The uniqueness companion turns the theorem into a selection principle: equalizing distances to ideal allocations determines the allocation completely. The paper also remarks that the same principle, applied to the elementary problems with unit-vector ideal allocations, selects the serial rule, which shows that the choice of ideal allocations drives the result.
The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. The mission produces a formal model of loss chains, allocations and fixed-fraction rules on which the other missions of the series also build, and a checked version of the paper's computation, including the boundary cases (, ) that the printed proof passes over.
The theorem is a computation, and the obstacles are the ones a careful formalization has to face rather than conceptual ones. The squared distance to splits into a part common to all and a part linear in the prefix sum , and the printed argument passes between the two forms by dividing by , which is not allowed for the zero problem. The uniqueness statement must also hold at , where every ideal allocation is the zero vector and the prefix characterization breaks down. Prefix sums over must be matched exactly with the nonzero coordinates of ; an off-by-one in either produces a different family of points. Finally, the equal-loss hypothesis cannot be dropped: for , , at distance from and from .
Agents are indexed in Lean (the paper's agent is index ), vectors are functions Fin n → ℝ, and nonnegativity of a loss vector is the predicate IsLoss. The fixed-fraction rule is a function of , and ; is named lam. The ideal allocation ideal ℓ k is defined for every natural but is used only for ; every statement quantifies over exactly that range, because ideal ℓ 0 is the zero vector in Lean and is not one of the paper's points. Distances are Mathlib's distance on EuclideanSpace ℝ (Fin n); the sup distance on Fin n → ℝ is not used, and would not even be detected by the Figure 1 example, where the sup distances to are also all equal.
Disclosed additions and corrections:
A formalization that states the conclusion with the sup metric, that ranges over or , or that drops the equal-loss hypothesis does not formalize Theorem 2. Contributions of proofs of any item are welcome; milestone 1 is a finite-sum computation reusable for any distance-to-ideal-point argument in this setting.
Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor per step, so it needs on the order of iterations, which is slow when is close to , the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate of plain VI on every MDP? Theorem 6.3 of the paper answers no.
A finite MDP consists of a state set with , a finite nonempty action set , transition probabilities with , rewards , and a discount factor . Its Bellman operator is
a -contraction for the sup norm . Its unique fixed point is the optimal value function.
A sequence in is a first-order sequence for if
VI from () and relaxed VI () from produce such sequences.
The chain MDP of Figure 1 has states and a single action. State is absorbing with reward ; every state moves deterministically to and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.
For every , every , the fixed point of the Bellman operator of the -state chain, every first-order sequence for , and every ,
The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from to ; with , , the analogue for MDPs would be a rate of about , and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.
The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index . The support claim has to be carried through the nonlinear max in , which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of into a bound in sup norm with the exact constant , which requires the two-sided inequalities (3.5)–(3.6) for and the explicit value .
Fin n and are 0-based: the paper's state is index , so is lam ^ k / (1 - lam) at index and "" is . The action set of the chain is Unit.Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index inclusive.FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.
In many auctions a bidder's value for what is sold depends on information held by other bidders: the value of an oil-drilling lease depends on every bidder's geological survey, the value of a piece of art on what other experts know about its provenance. This is the interdependent values model of Milgrom and Weber (1982). With interdependent values the standard private-value tools fail: the Vickrey–Clarke–Groves (VCG) mechanism is no longer incentive compatible, exact efficiency in ex-post equilibrium requires a single-crossing condition, and with multidimensional signals maximizing welfare is generically impossible even in Bayes–Nash equilibrium (Jehiel and Moldovanu 2001). Without some structural condition on how values respond to others' information, even a single-item auction can force every truthful randomized mechanism to lose a factor of order (Example 1.3, after Eden et al. 2018), when values treat the signals as complements.
Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384, Mathematics of Operations Research 2024) identify such a condition, submodularity over signals (SOS), and show that under SOS simple randomized mechanisms recover a constant fraction of the optimal welfare in rich settings. This mission formalizes their result for combinatorial auctions with multidimensional signals and separable SOS valuations, where the mechanism is a random-sampling variant of VCG with explicit payments.
Timeline of the line of work:
There are agents and items; a bundle is a set . Each agent privately holds a signal for every bundle , and collects all agents' signals for . Agent 's value for bundle is , a known function of , weakly increasing in every signal and strictly increasing in ; the empty bundle is worth .
A function of the signal vector is SOS when raising a single coordinate helps at least as much at a coordinatewise lower profile of the other coordinates: for every coordinate , and profiles off ,
The valuations are separable SOS when
with (depending only on the other agents' signals for ) and weakly increasing and SOS.
An allocation gives agent the bundle , with the bundles pairwise disjoint. A deterministic mechanism maps reported signals to an allocation and payments. It is ex-post incentive compatible (IC) if, whatever the true signals, no agent gains by misreporting when the others report truthfully, where the agent's utility is her value at the true signals for the bundle she receives minus her payment; it is ex-post individually rational (IR) if the truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support is.
Random-Sampling VCG (RS-VCG) partitions the agents uniformly at random into and . For it sets the proxy weight
the value with the bundle- signals of the other members of replaced by . It allocates to a feasible allocation maximising , and a winner pays
where is the maximum proxy welfare of an allocation to .
For separable SOS valuations, RS-VCG is ex-post IC and IR for every partition, and for every true profile and every feasible allocation ,
The theorem shows that VCG-style reasoning survives interdependence when the dependence on other agents' information enters additively and submodularly: separability makes the payment absorb the effect of the others' signals, so that each agent of faces the proxy welfare as its objective. It gives a constant-factor welfare guarantee in ex-post equilibrium for combinatorial auctions with multidimensional interdependent signals, a setting in which exact efficiency is generically out of reach. The construction is the template for the paper's single-dimensional results in §6.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a reusable Lean model of interdependent-value combinatorial auctions (multidimensional signals, ex-post IC/IR, universal truthfulness of random mixtures) and of the SOS condition, and a checked account of the VCG accounting identity in this setting.
The approximation part rests on the Key Lemma 3.1: a uniformly random half of the other agents' signals set to zero keeps, in expectation, half of an SOS value. The obvious argument — monotonicity alone — gives no constant: with values depending on many signals, zeroing half of them can destroy almost all of the value, and the SOS condition is exactly what rules this out. The incentive part is where the obvious transfer of VCG fails: the proxy weight of agent is not its value, and the true value depends on signals that the proxy zeroes. Without separability, the payment of a VCG-style rule would itself depend on the agent's report (the paper's remark at the start of §5), and alignment of the agent's utility with the proxy objective breaks. Ties in the argmax and agents receiving the empty bundle must be handled for every tie-breaking rule.
Agents are Fin n and items Fin m, with arbitrary; bundles are Finset (Fin m). Signals are NNReal, one per (agent, bundle), and is a function of the bundle- signal vector. The empty bundle is worth ; monotonicity, strict own-signal monotonicity and the separable decomposition are assumed for nonempty bundles. The function is written on the whole vector with the hypothesis that it ignores coordinate . The decomposition is data of the mechanism, since the payments use .
The allocation is produced by an arbitrary selector returning a feasible maximiser of the proxy welfare for every partition and report; all statements hold for every such selector. is a maximum over the finite set of feasible allocations to . Agents of , and agents of that receive the empty bundle, pay (the paper defines payments for winners only). The expectation over the partition is the uniform average , never an existential or universal over ; the approximation is stated for every feasible comparator allocation, with welfare at true values under truthful reports, never for proxy welfare or through a supremum. IC and IR are stated for each partition with the paper's explicit payments, not with existentially chosen payments.
A complete development needs finite averages over subsets, the Key Lemma 3.1 for SOS functions (posed in the companion mission on RS-V and not restated here), and finite argmax reasoning; the SOS layer and the combinatorial mechanism model are reusable for the other missions of this series. Proofs of the milestones, and of the d-SOS variant mentioned after the proof (a -approximation, not posed here), are welcome.
The source is the arXiv preprint arXiv:1903.08384v2 (2 June 2019); all page and display numbers refer to it, not to the journal version in Mathematics of Operations Research (2024).
Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.
A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter , which measures how quickly a miner's operating cost grows with its scale, and the mining reward . The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.
There are active miners, indexed , with costs per hash (sorted, without loss of generality), a reward and a capacity parameter . Miner choosing hash rate earns , where is the aggregate hash rate (the paper's (3.4)). The cumulative cost is .
In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of , and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:
with and . Miner is active exactly when . The hash rate share of miner is .
The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For , (B.4) splits the derivative of into a direct part, with held fixed, and an indirect part through the aggregate, .
For every active miner ,
and the derivatives of with respect to and to are increasing in , for .
The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the and columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).
Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the and directions, the sign analysis, and the monotonicity in . The proof text on p. 43 says "decreasing in " where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).
Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity , i.e. , and the first-order identity . The sign of the indirect parts is not visible from the raw derivative: it requires rewriting so that the threshold appears. The positivity of needs a separate bound, since its indirect part can be negative. The monotonicity in is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on (decreasing in ) from that on (increasing in ), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.
Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner , so "increasing in " is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost (), gH ((4.1)/(B.3), with both branches of (4.1)), fH ( with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: , , , , costs sorted, and for every (all miners active). The condition is the paper's: (B.3) defines only for . The definition Sensitivities defines the four 's as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.
The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That and are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and are posed in mission 2. This mission uses those identities but does not pose them.
Trivializing formalizations are ruled out: the 's are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with , , give , ); and the monotonicity is stated for derivatives asserted to exist.
Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for (the root identity, positivity, ) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.
Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack . Approximate incentive compatibility (-IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.
Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With -IC the feasible set grows, and the paper determines the order of the additional revenue as .
Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an -IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only (Theorem 2), and give a matching lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.
A seller sells one item to one buyer. The buyer's value has a cumulative distribution function with density supported on , . Assumption 1 requires to have bounded variation on . Write , the revenue curve (the revenue of a posted price ), and .
A direct mechanism gives a buyer who reports the item with probability and charges . It is individually rational (IR) if for all , and -incentive compatible (IC) if
is the set of IR and IC mechanisms, the expected revenue, and . A best reporting mapping for picks, for each value , a report in .
Local -power envelopes (Definition 1): has a unique maximizer on , interior, and there are , and with and
The parameter measures how flat is at its peak; is the generic smooth case.
Perturbed delayed mechanisms (§5.1). For the buyer is steered to report , equal to below , to on , and to above. With its generalized inverse, the allocation solves on the ordinary and delay differential equations
is above , and the payment is given explicitly in terms of and .
Under Assumption 1 and local -power envelopes there are and such that for all some satisfies
The constants may depend on the distribution, but not on .
The result. Theorem 3 shows that the upper bound of Theorem 1 is tight up to the logarithm. Since for , the revenue gain from approximate incentive compatibility is supralinear in : a seller who exploits -optimizing buyers gains strictly more than the order- gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature of the revenue curve at the optimal price determines the exponent, which ranges from (as ) to (as ), the latter matching Nisan's universal bound.
Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of -IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on , which the paper derives from the renewal function of uniform interarrival times.
The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples to ); choosing the delay so that the allocation reaches exactly at , which requires the sharp two-sided bound on and an intermediate value argument; and verifying global -IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain against losses of order , with of order .
Values are reals, every function is a total function whose values matter only on , and the density is integrable on with total mass . Mechanisms are required to be measurable, which the expectation presumes. is a supremum (sSup); the goal is stated with an explicit witness , which is equivalent because the revenue image is nonempty and bounded above by . is defined as , not as a derivative. The constants are quantified after the distribution and before .
The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.
Disclosed additions relative to the page: in the §5.1 statements (presumed by the paper's definition of ); Propositions 3–6 and Lemma 5 are stated for any price with and , since their proofs never use optimality of ; in Proposition 6 the integrand is written in product form because divides by .
A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.
Fair division asks how to split a divisible resource among agents whose preferences differ. In the non-atomic ("cake-cutting") model the resource is a region of Euclidean space and an agent values each measurable piece. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research, 2023) study fair guarantees: utility levels that a division rule lets every agent secure for herself, whatever the other agents' preferences and behaviour. Two numbers bracket every such guarantee. Maxmin is an upper bound on any fair guarantee, and minMax is what Kuhn's Divide & Choose rule secures for arbitrary continuous preferences (Theorem 1 of the paper; a companion mission formalizes it).
For utilities that are monotone in the share (the manna is unanimously good), the authors ask whether rules of a different shape improve on minMax. They consider the classical Moving Knife rules, where a knife sweeps the manna and agents shout "stop", and introduce Bid & Choose rules, where a clock runs and the agent who stops it picks any share of a prescribed size. Each rule comes with a computable guarantee, for the knife and for Bid & Choose. The question this mission formalizes is where these guarantees sit relative to the two benchmarks.
The manna is a bounded measurable subset of , , with Lebesgue measure and . A share is a measurable . Shares are compared by the pseudo-metric . A utility is a bounded, -continuous function on shares with ; it lies in if implies .
An -partition of is a tuple of shares with union and pairwise null overlaps; it is an equipartition for if all are equal. The benchmarks are
over all -partitions .
A moving knife is a -continuous path of shares on from to with whenever . A benchmark measure is a probability measure on , mutually absolutely continuous with Lebesgue measure on . Write for the sequences , and
For the guarantees are
For , , every moving knife and every benchmark measure :
The paper also claims . That inequality is false and is not posed. Take , Lebesgue measure and . There is an increasing continuous , built from dyadic "spike" sets, for which while every 2-partition has a share worth about .
A further item records what the page's left-hand argument for does prove: for every .
The goal shows that, for a good manna, a Moving Knife rule is never worse than Divide & Choose by the minMax measure and never promises more than the Maxmin ceiling. Bid & Choose likewise never exceeds Maxmin. Since Maxmin profiles need not be feasible (the paper's Leontief example, p. 16), these inequalities locate the new guarantees inside the only interval where fair guarantees can live.
The mission also corrects the record. The paper is published, but its Lemma 4 and Theorem 2 iii) as printed in the arXiv v3 preprint are not right for . Lemma 4 i) asserts continuity of and Lemma 4 ii) the existence of an equalising -sequence, and both fail for some . The left-hand θ-inequality fails as well. The mission states only true claims and leaves precise statements on record. As far as we know none of these results has been machine-checked. The platform has no prior cake-cutting, moving-knife or equipartition development, so the definitions here are new.
The knife sandwich hinges on an equalising sequence. One must show that is jointly continuous and run an -step intermediate value argument whose optimality proof needs the two-sided monotonicity of . Proposition 1 ii) needs the trimming step. A share must be continuously shrunk inside while its utility is tracked, and then iterated across shares while all trimmed shares are kept equal. This is the longest argument in the mission.
For , the natural first idea is to copy the knife argument: prove continuous, then equalise. It fails, because is an inf–sup over the non-compact space of shares and can jump. The right-hand inequality has to hold for every without any attainment, and any argument for it requires shares of every prescribed -size, i.e. a non-atomicity (Sierpiński-type) argument for .
Space: EuclideanSpace ℝ (Fin d) with volume, and is assumed in every theorem, because in Lebesgue measure is a point mass, which the paper's non-atomic model excludes. Utilities are functions on all subsets, constrained on shares only. Partitions are Fin n-indexed, with union exactly and null pairwise overlaps (not disjointness). Every min/max of the paper is an inf/sup (sInf, sSup), as the paper itself says on p. 9. Each defining set is nonempty and bounded for , which every theorem assumes. Knife continuity is – continuity for on . is mutually absolutely continuous with volume.restrict Ω, with . quantifies over shares , with exact disjointness and exact -sizes. Only is treated, as Theorem 2 states.
Ruled out: as a supremum over a possibly empty set, an inner supremum in over arbitrary sets, the sandwich without monotonicity of , a single rule in place of both, and replaced by its value at one particular . None of these is the paper's statement, and some are trivially true.
Needed infrastructure: δ-continuity of set-valued paths, existence of measurable subsets of prescribed measure for non-atomic measures on , and intermediate-value arguments in several variables. The model definitions are reusable for any non-atomic fair-division development. Proofs of any item are welcome, as are formal versions of the counterexamples to the θ claims.
Ride hailing, online advertising and kidney exchange share a decision problem: resources that are present from the start must be matched, irrevocably and one at a time, to requests that arrive at random. When the arrival probabilities are known in advance, the natural benchmark for an online algorithm is not the offline optimum (the "prophet", who sees every arrival in advance) but the optimal online algorithm: the best expected profit any algorithm can earn when it must decide without seeing the future. That benchmark is well defined and computable in exponential time, so the question becomes one of approximation algorithms: how much of it can a polynomial-time algorithm guarantee?
Papadimitriou, Pollner, Saberi and Wajc (arXiv:2102.10261, Math. Oper. Res. 2024) answer both halves of that question for online Bayesian bipartite matching. They show that approximating the optimal online algorithm within some constant is PSPACE-hard (Theorem 1.1, not part of this mission), and they give a polynomial-time algorithm that earns a fraction of it (Theorem 1.2). The number matters because is the best possible ratio against the prophet, already for a single bin, so shows that comparing with the online optimum genuinely permits better guarantees.
Timeline:
A RideHail instance has a finite set of bins (taxis) and balls (passengers) , revealed in this fixed order. Ball arrives with probability , independently of every other ball. If it arrives it may be matched, irrevocably and before ball is revealed, to an unmatched bin , earning . A deterministic online policy chooses the bin for ball as a function of the arrivals of balls only. Its expected profit is the average, over the arrival patterns, of the total weight of the matching it builds, and is the largest expected profit over all such policies.
LP-Match is the linear program in variables , read as "the probability that the algorithm matches to ":
Its optimal value is . The third family of constraints, (11), holds for online algorithms only.
Algorithm 1 (Rounding LP-Match Online), with , takes an optimal solution of LP-Match, adds a weight-zero dummy bin for each ball so that , and then processes the balls in order. When ball arrives it picks a bin with probability . If is vacant, is matched with probability
If is still unmatched, it picks again from the same distribution, and is matched to the new pick when that bin is vacant and . Edges added by the first pick form , those added by the second pick form , and .
For every instance and every optimal solution of LP-Match,
where is the output of Algorithm 1 run on .
The milestones follow the paper's proof. LP-Match is a relaxation of the online problem (Lemma 4.1). Algorithm 1 matches every edge with probability at least (Theorem 4.2), which rests on two bounds:
Lemma 4.8 comes from the negative association of early-occupancy indicators: Lemma 4.9 and Corollary 4.10, resting on Definition 2.5 and Propositions 2.6–2.8.
The result. Theorem 1.2 is the first polynomial-time algorithm for online stochastic matching with a ratio above against the optimal online algorithm. It separates the online benchmark from the prophet benchmark in an algorithmic sense, and its main technical step, bounding positive correlation between bins' matched statuses through negative association, has been reused for online edge colouring.
Formalizing it. The result is proved on paper and is not machine-checked anywhere. The mission produces:
The negative-association layer (Definition 2.5, Propositions 2.6–2.8) is general probability, absent from Mathlib, and reusable well beyond this mission.
The obvious argument fails at the second pick. Once ball has been rejected by its first pick, the events "bin is vacant" and "the first pick was rejected" are dependent, for two reasons:
Either effect alone can make the second pick useless. The first is controlled by Constraint (11) (Lemma 4.7). The second needs a quantitative bound on the covariance of vacancy indicators (Lemma 4.8), proved by splitting occupancy into early and late parts and showing that the early parts are negatively associated, through a coupling of the algorithm's randomness with independent pick and coin variables. Lemma 4.1 is also not routine to formalize: it requires turning an arbitrary history-dependent online policy into a feasible LP solution, using the independence of arrivals from past decisions.
Conventions committed to in Lean (namespace OnlineMaxWeightMatch.Approx):
ι; balls are Fin n in arrival order (paper ball is index ). Weights and probabilities are real numbers with and ; missing edges have weight .Option-valued: "no bin" carries the leftover mass . When , is in Lean and the ball never arrives.ι ⊕ Fin n with weight . A dummy first pick is accepted with probability and consumes the ball's turn, as in the paper. A dummy is never matched as a second pick.ProbabilityTheory.cond, which is on null events. Equation (20) and Lemma 4.7 therefore carry positivity hypotheses (, ) that make the conditioning event non-null.ProbabilityTheory.covariance."Polynomial time" is not formalized. Because "some online algorithm earns " is trivially true of the optimal online algorithm itself, the goal names Algorithm 1 run on an arbitrary optimal LP-Match solution. That solution exists, so the goal is not vacuous. Replacing by an offline benchmark, dropping Constraint (11), restricting to non-adaptive policies, or treating the dummy pick as "pick nothing" would each change the theorem.
Infrastructure a complete development needs: negative association with its closure properties, finite product probability spaces, conditioning on events, covariance of indicators, and linear-programming feasibility arguments for online policies. Contributions to any milestone are welcome; the probability layer (Propositions 2.6–2.8) is independent of the rest.
Community detection asks for a partition of the vertices of a graph into groups that are densely connected inside and sparsely connected across. In its simplest form there are two communities of equal size, and the natural combinatorial formulation is the minimum bisection problem: among all ways of splitting the vertex set into two halves, find one that cuts the fewest edges. The problem is NP-hard in general, yet on graphs that genuinely contain two well-separated communities one expects it to return exactly those communities. For the two-community stochastic block model, minimum bisection is the maximum a posteriori estimator, so understanding when it returns the hidden partition is the baseline against which convex relaxations are compared.
Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research 2023) study this question deterministically, without a random graph model, in terms of two worst-case degree parameters. Their Theorem 1 gives a sufficient condition for the minimum bisection problem to recover the hidden partition, and Theorem 2 shows the condition cannot be weakened. The rest of the paper compares this with the metric linear programming relaxation of minimum bisection. This mission formalizes Theorem 1.
Let be a simple graph on . A bisection of is a partition of into two sets of equal cardinality ; it exists only for even . Its cost is the number of edges with one end in each set. The minimum bisection problem asks for a bisection of minimum cost.
A fixed bisection , unknown to the solver, is the planted bisection. Write and for the subgraphs induced on the two sides and for the bipartite graph of edges between them. Two parameters measure how well the planted bisection separates the graph:
An optimization problem recovers the planted bisection if its unique optimal solution corresponds to the planted bisection. For minimum bisection a solution is an unordered partition, so this means: every bisection whose cost is at most that of is the partition itself.
The hypothesis is the only one; no connectivity, regularity or lower bound on is assumed.
Fix a second bisection and set , , , , . Let be the edges between and or between and , the edges between and or between and . The paper's proof combines
The last two hold for every pair of bisections.
Theorem 1 is a purely combinatorial certificate of exact recovery: it applies to any graph, random or not, and its two parameters are computable in linear time. Together with Theorem 2 of the same paper, which shows that for every divisible by eight and every admissible with some graph is not recovered, it determines exactly which degree pairs guarantee recovery. The paper then shows that the metric LP relaxation recovers under the nearly identical condition with an additional regularity assumption, so the LP loses almost nothing against the NP-hard problem in this deterministic regime.
The theorem and its proof are published, and the proof is elementary. To our knowledge no machine-checked version exists. Formalizing it fixes a reusable Lean vocabulary for planted bisections (bisections as Finsets, intra- and inter-community degrees, cut cost, recovery up to swapping the sides). The later missions of this series, on the LP relaxation and on the stochastic block model, use the same vocabulary.
The argument is short, and the work lies in the bookkeeping. The obvious contrapositive step, "an optimal bisection different from the planted one cuts at most as many edges", only compares two totals. The proof has to split those totals into the six edge classes between the four sets , and it relies on the identity , valid for any two bisections. The lower bound on needs a double-counting step: the degrees inside of the vertices of sum to at least , and edges inside account for at most of that sum. In Lean the edge classes are filters over ordered pairs , so each identity between them is a statement about disjoint unions of finite sets. The quantity can be negative, so the integer arithmetic must not truncate.
Fin n (0-based, the paper's ), graphs are SimpleGraph (Fin n), and a bisection is a Finset V1 with 2 * V1.card = n, the other side being V1ᶜ. The second bisection of the proof is a Finset W, with = Wᶜ.dIn is the minimum over all vertices of the number of same-side neighbours (defined as when ), and dOut is the maximum over all vertices of the number of other-side neighbours. They are the paper's parameters, not free integers.∀ S, IsBisection n S → cutCost G S ≤ cutCost G V1 → S = V1 ∨ S = V1ᶜ. Requiring S = V1 alone would make the theorem false, since has the same cost.The definitions are finite and decidable in principle and need nothing beyond Mathlib's SimpleGraph and Finset. Contributions of proofs of the three milestones and of the goal are welcome. Lemmas expressing the cut cost of as and that of as are useful intermediate results.
Outpatient clinics serve two kinds of patients: those who book an appointment and those who walk in on the day. Many providers now run open-access or hybrid schedules, which reserve part of the day for walk-ins. Whether patients book or walk in depends on what they know about the appointment delay. Some clinics publish the next available slot in real time (online booking). Others take requests asynchronously, so patients act on a typical delay. Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science, 2023, doi:10.1287/mnsc.2023.4676) model this choice as a game between strategic patients and a provider who splits capacity between appointment and walk-in hours. This mission formalizes their first comparison result: when capacity is short, showing patients the exact delay is at least as good for the provider as hiding it.
The model extends Naor's observable-queue joining problem (Naor, Econometrica, 1969) to an M/D/1 appointment queue with a continuous delay threshold, and adds a walk-in channel whose waiting cost depends on congestion.
Demand. Strategic patients arrive as a Poisson process of rate per day. Exogenous walk-ins arrive at rate and always walk in.
Capacity. The provider has total daily capacity . It allocates to appointment hours and to walk-in hours, with . Appointments form a single-server queue with deterministic service time .
Utilities. Service is worth . A patient who books with delay gets , where . A patient who walks in gets , where and is the walk-in traffic intensity (walk-in arrivals divided by ). Balking is worth . The function is convex and strictly increasing on with (Assumption 1).
Provider cost. Each balking patient costs , and overtime costs with , where is convex and strictly increasing on (Assumption 2).
Observable setting. Each patient sees the exact delay , where is the number waiting and is uniform on . A strategy is a triple : book if the delay is at most , and otherwise walk in or balk with probabilities and . The appointment queue is then the M/D/1/K−1+p queue with and . Its blocking probability has the closed form
where is the probability that a departure leaves the system empty, given by Brun–Garcia sums of Poisson weights. An observable equilibrium satisfies conditions (6)–(10): booking is preferred to the walk-in/balk mixture exactly for delays up to ; ; and patients walk in only if walking in is worth at least , and balk only if it is worth at most . The cost is
Unobservable setting. Patients see only the expected M/D/1 delay and choose rates that sum to . An unobservable equilibrium uses only options of maximal utility among , and . The cost is
If
then for every allocation and every unobservable equilibrium at , there is an allocation at which an observable equilibrium exists and every observable equilibrium costs at most . Equivalently, the optimal observable cost is at most the optimal unobservable cost. The paper states "when is sufficiently small"; the threshold is the one its proof establishes.
The result says that real-time delay information helps a capacity-constrained provider. Patients who see a short queue book instead of balking, so the appointment hours are better used. The second part of Theorem 2 shows that the comparison can reverse when capacity is large, so the information choice depends on the regime. The small-capacity side is the one that applies to clinics without spare capacity.
The formalization also produces reusable queueing content. It gives a machine-checked closed form for the M/D/1/K−1+p queue with fractional buffer (Hassin–Haviv notation): its departure-epoch law, its blocking probability, and the monotonicity and continuity of that probability in the buffer. The paper's proofs are in its Online Appendix: E.3 for Lemma E.5 and Theorem 2, and E.4 for Appendix C. None of these results has a machine-checked proof.
The obvious argument fixes an optimal unobservable allocation and compares both settings there. That argument has three gaps. First, the existence of an optimum of (Un.P) is never proved, so the comparison has to work at every allocation. Second, the same-allocation comparison (Lemma E.5) is a three-by-three case analysis over the equilibrium regimes (schedule-balk, schedule-walk-balk, schedule-walk) of the two settings. One printed case concludes the opposite inequality; under the lemma's hypothesis that case forces equal costs. Third, the closed-form blocking probability is an alternating sum. Its positivity, its bound and its monotonicity across the seams where jumps are not visible term by term. Existence of the observable equilibrium needs an intermediate-value argument through the continuity of in .
Everything lives in the namespace OutpatientWalkIn.SmallCap, in two definition modules.
MD1Queue holds the Poisson weights, the recursion (one clause for ), , of (26), the departure law (27), of (24) and .Setting holds the model, the standing assumptions, both equilibrium notions and both costs.The conventions are the following.
A trivializing formalization is ruled out on four counts: is the paper's closed form, not an assumed function; the goal quantifies over every unobservable equilibrium and every observable equilibrium at the chosen allocation; no infimum over a possibly empty set appears; and both equilibrium sets are nonempty (milestones 4 and 5).
The infrastructure needed is elementary real analysis and finite sums. Contributions are welcome on the queue lemmas (positivity of and , the bound , continuity across seams), which are reusable for any finite-buffer M/D/1 model. The companion mission on the triage model uses the same encoding.
Online marketplaces (Amazon, Booking.com, Airbnb, Upwork) charge sellers a fee on every transaction they intermediate. Once a buyer has found a seller on the marketplace, both have an incentive to complete the sale off the platform and split the fee they save. This is leakage (also called disintermediation or showrooming), and it limits the fees a marketplace can sustain. Hagiu and Wright, Marketplace Leakage (Management Science, 2023, doi:10.1287/mnsc.2023.4757), build a minimal model of leakage and compare the strategies a marketplace can use against it.
One of these strategies is contractual: a price-parity clause (PPC), under which the seller must not charge less in its direct channel than on the marketplace, on pain of being delisted. The paper notes that such clauses have been used by hotel-booking platforms, price-comparison platforms and Amazon (p. 22). The paper's Proposition 4 asks when a marketplace that cannot observe how easily buyers switch actually wants such a clause. This mission formalizes that proposition and the profit formulas behind it.
A marketplace , a seller and a unit mass of buyers with unit demand. Every buyer values 's product at ; 's marginal cost is ; the outside option is worth . sells on at price , paying a fee per transaction, or directly at price with no fee. A buyer who buys directly bears a switching cost . In the baseline state switching costs are uniform on , , with clamped distribution function . In the no-switching state switching costs are infinite and nobody buys directly. The baseline state occurs with probability . knows the state when it decides; does not when it sets .
Without a PPC, always lists, sets , and in the baseline state picks to maximize
A maximizer is a seller-optimal price . 's value is
With a PPC, a listed seller must set and earns . A seller that delists earns in the baseline state and in the no-switching state. It accepts 's offer when listing pays at least as much, so 's value is the largest expected revenue over all fees .
For , and , both values exist, and
The goal states the comparison for any values satisfying the optimality predicates, so it is insensitive to how either value is later computed.
Proposition 4 identifies a trade-off. A PPC removes leakage entirely, but it also takes away the seller's ability to divert some buyers when the fee turns out to be too high, so the seller may refuse to participate. When the baseline state is unlikely and switching costs in it are high, the marketplace earns more by tolerating leakage and charging the full surplus . In every other case the clause pays. This makes the welfare and competition-policy debate about parity clauses explicit in a two-parameter region. It also contrasts with the case without uncertainty, where a PPC is always better for the marketplace.
The paper's proof (§8.5, pp. 39–40) is a short case comparison between closed forms. It has not been machine-checked. The printed formula for when omits the corner fee and is wrong for small . The conclusion still holds there, but by a different comparison. A formal proof pins down which steps survive.
Two optimizations are nested. The seller's optimal direct price changes regime at , where the uniform distribution's kink binds. The marketplace's revenue without a PPC is therefore piecewise in , with an interior candidate that is feasible only when . Under a PPC, revenue is discontinuous in because acceptance switches on and off. Its maximum is attained only because acceptance is weak. Comparing the two values requires a case split over and against and , and the boundary cases include genuine ties ( for , ). Reading off a single printed closed form for fails in part of the region.
All objects are in one definitions file in namespace MarketplaceLeakage.Parity. The parameters are real numbers v c μ q, with standing hypotheses c < v, 0 < μ, 0 < q, q ≤ 1 on every theorem. The paper states (p. 5) and (p. 9). is added: is a probability, and at both values equal , so the "if" direction of the goal fails. is allowed. The statements use the reduced seller problem (1), as the paper does after its Lemma 1 (p. 7), with . Lemma 1 itself is not posed.
Committed conventions:
IsSOpt), not a formula.IsPPCValue) is the attained maximum of over all . Acceptance is weak and is stated against every delisting price .IsNoPPCValue) is the attained maximum of over and seller-optimal .These choices rule out the trivializing formalizations. Neither value is defined by its printed max-expression, which would make the milestones definitional. Strict acceptance would leave the PPC optimum unattained. A value given by sSup would be meaningless off its domain. Reading "prefers to impose" strictly would make the statement false at the ties.
No published platform definitions are reused. A complete development needs only elementary real analysis: maximizing piecewise-quadratic functions, attainment on compact intervals, and case analysis over min/max. The lemmas on the seller's best response under the uniform are reusable in the companion missions on Propositions 1–3 of the same paper. Proofs of any milestone are welcome independently.
Contract breaches in supply chains rarely stay isolated. A supplier that delivers late forces its customer to breach its own downstream contract, which in turn harms the next firm, and so on. Each firm in such a chain both suffers a loss and causes one, and a court, an arbitrator or a self-executing smart contract has to decide who pays for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) treat this as an axiomatic cost-sharing problem. The two classical readings of strict liability are extremes: under direct liability every agent pays exactly the loss it causes, and under indirect liability the initiator of the chain pays everything. The paper asks which compromises between the two are justified by normative requirements that are simple enough to be written into a contract, and answers that the requirements single out a one-parameter family, the fixed-fraction rules.
This mission formalizes that characterization (Theorem 1 of the paper) together with the two propositions and the lemma its proof rests on, and the examples showing that none of the four axioms is redundant.
A loss chain has agents . Agent initiates the chain, and agent causes a loss to agent ; agent only suffers. A loss problem is a vector with total .
An allocation assigns liabilities such that no initial segment of the chain pays less than the losses it caused, and the liabilities balance the total loss:
A rule assigns to every problem , for every , an allocation , and is continuous along rays: as .
For the fixed-fraction rule (Definition 1) charges every agent the fraction of the loss it causes and the initiator in addition the residual:
The elementary problem has a single unit loss caused by the last agent.
The four axioms are:
A rule satisfies additivity, zero truncation, merging proofness and population monotonicity if and only if there is with
In attack order:
The proposal also contains four companion statements from Appendix B, which are not milestones: the serial rule and the rules each satisfy three of the axioms and violate the fourth.
Theorem 1 justifies a whole family of liability rules from four requirements, each of which has a concrete meaning: liability does not depend on how a loss is split into components, adding trailing zero losses changes nothing, adding agents without new losses makes no old agent worse off, and two consecutive agents cannot lower their joint liability by merging. The parameter is left free, and the paper then uses separate arguments (equidistance from ideal allocations, the Shapley value and the nucleolus of an associated game; the later missions of this series) to single out . Theorem 4 of the paper extends the characterization from chains to loss trees and relies on the same propositions.
A machine-checked proof of Theorem 1 adds an axiomatic cost-sharing layer to the platform, with reusable definitions of loss problems, allocations, continuous rules and the four axioms. It also fixes the axiom in a form under which the theorem is true: the manuscript's population-monotonicity axiom, read with its printed range, makes Theorem 1 false (see below). The result is proved in the paper; it has not been formalized before.
The proof combines three different kinds of argument. Additivity on the cone yields homogeneity only for rational factors; the step to real factors uses the weak, ray-wise continuity of rules, and needs care because continuity is only assumed at loss vectors, near the factor . The reduction to elementary problems decomposes a problem into single-loss problems and moves between problems of different lengths with zero truncation, so statements about vectors of different dimensions have to be related. Finally, the values on elementary problems are pinned down by population monotonicity, which compares problems of consecutive lengths only, so that information about and has to be carried to every . Without the case of the axiom the chain from to breaks, and the conclusion fails.
Fin n, 0-based: the paper's agent is index . A rule is φ : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ), a total function. IsRule φ requires, for every and every , that and as in the product topology. Only values on loss vectors carry meaning. Every axiom quantifies over loss vectors only, and every conclusion "" is agreement on every , never an equality of Lean functions, which would be false for an arbitrary extension of to .Fin.snoc ℓ 0; is admitted and adds nothing. is part of the conclusion of Theorem 1 and Proposition 2, not a hypothesis.IsRule changes the theorem (without , need not lie in ); both are hypotheses of every statement about an arbitrary rule.Needed infrastructure: finite sums over Fin n with filters, Fin.snoc/Fin.castSucc/Fin.succ bookkeeping, and a density argument from to with filters. The definitions are written to be shared with the other missions of this series. Proofs of the milestones in any order are welcome.
Online marketplaces for services (home repair, tutoring, beauty appointments, freelancing) earn a fee on each transaction they intermediate. After a buyer has found a seller on the marketplace, both sides can often complete the transaction, or the next one, off the platform and avoid the fee. This leakage (also called disintermediation) is a central constraint on how such platforms price, and platforms respond to it in several ways: lower fees, bans on exchanging contact details, price-parity clauses, and investment in features that make transacting on the platform itself more valuable (payment protection, scheduling, reminders, dispute handling).
A. Hagiu and J. Wright, Marketplace Leakage (Management Science, 2023), build a minimal model of a marketplace, a seller and buyers with heterogeneous costs of buying directly, and compare these responses. This mission formalizes the paper's analysis of the last one: investing in transaction benefits (§5.1 and Proposition 2).
There is one marketplace , one seller and a unit mass of buyers who each want one unit of 's product. Every buyer values the product at ; 's marginal cost is , with ; the outside option is worth . A buyer who buys directly from instead of through bears a switching cost , drawn from the uniform distribution on with :
The marketplace first chooses a transaction benefit , which buyers receive when they buy on , at cost with , and a per-transaction fee . Following the paper (p. 12), the marketplace's feasible choices are and . Given , the seller lists on at price and sets a direct price to maximize
The leakage is , the share of buyers who buy directly. The marketplace earns
An optimum is a triple with feasible, seller-optimal at , and no feasible with seller-optimal giving the marketplace more. The Lean development uses the same letters: G μ s, sProfitB, IsSOptB, MProfitB, leakage, IsOpt, and the threshold
An optimum exists, and at every optimum
Moreover is strictly decreasing in ; for fixed it is constant in on (with zero leakage there), strictly decreasing on (with strictly increasing leakage), and strictly increasing on (with strictly decreasing leakage).
Proposition 2 says that a marketplace's investment against leakage is non-monotone in how costly leakage is for buyers. When switching costs are small, the marketplace invests enough () to remove leakage entirely and charges a fee equal to the benefit. For intermediate switching costs it tolerates growing leakage and invests less. For large switching costs, where the fee is pinned at the seller's participation constraint, it again invests more as leakage falls. Leakage itself is zero, then rising, then falling in switching costs, so the comparative static that matters for platform design (how much leakage to tolerate) is not monotone in the parameter that measures how attached buyers are to the platform.
The result is proved in the paper by an explicit case analysis. As far as known, it has no machine-checked proof. A complete formalization certifies the closed forms, the joint optimality over (not just the first-order conditions), and the strictness of each comparative-static claim, including across the regime boundaries and , which the paper treats as "easily seen".
Every step is elementary, but the obvious argument through first-order conditions is incomplete. For fixed the inner problem in has a kink at and corners at and , so is piecewise with three regimes. is not concave when and : its derivative first decreases, then increases, then decreases, and showing that is the unique global maximizer requires comparing values across the pieces. The paper's case split is on for fixed ; the proposition is stated in for fixed , and translating one into the other needs the root structure of a quadratic in . Strict monotonicity in has to hold across regime changes, where the formula for changes.
IsSOptB; the marketplace's optimum is the predicate IsOpt over the joint choice . No closed form for , or is a definition; "max" is stated by attainment (IsGreatest), never by an unattained supremum. Comparative statics compare optimal choices at two parameter values, not formulas.A formalization that defined or the seller's response by its cases, stated the comparative statics about the closed-form formulas alone, or replaced "max" by an unattained supremum would trivialize the mission and is ruled out. Contributions welcome: proofs of the milestones, and reusable lemmas on maximizing piecewise quadratics.
The linear exchange market (the linear Arrow–Debreu model) is the basic model of general equilibrium with linear utilities: each agent brings goods to the market, sells them at the going prices, and spends the proceeds on the goods that give the most utility per unit of money. Computing its equilibrium is a classical problem in algorithmic game theory and in mathematical economics. Gale characterised when an equilibrium exists; Eaves (1976) gave a finite algorithm; Jain (2007) and Ye (2008) gave polynomial-time algorithms through convex programming and interior-point methods; Duan and Mehlhorn (2015) gave a combinatorial weakly polynomial algorithm, later improved by Duan, Garg and Mehlhorn (2016). Whether a strongly polynomial algorithm exists (described by Duan and Mehlhorn as a major open question), one whose number of arithmetic operations depends on the number of agents and goods only and not on the bit size of the utilities, remained open until Garg and Végh (arXiv:1809.06266, STOC 2019, Operations Research 2023).
The algorithm of Garg and Végh maintains a set of revealed edges, pairs (agent, good) that are known to be maximum bang-per-buck edges in every equilibrium, and enlarges until a relaxed equilibrium, an -equilibrium, is found. Two lemmas of §3–§4 of the paper make this work: a large money flow on an edge reveals it (Lemma 3.3), and an -equilibrium for revealed can be converted into a genuine market equilibrium at the same prices (Lemma 3.4). This mission formalizes these lemmas and the claims of their proofs.
There are agents and divisible goods , one unit of each; agent owns the unit of good . Agent has utility per unit of good . The edge set is , , and every agent and every good has an edge.
Given prices , agent 's budget is . The maximum bang-per-buck (MBB) edges are the edges with
and is their set. A money flow records how much agent spends on good . The pair is a money allocation if , , , no agent spends more than and no good receives more than . The surplus of good is , and is a market equilibrium if .
The set consists of the edges that are MBB edges in every market equilibrium. For an edge set , an -allocation relaxes a money allocation: money may be negative on the edges of , and every edge of must be MBB. It is an -equilibrium if . The potential of an -allocation is , and is its minimum over the -allocations supported on .
If a market equilibrium exists, , and is an -equilibrium, then there is a money flow such that
A further item, Lemma 3.9 (p. 7), is the progress step of the overall algorithm: if , some edge of joining two components of carries more than . It is not used by the goal and is not a milestone.
Lemma 3.4 is the termination step of the first strongly polynomial algorithm for linear exchange markets: the algorithm only ever needs to find an -equilibrium for a set of revealed edges, and Lemma 3.4 turns it into an equilibrium by one maximum-flow computation. Lemma 3.3 is the step that reveals new edges, and Lemma 3.9 is the step that guarantees one is revealed in every round. Together they reduce the computation of an equilibrium to a sequence of relaxed problems on a growing set of known edges; the paper notes (p. 3) that Lemma 3.3 is analogous to the identification of abundant arcs in Orlin's strongly polynomial minimum-cost flow algorithm.
The results are proved in the paper. As far as known, none of them, nor the linear exchange market model with money flows and MBB edges, has a machine-checked formalization. This mission produces the model as a reusable definition layer (markets, MBB edges, money allocations, equilibria, revealed edges, -allocations, the potential ), and machine-checked proofs of the structural lemmas behind the algorithm. The proof of Lemma 3.4 in the paper ends with "repeat the same analysis on the remaining set of agents and goods", an induction the paper leaves informal; a formal proof makes it explicit.
The equilibrium used in the proofs is an arbitrary one, with prices unrelated to . The obvious attempt at Lemma 3.4, rounding the negative entries of to zero, breaks the budget and market-clearing equalities. The paper's argument instead compares with through the maximal price ratio , shows that the agents and goods of maximal ratio form a block that trades only internally both at and at , and then removes the block and recurses. The step " is a union of components" is asserted in the paper without proof, and the recursion requires carrying an equilibrium of the remaining submarket. Lemma 3.3 is a counting argument over a set of goods whose prices increase; its sign bookkeeping, and the use of negative flows only on edges of , are where an informal reading goes wrong.
Agents and goods are both indexed by Fin n (0-based), so the good owned by agent i has index i; the bipartite graph lives on Fin n ⊕ Fin n with agents on the left and goods on the right. Utilities, prices and money are real. Every allocation predicate requires every price to be positive, and an MBB edge must have . keeps the absolute values of the paper's norm. quantifies over all market equilibria, so it equals when the market has none. is taken as an infimum: it is the paper's minimum when the minimum exists and when no -allocation is supported on , which makes Lemma 3.9 vacuous, not false, in that case.
The paper's running-time claims (Theorem 3.1, the " time" of Lemma 3.4) are out of scope; the goal poses the existence of that the maximum-flow computation witnesses. The goal adds the hypothesis that some market equilibrium exists. The paper guarantees one through its standing assumption (strong connectivity of the digraph of positive utilities) and Gale's cited existence criterion; the hypothesis is what the proof uses and makes the statement more general. It cannot be dropped: without an equilibrium , and there are markets with an -equilibrium and no market equilibrium. A formalization in which a market equilibrium could carry negative money or nonzero surplus would make the goal trivial and is ruled out by the definitions: a money allocation has on every pair and an equilibrium has .
A complete development needs finite sums, real division, connectivity in a SimpleGraph (SimpleGraph.Reachable), and an induction on the number of agents for Lemma 3.4. The market definitions are reusable for any work on linear Fisher or exchange markets. Contributions welcome: proofs of the milestones, of the goal, of Lemma 3.9, and a formalization of the existence criterion (Lemma 2.3).
Firms that hire for several roles at once face a timing problem. An offer occupies a candidate until they answer, a candidate can hold only one offer, and the hiring season has a fixed number of decision rounds. Sending offers one at a time is slow; sending them all at once risks over-hiring. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three stylised models of this pipeline: interviewing with a cap on interviews (ProbeTop-), offering in parallel rounds, and offering all at once. This mission formalizes their result for the second model, the Parallel Offering problem.
The question belongs to the literature on stochastic probing and LP-based approximation of adaptive policies. The Sequential Offering model of Purohit, Gollapudi and Raghavan (2019) sends one offer per round for identical positions. Parallel Offering lets each unfilled position send one offer per round, with heterogeneous positions, and asks how much a simple, non-adaptive policy loses against the best adaptive one.
A firm fills positions from candidates within rounds. Candidate accepts an offer for position with probability and then adds the value . An instance is with
In each round the firm may send one offer for every unfilled position, and each candidate receives at most one offer in total. Before the rounds start, each candidate has decided the set of positions they would accept, with . These decisions may be correlated across the positions of one candidate and are independent across candidates.
The linear program has a variable for the probability that candidate is offered position :
The paper shows (Lemma 6) that its value bounds the expected reward of every policy.
The dependent rounding of Gandhi, Khuller, Parthasarathy and Srinivasan (2006) takes a bipartite graph with edge weights and outputs random indicators with (P1) ; (P2) every vertex degree is the floor or the ceiling of its fractional degree, with probability 1; (P3) for every vertex , every set of edges at and every , .
The algorithm solves to optimality, rounds the optimal on the complete bipartite graph candidates positions, and puts candidate on the list of position iff . Every list is then run in parallel, in decreasing order of : position offers to the next candidate on its list each round until someone accepts, the list ends or the rounds are over. is its expected total value.
For the analysis, is the set of candidates on list who would accept, (zero on the empty set), is the same set built from independent Bernoulli() variables instead of , and .
The constant is tight (App. C.5 of the paper), so the goal states the paper's result in its final form.
Theorem 2 shows that a non-adaptive policy, fixed before any offer is answered, earns at least of the LP bound, hence of the best adaptive policy, for heterogeneous positions and with acceptance decisions correlated across positions. Through Lemma 9 it also bounds the cost of batching: parallel rounds lose at most a factor against sequential offers (Corollary 3 of the paper).
The results are proved in the paper; none of them is formalized. The mission adds to the platform a reusable statement of the GKPS rounding properties on bipartite graphs, an explicit finite model of a parallel offering process computed from its run, and a LP-rounding guarantee that a solver must connect end to end: the algorithm's reward, the per-position reduction, the comparison with independent rounding, and the bound for independent rounding.
The obvious first step, replacing the dependent rounding by independent rounding with the same marginals, is not free: the rounding couples the candidates of a list, and an expected maximum is not linear in the indicators. Only the negative correlation of the rounding at a single position rescues it, and the paper notes (App. C.3) that (P1) and (P3) alone do not suffice once several identical positions are pooled, so the argument is genuinely per position. The written proof of Lemma 7 (p. ec10) has a sign error and a wrong indicator; the statement is correct. Independent rounding then still has to be compared with the LP: the LP only controls each list in expectation, through , while the algorithm collects at most one value per list.
Candidates are Fin n, positions Fin k, all quantities real. All randomness is finite: an expectation is an explicit sum over the rounded edge set , weighted by a distribution , and over acceptance profiles , weighted by , where is any law on subsets of with marginals . The rounding is independent of the acceptance decisions.
The rounding scheme is represented by its properties: the goal holds for every distribution with (P1)–(P3) for the weights , which includes the scheme of Gandhi et al. The LP solution is any optimal one. The order of list is a permutation of the candidates that is decreasing in , ties in any order. is computed from the run: candidate is hired for iff is on list , would accept , nobody earlier on list would accept , and fewer than candidates precede on the list. It is not defined by the formula , which is a milestone, and the goal is compared with the objective at an optimal LP solution, never at an arbitrary feasible point. The degree condition (P2) is kept in the rounding predicate, not replaced by the list properties it implies.
A complete development needs finite sums over product distributions, expected maxima of random subsets of sorted values, and elementary estimates involving ; no measure theory is required. The GKPS definition is generic in the two vertex sets and reusable for other dependent-rounding results. Proofs of any milestone are welcome, as is a proof of Lemma 7 for general negatively correlated roundings.
A seller with scarce stock may offer a product before its main selling period. This gives buyers another chance to obtain it, but it can also alter when they compete for the stock. The seller must choose a price while anticipating that buyers respond to both the price and the chance that the unit will already be gone. Glazer, Hassin, and Nowik study this interaction for a single unit and strategic Poisson arrivals in their 2023 paper. Their high-demand model leads to an unusual comparative static: in the regime where buyers arrive in both periods, raising the price increases the total arrival rate (Theorem 1, p. 12). The eventual profit-maximizing price nevertheless induces arrivals in only one period (Theorems 3–4, pp. 13–15).
The seller has one unit and posts one price for two selling periods. Potential buyers are identical and each chooses to try to buy early, try to buy late, or stay away. A buyer pays an arrival cost even if the unit is unavailable. The good is worth less to a buyer who obtains it early. If several buyers arrive while the unit is available, each has the same chance of receiving it. The number choosing each period follows a Poisson arrival model; write and for the early and late equilibrium arrival rates. These are expected counts, not probabilities, and may exceed one.
Divide monetary values by the positive arrival cost. Let be the normalized late value, the penalty for early purchase, and the single normalized price. Set and for . The two arrival utilities and the seller's expected profit are
The factor in is the chance that no early buyer takes the unit. The value is the continuous limit of the competition factor, so a buyer considering arrival when nobody else arrives still faces the correct utility. In the paper's high-potential-demand limit (§5, p. 10), an equilibrium has and satisfies complementarity: a period with a positive arrival rate has utility zero, while a period with zero arrivals offers nonpositive utility to a buyer who considers entering. This selects the paper's equilibrium types 1–4. The finite-demand equilibria in which every potential buyer tries to arrive are outside this mission.
Several thresholds have precise definitions. The principal Lambert function is the inverse of on (Definition 11, p. 26). Put . The border between mixed and early-only arrivals solves (p. 11). The switching threshold is the larger root of (Definitions 24 and 26, pp. 42–43).
The goal is the four-case price rule of Theorem 4 (p. 15). It identifies a profit-maximizing price , its equilibrium rates , and the greatest attainable expected profit over all nonnegative prices:
The printed formula in the second case has a removable at ; this mission states that case for and states the boundary separately: there every nonnegative price induces zero arrival rates (so ) and the optimal profit is . A displayed price is a maximizer: the paper's candidates can tie at . The milestones cover equilibrium existence and uniqueness (Proposition 9), the regional Lambert-function formulas (Theorem 14), the mixed-arrival comparative statics (Theorem 1 and Corollary 2), and the candidate-profit comparisons and thresholds (Propositions 20–21 and Lemmas 22, 25, 29).
The theorem tells the seller which price and arrival pattern correspond to each value regime. It also gives an exact benchmark for comparing the option to sell early with selling only in the later period. In this model, offering an early period never raises the maximal profit above the late-only benchmark, a consequence discussed in Corollary 5 and Theorem 6 (p. 15). The price rule is proved in the paper; the work here is to give its model, boundaries, regional lemmas, and global optimality claim machine-checkable statements and ultimately proofs. The mission statements are compiled Lean targets with proof placeholders, not completed machine-checked proofs.
A higher price usually suggests fewer buyers. Here an early arrival can remove the only unit before the late period. In the mixed-arrival region a price increase changes the early rate and therefore changes the late buyer's chance of finding stock. The total rate can rise even as the early rate falls. The seller's profit also depends on the price times a sale probability, and its regional price formulas do not automatically give a global maximum. The proof must account for each regional border and compare the relevant candidates; the Lambert formulas and the switching root make those comparisons explicit in the paper.
Lean uses real parameters in units of the arrival cost. The standing assumptions and are explicit. The potential-demand limit is encoded directly by the utility complementarity conditions, and profit ranges over every price and every equilibrium satisfying them. The goal uses IsGreatest together with attainment at the displayed price, so it asserts an actual global maximum. The paper's , , and are defined from their characterizing equations on the principal branch and the stated root domains; they are not free parameters. The statements guard the logarithms and quotients that arise at and . The separate region listings in the paper differ at some harmless boundaries, so each milestone uses the borders relevant to its own statement.
A valid formalization must keep , define equilibrium through utility conditions rather than through the claimed closed forms, and compare profit across every nonnegative price. Otherwise the equilibrium and optimality results could become empty or immediate by definition. The reusable work includes the continuous Poisson competition factor, Lambert-function interface, and precise handling of attained extrema. The mission covers one unit and high potential demand; the paper's multiple-unit numerical section and finite-demand equilibrium types are separate topics.
Retailers that run predictable promotions teach their customers to wait for them. A customer who knows that a discount will come next week has no reason to buy at the list price today. Firms therefore lose margin on exactly the customers who would have paid in full. One response, documented in practice by Moon, Bimpikis and Mendelson (2017), is to randomize promotions: commit to a distribution of prices, draw a fresh price every period, and let customers know only the distribution. A customer cannot time a discount that arrives at random. Whether waiting is worthwhile then depends on how patient the customer is.
The classical deterministic answer to strategic waiting is cyclic pricing: Conlisk, Gerstner and Sobel (1984) showed that a durable-goods monopolist facing a stream of arriving customers lowers its price periodically. Besbes and Lobel (2015) characterized optimal deterministic policies when customers differ in valuation and patience. Randomized prices as a model of sales go back to Varian (1980) in a competitive setting. Chen, Hu and Wu (SSRN 3223844, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1194) ask the monopoly question directly: which price distribution should a seller commit to when two customer segments differ in both valuation and waiting cost? This mission formalizes their answer for the two-segment base model.
A monopolist sells one product over an infinite horizon. A fraction of arriving customers are low-valuation customers, who value the product at and pay a waiting cost per period; the remaining are high-valuation customers, with valuation and waiting cost . Assumption (S) of the paper is and .
The firm announces a price distribution: a random price with finitely many possible values and probabilities summing to one. Each period an independent price is drawn from it. Write for the distribution function, for the mean price conditional on , and for the expected one-period surplus of a customer with valuation . The purchase threshold of a customer with waiting cost is
A customer whose valuation exceeds her threshold waits and buys at the first price not above it.
The paper reduces the firm's choice to the regime where low-valuation customers wait and high-valuation customers buy on arrival. The firm's long-run profit per arriving customer is then the objective of problem (2):
where is the low type's threshold. Replacing by in the objective gives the relaxation, problem (3). The key constants are
In Lean the parameters are vL vH cL cH α, a law is w : ℝ →₀ ℝ with IsPriceDist w, and the objects above are cdf, condExp, gain, thresh, Feas, obj2, obj3, ΔR, bnd , U1, U2. Here is written p^L in milestone text.
Assume and , and let if and otherwise. Then every price distribution feasible for (2) earns at most in (2), and there is with as such that the two-point law
is feasible for (2) for all small and its profit tends to . This is the -optimality of the paper's Definition 1.
The result says that, in this model, the optimal randomized promotion is the simplest one. The firm posts the regular price most of the time and runs a promotion at with probability . High-valuation customers buy on arrival; low-valuation customers wait for the promotion. The discount below , of size , is the price of keeping low types in the market. The closed forms quantify the profit lost relative to perfect discrimination . The paper uses them to compare randomized with static and cyclic pricing (Propositions 4 and 8) and generalizes the structure to myopic customers and to segments.
The result is proved on paper; no machine-checked version exists. The mission produces a formal statement of the firm's problem over all finitely supported price laws on , a verified upper bound on its value, and a verified family that attains it in the limit. It also records three points the printed statements leave implicit (below).
The decision variable is an entire distribution, and the objective of (2) depends on it through the threshold , itself defined by a maximization over the distribution. The obvious approach, guessing the two-point law and checking first-order conditions, gives no upper bound over all laws. The upper bound has to hold for laws with arbitrarily many support points, of either sign and above , and both incentive constraints enter it. Problem (3) has a strict constraint and no maximizer, so every statement about "the optimal profit" has to be read as a supremum. The attainment half then needs the threshold of the two-point law, computed from its definition, to sit exactly below .
w : ℝ →₀ ℝ with nonnegative masses summing to one (finite support, as the paper assumes on p. 9). Prices range over all of : can be negative under the hypotheses, and with prices restricted to Proposition 3 is false for some admissible parameters.obj2 and thresh applied to it. The upper bound ranges over all feasible laws, not two-point laws or laws on . "Optimal" is not read as "beats static pricing" (that is Proposition 4) or as an attained maximum, and may not depend on the competing law.Finsupp supports, monotonicity and continuity of , and the elementary concavity argument for . A general library of finitely supported real price laws (distribution function, partial expectations, expected surplus) would be reusable for other pricing papers. Proofs of any milestone are welcome.Non-profit organizations depend on volunteers whose availability they cannot schedule. They can only influence it, through recruiting drives, reminders and recognition events. Ata, Tongarlak, Lee and Field (arXiv:2312.02920) model a food-recovery non-profit's volunteer pool as a queueing network. Repeat volunteers rest between shifts, one-time volunteers arrive at random, and all signed-up volunteers wait on one sign-up list, from which they may abandon. The organization pays for engagement activities that speed up volunteers' return, and it is penalized when tasks go uncovered because the list is empty.
In heavy traffic the problem reduces to a one-dimensional drift-rate control problem. A workload process behaves like a reflected Ornstein–Uhlenbeck process whose drift the controller chooses from an interval at cost , plus a penalty per unit of idleness at . The analytic core of the paper is the Bellman equation of this problem: a first-order ordinary differential equation on with an unknown constant. Its solution yields the optimal long-run average cost and a nested threshold policy for when to run each engagement activity.
There are engagement activities. The data are a lowest drift , drift increments , per-unit-drift costs , an idleness cost rate , a mean-reversion rate and a volatility . The breakpoints are
and . The engagement cost is piecewise linear and convex: , with slope on , so that for . Its convex conjugate is
The Bellman equation (68)–(69) asks for a constant and a continuously differentiable function on such that
with , strictly increasing, and .
The milestones use the shooting objects of the paper's Online Supplement §F:
The goal asserts existence only. It does not identify with , and it does not claim uniqueness.
The Bellman equation is what makes the paper's policy computable. Theorem 1 provides the constant , which the paper's Theorem 2 identifies as the optimal long-run average cost of the workload problem. It also provides the increasing function , whose level sets are the thresholds of the optimal nested policy: engagement activity is used when the workload is below . The companion mission (II) gives in closed form between consecutive thresholds. Both results presuppose the existence proved here.
The paper proves Theorem 1 in its Online Supplement, partly by citation: Lemma 4 is called standard and its proof is omitted. As far as is known, none of these statements has a machine-checked proof. A formalization would also settle two points that the printed argument leaves loose. The lower bound is written as an infimum over all of , which is when . And one step in the proof of Lemma 9 claims that a set of positive measure contains an interval, which is false; the formal chain avoids this step by posing Corollary 2 directly.
The equation is first order but nonlinear through , and it is posed on an unbounded interval with a boundary condition at infinity. A local existence theorem does not suffice: the right-hand side has linear growth with a coefficient that grows with , so global existence on and monotone, continuous dependence on must be established separately.
The main difficulty is the shooting step. For a fixed the initial value problem has a solution, but it generally fails the condition : either it eventually turns down and tends to , or it crosses and grows without bound. The proof must show the following:
Continuity in alone does not give the last point: it needs a separate argument at infinity.
Everything is stated for one fixed parameter set satisfying an explicit predicate Standing: , , , , . These are disclosed additions. The paper never restates them for the abstract control problem, but they follow from its queueing primitives ((24), (43), (50), p. 18). No hypothesis is made.
Conventions:
Trivializing formalizations are ruled out. The solution is never chosen: every lemma quantifies over all solutions of IVP(). The goal quantifies and existentially and requires all of (69), including the limit and strict monotonicity.
The source is the arXiv preprint v2, including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the equation but are not part of any formal statement.
A complete development needs:
IsPicardLindelof and Gronwall bounds are the starting point);Both are reusable beyond this mission. Proofs of individual milestones are welcome in any order. Lemmas 3, 4 and 6 are independent of the shooting lemmas.
A supplier who must build capacity before a selling season would like to know how large demand will be, and the retailer downstream often knows better. Under a simple wholesale-price contract, however, the retailer gains from overstating demand: more capacity means more sales for her, and the cost of idle capacity falls on the supplier. Since the retailer's message costs nothing and binds nobody, a rational supplier ignores it. That such cheap talk (Crawford and Sobel, 1982) cannot convey information in a one-shot wholesale-price relationship is the benchmark result of Özer, Zheng and Chen (2011), yet firms are observed to share forecasts informally.
Avinadav and Shamir propose an explanation based on partial vertical ownership (PVO): retailers often hold passive equity stakes in their suppliers. A retailer that owns a share of the supplier bears a fraction of the losses her misreport inflicts on him. Their Theorem 2 says exactly how large the stake must be for truthful reporting to be self-enforcing, and how this depends on the gap between the two possible demand levels. This mission formalizes that theorem.
A retailer sources a component from a supplier. The supplier secures capacity at unit cost ; after demand is realized, the retailer orders and pays the wholesale price per unit and sells at the retail price , with . Unmet demand is lost, and leftover capacity is worthless.
Demand in market state is with , where is a zero-mean random variable with a density, distribution function , and lower support end satisfying . The information gap is . Write and define the critical fractiles and .
The retailer may commit to an advance order which the supplier must cover. The supplier's and retailer's expected profits are
A retailer holding the share of the supplier maximizes the accounting payoff .
Only the retailer observes the state. In the cheap-talk game she places no advance order and announces a state; a supplier who believes the announcement builds the newsvendor capacity or . Truthful reporting requires
Let
The goal asserts: (12) holds for every ; for every , (12) and (13) hold if and only if ;
and for every the equation has a unique root , and truthful cheap talk is possible only if .
In attack order: the closed forms (2) and (3) of the expected profits; condition (12) always holds; (E.1), that (13) is equivalent to with positive numerator and denominator; (E.2), the closed form of ; and the properties of (strictly increasing on , limits at and at , values in ). A companion item states Proposition 1: if and only if the integrated chain earns less with than with in the low state.
Theorem 2 identifies an ownership channel through which a one-shot wholesale-price relationship can sustain truthful information exchange, in contrast with the impossibility of cheap talk without such links. The threshold is the ratio of the low-type retailer's operational gain from lying to the supplier's loss from being misled, and part (ii) turns it into a lower bound on the information gap: a sufficiently small gap rules out cheap talk for every stake. Proposition 1 translates feasibility () into a comparison of the integrated chain's profits. The same comparisons underlie the paper's later analysis of signaling with advance orders, which takes cheap talk as its benchmark.
The result is proved in the source, in Appendix E of the authors' manuscript; it has no machine-checked proof. The mission produces a formal statement in which every profit is an expectation over a general noise distribution, so that the closed forms the paper derives become theorems rather than definitions, together with the supporting analysis of the averaged distribution function .
The algebra after the closed forms is short. The work lies in two places. First, the closed forms (2) and (3) are integration-by-parts identities for expectations of truncated linear functions of , under a general law rather than a density on a compact interval, including the case of an upper support end at . Second, the properties of : the paper differentiates and applies L'Hôpital's rule, which presumes more regularity than the standing assumptions give; positivity of the numerator and denominator of , the strict bounds , and the existence and uniqueness of all rest on continuity and strict increase of near . The case in part (ii) is degenerate: the argument of is then , which never attains.
The source is the authors' manuscript of 2022-06-06; theorem numbers, equation numbers and pages are the manuscript's. The model is a structure with real fields and a measure on (the law of ), with cdf P. Every theorem assumes the standing hypotheses:
The profits are Bochner integrals against , is the plain quotient of profit differences (the first expression of (14)), and conditions (12)–(13) are the payoff comparisons themselves. Defining any of these by the paper's closed forms would make the milestones definitional and is ruled out. is used only at ; is characterized as the unique positive root rather than through a junk inverse, and part (ii) is stated for . The supply-chain profit is taken at advance order , as in the proof of Proposition 1. The prior over market states and the signaling and pooling equilibria (Theorems 3–4) are outside this mission.
Mathlib provides distribution functions, Bochner and interval integrals and limits. A complete development needs layer-cake identities for and in terms of , continuity of the CDF of an absolutely continuous law, and the monotonicity and limits of interval averages of a monotone function; these are reusable well beyond this model. Proofs of any milestone, or of general lemmas they need, are welcome.
Firms in a supply chain often hold equity in one another. A retailer may own a minority stake in a supplier without controlling it: the stake is passive, but it changes what the retailer cares about, because part of the supplier's profit now accrues to her. Avinadav and Shamir (Management Science, 2023) study how such partial vertical ownership (PVO) affects two classic frictions of decentralized supply chains: the supplier's under-investment in capacity, and the retailer's incentive to distort the demand information she shares. This mission formalizes the paper's benchmark result, Theorem 1, which settles the capacity question when both firms know the market state. It is the reference point against which the paper measures every asymmetric-information equilibrium, and a companion mission treats the paper's cheap-talk result (Theorem 2).
The question belongs to the literature on capacity investment with advance orders and on cross-ownership in vertical relations; the paper's Sections 1–2 survey it. The result itself is a threshold statement of a familiar newsvendor type, but in a model where the decision maker's objective mixes her own operating profit with a fraction of her supplier's.
A supplier builds a capacity at unit cost before the selling season. After demand is realized, the retailer orders at the wholesale price and sells at the retail price , where . Here is an advance order: a quantity the retailer commits to before the supplier builds capacity, and which the supplier must cover, . Unmet demand is lost and leftovers have no value.
Demand in market state is with , where the shock has mean zero, cumulative distribution function , a density, and support with . The expected profits are
The retailer owns a share of the supplier and maximizes the accounting payoff
The relevant critical fractiles are (supplier), (retailer without holdings) and
Under complete information both firms observe . The supplier answers with the capacity , equal to if and to otherwise (5). The retailer compares two options: order nothing and accept , or order and finance the whole capacity (6)–(7).
Let
Then the minimum exists, , and for both market states
The formal goal adds that the order chosen by (7) maximizes over .
In the order the proof uses them: the closed form (2) of ; the optimality of (5); the closed form (4) of ; the §4 observation that ordering a positive quantity up to is weakly dominated by ordering nothing; the closed form, concavity and unique maximizer of (Appendix E, p. 43); the identity between the payoff gain and the expression in (9) (pp. 43–44); and Lemma E1, the existence of a unique threshold with (p. 44).
Theorem 1 says that a large enough passive stake always makes the retailer finance the entire capacity, and that full ownership is never needed: for every choice of prices, costs and demand law. The mechanism is visible in : each unit the retailer buys costs her effectively , so her preferred capacity grows with , and from on it is worth paying for. The theorem is also the benchmark for the rest of the paper: the cheap-talk, signaling and pooling equilibria of §§5–7 are compared with , and the thresholds and jointly delimit the paper's regimes.
The result is proved in the paper (Appendix E, pp. 42–44). It has not been formalized. A formal proof adds two things beyond confirmation. First, it settles a step the paper asserts without argument: that whenever , which is what forces in the second case of (8). Second, it produces reusable lemmas about newsvendor-type expectations under a general demand law with a density: the layer-cake identities behind (2)–(4) and the unique maximization of at a quantile.
The identities (2)–(4) are integration-by-parts computations, but they must be done for an arbitrary law with a density, with oriented interval integrals and without assuming bounded support. The concavity and the maximizer at require that the quantile be a genuine inverse of on .
The central difficulty is Lemma E1. The natural argument computes and observes it is positive when . That does not settle the sign of on the complementary region, where the paper argues informally that the supplier "builds a higher capacity for free". The comparison in , however, uses capacity even when , so that informal argument compares the wrong objects; a separate estimate is needed there. Differentiability of is also not given: the density need not be continuous or positive at the quantile, so the monotonicity of cannot simply be read off a derivative.
The primitives , the law of and form a structure; is Mathlib's ProbabilityTheory.cdf P, and , applied only at levels in . The payoffs are defined as Bochner integrals of the realized profits; the closed forms are milestones, not definitions. The expression of (9) is defined as printed, because Theorem 1 defines by it, and a milestone ties it to the payoff gain , which is defined with its factor . The market state is quantified as and the share as .
The standing assumptions are those of §3: is a probability measure, has mean zero and a density, with , , , and . Three implicit assumptions are added and disclosed: (otherwise and is not defined), integrability of (presupposed by "zero mean"), and strict increase of on the support (the paper uses as an inverse). The advance order ranges over , and is a hypothesis of (2) and (4).
Two trivializations are ruled out. Defining the profits by their closed forms would make the payoff milestones true by definition, so they are expectations. Replacing the rule (7) by "an arg max of " would be ill-posed, because that maximizer is not unique (for every order up to ties with ); is the two-option rule as printed, and its optimality is a separate conclusion.
Proofs of any milestone are welcome, as are general lemmas on expectations of of a shifted random variable, on quantiles of continuous strictly increasing CDFs, and on the continuity of . The source is the authors' manuscript of 2022-06-06; its proofs are in Appendix E.
In 2018 New York City's Taxi and Limousine Commission adopted a minimum earnings rule for ride-hailing drivers: each platform must pay drivers, per hour spent with a passenger, at least a target hourly earnings level divided by the platform's measured driver utilization in the previous period. The rule ties next period's wage floor to this period's idle time, so a platform that over-recruits drivers must raise wages. Asadpour, Lobel and van Ryzin (SSRN 3502607, published in Manufacturing & Service Operations Management, 2022) model this rule as a dynamical system and ask when the regulated marketplace can stay stable, meaning wages stay bounded while the platform does not lose money.
Their main result (Theorem 1, a separate mission of this series) characterizes stability in a deterministic market. Real markets are hit by demand shocks: a sudden drop in ride requests lowers utilization in one period, and the rule then forces a high wage in the next. This mission formalizes the paper's answer (Theorem 2, §4.1) to whether a platform that may not subsidize rides can absorb such a one-time shock.
Time is discrete. In each period the platform chooses a price per ride hour and a wage per ride hour. The demand is the number of ride hours requested at price ; the supply is the number of driver hours offered when drivers earn per hour. Rides served are , the utilization is , and drivers' hourly earnings solve the equilibrium condition
A price, wage and earnings sequence satisfying this in every period is an equilibrium-augmented policy. The platform's profit is . With target , the minimum earnings rule requires
The revenue and cost functions are and . The paper assumes positive, strictly decreasing and continuous; strictly increasing, continuous, and positive and differentiable away from ; unimodal with maximum at ; and demand and supply crossing at , . is the inverse of , and is the inverse of on its decreasing branch: iff and .
A shock lowers utilization to in one period. A marketplace absorbs a utilization shock (Definition 3) if some feasible equilibrium-augmented policy obeying the rule, with first post-shock wage , has bounded wages and non-negative profit in every period.
The threshold is explicit in the model primitives; no constant is chosen by the formalization.
The result. Theorem 2 quantifies the fragility of a regulated marketplace whose platform cannot cross-subsidize: there is a sharp utilization level below which a single shock sends wages into unbounded growth, and above which the platform recovers immediately with a zero-profit stationary policy. Its threshold depends on the market only through the decreasing branch of revenue and the cost of paying , which makes it a concrete design criterion for the target : a regulator choosing also chooses how deep a utilization drop the market can survive. The remark after the theorem (p. 14) relates it to the stability threshold of Theorem 1.
Formalizing it. The result is proved in the paper; no machine-checked version exists. A formal proof must close points the published argument leaves implicit: the reduction to policies (the paper's Lemma 3, posed in mission I) must hold in the all-periods form used here; the wage recursion of Lemma 4 needs wages above , which the proof does not check; and the sufficiency policy needs , which holds only because utilizations are at most one. The mission also gives the platform a second, independent use of the shared marketplace model.
The sufficiency direction is a direct check of one stationary policy. The necessity direction is where the work lies. The natural attempt, to argue that a high first wage simply cannot be paid without loss, fails: profit only requires , and a platform may raise its price along with the wage. The obstruction is dynamic. Raising the price above lowers revenue below the cost of supplying earnings , so equilibrium earnings fall below , utilization falls, and the rule raises the next wage by a factor bounded away from one. Turning this into a proof requires controlling arbitrary policies with , not just the convenient , and carrying an induction hypothesis (wages stay above ) that the paper does not state.
The Lean development lives in namespace MinEarnings.Shock. Demand and supply are functions D S : ℝ → ℝ; all regularity is required on , and "differentiable" is read as differentiable on , which is all the argument uses. " unimodal with maximum at " is strict increase on and strict decrease on . The points , and the inverse cost are parameters carrying their defining properties. Time is 0-based: Lean's period is the paper's period , so the shock constraint is a bound on Lean's first wage and the rule constrains every later wage. Bounded wages means , and profit is non-negative in every period.
Three conventions are pinned and disclosed in every statement:
The development needs only Mathlib's real analysis: monotonicity on intervals, inverse functions on , and geometric growth of sequences. The setting file is shared, up to namespace, with the other two missions of the series. Contributions welcome: proofs of the milestones, a proof of the all-periods reduction to policies, and a general lemma that a sequence with , , is unbounded.
In 2018 New York City's Taxi and Limousine Commission (TLC) imposed a minimum pay formula on the largest ride-hailing platforms, following a proposal by Parrott and Reich (2018): the pay per minute and per mile driven is divided by the platform's utilization rate, the fraction of drivers' working time spent carrying passengers. Seattle adopted a similar rule in 2020. The rule targets drivers' hourly earnings while leaving them free to choose when and how much to work. Because utilization is only observed after the fact, the regulation computes the floor for the next measurement period (six months in New York) from the utilization of the current one.
Asadpour, Lobel and van Ryzin (2022) model this rule as a dynamic system and ask when a platform can comply with it while keeping wages bounded and profits non-negative. This mission formalizes their Theorem 3: the lag in the rule does not matter for stability, because the dynamic system is stable exactly when a single static system of equations has a solution. Two companion missions of the series formalize Theorem 1 (the threshold on stable earnings targets) and Theorem 2 (absorption of a utilization shock).
Time is discrete. In period the platform charges riders a price per hour of driving and pays drivers a wage per hour of driving riders. A demand function gives the ride hours demanded at price , and a supply function gives the driver hours offered at expected hourly earnings . The regularity assumptions are that is positive, strictly decreasing and continuous, and is strictly increasing, continuous, and positive and differentiable away from zero. The ride hours produced, the utilization and the platform's profit are
Drivers earn only while busy, so earnings satisfy the equilibrium condition . The minimum earnings rule with target is
The -minimum-earnings marketplace is stable if some policy that is feasible, satisfies the equilibrium condition and obeys the rule has a bounded wage sequence and in all but finitely many periods. It is statically stable if there are and with
The statement carries only the regularity assumptions on and and .
The milestones follow the proof in the Online Appendix.
Theorem 3 reduces a question about infinite sequences to a question about one system of four relations in four unknowns. The paper uses it to give a second proof of its threshold theorem, and it shows that the lag in the regulation cannot be blamed for instability: every earnings target that a real-time rule could sustain can also be sustained under the lagged rule, and conversely. This gives regulators and platforms a criterion that can be checked by solving equations rather than by simulating policies.
The result is proved in the paper. No machine-checked version of it or of the paper's other results exists. Formalizing it checks the passage to the limit in the dynamic-to-static direction, where the paper leaves one step implicit (the positivity of the limiting utilization), and it provides a Lean model of the regulated marketplace that the other two missions of the series share.
The static-to-dynamic direction is immediate. In the other direction, a stable policy is a sequence, and a solution of (8) is a single point. Fixing one period of a stable policy does not give such a point: the rule compares with , while (8) compares with the utilization of the same point. A solution has to be extracted either from a period where the comparison happens to go the right way or from a limit. The limit is delicate because the utilization is a ratio, and a limit with would not solve (8). The positivity of the limiting utilization has to come from the rule and the bound on wages together. The reduction to policies with (Lemma 3 of the paper) also has to be carried out on the policy before the case analysis can start; that lemma is posed as a milestone of the first mission of this series and is not repeated here.
Prices, wages and earnings are real numbers, and are constrained on . A policy is a triple of sequences indexed by starting at , so Lean's period is the paper's period , and the rule constrains every wage except the first. "Bounded" is an upper bound on the wages, which are non-negative; "all but finitely many periods" is an eventually-along-atTop statement. "Differentiable" is read as differentiability on together with continuity on .
The equilibrium condition requires . Without it the encoding is trivial: if , which the assumptions allow, Lean evaluates as , the rule becomes , and every target would count as stable. For the same reason Definition 4's is kept with its strict lower bound. The paper's standing assumptions that the revenue is unimodal and that and cross are not used by Theorem 3 or its proof and are not assumed, so the formal statements are slightly more general than the paper's.
A complete development needs basic real analysis from Mathlib (monotone convergence, continuity of , and , limits of quotients) and the equilibrium construction behind Lemma 3, which uses the inverse of the cost function . That construction is reusable across the series. Proofs of the milestones, of the reduction, and of the goal are all welcome.
Non-profit organizations such as food banks run on volunteer labour. Volunteers sign up for shifts, wait on a sign-up list, work, rest, and may or may not return; the organization can spend money on engagement activities (reminders, recognition events, recruitment drives) that raise the rate at which volunteers come back or arrive. Spending too little leaves shifts unstaffed; spending too much wastes a scarce budget. Ata, Tongarlak, Lee and Field (arXiv:2312.02920, Operations Research, 2024) model this as a multiclass queueing network, pass to a heavy-traffic limit, and obtain a one-dimensional drift-rate control problem: a reflected diffusion for the scaled workload whose drift is chosen, at a cost, from an interval of feasible drifts. The optimal policy they derive is a nested threshold policy: as the workload falls below successive thresholds , one more engagement activity is switched on.
To compute that policy one needs the thresholds, and the paper obtains them from a closed-form description of the solution of the Bellman equation between consecutive thresholds. That closed form, Proposition 3 of the paper, is the goal of this mission. A companion mission formalizes Theorem 1, the existence of a solution of the same Bellman equation.
There are engagement activities. The data are a lowest drift , drift increments , per-unit-drift costs , an idleness cost rate , a mean-reversion rate and a volatility . The breakpoints are
and the feasible drifts form the interval . The engagement cost is the convex, increasing, piecewise linear function with and slope on :
Its convex conjugate is
The Bellman equation of the drift-rate control problem asks for a constant and a continuously differentiable function on with
such that , is strictly increasing, and as . Here is the optimal long-run average cost and is the derivative of the transformed relative value function of the paper's §4 (p. 20).
Put for and . Since is strictly increasing from towards , each level is attained exactly once; the thresholds are
With the standard normal cumulative distribution function, the paper defines for
For every solution of the Bellman equation and every ,
The statement fixes nothing beyond the model: it holds for any solution, with the thresholds defined from that solution.
The result. Proposition 3 turns the nested threshold policy into something computable. Evaluating at the right end of its interval and inverting gives from , so the thresholds follow by a one-dimensional recursion once is known. The paper's simulation study of a food bank (§5) uses these thresholds to set engagement policy. The result also shows that the value-function derivative, although defined through a nonlinear equation involving a supremum, is an explicit combination of Gaussian-type functions on each threshold interval.
Formalizing it. The result is proved in the paper (Online Supplement §D); no machine-checked version of it, of the conjugate formula (E9), or of the truncated Gaussian integrals (D1)–(D2) is known to exist. A formal proof checks the transcription of a long explicit formula with many constants, which is exactly where printed closed forms tend to go wrong, and produces reusable pieces: the conjugate of a convex piecewise linear function and two interval-integral identities for the normal cdf.
The Bellman equation is nonlinear in through . The obvious approach, solving it directly, fails because has no single formula. What makes it tractable is that on the argument stays in one linearity interval of ; this is a property of the solution, derived from its monotonicity and the definition of the thresholds, not a hypothesis. A complete proof must therefore combine the piecewise description of a supremum, a uniqueness argument for a linear first-order equation on a half-open interval (with the one-sided derivative at the left end and, for , an unbounded interval), and the evaluation of Gaussian integrals over finite intervals in terms of the normal cdf, matching every constant of the printed formula. The two expressions for the arguments, in and in (D1)–(D2), are equal, but the identification must be made.
All objects live in the namespace VolunteerEngage.Thresholds, Lean 4 with Mathlib.
Model; and are -indexed sequences of which the indices are used. The standing assumptions (, , , , , , ) form the predicate Standing, a hypothesis of every model-level theorem. The paper states them in the model's derivation ((15), (24), (42), (43), (50), p. 18) rather than for the abstract control problem.Cohen2019.Robust.Phi, which is Mathlib's cdf (gaussianReal 0 1). Integrals in (D1)–(D2) are oriented interval integrals of continuous functions.The source is the arXiv preprint v2 including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the Bellman equation but are not part of any formal statement; the optimality of the threshold policy (Theorem 2) is not formalized here. Proofs of any milestone, of the goal, and general lemmas on conjugates of piecewise linear functions or on Gaussian integrals over intervals are welcome.
Banks and other financial firms lose money through operational errors: mistyped trades, missed reconciliations, compliance lapses. Regulators require the firm to hold capital against these losses, and internal audit teams spend most of their effort deciding when to inspect. Two inspection schedules are common in practice: a periodic schedule (inspect every month) and a random schedule (surprise audits). A periodic schedule leaves no error undetected for long, but an employee who knows the date can relax right after an inspection and work hard only before the next one. A random schedule removes that back-loading, but leaves some errors undetected for long stretches.
Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy (SSRN 3491006; published in Management Science, DOI 10.1287/mnsc.2021.00322), model this trade-off as a principal–agent problem with moral hazard. They show that neither pure schedule dominates the other (their Proposition 4, the subject of mission I of this series), and then propose a hybrid schedule that combines them. This mission formalizes their Proposition 5: the best hybrid schedule beats the best random schedule strictly and the best periodic schedule weakly.
The source used throughout is the authors' SSRN preprint, version of July 2023. All labels (Proposition 5, Lemma 5, (EC.55), …) and page numbers are those of that version, not of the published article.
A firm (the principal) employs an agent whose errors arrive as a Poisson process with rate . Here is the agent's effort at time since the last inspection, at unit cost . Each undetected error costs the principal per unit of time until an inspection finds it. At each inspection the agent pays a penalty per error found. The principal pays a wage per unit of time and an inspection cost per inspection, earns base profit , and both parties discount at rate . The agent accepts the job only if his payoff is at least his reservation payoff . Write .
The time between two inspections is drawn independently in every cycle from a law chosen by the principal, with mean (the frequency ):
is the periodic policy and the random one.
Given a policy and a strategy , the agent chooses an effort path that maximizes his discounted payoff (1). The principal's discounted payoff is (3):
where is the agent's optimal effort and is the number of errors made by time in a cycle. The principal maximizes over subject to participation (4)–(5). Throughout, Assumption 1 holds: . The optimal payoff under policy is written .
For every inspection cost there is a payoff achievable by some hybrid policy such that
In the paper's notation, and .
Proposition 5 says that reducing the randomness of a surprise-audit schedule, in the hybrid way, strictly improves the principal's optimal payoff whatever the inspection cost. Combined with Proposition 4 it yields the paper's Corollary 1: when inspections are expensive, the optimal mix lies strictly between the two pure policies. The comparison is between optima: each policy is evaluated at its own best frequency, penalty and wage, with the agent best-responding.
The result is proved in the paper (pp. ec34–ec35); to our knowledge it has no machine-checked proof. Formalizing it requires a measure-theoretic treatment of renewal-type payoffs against three inspection laws, the agent's optimal control problem under each law, and the closed-form solution of the random policy (Proposition 1). The model layer (laws, payoffs, best response, achievable payoffs) is shared with mission I of this series.
The weak part is immediate, because the periodic policy is the hybrid policy with . The strict part is not a comparison of two closed forms: the hybrid optimum has no closed form, and the optimal mix is not computed. The random optimum itself is one of two strategies of different nature (Lemma EC.3), effort-inducing or error-correcting, and the agent's response under has a different shape from his response under (Lemma 5), so the regime boundaries of the two policies do not coincide. The naive claim that beats at every strategy is false: with zero effort, whenever (EC.55), so whether mixing helps depends on the frequency.
ProbabilityTheory.expMeasure v; the periodic law is a Dirac mass at ; the hybrid law is plus times the shifted exponential law.The goal cannot be satisfied vacuously: it asserts the existence of an achievable hybrid payoff, so an empty achievable set does not make it true.
Contributions are welcome at every level: the integral identities for the three laws (Fubini for ), the pointwise solution of the agent's problem, the two-variable optimization behind Proposition 1, and the final perturbation argument. The law lemmas and the agent's problem are reusable for any renewal-type inspection model.