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?
Firms can raise money before production by selling claims on future output. In the model of Malinova and Park, these claims are tokens: a buyer prepays for a quantity of the good, and the final contract also gives token holders a share of tokens issued after demand becomes known. The firm must choose how many tokens to pre-sell. A larger pre-sale brings in more finance but changes the allocation of later sales revenue. The paper identifies contract terms that preserve the firm's monopoly output choice and determines the pre-sale quantity by investors' break-even condition (Proposition 3, p. 24). Proposition 4 asks how that quantity responds when financing need, production cost, or expected demand changes. These comparative statics make the contract's financing response explicit rather than leaving the break-even equation as an isolated root.
An entrepreneur pays a set-up cost to launch production and then incurs a marginal cost per unit. After financing, a demand intercept is drawn uniformly from , where . At output , the inverse demand price is . Without financing distortions, the monopoly quantity is and its profit is . For a realized payoff , expectation means the average . The venture's net present value is , equal in this domain to (equation (3), p. 14).
Under the optimal token contract of Proposition 3, investors buy tokens at time zero, and token holders receive the fraction of new tokens issued when output exceeds the pre-sale. A refund rule applies when output falls below the pre-sale. The resulting positive break-even pre-sale size is determined by equation (16):
For a positive-NPV venture, this equation has one positive root, in (Appendix A, pp. 40–41). The mission treats the root as a solution of the equation, so statements about the optimal quantity apply to every value satisfying it.
Proposition 4, p. 25, asserts three strict directions. If denotes the unique positive root of (16), then, while both endpoint ventures have positive NPV,
Thus a larger set-up cost or marginal cost requires more pre-sold tokens, while a higher demand level requires fewer. The Lean goal compares arbitrary positive roots directly. It places the NPV condition at the higher cost in the second comparison and at the lower demand level in the third; these are the restrictive endpoints. The first comparison places it at the higher set-up cost.
The milestone list follows the Appendix A proof: existence and uniqueness of the root of (41); the negative derivative (42); the positive derivative (45); the negative derivative (46); and the derivative in of the expression in (46), equation (47). These are source claims, with their displayed constants retained. Equation (42) and equation (45) contain printing errors in the SSRN copy; the formal statements use the actual derivatives and the milestone quotes retain the printed text.
Proposition 3 establishes that the chosen token contract can finance a positive-NPV venture while keeping the efficient monopoly output. Proposition 4 then describes the contract's response to the model's three principal parameters. Its strict inequalities distinguish an actual response from a weak monotonicity claim that could allow the pre-sale to remain unchanged. The demand comparative static is economically specific: a higher raises the demand intercept on average, but the quantity of tokens needed to finance the same set-up cost falls.
The paper proves these results analytically. This mission seeks machine-checked proofs of the root comparison and its stated derivative milestones. A completed development would provide reusable results about parameter-dependent roots of rational functions, especially when the root is specified by a break-even condition rather than by an explicit formula. The current Lean files are compiled statements with proof placeholders; compilation does not establish the mathematical results.
Equation (16) is cubic in a quantity that also occurs in a denominator, so the root does not offer a convenient closed expression for direct comparison. The endpoint restrictions matter: the meaningful root lies strictly between zero and , and derivatives that have the desired sign in that interval need not keep the same sign outside it. In particular, the derivative in (42) reaches zero at the upper boundary. The demand derivative in (46) also vanishes at , making its strict sign in the interior a separate claim. A literal transcription of two printed derivatives would give incorrect equalities even though their intended sign conclusions survive. The formal development therefore needs both careful domain control and the corrected expressions.
The namespace TokenFinance.Statics represents all quantities as real functions. Uniform expectation is the interval integral divided by . Monopoly output and profit use max to encode zero production below cost. The common Setting definition file also records the equity and debt payoffs and the token contract's case split, following the series-wide model. The break-even condition is exactly the closed-form equation (16), while NPV remains the integral of realized monopoly profit minus . The goal assumes the paper's standing , , , and positive NPV, written as using equation (3). Derivative statements state their own regions and nonzero-denominator conditions. The token size is quantified over positive roots rather than chosen by an arbitrary selection function.
The root cannot be defined to have the claimed monotonicity, and the derivative signs cannot be inserted as hypotheses of the goal. The missing work includes real-variable derivative calculations, root existence and uniqueness on the economic interval, and the strict parameter comparisons. The secondary token market, redemption mechanics beyond the contract payoffs, bankruptcy costs, consumer welfare, and the paper's institutional discussion are outside this mission's scope.
A reinforcement-learning agent chooses actions while learning how those actions affect future states. In a stationary model, observations collected long ago remain relevant to the current transition law. In a nonstationary Markov decision process, rewards and transition probabilities may change at each round. Old observations can then bias an estimate even when the agent has collected many samples. The challenge is to keep learning from recent observations without becoming blind to actions that the agent has not tried recently. Cheung, Simchi-Levi and Zhu study this tension for finite-state average-reward learning and introduce confidence widening in their SWUCRL2-CW algorithm Cheung et al., §4.
The paper's broad regret theorems suppress constants inside asymptotic notation. Proposition 2 gives an explicit one-round inequality that exposes the roles of estimation error, temporal variation, confidence widening, and the diameter of a plausible transition model. This mission targets that proposition and the stated auxiliary results used around it Cheung et al., pp. 14, 38–41.
Let be a finite state set. Each state has a nonempty finite set of permitted actions. At round , taking action in state gives expected reward and moves to state with probability . The one-step variation is the greatest change over permitted pairs; is the corresponding greatest distance between transition rows. These definitions make no stationarity assumption Cheung et al., pp. 6, 33.
At the start of an episode, the algorithm counts visits to each pair in a recent window of length . It divides empirical sums by , where is the visit count. Thus an unvisited pair has estimated reward and transition vector equal to zero. Reward confidence sets lie in ; transition confidence sets lie in the probability simplex and use an radius enlarged by a nonnegative parameter . Write and for their respective radii. The algorithm chooses a stationary policy and an optimistic model, gain , and bias from extended value iteration Cheung et al., pp. 11–13.
The diameter of a transition model is the largest, over ordered source and target states, of the smallest expected number of transitions needed to reach the target under a stationary policy. Source equal to target means a return time after at least one transition. The round- optimal gain is the value of the stationary occupancy-measure linear program for with only permitted actions. From the window's first round through the round before , let and be the sums of the corresponding one-step variations Cheung et al., pp. 8, 14, 33.
The main target is Proposition 2. Condition on the local reward and transition estimation events at . Assume that the widened transition confidence sets contain every permitted row of an MDP of diameter at most . For a round in which , the target is
The five milestones are the paper's Lemmas 2–5 and displayed inequality (32): a dual-bias span bound, a drift estimate for window averages, bounded optimistic bias, optimism under drift, and a transition-value error bound. Their exact constants are part of the targets Cheung et al., pp. 33, 38–39.
Proposition 2 separates the per-round change in optimal gain from the cost of the current action. Its first term tracks changes in the optimistic bias along transitions; the other terms identify window drift, reward and transition estimation, and widening. This decomposition can be summed across episodes when analyzing the algorithm. The result has a concrete role even though the later horizon-wide theorem is given in asymptotic notation Cheung et al., pp. 14, 41.
The paper proves these claims mathematically. The mission asks for machine-checked proofs of the explicit statements and for reusable definitions of finite nonstationary MDP variation, window estimators, confidence sets, occupancy gain, and hitting-time diameter. The source's Theorems 1–4 are not posed here: their displayed bounds hide constants in and, in one case, use an unspecified failure probability Cheung et al., pp. 14–25. This proposal supplies statements for solvers; it does not claim that these new statements already have machine-checked proofs.
The current model need not resemble the model that generated every observation in the window. A direct stationary confidence argument cannot control the resulting temporal error. The challenge is especially visible at a pair with no recent visits: its comparison transition vector is zero, although a genuine transition row has total mass one. The paper's Lemma 3, read literally for every pair, fails in that case. The mission states its positive-count condition explicitly while keeping the proposition and the later optimism and transition milestones valid at unvisited pairs Cheung et al., pp. 12, 38–40.
There is a separate issue with the printed dual-bias lemma. Feasibility alone permits an arbitrarily large dual gain and does not force the asserted span bound. The mission adds to Lemma 2 and records the change for audit. The EVI output is represented by its selected-model membership, bias normalization, optimism, and near-optimality properties; this is the contract stated for the algorithm's output, rather than a formal execution of extended value iteration Cheung et al., pp. 13, 33, 35–36.
States and ambient actions are Fin S and Fin A; permitted actions are state-dependent finite subsets. The setup has , , , and a nonempty action set at each state. Time is zero-based in Lean, while the paper's rounds are one-based; in particular its is represented by . Counts and confidence sets are evaluated at the episode start. Variations continue up to the target round. The estimation events are assumed at the episode start, which is the only time used by these statements.
Hitting times and diameter take values in extended nonnegative reals, so an unreachable target does not acquire a false finite diameter. The diameter includes return times and minimizes over deterministic stationary policies. The confidence-radius product counts actual permitted pairs. At an unvisited pair, the comparison averages remain zero and ; the large confidence radii under the stated bounds are essential. The local transition event uses the error condition: literal membership of the zero comparison vector in a simplex would make the paper's event fail. The printed coordinatewise maxima in Property 1 imply the standard joint-distribution optimism condition used here. The free printed in the last radius of Proposition 2 means , as the proof's context confirms Cheung et al., pp. 12, 14, 36, 40–41.
Two milestones carry a pinned hypothesis because the printed statement is false without it: Lemma 2 assumes the dual gain satisfies (an arbitrary feasible can make the bias span exceed ), and Lemma 3 assumes the pair was visited in the episode-start window (at an unvisited pair the comparison averages are zero). Proposition 2 is stated for every round before the horizon at which the action is the episode policy's choice, which covers the rounds of episode ; the coefficient of is kept as printed.
The witness MDP has genuine probability rows in the widened sets and a diameter bound. The EVI tuple obeys both stated properties, and the chosen action obeys its policy. These conditions prevent an unconstrained bias, a spurious zero diameter, a confidence event at the wrong time, or a reward bound for an unrelated action. The published FiniteMDPLearning model supplies probability rows and rewards in ; its different travel-time convention is not substituted for the paper's diameter. Contributions to the MDP linear program, finite-state hitting times, window-average inequalities, and confidence-region geometry are all useful beyond this mission.
Same-day and on-demand delivery services (groceries, meals, parcels) must decide how to assign incoming orders to drivers. One option is flexible dispatching: any driver may serve any order in the service region. Another is districting: the region is cut into districts, one per driver, and each driver serves only the orders from their own district. Districting is easier to run, since drivers learn their territory, routes are short and responsibility is clear, but it gives up the flexibility of pooling. A basic question is when a districting policy loses nothing against the best flexible policy.
Carlsson, Liu, Salari and Yu (Operations Research 72(1), 2024; accepted manuscript SSRN 3915544) answer this in heavy traffic, the regime where the drivers are almost always busy. Their comparison point is the policy of Bertsimas and van Ryzin (1993), whose expected delivery time has an explicit leading-order formula in heavy traffic. Their Theorem 6 gives two integral conditions on a partition under which districting matches to first order.
Timeline.
A service region is compact and convex and contains a depot . Orders arrive at rate at random locations drawn from a demand density on , Lipschitz, with . There are identical vehicles with speed and capacity , and each order needs an on-site service of mean . The constant comes from the Beardwood–Halton–Hammersley theorem.
The workload factor of the fleet is
the long-run fraction of time a vehicle spends in on-site service and in travel to and from the depot. The system is stable when it is below , and heavy traffic is the limit in which it tends to from below, with only varying.
Theorem 3 of the paper (Bertsimas and van Ryzin) states that achieves
in heavy traffic. A policy is asymptotically optimal if in heavy traffic.
A region partitioning policy fixes a partition of and dedicates one vehicle to each . District then receives orders at rate with conditional density . Its vehicle runs the single-vehicle version of , so Theorem 3 with gives its delivery time . The policy's overall expected delivery time is .
If for every
and and every obey Theorem 3, then
These are the displayed steps of the printed proofs of Theorems 5 and 6 (pp. ec5–ec6):
The result. Theorem 6 turns a question about stochastic, dynamic routing into a static geometric condition: find a partition that gives every district a share of two measures, (local tour length) and (service plus round-trip load). The rest of the paper builds on this. It computes such partitions with convex pieces, bounds the loss when the shares are only approximately equal (Proposition 3, the subject of the companion mission), and tests the policy in simulation. The theorem also shows that the arrival rates need not be equal across districts. What has to be equal is the combined load.
Formalizing it. The result has a short pen-and-paper proof, and no machine-checked version exists. The mission records exactly which part of the argument is real analysis (integral identities over a partition, and how heavy-traffic limits pass to ratios) and which part is borrowed from Bertsimas and van Ryzin. It also gives the platform a first districting and continuous-approximation development. Its definitions (workload factor, Theorem 3's leading term, heavy-traffic filter, conditional subregion data) can be reused for other results in the continuous-approximation literature.
The algebra in the proof is simple once Theorem 3 is applied to each district with its own rate , density and one vehicle. The obstacle is in the limits. Theorem 3 for district holds along that district's heavy-traffic limit, where its own workload factor tends to , while asymptotic optimality is measured along the fleet's limit. These are different limits unless the second equitable condition makes the two workload factors equal as functions of . A tempting shortcut is to state the district hypothesis directly with the fleet's quantities, such as and the fleet's workload factor. That assumes milestones 2 and 3 and empties the theorem. Division also needs care: and the ratios have denominators that must be shown nonzero from the hypotheses, not assumed.
The plane is EuclideanSpace ℝ (Fin 2) with the Euclidean norm, and integrals are Bochner set integrals for Lebesgue measure. The definition file CarlssonPartition.Equitable.Setting contains:
Conventions:
Filter.comap (fun λ => workload) (𝓝[<] 1): the arrival rates along which the workload factor tends to from below. Every "" is a ratio tending to .Two formalizations would make the goal trivial and are ruled out: defining or as the leading-order formula, and writing the district hypothesis with fleet quantities or the fleet's filter. The verification development checks that the heavy-traffic filter is not the bottom filter whenever .
Welcome contributions: proofs of the milestones; a general lemma on averaging ratio limits under a probability vector; and finite additivity of set integrals over a.e.-disjoint partitions in the form used here.
Reinforcement learning in a changing environment needs a benchmark that remains meaningful when the transition law and rewards vary from round to round. For a stationary Markov decision process (MDP), the optimal long-run average reward is a standard benchmark. In a nonstationary MDP, summing those stationary optima across rounds is convenient, but it need not equal the best expected reward achievable over the whole horizon: today's action changes tomorrow's state. Cheung, Simchi-Levi and Zhu use Proposition 1 to quantify this gap in their analysis of nonstationary reinforcement learning (preprint, pp. 7–8). This mission formalizes that proposition and the explicit estimates in its proof.
The paper develops algorithms for MDPs with drifting rewards and transitions. Its oracle comparison is useful before any algorithm is chosen: it relates a sum of local, stationary benchmarks to the reward of every non-anticipatory policy, including policies that adapt to the observed trajectory. This separates a property of the environment from the performance of a learning rule. The paper was published in Management Science in 2023; this mission follows the numbered statements and pages of the authors' pinned arXiv preprint (Cheung et al., 2020, pp. 6–8).
A finite nonstationary MDP has a finite state set , a nonempty available-action set at each state , and a horizon of rounds. At round , taking action in state gives a stochastic reward with mean and moves to a new state according to the probability distribution . A non-anticipatory policy selects an allowed action using the current state and observations from previous rounds. The target concerns expected sums of the mean rewards, so the distributional shape of the reward noise does not enter its formula (preprint, §2.2, pp. 6–7).
The one-step reward variation is the largest value of over allowed state–action pairs. The transition variation is the largest distance between the corresponding transition distributions. Their variation budgets are and , exactly as in equation (1). The budgets are computed from the MDP sequence; they are not independent inputs to the theorem (preprint, p. 6, (1)).
For the stationary MDP at round , is its optimal long-run average reward. The mission represents it as the optimum of the paper's occupancy linear program (15), whose variables are nonnegative state–action occupancies, satisfy flow balance, and sum to one. A diameter bounds the least expected hitting time between any two states under an allowed stationary policy. The paper's Definition 1 includes equal initial and target states, so this includes a return time. Assumption 1 requires a finite diameter at every round; is a common bound on those diameters (preprint, pp. 7–8, Definition 1 and Assumption 1; p. 33, (15)).
Write . For and the necessary small-budget condition , the target is
for every initial state and every allowed non-anticipatory policy . Quantifying over every policy expresses the paper's maximum over policies without introducing a supremum over an unbounded real-valued function space. The first five targets follow Appendix A.2: a bounded optimal dual potential, the gain-drift inequality (18), the pathwise dual inequality (19), the window inequality (23), and the full-horizon inequality (24). Their constants and index ranges are part of the targets (preprint, pp. 8, 33–34).
The result gives a finite-horizon comparison between two different benchmarks. The sum of stationary gains is additive over time, while the best expected cumulative reward accounts for how actions alter later states. Proposition 1 says that their difference is controlled by variation and diameter under its hypotheses. This is the paper's justification for using the additive oracle in its dynamic-regret definition; the authors note that the later algorithmic bounds are larger than this comparison term (preprint, p. 8, text after Proposition 1).
The mathematical result is already claimed in the paper. This mission asks for a machine-checked version with explicit finite-horizon distributions, the occupancy LP, the diameter convention, and the drift sums. The new Lean statements currently have placeholders for their proofs; the imported finite-MDP definitions are already published. A completed development would provide reusable code for time-dependent MDP trajectory laws and for comparing stationary LP values as a model drifts. It would also make the precise domain of the square-root bound reviewable independently of the algorithms in the remainder of the paper.
The stationary gain is not a per-round reward guarantee. An action can collect reward now and put the process in a state whose future reward is poor, so summing stationary optima does not directly bound a nonstationary trajectory. Conversely, treating each round as an independent stationary experiment discards the state dependence that the policy exploits. The diameter controls the cost of that dependence, and variation controls changes between the stationary problems. The proof must connect these objects while preserving the exact factors , , and in Appendix A.2 (preprint, pp. 33–35).
There is also a small-budget obstruction in the printed Proposition 1. Its stated permits , where the displayed inequality is false: a two-state, one-action example with a slowly returning state, , and reward drift has an oracle sum near while the proposed lower bound on that sum is near . The mission therefore adds and records the difference from the page. Inequality (24), posed separately, retains the paper's every-integer-window form and needs no such pin.
States and actions are Fin S and Fin A; available actions form a nonempty Finset at each state, and . The imported FiniteMDPLearning structure supplies reward rows in and transition probability rows. It has rows for actions unavailable at a particular state; all mathematical maxima, LP constraints, policy restrictions, and drift formulas use only allowed pairs. The source's time is stored at Lean index . No value of the MDP sequence after the horizon enters a stated budget or reward sum.
The occupancy LP has a nonempty bounded feasible-value set under the standing MDP assumptions; its real supremum denotes . Hitting times and diameters use extended nonnegative reals to retain infinity, rather than silently converting an infinite hitting time to zero. The diameter includes same-state return times and minimizes over deterministic stationary policies; such policies attain the hitting-time minimum. The policy used for cumulative reward is a history-dependent randomized kernel on state–action histories. Conditioning an action rule that also observes past rewards on that history yields the same state–action trajectory law. The nonstationary measure samples the next state with the current round's transition law and is a probability measure.
The fixed is constrained to bound every round's diameter; it is not an unrelated parameter. The stated pin rules out the false small-budget case. In (23), the paper's last-window drift sum includes , which equation (1) does not define; the formal sum retains all defined terms through . The goal and milestones do not weaken , restrict the policy class to a convenient subclass, or omit a time step. Contributions on LP duality, finite-horizon trajectory expectations, hitting-time bounds, and drift inequalities are useful beyond this proposition. The paper's headline Theorems 1–4 are not posed here because their notation hides constants (preprint, p. 6, §2.1).
Blood platelets, fresh produce and many pharmaceuticals have a fixed lifetime: a unit not used within periods of its arrival must be discarded. Optimal ordering for such products depends on the whole age profile of the stock, and the dynamic program that describes it has an -dimensional state. It is intractable beyond small (Nahmias, 1982; Nandakumar & Morton, 1993), so practice relies on base-stock policies, which raise the total stock to a fixed level every period.
Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first performance guarantees for base-stock policies in this system. Under first-in-first-out (FIFO) issuance a heuristic base-stock level is asymptotically optimal in the lifetime, the demand population, the penalty cost and the outdating cost (missions 1–4 of this series). Under last-in-first-out (LIFO) issuance, which models a customer who picks the freshest unit from the shelf, a simple base-stock level is asymptotically optimal in the penalty cost and, when demand can be arbitrarily small, in the outdating cost (Theorem 5, mission 5). This mission formalizes the complementary negative result: when the demand is bounded away from zero, no base-stock policy is asymptotically optimal under LIFO as the outdating cost grows.
Demands are i.i.d. copies of a nonnegative random variable with and distribution function . The lower support is , and the newsvendor level is with .
The product has lifetime . At the start of period the state is , where is the stock with remaining lifetime at most ; the system starts empty. The firm orders , which arrives at once, raising the total stock to . Demand is served youngest stock first, unmet demand is lost, and stock reaching the end of its lifetime outdates. Under LIFO the outdated amount and the next state are
Each period costs with and . A policy is admissible if its order in period is a nonnegative measurable function of the current state. Its long-run average cost is , and . The base-stock policy orders , with cost . The subscript marks the outdating cost; , , and the demand law are fixed.
If and , then
where is the best base-stock cost. The goal asserts that both costs are finite, and that the limit exists and is strictly positive.
The proof also uses Lemma 3 (, p. 16) and inequality (EC.22) (p. ec8). Both are milestones of mission 5 of this series and are not restated here.
Proposition 1 marks the boundary of Theorem 5(c). Together they show that under LIFO, with a large outdating cost, base-stock policies are asymptotically optimal exactly in the trivial cases or , and when . In the remaining case some optimality gap persists however large is. Under FIFO the heuristic level is asymptotically optimal in without conditions (Theorem 4), so the result separates the two issuance rules: a manager facing fresh-first customers and costly waste should look beyond base-stock policies.
The result is proved in the paper; nothing in it is machine-checked. A formal proof would give the first verified statement about the long-run cost of a perishable inventory system. It would also produce reusable pieces: the LIFO recursion, the base-stock cost under LIFO, and a time-dependent policy whose cost can be computed exactly.
The obvious argument compares two limits. The limit of the best base-stock cost needs a lower bound valid for every base-stock level at once, and that bound must be uniform as changes. The lower bound of Lemma 3 controls the outdating only through , so the limit of its minimum has to be computed separately. The upper side cannot use a base-stock policy at all. It needs an explicit policy that is not stationary. That policy must be shown never to outdate along every demand path, and its periodic cost has to be bounded strictly below . The strictness needs the facts that and that , which is where and enter. A long-run average over a non-stationary policy is a of Cesàro means, and the step from per-period bounds to the average has to be made explicitly.
CappedBaseStock.DemandLaw: a probability law on with finite positive mean. The demand path carries the i.i.d. product law. The newsvendor cost and are backorderCost and newsvendorLevel of the published LostSalesOrderUpTo.Asymptotic.Backorder.Fin (m - 1) → ℝ with , so is allowed. Levels range over .The work needs a Cesàro-limit toolkit for -valued sequences, the LIFO sample-path recursion, and convexity facts for the newsvendor cost. Proofs of the milestones, and of the definitional sanity facts (, ), are welcome.
For every and every integer , there exists a total Boolean function with and .
The construction refines the tournament recursion of OpenAI/math. It keeps all four sensitivity profiles, sharpens the target-row count to fifteen, and bounds the gate contribution by separating the cases with and without a sink.
At depth , use tournament parameter , label alphabet , and disjoint OR copies. The proof obtains a finite seed and integers satisfying global sensitivity , block sensitivity at zero , and the exact integer comparison . This implies ; the shared finite-certificate theorem supplies arbitrarily large sensitivity and the campaign conclusion.
The shared campaign definitions are retained. The local proof was checked in Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. This draft targets a certified campaign improvement; no global optimality claim is made
A manufacturer that already sells directly to consumers may also supply an independent retailer. Adding the retailer can reach consumers who prefer its service, but the two channels then compete for some of the same buyers. A wholesale price affects both the retailer's ability to serve consumers and its retail pricing. The manufacturer's choice of distribution channel therefore depends on the pricing tools available to each firm. Jullien, Reisinger, and Rey study this choice when either or both firms can charge prices tailored to individual consumers in Personalized Pricing and Distribution Strategies. The source used here is their authors' manuscript of March 2022, whose proof of Proposition 3 appears in Online Appendix A.
This mission addresses a particular case of that analysis: the manufacturer charges a single retail price, while the retailer may charge either a single price or a price tailored to each buyer. The consumers' valuations for both channels move in the same direction with their type. Under those conditions, the paper claims that opening the retailer channel raises total industry profit under either retailer pricing policy. This is a question about the distribution decision, with the downstream retail game determining the profit achieved by each decision.
A consumer type is a real number in , with unit density. Firm A is the manufacturer and direct seller; firm B is an independent retailer that obtains each unit from A. Their values to a consumer are
There are no fixed costs of opening a channel and no variable production or distribution costs. The market parameters satisfy and . These conditions express the positively correlated case in §5 and keep the market large enough that its upper boundary does not limit B's demand. The two values cross at , with common value . Types below value A's offer more; types above it value B's offer more, until valuations fall to zero.
A two-part tariff has a fixed fee and a wholesale price per unit B buys from A. The fee divides profit between the firms. Total industry profit is what consumers pay, so cancels from that total. The wholesale price is nonnegative. At the wholesale stage, the firms compare the total industry profit attainable with both channels against the profit from A selling alone. As on p. 9 of the manuscript, a tie is resolved in favor of mono distribution; a strictly greater profit is required for dual distribution.
When A sells alone and charges a uniform price , its profit is times the measure of types for whom . If both firms charge uniform prices, denoted UU, they set and simultaneously. A consumer buys the product with highest nonnegative net utility. A earns on each of its retail sales and on each B sale. B earns on each of its sales. A downstream Nash equilibrium requires each price to maximize its firm's variable profit against the other price, including deviations into market regions where demand is zero or the identity of the preferred firm changes.
If A charges a uniform price and B tailors its price, denoted UP, A announces first. B then responds separately to each consumer. Under the continuation selected in the manuscript, B serves a type when exceeds both zero and A's nonnegative consumer surplus. Its price is . Otherwise, A sells if its price does not exceed the consumer's value. A chooses its uniform price to maximize its retail receipts plus wholesale receipts. Industry profit is the integral over of the price actually paid by each consumer.
The mono-distribution benchmark is
The paper derives a wholesale price and retail prices for the UU game, together with a profit satisfying
For UP it derives , A's leader price , and a profit . Equation (15) gives . The milestone list follows these source results, including the consumer demands and the two profit identities. Its last comparison completes the UP side after the UU gain is established.
The goal is Proposition 3: for each of UU and UP, some nonnegative wholesale price admits a downstream equilibrium and every equilibrium at that price yields industry profit strictly greater than A could earn with any uniform price in mono distribution. The goal leaves the wholesale price existential, as the proposition does. It does not assume the paper's calculated candidates are the only possible wholesale prices that work.
Proposition 3 identifies a robust distribution choice within the positively correlated case: while A uses uniform pricing, permitting the retailer channel raises joint profit whether B uses uniform or personalized retail prices. The conclusion separates the effect of B's pricing technology from the effect of A's own pricing technology; the latter changes the distribution comparison in Proposition 4 of the same manuscript. The result also supplies a precise instance in which additional downstream competition and additional market coverage must be assessed together.
The paper proves Proposition 3 in its Online Appendix A. The remaining work for this mission is a machine-checked derivation of the downstream equilibrium conditions, the demand and payment integrals, and the strict profit comparisons. The Lean statements here are open proof obligations. A complete development would make the consumer-choice and profit model reusable for related distribution games, while the rational formulas and equilibrium calculations are specific to this paper's linear valuations.
The paper writes simple linear demand expressions in the region where both firms have positive sales. Actual demands are measures of consumer choice sets and change formula at market boundaries, when a price excludes a product, or when all consumers refuse to buy. A first-order condition within one region does not by itself establish a global best response in the full retail game. The UU equilibrium milestone consequently states global Nash optimality and uniqueness at the selected wholesale price. In UP, A's leader price must likewise maximize its variable profit over every real uniform price after B's per-consumer response. The integral of actual payments must then be shown to equal the paper's closed form.
Lean represents consumer types by real numbers in and their mass by Lebesgue volume. The Model fields are ; Model.Standing records exactly and . The valuations and crossing point are defined from these fields. Retail demand is clipped to the consumer interval, and profit is calculated from demand or actual payments. The expressions printed as (12) and (14) are theorem conclusions, not definitions of industry profit. A real supremum is unnecessary for mono distribution: the theorem bounds profit at every price and proves attainment at .
The UP response uses the manuscript's selected personalized-pricing continuation. At indifference, the choice rules assign UU ties between the firms to A and give B a sale in UP only with a strict margin. Ties occur only at isolated types at the candidate equilibrium prices; zero-price deviations can create ties across the flat zero-valuation tail, and the rules specify their outcome. Global best responses quantify over all real retail prices, including zero and negative deviations. The goal restricts wholesale prices to , the range used in the manuscript's analysis. The fixed fee is omitted from the model because it transfers profit between firms without changing industry profit. The goal includes existence of a continuation equilibrium, so a vacuous universal statement over an empty equilibrium set cannot establish dual distribution.
The development needs elementary properties of Lebesgue measure on real intervals, measurable piecewise choice sets, interval integration, and algebraic inequalities for the rational candidate prices. Proofs of the equilibrium and integral milestones, or reusable lemmas about volumes of intervals cut by affine utility comparisons, are welcome contributions. The shared primitives are duplicated in the companion mission on personalized pricing by A because unpublished draft definitions cannot be imported across proposals.
source.pdf, SHA-256 25a6c84ac0c48c6720f6a9e1f9b1f1ec516412c31dac044ac84c1d4c72dfc253, printed pp. 5–14 and Online Appendix A, pp. 1–4.Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that is not used within periods of its arrival must be discarded. Managing such products is a classical problem of inventory theory (Nahmias 1982, Operations Research 30(4), doi:10.1287/opre.30.4.680). The optimal ordering policy depends on the entire age profile of the stock, so it is computationally intractable beyond very short lifetimes, and practitioners use base-stock policies, which raise a single aggregate quantity to a fixed level every period.
Bu, Gong and Chao (SSRN 3724966, accepted manuscript, 2022; Management Science) give the first theoretical performance guarantees for base-stock policies in perishable systems. This mission covers §5 of the paper: the backlogging system with a positive replenishment lead time , where unmet demand waits and orders arrive periods after they are placed. Earlier missions of this series treat the zero-lead-time lost-sales system under FIFO issuance (missions 1–4) and under LIFO issuance (missions 5–6).
Demands are i.i.d. copies of a nonnegative random variable with . The product has lifetime , the lead time is , and the unit costs are (holding, per unit left over), (backlogging, per unit per period) and (outdating, in addition to holding). Throughout, .
In period the order placed in period arrives and serves backorders first. The firm then observes the state : for , is the on-hand stock with remaining lifetime at most minus the backorders, and for it adds the pipeline orders that arrive by period . The firm orders , which raises the inventory position to . Demand is served oldest-first (FIFO), the shortfall is backlogged, and with the outdated quantity the state moves by
The system starts empty. The cost of period is , where is the net on-hand inventory.
An admissible policy orders with each measurable. Its long-run average cost is , and . The base-stock policy orders ; its cost is . The heuristic level is any minimizer over of
For and every minimizer , the gap
(a) is at most for all lifetimes , with independent of ;
(b) if the one-period demand has the population form of (7), with and the moment assumptions of Theorem 2, is at most for all large , for every fixed lifetime ;
(c) tends to as , for every choice of minimizers.
Lemma 5 (p. 19): for and , , and is at most the same expression with replaced by . Proposition 4 (p. 23): for . Inequality (28) (p. 24):
Theorem 7 says that a policy computed from one convex function of one variable is nearly optimal for a control problem whose state has dimension , in three practically relevant regimes: long shelf life, high-volume demand, and expensive waste. The bound (28) is explicit and computable from the demand distribution, so it also certifies, for any given instance, how far can be from optimal. Lemma 5 gives two-sided bounds on the cost of every base-stock policy without solving for a stationary distribution of the age profile.
The paper proves Theorem 7 by sketch (§6.2: "We omit the details for brevity"), relying on the arguments for the zero-lead-time Theorems 1, 2 and 4. None of these results has a machine-checked proof. The mission's work is therefore to formalize the lead-time bookkeeping (EC.29)–(EC.33), the lower bound of Proposition 4 with its conditional-Jensen step, the convergence argument in each regime, and the omitted details of the sketch.
The lower bound on must hold for every admissible policy, including those that use the full age profile and the pipeline, whose optimal form is unknown. The obvious route, comparing with the non-perishable backlogging system where a base-stock policy is optimal (Karlin–Scarf), gives a lower bound that ignores outdating entirely and is too weak to make the gap vanish; outdating costs incurred by an arbitrary policy have to be accounted for, and the lead time means that units outdate up to periods after the order that created them. The standing assumption is exactly what keeps the coefficient of the outdating term in nonnegative. The upper bound requires the long-run cost of although the age-profile chain need not have a stationary law that is easy to describe.
In the limits, the heuristic level moves with the varying parameter. For (a), a uniform bound on in is needed; for (b), the newsvendor level of the compound demand grows with and concentration of is required (Scarf's bound and a Bernstein inequality in the zero-lead-time case); for (c), must be shown although the coefficient of (28) grows linearly in .
PerishBaseStock.Backlog. Demand laws, the i.i.d. path law, the lead-time sum law and the newsvendor expectations are imported from the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.d t is .Fin (m + L - 1) → ℝ of cumulative levels; when it is empty and .ℝ≥0).Params.Standing; is an explicit hypothesis of Proposition 4, (28) and Theorem 7. Proposition 4 is formalized for FIFO issuance, the only issuance rule the paper specifies for this system.Trivializing formalizations are ruled out: is an infimum over all measurable state-feedback policies, not over base-stock policies; is the long-run average of the simulated cost; neither , , nor the demand law is fixed; and no gap is stated through a truncated subtraction or an infinite .
A complete development needs the long-run behaviour of the base-stock dynamics, conditional Jensen for policies adapted to past demand, exponential tail bounds for sums of i.i.d. demands, and, for (b), renewal-count moments and concentration. The sample-path lemmas (EC.29)–(EC.30) and Lemma 5 are reusable for other perishable models with lead times. Proofs of any milestone and of the individual parts (a), (b), (c) are welcome.
Blood platelets, fresh produce, bakery items and many pharmaceuticals have a fixed lifetime: a unit that is not used within periods of arrival must be discarded. Replenishing such a product is a classical problem of inventory theory (Nahmias 1982), and its optimal policy depends on the whole age profile of the stock, so it cannot be computed for realistic lifetimes. Practice therefore relies on base-stock policies, which raise total stock to a fixed level every period.
Bu, Gong and Chao give the first theoretical guarantees for such a policy. Under first-in-first-out (FIFO) issuance they choose the level by minimizing an explicit surrogate of the long-run cost and show that its optimality gap vanishes in four regimes. This mission is the fourth: a large unit outdating cost . The regime matters in practice because outdating is expensive. Slonim et al. (2014) put the component cost of a unit of blood sold to U.S. hospitals at about $570, and disposing of expired products often requires costly handling.
Demands are i.i.d. copies of a non-negative random variable with and distribution function . The product lives periods. At the start of period the state is , where is the stock with remaining lifetime at most . The firm orders , raising the total stock to (lead time zero). Demand is served oldest first and unmet demand is lost. The quantity outdates, and the state evolves by
The system starts empty. The period cost is
with holding cost , lost-sales penalty and outdating cost .
A policy is admissible if each period's order is a non-negative measurable function of the current state. Its long-run average cost is , and is the infimum of over admissible policies. The base-stock policy orders , and is its long-run average cost. The heuristic level is any minimizer over of
The lower support of demand is .
for every selection of minimizers, with , , and the demand law fixed. The statement holds for every demand law, whether is zero or positive.
The goal's proof also uses inequality (21), . That inequality, together with Lemmas 1–2 and Proposition 2 behind it, is posed in mission 1 of this series and is not restated here.
Theorem 4 says that when outdating is expensive, a policy computed from a one-dimensional convex function is as good as the optimal age-dependent policy. A base-stock policy does not need to track the age distribution, and its level can be found by simulation and golden-section search between explicit bounds. Together with Theorems 1–3 it shows that is asymptotically optimal in all four regimes of the paper. Remark 2 of the paper notes that the plain newsvendor level fails in this regime.
The result is proved in the paper (Management Science, 2022). It has not been formalized. This mission adds a machine-checked model of the FIFO perishable system with lost sales: the age-structured dynamics, admissible policies, long-run average costs and the optimal cost over all policies. The model is reusable for the other missions of the series and for the wider perishable-inventory literature. The paper's proof leaves several steps to the reader: the monotonicity of , the identity , and continuity of the newsvendor cost. Each of these becomes an explicit statement.
The obvious argument compares the heuristic with an optimal policy directly. That fails because the optimal policy has no tractable form. The proof instead goes through (21), a lower bound on obtained by a sample-path argument, and then has to show that the outdating term of the heuristic level vanishes faster than grows. That needs uniform control of as . The level must eventually fall into , where no stock survives periods of demand, and the newsvendor cost there must match the restricted minimum. A naive reading of " decreases in " holds only for the least minimizer. For an arbitrary selection, the argument has to work through the bound (EC.16) alone.
PerishBaseStock.Outdating and builds on the published demand layer CappedBaseStock_Model (i.i.d. demand path, demand law with ) and the newsvendor functions of LostSalesOrderUpTo.Asymptotic.Backorder.Fin (m - 1) → ℝ≥0 of cumulative levels, with . When the state is empty and everything left over outdates. Levels range over .atTop there. The goal asserts that is finite and that the difference of real values tends to , so no convention enters.When customers request a customized product, their requests can reveal information about what they value. A seller can use that information when setting a price, while a customer can choose a request with the resulting price in mind. The question is whether customers with different preferences can make different requests in equilibrium. Liang Guo's The Voice of Customers in Customization, §3.3, studies this question in a two-type model of buyer-led product design, called O-Learning. It compares O-Learning with a separate game in which the seller chooses quality after a customer's cheap-talk message. This mission concerns only the O-Learning game.
Proposition 3 of the SSRN author copy identifies when a particular cheap-signaling equilibrium exists: each type asks for the quality it would prefer if its type were known. Section 3.3 then asks whether a different pair of requests could separate the types when that equilibrium fails. The Appendix, under “No Other Separating Equilibrium under the O-Learning Customization,” establishes nonexistence below the same threshold. It is this latter claim, for every request pair and every admissible off-path belief, that is the mission's target.
A buyer has one-unit demand and a privately known quality preference , where . A fraction of buyers have the high preference. Quality is a real number . Producing or delivering a product of quality costs , while preparing to sell it costs , with . The latter is sunk before the price is determined. These are the assumptions of §2 of the paper, pp. 5–9.
Under O-Learning, the buyer requests a quality. The seller observes the request, forms a perceived type , and accepts or rejects. If rejected, both parties receive zero. If accepted, the price-setting stage follows the paper's reduced-form bargaining rule: the seller has the opportunity to make the price offer with probability and the buyer has it with probability . The buyer's expected payoff, conditional on acceptance, is equation (9):
The seller accepts precisely when , including equality. A separating pure-strategy equilibrium consists of two distinct, nonnegative requests and , plus a belief about the buyer's type after each possible request. The seller identifies the correct type at and ; away from those two requests its belief can vary. Given that belief and the seller's acceptance rule, neither buyer type can improve its payoff by making any other nonnegative request. The pricing stage is represented by the payoff formula rather than by a separate bargaining game, as in §3.3 of the source.
For a buyer whose type is known, equation (10) gives the complete-information request
Proposition 3 defines three ratios and their combined threshold:
The prior is part of the model, although the separation threshold does not depend on it.
The goal says that, whenever the standing assumptions hold,
Equivalently, the existence of any such equilibrium requires . The goal quantifies over all pairs of nonnegative requests and all belief functions consistent at those requests. It does not prescribe the requests or Proposition 3's supporting off-path beliefs.
The milestone list follows the two failure regimes stated in the Appendix, pp. 28–29. When , it first identifies the low type's equilibrium request and then rules out separation. When , it records the form of and the bounds on acceptable equilibrium requests before ruling out separation in either order of and . These are the author's stated intermediate claims, with their source text attached to each milestone.
Proposition 3 shows when the two complete-information requests can be sustained as a separating equilibrium. The Appendix result strengthens the interpretation of its threshold: below , changing the requests or the off-path beliefs cannot restore separation. This matters for the paper's comparison of who controls quality design and when customization can reveal preferences. Without the nonexistence result, the failure of the cheap-signaling request profile would leave open another separating profile with distorted qualities.
The result is proved in the SSRN author copy, and this mission asks for a machine-checked version of that proof. The proposed definitions and statements compile as Lean declarations, but their proofs are open. A completed development would also supply reusable calculations about the seller's acceptance range and buyer payoffs with quadratic costs and endogenous beliefs. The milestones identify these specific pieces of work; they do not claim that a general signaling-game library is already formalized.
Ruling out just the request profile would be insufficient. An equilibrium candidate can use another pair of qualities and can assign either type to requests outside its path. Acceptance changes the payoff discontinuously: a request that would be attractive if accepted instead pays zero when rejected. The buyer's conditional payoff also contains two terms, so a polynomial formula obtained on an accepted range need not hold at every quality. The main challenge is to control all deviations and beliefs under the actual acceptance rule, while maintaining the strict threshold inequalities in both failure regimes.
Lean uses a two-constructor buyer type, a model with real parameters , and a predicate for the paper's standing assumptions: , , , , and . Requests and deviations are restricted to . Beliefs are total functions from real requests to the two named types, constrained only at the equilibrium requests. Seller acceptance is the printed inequality and accepts at equality; a rejected request pays zero. The conditional payoff retains both maxima from equation (9), and is the printed expression, not a value defined through equilibrium existence. No fixed cost for learning or customization is included, as in the paper's main analysis.
The equilibrium predicate does not fix off-path beliefs, require the requests to equal , or replace seller acceptance with a derived threshold. The proof therefore cannot become a restatement of Proposition 3. The local O-Learning definitions duplicate the draft model of the companion mission because unpublished drafts cannot be imported. The paper's last sentence on p. 19 calls the cheap-signaling equilibrium “the only separating equilibrium.” The Appendix proves nonexistence when the ratio is below ; it does not establish global uniqueness when the ratio is above it, and global uniqueness is false. This mission states the Appendix's precise claim.
News publishers depend on direct visits for advertising revenue, while social platforms can show publishers' content inside their own feeds. That arrangement can move reading time from the publisher's site to the platform without changing how much news a consumer reads. It can therefore change the publisher's return from improving content quality. De Cornière and Sarvary study this question in a sequential model of a monopoly newspaper, a social platform, and consumers who divide a fixed amount of attention between the two sites. Their Proposition 1 says that unilateral content bundling lowers the publisher's profit, yet can either raise or lower its equilibrium quality depending on the cost of quality. De Cornière and Sarvary, working paper, pp. 7–12.
This mission concerns the paper's unilateral content bundling regime: the platform can incorporate news into its feed without a payment or a negotiated agreement with the newspaper. The source for theorem numbering is the Toulouse School of Economics Working Paper n° 1152, August 2021. The article later appeared in Management Science in 2023. The working paper's Proposition 1, Lemmas 1–4, and equation (2) are the targets here. The paper separately studies subscription pricing, voluntary participation, and negotiated bundling; those are separate settings. De Cornière and Sarvary, working paper, §§4–6.
A newspaper first chooses news quality . A platform next chooses a news share in its feed. Consumers finally allocate one unit of time between the newspaper's site and the platform. Write for newspaper time and for platform time. The newspaper shows only news. A fraction of platform time exposes the consumer to news; the remaining fraction exposes the consumer to user-generated content (UGC). News and UGC consumption are
The representative consumer obtains utility . When unconstrained by the available mix, the consumer wants news consumption . The platform earns , where one unit of UGC time yields one unit of revenue and one unit of news time yields . The newspaper earns : direct time pays per unit and indirect news time pays . Producing quality costs , giving newspaper profit . De Cornière and Sarvary, working paper, pp. 8–9, equation (1).
A subgame-perfect equilibrium (SPE) specifies consumer attention after every feasible pair , a platform news share after every feasible , and an initial quality. At each stage the chosen action maximizes that stage's payoff given the continuation strategies. The no-bundling benchmark is the same game with , which forces . Consumer surplus is utility at the equilibrium attention allocation. De Cornière and Sarvary, working paper, pp. 9–10, §4.1.
The goal is Proposition 1, comparing every bundling SPE with every benchmark SPE. Both sorts of equilibrium must exist. Publisher profit is strictly lower under bundling. Away from the crossover cost, quality and consumer surplus increase exactly in the low-cost regime:
where . A further clause records that at there is an equilibrium with quality below the benchmark. De Cornière and Sarvary, working paper, p. 12, Proposition 1; p. 31, proof.
The milestones follow the paper's named results and displays: Lemma 1 gives benchmark quality and profit ; Lemma 2 gives consumer attention ; Lemma 3 identifies the platform share ; equation (2) gives the publisher's two-branch profit; the displayed definitions on p. 12 identify the branch maximizers and ; and Lemma 4 characterizes equilibrium quality. The proof of Proposition 1 also states the ordering and relates surplus to the optimal content mix. De Cornière and Sarvary, working paper, pp. 10–12, 31.
The profit and quality effects answer different questions. Even if total news consumption stays at the consumer's preferred level, moving some of that consumption onto the platform reduces the publisher's direct traffic and hence its profit. Quality responds to a comparison of the publisher's gains from direct and indirect readers. The cost threshold distinguishes when the equilibrium moves toward a higher-quality strategy that attracts direct visits and when it moves toward a lower-quality strategy consumed through the platform. Because surplus in this model rises with equilibrium quality, the same threshold governs consumer surplus. De Cornière and Sarvary, working paper, pp. 12–13, 31.
The paper proves these claims mathematically; the Lean theorems in this proposal are open statements awaiting machine-checked proofs. Formalizing the complete sequential game would produce reusable specifications for attention allocation, contingent strategies, and equilibrium comparisons in platform markets. The first-stage profit identity and the best-response theorems are also usable independently of the final comparative-static result. This mission does not assert that the article's other models have already been formalized.
Checking only the realized quality and platform share does not establish subgame perfection. A different quality chosen by the newspaper changes the platform's subsequent action and then the consumer's allocation; those continuation choices must be valid after every feasible deviation. The publisher's resulting objective also changes form at . At the cost the two candidate qualities both maximize profit, so an assertion about “the” equilibrium quality requires care. The article prints a low-quality choice at equality, while the game itself admits both. De Cornière and Sarvary, working paper, pp. 11–12, equation (2), Lemma 4; p. 31, proof.
The Lean model uses real parameters . The standing assumptions are exactly Table 1: , , , and . Quality, attention, and platform share range over , , and respectively. The paper's earlier convention is superseded here by its Table 1 interior range; appears only as the benchmark instance. Real division in the candidate formulas is used under assumptions that make every denominator nonzero. De Cornière and Sarvary, working paper, pp. 8, 10, Table 1; p. 31, proof of Lemma 4.
The pin applies only to Proposition 1's two “if and only if” comparisons. At equality, Lemma 4 is stated with both possible equilibrium qualities, and the goal retains the strict publisher-profit comparison. The platform's share theorem excludes , where platform time is zero and its choice is indifferent. The consumer-attention theorem assumes before dividing by . The benchmark is an SPE with cap zero, and surplus is evaluated from utility; neither is inserted as a closed formula. Equilibrium strategies are defined by best responses after all feasible histories, and explicit existence clauses prevent claims about all SPEs from holding vacuously. These choices rule out defining equilibrium quality, benchmark quality, or surplus by the expressions that the milestones are meant to establish.
The development needs real arithmetic and interval sets from Mathlib, a model-specific strategy profile, utility and revenue definitions, and the three stagewise best-response conditions. Contributions establishing the consumer, platform, or publisher stages, the crossover case, and the final profit and surplus comparison are within scope. Subscription pricing and negotiated bundling require different games and are outside this mission.
Blood platelets, fresh food and many pharmaceuticals have a fixed lifetime: a unit that has not been used within periods of its arrival must be discarded. A retailer of such a product faces the usual trade-off between leftover stock and lost sales, plus the cost of discarding outdated units. The issuance policy, the order in which units of different ages are handed to customers, changes the problem. Under first-in-first-out (FIFO) the oldest units go first, as in a blood bank. Under last-in-first-out (LIFO) the newest units go first, as when shoppers pick the freshest milk at the back of the shelf, so that old stock tends to accumulate and outdate.
The optimal ordering policy of a perishable system depends on the full age profile of the stock (Nahmias 1975) and is intractable to compute except for small lifetimes. Practice uses base-stock policies, which raise the total inventory to a fixed level in every period. Bu, Gong and Chao (SSRN 3724966, accepted in Management Science, 2022) give the first theoretical guarantees for such policies in perishable systems. This mission covers their LIFO results (§4.1).
Demands are i.i.d. copies of a nonnegative random variable with and distribution function . Its lower support is , and is unbounded when for every . Units live for periods. Leftover stock costs per unit, a lost sale costs , and an outdated unit costs an extra .
At the start of period the state is , where is the stock whose remaining lifetime is at most periods, and . The firm orders , which raises the total level to . Demand is served newest-first and unmet demand is lost. The amount outdated and the next state are
The system starts empty. A policy is admissible if each order is a nonnegative measurable function of the current state. Its long-run average cost is
and is the infimum of over all admissible policies. The base-stock policy orders , and its cost is .
The paper bounds between two explicit functions (Lemma 3):
The heuristic level is any minimizer of on . The newsvendor level is . The proof also uses and its minimizer .
All three parts are stated for every minimizer , and in (b) and (c) for every selection of minimizers as the parameter varies.
Part (a) gives a gap of order that holds for every demand law with finite mean. Parts (b) and (c) identify regimes in which a single explicit base-stock level is asymptotically optimal. Part (c) is sharp: the companion Proposition 1 (mission 6 of this series) shows that when and , even the best base-stock policy stays a positive distance from optimal as . Under FIFO the corresponding gap decays exponentially in (Theorem 1, mission 1), so the two issuance rules behave differently. Whether the LIFO gap also decays exponentially is left open in the paper.
The results are proved in the paper but are not machine-checked anywhere. Prove2Me has no perishable lost-sales model with LIFO issuance. This mission provides one, built on the published demand layer and newsvendor functions, together with the sample-path recursion (EC.18), which is specific to LIFO.
is a long-run average over a Markov chain on an -dimensional state, and no closed form is known. The upper bound needs an accounting argument over windows of periods. The lower bound needs the exact recursion (EC.18) for the outdating of a base-stock policy under LIFO, which differs from the FIFO recursion. Treating the system as a newsvendor problem with a correction term fails: the outdating cost of lies strictly between the two bounds, and the minimizer of one bound is not a minimizer of the other. In (b) the absolute gap does not vanish, so the argument needs . In (c) the levels and move with , and the limits must be controlled uniformly over all minimizers.
Fin (m - 1) → ℝ of cumulative levels, with . The case (empty state) is included.leadTimeLaw.No trivializing reading is admitted. OPT ranges over all admissible policies, not only base-stock ones. is not a formula. No gap can hold through or division by zero. The parameters , , and the demand law are not specialized.
Proposition 2 holds under any issuance policy. Its FIFO instance and the FIFO lemmas are posed in mission 1 of this series, and only the LIFO instance is posed here. Lemma 3 and (EC.22) are also used in mission 6. Proofs of any milestone are welcome. Reusable infrastructure includes the law of the maximum of i.i.d. demands, convexity and continuity of the newsvendor cost, and existence of minimizers of and .
Social services such as public housing, food banks and free clinics are congested: the users who arrive wait in a queue they cannot see, and some of them could do almost as well elsewhere. A provider who sees the queue can decide what to tell arriving users about it. Telling low-need users that the queue is long sends them to their outside option and shortens the wait for everyone else; telling them too much may send away users the provider would rather serve. Information design (Bayesian persuasion, Kamenica and Gentzkow 2011) studies what a sender who commits to a signaling rule in advance can achieve.
Anunrojwong, Iyer and Manshadi (2023) build on the queueing persuasion model of Lingenbrink and Iyer (2019) and ask how much welfare information design can add in a congested service. Their answer depends on whether users are heterogeneous. This mission formalizes the homogeneous case, Proposition 1: when every user is low-need, the simplest policy, full disclosure of the queue length, is already within an explicit factor of the best signaling mechanism.
A single server with exponential service times of rate one serves users first come, first served. Low-need users (type L) arrive as a Poisson process of rate and may leave for an outside option worth ; high-need users (type H, rate ) always join. The total rate is . A type- user who joins with users present receives utility , where , is strictly decreasing, for large , and the increments are non-increasing (Assumption 1).
By Lemma 1 of the paper, an obedient signaling mechanism is described by the stationary distribution of the queue length on it induces. The admission policies are the probability distributions with
and the signaling mechanisms are those that also satisfy the obedience constraints
The welfare of low-need users is .
A threshold policy with , , , admits L-users below queue length , admits them with probability at , and turns them away above . denotes . The full-information threshold is the least with , and the full-information mechanism is . The homogeneous setting is .
In the homogeneous setting, with
the goal asserts three facts:
The paper phrases parts 1 and 3 for "the optimal signaling mechanism sm". They are stated here for every element of , which implies the paper's form for any maximizer and requires no existence result.
Proposition 1 bounds what persuasion can do when users are alike. The ratio is at most , so the gain from optimal signaling is small whenever full information already admits a few users. The paper contrasts this with the heterogeneous setting (§4.2), where information design can Pareto-improve on full information substantially. The homogeneous bound is the baseline for that comparison: it shows that the gains there come from the presence of two types, not from pooling queue states.
The result is proved in the paper. Nothing in this model has been machine-checked so far. A formal proof would check the reduction from an arbitrary signaling mechanism to a threshold mechanism (Theorem 1), the unimodality of threshold welfare (Lemma 5(2)), and the obedience calculation on p. 40. It would also confirm that these hold at , where the stationary distribution of the always-join policy no longer exists. The model layer defined here is shared with three sibling missions on Theorems 1 and 6 and Proposition 3 of the same paper.
The two finite inequalities, the bound on and the comparison of with , are elementary. The difficulty lies in part 1 for an arbitrary , which is a distribution on an infinite state space. Restricting attention to threshold policies is not free: Theorem 1 only says that Pareto-efficient mechanisms are thresholds. An arbitrary obedient must either be shown to be dominated by a threshold mechanism, or bounded directly. The sets are not compact in the obvious topology at , so the existence of an optimal mechanism cannot simply be assumed.
Part 3 needs a strict comparison. When , the proof must exhibit an obedient threshold policy strictly better than full information, which requires the obedience constraint to hold for thresholds slightly below .
Lean represents queue lengths as ℕ and distributions as functions ℕ → ℝ, inside the namespace NeedPersuasion.Homog. Every statement carries the standing assumptions M.Standing: , , , , for some , strictly decreasing, and non-increasing. The homogeneous statements add . The type-H utility stays a field of the model so that the definitions coincide with those of the sibling missions; with it does not enter .
Conventions the formalization commits to:
The following trivializations are excluded: defining "sm" as , defining it through sSup of an unbounded set or Classical.choose, computing from Lemma 5's closed form, or stating part 3 with both sides about the same threshold. A sorry-free sanity check exhibits a model satisfying all hypotheses (, , , ) with .
A complete development needs:
ℕ.The perturbation arguments behind Theorem 1 and the lemmas about threshold policies are reusable in the sibling missions. Proofs of any milestone are welcome. So are intermediate lemmas, such as closed forms for and of a threshold policy in the homogeneous case.
Perishable products (blood platelets, fresh food, pharmaceuticals) have a fixed lifetime: units not sold within periods expire and are discarded. Managing such inventory well is a classical problem in operations research, going back to Nahmias (1975). The difficulty is that the state of the system is the whole age profile of the stock, so the optimal policy depends on an -dimensional state and is intractable for realistic lifetimes. In practice firms use base-stock policies, which raise total stock to a fixed level every period, but until recently there were no theoretical guarantees for them in the perishable setting.
Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first such guarantees. Under FIFO issuance with zero lead time they define a simple heuristic level and bound its optimality gap explicitly (Theorem 1). This mission formalizes their Theorem 2: when demand is generated by a large population of customers, the optimality gap of the heuristic base-stock policy decays exponentially in the population size . This regime corresponds to high-volume products, where demand is the sum of many small individual requests.
The inventory system. Time is divided into periods . The product lasts periods. At the start of period the state is , where is the stock whose remaining lifetime is at most periods. The firm orders , raising total stock to (zero lead time). Demand is served oldest-first (FIFO); unmet demand is lost. The quantity expires, and the remaining stock ages by one period:
The system starts empty. Each period costs with , , . A policy chooses by a non-negative measurable function of the current state. Its cost is , and . The base-stock policy orders ; its cost is .
The heuristic level. With i.i.d. copies of the one-period demand , let
and let be any minimizer of over . is the newsvendor level of .
Demand population form (7). For a positive integer , the one-period demand is
where the customer demands are i.i.d., non-negative, with mean and variance , and the are i.i.d., non-negative, independent of the , with , variance , and for some . Thus is the number of renewals in ; when , and is compound Poisson with mean when the are exponential. , , , denote the objects above for demand , with fixed.
There exist constants , such that, for all sufficiently large and every minimizer of ,
The constants may depend on and the laws of and . The goal asserts only the exponential rate, not the explicit constants of the proof.
The proof also uses the FIFO results (Lemmas 1–2, Proposition 2 and inequality (21)) that are posed in mission 1 of this series; they are not restated here, and (23) is their consequence at the population demand.
The result. Theorem 2 shows that the heuristic base-stock policy, which is computed from a one-dimensional convex function, is nearly optimal for high-volume perishable products: the loss from ignoring the age profile vanishes exponentially as demand scales. Together with Theorem 1 (exponential decay in the lifetime) it explains why simple base-stock rules perform well in practice, and it gives a quantitative criterion for when a firm can stop worrying about the optimal policy.
Formalizing it. The result is proved in the paper; no part of it is machine-checked. A formalization adds a checked perishable inventory model (FIFO dynamics, admissible policies, long-run average cost), a random-sum demand model built on a renewal counting process, and checked versions of three classical probabilistic tools that the proof cites: Scarf's minimax bound for the newsvendor, Wald's identity with the law of total variance for random sums, and a lower-deviation bound for renewal counts from Bernstein's inequality for sub-exponential variables. The paper's justification of cites convergence in distribution, which does not imply convergence of variances; the statement is still true, and a formal proof has to supply the renewal variance argument.
The cost comparison itself is inherited from Theorem 1; what is new is controlling both factors of (23) as . The level grows linearly in , so the factor grows exponentially, and must be beaten by the decay of . Neither factor is explicit: is a quantile of a compound distribution, and has a random number of summands. Simply replacing by its mean is not possible, because the lower tail of must be shown to be exponentially small with a rate that does not degrade with ; this needs a concentration inequality for the renewal count, not only a law of large numbers. When the right side of (23) is zero, so the substantive case is , where the constants must be balanced to make the exponent negative. None of the needed tools (renewal theory, sub-exponential Bernstein, Scarf's bound) is in Mathlib.
PerishBaseStock.Population. Demand laws are CappedBaseStock.DemandLaw (non-negative, finite positive mean); the newsvendor functions come from LostSalesOrderUpTo.Asymptotic.Backorder; the renewal count is the counting variable N of SmithRenewal.Elementary at time .Fin (m - 1) → ℝ≥0 holding cumulative levels, with ; is allowed.Public and nonprofit services such as food banks, shelters, free clinics and legal aid often run with too little capacity and serve two kinds of users: people with no alternative, and people who have a reasonable outside option. When the queue is long, a user who has an alternative but joins anyway imposes waiting costs on everyone behind them, including the users who cannot go elsewhere. Pricing is usually ruled out in such settings, which leaves the provider one lever: what it tells arriving users about congestion.
Anunrojwong, Iyer and Manshadi (arXiv:2005.07253v3; Management Science, 2023) study this lever as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (Operations Research 67(5):1397–1416, 2019). The natural benchmark is full information: announce the queue length and let users decide. This mission formalizes the paper's answer to when full information can be improved for both user types at once, and by how much.
A single server serves users first come, first served, with exponential service times of rate . High-need users (type H) arrive as a Poisson stream of rate and always join. Low-need users (type L) arrive at rate and either join or take an outside option worth . Write . A type- user who joins with users already present receives utility . The standing assumptions are , for some , each strictly decreasing, and the increments non-increasing (Assumption 1).
By a revelation-principle argument (Lemma 1 of the paper, from Lingenbrink and Iyer), a recommendation mechanism that users obey is described by the queue's stationary distribution . An admission policy is a distribution with for all ; their set is . A signaling mechanism is an admission policy that also satisfies the obedience constraints
called (JOIN) and (LEAVE); their set is . The welfare of the two types is and . A policy Pareto-dominates if it is at least as good for both types and strictly better for one; is Pareto-efficient within a class if no member of the class dominates it.
A threshold policy , , admits L users when fewer than users are present, admits them with probability at , and turns them away above . Write , and for its welfare and (LEAVE) value. The full-information threshold is the smallest with , and the full-information mechanism is .
For , with fixed, there is a threshold such that some signaling mechanism Pareto-dominates if and only if , and
If moreover , , , and , then a signaling mechanism exists with
where and .
The proposition gives a clean regime split. Full information is already Pareto-efficient when low-need demand is light. Once crosses an explicit level, revealing everything leaves welfare on the table for both types, so a provider who cares about either group has a reason to hide some queue information. The lower bound on is explicit in the primitives, and the factors give a guaranteed improvement, not only an existence statement. Theorem 4, the milestone behind part 1, reduces the comparison to two adjacent thresholds.
The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. A formal development checks the "little algebra" steps that the paper compresses (the equivalence with , the welfare identities of p. 41–42). It also produces a reusable layer for persuasion in birth–death queues: obedient mechanisms as distributions, threshold policies, and Pareto efficiency within a class. The companion missions of this series (threshold structure, the homogeneous case, first-best) are stated over the same layer.
The threshold comes from analysing the sign of on . Translating "fi is not dominated" into that sign condition is where the work lies. The obvious attempt, comparing only with nearby threshold policies, settles one direction: if , the threshold dominates. The converse needs every competitor in , not just threshold policies. That requires the structure theorem for efficient admission policies, the existence of maximizers, and unimodality of , followed by a transfer from to that only works because (LEAVE) is slack at . The welfare series are infinite, and the threshold family is parametrised by a real whose fractional part enters nonlinearly, so the comparisons are not finite-dimensional linear algebra.
Everything is stated over a structure Model with real fields and utilities , with a predicate Standing holding the standing assumptions ( is encoded as ). Queue lengths are natural numbers, and the two types are separate fields. Membership in includes summability of and : the paper treats all welfare as finite, and an unrestricted tsum would assign to divergent welfare. is the right-hand form of (2), with no division by . A finite threshold requires , and a joining fraction in , as in Definition 2. Threshold policies are defined from their unnormalised weights, is as a distribution, and Pareto efficiency is Definition 1 within an explicit class. "Exactly one" is exclusive or.
Added hypotheses, each disclosed in the item that carries it:
The page's range is intersected with . In part 2, "" is read existentially.
Ruled out as trivializing: choosing after (the goal quantifies it once, with fixed); defining through its welfare; replacing Pareto efficiency by maximization of a weighted welfare; replacing exclusive or by inclusive or; and any constant that differs from the page's , or lower bound symbol for symbol.
A complete development needs geometric and arithmetico-geometric series, rearrangement of infinite sums over , and convexity arguments in the space of summable sequences. Proofs of any milestone are welcome, as are lemmas about threshold policies that the other missions of the series can reuse.
Many social services are rationed by waiting rather than by price: public health clinics, food banks, shelters, legal aid. Users who need the service most often have no outside option, while users with less need could be served elsewhere but join the queue anyway and lengthen everyone's wait. The provider usually cannot force anyone to leave, and charging money defeats the purpose of the service. What the provider does control is information: it observes the queue and decides what to tell arriving users about it.
Anunrojwong, Iyer and Manshadi (2023) model this as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (2019, Operations Research 67(5):1397–1416). Their first structural result, Theorem 1, says that whatever trade-off the provider makes between the two user groups, the efficient way to signal is a simple threshold rule, and that the threshold never exceeds the one under full information. This mission formalizes Theorem 1 and the steps of its proof.
A single server serves users first-come-first-served; service times are exponential with rate one. Users of two types arrive by independent Poisson processes: low-need users (type ) at rate and high-need users (type ) at rate , with total rate . A type- user who joins with users already present receives utility , where , for large , is strictly decreasing, and the increments are non-increasing (Assumption 1). High-need users always join; low-need users take an outside option worth unless joining is at least as good in expectation.
By the revelation principle and Lemma 1 of the paper, an obedient binary signaling mechanism is identified with its steady-state distribution of the queue length. The admission policies are the probability distributions on satisfying the detailed-balance constraints
The signaling mechanisms additionally satisfy the obedience constraints
The welfare of the two groups is and . A mechanism Pareto-dominates if for both , with at least one strict inequality; is Pareto-efficient within if no dominates it (Definition 1).
A distribution has a threshold structure (Definition 2) if for some , for and for : low-need users are told to join below , to leave above , and to join with probability at . The threshold is . The full-information threshold is the smallest with : when the queue is revealed, low-need users join exactly below it.
For every that is Pareto-efficient within , there is a finite such that
No weight is fixed: the statement covers the whole Pareto frontier.
Theorem 1 reduces an infinite-dimensional design problem (a distribution on subject to obedience) to a one-parameter family of threshold policies . Every later result of the paper is computed in that family: the bound of the optimal signaling mechanism against full information when all users are low-need (Proposition 1), the condition under which information design Pareto-dominates full information (Theorem 4 and Proposition 3), and the conditions under which signaling achieves the first-best admission policy (Theorems 5 and 6). The bound also has a direct reading: efficient persuasion only ever discourages low-need users relative to full information, never encourages them.
The theorem is proved in the paper (App. A). This mission produces a machine-checked version of the proof, on top of a reusable Lean model of obedient signaling in an -type queue with two user types. To our knowledge no part of this model or of its results has been formalized before.
The statement quantifies over the full Pareto frontier, so it cannot be obtained from first-order conditions of a single weighted objective. Both steps are perturbation arguments on infinite sequences: each must build an explicit competitor, keep it inside the detailed-balance constraints and both obedience constraints at once, and show weak improvement for one group with strict improvement for the other. The obedience constraint (LEAVE) cuts against (JOIN): moving mass toward shorter queues raises but can raise , and the bound on is where is needed. Since is allowed, the geometric tails are not automatically summable and the infinite sums have to be handled with care. The threshold must be excluded explicitly; it is not ruled out by the structure argument alone.
All definitions live in NeedPersuasion.Threshold (file Def_NeedPersuasion_Threshold_Model). Queue lengths are ℕ, everything else is ℝ; the two types are two fields of a Model structure. The standing assumptions are the predicate Model.Standing: , , , , for some (equivalent to for a strictly decreasing sequence, and allowing ), both utilities strictly decreasing, and the -increments non-increasing. Every theorem assumes it; no other hypothesis is added, and in particular is not assumed.
Committed conventions:
HasSum, and finite welfare: and summable. The paper treats the welfare sums as real numbers; without this, a policy with welfare (possible at ) would receive welfare from Lean's tsum.HasThresholdStructure; HasThresholdAtMost π y asks for a finite with .ParetoEfficientIn), never maximization of .Trivializing encodings are ruled out: the threshold-structure predicate is not satisfied by every admission policy, efficiency is taken over all of (including the competitors the proof builds), and no sum whose value is compared can be a divergent tsum. A sorry-free sanity file exhibits a model satisfying Standing whose full-information mechanism lies in , so the hypotheses are not vacuous.
A complete development needs manipulation of tsum over shifted and truncated sequences, geometric tails, and first-order stochastic dominance for sequences on ; these pieces are reusable for the other missions of this series (missions 2–4 restate the same model). Contributions of proofs of individual milestones, or of general lemmas on detailed-balance sequences, are welcome.
Many models in statistics, machine learning and engineering are nonconvex, nonsmooth and coupled by constraints: a sparsity penalty such as SCAD, MCP or capped- on one block of variables, a smooth loss coupling the blocks, and a nonlinear equality constraint tying them together. Augmented-Lagrangian methods and ADMM-type splittings are the workhorses for such problems, but most convergence theory for them assumes linear constraints or convexity. Zhu, Zhao and Zhang (arXiv:2007.12219v1, published in Mathematics of Operations Research, 2024) propose a first-order primal-dual method, NAPP-AL (nonconvex auxiliary problem principle with augmented Lagrangian), for a nonconvex problem with a nonlinear coupling constraint, and prove that it reaches approximate stationarity at a sublinear rate. This mission targets that rate result and the chain of lemmas behind it.
Fix dimensions . Problem (P) is
where and are differentiable with Lipschitz gradients, is lower semicontinuous and possibly nonconvex and nonsmooth, is closed and convex, is Lipschitz with constant , each component of has a Lipschitz gradient (constants , ), and is an matrix with . These are Assumption 1 (H1)–(H7); (H7) asks to be bounded below and coercive on the feasible set .
The augmented Lagrangian of (P) at is
Its stationarity set (p. 6) collects the triples with, for ,
where is the limiting subdifferential and the normal cone of . A stationary point is a with , and , with .
NAPP-AL takes a -strongly convex with Lipschitz gradient (Bregman distance ), a penalty (Assumption 2) and . With it sets to a global minimizer over of the linearized model
to the minimizer of a strongly convex quadratic, and . The step lies in , with given by the explicit formula (8), which depends on . The analysis runs through the potential
with explicit constants .
Under Assumptions 1 and 2, with set by (8),
The result gives NAPP-AL an iteration complexity of to reach an -stationary point (Remark 4.1), for problems with a nonlinear, nonconvex coupling constraint and a nonsmooth nonconvex regularizer, using only gradient evaluations and one proximal-type subproblem per iteration. It is also the base layer for the paper's later results: linear convergence under an error bound (Theorem 5.1) and the sufficient conditions for that error bound (Propositions 6.1–6.2) all start from Theorem 4.1 and Lemma 4.3.
The result is proved in the paper; nothing here is formalized elsewhere. A formal development adds a machine-checked Lyapunov analysis of an augmented-Lagrangian method with nonlinear constraints, with every constant explicit. It also records a correction: Proposition 3.1 as printed is false by a factor of at most , and the corrected bound is what the paper's proof establishes.
The difficulty is the dual variable. The multiplier update has no step size of its own, so the augmented Lagrangian itself need not decrease along the iterates, and the obvious descent argument for fails; the step of (8) depends on the current multiplier estimate , so even the step sizes are not uniformly bounded a priori. Boundedness of the iterates is not a hypothesis, and the iterates are infeasible, so coercivity of on the feasible set does not apply to them directly. The rate needs the residual bound of Proposition 3.1 with a constant uniform in , while depends on and . Passing to cluster points involves the limiting subdifferential of a nonconvex, nonsmooth , which is not closed under arbitrary convergence of its arguments.
EuclideanSpace ℝ (Fin k). The norm of a triple is the Euclidean norm of the stacked vector, defined explicitly; Mathlib's sup norm on products is never used. is a continuous linear map with its operator (spectral) norm and adjoint; is the Rayleigh minimum over the unit sphere.Metric.infDist (zero on ) is not used; with it, every residual bound would hold whenever is empty. The goal is stated as in , not as a big-O bound.NonconvexSplitting.Shared.LimitingSubdiff) and the normal cone of , which is empty off , so that stationarity forces .LocallyLipschitzOn); (full column rank, invoked in the proof of Lemma 4.2); (H7) is coercivity on the feasible set only.Contributions welcome: proofs of the milestones in any order, general facts about limiting subdifferentials and normal cones of convex sets (sum rule with a locally Lipschitz function, closedness under attentive convergence), and the "non-increasing summable sequence is " lemma. These are reusable beyond this mission. The source is the preprint arXiv:2007.12219v1, not the published version; all labels and constants are those of v1.
Retailers and restaurants increasingly deliver orders from their own stores within an hour or less. Orders arrive throughout the day, a fixed pool of drivers is based at the store, and in each dispatch wave the operator must decide how many drivers to send out now and along which routes. Sending many drivers now gives short delivery times for the current orders but leaves few drivers for orders that arrive while those drivers are still on the road. Liu and Luo (arXiv:2107.13058, Manufacturing & Service Operations Management, 2023) model this trade-off as a finite-horizon stochastic dynamic program and propose a rollout policy built on a tractable approximation of its cost-to-go. Their Theorem 1 justifies the approximation: with suitable parameters it lies below the true expected cost-to-go, with other parameters it lies between that cost and the cost of any feasible simple policy, and in the last period it is exact. This mission formalizes that theorem.
A store (the depot ) serves a finite set of customer locations over periods with strictly increasing decision epochs . A fleet of drivers carries at most items per trip; travel times , an on-site service time and a delivery target are given. At epoch the operator observes the demand of period : the set of locations with an order and the quantities , drawn from a finitely supported law , independently across periods.
The driver status records how many drivers are still en route in each period because of earlier dispatches, so drivers are available at . A decision is a set of depot-to-depot routes , one per dispatched driver. It is feasible if it uses at most drivers, serves every current order exactly once, loads at most items per route, and delivers every order within . The delivery times are and ; the cost of is . A driver whose route lasts longer than is counted as en route in period ; this is the transition (9) from to .
The cost-to-go is the minimum over feasible of the period's cost plus at the resulting status, with the period cost alone ((7)–(8)). The single-period cost is the minimum cost of serving the demand with at most drivers.
The approximation (10) replaces the future by single-period problems coupled only through driver counts:
where and the nonnegative parameters , , estimate how many of the drivers dispatched in period are still en route in period . A static myopic policy dispatches a state-independent number of drivers in each period and routes them to minimize the single-period cost; it is feasible from if it never asks for more drivers than are available and its single-period problems are always feasible.
For and a status with :
and for every .
The rollout policy AJRP of the paper solves, at each epoch, the current routing problem together with as a stand-in for the future. Theorem 1 is what connects that stand-in to the dynamic program: it shows that the en route parameters move the approximation between a valid lower bound and the cost of an implementable policy, and its exactness part yields the paper's Corollary 1 (AJRP is optimal for ). Lemma 1 shows the approximation keeps the monotonicity of the true value in the driver status.
The paper's proofs are in its Online Appendix (Appendix D). They are short but informal, and the formal statement here differs from the printed one in three pinned-down respects: the single-period cost is read with at most drivers, as the proofs use it; the upper bound is capped by the policy's cost, since otherwise it is vacuous; and the parameter choice printed for the upper bound has to be corrected in the last period. No part of the result has a machine-checked proof. A formal proof makes these readings definitive, and it produces a reusable Lean model of multi-period dispatching with routes, en route drivers and a Bellman recursion over a random demand.
Every part is a backward induction on the remaining periods, but the inductions run over a state that grows: the status depends on the durations of the routes chosen in period , and the infimum in (7) is over finite lists of routes, not over a finite action set. The lower bound needs that a larger status can only raise the cost; the upper bound needs that a policy which is feasible on its reachable states stays feasible after every realized demand. Exchanging the expectation with the minimum over the driver count in the last period is not a general fact and holds only because the single-period cost is nonincreasing in the number of available drivers. The obvious choice of parameters for the upper bound, the one printed in the proof, does not bound the last period's count and fails.
Locations are a type with the depot as none; periods are 1-based natural numbers and every statement carries . Costs and values lie in ; every minimum is an infimum, equal to on an empty feasible set; expectations are sums against the probability mass function of . A decision is a list of nonempty routes covering the current orders exactly once. The parameters are nonnegative reals by their type, with the diagonal written into (10). The available drivers in the dynamic program are in ; in APT the right-hand side is the real .
Standing assumptions, shared by every statement: ; strictly increasing epochs; finitely supported, period-independent demand laws; off . Added hypothesis: for (the en route drivers belong to the fleet). Disclosed readings: travel times do not depend on the period; delivery times follow the recursion of Appendix C with equality, starting from the depot leg; a policy's expected cost is defined recursively along its decisions.
Ruled out: defining or through the APT objective (exactness would become definitional); decision sets that may leave orders unserved (every cost would vanish); an upper bound without the cap by the policy's cost; negative parameters .
The development needs the model and its recursion (provided as one definition file), monotonicity of in , and induction principles for the well-founded recursions. Proofs of the milestones in any order are welcome; Lemma 1 is not used by the paper's proof of Theorem 1 but is a natural first step.
Repair access changes more than the cost of fixing a broken product. It also changes how many used products reach a resale market, what those products sell for, and whether a manufacturer prefers to sell another new unit or earn a repair margin. Jin, Yang, and Zhu study these connected pricing decisions in a two-period durable-goods model in Right to Repair: Pricing, Welfare, and Environmental Implications. Their Proposition 1 identifies the manufacturer's prices and the resulting market outcome when independent and manufacturer repair restore the same product quality. This mission formalizes that proposition, including all seven rows of its Table 1.
The question is relevant to work on durable-goods markets because a repaired product can compete with a new one in the next period. A lower independent-repair cost can affect the manufacturer's behavior even if consumers do not choose independent repair in the final equilibrium. The paper's setting makes that effect precise through the used-product price, new-product demand, and the manufacturer's repair decision.
A new product provides one period of use and then fails with probability . If it remains functional, or if a failed unit is repaired, it can be used for one more period as a used product. After two periods of use it has no value. Consumers have types uniformly distributed on . A new product gives per-period gross utility ; a functional used product gives , with . This mission takes the paper's identical-repair-quality case and zero resale transaction cost .
The manufacturer chooses a new-product price and a manufacturer repair price . Producing a unit costs and repairing it costs . A consumer can instead pay for independent repair. A manufacturer repair price of means that service is unavailable. The used-product price emerges from the secondary market. Consumers who face a failure repair with probability : they repair whenever the resale gain exceeds , do not repair when it falls short, and may mix at equality.
Consumers can be inactive, buy a used unit every period, or buy a new unit every period. Their corresponding per-period utilities are , , and
The thresholds partition these choices. In a market with a positive used price, used demand equals the supply generated by new buyers: . At , used supply may exceed demand. The manufacturer's per-period profit combines new-unit margin with its repair margin on units it actually repairs. These primitives and Assumption 1 appear in §4.1 of the paper.
Lemma 1 states that consumer utility has the three-segment form above. The appendix then compares reduced pricing problems for no repair, full repair, and partial repair. One milestone records the full-repair optimum:
at a feasible full-repair maximizer. Other milestones record the profit-gap identities, the ordering of two production-cost cutoffs, and the appendix results for the two higher ranges of independent-repair cost. Their statements follow Online Appendix G.
The goal is the complete equilibrium characterization of Proposition 1 and Table 1. When , the optimal outcome changes at and from no repair to partial repair to full repair. When , three cutoffs give four rows: two no-repair regimes, partial repair, and full repair. Each row specifies , , , and ; the partial-repair rows require . The target fixes the paper's explicit formulas rather than only the number or order of the regimes.
The theorem gives a simultaneous answer for manufacturer pricing and the secondary-market outcome. It identifies when manufacturer repair is unused, offered to some consumers, or offered to all consumers facing failure. In the low- case it also distinguishes two no-repair regimes with different used prices. Those distinctions matter for subsequent welfare and environmental comparisons in the paper: a price change can alter new production and resale quantities even when the repair count does not change.
The paper proves Proposition 1 analytically; this mission asks for a machine-checked proof of its exact statement. A complete development would also establish reusable interfaces for a market-clearing equilibrium with a zero-price excess-supply corner, price optimization across several feasible regimes, and comparisons between algebraic cutoff formulas. The draft theorem statements are open Lean goals; the local sanity check proves that one specified market equilibrium is inhabited, not the proposition itself.
The manufacturer's choice affects both the direct repair margin and the resale price that determines demand for new and used goods. Optimizing the new-product price in isolation therefore does not give the global result. The appendix's candidate solutions come from distinct repair and market-clearing regimes, and their feasible sets meet at cutoffs where different prices can tie. A global claim has to compare each candidate against all admissible price pairs and their equilibria. The radical and rational cutoff formulas add boundary cases: a formula may be used only in the regime where its denominator and square-root argument have the intended meaning.
Lean uses real prices, costs, probabilities, and consumer thresholds. The standing assumptions are , , , and the paper's Assumption 1, and . It also pins the three unit costs to , consistent with the paper's nonnegative-cost appendix domain. An unavailable manufacturer repair service is represented by none, not by an arbitrary large real number. A real repair price must be nonnegative.
The equilibrium predicate requires actual utility-maximizing consumer segments, the repair rule, and market clearing. It allows excess used-product supply only at . It also admits the appendix's zero-demand outcome, in which neither product yields positive utility, no units sell, and profit is zero. An optimal outcome contains an equilibrium and beats every equilibrium at every admissible competing price pair. Thus an empty equilibrium relation cannot make the goal true. At cutoff ties the theorem asserts that the displayed prices are an optimum, without claiming uniqueness. The two partial-repair rows assert strict bounds on , excluding a vacuous value.
The appendix's Problems 1, 4, and 5 are separate reduced objectives and feasible sets. The rational partial-repair objective is accompanied by its polynomial continuation for the profit-gap identity; that continuation is used only where the printed rational form could produce . The source's second identity in (G.41) omits a factor in its denominator. The Lean statement uses the corrected algebraic identity, while the milestone preserves the printed line. Contributions that prove the consumer, reduced-problem, cutoff, and global-optimality milestones are all within scope. The remaining propositions on welfare, quality differences, and environmental effects are outside this mission.
b869b33a21376a298a2355fb4de697d59b1362d5895f166f3255348812bc1763.On-demand delivery platforms for meals and groceries promise delivery within minutes, and the main operational lever they control is how a courier is dispatched. A courier can carry each order as soon as it is ready (dedicated delivery), or wait until two orders are available and deliver them in one trip (batch delivery). Batching saves travel per order but makes the first customer wait for a second order to arrive. Which mode gives the shorter wait, and hence the higher revenue, is a question practitioners face daily; it is the subject of M. Chen and M. Hu, Courier Dispatch in On-Demand Delivery (SSRN 3675063; published in Management Science, DOI 10.1287/mnsc.2023.4858).
The paper answers the question in closed form for a stylized disk model. This mission formalizes its first headline result, for the case in which the demand rate is fixed exogenously (for example by a growth target or by kitchen capacity), as stated in Propositions 1 and 2 of the authors' version dated 2022-09-21.
A vendor sits at the centre of a disk of radius and employs one courier with unit travel speed, so travel time equals travel distance. Customer orders arrive as a Poisson process of rate , the demand rate, and each customer's location is independent and uniformly distributed on the disk.
Under dedicated delivery each trip is a round trip to one customer, of length with uniform on the disk. Its moments are and , so the courier is an M/G/1 server with
where is the service rate and the summed coefficients of variation. The paper defines the expected wait under dedicated delivery as the M/G/1 in-line delay
Under batch delivery the courier leaves only with two orders and visits both, so a trip has length for two independent uniform points, with . This gives
and a variability coefficient that the paper obtains by numerical integration. The paper defines the batch wait as the time for a second order to arrive, plus Kingman's approximation of the E/G/1 in-line delay, plus the expected delay of being second in a batch:
Customers have valuations with c.d.f. on and a wait cost per unit time; at price the potential arrival rate thins to . The vendor's revenue rate at demand rate and expected wait is
Dedicated delivery is stable exactly when ; batch delivery when .
For every there is a constant such that for all , with ,
and the same two equivalences hold for the revenues and , for every , every with , and every . The paper reports ; the goal asserts only the existence and the location in .
The result says that, with demand fixed, the choice between dedicated and batch delivery depends on the market only through the product : dedicated delivery is better when demand is low or the area small, batching when demand is high or the area large. The threshold is a single universal number, independent of the valuation distribution and of the wait-cost rate, because at a fixed demand rate the strategy with the shorter wait always earns more. This is the efficiency-driven benchmark against which the paper's second main result (endogenous demand in a crowded market, where the order reverses) is contrasted.
To our knowledge none of this has been machine-checked. The mission produces a checked version of the paper's closed-form comparison and, in milestones 1–2, checked computations of classical geometric-probability moments of the disk (the mean distance between two uniform points). The paper's own argument for the single crossing is numerical ("solved using standard methods"); a formal proof must replace it by an exact argument with rigorous bounds on .
The reduction to one variable is algebra. The difficulty is the sign analysis of on : it is a difference of two rational functions with poles at and , involving , and clearing denominators gives a cubic whose roots the paper only reports numerically. The natural first idea, showing is monotone on the whole interval, does not apply directly, since starts at , first decreases, and only later rises to ; a proof must establish that it crosses zero exactly once. A further point is that is not a closed-form number, so the crossing must be shown uniformly over an interval of values.
The moment milestones need integration in polar coordinates on the plane; the mean distance between two uniform points of a disk is a classical but nontrivial four-dimensional integral.
All objects live in the namespace CourierDispatch.Exogenous. Real numbers are ℝ, is lam, is Lam, and is an arbitrary function Q : ℝ → ℝ (no property of it is needed, since at equal the price terms cancel). The plane is EuclideanSpace ℝ (Fin 2) and the uniform law on the disk is Lebesgue measure conditioned on the closed ball.
Committed conventions:
Q stands for ; its properties cancel when the two strategies are compared at the same demand rate.The threshold (and , ) is existential in every statement; it is never a definition and never an infimum of a sign set, and , are never defined through , so the goal cannot be made true by construction.
Needed infrastructure: polar-coordinate integration on the plane (Mathlib's integral_comp_polarCoord_symm), and rigorous rational bounds on (Real.pi_gt_d6, Real.pi_lt_d6). The goal does not depend on the moment milestones 1–2, which ground the constants , , in the geometry of the disk and are welcome as separate contributions.
Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that has not been used within periods of its arrival must be discarded. Managing such stock is a classical problem of inventory theory, going back to Nahmias (1975), and it remains of practical interest for hospital blood banks and grocery retail. The difficulty is structural. The state of the system is the whole age profile of the stock, a vector of dimension , and the optimal policy depends on all of it. Dynamic programming over this state is intractable even for moderate lifetimes, so practice relies on simple heuristics, above all base-stock policies, which raise the total stock to a fixed level every period.
For decades the performance of base-stock policies in this system was understood only numerically. Chazan and Gal (1977) and Cooper (2001) bounded the long-run outdating of a base-stock policy; Nandakumar and Morton (1993) built a base-stock policy from bounds on the optimal order-up-to level and showed numerically that it performs close to optimal. Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first theoretical guarantees, comparing a simple base-stock policy with the optimal policy in several asymptotic regimes. This mission formalizes the first of them: the optimality gap decays exponentially in the lifetime .
Time is discrete, . Demands are i.i.d. copies of a nonnegative random variable with and distribution function ; .
At the start of period the state is , where is the stock whose remaining lifetime is at most periods. The firm orders , which arrives immediately and raises the total level to (with ). Demand is served oldest-first (FIFO issuance) and unmet demand is lost. Stock reaching the end of its life is outdated:
The system starts empty. Each period costs
with holding cost , lost-sales penalty and additional outdating cost . A policy is admissible if each order is a nonnegative measurable function of the current state; is the set of admissible policies. The long-run average cost is , and .
The base-stock policy orders ; its cost is . The heuristic level is a minimizer over of
and is the newsvendor level.
For every and ,
The bound holds for every minimizer and every demand law with positive finite mean. Since , the gap decays exponentially in .
Theorem 1 says that a single explicit base-stock level, computable from the demand law by a one-dimensional convex search, is nearly optimal once the lifetime is moderately long, with an explicit, distribution-dependent rate. It explains why the non-perishable newsvendor intuition carries over to long-lived products, and it is the first of seven guarantees in the paper. Its ingredients are reused throughout: Lemmas 1 and 2, Proposition 2 and the gap bound (21) are posed in this mission and used, without restatement, by missions 2 to 4 of this series (demand population size, penalty cost, outdating cost).
The result is proved on paper; nothing about perishable inventory has been machine-checked. A formal development would provide a reusable model of FIFO perishable dynamics with long-run average costs, sample-path inequalities for outdating, and the first verified optimality-gap bound for an inventory heuristic in a high-dimensional state space.
Most of the argument is sample-path bookkeeping plus Jensen's inequality, but two steps are not routine. Lemma 1 asserts that the long-run average outdating of exists and does not depend on the initial state. The natural route through a stationary distribution fails: when the chain can be periodic and has no steady state, so the identity must hold for Cesàro averages directly; in the aperiodic case the paper uses a minorization condition (Meyn and Tweedie, Theorem 16.0.2). Proposition 2 compares every admissible policy with the heuristic cost, which needs the independence of the order-up-to level from current and future demands, and a conditional Jensen step for nonlinear expectations of a policy-dependent quantity.
The Lean development fixes the following conventions.
Fin (m - 1) → ℝ holding the cumulative levels, with , so (empty state, all leftover stock outdates) is included; , , , are fields of the parameter record.ℝ≥0).CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.Trivializing readings are excluded: is the simulated cost of , not a formula; ranges over all admissible policies, not only base-stock ones; is the argmin predicate, not a closed form; , and the demand law are general; and no gap is stated with truncated subtraction. Contributions of any of the milestones, of general facts about Cesàro limits of Markov chains, or of the convexity of , are welcome.
Decentralized exchanges on public blockchains do not match buyers with sellers through an order book. Most of them trade against a liquidity pool: a smart contract that holds reserves of two tokens and quotes a price by a fixed formula. The most widely used formula is the constant product rule of Uniswap (Adams, Zinsmeister and Robinson, 2020), under which a trade must leave the product of the two reserves unchanged. Pools of this kind settle a large share of on-chain token trading, and their pricing rule is fixed in code, visible to every participant, and executed in the order in which transactions are included in a block.
That last feature creates a market-structure question. Pending transactions are public before they execute, so another trader can see an order and place her own trade ahead of it. The empirical literature documents this behaviour at scale (Daian et al., 2020; Zhou et al., 2021). Park's paper asks which properties of the pricing rule itself make such strategies profitable, independently of any information the front-runner has. The paper compares the constant product rule with the cost function of a traditional market maker whose marginal price is linear in quantity, in the tradition of inventory models such as Biais (1993), and then derives four properties of constant product pricing in its Proposition 3.
Timeline:
A pool holds units of a token and units of a token . A trader who takes units of out of the pool pays units of , where is fixed by the constant product invariant
A positive is a buy of ; a negative is a sale of units of into the pool, and then is negative: the trader receives . Solving the invariant gives the paper's cost function, equation (3):
After a buy of the pool holds units of and units of . Selling units of into a pool therefore earns units of . The paper writes for on the current pool.
For the companion comparison the mission also defines the linear market maker's cost , where is the fundamental value, the number of market makers, their excess inventory and a liquidity factor.
For , and :
Part (1) says that splitting an order in time does not change its cost; part (3) that splitting liquidity into identical pools, with the order split pro rata, does not change it either. Part (2) is the front-runner's profit: she buys , the victim buys , and she sells into the pool left by both buys. Part (4) is the profit of selling into a pool just moved by a buy of and buying on an identical untouched pool, for every .
A companion item poses Proposition 1: with , , and , constant product pricing has a larger signed cost than linear pricing for , and a smaller one for , .
Parts (1) and (3) are the consistency properties one asks of any market maker: an order's cost does not depend on how it is sliced in time, or on how liquidity is fragmented across identical venues. Parts (2) and (4) show that the constant product rule, despite these properties, rewards anyone who can trade ahead of an observed order or across two identical pools. These are properties of the pricing curve alone, with no informational advantage, which is what makes them relevant to the design of on-chain exchanges, transaction ordering rules and fee schedules.
All statements are proved in the paper by direct algebra, and they are not open. What this mission adds is a machine-checked record of the exact statements, with the paper's printed sign slips resolved explicitly, and a reusable definition of the constant product cost function in Lean on which statements about fees, multi-hop routing or other invariant curves can build. No machine-checked version of Proposition 3 is known.
The mathematics is rational-function algebra; the difficulty is in stating it correctly. Three points need care. First, the sale convention: the paper's cost function returns a negative number for a sale, while the printed statements of parts (2) and (4) add that number as if it were the positive proceeds. Read literally, both printed left-hand sides are negative. Second, the pool after a trade must be tracked exactly: part (4) prints the first pool's reserve as , whereas after a buy of it is . Third, every quantity is a ratio with a denominator such as , or , and the statements hold only on the domain where those are positive. A solver who simplifies before checking signs will prove the wrong inequality.
Everything lives in the namespace CPAMMFlaws.Properties over the real numbers. The definition pcmm x X Y := x * Y / (X - x) is equation (3) verbatim, argument order ; ptmm x V ℓ N I is the printed closed form of . Conventions committed to:
Trivializing formalizations are ruled out: Lemma 2 is the invariant characterization over all , not the defining equation of pcmm; parts (2), (4) and equation (4) are strict inequalities on the signed proceeds, not and not absolute values; and no statement drops .
Out of scope: the paper's CARA-normal market-maker equilibrium (Lemma 1), its results on the linear market maker (Proposition 2), the fee analysis of §IV and the calibration of §V. The linear cost enters only through the companion Proposition 1. Contributions welcome beyond the milestones: proofs of the goal's parts directly, and further invariant-curve properties built on pcmm.
Best subset selection fits a linear model using at most of available predictors: it minimizes the residual sum of squares over all with at most nonzero coordinates. It is the classical benchmark for sparse regression, and mixed-integer optimization has made it computable at scales that used to be out of reach (Bertsimas, King & Mazumder, 2016). When the signal-to-noise ratio is low, however, best subsets overfits, and Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty () to it. Their oracle inequalities for the penalized estimators hold for a fixed model size , and the practitioner still has to choose .
§3.5 of the paper removes that choice. It replaces the cardinality constraint with BIC-type penalties that depend on the candidate model size, and Theorem 5 shows that the resulting estimators satisfy oracle inequalities for the expected prediction error over all of , with no condition on the design beyond the normalization of its columns. This mission formalizes Theorem 5 and the steps of its printed proof.
We observe . The mean is deterministic and unknown, and has independent entries with . The design is deterministic, with and columns of unit Euclidean norm. The prediction error of an estimate is . For , is the Euclidean norm, , and is the number of nonzero coordinates.
For nonnegative tuning parameters and , the data-dependent penalties are
with the convention , so the empty model is not penalized. The BIC-type estimators are
where is a fixed number. Both are unconstrained problems. Solving them is equivalent to solving the constrained problems with for each and then choosing by the penalty. A minimizer exists but need not be unique.
The proof works on events of the noise vector. For an integer and the event requires
There exist universal constants such that, if or ,
and, if or ,
Here hides one universal multiplicative constant. The constants are not specified, so the goal records the shape of the bound and is not invalidated by later improvements of the constants.
The result. Theorems 2 and 3 of the paper give oracle inequalities only over the sparsity class for a fixed in advance. Theorem 5 makes the model size data-driven. Its bounds hold over all of and need no restricted-eigenvalue or sparse-eigenvalue condition on . Corollary 6 of the paper deduces from it that the estimators attain the error rates of Corollaries 3 and 4 while selecting models of the same order as the true model size. The paper also notes that the slow-rate bound for with is a bound for the Lasso.
Formalizing it. Theorem 5 is a published result with a printed proof (Supplement B.13). The proof is written up to unspecified universal constants, and it defers two steps to other parts of the paper ("repeating the argument after inequality (32)" and "repeating the argument in the proof of Corollary 3"). A formal proof makes every constant and every deferred step explicit. No part of the paper has been machine-checked, to the best of our search.
The argument is long rather than deep. The obvious first attempt fixes the selected model size and applies a high-probability bound for that size. This fails because is random and depends on , so a bound for each fixed says nothing about the random . The noise term must be controlled simultaneously over all model sizes, at a total failure probability that does not grow with . The second obstacle is the passage from high-probability bounds, which hold for every and grow like , to a bound in expectation. That passage needs the high-probability statement with a constant that is uniform in .
Representation. Vectors are Fin n → ℝ and Fin p → ℝ, and the design is a Matrix (Fin n) (Fin p) ℝ.
l2, l1, l0), because Mathlib's norm on Fin m → ℝ is the sup norm.noiseLaw).Model. The standing hypotheses are:
The quantities , , , , , and the penalties are inputs. The randomness is the law of alone, and .
Estimators are argmin predicates IsBIC2, IsBIC1: " minimizes the objective over all of ". Every statement holds for every minimizer.
Constants.
Correction. Theorem 1 of the paper states for an event with coefficient on . That bound is false for small (already for ). The union bound here uses the corrected event with coefficient , which inside changes nothing downstream.
Ruled out. None of the following counts as a formalization of the goal:
Not formalized here. The fixed- oracle inequalities (Theorems 2 and 3), the noise events of Theorem 1, the lower bound (Theorem 4), Corollaries 1–6 and the numerical study are not part of this mission. Some of them are the subjects of the other missions of this series. The proof of Theorem 5 needs the probability bounds for the events and of Theorem 1 and the deterministic arguments of Theorems 2 and 3. A solver may prove them here or import them once they are published.
Contributions welcome.
These are reusable well beyond this paper.
Best subset selection fits a linear predictor using at most of available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.
An penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.
Let be a fixed design matrix whose columns have Euclidean norm one. The observation is , where is a fixed mean and the coordinates of are independent random variables, with . The result below fixes one realized noise vector and assumes it lies in an event stated below. No assumption that is itself a linear combination of columns of is required.
For , write , where counts nonzero coordinates. An -regularized best subset estimator is any minimizer
The objective has no factor . The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is . When and its domain is nonempty. Write for the decreasing rearrangement of .
The paper defines three noise events used here. bounds the largest coordinate of by . On , every satisfies
On , every satisfies . Here and all logarithms are natural. These definitions, including the constant in , are the printed deterministic events of p. 13.
At , Theorem 3(A) states
For , a positive universal constant gives
For every , a positive universal constant gives
The multiplying distinguishes this rate from the -penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.
Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on . The second keeps a linear penalty term when meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.
The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the bound, the rearranged-coordinate bound, the case split and the sparse step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the -penalized estimator, or the event-probability theorem.
The constraint makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on and a maximum of a sorted-coordinate term and a prediction-norm term on . The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor in the fast rate would state a different theorem.
Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for . Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index is j.val + 1; the sum using is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.
The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every , avoiding the default value of an empty or unbounded real infimum. The standing conditions are , unit-norm columns, and . The first slow-rate branch retains the paper's equality for . The fast branch additionally requires or : this makes the term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original constant; this mission makes only a deterministic claim on that event.
The sparse domain for is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on , , , or , and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.
A retailer can pay a supplier when it places an order or after the supplier delivers it. When production yield is uncertain, the choice changes who bears the cost of missing units. It can also change the supplier's production decision and, through the amount available for sale, the surplus received by consumers. Geng, Guo, Xiao and Yang study these effects in a decentralized supply chain and show that payment postponement can help all three parties, hurt all three, or benefit some while hurting others, depending on production cost and the retailer's pricing rule. Their Proposition 4 gives the precise cost intervals for these outcomes in the SSRN author version, pp. 19–20.
The result matters to contract design in supply chains where realized output can be below planned production. Paying for units ordered and paying for units delivered allocate that shortage differently. A comparison based only on the retailer's expected profit would miss the effects on the upstream supplier and final consumers. Proposition 4 keeps all three outcomes visible while holding the retailer's pricing policy fixed.
There is one supplier and one retailer. The supplier chooses a wholesale price and plans production at cost . The retailer orders and sells to a market with linear demand , where and is the retail price. The yield factor equals with probability and with probability , with . Thus . The retailer receives units; the production cost applies to planned , including units lost to yield risk §3.1–3.2.
Under pay-by-order, the retailer transfers to the supplier and the supplier produces . Under pay-by-delivery, the transfer is and the supplier can choose a larger production quantity. Under ex ante pricing, the retailer fixes before yield is known. Under responsive pricing, the retailer sets after observing delivery. Combining payment and pricing gives OA (order, ex ante), OR (order, responsive), DA (delivery, ex ante), and DR (delivery, responsive). The supplier first sets , the retailer next orders and possibly fixes a price, the supplier chooses production, yield is realized, and responsive pricing occurs last Table 1, p. 9.
Both firms maximize expected profit at every stage. A subgame-perfect equilibrium is a complete plan of choices after every history in which each choice is optimal at that history. For scenario , write and for equilibrium retailer and supplier profit. The consumer surplus is expected surplus from sales: for delivered stock and market price , the model integrates inverse demand less from zero to . This is the paper's priority allocation convention for consumers with the highest willingness to pay p. 10.
The main target is Proposition 4, which compares OA with DA and OR with DR. Let mean the delivery-payment outcome minus its order-payment counterpart. A plus sign below means a strict increase, a minus sign a strict decrease, and zero equality. The admissible cost range is .
For ex ante pricing, with no restriction , the paper gives a threshold and the following pattern:
For responsive pricing, assuming , the pattern is on , on , on , and on . The thresholds are those specified in the paper: is equation (6), is equation (8), and the scenario cost thresholds come from Appendix B. The first ex ante interval can be empty for some parameters; its printed endpoints are retained. The milestones establish the supplier's production and responsive pricing rules, the four scenario outcomes, and the threshold ordering used in the comparison Appendices B–C.
The theorem separates the effect of changing the payment contract from the effect of changing the pricing rule. For advance pricing it identifies an interval where payment postponement helps both firms and consumers, then an interval where consumers lose despite both firms gaining. For responsive pricing the direction of every effect can reverse as cost passes successive thresholds. At high cost the change in payment timing leaves all three equilibrium outcomes unchanged Proposition 4, pp. 19–20.
The paper derives the equilibrium formulas in Appendix B and proves the comparisons in Appendix C. The result is therefore a known mathematical claim, while this mission asks for a machine-checked development from the sequential game through the cost-dependent equilibrium outcomes and final comparisons. The definitions of a two-point yield game and its complete contingent strategies can support other formal studies of payment or pricing postponement. There is no claim that Proposition 4 already has a machine-checked proof.
The supplier's production payoff has kinks at and . The retailer's best order changes when those production choices change, and responsive pricing adds another kink when delivered stock crosses . As wholesale price varies, the supplier must compare outcomes on both sides of these changes. Consequently a single first-order condition for a smooth objective does not characterize the equilibrium. The cost thresholds also depend on square roots and comparisons among several formula pieces, including the larger root chosen for Appendix B, pp. 33–37.
Lean represents expectation by the two weighted yield outcomes. Production cost is a separate argument, so thresholds depend only on . Parameters satisfy , , and . Wholesale and retail prices obey the strict admissibility bounds of equation (3). Orders are nonnegative; pay-by-delivery production is nonnegative; pay-by-order production equals the order. Consumer surplus is a real interval integral. Every comparison quantifies over actual subgame-perfect equilibria, and the goal separately asserts that the compared equilibria exist at every admissible cost. Equilibrium profits are computed from strategies and transfers, rather than defined to equal the Appendix B formulas.
The paper's statements require care at ties. The model selects when that is a profit-maximizing pay-by-delivery production choice, including the indifferent DR regime. The printed middle DR consumer-surplus expression combines outcomes from different production choices; the equilibrium-consistent expression is used here, and Proposition 4(R)'s comparison remains valid under either expression. Equation (2) swaps the scenario labels of committed and responsive prices, so consumer surplus uses the actual ex ante price in OA and DA and the price after delivery in OR and DR. The printed in Appendix B.1 is read as , as in Lemma 1. Outcome claims use open cost intervals because uniqueness at exact thresholds fails; equilibrium existence remains part of the targets there. The threshold is the larger root of the relevant quadratic factor, and and use the paper's explicit formulas. These conventions are recorded in the local moderation notes.
The development calls for real inequality reasoning, optimization of piecewise objectives, and careful handling of interval integrals. Contributions that prove the production and price best responses, establish the four equilibrium lemmas, or verify the threshold order each advance the final comparison.