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?
Financial reports help investors value a firm, but a firm can also learn and voluntarily disclose information outside the report. A regulator who makes mandatory reports more precise changes the firm's incentive to acquire that other information. Friedman, Hughes and Michaeli's 2020 preprint, Proposition 1, studies whether a reporting rule that is less precise about one component of value can induce enough additional disclosure about another component to improve investors' information overall. The question matters to accounting standard setters because the regulator's choice affects both the information in the required report and the firm's subsequent behavior. The paper gives a sufficient high-prior condition for conservative reporting to be preferred; this mission addresses the second sentence of Proposition 1 and the results in its proof.
The firm's value is . The reportable component is either zero or one, with prior probability of one. The independent privately discoverable component lies in , has law , mean , second moment , and cumulative distribution . Investors do not observe either component directly. The firm's payoff depends on whether their posterior mean of reaches a threshold . These objects and the sequence of decisions are specified in Section 2 of the preprint.
The regulator first chooses a reporting system with posterior probabilities that the reportable component is one after a good or bad report. Feasible pairs obey and . The perfect benchmark is . The candidate conservative system is , which gives a bad report even in some good states. Bayes' rule sets the probability of a good report from the two posteriors and the prior.
After observing the rule, the firm chooses an information-acquisition probability . If it learns , it discloses when exceeds a cutoff ; otherwise investors see no voluntary message and attribute the cutoff value to the hidden component. The cutoff is defined by the Bayes-consistency condition that its value equals the posterior mean under nondisclosure. The firm maximizes the probability of reaching the payoff threshold and, among ties, chooses the greatest , as stated on p. 10 of the preprint. The regulator anticipates this choice and minimizes , the expected posterior variance of after both reporting and disclosure.
Lemma 1 gives a unique, decreasing cutoff for :
Corollary 1 inverts it. Lemma 2 (iii) identifies the firm's greatest best response under the perfect system when : its cutoff is and its information probability is . These are the first three milestones (pp. 15–16).
The proof of Proposition 1 supplies two variance targets. Under , the firm gathers with and the expected posterior variance is . Under , let and . The expected posterior variance is
The goal uses the corrected sufficient threshold
For and , the candidate is feasible and strictly lowers relative to at their induced firm responses. Hence an optimal rule with must have . The goal is the second sentence of Proposition 1, with the threshold corrected using the expected-variance comparison in its proof on pp. 34–35. The first sentence, that every optimum has , is outside the scope of this mission.
The comparison establishes a concrete mechanism by which a less informative required report can yield more information in total: it raises the firm's chosen probability of acquiring and disclosing the unreportable component. A strict comparison with the perfect benchmark is stronger than an assertion about a particular optimum, since it certifies why the benchmark cannot be selected in the stated regime.
The result is proved informally in the cited paper, subject to the threshold correction explained below. This mission seeks Lean statements and eventually machine-checked proofs for the cutoff, induced firm responses and expected-variance comparison. No theorem in this mission currently has a machine-checked proof. The model definitions may also be reused for variations of mandatory reporting and voluntary disclosure.
The firm's objective depends on a cutoff that itself changes with the firm's information choice. The obvious approach of holding fixed while comparing report precision misses the behavioral response that drives the result. The p. 34 comparison has a second subtlety: equation (3) uses weights conditional on nondisclosure, whereas the regulator's averages over all messages. Comparing the candidate's unconditional variance directly with equation (3) changes the sufficient threshold. The general cutoff and best-response statements also need the distributional assumptions treated consistently; the appendix computations on p. 33 use a uniform distribution even though the main text states a general .
Lean represents by an atomless probability measure concentrated on with full support on every interior interval. This replaces the paper's differentiable density in the integrals and makes the cutoff strictly invertible. The binary component is summarized by its prior ; independence enters the derived second moment. The regulator chooses posterior pairs directly, as on p. 10. Strict separation of the pair excludes an uninformative system whose conditional posterior and Bayes weight are undefined. The firm chooses , with the greatest-maximizer tie-break; disclosure is for , equivalent almost surely to because has no atoms.
The cutoff relation is cross-multiplied, avoiding a zero-probability nondisclosure denominator at . Lemma 1 establishes the existence and uniqueness needed for the cutoff's sInf representation. Its printed open-range claim is adjusted at and , where the cutoffs are respectively and zero. The regulator's is defined from the law of total variance, using posterior means after disclosure and nondisclosure. The goal includes feasible , best-response existence for both candidate systems and a strict comparison, preventing a vacuous conclusion about regulator optima. These conventions and boundary cases are detailed in the source discussion and appendix.
The printed formula for is . It omits the nondisclosure probability in the comparison. For uniform , the printed condition is , while the corrected condition is . At and , the printed bound is met, but . The formal goal uses the corrected formula. Contributions that establish the cutoff and inverse relation, the two firm responses, or the two variance identities are welcome; measure integration and posterior-moment lemmas are reusable beyond this mission.
Mean field games describe Nash equilibria of games with very many symmetric players by a single limiting object. Whether, and how fast, the equilibria of the -player game converge to that limit is the convergence problem. For games with common noise, a source of randomness shared by all players, the standard route goes through the master equation, a PDE on the space of probability measures whose solution gives the equilibrium value of a representative player as a function of the population's distribution (Cardaliaguet, Delarue, Lasry and Lions, 2019, arXiv:1509.02505).
For finite state spaces the distribution is a point of the simplex. Bayraktar, Cecchin, Cohen and Delarue (J. Math. Pures Appl. 147, 2021) introduced a common noise of Wright–Fisher type, the noise of population genetics, which keeps the distribution in the simplex and makes the master equation uniquely solvable. Its -player counterpart is not obvious, because the Wright–Fisher diffusion is the limit of a resampling of the population, not of independent player noises. The paper behind this mission (Bayraktar, Cecchin, Cohen and Delarue, Mathematics of Operations Research, 2022, arXiv:2012.04845) builds such a game, in which players carry weights that are resampled at random times, and proves that its normalized equilibrium values converge to at a polynomial rate.
There are states and players. Player is at a state and carries a weight ; the weights are rational and sum to , and the set of such weight tuples is . The players interact through the weighted empirical measure
a point of the simplex .
Each player controls the rates at which it jumps between states, at quadratic cost. A drift pushes players towards nearly empty states, where is non-increasing and Lipschitz, equal to on and to beyond . At rate the common noise draws and replaces every weight by . Players pay per unit time and at time .
The equilibrium values divided by the weights, , solve the normalized Nash system: a countable family of ordinary differential equations in , indexed by , with the Hamiltonian and the terminal condition .
The limit object is on , solving the master equation
with . Here are the intrinsic derivatives on the simplex, , and the last term is the Kimura operator of Wright–Fisher diffusions. The mean-field prediction for player is .
For large enough, there are and such that for every , , , and ,
The exponent is existential, so an improvement of the rate does not invalidate the target.
Theorem 2.4 gives a convergence rate for a finite-state mean field game whose common noise keeps the population on the simplex. It shows that the master equation of the earlier paper is the right limit of a concrete finite game, and with a diffusion-approximation argument it yields the paper's second main result, the weak convergence of the equilibrium empirical measure to the Wright–Fisher-type SDE (Theorem 2.6). The bound is not uniform in : it degenerates near the boundary of the simplex and for spread-out weights, which reflects the singular coefficient in the resampling.
None of these results has a machine-checked proof. The mission produces a formal statement of the convergence problem for a game with weighted players, a formal Nash system on a countable state space, intrinsic derivatives on the simplex, and multinomial moment estimates.
The usual proof of convergence plugs into the Nash system, controls the rest, and closes with a Gronwall argument along the -player dynamics. Here the rest is small only on , away from the boundary of the simplex and for moderate weights; the second derivatives of may blow up at the boundary, and the resampling ratio is unbounded as . A uniform estimate of is therefore not available, and the comparison must be weighted by functions of whose expectations along the dynamics can be controlled. The weights are unbounded and enter through their moments.
States are Fin d and players Fin N, with and (no ). Weights are rational, and every equation and conclusion is required only for and . The simplex is Mathlib's stdSimplex. Intrinsic derivatives use lineDeriv; multinomial expectations are finite sums over Finset.Nat.antidiagonalTuple. The resampling ratio is when , as in the paper. Solutions of the Nash system and of the master equation are classical in , with one-sided derivatives at and . The Nash system is solved by any bounded classical solution; Proposition 3.1 says there is exactly one.
The formalization commits to the following readings of the source.
The bound is not trivial. Since and the right side is at least of order , a constant chosen after would make the theorem empty; precedes . The functions and enter only through the Nash system and the master equation, and the class of is not empty: for the function is in it.
The mission takes as given. Its existence for is Theorems 3.2 and 3.4 of Bayraktar, Cecchin, Cohen and Delarue (2021), quoted as Proposition 2.1, which is not a target. Also outside the mission are the -player game itself (Propositions 2.2–2.3), Theorem 2.6, and the process estimates of §4.1 (Theorem 4.1, Remark 4.2, Propositions 4.3–4.4), which need a continuous-time Markov chain with a martingale-problem characterization. Contributions are welcome on every milestone; the multinomial estimates and the simplex calculus are reusable elsewhere.
A game option (or Israeli option, introduced by Kifer, Game options, 2000) is an American option whose seller may also cancel the contract at any time, paying the exercise payoff plus a penalty. Pricing it is a Dynkin game: a zero-sum optimal stopping game in which the buyer chooses an exercise time to maximise the discounted payoff and the seller chooses a cancellation time to minimise it. Such contracts model, for instance, a public concession that the granting authority may revoke against compensation.
In the classical theory the drift of the underlying asset is known. De Angelis, Gensbittel and Villeneuve (arXiv:1705.07352v4, 2019; Mathematics of Operations Research, 2021) study the perpetual game call option when neither player knows whether the asset pays a dividend: the return is with an unobservable . Both players learn about only by watching the price. The paper's headline results are that the game has a value, that the value is globally , and that under explicit conditions on the parameters the game has a Nash equilibrium in pure strategies given by entry times into the two players' stopping regions. This mission formalizes the equilibrium result for the case .
Timeline. Kifer (2000) introduced game options. Ekström and Villeneuve (AAP 2006) proved existence of the value for one-dimensional diffusions without uniform integrability and analysed the perpetual call with . Ekström and Peskir (SICON 2008) proved existence of the value and of Nash equilibria for Markov processes under uniform integrability. Yam, Yung and Zhou (Game call options revisited, Mathematical Finance, 2012) treated the perpetual call with a known dividend (). De Angelis, Gensbittel and Villeneuve (2017–2019) treated the case with an unknown dividend, .
Fix a discount rate , a dividend jump , a volatility , a strike and a penalty , and set and . On a probability space carrying a Brownian motion and an independent random variable with , the asset is
The players observe only : their stopping times are stopping times of , the filtration generated by and augmented by the null sets, with values in . For such (buyer) and (seller) the expected payoff is
with payoff on . The upper value is and the lower value . A saddle point is a pair with for all .
The filter is the players' posterior belief that a dividend is paid; it has the closed form with the likelihood ratio of the observed path. The pair is Markov. With the value, the stopping regions are (buyer) and (seller), and the entry times are
Finally . In the coordinates one has , so the sign of decides whether this time-like variable increases or decreases.
Under Assumption 7.1, , and : for every and ,
The goal asserts the shape of the equilibrium (entry times into the model's own stopping regions), with no constant to be improved.
In attack order: the filter identity (§2, p. 5); the regularity of (Lemma 3.1); the value, the seller's optimality, and the super- and submartingale properties (Theorem 3.2); positivity of (Remarks 3.3); the location of the stopping regions (Proposition 4.1, Lemma 4.2 (i), (iii)); the boundaries (Corollary 4.5) and finiteness of (Lemma 4.6); the parabolic change of coordinates (5.1)–(5.4); connectedness of the regions in parabolic coordinates (Lemmas 5.2, 5.4); the boundary of (Corollary 5.5, (5.20)); and positivity of (Lemma 7.2).
The result. Existence of the value does not give an equilibrium: without uniform integrability the buyer's natural candidate may fail to be optimal, and in the complete-information case the pair is indeed not a saddle point (Proposition C.1). Proposition 7.3 shows that partial information about the dividend restores a pure-strategy equilibrium when , and identifies it: each player stops on entering their own stopping region, which is described by monotone free boundaries. This makes the option's hedging and cancellation policies explicit.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. The mission provides a Lean model of a continuous-time game with an unobservable parameter, built from Mathlib's Brownian motion, stopping times and martingales, and a decomposition of the proof into the paper's own lemmas. The theory the proofs use (optimal stopping games for Markov processes, Itô's formula, Girsanov's theorem) is largely absent from Mathlib.
The obvious argument fails at the buyer's side. The seller's optimality comes with the value (Theorem 3.2); for the buyer one needs for every , i.e. that the submartingale can be sampled at . The payoffs are not uniformly integrable (), so optional sampling cannot be applied directly and the term must be shown to vanish. That requires a pathwise bound on the price before , which in turn needs the geometry of in both coordinate systems, monotonicity of (), and strict positivity of the boundary (Lemma 7.2, which needs ). Theorem 3.2 itself rests on the Ekström–Peskir theory of Markovian Dynkin games applied to a degenerate two-dimensional diffusion.
filter_condexp ties to and records its observation measurability and continuous paths, while eq_5_3 ties the encoding to the paper's coordinates .Setting carries a measure , a Brownian motion with all paths continuous (a continuous modification), and uniform on independent of ; then realises every prior on one space, so is defined at every state.WithTop ℝ≥0, so infinite stopping times are allowed.lintegral) in , with payoff on ; , and as a real number (finite since ).hittingAfter … 0 into and , equal to if never reached.Call centres and hospital wards are run in the Halfin–Whitt regime: the number of servers exceeds the offered load by a margin of order , so that delays are short and servers are nearly always busy. With several customer classes, the operator must also choose a scheduling policy: which waiting class is served next. In the diffusion limit, every such policy becomes a control of an -dimensional piecewise-linear diffusion (Atar, Mandelbaum and Reiman 2004; Harrison and Zeevi 2004). Ergodic control of this diffusion, and the justification that its optimal policies are asymptotically optimal for the queues, both need the diffusion to be stable under every admissible policy, with bounds that do not depend on the policy.
A. Arapostathis, H. Hmedi and G. Pang (arXiv:1812.03528v3) prove that positive spare capacity alone gives this: the limiting diffusion is exponentially ergodic, at a rate and with constants that are uniform over all stationary Markov controls.
Timeline.
Fix classes, service rates , abandonment rates , and write , , , . Control values lie in the simplex ; is the fraction of the queue made up of class . The spare capacity is . The controlled drift is
and the diffusion is with a constant positive diagonal and a standard Brownian motion . The generator under the control value is .
A stationary Markov control is a Borel map , used as ; the class is . Its transition probability is , the law of started at . An invariant probability measure satisfies .
The Lyapunov function is built from the convex cut-off ( on , on ): for ,
For a weight , the -norm of a signed measure is .
Assume , and . Then there is such that for every there is with
and there are such that, for every , an invariant probability measure exists with
The rate and the constant do not depend on the control: that uniformity is the content of the theorem.
The result. Uniform exponential ergodicity makes the ergodic control problem for the multiclass Halfin–Whitt diffusion well posed over all stationary Markov policies: invariant measures form a tight family with uniformly integrable exponential moments, and long-run averages converge at a policy-independent geometric rate. In the paper it is the base for the prelimit results of Section 3, where the drift inequalities of Lemma 2.1 are compared with those of the -server queues. With the condition is sharp, since gives transience under every Markov control (Arapostathis, Pang and Sandrić 2019).
Formalizing it. The theorem is proved in the paper; none of it is formalized. The mission produces a machine-checked version with two printed slips corrected (see Formalization scope). Its analytic half, Lemma 2.1, (2.13), (2.10), (2.31) and the Foster–Lyapunov equation, is finite-dimensional calculus and is reachable now. The probabilistic half needs Itô's formula for SDEs with additive noise, existence and uniqueness for SDEs with Borel drifts, and a Harnack-type minorization, none of which Mathlib has.
The control enters the drift only through , but a Markov control may switch arbitrarily, so no single linear or quadratic Lyapunov function works for all policies; Dieker and Gao's common quadratic Lyapunov functions cover one static priority only. The function mixes an -scaled workload term with a -weighted idleness term, and the drift inequality must hold on both half-spaces and with explicit constants, which forces case splits over the classes with and .
For part (b), a Foster–Lyapunov inequality alone gives ergodicity for each control but not a control-independent rate: the constants of the standard Meyn–Tweedie argument depend on a minorization on a small set, and that minorization must be shown uniformly over all Borel controls, for which there is no regularity in to exploit.
EuclideanSpace ℝ (Fin m); classes are Fin m; control values are vectors in stdSimplex ℝ (Fin m). The model data is the published ManyServerQED.Scheduling.DiffusionData with its drift ; the SDE equation, invariant measures, generator and weighted total-variation norm use published GPhNGIDiffusion.EMError definitions. The local IsStrongSolution and IsMarkovTransition specify measurable, adapted solutions and their transition laws. The cut-off is the published cutoff.Measure.map returns a junk zero measure, so a local predicate is used here.Approximate counting asks for the number of marked items in a list of items, to within a multiplicative factor , when the marked set can only be accessed through a membership oracle. Brassard, Høyer, Mosca and Tapp (arXiv:quant-ph/0005055) gave a quantum algorithm that uses queries, which is optimal. Their algorithm combines Grover iterations with phase estimation, and so it needs the quantum Fourier transform (QFT). Counting is a basic subroutine in quantum algorithms for estimation, numerical integration and Monte Carlo speed-ups, so the circuit it requires matters.
Aaronson and Rall (arXiv:1908.10846, SOSA 2020) give an algorithm with the same query complexity that uses only Grover iterations and classical post-processing of measurement outcomes. Its analysis is short and elementary, and every constant in it is explicit. This mission formalizes their Theorem 1, the rotation lemma it rests on, and the numbered estimates of its proof (arXiv:1908.10846v6, pp. 4–10).
Timeline (as recounted on pp. 1–3 of the paper):
Let be a nonempty marked set with . The algorithm first pads the list to items, the added items being unmarked, and then works on . The membership oracle is the diagonal unitary . The uniform superposition is , and the Grover operator is
Preparing for an odd costs queries. Measuring it in the computational basis yields a marked item with probability given by the Born rule. With this probability is , so repetitions give a count of marked outcomes.
The algorithm has two loops. Step 1 tries , the largest odd integer at most , for , with measurements per round. It stops at the first at which at least 95% of the outcomes are marked. Step 2 keeps a bracket , initially and . In round it computes from the bracket by the rotation lemma (Lemma 2):
It then measures times, with , and shrinks by the factor : it raises if at least 12% of the outcomes are marked and lowers otherwise. It stops once and returns .
For nonempty , :
In the order of the proof:
Theorem 1 shows that the optimal query complexity of approximate counting is achieved without the quantum Fourier transform. The circuits involved are powers of the Grover operator followed by computational-basis measurements, and the classical control is a pair of loops with explicit thresholds. The same argument gives QFT-free amplitude estimation (Theorem 3 of the paper), and its rotation lemma is a reusable tool for any algorithm that brackets a rotation angle by biased coin tosses.
The result is proved on paper but not formalized. The platform has Grover's iteration for a single marked item; it has no Grover state for a marked set, no counting algorithm and no query-complexity statement of this kind. A complete development would provide a machine-checked quantum query algorithm whose output law is derived from the Born rule and the actual Grover operator. It would also provide a Chernoff bound in Kullback–Leibler form for the binomial distribution, which Mathlib does not have.
The deterministic estimates are elementary but numerous, and each constant (0.96, 7.5%, 16.5%, 1.102, 0.27, 0.42) must be checked against interval arithmetic for and . Two printed steps are numerically loose, (8) and (26), and must be replaced by correct intermediate values.
The probabilistic part has two difficulties. First, the success event of step 1 is not a single tail bound. Termination too early is controlled by a union bound over rounds , and the additive Hoeffding bound is too weak there: it needs the KL form (13). Second, step 2's output law is defined by a recursion whose bracket is random, and Lemma 2 applies to a round only while the bracket still contains . The union bound over rounds has to be carried through this recursion. Third, the paper bounds the queries only on its "ideal" event. Part 2 of the goal requires the bound on every run that ends with an accurate estimate, including runs in which step 1 stopped late.
Fin N' → ℂ, operators are Matrix (Fin N') (Fin N') ℂ, and is vecMulVec ψ (star ψ). The padding embeds Fin N as the first indices of Fin N'.approxCount N S ε δ F : PMF (Option (ℝ × ℕ)) is defined, not quantified. Its outputs are some (K̂, queries), or none when either loop runs out of its fuel F. Fuel exhaustion counts as failure. Measurement counts are Mathlib's binomial law with the Born probability computed from , and .round breaks ties upward, a choice the paper permits. The step-2 threshold is "at least 12%", as in the algorithm box; Lemma 2 is stated for both "more than" and "at least".Contributions of reusable infrastructure are welcome, in particular the KL-form Chernoff bound for ProbabilityTheory.binomial and lemmas on powers of a reflection product acting on a two-dimensional invariant subspace.
Manufacturers of products with fixed shelf lives must decide both how much to send from a warehouse to a store and which age cohorts to send. A shipment can reduce expiry at the warehouse while changing the age mix seen by shoppers at the store. In the two-echelon system studied by Akkaş and Honhon, the store does not control which items each shopper takes: some shoppers select older items first and the remainder select newer items first. The resulting waste at the warehouse and store can move in different directions when the manufacturer changes a shipment. The paper uses this setting to ask whether ship oldest first (SOF), a simple age-selection rule, minimizes waste over an infinite horizon. Akkaş and Honhon, SSRN manuscript.
The paper reports an inventory-age audit of a consumer packaged goods supplier and then studies the shipment decision analytically. Its Theorem 1 separates warehouse waste from the sum of warehouse and store waste. The former has a specified SOF policy that ships in full; the latter has an SOF age-selection rule but allows the shipped quantity to vary with the state. This mission formalizes those two claims, with a correction to one printed clause described below. Akkaş and Honhon, §3 and Theorem 1.
A unit remains saleable for periods, where . At the start of a period the warehouse holds units of age , and the store holds units of that age, for . Both age-zero entries are zero before replenishment. A plant then delivers fresh units so the warehouse's total post-replenishment stock reaches the exogenous order-up-to level . Thus its age-zero stock is . The manufacturer sends units of age from the warehouse to the store, subject to warehouse availability and the store's shelf capacity . In particular, and . Akkaş and Honhon, §4.1, pp. 10–13, and §4.2, p. 15.
The period's shopper population is . A fraction selects inventory first in, first out (FIFO), meaning older units first; the remaining shoppers select it last in, first out (LIFO), meaning newer units first. The discrete FIFO population is . If is the store stock after delivery, the paper's age-specific demand is
Here . Only units of age expire at the end of the period. Warehouse waste is , store waste is , and total waste is . The remaining units advance one age before the next period. An SOF shipment uses a younger unit only when every older available unit has been shipped. An SOF shipment in full fills the remaining store space or ships the entire available warehouse stock. Akkaş and Honhon, §4.1, pp. 11–12, and §4.2.1, p. 15.
Let and denote the upper and lower limits of expected Cesàro averages of warehouse waste. The first sentence of Theorem 1 is the mission's sole milestone:
The full goal also asserts that one stationary, feasible SOF policy minimizes total waste from every feasible initial state:
The policy chooses its shipping quantity from the current state; the theorem does not prescribe shipping in full for this second objective. These are waste objectives, independent of the paper's separate revenue, labor, and expiration-cost parameters. Akkaş and Honhon, Theorem 1, p. 15.
The warehouse result identifies a fixed, implementable shipment rule for minimizing waste at that location across the paper's whole FIFO/LIFO range. The total-waste result says that optimal age selection can remain SOF even when the quantity decision must respond to the store inventory and shopper behavior. Together they distinguish the two decisions in a setting where moving an expiring unit out of the warehouse can merely move the expiry to the store. The paper later uses its waste comparison in the analysis of profit policies under additional cost assumptions. Akkaş and Honhon, Appendix A.2–A.3.
The theorem is a published paper result, but this mission starts with open Lean statements rather than a machine-checked proof. A complete development would provide a reusable formal model of age-structured two-echelon inventory, stochastic shopper depletion, feasible shipment policies, and long-run waste criteria. The general controlled-process and Cesàro-average definitions can also support other finite inventory models.
An age-selection decision changes the stock carried into future periods, and a quantity decision changes the next warehouse replenishment. A comparison of immediate waste therefore does not by itself compare long-run averages. In particular, simply reordering each shipment to send older units first while keeping its quantity fixed can increase later warehouse waste for some policies; it cannot serve as an unrestricted policy-level argument. The store's FIFO/LIFO mixture introduces another intertemporal effect because a shipped younger unit can be sold ahead of an older one. Akkaş and Honhon, Appendix A.1, Appendix p. 1.
Lean uses finite age vectors indexed by Fin N, natural-number stocks and shipments, a real constrained to , and an arbitrary probability mass function for shopper population. The standing condition makes the final age cohort defined; and remain allowed. Demand samples are independent and identically distributed across periods, as in the stationary transition model of §4.2. Policies are time-dependent deterministic Markov rules: at period they choose a shipment from the current inventory state. This is the finite-state class used by the paper's dynamic program. The comparison includes every feasible rule in that class, every feasible initial state, and a common stationary SOF witness for total waste; it does not restrict competitors to SOF or full shipments. Standard finite-MDP results explain why stationary deterministic optimal policies suffice among broader history-dependent randomized classes. Puterman, Markov Decision Processes, Theorem 9.1.8.
Costs and expectations live in , and long-run criteria use upper and lower limits of expected Cesàro averages. The paper prints a plain limit without specifying what happens when a policy's average fails to converge. The upper-versus-lower comparison states the stronger optimality claim without relying on that convergence. Lean time starts at zero. Natural-number subtraction implements the paper's positive-part operation, and the post-replenishment stock formula is used only for feasible states. The model follows the printed balance equations when discarding the final-age store stock, despite a tension with the narrative timing of expired-unit pickup.
Three transcription corrections are explicit. The demand formula's sums use , the running index, where the page prints ; the action sum runs through age ; and the waste objectives are minimized despite a printed “max” in §4.2.1. More consequentially, Theorem 1's last clause says shipping is in full under pure FIFO. This is false and is omitted: for , , , , and a Bernoulli shopper population, SOF in full has average total waste while an SOF policy that holds stock back attains . The formal goal neither assumes this clause nor asserts its negation. Its feasible-policy and feasible-initial-state quantifiers rule out vacuous or artificially easy readings.
A complete proof may need finite-state inventory invariants, admissibility of the SOF-in-full rule, comparisons of age profiles over time, and results about average costs of controlled chains. Contributions establishing those reusable facts, or the stated warehouse and total-waste targets, are within scope. The separate profit theorems and numerical studies of the paper are outside this mission.
Many shared assets deteriorate unless someone pays to maintain them: a public infrastructure stock, a jointly used ecosystem, a joint venture's capital, a common research base. When several parties benefit from the same stock and each pays for its own contributions, every party is tempted to wait for the others to pay. Kwon (arXiv:1904.00500, published in Operations Research, 2022) models this as a two-player stochastic differential game in continuous time, in which each player may raise the stock at any rate, and studies the Markov perfect equilibria of the game.
The single-player version is a classical monotone follower problem of singular stochastic control (Alvarez 2001; Øksendal and Sulem 2005; Lon and Zervos 2011): the optimal policy reflects the stock upward at a threshold. In the game, a natural first guess is that free riding lowers that threshold, or that the players take turns reflecting. The paper shows instead that, in the symmetric game, there is an equilibrium in which both players contribute gradually, at a finite rate, below the same threshold as the single decision maker. The equilibrium is a continuous-state analogue of the mixed-strategy delay equilibrium of the war of attrition.
The stock lives in an interval ( or allowed) and satisfies
on a filtered probability space satisfying the usual conditions, where is a Wiener process, (the stock deteriorates) and . Player 's control is any adapted, nondecreasing, right-continuous process: its cumulative contribution. A control may jump, including at time . Player 's payoff from the initial stock is
where is an increasing, bounded-above flow profit, the unit cost and the discount rate. In the symmetric game both players have the same and .
The analysis uses:
Assumptions 1–3 of the paper require Lipschitz coefficients with linear growth, a uniform integrability condition on , integrability of , and boundary behaviour of and at and ; in particular increases below a point and decreases above it.
The single decision maker's value is
for a threshold and a coefficient that make twice continuously differentiable (Lemma 1). The candidate equilibrium rate is
If of (6) is Lipschitz on with linear growth, then the profile in which both players contribute at the regular rate is a Markov perfect equilibrium, and
The equilibrium is against all adapted deviations, from every initial state, with the opponent keeping its feedback rule .
Theorem 2 says that the free-rider problem in this game does not shift the threshold below which the stock is maintained; it changes how the stock is maintained, from instantaneous reflection by one party to gradual, rate-limited contribution by both. The equilibrium value equals the single decision maker's value, so the players lose nothing relative to a single owner who pays for everything, although each pays only part. This contrasts with the asymmetric case, where the paper's Theorem 3 rules out a regular-control equilibrium with smooth payoffs. The result is one of the few explicit equilibria of a nonzero-sum singular-control game with linear costs.
The paper's proofs are on paper only. A formalization requires machine-checked versions of a verification theorem for one-dimensional singular control (the optimality condition), of the analysis of the free-boundary point through the fundamental solutions, and of the passage from best response within a restricted class to best response among all adapted controls. The verification steps for a controlled diffusion with jumps, Itô's formula for semimartingales with a nondecreasing part, and the comparison with the uncontrolled process are reusable for other singular-control and monotone-follower problems on the platform.
The obvious route, Itô's formula applied to along an arbitrary deviation, requires the transversality limit and uniform integrability of the localised terms. is unbounded below when , and the deviation is arbitrary, so this needs the comparison of every controlled state with the uncontrolled process and Assumption 1(ii). The proof also passes through a best-response theorem for the restricted class (Theorem 1), whose conclusion is weaker than a Nash equilibrium; the upgrade to all of is a separate argument. Finally, the identification of uses the boundary behaviour of , and the scale density at the ends of , which Mathlib does not provide for general diffusions.
Time is . The probabilistic data (measure, filtration, Wiener process, the uncontrolled family , , ) form one structure, and the standing assumptions of §2.1 together with Assumptions 1–3 form one predicate, a hypothesis of every theorem. The Itô integral of the state equation is the published relation EthierKurtz.HasBrownianItoIntegral; Mathlib supplies Brownian motion, stopping times, uniform integrability and Stieltjes measures.
Conventions the formalization commits to:
The threshold and coefficient are not chosen by the formalization: the goal holds for every pair making twice continuously differentiable on , and smoothness at determines the pair. The rate is computed from through the generator, not supplied as a free function, and its nonnegativity is part of the conclusion. A payoff is never a Bochner integral of a non-integrable function, so no junk value can enter an equilibrium comparison.
Contributions welcome: proofs of the milestones, and reusable infrastructure for Itô's formula with nondecreasing càdlàg integrators, comparison theorems for one-dimensional SDEs, and the boundary classification of one-dimensional diffusions.
Personalized decisions in medicine, marketing and public policy are increasingly learned from observational data: records of who received which treatment and how it turned out. Standard policy-learning methods assume unconfoundedness, that treatment assignment depends only on observed covariates. When an unobserved factor influences both the treatment and the outcome, these methods can return a policy that is worse than the status quo, and nothing in the data reveals it.
Kallus and Zhou (arXiv:1805.08593, published in Management Science 2021 as Minimax-Optimal Policy Learning Under Unobserved Confounding) take the robust route. They fix a bound on how far the unobserved confounding may distort the propensity scores, in the marginal sensitivity model of Tan (2006), and learn the policy that minimizes the worst-case regret against a baseline policy over every distortion the model allows. The paper proves two guarantees for this policy: it never does worse than the baseline up to vanishing terms (Theorem 2), and it is asymptotically minimax-optimal (Corollary 7). This mission is about the second.
Data are iid triples : covariates , one of treatments , and a real outcome , read as a loss. The nominal propensity is . A policy assigns to each a probability vector over treatments; is a class of policies and a baseline.
Inverse propensity weights are unknown under confounding. The marginal sensitivity model with parameter confines them to the weight box
The set of such weight functions is , and its restriction to a sample of size is the box .
For weights , the Hájek regret of against is with
and is the same expression with replaced by the sample average . The worst-case regrets are
The learned policy minimizes over ; the population minimax regret is .
The complexity of is measured by its VC-major dimension (Definition 1): the largest such that some points have all subsets cut out by superlevel sets , , . The standing assumptions are bounded outcomes (Assumption 1), overlap with constant (Assumption 2), and VC-major dimension of at most (Assumption 3).
There is a constant depending only on such that, with probability at least ,
The result. Corollary 7 says that the confounding-robust policy loses at most against the best possible worst-case guarantee in its class. The worst-case regret cannot be identified from data. It is the regret the decision maker must budget for when the confounding is only known to lie within . With Theorem 2, it makes the procedure both safe and asymptotically optimal among safe procedures, for randomized and multi-treatment policy classes of finite VC-major dimension.
Formalizing it. The paper's proof of the dimension-only dependence of is incomplete. Its Proposition 5, which states that the monotone weight class has finite VC-major dimension under Assumption 3, is false as printed. A class of monotone policies on with VC-major dimension at most gives a that shatters arbitrarily large grids. The printed proof of Theorem 6 runs through Proposition 5 and Lemma 4, so Theorem 6 and Corollary 7 are believed true but are not established by the paper. A formal proof would settle the claim. None of the statements has a machine-checked proof.
The worst case over is a supremum over an essentially arbitrary bounded function class, which is far too large for a uniform law of large numbers. Proposition 3 reduces it to monotone transformations of the score . This is a linear-fractional program whose population version lives in a function space. The natural next step is to apply a uniform law over the pairs . That step needs a complexity bound on the composition in terms of the dimension of alone, and this is exactly where the printed argument fails. A different route is needed. One candidate exploits the Lipschitz dependence of the worst-case Hájek value on the scores. The Hájek ratios also need denominators bounded away from zero uniformly. The paper's decomposition (p. 42) uses , which holds for the true weights only.
All statements live in the namespace ConfoundRobust.Minimax, with one definitions file Setting.
𝒳 × Fin m × ℝ, with treatments 0-indexed as on the page. The population is a probability measure μ, and a sample is ω : Fin n → Obs 𝒳 m under Measure.pi. is .π : 𝒳 → Fin m → ℝ, with π x t , measurable and simplex-valued. The nominal propensity is a measurable version of , given by its defining integral identity, with .sSup/sInf; the weight sets are nonempty (they contain ) and the regrets are bounded, so these are true extrema. An empty treatment group gives a Hájek ratio .∀ v, ∃ K, ∀ (everything else). Letting depend on , , or would trivialize the bound and is ruled out.A complete development needs: linear-fractional optimization over function boxes; Dudley-type entropy bounds for VC-major and VC-hull classes; the Dvoretzky–Kiefer–Wolfowitz inequality with Massart's constant (posed separately on the platform as MassartDKW.Tight.corollary_1); and a uniform bound for Hájek ratios. The empirical-process pieces (VC-major classes, monotone classes) are reusable well beyond this mission. Contributions to any milestone, and alternative routes to Theorem 6 that avoid Proposition 5, are welcome.
Characterizing the state of an -qubit device is a basic task in quantum computing and simulation. Full quantum state tomography reconstructs completely, but it needs a number of measurements exponential in (Haah et al., 2017; O'Donnell–Wright, 2016). In practice one usually wants only a list of properties, such as the expectation values of observables (fidelities with target states, entanglement witnesses, local energies). Aaronson's shadow tomography (Aaronson, 2018) showed that such properties can be learned from a number of copies polylogarithmic in , but with collective measurements across many copies that are far beyond present hardware.
Huang, Kueng and Preskill (arXiv:2002.08953, Nature Physics 16, 2020) gave a procedure that uses only single-copy randomized measurements: rotate by a random unitary from a fixed ensemble, measure in the computational basis, and store the outcome classically. From these records, called classical shadows, a median-of-means estimator predicts all properties at once. Their Theorem 1 bounds the number of measurements by times a state-independent norm of the observables. The method has since become a standard tool for benchmarking and for estimating many observables in experiments.
Fix qubits. Computational-basis labels are bit strings , and operators are complex matrices. A state is a positive semidefinite matrix of trace one.
A measurement primitive (Definition 1) is a finite ensemble of unitaries drawn with probabilities . One snapshot of draws with probability , applies , and measures, obtaining with probability (S1). The primitive is tomographically complete if any two distinct states give different outcome probabilities for some and some of positive weight.
The measurement channel (S2) is the linear map
and the classical shadow of the outcome is (S3). For an observable the single-shadow prediction is . The shadow norm (S7) is
and is the traceless part of .
The median-of-means prediction (S12) takes independent snapshots, splits them into batches of , averages within each batch, and outputs the median of the batch means.
For Hermitian , and integers
the median-of-means predictions from independent classical shadows satisfy
The constants , and are the paper's own. Remark 1 of the paper says they are chosen for simplicity, not tightness.
Theorem 1 gives a sample complexity . It grows only logarithmically in the number of properties and does not depend on the dimension except through the shadow norm. For random global Clifford measurements the shadow norm is at most . For random single-qubit Pauli measurements it is at most for an observable acting on qubits (Propositions 1–3 of the paper). These instantiations are what make the protocol useful for fidelity estimation and for local observables. The theorem also separates two independent ingredients, a state-independent variance bound and a generic median-of-means concentration bound, and each is reusable.
The result is proved in the paper. As far as the platform's corpus shows, it has not been machine-checked. This mission produces a formal statement of the protocol and its guarantee, and its definitions (measurement channel, classical shadow, shadow norm) can be reused for the Clifford and Pauli instantiations and for the paper's quadratic-function estimator (Theorem 4).
The linear-algebra layer is elementary but has to be set up carefully. The channel must be shown invertible from completeness on states alone. Its inverse must be shown trace-preserving and self-adjoint, and the variance has to be rewritten as an expectation of squared diagonal entries.
The probabilistic layer is where the naive argument fails. Chebyshev's inequality on a single empirical mean gives a sample size proportional to , not . Applying Hoeffding's inequality to the number of failing batches gives exponent . That is weaker than , so it does not reach the stated constant . The bound needs the relative-entropy form of the Chernoff bound for a binomial tail, which Mathlib does not provide in this form. The median also has to be related to a count of deviating batch means without sign or tie errors.
Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ. States are the published WildeQIT.IsDensityOperator.WildeQIT.FinDist of weights and a family in Matrix.unitaryGroup. The paper's ensemble is general, but both of its examples are finite with uniform weights. "" in completeness means positive weight.Ring.inverse of it. Every statement using assumes tomographic completeness.Theorem 1 must not be restated about an abstract estimator with a variance bound; that is milestone 6. The goal is about the median of means of classical shadows of a concrete primitive, with the shadow norm of (S7). Tomographic completeness is satisfiable non-trivially: the three single-qubit Pauli bases form a complete primitive, so the goal's hypotheses are not vacuous.
Needed infrastructure: elementary facts about the trace pairing and diagonal entries of ; finite product measures, or direct finite-sum manipulations; Chebyshev's inequality; a binomial Chernoff bound in relative-entropy form; and order-statistic facts about the median. The binomial tail bound and the median-of-means lemma are independent of quantum information and reusable elsewhere. Contributions to any milestone are welcome. The Clifford and Pauli shadow-norm computations are natural follow-up work on top of these definitions.
Fast and fault-tolerant logical measurements: Auxiliary hypergraphs and transversal surgery.
Let be finite based chain complexes over , and let . Their tensor complex has differential . There exists an -linear isomorphism
The direct sum is algebraic; the finite based complexes have only finitely many nonzero graded components. No particular isomorphism or representative map is asserted.
Let binary check matrices satisfy , and let be the prescribed pair-reading matrices of Eq. (2). Write and . Then
The deformation of two identical memories therefore retains exactly logical qubits, with no additional logical classes. All spaces and isomorphisms are over .
Let and satisfy , and let . In the product bases, the three coboundaries of the pair-reading deformation are
Here old data precede new data, and old Z checks precede new Z checks; denotes the metachecks. These are the explicit tensor-product differentials, retaining the final degree as in pp.21-22.
Let define a binary CSS memory with X and Z distances at least . Its prescribed pair-reading deformation has check matrices satisfying
A lower distance bound quantifies over every nontrivial normalizer class modulo stabilizers; the distance is infinite when no such class exists. This is a spatial code-distance assertion.
Let define a binary CSS memory with both distances at least . Let have full row rank and every row of Hamming weight greater than one. The prescribed Z-pattern deformation of identical memories, with new data qubits indexed by pattern rows and memory X checks, satisfies
The conclusion includes CSS commutation and every nontrivial logical class. Sparsity belongs to the separate resource claim.
Let be a finite incidence matrix, , and its support union. Put , where restriction to is zero extended and bars denote Hamming weight. For , suppose for every binary vector . Let the integer satisfy , and form , with the path incidence on vertices. At any selected level , embed as . Then
Thus the thickening has certified modular expansion at least one at every choice of a single level. Cut certificates avoid asserting a largest finite expansion on degenerate inputs.
Let be finite, let contain , and let . Let be the support union of , and let , using zero-extended restriction and Hamming weight. Then
Hence is a certified modular-expansion lower bound, even when no largest finite expansion exists.
Let be finite and . For an integer , form . Embed at any one level as , and write for its support union. Then
Restrictions are zero extended and weights are Hamming weights. Integer -fold thickening thus certifies modular expansion one.
Let satisfy , defining a self-dual CSS code with . Let isometrically encode all logical qubits onto its entire codespace. Suppose matching binary supports satisfy , and their physical X and Z products implement the corresponding logical through . There exists a physical Pauli correction , independent of the encoded state, such that
Here , and includes its Pauli phase. The matrix equality holds on the entire encoded space, implementing S on every logical qubit.
Let have finite nonempty vertex and edge sets, with every column weight at most . Let and . Write for the modular cut inequality using the support union of , and let indicate . Then
If , the relative inequality at is equivalent to global expansion . If also the support union of is all of , then
The last inequality, with locality , is classical soundness . The support condition implements the source's explicit specialization.
Let be a chain map of finite based binary complexes and . Let be its induced homology map. Then
All dimensions are over , and map images are constructed from . The addition form avoids truncated subtraction of natural dimensions.
Let be a finite binary CSS complex supported in degrees , and let be the repetition length. Let , and let be its prescribed two-endpoint cone. Let and be the cochain-oriented bulk and cone obtained by the specified degree-reversing dual constructions. Put and . Then
These retain all boundary homology classes, including immediately terminating classes. They imply no operational fault-distance bound by themselves.
Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.
NLTS Hamiltonians from good quantum codes establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Fix positive clustering constants , a bound on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant bounding the total number of checks by . There exist and an integer , uniform over the code, state, energy density and preparing circuit, with the following property.
For , let and be check matrices with , sparsity at most , and . Put and , and assume the CSS condition . Write for the encoded dimension, and assume . Assume Property 1: for every and every , implies or , and the same implication holds with interchanged. Here , and is Hamming weight. Define the unnormalized check Hamiltonian , counting all supplied rows.
Define
The corrected permitted cutoff is
For every density matrix and every ,
for every preparing circuit . A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on qubits, for any , starts in , and has reduced output on the first qubits after discarding the other qubits. Depth is its number of layers; is the natural logarithm.
Moreover, for every fixed , there exist and , uniform over all code instances, such that whenever , and , one has
Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at already implies linear distance.
This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.
Source correction. The paper prints only . Its proof uses Property 1 at with , so we also require . This is exactly the missing domain condition; it is automatic if . No normalization is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.
Correction to the printed source.
Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.
Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.
Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.
Fix positive clustering constants , a bound on the number of nonzero entries in each row and column of the binary check matrices, and a positive constant bounding the total number of checks by . There exist and an integer , uniform over the code, state, energy density and preparing circuit, with the following property.
For , let and be check matrices with , sparsity at most , and . Put and , and assume the CSS condition . Write for the encoded dimension, and assume . Assume Property 1: for every and every , implies or , and the same implication holds with interchanged. Here , and is Hamming weight. Define the unnormalized check Hamiltonian , counting all supplied rows.
Define
The corrected permitted cutoff is
For every density matrix and every ,
for every preparing circuit . A preparing circuit consists of layers of disjoint arbitrary one- and two-qubit unitary gates on qubits, for any , starts in , and has reduced output on the first qubits after discarding the other qubits. Depth is its number of layers; is the natural logarithm.
Moreover, for every fixed , there exist and , uniform over all code instances, such that whenever , and , one has
Consequently the allowed energy density can be chosen as a positive constant for the constant-rate, linear-distance qLDPC families satisfying Property 1 considered in the paper. The distance parameter does not enter the displayed cutoff; the paper's footnote 3 notes that Property 1 at already implies linear distance.
This gives a depth obstruction for every low-energy density matrix, including mixed states, rather than only ground states.
Source correction. The paper prints only . Its proof uses Property 1 at with , so we also require . This is exactly the missing domain condition; it is automatic if . No normalization is imposed, and the frozen printed cutoff is retained as the first entry of the minimum.
Correction to the printed source.
Printed: Theorem 5 permits eps < E(C), where E(C) is the printed energyCutoff, for arbitrary positive c1.
Corrected: Use eps < min(E(C), delta0min(mx,mz)/(400n)); give the eventual positive floor for this same minimum. No other hypothesis, constant, or conclusion is changed.
Reason: The source proof sets epsilon1=200neps/min(mx,mz) on p.3 and applies Property 1 at 2epsilon1 on p.4. Its domain is delta<delta0, but the printed cutoff only supplies 2c1epsilon1<delta0. The additional strict upper bound is exactly 2epsilon1<delta0. It is redundant for c1>=1 and retains every c1<1 instance satisfying the actual proof-domain condition.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
There is a deterministically explicit family of binary CSS check descriptions on qubits, and constants , a locality bound , and a threshold , all independent of . Explicit means that a deterministic polynomial-time function on unary outputs the actual row counts and both binary check matrices. For every , both check matrices have row and column weights at most , their total row count satisfies , and their associated projector terms or act on at most qubits, commute, and annihilate a common unit vector. Let be this unnormalized Hamiltonian. Every circuit of parallel one- and two-qubit unitaries on disjoint wires, starting from zero qubits and allowing arbitrary clean ancillas and discarded qubits, has an output density operator satisfying, for ,
This is the existence of an NLTS Hamiltonian family. Quantifying over every preparation circuit gives the lower bound for mixed as well as pure low-energy states.
Formalization Note The deterministic interpretation of explicit and the CSS witness implementation are recorded for independent moderation; the theorem does not assume an NLTS guarantee on its family.
Let be a binary CSS check presentation with , and let be any density operator with , where and is the sum of the actual check projectors. Write for its standard- and product-Hadamard-basis distributions and for the words violating at most a fraction of the actual checks on side . For every ,
If , both and have probability one. If , choosing gives both masses at least .
These bounds place low-energy measurement outcomes in the approximate classical codes. The energy identity and probability bounds are conclusions of the source argument, not hypotheses of the formal statement.
Let and be a binary CSS pair satisfying Property 1 with positive constants . Assume , , and . On define when , with the corresponding definition on modulo . Here . For either basis this is an equivalence relation. Its distinct computed classes are nonempty, pairwise disjoint, and cover the corresponding approximate code. Distinct classes satisfy
This constructs the separated clusters needed for the depth argument.
Formalization Note The strict domain follows Property 1 on page 2; the page-4 prose writes a non-strict endpoint. The classes are computed from the relation rather than supplied with a separation guarantee.
Correction to the printed source.
Printed: Page 4 says 'assuming 2 epsilon1 <= delta0', but Property 1 on page 2 is stated only for delta < delta0.
Corrected: Use 0 <= epsilon1 and the strict inequality 2 epsilon1 < delta0 in the clustering regime.
Reason: The proof invokes Property 1 at delta = 2 epsilon1; the strict domain is necessary. This is a standing-domain clarification pending independent moderation.
Consider a binary CSS presentation with and logical dimension , satisfying Property 1 with . Let be any density operator. Assume , , , and
For the computed clusters in the preceding result, either every standard-basis cluster has -mass strictly less than , or every Hadamard-basis cluster has -mass strictly less than .
This uncertainty consequence selects a basis in which no single cluster captures almost all probability. It requires no low-energy hypothesis once the clusters are defined.
Formalization Note The subtraction takes place in the reals. The positive- reading comes from the section's positive-rate setting and is flagged for independent moderation.
Correction to the printed source.
Printed: The displayed finite lemma does not explicitly say k>=1, while Section 2 is introduced for constant-rate code families.
Corrected: State the finite lemma for k>=1 and n,mx,mz>0, keeping ((k-1)/(4n))^2 with real subtraction.
Reason: The proof uses a positive logical dimension; at k=0 the zero-radius clusters can concentrate in both bases. The finite positive-rate reading requires independent moderation.
Let be any -qubit density operator, and let be its standard- and product-Hadamard-basis measurement distributions. For all sets ,
This bounds concentration in conjugate bases and applies to mixed states. No positive-mass hypothesis on is required; empty sets and are allowed.
Let a binary CSS presentation on qubits satisfy Property 1 with , and assume , , and . Fix either basis and any density operator . Suppose its measurement distribution gives the approximate-code set mass at least , while each computed class has mass less than . Then there are disjoint subcollections of the computed classes whose unions are disjoint and satisfy
This extracts two positive-mass separated sets in whichever basis Lemma 2 selects. Both probability constants and the cross-union separation are retained.
Let be a circuit of depth consisting of layers of disjoint one- and two-qubit unitaries, starting in the all-zero product state. Allow any number of clean ancillas and measure only its output qubits in the standard basis, giving distribution . Let , and suppose . For any such that every has Hamming distance at least ,
For positive set distance this is equivalently .
This is the quantitative circuit-depth obstruction for well-spread output distributions. The exponential formulation also covers overlapping sets without taking the logarithm of zero; the original circuit's workspace is unrestricted.
Let and . Let and . Suppose every with satisfies . Then
This transfers small-set expansion to the clustering dichotomy. Both the size cutoff and syndrome cutoff use the number of columns , even for rectangular matrices.
Formalization Note Positivity is taken from the proof and the paragraph immediately following Lemma 8; the unsupported zero- extension is excluded.
Correction to the printed source.
Printed: The displayed Lemma 8 omits its parameter domain; its proof uses delta>0 and mu>0 and the following paragraph takes mu<nu.
Corrected: State Lemma 8 on the meaningful positive regime delta>0 and 0<mu<nu, as pinned by the plan and proof.
Reason: For delta=0, an expansion hypothesis with beta=0 supplies no information and the claimed nontrivial dichotomy can fail. Independent moderation must confirm the intended domain.
Let be a family of binary CSS check presentations. Fix positive and . For all , suppose . For every , define as the words in of minimum Hamming weight within their coset modulo , and define analogously modulo . Assume is -expanding on and is -expanding on . Then there are constants , independent of , such that for all and ,
and the same dichotomy holds on the side modulo .
This derives Property 1 from uniform expansion of minimal representatives, without assuming the desired dichotomy. The check-density factors converting to a threshold relative to are retained.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
Classical statistical mechanics describes a particle by a probability density on phase space; quantum mechanics replaces this by a wavefunction, and the uncertainty principle forbids any honest probability interpretation of simultaneous position and momentum. In 1932, Eugene Wigner introduced the transform that has become the standard way of placing quantum states on classical phase space anyway: a quasiprobability distribution , defined by an explicit integral formula, whose marginals reproduce the Born position and momentum distributions of the wavefunction (Wigner 1932). Unlike a probability density, generally takes negative values, and this negativity is the standard marker of genuinely quantum behavior — of interference — in quantum optics, quantum information, and the study of the quantum-to-classical transition.
The central question about the probabilistic character of is: which quantum states have an everywhere nonnegative Wigner function? Hudson's theorem (1974) gives the complete answer in one dimension: only Gaussian wave packets (Hudson 1974). This mission formalizes the definition, the basic properties, and the positivity characterization of the Wigner function, following the source text, the Wikipedia article Wigner quasiprobability distribution (oldid 1376057304).
Timeline of the key results:
A wavefunction is a function , and denotes the reduced Planck constant. The Wigner function of at the phase-space point is
a Lebesgue (Bochner) integral over . The Lean development factors this into three definitions mirroring the formula: the integrand (Wigner.wignerIntegrand), the integral (Wigner.wignerIntegral), and the Wigner function itself (Wigner.wigner), defined as the real part of the integral divided by ; that the discarded imaginary part vanishes is itself milestone 1. The Fock states of the harmonic oscillator enter through the physicists' Hermite polynomials and the ordinary Laguerre polynomials , defined by their standard three-term recurrences, and the normalized -th Hermite function
This is exactly the source's statement of Hudson's theorem; nothing is left unfixed. The mission is complete when the goal is proved.
The milestone list is the source's property list, ordered as the attack path: (1) reality of the defining integral; (2) the position marginal ; (3) the total integral ; (4) Groenewold's closed formula for the Fock states; (5) a concrete negativity witness, the first excited Fock state at the origin; (6) the pointwise bound ; (7) the converse of Hudson's theorem, that Gaussian pure states have nonnegative Wigner function.
The result itself. Hudson's theorem draws the exact boundary between the classical and the quantum in phase space: Gaussian states — coherent and squeezed states — are precisely the pure states that can be described by an honest phase-space probability density. This is used in quantum optics as a nonclassicality criterion, in tomography and state-reconstruction theory, and in the study of the quantum-to-classical transition: negativity of is shielded by the uncertainty principle (negative regions cannot extend beyond a few ) and disappears in the classical limit, as the source emphasizes.
What formalizing it adds. The Wigner transform and this circle of ideas are absent from current Mathlib, so the mission builds the foundations itself: the integral transform and its basic identities (reality, marginals, normalization, boundedness), the Hermite/Laguerre recurrences and Groenewold's Fock-state formula, and finally Hudson's theorem with its converse. All of these are reusable well beyond the mission — for quantum optics, for the Wigner–Ville time–frequency distribution used in signal analysis, and for the wider phase-space formulation of quantum mechanics (Moyal brackets, star products). These are known results: this is formalization of known mathematics, not new mathematics, and no machine-checked proof of Hudson's theorem exists in Mathlib today.
The naive approach to Hudson's theorem is doomed from the start, and solvers should know it: since the Husimi function (a Gaussian smoothing of ) is positive for every quantum state, no smoothing or positivity-of-convolution argument can extract any information from . The known route (Soto–Claverie) is: everywhere forces the Husimi function strictly positive everywhere; the Husimi function is the squared modulus of the Segal–Bargmann transform of , so is a zero-free entire function; hence for some entire , and square-integrability of against a Gaussian measure forces to have at most quadratic growth, hence to be a quadratic polynomial; inverting the Segal–Bargmann transform then exhibits as a Gaussian. The hard Lean steps are the growth-to-polynomial (Liouville-type) step, the inversion of the transform, and, for the milestone properties, the Fubini and Fourier-inversion machinery. Mathlib contains the raw harmonic analysis (Fourier inversion for Schwartz functions) but none of the assembled phase-space layer.
Infrastructure contributed and reusable beyond this mission: hermiteP, laguerreL, fockState, wignerIntegrand, wignerIntegral, wigner. Welcome additional contributions: the momentum marginal, the state-overlap formula (Property 6), Galilei covariance (Property 4), and harmonic-oscillator time evolution, as further theorems in the same namespace.
Qubit Entanglement Breaking Channels.
Let be complex-linear, completely positive and trace preserving. Let and . Then
The inequality is the positive-semidefinite operator order. This provides an operator test on the normalized Choi state.
Let , and let be the trace-preserving canonical Bloch map . If it is entanglement breaking, then
There is no unitality assumption. This is a necessary condition for the general translated channel.
Let be a completely positive trace-preserving qubit map with . Suppose independent unitary changes of input and output bases put it in canonical form with parameters . Then
This makes the necessary condition sufficient in the unital case.
For , let have translation and diagonal Bloch parameters . These maps are completely positive and trace preserving, and
Moreover, for every there is with and not entanglement breaking. Thus small diagonal-parameter sum does not suffice for translated channels.
For and , let . Then
Whenever this holds, is CQ and equals , where and . This includes , when the image is a point.
Let be a QC qubit channel: it measures a POVM and prepares one of two orthogonal pure states. There are qubit unitaries and a CQ map such that
A CQ map measures rank-one orthogonal input projectors and prepares density matrices. The assertion relates these two channel subclasses without identifying their definitions.
Set , , , and . Set , with , and define
The effects form an extreme three-outcome POVM, each is a density matrix, and is EBT, neither CQ nor a point channel, and not extreme in the EBT set. Thus extreme measurement data need not produce an extreme channel.
Let be a CPT qubit map in the fixed canonical basis, and let . Then is completely positive, and changing any individual translation coordinate to preserves complete positivity. In addition,
Here CP denotes complete positivity. These are all three numbered assertions, together with the any-coordinate translation invariance explained immediately before the proposition.
Let be a CPT qubit map in canonical form. Then
The planar regime includes degenerate lines and points. This is a sufficient condition only.
Let with , and set . The canonical point map is CPT and CQ, is a density matrix, and on every operator it satisfies
If , there is a unit vector with , and the map is extreme in both the CPT and EBT sets. This identifies the pure-output endpoint of the point-channel family.
Let be a CPT canonical qubit map. If exactly one coordinate of is zero, then
Also, when , . If both are nonzero and equality holds, then . Thus a truly planar image stays strictly inside the Bloch sphere.
In a fixed diagonal basis, let , and . Then
The theorem determines both the entire parameter octahedron and exactly its six extreme points.
In the real vector space of complex-linear qubit maps, let be the unital trace-preserving entanglement-breaking maps, and the unital CQ maps. Then
The channel sets allow arbitrary input and output bases. This is a statement in map space, not only in one diagonal parameter slice.
Fix any translation , and define . Then
Inversion negates and leaves fixed. Infeasible translations are permitted; both sides can be empty.
Let be the trace-preserving entanglement-breaking complex-linear qubit maps, and the CQ maps. Then
These are both conclusions of the main theorem. It does not assert that every CQ map is extreme. The proof gap concerning intersecting planes on p.15 is recorded separately, without becoming a theorem hypothesis.
Suppose is EBT and for a chosen coordinate . It belongs to the real convex hull of canonical CQ maps satisfying and having at most one nonzero coordinate of . Moreover, if denotes the CPT parameter slice fixing only and , then
This preserves the canonical coordinate plane, including point-channel endpoints; the other translation coordinates may vary.
For a CPT canonical qubit map with ,
For fixed with and , its EBT slice is exactly . This includes the filled square and its collapsed endpoints; a negative radicand is not totalized into an extra radius-zero slice.
Fix and . Let consist of canonical EBT maps with these fixed parameters and either or . Let be all CQ maps canonical in the same basis. Then
This gives the same-basis decomposition on the illustrated parallelogram. It neither covers the entire slice nor requires CQ summands to retain .
Let be EBT, with for all three coordinates. There are input/output unitaries and such that, writing ,
Here consists of canonical CQ maps for which for some . Also . Thus summands are canonical in the rotated basis and need not be canonical in the original one.
Only these reviewed original-paper statements are in scope. Definitions have reviewed bodies; target proofs remain open (sorry). Reviewed deferrals are excluded. No theorem proof or whole-paper formal proof is claimed.
Many quantum algorithms act on a matrix that is not itself unitary: a Hamiltonian to be simulated, a linear system to be inverted, a projector to be amplified. The standard way to hand such a matrix to a quantum computer is to embed it as a block of a unitary , so that for two orthogonal projectors . The question is then which functions can be produced from a few uses of and .
Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019) answered it for polynomials: interleaving and with phase rotations about and applies a polynomial to every singular value of . This quantum singular value transformation (QSVT) recovers Hamiltonian simulation, amplitude amplification, fixed-point search, quantum walks and matrix inversion as instances of one identity, and is now the common language of these algorithms (see the survey of Martyn, Rossi, Tan and Chuang, PRX Quantum 2021).
Timeline.
Let be a finite-dimensional complex Hilbert space, a unitary on it, and orthogonal projectors. The projected unitary is . Put , , . A singular value decomposition of consists of orthonormal bases of and of and numbers with
For , the singular value transformation is when is odd and when is even, with for .
The phase operator of a projector is . For , the alternating phase modulation sequence is the product, from on the left to on the right, of when is even and of when is odd. On the single-qubit side, for , and is said to realize if is the top-left entry of for every .
In Lean these are ProjUnitarySVD U Proj Projt (the decomposition data), svtOdd/svtEven, phaseRefl, altPhaseSeq, reflR and qspRefl, in the namespace QSVT19.Main.
Let and let have degree , parity , and on . Then there is such that for every singular value decomposition of
with for odd and for even . The only constraints on are those that are necessary; no degree-dependent constant appears.
The result. Corollary 18 says that every real polynomial of degree , of definite parity and bounded by on , can be applied to the singular values of with uses of and and one ancilla qubit. Every application in §3.4–§5 of the paper (fixed-point amplitude amplification, singular vector transformation, the pseudoinverse, Hamiltonian simulation, Gibbs sampling) is this corollary applied to a suitable approximating polynomial, so a formal proof makes all of them conditional only on polynomial approximation bounds.
Formalizing it. The result is proved in the paper; none of the statements of this mission has a machine-checked proof on the platform. A formal development would provide reusable infrastructure absent from Mathlib: singular value decompositions over sub-spaces, the two-dimensional invariant-subspace decomposition of a projected unitary (a quantitative form of Jordan's lemma), and the polynomial characterization of single-qubit QSP. Theorem 3 of the paper, the form of the QSP characterization, is already posed on the platform as QAlgorithms.Childs.qsp_characterization; Corollary 8 depends on it.
The obvious argument for Theorem 17 is "restrict to each two-dimensional subspace and read off the QSP product". Making that rigorous means proving that the subspaces of Definition 12 are pairwise orthogonal, invariant under every factor of , and that acts on each pair of bases by exactly the reflection , including the degenerate blocks with , the one-dimensional blocks where contributes a phase , and the complement . The polynomial side is harder still: Lemma 6 factors a nonnegative even polynomial through its multiset of complex roots, grouping roots in , in , on the imaginary axis and in the open quadrant, while tracking degree and parity. Neither step reduces to a library lemma, and an argument that works only for Hermitian , or only when , proves a different theorem.
ι → ℂ for a Fintype ι with the inner product star v ⬝ᵥ w; operators are Matrix ι ι ℂ; "unitary" is U ∈ Matrix.unitaryGroup ι ℂ; "orthogonal projector" is IsStarProjection. The projectors are named Proj, Projt because Π is Lean notation. Indices are 0-based.ProjUnitarySVD U Proj Projt of data: orthonormal families with , , nonnegative non-increasing , and (17). The goal is posed for every such decomposition, with chosen first; the Definition 11 milestone shows that one exists. is a consequence and is not assumed.QAlgorithms_Defs_Hamiltonian. "deg ≤ k − 1" is degree < k and "parity " is parity , avoiding natural-number subtraction.A seller who sells over two periods, at a full price now and a discount later, loses revenue to strategic customers who wait for the discount. Waiting is costly to the customer only through availability risk: if inventory is scarce, the product may be gone by the second period. Inventory is usually known to the firm and not to its customers, so the firm can try to shape how scarce the product looks. Drakopoulos, Jain and Randhawa (SSRN 3191629, version of April 17, 2020) study this as a problem of Bayesian persuasion (Kamenica and Gentzkow, AER 2011) with many receivers: the firm commits to prices and to a signaling policy before it learns its inventory, and then sends each customer a recommendation.
Their two main results separate public from private information. Theorem 1 (p. 15): with a public signal, seen by all customers, the firm earns no more than with prices alone. Theorem 2 (p. 17): with personalized signals, which may depend on each customer's valuation and be randomized independently across customers, a simple Buy/Wait/No mechanism is optimal and strictly beats every public mechanism when the low inventory level is small. Personalized recommendations are the kind of information online retailers and travel platforms send (low-stock alerts, buy-now prompts).
There is a unit mass of customers with valuations distributed on with density and complementary distribution ; the hazard rate is non-decreasing. The firm's inventory is high, (enough for everyone), with probability , and low, , with probability . The monopoly price is , and is the valuation at which a mass of customers lies above.
A straightforward mechanism fixes prices and, after seeing , draws a latent index from a finite set with a state-dependent law; given , each -customer is independently told Buy (in period 1), Wait (buy in period 2) or No. A customer who requests the product in a period with units left and demand of mass from the others gets it with probability : if , if , otherwise (random rationing). The mechanism is obedient if every customer (for almost every ) weakly prefers to follow her recommendation, given the availabilities she can expect conditional on it: (Buy-1)–(No), p. 40. The firm's revenue is the expected value of rationed sales . A mechanism is public when the recommendations depend only on and obedience holds for each realized .
The personalized mechanism (PS1)–(PS2), p. 17, sets . In state it tells customers with to buy and the rest No; in state it tells to buy with probability
and to wait otherwise, tells to wait, and No. The price solves (14) with (15).
If , then (14) has a root , and for every such root the mechanism (PS2) is obedient, its revenue is at least that of every obedient mechanism at any prices, and
The result says that the value of information in this market lies entirely in its personalization: public information is worthless (Theorem 1), and private recommendations strictly raise revenue whenever low inventory is scarce relative to the monopoly market. The optimal mechanism is explicit and has a simple form, with the low-type firm selling out exactly in period 1 and the high-type firm mimicking it as far as incentive compatibility allows; in the paper's uniform example () revenue rises from to . The proof technique, a relaxation to a linear program over signal profiles followed by a dual reduction to a single threshold, is a template for many-receiver persuasion problems with congestion.
The theorems are proved in the paper; none of them has a machine-checked proof. The mission produces a formal model of strategic customers under rationing and personalized signaling, and the formal versions of the five steps. Two printed steps need correction to be true and are stated in corrected form (Lemma 4's tie case, the location of the root of (14)); formal proofs settle that the corrections suffice.
The obvious argument is a pointwise one: for each valuation, the Buy incentive constraint caps the high-state Buy probability given the low-state one, so set every cap tight. It fails because the availabilities in the constraints depend on the aggregate masses that the recommendations themselves create, so the constraints for different valuations are coupled; the paper resorts to an infinite-dimensional linear program and asserts strong duality without proof (p. 41). Lemma 4 is the algebraically heavy step (pp. 46–50): an envelope argument over the threshold combined with the hazard-rate monotonicity. Theorem 2 then needs a one-dimensional optimization in , the existence of a root of (14) (a fixed-point equation, since depends on ), and the case , which the paper never treats.
The paper's game (Definitions 1–2: a continuum of customers, Bayesian Nash equilibrium, sender-preferred selection) is re-expressed as the class its proofs reduce to by the revelation principle (p. 39, footnote 5): obedient straightforward mechanisms with aggregate masses. Revenue optimality over this class is what Theorem 2 asserts after that reduction. The latent index is finite (Fin n, for every n); it carries the correlation between customers' signals that public signals need. Obedience is required for almost every valuation, as in Definition 1.
Committed conventions: , , continuous on and positive on ; , ; and customer mass . Availability is avail above; at zero demand it is with stock left and without. (14) is written . In (PS2)(a) "" is taken as (a null set). (B) is read with . The program (A.16) keeps the no-Buy mechanism (), which the printed version drops. "The optimal mechanism" is stated as "an optimal mechanism" (ties exist). Lemmas 3–4 take , implicit in the paper's divisions; the goal ranges over all prices , including (p. 8). Milestone (16) is stated at the prices of (PS1): and a root of (14).
Trivializing formalizations are ruled out: revenue counts rationed sales, not ; obedience is the printed conditional constraint multiplied by the probability of the recommendation, never divided by a possibly zero probability; availability never uses Lean's ; the goal carries the existence of a root of (14), so "for every root" is not vacuous; the mechanism class contains public and correlated mechanisms; and is the revenue of the mechanism (PS2), tied to the formula (16) by a milestone.
A complete development needs: the density measure on and its tail function , monotonicity and continuity of and its inverse, the quasi-concavity of under a non-decreasing hazard rate, and bounds for the rationing function. The hazard-rate and lemmas are reusable for other pricing models. Contributions of helper lemmas, of a primal proof of Lemma 3 avoiding the duality argument, and of the case are welcome.
The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-32 mission already covers every , the new work is the range from 16 to 32.
The cutoff came down from 256 to 32 across eleven missions. The first phase (256 to 62) used a confinement estimate, exhausted at . The second phase (62 to 32) used a new technique that broke through the confinement barrier. Whether it extends to 16 is not known; 16 asks for sixteen more units below the current best.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. The campaign conjectures the formula for all . Any proof for a cutoff of 16 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh's Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryDigital services are paid for with attention: an ad-financed platform earns more the longer its users stay. Policy reports on digital markets (Crémer, de Montjoye and Schweitzer, 2019; the U.K. Digital Competition Expert Panel, 2019; Scott Morton et al., 2019) worry that such firms degrade their services with features that capture attention at the user's expense, and they usually recommend more competition. Ichihashi and Kim, Addictive Platforms (Bank of Canada Staff Working Paper 2022-16; Management Science, 2023), ask whether competition actually helps. Their answer depends on how scarce attention is. When attention is scarce, platforms compete by making their services more addictive rather than better, and a monopoly serves the consumer better than a duopoly. This mission formalizes that comparison, the paper's headline result, together with the two equilibrium characterizations it rests on.
There are platforms and a single consumer. Each platform chooses an addictiveness . The consumer observes , joins a set of platforms and allocates attention to each . She receives if , and otherwise
subject to the attention cap , where . Platform earns the attention if the consumer joins it and otherwise.
The service utility is twice differentiable, strictly increasing and concave in attention , and strictly decreasing in . The marginal utility is strictly increasing in , so a more addictive service is worse to join but harder to stop using. There is some at which no amount of attention makes the service worth joining, and . The attention cost is strictly increasing, convex and twice differentiable, with . These are Assumptions 1 and 2 of the paper.
Platforms choose addictiveness simultaneously, and then the consumer chooses and . The solution concept is pure-strategy subgame perfect equilibrium: the consumer chooses optimally at every profile , and no platform gains by changing its own . A monopolist () breaks ties in the consumer's favour. Consumer surplus is the consumer's payoff in the equilibrium outcome.
The monopoly benchmark uses three quantities. The first is , the consumer's attention on one platform when there is no cap. The second is , the lowest addictiveness at which she exhausts her attention. The third is , the addictiveness at which her best capped payoff from one platform falls to zero. Under competition, is the total attention she spends on platforms of common addictiveness .
Let be the least cap from which on monopoly consumer surplus is zero. For every monopoly equilibrium with addictiveness and every duopoly equilibrium with :
The proposition is silent about intermediate caps, and so is the goal.
Proposition 3 separates two effects of competition. Business stealing pushes duopolists to raise addictiveness, because a more addictive service captures a larger share of a fixed attention budget. Competition for participation restrains them, because a consumer can drop a platform and spend her time on its rival. When attention is scarce the first effect dominates and the consumer is strictly worse off under duopoly. When it is abundant the monopolist extracts the whole surplus and duopoly cannot be worse. The result is the basis of the paper's policy discussion: digital curfews and the comparison between the equilibrium and the joint-profit outcome (Propositions 4 and 6). Propositions 1 and 2 are used throughout the paper.
The paper proves these results on paper. No machine-checked proof exists. A formal proof would check several delicate points. One is the role of the monopolist's tie-break, without which every is a monopoly equilibrium when attention is scarce. Another is that the uniqueness argument for the duopoly needs a consumer who best-responds off the equilibrium path. The appendix also asserts a few claims without argument or slightly too strongly, recorded below. Verifying them is part of the work.
The obvious argument for Proposition 3 compares equilibrium payoffs through the closed forms of Figure 3, and closed forms do not exist in general. Every object is defined by an optimization problem whose maximizer has no formula. The value functions are concave but need not be differentiable, so the envelope-theorem steps of Appendix B cannot be applied as written; they have to be replaced by monotone comparative statics or one-sided derivatives. Proposition 2's uniqueness is the hardest part. It rules out asymmetric equilibria by a deviation argument that controls which platforms the consumer joins after a small change in one platform's addictiveness (Lemma B.4). It also needs the consumer's whole strategy, not only her choice on the path.
Platforms are Fin K; the paper's platform 1 is the index 0. Addictiveness and attention are real numbers restricted to , and only the values of and there matter. The cap is an extended nonnegative real (ℝ≥0∞), so is a genuine case and "" includes it. Derivatives on are one-sided at .
The definition file states the paper's Assumptions 1–2 as printed and adds disclosed pins:
"Increasing" and "decreasing" are weak unless the page says "strictly". The one exception is "higher addictiveness" in the first half of Proposition 3, which is stated strictly because the proof gives .
Three statements differ from the printed text. Lemma B.2's " is strictly concave" is false on the paper's own Figure 3 instance and is stated as concavity. The strict clause of Lemma B.4 fails when is linear and is not posed. The derivative claims of Lemmas B.2–B.4 are stated as decreasing differences of value functions.
Several trivializing formalizations are excluded:
Not posed: Proposition 4 and later results, and the side models of Remarks 2–3. A complete development needs maximizers of concave problems on intervals and simplices, monotone comparative statics (Topkis, Milgrom–Shannon), and envelope arguments for concave value functions. These pieces are reusable well beyond this paper, and contributions of them as separate lemmas are welcome.
A portfolio chosen from historical returns can look attractive in the data used to construct it and deliver a different result when evaluated under the population return distribution. The gap is driven by estimation error in both the mean return and covariance matrix. A mean of future utility values describes average performance, but it does not describe how much that utility varies across possible estimation samples. Lassance, Martín-Utrera and Simaan study this variation for a portfolio that blends an estimated mean-variance choice with an estimated global-minimum-variance choice. Their closed-form variance makes the sampling risk of that blend an explicit function of market and sample parameters. The source for this mission is the authors’ SSRN manuscript, version dated August 18, 2023, including its Internet Appendix; appendix pages are cited as IA pages.
There are risky stocks. Their excess-return vector has population mean and positive-definite population covariance . The investor has risk aversion . A portfolio is a vector of weights whose entries sum to one. Its population mean-variance utility is
Write for the vector of ones. The global-minimum-variance portfolio and its variance are and . Its mean is . The population matrix maps the mean vector to a zero-cost portfolio. The variance of that portfolio is . These quantities are computed from and ; they are not independent inputs. These definitions are equations (3)–(7) of the manuscript.
The investor observes independent return vectors , each with multivariate Gaussian law . The sample mean is , and the sample covariance is . Replacing the population parameters in and by these estimates gives the sample GMV portfolio and the sample zero-cost portfolio . The estimated mean-variance portfolio is . At shrinkage intensity , the portfolio under study is . Its out-of-sample utility, , is evaluated using population and . It is random because the weights depend on the sample. These choices are fixed by equations (9)–(12) and Assumption 2 of the manuscript.
The goal is Proposition 1, equations (13)–(19). Under and , it asserts that the utility has a finite second moment and that
The coefficients and are the exact rational expressions in on pp. 14–15 of the manuscript. In particular, the result covers every , including the sample GMV portfolio at and the sample mean-variance portfolio at .
The milestones follow the quantities named in the authors’ proof, Section IA.10. Equation (IA43) gives the covariance matrix of the random weights, and (IA44) gives the variance of their population mean return. The jointly distributed mean-return and return-variance pair in (IA45)–(IA48) supplies the setting for two auxiliary moment identities, (IA53) and (IA57). Equations (IA49), (IA59), and (IA60) give the first and second moments needed for return variance and mean return; (IA68) gives their covariance. All are statements from the Internet Appendix, pp. IA35–IA39.
The expression tells an investor how the sampling risk of utility changes with the shrinkage intensity, sample size, stock count, risk aversion, and the two population variance parameters. The later comparison of variance-minimizing, mean-maximizing, and robustness-maximizing intensities uses this formula. Without Proposition 1, those comparisons have no explicit OOSU risk function to analyze. The result is already proved in the paper; this mission asks for its Lean proof and for reusable formal statements of the associated Gaussian portfolio and moment identities. No machine-checked proof of this paper’s proposition is included in the draft.
The sample covariance is random and its inverse appears in the estimated weights. Taking the variance of utility therefore involves inverse-covariance terms and moments beyond those needed for expected utility. The requirement is tied to existence of the fourth negative moment of a chi-squared variable in (IA57). A direct calculation that replaces random weights by their population counterparts loses the dependence on the estimation sample. A calculation from separate marginal laws also does not determine the covariance between mean return and return variance; the representation in (IA47)–(IA48) describes them jointly.
The Lean market uses vectors Fin N → ℝ, matrices indexed by Fin N, and returns in EuclideanSpace ℝ (Fin N) to use Mathlib’s multivariate Gaussian law. The sample has Fin T observations on a probability space. Its covariance divisor is exactly , as in (9). The standing assumptions are , , , , and independent, identically distributed Gaussian returns. Every theorem about a variance or covariance explicitly asserts finite second moments; expectation statements explicitly assert integrability. The source’s finite-variance convention is thereby represented without Lean’s default value for a nonintegrable variance.
The left side of the goal is the probability-theory variance of utility under the sampling law. It is not defined by the closed formula. Likewise , , and are computed from the market; independence is part of the sampling hypothesis. In the auxiliary representation, the chi-squared law is the squared norm of independent standard normals. The zero-degree cases and footnote 6’s rules are encoded explicitly. Mathlib’s matrix inverse and real division are total operations; their values on singular sample covariances or zero denominators do not alter the distributions because those events have probability zero under the stated assumptions. Contributions establishing the sample-covariance distribution, the joint representation, the negative moments, and the final variance identity are within scope and can support other Gaussian portfolio results.
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.
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.
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.
Many problems in signal processing, statistics and engineering design have the form of a nonconvex, possibly nonsmooth objective subject to nonlinear equality constraints. Zhu, Zhao and Zhang (arXiv:2007.12219v1, 2020; published in Mathematics of Operations Research, 2024) propose NAPP-AL, a first-order primal-dual method that takes one linearized step on the augmented Lagrangian per iteration. Their analysis has three layers: subsequential convergence with an stationarity rate (§4), linear convergence under a new value proximity error bound (VP-EB, §5), and sufficient conditions for VP-EB (§6).
This mission formalizes the second sufficient condition: metric subregularity of the stationarity map, together with a local value condition on nearby stationary points, implies VP-EB. Metric subregularity is a standard regularity notion of variational analysis (Dontchev–Rockafellar), and error bounds of this kind are the classical route to linear convergence (Luo–Tseng). The paper attributes the cost-to-go inequality it relies on to Tseng and Yun [18]. A companion mission treats the KL-property route (Proposition 6.1); a third proves linear convergence from VP-EB (Theorem 5.1).
Write with the Euclidean norm of the stacked vector, , and the open ball. The problem (P) is
with smooth with Lipschitz gradients, lower semicontinuous and locally Lipschitz near , closed and convex, Lipschitz, each component of with Lipschitz gradient, and an matrix of full column rank with ; is bounded below and coercive on the feasible set (Assumption 1).
The augmented Lagrangian is . The set is the KKT display of p. 6: with , it collects the triples
with the limiting subdifferential and the normal cone. A point is stationary if ; is the set of stationary points. Distances follow the paper's convention: , and .
NAPP-AL keeps , takes as a global minimizer over of a linearized model with a Bregman term , as the minimizer of a strongly convex quadratic, and sets . The step lies in with given explicitly by (8), and (Assumption 2).
VP-EB at (Definition 5.1): there are such that whenever and .
Metric subregularity (Definition 6.2): is metrically subregular around if, for some , for all . Assumption 3 at a stationary : for some , for all with .
Let be generated by NAPP-AL in the standing setting and let be a cluster point. If Assumption 3 holds at with , and is metrically subregular around with and , , then
The constants are existential, as in Definition 5.1, so the statement survives any improvement of them.
The result. Combined with Theorem 5.1 of the paper, Proposition 6.2 gives finite length, convergence of the whole sequence, Q-linear convergence of the potential and R-linear convergence of the iterates whenever the stationarity map is metrically subregular at the limit and Assumption 3 holds there. Metric subregularity is known for broad classes, such as piecewise linear-quadratic problems and polyhedral multifunctions, so the proposition turns a structural property of the problem into a rate for this algorithm.
Formalizing it. The proposition is proved on paper; nothing about NAPP-AL has a machine-checked proof. The formalization makes two things exact that the paper leaves loose. First, the proposition’s proof needs a cost-to-go constant independent of the stationary point, and the proof of Lemma 6.1 supplies one even though the lemma’s printed statement fixes the point first. Second, the proposition's proof places the nearest stationary point in , while only follows from its steps; the existential conclusion leaves room to shrink the radius. A formal proof settles both, and the general facts it needs (metric subregularity in , closedness of limiting-subdifferential graphs) are reusable.
The obvious route is to combine subregularity with the residual bound of Theorem 4.1(iv), , which bounds the distance from to by the step. The difficulty is transferring a distance bound into a value bound of second order: local Lipschitz continuity of would bound only by a multiple of , which is first order in the step, while VP-EB asks for the square; and is nonsmooth and nonconvex, so no Taylor expansion at the stationary point is available. Moreover, the stationary point closest to changes with . The proposition’s proof needs a cost-to-go inequality with a constant uniform over stationary points, which in turn rests on the boundedness of the iterates and on the lower bound for coming from (8). The radius bookkeeping between the subregularity ball, Assumption 3's radius and the VP-EB ball is a second, smaller obstacle.
is EuclideanSpace ℝ (Fin k) and points are triples E n × E d × E m; every norm and ball uses the stacked Euclidean norm tnorm, never Lean's product (sup) norm. is a continuous linear map with its operator norm (the spectral norm), never a Matrix with the entrywise norm; is the Rayleigh minimum over the unit sphere. Distances and are infima in , equal to on the empty set; Metric.infDist, which returns on and would make subregularity and the residual bounds trivial, is not used. The normal cone is empty for , so a nonempty normal cone off cannot manufacture stationary points. (H3)'s local Lipschitz continuity is read on neighbourhoods in of points of , not Mathlib's relative LocallyLipschitzOn.
Disclosed readings of the arXiv v1 text: are real-valued with globally Lipschitz gradients; ; NAPP-AL is a relation on given sequences (any global minimizer may be selected; existence is not asserted); VP-EB is the inequality alone, without Definition 5.1's presupposition that the sequence converges to ; "generated by NAPP-AL" in Lemma 6.1 and Proposition 6.2 carries the standing setting of Theorem 4.1 (Assumptions 1–2 and rule (8)); Lemma 6.1 follows the printed quantifier order; its proof supplies the uniform constant needed by Proposition 6.2. The radius of Assumption 3 is δ3 in Lean, distinct from the step sequence .
Welcome contributions: a proof of Lemma 6.1 from the optimality of (5)–(6), Lipschitz estimates and the bounds of Theorem 4.1(ii); the boundedness and residual results of Theorem 4.1 (formalized in the companion mission on the rate); closedness of ; and the radius argument of Proposition 6.2. The source is arXiv:2007.12219v1; numbering and constants of the published version are not used.
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.
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 sells billions of impressions a day through auctions, and most advertisers do not bid by hand: they hand a budget to the platform, which paces their bids so that spending over a campaign matches the budget. Over the last decade the major ad exchanges moved from second price to first price auctions. An advertiser who has tuned a pacing policy for one format wants to know whether it still works after the switch, and a platform wants to know whether its revenue changes.
Classical revenue equivalence (Myerson 1981; Riley and Samuelson 1981) says that, with independent private values, risk-neutral buyers and no budgets, every standard auction yields the same expected revenue. Che and Gale (1998) showed that this fails when budgets are hard: first price auctions then raise more revenue than second price auctions. Balseiro, Kroer and Kumar (2023) study budgets that bind in expectation over many auctions, with values driven by item features, and show that equivalence is restored. This mission formalizes that result, their Theorem 2.
An item has a context drawn from a law with a density. Each of buyers has a type drawn independently from a law with a density on . Here are feature weights and is a budget. The buyer's value for the item is , and is the supremum of all values. The seller discloses , then runs an auction with reserve price . A buyer must keep its expected payment, over contexts and competitors' types, at most .
A pacing function shades every value to the paced value . Let be the law of the paced value when , and the c.d.f. of the highest of independent paced values. In first price auctions the paper's candidate strategy is , where is the first-price equilibrium bid against paced competitors.
The buyer's dual function is the supremum over bid functions of the Lagrangian , with competitors bidding . The set collects pacing functions with values in and total variation at most . The correspondence is the set of minimizers over of . A fixed point is an equilibrium pacing function for first price auctions.
An anonymous standard auction gives the item to the highest bid at or above the reserve. Its payment for a bid against competing bids does not depend on the buyers' identities. An oracle returns, for each atomless value law on , a single-auction equilibrium bid that is nondecreasing, meets the reserve exactly for values above it, gives a zero-value bidder zero payoff, and has an atomless bid law. The candidate strategy is
For every family of anonymous standard auctions with such an oracle and every with :
Theorem 2 says that pacing is portable: an equilibrium pacing function computed for first price auctions is an equilibrium pacing function for second price auctions, all-pay auctions, or any context-dependent mixture of standard formats. Each buyer's expected spend is the same in all of them, so the seller's expected revenue is too. This explains why budget-management systems built for second price auctions keep working after a move to first price. It also separates in-expectation budgets, where equivalence holds, from the hard budgets of Che and Gale, where it fails. Theorem 3 of the same paper, a liquid-welfare price of anarchy of , uses Theorem 2 to argue in the second price auction.
The paper's proofs are in its online appendix, which is not part of the source this mission cites. To our knowledge no part of the argument has been machine-checked. Classical revenue equivalence for incentive-compatible direct mechanisms without budgets exists on the platform as other items, but none has pacing, budgets or contexts. The mission asks for a machine-checked proof of Theorem 2 and of the two steps the authors name.
The classical argument pins payments by the allocation rule and the envelope formula, value by value. Here a buyer's decision is a whole bid function of the context, coupled across contexts by one budget constraint, and the budget-constrained problem is not convex. So the envelope argument cannot be applied to the constrained problem directly. The obvious move, Lagrangian relaxation, needs strong duality for a non-convex problem, and it needs the dual of each standard auction to agree with the first-price dual for every multiplier, not only at the optimum. The paced value laws need not have densities, so the textbook single-auction results, which assume a positive density, do not apply verbatim. Finally, the fixed-point hypothesis ties all buyer types together, and optimality must be recovered almost surely in the type.
Everything is defined in the namespace ContextualAuctions.RevEquiv. Contexts are Fin d → ℝ, types are (Fin d → ℝ) × ℝ, and is an explicit sum. The joint law of the context and the competitor types is F.prod (Measure.pi fun _ => G). Ties win, as in the paper's tie-breaking rule. The standing assumptions are , and probability measures with densities concentrated on and , in the open positive orthant, and measurable. Disclosed additions, implicit in the paper:
The dual function is the supremum over admissible bids, which are measurable with integrable payment. Its closed form is a milestone and never its definition. Total variation (Definition 3) is extended-real valued and uses the Euclidean norm of the test field. In oracle property 1, expected payments are taken in , so a bid with infinite expected payment can never look free. The payment identity of Theorem 2 is stated in , so it also asserts that the left side is finite. This rules out the trivializing readings: a closed-form definition of that makes the first milestone hold by definition, Bochner junk zeros for non-integrable payments, and a vacuous variation bound.
A complete development needs single-auction revenue equivalence for i.i.d. atomless value laws without densities. It also needs the measure-theoretic interchange of a supremum over bid functions with the expectation over contexts, and strong duality for the budget-constrained problem. These pieces, notably the single-auction equivalence for general atomless laws, are reusable beyond this mission. Contributions toward any of them are welcome.