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?
Round-Robin is the simplest allocation rule for indivisible goods: agents take turns, in a fixed order, picking their favourite remaining good. When agents have additive valuations and report them truthfully, the outcome is envy-free up to one good (EF1) — every agent values its own bundle at least as much as any other bundle with one good removed, a notion going back to Lipton et al., 2004 and Budish (2011) — which makes Round-Robin a standard baseline in fair division (Markakis, 2017). The mechanism, however, only sees reported rankings, and agents can gain by misreporting; without monetary transfers no truthful mechanism has a meaningful fairness guarantee even for two additive agents. Amanatidis, Birmpas, Lazos, Leonardi and Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research, 2025) therefore study equilibrium fairness of Round-Robin when valuations go beyond additive. This mission concerns their fairness result for submodular valuations: strategic play does not destroy fairness, it only degrades it by a constant factor.
Timeline. Aziz, Goldberg and Walsh (ADT 2017) proved that Round-Robin always has a pure Nash equilibrium for additive valuations. Amanatidis et al. (WINE 2021) initiated the study of equilibrium fairness and showed that, for additive valuations, Round-Robin has equilibria and each of them yields an EF1 allocation with respect to the true valuations. The 2023 paper extends equilibrium existence to cancelable valuations (exact PNE) and submodular valuations (1/2-approximate PNE, with 1/2 tight), and proves that approximate equilibria are approximately EF1: factor for submodular and for subadditive cancelable valuations.
There are agents and a set of goods. Agent has a valuation that is normalized () and non-decreasing. The marginal value of a good with respect to a set is , and is submodular if whenever and .
Each agent reports a ranking , a total order on . Round-Robin runs steps; in step (counted from ) agent receives its -top good among those still unallocated. The result is an allocation . An allocation is -EF1 if for all agents with some satisfies . A profile is an -approximate pure Nash equilibrium (PNE) if no agent can, by reporting any other ranking , obtain a bundle worth more than times its current one:
In Lean the objects are marginal, IsValuation, IsSubmodular, IsRanking, roundRobin, IsApproxEF1 and IsApproxPNE in RoundRobinEq.SubmodularEF1.Setting; the step-to-agent map agentAt n t = t % n comes from the shared module RoundRobinEq.CancelableBluff.Setting.
For and submodular valuations, every -approximate PNE of Round-Robin yields an allocation that is -EF1 with respect to the true valuations:
Companions (not milestones): Lemma 4.1 (the greedy response is 1/2-EF1 from the deviator's perspective) and Theorem 4.2 (two agents: ).
The theorem says that fairness of Round-Robin is robust to strategic misreporting for a class far beyond additive valuations: whatever approximate equilibrium agents settle in, each agent's envy up to one good is bounded by . Combined with the existence of a 1/2-approximate PNE (Theorem 3.7 of the same paper), it gives an equilibrium that is 1/6-EF1. Lemmas 4.6 and 4.7 are statements about two runs of Round-Robin that differ in one agent's report; they involve no valuations and are reused verbatim for subadditive cancelable valuations (Theorem 4.5).
The result is proved in the paper; nothing in it is formalized anywhere to our knowledge. The mission builds a finite fair-division layer (Round-Robin as a step-by-step process, rankings, α-EF1, approximate PNE) that does not exist in Mathlib, and checks the combinatorial coupling of two runs, which is where the paper's argument carries its weight.
The obvious argument compares agent 's equilibrium bundle with its bundle after a good deviation (Algorithm 4's greedy response) and then compares that with agent 's bundle. With two agents everything not in or goes to , and this closes the argument. With agents the deviation reshuffles goods among all other agents, and there is no direct control on what ends up holding relative to the deviation run. The proof needs a global statement (Lemma 4.6) about how much two Round-Robin runs that differ in one report can diverge before each of 's turns, and then a careful indexing of by allocation time in the other run, so that a counting bound turns into the good-by-good inequality (2). The bookkeeping of steps, rounds and two simultaneous runs is the main work.
Fin n with , 0-based; goods a finite type M. The paper's standing simplification (p. 7) is a hypothesis Fintype.card M = k * n of every theorem; the paper's reduction to this case (dummy goods) is not formalized.allocBefore σ (r*n + i), and the paper's bounds for , , appear as for .Trivializing formalizations are excluded: deviations over arbitrary lists (which would strengthen the hypothesis), , EF1 computed on reported rankings instead of the true valuations, or the EF1 witness fixed in the goal statement would each change the theorem, and none is used.
Contributions welcome: proofs of Lemma 4.6 by induction on rounds (the reusable core), basic API for allocBefore/roundRobin (every good is allocated once, ), and Theorem 2.1.
Service providers such as hospitals or retail stores each fit a predictive model on their own data, and many of them have few observations. The models of different providers are usually similar but not identical: most coefficients agree, while each provider deviates from the common model in a few features of its own. Multitask learning asks how data from all providers can be pooled to estimate every provider's model better than it could estimate alone, without being misled by the providers that differ.
Xu and Bastani (arXiv:2112.14233v5) model this with sparse heterogeneity: every task parameter is a shared vector plus a sparse deviation. They propose the robust multitask estimator (RMEstimator), which combines per-task least-squares estimates by a coordinatewise trimmed mean and then corrects each task by a LASSO regression centred at that shared estimate. Their main fixed-design guarantee, Proposition 5, is a high-probability bound on the estimation error of each task. The same estimator drives the paper's multitask contextual bandit algorithm (§5), whose regret analysis rests on this bound. The approach builds on transfer learning with a single proxy model (Bastani 2021) and on the robustness of the trimmed mean to corrupted samples (Lugosi and Mendelson 2021).
There are tasks. Task has observations, a fixed design matrix whose columns satisfy the normalization (equation (1)), and responses
The noise terms are mutually independent across all tasks and observations, and each is -subgaussian with mean zero: for all . Assumption 1 asks that the sample covariance matrices satisfy .
Given a trimming level and regularization levels , Algorithm 1 computes:
A coordinate is -poorly-aligned, , if fewer than a fraction of the tasks satisfy ; otherwise it is -well-aligned (Definition 2).
For every constant , every , every , every task and every , every output of Algorithm 1 with satisfies
with probability at least .
The printed Proposition 5 (p. 17) has where this statement has . The proof on pp. 41–43 ends with and combines it with (16), whose coefficient is , so it establishes the bound with . The goal is the bound the proof supports.
Proposition 5 separates two error sources: a LASSO term of order , which depends only on the task's own sample size, and a trimmed-mean term that shrinks with the number of tasks through . With the hyperparameters of Appendix A.2 it yields Theorem 1, an error of order up to logarithmic factors, against for a single task alone. The same decomposition underlies the paper's data-poor guarantee (Proposition 8) and the regret bounds of its multitask bandit algorithm.
The result is proved on paper; none of it has been machine-checked. A formal development checks the constant bookkeeping, including the factor 4 that the printed statement omits, and the use of the trimmed mean for samples that are independent but not identically distributed, which is where this paper departs from the classical i.i.d. robust-statistics results. Proposition 4 and Lemma 1 are reusable on their own: a corruption-robust concentration bound for the trimmed mean and a noise bound for fixed-design LASSO.
The obvious estimator of the shared parameter, the average of the per-task estimates, converges to the average of the , which differs from in up to coordinates, so the LASSO correction would have to undo a dense bias. The trimmed mean avoids this only on poorly-aligned coordinates, and only with high probability. The proof of Proposition 4 must control the samples that survive trimming even though they are not identically distributed and trimming biases the conditional means; that step needs a moment bound for subgaussian variables and a Hoeffding argument on a random index set. The LASSO step needs the cone inequality with a support that is not the support of , and the counting bound (6) to control its size.
Fin N, Fin d, Fin (n j); paper index is Lean i − 1. Designs are deterministic matrices; only the noise is random.HasSubgaussianMGF with variance proxy , . Independence of all noise terms is iIndepFun over the pairs .A formalization that drops Assumption 1 (making the OLS inverse a junk zero), lets the corrupted samples of Proposition 4 be independent or well-behaved, fixes a single existentially, or reads a junk minimizer from Classical.choose, does not state the paper's result.
The development needs least-squares algebra for fixed designs, a Hoeffding bound for independent bounded variables, moment bounds for subgaussian variables, and the LASSO basic inequality. Proofs of any milestone are welcome, and so are alternative arguments for Proposition 4 with better constants.
Firms that hold purchase-history data can treat past customers and a rival's customers differently. The economics of behavior-based pricing (BBP), charging different prices to the two groups, is well developed: in a symmetric duopoly, poaching the rival's customers with discounts intensifies competition and usually lowers profits (Fudenberg and Tirole 2000; Villas-Boas 1999). The same data can also target information. A firm launching a new product of uncertain quality can disclose that quality (free samples, demonstrations, trials) at a cost per customer reached, and it may disclose to one segment and not the other. This is behavior-based quality disclosure (BBD).
Zhang and Li (Management Science 71(10), 2025) combine costly voluntary disclosure in the style of Jovanovic (1982) with BBP in a two-period Hotelling duopoly. Their Proposition 1 answers two questions about the second period: to which segment should a firm disclose more readily, and does the option to target disclosure help or hurt profits? This mission formalizes that proposition and the displayed formulas from which it is derived.
Two firms, A at and B at , face a unit mass of consumers spread uniformly over , with unit transportation cost and a base value high enough that every consumer buys in every period. The first-period purchase splits the line at a share : A's turf consists of A's old customers, B's turf of B's.
In period 2 firm launches a product of quality ; and are independent and uniform on , and consumers do not observe them. Disclosing to the consumers in an interval of length costs , where is the unit disclosure cost. A firm discloses to a segment exactly when its quality exceeds a disclosure threshold ; consumers who see no disclosure infer and hold the belief . The updated belief is therefore if and otherwise.
In both regimes firms then set four prices: on A's turf and on B's turf. On A's turf, with beliefs , the consumers who stay with A are with , clamped to the turf; B's turf is symmetric. A second-period equilibrium is a profile of thresholds and turf price strategies such that, for every belief pair, the turf prices are a Nash equilibrium among nonnegative prices, and every threshold is a best response: disclosing is optimal above it and withholding below it. The ex ante second-period profit is A's expected revenue minus expected disclosure cost, over .
For , at the symmetric first-period share : equilibria exist under both regimes; in every BBD equilibrium
in every BBD equilibrium and for every realization , at the induced beliefs, each firm charges the rival's customers less than its own,
and for every BBD equilibrium and every uniform-disclosure equilibrium, each firm's ex ante second-period profit is strictly higher under BBD:
The goal asserts the shape of the result (an order of thresholds, of prices and of profits) and no closed form.
The result. Part (a) says that disclosure should be retention focused: a firm reveals quality to its own customers over a wider range of qualities than to the rival's. This is the opposite of the acquisition focus BBP prescribes for prices, so the two instruments built on the same data pull in different directions. Part (b) records that prices stay acquisition focused: the rival's customers get the lower price. Part (c) says that targeted disclosure raises second-period profits, in contrast with the classical finding that targeted pricing lowers them. Under uniform disclosure a single threshold over-discloses to the rival's customers and under-discloses to one's own; BBD separates the two, and the paper locates the gain in the expected disclosure cost in (5) against in (14).
Formalizing it. The paper's proofs are in an Online Appendix; the main text shows the displayed formulas only. A formal proof checks the whole chain from the clamped price games, through the best-response conditions, to the closed forms of Table 1 and the final comparison. The comparison in (c) is delicate: the profit difference is positive on all of but tends to as (about at ), so a numerical check does not settle it. The mission also gives the platform its first Hotelling duopoly, its first behavior-based pricing model and its first costly-disclosure model.
There are three nested equilibrium notions: Nash prices in each turf for every belief pair, best-response thresholds given those prices, and expectations of piecewise-defined profits over the belief support. Lemma 2's prices solve first-order conditions only in the interior; uniqueness among nonnegative prices requires ruling out the corners where one firm sells nothing on a turf. Each threshold is characterized by a best-response condition rather than an equation, so obtaining (4) or (13) requires showing that the disclosure gain is monotone in quality and crosses the cost exactly once inside . The expected profits integrate squares of linear functions of beliefs that switch at the thresholds. Finally, (c) is a sign statement about a difference of algebraic functions of with three different square roots that vanishes at ; plugging in endpoints or bounding term by term loses the sign near .
The Lean development lives in the namespace BBDisclosure.Stage2. Conventions:
A formalization in which thresholds or prices are pinned to their closed forms, or in which the equilibrium predicate is unsatisfiable, would make the goal trivial; the goal therefore quantifies over equilibria of the game itself and includes existence of an equilibrium in both regimes. "Firms'" is stated for both A and B rather than assumed by symmetry.
Needed infrastructure: piecewise-quadratic optimization on a half-line (the clamped turf games), interval integrals of piecewise polynomials, and sign analysis of algebraic expressions in , , . The turf-game analysis is reusable for any Hotelling model with behavior-based pricing. Contributions to any milestone, or to intermediate statements such as the conditional profits (3) and (12), are welcome.
In a Bayesian multi-armed bandit a decision maker pulls one of arms in each of periods, observes the reward, and updates a prior belief about each arm's unknown parameter. The best achievable expected total reward, , is the value of a dynamic program over beliefs, and for all but the smallest instances it cannot be computed. Upper bounds on are therefore the yardsticks against which heuristics such as Thompson sampling (TS) are measured: the gap between a policy's performance and an upper bound certifies how far the policy can be from optimal.
The conventional benchmark is the expected total reward of a clairvoyant who knows the arms' parameters, , the quantity behind every Bayesian regret bound. Min, Maglaras and Moallemi (arXiv:1902.04251v2, Management Science 2025) apply the information relaxation duality of Brown, Smith and Sun (Operations Research 2010) to the bandit: a clairvoyant who sees the whole future but pays a penalty for using it. Each penalty yields a performance bound and a randomized policy (IRS, "information relaxation sampling"); the zero-information penalty recovers TS and , the ideal penalty recovers . The paper's Theorem 2 shows that its intermediate penalties give bounds that are provably tighter than . This mission formalizes that theorem.
Let , . Arm has an unknown parameter ; given , its rewards are i.i.d. with law . The parameter has a prior from a conjugate family indexed by a belief , and the Bayesian update is the belief after a reward : if then . The outcome has law , under which arms are independent. Throughout, for every belief.
The conditional and predictive mean rewards are and , and the posterior predictive mean after rewards of arm is . With and , the four bounds compared are
In the last one the clairvoyant chooses a whole action sequence knowing , and at time receives the conditional expected reward under the current belief , minus , plus the expectation of given the history . A supersolution is a function with and for all , , (Definition 2).
for every horizon and every belief vector of every conjugate model satisfying the standing assumptions.
The result. Theorem 2 says that the penalties IRS.FH and IRS.V-Zero, which only require sampling a future and solving a deterministic allocation problem, produce upper bounds on that are never looser than the regret benchmark , and that IRS.V-EMax is too. A bound below gives a sharper certificate of suboptimality for any policy, and the paper's experiments (§5) report these bounds next to the policies' performance. The ordering also organises the paper's family of policies: the bounds move monotonically from the TS benchmark towards the optimal value.
Formalizing it. The theorem is proved in the paper (Appendix D.3); it has no machine-checked proof. A formal development checks three different mechanisms: conditional Jensen for (124); a one-arm-at-a-time interpolation through , driven by a non-standard Jensen-type inequality (Lemma 1, Corollaries 1–2), for (57); and the supersolution argument of Desai et al. for (58). The paper's own remark (pp. 59–60) shows that the middle inequality does not follow from the general "finer information gives a weaker bound" principle of Brown et al.; formalization fixes exactly which properties of the bandit (conjugacy, independence of arms, the martingale property of ) carry the argument.
The obvious route to is to observe that IRS.FH conditions on more information ( rewards of every arm) than IRS.V-Zero (only the history so far) and invoke monotonicity of dual bounds in the relaxation. That argument fails: the two penalties are not generated by a common function, and the paper exhibits a modified bandit (163)–(165) in which the inequality reverses. The interpolation must instead trade one arm's realized cumulative payoff for a constant per-pull payoff one pull at a time, and each step needs Corollary 2, where conditioning acts inside a maximum of affine functions; ordinary Jensen points the wrong way there.
For (58), the difficulty is that the payoff of the penalised inner problem depends on the whole outcome along an adaptively chosen action sequence; the bound must hold uniformly over all sequences, which is why it is proved pathwise by backward induction rather than in expectation.
Arms are Fin K (0-based) with [NeZero K]. All arms share one parameter type (standard Borel, nonempty) and one belief type , the disjoint unions of the per-arm ones. Rewards are a Kernel Θ ℝ per arm, priors a Kernel Y Θ per arm, both Markov. The outcome is Fin K → Θ × (ℕ → ℝ) with law the product over arms of followed by an i.i.d. reward sequence. The standing assumptions are one predicate: conjugacy (the update agrees a.e. with Mathlib's posterior of the reward kernel), joint measurability of each , and for every belief, (3). is the conjugate (pathwise) version of the conditional expectation (10). is defined by its closed form (33). In the penalties (26) and (168) the conditional expectations given are replaced by their conjugate closed forms: , and the expectation of is the integral over the predictive law of the next reward. The supersolution predicate requires the expectation in (166) to exist. Lemma 1 and Corollary 1 compare lower Lebesgue integrals in ; Corollary 1 adds joint measurability of ; Corollary 2 assumes the integrable; Lemma 2's integral form assumes the pathwise maximum integrable.
Trivializations ruled out. No expectation in a goal can silently be a junk : the standing integrability makes every bound an honest integral, and Lemma 1 and Corollary 1 are stated with lower integrals. is the penalised clairvoyant value of the penalty generated by , not itself or the closed form (41) substituted into it. The standing assumptions are satisfiable (a sorry-free check with a one-point parameter space is in the development).
A complete development needs: conjugate updating along reward sequences and the martingale property of (Remark 1); measurability of ; independence of arms under ; conditional Jensen for finite maxima. Lemma 1, Corollaries 1–2 and Lemma 2 are reusable beyond this mission. Contributions of any milestone, or of the infrastructure lemmas above, are welcome.
Many operational risk questions ask for a small probability : the chance that the cost of a decision, evaluated at a random scenario , exceeds a large threshold . Examples are large delays in project networks or vehicle routing, large portfolio credit losses, and failures in engineered systems. Plain Monte Carlo needs on the order of samples to estimate to fixed relative accuracy, which is prohibitive when is or smaller. Importance sampling (IS) draws samples from a different distribution and reweights them by a likelihood ratio, but classical efficient IS schemes are built for one model at a time: they need the distribution of and the structure of (e.g. linearity or convexity) to solve for a good sampling distribution.
Deo and Murthy (arXiv:2102.07060v3, published in Operations Research, 2025) propose a self-structuring sampler that needs neither: it applies a fixed multiplicative stretching to ordinary samples of and uses only black-box evaluations of . Their main result is that this sampler is asymptotically optimal in the standard sense of logarithmic efficiency (Asmussen and Glynn 2007, Ch. 6) over a nonparametric class of light- and Weibull-type-tailed distributions and nonconvex losses.
Write and (componentwise), and . The random vector has density . Its marginal cumulative hazards are , , and is the standardized vector. Let be the left-continuous inverse, , and .
The standing assumptions are:
The sampler (Algorithm 1) fixes a hyper-parameter and maps a sample to , with either exponent
With the closed-form Jacobian of Table 1 and , the single-sample estimator is
Under Assumptions 2.1, 3.1, 3.2, 5.1, existence of , for some , and any slowly varying , for either exponent,
The goal fixes neither the exponent, nor the hyper-parameter , nor the loss or the distribution beyond the stated assumptions.
The milestones follow the paper's proof chain (Appendix A.3 for , Appendix E for ):
Theorem 4.1 gives the exponential decay rate of for a broad class of nonconvex losses (piecewise affine and quadratic functions, values of mixed integer programs, neural-network feature maps) under nonparametric, copula-style dependence. Previously such asymptotics were known only for specific losses and distribution families. Theorem 5.1 shows that one simple, model-oblivious transformation attains the best possible exponential rate for the second moment, so the relative error grows more slowly than any power . This supports using the sampler for value-at-risk, conditional value-at-risk and chance-constrained optimization.
The results are proved in the paper's appendices (Appendices A, D.1 and E). None of them has a machine-checked proof. Formalizing them would require regular variation and Potter bounds, a tail large deviations principle in , and a Varadhan-type integral lemma along a real speed. These are general tools that are missing from Mathlib and are reusable well beyond this paper.
The obvious argument is to bound by computing the likelihood ratio on the rare set. This fails because the rare set, after standardization, is described only asymptotically: converges to only continuously on , not uniformly. The exponent of the likelihood ratio involves the density of at two different scales ( and ) and the hazard rates at points pulled back by . A lower bound on it must hold uniformly enough to apply a Varadhan-type lemma with a varying family of functions, while the transformed sample stays inside a region where the asymptotic density assumptions apply. The upper and lower large-deviations bounds also rely on homogeneity of and , which hold only for the heaviest-tailed coordinates of .
Points of are Fin d → ℝ with the sup norm, and components are 0-based. is modelled by its law together with a density . is a lower Lebesgue integral and ; both are extended nonnegative reals, so neither nor is collapsed to a junk value. Logarithms of probabilities in large-deviations statements are taken in EReal, where . is an EReal infimum, equal to over an empty set. Regular variation is the real-variable limit with an eventually positive denominator, and reuses the published definition HeavyTailNV.Tail.IsRegularlyVarying. The Jacobian is Table 1's closed form. Statements that evaluate at take .
The following hypotheses are added relative to the printed statements, each disclosed on its item:
The following printed statements are corrected:
Lemmas A.8 and A.10 and Corollary A.1 are not posed. Their uniform claims over all of depend on pointwise versions of the hazard rates and on the values of off the support and off , which the hypotheses do not control; Corollary A.1 fails as printed when has negative components.
A trivializing formalization is ruled out explicitly. The goal is the limit (23) for the estimator of §5.2 with Table 1's Jacobian, for every admissible and both exponents. It is not the bound , not a statement about an unspecified IS density, and not a statement for one fixed . The finiteness conjunct prevents Lean's convention from satisfying it.
Contributions are welcome at every level. The general tools (Potter bounds, the tail LDP, a Varadhan lemma for continuously converging functions) are useful as separate developments.
Large retail platforms both host independent sellers and sell their own products, and they control the order in which products appear in search results. When the platform ranks its own product first regardless of relevance, it engages in self-preferencing. Regulators have treated this as a competition problem: the European Commission opened a second antitrust investigation into Amazon's treatment of its own retail offers in 2020 (CNBC, 2020), and search neutrality, the requirement that results be ranked by relevance alone, is the remedy most often proposed.
Zou and Zhou ask whether such a rule helps consumers once prices respond to it. Their model builds on the economics of prominence in consumer search (Armstrong, Vickers and Zhou, 2009), in which the product shown first is searched first and so enjoys a demand advantage. The answer they obtain is negative in an identifiable region: when the two competing products are similarly popular, search neutrality strictly lowers consumer surplus. This mission formalizes that result and the equilibrium analysis on which it rests.
A platform sells its own product and hosts a third-party seller of a competing product ; marginal costs are zero. A unit mass of consumers has unit demand. A product either matches a consumer (value ) or not (value ).
Under Condition 1 there are thresholds , depending only on , with
such that for every , consumer surplus in every equilibrium with search neutrality is strictly smaller than in every equilibrium without it:
The equilibria without neutrality: the price order when is prominent for all (Appendix, p. 42); the closed-form equilibrium of that pricing game (cases (A)–(B), pp. 42–43); the statement of Lemma A1 (p. 42); Proposition 1 (p. 16) and the uniqueness claim before it. The equilibria with neutrality: the price order by (pp. 44–45); cases (A2), (A3)/(B3) and (B2) (pp. 45–46); Proposition 2 (pp. 17–18). The two consumer-surplus displays (pp. 43–44 and 46). Proposition 3(2) and Corollary 1 are included as companion statements.
The result. Proposition 3(1) shows that a relevance-based ranking rule can backfire. Under self-preferencing the third-party product is never prominent, so its seller prices low to invite search, and this disciplines the platform's own price. Under neutrality each seller is prominent for the consumers who like its product best, and for similarly popular products both sellers charge the maximal price ; on consumer surplus with neutrality is exactly zero. The goal makes this precise and shows that the harmful region strictly contains that interval. It is the paper's central short-term finding and the basis of its policy discussion.
Formalizing it. No part of this analysis is machine-checked anywhere, and the platform has no model of consumer search with prominence. The source file contains the equilibrium derivations of §4.1 in its Appendix, but the proofs of Propositions 1–3 and of Lemma A1 are in an online appendix that is not part of the source; a formal proof would supply them. Several of the Appendix's closed forms are misprinted (the interior prices of cases (A1) and (B1), the thresholds and ), and the threshold misclassifies the boundary when ; the formal statements fix what is actually true.
The profits are piecewise quadratic with a kink at , so first-order conditions do not characterize equilibria: every candidate must be checked against global deviations across the kink. Without neutrality, a deviation can also change the platform's ranking, so the deviating seller faces a different demand system; this is the content of Lemma A1 and the reason Condition 1 is needed. The obvious argument for the goal, "consumer surplus with neutrality is zero on and positive without it", proves only the closed interval. The strict extension to requires controlling the neutral equilibrium just outside that interval, in the regions (A2) and (B2), where it is no longer at the corner.
A complete development needs elementary real analysis only: piecewise quadratic optimization on , the integral , and continuity of the neutral equilibrium in . The model definitions are shared, with the same names, with the companion mission on equal popularity and the commission rate. Proofs of any milestone are welcome, as are proofs of Lemma A1 and of uniqueness, whose arguments are not in the source.
Heavy-traffic analysis is the standard tool for scheduling queues whose servers are almost always busy: after diffusion scaling, a multiclass queue is approximated by a reflected Brownian motion, and asymptotically optimal policies are read off a limiting control problem. Classical results of this kind, such as the asymptotic optimality of the cµ rule (serve the class with the largest holding cost times service rate first; van Mieghem, 1995), assume that the job-size distributions are known.
In practice the first moments of service times are usually estimated well, while their variability is not. Atar, Castiel and Shadmi study a high-uncertainty regime: the means of the job-size distributions are pinned down to within , but their variances are uncertain at order one, and an adversary chooses them job by job with full knowledge of the past. The scheduler wants to minimize, and the adversary to maximize, a discounted holding cost. The paper solves this game asymptotically: the nonpreemptive cµ policy is asymptotically optimal against every adversary, and the value of the game converges to the value at of a one-dimensional Hamilton–Jacobi–Bellman (HJB) equation.
There are job types and one server. In the -th system one job of each type arrives at each time , , and the server works at rate , so that a job of size occupies it for time units. The system starts empty.
Adversary. For each and type an uncertainty class , a nonempty closed set of probability distributions on , is given. At each epoch the adversary chooses for every , based on the past job sizes, and the job sizes are then drawn independently across types from these distributions. The set of such controls is .
Scheduler. The scheduler chooses the cumulative effort devoted to each type, an -dimensional Lipschitz path whose increments over lie in . An admissible strategy is a measurable, non-anticipating, work-conserving map from the adversary's control path to such an effort path that never serves more work than has arrived.
Cost and value. With , the workload is , the queue length is the number of arrived type- jobs not yet completed, and hats denote scaling by . For holding costs ,
Assumptions. With the mean and half the variance of , and , the sets converge in the Hausdorff distance to compact sets ; fourth moments are uniformly bounded; (heavy traffic); and types are labelled so that , with .
HJB equation. With ,
for the classical solution of the HJB equation. The paper states with the value of a martingale control problem; the goal uses the form, which leaves the martingale problem out of the statement.
The result gives the first-order asymptotics of a scheduling game with model uncertainty: the scheduler loses nothing by ignoring the adversary and using the cµ rule, and the adversary's best response is a state-feedback choice of drift and variance determined by and . Theorem 1 is a robustness statement for one of the most widely used scheduling rules; Theorem 2 reduces a game on path space to a scalar nonlinear ODE.
The paper's proofs are complete, so the remaining work is formalization. No part of this result, and none of its objects (heavy-traffic queues with adversarial service distributions, the nonpreemptive cµ policy as a map on path space, the HJB equation of a reflected controlled diffusion), has a known machine-checked statement or proof.
The statement is a limit of a real sequence, but each term is an infimum over measurable, causal, work-conserving maps on path space of a supremum over feedback choices of distributions. The proofs (§§4–7 and the appendix) use uniform C-tightness of prelimit processes, weak convergence in , the existence theory for fully nonlinear uniformly elliptic equations (Gilbarg–Trudinger, Thm 17.18), martingale characterizations of limits (Jacod–Shiryaev, Cor. VI.6.30; Karatzas–Shreve, Thm 5.5.15), measurable selection (Budhiraja–Dupuis, Lemma 8.10), and Taylor expansion of along the prelimit workload. The obvious route through the uncontrolled diffusion limit fails because the adversary's variance choice is state dependent, so no single limiting Brownian motion describes all adversaries; the limit is a control problem, not a process.
The Lean development lives in the namespace HighUncertHT.Game. Types are Fin L, 0-based (the paper's type 1 is index 0). Distributions are ProbabilityMeasure ℝ with no mass on , with the weak topology. Systems are indexed by ; the class at is required to satisfy the same conditions so that control sequences indexed by exist. Costs and values are in (lower Lebesgue integrals), sup norms are in , the Hausdorff distance is the extended one, and derivatives of are one-sided on .
An adversary control is encoded by its feedback map from past job sizes to distributions and the measurable Markov kernel it induces; its law is the Ionescu–Tulcea trajectory measure. By (5), the Doob–Dynkin lemma and (7), this has the same laws, hence the same costs, as the paper's . Strategies are measurable for the product σ-algebras. The cµ strategy is defined explicitly by an event recursion over service decisions.
The standing assumptions (Assumptions 1–2, labelling (14), ) are fields of the Setting and hold in every statement. Corrected printed slips: the priority rule serves the highest index (p. 9 prints "lowest", contradicting the cµ rule and Lemma 5); the departure count is capped at the number of arrived jobs (p. 6); "→ 0 in probability" for processes is read as convergence of the sup norm on compact intervals (Lemma 5); (55) is stated for the control (61), not (15).
Trivializing formalizations are ruled out: is nonempty because is a milestone; the HJB has a classical solution (Proposition 1.1), so the goal is not vacuous; no expectation is a Bochner integral that could vanish for non-integrable integrands; is not a junk deriv; and (55) asserts that its feedback control exists.
Needed infrastructure: diffusion-scaled processes and their tightness in , the one-dimensional Skorokhod map and its Lipschitz property, martingale estimates for sums of conditionally centred job sizes, and the existence theory for the HJB equation. The Skorokhod map, the queue primitives and the cµ policy are reusable for other heavy-traffic missions. Contributions on any milestone, or on general lemmas they need, are welcome. Not included: Lemmas 1, 6, 7, 8, Proposition 1.2, Proposition 2, Theorem 2.3 and the martingale control problem.
In adaptive video streaming and online gaming, tasks are dispatched to one of identical server pools; all tasks in a pool are served in parallel, so a task's duration does not depend on the load, but its quality of service does. The total number of tasks then does not depend on how tasks are dispatched (the pools together form an infinite-server system), and the relevant objective is a balanced distribution of tasks over the pools: every Schur-concave utility of the occupancy vector, including the -fair utilities, rewards balance (Goldsztajn, Borst & van Leeuwaarden 2024, §1). Join the Shortest Queue is optimal for this purpose but needs the exact occupancy of every pool.
A threshold dispatching rule needs much less. With an integer and a threshold , it keeps every pool between and tasks whenever it can. Choosing well requires the offered load , which in practice is unknown and varies in time. The refined learning scheme of Goldsztajn, Borst and van Leeuwaarden adjusts online, in steps of , using the same coarse state information as the dispatcher. This mission formalizes their main result on that scheme (Theorem 2 of arXiv:2012.10142v3): along time intervals where the load is suitably bounded, the threshold settles at the right value and the load becomes balanced.
Timeline. The threshold rule with and the fixed threshold was shown to have the same fluid and diffusion limits as Join the Shortest Queue for constant arrival rates and exponential service (Goldsztajn et al., INFORMS Journal on Computing, 2022). The present paper (arXiv 2020, revised 2024; Mathematics of Operations Research, 2025) removes the knowledge of , allows a time-varying arrival rate, and proves almost-sure statements about the learned threshold.
Fix a horizon , a measurable arrival-rate function , a service rate and an integer . The system with pools receives tasks at rate ; service times are exponential with rate . The occupancy state records the fraction of pools with at least tasks, so it lies in
The threshold is a nonnegative multiple of . An arriving task goes to a pool, chosen uniformly at random, with fewer than tasks if there is one; otherwise to one with fewer than tasks if there is one; otherwise to any pool. The refined learning scheme with parameters acts at arrivals: if, right before the arrival, the fraction of pools with at least tasks is at most , the threshold drops by ; if all pools have at least tasks and at least have at least , it rises by .
All systems are built on one probability space from independent unit-rate Poisson processes , i.i.d. uniform selection variables , and random initial conditions with almost surely, and . The paths are the solutions of the implicit equations (9a)–(9b): arrivals follow and are routed by the ; departures from pools with tasks follow run at the clock .
The fluid total mass is with . On an interval let be the infimum and supremum of . The load is -bounded on (Definition 1) if and exceeds an explicit constant built from and .
Assume and for some , the load is -bounded on , and . Then almost surely
In the order of the proof: well-posedness of (9a)–(9b) (§5.1.1); Lemmas 21 and 22 and Proposition 4 (relative compactness); Lemmas 5 and 6 and Proposition 7 (the set of nice sample paths); Proposition 8 ( uniformly); Proposition 9 (decay of tail masses below the threshold); Proposition 10 (the threshold eventually stays at most after ); Corollary 11 (the bound (6c)); Lemmas 12 and 13 (the threshold locks at ).
The result. Theorem 2 shows that a scheme using only two bits of state per arrival finds the balancing threshold without knowing , within the explicit time , which is tight for an initially empty system with constant load. It quantifies balance: the fraction of pools with fewer than tasks is for every , and the mass beyond column decays exponentially. Conditions (5) are sharp in kind: prevents settling too high, and the rate stops fluctuations from pushing the threshold down.
Formalizing it. The result is proved in the paper; nothing here is open mathematically. Nothing of it is machine-checked. A formal proof would add an almost-sure coupled construction of a many-server Markov process on Poisson primitives, a rate- functional strong law for the Poisson process, and a pathwise relative-compactness argument in the uniform topology. None of these is in Mathlib.
The usual fluid-limit route fails here. The learning scheme reacts to excursions of the occupancy process of vanishing size: a threshold increase needs , a decrease with . So the threshold is not a continuous function of the fluid state, and limits of need not satisfy any closed ODE. The natural first idea, deriving a limiting ODE for jointly and studying its equilibria, fails for exactly this reason: whether the threshold moves is decided by fluctuations of order around the fluid path, which a law of large numbers does not see. The statements must therefore hold almost surely and uniformly in time for the coupled sequence, not in law.
UnknownLoads.Refined.LoadData holds (with measurable, an assumption the paper uses tacitly). Primitives holds the Poisson processes (the published BesbesZeevi.Parametric.PoissonProcess, independent as a family), the uniform , the initial conditions, and the independence of the three families. Any probability space carrying them is allowed; completion is immaterial for almost-sure statements.System with the hypothesis that, almost surely, for every , is a càdlàg, -valued solution of (9a)–(9b) on . Left limits are Function.leftLim, and . The well-posedness milestone states that such solutions exist and are unique almost surely, so System is not vacuous.IsNicePath B_T ω. It holds the equations at , simple events (unit jumps, no coincidences) and the initial conditions at , Proposition 4's property, (11) and (12a)–(12c). Proposition 7 asserts it almost surely; "for each " becomes "for every with IsNicePath B_T ω".StrictMono maps. Tail sums in inequalities ((6c), Corollary 11) are in ; and in limit statements are real series, finite sums for large on . is "eventually for some ". The constant in (6c) is fixed to .tsum in (6c) would make the bound vacuous for non-summable tails, and a real supremum would make (6a) vacuous for unbounded thresholds. Neither appears. (6a) says that equals on for all large , a property of the learned threshold that no fixed threshold could satisfy for all admissible loads.Data brokers sell consumer data to firms that use it to decide whom to target, whom to lend to, or where to open a store. Two kinds of products are common: a marketing list, which supplies contact information without which the buyer cannot act at all, and a data append, which enriches information about consumers the buyer can already reach (Federal Trade Commission, Data Brokers, 2014). A seller who does not know a buyer's cost of acting must screen buyers with a menu of plans that differ in price and in how informative the data are.
Liang Guo's paper Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) characterizes the optimal menu, first for a binary-value model (§3) and then for a general information structure ordered by rotation (§4), following Johnson and Myatt (2006). This mission formalizes Proposition 7: data appends under the rotation order. It is the fourth mission of a series built from the same manuscript; the first three cover marketing lists and data appends in the binary model and marketing lists under the rotation order.
A marketer can take an action (target a consumer) at cost ; the action's value is uncertain with prior mean . A data service of informativeness produces a signal, and its information is summarized by the posterior mean . For each , has cumulative distribution function on a support , with a strictly positive density and mean for every . The family is rotation ordered: there is a point with
A more informative service spreads the posterior mean away from .
A service plan charges a fixed fee . Serving a marketer with informativeness costs the seller , with and increasing. A marketer targets exactly when , so a marketer with cost who buys earns
Costs are with probability and with probability , . A data-append buyer can act without the data, so its outside option is .
The seller offers a menu and maximizes subject to individual rationality and incentive compatibility for both types. Call any maximizer an optimal menu, with levels . The benchmark with observable costs is
and its maximizers are the efficient levels .
Assume . If , then
and if , then
Here means that the set of -levels of optimal menus equals the set of efficient levels, and each strict inequality holds for every optimal menu and every efficient level.
Proposition 7 is the general-distribution form of a "double reversal". With marketing lists the low-cost marketers are the high type: they get efficient information, and the high-cost marketers' information is distorted (Proposition 5 of the paper). With data appends and costs below the prior mean, the outside option makes the high-cost marketers value data more. The roles of the types swap, and the direction of the distortion flips with the position of the costs relative to the rotation point. The result tells a data seller which customers to under- or over-supply, and shows that the answer depends on whether its data enable an action or only refine it.
The paper proves the result on a few pages, partly by phrases such as "it can be readily verified". No machine-checked version exists. A formalization makes explicit what the printed argument leaves implicit: that the dropped constraints hold at the reduced optimum, which regularity of and the strict inequalities need, and that statements about "the" optimum hold for every optimum when maximizers are not unique.
The obvious approach substitutes the binding constraints and compares first-order conditions. Two steps of it fail as stated. First, the reduction to (15) drops and ; holds at a maximizer of (15) only when the two informativeness levels are ordered as the rotation order dictates. That ordering is available only when both costs lie on the same side of . Second, first-order conditions say nothing at a corner of . The strict comparison needs the efficient level to be interior, where the derivative of exists. That comes from the conditions of footnote 5 together with the mean-preserving property of the family. The selling cost need not be convex, so maximizers can be non-unique, and every comparison must hold for every pair of maximizers.
RotationFamily with a bounded support (the paper allows an unbounded one). is continuous on with , and derivative , continuous on the closed support. exists on the closed support. The rotation order (9) holds on the open support, and the mean is for every . Condition (10) is not assumed; it follows.Model extends it with , , and with both costs in (a pin: the integrals presume it). It also fixes with monotone on . is written as .Global sensitivity analysis asks how much of the uncertainty in a model output is due to an input . Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose a family of indicators built on optimal transport: the expected optimal transport cost between the marginal law of and the law of conditioned on the information carried by . The family contains the variance-based and -based indices used in practice as special or limiting cases, and it applies to multivariate outputs.
In applications these indicators are never computed from the true joint law of . They are computed from a sample, by splitting the range of into cells, estimating the law of on each cell, and solving one optimal transport problem per cell (the estimator (76) of the paper). Whether this procedure converges to the quantity it is meant to estimate is the question of consistency, settled by Theorem 21 of the paper. This mission formalizes Theorem 21 and the steps of its proof.
Let and be Polish spaces with their Borel -algebras. A cost is a continuous function with exactly when . The optimal transport cost between probability measures on is
the infimum over couplings with marginals and .
Let be the joint law of on , with marginals (of ) and (of ). For a -algebra on , a version of the conditional distribution of given is a Markov kernel , -measurable in , with for . The OT-based sensitivity measure (Definition 1) is
written when is the Borel -algebra.
Estimation setting. A sequence of joint laws on (for instance empirical laws of a sample of size ) converges weakly to ; are its marginals. The cost has bounded separate costs: with continuous, and with ,
A sequence of finite measurable partitions of generates -algebras with
The quantities of interest are (finite ) and .
Under (73) and (75), the iterated limit exists and
The statement fixes no rate and no constant; it asserts only that refining the partition after the sample size has grown recovers the sensitivity measure.
The last step of the paper's proof, , is the continuity of along increasing -algebras, Theorem 9 of the paper. It is posed in the companion mission of this series (part 2, on information continuity) and is not restated here.
Theorem 21 is what licenses the partition estimator: without it, the number computed by solving one transport problem per cell of a sample has no proven relation to the sensitivity measure. The result is deterministic in the laws, so it applies to any sampling scheme whose empirical laws converge weakly with converging -moments, not only to i.i.d. samples. The finite case covers categorical inputs directly.
On the formal side, no part of this argument is machine-checked. A complete development produces reusable pieces beyond this paper: the conditional law on a cell of null boundary as a continuous functional of the joint law, uniform integrability from convergence of moments under weak convergence, and the stability of optimal transport costs under weak convergence of the marginals with uniformly integrable cost bounds. The last is a standard theorem of optimal transport (Villani 2009, Theorem 5.20 and its proof) that the paper invokes without proof in (86).
The naive argument passes to the limit term by term in the finite sum (83). Two steps of it fail without further work. First, the optimal transport cost is only lower semicontinuous under weak convergence in general; convergence of needs the cost to be dominated by functions whose integrals converge, which is why (73) is assumed and why uniform integrability (85) must be transferred from to the cell laws. Second, cells of zero limiting mass may carry positive empirical mass for every , and their conditional laws need not converge at all; their contribution must be shown to vanish through the product , not through the cell laws. Finally, the two limits do not commute in general, so the order matters.
Fintype with the discrete topology, so .ProbabilityMeasure.RWPI.SqrtLasso.transportCost; all of , and the integrals take values in .IsCondDistrib.lim.A trivializing formalization is ruled out: is not assumed bounded, the laws are not assumed eventually equal to , the conditional laws are not assumed to converge, and cells of zero mass are allowed.
Contributions are welcome on each milestone separately, in particular on the stability of transport costs (86), which is reusable well beyond sensitivity analysis.
Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. Computing the optimal adjustable solution is intractable in general, and even for a single budget constraint it cannot be approximated within under a standard complexity assumption (Feige, Jain, Mahdian, Mirrokni, IPCO 2007), where is the number of decision variables.
Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by one linear program and are widely used in practice. The question is how much they lose in the worst case.
Uncertainty sets in applications are rarely a single budget: demand is usually grouped (by region, product family or time period) with a separate budget per group. When the groups are disjoint the set is a Cartesian product of budget sets, a class studied by Gupta et al. and by Feige et al. in the robust covering literature.
Timeline. Bertsimas and Goyal (2012) proved that affine policies are within of the adjustable optimum for general uncertainty sets and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved for a single budget set (Theorem 3.1, the first mission of this series) and for disjoint constrained budgeted sets (Theorem 4.1, the goal of this mission).
Let , a non-negative recourse matrix , costs and a polyhedral set be given. For an uncertainty set of right-hand sides, problem (1.1) is
A first-stage and a recourse rule form a feasible solution when and , for every . The affine problem (2.1) restricts the rule to (still requiring on ); its value is .
Let be a partition of and weights. The disjoint constrained budgeted set (4.1) is
With it is the budget of uncertainty set of the first mission.
The fractional covering value (3.2) of a requirement is . In an online fractional covering problem the rows to be covered arrive in batches and a solution may only be increased; an online algorithm is -competitive when its cost on every sequence is at most times the offline optimum . Throughout, is the natural logarithm and .
for every instance with a disjoint constrained budgeted set: there are and such that for all , all , every number of blocks and all data. The constant is unfixed, and the bound must not depend on .
With , Lemmas 4.3 and 4.4 give the goal.
The result. For disjoint budgets the bound is within a factor of the hardness bound for a single budget, and it does not depend on the number of groups . It shows that affine policies stay near-optimal beyond the single-budget case, for a class that models grouped demand. The paper notes that it is open whether the extra factor is necessary. Gupta et al. give an -approximation for a special case with 0/1 matrices and equal weights, but their algorithm is not an affine policy.
Formalizing it. The theorem is proved on paper; no machine-checked proof is known. The formal development makes explicit what the paper uses about the online covering algorithm (monotone, covering, competitive), handles the "without loss of generality" relabelling of the blocks in the greedy scenario, and records two gaps in the proof of Lemma 4.4 (zero weights, and a zero increment , for which Lemma 3.3 is stated with ).
The thresholds that split cheap from expensive components cannot use the single quantity as in the single-budget case: a scenario may activate one budget in every block at once, and summing per-block bounds gives a factor . That is the bound of the paper's Section 5. Removing the dependence on requires per-block thresholds that add up to , and the paper obtains them from the increments of an online covering algorithm along a greedily chosen worst sequence of scenarios. A proof of the goal therefore needs an -competitive online fractional covering algorithm, Buchbinder and Naor's Theorem 4.1, posed on this platform as BNCovPack.Covering.theorem_4_1 (b57de23d-5953-424f-a729-5a018aa74b37, open). That theorem requires positive costs, so zero-cost columns, which this paper allows, need separate handling. The static part also needs Lemma 3.3, the core of the first mission.
Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean indices and blocks are 0-based. First stage and recourse share the dimension , as on p. 1. The partition is S : Fin L → Finset (Fin m), pairwise disjoint and covering Fin m (empty blocks allowed).OnlineCover with ratio : starting at , non-negative, monotone, covering every revealed coverable row, and -competitive on disjoint batches. The milestones hold for every such algorithm, with the paper's written as . The goal does not mention the algorithm. Algorithm 1 is a predicate on a run (a bijection of blocks and the chosen scenarios) with its maximality clause, so ties are arbitrary.The source is arXiv:1807.00163v2; its printed page numbers equal the PDF page numbers.
Approximate policy iteration is the template behind most practical reinforcement-learning systems for large state spaces: alternate between choosing a policy that looks good under the current value estimate and estimating the value of that policy, with errors in both steps. Game-playing systems such as AlphaZero add two ingredients to this template: a multi-step lookahead (tree search) when choosing the policy, and a linear or neural value-function approximation fitted from a few evaluated states. Classical error bounds for approximate policy iteration (Bertsekas and Tsitsiklis, 1996) assume that each evaluation error is bounded by a fixed ; Efroni, Dalal, Scherrer and Mannor (2019) extended them to -step lookahead policies. Neither analysis asks whether a fitted value function actually meets such a bound.
Winnicki, Lubars, Livesay and Srikant (arXiv:2109.13419, Operations Research, 2025) show that it need not: with least-squares fitting on a subset of states, the iterates of approximate policy iteration can diverge (their Section 3.2). They then prove that sufficient lookahead and rollout length restore convergence, with an explicit finite-time error bound. This mission formalizes that bound.
A Markov decision process has a finite set of states , a finite set of actions , transition probabilities of moving from state to state under action , mean rewards , and a discount factor . A deterministic policy is a map . Its value is the expected discounted reward
and the optimal reward-to-go is . Vectors are compared in the sup norm . The policy operator and the Bellman operator are
Each state has a feature vector ; is the matrix with rows . For a set of states , keeps the rows indexed by and selects the entries of a vector indexed by .
Algorithm 2 starts from an arbitrary and, at iteration , (i) picks a policy with (an inexact -step lookahead); (ii) forms the noisy return on an evaluation set ; (iii) fits by least squares on and sets . Assumption 1 asks that the features of have rank for every and that . Under it the fit is linear, with , and the paper defines
If , then under Assumption 1 every run of Algorithm 2 satisfies, for every ,
In the order the proof uses them:
Theorem 1 states a sufficient condition for convergence that does not depend on the size of the state space: lookahead plus rollout depth must exceed , where depends only on the features and the evaluation sets. Paired with the divergence example of Section 3.2, it shows that lookahead is not merely a heuristic improvement but can be what makes approximate policy iteration with linear function approximation stable. Proposition 1 is a reusable interface: any policy-evaluation scheme whose errors satisfy a geometric-plus-floor bound inherits the same convergence guarantee; the paper's gradient-descent variant is obtained this way.
The result is proved on paper; it has not been machine-checked. The Prove2Me platform has the finite-MDP layer used here (transition kernels, policy values as discounted series, the Bellman optimality operator), exact modified policy iteration, and a one-step bound for greedy approximate policy iteration with -functions (, no lookahead error). It has no lookahead bound, no least-squares value-function fit, and no finite-time bound for approximate policy iteration with function approximation. A complete development would add the Bellman equations for deterministic policies, the lookahead step (15), the least-squares projection identity, and the error recursion, all of which are reusable for other analyses of approximate dynamic programming.
The obvious argument fails at the evaluation step. Classical analyses treat as given; here the error is produced by the algorithm and fed back: the fitted is the input of the next lookahead, and the least-squares operator can amplify sup-norm errors by a factor , which is at least whenever . The error recursion therefore contracts only when . A second point is the lookahead step (15), which must hold for an arbitrary previous policy and an inexact lookahead, and rests on the increase of in rather than on contraction alone. Finally, combining the geometric decay of the evaluation errors with the -contraction of (15) requires a convolution estimate that yields the factor .
States and actions are finite nonempty types; the transition kernel is the published IsTransitionKernel, is the published PolicyValue (a discounted series of expected rewards, not a fixed point of ) of the point-mass policy at , is the published BellmanOperator, and is the maximum of over the finitely many deterministic policies. Rewards enter only through their means . Vectors are functions with the sup norm; matrix norms are Mathlib's operator norm (maximum absolute row sum). The rank condition of Assumption 1 is for every ; Lean's matrix inverse is zero on singular matrices, so no statement relies on it without this hypothesis.
Conventions fixed where the page is loose: Algorithms 2 and 3 are predicates on whole runs, quantified over every admissible lookahead policy, noise and minimiser. , which Algorithm 2 never produces, is free, so every bound holds for every deterministic . is the operator of (eq. (6) calls it ; the suprema agree). is the supremum over all and all deterministic policies. Algorithm 3 is stated with , the index of (15) and Appendix B, and without the representation , which Proposition 1 does not use. Proposition 1's first display divides by and is stated for ; the other results take . The noise bound is imposed on the whole vector instead of setting off ; off it constrains only entries the run never reads. The limsup is stated as "for every , eventually bound ". The hypothesis of Theorem 1 is kept with the real logarithm as printed; for it is equivalent to , and when (possible only if ) it reads .
A formalization that fixes the lookahead policy to an exact argmax, the noise to zero, or to a convenient policy proves a special case and is ruled out; so is defining or as a fixed point, which would make eq. (2) definitional.
Contributions welcome: proofs of the Section 2 milestones from the series definition of , the least-squares identity (6), the lookahead step (15), and the recursions of Proposition 1 and Appendix B. Theorem 2 of the paper (gradient-descent fitting) is not part of this mission: its Assumption 2 places no lower bound on the step size, and the statement fails for negative step sizes.
The joint replenishment problem is a basic model of coordinated inventory control. A firm stocks commodities, each of which follows its own Economic Order Quantity (EOQ) model, but every order also incurs a joint ordering cost , regardless of which commodities it contains. Ordering commodities together therefore saves money, and the question is how to synchronize their replenishment cycles.
Since the mid-1980s the best known guarantee for the continuous-time problem came from power-of-2 policies (Roundy 1985, 1986; Jackson, Maxwell and Muckstadt 1985; Muckstadt and Roundy 1987). Their cost is within of optimal for a fixed base period, and within when the base is optimized. On the hardness side, Schulz and Telha (2022) and Tuisov and Yedidsion (2020) showed the problem to be intractable; the latter proved it strongly NP-hard, which rules out a fully polynomial-time approximation scheme.
Segev (arXiv:2302.09941, published in Management Science, 2025) gave the first improvement over power-of-2 policies. For every the problem can be approximated within of optimal in time . This mission formalizes the approximation guarantee behind that theorem. The source is the arXiv v1 preprint, and all theorem numbers refer to it.
Commodity has ordering cost and holding cost . Ordering it every time units costs per unit time
A policy is a vector of positive intervals. For and , let be the multiples of in . A policy places
joint orders in . Its joint ordering cost and total cost are
For , is the least common multiple of , and when the intervals have no common multiple.
The algorithm works against a reference policy with and an estimate .
Two representatives are -aligned when for positive integers . The alignment graph joins -aligned active segments. The linear system (LP) asks for satisfying the same alignment relations as . A solution is misaligned across components when representatives in different components of are not -aligned. The final policy gives commodity the -cheapest of the and of the single large interval , rounded up to a multiple of .
Fix , , , a policy with all , and with .
The goal's proof uses the following results, in this order:
The theorem gives the first approximation scheme for continuous-time joint replenishment. It settles the problem's approximability up to the form of the exponential dependence on , after nearly four decades in which power-of-2 policies were the best available. Its central device, synchronizing pairs of representatives through bounded integer multiples and controlling everything else by inclusion–exclusion over the alignment graph, is proposed in the paper as a template for other multi-item lot-sizing models.
The result is proved on paper, and no machine-checked version is known. A formalization adds three things.
The obvious argument runs as follows: round every to a nearby point of a small grid and charge joint orders to the grid. It fails because the cost of the joint orders depends on the least common multiples of the intervals, not on their sizes. Two nearby reals can have a small lcm, or none at all, and an arbitrarily small perturbation changes by a constant factor. The proof must therefore keep the arithmetic relations among the representatives exactly where they matter: within components of , through (LP). It must also show that relations across components contribute only lower-order terms. This requires two nested inclusion–exclusion expansions (Lemma 3.3 and Claim 3.5) whose error terms, of order , are absorbed by the choice of .
Lemma 1.2 is a squeeze argument, but it rests on showing that the common multiples of finitely many positive reals form the set .
All declarations live in the namespace ContJRP.Align.
Representation.
Fin n with .Finset ℝ, and is a member of every .limUnder.0 when no common multiple exists.R 0.Committed conventions.
What is left out. The running-time half of Theorem 1.3, the time bounds of Lemmas 2.4 and 2.5, and the final selection of the cheapest candidate (§3.3) are not formalized. The goal carries the constants the analysis proves, and , rather than the rescaled .
Trivializing formalizations ruled out.
limUnder cannot return a junk value, because Lemma 1.2 and (3) are stated as Tendsto limits.Infrastructure and contributions. A complete development needs three pieces:
Finset.inclusion_exclusion_card_biUnion in Mathlib);The density results (Lemma 1.2) are reusable for any periodic-scheduling model. Proofs of any milestone are welcome, as are alternative statements of the selection step.
In many sequential decision problems the state of a system is not observed for free. A controller monitoring a machine, a patient or an inventory must pay to inspect it, and between inspections it acts on a belief rather than on the state. The observation cost model (OCM) makes this precise for a finite Markov chain: at each time the controller either pays a fixed cost to observe the state and choose a new action, or keeps the previous action without observing. Reisinger and Tam (arXiv:2201.07908v3, published in Mathematics of Operations Research, 2025) show that, after augmenting the state with the time elapsed since the last observation, the dynamic programming equation of the discounted OCM is a discrete quasi-variational inequality (QVI): an obstacle problem whose obstacle depends on the unknown itself.
Earlier work on the OCM (Anderson and Friedman, 1977; Hajek, Mitzel and Yang, 2008) treated fixed dynamics of the underlying chain. Discrete QVIs with interconnected obstacles and their penalty approximation were analysed by Reisinger and Zhang (2019) for switching problems, with the identity matrix in place of the transition operator . The paper recasts the OCM QVI in an abstract form and proves it is well-posed.
Let be a finite state space and a finite nonempty action set. The unknown is a function with components . A driver is a family , ; its third argument is the vector and its fourth the whole function . Given a sequence of substochastic matrices on (nonnegative entries, row sums at most ) and a vector , the inspection operator is
It reads only at time and couples all actions. The QVI (3.1) is
Assumption 3.2 asks for a constant with whenever are bounded and , together with boundedness in and uniform continuity in . Assumption 3.12 asks that depend on only through finitely many values. For the OCM, .
For the computation the paper truncates time to , giving a finite QVI (3.7) for a map with the monotonicity property (3.5), and replaces it by the penalised problem (3.8), , with a continuous non-decreasing penalty vanishing exactly on .
Under Assumptions 3.2 and 3.12, a uniform bound , and :
The well-posedness theorem identifies the value function of the discounted observation cost model as the unique bounded solution of a QVI, which is what justifies computing it: truncating time and penalising the obstacle gives a sequence of finite nonlinear systems whose solutions converge to it, and these systems are solved in practice by semismooth Newton iterations. The abstract framework covers other models with a non-local, action-coupling obstacle, such as discretised switching problems.
The results are proved in the paper, partly by reference: existence of the penalised solutions and the convergence are delegated to Reisinger and Zhang (2019, Theorems 2.5 and 2.6), and Lemma 3.11 is stated as "a direct adaptation" of a lemma there. None of the results is formalized. A formal development makes the delegated steps explicit and fixes the hypotheses under which the statements hold (see Formalization scope).
The comparison principle (Proposition 3.3) is a maximum principle on an infinite index set: the supremum of need not be attained, so the argument works along maximising sequences and needs the uniform continuity of the driver in . In the obstacle branch, the inspection operator transports the maximum to time , and excluding that case uses through a chain argument over the finite set ; with comparison fails.
Existence is harder. A direct fixed-point argument fails because the driver is only monotone, not a contraction, and the obstacle depends on the unknown. The paper's route goes through two limits, and , each requiring bounds uniform in the other parameter and a passage to the limit in a nonlinear, non-local equation; the limit uses Assumption 3.12 to localise the dependence on .
Everything is finite-dimensional or a function on the discrete set ; no measure theory is involved. Unknowns are curried as u n x a , costs as c a x. Time in (3.1) ranges over all of , including , and is u 1. The truncated time set is Fin N with the index standing for time , so is u 0. Substochastic means nonnegative entries with row sums at most ; and are componentwise; norms are sup norms, written out entrywise. Bounded sets of in Assumption 3.2.2 are cubes.
Two additions to the paper's hypotheses are made, each because the statement is false without it. The goal assumes : Assumption 3.2.2 only bounds for each fixed , and the driver satisfies both assumptions yet has no bounded solution. Corollary 3.4 is stated for bounded solutions of (2.11). The truncated QVI is stated without Problem 3.6's time boundary condition , which (3.8) does not encode. The continuity of the restricted driver claimed in Lemma 3.5 is not part of that milestone; the truncated part of Theorem 3.13 takes continuity of an abstract as a hypothesis.
The clause of Theorem 3.13 (", monotone from below") is not stated: the paper does not define the truncated operator beyond time , and with the zero extension the monotonicity in fails. The goal keeps the clause's well-defined content, existence and uniqueness of the bounded solution. A goal asserting only uniqueness (Proposition 3.3), or existence with the uniform bound hidden inside a definition, would be a different theorem; the bound is an explicit hypothesis.
A complete development needs solvability of finite-dimensional monotone nonlinear systems (the existence result cited from Reisinger and Zhang), monotone convergence in finite dimensions, and maximum-principle arguments on . The comparison principles and the a-priori bound are reusable for other monotone schemes. Proofs of any milestone, and alternative existence arguments for the goal, are welcome.
In shoppertainment live streaming a single streamer sells products from many manufacturers during live sessions that mix product presentation with entertainment. Some of the most successful streamers spend much of their air time on content unrelated to the products; the paper cites Dong Yuhui, who devotes his sessions to English lessons. Traditional TV shopping (QVC) does the opposite and spends all air time on product features. This raises a question for operations and marketing: how should a streamer split a session's limited bandwidth between entertainment and product information?
Gu, Zhao and Wu (Management Science, 2024) answer it in a three-stage game between a streamer, a pool of manufacturers and a population of consumers. Entertainment attracts consumers directly, but it also leaves them less certain whether a product fits, and that uncertainty changes how manufacturers price. The paper's headline result, Proposition 3, says that zero entertainment is never optimal. This mission formalizes Proposition 3 together with the chain of lemmas and propositions of Section 4 on which it rests.
A product has quality , the probability that it fits a consumer. A good fit is worth and a bad fit . The qualities of the contracted manufacturers are uniform on , where is the streamer's quality threshold; write . The streamer keeps a commission rate of sales revenue.
The streamer chooses an entertainment bandwidth , the share of a session spent on entertainment. Each attending consumer receives a fit signal whose accuracy is . After a good signal the posterior fit probability is , after a bad one it is . The two willingness-to-pay levels are therefore
With attending consumers, the demand at price is if (everyone buys), if (only good-signal consumers buy), and above . A manufacturer earns .
Write and . In equilibrium a manufacturer of quality prices low () exactly when , that is, when . A consumer's expected shopping surplus is the average, over manufacturers, of what the consumer gains at the equilibrium price. Attending costs are uniform on , and the streamer's entertaining capability gives the entertainment utility , so the attending traffic is
The individual profitability is the streamer's expected commission from one attending consumer, and the streamer's payoff is .
For , , , and :
Proposition 3 is the paper's managerial conclusion. Spending all bandwidth on product information, as TV shopping does, is never optimal. A streamer should allocate at least the traffic-maximizing share to entertainment, and should go to full entertainment once its entertaining capability exceeds . Corollary 2 and the extensions of Section 5 of the paper (informing capability, in-session adjustment, competing streamers) build on this result and on the Section 4 chain.
The results are proved in the paper and its Online Supplementary, and none is machine-checked. The supplement's argument for the regime shows only that at , a local statement. The goal here asks for the global claim that is the unique maximizer, so a complete formalization closes a gap in the published argument. The milestones make the paper's equilibrium derivation (manufacturer pricing, consumer surplus, traffic, profitability) checkable step by step.
Lemma 2, Proposition 1, Lemma 3 and display (14) are elementary: case analysis of a price and integrals of piecewise polynomials whose switch point depends on . Proposition 2 and Lemma 4 need sign analysis of explicit rational functions of on , uniformly in . The traffic is not concave there: its surplus component is convex on part of the interval and concave on the rest.
The goal is the hard part. is the product of a function that rises and then falls (Proposition 2) and a function that falls and then rises (Lemma 4), so the shape of either factor does not settle where the product peaks. Comparing maximizers of with maximizers of , and ruling out an interior maximum of above the threshold for every and , requires quantitative control of the product, not just the monotonicity pattern of its factors. Checking the sign of at alone is not enough.
All parameters are real numbers and every function of the model is total; the statements carry the standing ranges as hypotheses. The bandwidth domain is Set.Icc 0 1, and "optimal" means IsMaxOn on that set. The single definitions file Shoppertainment.OptimalBandwidth.Model contains , , the demand (8) extended by above , the manufacturer's profit, , , the equilibrium pricing rule, (as a Lebesgue measure), the consumer's ex-ante surplus, , , the revenue per attending consumer, and . and are integrals over the uniform law of quantities evaluated at each manufacturer's equilibrium price. They are not defined by the closed forms (12) and (14). This keeps Lemma 3 and (14) genuine statements and ties the goal to the manufacturers' equilibrium.
Conventions and pinned hypotheses:
Two formalizations would trivialize the mission, and both are excluded. Without the existence clause, a "for every maximizer" statement could hold vacuously, so the goal asserts existence. Defining and by (12) and (14) would make two milestones true by definition.
Lemma 1, Corollaries 1–2, Remark 1 and the Section 5 extensions are not posed. A complete development needs only Mathlib's interval integrals, Lebesgue measure on and elementary real analysis. Proofs of the closed forms of the Online Supplementary ( in A.4, (A1) in A.6) are welcome as auxiliary lemmas.
3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the input-size exponent, rather than an experimental speedup, is the quantity being studied.
Alman and Vassilevska Williams (2026) give a deterministic truly subquadratic integer 3SUM algorithm through thin matrix products and reductions involving Exact Triangle. Xu's manuscript, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, dated 13 October 2026, refines the analysis of that framework. Its claimed bound is the formalization target here. The Hexagon link identifies the author's submission page, which may require authentication; it is not presented as a public article identifier or evidence of peer review.
An input of size is a function . For a fixed natural number , every entry obeys . Acceptance means that there are pairwise distinct indices with . Repeated values at different positions are allowed. This is a decision problem, so the algorithm need not return a witness triple.
The word-RAM specification is the campaign's existing EndStatement definition, imported from its foundation mission. For each fixed , one finite deterministic program, one word-width threshold constant, and one time-bound function must work for all input sizes and all word widths above that threshold. Words have finite signed interpretations; arithmetic, indirect memory access, branching, acceptance, and rejection are defined operationally. The result concerns this exact model.
For the supporting analysis, let , with endpoint values . All logarithms are natural. For an integer , a positive integer , and , set , , , and
The sharp preprocessing saving, query exponent, and encoding exponent are
These auxiliary definitions describe costs; they neither redefine 3SUM nor assume the existence of a fast algorithm.
The campaign goal is the exact fixed bound
The first supporting milestone is the two-sided binomial entropy estimate. The second is the manuscript's normalized tail bound
A further milestone establishes strict improvement over the earlier preprocessing saving at fixed parameters. The algorithmic milestone combines the manuscript's Propositions 4.1 and 5.1: admissible sharp-tail parameters must yield a program satisfying the shared 3SUM specification, not merely a numerical inequality.
The final supporting milestone certifies the exact choice
It includes the preprocessing, query, encoding, prime-selection, and instance-construction inequalities, together with
Every terminating decimal denotes an exact rational number. The target is the fixed big- exponent 1.999017; the smaller cutoff is accompanied by residual asymptotic losses in the manuscript and is not asserted as the same fixed bound.
A complete proof would certify the manuscript's improved integer 3SUM bound in the campaign's common machine model. The gain is an analysis refinement of the inherited algorithm and reductions. It does not claim a new algorithmic framework, optimal parameters, global optimality, or priority over all other work.
The manuscript also gives an auxiliary bound by retuning the previous estimate. That weaker result is background, not this mission's campaign value. The existing upstream formalization is prior work; it does not automatically certify either refinement. The supplied rational interval verifier checks the parameter inequalities, but those checks alone do not prove a word-RAM running-time theorem. The main goal and the newly drafted supporting statements remain open Lean proof obligations.
A better tail estimate is insufficient unless every other cost remains within the final budget. Shared encoding work, all queries, deterministic prime selection, witness scanning, and instance construction must be included. The word-size and address bounds must remain valid after changing parameters. Ceiling operations, restricting to powers of four, and bounded-size exceptions must also be handled.
The central formalization burden is the connection between the analytic estimates and an actual deterministic program. Assuming an oracle with the desired running time would remove that burden and would not establish the stated target. Likewise, checking a finite range of sizes or a floating-point optimizer's output cannot establish the universal algorithmic statement.
The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The foundation reference and the campaign goal's import are retained. Supporting definitions use real logarithms, real powers, natural binomial coefficients, finite sums, and a natural ceiling. Domain hypotheses exclude invalid entropy-tail regimes; endpoint binomial cases are included explicitly.
For , the shared time predicate means that there exists such that for every . Correctness and termination still cover every input size, including . The manuscript's convention must be extended to the campaign's case, and its word-size analysis must justify uniform correctness at every sufficiently large word width. Both are explicit interface obligations.
Reusable contributions include entropy and tail estimates, rigorous logarithm enclosures, and parameterized cost-to-program results. Existing compatible library results should be reused where available. The manuscript and metadata were prepared with AI assistance; this mission makes no claim of completed human review or completed formal verification of the improved bound.
EndStatement.lean supplies the shared specification, not a proof of this mission's new exponent.Two-stage adjustable robust optimization models decisions taken in two steps around an uncertain demand: a first-stage decision is fixed now, the demand is revealed, and a second-stage (recourse) decision reacts to it. The objective is the worst-case total cost over a set of possible demands. The model covers set cover, capacity planning and network design under uncertain demand (Bertsimas, Goyal 2012; Gupta, Nagarajan, Ravi 2014). Computing the optimal adjustable solution is intractable in general: Feige, Jain, Mahdian and Mirrokni (2007) showed that, for the budget of uncertainty sets below, the problem cannot be approximated within a factor better than under a standard complexity assumption, where is the number of decision variables.
Affine policies, in which the recourse is restricted to an affine function of the revealed demand (Ben-Tal et al. 2004), are computable by a single linear program and perform well empirically. The question is how much they can lose in the worst case.
Timeline. Bertsimas and Goyal (2012) proved that affine policies are within of the adjustable optimum for general uncertainty sets ( = number of uncertain parameters) and that this is tight for some sets. El Housni and Goyal (arXiv:1807.00163, 2018; Mathematics of Operations Research 2021) proved that for budget of uncertainty sets the factor is , matching the hardness bound. That result is the goal of this mission.
Let , a non-negative recourse matrix , costs and a polyhedral set be given. For an uncertainty set of right-hand sides, problem (1.1) is
A first-stage and a recourse rule form a feasible solution when and , for every . The affine problem (2.1) restricts the rule to with , (still requiring on ); its value is .
The budget of uncertainty set (1.2) with weights is
The fractional covering value (3.2) of a requirement is , and for . Throughout, is the natural logarithm and .
for every instance with a budget of uncertainty set: there are and such that for all , all and all data. The constant is left unfixed, so the goal survives any improvement of the constant.
The result. The bound shows that affine policies are an optimal approximation for this class, up to a constant factor: no polynomial-time algorithm can beat them by more than a constant in the worst case (under the hardness assumption). It improves the earlier bound for budget sets exponentially, and it is the base case from which the paper derives bounds for intersections of budget constraints (Sections 4–5). Lemma 3.3 is a statement about fractional covering problems alone; it generalizes a set-cover result of Gupta, Nagarajan and Ravi (2014) to arbitrary non-negative matrices and weights, and improves its bound from to .
Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of the structural lemma is known. A formal development would also settle the paper's slips: Claim 3.2's does not follow from its proof (stated here in the explicit form the proof gives), Lemma B.2's strict inequality fails when , and Lemma 3.3 needs large.
Feasibility and the cost of the linear part follow directly from the construction. The difficulty is the static part, that is, Lemma 3.3. The obvious argument covers by a union of cheap scenarios, and it fails: each scenario covers rows of total weight at most , there can be many disjoint scenarios, and adding up their costs gives a bound proportional to , which may be as large as . The lemma asserts a bound that depends on alone, at the rate of the hardness result. Any argument therefore has to exploit condition 1 (every single row is expensive) together with condition 2 across all scenarios at once. As printed, the lemma holds only for large; for it is false.
Fin m, Fin n with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ; Lean index is the paper's . First stage and recourse share the same dimension , as on p. 1.SpectralSparsify.Sampling.BernoulliSubset. No measure theory is needed.LinearOptimization.lp_strong_duality, proved on the platform) is a tool for Lemma 3.3. The Chernoff bounds and the structural lemma are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3.3, are welcome.The source is arXiv:1807.00163v2; its printed page numbers equal the PDF page numbers.
Food, blood and pharmaceuticals are perishable: a unit not sold within its lifetime is thrown away. A seller decides each period how much to order, which price to charge, and whether to dispose of stock early. A large stock of old units argues for a lower price and a smaller order.
Optimal policies for fixed-lifetime inventory are hard to characterize: the state is a vector of inventory levels by remaining lifetime (Fries 1975; Nahmias 1982), and later work turned largely to heuristics.
Chen, Pang and Pan (Oper. Res. 62(2), 2014) obtained structural results for the joint ordering, pricing and disposal problem with a positive replenishment lead time. They used L♮-concavity, a notion from discrete convex analysis (Murota 2003) that Zipkin (2008) used to analyze lost-sales inventory systems with lead times. This mission formalizes the paper's result for the case where unmet demand is backlogged.
A product with a lifetime of exactly periods is reviewed periodically over a finite horizon of periods. Orders arrive after a lead time of periods, . Write .
Vectors and L♮-convexity. For vectors , and are the componentwise minimum and maximum, and is the all-ones vector. A set is L♮-convex if and lie in for all and . A function is L♮-convex on if moreover
and L♮-concave if is L♮-convex. The ordered sets are .
Data. The unit costs are (ordering), (holding), (backlogging) and (disposal), all nonnegative, and is the discount factor. The seller chooses the expected demand in place of the price. The price is , strictly decreasing, and the expected revenue is continuous and concave on . The realized demand is , where the noise terms are i.i.d. with mean zero and support in , , and .
State and decisions. The state satisfies , so the state space is . The coordinate is the inventory, net of backorders, with residual lifetime at most , including orders in transit. Each period the seller chooses:
The next state is .
Recursion. The modified profit-to-go satisfies and
In §4 the paper also assumes .
For , , and are L♮-concave in , and . The largest optimal order-up-to level and demand level are nondecreasing in , the optimal price is nonincreasing, and
The largest optimal depletion is nondecreasing, and .
The result. Theorem 1 gives a qualitative description of the optimal policy in a model where no closed form is available. Fresher inventory leads to ordering less and charging more. One more unit of inventory of any age raises the order-up-to level and the demand level by at most one unit. Corollary 1 refines this by age: the order quantity is most sensitive to young inventory, and the price discount is most sensitive to inventory close to expiry. These properties underlie the bounds and heuristics of §6 of the paper.
The formalization. The result is proved in the paper, but parts of the argument are informal: the bound is a coupling argument, existence of optimal solutions is "straightforward to check and thus omitted", and Lemmas 1–3 are stated without proof. A formalization makes the induction checkable and yields a reusable library of L♮-convexity on real vectors with domains, used by the wider family of inventory models built on the same technique. None of these results is known to be machine-checked.
The obvious induction, that each step of the recursion preserves L♮-concavity, fails at the depletion problem (5): its constraint set is not L♮-convex, because of the upper bound , so Lemma 2 does not apply. The bound must first be shown inactive, which needs a quantitative estimate of how the profit-to-go changes when backorders are added, a property of the value function itself.
Lemma 3 handles a scalar decision, while Theorem 1 has a pair and needs the componentwise-largest maximizer; every supremum and expectation must also be shown to be finite.
Carrier. The paper treats at once. The mission formalizes the real case only.
L♮-convexity. Functions are real-valued on an explicit domain set, which is the paper's own convention for "L♮-convex on a set". The submodularity characterization is not used as the definition.
Indexing. States are Fin L → ℝ with , indexed from 0, and the lead time satisfies . The paper's is coordinate of : at it is the decision , and at it is .
Time. Time is counted in periods to go, which is faithful because the data are stationary. f 0 = 0 is . The parts of Theorem 1 about , and decisions cover the decision periods .
Suprema and expectations. Every maximum is sSup of the image of a nonempty feasible set that is bounded above. Expectations are Bochner integrals against the noise law .
Optimal decisions. Largest optimal decisions are hypotheses at the points compared; at , no largest order-up-to level exists in the last period.
Standing assumptions. All the §3 assumptions (nonnegative costs, , strictly decreasing , continuous concave revenue, zero-mean noise with support in , ) are fields of the model structure. The §4 assumption is a hypothesis of every §4 statement.
Corrected slips.
Ruled-out formalizations. Any of the following would trivialize the mission:
The value functions here are the model's own recursion, for every .
What is needed. L♮-convexity on with domains (shifts, sums, expectations, partial maximization, comparative statics for largest maximizers) and integrability of in the noise; all reusable. Proofs of single milestones are welcome.
Source. The source is the published Operations Research article; in the copy held, printed page = PDF page + 282.
A two-stage adjustable robust linear program chooses a first-stage decision before an uncertain right-hand side is revealed, and a second-stage (recourse) decision afterwards, minimising the worst case over an uncertainty set of the total cost. Computing the optimal value is hard in general (Feige et al., 2007), and the standard tractable restriction is to affine policies (Ben-Tal et al., 2004), whose optimal value is computed by a single linear program.
El Housni and Goyal (arXiv:1807.00163v2) show that, when the recourse matrix is non-negative and is a budget of uncertainty set, is within a factor of . Their Section 7 asks whether the non-negativity of is needed, and answers with a family of two-stage lot-sizing instances whose recourse matrix is a network matrix with entries in . On this family the adjustable problem has value while every affine policy costs at least . Lot-sizing and transportation recourse are among the most common uses of two-stage robust optimisation (see Bertsimas and de Ruiter, 2016), so the instance is a natural one, not an artefact.
Lower bounds on the gap between affine and adjustable policies were known before (Bertsimas and Goyal, 2012); the point of the present family is that the adjustable value is exactly , so the ratio is infinite and the difference grows linearly in .
The lot-sizing problem (7.1). There are nodes. Node stores inventory at cost per unit, up to a capacity , and faces an uncertain demand . After is revealed, inventory may be shipped from node to node in amount at cost per unit. A solution is feasible when and, for every ,
The objective is the first-stage cost plus the worst case over of the transportation cost . The optimum over all rules is , and the optimum over affine rules (one row of per arc, one column per node) is .
The family (7.2). Let , and split the nodes into and with . Set on and on , everywhere, for , , and otherwise. The uncertainty set is
Inventory can thus move only from to , at no cost; stocking is free and stocking costs one per unit.
In the Lean development the general problem is the structure LotSizing N E (nodes N, usable arcs E with tail src, head tgt, distances d), with the predicate Feasible, the cost cost, and the sets adjustableValues, affineValues of objective values. The family is lotSizingFamily k, on nodes Fin k ⊕ Fin k and arcs Fin k × Fin k.
For every ,
each stated as IsLeast of the corresponding set of objective values, which asserts that the value is attained and is the minimum. The unboundedness of the gap, , is immediate.
The result. The approximation guarantees of the paper ( for budget sets, for disjoint constrained budgets) assume . Lemma 7.1 shows that this assumption is not a convenience of the proof: with a network recourse matrix no bound on of any form holds, even for a budget set and a bipartite network. Any extension of the guarantees to transportation or flow recourse must therefore change the policy class or add structure, which is the open direction the paper states after the lemma.
Formalizing it. The lemma is proved in the paper; it has not been machine-checked. The mission produces a reusable definition of the two-stage robust lot-sizing problem with arc-based recourse, the precise instance family, and checked versions of the five steps of Appendix D. Two of those steps hold only for and one is printed with its indices swapped (see the scope section); the formal statements make those boundaries explicit.
The adjustable half is a transportation argument, and the affine upper bound is a direct verification of one explicit solution. The substance is the affine lower bound, which must hold for every feasible affine solution, not for a particular one. Comparing an affine policy with the adjustable optimum on a few extreme scenarios gives nothing: on any single scenario an affine policy can match the adjustable cost. What fails for affine policies is simultaneous feasibility over the whole of , and the lower bound has to extract a cost from that requirement alone. It is also sensitive to the size of the instance: two of the intermediate steps of Appendix D are false for , so a formal proof has to treat small separately.
IsLeast. No real infimum is used, so "" cannot hold on an empty feasible set; feasibility includes , on all of , and the coverage constraint at every node, including the outflow constraint (D.2) at .LotSizing (any node set, any arc set, any uncertainty set) can host other two-stage lot-sizing and transportation results. Proofs of any milestone, and alternative arguments for the affine lower bound, are welcome.The source is arXiv:1807.00163v2; its printed page numbers equal the PDF's.
Superconducting circuits built from capacitors, inductors and Josephson junctions are the dominant platform for current quantum processors (Google, IBM, Rigetti, IQM and others). The source article — the Wikipedia entry Superconducting quantum computing — states two facts about the gate model on this hardware that this mission makes precise:
Statement 2 is a mathematical theorem, not an engineering claim: it says that every unitary operation on qubits can be written exactly as a finite product of the hardware's elementary gates. Its classical form with CNOT as the two-qubit gate is due to Barenco et al. (1995); the iSWAP version follows because CNOT can be built from two iSWAPs and single-qubit gates (Schuch–Siewert 2003).
Timeline.
An -qubit register has computational basis states labelled by bit strings ; its operations form the unitary group . For a unitary and a qubit , the single-qubit gate applies to qubit and leaves the others unchanged. For a matrix and an ordered pair of distinct qubits , applies to qubits (qubit is the first tensor factor). Write
The gates used are
in the basis , and the Toffoli gate . Time evolution under a Hamiltonian is , and the coupling Hamiltonian is . A two-level unitary acts as the identity outside the span of two basis vectors.
For every ,
The goal theorem is the formal justification for compiling arbitrary quantum algorithms to superconducting hardware whose native entangling interaction is of XY/iSWAP type: any target unitary, however large, has an exact decomposition into the hardware's elementary operations. Milestone 1 connects the abstract gate to the physical Hamiltonian; milestones 3–4 are the textbook universality theorem in the CNOT form, reusable for any other two-qubit gate that can synthesise CNOT; milestone 5 is the Toffoli construction mentioned in the source.
All results are classical and proved in the literature. To the best of the drafter's knowledge they are not yet available as machine-checked statements in Mathlib in this form; the mission's contribution is a complete formal development.
The naive route — "decompose into two-level unitaries, then implement each with gates" — hides real work: a two-level unitary on basis states with differing in many bits must be conjugated by a Gray-code sequence of controlled-NOT style gates into one acting on a single qubit, controlled on all others, and multiply-controlled single-qubit gates must then be reduced to single-qubit gates and CNOTs. Keeping indices, tensor embeddings and controls consistent over qubits is the main formal burden. Milestone 1 requires computing a matrix exponential exactly, which in Lean means handling NormedSpace.exp on a non-diagonal matrix.
Fin n → Fin 2; two-qubit operators are indexed by Fin 2 × Fin 2 with the Kronecker product ⊗ₖ, first factor = first qubit.Subgroup.closure) inside Matrix.unitaryGroup equals ⊤; no approximation or topological closure is involved, which is why the full continuous family of single-qubit gates is included.onQubit, onPair) and multiply-controlled gates are reusable for any quantum-circuit mission.Grover's algorithm is a quantum algorithm for unstructured search: given black-box access to a function that takes the value at exactly one input , it finds with high probability using evaluations of . It was devised by Lov Grover in 1996 (Grover, STOC 1996). Classically the same task needs evaluations, since there is no better approach than trying the inputs one after the other. Bennett, Bernstein, Brassard and Vazirani showed that every quantum algorithm needs evaluations (BBBV, SIAM J. Comput. 1997), so the quadratic speedup is optimal.
Because many problems contain exhaustive search as a subroutine, the algorithm and its generalization, amplitude amplification, speed up a broad class of algorithms: brute-force attacks on symmetric-key cryptography (a 128-bit key in roughly iterations), algorithms for NP-complete problems such as 3SAT, and black-box problems such as element distinctness and the collision problem.
This mission follows the presentation of the algorithm and of its analysis in the Wikipedia article Grover's algorithm (revision 1373498442), which gives two analyses of the same algorithm, a geometric proof and an algebraic proof, following Nielsen–Chuang 2010, Chapter 6.
Fix . The state space is with standard basis and inner product . Let have exactly one index with .
The algorithm. (1) Initialize the system to . (2) Perform the Grover iteration times. (3) Measure the resulting state in the computational basis; by the Born rule the outcome is with probability .
Two further objects appear in the analysis: the ket perpendicular to , and the angles (geometric proof) and (algebraic proof).
This combines the article's headline claims: the algorithm outputs with probability at least (for ) using applications of , the success probability approaches for , and the number of iterations satisfies . The goal does not fix .
Listed in the article's order.
The result. The goal says that unstructured search over items costs oracle queries on a quantum computer, with failure probability at most for a single run, and hence that the expected number of queries until is found is still . It is the quantitative content behind the use of Grover's algorithm as a subroutine and behind its role in post-quantum key-length recommendations.
Formalizing it. The result is classical and fully proved on paper. The work here is to formalize the article's two proofs: the reflection/rotation picture and the algebraic diagonalization, together with the equivalence of the two oracle models and the explicit bound stated in the article. A separate platform mission, Grover's Algorithm, already contains machine-checked proofs of the amplitude formula and of a success guarantee with iteration bound , in a model where the oracle is given by the marked index. This mission differs in that it derives the oracle from the function , includes the ancilla-based standard oracle, the Householder and reflection statements, the algebraic Jordan-form analysis, and the bound in terms of . The lower bound of Bennett–Bernstein–Brassard–Vazirani (optimality) is out of scope.
None of the steps is deep; the difficulty lies in the bookkeeping. The plane is not spanned by an orthonormal pair, so the matrices of the algebraic proof are in a non-orthogonal spanning set, and the probability formula must be transported from that picture back to the -dimensional state. Passing from the exact formula to the bound requires choosing an integer , controlling to within of , and comparing with to reach . Edge cases matter: (where , is undefined and is singular) and the integer rounding of .
All statements import one definitions file, GroverWiki_Defs, and live in the namespace GroverWiki.
Fin N → ℂ; operators are matrices Matrix (Fin N) (Fin N) ℂ acting by mulVec; the two-register space is indexed by Fin N × Fin 2. Bit values are Fin 2, so ⊕ is addition in Fin 2.f : Fin N → Fin 2; uniqueness of the marked item is the hypothesis ∀ x, f x = 1 ↔ x = ω.x is ‖ψ x‖ ^ 2, applied to the state (U_s U_ω)^r |s⟩.The goal is not trivialized by the model: the state is the actual output of the algorithm, the iteration count is bounded explicitly, and the probability bound is the Born-rule probability of the marked index. Contributions of reusable lemmas on reflections and rotations in two-dimensional subspaces of are welcome.
A sequence of real numbers often arrives as a list of moments: averages of powers of a random variable, traces of powers of a self-adjoint operator, or coefficients of a continued fraction. The Hamburger moment problem, named after Hans Ludwig Hamburger (1920–21), asks when such a list really comes from a measure on the whole real line, and, when it does, whether the measure is determined by its moments. The question sits at the junction of probability (the method of moments, identification of limit laws), spectral theory of symmetric operators and Jacobi matrices, and the theory of orthogonal polynomials; standard monographs include Shohat–Tamarkin (1943) and Schmüdgen (2017).
Timeline (as summarized in the source article and its references):
Let be a sequence of real numbers. A solution of the Hamburger moment problem for is a positive Borel measure on such that every power is -integrable and
The sequence is a moment sequence if at least one solution exists.
The Hankel kernel of is the infinite matrix . It is positive definite (in the sense of the source) if
for every finitary complex sequence , i.e. for all but finitely many . Its finite sections are the Hankel matrices
In the Lean development these objects are IsMomentMeasure m μ, IsMomentSequence m, hankelForm m c, HankelPosDef m and hankelMatrix m n, all in the namespace HamburgerMoment.
The result. Hamburger's theorem turns an existence question about measures into a family of finite-dimensional positivity conditions that can be checked on the data. It is the basic tool behind the method of moments in probability (identifying a distribution from its moments, when the problem is determinate), behind the spectral theory of Jacobi matrices, and behind Gauss quadrature and orthogonal polynomials on the line. The uniqueness criteria decide when moments determine a law; the non-uniqueness examples (for instance the log-normal distribution) show that they do not always do so.
Formalizing it. All results here are classical and proved in the literature; to the best of the captain's knowledge none of them is currently available as a formal statement in Mathlib, which has neither moment problems nor Hankel kernels. The mission produces a reusable vocabulary (moment measures, Hankel forms and matrices) and machine-checked versions of the existence theorem, the uniqueness criteria and the non-uniqueness phenomenon.
The "only if" direction is a direct computation. The converse is the substance: from positivity of countably many finite quadratic forms one must produce a countably additive measure on a non-compact space with all moments matching. Compactness arguments on finite sections give measures whose low-order moments match, but mass can escape to infinity and higher moments need not converge; the source's route instead goes through the Hilbert space completion of finitary sequences, self-adjoint extensions of the (generally unbounded) shift operator and the spectral theorem for unbounded self-adjoint operators — machinery that is only partly present in Mathlib. An alternative route via positive linear functionals on polynomials (M. Riesz extension, Riesz–Markov–Kakutani) has to control the same escape of mass. The uniqueness criterion requires quasi-analyticity or Carleman-type estimates.
m : ℕ → ℝ; measures are Measure ℝ on the Borel σ-algebra of . A solution must have every power integrable, so in particular is finite with total mass .ℕ →₀ ℂ, and the Hankel form is the finite double sum over the support. "" is the order on (the value is a nonnegative real number), matching the source.Fin (n + 1); positive semidefiniteness is Mathlib's Matrix.PosSemidef.Needed infrastructure and welcome contributions: polynomial integrability under finite moments, positive linear functionals on , a Riesz–Markov or spectral-measure construction on , Vandermonde arguments for finitely supported measures, and Carleman / quasi-analyticity estimates. The definitions of moment measures and Hankel kernels are reusable for the Stieltjes and Hausdorff moment problems.
Shor's algorithm is a quantum algorithm that finds a nontrivial factor of an integer in time polynomial in , and its variants compute discrete logarithms in finite cyclic groups. It was developed by Peter Shor in 1994 (Shor, FOCS 1994; Shor, SIAM J. Comput. 1997). No classical polynomial-time factoring algorithm is known; the best classical method, the general number field sieve, runs in sub-exponential time. Because the security of RSA and of finite-field and elliptic-curve Diffie–Hellman rests on the hardness of factoring and of discrete logarithms, Shor's algorithm is the main reason these schemes are considered breakable by a large fault-tolerant quantum computer, and the main motivation for post-quantum cryptography.
This mission follows the presentation of the algorithm in the Wikipedia article Shor's algorithm (revision 1378862216), which describes the quantum part through quantum phase estimation, an approach due to Kitaev (Kitaev 1995) and standard in textbooks (Nielsen–Chuang 2010).
Let be integers with . The order is the smallest positive integer with .
Classical reduction. If is even and , then is a nontrivial factor of . Factoring therefore reduces to computing orders.
Quantum order finding. Let and . A state of an -qubit register is a vector in with standard basis . The modular-multiplication gate is the -qubit gate
With , the states are eigenvectors of with eigenvalues . The order-finding circuit acts on a -qubit first register and the -qubit second register: Hadamard gates on the first register, controlled gates for (qubit of the first register controls on the second), and the inverse quantum Fourier transform on the first register. It is applied to and the first register is measured, producing an outcome with probability . Finally the continued fractions algorithm is run on .
For every ,
and for every such some continued fraction convergent of equals in lowest terms, i.e. has numerator and denominator . Summed over , a single run yields with probability at least an outcome from which the continued fractions algorithm recovers some in lowest terms.
The goal is the quantitative statement behind the article's claim that phase estimation "gives as output a random integer of the form " and that a -qubit first register suffices to recover . Combined with the classical milestones, it is the correctness argument of Shor's factoring algorithm, minus the separate number-theoretic estimate of how often a random has even order with , which the article does not state.
The results are classical and their proofs are published. The work this mission asks for is a machine-checked proof against an explicit gate-level model of the circuit — Hadamard tensor power, controlled modular-multiplication gates, inverse QFT — rather than against a closed-form output distribution assumed up front. Related missions on the platform formalize Shor's 1997 paper, which analyses the circuit by a direct Fourier-sum computation with ; this mission follows the phase-estimation route with the article's constants.
The spectral facts about and the classical reduction are short arguments. The main obstacle is the circuit: showing that the product of the controlled gates acts on as multiplication by requires the binary expansion of and the commutation of the controlled gates, and the subsequent inverse QFT must be computed explicitly. The bound requires an estimate of for which is uniform in ; a crude estimate gives a weaker constant. The measurement identity requires the orthonormality of the , which uses that are distinct modulo .
States are coordinate vectors Fin d → ℂ, gates are complex matrices acting by Matrix.mulVec, two-register operators are Kronecker products on Fin d₁ × Fin d₂, and measurement probabilities are sums of squared moduli. The order is orderOf (a : ZMod N) and is Nat.clog 2 N. Convergents are Mathlib's Real.convergent, the standard continued fraction expansion. The goal is a statement about the specific circuit defined in the mission's definition file, so it cannot be satisfied by choosing a convenient output distribution, and the recovery statement is quantified over a fixed , so the trivial convergent (which equals ) does not discharge it for .
Reusable infrastructure welcome from this mission: the action of the Kronecker-product phase estimation circuit on eigenstates, the explicit inverse QFT computation, and the estimate for the Fejér-type kernel.
Generalized complex geometry, introduced by N. Hitchin (Generalized Calabi–Yau manifolds, 2003) and developed by M. Gualtieri (thesis, 2004; Annals 2011), treats complex and symplectic structures as two special cases of one notion. It replaces the tangent bundle of a manifold by the generalized tangent bundle and an almost complex structure on by an orthogonal almost complex structure on . The framework is used in string theory: supersymmetric flux compactifications require (possibly twisted) generalized complex structures (Graña 2006).
The pointwise theory is pure linear algebra, and the global statements of the subject rest on it: the equivalence between a generalized almost complex structure and its -eigenbundle, Gualtieri's classification of maximal isotropic subspaces by pairs , the type invariant and its behaviour under B-field shifts, and the two model examples (complex and symplectic). This mission formalizes that linear-algebraic layer as presented in the Wikipedia article Generalized complex structure.
Fix . A fiber of the tangent bundle is ; its dual is identified with through the standard dual basis, so a one-form acts by . The generalized tangent space is , whose elements are formal sums , with the natural inner product of signature
The same formula defines a complex bilinear form on the complexification , which carries the complex conjugation .
For every generalized almost complex structure , its eigenbundle satisfies
and conversely every complex subspace satisfying (i) and (ii) is the -eigenbundle of a unique generalized almost complex structure. Hence (i), (ii) form an alternative definition of generalized almost complex structure.
The goal makes the two descriptions of a generalized almost complex structure interchangeable: integrability (closure of under the Courant bracket), the canonical pure-spinor line and the type are all phrased in terms of , while the definition is phrased in terms of . The classification by is the normal form behind the type, the local classification near regular points, and the identification of the complex and symplectic extremes. All of these results are classical and proved in the cited literature; the remaining work is their machine-checked formalization. A formal library of this linear algebra is a prerequisite for later missions on the manifold-level theory (Courant bracket, generalized Darboux theorem).
The goal mixes real and complex linear algebra. Recovering a real map from a complex subspace requires knowing that is the whole complexification and that the map which is on and on commutes with conjugation and is orthogonal; each of these uses hypotheses (i) and (ii), and the dimension condition cannot be dropped. The classification needs a dimension count for (functionals on versus the annihilator of ) and, in the converse direction, the extraction of from an arbitrary maximal isotropic subspace. For the complex example, the type computation requires the dimension of the -eigenspace of a real complex structure, which is exactly .
Everything is fiberwise and in coordinates: is Fin N → ℝ, is GIdx N → ℝ with GIdx N = Fin N ⊕ Fin N (vector part on Sum.inl, one-form part on Sum.inr), endomorphisms are matrices over GIdx N, and the complexification is GIdx N → ℂ with the real matrix acting through . 2-forms on are skew matrices with ; 2-forms on a subspace are skew bilinear forms on . Nondegeneracy of is (the inverse used in is the matrix inverse). The type uses the article's real-dimension convention, so it is twice Gualtieri's complex type. The classification milestones are stated over RCLike fields, i.e. for both and , as in the article.
Out of scope for this mission: the Courant bracket and integrability, the canonical (pure spinor) bundle, upper semicontinuity of the type, the generalized Darboux theorem, local holomorphicity, and the -structure description. These need manifold-level infrastructure (Lie derivatives and exterior derivatives of forms on manifolds) and are left for later missions.
The AdS/CFT correspondence (Maldacena 1997) relates quantum gravity on anti-de Sitter (AdS) space to a conformal field theory (CFT) living on its timelike boundary. Gubser–Klebanov–Polyakov and Witten gave the CFT-from-AdS direction of the dictionary: CFT correlators are computed from bulk Green functions. Giddings (PRL 83, 2707, 1999) supplies an entry in the reverse direction. Because AdS confines particles and has no ordinary asymptotic states, a flat-space S matrix does not exist; the paper defines a boundary S matrix from in/out states built out of wave packets incident from the boundary, derives an LSZ-type reduction formula (eq. 42), and concludes that the boundary S matrix equals the boundary CFT correlator (eqs. 44–45).
Every step of that argument rests on the classical theory of the free Klein–Gordon field on global AdS: the parameters (eq. 4), the discrete normalizable spectrum with modes behaving like at the boundary (eqs. 5–7), the non-normalizable modes behaving like (eqs. 8–9), and the boundary limit (eqs. 19–20) that fixes the normalization of the bulk–boundary propagator.
Fix an integer , an AdS radius and a scalar mass . Global has metric (eq. 2)
Define (eq. 4)
A mode , with a spherical harmonic on , solves the free equation (eq. 3) exactly when the radial profile satisfies, on ,
A normalizable mode is a nonzero solution that is bounded as (regular at the centre of AdS) and has finite Klein–Gordon norm, i.e. . The explicit modes of eq. (5) are
with the Jacobi polynomial, and the eigenfrequencies of eq. (7) are .
For every , and radial profile ,
The goal is the precise mathematical content behind the paper's statement that free solutions "exist at arbitrary frequency but are only normalizable for a discrete set of frequencies". This spectrum is what makes the boundary operators of eq. (25) act as creation and annihilation operators (eqs. 27–29), and the boundary exponents and the constant determine the normalizations in eqs. (20), (21), (28) and (29). The physics derivation of eqs. (28)–(42) is not rigorous mathematics; milestone 8 isolates the final step from (42)–(43) to (44), which is an exact identity about integral kernels.
The radial results are classical (the paper attributes the explicit solutions to Balasubramanian–Kraus–Lawrence). This mission asks for machine-checked proofs of these results, together with the reusable Jacobi-polynomial and boundary-asymptotics infrastructure they require.
Verifying that solves the equation is a computation. The goal's converse direction is the hard part: one must show that a solution regular at can have finite Klein–Gordon norm only when equals some , and that it is then unique up to a scalar. This requires controlling both regular singular points and of the radial equation, including the resonant cases where or is an integer and logarithms appear. Since forces , the branch is never square-integrable, so the second quantization available for does not arise.
Real.rpow; on the relevant range.