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?
An online display impression often reaches an advertiser through a chain of ad exchanges and networks instead of through a direct sale. Each intermediary runs its own auction among its downstream bidders and decides what to report to the auction above it. Its profit depends on whether it wins upstream and on what it can charge downstream. Even when every local auction is a second-price auction, the sale becomes a sequential game in which agents choose mechanisms. Balseiro, Candogan and Gurkan study this game on a symmetric tree. They characterize a subgame perfect equilibrium in which every intermediary applies a projected virtual value to its highest downstream report (SSRN 2661459; journal version in Manufacturing & Service Operations Management, 2020, doi:10.1287/msom.2019.0854). The single-auctioneer case is Myerson's optimal auction (Myerson 1981). In it, a seller facing i.i.d. bidders with increasing virtual values sets the reserve at the zero of the virtual value.
The seller occupies tier of a symmetric -tree, intermediaries occupy tiers , and buyers are the leaves at tier . Every tier- node has downstream agents. Buyers' values are i.i.d. draws from a law on with lower support end , a continuous strictly positive density on its support, and a finite mean. Buyers report their values.
An intermediary's mechanism is a reserve and a nondecreasing reporting function . If its highest downstream report satisfies , it reports upstream. If it wins upstream, it allocates to that downstream agent. The seller runs a second-price auction with a reserve . A winning agent pays the minimum report that would still have won (Definition A.1). An intermediary's profit is what its winning child pays minus what it pays upstream.
For a law with cdf and density , the virtual value is and its inverse is . The projection point is . The projected virtual value equals below , equals from up to , and equals beyond. If has an atom at , these objects use the positive part (Definitions 3.1–3.2).
The anticipated reports are laws defined by recursion: and , the projected virtual value of the maximum of i.i.d. copies of (Definition 3.3). Assumption 3.1 asks that, for , has finite mean and its positive part has a continuous positive density and a strictly increasing virtual value.
form a subgame perfect equilibrium. Fix any tier and any history: arbitrary mechanisms in for tiers and any seller reserve. Then no tier- node gains by switching to any mechanism in . The seller gains nothing from any reserve instead of .
The theorem identifies optimal mechanisms at every tier from the distribution of the reports directly below that tier alone. It also gives the seller's reserve after the network has transformed the buyers' values. Every later result of the paper is stated at this equilibrium. Examples are the profit ratios along chains with generalized Pareto values, the effect of market size, and the comparison of network shapes. Without the characterization each of these would need its own strategic analysis.
The paper proves the result on paper; none of these statements has a machine-checked proof yet. Formalizing it means building a finite tree auction with threshold payments and laws of maximum reports. It also needs virtual values for laws on unbounded supports and with an atom at zero, and Myerson-type reserve optimality for such laws. The last two are standard tools of auction theory that are absent from Mathlib in this generality.
In a single second-price auction, truthful bidding is dominant and the reserve is the only choice. An intermediary is different. Its report changes its chance of winning upstream, while its reserve and reporting function change what it can charge downstream. So the local second-price argument does not settle its choice. In a tree, a deviation must also be evaluated after arbitrary upstream histories, including reporting functions that are flat on intervals or jump. There, ties and payment thresholds matter. The paper's closed payment formula (2) can disagree with the minimum report that actually wins under a fixed tie rule. With that formula, a deviation with a jump beats , so the theorem would be false. The anticipated reports also carry an atom at zero from tier on, so the one-stage lemma is needed in its atom version.
Laws are probability measures on ; is the pushforward of a product measure under . The density is the derivative of the cdf, read only at , where it also gives the virtual value of the positive part. The support of a positive part is the interval , and "" means . The general objects (virtual value, projection, regularity, reserve objectives) are a separate definition module, reusable beyond this mission.
The tree has buyers with a product law. A report below the reserve is no report, which is never allocated. Ties go to the lowest index, and a report equal to a reserve wins. Payments are minimum winning reports. Buyers report truthfully (Lemma 2.1(B)). The seller's reserves range over , and in Lemma 3.1 the competing bid is independent of the buyers. Strict increase of is an explicit hypothesis: Assumption 3.1 starts at tier , but and Lemma 3.1 need it at tier .
Expected profits are single integrals of realized profits. The equilibrium profit is nonnegative pointwise, so a non-integrable deviation never violates the inequality. Deviations range over all of , and histories over all upstream mechanisms and reserves, so the equilibrium cannot hold for want of competitors. With rate-one exponential values and one intermediary with one buyer, the intermediary earns . Proofs of any milestone, and the measure-theoretic groundwork (measurability of , laws of maxima, Myerson's reserve on unbounded supports), are welcome.
The Hospital Readmissions Reduction Program (HRRP), created by the US Affordable Care Act and run by the Centers for Medicare & Medicaid Services since 2012, cuts the Medicare payments of hospitals whose 30-day readmission rates exceed a benchmark computed from other hospitals. It is a form of yardstick competition in the sense of Shleifer (1985): a regulator that cannot observe a provider's costs pays it according to what comparable providers achieve. The penalty differs from Shleifer's scheme in three ways: it is scaled by a multiplier that grows as the benchmark readmission rate falls, it is capped, and no bonus is paid for beating the benchmark.
Arifoğlu, Ren and Tezcan (2021) build a game-theoretic model to separate the effect of each feature. Their Proposition 1 isolates the multiplier: with the cap and the no-bonus rule removed (the scheme they call HRRP-I), hospitals still choose readmission rates below the social optimum and treatment costs above it. Medical and policy researchers had argued informally that the multiplier distorts incentives; Proposition 1 is the paper's precise version of that argument.
There are identical hospitals. Patients arrive at each hospital at rate . Hospital chooses a readmission rate and a marginal treatment cost in the action box
and pays an investment cost to reach them. Each admitted patient is readmitted with probability , so the hospital treats patients per unit time at cost each.
Standing assumptions on (p. 10 of the paper): is twice differentiable, decreasing in each variable, and jointly convex; on ,
where subscripts denote partial derivatives.
The regulator's objective is the social welfare
where is a fixed total patient utility. A maximizer of over is the first best (Lemma 1 of the paper: it exists, is unique and is interior).
The regulator observes every hospital's cost, readmission rate and investment, and computes the yardsticks
Under HRRP-I hospital receives
and earns the profit . The factor multiplying the excess readmission rate is the multiplier. An equilibrium is a pure-strategy Nash equilibrium: a profile of actions in from which no hospital can raise its profit by changing its own action within . A symmetric equilibrium is an equilibrium in which every hospital plays the same action.
For every :
and for every equilibrium is symmetric.
The goal is the conjunction of milestones 2–4; Lemma 1 supplies the comparison point.
Proposition 1 is the paper's first main result and the base for its later analysis: the capped scheme HRRP-II and the actual HRRP (Propositions 2 and 3) are studied relative to the HRRP-I symmetric equilibrium, and the remedy the paper proposes (m-HRRP, Proposition 4) removes the multiplier precisely because Proposition 1 identifies it as a source of distortion. The ordering says that hospitals over-invest in readmission reduction; says that, as a consequence, they under-invest in reducing treatment costs.
The paper's proofs are in its online appendix, which is not part of the source this mission cites (the authors' accepted manuscript, LBS Research Online eprint 1402). No machine-checked proof of any statement of the paper is known. The mission produces a checked version of the model and of all three claims of Proposition 1; the two-hospital claim in particular has no published argument in the cited source.
Lemma 1 is the routine part. The ordering claim is harder: a symmetric equilibrium need not be interior (in simple examples ), so the first-order conditions of the hospital's problem hold only as variational inequalities on , and the comparison with must work from those inequalities and the curvature hypotheses alone. The existence claim needs a fixed-point theorem for the best-response map of a hospital facing yardsticks , and therefore continuity of the best response, which rests on strict concavity of the hospital's profit; Brouwer's theorem is not in Mathlib. The two-hospital claim is a uniqueness-type statement about a two-player game with non-separable payoffs; the obvious route through contraction of the best-response map does not follow from the stated assumptions without further estimates.
The Lean development lives in the namespace ReadmissionsHRRP.HRRPI. A Model carries lam (, a Lean keyword), V, the box bounds and the curried cost R r c. Partial derivatives are deriv of the sections of R. Profiles are maps Fin N → ℝ × ℝ (first coordinate , second ); the averages divide by the real number . The equilibrium notion is the published pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every hospital's feasible set equal to ; deviations keep the other hospitals' actions, so the yardsticks of the deviating hospital do not move.
The standing assumptions are one predicate, Model.Standing: the inequalities on the box bounds, (implicit in the paper), of class on an open set containing , non-increasing in each variable on , jointly convex on , and the two pointwise curvature conditions on . The paper's Appendix A, which imposes boundary conditions "to ensure that optimal actions are interior", is not in the cited manuscript; it is replaced by the separate hypothesis Model.FirstBestInterior, that every maximizer of over is interior. Every theorem assumes .
The first best is a maximizer of over , never a solution of the first-order conditions; the ordering claim quantifies over every such maximizer, and the existence claim is part of the goal so that the ordering claim is not vacuous. A sorry-free sanity file checks that the hypotheses are jointly satisfiable for , , .
Useful infrastructure: strict concavity on a box from a Hessian condition, variational inequalities at constrained maxima, continuity of argmax maps, and Brouwer's theorem on a planar box (proved on the platform as AGT.brouwer_fixed_point). Contributions to any of these, or to the hand proofs of the separate claims, are welcome.
The apparel industry produces far more garments than it sells. A large part of its environmental footprint comes from overproduction: inventory made against uncertain demand and then burned, landfilled or downcycled. Mass customization (MC), where a garment is made to order after the customer specifies it, is often promoted as a remedy. Under MC, supply matches demand exactly for the products it makes.
Alptekinoğlu and Örsdemir (MSOM, 2022; SSRN 3685235) ask whether this intuition survives once the firm's profit motive is taken into account. A firm that adopts MC does not abandon mass production (MP). It runs a hybrid system and re-optimizes its mass-produced line around the new option. The paper characterizes exactly when adopting MC is a win-win, meaning more profitable and better for the environment, and when the hybrid firm ends up overproducing more than the pure MP firm would.
Consumers' ideal products are spread uniformly on the Hotelling line . A consumer at distance from a mass-produced product priced gets utility . The total market size is random: with probability , otherwise, where , , and . Units cost , and offering variants costs .
The MP firm chooses the number of variants , the market share of each variant (which fixes the price ) and the stock of each variant before is known. Its expected profit is
The hybrid firm can also make any consumer's ideal product to order, at price , but the consumer then bears a waiting cost . It adds MC share , with , and earns an additional .
The environmental impact counts per sold unit (production, use, disposal) and per leftover unit (production, overproduction):
MC is made to order and leaves no leftovers.
The standing assumptions are , , and . Products are classified by the cost-adjusted value as high-value (), moderate-value () or low-value (). The paper's thresholds are closed-form functions of the parameters (Table 2 of the paper).
Adopting MC is a win-win if and only if
Here "win-win" means that both firms' problems have optimal decisions and that every optimal hybrid decision is strictly more profitable and has strictly lower expected impact than every optimal MP decision.
The result separates the two ways MC changes the footprint. It adds sales, because the gaps between mass-produced variants are now served, and each such sale carries the impact . It also reshapes the mass-produced line: the market served by MP shrinks, each variant captures a smaller share at a higher price, and stocking for the high market size can become profitable (§4.2, pp. 16–17). That raises overproduction even though the MC part produces none. Proposition 3 states exactly when the net effect, together with the profit gain, is a win-win. The paper's policy section (§6) builds on this characterization to study how promoting MC, a disposal fee for overproduction, and recycling move the win-win region.
The paper proves the result by hand, with case analyses across nine orderings of thresholds. No part of the model or its proofs has been machine-checked. A complete development gives a checked solution of a newsvendor-type stocking problem embedded in a Hotelling variety model, which is a common pattern in operations-management research.
Both optimization problems are non-concave. Profit is piecewise in (Lemma 1), and after substituting the optimal stock it is piecewise in , with a kink at and a corner at full coverage . The global optimum therefore switches between four solution types, and the switching thresholds include , a root of a non-polynomial equation. A comparison of first-order conditions alone does not settle which type is optimal. The goal compares two such case analyses, MP and hybrid, at once, so the threshold orderings ( versus , versus , versus ) have to be established across all three product-value classes.
Contributions are welcome on any milestone. The stocking lemmas and Lemma 2 are elementary. The root lemmas need monotonicity analysis of . Propositions 1 and 2 are the bulk of the work.
New brand-name drugs, in particular biologics, are expensive. Their benefit is also uncertain: a given patient cannot know in advance whether the treatment will work for her. Outcome-based pricing (also called performance-based or risk-sharing agreements) responds to this. The manufacturer is paid only when the treatment reaches a pre-specified goal and rebates the price otherwise. Agreements of this kind between manufacturers and payers have been signed for cholesterol, diabetes and oncology drugs. Carlson et al. (2010) give a taxonomy. Whether such a contract actually helps the parties that must agree to it is a question about incentives. It cannot be settled by noting that the patient bears less risk.
E. Adida (Management Science, 2021; accepted manuscript at eScholarship) studies it in a three-stage game between a monopolist firm, a payer and risk-sensitive patients. The patients follow prospect theory (Kahneman and Tversky 1979; Tversky and Kahneman 1992). The paper's headline result is that, in the region where the payer covers the drug under both systems, the firm and the payer typically disagree about outcome-based pricing. A side payment from the firm to the payer can make both strictly better off, but only for high-risk drugs. This mission formalizes that result and the chain of equilibrium computations that leads to it.
There are patients with values , , a unit cost , a co-insurance rate and a success probability . On success the payer gains a fixed surplus . The game has three stages.
Under uniform pricing the price is paid on every purchase, and the buyer's welfare is . Under outcome-based pricing it is paid only on success, and the welfare is . Demand is times the measure of buyers in . The firm earns per buyer under uniform pricing and under outcome-based pricing. The payer's objective is its own expected payoff plus the patients' total expected (risk-neutral) payoff. It covers iff its objective with coverage is at least its objective without. An equilibrium price maximizes the firm's realized profit, with the payer's coverage response, over all .
Let
A drug is high-risk if and low-risk if ; the risk premium is positive exactly for high-risk drugs. Assumption 1 is . Assumption 2 is
with , , and the solution of . It is the region of large payer benefit, in which both systems end in coverage. Finally,
Under Assumptions 1 and 2, let and be equilibrium prices, and write and . Then
and, if and , : every transfer strictly between the two amounts, which runs from the firm to the payer, works.
In attack order:
Proposition 4 says that for a high-risk drug outcome-based pricing raises total firm-plus-payer surplus, even where it hurts the payer. A negotiated side payment therefore always exists that makes both parties prefer it. For a low-risk drug no such payment exists, because the payer's gain is smaller than the firm's loss. The result locates where outcome-based contracts can be self-enforcing and identifies the risk premium as the quantity that decides it. In this model the patients' loss aversion and risk sensitivity act on the comparison only through and .
The paper proves the result with explicit algebra once the equilibrium is pinned down. The formalization adds two things. First, the equilibrium layer is checked, not assumed: the statements quantify over the backward-induction equilibrium prices, with an explicit payer coverage rule and an integral model of demand. The closed forms and the unique optima , become theorems. Second, the formalization makes the small hypotheses explicit (positivity of , non-negativity of , strict versus weak improvement), which the published proof uses without listing. As far as is known, none of these results has a machine-checked proof.
The algebra of Propositions 3 and 4 is short once and with coverage are established. The work is in establishing them. The firm's realized profit is a discontinuous function of the price, because the payer's coverage decision switches at the thresholds , , , , which depend on the regime of . Showing that is the unique global maximizer requires comparing the covered and uncovered profit curves on every piece. It uses Assumption 1, the bound (which places above and above ), and the monotonicity of through the root of . Reading the closed forms off the paper's formulas is not enough: they must be derived from the purchase rule, which itself rests on the prospect-theory inequality . A natural shortcut is to state Proposition 4 at and directly. That deletes the equilibrium content and is not the goal.
All quantities are real numbers in one structure Params with a Standing predicate: , , , , , . Two of these are added to the page's assumptions: ( divides by ) and (used in the proof of Theorem 1).
Powers are Real.rpow on non-negative bases only. The roots (of ), (of ) and (of ) are passed as numbers together with their defining equation on ; uniqueness is a milestone. Demand and patient payoff are a Lebesgue measure and a set integral over the buyers in . Ties follow the paper: an indifferent patient buys, and an indifferent payer covers. "The firm prices at " is read as " is the unique equilibrium price". "Better for both parties" is read as strict improvement, and the paper's closed range of transfers is replaced by the open range, because at its endpoints one party is only indifferent. The payer's side of every comparison is its objective .
A formalization that fixes and by hypothesis, or takes the closed forms as definitions, would make the goal an algebraic identity. The goal here quantifies over all equilibrium prices of the integral model.
A complete development needs elementary real analysis (convexity and monotonicity of , rpow manipulations), Lebesgue measure and integrals over intervals, and piecewise maximization of concave quadratics. The prospect-theory value function and the threshold purchase rule are reusable for other behavioral pricing models. Proofs of any milestone are welcome, as are proofs of the omitted parts of Theorems 1 and 2 (the constrained prices , , , ).
The circular economy movement argues that manufacturers should keep control of their products after use (by leasing instead of selling) and design them so that worn parts can be replaced individually (a modular architecture). Each of the two levers has a long literature in operations management and economics. Leasing versus selling durable goods is studied in models of durable goods with secondary markets (Desai & Purohit 1998; Agrawal, Ferguson, Toktay & Thomas 2012), and modularity in the product-design literature, where its value lies in replacing modules independently. Agrawal, Atasu and Ülkü (Management Science) ask whether the two levers reinforce each other: when is leasing a modular product strictly the most profitable of the four combinations of business model and architecture? Their answer (Proposition 3) is a closed-form partition of the parameter space by cost thresholds, and it shows that the combination is optimal only under limited conditions.
A monopolist offers a durable product made of two modules, each with a useful life of two periods; module 1 is the more durable one. A customer of type , uniform on , values a new product at per period. Under selling, a used module retains a fraction of its value; under leasing, off-lease modules retain , where is the relative return condition (: off-lease products are in worse shape than previously sold ones; : in better shape). Each module costs to produce. The standing assumptions are
In steady state the firm solves one of four quadratic problems, each written in quantities through inverse demand functions derived from customer self-selection and secondary-market clearing:
The optimal profits are the attained maxima of these problems. The paper's thresholds are explicit functions of :
together with , , and the square-root expressions , of the Appendix.
With ties between architectures broken towards the integral one (footnote 13 of the paper):
In each region the chosen option's optimal profit strictly exceeds the others, except at exact ties of the model. These are for , for , , and at further ties between leasing and selling. The goal states these as equalities or weak inequalities and restores strictness for .
The result gives a complete description of the firm's joint choice in a standard durable-goods model with a secondary market, and it qualifies a common claim. Leasing a modular product is strictly optimal only at low production cost. For modularity can even push a leasing firm to selling (Proposition 2), and for the firm never sells. The thresholds feed the paper's later environmental and consumer-surplus comparisons.
The paper's proofs are pencil-and-paper KKT computations reported in compressed form, and nothing in the paper is machine-checked. A formalization would certify the four closed-form optima, every threshold comparison, and the case split of Proposition 3. It would also settle two printing errors found while preparing this mission (see below), one of which changes the statement of Lemma 2 and Proposition 3.
Each firm problem is a strictly concave quadratic program over a polyhedral cone, so existence of the optimum is routine. The difficulty is everything after that. The optimum changes face as moves: LM alone has four KKT cases, and each must be shown to be optimal exactly on its cost interval. The profit comparisons then reduce to sign conditions on rational functions of four parameters. Some involve the square roots in and , which are only meaningful for and are defined as roots of quadratics in , so the comparisons must be placed relative to them. The ordering is an inequality between such expressions on the whole parameter region. It is not a symbolic identity, and checking it at sample points proves nothing.
IsGreatest (profit '' feasible) v, never a supremum without attainment. Statements about the optimizer ("the UN segment exists", "") quantify over every optimal decision.Real.sqrt for , , , . and are used only for , where their radicands are nonnegative.Online platforms show a reader many short signals about the same question (posts, headlines, tweets), more than the reader can absorb. The reader screens the menu and consumes only a few items. Allon, Drakopoulos and Manshadi (Information Inundation on Platforms and Implications, SSRN 3385627; Operations Research, 2021, doi:10.1287/opre.2021.2119) ask what a purely information-seeking reader picks when the accuracy of each post is unknown. Their answer, Proposition 1, is that she picks the post closest to her current belief, the effect the paper calls screening bias. It is the mechanism behind the paper's later results on slow learning and polarization, and it explains a pattern resembling confirmation bias without assuming any bias in how beliefs are updated. Confirmation bias was documented empirically by Lord, Ross and Lepper (1979) and modelled through source reputation by Gentzkow and Shapiro (2006) and Suen (2004). In those models the bias comes from repeated interaction with strategic sources; here it comes from a single screening decision by a Bayesian reader.
An unknown fact is a real number . A post is a noisy observation
where and the accuracy (a standard deviation) is drawn independently from a publicly known law . The paper assumes throughout (§3, p. 8) that is a probability law whose support lies in an interval with .
A consumer holds a normal belief about , with . From her point of view, a post of accuracy is distributed , so its likelihood is
By Bayes rule (4), her posterior on the accuracy after seeing the post value has density proportional to with respect to ; write for the posterior expectation.
If she reads a post and learns its accuracy (ex-post known accuracy), her belief becomes normal with standard deviation (Belief Updating Equations). Before reading, she scores each post by the expected reduction of her uncertainty. The Screening Equation prints the score as
while the text calls it the expected decrease in posterior variance, . A menu is a finite list of post values, and she picks a post in the argmax of the score.
In Lean the model lives in InfoInundation.Screening.Model: AccuracyLaw G (the standing assumption), psi, likelihood, postExp (the Bayes ratio), nextSd, sdScore, varScore, argmaxMenu, closestPosts, and the auxiliary moments auxMoment/auxExp used in the proof.
For every accuracy law satisfying the standing assumption, every belief with and every menu :
(a) if is not a point mass,
(b) if with , the argmax of both scores is the whole menu.
The proof on pp. 10–11 has no numbered lemmas; the milestones are its labelled steps:
Proposition 1 turns a modelling choice (each reader maximizes expected information) into a behavioural prediction (each reader consumes the post nearest her belief). Every later result of the paper is built on it: the slow-learning theorem, in which the speed of learning decreases with menu size, and the multimodal belief distribution, both come from feeding the closest post back into the belief dynamics. Part (b) is the benchmark: with known equal accuracy there is no screening bias, and learning is fast.
The result is proved in the paper; it has no machine-checked proof. The mission produces one, and with it a small reusable library on posteriors over a Gaussian scale mixture: the predictive density of a normal belief under a known noise scale (milestone 1), a measure-theoretic Bayes rule for the noise scale given one observation (milestone 2), and moment inequalities under exponentially tilted mixing laws (milestones 5–6). The formalization also settles two points that the printed proof leaves open (see Difficulty): which of the two scores the conclusion holds for, and why the conclusion is an equality of sets rather than an inclusion.
The proof covers the variance score. Reducing it to the monotonicity of in is algebra. The monotonicity itself requires differentiating a ratio of -integrals under the integral sign, for an arbitrary law , which in turn needs the boundedness of the support to dominate the integrands.
Three places need more than the printed argument:
Measure ℝ with AccuracyLaw G: a probability measure with for some . "Supp() includes at least two distinct values" is ∀ σ, G ≠ Measure.dirac σ; "Supp() = {σ}" is G = Measure.dirac σ with .Z : Fin K → ℝ; argmax and argmin are Finset (Fin K), so posts of equal value are distinct posts, and "" is Finset.univ.Needed infrastructure: dominated differentiation of parameter-dependent integrals against a finite measure on a bounded set (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le), the equality case of Cauchy–Schwarz in , Gaussian convolution (gaussianReal_add_gaussianReal_of_indepFun) and conditional expectation via densities for milestone 2. Contributions of a covariance or likelihood-ratio ordering lemma for the standard-deviation conjunct are welcome as supporting theorems.
A new venture rarely knows two things at once: whether its core idea is worth anything, and whether the particular way it has chosen to bring the idea to market — its strategy — will work. A failed pilot, a disappointing A/B test or a lukewarm customer experiment can mean either, and the founder cannot tell which. Work on entrepreneurial experimentation (Kerr, Nanda and Rhodes-Kropf, Journal of Economic Perspectives, 2014, doi:10.1257/jep.28.3.25; Gans, Stern and Wu, Strategic Management Journal, 2019, doi:10.1002/smj.3010) treats testing as the main tool founders have to resolve uncertainty before they commit resources.
Agrawal, Gans and Stern (NBER Working Paper 27379, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3920) give a two-period model in which a single test produces a conflated signal about the idea and the strategy together. Two consequences come out of it. A signal that the strategy is good can still lead the entrepreneur to abandon the venture. And when a mentor can sharpen a test, the better direction to sharpen it depends on the founder's prior beliefs. This mission formalizes the model and its two propositions.
The idea is worth (state ) with prior probability , or (state ). Value is realized only if the strategy used is effective (state , against ineffective ). Every strategy is effective with prior probability , independently of every other strategy and of the idea, and there are several strategies to choose from. Implementing a strategy costs and testing one costs . The standing assumptions are
where means that launching a randomly chosen strategy without testing exactly breaks even.
A test of the selected strategy has precisions and emits one of four signals, , , or :
| w.p. | w.p. , w.p. | |
| w.p. , w.p. | w.p. |
Write and for the posterior probabilities that the idea is high-value and that the tested strategy is effective, given signal . Assumption (A1), that tests are weakly informative, requires
After the signal the entrepreneur picks one of three period-1 actions:
is the best of these three conditional values. The value of testing is
The strategy-biased test is and the idea-biased test is , where is the baseline test.
For baseline precisions , if both precise tests satisfy (A1) and
then
The statement leaves and the baseline precisions free, subject only to the standing assumptions.
Proposition 2 answers the question a mentor faces when it can make a test more precise in one direction only. A test with high makes abandoning a poor idea more efficient. A test with high makes it more efficient to continue the idea with a different strategy. The condition weighs these two benefits, and it shows that the choice is driven by the prior . Proposition 1 shows why: the idea is the same in every test while the strategy can change, so switching strategies after an ambiguous signal is how the entrepreneur learns about the idea. The paper's later sections (differing priors between mentor and entrepreneur, §5.2) start from these two results.
The results are proved in the paper by hand-calculation, and Proposition 2 has no printed proof. No part of the model has been machine-checked before. The formalization produces an explicit, reusable encoding of a two-dimensional Bayesian test with a conflated signal, together with machine-checked versions of the case analysis that Proposition 1 summarizes. It also gives a checked replacement for the printed display: the second line of that display does not follow from the first.
The obvious argument reads the paper's prose, takes and as given, and subtracts. In the formal model these values are optima over three actions, computed from the signal table, and each one needs an argument.
The model lives in the namespace EntrepChoice.TestChoice. Params holds . Standing collects the standing assumptions, with kept as the hypothesis rather than substituted. Test holds , and Test.Valid bounds both in . The states, signals and actions are small inductive types, and sums over them are written out explicitly.
Action values are unnormalized: times the conditional expected payoff. With this choice (testValue) needs no division. (A1) is stated cross-multiplied by . It agrees with the posterior form whenever and is harmless when . The posteriors p1 and e1 are real quotients, equal to on a probability-zero signal.
Several conventions are disclosed readings of the paper:
testValue is the maximum over the three period-1 actions, built from the signal table. It is never defined by the closed form of milestone 6, and neither Standing nor A1 mentions it, so the goal cannot be closed by unfolding a definition.
Contributions are welcome on every milestone. Further results of the paper — testing order under irreversibility (§4.1), heterogeneous strategy priors (§4.2) and the mentor–entrepreneur game with differing priors (§5.2) — are natural follow-on missions on the same definitions.
Farmers who sell the same crop can benefit from better forecasts of the market price, but their production decisions also affect one another through the price. A forecast sent to one farmer may improve that farmer’s decision; a forecast sent to many farmers can make their output responses move together. A planner choosing who receives a common forecast therefore faces a question that differs from asking whether the forecast is accurate. Zhou, Fan, Chen and Tang study this question for a public signal about the uncertain intercept of a Cournot market’s inverse demand curve in Information Provision and Farmer Welfare in Developing Economies (SSRN preprint dated June 27, 2019, §§3–4).
The paper’s base model concerns a publicly funded information service. The planner can send the same signal to any number of farmers without charging them, and its objective is the sum of farmers’ expected profits. The target here is the paper’s Proposition 2, which says that the planner should inform either exactly one farmer or none, according to the sign of an explicit polynomial in the model’s signal precisions and number of farmers. The statement is about equilibrium production choices and the resulting profits, rather than about forecast quality alone (Zhou et al., pp. 11, 14).
There are farmers producing the same good with deterministic yield. Farmer chooses a quantity and pays . The total harvest is , and the inverse demand at sale is , where is market potential, measures price sensitivity, and is a centered Gaussian demand shock. Farmer earns . The quantities in this formalization are real valued, as required by the paper’s affine equilibrium formula; this interpretation is explained below (Zhou et al., p. 8, (1); p. 10, (2)–(3)).
Each farmer sees a private signal . The are independent centered Gaussian noises of common precision ; the shock has precision . Thus their variances are and . A planner also observes a public signal , where the independent Gaussian noise has precision and variance . The planner chooses an informed set of farmers who may see ; every farmer sees only its own , and an uninformed farmer cannot use . Write , so is an integer from zero through (Zhou et al., pp. 8–9).
A farmer’s strategy is a measurable function of the information available to that farmer. The realized quantity must be square-integrable under the joint Gaussian law. A Bayesian Nash equilibrium is a profile of such strategies in which no farmer can increase ex-ante expected profit by changing only its own admissible strategy. Write for the sum of the expected profits of all farmers at a profile . Proposition 1 gives a linear equilibrium and its almost-sure uniqueness. Lemma 2 gives the ex-ante profit of each informed and uninformed farmer at that equilibrium (Zhou et al., pp. 12, 14, 34).
The goal is the equilibrium welfare conclusion of Proposition 2. Let be the explicit polynomial displayed in that proposition, with also fixed by the model. For every informed set, an equilibrium exists. When , every one-farmer informed set strictly outperforms all sets of another size. When , the empty informed set is optimal; for it strictly outperforms every nonempty set:
At , informing zero and one farmer gives the same welfare, so the second case asserts that zero is an optimal choice rather than the unique choice. The goal compares for every Bayesian Nash equilibrium of each informed set, allowing any subset of the prescribed size (Zhou et al., p. 14, Proposition 2; p. 36).
The milestone statements follow the claims used for that result: Lemma 1’s two Gaussian posterior identities; Proposition 1’s equilibrium existence and almost-sure uniqueness; Lemma 2’s profit formulas and advantage for informed farmers; and the Appendix A claims that welfare declines after two recipients, one recipient beats two, and the sign of is controlled by (Zhou et al., pp. 10, 12, 14, 35–36). Here is the paper’s closed-form welfare expression for the linear equilibrium, extended from integer to real only for the paper’s continuous analysis.
The result identifies the welfare-optimal reach of a common forecast in a competitive production market. Under the stated model, informing more farmers does not necessarily raise their aggregate expected profit. The threshold decides whether the planner should send the signal to one farmer or withhold it. Proposition 1 and Lemma 2 are needed to connect that policy claim to farmers’ actual equilibrium decisions, rather than to a free-standing polynomial comparison (Zhou et al., pp. 12–14).
The paper proves the result mathematically. This mission asks for a machine-checked development of the Gaussian signal model, the equilibrium result, the profit identities, and the final optimization statement. The Gaussian posterior and square-integrable game infrastructure can be reused in other information provision models. The proposal statements compile, but their proofs are open; no machine-checked proof of these mission claims is asserted here.
The planner can compare policies only after accounting for how all farmers change production when the public signal is shared. Informed farmers use both their private observation and the common signal, while uninformed farmers use only their private observation; the same signal changes both the informed farmers’ expected profit and the Cournot price faced by everyone. The linear equilibrium formula alone does not justify restricting all possible strategies to linear ones. The proof must establish that it is an equilibrium against every admissible deviation and that any equilibrium gives the same realized quantities almost surely. The integer policy choice must then be related to the paper’s real extension without allowing noninteger informed sets (Zhou et al., pp. 32–36).
Lean represents the uncertainty by a product of independent Gaussian measures for , the private noises, and the public noise. The variances are the reciprocals of the positive precisions , , and . Informed sets are finite subsets of Fin n, including the empty and full sets. The observation map gives to a member of and to a farmer outside , so neither type sees another farmer’s private signal. Strategies are measurable functions with square-integrable realized quantities, and both equilibria and deviations satisfy that condition. Welfare is the sum of integrals of realized Cournot profit. The goal quantifies over all equilibria and does not replace their welfare by the closed-form function .
The base game assumes , , , and positive ; no sign condition is imposed on . The paper mentions as an unavailable-private-signal limiting case, but a Gaussian noise with variance is undefined there, so that separate regime is outside this mission. The positive public precision likewise excludes the degenerate case. Equations (2)–(3) print , but the claimed affine equilibrium takes negative values with positive Gaussian probability; the formalization uses unrestricted real quantities, which is the game solved by the paper’s displayed first-order calculations. All of these choices are explicit in the statements and should be checked against the source’s intended reading (Zhou et al., pp. 8–10, 12).
The coefficient definitions , the linear profile, the two type-specific expected profits, and are fixed to the source displays. The useful contributions are proofs of the posterior identities, unrestricted equilibrium existence and uniqueness, expected-profit identities, and the welfare inequalities. Neither an arbitrarily chosen equilibrium nor an affine-only strategy class would establish the target.
A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.
There is one buyer in tier 0 and two possible tier-1 firms, and . The tier-2 suppliers are divided into three disjoint sets: , whose members supply only ; , whose members supply only ; and , whose members supply both. A network is , where is the set of tier-1 firms still present. Its supplier set contains those tier-1 firms and the members of the three tier-2 sets. The set of dependents of supplier includes itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.
An auditing state records the current network and its finite set of unaudited suppliers, . The state is terminal when . The operator vets an unaudited supplier without changing the network. The operator drops and . If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.
At a state, the buyer can proceed to production (), audit and rectify an unaudited supplier (), or audit and drop one if it fails (). An auditing policy chooses an admissible action at every state. Let be the audit cost, the rectification cost, the chance that a supplier is noncompliant, the chance that an uncorrected violation is exposed, and the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit less the expected penalty .
The optimal value is the maximum of the values of the admissible actions at , using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value of a fixed policy and the restricted value when only and are available.
The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison
The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.
Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With , its value formula is
Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.
The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.
An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.
Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require , , and . The paper derives from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.
The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.
Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).
The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.
Time is discrete and counted backward: is the number of periods to go and period is the last. Each order must be delivered at most periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack means the order must leave now.
Shipping a package that must arrive within periods costs , the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on . In each period new orders arrive with probability .
With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack among pending orders. The state is therefore , or when nothing is pending. The cost-to-go functions and satisfy the recursion (2)–(3): for and ,
with and . Holding is infeasible at . Shipping is optimal at when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.
For every period there is an integer such that, for every slack ,
The threshold may depend on , and no formula for it is asserted.
Theorem 1 reduces the policy of a -period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.
The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for , and the case is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.
The natural first idea is to argue that the cost-to-go inherits convexity in from and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of and the slope of (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference can a priori be larger or smaller than , because the optimal shipping periods for slacks and may differ. The recursion couples two indices, period and slack, through the no-order value , and its boundary cases (, where shipping is forced, and , the last period) behave differently from the interior. The paper's own argument covers only ; the regime , in which the horizon ends before the most urgent order's deadline, is left to the reader.
valuePair F α d t returning . The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; stands for the smallest slack among pending orders. All objects are deterministic; enters only through (3).Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.Autonomous vehicles (AVs) can drive closer to one another than human drivers, because they react faster and can coordinate in platoons. Transport agencies and industry groups have therefore proposed reserving a designated lane for AVs on highways, so that AVs can exploit short headways without mixing with human-driven vehicles (HVs). Whether such a lane helps depends on a trade-off that is familiar from queueing theory: splitting a highway into two separate lanes loses the efficiency of pooled capacity, while a lane reserved for AVs moves faster when it is busy.
Mirzaeian, Cho and Scheller-Wolf (Management Science, 2021; manuscript SSRN 3278330) model a highway segment as a state-dependent loss queue and compare a no-AV benchmark with the designated-lane policy (the D policy). Their headline finding is that the D policy reduces mean travel time only when the highway is heavily loaded and AVs make up a large enough share of traffic. This mission formalizes that finding.
The queueing model is the state-dependent queue of Cheah and Smith (1994), developed for pedestrian flows, which Jain and Smith (1997) applied to vehicular traffic; its stationary law, display (12) below, is due to Cheah and Smith.
A highway segment has length and lanes, each holding at most vehicles. Vehicles arrive as a Poisson process of rate ; a vehicle that finds the segment full is turned away. When vehicles are on a segment of capacity , each travels at mean speed , for , with . This is the queue. Its stationary law is (display (12) of the paper)
its throughput is , and its mean travel time is, by Little's law, (display (13)).
The benchmark pools all lanes into one queue of capacity with speeds ; its mean travel time is . Under the D policy, a fraction of arrivals are AVs and must use the designated lane, so there are two independent queues: the AV queue (capacity , speeds , arrival rate ) and the HV queue (capacity , speeds , arrival rate ). The overall mean travel time is
The jam speeds , , are the speeds of full queues. The paper assumes throughout, and the AV lane is faster when full than the HV lanes, . The threshold is
For every with there is such that
The goal makes precise the paper's main policy conclusion: under heavy load a designated AV lane lowers mean travel time relative to the benchmark exactly when the AV share exceeds a threshold that depends only on the three jam speeds. Below the threshold, the loss of pooling dominates. This is the basis for the paper's caution against designating lanes for AVs while AV penetration is low, and the same heavy-traffic argument underlies its comparisons with the integrated policy (Propositions 2 and 3).
The printed Proposition 1(a) is not correct as stated, and the formal statement records the repair. Its heavy-load clause asserts a single valid for every ; the travel-time gap behaves like with affine and vanishing at , so no single threshold works for AV shares arbitrarily close to , and at the equivalence can fail for all . Its light-load clause (" for when is small") fails at whenever the AV lane is as fast as the benchmark at low occupancy and faster at higher occupancy, which includes the paper's calibrated model. The mission therefore poses the heavy-load clause pointwise in , excluding , which is what the paper's proof establishes. None of these results has a machine-checked proof; the queueing layer (the stationary law, travel time and their heavy-traffic limits) is new on the platform.
The heavy-traffic limits are the core. The obvious route, letting in the definition , gives the indeterminate form : the blocking probability and tends to the jam throughput. The limit has to be read off a rearranged expression, the closed form (16), whose leading terms in cancel to . Lemma 1 is a genuine monotonicity statement about a ratio of polynomials in whose coefficients depend on an arbitrary nonincreasing speed sequence; it cannot be checked degree by degree. The goal then needs strict separation of the two limits away from , together with an eventually-in- argument, and care at , where one of the two D-policy queues receives no traffic.
The queue is represented by its closed-form stationary law (12), exactly as in the paper; no continuous-time Markov chain is constructed. Speeds are arbitrary real sequences , read at ; the platooning model of §3.1.2 (a Markovian arrival process that generates the speeds) is out of scope, and Proposition 1 is stated in terms of the speeds only. "Decreasing" speeds are read as nonincreasing (AntitoneOn on ), and "increasing" in Lemma 1 as weakly increasing. Capacity is per lane. The arrival rate is real, and the limit is in . Lean's assigns at , where the throughput vanishes; Lemma 1 and (16) are therefore stated for , and the goal's is positive. At or the idle queue's junk value carries weight zero. The strict inequality (the proof writes ) keeps the threshold's denominator nonzero, and it is necessary for the equivalence. The goal is not trivialized by vacuous hypotheses: the instance , , , , satisfies all of them, with strictly inside . A statement that drops the exclusion , uses one for all , or feeds the full rate to both D-policy queues would not be this result.
A complete development needs finite sums and products, factorials, polynomial-ratio limits at infinity, and a monotonicity argument for ratios of power series truncations. The loss-queue layer (stationary law, throughput, travel time, its closed form, monotonicity and heavy-traffic limit) is reusable for any model, including the paper's integrated policy. Contributions to any milestone, and alternative proofs of Lemma 1, are welcome.
The apparel industry is a large source of carbon emissions, water use and landfill waste, and much of that footprint comes from garments being discarded early. Fast-fashion retailers such as Zara and H&M combine two operational choices: they offer a very large number of styles each season, and they replenish the styles that turn out to be popular through quick response, i.e. production during the selling season at a higher unit cost. Their garments are also widely reported to be of low quality, which shortens their useful life and reduces the chance of reuse.
X. Long and J. Nasiry, Sustainability in the Fast Fashion Industry (SSRN 3486502; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2021.1054), give an operational explanation of low quality: it is driven by the firm's incentive to offer variety. The paper's headline (abstract, and the first sentence of its conclusion) is that when variety is chosen by the firm, quality falls as consumers become more sensitive to fashion or as introducing new styles gets cheaper. This mission formalizes that result and the chain of propositions leading to it.
A firm sells one season of a fashion product. Before the season it chooses a number of styles (design cost ), a common quality , and an inventory per style produced at unit cost . Styles are points on a circle of unit circumference (Salop's circular city). During the season, a trend uniform on the circle and a market size are realised. All consumers buy the style closest to the trend at their valuation
where is the arc distance, is a base value, and and measure the sensitivity to quality and to fashion. Demand above is met by quick response at unit cost with ; unsold units of the other styles are wasted.
The paper shows that equally spaced styles are optimal (Lemma 1), computes the expected price and the expected quick-response volume , and arrives at the firm's problem (1):
An optimal solution is a feasible triple with the largest expected profit. The parameters satisfy and ; is any real number.
For admissible parameters, problem (1) has an optimal solution, and
where each comparison changes one parameter, keeps the others fixed, and holds between every optimal solution before the change and every optimal solution after it. Monotonicity is weak: on part of the parameter space the optimal quality does not move.
In attack order:
The result separates two channels by which fashion sensitivity could affect quality. For a fixed number of styles, the optimal quality does not depend on , or at all (p. 17). All of the effect therefore runs through variety: more styles mean more leftover inventory or more reliance on expensive quick response, and the firm cuts quality to lower the unit cost. Policy conclusions in the paper rest on this mechanism. The disposal-cost and production-tax analyses of §5 ask whether a regulator can reverse the quality decline, and the environmental-impact comparison (Corollary 3) compares fast fashion with a single-style firm.
The paper proves the result with Karush–Kuhn–Tucker conditions on a non-concave reduced problem, split into four regions of and several cases in . No machine-checked proof of any of its statements exists. A formal development would certify the region analysis, which the paper itself states with thresholds that are easy to mistype. It would also supply a reusable treatment of monotone comparative statics for every selection of a non-unique optimum. Two printed slips are already corrected in the statements: the expectation "" on p. 11 should read , and the optimal-inventory display on p. 14 needs .
The reduced profit is not concave in : on its second derivative changes sign, and the optimum can jump between , an interior critical point , and the region-III value . Differentiating an optimality condition, the implicit-function argument the paper uses for , says nothing about these jumps or about ties. The goal is stated for every optimal solution, including the parameter values where two values of are optimal, so a proof needs an argument valid across jumps.
Everything is real-valued. Parameters form a record with an admissibility predicate. Problem (1) is one explicit real function, and the feasible set is , , , with the number of styles a real number as in the paper's analysis. "Optimal" means a feasible maximiser over this set. "The optimal " is read as the -component of every optimal solution; "increases/decreases" are weak; parameter changes are strict and vary one record field ({ P with γ := γ₂ }). Ties at the thresholds of Proposition 3 are handled by asserting uniqueness of only off the thresholds. The circle is AddCircle (1 : ℝ), whose metric is the arc distance and whose Haar measure is the uniform probability; the uniform market size is an interval integral divided by . Lemma 1 is stated in the reduced form its proof uses: equal spacing minimises the expected nearest-style distance. The paper's standing assumption that the base value is high enough to make quick response always worth using does not enter (1) and is not a hypothesis.
The goal is a statement about every joint maximiser of the expected profit (1) over , , . It compares parameter values that differ in one coordinate only, and it asserts that an optimum exists. For a fixed number of styles the optimal quality does not depend on , or , so a formalization about the per- optimum would be trivially true; the content lies entirely in how the optimal variety responds.
A proof needs only real analysis: one-variable optimisation of quadratics, existence of a maximiser of a continuous coercive function, and an increasing-differences (Topkis-type) monotonicity argument. A proved abstract version of the latter is on the platform, Supermodularity.Monotonicity.argmax_mono_of_strictly_increasing_differences. Lemma 1 needs integration on AddCircle and a convexity inequality over arc lengths. Contributions of alternative proofs of Proposition 3, and of reusable lemmas on comparative statics of argmax sets, are welcome.
A two-sided platform (a ride-hailing service, a marketplace, a payment network) earns money only when its two sides transact, so its value depends on the stock of participants on both sides. A young platform has to decide not only how fast to grow but also which side to grow, and it does so through the prices it sets on each side. Whether to subsidize drivers or riders, sellers or buyers, is a recurring operational decision, and the economics literature on two-sided markets (Rochet and Tirole, 2003; Armstrong, 2006) studies it mostly in static models.
Lian and van Ryzin (SSRN 3310559, later published in Management Science, 2021, doi:10.1287/mnsc.2020.3832) pose the question dynamically: supply and demand stocks grow with the surplus each side receives and decay at their own attrition rates, and the platform chooses prices over time to maximize discounted profit. Their first main result, Theorem 1, says that the optimal mix of the two sides at any moment depends only on the current size of the market, and it describes exactly how that mix moves as the market grows. This mission formalizes Theorem 1 and the lemmas its proof rests on.
A supply stock and a demand stock generate transactions per unit time, where the output function is homogeneous of degree : for . The returns to scale are decreasing if and increasing if . Buyers value a transaction at , sellers incur cost . Supply and demand decay at attrition rates and grow with adoption coefficients ; the platform discounts at rate .
When prices are unconstrained, the two stocks reduce to one market size and a balance , the share of the size held by supply. With the output is , and the size evolves by
where is the platform's per-transaction margin. The platform maximizes over balance and margin paths (problem (13)). The net welfare rate is
The paper assumes (Assumptions 1–4) that is twice differentiable and positive on , nonnegative at and , strictly concave (), that has a unique zero , the output-maximizing balance, and, when , that .
In Lean the primitives are the fields of TwoSidedGrowth.Balance.Model (with ASCII names bs0 bd0 bs1 bd1 for the four 's), the assumptions are the structure Model.Standing, and h, out, G, kappa, IsBalance, Admissible, profit are the objects above.
Write . For every market size the optimal balance is
in the sense that exactly one balance satisfies (14); it is the unique maximizer of on ; and along any size path the balance path yields at least the discounted profit of every other admissible balance path on every finite horizon. Moreover, as grows from to , moves monotonically:
The balances and are the durability-maximizing balances: all of the market on the side that attrites more slowly.
Theorem 1 separates the two controls of the growth problem: the balance is chosen myopically from the current size, and only the margin, which determines how fast the size moves, remains a dynamic decision. Every later result of the paper (the stationary size of Theorem 2, the subsidy and growth policies of §4) analyses a one-dimensional problem in because of this reduction. The table also has a direct managerial reading: a small market with decreasing returns should be balanced for output, a large one for durability, and with increasing returns the order is reversed.
The result is proved in the paper, partly in prose ("the other three cases can be checked similarly"). No machine-checked version of it is known. The formal development adds a precise reading of (14) when is unbounded at the ends (as it is for the paper's own Cobb–Douglas example, where the printed claim that is bounded by and fails), explicit monotonicity and limit statements for all four cases, and a machine-checked version of the profit identity that underlies the reduction.
The identity of Lemma 5 is an integration by parts, and the argmax of a strictly concave function is unique. The work lies elsewhere. The first obstacle is that need not be bounded on , so has to be read as an extended inverse with three regimes, and the argmax characterization must handle the boundary cases where is monotone on and its maximum sits at an endpoint where has no derivative. The second is the monotonicity: the naive argument differentiates everywhere, but is constant at or on whole intervals of sizes when is bounded at an end, and it is not differentiable where it reaches the boundary; monotonicity has to be proved for the clamped function directly, and the derivative formula (34) only on the open set of interior balances, through the inverse function theorem. The limits require continuity of the extended inverse at and the divergence of at the other end of the size range.
TwoSidedGrowth.Balance; the single definition file Setting holds the model and all derived objects.IsBalance: an interior root of , or when on , or when on . It is not defined as an argmax of , and the profit of (13) is the integral of , not the right-hand side of Lemma 5; either shortcut would make the main conjuncts definitional and is ruled out.Retailers that sell both through physical stores and online increasingly offer buy-online-pickup-at-store (BOPS): a customer reserves an item online against the store's inventory and collects it in the store. Whether this helps the retailer is not obvious. BOPS changes which customers draw on the store inventory, and therefore how much stock the store should carry and how often a visiting customer finds the item. Gao and Su (Management Science, 2017) modelled BOPS with customers who respond to store inventory availability and found that it need not be profitable for every product; Hu, Xu, Xue and Yang (Management Science 68(2), 2022; accepted manuscript SSRN 3214047) ask when it helps, through the inventory side. They identify two opposing effects: demand pooling, where BOPS moves online demand onto the store inventory, and demand depooling, where BOPS splits off customers who used to buy in the store. This mission formalizes their first effect, Proposition 3: in a stated region of costs, BOPS benefits the retailer.
A retailer owns one brick-and-mortar store and an online channel fulfilled from a distribution centre. On a probability space there are two customer segments with random market sizes: store-only customers, who buy only in the store, and omni-customers, who may buy in the store or online. The store sells at price with unit cost ; the online channel sells at with unit cost . A store visit costs a customer , waiting for an online delivery costs . The base surpluses are online and in the store, and Assumption (U) holds throughout.
The retailer chooses a store order quantity before demand is realized. A customer who visits the store finds the item with probability equal to the store's fill rate , where is the demand facing the store (Deneckere and Peck). Customers decide on the basis of a belief about the fill rate; the retailer orders on the basis of beliefs about the fractions of each segment that shop in the store.
A rational-expectations (RE) equilibrium is a profile in which customers' choices are optimal for the believed fill rate, the order quantity is optimal for the believed choices, and both beliefs are correct. When several exist, the paper selects the Pareto-dominant one. The optimal order quantities , (BASE, with only store-only customers, respectively both segments, in the store) and (BOPS, store-only customers in the store) define fill rates .
If
then Pareto-dominant RE equilibria exist under BASE and under BOPS, and at any such pair the retailer's expected profits satisfy
Proposition 3 is one half of the paper's comparison of BOPS with independent channels (Figure 3 of the paper): together with the depooling effect (Proposition 4) it partitions the cost region below the diagonal into areas where BOPS helps, hurts, or is neutral. It isolates a mechanism that does not appear in models with exogenous store demand: the fill rate, and hence customers' channel choices, respond to the inventory decision.
The paper's proof is short once the equilibria are characterized, but it is a proof in the paper's normal-demand model, where the statement does not hold (see below). The mission produces a corrected, machine-checked version: an explicit equilibrium model with rational expectations and Pareto selection, the characterization of the equilibria that the comparison needs, and the comparison itself. None of these results has a machine-checked proof.
The comparison of profits is easy once one knows which equilibrium each strategy selects; the work lies in the equilibrium analysis. Equilibria are fixed points of a map that couples a newsvendor problem with a discrete choice through the fill rate, and the fill rate is a ratio of expectations of the optimizer. Showing that a candidate profile is consistent, that the remaining profiles are not, and that the selected one Pareto-dominates every other, requires comparing optimal values of different newsvendor objectives and monotonicity of optimizers between them (Lemma 2), without closed forms. The obvious shortcut, reading off the equilibria from the paper's case tables, is not available: the tables are the theorems to be proved.
All objects live in the namespace OmniPool.BOPS; a single definitions file encodes the profits (2) and (4) term by term, the fill rates, the choice rules in utility form, and the RE equilibria of Definitions A1 and A2 as fixed points.
The goal asserts existence of Pareto-dominant equilibria under both strategies; without these conjuncts the universally quantified comparison could hold vacuously. Defining by the paper's region tables instead of through equilibria would make the goal a tautology and is ruled out.
Infrastructure needed: integrability of truncated demands, monotone comparative statics for maximizers of functions with increasing differences, and pointwise identities between the profit expressions. The equilibrium definitions are reusable for the paper's other results (Propositions 4 and 5) and for RE models of omnichannel retail. Proofs of the milestones, and formalizations of Propositions 1(i) and 2(ii)–(iii), are welcome.
Mean-variance analysis, the trade-off between the expected value and the variance of a portfolio's outcome, is the most widely used criterion for portfolio choice in practice. In continuous time it has two well-known defects when applied to terminal wealth: the criterion is time-inconsistent (a strategy that is optimal today is no longer optimal tomorrow), and the resulting equilibrium strategies of Basak and Chabakauri (2010) and Björk, Murgoci and Zhou (2014) prescribe a dollar amount in the stock that does not scale with wealth, which is at odds with how investors and advisers think in terms of portfolio fractions.
Dai, Jin, Kou and Xu apply the mean-variance criterion to the log-return of the portfolio instead of to wealth. They show that, in the classical complete market with constant coefficients, the resulting equilibrium strategy is a constant fraction of wealth, that it coincides with the classical optimal strategy of Merton (1969) for a CRRA investor with relative risk aversion , and that the investor's preference parameter is in one-to-one correspondence with a target annual return. The last fact is what the paper uses to elicit from an investor's stated target return.
A bond pays the constant interest rate . One stock has price with constant drift , volatility , and a standard Brownian motion on a probability space. An investor with horizon holds the fraction of wealth in the stock. A feedback strategy is a function of time and current log-wealth . The log-wealth then solves the stochastic differential equation (6)
For a time and a log-wealth , the investor evaluates a strategy through the reward function
the mean minus times the variance of terminal log-wealth for the process started at . Here is a constant (Assumption A). A strategy is admissible if .
Because is time-inconsistent, optimality is replaced by an equilibrium, following Björk, Khapko and Murgoci (2017). For and , the perturbation holds the constant fraction on and follows afterwards. An admissible is an equilibrium strategy (Definition 1) if, at every , every and every ,
With the market price of risk, the mission's two named quantities are
In Lean these are piHat M and aHat M for a market M : Market with fields μ r σ γ T; the SDE is IsLogReturn, admissibility Admissible, the reward J, the perturbation spike and Definition 1 IsEquilibrium.
A supporting item (not a milestone) states the reward of an admissible deterministic policy, (p. O–10); another states that and all its perturbations are admissible.
Part (i) shows that the dynamic mean-variance criterion on log-returns and CRRA expected utility of terminal wealth share the same optimal strategy in a complete market, although the first is time-inconsistent and the second is not. Part (ii) gives a closed-form, strictly increasing link between the target annual return and , which is the basis of the paper's procedure for eliciting the risk parameter (Corollary 1) and of its comparisons with terminal-wealth mean-variance strategies.
The result is proved on paper; nothing in it has a machine-checked proof. Formalizing it requires a working account of the Itô integral of deterministic integrands against Brownian motion (Gaussianity of the integral, its mean and variance, and uniqueness of solutions of an SDE with deterministic coefficients) in the form of the published step-sum relation EthierKurtz.HasBrownianItoIntegral. That account is reusable by any mission that computes moments of linear SDEs.
The paper's proof is three displays long because it takes the moment formulas for granted. Mathlib has Brownian motion (IsBrownianReal) but no Itô integral, no Itô isometry and no existence theory for SDEs, so each of the following is real work:
The equilibrium inequality itself is pointwise algebra once the reward is known.
EthierKurtz.HasBrownianItoIntegral, in elapsed time from , with the integrand set to after the horizon.Classical.epsilon); under admissibility the choice is immaterial.Market.Standing. The coordinates of are assumed measurable.Trivializing encodings are ruled out: is defined from the SDE and never by the closed form of Appendix C.2, and the goal's conclusion (not its hypotheses) asserts admissibility of and of every perturbation, so the equilibrium claim cannot hold vacuously. The moment milestone concludes , because Lean's integral and variance are on non-integrable inputs.
Welcome contributions: the Gaussian law of for deterministic under the step-sum relation; existence and uniqueness for (6) with deterministic coefficients; and the algebraic milestones, which are independent of the stochastic layer.
Two-stage stochastic linear optimization is the standard model for decisions taken before uncertainty is revealed and corrected after it: capacity before demand, inventory before transport capacities, generation commitments before load. In practice the probability distribution of the uncertainty is unknown and only historical samples are available, so the stochastic problem has to be replaced by a data-driven one. The sample average approximation (SAA) is consistent but can overfit badly on small samples; distributionally robust formulations hedge against this, but for two-stage problems they are typically intractable.
Bertsimas, Shtern and Sturt (arXiv:1907.07142v4, published as a Technical Note in Operations Research, 2022) study sample robust optimization (SRO): each sample is perturbed adversarially within a small ball intersected with a known support polyhedron. SRO is equivalent to two-stage distributionally robust optimization over a type-∞ Wasserstein ball (Bertsimas, Shtern, Sturt 2018, Proposition 3, as cited on p. 7), and evaluating its objective is NP-hard even for one sample. The paper proposes a tractable multi-policy approximation (MP), with one linear decision rule per sample, and proves that it recovers the optimal value and the optimal decisions of the underlying stochastic problem as the data grow, without assuming relatively complete recourse.
The data are , , , and an affine right-hand side . The second-stage cost of a first-stage decision under the realization is
equal to when no recourse is feasible. With a random vector of law , the stochastic problem is
The support of lies in a known polyhedron . Given i.i.d. samples , a radius and an -norm, the uncertainty sets are and
A linear decision rule is a policy ; the set of them is . The multi-policy approximation chooses, besides , one rule per sample, feasible on its own set:
The single-policy approximation (SP) uses one shared rule for all .
Assume [A1] ; [A2] is finite and ; [A3] the optimal set of (OPT) is nonempty and bounded; [A4] there are and such that around every some linear decision rule is feasible on . Then
and almost surely every accumulation point of optimal first-stage decisions of (SRO) or (MP) is optimal for (OPT).
Theorem 2 says that a linear or second-order cone program with variables and constraints (Proposition 1) is a consistent estimator of the optimal value and decisions of a two-stage stochastic linear program, under assumptions comparable to those for SAA, for unbounded and without relatively complete recourse. Theorem 1 adds that (MP) is always a valid upper approximation of (SRO), so the same limit holds for the intractable SRO problem.
The result is proved in the paper; nothing here is open. No part of it has been machine-checked. A complete development would give a verified model of two-stage linear programs with extended-valued recourse, a verified sample-robust and multi-policy layer, and the polyhedral lemmas on balls intersected with polyhedra (Lemmas 5, 9 and display (3)), which are reusable for other robust and distributionally robust convergence results. The two cited consistency statements (milestones 1 and 7) would be the first formal consistency results for SAA with extended-valued convex integrands.
The upper bound cannot be obtained by plugging an optimal into (MP): need not admit any linear decision rule feasible on a neighbourhood of a sample, and without relatively complete recourse a sample near the boundary of the feasible region may admit none at all. The proof perturbs towards the point given by [A4], which requires the uniform radius of display (3), obtained from an induction over the faces of in Appendix C. Lemma 1's direction [A4] [A6] is a second induction over face dimension (Appendix B).
The lower bound reduces to SAA, but the SAA consistency it needs is for an extended-valued, merely lower semicontinuous convex integrand (King and Wets 1991), for which Mathlib has no epi-convergence theory and no law of large numbers for random lower semicontinuous functions. A uniform law of large numbers on a compact set does not apply: the feasible region need not be bounded and is off a polyhedron.
Vectors are Fin k → ℝ; the -norm is that of PiLp p for an arbitrary p : ℝ≥0∞ with 1 ≤ p, the dual norm is , and the same p is used on in Lemma 3. Every optimal value (, , , the SAA, SRO, SP and MP values, , , ) is an infimum or supremum in EReal: "min" and "max" are read as inf and sup, attainment is never assumed, infeasibility gives , and the factor is the real . The expectation is the platform definition DupacovaWets.Consistency.expect ( when , else ), which agrees with the usual expectation whenever is finite. Samples are ξ 0, ξ 1, …, independent with law and ; the paper's are the first . The radii are deterministic. (MP) is stated as printed with policies. Faces of are nonempty sets , and the relative interior is intrinsicInterior.
Trivializing encodings are ruled out: is not real-valued with a junk value for infeasibility, the expectation is not a Bochner integral of a real truncation, optimal values are not real sInfs, [A4] is the printed local condition and not the global single-rule condition of Proposition 2, and the accumulation-point clauses quantify over sequences that are optimal for all large (requiring optimality at would make them vacuous).
Disclosed readings: the accumulation-point clauses of Theorem 2 hold on one almost-sure event for every eventually-optimal sequence; Lemmas 2 and 3 and display (3) carry §4.2's standing [A2]–[A3], the support condition, and optimality of ; Lemmas 5 and 9 assume the appendix's normalization but not minimality of the representation; display (3)'s set-builder, which omits its bound variable, is read as in Theorem 3; Lemma 2 is stated as printed with , although its proof derives the equivalent form with and swapped.
Contributions welcome: proofs of any milestone, in particular LP strong duality in this inequality form for Lemma 3, the polyhedral Lemmas 5 and 9, and the SAA consistency results, which are reusable beyond this mission.
In the first weeks of the COVID-19 pandemic, diagnostic testing capacity in many countries was a small fraction of the population, and policy discussion centred on waiting for more accurate tests before deploying them widely. Drakopoulos and Randhawa (SSRN 3565245; Management Science, 2021, doi:10.1287/mnsc.2021.4029) treat a test as an information product: an agent's decision to request a test depends on how much the test's result could change that agent's own action. When tests are rationed among those who ask, the accuracy of a test therefore determines not only what is learned from each test but also who asks for one. The paper shows that, under scarcity and uniformly random rationing, a planner can strictly prefer a slightly imperfect test to a perfect one. The result speaks to operations managers and public-health planners who allocate scarce diagnostic capacity, and to the literature on pricing and allocating information goods.
A unit mass of agents has private priors of being infected, distributed with density on and distribution function ; write . An agent who acts (seeks treatment, self-isolates) earns , where is a normalized cost; an untested agent acts iff , with expected utility .
A -test has false positive rate and true positive rate , with ; the -test is the perfect test. The value of the test to an agent is , where is the expected utility of acting optimally after observing the result. Two critical values
split the agents into low-likelihood (, never act), medium-likelihood (, follow the test) and high-likelihood (, always act). Only medium-likelihood agents request a test, so the demand is .
A mass of kits is scarce and is allocated uniformly at random among requesting agents, so each requester is tested with probability . The planner gains for every infected agent who acts and loses for every uninfected one; its objective is the expected net gain over the population (display (9) of the paper with ). Finally
Assume a perfect test is available, , and . Then , and
In the order of the paper's argument:
The result. Proposition 2 gives explicit sufficient conditions, in terms of the density of priors at the extremes, under which accuracy and social value come apart: when many agents have priors near (respectively near ), lowering the specificity (respectively the sensitivity) of the test discourages those agents from requesting it and frees kits for agents whose actions depend on the result. It is the paper's main formal argument against waiting for a perfect test under scarcity, and it isolates the mechanism — demand that responds to test quality — that the paper's later examples and observations build on.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formalization fixes the model unambiguously (who requests, how kits are rationed, what the planner counts) and checks the proof's calculus, including one-sided derivatives at the boundary of the set of tests and a derivative of a parametric integral whose limits and integrand both move. Formalizing the proof also checks the printed derivative , whose middle term is printed as although the condition the paper derives from it, and the corrected computation, give ; milestone 12 states the corrected value.
The planner's objective is defined agent by agent from behaviour, so the first obstacle is to show that the set of requesting agents is exactly the interval (Lemma 1) and to turn into the three-integral closed form; only then is a function of through , and . The second is the derivative at the perfect test. At the thresholds sit at the endpoints and of the prior's support, so the derivatives exist only from one side, the integrand is evaluated at an endpoint where a density is not determined pointwise, and the availability moves with the thresholds. The naive argument "a more accurate test always helps" holds when tests are plentiful (Proposition 1 of the paper, where ); under scarcity the congestion term is what can reverse the sign, and it has to be tracked exactly.
All objects live in the namespace ScarceTesting.PerfectTest, in one definitions file Setting. Conventions:
f with IsPriorDensity f: nonnegative on , interval-integrable on , total mass ; cdf f x is . Values , are read with ContinuousWithinAt f (Icc 0 1) at the endpoint, a disclosed reading of "density with value ".if D ≤ κ then 1 else κ / D, so that zero demand gives .S integrates each agent's expected contribution against ; it is not defined by the paper's simplified formula, which is a milestone.A complete development needs Lebesgue and interval integrals with variable limits, the fundamental theorem of calculus at an endpoint of continuity, and one-sided derivatives of parametric integrals. The Bayesian value-of-a-test layer (Lemma 1, display (6)) is reusable for other models of testing and information products. Proofs of any milestone are welcome independently.
Data have become an input to innovation: firms use consumer data, together with research labor, to develop new products. Data differ from labor and capital in two ways. They are a by-product of consumption, so their supply is endogenous, and selling them costs consumers privacy. Cong, Xie and Zhang (arXiv:2109.10028, published in Management Science) put both features into a continuous-time semi-endogenous growth model in the tradition of Romer (1990) and Jones (1995). They then ask whether a decentralized market economy with data trading grows at the rate a social planner would choose.
The paper's headline has two halves. The first, which this mission formalizes, is analytical: on the balanced growth path the decentralized economy and the social planner grow at the same rates (Proposition 3). The second, that the market economy underemploys R&D labor and overuses data, is shown only numerically (§3.3, Figure 1) and is not part of the mission.
Time is continuous. The population is with . Parameters: discount rate ; inverse elasticity of intertemporal substitution , ; privacy-disutility curvature ; labor elasticity ; marginal cost of intermediate goods; innovation efficiency ; data share ; knowledge spillover .
Varieties of intermediate goods accumulate through the innovation possibility frontier
where is the data each consumer sells and , are the labor shares of R&D and final-good production.
The decentralized economy (§2). Per-capita consumption obeys the Euler equation . The data price obeys . Data are bounded by consumption: . Monopolistic intermediate producers earn the profit and pay the wage . A patent is worth the present value
Free entry equates the marginal value of data and of labor in R&D with their prices: and .
The social planner (§3.2) maximizes the consumer's utility subject to the frontier, the resource constraint with , and . The paper solves this problem through the necessary conditions of the current-value Hamiltonian, with shadow prices and ((A.7)–(A.10)).
A balanced growth path (BGP) is a path on which every variable grows at a constant rate of its own, and the interest rate is a constant . With , write
With , for a balanced growth path of the decentralized economy and one of the planner's system with the same parameters,
and the planner's per-capita output grows at . The goal states equality of rates, not their closed form.
The result. The equilibrium is inefficient: monopoly pricing and the knowledge spillover drive a wedge between private and social returns to R&D. Proposition 3 says that this wedge acts on levels (the R&D labor share and data intensity), not on long-run growth rates. Those rates are pinned by population growth, preferences and the frontier's returns to scale, and are free of scale effects. This puts the paper in the semi-endogenous growth family and isolates where data policy can matter. Privacy regulation and data ownership change allocations, not the long-run growth rate.
Formalizing it. The proofs in the paper are short and use growth-form identities freely. The mission makes the model precise: what a balanced growth path is, which equations hold in levels, and where integrability and positivity enter. The definition layer (constant-growth paths, present values of profit streams, Hamiltonian necessary-condition systems for growth models) does not exist on the platform and is reusable for other continuous-time growth models. None of these results has been machine-checked before.
The individual steps are short, but each has a gap the paper leaves open:
The tempting shortcut is to work with the growth rates directly. That skips the content: the rates of a balanced growth path are not given numbers, they are derived from the level equations.
Real.rpow and of the Bochner integral are excluded. Both BGP notions were checked to be inhabited at the paper's Table 2 calibration.A financial position can have many possible outcomes, and a risk measure assigns a number to the cash needed to make that position acceptable. A risk manager who uses expected disutility must choose a loss function to describe how strongly different losses matter. That choice is often uncertain: several functions can fit the available preference comparisons. Delage, Guo and Xu study how to measure risk when the loss function belongs to a set rather than being known exactly. Their model keeps one common probability law and makes the preference uncertainty explicit. This matters when an optimization problem uses risk as its objective or as a constraint, because the chosen loss function can change the resulting decision. The paper develops this model and later studies preference information, discrete optimization reformulations, and sample approximation (Delage, Guo and Xu, §§1, 3–5).
Fix a probability space . A position is a real random variable with finite th moment, where . Positive represents a gain, so the loss after adding cash is . A loss function transforms that loss before expectation. The paper's class consists of convex, nondecreasing functions that are strictly increasing on for some (Definition 2.1). This excludes a loss function that remains flat around zero and fixes the normalized benchmark .
The individual shortfall risk is the least cash amount for which expected loss is no greater than the benchmark:
If is a set of plausible loss functions, the preference robust shortfall risk requires the same cash amount to satisfy every member of :
The normalization belongs to each function separately. The paper also defines the worst risk of a set of risk measures as ; these are (1.2)–(1.4) of the dated preprint (Delage, Guo and Xu, pp. 2–3 of the April 25, 2018 preprint).
The goal is all three claims of Theorem 2.1. First, for every and every admissible ,
Second, with , the same value is . Third, if is a set of normalized convex utility-based shortfall risk measures and , then
The supporting targets follow the statements used on pp. 5–7: divergence of each at (Lemma 2.1(ii)); the extended Jensen inequality and its supremum form (2.11); divergence of the robust gap as cash tends to (2.12); the inequality (2.13); feasibility of the finite worst individual risk; and the infinite-value case. These targets retain the source's separate finite and infinite regimes (Delage, Guo and Xu, Theorem 2.1 and proof).
The identity gives two ways to use preference uncertainty. A decision problem may impose one common expected-loss constraint across all plausible preferences, or it may evaluate the worst individual shortfall risk. Theorem 2.1 says these produce the same risk for the admissible position. The paper uses this connection before characterizing loss-function sets from preference information and deriving optimization formulations. It also clarifies that robust shortfall risk need not itself equal the shortfall risk of one fixed loss function: the worst function can depend on the position (Proposition 2.2, Delage, Guo and Xu).
The theorem is proved in the cited paper. The remaining work here is a machine-checked proof of the exact extended-value statement and its supporting steps. The proposal contains compiled Lean statements with proof placeholders; no new machine-checked proof of Theorem 2.1 is claimed. A completed development would also provide reusable definitions for loss classes, extended shortfall risks, and worst-risk operators.
The tempting interchange of an infimum over cash with a supremum over loss functions is not valid for arbitrary constraint families. Here each loss function belongs to , and the proof must account for the behavior of its expected loss as cash varies. The expected loss can be infinite even when has a finite th moment, and the common feasible set can be empty. At the other boundary, an empty loss set makes every cash amount feasible. The proof therefore has to establish the finite case and handle the two extended endpoints without silently replacing them by ordinary real values. The page's finite-case argument also uses feasibility at an individual infimum; this requires a continuity fact that is implicit in its displayed calculation.
The Lean model represents by a real function with MemLp Z p P, , on a probability measure. It represents by convexity, monotonicity, and strict increase from a negative threshold. It imports the published DupacovaWets.Consistency.expect for extended expectation, which returns when the positive part has infinite integral. Risk values live in EReal. An infimum over cash is taken after embedding its feasible real cash amounts into EReal; this preserves for an empty feasible set and for one unbounded below. The supremum over an empty is , as in the extended-real convention.
The definition of uses the paper's single supremum constraint, with subtracted inside that supremum. It is not defined through the theorem's proposed right-hand side. Individual risk maps are total on real functions, while the goal evaluates them only for positions in . The converse describes the members of as maps for some , using the characterization in Proposition 2.1 without formalizing that proposition. The divergence target (2.12) requires nonempty; the source's displayed limit fails for an empty set, although the main theorem includes that case. Supporting statements use Integrable Z P, a consequence of the source's condition on a probability space. Contributions proving the extended Jensen step, endpoint behavior, and the representation are within scope; the paper's later numerical and sample-approximation results are separate work.
An assortment decision determines which products a customer can buy, but its expected revenue depends on the probability that the customer chooses each offered product. A distribution over complete rankings gives a direct model: sample a customer's ranking, then take the highest-ranked product in the assortment. The resulting choice probabilities are easy to define and expensive to evaluate by direct enumeration, because a universe of products has rankings. Désir, Goyal, Jagabathula and Segev study this issue for distributions built from Mallows models and use the resulting probabilities in assortment optimization and a case study (manuscript, §§2–5). This mission isolates their exact dynamic program for a single Mallows model, Theorem 1 of the manuscript.
Let the product universe be , with . A ranking assigns each product a distinct position from to ; a smaller position means higher preference. The modal ranking is , meaning that has position . This choice follows the manuscript's relabelling of the products in §4.1. It fixes a reference order without restricting which ranking a customer may draw.
The Kendall–Tau distance counts pairs of products whose order in disagrees with their order in . For a concentration parameter , the Mallows distribution assigns probability
The normalizer sums over all rankings. At they are equally likely; larger gives less weight to rankings with more pairwise disagreements. Every summand in is positive, so the distribution is well-defined (manuscript, §2.1, p. 7).
An offer set is a subset of the products. For an offered product , its choice probability is the Mallows weight of rankings that place before every other member of :
This is equation (1) of the manuscript for one Mallows component (§2.2, p. 8). The formula is an exact definition, but its sum ranges over every ranking.
Algorithm 1 is the repeated insertion method. It starts with and inserts each next product at a position with probability
Write . After step , let denote the probability that is first among the offered products inserted so far and occupies position . The manuscript's Algorithm 2 computes a separate table, , by its initial condition and recursions (3)–(4), without enumerating rankings (§4.1, pp. 16–18).
For , the mission's goal is Theorem 1: Algorithm 2 returns the Mallows choice probability of each offered product.
The table also returns zero for every product outside . The milestone list follows the source's intermediate claims: the repeated insertion law is Mallows; choice probability decomposes by final position; and the probabilities obey the two cases of the insertion transition (Lemma 1 and §4.1, pp. 17–18).
The result replaces an -term probability sum with the manuscript's dynamic program for all offered products at once. Those probabilities are inputs to its later assortment optimization model and permit computations on product universes where direct ranking enumeration is impractical (manuscript, pp. 16, 18–21). This mission targets the exact identity, not a numerical approximation or the later mixed-integer formulation.
The result is already proved in the cited manuscript; the goal here is a machine-checked Lean proof. A completed development would provide reusable finite-ranking definitions, a formal repeated insertion law, and verified transitions between a probabilistic model and an explicit recurrence. The definitions and theorem statements in this proposal compile locally; the theorem proofs remain open.
At a single insertion, the chosen offered product can keep its position, move down one position, or be displaced by the new product. Which outcome matters depends on whether the newly inserted product is offered and on where the previous best offered product stood. A naive table recording only each product's total choice probability loses the position information needed for the next insertion. Algorithm 2 retains that information in , so a proof must connect its state and boundary values to the distribution over complete rankings (manuscript, §4.1, pp. 17–18).
Products and ranks are represented by Fin n and rankings by permutations of Fin n, interpreted as product-to-rank maps. Lean's indices begin at zero; the paper's , insertion position , and table indices begin at one. The modal ranking is identity after the paper's relabelling. Offer sets are finite subsets of Fin n, and wherever is named. The concentration parameter satisfies . The Mallows normalizer is the finite sum displayed above, rather than the manuscript's printed product formula.
Algorithm 2 says “without loss of generality” that . The printed recurrence actually needs that condition, so the goal and the new-product transition state it explicitly. Equation (1), read literally for , can be positive because its indicator does not test membership. The main equality is therefore about ; the table's zero output for unoffered products is stated separately. Outside the paper's index ranges, , the probabilistic , and the dynamic-program table have explicit zero values. In particular, and settle the boundary in recursion (3).
The left side of the goal is the weighted sum over every ranking; the right side is the table computed from recursions (3)–(4) and never examines a ranking. A proof needs finite permutation reasoning, normalization of the insertion probabilities, and a link between the insertion law and the table's meaning. Lemmas about these pieces, as well as proofs of the listed milestones, are welcome contributions.
Industrial buyers rarely negotiate with suppliers from scratch. A common practice is to issue a request for proposal/quotation (RFx): suppliers first submit quotations, and the buyer then negotiates contracts with them one after another, possibly using the quotations as fallback options. Chu, Rong and Zheng (SSRN 3200030; Operations Research, doi:10.1287/opre.2019.1964) ask whether this extra stage helps the buyer when the actual terms are settled by bilateral bargaining anyway. Their answer is that it does: the buyer's equilibrium profit with an iterative tendering stage is at least her profit at the most favorable outcome of bargaining without one. The paper builds on the literature of bilateral bargaining in supply chains with competing suppliers, where the buyer's outside options are endogenous and the order of negotiations matters.
A monopoly buyer (player 0) procures from two suppliers (players 1 and 2) of substitutable products. Write and . The model is described by the following scalars:
The paper's Assumptions 1–2 (a unique interior maximizer of the chain profit, and submodularity) imply and . Each bilateral negotiation is an asymmetric Nash bargaining problem: maximize , where and are the supplier's and the buyer's profits and , their reservation utilities.
Without an RFx (simultaneous bargaining). Supplier 's dual-sourcing profit maximizes subject to and . Here is the buyer's profit when she sources from alone, and is 's profit as exclusive supplier. The most favorable bargaining outcome is the unique solution of
With an RFx. Suppliers quote offers , the profits they demand. The buyer then negotiates with a leader , accepting or rejecting his offer, and afterwards with the follower . Accepting an offer turns it into a reservation utility, so the leader's program [RFx-i] maximizes
over and the buyer's single-sourcing profit . The reservation utilities , are given explicitly on p. 18 for each accept/reject choice. The buyer accepts both offers when no choice of leader, accept/reject decision or negotiated solution gives her more than .
For every pair of nonnegative offers at which the buyer accepts both offers,
and the right-hand side also dominates the buyer's profit at every dual-sourcing equilibrium of simultaneous bargaining.
Theorem 5 is a robustness statement for an everyday procurement practice. Without an RFx, simultaneous bargaining has many equilibria, and is the best of them for the buyer. The theorem says the tendering stage secures at least this best case, whatever the bargaining powers and the substitutability of the suppliers. In the paper's Appendix A instance (, , , ) the gain is strict: the most favorable outcome gives the buyer , the RFx equilibrium . Lemmas 2, 4 and 5 describe how a buyer responds to quotations in a Nash bargaining framework, and that description is reusable for other sequential-negotiation models.
The paper's results are proved in its e-companion. As far as is known, none of them has a machine-checked proof. Formalizing them checks a case analysis over Nash bargaining programs with piecewise-linear reservation utilities and zero-surplus corner cases, which is where informal arguments are easiest to get wrong.
The obvious argument works offer by offer: compute the follower's split, plug it into the leader's program and compare closed forms. It breaks down in two places. First, the buyer's profit in [RFx-i] contains , so the leader's objective is neither concave nor smooth, and its maximizers move between regimes with the offers. Second, accepting an offer can leave zero bargaining surplus. Then every feasible point maximizes the Nash product, and the accept-both characterization has to hold for all of them, not for a convenient one. Comparing with needs a separate argument as well: is defined by a fixed-point system with positive parts, and [Q] has to be shown to have it as its unique optimum.
Fin 2 and offers are nonnegative reals.Real.geom_mean_le_arith_mean2_weighted) for the Nash split, and a case analysis over piecewise-linear constraints. Contributions are welcome in both. A general lemma on asymmetric Nash splits, on , would be reusable beyond this mission.Firms that sell large catalogues of digital goods (streaming titles, cable channels, software features) rarely price every subset of products separately: with products there are bundles. A common simplification is bundle-size pricing (BSP), where the price depends only on how many items the customer takes and the customer picks which items go into the bundle. BSP sits between pure bundling (one price for everything) and full mixed bundling, and its menu has only prices.
Bakos and Brynjolfsson (Management Science, 1999) showed that for many products a pure bundle extracts almost all surplus under suitable concentration. Armstrong (Review of Economic Studies, 1999) showed that a cost-based two-part tariff asymptotically achieves the perfect-price-discrimination profit. Chu, Leslie and Sorensen (American Economic Review, 2011) computed optimal BSP menus numerically for up to five goods. Abdallah, Asadpour and Reed (Operations Research, 2021) develop an asymptotic theory of BSP as . This mission formalizes their homogeneous-cost result: with identical marginal costs, optimal BSP asymptotically earns the perfect-price-discrimination profit.
A firm sells products to one customer with valuations , additive over bundles. Let be the order statistics. A bundle of size is worth to the customer, the sum of her largest valuations, with . The firm incurs a marginal cost for item , so a bundle of size costs , where lists the items by valuation and ties go to the lowest index.
A BSP menu is with , where means size is not offered. The customer buys a size , with the free no-purchase option. The firm's profit is , and the BSP problem is . The benchmark is perfect price discrimination, , the most any selling mechanism can earn.
The large-offering regime describes the valuations as one random sequence :
The normalized curves are and for . The quantile function is .
With identical costs , for every ,
The size fraction maximizes over , and when is a continuity point of . If ,
Theorem 1 is the general principle behind the goal. Suppose and pointwise, with nondecreasing continuous limits, and . Offer the single size at price , where grows faster than but is . Then
The milestones follow the appendix proofs in order:
Theorem 2 says that, with identical marginal costs and enough statistical concentration across products, a menu of size prices earns, to first order, everything a seller who knew each valuation could earn. Theorem 1 says more: one well-chosen bundle size, sold at a price slightly below its fluid value, is asymptotically as good as the optimal BSP menu. The paper's later results on heterogeneous costs (Theorems 3–4), clustered BSP and unknown budgets reuse this framework: Theorem 1 reduces each of them to computing the limit curves and .
The results are proved in the paper and have no machine-checked version. This mission formalizes them under a weak-convergence hypothesis on the empirical distribution, with no independence assumption. The formal statements also fix points the page leaves implicit: the tie-breaking rules, the value of the BSP problem as a supremum, and the case , where the goal's ratio degenerates.
The obvious route to Theorem 2 goes through Theorem 1, as the paper does. That needs a dominating the fluctuation of , and Assumptions 1–2 give no second moments. A proof of the goal must therefore avoid Theorem 1's condition or replace it with a weaker device.
The convergence is a statement about sums of top order statistics of a dependent sequence. Pointwise convergence of the empirical cdf does not by itself control the upper tail, which carries the mass of . The weak law and uniform integrability have to supply that control.
The upper bound (A1) requires exchanging a supremum over with a limit in probability, which uses monotonicity of in and continuity of the limits. The step " for " holds only at grid points , so the off-grid error must be bounded separately.
Everything lives in the namespace LargeBSP.Homog. Items are 0-indexed: coordinate n < N is the paper's item . The valuations are one sequence X : ℕ → Ω → ℝ on a probability space, measurable and nonnegative; the -product model uses its first terms. is cdf ν for a probability measure ν on with and finite mean. "" toward a constant is convergence in probability (TendstoInMeasure); deterministic sequences use Tendsto.
Menus are ℕ → WithTop ℝ, with ⊤ meaning "not offered". Within a bundle size, items are ranked by valuation with ties to the lowest index, as on the page. Among sizes, the customer picks the smallest maximizer of surplus, a disclosed tie-break, so an indifferent customer does not buy. is the real supremum of the expected profit over all menus with prices in . It is bounded by , so it is never the junk value of an unbounded supremum.
The quantile is . Its set is empty only outside , where Lean returns ; every use is at or inside an integral. The set defining is taken over .
Disclosed readings:
The tail condition (6) of the paper is not assumed: neither proof uses it.
The goal cannot be satisfied trivially. is the value of the BSP problem over all menus, not a chosen menu. PPD is the sum of the per-item expectations. The instance , satisfies every hypothesis with , and . So the ratio is neither nor fixed by a degenerate menu.
Needed infrastructure: order statistics of a finite family through a rank function, empirical distribution and quantile functions, the identity "mean = integral of the quantile function", convergence of quantiles under weak convergence (van der Vaart, Lemma 21.2), and uniform integrability of averages. These parts are reusable well beyond pricing. Contributions are welcome on any milestone, and on proofs of the goal that bypass Theorem 1's second-moment condition.
Philosophers of physics use category theory to decide when a formulation of a theory carries excess structure. Weatherall (2016) represents each formulation of electromagnetism as a category of models and the passage from potentials to field strengths as the functor . A functor that is not full forgets structure, one that is not essentially surjective forgets properties, and one that is not faithful forgets stuff. Weatherall's §4 argues on Minkowski space that the potential formulation with gauge transformations as arrows is related to the field-strength formulation by a functor that is full and essentially surjective. His footnote 9 sets topology aside, and the erratum to his Proposition 2 (arXiv v2, p. 15) records that the gauge-theoretic functor is not faithful, because constant gauge transformations act trivially on fields.
On a contractible spacetime these facts all rest on one theorem: the Poincaré lemma, which says closed differential forms are exact. A companion mission (Weatherall 2016: Potentials vs. Field Strengths on a Finite 2-Complex) proves the discrete version, in which fullness, faithfulness and essential surjectivity are equivalent to the vanishing of , and of a cell complex. This mission is the continuum version on a vector space, built on Mathlib's exterior derivative.
Timeline. The explicit radial homotopy operator proof of the Poincaré lemma is standard in textbooks; it is the proof of Theorem 4-11 in Spivak's Calculus on Manifolds (1965). Antiexact forms and the same operator are studied in Kycia (2020). Mathlib has the exterior derivative extDeriv with . In 2025 Kudryashov proved the degree-1 case for convex sets, stated for 1-forms written as E → E →L F with a symmetric derivative. Mathlib has no Poincaré lemma in higher degree, no de Rham cohomology and no Hodge star.
Let be a real normed space, for example , and a real Banach space of field values. A differential -form is a map that assigns to each point a continuous alternating -linear map. Smooth means (ContDiff ℝ ∞). The exterior derivative is Mathlib's extDeriv:
A function is a 0-form, and is its derivative viewed as a 1-form (grad). The radial homotopy operator sends a -form to the -form
Field equations enter through an arbitrary predicate on 2-forms. For example once a metric is chosen, and in vacuum. The categories are:
Fld P (Weatherall's EM1): smooth closed 2-forms with , with only identity arrows.Pot P (EM2 with gauge arrows, fn. 15): smooth 1-forms with . An arrow is a smooth with , and arrows compose by adding gauge functions.fieldStrength P : Pot P ⥤ Fld P: the functor , which sends every gauge arrow to an identity.The cohomology conditions are elementary Props:
For every that admits at least one potential:
So the potential description with gauge arrows forgets only stuff, namely the constant gauge transformations, and nothing else on a vector space.
Four supporting statements isolate the reusable ingredients of Milestone 2:
alternatizeUncurryFin.The result. The goal makes precise, on and with any field equation, the claim behind Weatherall's §4: up to the constants , potentials modulo gauge carry no more information than field strengths. With the discrete mission, it shows that the three ways of forgetting information correspond to , and in both settings. The continuum version is metric-free. Maxwell's equations, sources or any other field equation enter only through , so the classification holds for all of them at once.
Formalizing it. The homotopy formula and the Poincaré lemma for Mathlib's extDeriv in arbitrary degree are not in Mathlib. They are prerequisites for de Rham cohomology of manifolds, for the homotopy invariance of de Rham cohomology, and for any formal treatment of gauge potentials, Chern–Simons terms or Hamiltonian mechanics that uses local primitives. The classical proof is a textbook argument; the remaining work is to formalize it against Mathlib's alternating-map API. Machine-checked versions exist elsewhere only in other representations: Mathlib proves degree 1 for 1-forms written as E → E →L F on convex sets, and this platform's Rudin chapter 10 mission has proved Poincaré's lemma (Rudin, Theorem 10.39) as Rudin.ch10_poincare_lemma and Rudin.ch10_primitive_of_closed, for its own coefficient-style KForm on convex open subsets of . A bridge from those statements to Mathlib's extDeriv would be a welcome contribution.
The obstacle is the homotopy formula in general degree. Each side involves the alternatization alternatizeUncurryFin of a derivative, the insertion curryLeft of the position vector as the first argument, and Fin.removeNth reindexing. Matching the two sides requires the signs from moving an argument to the front to cancel exactly against those of . The degree-1 shortcut through Mathlib's existing curve-integral Poincaré lemma does not generalize, because it uses a different representation of 1-forms and has no analogue in degree 2, which the essential-surjectivity clause needs. A second, routine obstacle is smoothness of : need not be finite-dimensional, so differentiating under the integral needs bounds that are uniform in near each point.
E → E [⋀^Fin k]→L[ℝ] F and the exterior derivative is extDeriv. "Smooth" is ContDiff ℝ ∞, where ∞ means , not analytic. is any real normed space, not necessarily finite-dimensional or complete, and is a real Banach space (CompleteSpace F), so the integral defining is the Bochner integral.Fld P is a Mathlib Discrete category. Pot P has a hand-written Category instance whose arrows are the structure GaugeHom. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.[Nonempty (Pot P)], meaning the field equation has a solution. Without it Pot P is empty and faithfulness and fullness hold vacuously. The cohomology conditions are explicit statements about extDeriv and grad, not definitions that make a target hold by construction. The goal fixes nothing about .extDeriv, in the form used here, and the gauge invariance . The homotopy operator, the homotopy formula and the Poincaré lemma are stated for arbitrary degree and are intended for reuse in de Rham and gauge-theory missions. Contributions toward a Mathlib-quality homotopy-operator API are welcome.MeasureTheory/Integral/CurveIntegral/Poincare.lean (Poincaré lemma for 1-forms on convex sets), mathlib4 PR #24019.A computable measure of entanglement establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be positive integers, and fix an orthonormal product basis of . For a matrix on this space, let denote its partial transpose on the first subsystem, so that . Write and . Let be any finite family of Hermitian matrices on this space, and let be nonnegative real numbers with . Then
This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives outside the state domain.
Let be positive integers, and fix an orthonormal product basis of . For a matrix on this space, let denote its partial transpose on the first subsystem, so that . Write and . Let be any finite family of Hermitian matrices on this space, and let be nonnegative real numbers with . Then
This expresses convexity of negativity under mixing, a property used in the paper's subsequent study of entanglement monotonicity. As in the printed proposition and its proof, the matrices need not be positive or have trace one; the displayed definition therefore gives outside the state domain.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let be a Hermitian matrix on a positive finite-dimensional space. There exist density matrices and such that
Their coefficient sum is no larger than that of any other such decomposition. Eigenvalues are counted with multiplicity. This is an attained variational characterization, valid also for .
Let and be bipartite density matrices. Regroup their product as , and define . Then
All four local spaces are finite and nonempty. This additivity concerns logarithmic negativity.
There exist two density matrices and on two qubits for which
Thus logarithmic negativity is not convex. This states only the nonconvexity clause; the source's subsequent inference about LOCC increase is deferred separately.
Fix a finite adaptive LOCC protocol before a bipartite density matrix is supplied. Local instruments may change finite dimensions, add ancillas, discard systems, and choose later operations from prior outcomes. After any fixed classical coarse-graining, let be its subnormalized outputs, , and for . Then
Zero-probability outcomes contribute zero. This is the selective entanglement-monotone inequality.
Let be a compact convex set of Hermitian trace-one matrices whose real span is the full Hermitian space. Define and as the infima of and over , where and . These sets are nonempty and bounded below. The first functional is a norm on Hermitian matrices; is convex and nonnegative. Moreover,
Members of need not be positive. The statement includes definiteness, the triangle inequality, and absolute homogeneity of the norm.
For a density matrix on positive finite local spaces, let and use the variational base construction with separable states and PPT states, respectively. Then
Furthermore, exactly when is separable; and each hold exactly when . These zero sets distinguish the measures. The phrase “in general” is not a universal strictness condition.
Fix a finite adaptive LOCC protocol with arbitrary positive finite input and output dimensions, including a fixed final classical recording map. For input density matrix , write and for its probabilities and normalized positive-probability conditional outputs. Then both
The two robustness measures are defined by their actual separable and PPT bases. This retains selective, rather than only deterministic, monotonicity.
For any finite deterministic LOCC protocol and any bipartite density matrix ,
Here sums all subnormalized leaves after forgetting the transcript; input and output local dimensions may differ. This is the deterministic monotonicity asserted in the introduction and supported by §II.
Let and let be a state on . Let be its standard maximally entangled state, and let be the infimum of over deterministic LOCC protocols . Then
The trace norm is unhalved. No optimal protocol is assumed to exist.
Let and let be an bipartite density matrix. For a deterministic LOCC teleportation protocol , let map Alice's unknown input state to Bob's output. Define by taking the infimum over of the Haar average of . Then
The protocol is fixed before the unknown input. This optimized equality is the numbered result adapted from reference [27].
Let be a finite bipartite density matrix and . Define achievable nonnegative rates using the source's universal condition on diverging integer sequences: counts input copies, output Bell pairs, and requires . The supremum is taken in the extended nonnegative reals. Then
The case is included. The input/output letter interchange near Eq. (41) is resolved by Eq. (43) and the proof.
Let be a Schmidt expansion, where the two vector families are orthonormal, , and . For ,
Coefficients are amplitudes, not squared eigenvalues; zero padding and rectangular local spaces are allowed. The robustness identification retains the source's attribution to [18].
For normalized Schmidt data , with , write and . Its entropy in bits satisfies
Zero coefficients contribute zero. Equality holds if and only if every pair of nonzero coefficients is equal. This includes rank-one product states and maximal entanglement on a proper Schmidt support.
Let , let swap the two -dimensional factors, and let be the maximally entangled projector. Choose real so that is a density matrix. Set and . Then
This computes the measure on the actual family (51), including .
For a density matrix as in Eq. (51), put and . Then
Both robustness quantities retain their variational definitions. The background coincidence of PPT and separability is specific to this family and is attributed by the source to [22].
Let be a positive definite physical two-mode covariance matrix, so are real symmetric matrices and . Use with , and let reverse Alice's momentum. Then
The polynomial's plus sign is retained; its roots occur as imaginary symplectic pairs.
Correction to the printed source.
Printed: PDF p.9 prints the standard block [[0,1],[1,0]] and describes the roots near Eq.(64) as real pairs.
Corrected: Use J=[[0,1],[-1,0]], explicitly in symplecticTwo and the covariance hypothesis; preserve every coefficient of Eq.(64).
Reason: Eq.(54) explicitly requires an antisymmetric symplectic form; the preceding normal-mode paragraph gives imaginary eigenvalue pairs. At the physical vacuum gamma=I/2 the characteristic polynomial is (X^2+1/4)^2. The symmetric printed block would give (X^2-1/4)^2. This is the minimal sign repair consistent with the source's commutation convention.
For a tripartite density matrix, let , , and . For every finite adaptive LOCC protocol acting on the three separated parties, with normalized positive-probability outputs and probabilities , all three grouped negativities obey
All regroupings are computed from the same state. Local dimensions may change, and a fixed final coarse-graining is allowed. The other three functions in threePartyMeasures are reduced-state negativities defined by the source for a noncooperating discarded party; this theorem makes no monotonicity assertion about them under three-party LOCC.
For a four-party density matrix , form and . Then
and the same two inequalities hold for . These compare the measures and hence their distillation upper bounds. They do not compare actual optimal rates of different distillation tasks.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Fast and fault-tolerant logical measurements: Auxiliary hypergraphs and transversal surgery.
Let be finite based chain complexes over , and let . Their tensor complex has differential . There exists an -linear isomorphism
The direct sum is algebraic; the finite based complexes have only finitely many nonzero graded components. No particular isomorphism or representative map is asserted.
Let binary check matrices satisfy , and let be the prescribed pair-reading matrices of Eq. (2). Write and . Then
The deformation of two identical memories therefore retains exactly logical qubits, with no additional logical classes. All spaces and isomorphisms are over .
Let and satisfy , and let . In the product bases, the three coboundaries of the pair-reading deformation are
Here old data precede new data, and old Z checks precede new Z checks; denotes the metachecks. These are the explicit tensor-product differentials, retaining the final degree as in pp.21-22.
Let define a binary CSS memory with X and Z distances at least . Its prescribed pair-reading deformation has check matrices satisfying
A lower distance bound quantifies over every nontrivial normalizer class modulo stabilizers; the distance is infinite when no such class exists. This is a spatial code-distance assertion.
Let define a binary CSS memory with both distances at least . Let have full row rank and every row of Hamming weight greater than one. The prescribed Z-pattern deformation of identical memories, with new data qubits indexed by pattern rows and memory X checks, satisfies
The conclusion includes CSS commutation and every nontrivial logical class. Sparsity belongs to the separate resource claim.
Let be a finite incidence matrix, , and its support union. Put , where restriction to is zero extended and bars denote Hamming weight. For , suppose for every binary vector . Let the integer satisfy , and form , with the path incidence on vertices. At any selected level , embed as . Then
Thus the thickening has certified modular expansion at least one at every choice of a single level. Cut certificates avoid asserting a largest finite expansion on degenerate inputs.
Let be finite, let contain , and let . Let be the support union of , and let , using zero-extended restriction and Hamming weight. Then
Hence is a certified modular-expansion lower bound, even when no largest finite expansion exists.
Let be finite and . For an integer , form . Embed at any one level as , and write for its support union. Then
Restrictions are zero extended and weights are Hamming weights. Integer -fold thickening thus certifies modular expansion one.
Let satisfy , defining a self-dual CSS code with . Let isometrically encode all logical qubits onto its entire codespace. Suppose matching binary supports satisfy , and their physical X and Z products implement the corresponding logical through . There exists a physical Pauli correction , independent of the encoded state, such that
Here , and includes its Pauli phase. The matrix equality holds on the entire encoded space, implementing S on every logical qubit.
Let have finite nonempty vertex and edge sets, with every column weight at most . Let and . Write for the modular cut inequality using the support union of , and let indicate . Then
If , the relative inequality at is equivalent to global expansion . If also the support union of is all of , then
The last inequality, with locality , is classical soundness . The support condition implements the source's explicit specialization.
Let be a chain map of finite based binary complexes and . Let be its induced homology map. Then
All dimensions are over , and map images are constructed from . The addition form avoids truncated subtraction of natural dimensions.
Let be a finite binary CSS complex supported in degrees , and let be the repetition length. Let , and let be its prescribed two-endpoint cone. Let and be the cochain-oriented bulk and cone obtained by the specified degree-reversing dual constructions. Put and . Then
These retain all boundary homology classes, including immediately terminating classes. They imply no operational fault-distance bound by themselves.
Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.