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?
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.
Many optimization models in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer, . When is quadratic this is the quadratic composite problem, which also appears as the subproblem of sequential quadratic programming and of proximal Newton methods. First-order splitting methods (proximal gradient, forward-backward) handle such problems with only the proximal mapping of , but converge at best linearly. Newton-type methods converge superlinearly but classically need either smoothness or convexity of , or strong regularity (uniqueness and Lipschitz stability) of the solution.
Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research 2023) designed a Newton-type method for the stationarity inclusion of a nonconvex composite cost whose steps use only the proximal mapping and the second-order subdifferential (generalized Hessian) of , and proved local superlinear convergence under metric regularity rather than strong metric regularity. This mission formalizes that result, Theorem 7.8 of the paper, together with the chain of propositions through which it is proved.
Work in with the Euclidean inner product. A function is proper if it is finite somewhere, and prox-bounded if it is bounded below by a quadratic . The limiting subdifferential collects limits of Fréchet subgradients at nearby points with nearby values.
For a set-valued map the limiting coderivative is the set of with a limiting normal to at ; the second-order subdifferential is . is metrically regular around if near , and semismooth* at if for every in the directional coderivative .
is prox-regular at for with modulus if it is lower semicontinuous near and, for some ,
for within of , and within of ; continuously prox-regular if in addition along subgradient pairs .
The cost is with , symmetric. The proximal mapping is the argmin set of , and the forward-backward envelope (FBE) is
Algorithm 7.6 with parameter : if stop; otherwise set , pick , choose with
and set .
Let be proper, prox-bounded and continuously prox-regular at a stationary point () for with modulus , and let satisfy at : (H1) solvability of near , (H2) metric regularity, (H3) semismoothness*. Then
and every run from converges Q-superlinearly to .
The result gives a locally superlinear method for nonconvex composite problems that uses only first- and second-order information of the regularizer, and it replaces strong metric regularity, which forces isolated solutions, by metric regularity. The FBE reduction (Propositions 7.2–7.5) is reusable on its own: it identifies the stationary points, the generalized Hessian, and the regularity of a nonsmooth composite cost with those of a smooth function.
Formalizing it builds the first machine-checked library of coderivative calculus on Prove2Me: normal cones to graphs, limiting and directional coderivatives, second-order subdifferentials, metric regularity and semismoothness*. As far as the platform record shows, none of the paper's results has a machine-checked proof. The paper's proofs lean on second-order sum and chain rules from Mordukhovich's monograph and on Poliquin–Rockafellar's analysis of Moreau envelopes of prox-regular functions; those external results are part of the work.
The FBE of a nonconvex is not globally smooth; its smoothness near comes from the local single-valuedness of , which prox-regularity provides only for small and only near . The printed parameter range is too large: a far-away deep well of can capture the proximal point (see the correction below). Transferring (H1)–(H3) from to requires exact second-order calculus (sum and chain rules for coderivatives), not inclusions, and metric regularity is not preserved by the obvious estimates: the paper uses a coderivative characterization. Finally, Theorem 5.7 itself requires an inexact Newton analysis in which the Newton inclusion is solved by an arbitrary element of a coderivative, not by a matrix.
EuclideanSpace ℝ (Fin n); products carry the sup norm, which does not change any normal cone. A symmetric is a self-adjoint continuous linear operator.EReal; is assumed proper. The envelopes are EReal-valued infima; wherever is differentiated, finiteness on a neighbourhood is asserted and the real-valued function is differentiated. is the derivative of gradient f.NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric definition (2.9) for functions lower semicontinuous around the point, which covers every function the statements apply it to.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.
Reinforcement learning with a generative model (a simulator) is a basic way to measure how many samples planning needs. A learner may query, for any state , action and step , a fresh next state drawn from the unknown transition law , and must output a near-optimal policy. Model-based planning is the simplest approach: estimate each transition law by empirical frequencies, then solve the estimated model exactly by dynamic programming. It is widely used, and its sample complexity is the reference point for model-free methods.
G. Li, Y. Wei, Y. Chi and Y. Chen (arXiv:2005.12900v8; Operations Research, 2024) show that model-based planning is minimax optimal over the full range of accuracies, for discounted MDPs (Theorems 1–3) and for time-inhomogeneous finite-horizon MDPs (Theorem 4). This mission covers the finite-horizon case. Earlier model-based analyses of the finite-horizon setting, such as Yin et al. (2021), required samples per triple up to logarithmic factors before any guarantee applied; Theorem 4 needs only .
A finite-horizon MDP has a finite state space , a finite nonempty action space , a horizon , and for every step a transition kernel and a reward . The kernels may differ across steps (time inhomogeneity).
A deterministic nonstationary policy chooses action at step in state . Its value and Q-function satisfy the backward Bellman equations
so is the expected sum of rewards from step to started at , and lies in . The optimal values are and .
The generative model returns, for every triple , independent samples , all samples independent. The empirical kernel is
and the empirical MDP replaces every by , keeping the rewards. Model-based planning returns the policy obtained by backward dynamic programming on : at each step, maximizes the empirical optimal Q-function . So depends only on .
There is a universal constant such that for every finite-horizon MDP, every and every : if
then with probability at least ,
The constant is not specified, so the goal survives any improvement of constants.
The result. The total number of samples is , so Theorem 4 gives -optimal policies from samples, which matches the known lower bound up to logarithmic factors, for every . The extra factor of compared with the discounted case is the price of time inhomogeneity: each step has its own kernel to estimate. The guarantee holds from samples per triple on, instead of . Unlike the paper's discounted results, no reward perturbation or conservative action selection is needed. The step-by-step independence of the data makes the plain planner analyzable.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically, and no machine-checked proof of it is known. A formalization checks the details the paper leaves implicit: the index ranges of the backward recursions, the use of as an integer, the sample-size condition of Lemma 9 when it is applied to the planner's policy, and the independence argument that lets a data-dependent policy enjoy fixed-policy concentration. The finite-horizon layer here (time-inhomogeneous kernels, backward propagation, the DP planner, the empirical kernel and the finite law of the data) is reusable by other finite-horizon sample-complexity results.
The planner's policy is built from the same data that define , so the obvious route, applying a concentration inequality to as if were fixed, is not justified by itself. The argument has to use the backward structure: the step- quantities depend only on the data of later steps, which are independent of .
A second difficulty is the sample-size range. A Hoeffding-type bound on each one-step error, summed over steps, gives an accuracy that only becomes meaningful when . Reaching requires Bernstein-type bounds and the control of a whole sequence of auxiliary value vectors , of which Lemma 12 bounds the size. Lemma 9 then has to close the recursion in after about levels.
Fin H, 0-based: the paper's step is Lean's . Backward propagation returns at every index , which encodes . The paper's ranges in (63) and (66) are written h.val + 1 < H.sel (any argmax rule), fixed before the data and quantified outside the probability. Empirical Q-values tie with positive probability, and the proof needs to be a fixed function of the empirical kernels.Trivializing formalizations are ruled out: the planner is computed from the empirical kernels, not from the true ; the model is time-inhomogeneous, with one kernel per step; and cannot depend on , , or the MDP.
The only external definition is the published FoundationsML.ReinforcementLearning.IsTransitionKernel. A complete development needs Bernstein's inequality for bounded i.i.d. averages (on finite product laws), a union bound, and the independence of the per-step data. Contributions are welcome on all six milestones and on general lemmas about the finite law of the data, such as independence across steps and the distribution of .
When one agent breaches a contract, the breach often forces its counterparty to breach its own contracts in turn, and the losses propagate. Supply chains are the standard example: a supplier that fails to deliver makes its customer fail to deliver to its own customers. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss of such a cascade should be shared among the agents involved. Their aim is a rule simple enough to be written into a smart contract that settles disputes automatically. They first treat a single chain of agents and characterize the fixed-fraction rules by four axioms (Theorem 1). Section 5 then extends the model to loss trees, in which one agent may cause losses to several others, as when a firm supplies several downstream firms. Theorem 4 shows that the same four axioms, suitably extended, characterize the fixed-fraction rules on trees. This mission formalizes Theorem 4 and the steps of its proof in Appendix A.
The tree model follows a line of work on sharing liability and costs along hierarchies and networks; the paper compares its setting with Oishi, van der Laan and van den Brink (2023).
Agents are natural numbers. An edge records that agent causes a loss to agent . A finite edge set covers the vertices . It is a tree if it has a root (a vertex with no incoming edge) and every other vertex has exactly one incoming edge and is reached from the root. The root is the initiator of the cascade. Leaves are victims only. The agents who share the losses are the non-leaf vertices . A loss is a function on edges, and the total loss is .
A rule assigns a liability to each agent . Liabilities are non-negative and sum to . A rule is required to be invariant to agent labels: renaming the agents by a bijection of renames the liabilities. It is also continuous along as , the paper's standing assumption.
The fixed-fraction rule with parameter makes each agent pay the fraction of the losses it causes directly. The root also pays the remaining fraction of the total:
The elementary tree problem is the chain with a unit loss on its last edge. For a vertex , is the set of edges on the path from the root to , is the number of vertices on that path, and is the subtree rooted at .
The four axioms are as follows.
For every rule on loss trees,
Theorem 4 says that the axioms which single out the fixed-fraction rules on chains still single them out on trees, with nothing added. Because the rule only needs each agent's direct losses and the identity of the initiator, it can be computed locally. This is what the paper uses to implement liability sharing in a smart contract (Section 6, Figure 3). The characterization also justifies applying the rule to supply networks, where firms supply several customers, rather than only to chains.
The paper's proof of Theorem 4 is a short sketch: it reduces trees to chains by trimming and relabelling, then cites the chain argument. No machine-checked version of any part of the paper exists. Formalizing it would check the reduction in full, including the bookkeeping that the printed proof compresses. While preparing this mission, three places where the printed text differs from what the argument establishes were found; they are corrected here (see Formalization scope). The tree machinery built here (paths, depths, subtrees, relabelling of finite rooted trees over ) is reusable for other liability and cost-sharing models on hierarchies.
The obvious argument works edge by edge: use additivity to isolate one edge, use zero truncation to cut the tree down to the path through that edge, then relabel the path into a chain. The first gap is that additivity yields only rational homogeneity. Continuity, or the monotonicity that additivity and non-negativity give, is needed for real multiples. The second is that zero truncation only adds or removes leaf edges, so trimming must proceed leaf by leaf, keeping a tree at every step. It must also be shown that agents removed from the tree carried no liability, which needs balance and non-negativity. The third is that relabelling requires a bijection of all of that maps the path onto , together with a loss on the relabelled tree. Label invariance must hold for every such loss, not only one chosen extension. Finally, the chain part (Proposition 2) pins down by an induction that chains population-monotonicity inequalities with merging proofness.
Trees are Finset (ℕ × ℕ) with the root, unique-parent and reachability conditions above. Vertex labels keep the paper's numbering ( uses ); Lean's also contains , which label invariance makes harmless. A rule is a function φ T ℓ i on all edge sets, real functions and naturals. Every axiom and every conclusion is quantified only over trees, non-negative losses and agents . The conclusion is equality at those arguments. A function equality would be false, since a rule's other values are arbitrary. The rule conditions (non-negativity, balance, label invariance, continuity) are a hypothesis of every statement. Dropping them makes Theorem 4 false: the parameter need not lie in , and a rule need not respect the tree's labels. The root of is detected as the vertex with no incoming edge, never hard-coded as label 1.
Three disclosed departures from the printed text:
Continuity is taken from Section 2, where it is standing; the proof of Proposition 3 invokes it. A complete development needs finite rooted trees over , reachability (Relation.ReflTransGen), the extension of a finite injection to a permutation of , and leaf-by-leaf induction on trees. Proofs of any milestone are welcome, as are alternative routes to Theorem 4, for example through monotonicity instead of continuity.
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.
In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.
No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a -matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor . This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.
Matrices are rational. For integers a matrix is a -matrix, written , if every off-diagonal entry is nonpositive and every column sum is nonnegative:
For a non-square matrix the diagonal entries are the with . Square -matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.
is the set of rational matrices with at most one positive and at most one negative entry in every row. A system with is a monotone two-variable-per-inequality system (M2VPI).
For and with , the polyhedron of interest is
Write for the number of nonzero entries of , for , and
In §7 the right-hand side is called instead of , and .
The proof works with a square with positive diagonal. Its digraph has an arc whenever . is the set of vertices reachable from (including ), and is the submatrix of the rows , . The vertices split into (at most one outgoing arc), (at least two arcs and ) and (at least two arcs and ).
For with and nonzero entries, and with , there are , and with
Theorem 6.4 turns an LP over a constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor . In the exchange-market algorithm , so the starting prices of each phase come within a factor of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form over with a -matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.
The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on -matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.
The obvious approach, deleting all but two variables from each inequality of , fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc of , as a nonnegative combination of the inequalities . Finding it requires an ordering of in which every vertex but has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment is the hard direction. It splits by whether the rows on are linearly independent () or not (), and the case needs the extra constraint and the comparison of entries of the elimination multipliers in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.
Indices are 0-based (Fin k, Fin t); the paper's . Matrices , and right-hand sides , , are rational (ℚ), as on p. 15, and act on real vectors through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. is the image . is defined for only, and every statement using it assumes (resp. ).
Not formalized: the running time and the polynomial bound on the encoding size of , in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 (; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.
Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is " form would be nearly trivial, since satisfies all but one clause. In the goal, must have at most one positive and at most one negative entry per row, and . Dropping either requirement makes the goal weaker than the paper's theorem.
, defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the -th entry of , a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for , where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.
A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any -matrix. Contributions are welcome on any milestone, on the reduction from rectangular to the square positive-diagonal case, and on the two containments of the reduced case.
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.Fair division asks how to share a resource among agents with different preferences so that each agent can be promised a minimum level of welfare, whatever the preferences of the others. Classical cake cutting treats a good cake, valued additively or at least monotonically. Many real problems mix goods and bads: a plot of land with both fertile and polluted parts, a set of chores some of which are welcome, a workload whose value first rises and then falls with its size. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research 2023) study the most general non-atomic model, in which a utility is only required to be continuous and bounded, and ask which utility levels can be guaranteed simultaneously to all agents.
Their first main result is that Kuhn's -person Divide & Choose rule (Kuhn 1967) guarantees each agent her minMax utility, in this full generality. The key ingredient is an equipartition theorem of Avvakumov and Karasev ([4]), which lets the current divider cut any piece into equally valued parts even when the utility is neither monotone nor of constant sign.
The manna is a bounded Lebesgue-measurable subset of , , with ; is Lebesgue measure. A share is a measurable subset , possibly empty. For a share , an -partition is an -tuple of shares with and for . The pseudo-metric on shares is , the measure of the symmetric difference.
A utility assigns a real number to each share, with , and is bounded and continuous for . The set of utilities is . Nothing else is assumed: may increase or decrease with the share and may take both signs.
An -equipartition of a share for is a partition whose parts all have the same utility ; their set is . The two benchmarks are
minMax is what an agent gets choosing first from the worst partition for her; Maxmin is what she gets choosing last from the best one.
In the D&C rule the agents are ordered . At each step the first remaining agent, the Divider, proposes an -partition of the remaining manna among the remaining agents. Every other remaining agent reports which shares she likes (at least one); the Divider likes all of them. A set of agents is properly matched to a set of shares when they are matched one-to-one to liked shares and no other remaining agent likes any of those shares. The largest properly matchable set of agents is served; the other shares return to the manna, and the rule continues with the unserved agents.
An agent with utility follows the minMax strategy when, as Divider, she proposes an equipartition , and, as chooser, she likes exactly the shares with , the level of the initial problem. Then, whatever the other agents do,
The equipartition theorem of [4] on ; Lemma 1, for every share and every ; Lemma 2, existence of a largest properly matchable set containing the Divider; and the three steps of the proof of Theorem 1 i): the invariant that previously assigned shares are worth less than minMax to an unserved agent, the chooser step and the Divider step.
Proposition 1 iii), for every , and the statement that is a Fair Guarantee in : every profile admits with for all (Definition 3).
Maxmin is an upper bound on any Fair Guarantee, and in the mixed-manna domain it is not itself a Fair Guarantee. Theorem 1 establishes minMax as a guarantee that holds on the whole domain, is implemented by a simple decentralised protocol, and requires no knowledge of the other agents' preferences. Together with the companion results it brackets what can be promised to every agent in non-atomic division with arbitrary continuous preferences.
The result is proved in the paper; nothing in this mission is open mathematics. None of it is machine-checked. The formalization adds a non-atomic fair-division layer (shares up to null sets, -continuous utilities, equipartitions, minMax and Maxmin) and a precise model of a sequential division protocol in which the other agents' behaviour is quantified over, rather than fixed. The goal also makes explicit the step the informal proof passes over quickly: the minMax strategy is always a legal move.
Once the protocol is modelled, the guarantee is an invariant argument over the steps of a play. The difficulty is Lemma 1. For an additive utility, Lyapunov's theorem gives equipartitions; for a utility of constant sign, the Knaster–Kuratowski–Mazurkiewicz lemma does (Remark 1). A utility that takes both signs defeats both arguments, and an obvious intermediate-value argument handles only . The paper reduces Lemma 1, through a moving knife, to the interval theorem of Avvakumov and Karasev, whose proof is topological (mapping degree). Mathlib has neither that theorem nor the degree theory it uses. Lemma 2 needs the Gallai–Edmonds decomposition of a bipartite graph, which Mathlib does not have either; Hall's theorem is available.
The space is EuclideanSpace ℝ (Fin d) with volume, and every statement that needs non-atomicity assumes (on , a point of measure , Lemma 1 fails). A utility is a function on all subsets, but every condition is imposed on shares only. Partitions are indexed by Fin n, have union exactly the share and null pairwise overlaps; disjointness is not required. minMax and Maxmin are real sInf/sSup; every statement using them assumes , which makes the defining sets nonempty and bounded. Agents are Fin n, the Divider is the least remaining agent, and a play is a list of steps, each recording the remaining agents and manna, the proposed partition, all reports and the assignment. A step is admissible exactly as Definition 4 requires, including that the served set is the largest properly matchable one.
The following formalizations would trivialize the goal and are ruled out: fixing the other agents' behaviour; accepting against the minMax of the remaining manna instead of the initial one; assuming the utility monotone, additive or of constant sign; defining minMax as a minimum over a possibly empty set; and omitting the availability parts 1–2, which would make Lemma 1 irrelevant.
A complete development needs the interval equipartition theorem (a topological result of independent interest), moving knives through a measurable set, a Gallai–Edmonds-type argument for bipartite graphs, and the invariant over plays. The non-atomic model and the equipartition lemmas are reusable for the Moving Knife and Bid & Choose rules of the companion mission. Proofs of any milestone, alternative proofs of Lemma 1 for special classes of utilities, and the run-level lemmas are all welcome.
A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).
The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.
There are products with mean production times and holding, backorder and outsourcing cost rates . A symmetric positive definite matrix describes the curvature of the revenue rate. Write and
The drift cost and the effective holding cost are
Let be a Brownian motion with drift and variance , started at , with respect to a filtration . An admissible control consists of a progressively measurable drift rate and nondecreasing, right-continuous, adapted processes (effective outsourcing) and (idleness) with . The workload is
and admissibility also requires . The equivalent workload formulation (EWF) is to minimize
A barrier policy with barriers keeps in , increases only when and only when .
For put and . Let solve the Riccati equation
and solve on with . The paper's is the unique with ; pastes and at , and the candidate drift is .
For every filtered probability space carrying such a Brownian motion,
where is the expected cumulative cost in (29). The constant is the paper's construction, not a parameter.
The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes computable by line search.
The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.
The optimality half of Theorem 1 is a verification argument: apply Itô's formula to for an arbitrary admissible control with jumps in and , use the Bellman inequality pointwise, and control with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.
The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every and passing , fails: the solutions blow up in finite time, so exist only for in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at .
Time is indexed by and only matters. The Brownian motion is defined locally (drift, variance, start at , independence of increments from the filtration). Expected costs are computed in , so a control with infinite cost counts as . The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of and , jumps included. Derivatives at the barriers are one-sided; and up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in , (37), (40)) are stated as attained.
Standing assumptions added to every statement, all implicit in the paper: ; ; symmetric positive definite; , ; starts at ; right-continuous; progressively measurable with locally integrable paths; in the Bellman equations.
Corrected statements. Lemmas 18–20 are printed for solutions on , which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that exist for every is replaced by uniqueness, solvability at and order-connectedness of the solvability sets. Lemma 4's limits as become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.
Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.
, , and are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.
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.
Many problems in optimization reduce to a subgradient inclusion : for a smooth this is the gradient equation , and for an extended-real-valued (a smooth loss plus an indicator or a nonsmooth regularizer) it is the first-order optimality condition of a composite problem. Newton's method is the classical way to solve such equations with a superlinear rate, but its textbook form needs and a nonsingular Hessian. Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023) design a Newton-type method in which the Hessian is replaced by Mordukhovich's second-order subdifferential , and prove local superlinear convergence under two assumptions that are weaker than the usual ones: metric regularity (instead of strong metric regularity or tilt stability) and the semismooth* property of Gfrerer and Outrata.
Timeline of the ingredients:
Let be proper. Its limiting subdifferential collects the limits of Fréchet subgradients at points with . For a set , the regular normal cone contains the vectors with for ; the limiting normal cone contains the limits of regular normals at nearby points. For a set-valued , the coderivative is , and the second-order subdifferential is .
The function is prox-regular at for with modulus if it is l.s.c. around and, for some , whenever lie within of , and lies within of . It is continuously prox-regular if, in addition, along every with . It is prox-bounded if it is bounded below by a quadratic function.
For , the Moreau envelope and proximal mapping are
Algorithm 6.2 starts at . While it sets , picks any with , and moves to .
The standing assumptions at a solution are:
If is proper, prox-bounded, continuously prox-regular at for with constants , and (H1)–(H3) hold, then
The result gives a Newton method for nonsmooth, nonconvex subgradient inclusions whose convergence does not require strong metric regularity. Example 5.2 of the paper exhibits a function whose gradient is metrically regular and semismooth* but not strongly metrically regular, so the theorem covers solutions that earlier generalized Newton theories exclude. Through the Moreau envelope, the method reduces to a gradient equation; the same reduction, with the forward–backward envelope, drives the paper's composite algorithm (the companion mission) and its applications to Lasso-type problems.
The paper's results are proved on paper; none of them, nor the underlying theory of coderivatives, second-order subdifferentials or semismooth* maps, is formalized in Mathlib. This mission produces a machine-checked development of that layer and of the convergence theorem. It also fixes a defect: as printed, Lemma 6.3 and Theorem 6.6 claim their conclusions for every , which is false (see Formalization scope); the formal statements are the corrected ones.
The obvious argument says "Algorithm 6.2 is Algorithm 5.3 for , so apply Theorem 5.7". Each step of that sentence carries the difficulty. Transferring (H1)–(H3) from to requires the coderivative of the inverse , which needs a local graphical calculus for limiting normals that Mathlib does not have. The property of the envelope and single-valuedness of the proximal map hold only for small and near : prox-regularity is local while minimizes globally, so a far-away deep well can capture the proximal point. Theorem 5.7 itself rests on a uniform coderivative bound from metric regularity (Lemma 5.4, a pointwise-to-uniform form of the Mordukhovich coderivative criterion) and on the semismooth* estimate (Lemma 5.5), which combines directional normal cones with the symmetry of generalized Hessians.
EuclideanSpace ℝ (Fin n); definitions are stated on real inner product spaces, and carries the sup norm (the cones are norm-independent).NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric (2.9) for functions l.s.c. around the point, which covers every function is applied to here.EReal and is assumed proper; the envelope is EReal-valued, and finiteness is asserted wherever it is differentiated.Classical.choose; and is not specialized (no convexity, which would make ; no ; no strong metric regularity; no assumption that is a minimizer).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.
An insurer that pays dividends to its shareholders faces a trade-off studied since de Finetti (1957): paying out surplus early raises the discounted payout but brings ruin closer. Reinsurance changes the trade-off, because ceding part of each claim lowers the volatility of the surplus at the price of a reinsurance premium. When the insurer may choose both the dividend stream and, at every moment, an arbitrary reinsurance contract, the problem becomes a mixed singular–classical stochastic control problem. Most of the literature treats it on an infinite horizon, where the value function solves an ordinary differential equation. On a finite horizon the value function also depends on time to maturity, the Hamilton–Jacobi–Bellman (HJB) equation becomes a parabolic variational inequality with a gradient constraint, and neither its solvability nor the regularity of its solution is classical.
Guan, Xu and Zhou (arXiv:2008.00391v3, Mathematics of Operations Research, 2023) show by PDE methods that this variational inequality has a classical solution, identify it with the value function, and read the optimal reinsurance contract and dividend barrier off its derivatives. This mission formalizes the PDE part: Theorem 3.1 and the steps of Appendix A that lead to it.
Claims are nonnegative random variables with common distribution function , , possibly discontinuous. The paper assumes the tail condition
so the moments and are finite. The other data are the net reinsurance loading , the discount factor and the horizon ; the mission assumes throughout.
A reinsurance contract is described by the retained loss the insurer keeps out of a claim of size , with ; is the set of such functions. For a function of the surplus and the time to maturity the operator
is the generator of the controlled diffusion approximation of the surplus. The HJB equation is the variational inequality, on ,
The functions
with and for , compute the supremum in (3.2), and has a unique root . The penalized gradient problem (A.17) on is
with , a penalty function and a boundary datum that ramps from down to on .
There is a unique that solves (3.1) and satisfies
Uniqueness is among solutions in the same class with the same six properties, as equality on .
Theorem 3.1 is the analytic core of the paper. The verification theorem (Theorem 3.2) needs a classical solution that is increasing and concave in , which Theorem 3.1 provides, and Section 4 derives the shape of the optimal policy from (3.4)–(3.9): the optimal retained loss is , and (3.9) bounds the reinsurance barrier away from zero. Without the existence of a classical solution, the HJB equation could only be interpreted in the viscosity sense, whose uniqueness theory for this mixed singular–classical problem is not available, and the strategies would not be well defined.
The result is proved in the paper; nothing in it has been machine-checked. A formal development would produce, beyond the theorem, a reusable formal treatment of a parabolic obstacle problem with a Robin boundary condition through penalization, comparison principles for quasilinear parabolic equations, and the explicit reduction of a supremum over reinsurance contracts against an arbitrary claim distribution. The appendix lemmas (A.7)–(A.13) and Lemma A.1 are elementary real analysis and are self-contained targets.
The supremum in is over a function space and may have atoms, so even the closed form (A.10) and the everywhere-differentiability of require care with one-sided derivatives at the jumps of . The operator is fully nonlinear and degenerates as , since . The inequality carries a gradient constraint rather than an obstacle, and the left boundary condition is incompatible with the initial condition at the corner , which is why the solution is only claimed to be away from that corner. The obvious route, solving (3.1) directly by a fixed-point argument, does not control ; the paper differentiates in and works with the gradient , which turns the gradient constraint into an obstacle but introduces the Robin condition with the wrong sign for a direct maximum principle. The passage needs and Hölder estimates uniform in , which are not in Mathlib.
ℝ → ℝ → ℝ; is time to maturity. Partial derivatives are explicit functions tied to by HasDerivAt on sections at interior points (, ) and continuous on ; boundary values are these continuous extensions, and (3.1) holds at through them.deriv evaluated at boundary points, or uniqueness is stated as equality of functions on all of , would trivialize or falsify the goal; the statements avoid all three.Needed infrastructure: interval integrals of monotone functions and their one-sided derivatives, maximum and comparison principles for linear and quasilinear parabolic equations in one space dimension, existence for quasilinear parabolic problems (Leray–Schauder with Schauder estimates), and compactness in Hölder and Sobolev spaces. The parabolic comparison principle and the penalization scheme are reusable well beyond this mission. Proofs of individual milestones, in particular the elementary ones (A.7)–(A.13) and Lemma A.1, are welcome independently.
An insurance company pays out dividends to its shareholders and buys reinsurance to limit its exposure to large claims. Both decisions are dynamic: the right amount to cede and the right moment to pay depend on the current surplus and on the time left until a fixed maturity . Guan, Xu and Zhou (2023) solve the combined problem for a diffusion-approximated surplus with a general claim distribution, a general reinsurance contract (any retained-loss function ), and a finite horizon. Their main structural output is a description of the optimal strategy by free boundaries in the surplus–time plane: a dividend barrier , and for each claim size a reinsurance barrier .
A companion mission formalizes the existence and uniqueness of the classical solution of the HJB variational inequality (Theorem 3.1 of the paper). This mission takes that solution as given and formalizes the shape of the boundaries (Section 4 of the paper), culminating in the description of the reinsurance boundaries for discrete claim distributions (Theorem 4.5).
Claims are i.i.d. copies of a nonnegative random variable with distribution function , satisfying the tail condition that is bounded on . Write and . The reinsurance loading is , the discount rate , the horizon , and throughout (for the problem is trivial).
The value function , with the surplus and the time to maturity, is the solution of the variational inequality
where
It is the unique function of class that solves this inequality and satisfies , , , nondecreasing in , nondecreasing in , and . Here is the unique positive root of
The no-dividend region is , and the dividend boundary is
For a claim of size the optimal retained loss is if and otherwise, and the ceded loss is the difference from . The reinsurance boundary is . For a discrete law with , the -th reinsurance boundary is
For a discrete claim law, every is continuously differentiable on , and for every :
where is the smallest atom above .
The theorems turn an existence result for a fully nonlinear variational inequality into a usable description of the optimal policy. Claims below are never reinsured; a claim of size is partly ceded only when the surplus lies below a barrier that starts at the origin at maturity, stays below , and stays below the dividend barrier, which is itself bounded by an explicit constant independent of the horizon. For discrete claims the barriers are smooth, ordered, and separated by gaps of at most . The quantity , the optimal retention level, is shown to grow at rate at least in the surplus; this single monotonicity estimate is what makes the regions of the surplus–time plane ordered and nonoverlapping.
The results are proved in the paper; none of them, nor Theorem 3.1 on which they rest, has a machine-checked proof. Formalizing them requires the parabolic regularity statements of Lemma 4.3 (the paper's proof invokes interior Schauder estimates) and the implicit function theorem in a form that gives one-variable dependence of a level set. Statements of the boundary properties in this mission are posed for any function with the properties of Theorem 3.1, so they can be proved independently of the companion mission.
Most of the elementary statements reduce to a sign or a monotonicity property of , and the first idea is to differentiate the equation. That requires and to exist as classical derivatives in , which the class of Theorem 3.1 does not provide: it gives only two -derivatives and one -derivative, and a weak monotonicity of . Lemma 4.3's interior regularity is therefore not a formality but the gateway to Lemma 4.4, and its proof uses Hölder estimates for linear parabolic equations, which are not available in Mathlib.
The positivity and the limit are statements about the free boundary itself, not about at fixed points, and need the uniqueness part of Theorem 3.1 or a comparison argument. The strict inequalities in (4.13)–(4.14) need more than the bound as stated.
All objects live in the namespace DynReinsDiv.Barriers. Conventions:
μ on with ; ; no density is assumed. are Bochner integrals, finite under the tail condition. The standing hypothesis is a field of the model.vx vxx vt are explicit functions: they are HasDerivAt derivatives of the sections at interior points (, ) and continuous on ; boundary values (at and ) are the continuous extensions. " in the weak sense" is monotonicity of in , "" is monotonicity of in .IsTheorem31Solution. The milestone conclusions (, the bounds on , ) are never hypotheses; with them as hypotheses Theorem 4.5 would be a short mean-value argument.Fin N from . The paper's index is replaced by conditions on and , which also cover laws whose atoms all lie below .Contributions welcome: the interior regularity of Lemma 4.3, the monotonicity estimate (4.10), and the derivation of Theorem 4.5 from the milestones.