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?
Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.
The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.
There are items. A customer has a nonnegative valuation vector , sampled from a probability law . A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.
In discriminatory pricing (DP), the seller assigns a nonnegative price to each item and offers only the individual items. Write for expected revenue and for its optimum over item-price vectors.
In opaque selling (OPQ), the seller offers the items at a common price and also offers every set of at least two items. A set of size costs , independent of which items it contains. A pessimistic customer values at ; a risk-neutral customer values it at . Both value a singleton at its item value. A customer is pessimistic with probability and risk-neutral with probability , independently of the valuation vector. The expected revenue of a price menu is ; its optimum is .
A law is exchangeable if permuting the coordinates of leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers such that almost every valuation vector has every coordinate in . This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.
For exchangeable , nonnegative valuations, and , the target is
The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.
The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.
The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.
The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.
One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.
Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.
Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.
The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the -weighted sum of the two type-specific expectations.
Expected revenues and optimal revenues use extended nonnegative reals . The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.
The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.
ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.Rewards-based crowdfunding platforms such as Kickstarter and Indiegogo let a creator pre-sell a product before it exists. Most backers cannot judge the product's quality from a campaign page, while some (experts, early adopters, people who have seen a prototype) can. A creator who knows her product is good therefore faces a classical signaling problem: how to convince the uninformed crowd without simply copying what a creator of a worse product could also do. Chakraborty and Swinney (SSRN 2885457, forthcoming in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0833) show that crowdfunding offers a signaling device absent from ordinary retail: the funding target of an all-or-nothing campaign. The paper sits in the signaling literature that starts with Spence (1973) and Milgrom and Roberts (1986), and uses the equilibrium refinement of Cho and Kreps (1987).
A creator of private type runs an all-or-nothing campaign whose reward is one unit of her product. Backers value the products at ; producing requires a fixed startup cost , with . The number of interested backers is , and , so success is uncertain for both types.
The creator chooses a design : a funding target (the funding constraint) and a reward price . A fraction of the backers is informed and pledges iff . The remaining fraction is uninformed: it sees only , forms a belief about the type and pledges iff does not exceed the believed valuation. If a share of the backers pledges, the campaign succeeds iff ; then the creator collects and pays , otherwise all pledges are refunded. The expected profit is (1):
A separating equilibrium is a pair of distinct designs such that, with the uninformed backers believing exactly at and at every other design, neither type gains from any feasible deviation; in particular the L-type does not gain by mimicking . It survives the intuitive criterion if no off-path design makes one type strictly better off when recognized, while making the other type strictly worse off under any belief. With
the paper's target is
For every , the designs and form a separating equilibrium that survives the intuitive criterion, and every separating equilibrium that survives the criterion has
Proposition 3 says that a high-quality creator signals by raising her funding target, accepting a lower chance of success, and never by lowering her price; signaling is free when the informed fraction is large (). In contrast with signaling by price alone (Proposition 2 of the paper), a separating equilibrium always exists. The closed form is what the paper's later results build on, notably the endogenous quality choice of Proposition 5.
The result is proved in the paper's Online Supplement by calculus and case analysis. As far as is known, no part of it has been machine-checked. A formalization verifies the equilibrium characterization, including the boundary cases the printed proof treats in a sentence (uniqueness fails at , ), and gives a reusable model of all-or-nothing campaigns with a uniform crowd.
The algebra of each step is elementary. The difficulty lies in the equilibrium argument. Showing that the given pair is an equilibrium requires bounding the H-type's profit at every design believed to be low quality, including prices at or below , where the informed and uninformed backers both pledge. The paper checks only the deviation to . The characterization requires turning the intuitive criterion into a maximization of the H-type's profit over the mimicking-proof designs and showing that is its unique maximizer. A natural first idea, to fix and lower the price until mimicking stops (Proposition 2's equilibrium), does not give the maximizer: along raising the target pays more than lowering the price.
Real.sqrt algebra, monotonicity along a curve. All of it is in Mathlib; the model definitions are new. Proofs of any milestone are welcome, and so are alternative proofs of the goal that avoid the derivative.Firms that moved production offshore for low unit costs pay for it in lead time: a slow global supplier forces large safety stocks, and the cost of those stocks grows with demand variability. A recurring question in operations management is when it pays to re-shore part of production to a fast, local, more expensive plant. Adidas's "SpeedFactories" are the example that gives this paper its name. Boute, Disney, Gijsbrechts and Van Mieghem (accepted manuscript, 2020; Management Science 2022) answer this for a linear dual-sourcing policy. Their analysis yields an explicit break-even price for the off-shore supplier, together with a condition under which a small local plant that absorbs only demand variability beats full off-shoring, even when local production costs more per unit than off-shore purchasing.
The dual-sourcing literature (Whittemore and Saunders 1977; Song and Zipkin 2009; Janakiraman, Seshadri and Sheopuri 2015) shows that optimal dual-sourcing policies have no simple structure for general lead times. Xin and Goldberg (2018) proved that tailored base-surge (TBS) policies are asymptotically optimal as the global lead time grows. The present paper combines TBS with a smoothing local replenishment rule and prices the local capacity explicitly.
A firm serves demand , , from finished-goods inventory ; excess demand is backlogged. The demands are independent and identically distributed , where is the standard deviation. Holding costs and backlog costs per unit and period: .
Two sources replenish the inventory:
The TBS-POUT policy with allocation and smoothing parameter orders the constant globally and
locally, where is the safety stock. The inventory evolves by . The long-run average cost is . The optimized dual-sourcing cost is its infimum over .
The benchmark is full off-shoring with the order-up-to policy: order with inventory . Its optimized long-run cost over is .
With the standard normal density and distribution function, and . The paper's standard deviations are
and the break-even price (20) is
If
then is concave on and whenever . Otherwise is convex on , and whenever for some , the allocation is the unique minimizer of on and beats . The smoothing parameter is fixed and arbitrary in .
Proposition 4 is the paper's strategic prescription. It splits the parameter space by one dimensionless product of a financial factor, a variability factor and a service/flexibility factor. On one side, a small SpeedFactory serving only the demand variability is profitable in a price band below the local unit cost. On the other side, re-shoring is all-or-nothing. Since grows like while do not depend on , long off-shore lead times push towards the first regime (Figure 6 of the paper: concave at , convex at ).
The printed proof of Proposition 4 is a single sentence ("readily obtained from the second derivative of "). The content is in the chain behind it: the inventory under TBS-POUT is an AR(1) process, two Gaussian newsvendor problems give its optimal cost, and the order-up-to benchmark has inventory variance . Formalizing the mission machine-checks that chain from the dynamics to the strategic conclusion. None of these results is formalized anywhere to our knowledge. Reusable outputs include the variance of a linear filter of iid noise, the Gaussian newsvendor minimization, and the long-run cost of the order-up-to policy under iid normal demand.
Once the closed forms (13) and (18) are known, the goal is algebra: with , and (21) is equivalent to . The work is in reaching (13) and (18) from the dynamics:
Taking (13) and (18) as definitions would skip all of this and is ruled out.
Lean namespace SpeedFactory.BreakEven, two definition files and eight theorem statements.
d : ℕ → Ω → ℝ on a probability space, mutually independent, each with law gaussianReal μ (σ²). Periods start at ; d 0 is unused. Independence is assumed, although the printed propositions say "identically, normally distributed": (14), and §5 all need it.IsLeast) and unique minimizers, so no junk value of sInf or liminf can make a statement true by accident. The critical fractiles are computed from the quantile, not left free.Contributions welcome: proofs of the milestones, in particular a general Gaussian newsvendor lemma and the AR(1) variance recursion, which are reusable beyond this mission.
Online marketplaces such as Airbnb, Upwork and eBay match buyers and sellers but do not set transaction prices. They earn revenue through commissions (a fraction of the transaction price) and subscription fees (a fixed charge per transaction), and they often differentiate these fees by participant type. Prices then form endogenously, as a competitive equilibrium of the market the fees induce. Choosing revenue-maximizing fees is therefore a bilevel problem: the platform optimizes over fees, and every choice of fees changes the equilibrium prices and trades. Birge, Candogan, Chen and Saban (SSRN 3259716; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0853) show that, despite its nonconvexity, this problem is solved exactly by a convex program, and they characterize all optimal fee profiles. The rest of their paper, which compares commissions with subscriptions and studies how the network shapes revenue, rests on this result.
There are finitely many seller types and buyer types . A bipartite compatibility network says which types can trade; every type has degree at least one. Type consists of a continuum of sellers of mass , and type of buyers of mass . A type- buyer's value is distributed according to on , and a type- seller's reservation value according to on , with . A buyer who trades with a type- seller incurs a disutility . Assumption 1 asks that each be continuous, continuously differentiable and strictly increasing on , with bounded mean. Its inverse is .
The platform picks commissions and subscriptions in : and . A competitive equilibrium consists of prices , flows on and supplies and demands with
markets clearing (, ), and buyers trading only with their cheapest compatible sellers. The revenue problem (3) is
Assumption 2 asks that and be strictly concave in , a regularity condition on both sides of the market. The relaxation (7) is
over flows on with marginals , and .
Let be an optimal solution of (7). Then (i)
and every optimal solution of (3) has supply-demand vector . (ii) For with , with , , and , the pair is optimal if and only if some and some optimal flow of (7) solve the linear system (8a)–(8f).
In the order the proof uses them:
The result turns a nonconvex bilevel problem into a convex network-flow problem with separable concave objective: the optimal supply-demand vector is computed without reference to fees or prices. Part (ii) describes the whole set of optimal fees as solutions of a linear feasibility system, which is what the paper uses to compare fee structures: a subscription-only profile is always optimal (Step (i-2)), and the comparisons with homogeneous and one-sided fees (Propositions 4–6) and the analysis of which network positions earn surplus (Theorems 2–3) start from it. No machine-checked version of these results exists on the platform. The mission formalizes the statement chain of the paper's proof (main text and e-companion), including the equilibrium existence and uniqueness of Proposition 1 and the KKT theory of the relaxation.
The bound is a rearrangement. Equality needs an equilibrium that realizes the optimum of (7), and the natural candidate prices are the dual variables of (7). These need not exist with finite values in general: the objective pieces and can have infinite slope at the boundary, for instance for unbounded supports. The proof therefore needs the boundary-slope facts of Lemma EC.1(ii) and a "special" KKT system in derivative form. Proposition 1 needs its own convex program for the equilibrium and is the deepest milestone. In part (ii) the optimal flow of (7) is not unique, so necessity has to use the flow of the equilibrium, not a fixed optimal flow.
Types are arbitrary finite types; flows are functions whose values off are never read. The upper end of each support is in WithTop ℝ, and is defined from . The standing assumptions of pp. 7–8 (positive masses, , degree at least one, each a continuous CDF extended to ) are explicit hypotheses. Two conventions concern unbounded supports, where . The feasible set of (7) requires when , since the paper's objective is at . For the same sellers, Assumption 2 is posed on ; on with a finite stand-in value it would be unsatisfiable. "Optimal solutions exist" is stated as attainment (IsGreatest). An optimal fee pair is one for which some equilibrium attains . Slopes , are limits of derivatives from inside the interval (footnote 22). Proposition EC.1 is posed only at the instance (7); the general framework problem (EC.1) is not formalized.
Theorem 1(ii) is stated with an optimal flow of (7), because the printed version with the fixed is false when optimal flows are not unique. The sentence "the optimal commission-subscription vector is not unique" is not posed. Ruled out as trivializing: defining the revenue of an equilibrium as instead of (3a); reading "optimal solutions exist" as an unattained supremum; an equilibrium without the buyers' minimum in (2b) or the cheapest-seller restriction (2d); a feasible set of (7) that admits for unbounded sellers at a finite junk cost; and an Assumption 2 that no unbounded seller distribution satisfies.
A complete development needs basic facts on generalized inverses of continuous CDFs, existence and KKT theory for separable concave maximization over a flow polytope (not in Mathlib), and equilibrium existence for Proposition 1. The concave-programming layer is reusable beyond this mission. Proofs of individual milestones, and sanity checks such as uniform or exponential markets, are welcome. The paper's proofs are in its e-companion, which is part of the cited SSRN file (EC.1.1, pp. ec2–ec6; EC.2.1; EC.3.1, pp. ec38–ec44).
Portfolio selection uses observed asset returns to choose weights that balance expected return against variability. Estimates of both quantities can change sharply when the historical sample changes. A distributionally robust model addresses this uncertainty by allowing the return law to vary around the empirical law, then judging a portfolio by its worst variance and worst expected return. In the model of Blanchet, Chen, and Zhou, the allowed laws form a ball defined by an optimal transportation cost. Theorem 1 asks whether this optimization over probability laws can be expressed using only the sample and a norm of the portfolio weights.
The paper presents this equivalence as its first main contribution. Its later sections use statistical assumptions on a return time series to guide the choice of the ball radius and the return target. This mission concerns the finite-sample equivalence itself; those statistical choices are separate results. The distinction matters because the equivalence holds for a given nonnegative radius and target, without imposing a model for how the observations were generated. Theorem 1 and §3 of the preprint make these two roles explicit.
There are assets and observed return vectors . A portfolio is a vector whose weights sum to one. Its return when the asset return vector is is . The empirical law is , so empirical expectations and variances use the population normalization . No independence assumption is needed for this finite-sample problem.
Fix and its Hölder conjugate , so . The endpoint , is included. Moving a return vector to costs . For two probability laws , the transportation cost is the infimum of expected over joint laws whose first marginal is and second marginal is . With radius , the ambiguity set is
For target return , the feasible region contains portfolios whose weights sum to one and whose expected return under every is at least . This is the paper's worst-case mean condition. For any such portfolio, the robust objective is the supremum of over the same ambiguity set. These objects are defined in §§1–2.2 of the preprint.
Proposition 1 identifies the minimum expected return over the ball:
Proposition 3 evaluates the maximum second moment subject to a specified mean . Write , , and . When , its value is
The two displayed steps in the proof of Theorem 1 connect this constrained value to the unconstrained worst variance: , whose maximum over allowed is and is attained at . These milestones retain the paper's constants, feasibility range, and attainment claims. Propositions 1 and 3 and the proof of Theorem 1 give the source statements.
Theorem 1 is the goal. It says that the robust problem (2) and the empirical problem (9) have both the same optimal portfolios and the same optimal value:
The statement also equates the minimizer sets, rather than equating values alone. The paper calls (9) the dual problem; here that name denotes this regularized empirical optimization problem. Theorem 1, p. 6 is the pinned target.
The theorem replaces an optimization over probability laws with a finite-dimensional portfolio objective containing a norm penalty. It gives a precise interpretation of that penalty: its size and exponent follow from the Wasserstein radius and transport norm. It also preserves which portfolios are optimal, so the reformulation supports the portfolio decision itself, not only its reported objective value. The target-return constraint still depends on the worst expected return; Proposition 1 gives its explicit empirical form. These consequences are stated in §2.2 of the preprint.
A complete formalization would establish the finite-sample equivalence and the attained extrema that underlie it. It would also supply reusable results about finite empirical measures, transport balls with quadratic norm costs, and portfolio moments under those balls. The pinned results are proved in the paper; the work here is to give their statements and proofs in Lean under a shared, audited model. The current local proposal consists of statements with proof placeholders, not machine-checked proofs of those results.
The adversary changes the whole probability law, while the robust objective subtracts the square of the law's own mean from its second moment. Maximizing the second moment alone does not therefore give the worst variance. The mean constraint in Proposition 3 and the subsequent optimization over are essential to recovering the centered objective. Attainment also matters: the paper states minima and maxima, whereas a bound on an infimum or supremum would be weaker. At the level of Lean definitions, every law in the quadratic transport ball must have sufficiently integrable portfolio returns for the real moment formulas to express the paper's quantities. These are the central obligations of §2.2 and Appendices A–C.
Return vectors and weights are functions Fin d → ℝ; the sample is indexed by Fin n with . Exponents are extended nonnegative reals to include , while is finite as in the paper's fixed real exponent. The cost takes values in , and the reused transport definition fixes both coupling marginals. The ambiguity set contains all probability laws within the cost radius, with no added moment restriction. The portfolio moments are real Bochner integrals. Showing that the quadratic-cost ball makes these integrals meaningful is part of proving the results.
The robust variance objective uses an extended-real supremum. This represents an empty or unbounded indexing set without the default value of a real supremum. The feasible mean constraint is written as a universal lower bound over the ball, matching the paper's minimum constraint. The goal compares both minimizer sets and infimum values on that feasible region. It cannot be discharged by defining the robust objective to equal the regularized formula, narrowing the ambiguity set, or assuming the desired moment and value identities. Proposition 1 and Proposition 3 retain attainment through IsLeast and IsGreatest.
This mission covers the finite-sample reformulation in §§1–2.2. The time-series assumptions A1–A3, the data-driven choices of and in §3, Theorem 2, and Proposition 4 are outside its scope. Contributions on transport-ball integrability, the two attained extrema, the scalar maximization, and the final equivalence would all support the goal. The general-cost dual formula of Proposition 2 is omitted because the printed formulation has a boundary counterexample at ; a faithful version needs a separate audit of its duality hypotheses.
A seller with one item and several buyers whose values are private but drawn from known, independent distributions can maximize expected revenue with Myerson's optimal auction (Myerson, 1981). That auction depends on every distribution through virtual values, asks buyers to report their values, and allocates through a computation that buyers must trust. A sequential posted-price (SPP) mechanism is far simpler: the seller fixes one take-it-or-leave-it price per buyer and approaches the buyers one at a time. Posted prices are common in practice, and no buyer reports anything. The natural question is how much revenue this simplicity costs, measured as the worst-case ratio between the best SPP revenue and the optimal revenue.
Timeline. Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices earn at least of the optimal revenue in the single-unit setting with independent buyers. Azar, Chiplunkar and Kaplan (2018) improved this to for , which gave the best universal bound before the present paper. No SPP mechanism can guarantee more than about even for i.i.d. values (Hill and Kertz, 1982; Correa et al., 2017). Beyhaghi, Golrezaei, Paes Leme, Pál and Sivan (Operations Research, 2021; arXiv:1807.03435) proved the universal bound , valid for every , together with -dependent, multi-unit and matroid results and a bound of for eager second-price auctions. This mission formalizes their single-unit universal bound.
There are buyers . Buyer has a value drawn from a probability distribution on , independently across buyers; the profile has law .
SPP. Given prices , the mechanism approaches buyers in decreasing order of price, offers to buyer while the item is unsold, and sells to the first buyer with at price . Its revenue at the profile is therefore (zero if nobody accepts), and denotes its expectation.
Threshold mechanisms (the benchmark). By the taxation principle (Lemma 1 of the paper, cited from Nisan et al.), a deterministic truthful mechanism is described by thresholds depending only on the other buyers' values: buyer wins and pays when . In the single-unit setting, almost surely at most one buyer weakly exceeds their threshold. The expected revenue is . Define
so that (Equation (1)).
Two pricing rules. Myersonian prices post to buyer the threshold computed on an independent re-sample of the other buyers' values, freshly for each ; MP is the resulting expected revenue and the probability that some buyer has . The uniform price rule posts the same price to everyone; .
The factor-revealing program (FR). With ,
For every , every independent value distributions and every single-unit threshold mechanism with finite expected revenue , there is a vector of nonnegative prices with
The prices depend on the instance; the constant does not.
The intermediate statement , the "best of Myersonian and uniform" form shown first in the proof, is context only: Theorem 1 asserts one deterministic price vector, and that is the goal.
The result. Theorem 1 was the first improvement over for single-unit posted pricing that holds for every number of buyers and for arbitrary (regular or irregular) independent distributions. It quantifies the price of simplicity of posted pricing against the optimal auction, and its method (two pricing rules, each giving one constraint on the revenue curve , and a factor-revealing program over all curves meeting both) is reused in the paper for -dependent, multi-unit, position-auction and eager second-price bounds.
Formalizing it. The result is proved on paper; no machine-checked version exists. A formalization checks the probabilistic core, the solution of an infinite-dimensional program, and the numerical constants. The printed constants carry rounding slips ( is a rounding of ; , printed as ), which the milestones state precisely. The paper's normalization silently assumes that Opt is finite; the formal statement makes that hypothesis explicit.
The Myersonian rule alone gives only , and the paper's example (values uniform on ) shows this is tight for it; the uniform rule alone is also bounded away from 1. The improvement comes only from combining them, and the combination is expressed as an optimization over all decreasing curves : the step that the obvious argument misses is the exact solution of (FR), whose optimum must be guessed and certified for an infinite-dimensional program with a nonlinear constraint. The probabilistic step is subtle as well: the true thresholds are correlated across buyers, and Lemma 2 holds only for the independently re-sampled . Finally, the theorem claims a single deterministic price vector, so the random Myersonian prices and a possibly unattained best uniform price must both be converted into one concrete , with the slack between and absorbing the approximation.
Buyers are Fin n; values have law Measure.pi μ with each μ i a probability measure on ℝ; values need not be nonnegative. Revenues and probabilities are in ℝ≥0∞ (lower Lebesgue integrals and measures), never Bochner integrals, so that a non-integrable revenue cannot become a junk zero. The SPP revenue at a profile is the closed form of the price-ordered sale. A threshold mechanism is a family t i v with t i measurable, nonnegative, independent of coordinate i, and almost surely at most one buyer with t i v ≤ v i. Myersonian prices are read from a fresh copy of the whole profile per buyer, independent of everything else. In (FR) the constraint is encoded as and .
Benchmark. The goal is stated for every single-unit threshold mechanism, which is the taxation-principle form of Lemma 1; for the optimal mechanism's thresholds it is the printed theorem, and the paper's proof never uses optimality. Lemma 1 and Myerson's theorem are cited by the paper and are not part of the mission. The one added hypothesis on the goal, finiteness of Opt, is necessary: without it some single-unit threshold mechanisms have infinite revenue while every posted-price revenue is finite.
Ruled out. The SPP revenue is the revenue of the actual sequential sale, not a free function; thresholds may not depend on the buyer's own value (that would allow full surplus extraction) and must be single-unit feasible (otherwise Opt could be times any posted-price revenue); the constant is the explicit , not an existential one.
Out of scope. Theorem 2 (-dependent bounds), Theorem 3 and Lemmas 3–4 (multi-unit), Lemmas 5–7 and Theorem 4 (position auctions), the partition-matroid claim and Proposition 1 (matroids), Lemma 8 and Theorems 5–6 (eager second-price auctions), Inequality (6) of Lemma 2, the illustration of §4.1, and the numerical tables.
Infrastructure. The development needs the layer-cake formula for lower integrals, independence under product measures, the AM–GM inequality and , all in Mathlib, plus a numerical certificate for the root of a transcendental equation. The threshold-mechanism and SPP definitions are reusable for the multi-unit and matroid results of the same paper. Proofs of any milestone, alternative arguments, and sharper constants are welcome.
Online matching platforms (labor platforms such as Upwork or TaskRabbit, dating sites, short-term rental platforms) make it cheap to contact potential partners, but not cheap to find one who is still available. A worker who has already accepted a job, or a listing that is already booked, keeps receiving applications and keeps being screened. Arnosti, Johari and Kanoria, Managing Congestion in Matching Markets (M&SOM 23(3):620–636, 2021), build a stochastic game-theoretic model of this effect, in which applicants pay to apply and employers pay to screen, and employers cannot see which applicants have already matched. They prove that the model has a unique equilibrium, compute both sides' welfare in it in closed form, and use the formulas to evaluate platform interventions (application limits, application fees, a market-wide wage).
This mission formalizes the equilibrium characterization: the closed-form equilibrium welfare of Theorem 2, together with the existence and uniqueness results (Proposition 2, Theorem 1) and the identities from the paper's endnotes that connect them.
A market has four parameters: , the number of applicants per employer; , the probability that an applicant is qualified for a given employer; , the cost of one application; and , the cost of screening one applicant. Throughout, Assumption 1 holds: . Write .
Applicants choose an application intensity : an applicant sends a Poisson() number of applications, each of which becomes an offer independently with probability , the acceptance probability. The applicant takes the first offer, so the expected payoff is
maximized by the applicant best response
Employers receive a Poisson() number of applications. Each applicant is qualified with probability and still available with probability . An employer either screens sequentially until it hires (screening probability ) or exits. The employer best-response correspondence is
and the employer payoff is (5).
With (), the consistency conditions are
A solution is a mean-field steady state of the strategies . A mean-field equilibrium (MFE) is a pair with a steady state such that and (Definition 1). Equilibrium welfare is and .
There are unique with
the MFE is unique, and in it
The theorem is exact; it has no constants to improve.
Theorem 2 reduces equilibrium welfare on both sides to one scalar, , and splits markets into two regimes (Definition 2): application-limited (; all employers screen; applicants compete in a "tragedy of the commons") and screening-limited (; employers are indifferent and their welfare is zero, by (14) and (16)). All of the paper's later results, including the welfare bounds of Theorem 3, the effect of application limits (Theorems 4–5), application costs (Theorem 6) and wages (Theorem 7), are computed from these formulas.
Proposition 2, Theorem 1 and Theorem 2 are stated in the article but their proofs are in a technical report (Arnosti, Johari, Kanoria 2019, SSRN), not reproduced in the article and not used here. To our knowledge none of these results has a machine-checked proof. A formal development would give a self-contained, checked proof of the equilibrium characterization from the article's definitions alone.
The welfare identities (15)–(16) are algebra once and are known. The root statements are one-variable analysis. The hard part is the equilibrium itself. Proposition 2 is a fixed-point problem: substituting (7) into (6) gives an increasing map , and an increasing map can have several fixed points, so a monotonicity argument alone does not give uniqueness. Theorem 1 then has to handle the correspondence : an equilibrium may sit at the kink with an interior , and the case analysis has to show that exactly one of the regimes , applies and that it pins down .
All objects live in the namespace MatchCongestion.Welfare, over ℝ. The conventions are:
Params.Standing is Assumption 1 together with , , , , which the paper uses without listing them ("costs", a probability). Without , (14) has no root above .IsMFE instead asks for some steady state ; by Proposition 2 the two readings agree.Set ℝ.Real.log.Several formalizations would make the goal trivial or false, and none is used:
(1 - exp (-x)) / x in (6)–(7) would make a spurious second equilibrium;Classical.choose, or in Definition 1, would leave junk values unconstrained;Proposition 1 (the employer's sequential screening problem, specified only in an online appendix), the application-limit model (8)–(9) with Proposition 3, Theorems 3–7 and the finite-system limit theorems 8–10 are out of scope. Contributions of independent interest are a general lemma on unique roots of strictly convex or concave one-variable functions on an interval, and analytic facts about (positivity, strict monotonicity, on ).
A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading low-overhead family: the gross code of Bravyi et al. (Nature, 2024) stores 12 logical qubits at distance 12 using 144 data qubits, roughly a tenth of the overhead of a surface code with the same distance, and it is the basis of a published hardware roadmap. The search for higher-rate members of the family is active, and the claims made in it are claims about the exact distance of explicit finite codes. These are finite but very large computations, and they are rarely checked independently.
Timeline.
Fix positive integers and let . The monomial of the ring is identified with . A polynomial with coefficients in is identified with its support, the finite set of monomials with coefficient . The circulant of is the binary matrix with a in row , column exactly when .
Given two polynomials , the BB code acts on qubits, arranged in two blocks indexed by . Its check matrices are
where and also denote their circulants. Because is abelian, over , so this is a CSS code. Its parameters are:
The code is when . Each check of a code built from two three-term polynomials touches six qubits (weight 6). The Tanner graph joins each qubit to the X- and Z-checks acting on it, and the code is connected when this graph is connected.
each with (Table 9 of the source). Each new code is also a milestone on its own.
The result. The new codes encode 25% and 50% more logical qubits at distance 12 than the best weight-6 code reported by evolutionary search, with figures of merit of 8.57 and 9.60. The ladder distances turn published values, several of them previously supported only by heuristic searches or upper bounds, into exact statements. In particular settles an upper bound left open by Bravyi et al. The envelope statement is a negative result: within this family and size range, distance 12 is the ceiling at .
Formalizing it. In the source, each lower bound on a distance is a DRAT refutation or a replayable proof tree, checked by external programs. Only the pruning lemma (Lemma 1) has a machine-checked proof, in Lean 4. A complete formalization would make the code parameters kernel-checked facts about explicit Mathlib objects, independent of every external checker. Upper bounds on distance and the values of are finite linear-algebra facts. Lower bounds are exhaustive statements over -sized spaces and are the core of the work.
The upper bound needs one explicit weight-12 logical together with a proof that it lies outside the opposite row space. The lower bound asks that no nontrivial logical of weight at most 11 exist among roughly candidate supports. Direct enumeration is out of reach. A SAT encoding with a cardinality constraint is several orders of magnitude slower than the source's pruned search, and the resulting proof objects are large: hundreds of megabytes for the larger ladder codes. Kernel-checking such certificates, or finding structure that avoids them, is the central difficulty. Computing also requires an -rank of matrices with up to 180 rows and 360 columns, and Mathlib's Matrix.rank is not computable by decide. The envelope statement additionally quantifies over 971 group shapes and every pair of three-term polynomials on each.
All objects are in the definition file BBCode_Setting. is ZMod l × ZMod m, and a polynomial is a Finset of monomials, which makes it a set of distinct terms. The circulant has entry 1 at iff . Qubits are G ⊕ G (left and right blocks). is Matrix.fromCols (circulant A) (circulant B) and is Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ, over ZMod 2. The row space is the ZMod 2-span of the rows, and the weight counts nonzero coordinates. NumLogical A B k states additively, avoiding truncated subtraction. HasZDistance A B d requires both a nontrivial Z-logical of weight exactly and the lower bound for every nontrivial Z-logical, so a code without logicals cannot satisfy it vacuously. IsCode A B n k d bundles , and both distances.
The envelope quantifies over all with . The source enumerates 961 shapes; the 10 it omits () cannot have , so the two ranges are equivalent.
Reusable infrastructure includes computable rank certificates (explicit row-echelon or basis witnesses), a verified checker for DRAT or proof-tree certificates, and symmetry lemmas for group translations acting on BB codes. Contributions of any of these, of individual sectors ( or separately), or of upper and lower bounds as separate lemmas are welcome.
Finite sums provide a concrete setting for practicing precise mathematical statements. The sum of cubes identity relates two quantities that can be computed independently: adding the cubes of consecutive positive integers, and squaring the sum of those integers. This practice mission asks for a formal treatment of that known result, together with two supporting identities. Its purpose is to make the definitions, quantifiers, and endpoints explicit enough that each statement can be checked against the supplied mathematical source.
The material is suitable for practicing finite sums and elementary arithmetic in Lean. No research novelty is claimed. The classification is Textbook because the target is a known result; the source for this particular exercise is the statement supplied by the requester, rather than a named textbook chapter or research paper.
Let be a natural number, with natural numbers understood to include zero. Define two natural-valued functions:
Both sums run over the positive integers from through , including the upper endpoint. An empty sum has value zero, so both functions take the value zero at . These are actual finite sums, rather than formulas chosen to make a later theorem hold by definition.
For example, at , the first function has value , and the second has value . At , their values are and . These computations clarify the indexing convention. They are examples of the definitions, and the theorem statements below quantify over every natural number without an upper bound.
For every natural number ,
This statement relates the finite sum of consecutive positive integers to a product. It is stated with a factor of two, exactly as supplied, so its formula involves only addition and multiplication of natural numbers.
For every natural number ,
This statement specifies how the square of the triangular sum changes between consecutive inputs. The term added is the cube of the new endpoint, and the square on the right applies to the entire preceding sum.
For every natural number ,
This is the main goal. The two earlier targets are supporting milestones, and the two functions are shared definitions. Each theorem is stated without assuming another target as a hypothesis.
The result identifies the sum of the first positive cubes as a perfect square and specifies the natural number whose square it is. Together with the first milestone, it connects the same sum with the product . The second milestone records a separate arithmetic identity about consecutive values of the triangular sum, so it remains meaningful as an independently stated result.
The formalization work is to represent the two sums consistently and prove these three universal statements in Lean. The declarations in this proposal are proof targets, with theorem bodies left as placeholders. The proposal does not claim that those placeholders are completed proofs or that server verification has taken place. The shared definitions can be reused in later exercises about sums of positive integers or their powers.
The mathematical content is elementary. The main precision issue is keeping the summation endpoints and arithmetic expressions aligned across the definitions and the three targets. A sum ending at represents a different function; a square applied term by term represents a different quantity. Checking a few concrete inputs can expose transcription errors, but cannot establish a statement that quantifies over all natural numbers.
The zero input also requires consistent treatment. It is part of the domain of every declaration, even though the integers being summed are positive. At that input the definitions are empty sums, and the successor expression in the second milestone refers to the input one. No positivity assumption on is included or needed in the statements.
The Lean representation uses natural numbers for inputs, summation indices, and outputs. Each sum is taken over the finite inclusive interval Finset.Icc 1 n. Arithmetic and powers remain in the natural numbers. The statements use no division, subtraction, infinite sums, or coercions into the integers or real numbers.
The declarations share the namespace SumOfCubesPractice. Each definition is kept in its own module, and theorem files import the definitions they use. The required library infrastructure consists of finite sums and finite intervals of natural numbers. The scope consists of two definitions, two supporting milestone theorems, and one main theorem. Completed proofs of those exact statements are the intended mathematical contributions; no extra hypotheses, bounded ranges, or replacement definitions are part of the scope.
Source: the requester's supplied statement, definitions, Milestone 1, Milestone 2, and Final goal for “Sum of Cubes Identity (Practice).” No book, paper, author, page number, or external mathematical citation was supplied, and none is attributed to this exercise.
A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much can a low-degree decision rule vary across the edges of the Boolean cube?
The result collected here is a uniform bound with an explicit coefficient. The OpenAI weighted-grading development supplies a complete coefficient-eight construction. Lagdive, Aglave and Damre sharpen its probability estimate and obtain the sufficient coefficient 3.83. The present fixed-source development formalizes the refined estimate, extracts the coefficient 3.762, and connects it to the full polynomial-threshold statement.
This mission organizes that completed result and its reusable supporting theorems. Its goal and both milestones already have accepted Lean proofs. It does not present the coefficient as optimal, and it makes no claim of exhaustive historical priority.
Let be positive integers, and let be a real polynomial in variables with total degree at most . Choose an input uniformly from the sign cube . For a coordinate , write for the same input with coordinate negated. The threshold convention is
In particular, a zero of the polynomial is assigned the positive sign. The average sensitivity is
For the scalar supporting statements, let have the symmetric binomial distribution with parameters and . Its mean absolute deviation is
The accompanying definition module fixes this finite sum and the normalized central coefficient . These definitions contain no estimates or unproved hypotheses.
For every and every real polynomial of total degree at most , prove
The goal is the published theorem AverageSensitivity.polynomial_bound_3762_general. It has no multilinearity hypothesis and no requirement that . The narrower range used by the Big O board is therefore included. The goal's fixed coefficient records this particular verified result; a future sharper coefficient would be a separate statement.
Let a finite set carry nonnegative probability weights , and let real functions have identical weighted distributions. Let be any real centre and let . If on the support of the weights, prove
This is the finite form of the first estimate in Lemma 2 of Lagdive, Aglave and Damre. The centre is arbitrary; independence, exchangeability and a two-sided displacement bound are not hypotheses. Its published formalization is already proved.
For positive integers and a real number , prove the scalar implication
This is AverageSensitivity.extract_constant. Its statement is independent of the polynomial and matrix constructions. It records the coefficient extraction proved in this development, rather than attributing 3.762 to the earlier paper.
The result gives one coefficient that works simultaneously for every positive dimension and degree. Such uniformity distinguishes it from estimates that hold only for a fixed degree or only as the dimension tends to infinity. It also preserves the stated convention at polynomial zeros, so the class of threshold functions is unchanged at the boundary.
The formal contribution is a complete connection from the polynomial and the actual finite cube to the numerical bound. The final theorem does not assume the existence of a grading, an energy bound, a coupling estimate or a small-dimension certificate. Those mathematical components are discharged inside the proof chain. The two supporting milestones are independently importable results, and the live dependency graph records both as actual prerequisites of the goal's accepted reduction.
All three theorem nodes are currently Proved. The closed repository proof was rebuilt with Lean 4.33.1 and the platform's Mathlib revision, and an independent Linux build also passed. The final theorem's axiom dependencies are exactly propext, Classical.choice and Quot.sound. These checks establish the formal result under the displayed definitions; they do not establish optimality of the coefficient or independent human peer review.
A one-sided bound on the difference of two variables does not by itself bound the difference in the opposite direction. The equal-distribution condition is therefore essential to the coupling milestone. Omitting it would change the problem into a false assertion. In the polynomial application, the relevant distributions also have to come from the actual block masses of the constructed grading; treating those masses or the grading properties as free assumptions would omit the central analytic work.
The constant extraction must cover all admissible dimension-degree pairs. A calculation for finitely many dimensions cannot establish the universal statement, while an asymptotic first-moment estimate can leave uncontrolled small dimensions or degree-dependent errors. The formal target includes both the infinite range and every exceptional finite case. Numerical optimization and floating-point experiments are not premises of the accepted result.
Cube vertices are functions Fin n → Bool, interpreted coordinatewise as signs. A coordinate flip is an explicit function update, and each probability is a finite cardinality divided by . The polynomial is a Mathlib MvPolynomial (Fin n) ℝ; the degree bound refers to its total degree. General polynomial inputs are included through a proved value-preserving, degree-nonincreasing multilinearization. Positive dimensions ensure the normalizing denominator is nonzero. Degree zero and dimension zero are outside the displayed goal's quantifiers.
The two definition references provide the original cube/threshold interface and the exact scalar moment interface. The coupling milestone uses finite weighted sums, so equality of distributions is stated for every real test function without additional measurability assumptions. The scalar milestone quantifies over an arbitrary real satisfying its two explicit upper bounds. The main goal has no analogous auxiliary assumptions.
This is a Research Paper mission for a completed fixed-source development, with the main theorem and both milestones linked by their existing identities. It creates no duplicate theorem statements. Alternative proofs and subsequent sharper bounds can reuse these interfaces, but they are not claimed as completed by this mission. The construction and earlier probability refinement remain attributed to their original sources. Proof development and source preparation used OpenAI Codex.
0f539328-c783-4509-a78e-a86ac777468c.Extend the sharp diagonal Hlawka formula to smaller exponents.
The foundation mission establishes the least uniform complex coordinate Hlawka constant for every real exponent p ≥ 256. This entry proposes the cutoff 32: the same cyclic constant must be optimal for every real exponent at or above the proposed cutoff, across all finite complex coordinate dimensions and arbitrary triples, including unequal norms.
Use the foundation's unchanged definitions of the coordinate norm, Hlawka constant, and cyclic constant. The goal combines admissibility and uniform optimality in a single IsLeast statement.
Foundation: https://prove2.me/missions/Sharp_diagonal_Hlawka_constants%3A_foundation_and_proved_cutoff_256
When a decision rule is announced in advance, people may change the features on which the rule acts. A lender, for example, may offer loans with different probabilities to applicants with different reported characteristics. An applicant then weighs the greater chance of receiving a loan against the cost of changing those characteristics. The decision maker must account for this response when choosing the rule. Tsirtsis and coauthors study this problem with a finite feature set and a policy that specifies the probability of a positive decision at each value.
If moving to a better-outcome feature costs more and moving to a worse-outcome feature costs nothing, the paper shows that at least one optimal policy can be chosen to respect the ordering of outcomes. Section 5 asks what remains of that conclusion when change costs are general. Its three-value example answers the question sharply: an optimal policy exists, but no optimal policy respects outcome monotonicity. The example isolates the role played by the cost assumption in the earlier result. Source, §§4–5
There are feature values . An individual initially has value with probability . At feature value , the probability of a positive underlying outcome is . A decision policy assigns a positive-decision probability to each value. The decision maker incurs a cost for a positive decision. This is the paper's base model: the individual benefit is , and the outcome probability does not change when an individual changes features. Source, §2, p. 3, equations (1)–(3)
An individual at may move to , paying change cost . Their best response maximizes over all destinations. If several destinations tie, the paper selects one with the highest outcome probability . The resulting population distribution depends on . The decision maker's strategic utility is the expected outcome surplus under that response:
This sum is equation (7) regrouped by each individual's initial value. An optimal policy maximizes it over every policy in . The paper assumes a positive cost for moving to a distinct feature whose outcome is at least as good as the starting feature; its Section 5 matrix meets that assumption. Source, §3, pp. 4–5, equations (5) and (7)
The example has , , , and . Rows of the following matrix are starting features and columns are destinations:
Moving from to the lower-outcome costs . That violates the zero-cost requirement for such moves in the paper's outcome monotonic cost definition. A policy is called outcome monotonic here when a larger positive-decision probability implies a larger outcome probability: . Source, §§2, 4–5, pp. 3, 6, 9
For every admissible policy with , , and , the paper states that is optimal and that individuals initially at move to :
The endpoint matters: the move from to ties with staying in benefit less cost, and the paper's outcome tie rule chooses . Source, §5, p. 9
The principal target formalizes the Section 5 heading in this fixed instance:
The existence clause rules out an empty optimal set. This formulation follows the heading's assertion that an outcome-monotonic optimum may fail to exist, while the printed family supplies concrete optima. Source, §5, p. 9
The result gives an explicit boundary for the earlier outcome-monotonic-policy guarantee. With the Section 5 costs, favoring the lowest-outcome value as much as the highest-outcome value can be optimal, because the response to a published policy changes where population mass receives decisions. Thus a search restricted to outcome-monotonic policies can miss every optimum in a general-cost instance. The milestone on the printed family records a full interval of optimal policies, including its tie endpoint. Source, §§4–5, pp. 6, 9
The paper proves its example informally; this mission asks for a machine-checked account of the fixed instance and the universal quantifiers behind “every” and “no.” The development also yields reusable definitions for finite strategic policies, the outcome-aware best response, and utility. The other missions in this series treat the additive-cost theorem and a stochastic-optimum example separately. No theorem in this mission is presented as an open research problem.
Checking that one displayed policy has high utility is insufficient to establish optimality over every policy in . The best response changes at equality thresholds, so utility is piecewise defined and may jump when the tie rule changes the destination. The closed bound makes one such threshold part of the statement. A finite numerical grid misses both arbitrary real policies and the exact tie behavior. The negative goal also requires excluding outcome monotonicity for every maximizer, rather than exhibiting one nonmonotonic maximizer.
The features are Fin 3 in the example, with Lean indices representing . The general model uses Fin m with a nonempty finite feature set. Probabilities, costs, and utility are real numbers; the example's decimals are exact rational reals. Policies range over all real-valued functions with each coordinate in , and optimality uses IsMaxOn on precisely that set. The best response is constructed from the maximizers of and then the largest . If tied destinations also have equal , the least index is chosen; the example has distinct outcome probabilities, so this final convention never affects its claims.
Equation (1) prints strict outcome and policy comparisons as a biconditional, although the paper's later policy class permits equal policy values at distinct outcomes. This mission uses its one-way implication from a strict policy comparison to a strict outcome comparison. Failure of this weaker condition is a stronger counterexample than failure of the printed biconditional. The cost definition applies its printed pair and triple comparisons only to distinct values and records , as required for free staying. The example's constants satisfy the paper's standing positive-upward-cost assumption. These readings are disclosed so the formal claim has a consistent, nonvacuous model.
A complete proof needs finite argmax reasoning, exact rational inequalities, a case analysis over real policy regions, and the semantics of IsMaxOn. The finite best-response and utility definitions can be reused for other strategic-decision instances. Contributions may establish the printed family, its transport claim, bounds for all admissible policies, or the final exclusion of monotonic maximizers. Policies are never restricted to a grid, and the best response is computed from the model data rather than supplied as a free variable. The paper's algorithms, complexity claims, empirical studies, and changes to are outside this mission.
A component supplier may ask two downstream manufacturers to license their improvements to each other. Sharing raises each product's quality, but it can also reduce a manufacturer's reason to invest in its own improvement. The supplier must choose the licensing rule before those investments and before setting the wholesale price. Wang, Huang, and Lee study this choice in a two-manufacturer supply chain with unequal innovation costs. Their 2023 manuscript identifies cost regions in which the supplier gains from committing to cross-licensing and a region in which the choice depends on a further threshold. The question matters whenever a shared component provider controls a contract that changes both downstream competition and the incentive to improve products.
This mission targets Proposition 4 of the authors' SSRN manuscript, version of 2023-04-27. The appendix of that manuscript contains the proof and the explicit equilibrium formulas used here. The manuscript was later published in Manufacturing & Service Operations Management; the theorem and page labels in this mission belong to the held SSRN version.
There is one supplier and two manufacturers, and . Manufacturer invests at innovation level and pays the quadratic cost . Manufacturer 2 has the lower innovation cost: . If the manufacturers cross-license with effectiveness , the quality improvements of their products are and . Without cross-licensing the same model uses . The market-size intercept is normalized to one and unit production costs to zero, as in Section 3 of the manuscript.
After investment, the supplier selects a nonnegative wholesale price . The manufacturers then choose nonnegative Cournot quantities . Manufacturer 's selling price is , and its operating profit is . The supplier receives . A downstream duopoly has both quantities positive; at a downstream monopoly, only one manufacturer produces. The paper solves this sequence backward and distinguishes two equilibrium investment patterns within the duopoly: an interior outcome and a boundary outcome . Their dividing cost is . The paper's named innovation outcome is for and otherwise.
Write for the supplier's optimal wholesale revenue at that named innovation outcome. Thus is the same downstream model with no licensing. The choice to commit to cross-licensing is determined by comparing these two revenues.
Proposition 4 divides admissible into three regions. In the boundary region, licensing weakly benefits the supplier:
The threshold decreases as rises, and this boundary region eventually has no admissible . In the middle region there is a single threshold , fixed by and , below which the supplier weakly prefers licensing:
In the third region the direction of the threshold reverses. For a threshold fixed by and ,
When , throughout that last region. All three displays are restricted to . The full proposition is the mission goal. The milestone list records the paper's threshold monotonicity, the two explicit supplier-profit formulas, and the cost-region facts used to state the comparison.
The result makes the supplier's contract decision depend on both innovation asymmetry and the effectiveness of sharing. It separates the direct benefit of higher quality from the loss associated with weaker investment incentives. In particular, the supplier can benefit from cross-licensing when the superior manufacturer's cost is low enough for a boundary investment outcome, yet full effectiveness does not make licensing uniformly attractive. These conclusions are specific to the supplier's choice before investment; the paper's earlier ex post comparison holds the innovations fixed and addresses a different decision.
The mathematical result is already proved in the authors' appendix. The work here is to formalize its exact conditions and the optimization value being compared, then obtain a machine-checked proof. A development can reuse the Cournot quantity response, wholesale-price optimization, and piecewise investment formulas for the paper's later welfare and manufacturer-profit results. The local draft theorem statements compile in Lean; the results themselves remain open proof obligations.
The supplier's price can change which manufacturers remain active, and the manufacturers choose investments while anticipating that price response. A simple comparison of demand intercepts at fixed investments therefore does not decide the initial contract: the investments on the two sides of the comparison can differ, and a cost change can move one side across the boundary between the two equilibrium regimes. The paper expresses the outcomes with rational functions containing and analyzes three regions separated by and . A faithful formalization must also preserve the order of quantifiers: each single-crossing threshold is chosen once for fixed , before ranges over its region.
The Lean model uses real parameters and explicit pairs ordered as . It encodes the paper's displayed quantity formula for , with and . Its standing cost condition is . The wholesale-price domain makes explicit the economic domain implicit in the manuscript. The two displayed investment formulas use Real.sqrt 3; no decimal approximation enters a statement. The named innovation outcome follows page A.2: boundary below , interior otherwise. A separate mission targets its Nash-equilibrium characterization.
Most importantly, the supplier's optimal profit is the supremum of actual revenue over nonnegative prices at that innovation outcome. It is not defined to equal either closed form; a milestone asserts that the maximum is attained and identifies its value. This prevents the preference theorem from becoming a comparison true only by definition. The and thresholds are existential single-crossing statements because the latter's printed formula on page A.3 is malformed. The proof's weak profit comparisons determine the formal inequality. At , the statement uses interior profit on both sides, correcting an apparent slip in the final sentence of the proof.
Useful contributions include a proof of the attained supplier optimum, denominator positivity over the standing domain, exact inequalities involving , and the two single-crossing results. The general price-optimization facts and market-response lemmas can be reused beyond this mission.
Many consequential decisions, such as lending, hiring or admissions, are made by policies that map an individual's features to a probability of a positive decision. When the policy is published, individuals respond to it: they change their features, at a cost, to raise their chance of a positive decision. Tsirtsis, Tabibian, Khajehnejad, Singla, Schölkopf and Gomez-Rodriguez (arXiv:1905.09239, Management Science 2024) model this as a Stackelberg game and ask which policy maximizes the decision maker's utility once individuals best respond.
In the classical, non-strategic setting, where features do not react to the policy, the optimal policy is a deterministic threshold rule: decide positively exactly when the probability of a good outcome is at least a cost constant (Corbett-Davies et al., KDD 2017; Valera, Singla and Gomez-Rodriguez, NeurIPS 2018). The paper shows that strategic behaviour breaks this picture. A three-value example in §3 (p. 5) exhibits an instance whose costs satisfy the natural outcome monotonicity condition and whose optimal policy is nevertheless stochastic. This mission formalizes that example.
There are feature values , a feature distribution , an outcome probability , a constant , and a cost of changing from to .
with ties broken toward the feature value with the highest (standing assumption (ii)).
and a policy is optimal if it maximizes over all policies.
The instance of §3 has , , , and
row being the origin. In Lean the feature values are Fin 3 indices ; the model lives in the namespace StrategicPolicy.StochasticOpt, with Policies, br, u, uNS, OMCost, StandingI and the instance γ0, p0, q0, c0.
every optimal policy is non-deterministic, and . The paper prints a single optimal policy, ; the optimum is not unique, and the goal states the exact optimal set, which contains the printed policy and makes the "stochastic" claim a statement about every optimum.
The example separates two regimes. Without strategic behaviour the optimum is a deterministic threshold rule; with it, randomization is strictly necessary, even under the cost structure (outcome monotonicity) that the paper later uses to restrict the search for optimal policies to a structured family (Proposition 2, Theorem 3). It is the concrete witness for the paper's claim that "optimal decision policies are not always deterministic threshold rules", and it shows that the outcome monotonic binary policies of Theorem 3 must include fractional values such as .
The paper reports the optimum from "a brute force search", that is, numerically. A formal proof replaces the search by an argument valid over the whole continuum , determines the full optimal set rather than one optimizer, and certifies the tie-breaking at both thresholds. No part of this paper has a machine-checked proof that this mission is aware of.
The utility is piecewise linear in but discontinuous: it jumps whenever a best response switches, and the switching surfaces are exactly where the optimum sits. At the individuals at are indifferent between staying and moving to , and at those at are indifferent between staying and moving to . The optimum is attained only because tie-break (ii) resolves both indifferences upward. Checking finitely many candidate policies proves nothing about the rest of , and a naive concavity or first-order argument does not apply to a discontinuous objective. An upper bound must hold for every policy, across all configurations of best responses.
Fin 3 → ℝ with values in ; optimality is IsMaxOn u (Policies 3) π, over the whole cube, never over a grid or over deterministic policies.br is computed from , and as the maximizer of (5) with the highest outcome, then the least index; it is never a free function constrained by hypotheses. With the instance's distinct outcomes the least-index rule never fires.Needed infrastructure is small: finite sums over Fin 3, Finset.filter, Finset.min'. Lemmas evaluating br on regions of the policy cube are reusable across the series' examples.
A lender or other decision maker may publish a rule that assigns a positive decision to an individual with some probability. Once the rule is visible, individuals can change the features on which it acts. The decision maker must therefore evaluate a rule under the distribution it induces after individuals respond, rather than only under the original population. Tsirtsis and coauthors study this problem with finitely many feature values and a cost for changing from one value to another. Their preprint gives a utility model, a best response rule, and structural results for costs that respect the ordering of outcomes.
This mission isolates Theorem 3 of that preprint. It asks whether, under additive and outcome monotonic costs, an optimal decision rule can be found among policies with a particular binary choice at each relevant feature value. The result concerns the structure of an optimum. It does not assert that an arbitrary starting policy is itself binary or that every optimum has this form.
There are feature values , indexed from highest to lowest positive-outcome probability. Write for their original population masses and for their outcomes. The masses are nonnegative and sum to one, , and the outcomes are distinct in this mission. A policy chooses a positive decision at with probability . Each positive decision costs the decision maker .
An individual originally at can move to at change cost . In the paper's base model, the individual's benefit at a destination is , so she maximizes . Ties go to a destination with higher . If a tie remains, the formalization picks the smallest index. Write for this best response. The outcome probabilities themselves do not change after the response; the response changes where the population mass is counted. The decision maker's utility is
A policy is outcome monotonic here when implies . An outcome monotonic cost obeys the paper's two conditions for distinct feature values: improving outcome through successive values has the specified strict cost ordering, and a move to a lower outcome has zero cost. An additive cost satisfies when . Staying costs zero. The section's standing assumption also makes a distinct move toward a weakly higher outcome cost strictly positive.
If maximizes utility among all policies in , and the cost is additive and outcome monotonic, then some outcome monotonic policy has and satisfies
The paper calls this an outcome monotonic binary policy. Binary describes the two allowed relationships between adjacent policy values; the probabilities themselves can be fractional. The goal is conditional on a maximizer , exactly as Theorem 3 is stated. The preprint does not establish that an optimum always exists, and its best response tie thresholds make that question separate.
The first milestone records the observation following Proposition 2: under an outcome monotonic policy, an individual never selects a destination with lower outcome than the origin. Proposition 2 then states that some outcome monotonic policy attains the utility of an optimal policy under outcome monotonic costs. The final two milestones formalize the two individual policy changes stated in Appendix A.3, one when a policy value lies between its predecessor and the cost threshold, and one when it lies below that threshold.
Theorem 3 narrows a continuous search over policy probabilities to a structured family without losing the optimal value, provided an optimum exists. The restriction depends on how feature changes affect the induced population distribution. It is therefore a statement about decision making with strategic responses, not merely about sorting policy values by outcome. Proposition 2 is independently useful: under outcome monotonic costs, the optimal utility can be attained by an outcome monotonic policy even without additivity.
The result is proved in the cited preprint, while the proposed Lean declarations are open proof targets. A complete formalization would make the finite best response rule, the tie convention, and the cost assumptions explicit, then give checked proofs of the structural claims. The definitions of the policy space, response rule, and induced utility may also support later work on the same paper's stochastic examples and algorithms. No machine-checked proof of these proposed statements is claimed here.
The utility depends on a best response selected by an argmax, so changing one policy probability can switch the destination of several population groups at once. The utility need not vary continuously across tie thresholds. A naive coordinate adjustment that improves the outcome probability at one destination can alter who moves there and change the contribution from other origins. This is why a direct appeal to monotonicity of the displayed sum does not establish Proposition 2 or Theorem 3.
The Appendix A.3 statements identify two threshold regimes for a policy value. Their comparisons must account for the tie rule and for all origins whose selected destination changes. The mission keeps these comparisons as separate targets because the conclusion about the whole policy depends on them.
Lean represents the features by Fin m, with Lean index standing for . The model requires so that the best response has a value. The initial distribution and the conditional outcome probabilities are real valued, with explicit probability bounds. Policies range over the full cube . The best response is computed from the policy and cost, with the highest-outcome tie rule; it is not supplied as independent data. Optimality means membership in that cube and maximal utility over that cube.
The formalization records several readings needed to make the preprint's displays consistent. Formula (1) prints a strict biconditional, but formula (9) allows equal adjacent policy values, so policy monotonicity is the implication from a strictly larger policy value to a strictly larger outcome. The cost equivalences apply to distinct values; staying is free. Additivity applies along strictly improving outcome chains, since an all-triples equality would conflict with positive improvement cost. Outcomes are assumed distinct, as needed for this version of Theorem 3. These choices are stated on the definition item and checked against the source in the moderation notes.
The goal retains the optimal-policy hypothesis and every clause of the binary property. It cannot be satisfied by defining the best response arbitrarily, shrinking the policy set to a selected candidate, or asserting only that a binary policy exists. The model covers the paper's base case with unchanged . The algorithms, complexity claims, experiments, and the paper's other examples are outside this mission. Contributions on the best response interface, finite optimization lemmas, Proposition 2, and either Appendix comparison are welcome.
Firms can use information about individual customers to quote different prices. That ability changes their price competition, but it can also change where they locate their products or services in a market. For a firm deciding whether to invest in personalized pricing (PP), the order of those decisions matters: a positioning choice made after the investment can respond to a rival's new pricing capability. Li, Wang and Nault study this issue in a two-firm location game. In their August 3, 2021 manuscript, Section 6 reverses the timing of their basic model: firms decide whether to acquire PP before choosing positions. This mission concerns that Section 6 result, Proposition 5, rather than the similarly titled result as it may appear in the later Management Science article.
The question has a direct strategic interpretation. A technology can be useful in a pricing contest at fixed locations yet be unattractive when both firms can subsequently reposition. The mission asks for a precise equilibrium statement covering every nonnegative implementation cost, including the costless case. The three positioning subgames and the implementation payoff table are part of the target because they determine what an initial PP choice earns. The paper states these outcomes on pages 23–25 of the manuscript.
Consumers form a unit mass uniformly distributed on the interval . Each consumer buys one unit from one of two firms, A and B. Firm chooses a real position ; locations outside the consumer interval are allowed. A consumer at faces a quadratic misfit cost , where , in addition to the firm's price. The reservation value is assumed large enough for the whole market to buy. It therefore cancels from the gross profit expressions used here. These conventions come from Section 3.
A firm choosing PP can quote a price to each consumer according to that consumer's location. A firm choosing U quotes one uniform price. PP incurs a fixed cost . In the game studied here, the firms simultaneously decide between PP and U first, simultaneously choose real positions second, and compete in prices third. If exactly one firm has PP, the uniform-price firm posts its price before the PP firm sets its targeted prices. If both firms make the same PP choice, prices are set simultaneously. The cost is sunk by the positioning stage and is deducted only when stage-1 net payoffs are computed.
Write for the misfit advantage of firm over firm at equal prices. With PP at both firms, firm 's gross profit is the integral of over consumers. With one PP firm, the uniform-price leader chooses a price maximizing its price times the measure of consumers it serves; the targeted follower obtains the remaining gross profit. With two uniform prices, demand comes from consumers who prefer each firm's full price, with equal division at a tie. Positioning equilibria compare each firm's profit with moves to every real location, with the appropriate pricing continuation. The construction matches the pricing cases in Section 4 and Appendix A.
The benchmark with two uniform-price firms places A at and B at , with both prices equal to and gross profit for each. With PP at both firms, the positioning subgame places them at and , with gross profit each. When A alone has PP, it follows in the pricing stage and locates at , while B leads and locates at ; their respective gross profits are and . The reflected outcome applies when B alone has PP. These are the milestones from Sections 4 and 6.
Those outcomes give the stage-1 net payoff matrix, ordered as (A, B):
The main target is Proposition 5: for every and , both firms choose U in the equilibrium implementation game. The formal goal also states the pricing and positioning outcomes that generate this matrix, the existence of optimal uniform-leader prices in both asymmetric subgames, strict dominance of U, and uniqueness of the pure implementation equilibrium. The numerical constants belong to the source's specific quadratic-misfit model.
The theorem separates the value of a pricing capability at fixed positions from its value in a game where competitors can reposition. In the paper's short-run positioning game, adopting PP cannot improve either firm's equilibrium implementation payoff: U is strictly preferred against either choice of the rival. The conclusion holds even when acquiring PP costs nothing. It also explains why the observed no-PP outcome has the same positions, prices and profits as the uniform-pricing benchmark. The manuscript discusses this contrast immediately after Proposition 5.
The result is proved in the source, while the Lean statements in this proposal remain open proof obligations. A complete formalization would connect consumer-level demand, pricing optimality, positioning equilibria, the payoff matrix and the final Nash equilibrium within one model. The price and position predicates can be reused for other timing rules or cost assumptions built on the same Hotelling market. This mission does not claim to formalize the paper's later welfare comparisons or the costly-PP regimes under the original positioning-first timing.
The payoff matrix makes the final comparison short, but treating the matrix as a definition would hide the economic claim. Each cell must instead come from an equilibrium of the appropriate pricing and positioning subgame. Uniform-pricing demand changes when the indifferent consumer reaches an endpoint, and a firm can move across its rival; an argument using only interior demand formulas or ordered positions cannot establish the full position equilibrium. In the one-PP subgame, the targeting firm can make a reflected location move that ties its equilibrium payoff, so the position comparison must allow equality. A leader may also have several optimal prices at coincident locations, which makes the choice of an off-path pricing continuation material.
Lean uses real positions and prices, a two-element PP-choice type, Lebesgue measure for uniform consumer shares, and interval integrals for targeted gross profits. It assumes , , unit demand and full market coverage. PP cost appears only in net stage-1 payoffs. The reservation value is omitted because it cancels under full coverage. At a uniform-price tie, consumers are split equally; at a tie with a targeted follower, the follower serves the consumer. These rules make the demand functions defined even at coincident firm positions, although individual tie points have zero measure when positions differ.
The displayed closed-form prices require interior-demand conditions, stated explicitly on their milestone. Position deviations range over all of . The asymmetric positioning predicate requires an optimal pricing continuation after each deviation; this is a choice of continuation when the leader has multiple optima. It is recorded explicitly because the paper does not specify off-path tie selection. The goal's two asymmetric outcomes are mirror images under , as the source's “without loss of generality” convention requires.
Gross profits are defined from consumer shares and integrals; stage-1 payoffs evaluate those primitives at the source's subgame positions. The target cannot be satisfied by inserting Table 1's numbers as payoff definitions, by restricting position deviations to ordered pairs, or by assuming the desired equilibrium as a hypothesis. Contributions to measurable demand, interval integration, leader optimality, the uniform and PP position games, and the reflected asymmetric game are all within scope.
A component supplier can influence a product market through both the wholesale price it charges and the technology its customers may share. Wang, Huang and Lee study a supply chain with one upstream supplier and two downstream manufacturers that invest in product quality and then compete in quantities. A cross-licensing policy lets each manufacturer use some of the other's innovation. The supplier may promise a policy before the investments, or leave the decision until after the investments and wholesale price are fixed. The latter choice creates a precise comparison: at that final stage, does permitting cross-licensing reduce the supplier's revenue? The authors answer it in Proposition 1 of their SSRN manuscript, version of 2023-04-27. Its proof is in the attached appendix, p. A.1.
This mission concerns that final-stage comparison. It is one part of the paper's broader study of how a supplier's licensing commitment affects manufacturers' innovation incentives and downstream market structure. The later innovation and initial-contract comparisons are separate questions. Here, investments and wholesale price are fixed, so the result isolates the direct quantity-market effect of licensing at the moment the supplier chooses its policy.
Manufacturers and have already selected nonnegative innovation levels and , with in the presentation of equations (2) and (3). Each chooses a nonnegative production quantity . The wholesale price is the amount each manufacturer pays the common supplier for one unit. The market-size intercept is normalized to one and per-unit manufacturing cost to zero. If licensing effectiveness is , manufacturer receives a quality improvement ; represents no cross-licensing. Its inverse demand is . These are the model's conventions on pp. 9–10.
At fixed , the manufacturers play a simultaneous quantity game. Their respective profits are
A Nash equilibrium is a pair for which neither manufacturer increases its profit by changing its own nonnegative quantity while the other's quantity stays fixed. The supplier's profit at a quantity profile is . The supplier's comparison must therefore account for the manufacturers' responses under each licensing policy; it cannot compare profit at an arbitrary fixed quantity pair.
The first milestone gives the exact equilibrium quantities of equation (2). Write and . For both manufacturers can sell; for only sells; above neither sells. The statement characterizes every equilibrium and thereby gives existence and uniqueness across the two threshold boundaries, including the cases where a manufacturer's equilibrium quantity is zero.
The second milestone identifies the supplier's revenue at an equilibrium with the piecewise expression in equation (3). Setting in that expression gives the paper's no-licensing expression in equation (4). This milestone links the paper's algebraic profit comparison to the strategic quantity game, while keeping the equilibrium property as the premise.
The goal is the supplier's ex-post preference in Proposition 1. If is any equilibrium with licensing effectiveness and is any equilibrium at , then both equilibria exist and
This weak inequality is intentional. At the two games coincide, and there are other parameter values at which the profits tie. The comparison holds at the same innovation levels and the same wholesale price; it is not a comparison after re-optimizing the supplier's price or the manufacturers' investment decisions.
For fixed investments and price, the supplier need not lose revenue by enforcing cross-licensing after observing the manufacturers' innovation. This gives mathematical content to the paper's claim that, without an initial commitment, the supplier will choose to enforce licensing at the final contract stage. The model does not specify a separate final-contract bargaining game, so the formal goal is the profit comparison that supports that interpretation. The result does not settle whether committing to licensing before innovation is preferable: changing the initial policy can change the innovation levels themselves, which the ex-post comparison holds fixed.
The authors prove Proposition 1 by comparing the supplier-profit expressions (3) and (4) in the manuscript's appendix. A machine-checked development would additionally secure the connection from the manufacturers' Nash conditions to those expressions, including the monopoly and zero-sales regimes. These statements are currently posed as open formalization targets; a Lean file with sorry only checks that the statements are well formed, not that the paper's argument has been verified by Lean. The general two-player Nash definition can be reused for other real-strategy games; the payoff and threshold definitions are specific to this supply chain.
The quantity equilibrium changes form as the wholesale price crosses and . An argument confined to the two-selling-firms region misses cases in which sells nothing, or neither manufacturer sells. Comparing only the duopoly formulas cannot establish an inequality at every nonnegative price. The first milestone therefore covers all three regimes, and the goal compares the profits of actual equilibria. The fact that orders the possible monopoly toward under the paper's chosen labels; a formulation that silently assumes both equilibrium quantities are strictly positive would lose part of Proposition 1.
All parameters and quantities are real. The permitted quantity strategies and wholesale prices are nonnegative. The paper treats as a wholesale price without writing a bound in Proposition 1; is made explicit because a negative price can reverse the supplier-profit inequality. The innovation ordering is the convention immediately preceding equation (2). Licensing effectiveness lies in . Innovation costs and the paper's bound are unnecessary once innovation levels are fixed, so they do not enter this mission's statements.
The formalization uses an explicit pair , with the first coordinate for . The quantity-game equilibrium is defined by unilateral payoff comparisons over , and it is not defined by equation (2). Equation (2) is instead a theorem characterizing the equilibrium. The supplier's profit is defined as for any pair, independently of equation (3). These choices prevent the goal from becoming an inequality between two expressions whose connection to the game has merely been assumed. Equation (2)'s missing closing parenthesis in the manuscript is interpreted as the displayed first quantity divided by three. No division in the model's displayed formulas has a variable denominator.
Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time (the work already in the queue) and a price rate per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.
The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at depends on the value at . This mission formalizes the paper's existence theorem for that equation.
A model has a usage utility , a waiting cost , a Poisson arrival rate and a maximum service time , under Assumption 1 (p. 7):
At price a joining customer chooses the service time (5). They join when . Three thresholds follow:
The per-customer value is , with , for revenue and , for welfare (Lemma 1).
The optimality equations (12)–(15) ask for a constant (the average rate) and a relative value function with
Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess and grid cells on , it starts from for . It then builds a piecewise-linear cell by cell from right to left. On the cell ending at the slope is , where the slope adjustment is times the positive part of the inner maximum at . The shooting value is (23). Finally (24) and (Proposition 6).
The milestones follow the paper's proof in order:
Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off . Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.
The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.
The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. depends on on , so the equation must be integrated backwards from , and then the value is unknown. The shooting scheme fixes , integrates backwards, and tunes so that the boundary condition (13) at holds in the limit. For fixed the approximations need not converge as (the slope at can diverge), so and must be coupled through .
The hard step is Proposition 8. Each has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a -dependent price set to the limit.
All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:
Trivializations ruled out. The goal names the paper's and together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. and are not closed forms that would make (8) true by definition. The weaker statement "some solves (12)–(15)" is not the goal.
Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when .
Firms that collect data on individual consumers can price each one separately. This is personalized pricing (PP): targeted coupons, individualized offers, prices that depend on a customer's browsing or purchase history. Whether competing firms gain from this ability is a long-standing question in industrial organization. When firm positions are fixed, the classical answer is that they do not. Each firm adopts PP because it is individually rational, the targeted offers intensify price competition for every consumer, and both firms end up worse off: a prisoner's dilemma (Thisse and Vives 1988; Shaffer and Zhang 1995; Bester and Petrakis 1996; Choudhary et al. 2005).
Li, Wang and Nault ask what happens when firms also choose where to position their products, so that differentiation itself responds to the availability of PP. Their answer for the costless case is that PP makes things worse for the firms twice over. The firms still adopt it, and it also draws them towards the centre of the market, where competition is fiercest. This mission formalizes that result, Proposition 1 of their paper, together with the stage-3 and stage-2 analysis it rests on.
A unit mass of consumers is uniformly distributed on the interval . Each buys one unit. The reservation value is large enough that every consumer buys, so the market is covered. Two firms and choose positions ; positions outside are allowed. A consumer at who buys from firm pays the price plus a misfit cost , where measures taste heterogeneity. The misfit advantage of firm over firm at is
the amount by which the consumer at prefers to at equal prices.
The game has three stages:
A firm without PP charges one uniform price; a firm with PP charges a price to each consumer . When both or neither firm has PP, prices are chosen simultaneously. When only one firm has PP, the uniform-price firm moves first and the targeting firm responds.
The three stage-3 outcomes are:
For every :
Here a position equilibrium means that no firm can raise its both-PP profit by moving to any point of . "Both firms implement PP" means PP is strictly dominant for each firm at these positions in the stage-2 game.
The result. In the uniform-pricing benchmark of the same paper the firms locate at and , outside the market, and earn each: excess differentiation softens price competition. Proposition 1 shows that costless PP reverses this. The firms move to the quartiles, differentiation falls from to , and each firm's profit falls to , a loss of 83.3%. The fixed-position prisoner's dilemma is therefore not the whole cost of PP: endogenous positioning adds a second, larger loss. The positions also minimize total misfit cost, so the result separates firm profits from social efficiency. The costly-PP analysis of the paper (its Propositions 2–4) and the short-run positioning variant (Proposition 5) take these subgame outcomes as their starting point.
Formalizing it. The paper's proofs are short computations, and several are only asserted ("solving firm A's profit maximization problem we obtain", "straightforward to analyze and is omitted"). The formalization makes explicit what the page leaves implicit: the ranges of positions on which each closed form holds, the uniqueness of the leader's optimum that makes the follower's profit well defined, and deviations across the rival in the position game. To our knowledge none of these results has been machine-checked.
Each stage-3 outcome is an optimization over a market share that is a clipped linear function of the price. The first-order conditions on the page describe only the interior branch. A complete argument has to rule out the corners: a price at which the firm serves everyone or no one, negative prices, and coincident firms where ties matter.
The position game is harder than calculus on the closed forms. Those formulas hold only for , while a deviation can take a firm anywhere on , including past its rival, where the firms' roles are swapped and different formulas apply. Uniqueness requires showing that every ordered pair outside the interior region leaves some firm with zero profit and a profitable move.
Both-PP profits are integrals of a positive part, so every evaluation involves a case split at the midpoint .
All objects live in the namespace PPDifferentiation.Costless and are defined from primitives in one Setting file. Profits are integrals ∫ x in (0:ℝ)..1, … or real prices times the Lebesgue measure of a consumer set intersected with . No stage-3 profit is defined by its closed form. Optimality is a predicate (IsLeaderOpt, IsPriceNE), never an sSup, and every statement quantifying over optima also asserts that one exists.
Committed conventions:
The page states Lemma 1 "for any firm locations ". The formalization poses each closed form on the range where it holds: for the both-PP profits, (and for the mirror) for one-sided PP, for uniform prices, and , for dominance. As in the paper's proof, the position game of Proposition 1 uses the both-PP profits as stage-1 payoffs at every position pair.
A formalization in which is defined as , or in which deviations are restricted to one side of the rival, would make the goal a statement about a polynomial and is ruled out.
Contributions welcome: interval-integral evaluations of the positive part of a linear function, the optimization of over , and the stage-1 deviation analysis. The first two are reusable in other Hotelling models.
The source is the authors' SSRN manuscript of August 3, 2021 (abstract 3881900). The published Management Science version may number or state results differently.
Households and small firms increasingly own distributed energy resources (DERs): rooftop solar, batteries, small generators. A household that owns a DER is a prosumer: it consumes electricity and can also sell its surplus. Whether prosumers should be allowed to sell into the wholesale market, directly or through an aggregator that pools many small units, is now a regulatory question: in the United States, FERC Order 2222 (2020) requires grid operators to open their markets to DER aggregators.
Gao, Alshehri and Birge (SSRN 3931052) study two questions about such aggregation. The first, the subject of a companion mission, is efficiency: does a profit-seeking aggregator distort the market outcome? The second, the subject of this mission, is market power. Conventional generators are few and large, and they can raise the market price by withholding supply. The paper asks whether letting prosumers sell back to the grid weakens that power, and shows in a stylized one-node model that it does: participation raises welfare, and the welfare lost to strategic generators is smaller with participation than without it.
The source is the authors' SSRN working paper (PDF of September 26, 2021). A revised version appeared in Manufacturing & Service Operations Management (2024, doi:10.1287/msom.2021.0539) and may number or state the results differently; every index here refers to the working paper.
The market has one node and no network constraints. There are finitely many prosumers and identical generators .
At a market price , a prosumer is a price taker: it maximizes over its feasible purchases. A price clears the market at total generator supply if the prosumers' optimal responses sum to .
Four welfare numbers are compared.
Assumption 5 collects the hypotheses: , , at least one prosumer with , and two clauses the paper states informally, made precise as H1 (the participation clearing price at zero supply, , lies below every ) and H2 (, the efficient supply is positive).
where every inequality involving a strategic welfare holds for every strategic outcome of the model concerned.
The result. Theorem 3 gives a policy argument in welfare terms. Opening the market to prosumer sales, directly or through an aggregator, never lowers welfare in this model, whether the generators behave competitively or strategically. More specifically, the deadweight loss caused by the generators' market power, , is smaller than its counterpart without participation. Prosumer sales make the residual demand that generators face more elastic, and the theorem quantifies the effect through the explicit gaps of Proposition 10. Together with the companion efficiency result (the profit-seeking aggregator is fully efficient), it supports allowing DER aggregation in wholesale markets.
Formalizing it. The result is proved in the paper, by explicit computation. To our knowledge none of it has been machine-checked. A formal development adds two things beyond confirming the algebra. First, it fixes the solution concept: welfares are optimal values, prices are market-clearing prices, and strategic outcomes are equilibria with unilateral deviations, not closed forms read off first-order conditions. Second, it makes explicit the facts the paper uses without stating them: the open constraint never binds, the no-participation outcome lies on one linear piece of a kinked inverse demand, and its active set is nonempty.
With participation, everything is affine: the inverse demand is linear and the Cournot outcome is the textbook one. The difficulty is the model without participation. There the inverse demand, obtained from prosumers who can only buy, is piecewise linear and convex, with a kink each time one more prosumer starts buying. The equilibrium is characterized by the fixed point (81) on an active set that depends on the equilibrium itself. Two obvious shortcuts fail. One cannot take the paper's sorted closed form (86) as the definition of , because it is only valid at an equilibrium. One cannot assume an equilibrium exists either: numerical computation finds parameters satisfying Assumption 5 for which the no-participation game has no symmetric pure equilibrium, and others for which it has several. So (46b), (46d) and (46e) have to hold for every strategic outcome, whichever active set it uses. Comparing the two models then needs the active-set identities (95) and (96d) at each such outcome.
All quantities are real. Prosumers are a Fintype index ι; generators are Fin N, and Assumption5 includes 1 ≤ N. u a b i z = a i * z ^ 2 + b i * z. The definitions are:
WT and WTN: the sSup of the welfare over the feasible sets of (49) and (69). Propositions 5 and 7 show that both suprema are attained.IsRespP and IsRespN: price-taking optimal responses, over the open set and over .ClearsP and ClearsN: market clearing.IsStratP and IsStratN: symmetric equilibria with unilateral deviations to any , against every clearing price at the deviation total.welS and welSN: the true welfare .Hypotheses added to or read into the paper:
No welfare, price or equilibrium is defined by its closed form. Defining by (51), the price by (58) or the equilibrium by (60) would make the milestones definitional and the goal an algebraic identity about unverified objects. For the same reason the strategic outcome quantifies over unilateral deviations, not over symmetric profiles.
A complete development needs only elementary real analysis: maximization of concave quadratics, finite sums, and a case analysis on the active set. The definitions of price-taking response, market clearing and symmetric quantity equilibrium against a clearing correspondence can be reused for other single-node market models. Proofs of any milestone are welcome, as are alternative arguments for (46b) and (46e) that avoid the closed forms.
Distributed energy resources (DERs) — rooftop solar, home batteries, electric vehicles — turn electricity consumers into prosumers who can both buy and sell power. Their individual capacities are far too small to bid in a wholesale electricity market directly, so regulators have opened these markets to DER aggregators, intermediaries that pool many small resources and trade on their behalf (FERC Order 2222, 2020). An aggregator is a monopolist toward the prosumers it serves, and a profit-seeking monopolist between a market and its suppliers ordinarily distorts quantities: with a single unit price, the aggregator buys less than the efficient amount, and social welfare falls (Alshehri, Ndrio, Bose, Başar 2019, 2020).
Gao, Alshehri and Birge ask whether this loss can be avoided without regulating the aggregator. Their answer is that it can, provided the aggregator uses two-part pricing: a participation fee plus a per-unit price. This mission formalizes that efficiency result.
A power network has a finite set of nodes and a finite set of transmission lines. The ISO chooses nodal net injections ; the DC approximation of the AC network gives a matrix and line capacities , and the network constraints are (5b): and .
A finite set of prosumers sits at the nodes. Prosumer owns a DER capacity and has a utility of consumption on , . Assumption 1: is increasing, strictly concave and continuous on , differentiable on , with as and as . A finite set of conventional generators sits at the nodes; generator produces at cost . Assumption 2: is increasing, strictly convex and continuous on its interval, differentiable inside, with at the lower end and at the upper end.
Benchmark (direct participation). Prosumer sells and buys directly in the market at the locational price; only the net sale matters. Writing , , for the nodal totals of sales, purchases and generation, the ISO solves the economic dispatch problem (9):
The wholesale prices are the optimal Lagrange multipliers of the nodal balance constraints (5a).
Unregulated aggregation. Each prosumer sells only to the aggregator , which offers her a fee and a unit price . At wholesale price she maximizes the payoff (10), if she sells and otherwise, over , (11). The aggregator earns (13) and chooses nonnegative offers anticipating the responses: a Stackelberg game (Definition 1). The ISO now dispatches and separately, solving (21): maximize subject to (5a), (5b) and (18) , , ; its wholesale prices are again the multipliers of (5a).
Under Assumptions 1–3 (Assumption 3: (9) is feasible), with the optimal solution of (9),
every optimal solution of (21) has , , , the split is optimal for (21), and a price vector is a multiplier of (5a) for (21) if and only if it is one for (9).
The result. Theorem 1 shows that the efficiency loss attributed to profit-seeking aggregators is a consequence of one-part pricing, not of aggregation itself. With two-part pricing the aggregator passes the locational marginal price through as its unit price and extracts its profit only through participation fees, so welfare, dispatch and locational prices are exactly those of direct participation. The paper builds on this to analyse a regulated aggregator (§4) and the interaction of prosumer participation with generators' market power (§5, the companion mission of this series).
Formalizing it. The result is proved on paper, in a short argument relying on unstated conventions; no machine-checked version exists. A formal proof must make precise what "optimal Lagrange multiplier" means for a nonsmooth-at-the-boundary concave program on a network, handle the indicator in the prosumer's payoff (10) and the ties it creates, and settle the edge cases (nonpositive locational prices, capacity below the efficient consumption level) that the printed statements pass over.
The welfare identity is the easy part: the objective (20) and the balance (5a) of (21) depend on only through , and the box (18) projects onto the box (6). The work lies elsewhere. Price equality requires an argument about saddle points of the Lagrangian on two different domains, not just optimal values. The prosumer's two-part problem (11) is discontinuous at because of the fee, so its optimal responses must be found by comparing branches, and the aggregator's optimality in Lemma 4 must hold against every nonnegative offer — including unit prices above the wholesale price — and every optimal response to it, not a selected one. The first-order conditions (2) and (4) require interior optima, which follow from the derivative limits in Assumptions 1–2 but only at positive prices.
Everything lives in the namespace DERAggregation.Unregulated, in one definition file Setting. Nodes, prosumers, generators and lines are finite types; the node of prosumer is loc i. All quantities are real. Optimality is "feasible and at least as good as every feasible point", never a supremum. A multiplier vector of (5a) is a saddle point of the partial Lagrangian: (5a) and (5b) are dualized (with and complementary slackness for ), the participant box is kept as the domain, and is free. Prices are never free variables and never defined by a closed form.
Assumptions 1–2 read "differentiable" as differentiable on the open interval and continuous on the closed one, since the derivative limits rule out differentiability at the endpoints; and are added. Theorem 1 names no assumptions; it is stated under Assumptions 1–3. Problem (21) determines only , so "the same " is stated as equality of plus optimality of the canonical split. The first-order conditions are stated at nodes with positive price, Lemma 3 adds and , and Lemma 4's second part adds the standing restriction ; each addition is disclosed in its item. Problem (21) is written in the separate variables and with the constraint exactly as printed: a formalization through would make Theorem 1 true by unfolding and is ruled out.
The source is the authors' SSRN working paper (abstract 3931052, PDF of September 26, 2021); the published version in Manufacturing & Service Operations Management (2024) may number or state results differently. Useful contributions include the one-dimensional lemmas (unique maximizers of strictly concave functions with derivative limits at the endpoints), which are reusable well beyond this mission, and a general saddle-point lemma for separable concave programs with linear coupling constraints.
Spectral clustering recovers group labels from a similarity matrix: compute its leading eigenvectors, embed each point as a row of the eigenvector matrix, and cluster the rows with k-means. It is a standard last step of convex-relaxation methods for clustering, which first estimate a clustering matrix (with when and belong to the same cluster) and then have to turn the estimate back into labels.
Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) estimate by a linear program on a thresholded Gaussian kernel and then round it this way (Algorithm 1, steps 3–4). Their Theorem 2 controls the error of the rounding step in terms of the error of the estimate. The argument follows Lei and Rinaldo (Ann. Statist. 43(1), 2015), who analysed spectral clustering for stochastic block models with a polynomial-time -approximate k-means step, combined with the Davis–Kahan theorem in the form of Yu, Wang and Samworth (Biometrika 102(2), 2015). The same pattern, "matrix estimation error ⇒ eigenvector error ⇒ misclassification count", recurs throughout the analysis of SDP and spectral methods for community detection and mixture models.
There are points and clusters. A fixed labelling gives clusters of sizes , and . The true clustering matrix is if and otherwise. Its scaled membership matrix is
The estimate is any symmetric matrix with entries in . Spectral rounding takes a matrix of orthonormal eigenvectors of for its largest eigenvalues (ties broken arbitrarily), and runs k-means on the rows of . A membership matrix is a -matrix with exactly one per row; a pair with is a -approximate k-means solution on the rows of if
Let be an optimal rotation, an orthogonal matrix minimising . With and the rows of and , the misclassified set of cluster is
Norms: (entrywise), .
For every , , and optimal as above and every ,
If , the k-means labels agree with up to one permutation of on every point outside .
Inequality (15) separates the analysis of the algorithm into an estimation part (how close is to in , Theorem 1 of the paper) and a purely deterministic rounding part. Any estimator of the clustering matrix with entries in — the Robust-LP, the SDP relaxations of Peng–Wei or Amini–Levina, a thresholded kernel — inherits a misclassification bound from its error through this one statement, with an explicit constant. The companion statement shows that the sets really are the misclassified points.
The result is proved on paper; none of it is formalized. Mathlib has the spectral theorem for Hermitian matrices but no eigenspace perturbation bound of Davis–Kahan type, and the platform has no k-means approximation lemma for membership matrices. A machine-checked Davis–Kahan theorem in Frobenius norm and a machine-checked Lei–Rinaldo lemma are reusable well beyond this paper: they are the two standard ingredients of every spectral clustering guarantee for block models and mixtures.
The k-means part is elementary but bookkeeping-heavy: the comparison point in the bound must be a feasible k-means solution, which is why the true embedding has to factor as a membership matrix times a centre matrix. The main obstacle is the Davis–Kahan step. The naive route through individual eigenvectors fails when eigenvalues of or of are repeated (here has eigenvalue with multiplicity whenever cluster sizes coincide), and only the subspace is stable; the bound must be stated up to an orthogonal matrix and proved for the whole eigenspace, with no ordering or separation assumption on the eigenvalues of .
Points are Fin n, clusters Fin r, matrices Matrix ι κ ℝ; the norms are explicit sums, not Mathlib's matrix norm instances. The labelling is fixed; membership matrices are encoded by assignments , and "" by " the cost of every assignment and every centre matrix". "Top- eigenvectors" is variational: orthonormal columns, eigenvector equations, and every Rayleigh quotient on the orthogonal complement at most each selected eigenvalue. is a finite minimum and requires .
Departures from the printed text, each disclosed in the item concerned:
The goal quantifies over every optimal rotation , not over some orthogonal matrix chosen afterwards (which could make empty), and over every top-eigenvector matrix and every approximate k-means solution; a formalization that fixes to good eigenvectors, compares only against the true labels, or drops the eigenvalue-dominance clause (allowing bottom eigenvectors) proves a different and partly false statement.
Contributions welcome: Davis–Kahan in Frobenius norm for symmetric real matrices (general included), the Lei–Rinaldo lemma in full, and the eigenstructure of block-constant matrices.
Clustering separates observations into groups whose members resemble one another. In kernel clustering, a matrix records a similarity score for each pair of observations, and an assignment seeks groups with high total within-group similarity. Real data can also contain outliers, observations that should not be assigned to any cluster. Srivastava, Sarkar, and Hanasusanto use a binary assignment program that permits those unassigned observations and then express the same exact problem through a matrix of pairwise co-memberships. The relationship is stated as Proposition 1 of their preprint. It is the algebraic starting point for the tractable relaxations introduced immediately after the proposition in §3.
The two exact programs have different variables. The assignment program describes each observation's cluster directly. The lifted program records whether each pair belongs to the same cluster. The latter representation makes positive semidefiniteness and rank explicit, and it is the one the paper relaxes to obtain its semidefinite program. A precise equivalence matters because a relaxation of the wrong feasible set would no longer be a relaxation of the stated assignment problem.
Let be the number of observations and the number of available clusters. A binary assignment matrix has one row per observation and one column per cluster. In formulation (3), each row sums to at most one. A row with one nonzero entry assigns its observation to that cluster; a zero row leaves the observation unassigned. Thus the same matrix represents both inliers and outliers. Cluster sizes need not be equal, and unused cluster columns are allowed.
The clustering matrix has one row and column per observation. Its entry is one when observations and share a cluster and zero otherwise, including when either observation has a zero assignment row. Formulation (4) asks instead for an matrix whose entries lie in , that is positive semidefinite, and whose rank is at most . The rank bound limits the number of distinct nonzero cluster directions. Positive semidefiniteness is a property of the full real matrix, including its symmetry; it is not merely a condition on its diagonal.
Let be the similarity matrix, a penalty parameter, and the all-ones matrix. The entrywise Frobenius inner product is . The programs maximize, respectively, over feasible and over feasible . Both have a feasible zero matrix, even at the boundary values and .
The goal is Proposition 1, stated with its factor and rotation. If is an optimal matrix for (4), there must exist and an orthogonal such that is feasible and optimal for (3), with
Here “feasible and optimal” includes the zero-one entry condition, the row-sum bound, and comparison with every feasible assignment matrix. The objective identity alone would say little: once the Gram factorization and orthogonality hold, it follows algebraically. The substantive result is the existence of an assignment-compatible rotation of a factor of every lifted optimum.
The milestone list follows the five claims in Appendix B of the preprint: lifting a feasible assignment to a feasible without changing its value; factoring a rank-bounded positive semidefinite through columns; classifying factor rows as zero or unit vectors; showing that distinct nonzero rows are orthogonal; and rotating those rows into assignment coordinates. These statements address both directions of the feasible-set correspondence used by Proposition 1.
The proposition says that the matrix constraints in (4) describe the same exact clustering choices as the assignment constraints in (3), up to a choice of orthogonal coordinates for the factor. A lifted optimum therefore represents an assignment optimum rather than merely a matrix with the same numerical objective. Conversely, an assignment can always be lifted to a matrix accepted by (4). The paper can then drop the binary or rank constraints to obtain relaxations while keeping a clear exact program as their reference point; see §3 of the preprint.
The proposition is proved in the source paper. This mission seeks a machine-checked proof of that known claim and reusable finite-matrix results about binary positive semidefinite Gram matrices. In particular, the factorization and row-structure milestones can be used beyond spectral clustering whenever a zero-one Gram matrix appears with a rank bound. The Lean declarations here are proposed statements; their sorry proofs remain for solvers to complete.
The forward implication is immediate once a valid assignment matrix is given: its Gram matrix is positive semidefinite and has rank at most the number of cluster columns. The reverse implication carries the mathematical work. Positive semidefiniteness and low rank alone produce a real factor, but the factor need not have zero-one entries. A generic factor rotation also need not yield one-hot rows. The zero-one condition on every Gram entry is what constrains the relative positions of the nonzero rows strongly enough to recover assignment directions. The result must work when several observations share a direction, when some rows vanish, and when fewer than clusters are occupied.
The formalization uses Mathlib matrices indexed by Fin N and Fin r over . Feasibility of (3) is entrywise membership in together with row sums at most one. Feasibility of (4) is entrywise membership in , Matrix.PosSemidef, and Matrix.rank ≤ r. The objectives use the explicit sum of entrywise products, so no operator norm or alternate matrix inner product enters the statement. Global optimality is defined by comparison against the corresponding whole feasible set. The factor has exactly columns, and the rotation belongs to the real orthogonal group of dimension .
The paper obtains from a Gaussian kernel and takes for the clustering application. Proposition 1 and Appendix B use only the displayed algebraic programs, so the formal statement permits arbitrary real and . No probability model, symmetry assumption on , positive dimension assumption, or nonempty-cluster condition is needed. The boundary cases and retain their literal meanings. The formalization cannot assume that a feasible is already block diagonal or is already a Gram matrix of a binary assignment; that is the conclusion being established.
Useful contributions include proofs of the five Appendix B milestones, a finite-dimensional factorization theorem with the prescribed number of columns, and the rotation theorem that handles repeated or zero rows. These pieces should share the stated definitions so that the eventual proof of Proposition 1 uses precisely formulations (3) and (4).
Recommender systems on online platforms are usually trained to maximize engagement: time spent, items consumed, sessions returned. The implicit justification is revealed preference: a user who consumes more must value the content more. Behavioural economics questions that inference when a person's choices are driven by two conflicting processes, a deliberate one that weighs long-run utility and an impulsive one that reacts to the item in front of it.
Kleinberg, Mullainathan and Raghavan (2023) build a minimal model of such a user and ask when engagement is a good proxy for utility. Their first characterization (Theorem 4.1, a separate mission) says that the engagement-maximizing content differs from the utility-maximizing content only through higher moreishness, or higher span with lower value. This mission formalizes the complementary positive result, Theorem 4.2: on a content manifold where no content is very moreish and all content has roughly equal value (a "salad"-like manifold), maximizing engagement loses only a small, explicitly bounded amount of user utility.
A content distribution is a triple in the parameter space
The user consumes items one at a time. System 2, the deliberate agent, collects utility with mean per item while it is still interested, and pays an outside option per step spent on the platform. After each item system 2 stays interested with probability , the span. System 1, the impulsive agent, is hooked by each item with probability , the moreishness, and then consumes the next item without consulting system 2. Define
System 2 visits the platform only if this is worthwhile, so its expected utility is equation (1),
and the session length is when the user does not visit () and otherwise has expectation , equation (2).
A platform chooses content from a content manifold , which the paper assumes contains a point with . The utility maximizer maximizes over (3). The engagement maximizer maximizes over the points of at which the user participates, (4). The proof uses and for , so that .
Suppose for every , and for every , for some . Then
A supporting statement, implicit in the proof, is that participation at a point of forces .
The theorem is the paper's sufficient condition for engagement optimization to be benign. It is quantitative: the utility loss is linear in the value spread , scaled by the engagement of the utility-optimal content, plus a term that vanishes as the moreishness bound goes to . The paper notes that the linear dependence on engagement is unavoidable, since a user can lose a constant utility per step when . Together with Theorem 4.1 it delimits when a platform that observes only engagement can safely optimize it, and it motivates the paper's §5, on how a platform might learn which kind of manifold it is on.
The result is proved in the paper, with a short proof. As far as is known, neither the model nor the theorem has been machine-checked. The formalization fixes the participation convention for , the feasibility of in the engagement problem, and the implicit hypotheses listed below, which the printed proof uses without stating.
The algebra is elementary once the denominators are known to be positive. The difficulty lies in the bookkeeping the printed proof leaves implicit. Inequality (5) is derived from "", but (4) only gives , and only once is shown feasible for (4), which needs , i.e. the standing assumption on . Multiplying (5) by needs , which follows from and . The bound on splits on the sign of , and uses (from ) and . Finally, must be identified with through participation at . Using in place of , or dropping the participation constraint from (4), changes the theorem.
The Lean development lives in the namespace EngagementOpt.Salad and imports the frozen shared model in EngagementOpt.Misalign. There, a content distribution is a structure Params with real fields p, q, v; InOmega ω states , , . The shared functions gS W, gT and this chunk's ES W, ET W, aCoef, bCoef are as above, with ET W ω = if gS W ω < 0 then 0 else gT ω. The shared maximizer predicates IsUtilityMaximizer W M ωS (membership and IsMaxOn (gS W) M ωS) and IsEngagementMaximizer W M ωT (membership, 0 ≤ gS W ωT, and IsMaxOn gT {ω ∈ M | 0 ≤ gS W ω} ωT) hold for every maximizer, so the theorem holds for any tie-breaking rule. Closedness of only guarantees that maximizers exist and is not assumed. The goal's hypotheses are: ; ; a point of with ; the two maximizer predicates; and on ; and on for a given .
Three of these are implicit in the paper and are disclosed: (§2.1 normalizes ); , without which condition 1 is vacuous on and the bound fails (Lean's would turn into a false statement); and the standing assumption of p. 16. Neither nor is assumed; both follow from the hypotheses. Inequality (5) is posed with rather than the printed , because only is available from (4). The hypotheses are satisfiable: with , , , , , the maximizers are and , and the bound reads .
Everything needed is in Mathlib (real arithmetic, max, |·|, IsMaxOn). Proofs of the milestones and the goal are welcome; the base model module is shared with the Theorem 4.1 mission of the same paper.
Treatments for rare diseases can require substantial research and development spending while reaching a small patient population. A public subsidy can cover part of the manufacturer's development cost, part of the patient's price, or both. Which recipient should receive the subsidy depends on how the manufacturer responds. A further design choice is whether the manufacturer is paid when a drug is sold or only when treatment succeeds. Olsder, Martagan, and Tang formulate these choices as a sequential game between the government, a manufacturer, and patients in their SSRN working paper, §§3–4. This mission concerns their results for the case in which the manufacturer sets the price.
The paper reports that a manufacturer subsidy alone is optimal under either payment scheme and that the relative prices under the two schemes change with the government budget. The price comparison is useful because a payment contract intended to protect patients can change the price set by the manufacturer. The mission uses the working paper dated 2019-11-13. Its page and equation numbers are those of that version, which precedes the published article.
The government first chooses two subsidy shares: covers the fraction of research cost and covers the fraction of the unit price paid on a patient's behalf. The manufacturer then chooses a nonnegative unit price and a positive target efficacy . Research cost is , with , so the manufacturer's effective cost is . The government has a budget . The market size is one, and patient valuations are uniform on ; these conventions are given in §3.1–§3.2.
In Setting (1A) the manufacturer receives the price for every sale. Its profit is . At price and efficacy , patient welfare is , while government spending is . These are the paper's equations (2), (3), and (5). In Setting (1B) payment occurs only if treatment succeeds. The corresponding expressions are , , and , from equations (7), (8), and (10) of the same source.
For each scheme, a manufacturer best response is a pair maximizing that scheme's profit over all , . A government policy is optimal when it has a best response at which spending does not exceed , and its patient welfare is at least the welfare of every feasible policy evaluated at every manufacturer best response. This expresses the government's leader role and the manufacturer's follower role in the game's sequence of events, rather than assigning the closed forms of §§4.1–4.2 to either player by definition.
Proposition 1 of the working paper, p. 12, gives the unique optimal policy under sales-based payment. The paragraph after (16) on p. 13 says the same policy is optimal under outcome-based payment:
The budget binds at this policy. In both settings the optimal patient welfare and the manufacturer's profit equal . These policy claims, the two best-response formulas, and the two welfare and spending reductions form the six milestones.
Corollary 1 on p. 13 compares the manufacturer's optimal price in the two payment schemes. If and denote prices at optimal policies and best responses, the goal is the three-way statement
The printed second clause uses and says “higher”; equality of the two prices at the threshold is a boundary slip. The formal target records equality separately and preserves the strict high-budget comparison.
The policy result identifies which subsidy reaches patients most effectively within this model: when the manufacturer sets the price, the government uses its entire budget on the manufacturer's development cost, regardless of whether payment is per sale or contingent on treatment success. The price result adds a distinct comparison. Equal optimal subsidies and equal patient welfare do not imply equal prices; the sign of the price difference depends on relative to . This distinction appears explicitly in the paper's discussion following Corollary 1, pp. 13–14.
The working paper proves these results mathematically. The mission's remaining work is to give machine-checked proofs for the game definitions, both best-response results, both welfare and spending reductions, the unique optimum, and the final price comparison. It does not assert that those proofs have already been formalized. The definitions of attained best response and government optimality can also support later analyses of different subsidy or payment rules.
The government cannot compare the two schemes by holding the manufacturer's choices fixed. The manufacturer optimizes both price and efficacy after observing the subsidy policy, and the two profit functions have different price terms. Even after determining each manufacturer's response, identical formulas for government welfare and spending do not themselves establish an attained and unique optimum on the continuous half-open policy region . The price comparison then concerns the actual best-response prices at that optimum, including the threshold where the two prices coincide. These dependencies explain why the reduced expressions alone cannot serve as the definition of the game.
Lean represents all parameters, policies, prices, efficacies, profit, welfare, and spending in . The policy predicate requires . Every theorem assumes ; the budget results also assume . These positivity conditions make the paper's denominators meaningful and state its implicit economic regime. Prices chosen by the manufacturer satisfy . Its efficacy choice satisfies and has no imposed upper bound of one: equations (3) and (8) maximize over , and in the high-budget part of Corollary 1 their optimizer can exceed one. This is a convention of the paper's algebraic model, even though efficacy is introduced as a probability.
The demand expressions used in the paper's equations are left unclipped. At the stated best responses, they lie in the relevant nonnegative range. Best responses are represented as sets of all maximizers, and the goal compares every response at every optimal policy. Government optimality requires a feasible best response and comparison with every feasible competing policy and response, so neither existence nor uniqueness is obtained from an empty set. In particular, the reduced welfare and budget formulas (13) and (16) are milestone conclusions, not definitions of government choice. Reusable contributions include real optimization arguments for joint price and efficacy maximization and for attained welfare maxima over subsidy policies.