Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A queue layout represents a graph by placing its vertices in a line and assigning edges to queues. The order and assignment must prevent nested edges from sharing a queue. This gives a graph parameter that measures how much queue capacity is needed for a particular graph. Heath, Leighton, and Rosenberg asked whether one fixed number of queues suffices for every planar graph. The question remained open while bounds depending on the graph's number of vertices, degree, or treewidth were known. Dujmović, Joret, Micek, Morin, Ueckerdt, and Wood resolved it by proving a uniform bound of 49. Their paper also develops layered partitions, a structural tool used beyond queue layouts. These claims and the historical account appear in the source paper, pp. 3–5 and 16.
A finite simple graph has vertices and unordered edges . Choose a linear order of . Two disjoint edges nest when their endpoints appear as , with one edge joining to and the other joining to . A queue is a set of edges with no nested pair. A -queue layout is a vertex order together with an assignment of every edge to one of queues; means such a layout exists. Edges sharing an endpoint cannot nest. Empty queues are allowed, so an edgeless graph can use zero queues. These are the paper's definitions in §1, pp. 3–4.
A layering assigns vertices to layers such that endpoints of an edge lie in the same or adjacent layers. A BFS layering starts from one selected root in each connected component and places each vertex in the layer equal to its graph distance from that root. A vertex partition divides into disjoint nonempty parts. Its quotient graph has those parts as vertices; distinct parts are adjacent if an edge of joins them. An -partition may index the parts by vertices of another graph : the quotient's edges must be represented by edges of , while an indexed part may be empty. A partition has layered width at most with respect to a fixed layering if every part contains at most vertices of every layer. The exact definitions are in §2, pp. 7–9.
A graph is planar when it can be drawn in the plane with vertices at distinct points and edges as simple arcs that meet only at shared endpoints. A tree decomposition covers every vertex and edge of a graph by bags indexed by a tree, with the bags containing each vertex forming a connected subtree. Treewidth at most three means that a tree decomposition exists with every bag of size at most four. The paper uses these standard notions in §2 and §4, pp. 7, 12, and 16.
The goal is the explicit upper bound the paper derives for its Theorem 1:
The printed theorem says that planar queue-number is bounded, and the authors state 49 immediately after it. A bound that depends on would not express the result. The goal uses the paper's own constant, as given in Theorem 1 and the following sentence, p. 5.
The structural target is Theorem 15, p. 16: for every BFS layering of a planar graph, there is a partition of layered width at most three whose quotient remains planar and has treewidth at most three. The queue transfer target is Lemma 8, p. 10:
when has an -partition of layered width . Its layout orders vertices layer by layer. The milestone list also includes the rainbow characterization, the blowup lemma, the complete-graph queue number, and the five-queue bound for planar graphs of treewidth at most three. These are the stated supporting results along the route to 49 in §2–§4.1, pp. 7 and 10–16.
The goal establishes a constant queue bound for all planar graphs, independent of their size, degree, and treewidth. Theorem 15 supplies a reusable structural statement: even if the original graph has large treewidth, its quotient by small layer intersections has treewidth at most three while remaining planar. The paper goes on to treat graphs of bounded Euler genus and proper minor-closed classes, and describes connections with graph products and other graph parameters in its abstract and introduction, pp. 1 and 5.
The result is proved in the cited paper. This mission records Lean statements of the goal and six supporting milestones; their proofs remain to be formalized. A completed development would connect finite graph orders, nested-edge combinatorics, layered partitions, planar drawings, and tree decompositions in one machine-checked chain. The queue and partition definitions can also support later work on graph classes beyond the planar case.
A vertex order chosen without regard to a graph's structure can contain large rainbows, forcing many queues in that order. Planarity alone does not specify an order or an edge assignment, and a direct bound from ordinary treewidth does not cover planar graphs with arbitrarily large treewidth. The central structural requirement is to find a partition whose parts remain small in each BFS layer while its quotient has low treewidth. The queue transfer lemma must retain a layer-by-layer vertex order and account for edges within parts and between parts. The paper, pp. 10–11 and 16, identifies these as distinct constraints in its stated results.
Vertices form a finite type and edges are those of a Mathlib simple graph. A vertex order is an injective map into ; strict inequalities on four endpoints encode nesting. Queue assignments are functions on the graph's edge set, so the empty graph's zero-queue case is present. The statements use an existence predicate for , without taking a numerical infimum. Layerings are functions to , with BFS roots chosen separately for disconnected components. Theorem 15 uses a partition into nonempty parts, and the quotient has exactly those parts as vertices. Treewidth at most three uses a published tree-decomposition definition with bags of size at most four.
The locally checked drawing definition has the same fields as the published plane-drawing definition; the published module was unavailable from the local index in this run. Planarity means existence of a crossing-free drawing, not a drawing that permits crossings. The formulation does not use a universal edge carrier that would rule out zero queues, a non-strict nesting test, or a default numerical treewidth. The near-triangulation, Sperner, and tripod statements from the paper's deeper proof are outside this proposal's milestone scope; the partition theorem remains a full milestone. Solvers may contribute the omitted geometric and tree-decomposition infrastructure when proving it.
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 libraryIn a prophet inequality, a decision maker observes random rewards one at a time and must choose without seeing future realizations. The benchmark is a prophet who sees all rewards and selects their maximum. A nonadaptive threshold rule chooses a threshold for each reward before observations begin, then accepts the first arriving reward that crosses its threshold. This model captures a simple class of stopping rules and, through the prophet inequality connection, informs posted price mechanisms in which prices are set before buyers arrive. Correa et al. (2021) prove that under uniformly random arrival order some such rule earns at least a fraction of the prophet's expected reward. The question here is whether that guarantee improves when the reward distributions are identical.
Fix an integer and draw independent rewards from the same three point law. A reward is with probability , is with probability , and is otherwise. The three probabilities are nonnegative and sum to one for . Thus a typical sample contains roughly unit rewards, while a high reward is rare enough that its presence among all draws has probability on the order of . Its magnitude is on the order of , so it still makes a nonvanishing contribution to the prophet's expected reward.
Give each coordinate a predetermined threshold . A uniformly random order reveals the sampled rewards, and the rule accepts the first . Conditional on a sample, let . Each accepted coordinate is equally likely to arrive first among , so the conditional expected reward is
Write for the rule's reward and for the prophet's reward. These are expectations of nonnegative random variables. The thresholds may be infinite, allowing a coordinate to be discarded in advance.
The goal is the paper's i.i.d. tightness claim: for every , sufficiently large members of this explicit family satisfy
The universal quantifier includes every nonadaptive threshold vector, including asymmetric thresholds and coordinates that are never accepted. The proof in Appendix B supports the displayed statement for every sufficiently large , which strengthens the existence of one hard instance stated in Section 3.1. Together with the paper's lower bound, this shows that the factor cannot be raised for this rule class even under identical distributions.
The milestones cover the prophet limit , reduction of arbitrary thresholds to two-level rules, the three contributions to a two-level rule's expected reward according to the number of high observations, Proposition A.3's scalar maximization, and the resulting uniform asymptotic bound on all two-level rules. The first coordinates of a two-level rule accept both and ; the remaining coordinates accept only . These targets correspond to Section 3.1, Proposition A.3, and Appendix B of Correa et al..
The explicit i.i.d. family locates a limit of nonadaptive thresholds under random arrivals. Identical distributions remove heterogeneity as an explanation for the loss against a prophet: the obstruction remains even when every reward has the same law. Consequently, an improved guarantee requires a richer rule class or additional assumptions on the distribution. The paper studies an adaptive threshold rule separately and obtains a stronger i.i.d. guarantee; this mission isolates the upper bound for the nonadaptive class.
Formalizing this result supplies a reusable model for random-order threshold selection on a finite i.i.d. product space, including its conditional reward formula and extended nonnegative expectations. The paper proves the tightness result; the Lean declarations in this proposal state it and its supporting results as proof obligations. The published i.i.d. product-measure model from the Samuel-Cahn development already has machine-checked definitions and is reused here. The proposed upper-bound theorems have not yet been proved in Lean.
Bounding each coordinate's expected contribution in isolation loses the interaction between unit rewards and the rare high reward. When a high reward occurs, accepting many unit rewards can dilute its share of the random-order reward; rejecting unit rewards sacrifices ordinary samples. The reduction to two-level rules must apply to every threshold vector before the count of unit-accepting coordinates can be optimized. Appendix B then controls the cases of zero, one, and at least two high observations uniformly in that count. The one-high-value case contains a printed final inequality that drops a positive term; the formal target uses the preceding, valid bound, whose extra term vanishes in the limit.
Lean represents a sample as Fin (n ^ 2) → ℝ and its law as a finite product measure. The index set is 0-based: the paper's are coordinates . The law is used only for , where it is a probability measure. Thresholds have type , and crossing is strict, matching Theorem 1's indicator . The page describes its two-level rule with weak threshold language; under strict crossing the same acceptance sets use thresholds and . The reward uses the paper's convention. Expectations are lintegrals with values in $[0,\infty]`, avoiding a zero default for nonintegrable real integrals. The goal quantifies over all threshold vectors and uses the actual prophet expectation of the same law; no restricted rule class or surrogate benchmark can replace either one.
The general i.i.d. law, sample maximum, and expected maximum come from SamuelCahnProphet.IID.Setting. The paper's three point law, random-order reward, canonical two-level rule, and high-value count are local definitions. Useful contributions include exact finite-law calculations, dominance of two-level rules, uniform estimates in , and the scalar exponential inequality of Proposition A.3. These parts can also support formal work on other finite-support prophet inequalities.
Boundary 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.
An associahedron of dimension is a simple polytope whose nonempty faces correspond, reversing inclusion, to the sets of pairwise non-crossing diagonals of a convex -gon: its vertices are the triangulations of the polygon and its facets are the diagonals. Associahedra appear in the combinatorics of parenthesizations (Tamari, Stasheff), in the theory of cluster algebras of type , where the Chapoton–Fomin–Zelevinsky construction realizes the cluster complex as the normal fan of a polytope, and in the study of secondary polytopes (Gelfand–Kapranov–Zelevinsky).
Many different polytopes realize the associahedron. Ceballos, Santos and Ziegler (arXiv:1109.5544v2) compare them up to normal isomorphism, a linear isomorphism of normal fans. One of the families they study, the "type II" family, is a construction of Santos presented at a conference in 2004 and first published in that paper (§5, pp. 18–23). It produces one associahedron for every triangulation of the -gon, the seed triangulation, and contains the Chapoton–Fomin–Zelevinsky associahedron as the case of the snake seed. This mission formalizes the statement that the construction works for every seed: Theorems 5.1 and 5.2 of the paper.
Let and , and number the vertices of a convex -gon counterclockwise. A diagonal joins two non-adjacent vertices; two diagonals cross when their endpoints are distinct and alternate around the boundary; a triangulation is a maximal set of pairwise non-crossing diagonals, and has elements. Two triangulations differ by a flip when and .
Fix a triangulation and let , with basis vectors , . Santos' vectors (p. 19) are
For a set of diagonals, is the cone spanned by the vectors , . The fan is the collection of the cones for all non-crossing sets , the empty set giving .
The cones of the triangulations form a complete simplicial fan when the vectors of each triangulation are linearly independent, every vector of lies in one of these cones, and any two of them meet in the cone of their common diagonals.
For a polytope and , the exterior normal cone is , where . The normal fan of is the set of all , , one cone for each nonempty face (p. 5).
For every triangulation of the -gon,
A polytope with normal fan is an -dimensional associahedron. The goal fixes no weights and no right-hand sides: it asserts only that some polytope has this normal fan.
Theorems 5.1 and 5.2 are what make Santos' family a family of associahedra at all. Every later statement of the paper about type II, including the classification up to normal isomorphism (Corollary 5.7: seeds agreeing up to rotation and reflection) and the identification of the Chapoton–Fomin–Zelevinsky associahedron as the only realization of both types (Theorem 6.1), compares the fans , and the word "associahedron" in them rests on these two theorems. The construction yields Catalan-many fans with facet normals in -coordinates, and modulo rotations and reflections they are pairwise non-isomorphic.
The theorems are proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about normal fans of polytopes, complete simplicial fans or associahedra has been formalized there, and Mathlib at the pinned revision has no notion of fan. The formalization would provide a machine-checked polytopality criterion for complete simplicial fans (Lemma 5.4), an explicit flip analysis of Santos' vectors (Lemma 5.3), and a polytopal realization of the associahedron for every seed.
Theorem 5.1 is not a direct computation. Linear independence of each triangulation and a sign condition for each flip do not by themselves make a fan; the paper combines them with assertion (1), a region covered by exactly one cone, and appeals to a covering criterion for vector configurations (De Loera–Rambau–Santos, Triangulations, Cor. 4.5.20, properties (ICoP) and (IPP)). A solver will likely need to formalize that criterion, or an equivalent argument that a pseudo-manifold of simplicial cones with these properties covers the space exactly once.
Lemma 5.3 requires a case analysis of how the seed triangulation meets the quadrilateral of a flip; the paper distinguishes four configurations, each with its own dependence (equations (4)–(7), p. 21), and showing that the four are exhaustive is itself a combinatorial statement about triangulations. Lemma 5.4 requires constructing a polytope from weights and identifying all of its normal cones, including the lower-dimensional ones, with the cones of the fan. Finally, the uniform constant has to work for all flips at once; for the dependence (4) the unperturbed weights ( on , elsewhere) give exactly zero, so a perturbation is unavoidable and must not spoil the other cases.
Vertices of the polygon are Fin (n + 3), chords are Sym2 (Fin (n + 3)), and diagonals, crossing and triangulations are reused from the published definition ChvatalArtGallery.FanPartition.Triangulation. The space is {d // d ∈ T₀} → ℝ, coordinate being the coefficient of . Cones are nonnegative hulls (PointedCone.hull ℝ). The fan contains every face, including .
"Normal fan of a polytope" is encoded as: is the convex hull of a finite set, and the set of cones equals with exterior normal cones, functionals identified with vectors by the coordinate pairing. Because is a cone of , the polytope must be full-dimensional; a point, a lower-dimensional polytope, or "some polytope whose facet normals are the rays" does not satisfy the goal. The inner-normal convention would give the fan , which is a different statement. The polytope is specified only through its normal fan, as in the paper.
Lemma 5.4 is stated for fans whose rays are indexed by the diagonals and whose maximal cones are the triangulations, the case in which the paper uses it; adjacent maximal cones are flip pairs. Lemma 5.3 requires the two coefficients to be strictly positive, as assertion (2) does, so the zero dependence is excluded. The ε of milestone 6 is quantified as . The weight is computed on 0-based positions as for , which equals the paper's 1-based .
A complete development needs basic fan theory (simplicial cones, a covering criterion), the polar construction behind Lemma 5.4, and the flip case analysis. The first two are reusable beyond this mission, for any polytopality argument on simplicial fans. Contributions of general lemmas on simplicial cones and on normal cones of polytopes are welcome.
An associahedron is a polytope whose faces encode ways to dissect a convex polygon without crossing diagonals. Its vertices represent triangulations. Associahedra occur in geometric combinatorics because the same combinatorial object admits many geometric realizations. Ceballos, Santos and Ziegler ask when two such realizations have the same normal fan up to a linear change of coordinates. This question distinguishes geometric constructions that have identical face lattices but different arrangements of facet normals. Their Santos family is indexed by seed triangulations, so its classification asks exactly how much of a seed can be recovered from its fan. Ceballos, Santos and Ziegler, §5.3.
Santos' construction was presented at a conference in 2004 and first appeared in print in this paper. The paper proves that the number of normal-isomorphism classes in this family is the number of polygon triangulations modulo rotations and reflections. It also explains a useful limit of the result: the set of normal vectors alone determines only the abstract dual tree of the seed triangulation, while the fan retains the further information needed for classification. Ceballos, Santos and Ziegler, §5 and Proposition 5.8.
Take a convex polygon with vertices in cyclic order and label its positions . A diagonal joins two nonadjacent vertices. A triangulation is a maximal collection of diagonals with no crossings. Each triangulation has diagonals. A flip removes one diagonal shared by two triangles and inserts the other diagonal of their quadrilateral.
Choose a seed triangulation . Let , with a coordinate for each seed diagonal . Santos assigns a vector to every polygon diagonal :
For each noncrossing set of diagonals, take the cone spanned by the vectors , , with nonnegative real coefficients. The collection of these cones is the fan . The paper proves that it is complete and is the normal fan of an associahedron. This mission uses that explicit fan as the meaning of , following the paper's own convention in §5.3. Ceballos, Santos and Ziegler, pp. 19, 23, Theorems 5.1–5.2.
Two fans are normally isomorphic here when an invertible real linear map sends every cone of the first to a cone of the second. A dihedral symmetry is a rotation or a reflection of the cyclically ordered polygon. It acts on a triangulation by relabelling both endpoints of each diagonal. Write when such a symmetry sends to .
For every and triangulations of the -gon, the goal is Corollary 5.7:
The left side compares all cones of the two fans through a linear isomorphism. The right side permits only the rotations and reflections of the polygon. It makes no choice of an ordering for the diagonals within either seed.
The milestone list follows the paper's argument: the polygon symmetry theorem for the associahedron's face lattice (Lemma 2.2); the induced crossing and parallelism preserving bijection of diagonals; the description and count of parallel facet pairs for Santos fans (Proposition 5.5); the injectivity of , where contains a seed and all single-flip insertions (Lemma 5.6); and invariance under rotations and reflections. Ceballos, Santos and Ziegler, pp. 6, 23–24.
The classification says precisely which apparent choices of seed triangulation are redundant. In particular, different dihedral orbits produce different normal-fan geometries even though all the resulting polytopes have the associahedron's face lattice. Parallel facet pairs supply an intrinsic geometric trace of the seed: they correspond to each seed diagonal and its flip. Lemma 5.6 then separates distinct seeds from their collections of these pairs. Ceballos, Santos and Ziegler, Proposition 5.5, Lemma 5.6 and Corollary 5.7.
The result is proved in the paper. The formalization work is to give a machine-checked account of its fan model and classification, including the polygon combinatorics and the linear-algebraic implications of a fan isomorphism. The supplied statements are proof targets, with sorry at theorem bodies; a complete Lean proof of the classification is not yet claimed. The explicit diagonal and crossing representation and the seed-indexed vector construction can also be reused to formalize the paper's fan and polytopality theorems.
A face-lattice isomorphism alone does not identify the seed: every associahedron in the family has the same face lattice. A first attempt to compare only the vectors also loses information. Proposition 5.8 shows that two different seed triangulations with isomorphic dual trees can yield linearly equivalent vector sets. The full fan records which vectors span cones together. The central task is to recover a crossing-preserving map of diagonals from a linear map of fans, then use the opposite directions of facet normals to recover . Ceballos, Santos and Ziegler, pp. 23–24, Propositions 5.5 and 5.8.
Lean represents polygon positions by Fin (n + 3) and unordered diagonals by Sym2; crossings and triangulations come from the published Chvátal triangulation definition. The ambient real vector space for a seed is the function space on the subtype of its actual diagonals. This makes the basis intrinsic to . A cone is the nonnegative real hull of the Santos vectors attached to a noncrossing diagonal set. NormallyIsomorphic demands a real linear equivalence of these ambient spaces. The classifying symmetry is explicitly or modulo .
No premise asserts the classification, and the fan is built from the paper's vectors rather than from a chosen list of abstract cones. Arbitrary permutations of diagonals, nonlinear maps, and an abstractly isomorphic dual tree do not satisfy the target's symmetry condition. The goal and the diagonal-action clause of Lemma 2.2 cover every ; the separate group-order clause in Lemma 2.2 applies for . Lemma 5.6 carries the printed bound . The triangular and quadrilateral cases are included in the goal and require their own boundary treatment in a proof. Contributions on crossing preservation, ray distinctness, linear independence of maximal cones, single-flip combinatorics, and dihedral equivariance are welcome.
Many matrix algorithms spend most of their time reading their input. A matrix with few nonzero entries should admit routines whose cost scales with that number, rather than with the product of its dimensions. Clarkson and Woodruff study random maps that compress a matrix before a regression or low rank approximation calculation while retaining the geometric information those calculations need. Their sparse embedding has one nonzero entry per input coordinate, so applying it to a sparse matrix can be charged to the matrix's nonzero entries. The probability guarantee for its geometry is Theorem 11 of the preprint, the target of this mission.
The paper proves further results for faster regression and low rank approximation after sketching. Those applications use the subspace guarantee as an input. This mission concentrates on that guarantee and the statements in §3 that support it. The source is the 5 April 2013 arXiv version; theorem and page labels below refer to that version.
Fix a real matrix of rank . Its column space is . A map is a subspace embedding for when it approximately preserves the length of every vector in simultaneously. The dimension , rather than the number of rows , controls the size required of the compressed space.
Here is the sparse embedding matrix . Each input coordinate independently chooses one bucket uniformly. The binary matrix has a at and zero elsewhere in column . Independently, is diagonal with a fair sign or at each coordinate. Thus the output in bucket is the signed sum of input coordinates assigned to . The probability in this mission is over the joint, uniform choice of all bucket assignments and signs, with fixed in advance. This is the construction in §2, p. 7.
For an orthonormal basis matrix of , the leverage score of row is . A threshold separates light coordinates, with , from heavy coordinates, with . The paper describes this split after sorting rows by leverage; the threshold description selects the same coordinates and keeps the input's original order. The bucket event bounds the sum of light leverage scores assigned to each bucket. The heavy event says that distinct heavy coordinates receive distinct buckets. These are properties of alone; the later concentration statements take probability over the independent signs after fixing a suitable .
There is an absolute constant such that for every of rank , every , and every integer ,
The event contains the universal quantifier over : one draw must work for the whole column space. The squared-norm estimate implies the norm formulation printed in Theorem 11, p. 11 on this range of . The paper gives its proof in §3, pp. 7–11.
The milestone list follows the paper's statements: a coordinate bound from §3.1; the weighted bucket estimate of Lemma 2; light-coordinate concentration in Lemma 3; the collision and exact-preservation statement of Lemma 5; the heavy-light cross-term estimate in Lemma 6; fixed-vector preservation in Lemma 7; and the passage to the whole subspace in Lemma 8. Their distinct probability spaces matter. Lemmas 2 and 5 concern bucket assignments, Lemmas 3, 6, and 7 concern signs for a fixed suitable assignment, and Lemma 8 is a general statement about a random linear map.
Theorem 11 gives a single compact random matrix that retains the Euclidean geometry of every vector in a specified rank- column space with probability at least . It supports sketch-and-solve algorithms: a computation performed on can use a much smaller row dimension while reasoning about the original column space. The construction also has exactly one nonzero per column, the structural fact behind its input-sparsity running time. The running-time bound is stated in the paper, but this mission's Lean target concerns the mathematical norm guarantee.
The paper already proves the theorem; the open work here is a machine-checked development of its statement and proof. The finite probability model, explicit squared norms, leverage scores, and bucket events can support later formalizations of other sparse sketching results. No machine-checked proof of Theorem 11 is claimed by this proposal. A complete development may reuse proved concentration inequalities from Mathlib or the platform, but the cited inequalities need their hypotheses checked against the finite-sign and weighted-bucket models used here.
A fixed-vector estimate does not itself imply that one random sketch works for all vectors of an uncountable subspace: the quantifier cannot simply be moved through the probability. Collisions also have different effects on high- and low-leverage coordinates. Heavy coordinates need a no-collision event; light coordinates can share buckets only while their total bucket weight remains controlled. The paper's statements keep these events and probability spaces separate. The final whole-subspace claim requires a uniform estimate whose failure probability accounts for the dimension .
Vectors are functions Fin n → ℝ, matrices are finite real matrices, and and are explicit sums of coordinate squares. The sample space is the product of all bucket maps and all Boolean sign assignments, with counting probability. Every theorem with a freely chosen bucket count assumes ; otherwise a Fin 0 sample space could make division by its cardinality meaningless. The theorem's size threshold forces this automatically when and . Matrix rank is Mathlib's matrix rank.
The formalization fixes in Theorem 11. The upper bound prevents the logarithmic size expression from degenerating near , and keeps its logarithm and division meaningful. Positive and are explicit where needed; Lemma 6 restricts . The heavy/light split uses leverage thresholds rather than a row permutation, and constants described as absolute are quantified before every dimension, matrix, error, and failure parameter. In particular, Theorem 11's event quantifies over all inside the probability, while Lemma 7 fixes before sampling signs. These choices exclude degenerate distributions, vacuous error ranges, and a fixed-vector claim masquerading as the goal.
The refined clause at the end of Theorem 11 is left out: its printed conflicts with the proof's collision requirement , and its threshold parameter is not fixed in the claim. Lemma 1 and the cited Hanson–Wright moment result, Theorem 4, are proof tools outside this proposal's milestone set. Contributions that formalize those tools faithfully, prove the bucket and sign estimates, or connect the finite model to existing probability libraries are useful for the goal.
An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.
Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.
Fix and a convex polygon with cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.
A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.
For the Hohlweg–Lange family, choose a sign word and extend it to on the labels . The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels , let contain the labels strictly below it. Form by replacing with and with if those labels occur in . The characteristic vector of , considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.
For the Santos family, choose a seed triangulation and use one basis vector for each seed diagonal . The normal assigned to a diagonal is when . Otherwise it is the sum of over seed diagonals crossing . The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions ; this seed gives the CFZ fan. Source, pp. 13 and 18–19.
Let and be the two normal fans, and let be the fixed snake. If is a triangulation, the target says
and it also asserts that . Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.
The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of pairs, through their characterization by the seed flips or the labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.
Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.
The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.
An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.
Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in using quotient coordinates ; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.
Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.
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.
Many procedures in high-dimensional statistics reduce to computing the probability that a normalized sum of independent random vectors falls into a set: simultaneous confidence intervals for many means, max-type tests, multiple testing with family-wise error control, and inference after model selection. When the dimension is comparable to or much larger than the sample size , these probabilities are approximated by those of a Gaussian vector with the same covariance, the high-dimensional central limit theorem. That Gaussian law is not available in practice, because its covariance matrix is unknown. The Gaussian multiplier bootstrap replaces it by a Gaussian vector built from the data, whose covariance is the sample covariance, and simulates from it.
Chernozhukov, Chetverikov and Kato, Central limit theorems and bootstrap in high dimensions (Ann. Probab. 45 (2017)), prove that this bootstrap is valid uniformly over hyperrectangles and over simple convex sets (sets sandwiched between a polytope with polynomially many facets and its small enlargement), with error depending on only through . This mission formalizes their abstract multiplier bootstrap theorem, Theorem 4.1.
Timeline:
Let and . Let be independent random vectors in with coordinates , centred () with . Let be independent Gaussian vectors with and set
The multiplier bootstrap: let be i.i.d. , independent of the data , let , and
Given the data, is Gaussian with covariance , while has covariance .
A hyperrectangle is a set with . For a finite set of unit vectors and thresholds , the polyhedron has the enlargement . For constants , a Borel set satisfies condition (C) if for some such polyhedron with facets; denotes this polyhedron and its normals. Condition (M.1′) with constant asks for every . Finally,
Let be a class of sets satisfying (C) and (M.1′). There is depending only on such that for every , on the event ,
The theorem is deterministic in the data: it holds at every realization on the event, and turning it into a rate requires only a bound on .
In the order of the proof (App. E.2, p. 2342):
Theorem 4.1 is the abstract step behind the paper's explicit multiplier bootstrap rates: Proposition 4.1 combines it with maximal inequalities that bound with high probability, and obtains, with probability at least , the rate for simple convex sets with sparse facet normals. In applications it justifies bootstrap critical values for max-type statistics and simultaneous confidence regions when . Remark 4.1, the hyperrectangle case, is the version most used in practice.
The results are proved on paper; none is formalized on the platform. A formal development produces machine-checked versions of the smooth-max sandwich, a Gaussian anti-concentration bound (Nazarov's inequality), a quantitative Gaussian comparison inequality and the bootstrap theorem itself. The comparison display and Lemma A.1 are proved in the paper only by citation ([20] and Klivans–O'Donnell–Servedio, Thm. 20), so formal proofs of them are new work rather than transcriptions.
The obvious route compares and through the Kolmogorov distance of their laws or through a total-variation bound between two Gaussians. Both depend polynomially on and fail when . The proof instead compares smooth functionals of the coordinatewise maximum, where the error depends on only through , and then converts back to probabilities of orthants with an anti-concentration inequality whose constant grows like . Both conversions must hold uniformly in the threshold , and the final bound for simple convex sets requires passing to the -dimensional vectors with , which is why appears. The comparison inequality for is the step with the least existing infrastructure: it is a Slepian–Stein interpolation between two Gaussian laws with explicit control of second derivatives of .
EuclideanSpace ℝ (Fin p); is Mathlib's multivariateGaussian 0 Σ. Independence is iIndepFun; 's law is fixed by P.map (Y i) = multivariateGaussian 0 (covMat P (X i)), and square integrability of each makes covMat positive semidefinite, so this is the genuine Gaussian law.mbLaw x is the push-forward of under , and the bound is asserted at every on the event, for the data . Since is independent of the data, this is a version of the conditional law; no conditional expectation appears.Infrastructure needed: multivariate Gaussian laws and their linear images, Gaussian integration by parts or Slepian interpolation, Nazarov's inequality, and properties of log-sum-exp. Lemma A.1, display (21) and the comparison display are reusable beyond this mission, for the high-dimensional CLT of the companion mission and for any max-type Gaussian approximation. Proofs of any milestone are welcome, as are proofs of the conditional Gaussianity identity from Mathlib's Gaussian API.
Many statistical procedures look at a large number of averages at once: simultaneous confidence intervals for means, multiple testing of hypotheses, the maximum of -statistics. Their calibration needs the joint law of a -dimensional normalized sum, and in modern applications is comparable to, or much larger than, the sample size . Classical multivariate central limit theorems with explicit error, such as Bentkus's bound over convex sets (Bentkus 2003), require to grow slowly with (roughly ), which rules out these applications.
Chernozhukov, Chetverikov and Kato showed that when the class of sets is restricted to hyperrectangles, the Gaussian approximation error depends on the dimension only through (Ann. Probab. 45 (2017)).
Timeline. In 2013 the same authors proved a Gaussian approximation for the maximum of a sum (sets of the form ) with rate (Ann. Statist. 41 (2013)). The 2017 paper extends this to all hyperrectangles, improves the rate to , and adds bootstrap results.
Let and . Let be independent random vectors in with coordinates , each centred () with . Let be independent centred Gaussian vectors with , the same covariance as . The normalized sums are
A hyperrectangle is a set with ; is the class of all of them. The quantity to bound is
The error is measured through the third-moment parameter and the truncated maximal moments
the same with , and . Here is the natural logarithm.
If for all , there are constants depending only on such that for every ,
The constants are left existential, as on the page: the goal asserts the shape of the bound, not particular values.
Under the moment conditions (M.1)–(M.2) and either an exponential (E.1) or a polynomial (E.2) moment bound with parameter ,
The result. Under the exponential moment condition (E.1), Proposition 2.1 makes the Gaussian approximation error tend to zero when , allowing much larger than . Under the polynomial moment condition (E.2), its second error term must also tend to zero. Theorem 2.1 is the probabilistic basis of the paper's multiplier and empirical bootstrap results for simultaneous inference (Chernozhukov, Chetverikov and Kato 2017).
Formalizing it. The result is proved on paper; no machine-checked version of this theorem was found in the platform catalog during this mission's prior-art search. A formal proof needs interpolation between and , Gaussian anti-concentration (Nazarov's inequality), and third-order Taylor estimates of smooth approximations of indicator functions. Nazarov's inequality is used in the paper by citation, so its formal proof is a separate milestone.
The obvious route, a Lindeberg replacement of each by after smoothing the indicator of a hyperrectangle coordinate by coordinate, loses a polynomial factor in : the derivatives of a product of smoothed one-dimensional indicators add up over coordinates, so the error grows like a power of rather than of . Any smoothing must also be paid for by the probability that the Gaussian vector falls in a thin neighbourhood of the boundary of a hyperrectangle, and a dimension-free bound on that probability is not available for general hyperrectangles; the anti-concentration bound is the best one can use. Finally, a direct comparison yields an inequality in which the quantity to be bounded appears on both sides, and the rate is obtained only after that inequality is solved; a one-shot estimate gives a worse power of . The truncation in handles coordinates too large for a third-order Taylor expansion, since no moment condition beyond third moments is assumed.
Vectors live in EuclideanSpace ℝ (Fin p) and the coordinate is X i ω j. The Gaussian comparison vectors satisfy P.map (Y i) = multivariateGaussian 0 (covMat P (X i)) with covMat P Z = (E[Z_j Z_k])_{j,k}, which is positive semidefinite, so this is the genuine ; the are independent. Hyperrectangle endpoints are extended reals used only in comparisons. Every theorem carries the standing assumptions , , independence, centring and finite second moments. Items that involve or add ; when a third moment is infinite the paper's bounds are vacuous, so this loses nothing. is defined by its formula for every real , because Theorem 2.1 evaluates it at , which may be below . Lemma 5.1 and Corollary 5.1 assume the 's independent of the 's, as the definition of does; Theorem 2.1 and Proposition 2.1 do not. A bound on a supremum is stated set by set.
Constants that the paper says depend only on (or on and ) are quantified after and before , , the probability space and every random vector; a constant chosen after , or the law would trivialize every statement. Upper bounds on expectations in hypotheses ((M.2), (E.1), (E.2)) and in Lemma C.1's conclusion are lower Lebesgue integrals, so a non-integrable function cannot make a hypothesis hold with a junk value of . Dropping the independence of the or using a wrong covariance would make the goal false.
A complete development needs: a multivariate Stein or Slepian interpolation, third-order Taylor expansion with remainder for functions on , Gaussian integration by parts, and Nazarov's inequality. The anti-concentration and smooth-max lemmas are reusable for any max-type Gaussian approximation, including the bootstrap results of the second mission of this series. Proofs of individual milestones, of Nazarov's inequality in particular, are welcome on their own.
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.
Optimization models often build an objective from several intermediate quantities: constraints, penalties, and transformed measurements are evaluated first, then combined by an outer function. These intermediate and outer functions can be Lipschitz without being differentiable at the point of interest. Ordinary differentiation supplies no chain rule there. The generalized-gradient framework gives a set of possible first-order slopes, while semismoothness provides stronger directional behavior along sequences approaching the point. Mifflin's IIASA report asks whether this behavior survives such compositions and how the generalized gradient of the result relates to those of its ingredients.
The report first establishes basic properties of the generalized gradient in §2, including almost-everywhere differentiability and a nonsmooth mean value theorem. Section 4 then states a chain-rule inclusion as Theorem 4 and the semismooth composition result as Theorem 5. The report is dated December 1976; a journal version appeared in 1977. The mission cites theorem numbers and pages from the report version throughout. No claim about differences between the report and journal texts is needed here.
Work in finite-dimensional Euclidean spaces. Let , for , be component functions, and let be an outer function. Define the component map and the composite by
The functions are locally Lipschitz in the report's precise sense: on each bounded subset of their Euclidean domain they have a finite Lipschitz constant. For a scalar function , a point , and a direction , the generalized directional derivative is the joint upper limit of as and . Its associated generalized gradient is the support set
This is the definition used in Mifflin's report, not an identification assumed in advance with a hull of ordinary gradient limits. Proposition 1(c) supplies that identification under the paper's Lipschitz assumption. The ordinary one-sided directional derivative is the limit of for , when that limit exists.
Mifflin calls semismooth at if it is Lipschitz on a ball about and the scalar sequence has exactly one accumulation point whenever tends to zero, , and . The quantification is over every direction and every such sequence. This pointwise condition is Definition 1 of the report, and its link to one-sided directional derivatives is Lemma 2.
To state the chain rule, form the set
The same is used across all components. The sum is the action of the report's matrix on .
Theorem 4 asserts that is locally Lipschitz and that, at every point,
This is an inclusion, not a general equality. The report gives an example immediately after Theorem 4 in which the inclusion is strict: two identical absolute-value components cancel under an outer difference, while remains larger than .
The goal, Theorem 5, assumes the setting of Theorem 4. If each is semismooth at a selected and is semismooth at , then
The conclusion is pointwise. It does not assert semismoothness throughout from hypotheses at one point. The milestone list contains the chain rule and the source's stated support results: Proposition 2, Lemma 1, Proposition 1(c) and (d), Lemma 2, and the claims (4.2) and (4.11)–(4.12) from the proofs.
Theorem 5 permits composite nonsmooth objectives to be treated within the same semismooth class as their components. Theorem 4 gives a concrete set built from component generalized gradients that contains the composite's generalized gradient. Together, they let later statements about a composite use first-order information from its stated ingredients, subject to the inclusion's possible strictness. These are results proved in Mifflin's report, not open mathematical conjectures.
This mission drafts machine-checkable statements of those known results and their definition layer. The local Lean modules compile with proof placeholders; this staging does not supply machine-checked proofs of the theorems. A complete development would formalize the known arguments or another proof of the same statements. The reusable output would include the support-set generalized gradient, sequence-based semismoothness, the nonsmooth mean value result, and the chain-rule inclusion, all with their source assumptions exposed.
At a point where is differentiable, the component functions need not be differentiable, and the outer function need not be differentiable at . The ordinary smooth chain rule therefore cannot simply multiply ordinary gradients. The candidate is a convex set of combinations of generalized gradients; a single chosen combination does not in general describe all nearby limiting slopes. The report's strict-inclusion example also shows why replacing Theorem 4 by equality would be false. For semismoothness, the condition concerns every admissible sequence of generalized gradients near the point, so checking just one path or one gradient selection does not establish Theorem 5.
The Lean domain is EuclideanSpace ℝ (Fin n) and the outer domain is EuclideanSpace ℝ (Fin m). The report's norm is the Euclidean norm and its pairing is the real inner product. An index of type Fin m represents the components; is admitted, in which case the component space is a point and the composite is constant. A finite sum represents the column-matrix product. The generalized gradient is defined by all directional support inequalities, so Proposition 1(c) remains a theorem rather than becoming true by definition.
The generalized directional derivative is imported from the published definition matching the report's joint limit. Lean's real limsup has a default value for an unbounded quotient; Lipschitz hypotheses are carried wherever that operation is used. “Locally Lipschitz” is imported as Lipschitzness on every bounded subset, and the explicit constants of §2 use nonnegative reals, equivalent to the report's positive constants by enlarging them. The directional derivative is a relation asserting a limit, so no value is assigned when the limit fails. “Exactly one accumulation point” remains an existence-and-uniqueness assertion about cluster points. The report's means positive convergence to zero, as its proof of Lemma 2 says explicitly. These choices exclude a vacuous formulation that only asks about one convenient sequence or gives a default directional value.
The scope includes the two local definition files and the cited theorem statements, including both conclusions of Theorem 4 and Lemma 2. Proof contributions would need finite-dimensional Lipschitz and differentiability infrastructure, limiting-gradient compactness, convex hull and separation facts, and sequence convergence facts. Results about the alternative Qi–Sun vector-valued semismoothness notion are outside this mission's definition layer.
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.
A graph is 3-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding 3-colorability is NP-complete in general, and one of the standard ways to map the boundary between easy and hard cases is to forbid an induced subgraph. For the path on vertices, 3-colorability of -free graphs was known to be polynomial (Randerath and Schiermeyer, 2004, reference [21] of the paper), and Randerath, Schiermeyer and Tewes asked in 2002 whether the same holds for .
Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong (Combinatorica, 2017) answered this question. Their Theorem 1 states that the list version, in which every vertex may only receive a color from a prescribed list , can be decided for -free graphs in time . The algorithm first reduces the instance to a polynomial number of configurations described by a seed, and then calls Lemma 11 (p. 14) on each configuration. Lemma 11 rests on one structural fact about -free graphs, Claim 13 (p. 16), which is the goal of this mission.
Timeline:
All graphs are finite and simple. For a set of vertices of a graph , is the set of vertices outside with a neighbor in , and . A graph is -free if it has no induced subgraph isomorphic to .
A palette assigns each vertex a list . A seed of is a nonempty set that induces a connected subgraph, is 2-dominating (every vertex is at distance at most from ), and satisfies for and for .
The Lemma 11 setting consists of a graph , a palette and a seed such that
For , is the set of with , and . For , is the set of for which is not complete to , and for the paper fixes non-adjacent , .
In the Lemma 11 setting, let , , and let , be non-adjacent. Then
Claim 13 says that the neighbor triples of the vertices of pairwise touch. This is what allows the proof of Lemma 11 (Claims 14 to 17) to refine the palette of all of simultaneously with only polynomially many guesses: without it, the vertices of could interact independently and the number of cases would be exponential. Claim 12 and display (1) are the general tools for building long induced paths through a seed, used throughout §3.1.
The paper's result is proved and published. None of it is formalized in a proof assistant as far as the platform's index shows. This mission produces a machine-checked version of the structural core of Lemma 11, and the definitions it needs (seeds, the Lemma 11 setting, the sets and ) are reusable for the rest of the paper's argument.
The proof of Claim 13 is short on paper, but it assembles an induced from three pieces: the path through given by Claim 12 and the two short paths and . Showing that the union is induced requires every non-adjacency between the pieces, and these come from different hypotheses: the stability of , the fact that has no neighbor in , the list structure of the vertices of next to , and part (c) of Claim 12. Claim 12 itself is an extremal argument (choose the neighbor closest to an end of a path), which in a formal setting requires explicit manipulation of paths as sequences of vertices: splitting, reversing and concatenating them while keeping them induced. The obvious approach of taking any shortest path through between two of the four vertices fails, because such a path can have interior vertices adjacent to the other two.
Graphs are SimpleGraph V on a finite type V with decidable equality; vertex sets are Finset V. The colors are 0,1,2 in Fin 3, and a palette is V → Finset (Fin 3). -freeness is the negation of Mathlib's induced containment IsIndContained of pathGraph 7; ordinary subgraph containment would be a different, much stronger condition. Connectedness uses Mathlib's Connected, which includes nonemptiness. An induced path is the published platform definition StrongPerfectGraph.Main.IsInducedPath (a nonempty list of distinct vertices in which two vertices are adjacent exactly when consecutive); its ends are the first and last list entries and its interior is the list with both ends removed.
The Lemma 11 setting is a structure Lemma11Hyp G L S bundling its hypotheses. Lemma 11's own conclusion, a decision procedure with running time , and the running time of Theorem 1 are not formalized, since there is no machine model. The paper's arbitrary choice of is replaced by quantification over every non-adjacent pair , , which is Claim 13 for every possible choice. The case is allowed.
One hypothesis is added to Claim 12: the four vertices are pairwise distinct, and the ends of the path are required to be distinct. The paper's proof and its use in Claim 13 take the four vertices distinct; without the assumption the claim can fail, and without a one-vertex path would satisfy it vacuously.
The following trivializing readings are excluded: dropping the overline in "anticomplete to " (which, together with milestone 3, would force to be isolated); a one-vertex path or repeated vertices in Claim 12; and subgraph instead of induced-subgraph containment for -freeness. The setting is satisfiable with : the 5-cycle with , , , , , satisfies every hypothesis, with .
Proofs of the milestones and the goal are welcome, as are general lemmas about induced paths as lists (subpaths, concatenation through a connected set) that would serve other graph-theory missions.
Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main algorithmic consequence is that first-order model checking is fixed-parameter tractable on graphs given with a contraction sequence of bounded width. A parameter of this kind is useful only if the classes it bounds are closed under the constructions that arise in practice. Many such constructions are first-order definable: the complement of a graph, its square (join vertices at distance at most two), the map graph of a planar map. Section 8 of the paper shows that twin-width is stable under every such construction: a first-order interpretation of a class of bounded twin-width has bounded twin-width. Bounded VC-dimension, by contrast, is not preserved (interval graphs have VC-dimension at most two but interpret every graph, p. 3:41).
The result has since become the basis of the "model-theoretic" view of twin-width: bounded twin-width classes are closed under first-order transductions (Theorem 8.1 of the paper), and later work identifies them, among ordered structures, with the monadically dependent classes (Twin-width IV, Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé and Toruńczyk).
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if all pairs in are edges or none is. For a partition of , the red graph has the parts as vertices, two distinct parts being adjacent when they are not homogeneous. is a -partition if has maximum degree at most . The graph has twin-width at most , , if there is a sequence of -partitions from the partition into singletons to a partition with at most one part, each obtained from the previous one by merging two parts (p. 3:32).
A prenex formula of depth with two free variables is
with a Boolean combination of atoms and , . The interpretation is the graph on in which distinct are adjacent iff . For a class , is the class of all induced subgraphs of the graphs , .
The proof works with morphism-trees. The complete tree has as nodes all tuples of vertices with , the parent of a tuple being its prefix. Two sibling nodes are equivalent in if an automorphism of the tree swaps them, preserving equalities and adjacencies among the entries of every tuple and the part of of every entry. A reduction deletes one of two equivalent siblings with its subtree, repeatedly; a reduct admits no further reduction. Two vertices are adjacent in when and are equivalent in some reduction of , and is the partition into the connected components of .
For every prenex formula and every there is such that
The bound depends on and only. No explicit function is asserted: the paper gives none (the proof goes through a tower-type bound on reducts).
Theorem 8.3 turns every first-order definable graph construction into a source of bounded-twin-width classes: squares and fixed powers of planar graphs, complements, map graphs (as transductions, via Theorem 8.1), -planar graphs and bounded-degree string graphs. Combined with the model-checking algorithm it gives FPT first-order model checking on all these classes, provided a contraction sequence is available. The theorem is also the first step of the model-theoretic characterisations of bounded twin-width in the later papers of the series.
The result is proved in the paper; no machine-checked proof of it, or of any twin-width bound, exists to our knowledge, and Mathlib has no notion of twin-width or of first-order interpretations of graphs. The mission asks for a formal proof of the graph case. The morphism-tree milestones are also the combinatorial core of the paper's linear-time model-checking algorithm (Theorems 7.5, 7.15), whose running-time statements are not part of this mission.
The obvious approach refines the -partitions of by the "type" of each vertex with respect to . The number of such types is not bounded: a vertex's behaviour depends on the whole graph through the quantifiers. The paper replaces types by the components of , defined through reductions of morphism-trees that respect . Two facts must then be shown, and neither is local in an obvious way. First, the number of components inside a part is bounded (Lemma 8.5); this needs the pruned shuffle, which assembles a reduction of the whole tree from reductions of the local trees , and the fact that it commutes with reductions (Lemma 7.12), where an automorphism of one local tree must be extended to the shuffle without breaking adjacency between non-homogeneous parts. Second, far-apart components are homogeneous in (Lemma 8.6), which needs the evaluation argument of Lemma 8.4 inside a reduction of the partitioned tree.
SimpleGraph V on a Fintype with decidable equality. Twin-width is the predicate TwinWidthLE G d in the paper's partition form (pp. 3:12, 3:32); trigraphs are not formalized, and twin-width is never an infimum, so no junk value of sInf can make a bound vacuous. Merge steps merge exactly two distinct parts, so a sequence cannot jump to one part.FirstOrder.Language.graph.Formula (Fin 2), evaluated in G.structure; variable 0 is , variable 1 is . Prenex is Mathlib's IsPrenex; quantifier depth qdepth is defined in the mission ( counts once).Set (List V)), the paper's identification of a node with its current path (p. 3:30), which is exact for reductions of complete trees. Equivalent siblings are distinct. Distances in are in , so disconnected parts are far apart. The sequence graph uses 0-based indices, hence the exponent . The pruned shuffle is defined by its characterisation (each component of the sequence graph of a tuple lies in the tree of its local root). Lemmas of §7.3 carry its standing assumption .Reusable beyond this mission: the partition form of twin-width, quantifier depth of first-order formulas, and the morphism-tree machinery (reductions, pruned shuffles), which formalizes the algorithmic core of first-order model checking on bounded twin-width. Contributions welcome: proofs of the §7 lemmas, of Lemma 8.4 by induction on the quantifier prefix, and the closure of twin-width under induced subgraphs.
Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate , it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers .
Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.
There are identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is
For , is the number of servers with at least jobs. The process is a continuous-time Markov chain on
Its generator sends to at rate when , and to at rate . The fluid-scaled coordinates are , the negative of the fraction of idle servers, and for . The diffusion-scaled coordinates are . Expectations are taken under a stationary distribution of the chain.
The proof works with functions on and with the first-order operator
where is the partial derivative in , taken one-sided on .
For each there is a constant such that for all with and every stationary distribution,
The constant depends on only, not on , the stationary distribution, or .
with , vanishing second derivatives for , and explicit upper bounds of order above that level. 6. (3.18): . 7. Theorem 2, (2.2): the half of the goal.
Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are on average, and the number of servers holding jobs is on average, uniformly in . Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.
The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.
The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of through the fluid curves.
The obvious route is to bound in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by . General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at . So is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined and .
A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with that is controlled only by combining Lemma 2 with the monotonicity of .
ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's , so the goal's "" is Lean index . Each state is bounded by , nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit of (4.14), not about an arbitrary function.WithTop ℝ, with as ⊤, so a missing solution is never read as . is an if cascade, and Lemma 7 states the agreement of its branches. is defined by the closed form (4.14), not through the fluid model (4.1).Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.
Large networks are often modeled through a graphon, a measurable function that records how likely two labeled vertices are to interact. For interacting diffusions, this lets one ask whether a finite random network has a predictable population limit. Bayraktar, Chakraborty and Wu study that question for graphon weighted systems, including graphs obtained by independently retaining potential edges with a sparsity parameter . Their not-so-dense regime allows to decrease, provided the typical interaction scale diverges. Theorem 4.1 is the paper's law of large numbers for this regime; its two conclusions distinguish convergence of the population's empirical law from mean-square closeness of each particle to a coupled graphon limit. Bayraktar, Chakraborty and Wu, 2023.
The authors present three main convergence results: continuity of the continuum graphon system in Section 2, a dense-system law of large numbers in Section 3, and the percolated-system law of large numbers in Section 4. Section 7 establishes the latter. The graphon and cut-metric framework used here follows the graph-limit treatment cited by the paper. Bayraktar, Chakraborty and Wu, 2023; Lovász, 2012.
Let . A graphon is a symmetric measurable . The cut norm measures the largest absolute integral of over a measurable rectangle . A sequence of step graphons approaches when . The related operator norm measures the effect of on bounded measurable functions. Remark 2.1 says cut convergence implies convergence in this operator norm. Bayraktar, Chakraborty and Wu, 2023, Remark 2.1.
Fix a dimension and horizon . A label has an initial state and an independent -dimensional Brownian motion . The initial states are independent of each other and of the Brownian motions. The limiting graphon particle is a continuous path whose drift averages against the time- laws of all labels , and whose diffusion matrix is . The time- law at label is . The family of path laws is measurable in and has uniformly bounded second moments. Bayraktar, Chakraborty and Wu, 2023, (4.2).
For particles, label means , with . Each undirected edge weight is Bernoulli with mean ; diagonal weights are included. These edge variables are independent of the Brownian motions and initial states. The finite particle uses the same initial state and Brownian motion as . Its drift is the sum of divided by ; its diffusion is . The coefficients and are bounded and Lipschitz, and is invertible with uniformly bounded inverse. Initial laws have uniformly bounded second moments, , and . Bayraktar, Chakraborty and Wu, 2023, Conditions 4.1–4.2.
Let , , and . The main target, Theorem 4.1, first asserts convergence in probability in the weak topology on :
This uses Condition 2.2(a): on each of finitely many intervals covering , the initial law varies continuously in Wasserstein distance . If the graphon also satisfies Condition 2.2(b), its stated sectional continuity outside null sets, the theorem adds
The milestones record the paper's cut-to-operator observation, uniform coupling moments, the one-edge and two-edge estimates, the bound on the second interaction-error term, the quantitative coupling lemma, and the empirical law of large numbers for the independent limiting particles. The second displayed limit is conditional on 2.2(b); the first is not. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1.
The first conclusion identifies the population-level limit even when the sampled network has a decreasing edge-retention probability. It gives a deterministic law on path space, rather than only a limit at one time. The second conclusion is stronger: it compares each finite particle with the limiting particle built from the same initial state and Brownian motion, averaged over all labels. This comparison is available when the extra graphon continuity assumption holds. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1 and Remark 4.1.
The mathematical results were proved in the published paper. The present mission asks for machine-checked Lean proofs of its specified statements; the draft theorems themselves currently contain sorry. Reusable outputs would include the percolated-edge model, a path-law formulation of graphon diffusions, and estimates for random interactions that depend on the particle states they influence. The paper's proofs appear in Sections 5–7, with the sparse-system argument in Section 7. Bayraktar, Chakraborty and Wu, 2023.
The edge variables are independent of the driving noise, but a particle's state depends on its incident edges. Therefore an expression such as cannot be factored into the edge mean times the error moment. The same dependence affects pairs of edges in the squared interaction sum. Equations (7.10), (7.14), and (7.15) quantify the discrepancy. A second difficulty is that cut convergence controls integrals against fixed bounded tests, while the dynamics and their path laws supply tests that vary with the system. The paper's regularity conditions and quantitative estimates are needed to connect those forms of control. Bayraktar, Chakraborty and Wu, 2023, Sections 7.1–7.2.
Lean represents by Mathlib's unit interval, by Fin d → ℝ, and continuous paths by maps from into that vector space. The chosen vector and matrix norms are fixed sup-type norms; finite-dimensional norm equivalence preserves the limit statements and the estimates with existential constants. The horizon and dimension are explicitly positive. Particle index i : Fin n denotes the paper's st particle, and empirical laws use positive sizes to avoid division by zero. Wasserstein distances use extended nonnegative reals, while nonnegative expectations use lower integrals.
The noise lives on one probability space. The continuum equation uses the natural filtration of its own initial state and Brownian motion. The finite equation uses the natural filtration of its edge array, sampled initial states, and Brownian motions. A solution carries a measurable continuous-path law family in the paper's class ; this prevents a nonmeasurable pushforward or a default-zero integral from silently satisfying an equation. Edge symmetry, Bernoulli marginals, independence, and diagonal self-loops are explicit. The zero-coefficient system has a separate sorry-free Lean witness for both solution predicates, ruling out a vacuous solution concept.
The formalization uses the published Peng1990.SMP.Stochastic Itô interface and WassersteinDRO.Duality.wassersteinDistance definition. Contributions can prove the listed estimates, strengthen their reusable stochastic and measure-theoretic infrastructure, or connect this mission's local setting to the other graphon missions after their definitions are published. The auxiliary changed-measure particles of Section 7.1 are outside the initial milestone list. Bayraktar, Chakraborty and Wu, 2023, Sections 4 and 7.
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.
Twin-width is a graph and matrix invariant introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021). Classes of bounded twin-width include bounded tree-width and clique-width graphs, proper minor-closed classes, posets of bounded width, and permutations avoiding a fixed pattern; on all of them, first-order model checking is fixed-parameter tractable once a contraction sequence is given. The difficulty in applying this framework is to bound twin-width for a concrete class, because a contraction sequence is an intricate object.
Section 5 of the paper supplies the tool that makes such bounds routine: the Grid Minor Theorem for twin-width (Theorem 5.4). It reduces bounding twin-width to finding an order of the rows and columns of a matrix (for a graph, an order of its vertices) in which no large mixed minor appears. The paper then uses it for pattern-avoiding permutations, posets of bounded width and -minor free graphs (Section 6, Table 1). The argument is modelled on the proof of the Stanley–Wilf conjecture by Marcus and Tardos (JCTA 107, 2004) and on its use by Guillemot and Marx for permutation pattern matching (SODA 2014).
Timeline. Füredi and Hajnal (1992) conjectured a linear bound on the number of s in a -matrix avoiding a permutation pattern. Marcus and Tardos (2004) proved it, with constant , via -grid minors. Fox (arXiv:1310.8378) improved the constant to , and Cibulka and Kynčl (arXiv:1607.07491) to . Guillemot and Marx (2014) built from the grid structure a decomposition of permutations; Bonnet et al. (2020 preprint, 2021 journal) generalized it to arbitrary matrices over a finite alphabet, which is Theorem 5.4.
Let be an matrix with entries in a finite alphabet of size . For sets of rows and of columns, the zone is the submatrix on those rows and columns; it is constant if all its entries are equal.
A partition of is a pair of a partition of the rows and a partition of the columns. Its error value is the largest number, over all parts (respectively ), of parts of the other side forming a non-constant zone with it. A contraction sequence is a sequence of partitions starting from the finest one (all singletons), ending at the coarsest one (one row part, one column part), each obtained from the previous by merging two row parts or two column parts. has twin-width at most , , if some contraction sequence has error value at most throughout.
A division is a partition whose parts consist of consecutive indices. is -twin-ordered if it has a contraction sequence of error value at most consisting of divisions.
A zone is vertical if its rows are all equal, horizontal if its columns are all equal, and mixed otherwise. A -mixed minor is a division into row intervals and column intervals all of whose zones are mixed; is -mixed free if it has none. For -matrices, a -grid minor is such a division in which every zone contains a . Finally .
For :
$$M\ \text{-twin-ordered}\ \Longrightarrow\ M\ \text{-mixed free},
t\ge1,\ M\ \text{-mixed free}\ \Longrightarrow\ \operatorname{tww}(M)\le 4c_t,\alpha^{4c_t+2}.$$
The constant is the one the paper's proof produces; the paper's summary is not formalized.
Theorem 5.4 characterizes bounded twin-width of matrices, up to the order of rows and columns, by the exclusion of a mixed minor. Its second item is used in Section 6 of the same paper to show that -minor free graphs, posets of bounded width and pattern-avoiding permutations have bounded twin-width, and in later papers of the twin-width series as the standard route to twin-width upper bounds. Without it, each such bound needs its own explicit contraction sequence.
The result is proved in the paper; no machine-checked proof of it exists in Mathlib or on the platform. The mission produces a machine-checked statement and, once solved, a proof of the grid theorem with its explicit constant, a formal treatment of contraction sequences of matrices, and a statement of the Marcus–Tardos theorem with the Cibulka–Kynčl constant, which is itself absent from Mathlib.
The first item is comparatively short. The second item is where the work lies. The natural first idea — contract greedily as long as the error value stays below a bound depending on — does not work: the error value is not monotone under fusions, and nothing in the absence of a mixed minor directly prevents a greedy sequence from getting stuck with large error. Any proof has to identify a quantity that is monotone under fusion and is bounded by a density argument, and then turn a sequence controlled by that quantity into a contraction sequence of bounded error value; the paper's choices (mixed value, Lemmas 5.6 and 5.7) are the milestones. The density argument rests on the Marcus–Tardos theorem with an explicit single-exponential constant, a substantial combinatorial result in its own right and not available in Mathlib.
Matrices are Matrix (Fin n) (Fin m) A with [Fintype A], and is Fintype.card A. Partitions are Mathlib Finpartitions of univ; the finest is ⊥, and "coarsest" means at most one part. Twin-width is the partition form of p. 3:18, as a predicate MatTwinWidthLE M t with exactly one merge, of rows or of columns, per step; it is never an infimum over a possibly empty set. Divisions in minors are given by strictly increasing cut points , so all parts are non-empty. Vertical and horizontal mean "all rows (columns) of the zone agree". Grid minors use Bool entries. Since is not an integer, is a real power, and the bound is ; the mixed-value bound of Lemma 5.7 is .
Hypotheses added relative to the page: in Theorems 5.3, 5.4 and Lemma 5.7; in the second item of Theorem 5.4, in Theorem 5.3 and in Lemma 5.7, since for every non-empty matrix is vacuously -mixed free and the bound would be false; in the row-type count. Theorem 5.3 is stated with the explicit constant that the paper quotes and uses, not as a bare existence statement.
The statements are not trivializable by the usual routes: twin-width is not a junk infimum, a contraction sequence cannot jump to one part in a single step, the error value counts non-constant zones per part on both sides, minors range over divisions with non-empty interval parts rather than arbitrary partitions, and all bounds depend only on and , never on .
A complete development needs: finite partitions and their merges, divisions as interval partitions, the Marcus–Tardos theorem, and bookkeeping for sequences of partitions. The partition machinery and Theorem 5.3 are reusable beyond this mission (graph twin-width in the other missions of this series, pattern avoidance). Proofs of individual milestones, and of the Marcus–Tardos theorem from its original argument, are welcome.
Training a neural network means running a first-order method on a loss that is built from compositions of elementary operations, many of them nonsmooth: ReLU, max-pooling, absolute values, sorting, norms. The gradient the optimizer uses is not computed by hand. It is computed by automatic differentiation (autodiff), most often in its reverse mode, backpropagation, which applies the chain rule of calculus operation by operation. When every operation is smooth, the output is the gradient. When some are not, each nonsmooth operation is assigned some "derivative" at its kinks (for ReLU at , typically ), and the chain rule is applied anyway. The result is in general neither a gradient, nor a Clarke subgradient, nor an element of any classical subdifferential: the classical subdifferentials do not satisfy the chain rule that autodiff applies.
Bolte and Pauwels (TSE Working Paper 1044, 2019; Mathematical Programming, 2021) introduced conservative set-valued fields to give these outputs a meaning. A conservative field is a set-valued map whose circulation along every closed path vanishes, exactly as for a gradient field. It obeys a chain rule along absolutely continuous curves. This mission formalizes the paper's Theorem 8: forward-mode and reverse-mode automatic differentiation, run with conservative fields for the elementary operations, return a conservative field for the composed function. The companion mission of this series formalizes the paper's Theorem 1, that a conservative field equals the gradient of its potential almost everywhere.
Write for Euclidean space and for a set-valued map, assigning a subset to every point. A path is absolutely continuous, with derivative for almost every .
A conservative field (Definition 1) is a set-valued map with closed graph and nonempty compact values such that for every absolutely continuous loop () the circulation is Lebesgue integrable with integral . A function is a potential for , or is a conservative field for (Definition 2), if is conservative and for every absolutely continuous path from to . A map is a conservative mapping for (Definition 4) if, along every absolutely continuous curve , for almost every , for all .
An evaluation program (§5.1) has inputs and intermediate nodes . Node has a tuple of distinct earlier nodes and an elementary function . Algorithm 1 sets for and returns . Each comes with a conservative field (property (d)). Given a choice for every :
The autodiff fields are and , the sets of outputs of Algorithm 2 and Algorithm 3 over all choices at .
If every is a locally bounded conservative field for , then
"Conservative field for " is meant in full: closed graph, nonempty compact values, zero circulation and the potential identity.
Theorem 8 says what backpropagation computes on a nonsmooth program: an element of a conservative field of the function, a set that behaves like a gradient along curves. This is what lets the paper's later results apply to deep learning: stochastic subgradient methods driven by such outputs converge, for definable losses, to points that are critical for the conservative field. It is also the reason why spurious outputs of autodiff (a nonzero "derivative" of a function that is identically zero) are harmless: by the companion Theorem 1 they occur only on a Lebesgue null set.
The result is proved in the paper, and nothing here is open. To our knowledge none of it has been machine-checked: there is no formal account of conservative fields, and the existing formalizations of backpropagation treat smooth layered networks only. This mission produces a formal model of evaluation programs and of both autodiff modes, a formal chain-rule calculus for conservative mappings (Lemmas 2–5), and the theorem itself. Formalizing it exposed three points the printed text leaves to the reader: the overwriting update of Algorithm 3, the nonempty-values hypothesis missing from Lemma 2, and the local boundedness that Theorem 8 needs (see Formalization scope).
The obvious argument is "autodiff applies the chain rule, and conservative fields satisfy the chain rule". The chain rule along curves (Lemmas 3–5) only gives the derivative identity of Definition 4 for each element of . It does not give the set-valued properties of Definition 1. Passing back to a conservative field (Lemma 2) needs to have closed graph, nonempty compact values and local boundedness. These depend on how the sets vary with through the forward pass, and they fail without local boundedness of the . Lemma 2 relates an integral identity along every path to a pointwise almost-everywhere identity, and both directions involve the measure theory of absolutely continuous curves that Mathlib supports only in part. The equality of reverse and forward modes is linear algebra, but the two algorithms traverse the graph in opposite orders, and the printed reverse update is not the one the equality needs.
is EuclideanSpace ℝ (Fin n), and the conservative-field layer is polymorphic in the dimension: each lives on . A path is a function ℝ → ℝ^n that is AbsolutelyContinuousOnInterval on , with = deriv γ. Definitions 1–2 require the circulation to be interval-integrable, because Lean integrates a non-integrable function to . Definition 4 and the chain rule (5) assert HasDerivAt, not an equation for deriv, so they cannot hold by default at points of non-differentiability. Nodes are Fin q, numbered from . Parent tuples are duplicate-free lists of smaller nodes, and input nodes have none.
and range over all admissible choices. A single fixed choice would give a map that is not a conservative field in general, and the formal statement does not use one.
Deviations from the printed text, each recorded with its item:
Theorem numbers and pages are those of the TSE Working Paper 1044 (October 2019), the version this mission cites. The journal version is typeset differently.
The conservative-field definitions duplicate those of the companion mission and are meant to be merged with them. Contributions are welcome at every level: Lemma 2 and Lemmas 3–5 form a reusable nonsmooth chain-rule calculus, and the reverse-equals-forward identity is a standalone statement about backpropagation that holds for arbitrary weights.
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.
Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.
V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with discrete agents, and with a continuum of agents indexed by . For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the -agent model is close to the continuum model when is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.
Discrete agents. There are agents with real opinions , . Agents and interact when . A solution of (2.1) is a continuous with
for all and all . The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.
Continuum agents. Agents are indexed by with Lebesgue measure. is the set of bounded measurable functions . For , is the set of nondecreasing with for ; such are regular. The interaction operator is
and a solution of (3.2) from is a measurable with every and for all and all .
The embedding. For , is the step function with on and . It distributes the agents over blocks of of length .
Let , the solution of (3.2) from , and for each let be a proper solution of (2.1) with nondecreasing and . Then for every and there is with
The statement fixes no rate in and no dependence of on ; it asserts only uniform convergence on bounded time intervals.
The theorem says that the continuum model is the large-population limit of the -agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.
All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.
The operator is not Lipschitz on : moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some , where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time . The perturbed trajectory, coming from agents, is a step function and is never regular, so the estimate must be one-sided in this sense.
A literal reading of the page also fails. The page writes , but for in block the continuum interaction equals times the discrete right-hand side of (2.1). With and , both models are linear; at the sup distance between and tends to . The discrete time must be rescaled by .
Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on matter; trajectories are written x t α, time first, with time in ℝ and explicit guards. In 0-based form, on ; for the definition returns , and every statement assumes .
Explicit readings of the paper's phrases:
A trivializing formalization is ruled out: the hypotheses are satisfied by , the conclusion is not vacuous because is evaluated at only, and the perturbed initial values in Proposition 4 range over all of , not over regular functions.
Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for on step functions, and a change of variables in interval integrals. The Lipschitz estimate on and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.