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?
A Fisher market allocates a common supply of items among buyers with separate budgets. When the items form a continuum, such as positions in a measurable interval, a buyer's valuation and the market price are functions rather than finite lists. This is a useful model for divisible resources and for settings in which an allocation can be described as a measurable subset of a continuous item space. Gao and Kroer develop equilibrium and convex-programming results for this setting in Infinite-Dimensional Fisher Markets and Tractable Fair Division. Their Section 6 extends the analysis from linear utility to quasilinear utility, where the buyer subtracts the cost of the allocated bundle from its value.
Quasilinear utility changes the role of money. A buyer can retain an unspent part of the budget and value it outside the market. Consequently, normalizing each buyer's valuation independently, which is harmless for linear demand, changes quasilinear demand. The extension therefore needs its own equilibrium definition and its own pair of optimization programs. This mission concerns the existence and exact equilibrium characterization stated in Theorem 10 of the cited preprint, rather than the numerical algorithms discussed elsewhere in that paper.
There are buyers and an item space , a compact subset of , with restricted Lebesgue measure . Buyer has an integrable, nonnegative valuation density with , and a strictly positive budget . A bundle is an essentially bounded, nonnegative measurable function on . An allocation is feasible when almost everywhere. A pure allocation assigns almost disjoint measurable sets to buyers, so almost everywhere; some items may remain unallocated.
A price density is nonnegative and integrable. The pairing gives the value of a bundle and its cost. At price , buyer chooses an affordable bundle maximizing , with affordability . A quasilinear market equilibrium (QLME) is a feasible allocation and price at which every buyer makes such a choice and unsold items have zero total price: .
The quasilinear Eisenberg–Gale primal program uses a nonnegative variable for each buyer and maximizes , where . Its dual program minimizes subject to and . The primal is represented by with at an optimum. This saturated form has the same optimum as the displayed program and makes the optimality conditions unambiguous.
The goal is the full four-part statement. The primal attains its maximum at a pure allocation. The dual attains its minimum with a unique vector and price density almost everywhere. For feasible primal and dual points, simultaneous optimality is equivalent to market clearance and
Finally, is a QLME exactly when there are and for which and are optimal in the two programs. The same given must appear on both sides of this equivalence.
The milestones follow the statements in the proof of Theorem 10: attainment of the utility-space program (A.14), uniqueness of the minimizer in the reduced dual program, weak duality (A.15) with its additive constant , the KKT characterization, and each direction of the QLME equivalence. The earlier paper's Lemma 1 identifies the feasible utility set with utilities of pure allocations and supplies the compactness used here. It belongs to the first mission of this series and is not duplicated as a target in this one.
The theorem establishes that the two infinite-dimensional programs describe the quasilinear market exactly. Attainment guarantees actual optimal allocation and price objects rather than only approximating sequences. Pure attainment gives a measurable partition-type allocation. The unique pins down each buyer's utility price, while identifies the price density almost everywhere. The KKT equations give precise tests for a candidate optimal pair, and the final equivalence translates between optimization solutions and buyer-level equilibrium behavior. These are the claims made by Theorem 10 and its appendix proof.
The result is proved in the paper; the work here is to formalize its statement and, in later solver contributions, its proof in Lean. A complete development will also provide reusable infrastructure for integrating valuation densities against essentially bounded bundles, representing continuum-item allocations, and relating a finite buyer-indexed vector to pointwise price maxima. No machine-checked proof of this mission's goal is supplied with this draft.
The optimization variables include functions in and , and the positive cone of has no useful interior for a direct appeal to standard infinite-dimensional convex-duality theorems. The finite-dimensional utility vector is easier to optimize over, but recovering a pure allocation from it requires the measurable-allocation result established earlier in the paper. The dual price is a pointwise maximum of integrable densities, and equality of prices is meaningful almost everywhere. Equilibrium demand compares a buyer's assigned bundle with every affordable essentially bounded bundle, so an optimality statement about program variables must account for that full comparison.
Lean represents densities and bundles as functions on the ambient Euclidean space, with the measure restricted to ; values outside do not matter. The standing hypotheses are compactness of , integrability and almost-everywhere nonnegativity of every , strictly positive total valuation, and strictly positive budgets. There is no assumption that total budgets or total item measure equal one. The buyer type Fin n is zero-based; the paper numbers buyers from one. The empty-buyer case is allowed and has the expected trivial finite-vector interpretation.
The equilibrium predicate includes supply feasibility. The printed QLME definition on page 29 omits it, although the linear-market definition includes it and Theorem 10(d) requires it. Without it, a buyer can receive more than unit supply on part of the item space while buyer optimality and market clearance still hold. The primal uses the saturated value ; leaving free below that value makes the printed KKT converse false. These two choices are disclosed in the item descriptions and moderation notes, with concrete counterexamples there.
The paper treats as a limiting infinite cost. Lean's real logarithm is total, so optimality compares only points whose logarithm arguments are positive. The utility KKT equation is multiplied by to avoid division by zero. Valuation and price densities are integrable, and bundles are essentially bounded, so pairings are genuine finite integrals. The pointwise maximum over buyers is an indexed supremum; feasibility and uniqueness use almost-everywhere equality for price functions and exact equality for the finite vector . These conventions prevent degenerate total-function values from deciding the theorem.
Contributions can address the measurable utility-set and pure-allocation infrastructure, finite-dimensional attainment, weak duality, the equality conditions, or the demand comparison. The intermediate milestones are stated at the strength used in the paper; the goal contains the entire four-part result.
A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.
The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.
For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:
The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.
For vehicle count k, arrival rate a, region S, and density g, write the workload factor as
The heavy traffic expression from the paper's Theorem 3 is
The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.
For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor
When η < 1, the target is the two sided estimate
The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.
The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.
The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.
The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.
The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.
Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.
The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.
A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.
In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.
The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).
There are two privately known product qualities, . A seller commits to a price pair , where is paid by crowdfunding backers and is charged in the regular selling period. The project needs a financing target , so a feasible pair satisfies and . Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).
All funding customers have the same taste , uniformly distributed on and unknown to the seller. They believe quality is and back the campaign when . Thus success has probability . After a successful campaign, true quality becomes known. A fraction of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times is at least (manuscript, pp. 10–11).
Write for the seller's expected total profit when true quality is and customers believe . The expressions and distinguish the regions in which returning customers buy for sure or with a conditional probability. Write for the maximum of over feasible pairs. In particular, is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).
In a separating equilibrium, the two seller types choose different feasible pairs and . Funding customers believe the product is high quality exactly at and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).
Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in . Its crowdfunding price is
and its retail price follows the three cases of equation (11), depending on whether lies below , between that threshold and , or above the second threshold (manuscript, p. 23, Lemma 4).
The goal is Proposition 2 in the small-quality-gap regime . Define by its equations, requiring :
When , the goal states that the unique separating equilibrium surviving the intuitive criterion has and the low type at his full-information optimum. Relative to every full-information optimum of the high type, it also states
The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).
The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).
The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.
The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds , in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).
Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains , with , and . The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed and remain available for the page 41 equations; is only used away from its zero denominator. Suprema range over all feasible pairs , , and “optimal” means the displayed pair attains that supremum.
The manuscript's Proposition 2 needs the additional bound . Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with ; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all . Lemma 4 also records its displayed domain . The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.
The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.
Markets with network externalities can support several levels of adoption at the same price. A consumer's willingness to buy may rise when many other consumers buy, while the ordinary price effect still works in the opposite direction. A price and an aggregate demand curve can therefore identify several self-consistent quantities without identifying which one consumers reach. In Network Externalities and Market Dominance, Akerlof, Holden and Rayo study this selection problem before analyzing firms' pricing decisions (accepted manuscript, §2.1).
The paper uses an introspective equilibrium: consumers begin with an impulse about firm 1's sales and repeatedly revise consumption in response to the previous level. The resulting limit gives a selection rule tied to an observable starting condition rather than to an arbitrary choice among fixed points. The mission formalizes Proposition 1 of the accepted manuscript, dated September 16, 2022. Its source is the repository manuscript; the numbering and printed pages here refer to that artifact, not the journal typesetting (Akerlof, Holden and Rayo, Proposition 1, p. 10).
There is a unit mass of consumers, each with unit demand. Write for firm 1's relative price, and let be its current total sales. The aggregate demand is the quantity that would be demanded at price if consumers believed sales were . With one firm, the paper sets the second firm's price and quantity to zero, so the same two-argument demand map applies. With two firms, is the difference of their prices. An equilibrium quantity is a feasible fixed point,
The inverse demand curve gives a price at which a given quantity is self-consistent: for . The market assumptions say demand is continuous in price and feasible quantity, decreases with price, and increases with believed quantity. The formal market records weak monotonicity together with strict price comparisons at an inverse-demand point on the nonsaturated part of the range. These comparisons give the signs used in the paper's footnote 12 (§2, p. 5; footnote 12, p. 10).
An In/Out curve has two quantity thresholds . The curve is strictly decreasing and convex on , strictly increasing on , and strictly decreasing and concave on ; convexity and concavity here are weak. Define and . The endpoint conditions are and . At a price between the thresholds, the intersections of with the three branches are , , and . At either threshold price, two adjacent branch labels can name the same quantity (footnote 7, p. 6; §2.1, p. 8).
The consumers' impulse lies in . Level- consumption is the actual iteration , or with at level zero. An introspective equilibrium is the limit of this sequence as (Definition 1, p. 9).
For , the three branch quantities are distinct and exhaust the feasible equilibrium quantities. At or , two distinct quantities remain. The milestone from §2.1 also records uniqueness within each branch. Footnote 12 records where lies above or below between these intersections (§2.1, p. 8; footnote 12, p. 10).
The goal is the full two-part Proposition 1. When , the branch equilibria exist and
When or , exactly one feasible quantity solves , and converges to it for every . The proof's convergence and uniqueness passages are separate milestones, so the goal retains both claims without taking either as an extra assumption (Proposition 1 and proof, p. 10).
Proposition 1 ties a market's adoption outcome to the initial impulse. In the multiple-equilibrium price range, the middle equilibrium separates impulses that select the low and high quantities; outside that range, the selected quantity is independent of the impulse. This makes the refinement usable when the subsequent economic analysis asks how a price or a change in expectations can move the market between dominant firms (§2.1–§3).
The paper proves the result in ordinary mathematics. The remaining work here is a machine-checked proof of its precise selection statement and of the source passages that support it. The definition layer also supplies a reusable interface for continuous aggregate demand and inverse demand on a bounded quantity interval. There is no claim that this paper's later pricing-game propositions have already been formalized.
The inverse-demand picture shows three crossings, but a picture alone does not establish that every branch crossing exists or that no additional feasible fixed point is present. At a threshold, two branch labels meet, so a claim that always demands three distinct quantities would be false. Outside the threshold interval, the paper's reference to a unique intersection of fails at prices beyond or : the equilibrium can instead be a saturated fixed point at or . The formal statements must cover those prices with (Proposition 1 and proof, p. 10).
The convergence claim concerns a specific recursive sequence from every allowed impulse. Fixed-point existence by itself does not identify that limit or its dependence on the impulse. The market assumptions also require care at the saturation endpoints: strict decrease in price on the whole real line would conflict with nonnegative demand at , while merely weak decrease permits extra fixed points that would defeat the selection claim.
Lean represents prices and quantities by real numbers and restricts feasible quantities and impulses to . A Market stores , , continuity of on real prices and feasible quantities, range bounds, weak monotonicity in quantity and price, the inverse-demand identity, and the strict nonsaturation signs from footnote 12. The paper says demand is strictly increasing in quantity below ; the formal interface uses weak increase because its own saturated consumer model can have a constant zero-demand segment. The strict price signs make explicit the stronger reading of “decreasing” needed at inverse-demand points. Both choices are disclosed in the setting item. The polynomial and clamped-demand example in the local verification file witnesses that the assumptions are consistent.
IsInOut retains every monotonicity, convexity, concavity, threshold-order, and endpoint condition of footnote 7, even when a clause is unused in a proof. The branch quantities are predicates that include their intervals and the equation ; the goal asserts their existence before quantifying over them. IsIntrospectiveEq uses Function.iterate and Tendsto for the prescribed , so it cannot be satisfied by selecting an unrelated fixed point or sequence. Outside the threshold interval, uniqueness is over feasible fixed points of , including and . The assumptions apply to the aggregate map for either one or two firms; consumer types, their distribution, the micro-foundations, the firms' pricing game, profits, the WIN constraint, Corollary 1, and later sections are outside this mission.
A complete development needs continuity and intermediate-value results, monotonicity and convexity of real functions on intervals, and convergence of bounded sequences of real numbers. The market and level- definitions can be reused by later work on equilibrium selection. Contributions may prove the listed milestones, supply independent proofs of Proposition 1, or build the interval-dynamics lemmas they require, while retaining the statement's full price and impulse domains.
Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a certain sum code must occupy only a controlled number of complete rows and columns. The deterministic distance theorem in Leverrier and Zémor's Quantum Tanner codes assumes this condition; their Theorem 9 supplies it for randomly chosen component codes. Establishing that random codes satisfy the assumption makes the later existence result meaningful rather than conditional on a property with no known examples.
The appendix follows the approach of Panteleev and Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, with a separate treatment of puncturing. The historical relation here is limited: this mission formalizes Leverrier and Zémor's Theorem 9 and its own numbered supporting results, with their hypotheses and constants.
Fix two coordinate sets and , each of cardinality . A binary linear code is a vector subspace; similarly . Regard a word on as a matrix . The column code contains matrices whose column at every belongs to . The row code contains matrices whose row at every belongs to . Their intersection is the tensor code ; their sum is the dual tensor code . The Hamming weight counts its nonzero entries. These conventions are those of §3.5 of the source paper.
Write for the actual minimum distances of the two component codes. The dual tensor code is -robust if every codeword with vanishes outside the union of some set of at most rows and some set of at most columns. Thus a low-weight word cannot be spread thinly across many rows and columns. For retained coordinate sets and , the punctured codes and are the images under restriction. Robustness has -resistance to puncturing when the corresponding dual tensor code remains -robust for every pair of equal size obtained by removing at most coordinates from each side. These are Definitions 5 and 8 on pp. 15–16 of the paper.
A uniform generator matrix with rows and columns is sampled uniformly from all binary matrices of that shape. Its row span is . Independently, a uniform parity-check matrix with rows and columns defines as its kernel. Probability is the fraction of matrices, or matrix pairs, satisfying an event. In the asymptotic statement, tends through natural numbers to infinity.
For , , and , sample and from the matrix models above, using generator rows and parity-check rows. The goal, Theorem 9, is
The milestones are the paper's numbered appendix statements: Lemma 31 converts concentration on few rows and columns into Definition 5's sharper weight-based bounds; Lemmas 24–29 address ranks and probabilities for random kernels and punctured kernels; Theorem 30 gives the quantitative high-probability alternative used before the final limit. The goal fixes the exponents and quantifies over the whole uniform matrix experiment.
Theorem 9 certifies that the robustness hypothesis needed by the paper's distance construction occurs with asymptotic probability one. It covers all allowed puncturings at once, which matters because a later distance argument deletes coordinates selected by the codeword under study. A statement about one fixed puncturing would not provide that guarantee. The result is proved in the 2022 paper; this mission poses its statements for machine-checked proofs and does not claim that those proofs already exist.
Formalizing the result produces reusable finite probability statements for random linear codes, a parity-check treatment of puncturing, and rank bounds for sparse binary matrices. Those ingredients are independent of the group complex used in the paper's other mission. They can support later formalizations of random coding arguments where a union over many coordinate restrictions is necessary.
The evident first check is that one fixed low-weight matrix probably does not belong to a random dual tensor code. That alone does not establish robustness: the statement ranges over all such matrices and, for resistance, over every pair of large retained coordinate sets. The paper's intermediate results control this whole collection using rank information about sparse matrices and the exact probability that independent vectors lie in a random kernel. A further issue is that puncturing a parity-check code does not simply delete columns from its defining matrix; the discarded columns contribute a random subspace. The quantitative event in Theorem 30 and the simultaneous limit in Theorem 9 both have to survive these ranges.
Lean uses ZMod 2 for , Fin \Delta for each coordinate set, and functions on for matrices. Rows are indexed by and belong to ; columns are indexed by and belong to . The published TillichZemor.HGP.Setting supplies the parity-check kernel and the extended-natural minimum distance, whose value is infinity for the zero code. CodingTheory is a published prerequisite. Local definitions give the row and column codes, their sum, puncturing, robustness, uniform finite probability, generator row span, and binary entropy in bits.
The printed matrix sizes and need integer values. The chosen floor and ceiling keep their respective dimensions within the bounds used in the appendix. Every logarithm in the formalized appendix bounds means , including occurrences printed simply as . Theorem 30 includes an explicit sufficiently-large- threshold, as its proof's asymptotic count requires, and carries the appendix's preceding entropy condition as and . Lemmas 25, 26, and 29 use the preceding condition ; the symbol beside in the scan is ambiguous, and the argument on p. 29 determines this reading. These choices are recorded for audit in MODERATION_NOTES.md.
The probability space is all matrices of each stated size, with the two matrices in Theorem 9 sampled independently. There is no conditioning on a favorable code or an assumed version of Theorem 30 in the goal. The mission does not formalize the later quantum Tanner code construction or the cited Gilbert–Varshamov result as an additional item. Contributions proving the goal, the numbered milestones, or reusable rank and finite-probability facts are within scope.
Entrepreneurs sometimes sell claims on a product before it exists. A token can represent a claim on a future unit, and its eventual market price can depend on how much the entrepreneur produces. That link creates a production incentive absent from a simple sale of equity. Malinova and Park study whether the token allocation can fund a venture while preserving the output choice that maximizes operating profit Malinova and Park, 2023. Their Proposition 3 gives a contract that does so under exogenous demand. This mission formalizes that proposition, including its investor break-even calculation and the uniqueness of the pre-sale size.
The paper first examines two simpler arrangements. Giving investors a fixed fraction of revenue leaves the entrepreneur paying the full marginal cost while receiving only part of the marginal revenue, which induces underproduction. Selling a fixed number of output units without a later revenue share induces overproduction: an extra unit reduces the price of units already promised to investors, a cost the entrepreneur does not bear. These comparisons are Lemmas 1 and 2 of the paper Malinova and Park, pp. 18–20. Proposition 3 combines an output pre-sale with a share of tokens issued after production.
At time zero, an entrepreneur must pay a set-up cost and obtains financing from investors. At time one, the demand intercept is observed. It is uniform on , and producing units gives the inverse price . Each unit costs , where . With no financing distortion, monopoly output and operating profit are
For a realized payoff , . The project's net present value is . This mission assumes , the positive-NPV case of Proposition 3. Equation (3) evaluates it as Malinova and Park, p. 14.
Under the proposed token contract, investors buy initial tokens at time zero, providing . If production exceeds , the entrepreneur issues more tokens and grants the initial holders the fraction of those new tokens. If production is at most , token-holders receive the full output and a refund of the unused production funds, . Let and be the resulting realized payments to the entrepreneur and investors. Their definitions follow the two output branches of the contract Malinova and Park, pp. 21–24, 39–40.
For every demand realization and every feasible output, monopoly output maximizes the entrepreneur's realized payment under this contract:
The claim includes the low-demand branch , where several outputs can yield zero to the entrepreneur. No uniqueness of the production choice is claimed.
Investors must receive in expectation. For , this requirement is equivalent to the paper's equation (16):
Proposition 3 and its Appendix A proof assert that the equation has exactly one positive solution , that the solution lies below , and that the entrepreneur then receives Malinova and Park, pp. 24, 39–41. Milestones cover the revenue share, the high- and low-demand cases, the investor integrals, the entrepreneur's expected payoff, and the existence and uniqueness of the break-even size.
The result shows that token financing can preserve monopoly output in this model even though the two simpler token arrangements distort it. It identifies both the later-token share and the unique number of units to pre-sell, with investor break-even and the entrepreneur's full positive NPV in one contract. That contract provides the baseline for the paper's comparative statics and its later moral-hazard comparison of equity, tokens, and debt Malinova and Park, Propositions 4 and 8.
The result is proved in the cited paper. The remaining work here is a machine-checked development of its piecewise payoffs, interval integrals, and real-analysis claims. This proposal contains open Lean statements and definitions; it does not claim that their proofs have been completed. The expectation, monopoly payoff, and contract representations can also support subsequent formalizations of the paper's cost and demand comparisons.
The simple first-order calculation behind the revenue share covers the branch , but it does not establish the entrepreneur's incentives when output is at most the pre-sale. In that branch her contractual payment is zero, and the refund rule changes the investor payment. The output claim must compare every across both branches, including the threshold .
The financing claim has a separate difficulty. Investors receive three different payments over the demand ranges , , and . Their expectation must equal the explicit cubic equation, while the entrepreneur's expectation must equal its left-hand side. A root argument stated only for the cubic would omit the economic break-even assertion. The paper also uses the interior bound when evaluating the entrepreneur's expectation Malinova and Park, Appendix A, pp. 39–41.
Lean uses real parameters and a real interval integral for uniform demand. The expect definition integrates the realized payoff over and divides by ; endpoints have zero mass. The definitions qm and pim use a nonnegative maximum to represent no production below cost. The entrepreneur and investor payments use the contract's two branches. NPV is defined from the integral, while the formula in equation (3) is a theorem. Equation (16) is a predicate on , while the corresponding expected-profit identity is another theorem. No closed form replaces an expected realized payment by definition.
The hypotheses , , , and express the paper's positive-cost, productive, positive-NPV setting. A milestone about an integral over the upper demand region assumes ; a milestone about the cubic expected profit uses the same range. Proposition 3 states the break-even equivalence on the interior and establishes that its unique positive solution lies there. Output optimality is among under the specified contract. The paper does not define a space of all possible financing contracts, so the Lean statement does not claim an optimization theorem over such a space.
The secondary token market, the physical redemption mechanism, bankruptcy costs, consumer welfare, and the institutional discussions of Sections I and V are outside this mission. Needed reusable work includes real interval integration of piecewise polynomial payments, algebraic comparisons of quadratic payoffs, and strict monotonicity of the break-even cubic. Contributions that prove the listed statements while retaining the realized-payoff definitions are welcome.
Agricultural subsidies can raise total crop supply while changing which farmers produce it. A payment tied to planted input gives a larger reward per unit of harvested output to a farmer who needs more input for that output. A payment tied to harvested output gives the same reward per unit of output to every farmer. These differences matter when a government cares about the distribution of production and income across farms as well as total supply. Fan et al. (2023) study these effects in a finite market where farmers choose quantities and compete through a common market price.
This mission isolates the paper's distribution result for a combined subsidy, which pays on both planted input and harvested output. It asks how a difference in the dispersion of farmers' input-to-output ratios between two otherwise identical markets affects their equilibrium output and profit. The result is Proposition 4 of the SSRN version. The paper proves it in Online Appendix A, p. 4. The result is mathematically stated and proved in the paper; the machine-checked formalization of its statement and proof is the work here.
There are farmers, indexed in the paper by . Farmer must plant units of input to harvest units of output. Thus is an input-to-output ratio; a smaller ratio means more output per unit of input. The ratios are listed in nondecreasing order. Planting costs per unit of input, harvesting costs per unit of output, and total harvested output is . The market-clearing price is , where .
Under a combined subsidy , farmer receives per unit of output. The first part is payment for planted input and the second for harvested output. A farmer choosing while the other farmers' outputs stay fixed has profit
An equilibrium is a nonnegative output vector at which no farmer gains by changing its own nonnegative output. Costs and subsidies are real-valued: the paper permits a subsidy larger than its associated cost and also permits a negative subsidy, or tax. The formulas in this mission concern equilibria at which every farmer produces a positive quantity.
To compare dispersion, let be the sum of the largest entries of a vector . A vector majorizes , written , when for every and their total sums agree. The weak sub-majorization relation keeps the top-sum inequalities and drops equal totals. With this direction, says that is more dispersed. These are the orders of Definition 1 in Fan et al..
The first milestone formalizes Proposition 3's active branch. Write and . At an equilibrium with every farmer active, it states
The remaining milestones formalize the increment identities written in the proof of Corollary 1 and the two order properties invoked in the proof of Proposition 2: majorization under an affine map, and weak sub-majorization under an increasing convex map. These are the results used to interpret the change in each farmer's output and profit when a subsidy changes.
Consider markets and with the same , but with ratio vectors . Give them the same subsidy and let . For a vector of equilibrium outputs, is the difference between outputs at and ; is defined using . Profit increments use the corresponding profits at those equilibria. Proposition 4 asserts
The equality means majorization in both directions. These comparisons form one goal theorem so every part of Proposition 4 remains present. Proposition 4, p. 13 is the source for the target.
The first output comparison says that greater dispersion in input-to-output ratios leads to greater dispersion in equilibrium production under the same combined subsidy, while the total output stays equal. The increment comparisons identify which changes preserve or distinguish that dispersion when planting and harvesting payments increase. The profit statements give the corresponding order for farmer earnings. They make the distributional effect of a subsidy explicit rather than reducing it to a claim about aggregate crop supply.
A formal development supplies reusable definitions for finite majorization, this Cournot market, and best-response equilibrium. It also separates the paper's claimed order relations from the algebraic equilibrium formula. Proofs of the paper's known results remain to be checked in Lean. The mission makes no claim that Proposition 4 is an open research problem.
Directly comparing farmer in the two markets cannot establish majorization: the order compares sums of the largest coordinates, which need not belong to the same farmers in each market. The sign of can change because planting payments are unrestricted, so the ordering of farmers by output can reverse. Profit is quadratic in output, and the profit comparison is weak sub-majorization rather than equality of totals. Subsidy increments introduce additional equilibria; an increase in the planting payment can also alter which farmers are active. These features must be accounted for in a statement that retains every clause of Proposition 4.
Lean represents the paper's farmers by Fin N, so paper farmer has Lean index . The shared parameter record contains ; each market supplies its own sorted vector . A standing predicate records , , the ordering of , and . The positive-ratio condition makes explicit that each ratio is formed from positive physical quantities. The two markets have the same parameter record, and no sign restriction is imposed on costs or subsidies.
The combined payment is a per-unit-output vector . Equilibrium is a best-response condition over nonnegative output, not a definition by Proposition 3's formula. The top-sum order uses all subsets of farmers, with equal total sums required for majorization. Averages range over all farmers because the theorems work in the all-active regime. This rules out treating a formula-defined output vector or a weakened order as the market result.
The goal explicitly assumes positive output at the baseline and at both shifted subsidies. Positivity at the planting-shifted subsidy is needed for the paper's fixed-active-set increment formula but is unstated in Proposition 4. Positivity at the harvesting-shifted subsidy is implied by this market model; it is kept explicit without assuming an equilibrium-uniqueness theorem. The supporting increment milestone also includes an active equilibrium at the midpoint harvesting subsidy. The majorization lemmas can be reused for other finite-vector models, and the equilibrium characterization can support later analyses of this paper's subsidy programs.
In reward based crowdfunding, customers must decide whether to back a product before its quality is known to them. The entrepreneur knows that quality and chooses a funding price. A high quality entrepreneur may therefore use price to convey information, but the same price is available to a low quality entrepreneur. The choice also changes the chance that the campaign meets its financing target. Bolandifar, Chen, Kouvelis, and Zhou study how these effects interact when the entrepreneur chooses a second, regular selling price after the campaign succeeds. The one price mechanism in this mission concerns the case in which only the funding price is posted in advance.
The question matters to the design and interpretation of crowdfunding campaigns. A lower funding price can be a credible quality signal even though it forgoes immediate revenue. Whether that signal is sustainable depends on the later selling opportunity, the financing target, and the different incentives of the two quality types. The paper gives a precise threshold for the financing target below which one separating outcome survives a refinement of the equilibrium concept.
The entrepreneur's product has privately known quality , either low or high , with . The financing target is . The entrepreneur posts a funding price . Funding period customers all share a taste uniformly distributed on and evaluate the product using believed quality . They back it when . The funding market has size one, so a successful campaign raises at least and occurs with probability for . The formal definition extends this probability by zero for larger prices.
After success, true quality is revealed and the entrepreneur sets a regular selling price . A fraction of regular period customers have the same taste as the funding customers. Their taste distribution is therefore updated after success. The other regular customers have a fresh, independent uniform taste. The regular market also has size one. Production cost, salvage value, and discounting contribute no additional terms. Conditional regular period profit is , the two branch function in equation (2) of the manuscript. Its optimal value is the supremum over feasible . The total expected profit is the success probability times .
A separating equilibrium assigns different feasible funding prices and to the two entrepreneur types. Customers believe quality is high at and low at every other price, including off path prices. Under those beliefs, neither type benefits from a feasible deviation. The intuitive criterion removes an equilibrium if an off path price would strictly improve the high type's profit while strictly reducing the low type's profit, were customers to interpret that deviation as a high quality signal. This is the paper's stated test, with the strict low type comparison used in its appendix.
Define the price threshold
The goal is Proposition 1 of the manuscript. If , there is a separating equilibrium surviving the intuitive criterion, and every surviving separating equilibrium has exactly the prices
The formal goal also says that no separating equilibrium exists when . Its scope on this side of the threshold follows the manuscript's proof and the nondegenerate funding market; the printed “otherwise” sentence does not hold literally when .
Lemma 1 identifies the optimal regular price and its attained profit in each of three funding price ranges, split at and . Lemma 2 identifies the funding profit's single peak and the maximizing price . The three parts of Lemma 3 characterize the low type's mimicking indifference prices, the high type's upper indifference price, and the ordering of these thresholds. These are the milestones leading to Proposition 1.
The proposition gives both types' prices and shows why the high type's credible signal is a lower funding price than the low type's. It also identifies a financing target above which this separation disappears within the paper's nondegenerate range. The result relates a platform design parameter, the target, to equilibrium information revealed by price.
The result is proved in the cited manuscript, with proofs in Appendix A. The remaining work in this mission is a machine checked proof of the model's price optimization and equilibrium claims. The definition of the two period payoff, the treatment of the later optimal price, and the explicit deviation predicates may be reusable for other crowdfunding signaling mechanisms. The draft statements are open proof targets; the present mission does not claim those proofs are already formalized.
The later optimal price changes form as the funding price crosses two thresholds. That makes total expected profit a piecewise function, even before the two types' incentives are compared. Maximizing either type's full information payoff alone does not determine a separating equilibrium: the low type might imitate the high type, while the high type might deviate to a price customers would interpret as low quality. The intuitive criterion imposes a further comparison at prices outside the equilibrium path. The claim requires all of these comparisons with the same underlying payoff definition.
Lean uses one tuple of real parameters and the standing restrictions , , and . The prior probability of high quality does not occur in the separating price statements. The regular profit is the printed equation (2), with a positive regular price at most true quality. Campaign success probability is clipped at zero for funding prices above believed quality. Funding prices range over all reals at least ; the maximum profits are defined as suprema over those feasible prices. Milestones assert attainment, so those suprema cannot be replaced by convenient formula values.
The model uses the paper's market size, cost, salvage, and discount normalizations. Lemma 1 excludes : at that endpoint the printed third case can specify an infeasible regular price. Lemma 2 assumes and quantifies only over the four true and believed quality combinations. Lemma 3 is stated for to avoid its circular printed preamble, and one threshold comparison is expressed as a strict profit inequality because the lower crossing can lie below . Proposition 1 does not assert pooling existence, which would require the omitted prior; its no separation clause is restricted to .
Contributions toward the piecewise optimization lemmas, the threshold characterization, and the equilibrium theorem are welcome. The separating equilibrium is defined by incentive comparisons over all feasible deviations, and its refinement is defined by the off path deviation test. The optimal profits are supremum values of the model payoffs. These choices keep the goal from collapsing into a restatement of a closed form or of the paper's derived necessary and sufficient conditions.
An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called and errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the number of qubits grows. For years it was difficult to make both the number of encoded qubits and the minimum distance proportional to the block length while retaining bounded-weight checks. Leverrier and Zémor's quantum Tanner construction gives a route through local codes placed on an expanding square complex; its main distance theorem is the target of this mission Leverrier and Zémor, 2022.
The construction combines two earlier ingredients. Left-right Cayley complexes provide the squares and expansion properties used by the code Dinur, Evra, Livne, Lubotzky, and Mozes, 2021. Robustness of a dual tensor code, including after puncturing coordinates, controls local words Panteleev and Kalachev, 2021. The paper states the local reduction property as Theorem 1 and derives the rate and distance bounds as Theorem 17. This mission formalizes that implication under the paper's stated component-code and expansion conditions; the separate random-code result that supplies robust examples belongs to the second mission of this series.
Let be a finite group and let be inverse-closed sets, each of size . The total no-conjugacy condition says for every , , and . Vertices are two copies of the group, . A square associated with and has vertices , , , and . The set of squares is , and a binary word on has length . At a vertex , the incident squares are indexed by ; this indexing makes the local view of a word an matrix Leverrier and Zémor, §§3.2 and 4.1.
A binary linear code has coordinates indexed by , and has coordinates indexed by . Their tensor code consists of matrices whose columns lie in and whose rows lie in . The dual tensor code is the sum of the column and row codes. In Definition 5, it is -robust when every member of weight at most is supported on a union of few rows and columns, with the bounds determined by the two component minimum distances. Definition 8 requires this property after deleting up to coordinates from each side. These are conditions on all relevant codewords and all permitted puncturings, including the unpunctured pair Leverrier and Zémor, pp. 15–16.
The two Tanner codes are and . Here is the square-adjacency graph on the vertices in copy . Together they define the quantum CSS code . Its dimension counts encoded qubits. Its distance is the smaller of the minimum weights in and Leverrier and Zémor, pp. 14, 18.
The goal is Theorem 17. Fix , , , and . For sufficiently large , take a left-right Cayley complex satisfying total no-conjugacy and the paper's Ramanujan conditions. Require , , minimum distance at least for and both duals, and robustness with resistance to puncturing for both relevant dual tensor codes. The target is
The milestones mirror the paper's route to this result. Lemma 4 bounds the nontrivial eigenvalues of the union and square graphs. Propositions 6 and 7 turn dual-tensor robustness into a decomposition and a closeness bound. Theorem 1 supplies a weight-reducing local codeword for every sufficiently light nonzero Tanner-code word. Display (5) supplies the dimension lower bound. Theorem 17 combines the two distance directions with that rate estimate Leverrier and Zémor, pp. 12, 15–16, 18–23.
The lower bound on ensures a positive fraction of qubits can carry logical information when . The lower bound on rules out small undetectable logical errors. For a fixed allowable degree , both bounds scale linearly with . The paper also shows that random component codes can satisfy the robustness assumptions; that probabilistic result is a separate formalization target Leverrier and Zémor, Theorems 9 and 17.
A checked development would make explicit how the square indexing, duals, punctured codes, and CSS quotient fit together. The source proves the mathematical result; the statements here remain open Lean theorems. Reusable contributions include the tensor-code interface, spectral bounds for the graph construction, and lemmas connecting local views to the global Tanner codes. A proof of the existence of infinite Ramanujan complex families is outside this mission's stated target.
A light global codeword need not have a local view that is itself close to a tensor-code word. Some square-graph vertices have unusually large local weight, and puncturing is needed to isolate coordinates shared with those exceptional vertices. The paper's small-set expansion estimates and robustness conditions control those interactions. Simply averaging local weights does not yield the weight-reducing local codeword asserted by Theorem 1 Leverrier and Zémor, §4.2.
Words are functions into ZMod 2, codes are submodules, and a matrix is a function on with indexing rows. The square coordinates are four-element vertex sets. The construction uses and counts as the number of squares rather than building into a definition. The minimum distance of the zero code is infinity, and robustness uses inequalities involving that extended value. Powers of and the parameters are real; the paper uses integer in Definition 8, while the theorem's power thresholds need real comparisons. The formal robustness predicate includes Definition 5's range ; the theorem thresholds satisfy it for sufficiently large . These conventions are recorded with each item.
The goal quantifies over every finite complex satisfying inverse closure, total no-conjugacy, and Ramanujan conditions, with a uniform threshold chosen before the group and codes. This pins the complexes in the cited infinite family without formalizing their existence. In particular, the goal contains no auxiliary set or local reduction assumption that could make the distance bound immediate. The published CodingTheory and TillichZemor.HGP.Setting definitions supply dual codes and CSS dimension; the paper-specific setting supplies the square complex, local views, Tanner codes, and robustness. Contributions that keep these conventions and close any milestone theorem are welcome.
Certify the classical quadratic separation between sensitivity and block sensitivity: .
For a total Boolean function , write for the input obtained by flipping the coordinates in . Its sensitivity is . Its block sensitivity is the largest number of pairwise disjoint nonempty sets that satisfy at a common input .
The goal is to prove that for every and every integer , there is a total Boolean function with
The construction milestone is Rubinstein’s quadratic separation: for each integer , there is a function on bits with
These exact bounds imply the goal because and sensitivity grows without bound. This is a known theorem; the task is to formalize it using the campaign’s shared definitions.
The main combinatorial work is controlling sensitivity at every input and proving the matching block-sensitivity bounds. Lean represents functions as (Fin n → Bool) → Bool; both measures are maxima over all inputs. The goal reuses SensitivityCampaign.AchievesExponent, so it has exactly the same meaning as the campaign’s stronger targets. No composition theorem is required for this family argument.
References: David Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica 15 (1995), 297–299, DOI. The statement and construction are also recalled in Theorem 1 of Madars Virza, Sensitivity versus block sensitivity of Boolean functions (2010), arXiv:1008.0521.
A ride-hailing firm chooses prices while drivers move through a city. A trip from one region uses a driver immediately and returns that driver at another region only after a travel delay. Prices affect which trips are requested, but the actual requests fluctuate. A plan that ignores these fluctuations can run out of available drivers at a busy origin even when its average flows fit the fleet. Chen, Lei, and Jasin study how closely a feasible pricing control can approach a deterministic revenue benchmark in this setting (accepted manuscript, published article).
Their Arc Balancing Control (ABC) responds to realized trips. It groups each directed arc's periods into batches and adjusts the next batch's demand rates according to the previous batch's cumulative surplus or deficit. The paper proves a loss rate for ABC that is smaller than the rate established there for its Static Price Control. The target here is the paper's Theorem 3, with the model and parameters of its authors' accepted manuscript. Its e-companion contains the paper's proofs.
The network has regions and a horizon of periods. Every ordered pair , including , is an arc. At most one customer can request an arc's trip in a period. A served trip takes one server from region for periods, then returns it at . Region starts with servers. A control must respect the available server count before it serves each period's realized requests.
The decision is a demand rate rather than its inverse price. The expected revenue from that arc and period is . The revenue functions are nonnegative and strongly concave, vanish at zero, and have bounded first and second derivatives. The bound on those derivatives is . The paper's price-side assumptions imply these rate-side conditions; the Lean model states the conditions directly.
The deterministic convex program chooses rates to maximize the sum of expected revenues. Its flow constraints replace realized trips with their rates, while its cushion requires . Write for its value and for an optimal schedule. In the th system, the fleet, horizon, and travel times are multiplied by ; each original period's revenue curve is used for consecutive scaled periods. Thus and . For a control , the per-period benchmark loss is
ABC uses as its baseline. Its batches have a target sum of the baseline variance weights . Within a batch, the control subtracts a weighted share of the preceding batch's realized surplus . A rate is projected to , and an origin with too few available servers is turned off. The finite path law uses the rates posted along each path.
The principal target is Theorem 3. With and
there is a constant , independent of , for which every integer satisfies
The milestone list follows the source results used in the analysis: Lemma 2 bounds the deterministic cost of a small cushion and gives feasibility; Lemma EC.1 bounds a maximal cumulative Bernoulli deviation; and the two parts of Lemma 4 characterize ABC on a batchwise good event and bound that event's probability. Theorem 3 fixes the complete control and these exact parameters; its constant may depend on the fixed network instance and .
The theorem gives a finite- loss bound relative to , with the stated rate and logarithmic factor. In the paper, Lemma 1 shows that bounds the optimal admissible policy's revenue. Theorem 3 therefore bounds ABC's distance from a benchmark that is at least as high as the unknown stochastic optimum. The paper compares this rate with its result for Static Price Control and explains the resulting value of adapting prices to realized demand (Theorems 2–3).
The published mathematical result and its manuscript proof are known; the statements in this mission are Lean targets with proofs still to be formalized. A complete development would also make reusable definitions for finite controlled path laws, delayed network flow balance, and cushioned deterministic relaxations. The batch and feedback definitions isolate the paper-specific control from that general infrastructure.
The deterministic program controls expected flows, while ABC must keep every realized path feasible. An unadjusted baseline can accumulate demand fluctuations over the whole horizon; bounding those fluctuations alone does not describe the effect of ABC's feedback. The control's posted rate in a period depends on earlier realized requests, which changes the distribution of later requests. The manuscript's proof of Lemma 4 bounds a variance proxy from its deterministic baseline when treating the adaptive posted rates; that step needs separate justification in a formal proof. Lemma EC.1, as posed here, covers deterministic Bernoulli rates and does not by itself close that gap. The finite-horizon claim, including small scaling factors for which the cushioned DCP may be infeasible, must still be established.
Lean represents regions by Fin N, periods by natural numbers , travel times and server counts by naturals, demand by Boolean paths, and revenue and rates by real numbers. The program uses a real supremum; statements involving positive assert feasibility, and has the zero schedule as a feasible point. ABC's path law is the product of sequential Bernoulli factors at its own posted rates. Its rate history is built by structural recursion, and the event checks every nonempty batch and all its partial sums.
The accepted manuscript leaves the final incomplete batch unspecified, so the last short batch is merged with its predecessor. The printed ABC box turns an origin off at , while Lemma 4 and its base case require service when ; the formal control uses . If the cushioned DCP has no optimum, the baseline is zero. The sample-path part of Lemma 4 adds the hypothesis , which the manuscript does not print. Without it the part is false: when the horizon is shorter than every travel time, no server returns, and a single realized trip can leave a region below servers on the good event. These conventions are recorded with the source discrepancies in the moderation notes. The rate model drops assumptions A1 and A3(i), which concern only the price parametrization, and writes A2, A3(ii), , and directly. It assumes a twice continuously differentiable extension of revenue to . No statement substitutes expected demand for the realized batch surplus or lets the theorem's parameters depend on by existential choice. Contributions toward the source milestones, the adaptive concentration step, and the reusable model definitions are all within scope.
A firm can learn a customer's preference before choosing a customized product, or it can let the customer choose a requested design. The two approaches assign the design decision to different parties. That matters when design changes both the value of a sale and a cost the seller must incur before the price is negotiated. Guo's study of customer voice in customization compares these approaches in a model where a buyer has private information about how much it values quality. The payoff comparison asks who gains from holding the design right and whether the answer survives a modest fixed cost of using that approach.
This mission concerns Proposition 8 of the SSRN author copy, printed page 23. The result is a comparative statement about two already specified separating equilibrium outcomes. Earlier results in the same paper characterize when the outcomes arise: Proposition 1 treats communication before seller design, and Proposition 3 treats a buyer's design request. Proposition 8 compares the parties' payoffs at the qualities associated with those outcomes. Its four clauses distinguish gross payoff rankings from net rankings after an incremental fixed cost. The paper states Proposition 8 without a separate proof; its surrounding discussion explains its interpretation. All page and result numbers here follow the SSRN version of 2023-11-29.
There is one seller and a unit mass of buyers. Each buyer has one-unit demand and a privately known quality preference , with type and . The high type has population share , while the low type has share . A product's quality is a nonnegative real number . Producing a unit of quality costs , and offering that product incurs a selling cost , where . The selling cost is incurred before the price is settled. The seller makes a take-it-or-leave-it offer with probability ; the buyer does so with probability . These primitives and the timing are specified in Section 2.
In A-Learning, the buyer sends a costless message about its preference and the seller chooses the design. In O-Learning, the buyer requests a quality and the seller decides whether to accept it. The paper compares separating outcomes, so each type is associated with its true preference when the equilibrium payoff is evaluated. The pricing stage is represented by the paper's payoff formulas. If the seller regards a buyer's preference as , its payoff from quality is
The buyer's payoffs and retain the nonnegative parts in equations (5) and (9): each is , with its arguments ordered as in the relevant equation. For type , the paper's A-Learning and O-Learning equilibrium qualities are
Write and . The seller's expected gross payoffs are and . The buyer payoffs and evaluate and at type 's quality and truthful preference. These are the payoffs defined around equations (8) and (13) of the paper.
The first comparison says that the seller earns more from its own design, while each buyer type earns more from its requested design:
The two fixed-cost clauses hold the preference levels, population share, bargaining weight, and production-cost coefficient fixed while the positive selling-cost coefficient varies. For every seller-side incremental fixed cost , there is a positive threshold such that
For every buyer-side incremental fixed cost and each type , there is a positive threshold such that
The goal is the conjunction of these four clauses, exactly the payoff content of Proposition 8. The milestone list also includes the paper's strict quality comparison and its observation that the quality difference tends to zero as tends to zero. The printed statement and discussion are on pages 22–23.
The gross comparisons separate the seller's and buyers' preferences over who chooses quality. The fixed-cost clauses show why the party favored by the gross comparison need not favor that approach once its own extra effort or implementation expense is counted. The thresholds make this claim uniform over all sufficiently small positive selling costs, rather than treating the single case . This distinction is relevant when comparing preference solicitation, which requires seller effort, with buyer-led design, which requires customer effort.
Formalizing the result gives a reusable two-type model of quadratic production and selling costs, the two reduced-form buyer payoffs, and a finite-population expected-payoff calculation. It also creates separate targets for each clause, so the gross-payoff and small-cost claims can be checked independently. The result is proved in the mathematical paper only to the extent of its stated Proposition 8 and accompanying discussion; the local Lean statements in this proposal compile with proof placeholders and do not yet constitute machine-checked proofs.
The two approaches select different quality formulas, and O-Learning uses a minimum of two expressions. As changes, that minimum can switch branches. The buyer payoff formulas also contain maxima with zero, so replacing them unconditionally with simplified quadratic expressions would change the model. A valid payoff comparison must account for the relevant branch and preserve the strict inequalities for both buyer types. For the fixed-cost clauses, pointwise closeness at does not itself state a uniform claim for every sufficiently small positive ; the threshold must be positive and chosen before .
The Lean model uses a two-constructor buyer type, real parameters , and a Standing predicate carrying every displayed positivity and interval assumption. Qualities are real-valued, with the paper's intended domain ; the closed-form equilibrium qualities in this mission are nonnegative under those assumptions. Expected seller payoffs use a finite sum over exactly the high and low types, weighted by and . Buyer payoffs use the original maxima with zero. The pricing stage is in reduced form through equations (4), (5), and (9). The model and payoff notation are local to CustomerVoice.Payoffs, because the other missions' definitions are unpublished drafts.
The statements compare the printed closed-form qualities without adding the separate inequalities that guarantee both separating equilibria exist. Thus their domain is all parameter choices satisfying Section 2's standing assumptions; this is the stronger reading identified in the paper's planning notes for Proposition 8. In the small- statements, withS changes only the selling-cost coefficient, and the quantified values of satisfy . The proof targets cannot be reduced by deleting the nonnegative parts of the buyer payoffs, allowing a zero threshold, or checking only the limit at . Contributions to the elementary quality comparisons, branch-sensitive payoff inequalities, and positive-side limits all support the goal. The finite weighted-payoff and limit infrastructure can be reused in other small-cost comparisons.
A delivery vendor controls both how a courier serves orders and what customers pay. Serving one order per trip avoids waiting for a second order, but serving two together can save travel time when demand is high. If the vendor can change its price, it also changes the rate at which customers join the system. The preferred dispatch rule therefore depends on an economic decision as well as a queueing calculation. Chen and Hu study this interaction for a single courier in a disk-shaped market and compare the vendor's revenue under dedicated and two-order batch delivery in their paper. The present mission concerns their crowded-market results, Propositions 3 and 4, in the authors' SSRN version of 2022-09-21.
The paper first analyzes fixed demand rates, then lets the vendor choose a demand rate by setting a price. The latter decision changes the comparison: customers with a high cost of waiting favor a less crowded, dedicated service, while sufficiently patient customers can make batching more profitable. The service radius has an analogous effect. The paper's threshold is expressed through the product of wait cost and radius, so these two comparative statics describe the same switch Chen and Hu, §5 and Online Appendix A.
A vendor is located at the center of a disk of radius . Customers arrive at locations uniformly distributed over that disk. The vendor has one courier and chooses between dedicated delivery, one order per round trip, and batch delivery, two orders per trip. The effective demand rate is . A customer incurs wait cost at rate and has a valuation in . The vendor's price induces its chosen demand rate. Chen and Hu give the dedicated service rate and batch service rate in equations (4) and (9).
The paper uses the following expected waiting times, with variation coefficients and :
Dedicated delivery is evaluated for ; batch delivery for . The first batch term is the wait to form a pair. The final term represents travel while the other order is delivered. The batch in-line wait is the paper's Kingman-based approximation for an queue, whereas the dedicated in-line wait uses its expression equations (5), (11), and (12).
In a finite market, the valuation distribution affects the price needed to induce demand. As the potential arrival rate grows, the paper's crowded-market revenue becomes
For each dispatch rule, insert its wait into this function and optimize over its stable demand range. The resulting optimal revenues are denoted and . The mission uses suprema to express these values. The paper motivates this limiting objective in (14)–(15) and Lemma 1 (16)–(17).
The goal is a single such that, for every ,
Thus the wait-cost threshold at a fixed radius is , and the radius threshold at a fixed wait cost is . At the threshold the two optimized revenues agree. For the paper's numerical , it reports Online Appendix (A.7)–(A.8).
As either or increases through its threshold, the optimal demand rate has a downward jump and the corresponding optimal price has an upward jump. The formal statements require both one-sided limits to exist and the inequalities between them to be strict. They cover every selection of optimal demands, including any ambiguity at the tie. These are parts (ii) of Propositions 3 and 4.
The milestones cover strict concavity of the revenue objectives, their explicit optimizers and values where attained, the single crossing of the revenue gap, the demand comparison at the tie, and the two propositions individually. The goal combines those propositions through the common product .
The threshold tells the vendor which dispatch rule maximizes limiting revenue after the price has been adjusted optimally. It also locates a discontinuous operational change: a small movement in customer impatience or service area across the threshold changes the chosen mode, demand rate, and price. Comparing the waiting-time formulas at one fixed demand would not provide this revenue decision, because each mode can choose a different demand rate Chen and Hu, §5.
Chen and Hu prove the paper result analytically, while the threshold and its supporting claims here are proposed Lean statements awaiting proofs. A completed formalization would connect exact claims about the rational waiting-time expressions, optimization over open stability ranges, the unique revenue crossing, and one-sided limits. It would also record which conclusions use the paper's approximated batch wait and numerically estimated coefficient. These are reusable patterns for queue-based pricing models, even though this mission formalizes this paper's particular geometry and service rules.
The two dispatch modes have different singular boundaries and different optimizers. The batch wait diverges as demand tends to zero, yet batch revenue can have a finite boundary supremum that is not attained for some parameter values. The dedicated objective has a different service-rate pole. Consequently, replacing either optimization with an unrestricted real supremum, or asserting that every batch supremum has a maximizer, changes the claim. The revenue comparison also needs one crossing for the full positive range of , including values beyond the range where the appendix's interior batch optimizer applies. Finally, a strict jump in demand does not by itself supply the existence of both one-sided limits; the formal statements ask for those limits explicitly Online Appendix A.
Lean uses real-valued and the paper's closed-form waits, service rates, and limiting revenue. The name lam denotes . The batch coefficient is a real parameter satisfying , an explicit interval around the paper's numerical rather than a claimed exact evaluation of its integral. Every threshold statement assumes ; the auxiliary optimum statements use the page's range when they assert an interior maximizer. The domains are and , with zero excluded for batch because its wait is singular. The optimal revenues are defined as suprema of the actual objective images. The threshold is existential and is never defined from the desired answer.
The formal development does not construct the Poisson arrival process, random trip lengths, queue, or approximation behind the waits. It takes the paper's equations (5) and (12) as definitions. The finite-density function is recorded for context, but Lemma 1's convergence from finite to limiting optimized revenue is outside this mission's milestone list; the goal is explicitly the crowded-market limit. The printed (A.6)–(A.8) contain a coefficient error in the batch value, so the formal batch value uses the corrected expression and defines the revenue gap directly from the suprema. The printed batch optimization interval includes zero, which the stated waiting-time formula does not support. Definitions for objectives, stable domains, optimal demand, and one-sided jumps are reusable within related pricing formalizations. Contributions that establish the stated optimizer, crossing, or limit claims without changing their domains are within scope Chen and Hu, equations (12), (15), (A.3)–(A.8).
Augmented Lagrangian methods are a standard tool for constrained optimization, and first-order primal-dual variants of them are used when the objective is large, nonsmooth or nonconvex and second-order information is too expensive. Zhu, Zhao and Zhang (arXiv:2007.12219v1, published in Mathematics of Operations Research, 2024) analyse such a method, NAPP-AL (Nonconvex Auxiliary Problem Principle with Augmented Lagrangian), for problems with a nonlinear equality constraint, a closed convex set constraint, and a nonsmooth nonconvex term. They prove a sublinear rate in general and a linear rate under a local error bound they call the value proximity error bound (VP-EB).
An error bound is only useful if it holds in recognisable situations. Section 6 of the paper answers the question "can VP-EB ever be satisfied in a natural setting?" with two sufficient conditions. This mission formalizes the first: the Kurdyka–Łojasiewicz (KL) property with exponent , the condition behind most linear-rate results for nonconvex first-order methods since Attouch and Bolte (Math. Program. 2009) and Bolte, Sabach and Teboulle (Math. Program. 2014).
The problem (P) is
with , , , a linear map , and smooth, lower semicontinuous and possibly nonsmooth, and closed and convex. Primal-dual points are , with . The augmented Lagrangian with penalty is
The stationarity set (p. 6) collects the vectors with , , , where , is the limiting subdifferential and the normal cone. is the least norm in , and when is empty.
NAPP-AL updates by minimizing over a linearization of the smooth parts plus plus a Bregman term built from a strongly convex kernel ; it updates by a linearized quadratic step and by the multiplier step . The step lies in with given by the paper's formula (8). Assumptions 1 and 2 (Lipschitz gradients, , coercivity on the feasible set, a lower bound on ) are the paper's standing hypotheses.
For and , let . has the KL property at with exponent if, for some ,
VP-EB holds at if, for some , every iterate with and satisfies .
For a run of NAPP-AL under Assumptions 1–2 and (8), and an accumulation point of :
The constants of VP-EB are existential, as in Definition 5.1.
There is such that, whenever ,
Proposition 6.1 turns the paper's Theorem 5.1 (linear convergence under VP-EB) into a statement about a property that is known to hold for wide classes of functions: semialgebraic and subanalytic functions satisfy KL inequalities, and exponent is established for many structured problems (for instance by Li and Pong, Found. Comput. Math. 2018). With it, a user who verifies the KL exponent of obtains a linear rate for NAPP-AL.
The result is proved in the paper; none of it is machine-checked. A formal proof requires the residual bound of Theorem 4.1(iv) for NAPP-AL, which the companion mission on the sublinear rate states as a milestone, and the conversion of a KL inequality on the strict level band into an error bound on the half band. A formal version also pins down a convention the paper leaves implicit: where the stationarity set is empty, the KL inequality is satisfied trivially because the distance is .
The deduction itself is short once Theorem 4.1(iv) is available; the difficulty is that Theorem 4.1(iv) is not. It asserts a uniform constant with , which needs the boundedness of the iterates (from the sufficient decrease of the potential and coercivity on the feasible set), a lower bound on the steps through (8), and the optimality conditions of the nonsmooth, nonconvex subproblem (5), including the sum rule under local Lipschitz continuity of . Applying the KL inequality directly, without a residual bound tied to the algorithm, gives nothing: the KL inequality controls by a distance to , and only the algorithm links that distance to the step.
The Lean development works in EuclideanSpace ℝ (Fin k). Primal-dual points live in with the Euclidean norm of the stacked vector written out explicitly (tnorm), not Mathlib's sup norm on the product. is a continuous linear map with its operator (spectral) norm; is the infimum of over unit vectors. is an infimum in , equal to on the empty set. The algorithm is a relation on given sequences: global minimality in (5) and (6) and the update (7); existence of minimizers is not asserted.
Readings disclosed relative to the page: are real valued with gradients Lipschitz on the whole space; is Lipschitz on an -neighbourhood of each point of ; ; the normal cone is empty off ; VP-EB is the inequality of Definition 5.1 without its presupposition that the sequence converges; the KL property for uses the paper's set of p. 6. Proposition 6.1 says only "generated by NAPP-AL"; the hypotheses of Theorem 4.1 (Assumptions 1–2 and the step rule (8)) are included because the proof uses Theorem 4.1(iv).
Trivializing encodings are ruled out: the distance is not Metric.infDist (which is on the empty set), the product norm is not the sup norm, is not a matrix with an entrywise norm, local Lipschitz continuity of is not Mathlib's relative notion, and the normal cone is not nonempty off .
A complete development needs Theorem 4.1(iv) for NAPP-AL and thus most of §§3–4 of the paper (Proposition 3.1, Lemmas 4.1–4.3). That infrastructure is shared with the other missions of this series and is reusable; contributions of any of those lemmas are welcome. The source is the preprint arXiv:2007.12219v1, not the published version; all numbering is the preprint's.
Sellers often ask customers what they want before designing a product or service. The answer can affect both the quality delivered and the price paid. Because a customer can send a costless, unverifiable message, the seller cannot assume that a stated preference is true. Guo's customization model asks when the customer's own incentives make truthful communication sustainable. This matters for products with substantial presale effort, such as prototypes, proposals, and sales assistance: the seller incurs that effort before the final transaction price is set. The paper distinguishes this selling cost from the cost of producing the eventual product. This mission concerns the paper's A-Learning game, in which the seller learns through a customer's message before choosing quality.
Each buyer wants one unit of a product with quality . A buyer with preference values it at and can decline to trade. The preference is private and has two possible values, . The high type has prior share . Producing quality costs and selling it costs , with . The selling cost is incurred at the design stage. In the final price-setting stage, the seller makes a take-it-or-leave-it offer with probability ; the buyer makes the offer with probability . These are the assumptions of §2, pp. 5–9.
Under A-Learning, the buyer sends one of two costless messages before the seller chooses quality. A separating message rule sends different messages for the high and low types. On receiving message , the seller believes the type is . If its belief is , the seller's expected payoff from offering quality is
At a given quality, a buyer whose actual type is receives
The maxima preserve the buyer's option not to purchase. In the paper's perfect Bayesian equilibrium, the seller's beliefs agree with the types that send the observed messages, the seller chooses a nonnegative quality maximizing for each message, and each type chooses a message maximizing its own payoff. With two distinct messages and a separating rule, both messages occur on the equilibrium path. These payoff and equilibrium conditions are stated in §3.2, pp. 11–12, equations (4)–(7).
The seller's printed optimal design for belief is
With , the two incentive compatibility conditions are and . The supporting targets identify the seller's optimal design, characterize informative equilibrium by these two conditions, and express each condition as a threshold on type heterogeneity. They follow §3.2, pp. 12–13.
The goal is Proposition 1: an informative A-Learning equilibrium exists exactly when
The weak inequality includes the boundary at which a buyer is indifferent between messages. The Appendix's proof uses strict inequalities in a corresponding line; the statement on p. 13 and Proposition 1 use weak ones. The milestone list retains the source's optimal-design sentence, equations (6)–(7), and the two threshold sentences in their order in the SSRN author copy.
The theorem gives a precise answer to whether costless buyer communication can transmit preference information before a seller customizes a product. The condition separates the two possible failures of truthful reporting: a high type may prefer the design induced by the low message, and a low type may prefer the design induced by the high message. It also shows why the relevant threshold depends on bargaining power and both cost coefficients, while the prior share does not enter this particular equilibrium-existence condition. The result is a theorem of the paper; the mission seeks its machine-checked formulation and proof.
The formal development makes the equilibrium claim more than a comparison of two algebraic payoffs. It must connect an actual separating message strategy, beliefs, a seller optimum, and buyer best responses to the two incentive conditions. The model's payoff definitions and equilibrium predicate are reusable for other statements about A-Learning in the paper, including comparisons of equilibrium quality and payoffs. The threshold lemmas can also be reused when comparing A-Learning with O-Learning.
Costless messages alone impose no truthful-reporting discipline. A seller's belief changes both the design chosen after a message and the price a buyer might face. The high and low types therefore face different deviation incentives. A comparison that ignores the seller's design decision misses the equilibrium requirement; a comparison that treats every buyer as purchasing misses the low type's option to refuse an overpriced high-quality product. The second issue is visible in the terms of equation (5). The equilibrium result has to hold at equality in the thresholds as well as above them.
The Lean model uses real parameters and a two-constructor type for buyer types. Its standing assumptions are exactly , , , , and . A separate two-constructor type represents the two possible messages. Quality is real and every seller optimization ranges over ; optimality means that the chosen design attains the maximum. Buyer deviations range over both messages. Beliefs identify the types on the equilibrium path. The type's purchase option is kept in both maximum terms of the buyer payoff.
The price-setting stage is represented by the paper's reduced-form payoffs (4) and (5), without a separate bargaining game. The prior share is retained among the standing primitives even though it cancels from Proposition 1. The closed-form design is used in and the incentive conditions, while an equilibrium requires actual seller maximization. An equilibrium is not defined as the conjunction of incentive conditions, and is the printed maximum of the two explicit fractions. Separation rules out a one-message or pooling interpretation. The supporting statements require real arithmetic, optimization on a nonnegative domain, and finite case analysis for the two types and two messages. Contributions that preserve these definitions and the paper's weak boundary are welcome. The known proofs behind the milestones are in the Appendix of the SSRN version, pp. 27–28.
Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in , compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.
This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.
Let denote the real output of a quantum algorithm under one run, and let be its probability law. The mean is , and the variance is . The result assumes a known with . Although the paper describes a circuit that prepares and measures , its accuracy statements depend on the distribution of ; the Lean interface therefore represents a run as a measurable real random variable on a probability space.
For real thresholds , the truncation returns when and zero otherwise. The variants and retain the output below and at or above , respectively. They do not clip a value to a threshold. The size is . These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.
Algorithm 2 estimates a nonnegative mean using the base interval and the half-open bands for . It sets and , then adds the base estimate to times each band estimate. A successful Algorithm 1 call means that its estimate of a -valued output differs from by at most , the accuracy bound of Theorem 3, pp. 8–9.
Algorithm 3 rescales by , draws one sample from , and centers the rescaled output at . It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy and recombines their estimates. The two calls are specified to fail with probability at most each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.
When every Algorithm 1 call satisfies its accuracy bound and , the output of Algorithm 2 obeys
The constant is chosen once for a fixed positive universal constant from Theorem 3. It is independent of and .
For , , and , Algorithm 3 returns with
This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.
Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.
The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.
A bound for one -valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.
Lean uses probability measures and measurable real outputs for the laws of and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of , so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's and formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.
The hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression occurs only on bands indexed by .
The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.
Best subset selection fits a linear model by least squares using at most of available predictors. It is the classical -constrained estimator of sparse regression. Mixed-integer optimization now computes it for problems with thousands of variables (Bertsimas, King & Mazumder 2016), so its statistical behaviour matters in practice. Simulations in Hastie, Tibshirani & Tibshirani 2020 found that it predicts worse than shrinkage methods such as the Lasso when the signal-to-noise ratio (SNR) is low.
Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add an or shrinkage penalty to best subsets. They prove upper bounds of two kinds: slow rates, linear in the tuning parameter , and fast rates, quadratic in . Theorems 2 and 3 of the paper give them for the shrunken estimators. For best subsets, the paper only has a fast-rate bound, of order . When is small, the shrunken estimators' slow rate beats that bound. Theorem 4, the goal of this mission, shows that the comparison is meaningful: in that regime best subsets really does incur an error of the order of its upper bound.
The data follow the linear model
where the design is a deterministic real matrix whose columns have unit Euclidean norm. The noise has independent entries, with . Write for the Euclidean norm, , and . The ball is . The minimal -sparse eigenvalue of is
A best-subsets solution of size is any minimizer
A constant is universal if it does not depend on . The symbols and mean and up to positive universal factors. Logarithms are natural, and .
There are universal constants such that the following holds. Suppose , and . Then, with probability at least , every best-subsets solution satisfies
The constants are left unfixed, as in the paper. The statement asserts the order of the error, which is what the comparison with the upper bounds needs.
Theorem 4 matches the fast-rate upper bound for best subsets from Corollary 1 of the paper. When is bounded below, the prediction error of best subsets is of exact order in the low-SNR regime (Remark 10). This is the theoretical counterpart of the empirical observation that best subsets overfits at low SNR. It is also what makes the paper's case for shrinkage a theorem rather than a comparison of upper bounds. The paper's Proposition 4 applies it to a concrete correlated design, where it gives a ratio of prediction errors between best subsets and its -shrunken version that grows with .
The result is proved in the paper; this mission formalizes it. No formalization of this result exists on the platform. The mission also produces a reusable Gaussian lower bound on sparse correlations (Lemma 1) and a deterministic reduction of the best-subsets objective, (39)–(40), which are of independent use for estimators.
An upper bound on best subsets follows from comparing with in a basic inequality. A lower bound must hold for every minimizer, and itself gives no lower bound. The first idea is to compare with the noiseless fit. It fails because the noise can be fitted by sparse directions, which is exactly the effect to be quantified. The difficult step is Lemma 1. It requires a large set of sparse directions that remain separated after multiplication by , a lower bound on the expected maximum of a Gaussian process over that set, and concentration of that maximum around its mean, with all constants universal. A second subtlety is that the statement is about every minimizer of a nonconvex problem, so the proof has to bound the objective rather than the estimator.
Vectors are Fin n → ℝ and Fin p → ℝ, with indices starting at 0. The design is X : Matrix (Fin n) (Fin p) ℝ. The Euclidean norm, norm, support and are explicit definitions, since Mathlib's norm on Fin m → ℝ is the sup norm. is an infimum over the nonzero vectors with ; this set is nonempty when , and every ratio is . The noise law is the product of centred Gaussians of variance on . "With probability at least " means that a measurable set of noise vectors of probability at least exists on which the conclusion holds. Best subsets is an argmin predicate: Theorem 4 quantifies over every minimizer, and existence is neither assumed nor needed. Universal constants are quantified before every other parameter. "" is a comparison of real numbers.
The model consists of , (with ), and its Gaussian law, the estimator (1), and the minimal sparse eigenvalue .
Two hypotheses are pinned relative to the printed theorem:
The milestones carry neither pin. Because the constants are existential, a formalization in which , or may depend on , or would be trivial, and is ruled out by quantifying them first. A version asserting the bound for some minimizer would be weaker than the theorem.
Not formalized here: the upper bounds (Theorems 2, 3, 5), the noise events of Theorem 1, Corollaries 1–6, Propositions 3–4, and the numerical experiments. The proof of the goal also uses Theorem 1's event , which belongs to a separate mission of this series. Proved platform results that a proof of Lemma 1 can use include Sudakov minoration for separated Gaussian families (HighDimProb.RandomProcesses.sudakov_minoration_finite_separated), Gaussian Lipschitz concentration (HighDimStat.TailBounds.lipschitz_gaussian_concentration) and a lower bound on Gaussian maxima (HighDimProb.RandomProcesses.standard_gaussian_max_lower_bound). Contributions are welcome on any milestone, and on supporting lemmas: a packing of sparse sign vectors (Gilbert–Varshamov type), and the approximation of -bounded vectors by sparse ones.
Simulating the time evolution of a quantum system is a standard task in quantum algorithms: given a Hamiltonian, the algorithm must reproduce the phase acquired by each of its energy eigenstates. The cost is often measured by how many times the algorithm queries an operator describing that system. Low and Chuang's 2016 preprint connects this task to quantum signal processing, a method that programs a sequence of rotations of one ancillary qubit. Its Theorem 2 gives the quantitative link: a finite Fourier approximation of a desired phase function determines a phase sequence whose induced eigenvalue transformation has error at most and success probability at least .
The paper uses this link in a later Hamiltonian-simulation result with an optimal asymptotic query count (Theorem 3, p. 4). The present mission targets the finite, explicitly quantified signal-processing theorem that makes that application possible. The criterion for which response functions can be produced by the rotation sequence was established in earlier work by Low, Yoder and Chuang and is quoted as Theorem 1 in this paper.
An ancilla qubit has basis states and . Let be its Pauli matrices. For real angles and , a signal rotation is
The signal fixes the rotation angle; chooses its axis in the qubit's plane. A list of phases gives the response sequence , with acting first. Its four real Pauli coefficients are defined by
The ancilla state selects the scalar response . The realizability theorem characterizes these pairs when is positive and even: is a cosine series with frequencies through , is a sine series with frequencies through , , and for every (Theorem 1, p. 3).
For a finite-dimensional unitary , choose an orthonormal eigenbasis and real eigenphases , so . The signal operator applies to the ancilla in each eigenspace: . The ordered product therefore uses one common phase list on all eigenspaces. After preparing and projecting the ancilla on , the effective system operator is its block . The desired operator for a real phase function is (Eqs. (2)–(6), pp. 2–3).
Let be -periodic, valued in , and odd on the interior , and let be respectively a cosine and a sine series of degree at most for positive even . If at every real angle, the goal is one phase list for which, uniformly over angles and input unitaries,
The milestones state the exact realizability criterion, the paper's displayed scalar bounds, and the eigenspace identity that carries those bounds to the operator statement. The constants and are fixed because the mission formalizes Theorem 2 and Eqs. (7)–(11), pp. 3–4, rather than an unspecified approximation rate.
The theorem makes a Fourier approximation into a phase transformation of every eigenstate of an arbitrary finite-dimensional input unitary. Its quantified success guarantee means that projecting the ancilla succeeds with probability close to one when the approximation error is small. In the paper, the particular target connects this mechanism to sparse Hamiltonian simulation (Eq. (14), p. 4).
The result is proved in the cited paper; this mission asks for machine-checked proofs of its statements in the specified matrix model. The quoted characterization of achievable responses is also a proof target. A complete development would add reusable facts about products of qubit rotations, constrained trigonometric series, sum-of-squares completion, and block-diagonal operators. No machine-checked proof of this exact theorem was found in the local Prove2Me index at drafting time.
An arbitrary Fourier approximation is not automatically the response of a unitary rotation sequence. It may violate the squared-magnitude bound or the required value at zero, even though it is uniformly close to the target function. Those restrictions are exactly what the realizability theorem requires. The difficult part is the converse direction of that characterization: the paper quotes it from earlier work, while the present statement asks for all admissible pairs and all positive even sequence lengths. The completion of a nonnegative trigonometric polynomial into the remaining Pauli components is another substantial mathematical target; the needed factorization is not already packaged as the paper uses it in this Mathlib environment.
The qubit is a complex matrix indexed by . Rotations use the matrix exponential and the factor exactly as printed. The signal product has exactly factors in the paper's order. Cosine and sine series use the inclusive frequencies stated in Theorem 1. The operator model takes a finite unitary eigenbasis as data, with the ancilla as the first factor of the tensor product. The success inequality is pointwise in ; the error inequality is homogeneous in every system vector and represents the paper's maximum over unit vectors. The phases are chosen before the input unitary, so they cannot depend on its eigenspaces.
The paper writes ; the Lean target extends its domain periodically to and retains that codomain range. Oddness is imposed on the interval's interior, where both and belong to the printed domain. The phrase “real Fourier series in ” is represented by the cosine form for and sine form for that its proof applies directly. “Efficiently compute” is represented by existence of phases; no runtime claim is made. The source calls the operator-vector error a trace distance; the formalization uses precisely its displayed vector norm, rather than a distance between density matrices.
Some intermediate squared inequalities need or ; those conditions appear only on the corresponding milestone clauses. The goal has no separate bound on : its approximation hypothesis already forces . A valid formalization must use the concrete matrix product and matrix-entry Pauli components; defining response functions merely to satisfy the target would empty the theorem of its claim. Contributions that establish the realizability criterion, trigonometric completion, the explicit inequalities, and the operator lift are all in scope. The controlled- circuit of Fig. 1 and the asymptotic oracle-complexity claim of Theorem 3 are outside this mission.
Advertising platforms repeatedly sell opportunities to show an advertisement. The opportunity's features, such as audience and placement, affect each advertiser differently, while advertisers limit their average spending. This makes the efficiency of an auction a question about both heterogeneous values and budgets. The paper by Balseiro, Kroer, and Kumar studies this setting with a continuum of buyer types and context-dependent values. It constructs equilibria by value pacing, in which a buyer scales values before bidding. This mission asks how much attainable value those equilibria preserve when budgets cap useful value.
Earlier efficiency bounds for second-price auctions concern a different, non-Bayesian multi-item model. In particular, the half guarantee discussed by Azar and coauthors, as discussed in §5 of the paper uses a no-overbudgeting condition that the present pacing equilibria need not satisfy. Balseiro, Kroer, and Kumar prove their bound under their own contextual and in-expectation budget model; the distinction matters when interpreting the constant. Their existence and revenue-equivalence results also make it possible to speak about the same pacing-based allocation across standard auction payment rules. These claims and the limitation of the earlier assumption are explained in §5 of the paper.
An item has a context , with . There are buyers. Each buyer has a private type : the vector assigns a positive weight to every context feature, and is the buyer's budget, where . The buyer's value for the item is . A context is drawn from a distribution and buyers' types are drawn independently from a distribution ; both distributions have densities. The context and type ranges are the spaces and of §2. The reserve price is zero throughout the efficiency section.
A pacing function scales type 's value to . Let be the probability that the maximum paced value among independent competitors is at most . The first-price bid applies the paper's bid function to the paced value. A buyer may choose a context-dependent bid, subject to an in-expectation budget: expected payment over contexts and competitors must not exceed . The buyer's dual function is the supremum of its Lagrangian over such bids at multiplier .
The relevant pacing equilibria are fixed points of the correspondence . Its domain consists of measurable, integrable pacing functions in with total variation at most , where is the supremum of possible values. For a given , minimizes the average dual objective over . These are the objects of §3.3, including its multivariate definition of total variation.
An allocation assigns nonnegative shares summing to one. For buyer , keep fixed while averaging over the context and the other types. The buyer's liquid welfare is the smaller of this interim value and ; total liquid welfare sums its expectation over each buyer's own type. For an equilibrium pacing function , allocates to a highest paced bidder. Definitions 5 and 6 use this allocation to define the worst equilibrium liquid welfare relative to the optimal allocation.
The main target is the Theorem 3 guarantee, stated for every measurable allocation and every equilibrium pacing function :
The universal comparison expresses the paper's price-of-anarchy bound . It leaves no optimum or worst equilibrium as an arbitrary variable. The two milestones are the dual derivative identity and the first-order budget and complementary-slackness conditions stated in §3.2:
Here and minimizes over nonnegative multipliers. The milestones are posed in the zero-reserve setting used by the main target.
The theorem gives an explicit welfare guarantee despite private budgets, correlated values across buyers through a shared context, and equilibrium bidding that depends on those budgets. It applies to the allocation induced by pacing in every standard auction covered by the paper, since those auctions have the same equilibrium allocation even when payment rules differ Balseiro, Kroer, and Kumar, §4–5. Without an efficiency bound, existence of a pacing equilibrium alone would give no quantitative assurance about the allocation it produces.
The result has a mathematical proof in the paper's online appendix; it is an open formalization target here. A complete development would connect measurable Bayesian auctions, the buyer's nonconvex dual problem, the bounded-variation fixed-point domain, and interim liquid welfare. The definitions of interim welfare, dual expenditure, and multivariate variation can support other budgeted auction results. The source PDF held for this mission contains the published main article but not its online appendix, where the proofs and auxiliary lemmas appear.
The expected budget applies to each buyer type after averaging over contexts and opponents, while liquid welfare caps that same type's interim value before averaging over types. Moving the budget cap across the expectation changes the quantity. The natural first-price tie convention also awards the good to every highest bidder for the buyer optimization problem, while a welfare allocation must give total share one. The proof must reconcile the dual account of expenditure with a feasible allocation and preserve these different orders of expectation. The dual objective is a supremum over bids, so its derivative cannot be obtained merely by differentiating a chosen closed formula without justifying that formula and the maximizing bid.
Lean represents a context by Fin d → ℝ and a buyer type by its weight vector and real budget. Value is the explicit finite sum . The model requires a nonempty bounded measurable context set in the positive orthant, absolutely continuous probability laws and supported on their stated domains, measurable reserves and pacing, , and . Boundedness of makes finite; these conditions make the domain and integrals implicit in the article well posed. The welfare target assumes zero reserves as §5 does.
Admissible bids are measurable and nonnegative on , with integrable expected payment. The dual is defined by its supremum over bids. Total variation is extended-real-valued and uses Euclidean lengths of test fields; thus infinite variation cannot satisfy the bound through a real supremum's default value. Allocations are measurable and simplex-valued on the model domain. At a tied highest bid, splits the item equally; ties have probability zero under these equilibria, as the paper states by its appendix Lemma 6(d). The closed simplex permits zero shares, correcting the paper's notation in Definition 5, which §2.1 otherwise calls strictly positive. The universal welfare inequality avoids default real infimum and supremum values on pathological sets. Contributions to the measurable bidding, variation, duality, and welfare infrastructure are all useful within this scope.
Online advertising platforms sell billions of ad impressions a day, mostly by auction, to advertisers who care about the features of the impression (the user, the page, the time) and who spend under a budget fixed in advance. To keep spending within budget, platforms and advertisers use pacing: every value is multiplied by a factor smaller than one, so that the buyer bids less aggressively and spreads its budget over the whole campaign. Balseiro, Kroer and Kumar (2023) study the equilibria that pacing produces when items carry feature vectors and buyers' values are linear in them. They prove that a pacing-based equilibrium exists in the first price auction (Theorem 1), that the same pacing is an equilibrium of every standard auction with the same expected payments (Theorem 2), and that its liquid welfare is at least half the optimum (Theorem 3).
This mission concerns §6, Structural Properties, of that paper: what the equilibrium pacing multipliers look like as a function of the buyer's type. Its goal, Proposition 3, says that buyers who share a budget and whose weight vectors point in the same direction are paced down to one common weight vector. It is the qualitative statement behind a practical observation: scaling up the targeting weights of a budget-constrained advertiser without raising its budget does not change the outcome.
An item has a context , drawn from a law with a density. There are buyers; each has a type consisting of a weight vector and a budget , drawn independently from a law with a density on
The value of type for item is , and . The item is sold by first price auction with reserve price , and every buyer must respect its budget in expectation over the context and the other buyers' types.
A pacing function shades the value of type to the paced value , equivalently replaces by the paced weight vector . Let be the distribution function of the highest of independent paced values. The value pacing–based strategy bids , where
with when and below the reserve. A buyer of type facing competitors who bid has the dual function
the supremum over bid functions ; is the Lagrange multiplier of its budget constraint.
§6 assumptions. Reserve prices are zero; the support of is convex and compact; and takes values in with
the minimizer being unique. This is uniqueness of the best response, not of the equilibrium. A type with is unpaced, and paced otherwise. Norms are Euclidean.
Let be a unit vector and such that for some .
Proposition 3 describes equilibrium pacing along each direction of weight space as a single threshold. Along a ray with budget , buyers below a critical scale do not exhaust their budget and are unpaced; every buyer above it is paced down to the critical type, which spends its budget exactly. Equilibrium paced values, hence allocations and payments, are therefore constant above the threshold. By the paper's revenue equivalence result the same description holds for the pacing equilibria of all standard auctions, which makes it a statement about budget-constrained advertisers in general, not about one auction format.
The result is proved in the paper, with all proofs in its online appendix; the appendix is not part of the source this mission cites. No part of it has been machine-checked. The mission formalizes the statement on top of a from-scratch model of contextual budget-constrained first price auctions (types, pacing, the bidding function , the buyer's dual function), which is shared with the other missions of this series.
The dual function is a supremum over bid functions in which the competitors' bids themselves depend on , so the equilibrium condition is a fixed point: appears both inside the objective and as its minimizer. Comparing two buyers on the same ray requires relating their dual problems, and a buyer with weight vector does not simply face a rescaled problem, because the budget does not scale with . Part 2 requires in addition that the largest unpaced buyer exists, which needs continuity of on the support; continuity of an argmin requires uniqueness of the minimizer and continuity of in the type and the multiplier jointly. The monotonicity statement is a comparative-statics argument for a family of minimization problems parameterized by the type.
Types are pairs (w, B) : (Fin d → ℝ) × ℝ, values are the explicit sums , and the Euclidean norm is written as , never Lean's sup norm on Fin d → ℝ. is Mathlib's Measure.support. The expectation is over the product of and copies of ; ties win, as in the paper's tie-breaking rule. Bids are measurable, nonnegative and have an integrable payment, and is defined as the supremum over such bids (p. 7), not by its closed form. is defined by an explicit case split so that the case gives .
Standing assumptions: ; ; measurable inside the strictly positive orthant; and probability measures with densities, , ; measurable; and the §6 assumptions above, with the unique best response stated as membership, minimality and uniqueness over . Disclosed additions: ; ; nonempty and bounded (so that is finite); , since is defined on and is evaluated on . The maximization set of part 2 is read inside with the budget fixed, and the existence of the maximizer is part of the conclusion, so the statement is not vacuously true when no maximizer exists. The milestones are posed on , where uniqueness is assumed.
The development needs the support of a measure, argmin continuity (a maximum theorem for a unique minimizer), and comparative statics of parametric minimization; the auction model is reusable by the other missions of the series. Contributions of supporting lemmas on (its convexity in , continuity, the closed form of p. 8) are welcome.
The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.
For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold , and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.
Let with even. A bisection is a partition with ; its cost in a graph is the number of edges between and . Given a fixed planted bisection , an optimization problem recovers it if its unique optimal solution corresponds to .
The cut vector of has exactly when lie on different sides. With for edges and otherwise, the metric relaxation is
the first family over distinct and the second over , with . Every bisection's cut vector is feasible.
The distance is the length of a shortest – path ( across components). The diameter is and the average distance is .
The Erdős–Rényi model draws each edge independently with probability . The SBM chooses a bisection uniformly at random, then draws each pair inside a side with probability and each pair across with probability , independently, where . The logarithmic-degree regime (21) is
An event holds with high probability if as .
with high probability.
Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).
The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all , including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant ) the LP does succeed when ; Theorem 8 shows that at logarithmic degree no such window exists.
Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.
The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.
Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side with . The LP variable is a symmetric, zero-diagonal array , which is a point of ; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in and the average distance in , so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into , which matters only for the finitely many with . "With high probability" is a limit of probabilities equal to ; for the SBM the limit runs along . Logarithms are natural.
Disclosed choices relative to the printed statements: Theorem 8 prints only , and is added as the SBM's standing assumption (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary is left out.
The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every , the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.
A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.
In auctions with interdependent values, the value an agent assigns to an outcome depends not only on her own private information but on the information of the others: a bidder for drilling rights values a tract according to every bidder's geological survey, and a buyer of a used asset values it according to every inspector's report. Each agent observes only her own signal, while the mechanism designer knows how values depend on the full signal profile. Maximizing welfare truthfully is then much harder than with private values: the VCG mechanism no longer applies, and without structural assumptions on the valuations no ex-post truthful mechanism gives a good approximation of the optimal welfare (the source's Examples 1.2–1.3).
Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384) identify submodularity over signals (SOS) as a condition under which constant or near-constant approximations become possible, including for combinatorial auctions, where agents value bundles of items. For single-dimensional signals that take values, they give a -approximation under SOS (Theorem 6.1) and, under the stronger condition strong-SOS, a -approximation (Theorem 6.5). This mission formalizes the second result.
Timeline. Milgrom and Weber (1982) introduced the interdependent value model for auctions; Dasgupta and Maskin (2000) studied efficient auctions under the single-crossing condition. The computer science literature then gave approximation results for simple single-parameter settings (mostly single-item auctions or matroid constraints), again largely under single crossing or its variants, e.g. Roughgarden and Talgam-Cohen (2016) and Eden, Feldman, Fiat and Goldner (2018), as surveyed in the source. The SOS paper (arXiv v2, 2019; journal version in Mathematics of Operations Research, 2024) drops single crossing and gives, in its own words, the first welfare approximation guarantees for multi-dimensional combinatorial auctions with interdependent values.
There are agents and items. Agent holds a signal , and is the signal profile. For every bundle , agent 's value is , with ; for nonempty it is weakly increasing in every signal and strictly increasing in .
A function of the profile is strong-SOS if for every coordinate , every and profiles coordinate-wise,
Raising one signal helps less the higher the profile, including the raised coordinate itself; in particular the effect of an agent's own signal is concave. SOS asks this only when the raised coordinate starts from the same value in both profiles.
An allocation gives pairwise disjoint bundles. A deterministic mechanism maps reported signals to an allocation and payments; it is ex-post IC if, whatever the true signals and with the others truthful, no agent gains by misreporting, and ex-post IR if truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.
Let . Random Bucket picks uniformly, calls the high agents, and allocates to them a bundle assignment maximizing , the values with every high signal lowered to ; agent receiving pays . Random Sampling splits the agents uniformly at random into and , allocates to a bundle assignment maximizing , and charges nothing. k-SS runs Random Bucket with probability and Random Sampling otherwise.
For strong-SOS valuations, k-SS is universally ex-post IC-IR and, for every grid profile and every feasible allocation ,
The theorem shows that the price of truthfulness in combinatorial auctions with interdependent values grows only logarithmically in the number of signal values once values are concave in the agents' own signals, compared with the linear of the SOS mechanism. It also exhibits a decomposition of optimal welfare into a part driven by the other agents' signals (OTHER) and a part driven by the agent's own signal (SELF), each covered by a different randomized mechanism; this template recurs in later work on interdependent values.
The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact model behind a proof that is stated in a few lines and checks it against the paper's own appendix: the printed display (9) omits a factor 2 (it fails for one agent with , , ), and the mission states the corrected inequality, which is the case of the paper's display (12) and is what the ratio requires.
The obvious route compares the mechanism's allocation with the optimal one agent by agent, but the mechanisms allocate by proxy values computed from modified signal profiles, and the optimal allocation's value at the true profile is not directly comparable with any single proxy. Covering SELF requires bounding an agent's own-signal contribution within a bucket by its value at the bucket floor, which needs concavity in the own signal and is false under SOS alone. Covering OTHER requires the Key Lemma 3.1 on random zeroing of signals. Incentive compatibility needs the argmax to be read off the proxy profile alone; an argmax with tie-breaking on the full report fails it.
Signals are natural numbers and every hypothesis (nonnegativity, monotonicity, SOS, strong-SOS, the selectors' optimality) is quantified over the grid only. with is a disclosed reading: the buckets cover only for powers of two. The empty bundle is worth , and the monotonicity clauses apply to nonempty bundles. The argmax of each mechanism is an arbitrary selector that sees only the bucket index (or ) and the proxy profile and returns a feasible maximizer; theorems quantify over all such selectors. Random Sampling zeroes all of , the agent's own signal included (the paper's "" is read as ). Expectations are finite uniform averages; at Lean's makes the Random Bucket term vanish, matching .
The approximation is stated for every feasible allocation and with true values at the truthful profile, not with proxy values or a supremum; IC and IR are stated for each deterministic component, not for the mixture's expectation. Replacing the average over partitions by an existential, or the explicit payments by existence of payments, would not be this theorem.
The model layer (signal grid, combinatorial valuations, SOS, ex-post IC-IR, OTHER and SELF, Random Sampling) is shared with the companion missions and lives in InterdepSOS.KHL and InterdepSOS.RSV; strong-SOS, Random Bucket and k-SS are defined in InterdepSOS.KSS. Lemma 6.3 and the decomposition (7), which the proof uses, are posed in the companion mission on k-HL. Proofs of the milestones, and reusable lemmas on concavity in the own signal and on random zeroing, are welcome. The source is the arXiv v2 preprint; the journal version in Mathematics of Operations Research (2024) is not what the mission cites.
The minimum bisection problem asks, for a graph on an even number of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.
Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.
Let be a simple graph on , and write for an edge with ; set if and otherwise. A bisection is a partition of into two sets with . One fixed bisection, unknown to the solver, is the planted bisection; is the set of edges with one end in and the other in .
The cut vector of the planted bisection has exactly when and lie on different sides. The metric relaxation is the linear program, with ,
where (1) ranges over distinct with and (2) over . The LP recovers the planted bisection if is its unique optimal solution. The objective at is .
The graph distance is the length of a shortest – path ( across components). The diameter and the average distance are
The average is over all ordered pairs, the diagonal included. For define
For a connected graph on nodes with a planted bisection,
The proof of Theorem 5 works with the point ,
The mission poses three statements about it, for a connected on nodes:
The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, is small and (18) asks only that exceed roughly . In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.
Theorem 5 is not deep, but it is exact. The milestones fix the witness ; the work is in checking it. The obvious candidate, the graph metric itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by , which depends on and on the factor , is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization (ordered pairs, diagonal included), the factor , and the sign of , and must use wherever it divides by . In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.
Fin n (0-based). The planted bisection is a finset with , and . is the number of pairs adjacent in and on different sides.LPRecovers G V1 says that the cut vector of is optimal and every optimal point equals it.SimpleGraph.edist (in ), is SimpleGraph.ediam, and is the printed formula computed in . and use their real values. All statements assume connected, where these values are finite and .Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound .
Large-scale computing systems route incoming tasks to servers through dispatchers, one per task type. A task can only run on a server that holds the data or software it needs, so the set of admissible pairs forms a bipartite compatibility graph between task types and servers. Full flexibility (every server can serve every type) gives the best load balancing but requires each server to store everything. A central question is how sparse the compatibility graph can be while keeping the performance of the fully flexible system.
For the power-of- policy JSQ() (an arriving task samples compatible servers and joins the shortest of their queues), Rutten and Mukherjee (arXiv:2008.07562v2, Math. Oper. Res. 2023) identify two deterministic graph conditions, proportional sparsity and subcriticality, under which the occupancy process has the same mean-field limit and the same steady-state limit as in the fully flexible system (their Theorem 3.4). They then show that natural random designs satisfy both conditions almost surely. This mission covers the second random design: task types with inhomogeneous levels of flexibility, where each edge incident to task type is present independently with its own probability (Theorem 3.6 of the paper).
Earlier work on JSQ-type policies with constrained compatibility includes the stability analyses of Bramson (Ann. Appl. Probab. 2011) and of Cardinaels, Borst and van Leeuwaarden (Queueing Syst. 2019), to which subcriticality is equivalent for a fixed system (Remark 3 of the paper), and the mean-field analysis of the supermarket model on graphs by Budhiraja, Mukherjee and Wu (Ann. Appl. Probab. 2019), whose load condition is stronger than the condition (A.19) used here (Remark 11 of the paper).
For each there are a set of servers and a set of dispatchers. A compatibility graph is with , and the neighbourhood of is .
Proportional sparsity (Definition 3.1). For every ,
Every set of servers is seen by all but a vanishing fraction of dispatchers in roughly its global proportion.
Subcriticality (Definition 3.3). For each , and nonempty there is a probability distribution on such that, with ,
Some static routing of sampled sets loads no server asymptotically beyond its capacity.
The random graph. Given edge probabilities , the graph contains each pair independently with probability . Write and . Only the law of each is prescribed; the graphs for different may be coupled arbitrarily, and "almost surely" refers to any such coupling.
If, as ,
then almost surely is proportionally sparse and satisfies the subcriticality condition.
implies subcriticality. 3. Lemma B.2. If and , then satisfies the subcriticality condition almost surely.
The goal is the conjunction of Lemmas B.1 and B.2 under (3.5).
Combined with Theorem 3.4 of the paper, the goal says that JSQ() on a random compatibility graph with dispatcher-dependent flexibility behaves, in the large-system limit and in steady state, like JSQ() on the complete bipartite graph. Condition (3.5) allows the least flexible task type to be compatible with only about times a diverging factor of servers in expectation, far below , and allows strongly heterogeneous flexibility levels as long as the spread measured by is controlled. Remark 8 of the paper notes that for and equal probabilities, leaves a dispatcher isolated with probability tending to one, so the growth conditions are close to necessary.
The result is proved in the paper (Appendix B). As far as is known, none of it has been machine-checked. A formal proof requires a quantitative Chernoff bound for binomial tails, a bounded-differences (Azuma–Hoeffding) inequality for functions of independent Bernoulli variables, a union bound over all subsets of servers, and the first Borel–Cantelli lemma in a setting where only per- marginal laws are fixed.
Proportional sparsity quantifies over every subset of the servers. A concentration estimate for one fixed , or one fixed dispatcher, is not enough: whatever bound is used must survive a union over subsets, so a merely vanishing failure probability per dispatcher does not suffice.
Subcriticality is a maximum over all servers of a sum whose terms are not independent: depends on the edge itself, and a term is unbounded in the regime where is small. A direct concentration inequality for this sum therefore does not apply, and the logarithmic factors in (3.5) reflect the need to control all neighbourhood sizes and all servers at once.
Independence across is not available, so almost-sure statements cannot use the second Borel–Cantelli lemma or any law of large numbers along ; every bound must be summable in .
Fin N, dispatchers Fin (M N) with 0 < M N assumed, and a graph is a Finset (Fin N × Fin (M N)).A complete development needs binomial Chernoff bounds, a bounded-differences inequality and Borel–Cantelli for summable bounds; these are reusable for other random-graph statements. Proofs of the deterministic (A.19) reduction and of either lemma are welcome independently.
Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.
In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).
Let be a finite-dimensional real inner product space (the paper's ), and let be a embedded submanifold of dimension . The tangent space at is the linear span of the tangent cone of at . For a submanifold this is the set of velocities of curves in through , and it is a subspace of dimension . carries the metric induced by the inner product of , and denotes the orthogonal projection of onto .
A retraction is a map , . For every it sends all of into and is smooth on , with and differential the identity at . The Riemannian gradient of a differentiable is .
The objective is stochastic, , with noise distributed according to a probability measure . Two assumptions are imposed:
Given a smoothing parameter and a batch size , draw independent pairs , each with independent of , and put . The mini-batch zeroth-order Riemannian gradient is
ZO-RSGD (Algorithm 2) starts at and iterates with step and a fresh batch at every step. denotes a minimizer of over .
If , then for every
The constants are the paper's own. The goal states the rate for every , and . It does not state the parameter choices , , that follow from it.
Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an -stationary point in expectation after noisy function evaluations. The dependence is on the manifold dimension , not on the ambient dimension . This matches the Euclidean rate of Ghadimi and Lan with replaced by , and it is what makes projected-Gaussian estimators attractive when (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).
The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.
The Euclidean argument relies on a smoothed function whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: is not a translate, so is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.
The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step is projected onto , which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, .
stdGaussian E.ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a coordinate-slice submanifold), so is tied to and is never a free number. is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of and . So no statement can hold because a Bochner integral defaulted to .stdGaussian under an orthogonal projection.