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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
The logarithm of a share price is commonly modelled as a Brownian motion with drift, . The Black–Scholes option pricing formula needs the volatility but not the drift , so a practitioner must estimate from data. Observing the whole path would give exactly through its quadratic variation, but a real observer sees far less. The most readily available daily information is the opening and closing prices together with the day's high and low.
Parkinson (1980) proposed an estimator from the high–low range, and Garman and Klass (1980) found the minimum-variance estimator among a class of quadratic functions of high, low and close. Both were derived assuming zero drift, , and the Garman–Klass estimator is biased when . Rogers and Satchell (Ann. Appl. Probab. 1 (1991) 504–512) proposed the estimator
which is unbiased for every drift. Their estimator is now a standard tool in empirical finance for range-based volatility measurement.
Fix a probability space carrying a standard Brownian motion : , its increments over disjoint intervals are independent and Gaussian with variance equal to the length of the interval, and every sample path is continuous. Fix a drift and a volatility . The log-price is
and, for a trading period , the running maximum and running minimum are
Thus , and are the high, the low and the close of the log-price (with the open normalized to ). In Lean these are logPrice σ c B t ω, runMax σ c B t ω and runMin σ c B t ω in the namespace RogersSatchell.Unbiased.
The proof in the paper passes through an exponential time: a random variable with (rate , mean ), independent of the whole path . For the rates
appear, in Lean alpha σ c lam and beta σ c lam.
For every , every and every , is integrable and
At this is the unbiasedness of of display (2). The statement quantifies over all drifts; the absence of on the right-hand side is the content.
The goal certifies a drift-free unbiased volatility estimator built from four numbers per trading day. Because only enters the Black–Scholes formula, an estimator whose mean does not depend on the nuisance parameter is exactly what is needed. Milestone 7 complements this with a drift-uniform bound on its variance, , while the exact value quoted in the paper is only available at .
On the formalization side, the results are classical and proved; none is machine-checked as far as the platform's catalog shows. A complete development would give the first formal treatment of the joint law of the running maximum of drifted Brownian motion at an exponential time, of the Wiener–Hopf splitting at the maximum, and of a Laplace-inversion argument for a moment function of the time horizon. All three are reusable well beyond volatility estimation: in ruin theory, queueing (reflected Brownian motion), and the pricing of lookback and barrier options.
The obvious approach, computing directly from the joint density of for drifted Brownian motion, requires the reflection principle combined with a Girsanov change of measure, followed by a double integral involving Gaussian tails, done separately for each sign of . The cancellation that makes the drift disappear is not visible in that computation, and a statement specialized to (where the reflection principle alone suffices) does not carry over. Every step of the milestone list rests on path properties of Brownian motion (the strong Markov property, the law of the running maximum, splitting at the maximum) that Mathlib does not yet provide for IsBrownianReal, and the passage from milestone 4 to milestone 5 needs uniqueness of the Laplace transform.
ProbabilityTheory.IsBrownianReal B P with B : ℝ≥0 → Ω → ℝ, plus the hypothesis that every sample path is continuous (the standard choice of a continuous version). Time is ℝ≥0.sSup/sInf of the path over the interval ; with continuous paths they are attained. The supremum is never taken over all times or in extended reals.HasLaw T (expMeasure λ) P; "parameter " is read as rate . "Independent of " is independence from the path-valued random variable with the product σ-algebra. is evaluated at truncated to .A formalization that specializes to , takes the supremum over all of , or omits the integrability conjuncts is not the statement of this mission.
Infrastructure that a complete development needs: the reflection principle or the strong Markov property for Brownian motion, the exponential-time law of the running maximum of a Lévy process, and uniqueness of Laplace transforms for continuous functions. All of these are reusable; contributions of any of them are welcome. Related platform items cover other objects and are credited here: running maxima and exit problems for spectrally negative Lévy processes (Avram2004.Exit.reflected), a drifted Brownian motion in characteristic-function form in a queueing-network setting (Reiman84.QueueLength.Paths), and a GI/G/1 Wiener–Hopf transform identity (QueueingFundamentals.GG1.wiener_hopf_transform).
A convex minimization problem comes with a dual maximization problem, and the dual value never exceeds the primal value. When the two values differ, a duality gap occurs. Dual bounds, Lagrangian relaxations and optimality certificates are then weaker than hoped. Conditions that rule the gap out are constraint qualifications such as Slater's condition and Rockafellar's notion of a stably set problem. Such conditions say when the gap vanishes, but not what the dual value is when it does not.
R. T. Rockafellar's 1967 paper answers that question for the Fenchel-type pair of problems built from a convex function, a concave function and a continuous linear map between infinite-dimensional spaces. Its Theorem 6 (§6, "Weak duality theorems", pp. 179–180) "explains the exact way in which inf (P) and sup (P*) can fail to be equal", by expressing the dual value through the primal problem alone: the dual supremum is the lower limit of the optimal values of slightly perturbed primal problems. This perturbational view of duality was later developed in Rockafellar's Conjugate Duality and Optimization (1974). It underlies the modern treatment of value functions in convex optimization.
Two real vector spaces and are topologically paired when each carries a locally convex Hausdorff topology, they are in duality under a bilinear form that is continuous in each variable, and every continuous linear functional on either space is the pairing with exactly one element of the other. Let and be two such pairs. Let be continuous linear and its adjoint, the continuous linear map with .
A function is convex when its epigraph is convex in . It is proper when it never takes and is finite somewhere. A function is proper concave when is convex, never takes , and is finite somewhere. The standing hypotheses are that is lower semicontinuous proper convex on and is upper semicontinuous proper concave on . Their conjugates are
The primal problem (P) is to minimize over . The dual problem (P*) is to maximize over . For the perturbed problem (P()) is to minimize . Its value defines the perturbation function
The lower semicontinuous hull of is , where is allowed, so that . All infima and suprema are taken in .
valid except in the trivial case where the left side is and the right side is . No consistency, constraint qualification or attainment is assumed, and neither side need be finite. The exception is exactly the stated conjunction. A version assuming (P) consistent would be weaker, since an inconsistent (P), with , may still have a finite lower limit.
The paper's Lemma 2 (convexity of ) is used by the first claim. It is a milestone of the companion mission on Theorem 3 of the same paper and is not restated here.
Theorem 6 reduces every question about the dual value to a question about the primal value function near the origin. Strong duality holds exactly when is lower semicontinuous at (outside the trivial case). A duality gap is exactly a downward jump of at . The dual of (P*) obeys the same formula, which the paper uses to derive Theorem 7 on normal problems. An integer-lattice analogue appears in discrete convex analysis (Murota, Theorem 8.53, whose duality relation is already stated on Prove2Me as DiscreteConvex.ConjugacyDualityD.general_duality_relations). That statement has no topology and is not the same theorem.
The result is classical and its proof is published. As far as the platform's index shows, no machine-checked statement of it exists in the paper's generality, nor a statement of extended-real biconjugation on general paired locally convex spaces. The value of the mission is a formal proof in the paper's setting: arbitrary topologically paired spaces, extended-real-valued functions, and both the proper and the improper case of the hull. The biconjugation milestone (6.2) and the hull lemma are reusable for other perturbational duality results.
The obvious argument compares with the dual objective directly. It cannot give the theorem, because may jump at , and the dual objective does not detect the value of at a single point: the target is a lower limit, not a value. In infinite dimensions, conjugacy recovers a function only when it is lower semicontinuous and convex for a topology compatible with the pairing, so the statement depends on the full compatibility of the pairing on , not on a norm. The usual statements of biconjugation cover proper functions only, whereas here the lower limit may take both values , and both cases of the theorem must be covered. Finally, extended-real arithmetic must be tracked so that the dual objective, defined from , and , is matched in every infinite case.
Values lie in EReal. Infima and suprema are complete-lattice ⨅ and ⨆, so an empty or unbounded family gives as in the paper. The lower limit is Filter.liminf h (nhds y) over the full neighbourhood filter: a punctured limit would change the theorem. Convexity is epigraph convexity in , and properness is the paper's two-sided condition. A topological pairing is a structure holding a bilinear map, separate continuity, and existence and uniqueness of representing elements in both directions. No norm, inner product or finite dimension is assumed. The adjoint is continuous linear data satisfying the adjoint identity. The conjugates , are defined by the paper's formulas from , , so their regularity is a consequence, not a hypothesis. Properness of and excludes the form from and from . No statement is repaired relative to the page.
The dual value is the supremum of the maximand built from , and as on p. 172. Defining through (for instance as the biconjugate of at ) would make Theorem 6 true by definition and is ruled out.
A complete development needs extended-real conjugates on paired spaces, the lower semicontinuous hull and the closure of a convex epigraph, and Fenchel–Moreau for proper lower semicontinuous convex functions on a locally convex space. All of these are reusable beyond this mission. Proofs of the milestones, and lemmas toward Fenchel–Moreau in this generality, are welcome contributions.
Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.
A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.
The world is a continuous-time Markov chain on a countable set with generator , , and bounded rates , . While , unit demands arrive at rate , all demand is backlogged, and orders arrive after a random lead time that is independent of the world and the demand. Costs are discounted at rate . With the unit order cost , holding rate and penalty rate , set and
where is the demand during a lead time when the world starts in . Uniformizing at a rate with and , the myopic cost is . The linear-cost model () is solved by value iteration from :
, with limits and . The myopic level , the finite-horizon levels and the optimal level are the smallest minimizers of , and , and . Throughout, (Assumption 1).
The world states carry a partial order . The chain is stochastically partial-monotone (display (14)) if for every there is a probability space carrying copies of started at and at whose paths satisfy for all almost surely. Condition 1 requires this together with nondecreasing in .
Under Condition 1, the three families of levels exist and are nondecreasing along :
Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal parameters are monotone, and instead bound them between monotone functions.
All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.
The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term , which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain is monotone for every . As printed, this is false at : for two states with , swaps the states. A complete proof cannot rely on that lemma as printed.
A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits , must be justified by Lemma 4's uniform bounds.
The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law and the world transition function are defined by uniformization at the model's rate , the paper's own device. The lead-time law is a probability measure on , and is the series of display (16). uses an infimum over integers , and , are suprema over , which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in is Monotone/Antitone with respect to . Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on .
Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.
Lemma 7 is not included because it is false as printed. A guarded version (for instance with ) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on . Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.
Decisions under uncertainty are often modelled by a finite set of scenarios: possible futures with weights , each with its own optimization problem. Solving every scenario separately is easy but useless in practice, because the decision taken today cannot depend on which scenario will be revealed tomorrow. Progressive hedging, introduced by Rockafellar and Wets in Scenarios and policy aggregation in optimization under uncertainty (IIASA Working Paper WP-87-119, 1987; Mathematics of Operations Research 16(1), 1991), restores this nonanticipativity by iterating between scenario-wise solves and an averaging step, guided by price systems that act as multipliers. It is the standard decomposition method for multistage stochastic programs and is implemented in widely used software such as PySP/mpi-sppy. This mission formalizes the paper's convergence theorem in the convex case, Theorem 5.1, together with the duality theory of §4 and the proof steps of §5 it rests on.
Let be a finite set of scenarios with weights , . For each the scenario subproblem is to minimize over , where is nonempty and closed and is locally Lipschitz with bounded level sets . The convex case is when every and is convex.
A decision vector is split by time, . A policy is a map ; the policy space carries the inner product and norm . At each time the scenarios are partitioned into bundles of scenarios that cannot yet be told apart. The aggregation replaces by its -weighted average over the bundle of at time , and . The implementable policies are constant on each , the price systems are , and the admissible policies are . With the problem is
Its Lagrangian is on , the dual is : maximize over with .
The progressive hedging algorithm fixes , starts from any and any , and in iteration sets , lets minimize
for every scenario, and updates .
In the convex case with exact minimization, the sequences and are bounded if and only if (P) and (D) have optimal solutions. In that case there are optimal for (P) and for (D) with
and, with ,
for all , strictly unless , and the step lengths are nonincreasing from on.
Theorem 5.1 is the guarantee behind progressive hedging in the convex case: solving only small scenario problems and averaging, the method finds a nonanticipative optimal policy and an optimal price system whenever these exist, with a distance to the solution that never increases. The dual sequence converges to a solution of (D), which gives the prices of information that the paper interprets economically. Boundedness of the iterates is an exact test for solvability.
The result is classical and fully proved on paper; its proof reduces the algorithm to Rockafellar's proximal point algorithm for a maximal monotone operator. No machine-checked version is known to exist. The mission produces a formal statement and, eventually, a proof of the full chain from scenario data to convergence, including the duality theorem of §4, which is of independent use for scenario-based stochastic programming. A related platform mission in this series treats the nonconvex case (limits of the algorithm satisfy first-order conditions).
The algorithm is not a proximal point method in the variable : it acts on the pair , and the averaged policy is in general not admissible while is in general not implementable. The step that fails in a direct attempt is showing that the map is firmly nonexpansive, which requires recognizing it as the resolvent of the monotone operator of a saddle function restricted to , in the rescaled norm rather than in the original product norm. A second difficulty is duality: identifying the fixed points of the iteration with optimal pairs of (P) and (D) needs the convex duality theory of §4 for an extended-real-valued perturbation function without any constraint qualification.
is EuclideanSpace ℝ (Fin n); policies are functions S → EuclideanSpace ℝ (Fin n) with S a Fintype. Time periods are a monotone map assigning each coordinate to its period, and each is a Setoid S; no refinement between periods is assumed. The standing assumptions of §3 are fields of the model structure, and the convex case is a separate hypothesis.
The inner product (2.2), norm (2.3) and (5.2) are explicit weighted sums. Mathlib's norm on a function type is the sup norm; it is used only for topology (boundedness, convergence, local Lipschitz continuity, compactness), which coincides with that of (2.3) in finite dimension. Stating (5.3) or (5.26) with Mathlib's sup norm would change the inequalities and is ruled out. Optimal values , , , , and are EReal infima and suprema, so that infeasibility gives and an unbounded dual objective gives ; real-valued sInf would silently return there. A solution of (D) must have . The algorithm is a predicate on sequences, with arbitrary and ; Proposition 3.2 shows the predicate is satisfiable.
Subgradients and normal cones are those of convex analysis; the normal cone is the published definition FirstOrderOpt.ConvexTheory.normalCone. Not formalized: the nonconvex (Clarke) parts of §4, the linear-quadratic case and its rate result, and inexact minimization.
A complete development needs: separable minimization over product sets, finite-dimensional compactness arguments, convex duality for a perturbation function on a subspace, and the convergence of the proximal point algorithm for maximal monotone operators (Rockafellar 1976, Theorem 1 and Proposition 1). The last two are reusable well beyond this mission; contributions of either as standalone results are welcome.
Robertson and Seymour introduced tangles as a way to describe a region of a graph that cannot be isolated by a separation of low order. A separation divides the edges into two sides, and its order counts the vertices shared by those sides. A tangle makes a consistent choice of the side regarded as small at every order below a threshold. This turns an informal idea of a highly connected region into an object with explicit axioms. In Graph Minors. X, the authors connect tangles with branch-width, tree-width and grid minors; the grid construction is the direct example behind that connection. The paper states the existence of a tangle of order in every -grid as (7.3) on p. 173. Robertson and Seymour, 1991.
The result is already proved in the paper. The present target is its Lean statement and proof, together with the two numbered results from §7 on which the construction rests. This mission concerns the grid itself. The paper's further assertion that a grid minor induces a tangle in a larger graph uses the separate minor-transfer result (6.1), whose edge identities require additional definitions. Robertson and Seymour, 1991, pp. 170–173.
Fix an integer . The -grid has vertices for . Two vertices are adjacent exactly when their coordinate differences have absolute values summing to one. For each , is the horizontal row with vertices ; for each , is the vertical column. Write and for their edge sets. The Lean development uses the already published definition of this same simple graph, with coordinates shifted to start at zero. The shift changes no adjacency or row and column relation. Robertson and Seymour, 1991, p. 171.
For an edge set , the edge boundary consists of vertices incident both with an edge in and with an edge outside . The source prints “vertices ” when introducing this set. Since is a set of edges, this is a type slip; the two incidence conditions give the intended reading. An edge set is small if and it contains no complete row edge set . These are two separate requirements. An edge set can have a small boundary while still containing a whole row. Robertson and Seymour, 1991, pp. 171–172.
A subhypergraph specifies subsets and of the grid's vertices and edges, retaining the incidences of the ambient grid. A separation satisfies and ; its order is . Although the grid is a simple graph, these are the paper's hypergraph definitions. A tangle of order contains only separations of order below and satisfies three axioms: it chooses an orientation of every such separation; the union of the first sides of any three chosen separations is not ; and no chosen first side contains every vertex of . The chosen three may coincide. Robertson and Seymour, 1991, pp. 153–154.
The first milestone, (7.1), identifies a symmetry between rows and columns under a low boundary:
The second milestone, (7.2), says that three small edge sets cannot cover all the grid's edges:
The goal, (7.3), defines rather than taking it as an arbitrary set. It selects precisely the separations of order less than for which is small, and asserts
These are the numbered §7 results on pp. 171–173, in the order used by the paper. Robertson and Seymour, 1991, pp. 171–173.
The theorem gives an explicit tangle in a familiar graph for every order . A tangle is more than a numerical connectivity bound: it records coherent choices across all separations below its order. In the paper, the grid tangle feeds the link between large grids and tangles of high order. The extension from a grid minor in another graph to a tangle of that graph invokes (6.1), beyond this mission's goal. The converse direction, that large tree-width forces a large grid minor, is (7.4), proved in Graph Minors V (Robertson and Seymour, 1986); the published definitions and statements of that paper on this platform are about grid minors and tree-width, not tangles. Robertson and Seymour, 1991, pp. 170, 173.
Formalizing (7.3) will make the grid tangle available as a checked object alongside the already published grid graph. It will also produce reusable definitions for an edge boundary, small edge sets and the paper's hypergraph separations. The Lean files here are draft statements with open proofs; the published 1986 grid definition is the existing checked ingredient. No machine-checked proof of (7.1), (7.2) or (7.3) is claimed by this proposal.
The obvious attempt at (7.2) counts boundary vertices column by column. If every column has all its edges in and meets both sets, each column contributes at least two vertices to , so the two boundaries together have at least vertices. This only works when the third set misses the first and last rows; in general the third set can absorb edges of every column, and no single count over the whole grid bounds all three boundaries at once. The statement is a covering property of three sets, not a bound on any one of them, and the paper's argument for it is credited to D. Kleitman and M. Saks. The goal must then meet all three tangle axioms. The page's proof of (7.3) argues the first axiom and says only that the rest follows from (7.2); the third axiom, , is part of the definition and must be established, not dropped. Robertson and Seymour, 1991, pp. 172–173.
The source assumes finite hypergraphs throughout, and §7 fixes . Lean uses a finite simple graph on Fin θ × Fin θ, reusing RobertsonSeymour1986.GM5.grid, and views its edge set as the edge type of a local hypergraph. Subhypergraphs hold vertex and edge subsets with inherited incidence. Set.ncard counts boundary vertices and separation order. Rows and columns use all grid edges whose two endpoints have the specified coordinate. This representation keeps every grid edge's identity, even though it is written as a SimpleGraph edge subtype.
IsSmall retains both and the exclusion of full row edge sets. boundary requires an incident edge on each side of . Both details are necessary for the claimed tangle: an IsSmall without the row clause would call every set with a small boundary small, including sets that contain whole rows, and the resulting set of separations is not a tangle; a boundary defined with "every edge outside " instead of "some edge outside " would be empty and make the size condition vacuous. The formalization keeps the third tangle axiom and does not replace it with an easier condition. The definitions of hypergraph, separation and tangle duplicate the shared encoding used by the other missions for this paper and can later be consolidated. The definitions also include the paper's tangle number and maximum edge size for that shared layer, though the grid goal does not invoke them; on finite inputs their maxima are bounded, and their empty-set value is zero.
The companion missions are Graph Minors. X. Obstructions to Tree-Decomposition I: Tangle Number Equals max(Branch-Width, Largest Edge Size), max(β(G), γ(G)) = θ(G); Graph Minors. X. Obstructions to Tree-Decomposition II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1); Graph Minors. X. Obstructions to Tree-Decomposition IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions; and Graph Minors. X. Obstructions to Tree-Decomposition V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}. Those missions address the paper's other main results; this one isolates the grid construction.
Tangles were introduced by Robertson and Seymour in Graph Minors. X (JCTB 1991) to make precise the idea of a "highly connected region" of a graph. A tangle orients every low-order separation of the graph towards one side, consistently. They are the organising notion of the later papers of the Graph Minors series, which culminate in the graph structure theorem and the proof of Wagner's conjecture.
Section 11 of Graph Minors X, Structure relative to a tangle, asks how local and global structure are related. In the paper's words: suppose that has large tangle number, but relative to each high-order tangle the graph has a structure of a certain kind . What can be inferred about the global structure of ? One might guess that has a tree-decomposition into pieces each with structure , but that is false. The theorem of §11 shows that does have a tree-decomposition into pieces which almost have structure . The authors state that they need this for an application in a later paper of the series, cited as [6], Graph minors. XVII. Excluding a non-planar graph (submitted); it appeared as Graph Minors XVI (2003), where the local structure relative to a tangle is a near-embedding in a surface.
A hypergraph has a finite vertex set , a finite edge set and an incidence relation. A subhypergraph has and , with every end of an edge of in . A separation of is a pair of subhypergraphs with and , and its order is .
For , a tangle of order in is a set of separations of order such that (i) for each separation of order one of , is in ; (ii) no three members of have ; (iii) for .
A tree-decomposition of is a tree and subhypergraphs , , whose union is , which are pairwise edge-disjoint, and with whenever lies on the path of between and .
A design is a pair of a hypergraph and a set of subsets of .
For and a class that is -pervasive in ,
If is -pervasive in and , then either some separation of order has
or some location in with design in has for all .
If , there is a tree-decomposition of over with a node such that and the -extension of the design of is in . The goal is the case .
For every , if has no tangle of order , then
Consequently , where is the tangle number. This is the p. 188 remark following (11.3).
(11.1) converts local information, stated tangle by tangle, into a global decomposition. Every piece of the decomposition is either small (at most vertices) or differs from a structure in by at most added vertices. This is the kind of local-to-global step the later Graph Minors papers need: there the local structure near each high-order tangle is a near-embedding in a surface, and a result of this shape glues such local structures along a tree. With it gives a tree-width bound , a weaker form of the tangle/tree-width duality.
The result has been proved since 1991. To our knowledge no proof assistant formalizes it, and none formalizes the hypergraph tangles or tree-decompositions of this paper. This mission produces machine-checked statements of the paper's notions of design, enlargement, location and pervasiveness, the structure theorem, and its inductive strengthening.
The first idea is to take the pieces in themselves as the pieces of the tree-decomposition. That fails, and the paper says so: the pieces can only almost have the structure. Locations for different tangles interact, and the decomposition must absorb up to extra vertices into each piece. The induction also has to control a set of attachment vertices of bounded size: a piece built at one node must still accept the vertices through which it is glued to the rest of the tree. Keeping throughout the recursion is the delicate point, and it is why the strengthened statement (11.3), not (11.1), is the one that admits induction.
Hypergraph V E with an incidence relation. Finiteness is [Finite V] [Finite E] on every theorem. Subhypergraphs, separations, tangles and tree-decompositions are the series' shared encodings (namespace RobertsonSeymour1991.GM10.Structure). The tree of a tree-decomposition is a SimpleGraph on Fin n satisfying IsTree.G.Sub × Set (Set V), and a class of designs is a set of -designs. Classes need not be closed under isomorphism; the paper never uses that.IsPervasive is satisfiable: the class of all designs is -pervasive, through the empty location. The conclusion is satisfiable too: the one-node decomposition lies over . So neither the hypothesis nor the conclusion of (11.1) is vacuous.The other main results of the paper are separate missions of this series:
Contributions are welcome on any item: proofs of (11.2) and (11.3), and of the p. 188 companion. The companion needs two auxiliary facts: a tangle of order in a subhypergraph yields one of order in , and tree-width is bounded by bag size.
Tree-width measures how closely a graph resembles a tree. It is the central width parameter of the Graph Minors series of N. Robertson and P. D. Seymour, which proves that finite graphs are well-quasi-ordered by the minor relation, and it governs the complexity of many algorithms: problems that are NP-hard in general become solvable in linear time on graphs of bounded tree-width (Courcelle's theorem). Branch-width, introduced in Graph Minors X (Robertson, Seymour 1991), is a second width parameter, defined from ternary trees whose leaves carry the edges of the graph. It is the natural parameter for the paper's main minimax theorem, which equates branch-width with the maximum order of a tangle, the obstruction to small decompositions.
Section 5 of Graph Minors X shows that the two parameters are equivalent, within a factor 3/2. This is what transfers the tangle duality from branch-width to tree-width, and it is why later work (for instance on matroid branch-width and on rank-width) treats branch-width as an interchangeable substitute for tree-width.
All objects are finite. A hypergraph has a vertex set , an edge set , and an incidence relation; the ends of an edge are the vertices incident with it, and an edge may have any number of ends. is the maximum number of ends of an edge, or if . A subhypergraph consists of subsets of and such that every end of a chosen edge is a chosen vertex; unions, intersections and inclusion of subhypergraphs are taken setwise.
A tree is a connected non-null graph without circuits; its leaves are its vertices of valency at most , and it is ternary if every valency is or .
A branch-decomposition of is a pair with a ternary tree and a bijection from the leaves of onto . The order of an edge of is the number of vertices of such that is an end both of an edge labelling a leaf in one component of and of an edge labelling a leaf in the other. The width of is the maximum order of an edge of , and the branch-width is the minimum width, or if .
A tree-decomposition of is a pair with a tree and a subhypergraph of for every , such that
Its width is , and the tree-width is the minimum width; exactly when . Each part is a subhypergraph and each edge lies in exactly one part, which differs from the familiar vertex-bag tree-decompositions of graphs, but gives the same tree-width on graphs.
The tangle number is the maximum order of a tangle in (p. 154), or if there are none.
The result. (5.1) shows that branch-width and tree-width bound each other up to the factor and the edge-size correction, and the page records that both bounds are attained ( with for the right-hand side, minus a perfect matching for the left-hand side). Together with the minimax theorem (4.3) of the same paper, unless and , it yields (5.2): tangles are, up to the factor , the exact obstruction to tree-decompositions of small width. That duality is the form in which tree-width enters the later papers of the Graph Minors series.
Formalizing it. The result is proved (1991); no machine-checked proof of it is known to exist. The platform holds tree-width statements for simple graphs with vertex bags (Graph Minors V, RobertsonSeymour1986.GM5.treewidth_le_theta9 and excluding_planar_graph), which are a different theorem about a different object. This mission formalizes the hypergraph tree-decomposition and branch-decomposition of Graph Minors X and the comparison between them. The companion missions of this series are Graph Minors. X. Obstructions to Tree-Decomposition I (the minimax theorem (4.3)), III (the grid tangle (7.3)), IV (the tree-decomposition separating distinguishable tangles (10.3)) and V (the structure theorem (11.1)).
The second inequality converts a branch-decomposition into a tree-decomposition; the difficulty is to obtain the bound with the floor and the separate term exactly, not up to an additive error.
The first inequality is where the obvious approach stalls: a tree-decomposition of minimum width is not a branch-decomposition. Its tree may have vertices of any valency, its leaves may carry no edge or several, and an edge may sit at an internal vertex. The three claims of the proof normalize an optimal tree-decomposition step by step without increasing its width. Each step modifies a tree on a finite vertex type while preserving three structural conditions (covering, edge-disjointness, the path condition), and the final step, suppressing vertices of valency , must be shown to produce a ternary tree with the edge orders bounded by part sizes. Most of the formal work is this tree surgery.
V, E with [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154) and a hypergraph G : Hypergraph V E given by its incidence relation.SimpleGraph (Fin n) with IsTree (connected, hence non-null, and acyclic). A leaf is a vertex of valency at most ; valency is (T.neighborSet t).ncard.sInf of the widths, which is a genuine minimum because a branch-decomposition exists when .sInf in of all bounding every ; the set is nonempty (one-vertex tree with ) and bounded below by , so the sInf is the minimum width and not a junk value.3 * β / 2; the ceiling would be a weaker statement. In (5.2), is stated as , which is equivalent.Infrastructure needed and reusable beyond this mission: tree surgery on SimpleGraph (Fin n) (attaching a leaf, deleting a leaf, splitting a vertex, suppressing valency-2 vertices), the existence of branch-decompositions for , and the computation of sInf-defined widths. Contributions of such lemmas, of proofs of the individual claims, and of small examples (, grids) are welcome.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out, using Chebyshev-type lower bounds for and a Selberg sieve whose singular-series weight was crude. The entry hit the limit of that crude weight. This entry replaces it by the sharp weight , using the platform's proved prime-pair sieve (TaoFivePrimes.siebert_prime_pair_bound, Siebert's bound as used by Riesel–Vaughan) and its PrimePairSieve components. No zeta-zero input is used.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem. Write for the scale and for the twin-prime constant.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
PrimePairSieve nodes.The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform and imported: TaoFivePrimes.siebert_prime_pair_bound, PrimePairSieve_reciprocal_weighted_sifted_bound, PrimePairSieve.divisor_kernel_comparison, PrimePairSieve.reciprocal_base_denominator_dominates_threshold, PrimePairSieve.sieve_constants_certificate, Schnir.basis_of_density.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.
We strengthen the previously formalized bound to for deterministic APSP on directed graphs with polynomially bounded integer weights and no negative cycles, using the same word-RAM model. It formalizes the improvement outlined by Alman and Vassilevska Williams in their conclusion.
Many approximation results in probability and operations research take the form of a sequence of discrete or jump-driven systems converging to a diffusion or another limit process. When the approximating systems are written as stochastic integral equations, , the key step is to show that the stochastic integrals converge whenever the integrands and the integrators converge. That this is not automatic was known from the work of Wong and Zakai (1965): smooth approximations of Brownian motion produce a Stratonovich, not an Itô, limit. Kurtz and Protter (1991) give a condition on the integrators under which convergence in distribution of the pair (integrand, integrator) in the Skorohod topology implies convergence in distribution of the triple (integrand, integrator, integral). The result is essentially the theorem of Jakubowski, Mémin and Pagès (1989), with a formulation and proof that avoid the general theory of semimartingale characteristics. It underlies diffusion approximations for queueing and storage networks, approximation schemes for stochastic differential equations, and limit theorems for statistics and filters that are written as stochastic integrals.
Time is . A path in a metric space is cadlag if it is right-continuous and has a left limit at every ; is the set of cadlag paths, and . Let be the set of continuous, strictly increasing maps of onto itself. Cadlag paths converge to in the Skorohod (J1) topology if there are with and uniformly on bounded intervals. For a product space the pair converges if one sequence serves both components; this is strictly stronger than convergence of each component.
Let be the real matrices. For a -valued process and an -valued process , the stochastic integral (1.7) is
the limit in probability along partitions of whose mesh tends to zero. Throughout, means . An -adapted cadlag process is a semimartingale if with an -local martingale and of finite variation on bounded intervals, with total variation on . denotes the quadratic variation.
For let and
which collects the part of the jumps larger than ; then has jumps of size at most . Condition C2.2(i) on a sequence asks for decompositions such that for each there are stopping times with and . denotes convergence in distribution.
For each , let be -adapted with paths in , an -semimartingale satisfying C2.2(i) for some . If in the Skorohod topology on , then is a semimartingale with respect to a filtration to which and are adapted, and
The result. Theorem 2.2 reduces convergence of stochastic integrals to two checks: joint convergence of integrand and integrator, and the uniform control C2.2(i) on the integrators. Remarks 2.3 and 2.5 give simple sufficient conditions (stochastic boundedness of plus a second-moment bound; relative compactness for a fixed integrator), and Section 5 of the paper derives from it weak limit theorems for stochastic differential equations driven by semimartingales, including Wong–Zakai-type corrections. Without the theorem, each diffusion approximation that passes through an integral equation needs its own ad hoc argument.
Formalizing it. The theorem is proved and classical; nothing here is open. Lean's Mathlib has no Skorohod space, no stochastic integral against a semimartingale and no semimartingale, so the mission produces the first machine-checked definitions of J1 convergence on , of the left-point stochastic integral (1.7), and of convergence in distribution of cadlag processes, together with the deterministic facts about them that a proof of Theorem 2.2 needs. The definitions are meant to be reused by later missions on weak convergence of processes and on stochastic differential equations (the paper's Theorem 5.4 is planned as a follow-up that references them).
The obvious argument — the integral is a continuous function of the pair (integrand, integrator), so the continuous mapping theorem applies — fails in two ways. First, the map is not continuous in the Skorohod topology, and for a general semimartingale integrator it is not even defined path by path. Example 1.1 makes the failure concrete: with and , each component converges, yet for while , because the jumps of integrand and integrator coalesce in the wrong order; joint convergence of the pair excludes this. Second, Example 1.2 shows that joint convergence is still not enough: integrators whose variation grows without bound (piecewise linear interpolations of Brownian motion) produce an extra drift in the limit. C2.2(i) is the condition that excludes this, and the identification of the limit integral also requires knowing that the limit is a semimartingale, which is not given.
Time is ℝ≥0; a process is a map ℝ≥0 → Ω → E. is Fin m → ℝ and is Fin k → Fin m → ℝ, with the sup metric; products carry the max metric (J1 convergence does not depend on the product metric). The conventions the formal statements commit to:
The theorem has trivializing formalizations, all excluded here: componentwise convergence of in place of joint convergence; an integral not pinned to (1.7) (any process would do); and assuming the limit integral, or the semimartingale property of , as a hypothesis.
Local martingales and cross variations reuse the published Ethier–Kurtz definitions EthierKurtz_IsSourceLocalMartingale and EthierKurtz_HasCrossVariation. A complete development needs the Skorohod space and its tightness theory, the stochastic integral against semimartingales (existence and the Burkholder–Davis–Gundy/Doob estimates), and the quasimartingale criterion of Meyer and Zheng. Contributions to any of these layers are welcome; the deterministic milestones (Lemma 2.1, Lemma 6.2, the continuity of , (1.12)–(1.13), Lemma 6.1) are independent of the probabilistic ones and reusable for any work on the J1 topology.
Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve , where averages a random integrand over observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.
When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation
where is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of : the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.
Let be a separable Banach space with norm , and let be the Euclidean norm on and . A multifunction assigns a set to each . Its graph is and its inverse is .
For sets indexed by , the upper limit consists of the points with , for some , and the lower limit of the points reachable along every such sequence. The contingent derivative of at is the multifunction with
is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when as and . A single-valued is B-differentiable at when in the same sense.
The deterministic problem is with , data and solution map . At a reference pair set . The analytical assumptions M.1–M.4 are as follows. is jointly continuous and B-differentiable in each variable, with the -derivative strong (uniform in near ). is closed and proto-differentiable. is subinvertible: , and a closed-graph, convex-valued selection of near passes through . The contingent derivative is at most single-valued.
The statistical problem has i.i.d. random elements of a measurable space and an integrand on a compact neighborhood of . It satisfies the probabilistic assumptions P.1–P.4: continuity in , measurability in , a finite second moment at one point, and a Lipschitz bound with . The M-estimate is a measurable solution of
and the true equation is with .
Under P.1–P.4 on a compact neighborhood of , B-differentiability of at , and M.2–M.4 for , every sequence of measurable solutions of (2.5) with almost surely satisfies
The goal fixes the limit law completely: the map is the contingent derivative of , and the Gaussian has the covariance of the integrand at .
The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.
Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When is the normal cone of a polyhedron, is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.
The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.
The classical argument linearizes at , inverts the Jacobian and applies the delta method. Here is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from . The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.
The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function , so convergence of at finitely many points is not enough. The central limit theorem must hold in the sup norm on , which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.
Points live in EuclideanSpace ℝ (Fin n), and is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ( is 𝓝[>] 0, and is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. is s 0, empirical means sum over Finset.range ν, and (2.5) is required for . is empty off . Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of is fixed through linear functionals: . In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.
Explicit choices relative to the printed text:
The conclusion of the goal names its limit: the image of the stated Gaussian under a map whose values lie in the contingent derivative of . A statement asserting only that converges in distribution to some limit, or replacing by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with , ).
A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.
A flexible manufacturing system is a set of machines through which parts of several types travel along fixed routes; each machine serves several buffers and must pay a set-up time whenever it switches from one buffer to another. Real-time scheduling decides, as the system evolves, which buffer each machine works on. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989) introduced simple distributed policies for this problem, of which the most natural is the clearing policy: a machine keeps working on a buffer until it is empty, and only then switches. They proved that every clear-a-fraction policy, a subclass of clearing policies, keeps every buffer bounded on acyclic systems whenever each machine has spare capacity, and left open whether clear-a-fraction policies stabilize all systems in which material flows around cycles.
Kumar and Seidman (IEEE Trans. Automat. Control 35(3), 1990, doi:10.1109/9.50339) answered no. Their Example 1 is a single part type that visits two machines in the order 1, 2, 2, 1. Every machine has spare capacity, yet under the clearing policy the buffer levels grow without bound, and they do so even when all set-up times are zero, so the instability comes from machines starving each other rather than from time lost to set-ups. Until then, instability had been suspected to require positive set-up times. Shortly afterwards Lu and Kumar exhibited instability of a static buffer-priority rule in a re-entrant network (IEEE Trans. Automat. Control 36, 1991); together these examples started the study of stability of multiclass queueing networks.
A manufacturing system has part types arriving at rates . Parts of type follow a route of length : their -th operation is at machine , and they wait for it in buffer , where each part needs processing time . Machine serves the buffers , and switching from to costs set-up time .
Flows are continuous (fluid). The level of buffer at time is , where is its cumulative output and its cumulative input: for the first buffer of a route, and the output of the preceding buffer otherwise. Each machine works in runs: run is a set-up phase of length followed by a processing phase on buffer , during which the buffer is drained at rate while it is nonempty and passed through at its inflow rate when it is empty. The system is stable if for every buffer.
A clearing policy (Definition 1) is one in which a machine processing continues until the first time that is empty and some other buffer of the same machine is nonempty, and then commences a set-up for one of the nonempty buffers.
Example 1. One part type arrives at rate and visits machine 1, machine 2, machine 2 and machine 1; its buffers are , so and . Processing times are , and is the time to set up to buffer . The parameters satisfy the critical condition and the capacity condition
The initial state is , with machine 1 set up for buffer 4 and machine 2 set up for buffer 3. Write
Assume (3)–(5).
For large enough, every clearing trajectory from reaches, at ,
with machines 1 and 2 again set up for buffers 4 and 3.
With zero set-up times and any , every clearing trajectory reaches, at ,
with machines 1 and 2 again set up for buffers 4 and 3.
The example shows that the condition on every machine, which is necessary for stability and sufficient for the existence of some stabilizing policy, does not make natural distributed policies stable once material flows around a cycle. The throughput of the line falls to part per unit time although each machine could handle the demand. This motivates the paper's two positive results: sufficient conditions under which clear-a-fraction policies are stable (Theorem 1), and a supervisory mechanism that stabilizes any policy (Theorem 2), which are the subjects of the other missions of this series. The example is also an early instance of the phenomenon later studied as instability of multiclass fluid networks under work-conserving policies.
The paper's argument is a stage-by-stage computation of piecewise linear trajectories. No machine-checked version of it exists. A formal proof has to make precise what the paper leaves to the reader: that the clearing rule determines the trajectory, that the stage formulas are what that trajectory does, and that the cycle can be restarted. The formal model of runs, set-ups and the clearing rule built here is the same as in the other missions of the series.
The arithmetic of each cycle is routine once the trajectory is known. The difficulty is in the universal quantifier: the claim covers every clearing trajectory, and the clearing rule is defined implicitly, through "the first time thereafter" at which a buffer is empty and another one is nonempty. At several switching instants the buffer a machine switches to is empty and only starts to fill at that instant, and with zero set-up times a machine may begin a run at an instant where the switching condition already holds. Showing that each switch happens exactly when the paper says, and that the fluid levels then follow the printed formulas (including the reduced rate of a machine working on an empty buffer), is a uniqueness argument for a hybrid system, not a simulation. The existence half asks for the converse: an explicit trajectory, defined for all time, with infinitely many runs whose start times tend to infinity.
Fin P, machines Fin M, buffers ⟨p, i⟩ with i : Fin (n p), paper index = Lean index ), instantiated as Example 1 with , route , and for ; staying on a buffer costs nothing.Useful contributions include lemmas about fluid trajectories that do not depend on the example (continuity of levels, the pass-through rate on an empty buffer, restarting a trajectory at a run boundary), which also serve the other missions of the series.
Comparison theorems for stochastic processes answer a practical question: if one system starts "lower" and moves "upward" less aggressively than another, does it stay below the other one for all time? Queueing, reliability and inventory models use such statements to order performance measures of two systems without computing either distribution. Results of this kind for real-valued Markov chains go back to Kalmykov (1962) and Daley (1968); O'Brien (1975) proved a comparison theorem for real sequences with general (non-Markov) dependence on the past.
Kamae, Krengel and O'Brien (1977) placed these results on a common foundation: an arbitrary partially ordered Polish space, where the state can be a vector, a path, a configuration or a measure. Their tool is a characterization of the stochastic order through monotone couplings, which goes back to Strassen (1965).
Timeline.
Let be a complete separable metric space with a closed partial order (the set is closed in ) and its Borel -algebra. Write for the probability measures on . A set is increasing if and imply ; a function is increasing if implies . For , is stochastically smaller than , written , if
A stochastic kernel from to assigns to every a probability measure on , measurably in . For , is the measure on with , and is its second marginal. A kernel on is upward if is concentrated on for every .
For partially ordered Polish spaces , the products and carry the product topology and the coordinatewise order, and are again partially ordered Polish spaces. Given and kernels from to (), the measure on is the law of when and is drawn from ; its projective limit is the law of the whole sequence.
Let and let be stochastic kernels from to , . If and
then there are random sequences , on one probability space, with initial laws , and conditional laws , , such that
The result. Theorem 2 turns an inequality between one-step transition laws into a pathwise inequality between whole trajectories. Every functional that is increasing in the path, such as hitting times of increasing sets, maxima, occupation counts or cumulative costs, is then ordered between the two processes, as Corollary 1 illustrates. Because the state space is any partially ordered Polish space, the theorem covers vector-valued queue lengths, networks, and processes whose state is itself a sequence, not just real chains. Theorem 1 is the basic tool for working with the order on such spaces: it converts between integrals, couplings, kernels and closed increasing sets.
Formalizing it. All results are proved in the paper (1977); none is machine-checked. The platform has the special case of Theorem 1 (i) (iv) for as an open statement (PalmQueueing.Ordering.strassen_st); the general partially ordered Polish case, and the sequence comparison, are new. A formal development yields a reusable library for the stochastic order on general ordered spaces and its interaction with Mathlib's Ionescu-Tulcea construction of process laws (Kernel.trajMeasure).
The obvious argument for Theorem 2 couples the processes step by step: couple , then, given the two histories, couple , and so on. Each step needs a monotone coupling of and chosen measurably in the pair of histories; the existence of one coupling for each fixed pair (Theorem 1) does not by itself give a kernel.
Theorem 1's central implication, from the integral inequality to a coupling supported on the closed set , is Strassen's theorem. On it follows from quantile functions; on a general ordered space there is no such formula. Passing from finite horizons to the infinite sequence is a further step, since an ordering of every finite-dimensional marginal must be turned into an ordering of the infinite-dimensional laws.
[TopologicalSpace E] [PolishSpace E] [MeasurableSpace E] [BorelSpace E] [PartialOrder E] [OrderClosedTopology E]. This is the paper's standing assumption (Sec. 1, p. 899) and is carried by every theorem, also where a statement says only "Polish space". All sets and functions the paper quantifies over are measurable, also by the standing assumption.StochLE P₁ P₂ is defined through bounded measurable monotone functions, exactly as on p. 899. It is not defined through increasing sets, closed increasing sets or couplings, so none of the milestones holds by definition.E (i - 1), X (i - 1), and the paper's kernel () is p (n - 2) : Kernel (Π i : Iic (n - 2), E i) (E (n - 1)), the signature of Mathlib's Ionescu-Tulcea API.Kernel.trajMeasure P₁ p. Corollary 1 is stated about these laws directly. The goal therefore cannot be met by coupling only one-dimensional marginals or finite prefixes; it asserts the joint laws of the full sequences and one almost-sure event for all indices.EReal, and "the expectation exists" means the two parts are not both infinite; expectations equal to are covered.[AddCommGroup E] [Module ℝ E] [ContinuousAdd E] [ContinuousSMul ℝ E] plus the hypothesis that translates of increasing sets are increasing.Welcome contributions: proofs of the milestones, in particular Strassen's coupling theorem on partially ordered Polish spaces, a measurable-selection lemma for monotone couplings, and general lemmas relating StochLE to increasing sets.
The source is the published version (The Annals of Probability), and printed page = PDF page + 898 throughout.
An investor in a continuous-time market chooses, at every instant, how to split wealth between a bond and stocks and how fast to consume, so as to maximize expected utility of consumption and terminal wealth. Without constraints on the portfolio, this problem was solved by the martingale method: Pliska (1986), Karatzas, Lehoczky and Shreve (1987) and Cox and Huang (1989) showed that in a complete market the optimal terminal wealth and consumption are explicit functions of a single state-price density, and the portfolio that finances them comes from the martingale representation theorem.
Real investors face constraints: no short selling, no borrowing, a cap on the fraction of wealth in a sector, an incomplete market in which some stocks cannot be traded at all. Each makes the market effectively incomplete, and the single state-price density no longer exists. Karatzas, Lehoczky, Shreve and Xu (1991) treated incompleteness, Xu (1990, thesis) short-selling prohibition, and He and Pearson (1991) short-sale constraints in a general setting. Cvitanić and Karatzas (1992) unified these cases: the portfolio must take values in an arbitrary nonempty closed convex set , and the problem is embedded in a family of auxiliary unconstrained markets indexed by a dual process . This mission formalizes the paper's central characterization, Theorem 10.1, and the results its proof rests on.
A standard Brownian motion in lives on a complete probability space with its augmented filtration , on a finite horizon . The market has progressively measurable interest rate , appreciation rates and volatility matrix , with , , , and a relative risk with . The state-price density is , with and .
A portfolio gives the proportions of wealth in the stocks, a consumption rate is , and the wealth solves
The pair is admissible, , if . With utility functions , (strictly increasing, strictly concave, , , ), inverse marginals and conjugates , the investor maximizes
over , the admissible pairs with integrable utility losses and almost everywhere. The value is .
The support function drives the duality. For in the class of square-integrable processes with , the auxiliary market has interest rate and appreciation rates , state-price density and unconstrained value . For in the subclass (where is finite for all ), let solve . The -optimal consumption, terminal wealth and wealth are , and .
Five conditions are considered for a capital : (A) optimality of a pair , together with ; and, for , (B) financibility: some with finances in ; (C) minimality: for all , with attained by ; (D) dual optimality: minimizes over ; (E) parsimony: for all . The theorem asserts
and, under the conditions (5.8) ( nondecreasing), (8.25) (a uniform growth bound ) and (12.2) (finiteness of the dual functional for some ), that (A) implies (B)–(E) for some with .
In proof order: the conjugate inequalities (5.5)–(5.6); the budget constraint (3.6); the unconstrained solution (Lemma 7.2, Proposition 7.3, Theorem 7.4); the embedding (8.14), ; Proposition 8.3, (B) optimality; the constrained budget constraint (9.4) and the hedging Theorem 9.1, (E) (B); and Appendix A's Lemma A.1, Lemma A.2 and Proposition A.4, the steps of (A) (B).
Theorem 10.1 turns a constrained stochastic control problem into a family of unconstrained ones plus a minimization over the dual process . Condition (D) is a convex minimization over that does not involve portfolios. It leads to the dual problem of Section 12, whose solvability gives existence of optimal constrained policies (Theorem 13.1, the companion mission). Section 9's hedging theorem is the superreplication principle under convex constraints, the basis of later work on constrained hedging and pricing. With logarithmic utility the theorem gives explicit optimal policies, and for deterministic coefficients the dual problem reduces to a deterministic one.
These results are proved in the paper, which is the standard reference for the convex-duality approach. To our knowledge they have no machine-checked proof. The mission's statements also produce a reusable Lean model of a continuous-time Itô market with stochastic coefficients, admissible portfolios, consumption, utility functions and their conjugates.
The obvious argument, Lagrange duality for subject to , fails at the first step: the constraint is on the control process, not on terminal wealth, so there is no static budget constraint to dualize. The paper's dual variable is a process, and for each candidate it changes both the interest rate and the drift. The direction (B) (A) is relatively direct. The direction (E) (B) is a hedging theorem under convex constraints (Theorem 9.1), where financing a claim requires the portfolio to land in and to satisfy the complementary-slackness identity , which no unconstrained construction delivers. The converse (A) (B) must produce the dual process from an optimal pair that is only assumed to exist, and the paper needs the extra growth conditions (5.8), (8.25), (12.2) for it. In Lean, stochastic integrals for integrands that are square integrable only almost surely, the martingale representation theorem for the Brownian filtration, and the product rule for Itô processes are not available in Mathlib.
Processes are functions constrained on ; vectors are EuclideanSpace ℝ (Fin d), matrices Matrix (Fin d) (Fin d) ℝ. The Brownian motion is the published EthierKurtz.IsStandardBrownian. The stochastic integral is a binder I, constrained only by the standing hypothesis that it is an Itô integral for every locally square-integrable integrand. This almost-sure variant of EthierKurtz.HasBrownianItoIntegral uses the published dyadic step helpers itoStepValue and itoStepSum. The hypothesis is satisfiable, by the classical construction.
The following readings are explicit in the Lean.
A formalization in which the stochastic integral is an unconstrained function, a wealth process need not solve its equation, or is real-valued (so that over an unbounded set returns ) would make the statements vacuous or false; each is ruled out above. The proof will need almost-surely-square-integrable Itô integrals, Itô's product rule, nonnegative local martingales as supermartingales, and martingale representation in the Brownian filtration. All of these are reusable well beyond this mission, and contributions of any of them are welcome.
A firm that will receive or deliver a quantity of a commodity, currency or security at a future date carries price risk until that date. When the asset itself cannot be traded in the meantime, the standard instrument for reducing that risk is a futures contract on a correlated asset: the firm takes a position in futures and adjusts it over time, and the gains or losses of the futures position offset part of the movement of its commitment. Choosing that position is the hedging problem. The classical answer, the minimum-variance hedge ratio, is a static one-period rule. Duffie and Richardson (Ann. Appl. Probab. 1991) solved the dynamic version in continuous time with a quadratic criterion: minimize the expected squared deviation of terminal wealth from a target. Their explicit feedback solution became a reference point for the later literature on mean-variance hedging in incomplete markets (Schweizer, Gouriéroux–Laurent–Pham, and others), where the same quadratic criterion is studied under general semimartingale prices.
Fix a horizon and a probability space carrying a two-dimensional standard Brownian motion with its filtration . Let be bounded measurable functions on , with bounded away from zero and . The Brownian motion has instantaneous correlation with . The committed asset and the futures price follow
The hedger is committed to units of at time . A trading strategy is a progressively measurable process (the futures position) with ; denotes the set of them. Its futures gain is the stochastic integral , and the terminal wealth is . Given a target level , problem (3) is
With , the tracking process is , so that , and the feedback map is
where solves , . The strategy depends only on the gains realized so far and the current price .
for every commitment , every target and every solution of (10). No constant is hard-coded: the statement is the paper's for arbitrary coefficients satisfying the standing hypotheses.
Two further items, not milestones, formalize §4: Lemma 3 (a solution of (3) is mean-variance efficient) and §4.1 (maximizing the quadratic utility , , is problem (3) with ).
Proposition 1 gives the optimal dynamic hedge in closed feedback form for every target level at once. Varying traces out the whole mean-variance frontier of terminal wealth (Lemma 3), and the choice solves the quadratic-utility problem (§4.1); the minimum-variance hedge of §4.3 of the paper is obtained by optimizing over . The result is also an instance of a general pattern: a quadratic hedging problem in an incomplete market reduces to an projection onto the space of attainable gains, and the projection is computed by a linear SDE.
The result is proved in the paper, in six pages. No machine-checked version of it, or of any continuous-time hedging result, exists on the platform. A formalization requires Itô's formula for products of Itô processes, the zero-mean property of square-integrable stochastic integrals, Fubini's theorem for moments, and existence for a linear SDE with an Itô-process forcing term; each of these is reusable well beyond this paper.
The projection step (Lemma 1) is Hilbert-space geometry and the final ODE step is Grönwall. The difficulty lies in between: the orthogonality must be verified against every trading strategy , about which only is known. A computation that treats as bounded, continuous or simple does not suffice. Making the paper's moment computations rigorous requires controlling the integrability of products such as and , proving that the stochastic-integral parts of Itô's product rule are true martingales rather than local martingales, and differentiating expectations in time when the coefficients are only measurable, so that derivatives exist only almost everywhere.
The stochastic layer is the published definition file Peng1990_SMP_Stochastic (the Itô integral and Itô processes on time), imported, not redefined. The mission commits to the following conventions.
Proposition 1 would hold vacuously if equation (10) had no solution; the existence milestone rules this out and must be proved, not assumed. Contributions are welcome on Itô's product formula and the martingale property of Itô integrals in the Peng framework, on the existence of solutions of linear SDEs, and on the Grönwall-type uniqueness for (13).
A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition of players is assigned the set of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.
Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.
The players are . A coalition is identified with its characteristic vector , and . A fuzzy coalition is a vector of participation rates with support . Write , for the vectors vanishing off , for its nonnegative part, and for the vectors strictly positive on .
A fuzzy game without side payments assigns to each a nonempty, closed, convex set . Each is comprehensive, meaning , and bounded above, meaning for some . The map is positively homogeneous: for every . Its core is the set of such that for every fuzzy coalition . With the support function and the simplex , a weak (resp. strong) canonical cooperative equilibrium is a together with a (resp. with all coordinates positive) satisfying for every .
A usual NTU game lives on a family of coalitions that contains and every singleton. For each , the set is nonempty, closed, convex, comprehensive and bounded above. A balance of is a vector of weights on with for every , and is the set of balances of . The fuzzy extension of the game is
and the game is balanced if .
For a balanced game without side payments,
and in particular .
Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer , that sandwiches the core.
The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.
Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each , so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map at , Ky Fan's inequality on a truncated simplex where all , and a limit as . That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in and convex and lower semicontinuous in . Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.
All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.
Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. is encoded as "vanishes where ", which equals for .EReal, so an unbounded supremum is and never a junk .The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: is a superadditive fuzzy game, and is a balanced game on every admissible , with in both cores.
Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.
Alternating-offer bargaining asks how an agreement is selected when two people can keep making proposals until one accepts. A prediction based only on behavior at the start may rely on threats that would no longer be sensible after a rejection. Ariel Rubinstein's 1982 paper studies strategies after every possible sequence of offers and gives a characterization of the partitions compatible with perfect equilibrium. Its setting has a unit pie, complete information, no fixed last round, and preferences that may describe more than a particular discount formula.
The question matters for sequential bargaining models in which the order of moves and the cost of delay affect the agreement. The paper distinguishes the set obtained when player 1 offers first from the set obtained when player 2 offers first. It also provides applications to fixed bargaining costs and fixed discount factors. This mission targets the paper's general characterization, from which those examples can be studied without building a new equilibrium concept for each preference family.
A partition is a number : player 1 receives of the unit pie and player 2 receives . An outcome means that the offer is accepted in period ; denotes perpetual disagreement. Periods of actual play start at 1. The paper also uses when comparing acceptance of a current offer with a future outcome. Each player has a complete, reflexive, transitive preference relation on outcomes. Strict preference and indifference are derived from it.
The game alternates proposals and responses. One player offers a partition, the other accepts or rejects, and rejection makes the responder the next proposer. A strategy specifies what a player does after every possible history, including histories inconsistent with the player's earlier plans. A perfect equilibrium requires the relevant player's continuation to withstand every alternative continuation strategy at each rejected history and to make a planned acceptance or rejection consistent with the current offer. The empty history is included, so the opening proposer must also have no profitable deviation.
Write for the set of player-1 shares reached by perfect equilibria when player 1 opens, and for the corresponding set when player 2 opens. Perpetual disagreement contributes no share to either set. Define by a pair of one-period thresholds: for , is the smallest share whose immediate acceptance player 1 weakly prefers to , and is the largest share whose immediate acceptance player 2 weakly prefers to . Let and be its coordinate projections. All four sets contain numbers interpreted as player-1 shares, even when player 2 moves first. These are the objects of Sections 2–5.
Under the paper's five preference assumptions (A-1)–(A-5), the goal is its THEOREM on p. 106:
with and nonempty closed intervals and some satisfying
The translation parameter is allowed to be zero, and either interval may be a single point. The goal fixes the paper's general shape without choosing a particular utility representation or assuming immediate agreement in every equilibrium.
The attack path follows Lemmas 1–4 and Propositions 1–4 in their printed order. The lemmas constrain how a partition in one opening order relates to a feasible continuation in the other. Proposition 1 places each pair in inside ; Proposition 2 asserts existence; Proposition 3 describes as a closed segment parallel to the diagonal; Proposition 4 gives the reverse containment of and in the threshold projections. Each numbered result is a separate theorem target.
The theorem identifies the full set of equilibrium partitions from preference comparisons one period apart. Nonemptiness says the model admits at least one equilibrium partition in either opening order. The interval conclusion describes cases with multiple equilibrium shares, while the translate relation states exactly how reversing the first mover changes the two sets. In the paper's discounting example, a single share is selected under the stated parameter conditions; in a fixed-cost boundary case, multiple shares can occur. These are applications in Section 6, not assumptions of the general target.
Rubinstein proved the result in 1982. Here the definitions and theorem statements are Lean drafts; the numbered targets and the main theorem still require machine-checked proofs. A local verification module establishes that one discounting instance satisfies the first three axioms and that the paper's Section 3 strategy example accepts its first offer in period 1. Completing the mission would give a reusable formal account of an infinite-horizon alternating-offer game and its subgame equilibrium conditions, alongside the paper's characterization.
A first-round equilibrium condition does not control what a strategy promises after an offer is rejected. The paper's equilibrium definition checks the entire continuation at every history, with the player's role changing after each rejection. As a result, showing that a proposed share is an equilibrium partition requires more than checking the opening offer: the answer and the next proposal must remain consistent throughout the game tree. The model also allows arbitrary complete preferences satisfying axioms, so a calculation with one discount function cannot establish the general theorem.
The boundary at a zero share requires care. Assumption (A-2) asserts strict preference for earlier positive shares; it says nothing directly about a player receiving zero. The printed proof of Lemma 1 invokes it for a comparison that can occur at that boundary. The local lemma drafts explicitly carry the paper's (A-4) closedness axiom to support that comparison. This added assumption, and its propagation to Lemmas 2–4, is disclosed in the audit notes rather than silently attributed to the Section 4 statement.
Lean represents as the subtype of real numbers in . Outcomes are an option type: an agreement contains a partition and a natural-number period, while none is perpetual disagreement. This prevents an endless play from acquiring a default last partition. Strategies are unrestricted functions of lists of past offers. The play uses the first accepted offer, with period number one greater than its zero-based sequence index. A subgame after a rejected history restarts the period count and swaps the opening role when the history has odd length. The perfect-equilibrium predicate includes the empty history; acceptance comparisons use period 0 for the offer already on the table.
The threshold correspondence uses actual least and greatest elements among partitions in . No real infimum or supremum supplies a default for an empty candidate set. “Closed interval” in the goal means an explicit with . “” is the image of under . Proposition 3's “parallel line segment” is the full image of a nonempty interval under . These readings exclude a vacuous equilibrium set, a disagreement-to-zero coercion, and a hard-coded discounting special case.
The common outcome and preference definitions, the history-based strategy and play, and the equilibrium predicate are reusable for other alternating-offer questions. Contributions toward their structural properties, the numbered milestones, and the full theorem are in scope. The two displayed claims inside proofs and the fixed-cost and discounting conclusions are deferred to keep this proposal on the theorem's numbered path. Existing platform entries on Nash's axiomatic bargaining solution and a sealed-offer double auction concern different objects; neither supplies this game's equilibrium definition.
Large scale unconstrained optimization often makes an exact Newton step expensive. At each iterate, Newton's method asks for a solution of a linear system involving the Hessian, and the cost of solving that system can dominate the cost of evaluating the objective. Dembo and Steihaug's 1983 truncated Newton method uses conjugate gradients to stop the linear solve early, either when the residual is small enough or when the current direction has insufficient positive curvature. The resulting direction is paired with a line search. The question for this mission is whether those early exits still give a globally reliable optimization method under the paper's assumptions. The answer, in Theorem 2.1, is that every resulting run has gradient norm tending to zero, and a positive definite Hessian at one limit point makes the whole sequence converge to that point.
The objective is a twice continuously differentiable function . Write for its gradient and for its Hessian. For every initial point , the paper assumes that the sublevel set is bounded. The formalization uses the Euclidean norm and its inner product, so the operator norm of is also Euclidean.
At a major iterate , the minor conjugate-gradient iteration starts at with residual and direction . It maintains a scalar , initialized to , alongside the usual conjugate-gradient state. Before taking its next conjugate-gradient step, it checks whether . If so, it returns when and the current approximation otherwise. If this first test fails, it takes a conjugate-gradient step and checks whether . If so, it returns . A TNCG direction is the direction returned by the first exit that occurs. The forcing value sets the residual tolerance.
The major iteration chooses a positive step length . With the minor iteration's output and , , the line search requires both sufficient decrease and a curvature condition:
The update is . A run is a sequence satisfying this rule from its specified starting point. The paper also states an alternative function-value curvature condition; this mission defines it because the local unit-step theorem discusses both choices, although the main run uses the displayed gradient condition.
For every starting point there is a TNCG run, and every run satisfies
If is a limit point of that run and is positive definite, then
The existence clause is the formal meaning of the paper's assertion that the iterates are well defined. The six milestones follow the paper's appendix: the conjugate-gradient relations of Theorem A.1; the uniform descent and direction bounds of Lemma A.2; the line-search existence and directional-derivative limit used in the proof of Theorem A.3; Theorem A.3 itself; and eventual unit-step admissibility in Theorem A.4. The companion Theorem 2.2 addresses the eventual residual exit and unit-step behavior when a run converges to a point with positive definite Hessian. These results are all stated in the original paper.
The target shows that the computational shortcut in the inner linear solve preserves a global first-order guarantee: no TNCG run can maintain a gradient norm bounded away from zero. It also identifies when the sequence has one limit, rather than merely having stationary accumulation points. The local companion result describes the regime where the truncated method can take full steps and the residual stopping test governs the minor iteration.
The mathematical results are proved in the 1983 paper, while this mission's Lean statements are open proof targets. A complete formalization would connect the finite-dimensional conjugate-gradient recurrence, the line-search argument on bounded sublevel sets, and the convergence statement in one machine-checked development. The conjugate-gradient identities and line-search facts could be reused in other optimization algorithms; the exact first-exit model and the global conclusion are specific to this method.
The minor iteration is not an ordinary positive definite conjugate-gradient solve. The Hessian may be indefinite away from a solution, and the iteration must stop at insufficient curvature before using a later residual state. A convergence argument that assumes positive definiteness at every iterate would therefore miss the case the algorithm was designed to handle. The line search must work for the returned direction, including the first iteration's steepest-descent fallback. The limit-point conclusion adds a separate issue: a vanishing gradient norm alone does not force an entire sequence to converge to a chosen limit point.
Lean represents as EuclideanSpace ℝ (Fin n), uses its Euclidean norm and inner product, and defines as the derivative of the gradient. The objective is and every sublevel set is bounded, as specified at the start of the paper. The TNCG recurrence is total, but an admissible direction must come from its first actual exit, with the curvature test preceding the residual test. At , the curvature exit returns , not the zero initial approximation. This prevents a false stationary run. The residual test is written as a product inequality, equivalent to the paper's quotient when the residual test is reached.
Step lengths are positive. A run is extended through stationary points by zero directions, giving an infinite sequence on which a limit can be stated. Theorem 2.1 imposes no extra restriction on the forcing sequence and no upper bound on step lengths. Theorem A.1 corrects the printed Krylov-space index from to . Theorem A.4 adds , needed for the conclusion and true in the paper's applications. Theorem 2.2 requires nonnegative forcing values and guards its residual-exit conclusion at stationary iterates. These corrections are recorded item by item in the moderation notes. Contributions to the conjugate-gradient identities, bounded-level-set line search, and isolated-limit-point argument are all within scope.
In Stackelberg network pricing a leader sets prices on some resources, and a follower then buys the cheapest structure available to them, paying the leader for the priced resources they use. The Stackelberg Minimum Spanning Tree problem, introduced by Cardinal, Demaine, Fiorini, Joret, Langerman, Newman and Weimann (Algorithmica 2011), is the version in which the follower buys a minimum spanning tree. The best known approximation factors for it are those of uniform pricing, which gives every priced edge the same price (Berbeglia–Joret, p. 21).
Independently, revenue management studies assortment optimisation: a seller chooses which products to offer, and customers choose among the offered products according to a discrete choice model. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) analyse the revenue-ordered heuristic (offer every product whose revenue is at least some threshold) under any regular choice model, and prove tight approximation bounds.
§4.6 of that paper shows that the two problems are the same problem: a Stackelberg Matroid pricing instance is an assortment problem under a regular choice model, and uniform pricing is the revenue-ordered heuristic on that model. The bounds of Cardinal et al. on uniform pricing thus become special cases of the general bounds on revenue-ordered assortments. This mission formalizes that correspondence (Theorem 4.16).
Choice model. Let be a finite set of products. A system of choice probabilities assigns to each offered set and product a probability , with no-purchase probability . It is regular if (i) all probabilities are nonnegative, (ii) for , (iii) , and (iv) whenever and . With revenues , and . The revenue-ordered assortment generated by is .
Greedy algorithm. Given a family of independent sets, a linear ordering and a set , scans in the order induced by , starting from , and adds each element that keeps the current set independent.
Stackelberg Matroid problem. An instance is a matroid , a bipartition into red and blue elements, and red costs ; some base of lies inside . The leader chooses prices . The customer buys a minimum-weight base by running greedy on with an ordering that is non-decreasing in weight ( on , on ) and puts blue elements first on ties. The leader earns .
The assortment instance. Let be the distinct red costs. Products are with . The auxiliary matroid on declares independent when it holds at most one pair per blue and is independent in . With an ordering of that is non-decreasing in cost and puts products before red elements on ties, if and otherwise.
For the instance above, with and every admissible :
and uniform pricing corresponds to revenue-ordered assortments: for each some revenue-ordered assortment earns the revenue of the uniform price , and every revenue-ordered assortment earns the revenue of some uniform price .
Theorem 4.16 transfers every guarantee for revenue-ordered assortments under regular models to uniform pricing in Stackelberg Matroid pricing. Specialising Theorems 3.1, 3.2 and 3.3 of the paper through it gives exactly the three bounds on uniform pricing proved by Cardinal et al. for Stackelberg Minimum Spanning Tree (Theorem 3 of their paper), which those authors showed to be tight (p. 24). It also places uniform pricing inside a general picture: it is a threshold policy for a regular choice model whose purchase probabilities come from a matroid greedy algorithm, and the paper notes that the argument extends to polymatroids.
The result is proved in the paper, with two steps left to the reader ( is a matroid) or justified briefly (rounding prices). No machine-checked proof exists. A formalization also produces a reusable greedy algorithm on finite matroids with its monotonicity properties (Lemma 4.14, (14)), which Mathlib at the pinned revision does not have.
The obvious argument identifies the customer's run of greedy on with the run of greedy on step by step. That identification fails as stated: the choice probabilities are defined with one fixed ordering of , while the customer's ordering is any ordering compatible with the prices, and ties among blue elements of equal price, or between a product and a red element of equal cost, may be broken differently. Equality of revenues therefore needs the tie-independence property (14) applied to as well as to , which in turn needs to be a matroid. A second gap is axiom (iv) for the no-purchase option: it requires that offering more products never decreases the number of products greedy selects, which is Lemma 4.14 (i)–(ii) for combined, not a pointwise statement. Finally, the paper's "" price must be handled with the red base: without a base inside , a blue element priced above all costs can still be bought and the optimum is unbounded.
Matroid α; , are Finset α with equal to the ground set; costs and prices are functions α → ℝ, used only on and . A linear ordering is a duplicate-free List covering the set; greedy on scans the whole list and skips elements outside , so is never re-sorted.α ⊕ (α × ℝ). The paper's conditions (1)–(2) for contain two typos (a missing "" and for ); the intended conditions are formalized. The price is the real number , strictly above every red cost.IsGreatest) over positive real prices and all compatible customer orderings. Cost levels are quantified as elements of the set of red costs rather than by index.Contributions welcome: proofs of Lemma 4.14 and (14) for Mathlib matroids (reusable beyond this mission), the matroid property of parallel extensions such as , and the three revenue identities.
Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.
The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.
Let be a nonempty compact decision set. An observation has population law , and is the loss at decision . The quantity of interest is the optimal-value functional
The observations are independent and identically distributed with law . Write for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights with . Indexed weights also cover samples with repeated observations. For a convex divergence generator normalized by and , its divergence from the empirical law is . Assumption A further requires to be three times continuously differentiable near ; it permits .
At radius , the divergence ball consists of the weights with . The confidence set is its image under :
Assumption B makes compact and requires to be Lipschitz on it with a measurable random coefficient . The theorem adds finite second moments for and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.
The goal is the exact asymptotic coverage of the population optimal value, with the unique optimizer and :
Here denotes outer probability, and is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of ; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set , including both sides of that interval.
The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.
A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.
Pointwise control of each loss is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over . The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.
Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first observations are indices . Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.
The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is ; the different minimax expression is not substituted. The chi square target uses the standard Gaussian measure of .
Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.
Operations research has long studied the stochastic problem : choose a decision before an uncertain quantity (demand, prices, returns) is revealed. In practice the decision maker also observes covariates before deciding (web-search volume before stocking a product, weather before routing a shipment) and should solve the conditional problem instead. Bertsimas and Kallus (arXiv:1402.5481v4; Management Science 66(3), 2020) proposed predictive prescriptions: reweight historical observations by how relevant they are to the current , using weights borrowed from a nonparametric regression method, and minimize the reweighted sample cost. Their asymptotic theorems guarantee that this procedure converges to the decision that full knowledge of the conditional distribution would give.
The unconditional special case, sample average approximation (SAA) with i.i.d. draws of and no covariate, has a classical consistency theory (Dupačová–Wets 1988; Shapiro 2003). This mission conditions that theory on , with -nearest-neighbour weights.
Decisions lie in a set , covariates in , uncertainty in ; all three spaces carry the Euclidean norm. A cost is given. Let be the joint law of , the law of and the conditional law of given . The conditional cost and the full-information problem (2) are
The data are , the first terms of an i.i.d. sequence with law . The kNN weights (12) are is one of the nearest neighbours of among , with ties among equidistant points broken by lower index first. The predictive prescription (3) is any
The paper's standing assumptions: Assumption 3 ( for every , and for a.e. ); Assumption 4 ( is equicontinuous in , uniformly over ); Assumption 5 ( closed and nonempty, and either bounded, or is bounded below for large and for each there is a set of positive conditional probability on which uniformly as ).
Definition 1. is asymptotically optimal if, with probability 1, for -a.e. , ; it is consistent if, with probability 1, for -a.e. , .
Under Assumptions 3, 4, 5 and i.i.d. sampling, with , , : with probability 1, for -a.e. , is nonempty, the argmin is eventually nonempty, and every selection from it satisfies
The goal covers both cases of Assumption 5, including unbounded such as the newsvendor's .
Theorem 5 says that a decision computed from data alone, with no model of the conditional distribution, performs asymptotically as well as the decision a decision maker with full knowledge of would take, for almost every covariate value and under mild conditions on the cost. It justifies the kNN prescription in the paper's newsvendor and shipment-planning experiments, and its proof skeleton (a pointwise strong law for the weights, then Lemmas 5–7) is reused for kernel, local-linear and recursive-kernel weights (Theorems 6–9), which could follow as missions of the same shape.
The result is proved in the paper; it has not been machine-checked anywhere. Formalizing it requires a strong law for nearest-neighbour regression with integrable responses (Walk 2010, building on Devroye, Györfi, Krzyżak and Lugosi 1994), which Mathlib does not have, and a careful treatment of conditional laws at a point. One of the paper's lemmas (Lemma 6) is false as printed for unbounded ; the formalization isolates the correct statement.
The deterministic optimization part (Lemmas 5 and 6 for bounded ) is a compactness argument. The central difficulty is the probabilistic input. A natural first idea, applying the strong law of large numbers to , fails: the kNN weights depend on all of and on , the effective sample size grows sublinearly, and convergence is required for almost every simultaneously, including that are atoms of where ties are the rule. A second difficulty is the exchange of quantifiers: the strong law gives a null set depending on and on the set , and the conclusion needs one null set for all . Finally, for unbounded the minimizers of must be kept bounded, and weak convergence of alone does not do so.
All spaces are EuclideanSpace ℝ (Fin d), so kNN distances and are Euclidean. The data are a measurable, mutually independent sequence S i : Ω → ℝ^{d_x} × ℝ^{d_y} with each term of law ; samples are indexed from . The following readings are explicit in the Lean:
μ.condKernel x of the conditional law, and is its Bochner integral; Assumption 5's "for every " refers to this version, and is measurable.A formalization that replaces the conditional law by an arbitrary kernel unrelated to , takes to be a fixed measurable selection chosen outside the almost-sure quantifier, or reads on an empty set as without Assumption 3 would trivialize or weaken the result and is ruled out by the statements above.
Needed infrastructure: nearest-neighbour ranks and their combinatorics (Stone's lemma: a point is among the nearest neighbours of at most a bounded number of others), a strong law for kNN regression, portmanteau-type characterizations of weak convergence for weighted empirical measures, and stability of minimizers under locally uniform convergence. The kNN strong law and the stability lemmas are reusable well beyond this mission. Related platform items, credited but not reused (they concern unconditional SAA): SolutionQuality.SRP.prop1_i, SolutionQuality.SRP.prop1_ii, SolutionQuality.SRP.fbar_tendstoUniformlyOn (Bayraksan–Morton 2006) and DupacovaWets.Consistency.consistency_of_measurable_estimates (Dupačová–Wets 1988). Proofs of any milestone, and alternative routes to the goal, are welcome.
Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.
The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.
Fix a dimension and a continuously differentiable function . Problem (1) minimizes over the nonnegative orthant . The positive part replaces each negative coordinate of by zero. A feasible is critical when every partial derivative is nonnegative and wherever . This is the paper's componentwise first-order condition.
For a feasible iterate , the binding set is . The paper selects a larger working set using a fixed and the projected-gradient residual , where is fixed, diagonal and positive definite. More precisely, contains the indices with and . The matrix is symmetric positive definite and has zero off-diagonal entries in the rows indexed by . The projected arc and update are
Here , and is the first nonnegative integer passing the paper's two-sum Armijo test (37), with . One sum uses the scaled gradient outside ; the other uses the actual projected displacement on . These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.
The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:
The goal is Proposition 4. Let be convex and , let be the unique minimizer on satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is , where retains Hessian entries except for off-diagonal entries touching . Then
If the Hessian is Lipschitz in a neighborhood of , the same proposition states an at-least-quadratic error bound: eventually for some . The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.
Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.
Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.
A positive definite matrix by itself does not make projection along a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.
Lean represents as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's is diag μ with every . The run predicate includes a feasible initial point and the first acceptable integer , and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs from and does not assume its invertibility, admissibility, convergence or eventual active-set equality.
Assumption (C) includes local smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no restriction, so neither does the Lean hypothesis.
A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.
A global surface of section reduces a flow on a closed 3-manifold to an area-preserving map of a surface. It is a compact embedded surface whose boundary consists of periodic orbits, whose interior is transverse to the flow, and which every other trajectory hits infinitely often in forward and backward time. Poincaré introduced the idea for the restricted three-body problem. Once a section is a disk, results on area-preserving disk maps (Brouwer, Franks) give periodic orbits and other structure for the whole flow.
For Hamiltonian flows on star-shaped energy surfaces in , equivalently Reeb flows on the tight 3-sphere, it is natural to ask which periodic orbits bound such a disk. Hryniewicz's criterion answers this for dynamically convex flows, with no genericity assumption. The answer is purely topological: a periodic orbit bounds a disk-like global section exactly when it is unknotted with self-linking number . The criterion is used in celestial mechanics: Joung and van Koert apply it to validated periodic orbits of the restricted three-body problem (arXiv:2407.19159).
Timeline.
Use coordinates on , the Liouville form and the symplectic form .
Let be smooth and set . Assume that every ray from the origin meets exactly once, and that it crosses transversally:
Then is a strictly star-shaped hypersurface diffeomorphic to . Every contact form on that matters below arises this way, up to diffeomorphism (see Formalization scope).
The Hamiltonian vector field is defined by . With this sign, on . So is a positive multiple of the Reeb vector field of the contact form , and its orbits are the Reeb orbits reparametrized. A periodic orbit is a solution with and . It is prime when is its least positive period. The contact structure is .
that is, every nonzero transverse vector turns by more than one full turn.
the linking number in , with oriented as the boundary of the star-shaped domain it bounds. This agrees with Hryniewicz's Definition 1.5, which uses a section of over a spanning disk.
For every dynamically convex strictly star-shaped and every prime periodic orbit :
The statement fixes no constants and no non-degeneracy, and it covers every dynamically convex star-shaped surface.
If is unknotted with , then fibres smoothly over . Every fibre is the interior of a disk-like global surface of section whose oriented boundary is .
Let be any disk-like global section. Every periodic orbit through a fixed point of the first-return map of is unknotted, has self-linking number , and so bounds the page of an adapted open book.
The result. The criterion turns a dynamical question into a topological check. It does not depend on whether the orbit is degenerate, and degenerate orbits are what one meets at bifurcations and on symmetric levels. Every periodic orbit in a strictly convex energy surface that is unknotted with is a binding, so the flow is organised by many open books at once. Theorem 1.8 makes this concrete: the Hamiltonian flow twists around two different bindings, and . In applications, numerically validated orbits become analytic global sections without a separate non-degeneracy check (Joung–van Koert, Theorems 1.2 and 1.5).
Formalizing it. The theorem is proved, in a 50-page paper that relies on Hofer–Wysocki–Zehnder's theory of pseudo-holomorphic curves in symplectizations. It has no machine-checked proof. Mathlib has no Conley–Zehnder index, no self-linking number, no linking number of curves in , and no global surfaces of section. A Lean statement fixes every sign and orientation convention involved: the sign of , the orientation of , which push-off defines , and the index of degenerate orbits. Each of these is easy to get wrong in prose. Formal proofs of the parts that use no holomorphic curves are valuable on their own: the necessity direction, the description of the index by winding intervals, and the explicit ellipsoid examples.
The obvious route is to approximate the contact form by non-degenerate forms that keep as an orbit, and then apply the non-degenerate theorems. This fails. The need not be dynamically convex. They can have orbits of very high action with that are not linked with , so the Hryniewicz–Salomão criterion does not apply to (Hryniewicz, p. 4). The families of planes that would give the pages for have to be controlled directly as , and this is not a formal limit argument.
A second obstruction is genuinely global. A disk spanning and transverse to the flow in its interior is easy to produce when . Showing that every trajectory returns to it is the whole content of the theorem, and no local or perturbative argument gives it.
For the formalization, nothing in the proof of sufficiency avoids finite-energy pseudo-holomorphic planes: Fredholm theory, asymptotic analysis, bubbling-off and compactness all enter. None of this exists in Lean.
Fin 4 → ℝ with coordinates ordered . , and are defined explicitly, with the sign conventions above.ContDiff ℝ ⊤) functions with the ray condition and on . The Reeb flow of a general dynamically convex form on reduces to this case, up to diffeomorphism and positive time change: such a form is tight (Hofer–Wysocki–Zehnder), and every tight form on comes from a star-shaped hypersurface (Eliashberg 1992). That reduction is not part of the targets. Hryniewicz makes the same reduction (§3, first paragraph).A contact structure on a manifold of odd dimension is a field of hyperplanes that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.
Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If , , is a smooth family of contact structures, there is an isotopy with . A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on ) is a classification up to isotopy because of it.
Timeline.
The closed manifold is a compact submanifold of Euclidean space. Let be smooth, let be compact, and assume is surjective for every . Then is a closed smooth manifold of dimension with tangent spaces
A one-form is a smooth map , restricted to . Its exterior derivative is
This is the condition in the form of Geiges' Remark 2.3. It forces to be odd. The contact structure is . Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).
For every smooth family of contact forms , , on there is an isotopy of with
stated pointwise: for , iff .
The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.
The same isotopy can be chosen with smooth functions such that
Moreover, every point at which vanishes on for all stays fixed: .
The result. Gray stability is the basic rigidity statement of contact topology.
Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of :
All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.
The proof is soft, but two steps are not formal.
It has a unique solution at each point, but only because is non-degenerate on and the Reeb vector spans the kernel of . The solution must also depend smoothly on and be tangent to ; the ambient form is in general not contact off . 2. Integrating it. The isotopy is the flow of , which must exist for all and stay on . Compactness of enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).
The tempting shortcut of asking for does not work. Contact forms themselves are not stable, as the Hopf family on shows (Remark 2.21(1)), and the conformal factor cannot be dropped.
Fin n → ℝ; is a compact regular level set of a smooth .Whether the diameter of a polyhedron is bounded by a polynomial in its number of facets is one of the central open questions of convex geometry, and it bears directly on linear programming: the diameter of the graph of a polyhedron is a lower bound on the number of pivots of any simplex method that moves along edges. Write for the largest diameter of a -dimensional polyhedron with facets. The best known bounds are
due to Klee and Walkup (1967) and Kalai and Kleitman (1992), and the gap between them has stood for decades.
A recurring approach is to isolate a few purely combinatorial properties of polyhedra and to prove bounds for every object having them. Eisenbrand, Hähnle, Razborov and Rothvoß (2010) proposed a base abstraction defined by a single property, shared by all abstractions from which earlier bounds were derived. They showed that the known upper bounds survive in it, and, as their main result, that it admits almost-quadratic diameter. This mission formalizes that lower bound.
Timeline.
Let and let be the family of its -element subsets. Consider a graph whose vertex set is a nonempty subfamily of . The graph satisfies condition i) if
for each there exists a path connecting and whose intermediate vertices all contain .
The base abstraction is the class of all such graphs; is called the dimension and the number of facets. Write for the length of a shortest – path, and
The geometry behind the definition: in a non-degenerate polyhedron every vertex lies on exactly facets, so labelling vertices by their facets gives distinct -subsets of ; and two vertices can be joined without leaving the smallest face containing both, i.e. through vertices lying on every facet common to and . Hence (the subject of a separate mission of this series).
In the Lean development, EHRR10.LowerBound.CondI V G is condition i), and EHRR10.LowerBound.InB d n V G says that is nonempty, all its members have elements, and condition i) holds.
Explicitly, there are and such that for every with there is a graph and two vertices of with . The constants and are left unfixed, so the goal survives any improvement in the constant.
There are no milestones: the source is an extended abstract that states the result without a proof and names no intermediate lemma.
The result. Since , any proof of a bound on bounds the diameter of all non-degenerate polyhedra. The paper shows that the Kalai–Kleitman and Larman bounds are of this kind. The lower bound shows the limits of the approach: an argument that uses only condition i) cannot prove a linear (Hirsch-type) bound, because grows almost quadratically in . Any proof of a linear bound must use further geometric properties of polyhedra. A polynomial, even quadratic, upper bound for is not excluded by the result.
Formalizing it. The result is proved in the literature (Math. Oper. Res. 35 (2010) 786–794); it has no machine-checked proof. A formal proof requires an explicit combinatorial construction of graphs in the base abstraction with large diameter and a probabilistic existence argument, neither of which is currently on the platform. The platform's Hirsch campaign has the same abstraction in its layer-family form (Hirsch_clf, whose description mentions the families in prose) and the proved upper bound Hirsch.clf_saturated_quadratic_bound, , on a subclass that contains the constructions of this paper; neither states the lower bound.
A long path through all of has exponential length but violates condition i): two vertices of the path generally share elements that some intermediate vertex lacks. Condition i) must hold for every pair of vertices simultaneously, which forces the vertices containing any fixed set to induce a connected subgraph. Building a long graph means arranging many -sets so that each of these exponentially many connectivity constraints holds at once while the graph distance between two vertices stays large. The authors announce that their construction relies on disjoint covering designs, and that the existence of such designs with the required parameters is obtained from the Lovász Local Lemma.
Fin n; vertices are the -sets themselves, V : Finset (Finset (Fin n)) and G : SimpleGraph V. Distinct vertices carry distinct labels.Real.log); the base only rescales .SimpleGraph.dist at least ; is not defined as a supremum, so no junk value enters. SimpleGraph.dist returns for unreachable pairs, which could only make the statement harder.The goal cannot be trivialized by a non-injective labelling (vertices are the sets), by checking condition i) only on adjacent pairs (it is required for all pairs, with kept along the whole walk), or by a zero constant ( is required).
Infrastructure that a solution needs and that is reusable beyond this mission: covering designs and disjoint covering designs over Finset (Fin n), the Lovász Local Lemma (posed on the platform as AppliedComb.ManyFaces.local_lemma_symmetric), and a toolkit for proving condition i) for graphs assembled from blocks. Contributions of any of these as separate theorems are welcome.