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?
Online marketplaces such as Amazon are both the storefront of third-party sellers and a retailer in their own right. A platform that observes how well a seller's product sells can later launch a competing product in the same space, and empirical work finds that it does so selectively: Zhu and Liu (2018, Strategic Management Journal) report that Amazon is more likely to enter product spaces with high sales and ratings. A seller who anticipates this faces a strategic choice about how much to invest in her product before the platform decides.
Qi, Song and Xiao (Management Science, 2025) model this interaction as a two-stage game and ask how the seller's investment responds to the threat of entry. Their answer depends on whether the seller ultimately benefits from the platform's entry, which can happen through spillovers: the platform's own investment in the product space also raises the value of the seller's product. This mission formalizes the case in which the seller does not want the platform to enter, the protective regime, and the paper's characterization of her optimal effort there (Proposition 3).
The parameters are a degree of spillover , a referral rate (the share of the seller's revenue paid to the platform), a competition intensity , the seller's effort-cost coefficient , and the platform's fixed entry cost . The platform's own cost coefficient is normalized to .
In the first stage the seller's product has base value ; she chooses an effort at cost , raising the value to , and sells a quantity at price , keeping the fraction of revenue. In the second stage the platform, having inferred , decides whether to enter. If it does, it invests in the product space and the two compete in quantities.
The paper reduces the second stage to closed forms. Write for the left side of condition (5),
which says that the seller stays in the market after entry and is assumed throughout. With an explicit polynomial denominator , set (equation (8)). The seller's two-stage profits under non-entry and entry are
The platform enters iff the product value exceeds a threshold , where is a second explicit polynomial in (Proposition 1). Hence the seller's total profit is
The protective regime is ; there for every effort. The benchmark efforts and , equations (9)–(10), maximize and respectively.
In the protective regime, with defined by , there is such that an optimal effort is
and the optimal first-stage quantity is .
The result identifies strategic underinvestment as the seller's response to an unwelcome entrant: for intermediate base values she chooses less effort than her first-best so that the product's value sits exactly at the entry threshold. For low base values no distortion is needed, and for high ones the required distortion costs more than entry does. This explains why a seller's investment may fall short of what her own costs and demand would justify, and it is the starting point of the paper's analysis of non-entry commitments (Proposition 5).
The result is proved in the paper; nothing here is open. No part of it is formalized. A machine-checked version adds a complete check of a proof that compresses several steps into "verifiable" remarks: the positivity of and the sign of under (5), and the single sign change of that defines .
The seller's objective is discontinuous at , so the first-order condition alone does not locate the optimum: the candidates are the two unconstrained maximizers and the cutoff, and which one wins depends on . The step that needs care is the existence of a single switching point : it requires comparing the value of the constrained non-entry problem with the unconstrained entry optimum as a function of , and showing that the comparison changes sign once. The polynomial sign facts behind , namely and on the parameter box under (5), are elementary but involve quartic polynomials in three variables.
All quantities are real numbers. The standing ranges , , are hypotheses, as are condition (5) (assumed by the paper from p. 12 on) and (not stated by the paper, but presupposed by its formula for ; with the threshold degenerates to 0). Only the branch of and for which (5) holds is formalized; the paper's proof also covers the regime where (5) fails, with .
The closed forms (6), (7), the entry gain and are definitions taken from the paper. Their derivation from the second-stage Cournot game (Lemmas 1–2) is the subject of the companion mission On the Platform’s Entry I. The piecewise profit is the printed one, with the tie assigned to non-entry.
Efforts range over all of . This is the paper's implicit domain and it matters: the optimal effort is negative for some parameters (for instance , , and slightly above ), so a version restricted to would be false. "Optimal" means a global maximizer, with ties allowed; at two efforts are optimal and at the middle interval is empty.
Trivializing formalizations are ruled out: is pinned by its defining equation rather than chosen, every hypothesis is satisfiable (at , one has ), and the sign conditions keep from collapsing to a junk value of division or square root.
A complete development needs only real analysis of quadratics and polynomial inequalities on a box; contributions of reusable lemmas on maximizing concave quadratics under a threshold constraint are welcome.
A portfolio manager who observes side information (a covariate , such as a market indicator) before choosing a portfolio wants to control the loss of the asset returns conditional on the observed covariate value . The conditional law of given is unknown and must be learned from historical pairs . When itself was never observed, the empirical conditional law is undefined, and kernel or nearest-neighbour estimates are fragile. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research, 2025) robustify the conditional decision with an optimal transport ambiguity set: the decision maker hedges against every joint law of within transport distance of the empirical law. The resulting objective is a ratio of two linear functionals of , so the standard Wasserstein distributionally robust duality (Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) does not apply directly.
The paper settles every regime of the three parameters (ball radius , fiber radius , minimum fiber mass ). This mission formalizes the simplest regime, , where the answer is negative: the worst case does not depend on the data at all.
The covariate space and the return space are Polish spaces with their Borel -algebras. Two ground costs and combine into the separable cost . The data define the empirical measure .
The optimal transport cost between two probability measures on is
the infimum over couplings with marginals and . The ambiguity set is the ball .
Given a covariate value and a radius , the neighbourhood is , and is the fiber set. For a loss at a fixed decision and a law with positive fiber mass, the conditional expected loss is
The paper's standing Assumption 2.4 requires: (i) and are symmetric, non-negative and continuous, and vanishes exactly on the diagonal; (ii) every has a unique projection onto ; (iii) every boundary point of has points outside at arbitrarily small cost.
With the fiber is . With the fiber-mass constraint is taken as the strict inequality , so that the conditioning event is never null.
For every , every and every loss ,
both sides in .
The proposition shows that conditioning on a single covariate value with an optimal transport ball is uninformative: the worst-case conditional loss equals the robust optimization value for every data set. This is what motivates the rest of the paper: either a minimum fiber mass (Theorem 3.2) or a fiber of positive radius (Section 4) is needed for the data to matter. The paper contrasts this with the type- Wasserstein ball, for which it points to existing results to compute the worst case.
For the platform, the mission sets up the shared model of the series: the separable ground cost, the empirical measure, the fiber, the conditional expectation as an extended-real ratio, and the paper's Assumption 2.4. The ball representation (milestone 1) is used by every other mission of the series; it rests on the existence of optimal couplings on Polish spaces, which Mathlib does not yet have. The result is proved in the paper; no machine-checked proof is known to exist.
The statement is an equality of two suprema over very different index sets, and neither inequality reduces to the other. The natural first idea, that the worst case is attained by a small perturbation of the empirical measure, fails: the empirical measure may put no mass on the fiber , or put its mass there at returns far from where is large, and the value must be reached for every data set. Points of the data sitting exactly at are the delicate case, since the transport budget charges for every displacement of mass. The ball representation (milestone 1) is the hard infrastructure step in its "only if" direction: it needs an optimal coupling, i.e. attainment of the transport infimum on Polish spaces, which is absent from Mathlib.
Samples are indexed by Fin N with . The ground cost is as a -valued function. The transport cost reuses the published RWPI.SqrtLasso.transportCost, an infimum over couplings whose first marginal is and second marginal is ; the paper's "min" is not built into the definition. The radius enters as ENNReal.ofReal ρ, and the goal assumes as on the page (). Expectations use the published ModelRiskOT.Duality.extIntegral, in , so the loss is arbitrary: no measurability, boundedness or integrability. The loss stands for at an arbitrary fixed decision, which is how "for any feasible " is read. The fiber at is ; that it equals follows from Assumption 2.4(i). The boundary in Assumption 2.4(iii) is the topological frontier in .
One hypothesis is added to the paper and disclosed: is not isolated for (for every some has ). This is Assumption 2.4(iii) at when the boundary of is read in an ambient Euclidean space, as the paper's remark on p. 11 does; the proof uses it, and without it the statement fails at an isolated that is also a sample point.
Trivializing encodings are excluded: the supremum ranges only over probability measures in the ball with strictly positive fiber mass, so the conditional expectation is never evaluated at a null fiber; no Bochner integral (which is for a non-integrable loss) is used; cannot enter through ofReal; and the feasible set is exactly intersected with the positive-mass constraint.
Contributions welcome: the existence of optimal couplings for lower semicontinuous costs on Polish spaces (reusable far beyond this mission), the decomposition of couplings with a finitely supported marginal, and the two halves of the goal.
Ride-hailing platforms are expected to add autonomous vehicles (AVs) to fleets that today consist of human drivers. AVs have a cost advantage: a human driver must earn a reservation wage for every hour on the platform, while an AV owner pays a fixed capital cost per calendar hour and a smaller variable cost per operating hour. Whether that advantage reaches riders as lower prices depends on how the market is organized: who owns the AVs, and whether AVs and human drivers are dispatched on the same platform.
Z. Lian and G. van Ryzin study this question in Capturing the Benefits of Autonomous Vehicles in Ride-Hailing: The Role of Market Configuration (Management Science, 2025). This mission formalizes one of their central results: when a single AV supplier (a monopoly) shares a common platform with perfectly elastic human-driver supply, its choice of AV capacity is a newsvendor problem, and the optimal capacity is the pure human-driver fleet size of the scenario at a critical fractile of the demand distribution. The version formalized here is the authors' 2023 SSRN working paper (abstract 3716491, version of 23 August 2023); all theorem and equation numbers refer to it, not to the published article.
Vehicles and demand. Riders' values for a ride-hour are uniform on . In a scenario with potential demand mass , serving the demand rate requires the price , and generates the revenue , where is the trip time. Pickup times depend on the number of open vehicles through with and . Minimizing over gives the minimal fleet needed to serve ,
and the maximal utilization . The function is a strictly increasing bijection of ; its inverse is the largest demand that vehicles can serve.
Human drivers (HVs). In this mission HV supply is perfectly elastic at reservation earnings per hour (the paper's ). A demand rate is a pure-HV equilibrium when revenue covers the minimal HV cost, ; among stable equilibria the paper selects the largest, the maximal stable equilibrium , with fleet size . The market is loose when .
AVs. AVs cost per operating hour and per calendar hour, and (Assumption 1). On a common platform, the paper shows (Proposition 6) that the variable profit per AV at fleet size is
Scenarios and the monopoly problem. Demand has scenarios with masses and probabilities . The monopoly chooses a capacity , then a fleet in each scenario:
Let be the smallest index with . In a loose market,
is an optimal capacity for (5).
The result. Proposition 8 says that, on a common platform with elastic human-driver supply, a monopoly AV supplier never undercuts the human drivers' price: in every scenario it deploys at most the pure-HV fleet size, so riders pay the pure-HV price, and the whole cost advantage is retained by the supplier. Its capacity is set by the classical newsvendor trade-off between the margin of a used AV and the fixed cost of an idle one. With a cheap fixed cost the supplier covers the peak scenario; with an expensive one it covers only the lowest scenario and lets human drivers serve the rest. These conclusions drive the paper's policy comparison of market configurations.
Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version exists. A complete development requires the analysis of (real powers with exponent ), the identification of the maximal stable equilibrium under the loose-market condition, a monotonicity argument for the AV-only profit along the inverse , and the discrete newsvendor argument over a piecewise-linear concave objective. The last part is reusable for any discrete-scenario capacity problem.
The newsvendor step is elementary once the objective is in the form (20). The work lies in reaching (20) from (5). That requires, in each scenario, showing that the maximum over of is attained at . Below this is linear growth; above it, the profit is a function of , an inverse of a sum of a fractional power and a linear term with no closed form, and its decrease rests on the loose-market condition placing beyond the revenue-maximizing demand . Without the loose-market condition the claim fails: in a thin market the only equilibrium is , and the supplier's AV-only profit need not decrease past it. The continuity of at uses the equilibrium identity , which itself depends on identifying the maximal stable equilibrium.
Fin I (0-based): the paper's scenario is index , is a sum over indices strictly above , and "the smallest " is IsLeast.IsMaxStableEq on given numbers , not a choice function.Retail chains increasingly run their physical stores and online channels as one network. A customer who walks into a store and finds nothing she wants can be shown products stocked in other stores of the chain, to be shipped or picked up later. This raises a basic assortment question: when every store can point its customers to the rest of the network, should the stores still carry the assortment each would choose on its own, or should they coordinate?
Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing the network's products. Under simultaneous recommendation (SMR), a customer sees her store's products and the other stores' products at the same time. Under sequential recommendation (SQR), she sees the other stores' products only after declining everything in her own store. This mission formalizes the paper's result for SMR, Theorem 1, together with the lemmas of its proof and two consequences (Theorem 5(a) and Proposition 2). The single-store model it builds on is the multinomial logit (MNL) assortment problem of Talluri and van Ryzin (2004).
A seller operates stores and sells products, indexed , with revenues . Product has attraction value , where is its utility; the no-purchase option has attraction value . A fraction of customers first visits store , and .
An assortment profile lists the set offered by each store. Write for the products offered somewhere. A customer of store who buys product from store suffers a utility discount , with . She buys from the cheapest store that offers , so the effective discount is , and if no store offers .
Under SMR, the customer of store chooses product with the MNL probability
The seller's problem is
The single-store problem is
An assortment is revenue-ordered if it is for some . The paper writes for the smallest revenue-ordered optimal solution of (3).
Offering the single-store optimal assortment in every store is optimal under SMR. The goal asserts optimality, not uniqueness: with ties, other profiles can be optimal too.
Theorem 1 says that under simultaneous recommendation the network adds nothing for the seller: the revenue of independently run stores, , is the best achievable. The paper calls this revenue the benchmark. Every later comparison is made against it. The sequential strategy beats it (Theorem 5(a)), and the paper's structural results on SQR and its ½-approximation are phrased relative to and . Proposition 2 shows that adding an online channel enlarges the optimal assortments of the physical stores.
The results are proved in the paper, partly in an Additional Supplement. As far as is known, none of them has a machine-checked proof. The mission produces a reusable Lean model of multi-store MNL choice with cross-store discounts, the SQR choice probabilities, and checked proofs of the single-store threshold structure with discounted outside products (Propositions A.1 and A.2).
A store's SMR revenue depends on every other store's assortment, through both the denominator and the products of . The objective does not separate across stores, so the obvious idea of optimizing each store on its own does not directly apply. Products of other stores enter at reduced weight , so the standard MNL result for (3) does not cover (A.1).
Proposition A.1's exchange argument has two cases, depending on whether the added product is already available elsewhere. In the second case the gain is weighted by , which vanishes when . Proposition A.2 compares optimal values across two discount vectors whose optimal assortments differ.
Products are Fin n (the paper's product is index ), stores are Fin m, and a profile is a function Fin m → Finset (Fin n). The attraction values are the primitive parameters. The discount factor is the largest over the offering stores, and when none offers . In (A.1) the discounts are encoded by the factors , with for . and are predicates: revenue-ordered (hence nonempty), optimal, and of least cardinality among revenue-ordered optima. "Optimal" means a global maximizer, and comparisons of optimal values are written as "for every there is an with ", with no maximum operator. The SMR and SQR objectives are written from the choice probabilities (1) and (2), exactly as the paper writes them.
The standing assumptions are explicit hypotheses: , , strictly decreasing, , , . Two hypotheses are pinned. The first is : revenues are prices, which the paper uses but never states as a sign condition. The second applies only to the second part of Proposition A.1: , because its "if and only if" fails at ; the existence of a revenue-ordered optimum is stated for every . The goal and Proposition A.2 keep , so zero cross-store discounts are allowed. The Gumbel derivation of (2) (Proposition 1, cited from Gao et al. 2021) is not formalized; (1) and (2) are the model.
The hypothesis on is satisfiable: its existence is the first milestone. A statement that assumed some optimal profile, or that defined through a junk-valued supremum, would be trivial or vacuous, and the formalization avoids both. Contributions are welcome on any milestone. Propositions A.1 and A.2 are reusable for other multi-store and omnichannel MNL problems.
Small third-party sellers on e-commerce marketplaces often lack working capital to buy inventory. Two financing channels compete for them. Under trade credit, the supplier ships now and is paid after sales, bearing the seller's default risk. Under platform financing, the marketplace itself (Amazon Lending, Alibaba's microloans, JD's supply-chain finance) lends the seller the purchase cost at an interest rate it chooses, the supplier is paid upfront, and the platform bears the default risk. A platform that already earns a commission on every sale has a reason to lend that a bank does not: cheaper credit raises orders, and higher orders raise commission income.
R. Huang, G. Lai, X. Wang and W. Xiao study this in Platform Financing vs. Trade Credit for Lending to Third-Party Sellers (Management Science, 2024). Their §5 asks how a platform that can set its loan rate freely would set it. The answer at low demand uncertainty is a clean dichotomy in the production cost: the platform lends at exactly its own capital cost when cost is low, and strictly below its capital cost, subsidizing the loan, when cost is high. This mission formalizes that result, Proposition 8, together with the equilibrium analysis it rests on.
The source is the authors' manuscript on SSRN (abstract 4014045, titled Lending to Third-party Sellers with Platform Loan); every page and label below refers to that manuscript, not to the typeset journal article.
A seller with no capital buys units from a supplier whose unit production cost is , and sells all of them on a platform at the market-clearing price . The market size is uniform on with ; measures demand uncertainty. The platform keeps a share of revenue and passes to the seller. The supplier and the platform both have capital cost equal to the risk-free rate , and selling is profitable in expectation: .
Under platform financing at loan rate , the game has two stages after is fixed:
The seller has limited liability: if revenue falls short of the debt , she hands over all of it. The platform's profit is
A subgame-perfect equilibrium at rate is a price and an order rule such that the rule is a best response for the seller at every price, the supplier's price is optimal against the rule, and ties are broken as in the paper. The paper also defines a threshold rate (p. 15) below which the seller prefers platform financing to trade credit; the platform chooses subject to the participation constraint . Write
Let be the platform's profit in a subgame-perfect equilibrium of the stage game at rate , for an arbitrary choice of equilibrium at each feasible rate. If , then
The result separates two motives for platform lending. At low cost the platform gains nothing by undercutting its own capital cost, so the loan is priced at cost; at high cost the commission earned on the extra units ordered outweighs the interest forgone, so the platform subsidizes. The threshold is explicit and depends only on the mean market size, the commission share and the risk-free rate. Together with Proposition 7 of the same paper (whether the platform gains relative to trade credit), it is the paper's account of why marketplaces lend below market rates.
The proof in the paper is a chain of closed-form computations whose final steps are stated as "it can be verified". A formalization checks that chain end to end: the equilibrium of a limited-liability Stackelberg game with uniform demand, the reduction of the platform's objective to (10), and the sign analysis of . To our knowledge none of these steps has been machine-checked. The model file (uniform expectation, limited-liability payoffs, the equilibrium predicate with tie-breaks) is reusable for the two sister missions on the same paper and for other supply-chain-finance models with a uniform market-clearing price.
The objective is defined through an equilibrium, not a formula. The obvious approach, substituting the closed forms of Proposition 2 into the platform's profit, presupposes that every equilibrium has those closed forms; establishing this means solving the seller's piecewise problem (whose objective changes form where default becomes possible), then the supplier's problem over a piecewise best response, and handling the indifference point . Only then does the problem reduce to the one-variable function (10).
On that function, the low-cost case requires a polynomial inequality on a half-open interval in four parameters, and uniqueness needs strict monotonicity, not just a nonnegative derivative. The high-cost case requires both a single sign change of a cubic on and the existence of a maximizer on a set that is open at , where the profit tends to .
All objects live in the namespace PlatformFinance.EndogRate. Conventions committed to:
Corrections relative to the page: (10) is printed under the heading "the equilibrium profits under trade credit" on p. 35, a slip for platform financing; Proposition 8 states while its proof writes , and the statement follows Proposition 8.
A trivializing formalization is ruled out: the goal is stated about the platform's equilibrium profit, not about the closed form (10), and the high-cost clause asserts existence of a maximizer so that "every maximizer is below " cannot hold vacuously.
Needed infrastructure: interval integrals of piecewise polynomials, optimization of one-variable piecewise functions, and real-polynomial sign arguments. Proofs of any milestone are welcome, as are alternative proofs of the cubic sign analysis.
Large asset managers now hold significant stakes in many competing firms at once. When the same investor owns shares in rival firms, managers who weigh that investor's interests have an incentive to compete less hard, which raises industry profits at consumers' expense. This "softening of competition" effect is the subject of a large empirical and antitrust literature (see Azar, Schmalz and Tecu, Journal of Finance, 2018, and the review of Schmalz, Antitrust Bulletin, 2021). A natural question is then why common ownership is not complete: if buying stakes in rivals raises profits, why does an investor not buy the firms outright?
Denicolò and Panunzi (ECGI Finance Working Paper 927/2023; Management Science, 2025, doi:10.1287/mnsc.2023.03467) answer this with a corporate-governance cost. Common ownership is acquired from blockholders who monitor management; as a blockholder sells, his residual stake shrinks and so does his incentive to monitor, so managers appropriate more of the profit. The equilibrium level of common ownership trades off softer competition against weaker monitoring. The mission formalizes the paper's comparative statics of that trade-off with respect to the two corporate-governance parameters.
Two symmetric firms each have a blockholder owning a fraction of the shares; dispersed shareholders own the rest. A financial investor buys the same stake from each blockholder, who keeps the residual stake .
Each firm's manager diverts a fraction of the firm's profit unless monitored. A blockholder's monitoring cuts the diversion to at a private cost per unit of profit, with , , . Given , the blockholder chooses to maximize
and an optimal monitoring rule is a maximizer over for every . In the specification studied here the cost is quadratic, with .
Managers maximize their own firm's profit plus a weight on the rival's profit, where the common-ownership weight is
and measures the investor's influence on managers. Equilibrium industry profit is for a function of determined by the product market.
The large shareholders' payoff per unit of profit is
and their joint surplus is . An equilibrium level of common ownership is a stake that maximizes over .
With the quadratic cost, the equilibrium level of common ownership is monotonically decreasing in and monotonically increasing in :
for every equilibrium at each parameter value. The statement fixes no product-market model: it holds for every positive industry-profit function of .
A companion pair covers the §7.1 variant in which the blockholder himself diverts profits at a quadratic deadweight loss : the optimal diversion (46) and Proposition 9, which states that equilibrium common ownership is increasing in .
Both and measure the quality of corporate-governance institutions: lower values mean fewer opportunities to divert profits and cheaper monitoring. Proposition 3 shows that the two act in opposite directions on common ownership. Stronger legal protection of shareholders (lower ) raises common ownership, while cheaper monitoring (lower ) lowers it. The paper uses this to argue that improvements in governance may have contributed to the rise of common ownership, and that policy aimed at governance has consequences for product-market competition. Proposition 2 gives the bound that makes the comparative statics meaningful: the investor never acquires the blockholders' entire stakes.
The results are proved in the paper by a first-order argument on an interior optimum together with a separate argument for jumps between interior and corner equilibria. No machine-checked version exists. A formalization makes the statement precise in two respects the paper leaves implicit: it holds for every equilibrium, including ties between an interior and a corner maximizer, and for every positive industry-profit function, independent of the product-market model. Along the way it records a slip in (A4), where the constant is rather than the printed ; the paper uses only its sign.
The paper's argument differentiates the first-order condition of an interior optimum and treats jumps of the equilibrium separately through the sign of . Implicit differentiation alone does not give the result: the surplus is not concave in (it can have two local maxima, one at ), the equilibrium need not be unique, and it jumps. A proof for every equilibrium therefore has to compare global maximizers at two parameter values directly rather than follow a differentiable selection.
A second difficulty is that the surplus is built from the optimal monitoring rule as a maximizer, not from its closed form: the step from the optimality predicate to the formula (21) must be proved before any algebra on is available. For Proposition 2 with a general cost, the optimal rule is only implicitly defined, and the comparison near involves a first-order gain in monitoring against a second-order loss in industry profit.
All objects are real-valued. Stakes range over and monitoring over ; an optimal monitoring rule is a function constrained only on residual stakes . An equilibrium is a maximizer of the joint surplus on , ties allowed, and monotonicity is weak and asserted for every pair of equilibria. Derivatives are stated with HasDerivAt, except in the sign milestones, where deriv appears only inside strict inequalities.
Standing assumptions, all explicit hypotheses: and (pp. 7–8); ( is a fraction; is a disclosed pin, needed for the part); (footnote 19's form of ); on , one for both parameter values (industry profit does not depend on and ). Proposition 2 assumes twice continuously differentiable with on (the paper says convex but divides by ), and differentiable at with . The companion assumes , which keeps the optimal diversion inside .
The model is the weight (17), the monitoring stage of §3.2.1, and of (13)–(14), and the industry-profit function . Proposition 1 (the bargaining reduction from the investor's offers to the maximization of the joint surplus) and the product-market game itself are not formalized: equilibrium ownership is defined, as in §4.2, as a maximizer of the symmetric surplus, and is arbitrary, so the theorem covers every product-market model of §3.1.3. The paper's derivation of from the product-market conditions is not posed; in milestone 3 that sign is a hypothesis. §4.2's remark on the concavity of the joint payoff is not assumed.
Two trivializing formalizations are ruled out: the surplus is never typed with the closed form of (monitoring is any optimal rule, and milestone 1 is the bridge), and industry profit is required to be positive, since would make every stake an equilibrium.
The development needs only elementary real analysis: one-variable optimization on intervals, derivatives of rational functions, and a comparison of maximizers at two parameter values. A general monotone-selection lemma for functions with strictly increasing differences on an interval would be reusable beyond this mission. Proofs of any milestone, and alternative arguments for the goal that avoid the interior/corner case split, are welcome.
Data brokers sell information about consumers to firms that decide whom to target: a lender deciding whom to offer credit, a retailer deciding whom to mail. Two products dominate this market. A marketing list sells contact information together with an analysis, so that a firm cannot reach the consumer at all without buying. A data append adds information about consumers the firm already knows, so that the firm can act even without buying. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how a monopoly data seller should design a menu of data products when the buyers' targeting costs are private, and shows that the answer differs sharply between the two products.
This mission formalizes the data-append result in the paper's base model with a binary targeting value: Proposition 3 (p. 13 of the author's manuscript). The companion missions of the series cover marketing lists and the general model with a rotation-ordered family of posterior distributions.
A marketer can take an action at cost . The action yields a value , with with prior probability , so the prior mean is . Not acting yields .
The seller can produce a signal with , where the informativeness is chosen from . The signal probabilities are and , and the posterior means after and are and , computed by Bayes' rule. The standing assumption makes acting worthwhile exactly after the high signal, so a marketer of cost values information at . Serving a marketer with informativeness costs the seller , with and increasing.
Marketers have cost with probability and with probability , privately known. The seller offers a menu of two plans and with fees . Type 's payoff from plan is
With data appends, a marketer who buys nothing can still act on the prior, so its outside option is . The seller maximizes subject to () and (). An optimal menu solves this problem; its informativeness levels are .
The benchmark is the seller's problem when costs are observable: for each type it maximizes over . Any maximizer is an efficient informativeness .
When :
The first claim is an equality of sets: the high-cost informativeness levels of optimal menus are exactly the efficient ones at . The inequalities hold for every optimal menu and every efficient .
The result says that a data seller's distortion depends on the product's form. With marketing lists the low-cost marketers are the high type, their plan is efficient, and the high-cost plan is distorted (Proposition 2, p. 11). With data appends and costs below the prior mean, the outside option falls with faster than the value of information does, so high-cost marketers have the larger willingness to pay. The roles of the types switch, the low-cost plan is distorted, and the direction of the distortion is reversed, giving the paper's "double mirror image" (p. 13). The direction is set by the skewness of the prior through the sign of , not by an assumed single-crossing condition.
The result is proved in the paper, in an appendix argument of a few lines that invokes Topkis's monotonicity theorem. To our knowledge it has no machine-checked proof. Formalizing it makes explicit what the printed proof leaves to the reader: that the constraints dropped in (8) hold at its optimum, that the efficient and optimal informativeness need not be unique, and which regularity of the strict inequalities need.
The obvious argument substitutes the binding constraints, compares first-order conditions, and invokes Topkis's theorem. Three steps of it are not automatic. First, the reduction drops , and the nonnegativity of fees; these must be shown to hold at every maximizer of (8), and holds only because the maximizers of (8) are ordered in the right direction, which is itself a comparative-statics fact. Second, the reduction identifies the optimal menus only if (8) attains its maximum. Third, Topkis's theorem yields only weak inequalities, ; strictness needs the efficient informativeness to be interior and to be differentiable there, which footnote 5 (p. 7) supplies. Without it, both optima can sit at the same corner or .
Everything is stated over in the sub-namespace SellingData.AppendsBinary. The two types form an inductive type CostType with constructors H and L. A Model structure holds , , , , , , weakly increasing on , and the standing assumption for both costs. The posteriors are defined with the divisions of the paper's (2). The outside option is the printed .
Optimality and efficiency are predicates on maximizers, never a chosen maximizer. The optimal menu is defined from the data-append screening problem itself; defining it through (8) would make the first claim of the goal trivial and is ruled out. The goal additionally assumes the part of footnote 5 that the strict inequalities need: continuous on , differentiable on , right derivative at , and as . Convexity and twice differentiability, which the footnote also lists, are not assumed. The milestones carry only what they need: none for the willingness to pay, continuity of for one part of the reduction, and differentiability at the point for the derivative.
A complete development needs Bayes posteriors for a symmetric binary signal, elementary calculus (derivatives, the mean value theorem, extrema on compact intervals), and Topkis's monotonicity theorem, which is on the platform (Theorem 2.8.4) and is referenced by this mission. Proofs of the milestones and of the goal are welcome. Lemmas on the binary-signal posteriors (for instance the identity ) are reusable by the companion mission on marketing lists.
Third-degree price discrimination means charging different prices to identifiable groups of customers. Its welfare effects are a classical question in industrial organization. With linear demands and every market served under uniform pricing, discrimination leaves total output unchanged and lowers total welfare (Pigou 1920). More generally, welfare can rise only if total output rises (Schmalensee 1981; Varian 1985).
Many current markets are two-sided platforms: marketplaces, app stores and payment networks that charge sellers participation fees and differentiate those fees by seller category (for instance, app stores charging games and non-games differently). On such a platform, a seller's presence is worth something to the buyers on the other side. De Cornière, Mantovani and Shekhar (Management Science 71(4), 2025) show that this cross-side benefit overturns the classical conclusion: discriminating between seller types raises seller participation, which attracts more buyers, which raises seller participation further. In their linear model, total welfare rises, and for large enough cross-side benefits every group gains.
A monopoly platform serves a mass one of buyers and two categories of sellers, and , each of mass one.
The platform chooses participation levels, and the fees follow from the inverse demands.
Uniform pricing (). The platform chooses to maximize
At the common fee , type- participation is .
Price discrimination. The platform chooses to maximize
The participant with outside option joins when its net value exceeds . Buyer surplus and type- seller surplus are therefore integrals over from to the participation level of (net value ). Total welfare is .
Assumption 1 (p. 3343) restricts the parameters: (i) ; (ii) .
Two denominators recur: and .
Under , and Assumption 1, both optimization problems have a solution, and for every uniform optimum and every discrimination optimum:
When , all four groups (platform, buyers, low-type sellers and high-type sellers) are strictly better off: a strict Pareto improvement.
The result. Proposition 2 is a counterpoint to the Pigouvian benchmark. In a two-sided market with linear demands, seller-side discrimination can be a strict Pareto improvement, so a blanket presumption against fee differentiation by platforms is not justified on welfare grounds. The comparison also isolates the mechanism. The low-type sellers gain even though the platform could already serve them, and the high types gain only when the buyer-side benefit is large enough. The paper's extensions in §5 (seller-type-dependent buyer benefits, ad valorem fees, competition) start from this baseline.
Formalizing it. The paper proves Proposition 2 by explicit algebra in Appendix A.2. Most of that algebra is printed, but the positivity of is argued only through claims about the roots of a quartic in , which are asserted rather than shown. No part of the argument is machine-checked. A formalization would give:
The model is a small, self-contained template for platform pricing with linear demands, and the same definitions can serve later comparisons (fees, prices, exclusion).
The optimization steps are routine: both objectives are concave quadratics, strictly concave exactly when and , and Assumption 1(i) gives . The integrals have affine integrands. The comparison steps are where the work is.
Two-sided platforms (ride hailing, delivery, freight, cloud capacity) test product changes with user-split experiments: each arriving demand unit is assigned to treatment with probability and to control otherwise. Treated and control units then compete for the same supply, so the outcome of one group depends on the size of the other. This interference biases the standard estimator that compares the value earned by the two groups and rescales by and (Blake and Coey, 2014; Johari, Li, Liskovich and Weintraub, 2022).
Bright, Delarue and Lobel (arXiv:2205.02274v4, 2024; Management Science 2025) model each matching cycle as a linear program and propose a shadow-price estimator that weights the observed demand counts by the marginal values of demand in the experiment's matching problem. This mission formalizes their finite-sample result, Theorem 6: at every market size, the shadow-price estimator is unbiased for the slope of the expected value function at the experiment state. The fluid-limit comparison with the standard estimator (Theorem 4) and the fluid limit of the matching value (Theorem 1) are the subjects of the other two missions of this series.
A matching network has one sink node for each of demand types, one source node for each of supply types, a finite set of intermediate nodes, and arcs that leave a supply or intermediate node and enter a demand or intermediate node. Arc has a value and a capacity . For a density , demand and supply , the matching value is the optimal value of the linear program (2): maximize subject to inflow at at most , outflow at at most , flow balance at intermediate nodes, and . Write and for the -th unit vector.
Rates are a control demand rate , a treatment effect with , and a supply rate . In the partial-treatment market with treated fraction , the demand counts and supply counts are independent. The finite-sample partial-treatment value function is
and the global treatment effect is .
In the experiment with treatment fraction , the platform observes independent control counts , treatment counts and supply counts, and solves the matching problem at . The negative-demand subgradient is and the positive one . The shadow-price estimator is
with the vector at .
For every network, all rates as above, every and every , is differentiable at and
If on , then .
Theorem 6 says the shadow-price estimator measures, in expectation, the derivative of the value function at the experiment state, for every finite market and for every network, with no uniqueness assumption on optimal dual solutions. It is what licenses the estimator outside the fluid limit, where the matching problem is frequently degenerate. Corollary 2 turns it into an explicit bias bound in terms of the curvature of , and the same identity integrated over a uniformly random gives an unbiased estimator of (Theorem 8 of the paper, not part of this mission).
The paper proves Theorem 6 in Appendix C.4.4; none of the statements has been machine-checked. The formalization adds a precise account of the junk cases a proof on paper passes over (infeasible programs at zero demand, the choice of subgradient), a Lean development of Poisson derivative identities that does not exist in Mathlib, and a network-flow LP layer shared with the two sibling missions. Theorem 7 is a discrete-concavity statement about network-flow values that is of independent interest.
The two sides of (14) are expectations under different laws: the right-hand side differentiates an expectation over the total demand in its Poisson means, while the left-hand side is an expectation over the separately observed treatment and control counts of a quantity that depends on both. Differentiating needs control of an infinite Poisson series uniformly in the mean, and differentiability in is a joint statement about all means at once. Computing the left-hand side with the law of the total demand alone loses exactly the information the estimator uses. The finite-sample matching problem is often degenerate, so its optimal duals are not unique; the paper notes that the particular selection is what makes Theorem 6 hold (p. 25), so no argument that treats the duals as interchangeable can work. Theorem 7 is a discrete-concavity statement about network-flow values that needs integrality of the data, and is the hardest combinatorial statement of the mission.
Demand types are Fin nd and supply types Fin ns (Lean index is the paper's type ). A network is a structure with arcs carrying their endpoints by type, values and nonnegative capacities. is the supremum of the objective over the feasible set; for nonnegative arguments the set contains and lies in the box , so it is a maximum. Poisson vectors are products (Measure.pi) of Mathlib's poissonMeasure, and the experiment law is the product of the control, treatment and supply laws; independence across all counts is the paper's standing reading of one Poisson process per type. Derivatives are HasDerivAt, so every differentiability claim is part of a conclusion. Statements follow arXiv:2205.02274v4; its printed slips are corrected as disclosed in each item: (16) carries wherever , Lemma 1's uniqueness presupposition becomes a correspondence of optimal sets, Lemma 4 is stated for arbitrary capacities so that it covers , and (32) drops the redundant conditioning on supply.
Standing hypotheses are , , , , ; Assumptions 1–3 of the paper are not hypotheses of Theorem 6, because its proof uses none of them, and no integrality of capacities is assumed outside Theorem 7. The estimator is (18) applied to and its expectation is taken under the separate laws of control and treatment counts; it is not defined as a derivative, and its expectation is not computed from the law of the total demand. At zero demand, the infeasible value of is multiplied by a vanishing count, so it never affects the estimator.
Useful infrastructure beyond this mission: derivatives of Poisson expectations in the mean, the binomial conditional law of a Poisson split, and value-function facts for capacitated network-flow LPs. Contributions to any milestone are welcome; Lemmas 3 and 5 and (32) are pure probability and independent of the LP layer.
Music streaming platforms collect a subscription fee from each user and have to pass the revenue on to the artists whose content was played. The two rules used in practice are pro-rata (each artist is paid in proportion to their total number of streams, over all users) and user-centric (each user's fee is split among the artists that user played, in proportion to that user's streams). Which rule is fair has been debated by platforms, rights holders and regulators. Bergantiños and Moreno-Ternero (arXiv:2310.11861, Management Science, 2025) study the problem axiomatically, and in their §4 also through cooperative game theory: they associate a transferable-utility game with every streaming problem and ask which revenue allocations no coalition of artists could object to.
This mission formalizes their Theorem 2. It gives an explicit description of the core of that game.
There are artists and a finite set of users, each of whom pays , so is to be shared. A streaming problem records the number of times user played artist . Every user in is assumed to have played at least one artist.
This is a pessimistic estimate of what a group of artists could earn by leaving to found its own platform. Because every list is nonempty, .
The proof goes through two classical objects of cooperative game theory. The Harsanyi dividends are . A sharing system assigns to each nonempty coalition a probability vector supported on . The Harsanyi set is the set of allocations that a sharing system induces. The unanimity game has if and otherwise.
Theorem 2 says that the core-stable allocations of streaming revenue are exactly those that split each user's fee among the artists that user played. The user-centric rule is such a split, so its rewards always lie in the core. The pro-rata rule can fall outside the core: in the paper's Example 1 a coalition of one artist receives less than the fee of the user who played only that artist. This observation underlies the paper's Theorem 3, where core selection together with homogeneity and additivity characterizes the user-centric index. Beyond streaming, the theorem gives an explicit core for a class of games built from users' lists. The museum-pass games of Ginsburg and Zang have the same structure.
The paper's proof combines two cited classical theorems (Harsanyi's unanimity decomposition and Vasil'ev's identification of core and Harsanyi set for games with nonnegative dividends) with bookkeeping specific to streaming. None of these is formalized on the platform except the bare existence of a unanimity decomposition (Young 1985's exists_unanimity_expansion, Proved, referenced here). The mission therefore produces reusable statements of Harsanyi dividends, the Harsanyi set and Vasil'ev's theorem for arbitrary finite TU games, as well as the streaming result itself.
Most of the mission is finite bookkeeping: Möbius inversion over the subset lattice and regrouping sums by users' lists. The central difficulty is the inclusion in Vasil'ev's theorem. One has to show that every core vector can be generated by splitting each dividend among the members of its coalition. This is a feasibility statement for a transportation problem whose supplies are the dividends and whose demands are the core payoffs, with each coalition allowed to ship only to its own members. The core inequalities have to be turned into such a shipment plan, and neither of the obvious candidates does that. Splitting each dividend equally among a coalition's members gives the Shapley value, a single point. Taking extreme points of the core gives the marginal vectors, and writing an arbitrary core point through them is the same feasibility question again. The paper cites the result without proof.
Fin n, numbered from . Users are named by natural numbers. A problem is a finitely supported map t : ℕ →₀ (Fin n → ℕ) with t j i ; the user set is its support. Every user in therefore has a nonempty list, which is the paper's standing assumption (recalled on p. 19). Streams are natural numbers. The empty problem is allowed; there both sides of Theorem 2 are .Fin n → ℝ. The core is the published Supermodularity.Cooperative.Core Finset.univ. Convexity is the published Supermodularity.Cooperative.IsConvexGame. The unanimity game is the published MonotonicSolutions.StrongMono.unanimity.Large online marketplaces such as Amazon, JD.com and Walmart.com act both as a sales channel for third-party sellers and as a retailer of their own. A platform watches which third-party products sell well and may start selling the same product itself, a move called platform entry. Over ten months of 2013–2014, Amazon entered about 3% of the products first offered only by third-party sellers, and its entry lowered the affected products' sales rankings, that is, raised their total sales (Zhu & Liu, Strategic Management Journal 2018). The conventional view is that a seller should deter entry, since the platform becomes a competitor that also collects a referral fee on every sale the seller makes.
L. Qi, H. Song and W. Xiao (Management Science 2025) build a two-stage model with three features: the platform charges a referral rate on the seller's revenue, the platform's marketing effort spills over to the seller's product, and the two parties compete in quantities with differentiated products. Their Proposition 2 identifies exactly when the seller is better off if the platform enters. This mission formalizes that result together with the equilibrium analysis it rests on.
There are five parameters: the degree of spillover , the referral rate , the competition intensity , the seller's effort-cost coefficient and the platform's entry cost . The product has base value . The platform's effort-cost coefficient is normalized to .
Stage 1. The seller chooses an effort at cost , which raises the product value to , and a quantity . The price is , and the seller earns after paying the referral fee .
Stage 2 without entry. The seller alone sells at price and earns .
Stage 2 with entry. The platform chooses an effort at cost . Its own product's value becomes , and the seller's product's value becomes . The two then choose quantities simultaneously, with prices
The seller earns . The platform earns : the referral fee on the seller's revenue plus its own margin.
Backward induction gives closed forms. Write
and let be the quartic denominator of the platform's optimal effort (Lemma 2). Condition (5) is : under it the seller stays in the market after entry. The paper assumes (5) from that point on. Let
so that the seller's two-stage profits as functions of the effort are
The receptive regime is .
and the shape of on the box :
The thresholds are existentials, as the paper defines them only inside its proof.
The result. Proposition 2 says that the seller's preference does not depend on the seller's own effort or on the base value, only on . It shows that the conventional advice to deter entry is wrong on a nonempty region: a strong enough spillover, or a high enough referral rate (which gives the platform a stake in the seller's sales and so a reason to invest more effort), makes entry welcome. In the competition intensity the regime is not monotone. The seller welcomes entry when products are well differentiated, opposes it at intermediate , and can welcome it again near perfect substitutes. The paper's later results on the seller's optimal effort and on entry deterrence (Proposition 3 onward) are stated separately inside and outside , so this classification is their starting point.
Formalizing it. The result is proved in the paper, and nothing about it is machine-checked yet. Its proof leans on "one can verify" claims about quartic polynomials on a box: the positivity of , of the platform's effort and of under (5), and the sign patterns of (11). A formal proof checks each of them. The mission also ties the closed forms (6)–(7) to an explicit game, with equilibria defined as best responses, so the comparison is between equilibrium profits and not between formulas taken on trust.
The first part of the goal is immediate once (6)–(7) are known, since . The content lies elsewhere.
All quantities are real numbers. The parameters are explicit arguments, and the standing ranges , , are a hypothesis InBox δ f β. Every polynomial (, , the numerator of , (11), ) is written term for term as printed. keeps the case split of (8), so is false wherever (5) fails. Conventions:
CompetingChains.Cournot.IsPureNash), the entry equilibrium (the platform's effort is a global maximizer against every equilibrium after every deviation), and the stage-1 and no-entry problems.The first part of the goal is near-definitional given (6)–(7). The mission's content is the threshold structure of and milestones 1–3, which make (6)–(7) the equilibrium profits. A formalization in which the thresholds may depend on the varying parameter, or in which is taken as by definition, would not be this theorem.
A complete development needs real polynomial inequalities on boxes (nlinarith/polyrith-style certificates or interval arguments) and elementary concave maximization. A uniqueness lemma for two-player games whose best responses have slopes with product below one would be reusable for other differentiated Cournot models. Contributions are welcome for any milestone, for the step "(11) implies (5)", and for proofs of the sign lemmas by certificates.
Ride-hailing platforms match riders with drivers who choose for themselves whether to work. Autonomous vehicles (AVs) would replace part of this self-scheduling labor with capital whose fleet size the platform chooses. Lian and van Ryzin study when, and under which market configuration, the cost savings of AVs reach riders. Their comparison needs a benchmark: the market served by human drivers (HVs) alone. This mission formalizes that benchmark, Proposition 1 of the paper, together with the lemmas on minimal supply and utilization that the rest of the paper uses.
Two economic forces drive the benchmark. The first is the density effect: in a denser market an idle car is closer to the next rider, so pickups are shorter and each driver spends more of the hour on paid trips. The second is the supply effect of labor: a larger fleet requires higher hourly earnings to attract the marginal driver. Proposition 1 describes how the equilibrium demand, fleet size, utilization and price respond to market size when both forces are present.
The source is the authors' 2023 SSRN working paper (abstract 3716491, version of 23 August 2023); all theorem, lemma and equation numbers refer to that version, not to the 2025 Management Science article.
A market has an ETA function with and , the expected pickup time when cars are open (idle); is the ETA elasticity, and means a density effect. A trip lasts hours. Rider values for a ride hour are uniform on , . HVs have the supply curve , , : a fleet of drivers participates when hourly earnings are .
There are demand scenarios with potential demand masses . In scenario , the inverse demand at demand rate is , and the market revenue per hour is .
To serve demand with open cars, Little's law requires cars. The minimal supply level is
and the maximal utilization is . A demand rate is an equilibrium when revenue covers exactly the minimal driver cost,
It is stable (Definition 1) if there is no with and . The maximal stable equilibrium is the greatest stable equilibrium; then , and . The loose labor market condition of scenario is
the paper's restatement of its Assumption 2: the revenue curve meets the cost curve on its decreasing branch.
In Lean the parameters form the structure MarketParams, and the objects above are aTilde, nMin, uBar, priceFn, revenue, wage, hvCost, IsEquilibrium, IsStable, IsMaxStableEq and LooseMarket, in the namespace AVRideHail.PureHV.
Under the standing parameter assumptions and (33) in every scenario, each scenario has a unique maximal stable equilibrium, and for the family :
Proposition 1 is the reference point for every comparison in the paper: the AV markets of Sections 5–6 (common platform, independent platforms, monopoly AV supplier) are judged by how far their prices and served demand move from and . Its Item 3 isolates the density effect as the source of rising utilization, and the special cases of Item 5 show that the HV price can rise or fall with market size, so neither direction can be assumed in the AV analysis. Lemmas 1 and 2 are used throughout the appendices.
The paper proves these results by hand; to our knowledge none of them has a machine-checked proof. The mission produces a checked version of the benchmark and of the two technical lemmas, with every boundary case (, , ) stated explicitly.
The equation (13) always has the root , and it can have a second, unstable positive root below the stable one; the naive reading "the equilibrium is the root of (13)" therefore picks the wrong point. The work is to show that the greatest stable root exists, lies on the decreasing branch of the revenue curve, and moves monotonically with . This requires strict monotonicity of the cost curve , which combines a real power with the linear supply curve, and continuity on . Lemma 2 needs strict concavity of a quotient of real powers on a closed half-line including , where the function is defined by its limit.
All quantities are real numbers; fleet sizes and demands are continuous, as in the paper. Powers are Real.rpow. Scenarios are indexed by Fin I, 0-based. The maximal stable equilibrium is never chosen by Classical.choose: statements take a family dstar with IsMaxStableEq in each scenario.
Committed conventions and pinned hypotheses:
Real.rpow gives and ; agrees with Lemma 2.Encoding the equilibrium as "the root of (13) in " would make the goal follow from its own hypotheses; the goal instead quantifies over greatest stable equilibria, and that root is the conclusion of a milestone.
A complete development needs the intermediate value theorem on , strict monotonicity and concavity facts for real powers, and limits at infinity. The minimal-supply and utilization lemmas are reusable in any model with a pickup-time function . Proofs of any milestone are welcome, as are proofs of the remark of Item 5 in other parameter regimes.
Data brokers such as Acxiom, Nielsen and Oracle, and data generators such as Google and Facebook, sell processed consumer data to firms that use it to decide whom to target, whom to lend to, or which market to enter. The U.S. Federal Trade Commission's 2014 report on data brokers distinguishes two products: a marketing list, which carries contact information without which the buyer cannot act at all, and a data append, which enriches data the buyer already holds. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) asks how a seller should design a menu of data products of different informativeness when buyers differ in a privately known cost of acting.
The question belongs to the theory of optimal screening (Mussa and Rosen 1978; Maskin and Riley 1984), but with a twist: the buyer's marginal value of information is not a primitive. It is derived from the buyer's decision problem, so the direction of the single-crossing condition is itself an outcome of the model. This mission formalizes the paper's analysis of marketing lists in the base model with a binary value.
A marketer can take an action (target a consumer) at cost . The action's value is with prior probability and otherwise. The seller can provide a binary signal with , where the informativeness lies in an interval . The probability of the optimistic signal is , the posterior probability of after it is , and the posterior mean is ; are defined symmetrically. The paper assumes , so a marketer acts exactly after , and a marketer with cost who pays for a signal of informativeness gets
Serving a marketer at informativeness costs the seller , with and increasing.
There are two cost types, , with ; write , . Under the benchmark with observable cost, the seller extracts all surplus and chooses to maximize
whose maximizers are the efficient levels . With private costs the seller offers a menu with and maximizes subject to individual rationality and incentive compatibility , where . This is problem (6); its solutions are the optimal menus, with informativeness levels .
Under the regularity of described below,
The first claim is an equality of sets of maximizers; the inequalities compare every optimal menu with every efficient level.
obtained by making IR and IC bind. 5. The derivative of (7) in : .
In textbook screening the low type's allocation is distorted downward to reduce the high type's rent. Here the low type of the screening problem is the high-cost marketer, and its information can be distorted in either direction: the rent conceded to low-cost marketers falls with when and rises when . Proposition 2 therefore says that a seller of marketing lists may supply socially excessive information to some buyers, a possibility absent from the data-appends literature the paper compares against, where provision can only be insufficient. Proposition 1 isolates the mechanism: the prior decides whether information mainly prevents wasteful targeting or restores profitable targeting, and the cost of acting amplifies one or the other.
The result is proved in the paper; nothing in it has been machine-checked. The mission produces a checked version of the two-type screening reduction (including the verification that the constraints dropped in (7) hold at its solutions, which the paper asserts as standard) and of the comparative statics with set-valued optima, since is not assumed convex and optima need not be unique.
The derivative computations are routine once is simplified to . The work lies elsewhere. First, the reduction: "IR binds for the high-cost type and IC binds for the low-cost type" is the standard heuristic, but at a solution of (7) one still has to check the dropped constraint IC and the nonnegativity ; both depend on the ordering of and at the optimum, which in turn depends on the sign of . Second, strictness: comparative statics through increasing differences give only weak inequalities between maximizer sets. Upgrading to requires ruling out a common maximizer, which needs the optimum to be interior and differentiable there; the naive argument by first-order conditions fails at the corners . Third, as sets requires existence of optimal menus, hence attainment of the maximum of (7).
Everything is over . The model is a structure Model (values, prior, informativeness interval, selling cost) extended by Screening (type probability and the two costs); the standing assumptions , , , , increasing on (weakly), , , and for both types are fields. The posteriors are defined with the divisions printed in (2). Efficient levels and optimal menus are sets of maximizers, never chosen by Classical.choose or a first-order condition. Menus include .
The goal additionally assumes the part of footnote 5 (p. 7) that makes optima interior: continuous on , differentiable on , with right derivative and as . Convexity and twice differentiability, also in the footnote, are not assumed. The milestones carry no regularity beyond differentiability at the point considered (milestones 1, 5) and continuity for the optimality characterization in milestone 4.
The optimal menu is a maximizer of (6) under all four constraints, not a maximizer of (7): defining it through (7) would make half of the goal immediate and skip the reduction.
The development needs the algebra of the binary posterior, the two-type screening reduction, and a strict version of monotone comparative statics; Topkis's theorem on strictly increasing differences (Theorem 2.8.4) is already proved on the platform and referenced. Proofs of any milestone, and alternative arguments for the strict inequalities, are welcome.
Linear Cauchy–Riemann operators are the linearizations of the nonlinear Cauchy–Riemann equation for pseudoholomorphic curves. On the cylinder with the trivial bundle they take the form
where converges to loops of symmetric matrices as . These are the operators of Floer homology, of symplectic field theory and of contact homology. The dimension of their moduli spaces is the Fredholm index of , and the Riemann–Roch formula with punctures computes it from the Conley–Zehnder indices of the asymptotic operators :
This mission formalizes this formula, together with the Fredholm property of , following C. Wendl, Lectures on Symplectic Field Theory, Lectures 3–5, in the case of the cylinder (the sphere with one positive and one negative puncture). Mathlib has the notion of a Fredholm operator but no Sobolev spaces on cylinders, no Cauchy–Riemann operators and no Conley–Zehnder index.
If and the asymptotic operators are nondegenerate, then is Fredholm and (Wendl, Theorem 5.4 with Theorem 4.3, for the cylinder).
The result. The index formula is the dimension formula for moduli spaces of pseudoholomorphic cylinders: Floer trajectories in Hamiltonian Floer homology and holomorphic cylinders in symplectizations. It fixes the grading of these theories, and its sign conventions are those of the Conley–Zehnder index of the asymptotic orbits.
Formalizing it. The mission builds Sobolev spaces on the cylinder, the Fredholm theory of Cauchy–Riemann operators with cylindrical ends, and the Conley–Zehnder index of asymptotic operators. These are the analytic foundations of Floer theory and symplectic field theory and are reusable for transversality arguments and for the indices of other operators. Milestone 5 is a general statement about Banach spaces.
The operators act between infinite-dimensional spaces of functions on a non-compact domain, so finiteness of kernel and cokernel is a global statement that sees the behaviour at both ends. The Sobolev space is defined as a closure, and the operator acts on its elements through their weak derivatives. The Conley–Zehnder index is defined through a continuous argument of a normalized complex determinant along a path of symplectic matrices, extended to a normal form; the conventions (sign of , orientation of the cylinder, which end is positive) all enter the final formula. Several milestones are uniform estimates in which the constant is chosen before the function.
CauchyRiemannIndex. The definition module CauchyRiemannIndex_Setting defines the cylinder measure, W1p, crKernel, crRange, crIndex, IsFredholmCR, asymptotic operators through IsFundamentalSolution, IsNondegenerate and asymptoticCZIndex, and the Conley–Zehnder index czIndex of a symplectic path. The mission is standalone; czIndex and its auxiliary definitions repeat those of the ConleyZehnder mission word for word.EuclideanSpace ℝ (Fin n ⊕ Fin n), matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ, and is Matrix.J. Maps on the cylinder are maps ℝ × ℝ → ℝ²ⁿ, periodic in the second variable, and is taken on the strip . is a closed subspace of Lp × Lp × Lp, consisting of triples .ℝ≥0∞ with and . Norms of smooth maps are eLpNorm in ℝ≥0∞; constants are in ℝ≥0.finrank ker - finrank (Lp ⧸ range) in ℤ; statements that use it also assert that both are finite-dimensional.ContDiff ℝ ∞ (, not analytic). The coefficient is only assumed continuous, with uniform convergence at the ends.Contributions welcome: general lemmas on Sobolev spaces of periodic functions, on Fredholm operators between Banach spaces, and on the Conley–Zehnder index.
To sell a stock short, an investor must first borrow it, and the owner who lends it charges a lending fee. Securities lending is a large market, and the fee varies across stocks: D'Avolio (2002) documents that shorting costs are positively related to the dispersion of investors' beliefs. Short-sale constraints have a long history in asset pricing (Miller 1977; Harrison and Kreps 1978; Jones and Lamont 2002), but most models either forbid short sales outright or take the fee as an exogenous parameter. Neither explains where the fee comes from, nor when a lending market is active at all.
Evgeniou, Hugonnier and Prieto build a dynamic general equilibrium model in which the fee is endogenous: two investors with logarithmic utility disagree about the expected return of a risky asset, and a lending agent, acting for the asset owners, sets the fee charged to short sellers to maximize the owners' fee revenue. Their §3 derives the equilibrium shorting cost in closed form at every state of the economy. This mission formalizes that derivation.
The economy has a riskless asset and two risky assets with strictly positive volatilities . Asset 1 can be shorted at a cost; asset 2 cannot be shorted at all. There are two investors, an optimist and a pessimist , with wealths . Each investor perceives market prices of risk (Sharpe ratios) , and the optimist is more optimistic about asset 1: , the disagreement .
A short position in asset 1 pays a shorting cost per dollar shorted, and a long position earns a lending yield . Both are measured per unit of volatility of asset 1: and . A position in asset 1 earns fees at the rate
with and . Investor chooses wealth fractions with to solve the mean-variance problem
which is what logarithmic utility reduces to at each instant. The lending agent's revenue per unit of volatility at fee is
An equilibrium at a state consists of these quantities such that: the no-dominance condition holds for both investors (equation (7)); each investor's portfolio is optimal; asset 1, in positive supply , clears; the lending market clears (fees paid by short sellers equal fees received by long holders); and is the least maximizer of over . The inactive set is and the active set is its complement.
At every equilibrium state,
Lending is active exactly where the pessimist perceives a strictly negative net Sharpe ratio on long positions, and there the lending agent charges half the Sharpe ratio the pessimist could earn by shorting absent frictions.
Two companion statements are also included: (18) (p. 20), that the pessimist is strictly short on , and the fee flow (p. 19).
The goal is the paper's description of the short market. It identifies the active set by a condition on one observable-in-principle quantity, the pessimist's net Sharpe ratio, and it gives the fee as a fixed fraction of the pessimist's frictionless Sharpe ratio. The rest of the paper rests on it: the one-asset closed forms of §4.1, the trading regions of §3.3, and the pricing results of Proposition 2 all start from (15)–(16). The fee-flow identity shows that the optimist captures a quarter of the pessimist's frictionless excess return, which is the upper bound Remark 1 attributes to any alternative fee-setting mechanism.
The result is proved in the paper, partly in the text and partly in Appendix A. Some steps are argued informally: (11) rests on the sentence "agents cannot be short simultaneously in equilibrium", and (14) on "substituting the optimal portfolios of Proposition 1 into the market clearing conditions". As far as is known, none of it has been machine-checked. A formalization makes each step explicit, including the degenerate states the text passes over. In checking the statements against each other, three printed slips were found and are corrected here (see Formalization scope).
The goal combines optimality, clearing and revenue maximization, and the obvious argument fails at its degenerate edge. On the inactive set the shorting cost equals the lending yield (). There Proposition 1's characterization of optimal portfolios no longer holds: portfolios that short asset 1 to buy asset 2 are also optimal. So the step "substitute the optimal portfolios" is not available, and (14) must be obtained from the clearing conditions directly in that case. Similarly the revenue maximizer is not unique on the inactive set; the shorting cost is pinned down only by the paper's selection of the least maximizer, and (16) is false for any other selection. Finally, (11) requires an argument that the two investors cannot both be short while asset 1 is in positive supply. This uses optimality of both portfolios, not just of one.
Everything is stated at one state of the paper's continuous-time economy, about real numbers. The continuous-time economy of §2 (Brownian filtrations, consumption streams, the dynamics of wealth) is the paper's motivation and is not formalized; the formalized statements are its instantaneous equilibrium conditions. The time index is dropped throughout, and the paper's "arbitrary process " in Proposition 1 becomes an arbitrary real number.
Conventions:
if … then … else 0.Corrected slips of the page, each disclosed in the item concerned:
The results (11), (13) and (14) are not built into the equilibrium predicate. With them assumed, the goal would reduce to a four-line computation; they are separate items to be proved. The definitions are short and self-contained, needing only real arithmetic from Mathlib. Proofs of the milestones, and proofs of the goal that use the milestones, are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known, and the technique that reached 62 cannot go further. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-62 mission already covers every , the new work is the range from 50 to 62.
The cutoff came down from 256 to 62 across nine missions. The step from 90 to 80 used a weighted pair-curvature and confinement estimate introduced by moona3k, and further refinement pushed it from 80 through 70 to 62. The confinement method is now exhausted: at , every confinement radius whose tangent model stays positive already makes the budget-7 box factor larger than 1. Reaching 50 requires a fundamentally new idea. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 50 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryQuantum mechanics represents the states of a system by unit vectors (normed rays) of a complex Hilbert space and its observables by self-adjoint operators on . The most important observables — position, momentum, energy — are unbounded. A. Heathcote's paper Unbounded Operators and the Incompleteness of Quantum Mechanics (Philosophy of Science 57, 1990, 523–534) draws attention to a mathematical fact that is routinely glossed over in physical texts: an unbounded self-adjoint operator cannot be defined on all of , and there are concrete normalized wave functions on which the position and momentum operators do not act at all. The paper uses this to argue that the standard postulates of quantum mechanics are, in a precise sense, incomplete.
This mission isolates the mathematical content of that argument, which is a clean and checkable piece of functional analysis on .
Let be a complex Hilbert space. A (partially defined) linear operator has a domain ; it is bounded if there is with for all , and unbounded otherwise. It is self-adjoint if it equals its Hilbert adjoint, , which includes .
On :
There is a unit vector of , namely the class of , lying in neither domain:
The result. The goal shows that the two postulates "every normed ray is a state" and "observables are self-adjoint operators" force the existence of states on which the position operator (and, independently, the momentum operator) is undefined. Milestone 5 is what the paper uses to separate this phenomenon from the canonical commutation relations: the failure of is not explained by being "sharp in momentum", because is not even in . Milestone 6 records the physical reading: the mean position of this normalized state is infinite.
Formalizing it. The individual facts are standard and elementary; none of them is new. What the mission produces is a machine-checked version of the paper's argument stated against the actual space and Mathlib's notion of unbounded operators and adjoints, with the domain conventions made explicit.
The calculus is easy; the subtleties are in the bookkeeping. Elements of are almost-everywhere classes, so " is discontinuous at " does not by itself show : one must rule out every a.e.-modification of being absolutely continuous. Similarly, the Hellinger–Toeplitz argument gives but not density, which comes from the adjoint being a genuine operator.
H →ₗ.[ℂ] H; self-adjointness is IsSelfAdjoint with respect to the adjoint A†, over a complex complete inner product space.Lp ℂ 2 volume on ℝ; and are subsets of it. Integrals of non-negative quantities are Lebesgue integrals valued in , so "" is literal and not a junk value.This mission develops Chapter 7 of Quantum Algorithms and Learning Theory — Part II by Srinivasan Arunachalam. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
For a matrix of rank (the generator matrix of an linear code) and define the codeword state
For every rate there is a constant such that the following holds for all and all rank- matrices with : if a measurement (POVM ) on copies identifies from , for drawn uniformly from , with average success probability
then .
This improves the Holevo-type bound to the optimal for constant-rate codes, showing that codeword fingerprint states cannot be identified from few copies.
Formalization Note "" is read as a fixed rate , and the constant of may depend on only. Identifying the state means outputting , which is equivalent since is injective for rank . The code distance plays no role and is not a hypothesis.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 1 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a register made of a register of qubits followed by a register of qubits. Let be a pure state of , that is, a unit vector. Then there exist a finite index set , an orthonormal family of states of , an orthonormal family of states of , and nonnegative reals with , such that
This is the singular value decomposition rephrased for bipartite pure states. Classical simulation algorithms for quantum circuits use it.
Formalization Note The source leaves the index set unspecified; here it is Fin r for an existentially chosen r.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
Credit risk matters to insurer bond holdings, pension scheme fixed-income investment and counterparty guarantees. Merton's corporate debt model derives terminal shareholder and bondholder payoffs from limited liability and asset value. Jarrow–Lando–Turnbull introduces observable ratings with Markov state migrations and default, motivating a second, independently defined view of risky fixed-income valuation.
A firm has nonnegative terminal assets and a single promise of face-value debt. Creditors are paid no more than the promise and no more than available assets; equity gets the residual. Finite genuine probability masses attach to terminal asset scenarios and yield discounted debt and equity claim valuations. Separately, a three-state rating matrix contains two non-default ratings and a terminal default state, with nonnegative row probabilities and full row-sum constraints.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Strict asset deficit is equivalent to zero equity except for solvent zero-cashflow special cases.
A bond priced equally to risk-free debt has zero model spread.
Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.
Structural terminal solvency and an independent absorbing-rating transition system reconcile riskier defaultable debt prices, nonnegative credit value deductions and genuinely two-period probability conservation.
As discussed in Merton's corporate-credit model, The mission connects terminal firm claims to an actual finite risk-neutral weighted value: equity plus debt exhaust firm assets, expected discounted defaultable debt is bounded above by its risk-free counterpart, and credit value deductions are nonnegative. The genuine two-step rating migration law preserves total probability mass. These independently defined results jointly give an actuarial foundation for pricing defaultable corporate securities and recognising credit exposures in asset-liability valuation.
It must be proved that the limited-liability payoffs partition total assets, with exact boundary conditions where assets equal or fall below face value. The pricing theorem must distinguish actual discounted expected creditor payments from assuming a closed-form Black–Scholes price; no lognormal risk-neutral firm distribution is postulated. Credit spreads require positive debt prices and maturities. A rating transition matrix must be proved stochastic under composition, and an absorbing default state is a model condition rather than automatically true for arbitrary matrices.
Limited liability and rating-migration probabilities are distinct mathematical constructs in this model. The complete diffusion-based Merton option value and continuous-time rating default models remain future mathematical research. The current target is nontrivial because it derives the bond valuation from limited-liability terminal payouts and an actual probability space, and the migration law from an independent finite transition kernel. Existing bond-present-value and state-reward missions are useful, but they do not identify shareholder and debt recovery claims. Its expected payoff and finite rating matrix infrastructure is reusable in asset-liability modelling and insurer counterparty credit valuation.
A firm's terminal assets must be partitioned consistently between equity and creditor payoffs. Above the promised debt face amount bondholders receive the promise and owners receive remaining assets. At the strict default threshold the owners' limited liability makes equity worthless and bondholders recover the remaining assets. The source values these payoffs using a proper finite risk-neutral scenario law, proving that discounted risky debt is no more valuable than the risk-free debt promise. The other branch builds a genuinely stochastic three-state rating transition matrix and derives two-step migration probabilities from matrix multiplication. Those observed or risk-neutral migration probabilities are not interchangeable without an additional measure-change argument. This is precise finite corporate credit mathematics; it is not a fabricated full closed-form structural diffusion model or a continuous-time default-intensity theory.
The new credit mission establishes exact one-period finite-state structural debt/equity payoff pricing and two-step rating probability conservation. It does not claim Merton's Black–Scholes closed-form equity value, stochastic diffusion replication, or the full continuous-time JLT risk-neutral generator model. The default-state absorbing property needs additional row restrictions and is not asserted for unrestricted transition matrices. Those are substantial extensions, and the current theorem bodies remain unproved.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Insurance economics prices risk using the utility of wealth rather than merely its variance. Pratt's seminal work derives risk aversion and the certainty-equivalent insurance premium, while Rothschild and Stiglitz connect comparative risk to probability order. Earlier actuarial entropic premium missions contain special finite retention objectives but do not derive an independently constructed expected wealth utility with premium indifference and finite stochastic dominance.
Losses are monetary outcomes on a genuinely finite scenario probability model, whose masses are nonnegative and sum to one. The exponential CARA wealth utility is strictly increasing and concave for positive aversion. The certainty-equivalent premium is constructed from the actual exponential moment of loss. Full insurance replaces the uncertain loss with a fixed premium and its utility is compared with the truly weighted uninsured outcome.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Utility of deterministic wealth equals its scenario expectation.
Risk-averse exponential expected utility demands at least the expected claim cost.
The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.
The actuarial insurer and policyholder indifference premium follows from genuinely averaged utility, with positive risk loading and a finite-scenario stochastic risk ordering.
As discussed in Pratt's utility-risk treatment, The capstone proves a complete indifference premium identity, not merely its algebraic definition, and derives risk loading above expected loss from convexity of the exponential. A coupled stochastic order implies both the ordering of actual finite distribution functions and higher expected utility for increasing utility functions. The same ordering is related to excess-of-loss premiums through statewise monotonicity. These results supply core insurer and policyholder pricing foundations.
The logarithmic certainty equivalent requires strictly positive exponential moments and a nonzero risk-aversion parameter. The actual expected utility factorization must account for the sign of negative exponential utility. Risk loading requires Jensen's inequality or an equivalent discrete exponential-convexity argument, not the assertion that every risk is profitable to insure. The comparison of finite CDFs must reverse the inequality for higher wealth, while a higher loss severity raises stop-loss costs. Pathwise coupling is stronger than the entire stochastic-dominance order and is identified as such.
Certainty-equivalent premium and stochastic risk ordering are distinct mathematical constructs in this model. A future generalisation will derive second-order stochastic dominance via integrals of real CDFs and concave expected utility, not merely a pathwise coupling. The current project is nontrivial because the CARA indifference identity follows by differentiating and averaging the actual utility, and the insurer's risk loading is derived from Jensen's inequality. Existing specialised exponential risk-price examples provide a useful benchmark but do not replace these general sources. The premium and coupling functions are reusable for nonproportional reinsurance, risk classification and comparative risk analysis.
Under constant absolute risk aversion the negative exponential utility function is increasing and concave in wealth when risk aversion is positive, even though its numerical utility level is negative. A fair premium is not obtained by simply assuming a desired level of profit. The expected uninsured utility is calculated from true scenario probabilities, the utility with full insurance is calculated using a fixed premium and the resulting indifference equation is solved from the loss exponential moment. The log moment premium must then be compared against expected claim cost using convexity, and the sign of this loading depends on risk aversion. Finite distribution functions and expected excess claims are independently defined for comparison. The pathwise coupling order in the source is stronger than first-order stochastic dominance, so no false claim of characterising all stochastic orders is made. Second-order dominance requires a separate distribution-integral analysis.
This is a genuine finite-probability CARA model with exactly derived insured/uninsured premium indifference. The stochastic order is proven for explicit statewise couplings and thus yields a strong sufficient condition for first-order stochastic dominance, not a complete characterisation of arbitrary second-order stochastic dominance. General concave utility risk orders, mean-preserving spreads, Arrow–Pratt comparative aversion for all utility families, and infinite random variables are future developments. All proof obligations are open.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Mortality experience in joint-life assurance and pensions depends not only on whether someone died, but on which insured life survives and which survivor or joint reserve must then be held. Standard multiple-life actuarial valuations motivate last-survivor, reversionary and guaranteed pension benefits. Earlier actuarial missions XLV and XLVI treat basic reversionary annuities and single-life mortality profit separately; this connects them through a genuine four-outcome death-strain model.
Two members start alive and experience independent yearly survival outcomes. Exactly four mutually exclusive joint states follow: both survive, only the first survives, only the second survives, or neither survives. Their probabilities use product and complement survival factors. The year-end reserve and any benefits can differ for every one of these states. Opening reserves plus premiums earn the annual return before payment and the next state contingent reserve is recognized.
The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.
Each valid joint-life outcome has nonnegative mass.
Additional state-specific benefit claims add to expected death strain.
An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.
An exhaustive, correctly normalized two-life outcome model makes the mortality experience profit mean zero, retaining separate survivor reserves, death benefits and guaranteed payment conventions.
As discussed in Dickson, Hardy and Waters' multiple-life analysis, The capstone derives actual four-state normalization and reconciles joint mortality profit as expected death strain less observed state-specific death strain, whose expected result is zero under its own properly normalized law. The state-specific reserve functions distinguish the two possible remaining single-life liabilities rather than collapsing them into a single average. Limited-reversionary and certain guarantee payments are represented as separate conditional benefits.
Four disjoint probabilities must be normalized with exact endpoint treatment. Reserve releases after each death outcome may have opposite signs to death-benefit payments, so the state strain must include both payout and next-state reserve less the accumulated starting fund. Expected mortality profit cannot be asserted by defining it to have zero mean: it must follow from the actual weighted expectation of the observed strain. Independence is an explicit current assumption; arbitrary dependent lives need a separate four-state probability law.
Joint-life mortality profit and state-dependent death strain are distinct mathematical constructs in this model. A future mission could introduce dependent lifetimes and within-year order of deaths, then compute first-to-die and last-survivor benefit present values directly from the joint survival law. The present work is nontrivial because both survivor reserves and actual death claims differ across the four states, while the mean mortality profit emerges from their normalised probability distribution. Existing joint-life annuity and single-life profit missions do not establish this combination. The outcome-specific reserve and mortality gain functions are reusable for spouse's pensions, death-in-service benefits and multi-life experience analysis.
Four disjoint annual outcomes must be considered for a policy whose two insured lives begin the year alive. They are both alive, only the first alive, only the second alive and both dead. Each outcome has a separate year-end reserve and may have a different death or survivor benefit. Accordingly, its actual death strain includes the benefit paid plus the new reserve less accumulated beginning-year funds. Expected strain is a genuine probability-weighted average of those four observed strains. The mortality experience profit for any one realised outcome equals the expected strain less that outcome's actual strain. Its expectation must be shown to vanish under the normalised four-outcome probability distribution, rather than by assuming zero mean. This framework supplies an actuarial bridge from joint-life/reversionary benefits to experience profit analysis and guarantee-period pensions. Within-year timing and dependent life outcomes require additional formal work.
This is a complete one-year joint mortality-experience model with explicit separate survivor reserves, not a full continuous-time ordering of first and second deaths inside the same policy year. Guarantee-period timing is represented by a separate deterministic indicator input. Exact age differences, policy options, death-payment timing and dependence-copula extensions can build on these definitions later. All theorem statements remain unproved.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
Panjer's original 1981 result derives the aggregate claims recursion from a special frequency probability law and arbitrary nonnegative-integer severity mass distribution, including claims worth zero. The original article and the Sundt–Jewell extension underpin the mission. Earlier actuarial mission LIV handles direct recurrence algebra, while LXXIII derives the Bernoulli first positive aggregate mass identity. This mission formalises a full positive-aggregate-severity recursion for a genuinely constructed compound law.
A claim count N has probability weights p_n supported on {0,...,m}, with no artificial truncation of an otherwise infinite count distribution. Independent severity masses f_j on nonnegative integer amounts admit a genuine n-fold convolution, with count-zero convolution equal to a unit atom at zero. Thus g_k=Σ_{n=0}^m p_n(f^{*n})k is defined independently of Panjer's formula. The count recursion p_n=(a+b/n)p{n−1} is assumed only for 1≤n≤m+1, including its boundary p_{m+1}=0, and p_n=0 above m. No conclusion about the aggregate g is assumed.
Write for the probability of exactly claims and for the probability that one claim has size . The frequency law is genuinely supported on ; an infinite Poisson distribution is not silently truncated. The empty portfolio has aggregate size zero, while denotes the distribution obtained by summing independent severities.
The first group constructs the aggregate probability directly from the frequency and severity laws:
It also proves the zero-severity convolution identities, nonnegative mass preservation, and finite frequency and severity generating-function relationships.
The count probabilities obey a Panjer recurrence with coefficients and . Crucially, the finite-support model includes the transition from to the compulsory zero probability at :
This makes the assumed count law compatible with the finite aggregate distribution. For a claim size that may equal zero, the aggregate zero atom involves every possible claim count:
The central target is the entire positive-aggregate-size Panjer recurrence, not merely its first positive atom. For every integer , the result is
The factor is essential because a positive number of claims may still produce aggregate size zero. Further targets establish properties of cumulative aggregate probabilities, capital exceedance tails and finite stop-loss expectations. Every aggregate probability is defined independently of the recurrence it is subsequently required to satisfy.
The original Panjer paper gives the classical aggregate-loss setting. The capstone derives (1-a f_0)g_k=Σ_{j=1}^k(a+bj/k) f_j g_{k-j} for every positive aggregate amount from the actual random sum, together with g_0=G_N(f_0). The generator gives a count-supported finite Panjer family; it does not claim an infinite Poisson/negative-binomial count law. The exact zero claim-size correction is essential even when count N is positive, because multiple claims may all have zero monetary size. The authoring graph also includes frequency PGFs, severity convolution, CDF/tail and stop-loss identities.
Existing actuarial probability and Panjer steps are established subject areas. Every formal result introduced in this mission is an open Lean theorem target; none has an accepted proof. A vacuous or trivial definition of the aggregate as the recurrence solution is explicitly ruled out. The proof must rearrange nested severity convolutions, differentiate coefficient identities or establish the equivalent frequency recursion, and manage the zero-severity term that multiplies g_k itself. The count-support cutoff must satisfy the Panjer multiplier at m+1 to avoid invalid boundary terms. The recurrence at k=0 is not defined due to division by k; zero aggregate mass follows separately from the frequency PGF. Because f_0 may be positive, truncating the count sum at arbitrary m with an infinite count law would be mathematically invalid; we avoid that by using a genuine finite count distribution.
This mission supplies a full k≥1 Panjer relation under an exact finite-support frequency model, not general infinite Poisson or geometric counts and not continuous claim severities. Positivity and mass normalisation require additional explicit probability conditions beyond the purely algebraic count recurrence, so the capstone is a valid algebraic identity even before imposing proper probability weights. All formal results remain Lean theorem targets without accepted proofs. The finite model is a reusable foundation for formal-power-series and analytic infinite-frequency cases.
These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The Yang–Mills functional measures the total curvature of a connection on a principal bundle. Its critical points, the Yang–Mills connections, are the non-abelian generalization of solutions of Maxwell's equations, and in four dimensions the most important among them are the self-dual and anti-self-dual connections (instantons), whose moduli spaces underlie Donaldson theory of smooth four-manifolds. A basic and frequently used fact, recorded as Proposition 3.1.1 in K. Uhlenbeck's lectures Equations of Gauge Theory (notes by L. Fredrickson, Temple University, 2012), is that instantons are not merely critical points: within a fixed topological class and with fixed boundary data they are absolute minimizers of the Yang–Mills energy. The same "energy identity" argument is the template the notes later apply to the Kapustin–Witten equations (Proposition 3.1.5).
Timeline of the ideas involved: Yang and Mills introduce the equations (1954); Belavin, Polyakov, Schwartz and Tyupkin observe the topological lower bound on the energy and its saturation by self-dual fields (1975); Atiyah, Hitchin and Singer study the deformation theory of instantons (1977–78); Donaldson uses the instanton moduli space in four-manifold topology (1983).
Work on the trivial principal -bundle over a closed box with the Euclidean metric. A connection is with , where each is a smooth map into the Lie algebra of traceless skew-Hermitian complex matrices. Its curvature is the -valued two-form with coefficients
The Hodge star on two-forms is , with the Levi-Civita symbol. A two-form is self-dual if and anti-self-dual if . The pointwise norm is , and the Yang–Mills functional on is
The Chern–Weil density is the coefficient of , and the Chern–Simons three-form is , with flux components .
If and are smooth -connections on that agree on , and is self-dual on all of or anti-self-dual on all of , then
The energy identity turns a second-order variational problem into a first-order one: any connection satisfying the first-order self-duality equation is automatically a Yang–Mills connection, and in fact a global minimizer in its class. This is the reason instanton moduli spaces are the natural objects of four-dimensional gauge theory, and it is the model for the corresponding minimization statements for the Kapustin–Witten equations treated later in the same notes. The result is classical and its proof is known; the remaining work is formal: a machine-checked development of the curvature, Hodge star, Chern–Simons transgression and the boundary integration on boxes, none of which are currently packaged in this form in Mathlib.
The algebraic identity of Lemma 3.1.2 is a finite computation. The substantive step is the transgression formula , a cancellation between derivative terms and cubic terms that depends on cyclicity of the trace and on the antisymmetry of , followed by Stokes' theorem on the box with correct face orientations. The naive approach of comparing and pointwise fails: the two connections agree only on the boundary, and only the integrated topological term is boundary-determined.
The general setting of the notes (a -bundle over a compact oriented Riemannian four-manifold with boundary, topological class ) is replaced by the trivial -bundle over a closed axis-parallel box in Euclidean , so the topological term is zero. Connections are smooth on all of (equivalently, smooth up to the boundary of the box) and every coefficient takes values in . Two-forms are stored as antisymmetric families of matrices; partial derivatives are taken entrywise; integrals are Lebesgue integrals over the box and over its faces. "Fixed boundary data" means at every point of . Self-duality is , matching in Section 2.2 of the notes.
Two sign/normalization corrections relative to the printed notes are made deliberately: Lemma 3.1.2 is stated with the sign obtained in its own proof on p. 32 ( rather than the printed , because on ), and the Chern–Simons form uses the standard coefficient in , i.e. , for which holds, instead of the printed .
A trivializing formalization would make the boundary condition or the self-duality hypothesis unsatisfiable; here the zero connection is self-dual and satisfies every hypothesis, and the statements are not vacuous.
Reusable infrastructure: Levi-Civita symbol and Hodge star on with matrix coefficients, curvature of matrix-valued connections, the Chern–Simons transgression, and Stokes' theorem for flux forms on boxes (Mathlib's divergence theorem on boxes is the natural tool). Contributions to any milestone are welcome.
How large can the order of a single permutation of objects be? The answer, Landau's function , is a basic invariant of the symmetric group : it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, is also the largest least common multiple of the parts of a partition of , which ties the question to the distribution of prime numbers.
Timeline.
For a natural number , let be the group of all permutations of an -element set. The order of is the least with . Landau's function is
A partition of is a multiset of positive integers summing to . The prime counting function is the number of primes , the (offset) logarithmic integral is , and is its inverse on . Throughout, is the natural logarithm.
Landau's theorem pins down the growth rate of the largest element order in , which bounds, for example, how long any fixed shuffle of cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in and quantitative prime-counting estimates on top of Mathlib.
The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.
Equiv.Perm (Fin n); is the supremum of orderOf σ over the finite group (a natural number; ).Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.Real.log (which returns at and is defined for negative input); all asymptotic statements are about , so the values at small are irrelevant there. The bounds in milestones 8–9 are stated for every and are true at .Nat.primeCounting ⌊x⌋₊; is the offset logarithmic integral ; is the least with , which for is the inverse function value. Replacing by the full integral changes the inverse by and does not affect any of the asymptotic statements.RiemannHypothesis.Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.