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?
Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length , not with the amount of distinct content. The number of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to for a sampling step , which defeats the purpose on repetitive data.
Timeline.
A text is a sequence over the alphabet whose last symbol T[n]=\=1SA[1..n][1..n]T[SA[p]..n]SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that is read as . The LF mapping is the counting formula , where counts BWT symbols smaller than and counts copies of in .
A run is a maximal block of equal consecutive BWT symbols, and is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most positions are sampled. Definition 3 cuts into phrases that begin exactly at the sampled positions. For a text position , the phrase head of is the greatest sampled position . The permutation (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are and . A text position starts a phrase of when is the first position of a run.
Let , let be the phrase head of , let , and let be the sample stored at . Then
and , respectively, so that is defined.
A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both and a non- symbol contains an occurrence of at the first or last position of a run.
The goal says that the numbers , one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval of a pattern, it lets an index list all occurrences in space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for and in §5.
The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the -index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.
The obvious argument follows the three cells backwards under LF for steps. It rests on two facts that are easy to state and not routine to prove. First, must be derived from the counting formula : this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]T[i+1]i\le k[1..k]T[i+1]T[i]qk-i$ must be tracked through natural-number arithmetic.
Positions are 1-based natural numbers, as in the paper. and are functions read only on . is a hypothesis, IsSuffixArray: it maps injectively into and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1ISA[i]0iDSADISA$ are integer-valued.
Pins and guards:
The space and time claims of Lemmas 2–3 and Theorem 1 ( words, time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding ", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions .
A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and for the left half of the goal.
Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.
The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.
Let be a finite ground set and a family of feasible sets. A fractional point determines a random active set : each belongs to independently with probability . Thus a particular set has weight
A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family . As active elements arrive, it accepts an element when adding that element to those already accepted remains in . In a randomized scheme, the choice of is random and independent of . The family contains the empty set, as the procedure begins with no accepted elements.
An element is selectable for a realized active set and family if every with still permits : . This condition covers every possible set that might have been accepted before arrives. A greedy OCRS is -selectable for a relaxation when the probability of this event is at least for every and every . The probability includes both draws when the family is randomized. Here and .
For two feasible families , the combination of their greedy OCRSs independently draws and , then uses . This is a family of sets satisfying both constraints. The proof also uses , the indicator that for every lying in . For selectability itself, .
For , let the first scheme be -selectable and the second -selectable. The mission asks for a greedy OCRS on the intersection with
The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.
The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same bound for that specific scheme. The earlier milestones record the two order properties of and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.
The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter , their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.
Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.
The obvious argument would multiply the two probabilities that is selectable for the separate families. Both events depend on the same active set , so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.
The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound . The scale and selectability parameters belong to . The point ranges over , not over an independently chosen intersection of scaled sets, so the case retains the paper's meaning. The finite products define the law of ; no measure-theoretic integral is used.
A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.
The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.
Large network games can be described by a graphon, a measurable kernel that assigns an interaction weight to each pair of players in a continuum. This representation is useful when a finite network is viewed as an approximation to a limiting network. A basic question is whether a small change in interaction weights can cause a large change in equilibrium behavior. Carmona, Cooney, Graves, and Laurière answer this question for a static game with real actions, noisy player states, and costs coupled through an aggregate state. Their static graphon games paper establishes existence and uniqueness under different hypotheses, and Theorem 3.20 gives an explicit stability estimate under its contraction condition.
The mission isolates that stability estimate and the results on which it depends. It belongs to the same development as the paper's existence theorem, but has a narrower question: how sensitively does the equilibrium respond when one graphon is replaced by another? The paper later studies finite-player approximations, for which understanding the limiting graphon game's equilibrium is useful. Those later approximation theorems are outside this mission.
The player set is with Lebesgue probability measure. Every player chooses a real action. A strategy profile assigns an action to almost every player and belongs to . Profiles that differ only on a null set represent the same strategy.
A graphon is a symmetric, real-valued, measurable, square-integrable function on . It defines an integral operator on by
Its norm is the -to- operator norm. In particular, interaction weights are allowed to be negative and are not restricted to . A second graphon has operator , and is the operator norm of their difference.
A player's state is , where is the player's action, is an aggregate state, and has a common centered probability law with finite second moment. Assumption 1 bounds squared changes in by times the squared action change plus times the squared aggregate change. For a profile , its aggregate is the solution of
Proposition 3.1 states that this aggregate exists and is unique when . This equation is the deterministic aggregate obtained from the paper's continuum model.
The expected cost of action at aggregate is . Assumption 4 says that is continuously differentiable and uniformly -strongly convex, and its action derivative changes at most when the aggregate changes. The best response minimizes this cost pointwise. A Nash equilibrium is an profile whose action minimizes for almost every player. Assumption 5 adds the uniform bound .
The first targets are the unique aggregate of Proposition 3.1, the best-response bound of Lemma 3.7, and the aggregate bound (15) of Lemma 3.16. Together these support the uniqueness condition in Proposition 3.17:
Lemma 3.19 then bounds the change of aggregate when the same profile is placed in two graphons. The goal, Theorem 3.20, concerns an equilibrium for and any equilibrium for :
Here satisfies both and (17), while is required only to satisfy . The displayed coefficient is the paper's expression, including its common factor.
The theorem gives a quantitative guarantee: as long as the original game's contraction condition holds, the distance between equilibria is controlled by the operator distance between graphons. The bound identifies how state sensitivity , cost sensitivity , strong convexity , and the state bound enter that guarantee. The result also separates two questions: whether an equilibrium exists for a changed graphon, and how far any such equilibrium can lie from the original one.
The mathematical theorem is proved in the paper; the Lean goal is open. A complete formal development would establish the integral-operator estimates, the aggregate and best-response regularity results, the unique equilibrium under (17), and finally the stability inequality. The definitions of real-valued graphons, aggregates, and their extended-valued operator norm can support later work on graphon games beyond this particular estimate. The paper's §4 finite-player results, including Theorems 4.3, 4.7, and 4.9, are not posed here.
An equilibrium is a fixed point of a response to an aggregate, so changing the graphon changes both the aggregate and the equilibrium profile. A direct comparison of costs at two equilibria does not by itself separate these effects or yield the printed constant. The aggregate is defined only as an equivalence class, while its equation and pointwise best responses use representatives. The formalization must keep those almost-everywhere statements aligned with the operator norm estimate. It must also retain the paper's asymmetric hypotheses: (17) is assumed for the original graphon, while the second graphon is allowed to have any Nash equilibrium under its own aggregate condition.
Lean uses unitInterval with its volume measure for , real actions, functions with MemLp for profiles, and almost-everywhere equality for profiles and aggregates. IsGraphon includes measurability, symmetry, and square integrability. IsAggregate records equation (6) and membership in . The integral cost is computed from , , and rather than supplied as an unrelated function. Assumptions 1, 4, and 5 are explicit; the centered noise law is part of the standing model. Lemma 3.7 is stated for an arbitrary cost satisfying Assumption 4, as on the page.
The paper defines equilibrium through a best-response map on a rich Fubini extension. Proposition 3.6 identifies that with the almost-everywhere pointwise minimization condition under Assumption 4. The mission uses that equivalent condition as its equilibrium predicate. This is a disclosed model choice because the Fubini extension itself is not formalized. A best response is selected by classical choice; Assumption 4 gives the minimizer that makes the selection meaningful.
Norm inequalities use extended nonnegative reals. For a square-integrable graphon, its operator norm is finite, and real hypotheses use that finite value. The operator norm is never a real supremum with a default value for unbounded inputs; an equilibrium always includes an aggregate; and an infinite left-side norm is never converted to zero. These choices prevent the stability claim from becoming empty at a bad input. Contributions to the integral-operator infrastructure, the existence and uniqueness of aggregates, and the five named milestones are all within scope.
First order primal–dual algorithms are used when a linear program is too large for a direct factorization or when matrix operations are cheaper than solving a sequence of linear systems. Their basic guarantees often bound an averaged duality gap by a quantity proportional to after steps. A restart discards the current inner iteration history and begins again from an averaged output. For problems with a suitable error bound, restarts can turn sublinear progress into geometric decrease in distance to the solution set. Applegate, Hinder, Lu and Lubin analyze this mechanism for a class that includes proximal point, extragradient, primal–dual hybrid gradient and ADMM methods, with constants listed in their Table 1. Their adaptive rule is useful when the sharpness constant is unavailable to the algorithm designer. Applegate et al., arXiv:2105.12715v4, §§2–4
Let and be closed convex sets. The primal–dual problem is , where is differentiable, convex in and concave in . A point is feasible when . Its saddle-point set contains the feasible pairs satisfying for every and . Distances and balls use a chosen seminorm ; this matters for methods whose natural geometry is degenerate. Applegate et al., arXiv:2105.12715v4, pp. 2–3
For , put . The normalized duality gap is . At it is the upper limit as positive radii decrease to zero. The gap can be infinite under a seminorm, so its values are extended real. A problem is -sharp on when for every and every . This condition connects a computable local gap to the distance of interest. Applegate et al., arXiv:2105.12715v4, pp. 3, 11, (4), Definition 1
The base algorithm begins at and supplies averaged outputs for positive inner times . Property 3 requires constants , uniform over every feasible start and output run, for which , , and . An outer run starts at , runs its inner algorithm for steps, and sets . Its first length is selected by the user. At later outer indices, it restarts at the first positive time when the normalized gap has fallen below times the gap at the previous outer transition, with . Applegate et al., arXiv:2105.12715v4, pp. 9–10, 15–16, Property 3, Algorithm 1, (30)
The goal is both parts of Theorem 2. Assume all outer starts lie in one set on which the problem is -sharp, with . Define the ceiling time . For every the target is
The milestones are Proposition 8's treatment of zero displacement, the displayed restart comparison in the proof of (33), the bound (33) itself, and the repeated normalized-gap inequality in the proof of part (ii). Each is tied to the arXiv version's printed page and label. The assertion begins at : the first interval is free and need not be at most . Applegate et al., arXiv:2105.12715v4, pp. 17–18
The first conclusion gives a uniform bound on the inner work of every subsequent adaptive interval. The second translates the gap-based restart rule into a geometric distance guarantee while retaining the user-selected first interval as a visible factor. Together, they explain why an algorithm that does not know can have the same characteristic restart scale as one using a fixed frequency chosen from . The paper proves this theorem and gives linear-programming settings in which its sharpness premise holds; this mission asks for a machine-checked statement and, eventually, a machine-checked proof of that known result. Applegate et al., arXiv:2105.12715v4, Theorems 1–2 and Lemma 5
Formalizing the result also produces reusable interfaces for saddle sets, seminorm distances, localized duality gaps, uniform algorithm properties, and first-trigger restart runs. Those interfaces can support other primal–dual analyses without committing to a particular inner update map. A complete proof can later connect Property 3 to the paper's individual algorithms, while this mission preserves the abstract theorem that they share. Applegate et al., arXiv:2105.12715v4, Proposition 4 and §4
The restart test uses a gap evaluated at the moving radius , whereas sharpness relates a gap at the radius of the previous outer transition to distance from . This mismatch must be reconciled while preserving the exact ceiling constant. A zero seminorm displacement is a separate boundary case: sharpness only speaks about positive radii, but the algorithm can still encounter radius zero. The theorem also needs the first qualifying time; knowing merely that a later time satisfies the test gives no upper bound on the interval length. Applegate et al., arXiv:2105.12715v4, pp. 16–18
Lean represents and by finite-dimensional Euclidean spaces and by their product, allowing either dimension to be zero. The geometry on that product is an explicit Seminorm, never the product type's default norm. is the set of saddle pairs. The standing problem predicate includes closed convex feasible sets, separate convexity and concavity, and differentiability on the whole ambient product space. It also requires , a disclosed strengthening of the paper's standing feasibility and finite-optimum assumptions so the real-valued distance to cannot collapse to an empty-infimum default. The infimum defining distance is over saddle points only; the supremum defining the gap is over feasible pairs only. The normalized gap and diameter use extended reals so an unbounded seminorm ball does not silently acquire value zero. Applegate et al., arXiv:2105.12715v4, pp. 2–4
The base method is a relation from a start to possible averaged-output sequences. Property 3 fixes before quantifying over starts, runs and positive times. The theorem assumes initial feasibility; Property 3 then makes restarted outer points feasible. An adaptive run records the positive first interval and the first qualifying positive time for each later interval. The ceiling is Nat.ceil; the factor is division in the reals. A formalization with arbitrarily chosen qualifying restart times, sharpness only along one chosen trajectory, a real-valued supremum over an unbounded ball, or a vacuous solution set would change the result. Contributions to the gap and seminorm infrastructure and to either half of Theorem 2 are useful; the individual algorithm implementations are outside this mission's core. Applegate et al., arXiv:2105.12715v4, pp. 9–10, 16–18
Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, , is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty exceeds the input-smoothness constant of the loss: the Lipschitz constant of . For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.
A layered network of depth has widths (pre-activation of layer ) and (output of layer ), with the input dimension and the number of classes. Its parameters are weight matrices , and each linear layer is followed by a nonlinear operation (an activation, possibly combined with pooling). The output of the first layers is
and its Jacobian in is . All spaces carry the Euclidean norm , and is the -operator (spectral) norm.
Assumption E. For , the map is -Lipschitz for , its Jacobian is -Lipschitz from to , and . From these constants define
The classification loss is the softmax loss with , for a class .
Under Assumption E, for every class and all inputs ,
Under Assumption E, for ,
In the order the paper's proof uses them: Lemma 6 (the chain rule for , recursively and as a product); Proposition 5, first part; the telescoping representation (34) of ; Proposition 5, second part; the softmax constants of §B.9 (gradient , Lipschitz constant , smoothness constant ); and the recursion of §B.9 for with its instance for a softmax output layer.
Corollary 4 converts the abstract hypothesis of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: , computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.
The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.
The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on needs both a bound on , which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly of (21), whose definition uses quotients by . For the corollary, the softmax loss must be shown to have Lipschitz constant (a supremum that is not attained) and a -Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.
EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.l is the paper's layer (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index . Widths vary with the layer; they are not collapsed to a single dimension.Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.
Linear programs at very large scale are increasingly solved by first-order primal-dual methods, which use only matrix-vector products instead of matrix factorizations. Such methods parallelize well and have a small memory footprint, but on their own they are slow to reach moderate or high accuracy. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715, Math. Program. 2022) showed that periodically restarting a primal-dual method from the average of its iterates turns its sublinear ergodic rate into a linear rate on sharp problems, a class that contains every linear program. The analysis underlies PDLP, a restarted PDHG solver studied computationally by Applegate et al. (arXiv:2106.04756) and shipped in Google OR-Tools.
This mission formalizes the paper's first convergence theorem: with restarts at a fixed frequency, the distance from the restart points to the solution set shrinks by a factor per restart.
Let and be closed convex sets and let be differentiable, convex in and concave in . Problem (1) is
with feasible region and primal-dual points . Its solution set is the set of saddle points : for all , . Throughout, .
Distances are measured in a semi-norm , which the paper allows in order to cover ADMM. Write , , and . The primal-dual gap (3) at is , and the normalized duality gap (4a)–(4b) is
By Definition 1, problem (1) is -sharp on if for all and all .
The base method is abstract. From a start it outputs averaged points , . It has Property 3 with constants if, for every start and every , and
i. ,
ii. .
Algorithm 1 with fixed-frequency restarts (29) runs the base method from for
steps, sets , and repeats, with .
If the base method has Property 3 and (1) is -sharp on with , then for every
Proposition 2 (p. 8) and Proposition 4 (p. 10) show where Property 3 comes from. A generic algorithm (6) with iterates and targets has Property 1 with if for every (12). It has Property 2 with if or .
Fact 1 (p. 11), that is non-decreasing in , is included as well.
Theorem 1 converts any primal-dual method with an ergodic rate on the normalized duality gap into a linearly convergent method on sharp problems. The rate is iterations to reach (Remark 3). Through Proposition 4 it applies to PPM, EGM, PDHG and ADMM. Combined with the paper's Lemma 5, which shows that linear programs are sharp with the inverse of a Hoffman constant, it yields linear convergence of restarted PDHG for LP. The paper also shows that this rate matches a lower bound for a general class of primal-dual methods.
The result is proved in the paper. As far as is known, no part of it, and no normalized duality gap or primal-dual sharpness notion, has a machine-checked proof. The mission adds a checked version of the restart argument, with every degenerate case resolved: zero displacements, unbounded balls, and semi-norms that are not norms.
Each proof is short, but the statements are delicate in ways the paper passes over.
A direct contraction argument that applies sharpness at an arbitrary radius, or on all of , does not prove the theorem as stated.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). and are allowed.Seminorm ℝ on their product, never the product's built-in norm.EReal, so unbounded sets give and not a junk . is a real infimum over the nonempty set .Standing assumptions and added hypotheses:
Departures from the page:
The goal is not trivialized by its hypotheses. A companion check file exhibits on , with the sup norm and an oracle base method, on which every hypothesis of Theorem 1 holds and . Sharpness is assumed only where Definition 1 and the theorem assume it: replacing by , or the radius range by all , would weaken the theorem.
A complete development needs elementary facts about suprema in EReal, Jensen's inequality for convex-concave functions on averages, and geometric sums. The definitions of , sharpness and Property 3 are reusable for the adaptive-restart theorem of the same paper (Theorem 2, a separate mission) and for other restart analyses. Proofs of any milestone or companion are welcome.
Posted prices turn an offline allocation problem into a sequential choice process: each agent sees a menu of outcomes and prices, then chooses an outcome without revealing its full valuation. The balanced prices framework of Dütting, Feldman, Kesselheim, and Lucier gives welfare guarantees by comparing the revenue collected from an allocation with the welfare that remains feasible after it. Its appeal is that the comparison can be checked in a deterministic full-information setting before any probability distribution over valuations enters the analysis. Dütting et al., 2020
One valuation class at a time would make that framework difficult to reuse. Combinatorial auction valuations are often built by taking pointwise maxima of simpler valuations or by adding values from separate markets. Section 5 of the paper asks whether a price construction balanced for the simple class remains balanced after these operations. Theorem 5.3 gives the maximum closure result; Theorem 5.4 gives addition across markets. Appendix B extends both to the weaker balancing condition used elsewhere in the paper. Dütting et al., 2020, §5 and Appendix B
There are agents in a fixed order. Agent receives an outcome from a space containing a null outcome. A profile is feasible when it lies in . The model assumes downward closure: removing the outcomes of any group of agents from a feasible profile keeps it feasible. For a set of agents , write for the profile retaining on and assigning the null outcome elsewhere. The prefix retains only the agents before . Dütting et al., 2020, §2
A valuation profile assigns each agent a function . The welfare of is . Every base valuation takes values in , the normalization stated in §2. For any set of profiles, denotes the best welfare achievable in . An allocation rule ALG chooses a feasible profile from a valuation profile. A pricing rule assigns a nonnegative, possibly infinite price to outcome when the partial profile is ; an infeasible extension has infinite price. Dütting et al., 2020, pp. 547–548
An exchange-compatible family specifies a set of comparison profiles for each profile . It is exchange compatible when replacing any one coordinate of by the corresponding coordinate of any gives a feasible profile. This property is required for every in the full outcome space. A rule is -balanced for valuation , ALG, and that family, for constants and (Definition 3.1), when both inequalities hold for every feasible and every :
The maximum extension of a base valuation space consists of nonempty finite pointwise maxima of elements of . A base profile supports an extended profile at if at every outcome and for every agent. ALG is consistent when whenever supports at . The optimal allocation rule has this property by Lemma 5.2. Dütting et al., 2020, p. 554
The goal is Theorem 5.3. Given one exchange-compatible family and a collection balanced for every base profile, consistency of ALG preserves the same constants for every extended profile and every corresponding supporting base profile:
The milestone list records the welfare supremum comparison and the two price inequalities in the paper's proof. The family remains the same for all base and extended profiles. Dütting et al., 2020, Theorem 5.3 and proof
Theorem 5.4 treats separate allocation problems. The joint outcome and feasible set are products; values and prices add across components; ALG applies each component's rule. It asserts balancedness with the same and . Appendix B changes the second balancedness bound to and requires strong consistency for maximum closure. Theorems B.2 and B.3 preserve under maxima and addition, respectively. Dütting et al., 2020, Theorems 5.4, B.2, B.3
The maximum closure theorem lets a balanced-price construction for a simple valuation class cover finite maxima of that class without worsening its balancing constants. The addition theorem lets separately priced markets be combined by summing prices. Together these two operations account for the XOS composition discussed immediately after Theorem 5.4; the paper uses the results to connect its general framework to combinatorial auctions and multidimensional matroid settings. Dütting et al., 2020, p. 555
These results have paper proofs. The work here is to state their exact deterministic content in Lean so later formalizations of the price constructions can import the closure theorems. The definitions of supporting valuations, exchange-compatible families, and extended-real prices are reusable beyond this mission. The companion statements keep the product-market and weak-balancedness variants alongside the central theorem, while their proofs remain to be formalized.
For maximum closure, the prices are indexed by a base profile but must be balanced for a different profile that is pointwise larger. A supporting profile agrees with only at ALG's outcome , while condition (a) refers to , an outcome ALG chooses for a different input, and both conditions refer to optimal welfare over , where and can differ. Balancedness of for therefore says nothing about on its own; without a hypothesis tying ALG's choices for and together the statement is false, which is why consistency (Definition 5.1) is part of the theorem. The formal statement must keep the real-valued optimum meaningful for maxima of base valuations, so the normalization of §2 is carried through to . Dütting et al., 2020, Definition 5.1 and Theorem 5.3
For addition, a direct product of the component comparison families has an edge case: a component family can be empty while another is nonempty. The paper's displayed product family then makes the lower balancedness inequality too strong. The theorem statements ask for an exchange-compatible family to exist, as the printed theorems do; they do not require that failing product family. This discrepancy is recorded for review. Dütting et al., 2020, proof of Theorem 5.4
Agents and markets use zero-based finite indices; the paper writes agent indices from one. A profile's prefix contains exactly the agents with smaller indices. Valuations are functions to with base values in . The maximum extension uses a nonempty finite set of base functions, so its maximum is defined at every outcome. Optimal welfare is a real supremum; bounded valuations keep it finite, and the empty set has value zero. Prices are extended nonnegative reals so is retained. The lower balancedness inequality embeds its real right side using ofReal, which handles a negative lower bound consistently with nonnegative prices. The upper inequality keeps the price sum in extended reals.
The maximum theorem quantifies over every extended profile and every supporting base profile, including genuinely new maxima. It keeps one exchange-compatible family for all valuations. The maximum-closure theorems require every base price to satisfy the pricing-rule condition and conclude it for the supporting price. ALG feasibility is assumed on , which contains the base profiles. The product theorems construct joint outcomes, additive values, componentwise ALG, and summed prices from the component data; they do not admit an unrelated joint allocation rule. Downward closure and a zero price for the null outcome at feasible partial allocations are included for the product statements. The latter is a disclosed assumption satisfied by the paper's pricing examples and needed to handle empty component families. No distribution or posted-price run is part of this deterministic mission. Lemma 5.2 and the strong-consistency companion take an optimal rule to be one that attains the welfare supremum over on every profile in , the profiles to which Definitions 5.1 and B.1 apply it; the product companions additionally conclude that the summed prices form a pricing rule (infinite off ). Their ALG feasibility premise concerns the component profiles supplied in the theorem.
The development needs finite dependent products and sums, finite maxima, real suprema of bounded sets, and extended nonnegative arithmetic. Contributions proving the three maximum-closure milestones, the goal, or the product-market companions are all within scope. A proof that specializes the supporting profile to would lose the intended maximum extension and does not satisfy the goal's universal quantification.
A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.
Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.
The hidden state space is and the observation space is with Lebesgue probability measure . The action space is , equipped with the topology inherited from . The state does not move: its transition law is the point mass at for every action. Its continuity in total variation is immediate from this fixed-state behavior.
At hidden state 1 the observation law is always . At hidden state 2, action zero also produces . Under action , state 2 produces a law . The density equals zero on the open left half of each cell in the -part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as grows, and the paper establishes for every fixed Borel set . Thus the observation kernel is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.
A belief assigns a probability to each hidden state. For a current belief and an action , the joint law covers the next state and its observation, and is the observation marginal. A filter is a conditional law of the next state given observation : it satisfies the disintegration identity (3.3). The belief transition is the law of the random posterior when has law . These objects are defined in (3.1)–(3.5) of the paper. Different versions of agree only almost everywhere for each current belief and action, yet they yield the same belief transition.
At the uniform belief , action zero reveals nothing, while every positive-index action produces the same two-point posterior law:
The mission's goal asserts that is total-variation continuous, is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as . It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of , the two posterior values almost everywhere, and the explicit laws of .
The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.
A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.
Setwise continuity controls for each fixed Borel set . A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with , so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of to weak convergence of .
The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of .
Lean represents by Fin 2, with 0 for the paper's state 1 and 1 for state 2; by unitInterval; and by the specified subtype of . Positive integers are a subtype of , so the density and the action are never evaluated at . The measure is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition and observation law use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete and existence of a valid , guarding the universal filter clause against vacuity.
Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of carries the Borel σ-algebra of the weak topology on , stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in for fixed in both structures. Joint measurability in is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.
No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on , or a claim for only one version of would change the counterexample and is excluded by the definitions and goal.
First-order primal-dual methods (PDHG, extragradient, ADMM) are the engine of a new generation of large-scale linear programming solvers, such as PDLP, because they need only matrix–vector products with the constraint matrix. Their textbook guarantees for convex–concave saddle-point problems are sublinear, for the averaged iterate, while in practice restarted variants converge linearly on linear programs. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715v4, Math. Program. 2022) explain this gap through a sharpness condition on the normalized duality gap, and show that restarts turn sharpness into linear convergence.
This mission formalizes the part of that paper which shows that linear programming is sharp: Lemma 5 (p. 15), together with the bound of the KKT residual by the normalized duality gap (Lemma 4, p. 14) and the bilinear results of §3.2. The restart theorems that consume this property are the subject of the companion missions II and III of this series.
Let , , . The standard-form LP and its dual are
and their Lagrangian form is the saddle-point problem
A primal-dual point is , the feasible region is , and is the set of saddle points of on . On the norm is the Euclidean norm , and .
For let . The normalized duality gap (4a) is
The problem is -sharp on a set (Definition 1) if for all and all .
The KKT system (20) collects primal feasibility, dual feasibility and a nonpositive duality gap as , with
The KKT residual is the Euclidean norm of the componentwise positive part, a standard stopping criterion of LP solvers. A Hoffman constant (Hoffman 1952) is a constant with
If (19) has a solution and satisfies (26), then for every the problem (19) is -sharp on with
With :
and their combination, Lemma 4:
Lemma 5 is the input that makes the paper's restart theorems apply to linear programming: combined with Theorems 1 and 2 (missions II and III), it yields linear convergence of restarted PDHG, extragradient and ADMM on any feasible LP, with a rate governed by the Hoffman constant of the KKT system. Lemma 4 is of independent use: it shows that the normalized duality gap, which restart schemes can monitor, controls the KKT residual that solvers report.
The results are proved in the paper. As far as the platform and Mathlib show, none of them is formalized: there is no normalized duality gap, no primal-dual sharpness and no Hoffman bound for KKT systems in Mathlib. The remaining work is to formalize the paper's proofs. Strong duality for standard-form LP, needed for the §3.3 companion, exists on the platform (Polyhedral.lp_strong_duality, LinearOptimization.lp_strong_duality) in a different form.
The sharpness inequality relates two quantities of different nature: is a geometric distance to an implicitly defined polyhedron, while is a supremum of a bilinear gap over a truncated ball that is cut by the constraint . The unconstrained argument of Lemma 3, which identifies with , fails once is imposed, because the ball is no longer symmetric around and the maximizing direction may leave . Control of the duality-gap row of the KKT system also depends on the size of , which is why the constant degrades with and sharpness is claimed only on bounded sets . In Lean the normalized duality gap is an extended-real supremum over a set defined by a non-default norm, so each lower bound requires exhibiting a feasible point of and computing its gap.
Vectors live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and a primal-dual point is a pair. The norm on pairs is the norm of WithLp 2, eucl. The norm instance of the bare product type is the sup norm and is not used: with the sup norm the constants and would describe different statements. and are suprema in EReal. is a real infimum, and every statement that uses it assumes ("(19) has a solution"). is defined as the set of saddle points of on . and are encoded row block by row block exactly as (20) prints them; the page's "" in (18) is a misprint for , which is what (20) encodes.
The Hoffman constant enters only through its defining property (26), quantified over all , together with . Lemma 5 is stated for every such constant. Sharpness follows Definition 1 literally, with ; replacing that range by would be a different statement. A formalization that restricts (26) to , uses the sup norm, or takes a real-valued supremum for would trivialize or change the goal and is ruled out. is the least with an eigenvalue of ; its Lean value for is .
Contributions welcome: proofs of (22) and (25), whose combination gives Lemma 4 and then Lemma 5; general lemmas on suprema over Euclidean balls in WithLp 2 products; and a Hoffman-type existence theorem for , which this mission does not pose. The bilinear statements (Lemmas 2–3) need a minimum-nonzero-singular-value API and are reusable beyond this mission.
The newsvendor problem is the basic single-period inventory decision: a retailer orders units at unit cost before a random demand is observed, sells at unit price , and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.
Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an -th moment for an arbitrary real . This mission formalizes their result that the zero-order phenomenon survives for every such .
Write the critical ratio as . A demand law is a probability measure on . Fix a real and two moments with
The ambiguity set is
the laws on with mean and -th moment . The worst-case expected shortage is
and the robust newsvendor problem (3.2) is
An optimal order quantity is a minimizer of this objective. Two thresholds appear:
In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.
, and
and the two-point law with mass at and the rest at lies in and attains the supremum. 2. Properties of (§2.1, p. 6): is non-increasing and convex, for , and as . 3. Display (3.10) (p. 14): for and ,
Proposition 3.2 shows that for every finite moment order , however high, there is a nonempty interval of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold and the minimum positive order in closed form. For it recovers Scarf's zero-order region. The worst-case law associated with therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).
The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on , of the stop-loss transform , and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.
The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in , including laws with unbounded support and non-integer . The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on . To conclude anything about minimizers on all of , where no closed form is known for general (the dual leads to equations , p. 11), one needs convexity of on the whole line. Inspecting the objective on alone does not determine the global minimizers.
Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.sSup. Under the standing hypotheses , , the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by , so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range in (3.10), which is the paper's standing range of the critical ratio.HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.The Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-80 mission already covers every , the new work is the range from 70 to 80.
The cutoff came down from 90 to 80 in under two days, through moona3k's proofs at 89, 88, 87, 85, 84 and 80. The step to 89 sharpened the estimates of the cutoff-90 argument, and the step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far these methods reach is not known; 70 asks for ten more units. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 70 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryBoundary control of a transport equation acts at the edge of a spatial interval, while the state evolves throughout the interval. A backstepping transformation connects the original state to a simpler target state by integrating against kernels on a triangular region. The transformation is useful only when those kernels exist with the regularity and uniqueness needed to define a single feedback law. Coron, Vazquez, Krstic and Bastin use this construction for a two-component quasilinear hyperbolic system. Their Appendix A isolates a four-component linear kernel system and proves its well-posedness independently of the later stability arguments (Coron et al., Appendix A).
This mission concerns that appendix result. The paper states a generic system broad enough to include the kernel equations arising from its controller design. Its goal is a unique continuous solution on the closed triangle, assuming continuous coefficients and strictly positive transport speeds. The result supplies the existence and uniqueness premise for the paper's later linear and quasilinear stabilization results. It is a proved result in the source preprint; the work here is to state its analytic content precisely in Lean and leave its proof as a formalization target.
Let . There are four unknown real functions on . Two positive, continuous functions describe the characteristic speeds. Four functions supply forcing, and sixteen functions couple the unknown components. The functions and are continuous on . Boundary functions are continuous on . The paper's equations (A.1)–(A.4) have first-order directional derivatives of on the left and on the right (Coron et al., p. 18).
The boundary data have two forms. Components and are prescribed on the diagonal : and . Components and are prescribed on the lower edge with linear dependence on and . For example, . The fourth component uses in the same way. Those edge couplings are part of the problem, rather than optional side conditions.
For merely continuous , a classical partial derivative need not exist. Accordingly, the mission uses the paper's characteristic integral equations (A.23) as the meaning of solution. The travel-time coordinates are for , with . Each characteristic starts on the prescribed part of the boundary and ends at . The value of equals its starting boundary value plus the forcing and coupling integrals along that characteristic. A continuously differentiable solution of the differential equations and the boundary conditions satisfies this integral form (Coron et al., pp. 19–20).
The goal is Theorem A.1: for every set of data with the continuity and positivity assumptions above, there is a continuous characteristic solution on , and any two such solutions agree at every point of :
Four source results mark the path to that goal. Lemma A.3 keeps every characteristic in and records its continuity and coordinate inequalities. Lemma A.4 bounds the integral of the th power of its first coordinate by . Lemma A.5 bounds one application of the linear integral operator to an increment satisfying a factorial estimate. Proposition A.6 bounds the resulting infinite series by (Coron et al., pp. 19, 21–23). These are the mission's four milestones.
Theorem A.1 fixes a genuine mathematical issue behind the feedback construction: a kernel cannot be treated as an arbitrary coefficient of a controller when its defining boundary problem has not been solved. Existence gives a kernel for the transformation; uniqueness makes that kernel determined by the coefficient data. The theorem is stated for a generic coupled system, so the same result can support several kernels rather than just one equation in the control design (Coron et al., Appendix A).
Formalizing this known proof would add a reusable interface for characteristic coordinates, bounded coefficient functions on a triangle, and coupled Volterra-type integral operators. The present proposal contains statements, not completed proofs. The local prior-art search found no published Goursat kernel item with the same four-component system and boundary conventions. The broader paper's linear and quasilinear stability results are separate missions; this one records their analytic kernel prerequisite without importing their controller definitions.
The mixed boundaries make the usual one-direction transport picture insufficient. Two characteristic families enter from , while two enter from the diagonal. Moreover, the lower-edge values of and depend on the other components at that edge. Thus a bound for one component cannot ignore the other three or assume all boundary values are given independently. A candidate continuous solution must also be shown to agree with the same integral equations at the corner and along both boundary segments. The explicit characteristics involve the inverse of , whose argument and range must be checked throughout (Coron et al., pp. 19–23).
The Lean data bundle contains globally defined real functions, with continuity and positivity imposed only on or . Such functions represent continuous data on those closed domains by extension; values outside the domains do not enter the statements. The four components use Fin 4, indexed in Lean for the paper's . The two lower-edge couplings and the two diagonal values are all included in IsCharSolution. Equality in the uniqueness clause is restricted to , because the extensions outside it are unconstrained.
The coordinate inverses are Function.invFunOn on ; only arguments in their ranges have mathematical meaning here. Lemma A.3 includes the domain facts that keep the characteristics in range. Integrals are over finite characteristic intervals with continuous integrands, and the maxima in (A.35) are suprema of continuous images of compact sets, not suprema over all real inputs. Proposition A.6 asserts summability before using an infinite sum. Lemmas A.4 and A.5 include , a valid base case needed by the source's induction. Lemma A.5 makes the continuity of the increment explicit so its integrals retain their intended values. Existence and uniqueness both remain in the goal; retaining only one would change Theorem A.1. Two formalizations would trivialize or falsify the goal and are ruled out: dropping the boundary conditions (A.5)–(A.7) from the solution notion makes uniqueness false, and reading the PDEs (A.1)–(A.4) classically for a merely continuous would make existence false; the solution notion is the paper's characteristic integral form with all boundary conditions. Contributions to the characteristic and operator estimates, continuity of the constructed limit, and the uniqueness argument are within scope.
Least-squares regression, for a tall matrix with , is among the most frequently solved problems in numerical computation. Direct methods (QR or SVD) cost time, which is prohibitive when is in the millions. Sketching replaces the problem by a much smaller one: choose a matrix with , form and , and solve instead. The question is when the solution of the small problem is nearly optimal for the original one.
Clarkson and Woodruff, Low Rank Approximation and Regression in Input Sparsity Time (STOC 2013; JACM 2017), showed that a very sparse random sketch (one non-zero per column, the CountSketch matrix) can be applied in time proportional to the number of non-zero entries of and still yields -approximate regression and low-rank approximation. §7 of that paper isolates the deterministic part of the argument: two conditions on a fixed sketch that guarantee a near-optimal solution, whatever distribution produced .
Timeline. Sarlós (FOCS 2006) introduced sketch-and-solve regression with fast Johnson–Lindenstrauss transforms. Drineas, Mahoney, Muthukrishnan and Sarlós (Numer. Math. 2011) stated the structural conditions for single-response regression (their Lemma 1); Theorem 36 of Clarkson–Woodruff generalizes it to multiple responses. Clarkson and Woodruff then supplied the sparse sketches meeting the conditions in input-sparsity time.
All matrices are real. For a vector let ; for a matrix let . Fix of rank at most , a right-hand side and a sketch . Let be the column space and a matrix with orthonormal columns () spanning .
If is a subspace embedding for with and satisfies the event of Lemma 32 for with error parameter , then every sketched minimizer satisfies
This is the explicit form the paper's proof establishes; the printed bound on norms follows after rescaling .
Theorem 36 separates the algorithm design for sketched regression from its correctness proof: any random construction (CountSketch, subsampled randomized Hadamard transforms, leverage-score sampling, Gaussian matrices) yields a -approximate regression solver once it is shown to satisfy the two conditions with constant probability. Clarkson and Woodruff use it for their input-sparsity-time regression algorithm (Theorem 38) and, through Theorem 39 and affine embeddings, for low-rank approximation. The same conditions recur throughout the randomized numerical linear algebra literature (see Woodruff's survey Sketching as a Tool for Numerical Linear Algebra, 2014).
The results are proved in the paper (§7.3, §7.5 and Appendix A, p. 37). To our knowledge none has a machine-checked proof. Formalizing them produces a reusable, distribution-free layer of sketching theory: the probabilistic statements about specific sketches can then be proved separately and composed with it.
The obvious argument applies the subspace embedding to the residual , but that vector does not lie in , so an embedding of alone says nothing about it; embedding augmented with the columns of instead costs a sketch dimension that grows with . The hypotheses of Theorem 36 control the optimal residual only through the approximate-product condition, which is far weaker than norm preservation, and the difficulty is to transfer that control to the sketched solution (Lemma 37) with the constants and . A second obstacle is the passage from a general of rank at most to an orthonormal basis of : it changes , which is why the approximate-product condition is stated for .
Matrices are Matrix (Fin m) (Fin n) ℝ; squared norms are explicit sums sqNorm and frobSq; the column space is the range of Matrix.mulVecLin; rank is Matrix.rank. Everything is deterministic: is an arbitrary fixed matrix and no probability space appears. The committed conventions are:
A trivializing formalization is ruled out: is never defined as , the approximate-product hypothesis is an inequality and not the exact identity , is non-negative, and the goal is stated for general of rank at most , not only for orthonormal . The hypotheses are jointly satisfiable (for instance ).
A complete development needs the Frobenius inner product and its Pythagorean identity, the normal equations for matrix least squares, the existence of the Moore–Penrose inverse, and the spectral-norm bound for a symmetric matrix from its quadratic form; all are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 36, are welcome.
An intermediary such as a ride platform must attract buyers and sellers who arrive at different times. A buyer may wait for a seller; a seller may wait for a buyer. Both sides can choose when to request a match, so an ask price and a bid price affect participation as well as the intermediary's margin. Chen and Hu study whether a simple posted-price policy remains profitable despite this waiting and the uncertainty of arrivals. Their submitted manuscript proves a finite-market guarantee and an asymptotic rate for the policy used here. The proof appears in its Supplemental Note, while the model and theorem are in the main text.
Buyers arrive during a horizon as a Poisson process of rate , and sellers arrive independently at rate . A buyer's valuation has density on and a seller's cost has density on . Marks are independent of arrival times. A buyer and a seller each trade at most one unit. If they wait after arrival, they incur costs and per unit time, respectively. The paper assumes regularity: the buyer's virtual value and the seller's virtual cost are weakly increasing on their supports. Here .
A clairvoyant assignment knows all arrivals through . For each possible buyer–seller pair it assigns virtual surplus less the waiting cost determined by their arrival order. It chooses a partial matching with greatest total value, denoted . A separate fluid program chooses a measurable, nonnegative pair of price trajectories that clears demand and supply at every time. Its optimal value is . These are different objects: is random and uses indivisible agents, whereas is a deterministic continuous-flow optimum. Lemma 2 of the manuscript compares their values in expectation.
Let be the greatest volume in with nonnegative marginal virtual surplus. The buyer and seller prices are inverse-distribution prices at that volume. Proposition 1 states that these constant prices attain the fluid optimum and .
The greedy matching policy pairs requests first come, first served. Under the waiting-adjusted fixed-price policy, a buyer's posted ask is minus times a conditional expected wait per match probability; the seller's posted bid is plus the corresponding term. The buyer adjustment is conditioned on the observed pre-arrival inventory signal. Agents request immediately exactly when their valuation or cost crosses the base-price threshold. The policy's expected profit is computed from posted prices paid by successfully matched agents.
The first target is the paper's finite-market bound:
When , the benchmark comparison also gives . For scaled systems with arrival rates and , where both exponents are positive, the second target is a constant independent of such that
The milestone list follows the source's Proposition 1, Lagrangian relaxation, Lemma 2, Poisson request counts, policy profit identity, Gallego–van Ryzin moment bound, and Lemma S.5 on arrival-rate monotonicity. The last three supply the finite bound and its scaling statement in the Supplemental Note.
The finite bound quantifies the cost of using fixed base prices and greedy matching instead of the fluid ideal. Its two terms separate the loss from random mismatch and the extra waiting adjustment. The scaled bound says that, as both sides' arrival rates grow, the fraction of the fluid value lost by this policy vanishes at a rate governed by the slower-growing side. This offers a concrete reason to use a simple policy when the market is large, while keeping the smaller-market correction visible.
The paper already proves these claims. This mission asks for machine-checked proofs of their precise statements. The fluid optimizer, the clairvoyant matching problem, the marked Poisson arrival model, and the policy-profit identity are reusable mathematical objects beyond this theorem. The positive-part moment bound is an already published theorem and is referenced rather than posed again.
The obvious comparison between posted-price profit and fluid revenue misses the cost of requests that wait or never match. The price corrections themselves are conditional expectations divided by conditional match probabilities; their effect cannot be captured by simply subtracting a constant waiting charge. The proof must connect those corrections to the time integral of the queue imbalance, then control the imbalance of two Poisson request streams. A second difficulty is that the fluid optimum and the expected clairvoyant optimum are defined through different feasible sets, so their comparison needs a separate relaxation argument. These obstacles are visible in the source's proof of Lemma 2 and Theorem 2.
The density and virtual-value environment is the published bilateral-trade definition, imported through a local name alias required by the frozen shared market module. Lean represents arrivals by independent Poisson counts and independent identically distributed time-and-value marks. This is equal in law to the paper's homogeneous marked Poisson processes on . Arrival time marks are uniform probability laws, and valuation and cost marks use the source densities. Simultaneous requests are ordered by index; such ties have probability zero. The deterministic program ranges over measurable, nonnegative, market-clearing paths with interval-integrable objective terms. Its value is the supremum of their objectives, not a formula involving and ; Proposition 1 must establish that formula. The clairvoyant value uses the published partial-assignment-game worth, so negative-weight pairs may remain unmatched.
The density functions are continuous on their supports, an explicit addition needed for the inverse prices and maximum volume used by Proposition 1. The lower support endpoints are nonnegative so the constant prices belong to the nonnegative fluid price domain; this fills an implicit domain convention in the manuscript. For Theorem 2 the overlap condition is strict, , ensuring positive and . The printed chain comparing and is stated under : when the numerator is negative, the claimed direction fails. Both expectations used as finite numbers are accompanied by integrability conclusions. Division by a zero match probability at the terminal time uses a zero convention on a set of arrival times with probability zero.
The policy model builds in the myopic request behavior that Theorem 1 identifies as an equilibrium; its strategic proof is outside this mission. The policy profit is the expectation of actual posted-price payments, and the waiting compensations are literal tagged-arrival conditional ratios. Contributions that prove the inverse-distribution properties, Poisson thinning, queue profit identity, fluid optimization, or final moment estimate all address parts of the stated target.
Two-sided intermediaries charge buyers and pay sellers while trying to match the two groups. A larger arrival stream on one side changes both the number of possible matches and the prices that clear the market. Chen and Hu study this in a model of buyers and sellers who arrive over time and may wait before requesting a match. Their market-size theorem concerns the deterministic fluid benchmark used to choose fixed prices for the dynamic system. This mission formalizes that theorem from the submitted manuscript, main text §6, rather than the performance of the waiting-adjusted policy itself.
The fluid benchmark matters because it supplies an interpretable price and quantity for each pair of arrival rates. When buyers become more numerous, the model predicts that both the buyer price and the seller payment rise. When sellers become more numerous, both prices fall. In either direction, more arrivals raise the maximum matching quantity and the fluid profit. These claims concern the same valuation and cost distributions as the rates vary, so they isolate the effect of market size.
Buyer valuations lie in , with density and distribution function . Seller costs lie in , with density and distribution function . Write . Buyer and seller arrival rates are and , and the horizon has length . A buyer accepts a fixed ask price when the valuation is at least ; a seller accepts a fixed bid price when the cost is at most . Thus and are the corresponding acceptance rates.
The buyer virtual value is , and the seller virtual cost is . Assumptions 1 and 2 of the manuscript say these functions are weakly increasing on their respective supports. The supports overlap in the sense . The density assumptions ensure that the survival and cost distribution functions have inverse quantiles on . For a candidate volume , the virtual surplus is
The optimal fluid matching quantity is the largest in for which . The corresponding fixed prices are and .
The fluid program (D) permits any measurable nonnegative ask and bid price path on that clears the market at every time: . Its value is the supremum of buyer revenue minus seller payments, integrated over the horizon. Proposition 1 states that the constant path attains this value and that .
The goal is Theorem 3, the eight weak comparisons of prices, volume, and fluid profit. For with fixed, it asserts
For with fixed, the two price inequalities reverse while the volume and profit inequalities retain their directions. The goal leaves the rates and the two distributions as variables, so it states the market-size result across all systems meeting the paper's assumptions.
The milestones follow the source's dependency structure: Proposition 1 identifies the fluid optimizer; the proof of Lemma S.5 notes that decreases in ; Lemma S.5 establishes the volume and profit comparisons; and the two parts of the proof of Theorem 3 compare the fractions and served on the growing side. The paper's proofs are in the Supplemental Note, with related proofs in the Online Appendix.
The theorem gives directional predictions without differentiating optimal prices with respect to arrival rates. A platform comparing two otherwise identical markets can infer which way its fluid ask and bid prices move, whether it matches more units, and whether the benchmark profit increases. Proposition 1 also connects the optimization over time-varying paths to a fixed price pair, so the static claims apply to the entire feasible fluid program.
The result is proved in the manuscript; this mission asks for a machine-checked proof of the same statement. The formal development would make the inverse-quantile construction, attainment of the optimal volume, and the nonempty bounded fluid optimization problem explicit. Those objects can be reused in other two-sided pricing or matching models. This mission does not claim that the corresponding stochastic system has identical comparative statics; the manuscript itself focuses on the fluid regime in §6.
Increasing one arrival rate expands the feasible number of matches, but the two optimal prices do not follow from that fact alone. The buyer price depends on the fraction of buyers served, and the seller price depends on the fraction of sellers served. A growing side can have a larger matched volume yet a smaller matched fraction. The proof must control both quantities under the appropriate inverse distribution function. Profit also needs a comparison of two separate fluid optimization problems, rather than only a comparison of their candidate fixed-price formulas.
The Lean model reuses the published bilateral-trade environment for the two positive densities, interval supports, cumulative distributions, and virtual values. The new definitions clamp both cumulative distributions to their supports so a price outside the support still has the correct acceptance probability. Inverse quantiles are supported level-set infima, used only at arguments in . All rates and the horizon are positive; both densities are continuous on their supports; the virtual functions satisfy the paper's regularity assumptions; and . Density continuity is a disclosed addition needed for the asserted inverse-quantile and maximum properties.
The claims involving the value of (D) assume a nonnegative seller cost support. This disclosed domain correction puts the fixed seller price in (D), whose price paths take values in ; the imported bilateral-trade environment itself permits negative supports. The virtual-surplus and served-fraction inequalities hold without this condition. Every feasible path is measurable, nonnegative on , clears the market at every point of that interval, and has integrable buyer and seller revenue terms. The fluid value is defined as the supremum over those paths. It is never defined by Proposition 1's fixed-price identity, which would erase the optimization claim. The volume set is restricted to , so its supremum has the source's intended domain. The source uses “increasing” and “decreasing” in the weak sense.
Useful contributions include lemmas showing the clamped distributions are monotone, their supported inverses have the stated identities, the candidate volume set has a greatest member, the fluid feasible set is nonempty and bounded above, and the two fraction comparisons. These are substantive mathematical obligations: no arbitrary inverse, empty feasible set, non-integrable path, or preassigned fluid value should satisfy the goal by a default value.
Mode-seeking clustering groups data points by the peak of an underlying probability density that they "flow up" to. Methods of this kind (mean-shift, graph-based hill climbing) are widely used, but their output depends heavily on noise: a density estimated from finitely many samples has many spurious local maxima, and each of them becomes a cluster. Chazal, Guibas, Oudot and Skraba (INRIA RR-6968, 2009; journal version J. ACM 60(6), 2013, doi:10.1145/2535927) combine graph-based hill climbing with topological persistence. Persistence measures how prominent each peak is, and peaks of low prominence are merged into their neighbours. The paper's main guarantee says when this algorithm recovers the right number of clusters from random samples. It holds on Riemannian manifolds that may be non-compact, and the clustering method is now known as ToMATo.
Let be an -dimensional Riemannian manifold, possibly with boundary, with geodesic distance and -dimensional Hausdorff measure . The strong convexity radius is the infimum over of the largest such that any two points of the closed ball are joined by a unique shortest path, and that path stays in the ball. Let be a probability density with respect to that is -Lipschitz, and write for its superlevel sets.
Persistence diagram. As decreases from to , path components of are born at peaks of and die when they merge into an older component. The 0-th persistence diagram records each component as a point of the extended plane , with birth and death ; a component that never dies has . The prominence of the peak is . The diagonal is added with infinite multiplicity. is tame when this structure is of finite type. For , is -separated when every off-diagonal point either has prominence (noise), or has prominence and birth (signal).
Algorithm. The input is sample points , the values , the matrix of distances and parameters . The Rips graph joins two points at distance . The algorithm processes the points by decreasing and keeps a union-find structure whose entries are rooted at their highest point. When a point is processed, every neighbouring entry whose root is less than higher than the point is merged into the point's entry. The point's own entry is then merged into the neighbouring entry with the highest root, if its own root is less than higher than the point. The output is the set of final entries whose root has value .
Sampling quantities. is the least number of closed geodesic balls of radius covering , and .
Assume , is a tame -Lipschitz density, is -separated, and . Then for i.i.d. samples from ,
The theorem gives a sample-complexity guarantee for a practical clustering algorithm, with an explicit failure probability. It needs neither compactness of the manifold nor a density bounded away from zero; dense sampling of one superlevel set is enough. The separation hypothesis is a signal-to-noise condition, and it tells the user which range of recovers the true number of clusters.
On the formalization side, the paper's results are proved on paper, but nothing about them is machine-checked. Of the steps, the paper proves Lemma 4.3 and the region analysis. Theorem 4.5 rests on the Rips-filtration analysis of Chazal–Guibas–Oudot–Skraba, SODA 2009, the interleaving and stability results of Chazal et al., SoCG 2009, and the paper's Lemma 4.6. The algorithm-output step (milestone 6) is asserted in the paper, not proved. The mission therefore asks for formal proofs of all six steps. A by-product is the first library of 0-dimensional persistence diagrams, multi-bijections and Rips filtrations on the platform.
The probabilistic step is a union bound over a minimal cover, but it has a gap. Covering balls need not be centred in , while is an infimum over balls centred in , so the comparison between the two is not justified on a general manifold. Theorem 4.5 is the hardest step. The obvious route, a bottleneck stability theorem, does not apply, because the sample covers only one superlevel set and not . This is why the conclusion distinguishes the quadrant above , where both coordinates are controlled, from the quadrant below, where only births are. Milestone 6 is a correctness proof for a union-find procedure with ties: entries are not path components, because prominent entries stay separate after their components meet.
IsRiemannianManifold, a ModelWithCorners for the boundary), so is dist.Fin n → X. "With probability at least " is an upper bound on the outer measure of the failure event. uses and .No formalization in which the number of clusters is defined as a count of diagram points, or in which the diagram is a free parameter, is acceptable: either one empties the goal. The running-time and memory claims of §3, the basin approximation of Theorem 4.9 and the Morse-theoretic material of §2.3 are out of scope. Lemma 4.3 is stated as printed, with covering balls centred anywhere, and its proof gap is an open risk that Theorem 4.8 inherits.
Contributions are welcome on every milestone. The persistence-diagram layer (rank functions, multiplicities, multi-bijections) and the union-find correctness proof are reusable beyond this mission.
Many constrained optimization problems in operations research have objective and constraint functions that are continuous but not differentiable: maxima of finitely many smooth functions, value functions of inner optimization problems, piecewise-linear costs. For such problems the classical Karush–Kuhn–Tucker theory does not apply directly, and algorithms need a nonsmooth replacement for the condition "the gradient of the Lagrangian vanishes". R. Mifflin's report Semismooth and semiconvex functions in constrained optimization (IIASA RR-76-21, 1976; SIAM J. Control Optim. 15(6), 1977) supplies one. It introduces a point-to-set map built from Clarke's generalized gradients and shows, in §5, that is necessary for optimality of locally Lipschitz problems and, for a class of semiconvex functions, also sufficient as soon as a strictly feasible point exists. The map goes back to Merrill's fixed-point work on differentiable and convex problems; Mifflin's own algorithm for semismooth problems converges to points satisfying , so the sufficiency result says when such points are actual minimizers.
This mission is the third of three on the report. Mission I treats pointwise maxima of compact families of smooth functions, mission II the chain rule for semismooth compositions.
Write for Euclidean space with inner product . For , a point and a direction , the generalized directional derivative is
and the generalized gradient is the set . When exists it is the directional derivative ; is quasidifferentiable at if exists and equals for every .
Let . is semiconvex at with respect to (Definition 2) if (a) is Lipschitz on a ball about , (b) is quasidifferentiable at , and (c) and imply . It is semiconvex on if this holds at every point of . Convex functions and differentiable pseudoconvex functions are semiconvex.
The problem of §5 is to minimize subject to , where . A point is feasible if and strictly feasible if ; is optimal if it is feasible and for every feasible . The map is
and is stationary if and . In Lean these are genGrad, HasDirDeriv, QuasidiffAt, SemiconvexAt/SemiconvexOn, IsFeasible, IsOptimal, Mmap and IsStationary in the namespace MifflinSemismooth.Optimality; is the published ClarkeGradients.Shared.genDirDeriv.
Suppose and are semiconvex on and . Then
The first alternative says the problem is infeasible, the last that it has no strictly feasible point. The theorem carries no constants and holds for any constraint function , not only a finite maximum.
The proof uses, in order: a point with minimizes a semiconvex over (p. 20); on the boundary , the condition yields , , with (p. 20); Proposition 1(b), (p. 3); Theorem 8, for semiconvex on a convex , implies (p. 19); and, if , for every feasible (p. 21).
Theorem 7 (p. 18): for locally Lipschitz , an optimal point is stationary. Theorem 6 (p. 17): for locally Lipschitz , is locally Lipschitz with , where ; semismoothness, semiconvexity and quasidifferentiability on pass from the to , and in the last two cases the inclusion is an equality at points of .
Theorems 7 and 9 together give a nonsmooth Karush–Kuhn–Tucker theory: for semiconvex problem functions with a strictly feasible point, stationarity in the sense of is equivalent to global optimality. For differentiable functions this recovers the sufficiency of the Fritz John conditions for pseudoconvex objectives and constraints (Mangasarian, Nonlinear Programming, Theorem 10.1.1); for convex functions it recovers the saddle-point characterization. Since Mifflin's algorithm produces stationary points, Theorem 9 is the certificate that turns its output into a global minimizer. Theorem 6 lets the constraint stand for a finite system .
The results are proved in the report. None of them, and neither the notion of semiconvexity nor the map , has a machine-checked proof on Prove2Me or in Mathlib as far as the platform search shows; Mathlib has no Clarke generalized gradient. The work is to formalize the known proofs, which also produces reusable facts about (nonemptiness, compactness, the max formula) and about semiconvex functions on convex sets.
The case analysis of Theorem 9 is short; the weight sits in its ingredients. Theorem 8 is the delicate step. Semiconvexity constrains only along directions where , so it says nothing directly about a direction along which does not increase; and a mean value inequality along the segment from to ignores quasidifferentiability and does not determine the sign of . Proposition 1(b) is an attainment statement for a sublinear function whose finiteness rests on the Lipschitz hypothesis, and it fails for the real-valued limsup without that hypothesis. The convex-combination step depends on and being nonempty and convex: the convex hull of a union of two sets need not consist of two-point combinations otherwise. Theorem 7 needs to be closed, which in the boundary case is a statement about the convex hull of two compact sets.
is EuclideanSpace ℝ (Fin n). is a real limsup and equals when the difference quotient is unbounded; every statement therefore has a Lipschitz hypothesis at the points where or is used, and semiconvexity includes "Lipschitz on a ball". is the paper's support-set definition, not the hull of gradient limits. is a relation (HasDirDeriv), never a function with a default value, so Definition 2(c) cannot hold vacuously. "Semiconvex on " means with respect to . "max" is IsGreatest, which asserts attainment. Lipschitz constants are nonnegative reals, which is equivalent to the page's positive constants.
The goal, Theorems 7, 8 and 9 are stated for an arbitrary constraint function ; the paper's is the special case maxConstraint hs with , and Theorem 6 is the bridge. Theorem 9's hypothesis is alone, without feasibility. Theorem 6(c) as printed asserts "for each "; that is false when (, , , ), so it is stated for . A formalization with the hull-of-limits , a junk-valued , a feasibility hypothesis added to Theorem 9, or semiconvexity with respect to a smaller set would prove a different and weaker theorem, and is ruled out.
A complete development needs the basic theory of the generalized gradient (Proposition 1(a), (b)), a Lebourg-type mean value theorem for case analysis along segments, and the finite-max rule. These are reusable beyond this mission, by missions I and II of the series in particular. Proofs of the milestones in any order are welcome, as are proofs of Proposition 1(a) as an auxiliary lemma.
Carbon accounting assigns emissions from a shared supply-chain process to firms that can reduce them. If more than one firm can change the same emissions, charging each firm only a share may leave each with too little incentive to abate. Caro, Corbett, Tan and Zuidwijk study the conflict between avoiding double counting in an emissions ledger and inducing the effort a social planner would choose. Their working paper, published in Manufacturing & Service Operations Management in 2013, states an impossibility result for differentiable, increasing carbon-payment rules. It covers multiple firms, processes, and abatement actions, where a process can be influenced by several firms.
The question matters when a carbon footprint is used as a payment base rather than only as a report. A payment rule changes a firm's private incentive to exert costly effort. The rule may also include transfers between firms, so its incentive effect cannot be judged by looking at a single firm's allocated emissions alone. The paper asks what aggregate marginal payment is necessary if decentralized choices are to reproduce the social first best.
Timeline. Holmström (1982) showed for a team with one joint output and one-dimensional efforts that no budget-balanced sharing rule supports the efficient efforts as a Nash equilibrium (stated in the paper as Proposition 1, p. 11). Charging every team member the full social cost ("charging everything to everyone") is known to restore efficiency, as the paper recalls on p. 12. Caro, Corbett, Tan and Zuidwijk (2012 working paper, 2013 journal version) extend the impossibility to many processes, many abatement actions per firm and an explicit influence structure between firms and processes. They also characterize the linear rules that achieve the first best.
Let be a finite set of firms and a finite set of emission-producing processes. Firm chooses a vector of abatement efforts in , with . The full profile is . Firm 's profit before carbon payments is , concave and componentwise decreasing in its effort. Process 's footprint is , convex and componentwise decreasing in the collective effort, and nonnegative on the feasible box. The functions are differentiable, as assumed in the paper's model.
The influence matrix has entries in . An entry is one when the sum of the partial derivatives of with respect to firm 's actions is negative. The paper treats this matrix as independent of the effort profile. Joint carbon production means that a process has at least two influencing firms: for some , .
The societal cost per unit of footprint is . The social first best maximizes
over the effort box. The paper assumes that this solution is unique and that the effort bound is large enough for the relevant optimum to be interior. The first-best footprint is .
A carbon-based payment rule charges firm as a function of the observed footprint vector , rather than the unobserved effort profile. In the social-planner setting of equation (5), , where is its footprint allocation and the transfers balance: for . A Nash equilibrium is a feasible effort profile where no firm improves by changing its own entire effort vector while the other firms hold theirs fixed. At a footprint vector , the rule double-counts process when .
The goal is Proposition 2, evaluated at the first-best footprint:
The paper defines double counting existentially over footprint levels. Its Appendix A.1 proves the stronger assertion at , which is the target here. The rule remains of the form (5), with balanced internal transfers on the nonnegative footprint domain.
Two source statements form the milestone list. The necessary part of Lemma 7 gives equation (14): at an interior first best that is also a Nash equilibrium, the sum over processes of each footprint derivative times the gap between the firm's marginal payment and is zero, both with and without the influence indicator . Equation (18) says that if aggregate marginal payments do not exceed at , every individual process contribution to that sum is zero. The mission also drafts the sufficient part of Lemma 7 and Proposition 3, which characterizes the linear rules with : they implement precisely when .
Proposition 2 identifies a limit on footprint-based incentives under joint production. With more than one firm able to lower a process's emissions, a differentiable increasing rule that implements the first best cannot keep every aggregate marginal charge at or below the social carbon price. Balanced transfers among firms do not remove that requirement. Proposition 3 supplies a complementary characterization for linear payments, identifying which firms must bear the full marginal charge for the processes they influence. These are results proved in the paper, not open conjectures.
The formalization contributes a precise, reusable model of finite effort profiles, process footprints, unilateral deviations, and coordinate marginal payments. It also separates a global Nash best-response condition from first-order identities, so the necessary condition in Lemma 7 has mathematical content. The listed Lean theorems are draft statements with proof holes; they do not yet have machine-checked proofs. Completing them would formally verify the paper's stated claims under the declared model conventions.
The obstacle is the interaction between a shared footprint and unilateral decisions. A firm's payment derivative with respect to a process footprint is multiplied by that firm's own effect on the process, while the social objective prices the total footprint at . A condition on the sum of marginal payments alone does not specify the charge faced by each influential firm. With several actions and processes, the necessary condition is a sum over process contributions, so it cannot simply be read as a coordinatewise equality without further assumptions. These issues occur even though all effort and process index sets are finite.
Lean represents firms, each firm's action indices, and processes by finite types. Efforts and footprints are real-valued functions. The firm and collective effort boxes are closed coordinatewise intervals, with ; optimality and Nash equilibrium quantify over all feasible profiles or unilateral deviations. Coordinate partial derivatives use one-variable derivatives after replacing the corresponding coordinate. Payment rules are functions on real footprint vectors and “increasing” means componentwise nondecreasing.
The source's sign test for does not name an effort profile. The formalization pins it to every profile in the effort box, matching the paper's use of a fixed influence matrix. Interiority is required only of the named first best. The paper's “without loss of generality” nonempty row and column sums for are omitted because the results do not use them; the strict part of its cost monotonicity is likewise unused. Its participation condition (3) is outside the decentralized game (4) and is not added to Nash equilibrium. Equation (5) and transfer balance are imposed only for nonnegative footprint vectors, as printed. The effort bound and Proposition 3's matrix have distinct names.
The first best is a feasible global maximum, not a default-valued real supremum; Nash equilibrium tests full unilateral deviations, not stationarity. These choices rule out a vacuous first-best target and a first-order surrogate for the game. The supporting definitions of finite effort boxes, coordinate derivatives, social value, and Nash best response are useful beyond the final impossibility statement. Contributions that prove the source's necessary and sufficient conditions, the linear characterization, or the goal against these definitions are within scope.
The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.
The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.
Let be a finite simple graph with vertex set . Let and be subsets of its vertices. The deleted graph retains precisely the vertices outside and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of . Write for the vertex set of the component containing . This interpretation follows the paper's notation on page 320.
A balanced -separator is a set for which each component of contains at most half the vertices of :
The paper introduces this phrase on page 321. Here balance is a property of relative to ; it imposes no bound on the size of . The denominator counts all vertices of , including any that lie in .
A three-part partition of is a triple of pairwise disjoint sets whose union is . A part may be empty. Two parts have no edge between them if no edge of joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every .
The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:
The equivalence is the target, including both directions. It applies even when or is empty. It does not include a bound on .
The main supporting result on page 363 says that nonnegative integers with total and can be divided into three classes, each with sum at most . The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.
Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.
Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.
There may be arbitrarily many components of , although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in , and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold . In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in would allow a walk through and would describe the wrong components.
The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside , including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for when quantifying over components. This shared definition matches the paper's . The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.
Half bounds are written as or in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so is a genuine boundary case. The set may meet ; the right-hand denominator remains . The graph may have no vertices. There is no treewidth parameter or size condition on : adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.
The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.
Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).
In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.
Uncertainty is a probability space , and decisions are made in periods . The natural filtration records what is known in each period, with . An action sequence is , chosen from feasible sets . Period rewards are -measurable random variables and the total reward is .
A policy is a map from outcomes to feasible action sequences. It is adapted to a filtration if the period- action is -measurable; denotes these policies. A filtration with for all is a relaxation of , written . A penalty is a function ; it is dual feasible if for every . For any relaxation and dual feasible , the dual bound
is at least the optimal value (weak duality, Lemma 2.1).
The paper's main source of penalties is Proposition 2.2. Given generating functions depending only on , set
Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards and conditional expectations given .
For filtrations and one common sequence of generating functions , let be the Proposition 2.2 penalty of . Then
With a common generating function, a looser relaxation gives a weaker bound.
Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.
Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance , the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains ; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.
The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.
The obvious argument for (12) compares the two suprema policy by policy: . This fails, because the two bounds use different penalties: for a fixed -adapted policy, and need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.
In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: , where each is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.
Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value arises from an unbounded supremum.
Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are (where the page's difference is undefined) is excluded.
The penalties of the goal are computed from by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise in part (iv) is constructed from and the estimates.
The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.
In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.
For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).
Agent A owns the jobs and agent B owns , with . Every job has a processing time . All jobs are available at time . A schedule is an ordering of all jobs; the machine processes them in that order from time without idle time, so the completion time of a job is the sum of the processing times of the jobs up to and including it.
Each A-job carries a cost function and each B-job a cost function , all nondecreasing (regular). The agents' objectives are the maximum costs
This covers the makespan and maximum lateness of each agent as special cases.
A schedule is nondominated if no schedule satisfies and with at least one inequality strict. The pair of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem asks for , with one schedule per pair. Job precedes job in if comes before in the ordering.
The paper prints the bound . It is off by one: with , unit processing times and , the schedules AB and BA give the two nondominated pairs and . The goal states , the bound the printed argument supports once the first schedule is counted.
The bound places among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).
The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.
The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.
The count is over pairs, , measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound is replaced by and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.
A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.
Multivariate multipoint evaluation asks for the values of one polynomial at points of . Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.
The paper gives two such algorithms. Section 4 works over any ring and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the -variate at a point be read off from the evaluation of a single univariate polynomial at a related point of an extension ring.
Let be a prime and a finite field of characteristic . Fix integers and . Let be a power of with (the paper takes the least such power), and let be a polynomial of degree that is irreducible over . Then:
Three maps connect the problem to :
In the Lean development these are K, R, h, ι (the inclusion ), sigma i (), E, S, sigmaInv i ( on ), gAlpha, phi, pi, gIter () and fStar, in the namespace KedlayaUmans.FrobeniusLift.
For every with degree at most in each variable and every ,
The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate at points one computes the lifts , evaluates the one univariate polynomial at all of them by fast univariate multipoint evaluation, and projects back with . Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth . Corollary 6.3 turns this into an operation count of for every , provided and the characteristic satisfies .
Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for , the canonical-representative projection for ) and splits its proof into the five steps above. The definitions of the rings and , the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).
The obvious attempt is to treat as evaluation at and push it through . This fails: is a unit, not zero, so evaluation at does not factor through , and is not a ring homomorphism. The identity holds only because the polynomial is already reduced modulo , which requires both the degree bound and the fact that raising to the power does not raise the degree of modulo . The second fact depends on being fixed by and on . The equality further needs that does not kill the leading coefficient in , a ring with possible zero divisors. Finally, interpolation must happen in , not a field, which is possible only because the nodes lie in the subfield .
F with [Field F] [Fintype F] [CharP F p], a prime ([Fact p.Prime]). is a polynomial over ZMod p with [Fact (Irreducible P)]; is P.natDegree and is p ^ P.natDegree. is AdjoinRoot of mapped to F; is never assumed to be a field and is never assumed irreducible over F.m ^ 2 * d < h, which contains the paper's case. is a hypothesis.IsPrimitiveRoot η (h - 1), equivalent to generating since .∀ i, f.degreeOf i ≤ d - 1.Fin m, starting at ; substitutes for .Lagrange.basis over the field at the nodes , mapped into , with coefficients . is the remainder modulo (AdjoinRoot.modByMonicHom) evaluated at .A formalization that takes to be any element satisfying (6.2), or defines as a ring homomorphism, would make the goal trivial or false; both are ruled out because and are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.
Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic (, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of (from separability of over the perfect field ). Proofs of any milestone, and alternative arguments, are welcome.
Multivariate multipoint evaluation asks for the values of a polynomial over a ring , with individual degrees at most , at given points of . Kedlaya and Umans showed that, over finite fields and rings , this problem can be solved in time nearly linear in the input size , for (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of , to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over , with bit operations for a randomized algorithm on degree- polynomials (abstract and §8).
Timeline. Brent and Kung (1978) gave the baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.
Let and write for the integers modulo . Every element of has a lift, its representative in . For , replaces each coefficient by its lift; lifts a point coordinatewise.
Algorithm MULTIMODULAR with degree parameter and rounds takes (degree at most in each variable) and a point . It lists the primes at most , reduces and modulo each , and evaluates the reductions . It does this directly when , and by recursion with rounds otherwise. It then returns, reduced modulo , the unique integer in congruent to modulo every .
Let be monic of degree and . The lift of is its representative of degree at most , with coefficients lifted to , an element of . Put
Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.
For monic of degree , , , , every of degree at most in each variable, and every :
In the order the paper's proofs use them:
The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form , which includes every finite field . Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree- polynomials over in bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).
The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold , and the base- digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all , and is reusable independently of this mission.
The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to , so its correctness depends on the explicit inequality of Lemma 2.4 for every , not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer produced over must determine the polynomial exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants and . A bound on evaluated at a point does not by itself suffice.
Lean represents as ZMod r with (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed , and as AdjoinRoot E for a monic E with E.natDegree. "Degree at most in each variable" is ∀ i, f.degreeOf i ≤ d - 1. is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes for real are the primes . Each algorithm is defined for a single evaluation point, since the paper processes the points independently. The leaf evaluates at directly; that value is what Theorem 4.1's FFT algorithm outputs. is as printed on p. 15; p. 16 prints .
The hypotheses and are not written in the paper but are needed. For , , the threshold is , no prime is used, and MULTIMODULAR returns . For the inequality and the degree bound both fail.
Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from alone: an algorithm that evaluates in and reduces it, or that computes in directly, would make the theorems trivial and is not the algorithm stated here.
Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's ), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base- representations of polynomials. Lemma 2.4 and the base- uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.
Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off (), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.
The problem (1.1) has blocks :
with , twice continuously differentiable, and . One iteration of Algorithm 2 (ALADIN) starts from a primal point and prices and does the following.
and the new prices are .
On the dual-decomposition side, (A.3) is the gradient of the dual function at , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix and step size is
where plays the role of a Levenberg–Marquardt regularization parameter.
Assume every strictly convex, every convex, of full row rank, positive definite, and . Then for every , with
the matrix is invertible and
The result. Lemma 5 places ALADIN on a known map. With it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations , are, as long as . It also reinterprets the augmented-Lagrangian parameter as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.
Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse , the semidefiniteness of , and the closed-form maximizer of a regularized concave quadratic.
The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over : the constraint couples the block coordinates, the minimizer is expressed through the inverse of (invertible only because has full row rank). A second trap is the sign convention for : it must agree with footnote 4 (), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.
Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and enter through the KKT system of (3.3), not through a closed-form expression: defining or by the formula of the conclusion would make the goal true by definition and is ruled out. is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of is part of the conclusion, because Mathlib's matrix inverse returns on a singular matrix.
Correction of (A.6). As printed, (A.6) has the bracket . This is a typo for , as in (A.5) on the same page and as the explicit minimization over forces; with the printed bracket the identity fails already for , , , . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.
The hypotheses of strict convexity of , convexity of and are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.
Training a neural network with nonsmooth activations (ReLU, max-pooling, absolute values) means running a stochastic gradient method in which the "gradient" is whatever the automatic differentiation library returns. For nonsmooth programs that output is in general neither a gradient nor a Clarke subgradient: the chain rule fails for the Clarke subdifferential, and the same function written in two ways can receive two different derivatives at the same point. Bolte and Pauwels (TSE Working Paper 1044, 2019; published in Mathematical Programming, 2021) introduced conservative set-valued fields as a class of generalized derivatives that is closed under the operations automatic differentiation performs and still carries enough information to analyse descent methods.
The framework is used in the analysis of nonsmooth automatic differentiation and of stochastic subgradient methods in machine learning (for instance Bolte and Pauwels, NeurIPS 2020). The present mission formalizes the first structural theorem of the theory.
Write for Euclidean space with inner product . A set-valued map assigns to each a subset ; it has closed graph if is closed in . A path is absolutely continuous if it is differentiable almost everywhere and ; it is a loop if .
Definition 1. is a conservative field if it has closed graph, nonempty compact values, and for every absolutely continuous loop
The integrand is Lebesgue measurable (Lemma 1), so the condition is that circulations along loops vanish, as for gradient fields in classical vector calculus, but with a maximum over the set in place of a single vector.
Definition 2. A function is a potential for (and is a conservative field for ) if for every and every absolutely continuous path from to
Examples: the gradient of a function; the Clarke subdifferential of a semialgebraic locally Lipschitz function; the output of forward or reverse mode automatic differentiation on a program built from definable elementary functions (the subject of the companion mission in this series).
If is a conservative field and a (locally Lipschitz continuous) potential for , then for Lebesgue-almost every , is differentiable at and
The result. Theorem 1 says that a conservative field, although set-valued and possibly far from any subdifferential, differs from the gradient of its potential only on a Lebesgue-null set. Several consequences in the paper rest on it: the Clarke subdifferential of is contained in the convex hull of every conservative field for , so it is the minimal convex-valued conservative field (Corollary 1), and a Fermat rule at local extrema of (Proposition 1). Combined with the companion result that automatic differentiation produces conservative fields, it implies that the derivatives returned by automatic differentiation agree with the gradient outside a Lebesgue-null set.
Formalizing it. The theorem is proved in the paper; this mission formalizes the known proof. No conservative-field calculus exists in Mathlib or on the platform. The mission produces the definitions of conservative fields and potentials in Lean, a measurability result for marginal functions of closed-graph set-valued maps along absolutely continuous paths, and an almost-everywhere identification of measurable selections with gradients that can be reused for other "derivative equals selection almost everywhere" statements.
The obvious argument runs: is locally Lipschitz, hence differentiable almost everywhere by Rademacher's theorem, and at a point of differentiability must be . The second step fails. Conservativity is an integral condition along curves, and it says nothing about the value of at an individual point of differentiability; a pointwise argument cannot exclude extra elements of . The identification therefore holds only almost everywhere and has to be extracted from integral information, which brings in three ingredients absent from Mathlib: measurability of for closed-graph compact-valued maps with no local boundedness assumption; measurable selections of such maps, including a countable family dense in every value (a Castaing representation); and, for Remark 3(d), the local boundedness of conservative fields (Borwein, Moors and Wang). Passing from "almost every point of every line" to "almost every point of " also requires measurability of the exceptional set, which is not automatic.
is EuclideanSpace ℝ (Fin p), Lebesgue measure is volume, and a set-valued map is EuclideanSpace ℝ (Fin p) → Set (EuclideanSpace ℝ (Fin p)). A path is a function ℝ → ℝ^p satisfying AbsolutelyContinuousOnInterval γ 0 1 (Mathlib's – definition on , equivalent there to the paper's); its values outside are irrelevant and is deriv γ. The maximum and minimum over are sSup and sInf of the image of a nonempty compact set, hence attained.
Since Lean's integral of a non-integrable function is , Definitions 1 and 2 require the circulation to be integrable in addition to having the stated integral; without this conjunct every field with non-integrable circulations would count as conservative, which is a trivializing reading excluded here. Likewise "" is formalized as differentiability of at together with set equality , because Lean's gradient is where is not differentiable. Definition 2 is the paper's form (2) with base point ; the min-form and the forms (3)–(4) are consequences, not definitions. Measurable selections appear as hypotheses (Borel measurable with ); their existence is not claimed by any milestone. The local Lipschitz hypothesis of Theorem 1 is kept as printed, and local (not global) Lipschitz continuity is used throughout.
Theorem numbers and pages refer to the TSE Working Paper 1044 version (October 2019), not to the Mathematical Programming typesetting.
Welcome contributions: a Castaing representation / Kuratowski–Ryll-Nardzewski selection theorem for closed-graph compact-valued maps on ; Rademacher's theorem for locally Lipschitz functions; Fubini-type "null on every line implies null" lemmas on EuclideanSpace; the fundamental theorem of calculus for absolutely continuous vector-valued paths.