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?
In 2018 New York City's Taxi and Limousine Commission adopted a minimum earnings rule for ride-hailing drivers: each platform must pay drivers, per hour spent with a passenger, at least a target hourly earnings level divided by the platform's measured driver utilization in the previous period. The rule ties next period's wage floor to this period's idle time, so a platform that over-recruits drivers must raise wages. Asadpour, Lobel and van Ryzin (SSRN 3502607, published in Manufacturing & Service Operations Management, 2022) model this rule as a dynamical system and ask when the regulated marketplace can stay stable, meaning wages stay bounded while the platform does not lose money.
Their main result (Theorem 1, a separate mission of this series) characterizes stability in a deterministic market. Real markets are hit by demand shocks: a sudden drop in ride requests lowers utilization in one period, and the rule then forces a high wage in the next. This mission formalizes the paper's answer (Theorem 2, §4.1) to whether a platform that may not subsidize rides can absorb such a one-time shock.
Time is discrete. In each period the platform chooses a price per ride hour and a wage per ride hour. The demand is the number of ride hours requested at price ; the supply is the number of driver hours offered when drivers earn per hour. Rides served are , the utilization is , and drivers' hourly earnings solve the equilibrium condition
A price, wage and earnings sequence satisfying this in every period is an equilibrium-augmented policy. The platform's profit is . With target , the minimum earnings rule requires
The revenue and cost functions are and . The paper assumes positive, strictly decreasing and continuous; strictly increasing, continuous, and positive and differentiable away from ; unimodal with maximum at ; and demand and supply crossing at , . is the inverse of , and is the inverse of on its decreasing branch: iff and .
A shock lowers utilization to in one period. A marketplace absorbs a utilization shock (Definition 3) if some feasible equilibrium-augmented policy obeying the rule, with first post-shock wage , has bounded wages and non-negative profit in every period.
The threshold is explicit in the model primitives; no constant is chosen by the formalization.
The result. Theorem 2 quantifies the fragility of a regulated marketplace whose platform cannot cross-subsidize: there is a sharp utilization level below which a single shock sends wages into unbounded growth, and above which the platform recovers immediately with a zero-profit stationary policy. Its threshold depends on the market only through the decreasing branch of revenue and the cost of paying , which makes it a concrete design criterion for the target : a regulator choosing also chooses how deep a utilization drop the market can survive. The remark after the theorem (p. 14) relates it to the stability threshold of Theorem 1.
Formalizing it. The result is proved in the paper; no machine-checked version exists. A formal proof must close points the published argument leaves implicit: the reduction to policies (the paper's Lemma 3, posed in mission I) must hold in the all-periods form used here; the wage recursion of Lemma 4 needs wages above , which the proof does not check; and the sufficiency policy needs , which holds only because utilizations are at most one. The mission also gives the platform a second, independent use of the shared marketplace model.
The sufficiency direction is a direct check of one stationary policy. The necessity direction is where the work lies. The natural attempt, to argue that a high first wage simply cannot be paid without loss, fails: profit only requires , and a platform may raise its price along with the wage. The obstruction is dynamic. Raising the price above lowers revenue below the cost of supplying earnings , so equilibrium earnings fall below , utilization falls, and the rule raises the next wage by a factor bounded away from one. Turning this into a proof requires controlling arbitrary policies with , not just the convenient , and carrying an induction hypothesis (wages stay above ) that the paper does not state.
The Lean development lives in namespace MinEarnings.Shock. Demand and supply are functions D S : ℝ → ℝ; all regularity is required on , and "differentiable" is read as differentiable on , which is all the argument uses. " unimodal with maximum at " is strict increase on and strict decrease on . The points , and the inverse cost are parameters carrying their defining properties. Time is 0-based: Lean's period is the paper's period , so the shock constraint is a bound on Lean's first wage and the rule constrains every later wage. Bounded wages means , and profit is non-negative in every period.
Three conventions are pinned and disclosed in every statement:
The development needs only Mathlib's real analysis: monotonicity on intervals, inverse functions on , and geometric growth of sequences. The setting file is shared, up to namespace, with the other two missions of the series. Contributions welcome: proofs of the milestones, a proof of the all-periods reduction to policies, and a general lemma that a sequence with , , is unbounded.
In 2018 New York City's Taxi and Limousine Commission (TLC) imposed a minimum pay formula on the largest ride-hailing platforms, following a proposal by Parrott and Reich (2018): the pay per minute and per mile driven is divided by the platform's utilization rate, the fraction of drivers' working time spent carrying passengers. Seattle adopted a similar rule in 2020. The rule targets drivers' hourly earnings while leaving them free to choose when and how much to work. Because utilization is only observed after the fact, the regulation computes the floor for the next measurement period (six months in New York) from the utilization of the current one.
Asadpour, Lobel and van Ryzin (2022) model this rule as a dynamic system and ask when a platform can comply with it while keeping wages bounded and profits non-negative. This mission formalizes their Theorem 3: the lag in the rule does not matter for stability, because the dynamic system is stable exactly when a single static system of equations has a solution. Two companion missions of the series formalize Theorem 1 (the threshold on stable earnings targets) and Theorem 2 (absorption of a utilization shock).
Time is discrete. In period the platform charges riders a price per hour of driving and pays drivers a wage per hour of driving riders. A demand function gives the ride hours demanded at price , and a supply function gives the driver hours offered at expected hourly earnings . The regularity assumptions are that is positive, strictly decreasing and continuous, and is strictly increasing, continuous, and positive and differentiable away from zero. The ride hours produced, the utilization and the platform's profit are
Drivers earn only while busy, so earnings satisfy the equilibrium condition . The minimum earnings rule with target is
The -minimum-earnings marketplace is stable if some policy that is feasible, satisfies the equilibrium condition and obeys the rule has a bounded wage sequence and in all but finitely many periods. It is statically stable if there are and with
The statement carries only the regularity assumptions on and and .
The milestones follow the proof in the Online Appendix.
Theorem 3 reduces a question about infinite sequences to a question about one system of four relations in four unknowns. The paper uses it to give a second proof of its threshold theorem, and it shows that the lag in the regulation cannot be blamed for instability: every earnings target that a real-time rule could sustain can also be sustained under the lagged rule, and conversely. This gives regulators and platforms a criterion that can be checked by solving equations rather than by simulating policies.
The result is proved in the paper. No machine-checked version of it or of the paper's other results exists. Formalizing it checks the passage to the limit in the dynamic-to-static direction, where the paper leaves one step implicit (the positivity of the limiting utilization), and it provides a Lean model of the regulated marketplace that the other two missions of the series share.
The static-to-dynamic direction is immediate. In the other direction, a stable policy is a sequence, and a solution of (8) is a single point. Fixing one period of a stable policy does not give such a point: the rule compares with , while (8) compares with the utilization of the same point. A solution has to be extracted either from a period where the comparison happens to go the right way or from a limit. The limit is delicate because the utilization is a ratio, and a limit with would not solve (8). The positivity of the limiting utilization has to come from the rule and the bound on wages together. The reduction to policies with (Lemma 3 of the paper) also has to be carried out on the policy before the case analysis can start; that lemma is posed as a milestone of the first mission of this series and is not repeated here.
Prices, wages and earnings are real numbers, and are constrained on . A policy is a triple of sequences indexed by starting at , so Lean's period is the paper's period , and the rule constrains every wage except the first. "Bounded" is an upper bound on the wages, which are non-negative; "all but finitely many periods" is an eventually-along-atTop statement. "Differentiable" is read as differentiability on together with continuity on .
The equilibrium condition requires . Without it the encoding is trivial: if , which the assumptions allow, Lean evaluates as , the rule becomes , and every target would count as stable. For the same reason Definition 4's is kept with its strict lower bound. The paper's standing assumptions that the revenue is unimodal and that and cross are not used by Theorem 3 or its proof and are not assumed, so the formal statements are slightly more general than the paper's.
A complete development needs basic real analysis from Mathlib (monotone convergence, continuity of , and , limits of quotients) and the equilibrium construction behind Lemma 3, which uses the inverse of the cost function . That construction is reusable across the series. Proofs of the milestones, of the reduction, and of the goal are all welcome.
Non-profit organizations such as food banks run on volunteer labour. Volunteers sign up for shifts, wait on a sign-up list, work, rest, and may or may not return; the organization can spend money on engagement activities (reminders, recognition events, recruitment drives) that raise the rate at which volunteers come back or arrive. Spending too little leaves shifts unstaffed; spending too much wastes a scarce budget. Ata, Tongarlak, Lee and Field (arXiv:2312.02920, Operations Research, 2024) model this as a multiclass queueing network, pass to a heavy-traffic limit, and obtain a one-dimensional drift-rate control problem: a reflected diffusion for the scaled workload whose drift is chosen, at a cost, from an interval of feasible drifts. The optimal policy they derive is a nested threshold policy: as the workload falls below successive thresholds , one more engagement activity is switched on.
To compute that policy one needs the thresholds, and the paper obtains them from a closed-form description of the solution of the Bellman equation between consecutive thresholds. That closed form, Proposition 3 of the paper, is the goal of this mission. A companion mission formalizes Theorem 1, the existence of a solution of the same Bellman equation.
There are engagement activities. The data are a lowest drift , drift increments , per-unit-drift costs , an idleness cost rate , a mean-reversion rate and a volatility . The breakpoints are
and the feasible drifts form the interval . The engagement cost is the convex, increasing, piecewise linear function with and slope on :
Its convex conjugate is
The Bellman equation of the drift-rate control problem asks for a constant and a continuously differentiable function on with
such that , is strictly increasing, and as . Here is the optimal long-run average cost and is the derivative of the transformed relative value function of the paper's §4 (p. 20).
Put for and . Since is strictly increasing from towards , each level is attained exactly once; the thresholds are
With the standard normal cumulative distribution function, the paper defines for
For every solution of the Bellman equation and every ,
The statement fixes nothing beyond the model: it holds for any solution, with the thresholds defined from that solution.
The result. Proposition 3 turns the nested threshold policy into something computable. Evaluating at the right end of its interval and inverting gives from , so the thresholds follow by a one-dimensional recursion once is known. The paper's simulation study of a food bank (§5) uses these thresholds to set engagement policy. The result also shows that the value-function derivative, although defined through a nonlinear equation involving a supremum, is an explicit combination of Gaussian-type functions on each threshold interval.
Formalizing it. The result is proved in the paper (Online Supplement §D); no machine-checked version of it, of the conjugate formula (E9), or of the truncated Gaussian integrals (D1)–(D2) is known to exist. A formal proof checks the transcription of a long explicit formula with many constants, which is exactly where printed closed forms tend to go wrong, and produces reusable pieces: the conjugate of a convex piecewise linear function and two interval-integral identities for the normal cdf.
The Bellman equation is nonlinear in through . The obvious approach, solving it directly, fails because has no single formula. What makes it tractable is that on the argument stays in one linearity interval of ; this is a property of the solution, derived from its monotonicity and the definition of the thresholds, not a hypothesis. A complete proof must therefore combine the piecewise description of a supremum, a uniqueness argument for a linear first-order equation on a half-open interval (with the one-sided derivative at the left end and, for , an unbounded interval), and the evaluation of Gaussian integrals over finite intervals in terms of the normal cdf, matching every constant of the printed formula. The two expressions for the arguments, in and in (D1)–(D2), are equal, but the identification must be made.
All objects live in the namespace VolunteerEngage.Thresholds, Lean 4 with Mathlib.
Model; and are -indexed sequences of which the indices are used. The standing assumptions (, , , , , , ) form the predicate Standing, a hypothesis of every model-level theorem. The paper states them in the model's derivation ((15), (24), (42), (43), (50), p. 18) rather than for the abstract control problem.Cohen2019.Robust.Phi, which is Mathlib's cdf (gaussianReal 0 1). Integrals in (D1)–(D2) are oriented interval integrals of continuous functions.The source is the arXiv preprint v2 including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the Bellman equation but are not part of any formal statement; the optimality of the threshold policy (Theorem 2) is not formalized here. Proofs of any milestone, of the goal, and general lemmas on conjugates of piecewise linear functions or on Gaussian integrals over intervals are welcome.
Banks and other financial firms lose money through operational errors: mistyped trades, missed reconciliations, compliance lapses. Regulators require the firm to hold capital against these losses, and internal audit teams spend most of their effort deciding when to inspect. Two inspection schedules are common in practice: a periodic schedule (inspect every month) and a random schedule (surprise audits). A periodic schedule leaves no error undetected for long, but an employee who knows the date can relax right after an inspection and work hard only before the next one. A random schedule removes that back-loading, but leaves some errors undetected for long stretches.
Y. Kim and Y. Xu, Operational Risk Management: Optimal Inspection Policy (SSRN 3491006; published in Management Science, DOI 10.1287/mnsc.2021.00322), model this trade-off as a principal–agent problem with moral hazard. They show that neither pure schedule dominates the other (their Proposition 4, the subject of mission I of this series), and then propose a hybrid schedule that combines them. This mission formalizes their Proposition 5: the best hybrid schedule beats the best random schedule strictly and the best periodic schedule weakly.
The source used throughout is the authors' SSRN preprint, version of July 2023. All labels (Proposition 5, Lemma 5, (EC.55), …) and page numbers are those of that version, not of the published article.
A firm (the principal) employs an agent whose errors arrive as a Poisson process with rate . Here is the agent's effort at time since the last inspection, at unit cost . Each undetected error costs the principal per unit of time until an inspection finds it. At each inspection the agent pays a penalty per error found. The principal pays a wage per unit of time and an inspection cost per inspection, earns base profit , and both parties discount at rate . The agent accepts the job only if his payoff is at least his reservation payoff . Write .
The time between two inspections is drawn independently in every cycle from a law chosen by the principal, with mean (the frequency ):
is the periodic policy and the random one.
Given a policy and a strategy , the agent chooses an effort path that maximizes his discounted payoff (1). The principal's discounted payoff is (3):
where is the agent's optimal effort and is the number of errors made by time in a cycle. The principal maximizes over subject to participation (4)–(5). Throughout, Assumption 1 holds: . The optimal payoff under policy is written .
For every inspection cost there is a payoff achievable by some hybrid policy such that
In the paper's notation, and .
Proposition 5 says that reducing the randomness of a surprise-audit schedule, in the hybrid way, strictly improves the principal's optimal payoff whatever the inspection cost. Combined with Proposition 4 it yields the paper's Corollary 1: when inspections are expensive, the optimal mix lies strictly between the two pure policies. The comparison is between optima: each policy is evaluated at its own best frequency, penalty and wage, with the agent best-responding.
The result is proved in the paper (pp. ec34–ec35); to our knowledge it has no machine-checked proof. Formalizing it requires a measure-theoretic treatment of renewal-type payoffs against three inspection laws, the agent's optimal control problem under each law, and the closed-form solution of the random policy (Proposition 1). The model layer (laws, payoffs, best response, achievable payoffs) is shared with mission I of this series.
The weak part is immediate, because the periodic policy is the hybrid policy with . The strict part is not a comparison of two closed forms: the hybrid optimum has no closed form, and the optimal mix is not computed. The random optimum itself is one of two strategies of different nature (Lemma EC.3), effort-inducing or error-correcting, and the agent's response under has a different shape from his response under (Lemma 5), so the regime boundaries of the two policies do not coincide. The naive claim that beats at every strategy is false: with zero effort, whenever (EC.55), so whether mixing helps depends on the frequency.
ProbabilityTheory.expMeasure v; the periodic law is a Dirac mass at ; the hybrid law is plus times the shifted exponential law.The goal cannot be satisfied vacuously: it asserts the existence of an achievable hybrid payoff, so an empty achievable set does not make it true.
Contributions are welcome at every level: the integral identities for the three laws (Fubini for ), the pointwise solution of the agent's problem, the two-variable optimization behind Proposition 1, and the final perturbation argument. The law lemmas and the agent's problem are reusable for any renewal-type inspection model.
Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.
Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.
There is one marketplace , one seller and a unit mass of buyers, each wanting one unit of 's product. Every buyer values the product at ; 's marginal cost is , with ; the outside option is worth .
can sell through , paying a fee per transaction, or through its direct channel, which carries no fee. It sets a price on and a direct price . A buyer who buys directly bears a switching cost ; in this mission is uniformly distributed on with , so its CDF is
The timing is: sets ; observing , sets its prices; buyers then choose. The paper's Lemma 1 lets one fix , so only chooses . A buyer buys directly iff , so a share of buyers — the leakage — buys directly. 's profit at fee is
and earns . A direct price is seller-optimal at if it maximizes over . An equilibrium outcome is a pair with , seller-optimal at , such that no other fee , followed by a seller-optimal response, gives more.
For every an equilibrium outcome exists, and every equilibrium outcome satisfies
with leakage . As increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.
Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome , and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.
The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.
The seller's problem is not a smooth concave program: the clamped distribution creates a kink at , below which every buyer switches and the profit is linear in . The first-order condition is the optimum only while ; above that the optimum sits at the kink. The marketplace's objective inherits a kink at , and its feasible set adds a corner that binds exactly when . Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.
All parameters are real numbers, with the standing assumptions and as explicit hypotheses. is the clamped uniform CDF above. The statements use the reduced seller problem (1) with , as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which also chooses , is not posed. Seller-optimality is an optimality predicate over , and the equilibrium is an optimality predicate over feasible fees (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for , which is what they require; the paper's preface "Assuming " is not needed and does not exclude .
Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of , not about the formulas alone.
The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.
Digital businesses (search engines, social networks, marketplaces) record what their users do and decide how well to protect what they record. Both choices affect users: stored data can improve the service, and it can also be accessed by adversaries such as hackers, fraudsters or data brokers, whose activity harms users. Regulation of data collection and data protection (the GDPR, the CCPA, liability rules for breaches) presupposes an answer to a basic question: in which direction does a profit-maximizing business's data strategy deviate from the one a benevolent planner would choose?
I. P. Fainmesser, A. Galeotti and R. Momot, Digital Privacy (Management Science 69(6), 2023; author manuscript SSRN 3459274), answer it in a model where users, adversaries and the business all respond to each other. Their Theorem 2 shows that the deviation is not arbitrary: one combination of errors never occurs, and the sign of the error is pinned down completely for a business whose revenue depends only on usage. This mission formalizes those two claims.
A data strategy is a pair : the share of each user's activity that the business stores, and a protection level , which costs . The parameters are real numbers: a network effect , the users' marginal benefit from stored data , the cost , the revenue model , and the planner's weight .
Given , a unit mass of identical users choose activity levels and a large population of adversaries decide whether to access the stored data. The resulting equilibrium (Proposition 1 of the paper, display (3)) has average user activity
The value at is the activity when nothing is stored, the value the paper uses where (3) reads . From one builds the consumer surplus (4), the business's profit (2) and the planner's objective (7):
The revenue model interpolates between a purely usage-driven business (, revenue proportional to activity) and a purely data-driven one (, revenue proportional to stored data ). A business optimum maximizes over the feasible set ; a social optimum maximizes over the same set. The business under-collects if and over-protects if , and so on.
The paper's Theorem 2 (p. 13) reads:
Relative to the socially optimal strategy, the equilibrium data strategy of a purely usage-driven business (P = 0) prescribes under-collection and under-protection of users' data, i.e., ξ* ≤ ξ^W and C* ≤ C^W. The equilibrium data strategy of a business with any data-driven component in its revenue model (P > 0) never prescribes under-collection and over-protection of users' data i.e., it is never the case that ξ* ≤ ξ^W and C* ≥ C^W with at least one of the inequalities being strict. Any other direction in which the optimal business's data strategy deviates from the socially optimal strategy is the outcome for some specification of the business's revenue model and values of other model parameters.
The goal is its first two sentences, for every business optimum and every social optimum:
The third sentence is established numerically in the paper (Figure 3) and is not a target.
The result. Theorem 2 identifies the one inefficiency that no revenue model produces: a business never stores too little data while protecting it too much. All other combinations occur for some parameters, so a regulator cannot infer the direction of a business's error without knowing its revenue model; but for a purely usage-driven business the direction is known, and it is too little protection. This underlies the paper's discussion of policy in §6, where the instruments considered (liability for data breaches, taxes on data) are compared by how they move towards .
The formalization. The result is proved in the paper (App. A.4, with Proposition 5 in Online App. C.5); it has not been machine-checked. The paper's argument for the purely usage-driven case refers to first-order conditions and does not treat the boundary strategies (, ) or parameter corners () separately; a formal proof has to handle them. A complete development also yields reusable facts about the equilibrium activity : its sign, its behaviour in for fixed , and the monotonicity in of the activity-maximizing collection level.
Both optima are defined only implicitly, as maximizers over a non-compact feasible set of a non-concave objective, and neither has a closed form that this mission may use. The comparison must therefore work from the optimality inequalities alone. The tempting approach, comparing first-order conditions, does not give a global statement: and may have several local maxima, the maximizers need not be unique (both optima are in a whole region of parameters), and the constraint binds for large protection. In the purely usage-driven case the profit and welfare share their maximizers in for each fixed , but turning that into a comparison of with requires control of how the maximizing moves with , including at .
All objects are real-valued functions of explicit real parameters and of the strategy , in the namespace DigitalPrivacy.Welfare, which imports , CS, the feasible set and the business optimum from the shared module DigitalPrivacy.Strategy.Setting. The equilibrium activity takes the value at for every , as in the paper; Lean's default is not used. Optima are predicates (IsBusinessOpt, IsSocialOpt): a feasible point at which the objective is at least its value at every feasible point. Theorem 2 quantifies over every pair of optima and asserts neither existence nor uniqueness. The P > 0 clause keeps the "at least one strict" condition; without it the clause is false, because both optima coincide at in part of the parameter space.
The standing assumptions are the paper's ranges , , , , with two disclosed strengthenings: (with , , , every is both a business and a social optimum and the sentence fails) and (with the planner's problem is the business's, and step (11) does not hold). Proposition 5(i) is stated with the printed ranges, included. No other hypothesis is added, so the hypotheses on the optima cannot be made vacuous by the encoding; a sanity check exhibits parameters at which is both a business and a social optimum.
A complete development needs elementary real analysis of the rational function on and nothing beyond Mathlib. Proofs of the milestones, of lemmas about , and alternative arguments for the goal are all welcome. The paper's proofs are in App. A.4 (pp. 33–35) and Online App. C.5 (Online pp. 8–9).
Two classical online selection problems sit at opposite ends of an information spectrum. In the secretary problem items arrive in uniformly random order, only their relative ranks are observed, and the best possible probability of stopping on the best item tends to . In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant of Hill and Kertz (1982), shown tight by Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017).
Correa, Cristi, Epstein and Soto (arXiv:2011.06516) interpolate between the two with the -sample-driven optimal stopping problem. Each of items is sampled independently with probability ; the decision maker observes the relative rankings of the sampled items, then faces the remaining items online, observing relative rankings, and makes irrevocable stop/continue decisions. Stopping on the item of overall rank earns a reward , with . At and this is the secretary problem; for adversarial the optimal guarantee tends to as , the i.i.d. prophet constant.
For known , the paper writes a linear program over the stopping probabilities of rank-based algorithms (after Buchbinder, Jain and Singh, 2014) and takes its limit as . The analysis rests on one structural result, Theorem 2: this limiting program can be restricted, without loss, to solutions of an explicit threshold form, so that the optimal algorithm stops on an item of current rank after a time . This mission is that theorem.
Fix . Time runs over (time is the fraction of the items seen so far; the sample accounts for the first fraction in the limit), and ranks refer to the relative rank of the current item among all items seen so far. A candidate solution is a function , the density of stopping at time on an item of relative rank .
The cumulative mass of is . A solution is feasible for the continuous linear program CLP when , each is integrable on , and
For the negative-binomial term is , the probability that a NegativeBinomial variable is at most , and
is the limit of the probability that the algorithm stops on an item of overall rank at most . The objective of CLP is for a non-increasing sequence , so any solution that increases every is at least as good.
A threshold sequence is a non-decreasing with ; put .
For every feasible there are a feasible and a threshold sequence with for all , such that for every and
Theorem 2 turns an infinite-dimensional linear program over functions of two variables into the reduced problem RP, an optimization over a single non-decreasing sequence of thresholds. Every quantitative result of the paper is read off RP: the optimal ratio for each , its limit as (Theorem 8, mission II of this series) and the explicit lower bound (Theorem 9, mission III). It also identifies the optimal rank-based algorithms as threshold rules: accept the current item if it is among the best seen so far, where grows at the times .
The result is proved in the paper. It has not been formalized, and neither has any part of the continuous-LP approach to secretary and prophet problems. The formal development produces a reusable layer: continuous stopping LPs with extended-real cumulative constraints, monotonicity of negative-binomial distribution functions in both parameters, and a rearrangement argument for integrals against monotone weights.
The obvious argument is to improve greedily: push each component's mass as far right as the constraint allows. One step is easy, but the step changes the constraint itself, since the envelope depends on all components. The proof iterates, needs the thresholds to be monotone in , and must pass to a limit in with a dominating function that exists only because the smallest threshold is bounded away from . The limit thresholds need not be monotone in , and the components must then be reordered using Lemma 18. Finally, (5)–(6) are an integral equation in which each component depends on the sum of all others; identifying their unique solution with (7) needs both a uniqueness argument for a linear ODE and a telescoping computation.
q : ℝ → ℕ → ℝ, a representative of an element of . Ranks, , , are 1-based; is never used. Constraints are imposed pointwise for all , as printed.Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.
P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.
This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.
The principal faces a Poisson stream of arrivals, each worth revenue . Without effort the arrival rate is ; an agent who exerts effort, at cost per unit time, raises it to . Write . The principal's total cost rate while the agent works is , every start of work costs a switching cost , and the principal and agent discount at rates . Assumption 1 is .
The paper's derived constants are
together with the revenue thresholds (28) and (34) and the switching-cost threshold (33). Condition 2 is and : the agent is much more impatient than the principal and revenue is high.
The state variable is the agent's promised utility . Two operators act on functions of , where is the left derivative:
The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair satisfies the optimality condition (20)–(22) when , , and .
The suspended-state equation with is solved by (24). In the region of this mission the paper builds
from parameters chosen so that pastes smoothly onto the line at and ends at at .
Under Condition 2 and , for every triple with , , and
the functions above satisfy (20)–(22).
Lemma 5 guarantees that the goal is not vacuous.
Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent per arrival and never suspends. The threshold separates this region from the control-band region of Proposition 7, so the explicit formula for is the boundary of the phase diagram.
The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near , where has infinite slope, and it checks the threshold , whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), , is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).
The cases and are algebraic. The difficulty is : there is the curve , and lands beyond (Condition 2 gives ), so couples the curve with the constant . Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on in (35), which is exactly where the threshold enters. A direct sign check at alone does not cover the interval. The existence lemma requires monotonicity of , whose expression mixes powers with a linear factor.
All functions are ℝ → ℝ and every quantifier ranges over ; powers are Real.rpow. The standing assumptions , , , , are one hypothesis Standing; and are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for only: at the right derivative of is , so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.
The threshold of (33) is corrected: the printed bracket contains , but the paper's own proof identifies with of (EC.69), which gives . With the printed term Lemma 5 fails (for , the printed value is , the corrected one ). Equation (36) is printed with a free that should read . The range , given by the proof, is stated.
The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound in (21), the condition (22), or the lower bound on would trivialize or change the statement.
The development needs the derivative of , sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.
One-way vehicle-sharing systems (car sharing, bike sharing, ride-hailing fleets) set a price for every origin–destination trip. Prices decide which trips are taken, and so they decide where vehicles end up. Pricing that depends on the current position of every vehicle is in principle optimal, but its state space grows combinatorially with the fleet. Practitioners therefore use static prices, which depend only on the origin and destination. The question is how much revenue, throughput or welfare such prices give up.
Benjaafar and Shen (SSRN 3998297; Technical Note, Operations Research, 2023, doi:10.1287/opre.2023.2446) answer this with explicit lower bounds on the performance ratio of the static policy obtained from a fluid relaxation. Banerjee, Freund and Lykouris (arXiv:1611.07624) proved the earlier guarantee, which requires the fleet size to be at least and the workload to be at most . Benjaafar and Shen give two bounds that hold for every . The first is (their Theorems 1–2), and it degrades when total demand grows with . The second, Theorem 3, does not depend on demand or travel times at all. This mission is about Theorem 3.
There is a finite set of locations and vehicles. Trip requests from to arrive as a Poisson process of rate , and is the set of pairs with demand. The graph is strongly connected. A trip from to lasts a random time with mean . A static policy is a matrix of quantiles: is the fraction of customers who accept the posted price. Each accepted trip earns a reward , and is concave. A customer who finds no vehicle at the origin is lost.
Problem (2) is the fluid relaxation, in which vehicles are always available:
The first constraint balances the flows, and the second caps the workload (the mean number of vehicles in transit) by a budget . Let be an optimal solution that induces a strongly connected network.
Under a static policy the vehicles move in a closed queueing network. Each location has a single-server pick-up queue with service rate . Each pair has an infinite-server transit queue with mean service time . This network is of BCMP type, so its stationary law has product form. With a positive solution of the traffic equations (9), a state with vehicles at location and in transit from to has weight . The availability is the stationary probability that location holds at least one vehicle. The reward rate of the policy is Equation (3):
For , , optimal for (2), inducing a strongly connected network, with :
The paper states the bound for , where is the optimal dynamic policy. It passes from one ratio to the other with Proposition 1, (p. 6), whose proof needs the stationary analysis of arbitrary state-dependent policies. Proposition 1 is not part of this mission. The goal implies the paper's Theorem 3 once Proposition 1 is available.
The bound tends to at rate , uniformly in demand rates, travel times and the reward functions. It is the regime-free counterpart of the bound: that bound is better for light demand, this one for heavy demand (Remark 7). Remark 6 reports that it is also numerically tighter than the guarantee of Banerjee et al., and unlike that guarantee it applies to every fleet size.
Formalizing it adds several things to the platform. The first is availability in closed networks of single-server and infinite-server stations, defined from the product form. Two classical facts about this model follow: availability is equal across locations under balanced flows, and it satisfies the mean-value recursion (5). Milestone 4 is a concavity statement about the throughput of a closed network in its population, and for it contains the concavity of the Erlang-B carried load in the number of servers. The paper does not prove it; it cites George and Xia (2011) and Shanthikumar and Yao (1988). None of these results is formalized anywhere that this mission is aware of, so the mission formalizes a proved result, not an open problem.
The algebra at the end (milestones 6–7 and the substitution ) is elementary. Two steps are not.
Equation (5) is stated as a relation between availabilities, but its content is an identity between normalizing constants of the product form. The paper derives it from the arrival theorem and Little's law, and neither is available. A direct proof has to compute under balanced flows, which takes a counting argument over the state space. Equal availability likewise needs the positive solution of (9) to be unique up to scale on a strongly connected network.
Concavity of is the hard milestone. A natural first attempt is induction on the recursion: if is non-increasing up to , show that the next increment is no larger. The map is increasing and convex in its argument, and convexity points the wrong way, so increments do not propagate directly. The published proofs go through the closed-network interpretation, not through the recursion.
The Lean development lives in VehicleSharePricing.DemandFree. Locations are a Fintype with Nonempty, and is its cardinality. Λ, μ, q are real matrices on all pairs, and entries outside enter only multiplied by . Strong connectivity is the transitive closure of the positive-flow relation (Relation.TransGen). This guarantees at every location, even for . Availability is the product-form busy probability of the general definition ProductFormNetwork, applied to the induced network. That law is a definition that records the paper's appeal to BCMP (p. 6), not a theorem of this mission. Theorems quantify over every positive solution of (9). is Equation (3) with per-location availabilities. The sequence is defined by its recursion, which is correct because it is a proof device, not the availability of . All arithmetic is in , and appears only under .
Two trivializations are ruled out. Defining by the recursion (5) would make milestones 1–3 empty, and defining as would make milestone 1 empty. The hypothesis is added because the ratio is otherwise .
The proof of the goal uses only feasibility of and the strong connectivity of the induced network; optimality is kept because it is the paper's hypothesis. Contributions are welcome on any milestone. A library for normalizing constants of closed product-form networks, and the concavity of throughput in the population, would be reusable well beyond this paper.
One-way vehicle-sharing systems (car sharing, bike sharing, on-demand fleets) move a fixed fleet of vehicles among locations. Customers take a vehicle at one location and leave it at another, so prices shape both revenue and where the fleet ends up. The optimal dynamic pricing policy, which reacts to the current position of every vehicle, solves a dynamic program whose state space grows combinatorially in and . Static policies, with one fixed price per origin–destination pair, are simple to compute and to operate, and the question is how much they lose.
Benjaafar and Shen (SSRN 3998297; Operations Research, 2023, doi:10.1287/opre.2023.2446) take the static policy that solves a fluid relaxation, Problem (2), and bound its performance ratio. When induces a strongly connected network, Theorem 1 gives the ratio . Waserhole and Jost (2016) observed that the best static policy may deliberately disconnect the network: prices that make some trips unattractive can leave two or more separate networks. The fleet then has to be split among the pieces, and Theorem 1 no longer applies. This mission formalizes Theorem 4 of the paper (§6, p. 18), which shows that the same guarantee holds in that case, provided the vehicles are allocated optimally among the networks.
There are locations and vehicles. Trip requests from location to arrive at rate , and is strongly connected. A trip on lasts on average . A static policy is a vector of quantiles (the fraction of customers who accept the price), and earns per trip, with concave.
Problem (2) maximises the fluid reward over balanced flows ( at every location) with workload , where . Let be an optimal solution.
The policy splits the locations into networks with location sets () and pair sets : accepted demand only joins locations of the same network, and within each network it is strongly connected. With vehicles, network is a closed queueing network: a single-server pick-up queue at each location (rate ) and an infinite-server transit queue on each pair. Its stationary law is the BCMP product form, with loads computed from a positive solution of the traffic equations (9). The availability is the stationary probability that a location of network has a vehicle.
An allocation with earns (Equation (3)), and Problem (8) chooses to maximise it. Write , for network 's share of , and .
The paper's Theorem 4 opens with , where is the reward of the optimal dynamic policy. That inequality is Proposition 1 (, p. 6). It needs the stationary distribution of the network under an arbitrary state-dependent policy, a controlled-Markov-chain development that is not part of this mission. The goal is the rest of the chain, and it implies the paper's theorem once Proposition 1 is available.
The result. Theorem 4 removes the connectivity assumption from Theorem 1. A static policy chosen by the fluid relaxation may disconnect the network, and it then still earns at least of the fluid optimum, uniformly in the demand and reward data. The bound tends to as for fixed and . Milestones 6–7 hold for arbitrary weights, location counts and workloads, so they apply to any separable allocation problem whose pieces satisfy recursion (5).
Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked so far. The mission adds closed-network availability on a disconnected network, the mixture decomposition of the performance ratio, a real-argument Vandermonde identity in the paper's own notation, and a discrete allocation inequality proved by an averaging argument. The companion missions of this series formalize Theorems 1–3 of the same paper.
The obvious argument applies Theorem 1 to each network: . This leaves a maximisation over allocations, and no single allocation obviously beats . Proportional splitting fails because does not scale with , and the best allocation depends on all of , and . The paper does not exhibit a good allocation. It averages the objective against probability weights from the Chu–Vandermonde identity, which needs binomial coefficients with real upper arguments. It then passes from two networks to many by an induction that merges networks. The recursion (5) itself rests on a computation with the normalising constants of a product form that has both single-server and infinite-server stations.
Locations form a finite type. is the set of pairs with , and its strong connectivity is a transitive closure. The split is a surjective map from locations onto a finite index type of networks. Every pair with positive accepted demand stays inside one class, and each class is strongly connected under accepted demand, again as a transitive closure. So every location has positive accepted demand. The paper's is relaxed to .
Availability is the BCMP product form of each network on its own, with loads (pick-up) and (transit), and a positive solution of (9). This is a disclosed definition, since the paper invokes the BCMP class without writing it. Availability is defined per location; its equality across a network follows from milestone 1. is Equation (3) with per-location availabilities. Problem (8) is an explicit maximisation over the finite set of allocations. All ratios are real numbers, is assumed so that the ratio is defined, and is computed in .
Defining availability by the recursion (5), or as , would make milestones 1–2 trivial and is ruled out.
A complete development needs:
Ring.add_choose_eq);The closed-network definitions and milestones 5–7 are reusable beyond this mission. Proofs of any milestone are welcome, and so is a proof of Proposition 1.
Online marketplaces depend on consumer reviews, and a single negative review can move a seller's future sales. Review blackmail exploits this: a consumer buys a product, posts a negative review, and offers to remove it in exchange for a payment. Platforms such as Amazon, eBay, Taobao and TripAdvisor respond with dispute resolution mechanisms that let sellers contest reviews. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) build a game-theoretic model of the seller, the blackmailer and the market's belief about product quality, and ask how the design of such a mechanism changes the blackmailer's leverage. Their first finding concerns a centralized mechanism, where the seller reports the review and the platform judges it: making the platform faster or more accurate does not always lower the ransom the blackmailer can extract. This mission formalizes that result together with the equilibrium analysis it rests on.
A monopolist sells a product of unobservable quality ; the market's prior that quality is high is . A buyer of a high-quality product has gross utility with probability and otherwise, with standard uniform; a low-quality product always gives . One consumer arrives.
The market sees the review , updates its belief to a posterior by Bayes' rule, and the seller then earns a continuation payoff , with nonnegative, convex and strictly increasing on .
Facing a ransom demand the seller can settle (: pay , the review disappears), do nothing (: the review stays), or report () the review to the platform's centralized mechanism at a hassle cost . The platform investigates immediately with probability (timeliness) and identifies a malicious review correctly with probability (accuracy); the review is removed with probability , the mechanism efficiency.
The market cannot observe the seller's interaction with the blackmailer. It holds a belief about the seller's response, and this belief determines the posteriors: under belief a malicious review stays visible with probability , or , and is the Bayes posterior computed from the resulting review likelihoods. When the market believes and the seller plays , his payoff is (), (), or (). A response is an equilibrium if it is a best response to the belief ; among several equilibria, the seller-preferred one prevails. The malicious consumer buys iff some ransom is accepted in the prevailing equilibrium, and the equilibrium ransom is the greatest ransom at which settling prevails.
If and , there are efficiencies at both of which the malicious consumer purchases, with
The equilibrium ransom is not monotonically decreasing in the efficiency .
and the malicious consumer purchases iff .
Corollary 1 is the paper's headline message about centralized dispute resolution: improving the mechanism's timeliness or accuracy can raise the ransom. Below an efficiency threshold the mechanism is never used and the ransom equals the seller's loss from a visible negative review; just above it, the market expects the seller to report blackmail, which softens how it reads a negative review, and the blackmailer can ask for more. This is the motivation for the paper's second design, semi-decentralized dispute resolution, analysed in a companion mission. Proposition 2 is the complete characterization of the blackmailer's equilibrium behaviour under the centralized mechanism and is used again in the paper's pricing analysis (§4.4).
The results are proved in the paper (Appendix C). No machine-checked version exists. This mission produces Lean statements of the model, of the Bayes posteriors, of the equilibrium conditions, of the seller-preferred selection and of the ransom characterization, all derived from the primitive game rather than from the paper's closed forms.
Each step is elementary, but the chain is long and sign-sensitive. The equilibrium conditions require handling a belief-dependent payoff (the posterior depends on what the market believes, not on what the seller does), so a deviation changes the action without changing the posteriors. The ransom characterization needs a three-way comparison of equilibria and the tie-breaking in favour of settling at the boundary, where two equilibria give the same payoff. The corollary needs the jump at the threshold efficiency to be strictly positive and to survive a small increase of the efficiency: the posterior moves with the efficiency, so a continuity argument for composed with the posterior is required, and is only assumed convex and strictly increasing on . The natural first idea, comparing the two closed forms of Proposition 2 at a single point, does not suffice, since at the threshold itself the two regimes coincide in value.
Model with fields and ; inductive types for quality, reviews (, Z for , ) and responses. The posterior post m R is Bayes' rule over the likelihood table with visibility probability of a malicious review; is post (keep (γ*δ) i) R.Standing): ; , convex and strictly increasing on ; ; and . The last is implicit in the paper: it makes the purchase probability that of a standard uniform valuation and keeps the event of positive probability. Every theorem also assumes .IsGreatest of the set of ransoms at which settling prevails; purchase means some such ransom exceeds . "Not monotonically decreasing" means not nonincreasing.ConvexOn, StrictMonoOn, IsGreatest). Proofs of the milestones in order, and reusable lemmas on the monotonicity of the posterior in the visibility probability, are welcome.Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty .
This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.
A product has quality . The prior that is . A buyer of a high-quality product gets a positive experience with probability ; a low-quality product never gives one. With probability the consumer is malicious. A malicious consumer buys at price , posts a negative review and demands a ransom . Otherwise the consumer is regular. A regular consumer buys with probability (valuation uniform on ) and reviews truthfully: positive () or negative (). No purchase means no review, written ; a removed review is also seen as .
The market observes and forms the posterior by Bayes' rule. The seller then earns , where is nonnegative, convex and strictly increasing on .
Facing a ransom demand, the seller can settle (: pay , review removed), do nothing (), or use the mechanism (). Under the platform judges immediately with probability (timeliness). It recognises a malicious review with probability (accuracy). The review is therefore reinstated with probability , and the penalty is paid with probability . Write for the posterior after review when the market believes the seller's response is . The payoffs of the three responses are then
The market cannot see the interaction, so is an equilibrium at if no response pays more given the belief . The equilibrium ransom is the largest at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff .
A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when .
Let and .
Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold rises with the accuracy and falls with the timeliness . The paper's later results on pricing and on the platform's penalty build on this characterization.
The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor .
Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on . So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering , which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for alone as the answer gives the wrong ransom in case 1.
Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding and the payoff fut (the paper's ; Real.pi is never used). The predicate Standing collects the standing assumptions: ; nonnegative, convex and strictly increasing on ; ; ; and the disclosed addition , which makes the purchase probability lie in . Per-statement additions, each disclosed in the item:
Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: for malicious and for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews (), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.
The posteriors are never defined by their closed forms, and is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.
A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.
Young innovative firms often fund research out of internal cash flow rather than external capital. Whether such financial constraints make firms invest less in research and development (R&D) is a long-standing question in corporate finance and the economics of innovation. Myers (1977) showed that the possibility of default leads to under-investment in growth options. Danmo Lin (Management Science, 2022) separates two ways in which spending more on a project can pay off: it can make the payoff larger (scalability) or make the discovery arrive sooner (accelerability). The paper's Corollary 1 says that the classical under-investment result holds exactly when the project is scalable but not accelerable, while acceleration can reverse it. This mission formalizes the under-investment half of that corollary.
A firm faces a one-time R&D opportunity. It chooses an investment intensity , a spending rate per unit of time, and pays it until discovery. Discovery is the first arrival of a Poisson process of rate , and on discovery the firm receives a payoff with mean . As in the paper's equation (2),
and intensities are at least . The project is scalable if (here ) and accelerable if (here ). Future cash is discounted at rate .
An unconstrained (UC) firm can always pay . By the paper's Lemma 1, equation (5), its project value at intensity is the perpetuity
A financially constrained (FC) firm pays out of an asset-in-place (AIP) cash flow , a geometric Brownian motion with drift and volatility that starts at . It must abandon the project once . Lemma 1, equation (6), gives its project value as
The ranges of intensities are those of (7): for the UC firm and for the FC firm, with . The optimal intensities and are the sets of maximizers of and over these ranges.
If and , then . Formally: under the standing assumptions, , , , , and , both optimal sets are nonempty and
The statement pins down when the textbook under-investment effect of financing frictions holds: exactly when extra spending scales the prize but cannot speed it up. The paper contrasts it with the possibility of over-investment on accelerable projects (Corollary 1's second statement, supported by numerical exercises). Taken together, the two statements show that the R&D technology, not only the severity of the constraint, decides the direction of the distortion.
The result is proved in the paper (Appendix A.4); it has no machine-checked proof. A formal proof certifies the comparison for every pair of optima, without the paper's tacit assumption that optima are unique. It also makes explicit the interior-optimum condition under which the inequality is strict. The resulting facts about maximizers of products of a concave power-law profit and a decreasing survival factor are reusable for other real-options models with a survival discount.
The first idea is to compare the two first-order conditions. The UC optimum solves , and at an interior FC optimum the derivative of the survival factor pushes to be positive. Concavity of then orders the two. Turning this into a theorem about sets of maximizers needs more. The FC optimum can sit at a corner, either or the right end , where no first-order condition holds, and the corners must be ruled out or handled separately. The survival factor vanishes at . The UC value vanishes at . When , the comparison is settled by the range rather than by the first-order condition. The strict inequality is false without an interior UC optimum: if , both optimal sets equal .
All objects are in the namespace AccelScal.FCMonopoly, in one definition file. It holds the parameter structure Tech , the predicate Standing, , , , , (5), (6), and the maximizer sets RstarUC, RstarFC over the ranges (7). Powers are Real.rpow, and is Mathlib's deriv.
Committed conventions:
Trivializing formalizations are ruled out. is never defined by its closed form, and neither optimum is a selected value. The goal asserts that both optimal sets are nonempty. The FC range depends on through . The conclusion is the strict "", not "".
The paper's second and third statements of Corollary 1 (over-investment when , and when it is "more likely") are numerical or informal and are not posed. Contributions are welcome on both milestones and on the goal. Also welcome: general lemmas on the maximizers of a positive concave function times a decreasing positive factor, and a future formalization of Lemma 1 (6) from a geometric Brownian first-passage Laplace transform.
Firms that serve several customers from shared capacity must decide which demands to fulfil after demand is observed. A customer-level service commitment constrains the allocation policy even when total capacity appears adequate: serving one customer can consume resources that another customer needs. The question in this mission is how to test a fixed capacity vector against all individual service targets without first specifying a particular rationing rule. Jiang, Wang, and Zhang give a characterization for a broad family of pooled-resource models, including inventory pooling, process flexibility, and assemble-to-order systems (SSRN preprint, §§1.1–2).
The authors' model allows service to mean more than the probability of completely filling an order. It can represent the probability of full service, a fulfilled fraction relative to expected demand, or a fulfilled fraction of realized demand. Their Theorem 1 addresses asymptotic feasibility: every target can be met to within any prescribed positive tolerance. It is distinct from exact feasibility, which the paper treats later under stronger conditions (Jiang, Wang, and Zhang, Theorems 1–2).
There are customers and resource types. A nonnegative capacity vector is fixed before a random, nonnegative demand vector is observed. The joint law of is and has a bounded second moment. After seeing , a decision consists of a vector of fulfilled customer demands and an allocation array recording the amount of each resource assigned to each customer. The paper's set specifies all feasible pairs for that capacity and demand. It is a model input: the three operational examples use different feasible sets (§1.1, equations (1)–(4)).
For customer , a service measure assigns a nonnegative score to fulfilled demand and demand . The customer has a target . A deterministic policy chooses a feasible pair in for each . A randomized policy chooses among deterministic policies. Its expected service to customer is denoted . The capacity is asymptotically feasible when, for every , some randomized policy satisfies for every customer (Definition 1, equation (8)).
For nonnegative customer weights , define maximum weighted service at a realized demand by
The maximum uses only service, with zero allocation cost. The paper also introduces a linear allocation cost , a deterministic Max-Weighted-Service minimization problem, and its expected dual functional; Lemma 1 concerns those general objects (§2, equations (14), (16)–(17)).
Under Assumption 1, the target is the equivalence
The weights range over the whole nonnegative orthant; they are not restricted to a simplex in the theorem. Assumption 1 requires each to be nondecreasing and upper semicontinuous in fulfilled demand at fixed realized demand, and each to be compact (Theorem 1, equation (18)).
Lemma 1 identifies the value of the pointwise Max-Weighted-Service rule: for a fixed . The proof of Theorem 1 then uses a minimax display over to obtain, for every , a randomized policy whose weighted service shortfall is at most throughout (equation (21)). Equation (22) gives the corresponding individual service bounds. These three source claims are the mission's milestones (Lemma 1 and proof of Theorem 1, pp. 12–14).
Theorem 1 supplies a test for a vector of simultaneous service targets using a family of deterministic, weighted allocation problems. It applies to any feasible-set model satisfying the stated assumptions, rather than only to one pooling network. It also delineates the strength of the conclusion: satisfying all weighted tests guarantees arbitrarily close service, while exact attainment requires the additional assumptions in the paper's next result (Theorems 1–2).
The statements in this mission compile as Lean declarations, but their proofs have not yet been machine checked. Completing the mission would provide a reusable formal interface for demand-dependent feasible sets, measurable rationing policies, finite policy randomization, service expectations, and pointwise weighted optimization. Those definitions can also support formal study of the paper's later exact-feasibility and policy-optimality results.
The forward implication compares service under one policy with a maximum over feasible decisions at every demand. The reverse implication is harder: a weighted inequality for each must yield one policy that serves all customers simultaneously to a common tolerance. A separate policy chosen for each weight does not itself meet the vector of targets. The optimization involves a set of demand-dependent policies, and the source's argument relies on properties of its attainable service vectors that need explicit representation in Lean (proof of Theorem 1, pp. 13–14).
Customers and resources are Fin n and Fin m, with zero-based indices; the paper numbers them from one. A solution is a pair , and remains an arbitrary feasible set. Deterministic policies are measurable functions of that select from for every demand realization, at the theorem's fixed capacity. Randomized policies are finite probability mixtures of these selectors. Only finitely many expected services and costs occur in the statements, and finite mixtures represent the corresponding finite-dimensional expectation vectors of the paper's policy measures. The definition of asymptotic feasibility is made directly from these policies and their service values. The maximum in the theorem is made directly from and , so the equivalence cannot follow from defining either side in terms of the other.
The paper defines on nonnegative pairs. Lean uses a total real-valued extension; the theorem requires it to be nonnegative, monotone and upper semicontinuous as specified, and jointly measurable. A common integrable envelope bounds every feasible service value, preventing a nonintegrable Bochner integral from silently taking Lean's default value of zero. A measurable maximizing selector is assumed for every nonnegative ; it ensures that the expectation of and the policy behind the source's tie-breaking are meaningful. The demand law is a probability measure with bounded second moment and nonnegative demand, capacity is nonnegative, and , matching the section's standing setup. Compactness alone permits an empty feasible set in Lean; the selector assumption ensures nonemptiness at each demand.
The definitions include the linear allocation-cost functional because Lemma 1 is stated with the paper's general . An integrable envelope also bounds its absolute value in that milestone. Reusable work includes measurable selection for a demand-dependent compact feasible set, integrability of finite policy mixtures, interchange of the pointwise optimum and expectation under the stated bounds, and the finite-dimensional minimax statement. Proofs or improvements to these interfaces are welcome as long as the source claims retain their stated strength.
In the classical secretary problem, candidates arrive one at a time in random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones, and must irrevocably hire or pass. The goal is to hire the best candidate, and the optimal rule (wait for about arrivals, then take the first candidate better than all before) succeeds with probability about .
In many applications the decision maker also receives advice about each candidate: a noisy score, a prediction from a machine-learned classifier, or samples from the same distribution. Dütting, Lattanzi, Paes Leme and Vassilvitskii (arXiv:2011.06726, Mathematics of Operations Research, 2024) propose a single model covering these cases: each secretary carries a signal, ranks and signals have an arbitrary known joint distribution, and the question is which policies are optimal. Their first structural result says that, under two natural conditions on the distribution, the optimal policy can ignore almost all of the history: it needs only the current signal and whether the current secretary is the best so far. Such memoryless policies are simpler, store less, and are relevant where data retention is restricted.
Timeline. Dynkin (1963) gave the rule for the advice-free problem. Gilbert and Mosteller (1966) studied the full-information version, where the advice is the candidate's value drawn from a known distribution. Buchbinder, Jain and Singh (2014) wrote secretary problems as linear programs. Dütting et al. (arXiv 2020) extended this LP to general advice and proved Theorem 8, the result of this mission.
There are secretaries, arriving in the order , and a finite signal space . An outcome consists of ranks (ties allowed) and signals . A signaling structure is a known probability distribution over outcomes such that, almost surely, some secretary has the top rank .
At round the algorithm sees the information : the relative order of the first arrivals and their signals, not the ranks themselves. A policy assigns to every round and every information value a stopping probability in . The policy stops at with probability , and its winning probability is the probability that it stops at some with .
The best-so-far event is . A policy is memoryless if its stopping probability at round depends only on , on whether holds, and on .
Two properties of are assumed. Non-Filtering (NF): for , the conditional law of given is unchanged by additionally conditioning on . History-Irrelevance (HI): conditioned on , the information at round is independent of the event .
For , and let and . The LP of §3 has variables , constraint
and objective (5).
If satisfies NF and HI, then there is a memoryless policy with
Theorem 8 reduces the search for an optimal policy from functions of the entire history, whose number grows exponentially in , to numbers, and with Propositions 9 and 10 it turns the problem into a linear program of polynomial size. The later sections of the paper build on it: threshold policies (§4), secretaries with samples (§5) and binary-classifier advice (§6) are all analysed through this LP. The examples satisfying NF and HI include the classical problem, the full-information problem, samples, and noisy classifier advice.
The paper gives a complete proof. As far as is known, none of it has been machine-checked, and Prove2Me has no formal model of secretary problems with advice. A formal development makes precise the parts the paper's argument leaves informal: the handling of conditioning on null events, of randomized policies, and of the existence of an optimum.
The obvious argument replaces a general policy by its conditional stopping probability given . This fails directly: the probability of reaching round depends on the whole history, so averaging the decision at round changes the distribution of the earlier stopping events, and the winning probability with it. The paper therefore goes through the LP. The variables summarize a policy, NF is what makes constraint (4) depend only on the distribution and not on the policy, and HI is what makes the objective linear in . The reverse direction, Proposition 10, rebuilds a policy from through an induction over rounds in which the survival probability must be tracked exactly.
Fin n, 0-based: Lean secretary is the paper's , and Lean rank is the paper's top rank . The signal space is a finite type, so every probability is a finite sum. Continuous signals (the paper's Example 2, ) and the non-NF Example 11 are out of scope. Ties are allowed, as in §2.Memoryless predicate that allowed dependence on the whole information, or a winning probability without the survival product, would make the goal empty. Neither is used here: a memoryless policy is a function of only, and the winning probability includes .prob, expectOn, cross-multiplied conditioning) and the identity are reusable well beyond this mission. Proving the milestones in the order listed follows the paper's proof. The running time of the LP and the paper's plots are out of scope.Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.
Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.
Let be a finite set of states and the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior . The receiver chooses an action from a finite nonempty set . Her utility is an arbitrary function ; the sender's utility is .
For each action , the beliefs at which is optimal for the receiver form the set
The paper assumes throughout (Assumption 1) that every is closed.
A signaling scheme consists of a measurable signal space and a probability measure on whose -marginal is . After signal the receiver holds the posterior given by Bayes' rule, and plays an optimal strategy , with , that is . The sender's persuasion problem (3) is to maximize over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.
A probability measure on is Bayes-plausible if its mean is the prior: .
The sender's problem (3) can be optimized by solving the convex program
It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.
Let be the states at which is sender-optimal, assume these sets partition , and set . Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if is feasible for (7), i.e. for all .
The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has vector variables in , each in a convex set that depends only on the receiver's utility. Its variable is the joint probability of state and action . The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each is convex, and (7) reduces to the familiar obedience-constrained linear program.
Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).
The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in can produce a belief outside , since need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex to a finite-dimensional variable in . The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.
Fintypes, nonempty, and carries a measurable space in which singletons are measurable. Beliefs are functions in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, is convexHull ℝ, and is the zero function. is a function on , used only on the simplex.Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on , and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.Ride-hailing platforms such as Uber and Lyft match riders with self-scheduling drivers who decide for themselves whether to work. Two features make capacity planning on such a platform different from classical fleet management. Demand is spatially imbalanced: more trips start in some locations than end there, so cars accumulate where they are not needed unless they drive back empty. And capacity is endogenous: the number of participating drivers depends on what drivers expect to earn, which in turn depends on how the platform uses them.
Afèche, Liu and Maglaras (MSOM 2023) study how much a platform gains from two operational controls under these conditions: admission control (rejecting some ride requests, depending on destination) and centralized repositioning (directing idle drivers to move empty between locations). The benchmark of their comparison is the regime in which the platform has both controls, called centralized control (regime ). This mission formalizes the paper's characterization of that benchmark: how a fixed number of drivers should be allocated, what each driver then earns, and why the resulting driver equilibrium is the platform's optimum.
There are two locations and four routes , . Route has potential demand rate and travel time . The price is per unit of travel time; the platform keeps a share and drivers keep , with , while paying a driving cost rate , with . Demand is imbalanced: (Assumption 1). Repositioning is profitable: and (Assumption 2).
A pool of potential drivers has opportunity cost rates drawn from a continuous distribution with CDF , strictly increasing on with , and (Assumption 3). If drivers expect a profit rate , then of them participate.
In steady state the platform splits a driver capacity into service capacity on each route, repositioning capacity (empty driving) and queueing capacity (idle drivers). With totals , , and , the set of feasible allocations is
The first equation balances the flows of cars between the locations. The platform earns ; each driver earns
The platform's problem (13) maximizes over with and the participation equation ; its value is .
The paper solves (13) in two steps. Step 1 fixes , computes the maximal revenue over , and among the revenue-maximizing allocations selects one that maximizes , giving the per-driver profit . Step 2 solves . The constants
split capacities into scarce, moderate and ample zones.
The corollary is what makes centralized control a usable benchmark. It says the platform's joint problem, which couples a linear program with a fixed-point equation in , decomposes: the platform can optimize a fixed capacity and then let drivers settle, with no loss. Under the other regimes of the paper this alignment of platform and driver incentives can fail, and the paper's comparisons of regimes (value of admission control, value of repositioning) are measured against the regime- optimum characterized here. Proposition 1 also makes explicit that a centralized platform keeps drivers idle only when all demand is served.
The paper's proofs are in its e-companion, which is not part of the source this mission cites; no machine-checked version of these results exists. The mission produces a checked parametric solution of a small linear program, a checked closed form of the per-driver profit, and a checked equilibrium-and-optimality argument, with every standing assumption made explicit.
Proposition 1 is a parametric linear program in eight variables, but stating its solution is not enough: each zone needs an upper bound on valid on all of , and a second optimization (per-driver profit) over the set of revenue maximizers, which is not a singleton. Driver-optimality (16) is a separate claim about a different objective over the full set ; it holds only because Assumption 2 makes the capacity used for excess cross-location demand still profitable for drivers. Finally, Lemma 1 compares tuples of (13) at different capacities, which requires monotonicity of and in and the participation equation at both capacities. The natural reading of "" as uniqueness of the optimal capacity is false when , since wasteful repositioning can keep revenue at a smaller capacity; the targets assert attainment instead.
All objects live in the namespace RideHailing.Central, in one definition file. Routes are named fields (Λ11 … Λ22, t11 … t22), not indexed. is ProbabilityTheory.cdf μ of a measure μ on . The standing hypothesis Model.Standing bundles , , Assumptions 1–3 as printed, and the paper's implicit conventions, made explicit: , , , , , a probability measure with continuous CDF.
and are defined as suprema over the allocation problem; every target states attainment with IsGreatest or with membership in the selected set, so no conclusion rests on a supremum convention. Capacities in (13) and (16) are strictly positive, because (12d) divides by .
Trivializing formalizations are ruled out: is defined through the two-step selection, never by its closed form (18); "max" is never an unattained supremum; feasibility for (13) includes the participation equation and ; and is characterized by and then quantified over, never chosen.
Regimes and of the paper, which need objects defined only in the e-companion, are out of scope, as are the reformulation of §2.4 and Remark 2. Proofs of any milestone, and lemmas on monotonicity of or attainment of linear programs over , are welcome.
Submodular function minimization (SFM) asks for a set minimizing a function with diminishing marginal returns. It contains minimum cut, matroid intersection and many problems of combinatorial optimization, and the question of how fast it can be solved with a value oracle has a long history: Grötschel, Lovász and Schrijver (1981) gave the first polynomial algorithm via the ellipsoid method; Iwata, Fleischer and Fujishige (2001) and Schrijver (2000) gave the first combinatorial strongly polynomial algorithms; Orlin (2009) brought the bound to .
Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) applied their faster cutting plane method to SFM and obtained an strongly polynomial algorithm. Like several earlier strongly polynomial algorithms, theirs works over a ring family and repeatedly adds new valid arcs that shrink the family without losing a minimizer. The combinatorial core of that step is Lemma 79 (p. 84) and its mirror image Lemma 80 (p. 86), which the authors describe as new to their work. This mission formalizes Lemma 79 and the lemmas its proof uses.
Let and let be submodular (Definition 58): whenever and , where . As in §13.1, .
For write . The base polyhedron is
Every permutation of defines a basic feasible solution (BFS) of by (Theorem 62); precedes when .
A set of arcs on (an acyclic digraph) represents the ring family of sets such that implies for every arc . and are the descendants and the ancestors of , both including . A permutation, or its BFS, is consistent with if for every arc the element precedes (Definition 74). A vector is non-degenerate if it has both a positive and a negative entry. Finally,
An arc is valid if adding it keeps a minimizer of over .
Let be a non-degenerate convex combination of BFS's consistent with . If
then there is such that every minimizer of over that contains also contains .
The mission also contains Lemma 76 (the mirror of Lemma 77), Lemma 78 ( for consistent BFS's) and Lemma 80 (the mirror of Lemma 79, giving an arc with when ).
Lemmas 79 and 80 are what make the paper's SFM algorithms strongly polynomial: each application adds one of at most arcs, and the cutting plane method supplies, through its separating hyperplanes, exactly the convex combinations of consistent BFS's the lemmas take as input. Lemma 80 has no counterpart in earlier work, and the two lemmas are stated for general ring families, which the earlier versions were not. They are also a robust version of Lemma 65: a point of the base polyhedron that is only approximately degenerate still yields structural information about every minimizer.
The lemmas are proved in the paper; none of them is formalized. The mission produces machine-checked statements and proofs of the arc-adding step, in a form independent of the cutting plane machinery and reusable by any formalization of a ring-family SFM algorithm (Iwata–Fleischer–Fujishige, Orlin, or Lee–Sidford–Wong).
The inequality chain of each lemma is short; the work is in the combinatorics of permutations. Moving to the front of a permutation must be shown to produce a permutation again, and the comparison (15.2) depends on knowing exactly which elements precede each before and after the move; the identity holds only because consistency puts all of before , which needs an induction along paths of . The restriction to changes the ground set, so Lemma 77, stated on the full ground set, does not apply verbatim to the restricted problem. The paper's application of Lemma 77 also does not check that the restricted vector is non-degenerate, so that case has to be handled as well.
The ground set is Fin n (0-based); sets are Finset (Fin n), is integer valued and vectors are real. A permutation σ : Equiv.Perm (Fin n) is a position map ( precedes iff σ u < σ v), and the BFS of a permutation is defined by the formula of Theorem 62; Theorem 62 itself (that these are the vertices of ) is not formalized and not needed. Arcs are a relation on Fin n; and use its reflexive-transitive closure, and the digraph is assumed acyclic, as the paper does. Minimizers in Lemmas 76–80 are over the ring family ; in Lemma 65 over all subsets. Constants , and are real numbers.
Running-time and oracle-count clauses ("using oracle calls and time") are out of scope, as is the paper's main Theorem 31 and the bound on the number of BFS's in the combination (the existence claim holds for any finite combination). Validity of the new arc is stated in the strong form proved on p. 85: every minimizer containing contains . The page's base polyhedron constraint "" is read as . The restricted base polyhedron in the restriction claim uses the normalized .
The hypotheses are satisfiable: with , , , , the combination satisfies them for . A modular never does, so the goal is not vacuous only because is genuinely submodular; a formalization in which the BFS's are not tied to , or in which non-degeneracy is non-strict, would change the statement and is ruled out.
Useful infrastructure: greedy vectors of a submodular function lie in its base polyhedron; reordering lemmas for permutations of Fin n; restriction of a set function to the complement of a set. Contributions of proofs of any milestone, and of Lemmas 76, 78 and 80, are welcome.
A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.
Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.
There are manufacturers, . Manufacturer has a horizontal type and a vertical type ; each of the four type classes has exactly members. Joining the blockchain costs manufacturer an amount ; records the decision. A unit mass of consumers values a matching product at and a mismatched one at , with , plus a vendor quality ; the high-quality vendor has marginal cost . Each consumer also has an outside option , drawn from a continuous distribution supported on . The parameter of interest is the horizontal differentiation ; is held fixed and .
Under full adoption, a consumer who has access to the blockchain's information finds a best product utility ; without access, only . A system of transfers charges each consumer who wants access a fee and pays manufacturer an amount . A consumer pays () when
and denotes the mass of paying consumers. The system is self-financing if
Manufacturer earns (15), where the gross profit is zero because of price competition. The system overcomes adoption failures if full adoption ( for all ) is an equilibrium of this game.
The proof of Proposition 4.9 uses the fee and the gain from access
The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.
(a) For and every , is continuous and weakly decreasing on .
(b) For all sufficiently large there is with
so that at the fee exactly the consumers with pay.
Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme (, ) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.
The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.
The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point , and the delicate points are positivity of at the relevant arguments (so that the fee is finite), the three-piece shape of , and choosing large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.
Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. is ProbabilityTheory.cdf μ for a measure μ on ℝ. is an argument of every object, with .Model.Standing): , , , , ; a probability measure without atoms, , and for (support ). No cost function , no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes , the model's .ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.Y. Bai (arXiv:2609.11276, September 2026) proves that the irrationality measure of π is at most 7.101862832357, improving the Zeilberger–Zudilin bound 7.103205334137 (2020). The proof keeps the Zeilberger–Zudilin integral but gives its numerator two independent exponents, specialised at A₁ = A₂ = 1857/2785; the resulting integer linear forms in 1 and π, combined with Hata's lemma, give μ(π) ≤ 7.101862832357. This entry is the campaign template with the value 7.101862832357. Source: https://arxiv.org/abs/2609.11276
The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate from the algorithm proof. Scientific priority and global optimality are not asserted by these formal verification results.
3SUM asks whether three entries at distinct positions in an integer input sum to zero. Its familiar quadratic algorithm makes it a benchmark for studying how much arithmetic structure can reduce the cost of an exhaustive search. The relevant comparison is the exponent of input size in a precisely specified machine model. An improvement to that exponent is an asymptotic statement; it need not provide better measured running times at accessible input sizes.
Alman and Vassilevska Williams, 2026 developed a deterministic truly subquadratic framework for polynomially bounded integer 3SUM. The c0ldzy17 source snapshot, dated 11 October 2026, develops a subsequent deterministic construction with a formally stated 1.962 target. The author-supplied certificate package 3sum_certificate_1p960614_v3, dated 14 October 2026, studies a further parameter and switch refinement. It contains mathematical arguments and exact rational checks, and explicitly leaves the complete modified machine-program theorem unproved. This mission studies that remaining extension together with its supporting certificates.
An input of size is an integer-valued function on the positions . For each fixed natural number , every value has absolute value at most . A YES instance has pairwise distinct positions satisfying . Equal values at different positions are allowed. The problem asks for a decision, so a successful algorithm need not return the positions. Inputs of size less than three are NO instances.
The word RAM is the existing campaign foundation specification. A program is a finite list of instructions for constants, arithmetic, direct and indirect memory access, branching, acceptance and rejection. Words have a fixed width and a signed integer interpretation. For each fixed , one program, one word-width constant and one time function must work for every input size and every sufficiently large word width. The mission retains that specification without introducing an alternative computation model.
The supporting binary entropy is measured in bits:
For an integer expansion , write
These are analytic quantities used to describe local encoding and reporting costs. The source's twelve charges also depend on a representation-scale parameter , a band shift , a box saving , an initial threshold , a terminal fraction , and a uniform entropy coefficient .
The campaign goal is the exact proposition
For , its time requirement is
Correctness and termination still cover all input sizes. The integer-size exponent includes , and the same program must be correct for every word width above its specified threshold.
The primary certificate uses and the rational quartic
Supporting targets establish its validity on , its derivative and tangent bounds, and the uniform inequality . The fixed parameters are , , , , and . The parameter theorem bounds every one of the twelve costs strictly below . Integer scheduling and general local-cover identities are separate milestones. A further independent milestone proves for the explicitly defined relaxed fixed-expansion cost model. That model bound concerns its admissible parameter tuples; it is not a lower bound for 3SUM itself.
The supplied certificate demonstrates that a quartic switch already suffices for the proposed 1.960614 cost target. It also separates a uniform analytic inequality from a numerical experiment: the statement quantifies over the full closed interval. Its finite scheduling statement uses integer comparisons and accounts for the rounding error at every admissible level, rather than requiring executable logarithms.
Formalization adds checked statements about these continuous and finite objects and a reusable dependency structure. The full campaign goal requires an additional result: the actual modified program must obey the certified costs, and its operational correctness must reach the foundation specification. The upstream parameter certificate likewise distinguishes its exponent ledger from its separate implementation obligations. An exact rational checker passing is evidence for the numerical certificates; it does not establish the full new machine theorem.
Changing expansion from 256 to 232 changes the local universe and the vertex, output and degree counts together. The representation scale, band denominator and polynomial switch also change. Consequently, the original fixed-parameter runtime result cannot simply be invoked after replacing a few numerical constants. The new local construction, global encoding, sparse queries, reporting and arithmetic operations must share consistent parameters and a complete cost account.
The small gap between the principal cost cap and the target must absorb the proved subpolynomial overheads, including exceptional-size handling and the conversion to word instructions. The machine bridge has now been proved in this mission. Its accepted dependency tree connects the modified program and its runtime analysis to the unchanged campaign specification. Its statement has no assumed solver callback or unproved runtime contract. The fixed-model lower-bound milestone is an independent analytic root, and is not used to justify a faster algorithm.
The campaign pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Entropy and its derived quantities are real-valued; the final exponent is rational; finite subset counts and cleared switch comparisons use natural numbers. Theorems explicitly restrict logarithmic arguments and denominators to their intended domains. Natural-number subtraction in the switch is used only below the final level, with positive even microblock size.
The local-cover milestone covers every natural and positive half-block size. The cost-model milestone quantifies over all tuples satisfying its written assumptions and includes a whole-interval entropy constraint. Neither finite testing nor a floating-point optimizer substitutes for these universal statements. The initial package includes no Lean proof of the new machine goal, and the mission does not represent it as an established record.
The underlying algorithms and formal infrastructure retain their attribution to Alman and Vassilevska Williams; Björklund, Husfeldt, Kaski and Koivisto; Swapnil Jain; c0ldzy17; Anthropic; Jihoon Hyun; and Lean/Mathlib, as documented by the upstream source. The certificate development and this formalization use AI assistance. Scientific priority and global optimality are outside the mission's claims.
3sum_certificate_1p960614_v3/3sum_certificate_v3/PROOF.md, Sections 0–8; certificates/c232_quartic.json; verify_certificate.py. This is a supplied research artifact, not a claimed public publication.Source code and complete Lean formalization: GitHub repository. Fixed source revision: 8c25c0325de5.
Retail prices are rarely constant over long horizons: promotions, high–low cycles and staggered discounts across similar items are the norm. One explanation in the pricing literature is the reference effect: consumers compare a posted price with a reference price formed from past prices, and react to gains and losses relative to it. Single-product models with reference effects (Popescu and Wu 2007; Hu, Chen and Hu 2016) predict that, for consumers who react symmetrically to gains and losses, the optimal price usually settles to a constant. Guo, Jiang and Shen (SSRN 4189049, published in Manufacturing & Service Operations Management, 2025) study the same question for several substitutable products sold under multinomial-logit (MNL) demand. Their §4.3 shows that pricing substitutes jointly, rather than at one common price, makes cyclic optimal pricing more likely. This mission formalizes that comparison, Theorem 7, together with the results the paper ties it to.
A seller offers products over periods . In period product has price and reference price , both in with . Reference prices follow exponential smoothing with memory .
The deterministic utility of product is
with and . The market share is and the period revenue is . Product is loss-neutral when . The seller maximises with discount ; is the optimal value. The myopic policy maximises over . Throughout, the paper assumes , where solves its equation (9); this makes the ceiling inactive for the myopic problem.
A policy has a steady state if it maps reference to price . An optimal steady state (Definition 4) is a steady state of an optimal policy, and a policy is cyclic when it has no steady state.
§4.3 takes perfect substitutes: , , for all , loss-neutral. The single-product-based policy solves the problem (25) restricted to one common price for all products, from a uniform reference . The common myopic steady state comes from Corollary 2, where solves . The constants are
For identical loss-neutral products with :
and
hold, then has a steady state and the optimal policy has none.
Theorem 7 separates two models that coincide in their steady states (Remark 3) but differ in whether a steady state exists. Joint pricing can sustain asynchronous cycles, in which some substitutes are discounted while others are not, and these keep total purchase probability high. A single common price can only cycle synchronously. Part 1 says the multi-product optimum never settles when the single-price one does not. Part 2 gives explicit parameter regions, strong reference effects (large ), short memory (small ) and patient sellers (large ), where the single-price model predicts a constant price but the true optimum is cyclic. Practically, a retailer who prices similar items at one price can misjudge whether long-run promotions are optimal at all.
The paper's proofs are in its online supplement (Appendix C.6), which is not part of the source file used for this mission. To our knowledge none of these results has a machine-checked proof. A formalization would check the inequality algebra behind (26)–(28) and pin down exactly what "the optimal policy is cyclic" means when optimal policies need not be unique.
The statements compare two infinite-horizon problems, each with a continuous state, through the existence of fixed points of their optimal policies. Neither problem has a closed-form value function. A steady state is optimal only if no deviation, however long, improves on the constant path, so ruling it out requires a profitable deviation, and establishing it for requires a global optimality argument for (25). Stationarity conditions at a steady state only produce candidates (Corollaries 2 and 4); they do not decide whether a candidate is optimal, so the obvious argument stops exactly where the theorem starts. The revenue is not concave in prices, the reference dynamics couple all periods, and the comparison must hold uniformly over every optimal policy, not one computed policy.
Products are Fin n (index for the paper's product ), and parameters are functions Fin n → ℝ; the identical-products results use constant functions of scalars . The market share (3) is defined directly, without the Gumbel derivation. is the supremum of the discounted revenue over all price sequences in , and the single-price value is the supremum over uniform sequences from a uniform reference. Steady states are in sequence form: is an optimal steady state when the constant path from reference attains , and similarly for . "Cyclic" is the universal statement that no point is a steady state. A myopic policy is any maximising selection, and every statement about it quantifies over all selections.
Standing hypotheses in every theorem: , , , , , and stated as "some root of (9) is at most ". Added hypotheses: (the setting of §4.3); in Theorem 7.2, so that is defined (it excludes only , where (26b) fails anyway); for the limit claims of Corollary 2 (at the reference never moves). Quantities the paper calls "the unique solution" are bound as variables solving their equation, never chosen. Remark 4 evaluates (28) at the candidate of Corollary 4, because the conclusion is that no optimal steady state exists.
A trivial formalization is ruled out: "cyclic" may not be read as a statement about one chosen policy or one initial reference price, and the single-price problem may not be replaced by the problem, since it keeps all products and the shared MNL denominator.
A complete development needs: summability and boundedness of discounted revenue, the Bellman characterisation of steady states, analysis of the myopic MNL problem (Theorems 1–2 of the paper), and the second-order analysis behind (28). The MNL revenue lemmas and the sequence-form steady-state calculus are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 7 separately, are welcome.
The Lightning Network is a payment layer built on top of Bitcoin: pairs of participants lock funds in a bilateral payment channel and then exchange payments off-chain, settling on the blockchain only occasionally. Keeping a channel open costs money, because it ties up capital and needs periodic rebalancing, and Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]) showed that this recurring cost depends on the channel's net flow and grows less than proportionally with it. Which network topology a population of payers and payees should use is therefore an economic question about subadditive costs on graphs.
Lightning Network Economics: Topology (SSRN 4439190; published version in Management Science, 2024, doi:10.1287/mnsc.2023.03872) answers this question in an axiomatic model. Its §3.2 introduces hermetization, which replaces the channels inside a group of nodes by channels to a new hub, and asks when this reduces cost. Theorem 3.8 gives a deterministic sufficient condition, a large average degree compared with the spread of channel sizes. Theorem 3.9, the subject of this mission, shows that the condition is typical: if channel sizes are random with thin, power-law-bounded cost tails, the network is hermetizable with high probability. The paper reads this as "cost reduction is the norm, not the exception", which is the economic argument for hubs in payment-channel networks.
Nodes form a finite set . A Lightning Network (LN) is an anti-symmetric real matrix , , of net channel flows; means there is no channel between and . A channel cost is a function with
The cost of the network is . For a node , is its number of channels, the smallest and the largest over its channels.
The hermetization of a set of nodes deletes all channels inside , adds a new node , and joins each to by a channel carrying , its net flow towards the rest of . The set is hermetizable if this strictly lowers the cost, and the LN is hermetizable if some is.
In the random model a simple graph on fixes the channels, so is the degree of in and is not random. On a probability space , the flows are random variables, nonzero exactly on the channels of , and is an LN for every .
Let , , . There is , depending only on , such that for every finite with at least one channel, every satisfying (MO)–(SA+), and every random LN with, for all channels ,
the LN is hermetizable with probability at least
The constant is not fixed: any uniform in the network and in is a proof of the goal.
The paper closes with "for some constant , , whence the claim."
The theorem turns the deterministic criterion of Lemma B.1 into a statement about typical networks. When degrees grow, decays, and the probability that no hub can reduce cost vanishes for any law with a power-bounded cost tail and a positive cost floor. This is the paper's evidence that hub-and-spoke structures are the economically stable outcome; the companion results of the paper (Theorem 3.1 on local restructuring, Theorem 3.10 on the star topology) are treated in sibling missions of this series.
The result is proved in the paper, in about half a page. It has no machine-checked proof. Formalizing it makes the quantifier structure explicit, in particular that does not depend on the network, settles the boundary cases the paper leaves implicit, and records corrected forms of two axioms that are unsatisfiable as printed. Lemma B.1 is shared with the mission on Theorem 3.8.
The probabilistic estimates are elementary; the obstacles are in the bookkeeping. Lemma B.1 compares two costs on different node sets (the hermetized network has one more node), and its degrees and channel sizes must be read in the subnetwork induced on ; with the degrees of the whole network the lemma is false. To apply it to a random network one must choose : the set of all nodes fails when some node is isolated, because is then undefined. The step from the strict tail of (i) to the weak tail used in (12)–(13) is a limit the paper does not write out. The inverse that the paper uses need not exist, since is not assumed onto.
Nodes are an arbitrary finite type V; the LN is Λ : V → V → ℝ, anti-symmetric; the channel graph is E : SimpleGraph V, with for every , and is E.degree i. The cost is the form. The hub of a hermetization is none : Option V. Probabilities are toReal of a probability measure, and events are not assumed measurable. Each is assumed measurable in the goal. The conventions committed to:
The following formalizations are trivializing and are ruled out: a allowed to depend on , , , , or (take large enough that the bound is ); a specific law, such as a Pareto law, or a specific cost such as ; replacing "the LN is hermetizable" by the event that every node satisfies Lemma B.1's inequality; an empty channel set; and the printed, unsatisfiable (SA) or (SA+), under which every statement is vacuous.
The development needs finite sums over Option V, a min/max over a node's channels, and union bounds for outer measures (Mathlib's measure_biUnion_finset_le). Contributions welcome: proofs of the milestones, a proof that the corrected axioms are satisfiable by , , and a reusable statement of Lemma B.1 for the series.
Most online advertising inventory is sold one impression at a time in automated auctions, and since about 2019 the major ad exchanges have moved from second-price to first-price rules: the highest bidder wins and pays its own bid. A bidder in a first-price auction must trade off winning probability against the price paid, and that trade-off depends on the unknown distribution of competing bids. A bidder who takes part in many such auctions can learn that distribution as it goes. The natural yardstick is regret: the expected shortfall of the bidder's cumulative reward relative to an oracle that knows the distribution of competing bids from the start.
Han, Zhou and Weissman (arXiv:2003.09795, Operations Research, 2025) give bidding policies whose expected regret is over auctions, both for iid and for adversarial private values, under the censored feedback that real exchanges provide (only the winning bid is announced). Their Theorem 9 shows that the rate cannot be improved, even in a much easier setting. This mission is that lower bound.
Related results put it in context. With binary feedback (only "won" or "lost"), regret of order is unavoidable (Kleinberg and Leighton, 2003). With a fixed value, repeated first-price bidding is a pricing problem on a one-dimensional action set whose reward need not be continuous in . Theorem 9 shows that the extra information of the full competing bid buys and nothing better.
In each round a bidder has a private value , submits a bid , and faces the highest other bid (HOB) , the largest bid of all competitors. The bidder wins when , and its payoff is
The HOBs are iid with an unknown cumulative distribution function on . No smoothness is assumed: may have atoms. The expected reward of bid at value is , and the regret of the bids is
A policy chooses from what it has observed before round , and it may use internal randomness. Theorem 9 makes the problem as easy as possible: the value is in every round, and the HOB is revealed at the end of every round (full information), rather than only when the bidder loses. A policy is then a rule , where is the policy's internal randomness.
The lower bound uses two HOB laws on . For , puts mass on and on , and the reverse. is the law of iid HOBs from . The total variation distance is , and is the Kullback–Leibler divergence.
There is an absolute constant such that, for every horizon ,
where the supremum is over all HOB distributions on and the infimum is over all full-information policies, randomized ones included. The constant is left unspecified, as in the paper; the paper's proof gives .
The theorem shows that the upper bounds of the paper, for iid values and for adversarial values, are optimal up to logarithmic factors. Because the lower bound holds with a constant value and with every HOB revealed, it is not caused by censoring or by the value process. The comes from the statistical difficulty of locating the maximizer of when is learned from samples. The same lower bound therefore applies to every richer feedback model and every value model that contains the constant sequence.
The milestones are general tools. Lemma 12 (a symmetrised Bretagnolle–Huber inequality), the product rule for KL divergences of iid laws, and the reduction (21) are the standard steps of Le Cam's two-point method. They recur in essentially every minimax lower bound for bandits and online learning.
The theorem has a complete proof in the paper (App. B). As far as is known it has not been machine-checked, and the needed pieces are only partly in Mathlib: there is a Kullback–Leibler divergence with a chain rule, but at the pinned revision there is no total variation distance and no Bretagnolle–Huber or Le Cam inequality. The work is to formalize the known proof.
The arithmetic is elementary, and the difficulty lies in the probabilistic reduction. The first idea, bounding the regret round by round under a single law, fails: for any fixed a policy that happens to bid the right point has zero regret, so the lower bound must come from a policy's inability to know which of two laws it faces. Making that precise requires the law of the observed history under each hypothesis, the identity , and monotonicity of total variation under marginalization from to coordinates. A randomized policy adds one more integration, over its internal randomness, before the per-round bound applies. The KL step needs the tensorization of KL over product measures and an elementary but explicit logarithmic inequality.
All declarations live in the namespace FirstPriceLearning.LowerBound.
Fin T; Lean round t is paper time .μG on ℝ. The goal asks for a probability measure giving no mass outside . The CDF is (μG (Set.Iic x)).toReal, with atoms allowed.U : Type, for its internal randomness and bid maps bid t : U → (Fin t → ℝ) → ℝ that are jointly measurable with values in . The history type Fin t → ℝ makes the policy non-anticipating by construction: it cannot read or later HOBs, and it never sees .Measure.prod with Measure.pi).InformationTheory.klDiv, valued in . Total variation is defined locally as with Radon–Nikodym densities. In Lemma 12 the right-hand side is when a divergence is infinite ().Two trivializing formalizations are excluded. A policy that observes (or ) before bidding would make the bound false rather than trivial, and the types forbid it. A non-measurable bid map would make the expectation the junk value , and measurability is required. Restricting the policy class to deterministic policies, or reading in Lemma 12, would change the theorem and is not done.
Reusable beyond this mission: the total variation distance, Lemma 12, and the tensorization bound for KL. Contributions are welcome at every milestone, especially Lemma 12 and the data-processing step behind (21).
Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price above the reference is perceived as a loss and a price below it as a gain. When gains and losses weigh differently, the seller's current price shapes tomorrow's demand, and dynamic pricing becomes a sequential decision problem. A central question in this literature is whether the seller should hold a constant price in the long run or keep cycling through high and low prices.
For a single product, classic results show that loss aversion favours constant prices (Fibich, Gavious and Lowengart 2003; Popescu and Wu 2007; Nasiry and Popescu 2011). Hu and Nasiry (2018) showed that individual loss aversion need not carry over to aggregate demand, and under logit demand Jiang, Cao and Shen (2022, Proposition 5) found loss-averse single-product settings in which cyclic pricing is optimal. Guo, Jiang and Shen (2025) study the multi-product version under multinomial logit demand. For general parameters they show that an optimal steady state may fail to exist. This mission formalizes their positive result for one market: consumers who ignore gains, i.e. who do not respond to discounts. The paper motivates this case with luxury goods, where promotions can signal declining prestige.
A seller offers products . Product has intrinsic utility , price sensitivity and reference sensitivities (to gains) and (to losses). At price vector and reference price vector , the utility of product is
with . The multinomial logit market share and the single-period revenue are
Prices and reference prices lie in the admissible box with . Reference prices follow exponential smoothing with memory : . Revenue is discounted at rate , and the optimal value from reference price is
The myopic policy maximises over . An optimal steady state (Definition 4) is a price fixed by the optimal policy: holding the price at forever is optimal when the reference price is .
Throughout §3–§4 the paper assumes the price ceiling is large enough: , where is the root of
Under this assumption the ceiling does not bind for the myopic problem.
Consumers are promotion-insensitive when for every : a price below the reference brings no extra utility, while a price above it is penalised at rate .
If for all , then there exists with
This holds for all parameters, memory and discount factors satisfying the hypotheses.
Under there is that is a fixed point of the myopic policy and whose diagonal pair attains the largest single-period revenue:
Theorem 6 is the only general existence result for optimal steady states in the paper. Theorem 4 shows that a single gain-seeking product rules out any optimal steady state. Theorem 5 constrains where a steady state can lie when there is no gain-seeking product, but it does not say that one exists. Theorem 6 settles existence for promotion-insensitive markets, for every number of products and every parameter value: constant pricing is optimal in the long run regardless of parameters and initial reference prices. This holds even though the aggregate logit demand can be more sensitive to gains than to losses in some regions, which is exactly the situation in which earlier general guarantees for constant pricing do not apply.
The result is proved in the paper's online supplement (App. C.5), which is not part of the source file used here. It has no machine-checked proof. Formalizing it requires the first Lean treatment of reference-dependent MNL revenue, with a kinked utility, an outside option and an exponentially smoothed state. It also requires a sequence-form optimal value function for a deterministic infinite-horizon problem with a continuous state. The other missions of this series (myopic dynamics, optimality gap, gain-seeking cycles, steady-state structure, multi- versus single-price policies) use the same objects.
is neither concave nor monotone in a convenient way. Setting does not simply make the reference price irrelevant. Lowering a product's utility raises the logit revenue when that product's price is below the current revenue level, so a larger loss term can help. The joint maximisation over therefore does not reduce to "take ". The diagonal maximiser must also lie inside the box, and that is where the ceiling assumption , which involves the transcendental equation (9), enters. Finally, an optimal steady state is a statement about the infinite-horizon optimum , a supremum over all price sequences. It is not about the myopic policy, and a myopic fixed point is not in general an optimal steady state.
Products are indexed by Fin n (the paper's product is index ), and vectors are Fin n → ℝ. The market shares (3) are defined directly. The Gumbel random-utility derivation is motivation only. Every statement carries the standing hypotheses of §2:
Fin n (zero when ).is the supremum of the discounted revenue over all admissible price sequences rather than over stationary policies. For this deterministic problem with continuous revenue on a compact box the two values coincide. Optimal policies need not be unique, so an optimal steady state is stated as optimality of the constant price path: and . The milestone's "myopic fixed point" is stated as " maximises over the box", without fixing a myopic selection.
No trivializing reading is available. On the box , so the sequence family is bounded by and is the genuine supremum, not Lean's default value . The hypothesis is (no response to gains), not the opposite case , and the conclusion is existence only, not uniqueness. A complete development needs bounds and continuity for the logit revenue, the joint single-period maximisation behind the milestone, and the comparison of the constant path with arbitrary sequences. The revenue model and the value function are reusable throughout the series. Proofs of either item, and of general facts about the shared model, are welcome.