Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy .
Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed , but its space requirement grows like . The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in , and in . This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).
Timeline:
There are machines and jobs. If job is scheduled on machine it takes time units, a positive integer; is the processing-time matrix. A schedule assigns every job to one machine. The load of machine is , the makespan is the largest load, and is the smallest makespan over all schedules.
Fix an integer deadline and an accuracy . Assigning job to machine is long if and short otherwise. A schedule of long assignments is a partial assignment of jobs to machines using only long assignments; its long load on machine is , and is admissible if for every .
For a threshold and deadlines , the linear program (LP) of the Rounding Theorem has a variable for every pair with , the constraints for each job, and for each machine. The residual LP of is (LP) for the jobs left unassigned by , with and .
The procedure , on input , tries every admissible ; if the residual LP is feasible it takes a vertex , rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with . It answers 'no' if no residual LP is feasible. A -relaxed decision procedure answers 'no' only when no schedule has makespan at most , and otherwise returns a schedule of makespan at most . The binary search of Lemma 1 runs such a procedure on deadlines between and , where is the makespan of the greedy schedule, and returns the best schedule found.
For every , every positive integer matrix , every , every LP solver , the procedure run with exists, and the binary search driven by any such procedure returns a schedule with
Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in . It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.
The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold ).
The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than . The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent and a strict inequality.
Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to , which leaves the vertices unchanged.Real.rpow.Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.
A nonlinear program is rarely solved once. Its data are estimated, rounded, or varied on purpose in a parametric study, and an algorithm such as sequential quadratic programming replaces it at every iteration by a nearby linearised problem. Both uses need the same fact: near a solution, the Karush–Kuhn–Tucker (KKT) system should have exactly one solution for every small perturbation, and that solution should move Lipschitz-continuously with the perturbation. For problems with equality constraints only, or with strict complementary slackness, the classical implicit-function theorem gives this, as in Fiacco's sensitivity analysis (Fiacco 1976, reference [4] of the paper). Without strict complementarity the KKT system is not a smooth equation, and the classical theorem does not apply.
S. M. Robinson's paper Strongly regular generalized equations, Math. Oper. Res. 5 (1980) 43–62 introduced strong regularity to handle exactly this case. §2 of the paper proves an implicit-function theorem for generalized equations, §3 characterises strong regularity of linear generalized equations through a Schur complement, and §4, the subject of this mission, applies both to nonlinear programming. Its Theorem 4.1 identifies the conditions under which the KKT system is strongly regular. These conditions (strong second-order sufficiency and linearly independent binding gradients) became standard hypotheses in the stability theory of nonlinear programs and in the local convergence analysis of Newton-type methods.
Let be open and let , , be Fréchet differentiable. The program is
The Lagrangian is , and is its gradient in .
For a set and a point , the normal-cone operator is the set of vectors with for all when , and the empty set when . The KKT conditions of (4.1) are the generalized equation
Its middle block says , and .
A generalized equation is strongly regular at a solution (DEFINITION, p. 45) if its linearisation satisfies the following. There are neighbourhoods of and of and a constant such that, for every , the inclusion has exactly one solution in , and is -Lipschitz on .
At a solution the inequality constraints split into three groups:
Write for the Hessian of the Lagrangian in , , and . A square matrix is a P-matrix if all its principal minors are positive.
Assume are twice differentiable at and solves (4.3). Assume also:
Then
The Lipschitz constant is not fixed; the goal asserts that one exists.
A further item formalizes the example (4.9)–(4.10) on pp. 56–57: a linear generalized equation in whose unique solution satisfies the ordinary second-order sufficient condition and (b), yet is not strongly regular.
Strong regularity is the hypothesis of Robinson's implicit-function theorem (Theorem 2.1 of the paper). Theorem 4.1 therefore yields, for a parametrised nonlinear program, a locally unique and Lipschitz-continuous KKT point together with its multipliers, without strict complementary slackness. The same property underlies the local quadratic convergence of Josephy–Newton and SQP methods, and the criterion of milestone 5 is the form in which it is usually checked. The example of (4.10) shows that the ordinary second-order sufficient condition is not enough; the weakly active constraints have to be dropped from the cone on which must be positive.
All statements are proved in the paper. None of them, nor the notion of strong regularity, has a machine-checked proof on this platform. The matrix milestones (1–4) are self-contained linear algebra and can be proved independently. Milestone 3 for arbitrary symmetric matrices is a variant of Sylvester's criterion, which Mathlib does not currently state. Milestone 5 rests on §3 and the appendix of the paper (the Schur-complement criterion and the reduction of a linear generalized equation over a polyhedral set), which are the subjects of the companion missions II and III of this series.
The obvious argument would apply the classical implicit-function theorem to the active KKT equations. It fails because of the weakly active constraints. Near a constraint with can become active or inactive under arbitrarily small perturbations, so the solution map is piecewise smooth, not smooth. Uniqueness has to hold across all the pieces simultaneously, which is a combinatorial condition: the P-matrix property of a Schur complement, not the nonsingularity of a single Jacobian. Example (4.10) shows that the natural guess (nonsingularity of every piece, guaranteed by ordinary second-order sufficiency) is insufficient: three distinct KKT points can coalesce at the origin.
The analytic part is also not routine. Strong regularity concerns the linearised problem with an arbitrary small perturbation on the right-hand side, including perturbations of the complementarity block. The criterion needs the reduction of §3 and the appendix, which localises the polyhedral set around the solution.
EuclideanSpace ℝ (Fin n). The triple lives in EuclideanSpace ℝ (Fin n ⊕ (Fin p ⊕ Fin q)), the Euclidean , so the normal cone uses the standard inner product. A product type, which carries the sup norm and no inner product, is deliberately not used.The Four-Colour Theorem was proved by Appel and Haken (1976–77) and re-proved by Robertson, Sanders, Seymour and Thomas (RSST, 1997) with a simpler, fully computer-checkable argument. Both proofs rest on reducibility: a configuration is reducible when every 4-colouring of the ring around it can be modified, by Kempe-chain recolouring, into one that extends inside. RSST make this precise with a purely combinatorial notion, the consistent set of edge-colourings of a circuit (§3 of their paper), which captures exactly which boundary colourings Kempe interchanges can reach from one another.
The oldest results about consistent sets predate the computer proofs. G. D. Birkhoff (1913) analysed rings of length 4 and 5 and showed that the possible "Kempe-closed" sets of boundary colourings on such short rings are very restricted. RSST restate Birkhoff's analysis in their language as (6.3) (rings of length 4) and (6.4) (rings of length 5). These two lemmas power the short-circuit subroutine of their quadratic 4-colouring algorithm (6.5), which colours a triangulation across a separating circuit of length 4 or 5.
Timeline:
Let be a circuit of length : a cycle with edges in order, with no repeated vertices or edges. An edge-colouring of is a map .
A match is an unordered pair of distinct edges, and a signed match is a pair with . A signed matching is a set of signed matches such that for any two distinct members , : the pairs and are disjoint, and lie in the same component of with and deleted. Write for the edges covered by .
For , the colouring -fits when is exactly the set of edges with , and for each , holds if and only if . A set of edge-colourings is consistent if for every and every there is a signed matching that -fits such that contains every edge-colouring that -fits .
Two edge-colourings are equivalent if one is obtained from the other by a permutation of . On the circuit of length 5, () is the equivalence class of the colouring that is on , on and elsewhere. Then , where are the two edges sharing an end with ; , where are the other edges in order; and . In Lean these are A, C5, D5, E5, and Consistent.
With the classes of , , , , every non-empty consistent set includes one of , , , .
The result. (6.3) and (6.4) say that on rings of length at most 5 the Kempe-closed families of boundary colourings are rigid: a non-empty consistent family always contains one of a short explicit list of families. This is what makes separating circuits of length 4 and 5 harmless in a minimal counterexample and in the RSST colouring algorithm: whatever colourings one side of the circuit admits, the other side can be made to agree after Kempe changes.
Formalizing it. The Four-Colour Theorem itself is machine-checked (Gonthier, Coq), but that proof uses a different combinatorial encoding; RSST's notion of a consistent set, their signed matchings, and Birkhoff's ring lemmas in their formulation have no machine-checked version. The Four-Colour Theorem as such is not part of this mission; it is posed separately on the platform as the open goal FourColor.four_color. This mission builds the self-contained §3 layer (consistency) that RSST's reducibility computations rest on, proves two of its basic structural facts, and proves the two Birkhoff lemmas the paper uses. The definitions are reusable for a later formalization of (3.1) (lifts of tri-colourings form a consistent set) and of D-reducibility.
The statements are about finite objects: on a 5-ring there are edge-colourings, and the signed matchings have at most two matches. The difficulty lies elsewhere. Consistency quantifies over every member of , every and the existence of a signed matching together with a closure property, so a consistent set cannot be checked locally. The component condition on signed matchings is a statement about connectivity in a graph with two edges deleted, which must be connected to elementary arithmetic on the cycle before anything can be computed. An argument by brute force over all subsets is infeasible, so a proof has to pass through the structure of the classes . The paper's own proof also uses the dihedral symmetry of the 5-ring without stating it as a lemma; it is not a milestone.
SimpleGraph.cycleGraph k on Fin k; its edges are indexed by Fin k, edge being (mod ). The paper's is edge : is A 0 1, is A 0 4, is A 1 4, is A 2 4.SignType; an edge-colouring is Fin k → SignType; ℤˣ; a match is a non-diagonal Sym2 (Fin k) of edge indices; a signed matching is a Set.deleteEdges and Reachable, for both orders of every distinct pair; both halves of "consistent" are kept; equivalence uses Equiv.Perm SignType.C5 i uses edges ; D5 i uses mod 5, the order along the path , which is the reading the paper's proof requires ().A i i, and degenerate circuits.All definitions are in one file, FourColourRSST.Ring.Setting. Proofs of any item are welcome, as are lemmas making consistency decidable on small rings and the symmetry of the 5-ring under rotations and reflections.
Many problems of optimization and equilibrium reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: nonlinear complementarity problems written as , variational inequalities through the normal map, and Karush–Kuhn–Tucker systems of constrained programs. Newton's method in its classical form needs the Jacobian of , which does not exist at the points of interest. Two kinds of generalized Newton methods replace it: one uses an element of a generalized Jacobian, the other uses the directional derivative and solves for the step.
J.-S. Pang (Newton's method for B-differentiable equations, Math. Oper. Res. 15 (1990), doi:10.1287/moor.15.2.311) globalized the second kind with an Armijo line search on the merit function , the damped Newton method, and proved that its accumulation points are zeros of under suitable conditions. Three questions were left open: does the whole sequence converge to one point, how fast, and when does the line search accept the full step? L. Qi (Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18 (1993) 227–244, doi:10.1287/moor.18.1.227) answered all three in his Theorem 4.3, under semismoothness and a regularity condition on the B-subdifferential. This mission formalizes that theorem and the results it rests on.
Timeline:
Write with the Euclidean norm, and let be locally Lipschitz. The norm function is .
The directional derivative of at in direction is the one-sided limit . is B-differentiable at if exists for every and (2.1).
Let be the set where is differentiable. The B-subdifferential is the set of all limits with , (2.12). Its convex hull is Clarke's generalized Jacobian . is strongly BD-regular at if every is nonsingular. is semismooth at if over , , exists for every (2.6). The directional derivative is semicontinuous of degree 2 at if for all in a neighbourhood of (2.5).
The damped Newton method (Algorithm 4.1) fixes , , . Given with , it takes a solution of the generalized Newton equation
lets be the first nonnegative integer with
and sets , .
Take . Let be B-differentiable, let be a run of Algorithm 4.1 with for all , and let be an accumulation point of with , at which is semismooth and strongly BD-regular. Then
The goal fixes no rate constant; it asserts convergence of the whole sequence, superlinearity and the eventual unit step.
Theorem 4.3 is an attraction result: a regular zero that the damped iteration merely visits infinitely often captures the whole sequence, and from then on the method is the pure (undamped) directional Newton method with its fast local rate. Together with Pang's global theorem it gives a globally convergent method whose tail is superlinear, the standard template later followed by semismooth Newton methods for complementarity and variational inequality problems. Corollary 4.4 turns the theorem into a diagnostic: the behaviour of the step sizes decides whether a limit point solves the equation.
The theorems are proved in the paper. As far as a search of the platform shows, none of them, and no damped Newton method for B-differentiable equations, has a machine-checked proof. Formalizing them requires a reusable layer of nonsmooth analysis (directional derivatives of locally Lipschitz maps, the B-subdifferential and its local uniform invertibility) that other missions on semismooth Newton methods can import.
The local step of the obvious argument, "near the Newton step is accurate, so the Armijo test passes with ", needs two facts that are not automatic. First, the generalized Newton equation involves the nonlinear map , not a matrix; the error estimate of Corollary 3.4 goes through a representation with , together with a uniform bound on for near . Second, the Armijo test involves , whose value along a Newton direction has to be identified as . A further subtlety is global: an accumulation point only guarantees that the iterates come close to infinitely often, and the argument must show that once they are close enough they never leave, which needs the invariant ball of (4.5) and the fact that the step is exactly there.
is EuclideanSpace ℝ (Fin n) (all norms are 2-norms, as in the paper), allowed. Every statement assumes locally Lipschitz (the paper's standing assumption of §1). The B-subdifferential, semismoothness and the directional derivative are the published definitions NonsmoothNewton.Shared.bJac, NonsmoothNewton.Local.SemismoothAt and NonsmoothNewton.Local.dirDeriv. Since dirDeriv takes a default value where the limit does not exist, (3.12) is encoded as the existence of the one-sided limit with value . Nonsingularity is an explicit two-sided inverse. A run of Algorithm 4.1 records , and the minimality of ; without the minimality any would do and " eventually becomes 1" would not be the paper's claim. An accumulation point is a cluster point of the sequence; superlinear convergence is .
Added hypotheses, disclosed in each item:
The theorems are not vacuous: runs of Algorithm 4.1 exist (for the Armijo test passes at ), and a statement in which the line search index is not the first passing one, or in which is a default value, would not be the paper's theorem.
Contributions welcome: proofs of the milestones, in particular the representation and the local uniform invertibility of (Lemma 2.6), which are reusable well beyond this mission.
Many problems of operations research reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: the nonlinear complementarity problem , , becomes componentwise, and variational inequalities, KKT systems and max-type equations admit similar reformulations. Newton's method is the natural local solver, but it needs a substitute for the Jacobian at points where is not differentiable.
Timeline:
A map is locally Lipschitz throughout; the norm is the Euclidean 2-norm. Let be the set of points where is differentiable (almost every point, by Rademacher's theorem). The B-subdifferential of at is
and Clarke's generalized Jacobian is its convex hull, . The directional derivative is . is semismooth at if over , , , exists for every . A map is strongly BD-regular at if every is nonsingular.
The Newton method is
with any choice of , and the directional-derivative Newton method is with (3.11)–(3.12). In Lean, is EuclideanSpace ℝ (Fin n), is NonsmoothNewton.Shared.bJac F, is clarkeJac F, semismoothness is NonsmoothNewton.Local.SemismoothAt, and a run of (3.2) is IsBDNewtonRun F x V.
If and is semismooth and strongly BD-regular at , there is such that every , , is nonsingular with , and every run of (3.2) from satisfies
and, when for all ,
NonsmoothNewton.Local.theorem_2_3.NonsmoothNewton.Local.remark_2_17.Lemma 2.3 (degree-2 semicontinuity, p. 230); the quadratic second paragraph of Theorem 3.1; Corollary 3.3 (the directional-derivative method, p. 235); Lemma 2.2 (1) ⇔ (2); and the counterexample of Final Remark (6) (pp. 243–244), which shows that (3.12) need not be solvable near a semismooth, strongly BD-regular zero.
Theorem 3.1 is the local convergence theorem for the semismooth Newton method in the form most used later: the B-subdifferential version under strong BD-regularity is what generalized Newton methods for complementarity problems (through the min and Fischer–Burmeister reformulations) rely on, because is finite in typical piecewise-smooth examples while is a polytope that may contain singular matrices. The statement (1.9) makes the method a descent method for near the solution, which is how the paper later globalizes it (damped Newton, §4; hybrid method, §6). Corollary 3.2 is reused verbatim in the analysis of the damped method.
The results are proved in the paper; none of them is formalized. The mission produces a machine-checked version of the local theory, on top of the published B-subdifferential and semismoothness definitions of the Qi–Sun series, and makes the Clarke-to-B-subdifferential refinement available to later missions.
The Clarke-Jacobian argument cannot be copied. There, nonsingularity of the compact convex set propagates to a neighbourhood by upper semicontinuity of . Here only the extreme set is assumed nonsingular, and its convex hull may contain singular matrices. Lemma 2.6 therefore has to work with limits of genuine Jacobians, and the error estimate (3.3) has to combine an estimate stated for , namely Lemma 2.2, with the bound on , which exists only for . A second subtlety is (1.9), which needs a lower bound that does not follow from superlinear convergence alone.
is EuclideanSpace ℝ (Fin n), with the 2-norm and the spectral operator norm, as the paper fixes ("we use 2-norms"). The dimension is allowed.
Standing assumption. Every statement carries LocallyLipschitz F (§1, p. 227).
Nonsingularity is the existence of a two-sided inverse (IsInverse V W), never a junk inverse. A run of (3.2) is written without an inverse, so nonsingularity of is a conclusion.
Quantifier order. is chosen before the run and serves every starting point within and every choice . Writing "for every run there is a " would trivialize the theorem and is ruled out.
(1.9) is stated under the paper's hypothesis for all , since otherwise the quotient is not defined.
Disclosed deviations.
Infrastructure needed.
NonsmoothNewton.Shared.exists_local_bJac_control, bJac_mem_of_tendsto, isCompact_bJac.These are reusable for the other two missions of this series and for later semismooth Newton developments. Proofs of the milestones, and alternative arguments, are welcome.
Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.
The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.
Let be a finite set of workers, with . A coalition technology assigns a real output to each worker set . A one-sided allocation consists of a partition of all workers and one real salary for each worker. The parts of are disjoint and cover . Each worker has a utility that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.
The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:
It does not require each partition block to finance its own salaries. An improving coalition is a worker set with salaries for every , a strict inequality for at least one member, and . A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.
To state gross substitutes (GS), imagine identical firms, each with production . At a salary vector , a firm's profit from employing is ; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from to , then for every demanded set at there is a demanded set at containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.
Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:
The goal is the exact existence statement
Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.
The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.
The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.
A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.
Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when . Salaries and output are real. In the fictitious market, every firm uses the same , each worker's utility at every firm is , and reservation salary is zero, matching unemployment utility . The milestones retain arbitrary strictly increasing continuous functions ; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.
Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.
Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.
Branch and bound was introduced for integer programming by Land and Doig (1960) and for the travelling salesman problem by Little, Murty, Sweeney and Karel (1963). Ignall and Schrage (1965) were among the first to apply it to machine scheduling. They give lower bounds for two permutation flow-shop problems: the makespan on three machines, and the mean completion time on two. Their Appendix then asks how the method depends on the units and the origin of the data. Its THEOREM says that changing the location and the scale of all processing times changes neither the optimal sequence nor the path the branch-and-bound procedure takes.
The statement matters for computational experiments of the kind the paper reports. Run times and node counts measured on one jobset carry over to every jobset obtained from it by a positive affine change of the processing times, so a test family need only vary the shape of the data, not its location and scale. It is also a correctness property of the procedure: a branch-and-bound method whose behaviour depended on the time unit would be suspect.
There are jobs, and every job visits the machines in the same order: , then (two-machine problem), or , , then (three-machine problem). Job has nonnegative processing times (and ). Following Johnson (1954), both problems are restricted to permutation schedules. A full sequence lists the jobs in the order in which every machine processes them, and each operation starts as early as possible. The makespan of is the time machine finishes its last job. The completion time of job is the time machine finishes it, and the two-machine objective is , which is times the mean completion time.
A node is a partial sequence of distinct jobs, and is the set of the jobs it has not scheduled. For three machines, are the times the machines finish , and the lower bound (p. 401) is
For two machines, and are the minima over orderings of of two explicit sums , (pp. 405–406), and the lower bound is .
The branch-and-bound procedure (p. 402) keeps a list of nodes ranked by , starting from the root alone. At each step it removes the first node and inserts each of its children ranked into the list. On ties a new node goes before an old one (p. 403). It stops when the first node has scheduled jobs, which fixes the whole sequence. The list after steps is .
Problems (data ) and are related by a change of location and scale when
For both the three-machine makespan problem and the two-machine sum-of-completion-times problem:
The THEOREM makes the method's behaviour a function of the shape of the data alone, not of its location or scale. This justifies normalizing test data, comparing running times across jobsets that differ by a change of units, and reporting results for one representative of each class. The proof also isolates a general principle: a deterministic best-first search depends on its bound only through the order the bound induces on the nodes it compares. Milestone 6 states that principle for the procedure of p. 402 with an arbitrary bound, so it applies to any other bound plugged into the same procedure.
As far as is known, no machine-checked version of this result or of the two lower bounds exists. The formalization needs the paper's procedure, with its tie rule, as an explicit deterministic function, and both lower bounds as functions of a node. The mission produces both, along with exact shift identities for every quantity the procedure uses.
The obvious argument is "adding adds a constant to everything", and it is not literally true. The constant depends on the position of a job and on the machine, so the identities must be computed term by term: maxima over machine-availability times commute with the shift only because both arguments move by the same amount, and that fails at the first job if processing times may be negative. The paper's own accounting contains a slip, the missing factor in . Its claim that "all lower bounds" of the three-machine problem rise by is false at the root, where does not move. The run equality therefore has to use the fact that the root is never compared with another node. The minima , range over all orderings of , so their shift requires every ordering to move by the same amount. Finally, "the same path" has to be shown for the procedure's insertion with ties, step by step.
Fin n, numbered from . Processing times are real, and the shift statements and the goal assume them nonnegative, the paper's standing convention for durations. With negative times the goal is false (a three-job counterexample is recorded in the goal's statement). Scaling needs no sign condition.JohnsonFlowShop.ThreeStage.asapDone, JohnsonFlowShop.TwoStage.asapC2). Node attributes are computed by the same recursion on lists.Credit: Johnson (1954) for the reduction to permutation schedules and the published schedule definitions. No platform item treats flow-shop lower bounds or branch and bound over sequences. The nearest is the branch-and-bound mission BiconvexProg.BranchBound (Al-Khayyal and Falk), an unrelated algorithm for biconvex programs.
Labour markets match workers to firms that hire teams: a firm's output depends on the whole set of workers it employs, while each worker holds one job. A salary agreement is stable when no firm and group of workers can renegotiate among themselves to the benefit of all of them. Shapley and Shubik (1971) showed that such stable outcomes exist when each firm hires at most one worker and utility is transferable; Crawford and Knoer (1981) extended this to general utilities, still one-to-one. Kelso and Crawford (1982) let firm size be endogenous and identified the condition under which existence survives: workers must be gross substitutes for every firm. Their condition later became the standard assumption for existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti, 1999) and the basis of matching with contracts (Hatfield and Milgrom, 2005).
This mission is the second of a seven-mission series on the paper: 1, the salary-adjustment process; 2, existence of a strict core with continuous salaries (this mission); 3, one-sided coalition formation; 4, the firm-optimal allocation; 5, comparative statics; 6, gross substitutes versus nonincreasing returns; 7, a market with no core. Each mission is self-contained. Nothing of this paper was on Prove2Me before this series.
There is a finite set of workers and a nonempty finite set of firms. Worker 's utility of working for firm at salary is , strictly increasing and continuous in . Firm 's gross product when it hires the set is , and its profit at the salary vector is
The reservation salary is defined by , worker 's utility of unemployment. Section 2 of the paper assumes, for every firm :
An allocation assigns each worker to a firm at salary ; firm hires . It is individually rational (D1) if and for all . A firm , a set and salaries improve upon it if for and , with at least one inequality strict; they strictly improve upon it if all are strict. A strict core allocation (D2) is an individually rational allocation no coalition improves upon; a core allocation (D3) is one no coalition strictly improves upon. In the continuous market coalitions may use any real salaries; in the discrete market of unit all salaries lie on the grids .
Under regular utilities, (MP), (NFL), the reservation-salary relation and (GS) on all real salary vectors,
The goal fixes no grid, no constant and no particular technology.
Theorem 2 gives existence of a stable assignment of workers to firms with salaries, for arbitrary technologies under which workers are gross substitutes, without any convexity or divisibility of labour. Because the core and the competitive equilibrium coincide in this model when salaries are divisible (p. 1487), it is also an existence theorem for competitive equilibrium in a market with indivisible workers; the example of mission 7 shows that it fails without (GS). The Shapley–Shubik assignment game is the special case , with at most one worker per firm.
The result has been proved since 1982; it has not been machine-checked. Prove2Me holds a formalization of the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core-existence theorem is a different model and is not yet proved, and Murota's gross-substitutes axioms for demand on , which concern one price per good rather than firm-specific salary vectors over sets of workers. Neither supplies this market or Theorem 2.
Discrete core allocations exist at every unit , so the natural first idea is to take a sequence of them as and pass to a limit. A limit of discrete core allocations need only be a core allocation of the continuous market in the weak sense D3, and a coalition that improves upon the limit may need salaries off every grid; nothing in the discrete statements controls how much a coalition gains, so the blocking coalitions of the continuous market may vanish on the grids. The required control has to be uniform over all individually rational allocations, which form an infinite set, while each blocking comparison involves the utilities of several workers and a nonadditive technology. A second obstacle is in the paper's notation: the gain (8) uses the salary with , which need not exist when is bounded.
Workers and firms are arbitrary finite types; every theorem assumes at least one firm (the paper's ), since with no firm and some worker no allocation exists. Salaries, utilities, outputs and profits are real numbers. An allocation has no unemployment, as in D1. The reservation salaries are data, and the paper's definition of enters as the hypothesis ; it is assumed on the goal and on milestones 2 and 3, where the discretization step needs every improving salary to be at least . Milestone 1 assumes neither this relation nor continuous (GS). The standing assumptions of p. 1486, which Theorem 2's sentence does not repeat, are hypotheses of the goal.
Explicit readings of the paper's phrases: "continuous market" means coalitions may use any real salary; "bounded above zero" is one valid for every individually rational allocation, stated without by quantifying over admissible coalition salaries; "the unit of measurement smaller than " is with and the division in ; the discrete market's salaries are , , the paper's integer salaries starting at (R1, R4) with a general unit.
Trivializing formalizations are ruled out: the goal assumes (GS) on all real vectors rather than on one grid (a stronger theorem the paper does not prove), its conclusion is the strict core D2 rather than the weaker core D3, and its hypotheses are satisfiable (a one-worker, one-firm market satisfies all of them).
A complete development needs finite optimization over sets of workers, a compactness argument over the individually rational salary schedules of each assignment, and the existence of discrete core allocations (the existence form of Theorem 1, mission 1). Proofs of the milestones, of the equivalence of D2 and D3 in the continuous market, and lemmas on finite demand correspondences reusable across the series are welcome.
A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate .
That analysis assumes that the manager knows an upper bound on the newsvendor quantity, and the algorithm projects onto . This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).
Periods are . Demands are i.i.d. copies of a nonnegative random variable with finite mean and distribution function . Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost per unit left over and shortage cost per unit of unmet demand, the expected one-period cost at level is
The newsvendor quantity is , the minimizer of .
Write and . After period , the manager observes whether demand fell short of the stock level and forms the signal
Fix . The modified AIM algorithm starts from a level and updates
Neither the step size nor the projection interval uses any bound on . The level depends only on , and only through the censored observations.
For every and every ,
The bound holds uniformly over all demand laws with finite mean. The price of not knowing is the slower rate and a transient term in which enters polynomially.
The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are , and the tuning parameter . The explicit constant separates two effects. A transient cost grows with and vanishes like . A steady-state rate approaches the known-bound rate as , at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.
Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.
The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain , so the distance to can grow from step to step. Once the interval contains , the diameter that controls the telescoping sum grows with . The step sizes and the growing radii must be traded against each other through Abel summation. The bound on needs the conditional-expectation argument that is an unbiased subgradient of at a random point independent of . Applying the known-bound theorem with replaced by does not work, because the algorithm is not given and the projection radius changes at every step.
CappedBaseStock.DemandLaw (a probability law on with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's is coordinate . The positive-mean field is not needed by Theorem 7. It excludes only almost surely.backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.A machine whose condition is described by one real number — the temperature of a furnace, the setting of a cutting knife — must process jobs in some order. Job must be started in state and leaves the machine in state ; moving the state between jobs costs money. Ordering the jobs so that the machine returns to its starting job after the last one is a traveling salesman problem whose distance matrix has a special structure. P. C. Gilmore and R. E. Gomory showed in 1964 (Oper. Res. 12(5), 655–679) that this special traveling salesman problem can be solved exactly with operations, one of the first nontrivial polynomially solvable cases of the problem.
The same paper also treats a second objective: instead of the total changeover cost, minimize the largest single changeover cost of the cycle. This is the bottleneck traveling salesman problem, relevant whenever the binding constraint is the worst transition (a maximal temperature swing, a longest retooling) rather than the total. Without the tour constraint it is the bottleneck assignment problem solved by O. Gross (RAND, 1959). Gilmore and Gomory solve the bottleneck tour problem for the cost matrix of their model when only increases of the state cost anything. This mission formalizes that solution.
Timeline: Gross (1959) solves the bottleneck assignment problem; Gilmore and Gomory (1964) solve the sum and bottleneck traveling salesman problems for one state-variable costs; Gilmore, Lawler and Shmoys survey the well-solved special cases of the traveling salesman problem in The Traveling Salesman Problem (Wiley, 1985), where this case is a standard entry.
There are jobs. Job has a starting state and a final state , and the jobs are numbered so that . Given two cost densities , the cost of having job follow job is
A permutation of the jobs means "job follows job ". It is a tour if for every nonempty proper subset of the jobs, i.e. if is a single cycle. The bottleneck cost of is
The bottleneck case of the paper is and : lowering the state is free, raising it costs .
A permutation ranks the 's if implies . An interchange is the transposition of and ; means "first apply , then ". The graph has the jobs as nodes and an undirected arc for each ; is the arc joining consecutive nodes and . A spanning tree of is a set of arcs such that is connected and no proper subset of connects . In the bottleneck case the arc is given the cost , and a minimum spanning tree minimizes the sum of these costs. If its arcs are with , the paper's candidate tour is
For sorted, locally integrable, , ranking the 's and a minimum spanning tree as above,
The goal fixes no numerical constant. It asserts both that the construction produces a tour and that the tour is optimal, so it is a statement about the paper's algorithm, not only about the optimal value.
The result gives an exact solution of a bottleneck traveling salesman problem by one minimum spanning tree computation and a fixed sequence of transpositions. Since general bottleneck traveling salesman problems are NP-hard, cases with an exact algorithm are the reference points against which heuristics and approximation results are compared. Theorem 6, an application, characterizes Hamiltonicity for directed graphs whose out-neighbourhoods form a chain, a class on which the general Hamiltonian circuit problem becomes a connectivity test.
The result is proved in the paper; the mission formalizes the proof. To our knowledge none of it has a machine-checked proof. The formalization adds two things to the paper. First, the statements are made explicit: the order in which interchanges are applied, the reading of "spanning tree", the integrability of . Second, Theorem 6 as printed is false (see below), and the mission states and asks for a proof of the corrected version. Machine-checked statements of and Lemmas 7–8 are also the shared core of the companion mission on the minimal sum tour.
The obvious argument — every tour must "cross" each gap between consecutive components of , so it pays at least the cheapest crossing — fails because the cost of a crossing is not intrinsic to the gap: a tour may cross between components using arcs that are not of the form , and looks at one arc at a time, not at a sum. The connection between an arbitrary tour and the spanning trees of goes through the auxiliary graph and a counting argument (Lemma 8), and the sum-minimizing tree must be shown to be bottleneck-optimal as well. For the upper bound, the transpositions in cascade along runs of consecutive tree arcs, so need not be or ; only the maximum has that form, and showing it needs the monotonicity of in and , which holds because and .
Jobs are Fin (n + 1) (0-based; the paper's job is index ). with Monotone B. The cost keeps the general two-density form (1); the bottleneck hypotheses are everywhere, identically , and locally integrable, so that every interval integral is genuine. Permutations are Equiv.Perm, and is ψ * Equiv.swap i j. is a Finset.sup' over all jobs, including those that leaves unchanged. The arc is indexed by q : Fin n.
Explicit readings of the paper's phrases:
Not formalized: the remark that the results hold for , ; the remark that when ; the operation count.
Trivializing formalizations are ruled out: with a Bochner integral and no integrability hypothesis every cost could collapse to and every claim would hold; dropping the tour conjunct of the goal would let itself be "optimal"; and a maximum that ignored the unchanged arcs would make the goal false.
The traveling salesman items already on the platform (metric and symmetric models with tours as visiting orders, e.g. MetricTSP, TSPHeuristics.Shared.TSPModel) describe a different model and are not used. A complete development needs permutation cycle structure (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, and interval integrals of nonnegative functions; the lemmas on and Lemma 8 are reusable for the sum objective. Proofs of any milestone are welcome independently.
The contact process is the basic model of an infection spreading on a graph: infected sites recover at a constant rate, and healthy sites are infected at a rate that depends on how many of their neighbours are infected. T. E. Harris introduced it in Contact Interactions on a Lattice (Ann. Probab. 2, 1974, doi:10.1214/aop/1176996493), and it became one of the central examples of the theory of interacting particle systems (Liggett, Interacting Particle Systems, 1985, Ch. VI; Liggett, Stochastic Interacting Systems, 1999, Part I). Its questions are those of epidemiology and population dynamics on a spatial grid: does a finite infection die out, and how large does it get on the way?
Harris's paper gives the first rigorous subcritical bounds. Section 7 treats two quantities for a process started from a finite set: the probability of surviving forever, and the expected size at time . This mission formalizes the second, Theorem 7.6: under an explicit condition on the rates, the expected size is integrable in time. The companion mission (Contact Interactions on a Lattice I) formalizes Theorem 7.1, extinction under the same condition.
A short timeline. Harris (1974) defined the process, proved monotonicity, subadditivity and submodularity by coupling, and gave the bounds of §7 and a survival result for large rates (§9). Holley and Liggett (Ann. Probab. 3, 1975) developed duality for such systems. Holley and Liggett's paper also proves, for a discrete-time branching process with interference, the analogue of the size bounds studied here; it is a different process, related but not reused.
Fix and the lattice of integer points . Sites are neighbours, , if ; is the set of the neighbours of . A configuration is a finite set (the set ); is its number of points, is the number of neighbours of in , and means and has a neighbour in .
The parameters are a death rate and birth rates . The contact process is the continuous-time Markov chain on finite configurations that, from , removes a point at rate and adds a site at rate . Its total jump rate is
The empty configuration is absorbing. is its transition function, the transition matrix of its jump chain, and
the expected size at time . In the Lean development these are trans μ lam t ξ η, jump μ lam ξ η and meanSize μ lam t ξ, where lam k is .
If and
then for every finite ,
In the paper's proof order:
After the goal come two consequences: Lemma 4.11, , and Remark 7.12, .
The theorem says that the total expected infection time, summed over all sites, is finite. That is stronger than extinction (Theorem 7.1), and it quantifies how fast the process dies out on average. With Lemma 4.11 it gives . Bounds on the expected size are the standard route to subcritical estimates for spatial epidemics and branching systems with interference. The milestones are also the paper's general tools. Monotonicity, subadditivity and submodularity of , comparison of rate sequences, and time scaling hold for every contact process and are reusable beyond this mission.
The theorem has been known since 1974, and the formalization of the contact process is new work: the platform has no machine-checked development of an interacting particle system on , nor of a continuous-time chain with unbounded rates. The mission produces a formal model of the contact process from a finite set, a Lean proof of the subcritical bound, and the coupling inequalities (stated here for ) that any further work on the process will need.
The obvious argument fails. One would bound the growth rate of by its worst case: a site is born at rate at most for each of at most boundary sites. This gives only Lemma 4.7, an exponential bound whose exponent is positive in most of the regime of the theorem. The factor instead of comes from correlations: a newly born site always has an occupied neighbour, so it adds at most new boundary sites. Capturing this needs the comparison between a single site and a pair of neighbours in (7.7)–(7.11), together with submodularity, which is a coupling statement about the whole process. Lemma 7.5 then has to turn a bound on the difference into a bound on , and the paper omits its proof.
In the formal setting the chain has unbounded rates (since grows with ), so its transition function is not a matrix exponential. Uniformization does not apply either, and every statement goes through the minimal solution of the backward equations.
Fin d → ℤ with the adjacency of the paper.Several trivializing formalizations are excluded:
tsum, which would be when the series diverges;A complete development needs the backward equation and non-explosion for (Theorem 4.3, formalized in the companion mission), Fubini–Tonelli for and in , and couplings of contact processes. The couplings are the paper's auxiliary multi-type processes (§§5–6), or an equivalent argument on the generator. Contributions are welcome at every level. The coupling lemmas and the backward and forward equations for minimal chains are the parts most reusable beyond this mission.
Nonlinear conjugate gradient methods minimize a smooth function of variables using only function values, gradients and a few vectors of storage. They are the standard choice when is too large for quasi-Newton matrices, and they remain building blocks of large-scale solvers in optimization, scientific computing and machine learning. The method of Polak and Ribière (1969) is usually the most efficient member of the family in practice, but Powell (1984, doi:10.1007/BFb0099521) showed that, even with exact line searches, it can cycle forever without approaching a stationary point. The Fletcher–Reeves method, by contrast, has a global convergence theory (Zoutendijk 1970; Al-Baali 1985, doi:10.1093/imanum/5.1.121) but is often slow.
Powell (1985, report DAMTP 1985/NA1; published in SIAM Review 1986) suggested truncating the Polak–Ribière scalar at zero. Gilbert and Nocedal, in the INRIA research report that became SIAM J. Optim. 2 (1992) 21–42, proved that this truncation, and a whole class of methods sharing a structural property with Polak–Ribière, converge globally with practical inexact line searches. This mission formalizes that result (§4 of the report).
Timeline. 1952: Hestenes and Stiefel, linear conjugate gradients. 1964: Fletcher and Reeves, nonlinear extension. 1969: Polak–Ribière and Polyak. 1970: Zoutendijk, convergence of Fletcher–Reeves with exact searches. 1984: Powell, a nonconvergent Polak–Ribière example. 1985: Al-Baali, Fletcher–Reeves with strong Wolfe searches. 1990/1992: Gilbert and Nocedal, the present results.
Let be a finite-dimensional real inner product space and continuously differentiable with gradient . From , a conjugate gradient run produces directions and iterates
with , a scalar , and a steplength chosen by a line search. Write .
Assumptions 2.1: the level set is bounded, and on an open neighbourhood of the gradient is Lipschitz: .
The line search is described only through three properties:
Property (*): whenever for all , there are and with
Finally and .
If Assumptions 2.1 hold, for all , , the line search has properties 1–3, and Property (*) holds, then
Theorem 4.3 separates what a convergence proof needs from the method (nonnegativity and Property (*) of ) from what it needs from the line search (three abstract properties). It therefore applies at once to the truncated Polak–Ribière and Hestenes–Stiefel methods, to their absolute-value variants, and to any line search, exact or inexact, that delivers the three properties. Corollary 4.4 is the guarantee behind the "PR+" rule that is the default in many nonlinear conjugate gradient codes; Powell's example shows that dropping breaks it.
The results are proved in the paper, not open. To our knowledge none of them, nor Zoutendijk's theorem in this form, has a machine-checked proof. The mission produces checked statements of the theorem, its two lemmas and its main application, and a reusable formal vocabulary for line-search methods (level sets, Wolfe steps, Zoutendijk and sufficient descent conditions).
The usual route to convergence of a descent method bounds away from zero, or shows that grows at most linearly, and combines this with the Zoutendijk condition. For Polak–Ribière-type methods neither bound is available a priori: can be as large as on many consecutive iterations, so can grow geometrically along stretches of the run. The argument must instead control the proportion of large steps over blocks of iterations and relate it to the change of direction, and reconcile both with the boundedness of . The combinatorics of blocks (floor and ceiling of , products of grouped by blocks) and the interplay between Lemma 4.1 and Lemma 4.2 carry most of the formal work. Corollary 4.4 additionally needs Zoutendijk's theorem for Wolfe line searches, which is not assumed here.
gradient f for its inner product, matching "the scalar product used to compute the gradient" (p. 2).Needed infrastructure: summability arguments for the series (4.5) and , Cauchy–Schwarz in , finite counting over index blocks, and, for Corollary 4.4, Zoutendijk's theorem (Theorem 2.1 of the report, a target of the companion mission). Contributions of general line-search lemmas are welcome and reusable well beyond this paper.
The single-machine sequencing problem with precedence constraints, written , asks for an order of jobs on one machine that respects a given acyclic digraph of precedences and minimizes the weighted sum of completion times. It is NP-hard in general (Lawler 1978; Lenstra and Rinnooy Kan 1978), and much of its structural theory goes through a decomposition due to Sidney (Sidney 1975): find an initial set of jobs of maximum weight-to-processing-time ratio, schedule it first, and recurse on the rest. Sidney's decomposition underlies the series-parallel algorithm of the same report, the 2-approximation algorithms for the general problem, and the vertex-cover view of Chudak–Hochbaum, Correa–Schulz and Ambühl–Mastrolilli.
The decomposition is only usable if a ratio-maximal initial set can be found efficiently. Section 7 of E. L. Lawler's report Sequencing jobs to minimize total weighted completion time subject to precedence constraints (IRIA-LABORIA Rapport de Recherche No. 205, December 1976; journal version in Annals of Discrete Mathematics 2, 1978) gives the polynomial algorithm: a binary search on the ratio, where each trial value is tested by one minimum-cut computation in an auxiliary network. This mission formalizes the correctness of that procedure.
Timeline.
A finite set of jobs carries an acyclic digraph ; job must precede job when has a directed path from to . Job has an integer processing time and an integer weight of either sign.
An initial set of is a set that contains, with each of its jobs, every predecessor of that job. The ratio of a nonempty set is
and a nonempty initial set is ρ-maximal if for every nonempty initial set . Its ratio is the optimal ratio.
For a trial value , the trial weights are . A maximum-weight initial set for is computed in the network : add a source and a sink , give the arc capacity , the arc capacity , and every arc of capacity . An cutset is a partition of the nodes with , , of capacity .
The integer data satisfy and , and .
If , then every nonempty initial set of maximum trial weight,
is ρ-maximal. This is the paper's sentence "At this point the smallest value in the interval is chosen for a trial value ρ. … In either case, the maximum weight initial set I which is determined is ρ-maximal" (pp. 16–17).
The goal is what makes Sidney's decomposition algorithmic: a ρ-maximal initial set can be found by a polynomial number of minimum-cut computations, with the bound on the number of trial values. Ratio-maximal initial sets are the first step of every Sidney-decomposition-based algorithm for , and the cut network is the standard reduction of maximum-weight closure to minimum cut, used across open-pit mining, project selection and parametric optimization.
The results are classical and proved in the report. No machine-checked version of the closure–cut correspondence, the ratio-separation bound, or the binary-search correctness is known to exist in Lean or on Prove2Me. The mission produces a reusable formal account of initial sets, the network with infinite capacities, and the parametric test of a ratio.
Each step is short on paper; the difficulty is in the corners the paper does not discuss. The paper's "maximum weight initial set" ranges over all initial sets, and the empty set has weight . At the empty set is a maximizer and is not ρ-maximal, so the final step needs a nonempty maximizer; and Case 2, read literally over all initial sets, can never occur. The argument at the left end of the interval also needs the separation bound in the right direction: the printed display ends with "", while the argument needs "". Finally, initial sets are closed under predecessors along paths, while a cut only sees single arcs, so the correspondence between finite cuts and initial sets needs the arcs of to stay inside .
Jobs are a Finset N in a type ι; the precedence digraph is a relation G with every arc inside N and no directed cycle, and "must precede" is Relation.TransGen G. Weights and processing times are real in the general statements and integers cast to reals in the integer-data statements. Lean evaluates as ; ρ-maximality and every statement about attainable ratios therefore range over nonempty sets. Capacities take values in WithTop ℝ, with ; a pair of nodes that is not an arc of has capacity , and an infinite cut has capacity . A cutset is given by its sink side .
Added hypotheses and corrected slips, all disclosed in the items:
A trivializing formalization is ruled out: the goal assumes neither Case 1 nor Case 3, nor the separation bound, nor anything about cuts; those appear only as milestones. The running-time statements of §7 and the binary search loop itself are out of scope.
A complete development needs finite sums over finsets, path closure of initial sets, and extended-real arithmetic in WithTop ℝ. The cut network with infinite capacities and the closure correspondence are reusable for any maximum-weight closure problem. Proofs of the milestones, and of the goal from Cases 1 and 3 with the separation bound, are welcome.
A flexible manufacturing system processes several part types on shared machines, and a machine that switches from one part type to another pays a set-up time. Real-time, distributed scheduling rules for such systems decide locally, at each machine, when to switch and to which buffer. The simplest such rules are clearing policies: a machine keeps working on its current buffer until that buffer is empty, then switches. Perkins and Kumar (IEEE TAC 34, 1989; reference [18] of Kumar–Seidman 1990) showed that every clear-a-fraction (CAF) policy, a clearing policy that always switches to a buffer holding at least a fixed fraction of the machine's work, keeps all buffers bounded in every acyclic system whenever each machine's load is below one.
Kumar and Seidman (IEEE TAC 1990) showed that acyclicity cannot simply be dropped. In §III of the paper, a two-machine re-entrant line and a two-part-type system, both with every machine loaded below capacity, have clearing trajectories whose buffer levels grow without bound. This mission formalizes the paper's positive result for non-acyclic systems: Theorem 1, a stronger capacity condition under which every CAF policy is stable from every initial state.
There are part types and machines. Part type enters at rate and visits the machines in turn; revisits are allowed. At its -th stage a part waits in buffer and needs processing time . Machine serves , and switching from to costs . Flows are fluid. The level satisfies , where is the cumulative output and the cumulative input: for the first buffer of a route, the output of the previous buffer otherwise. Each machine works through runs. A run is a set-up for a buffer, during which nothing is processed, followed by processing of that buffer at rate at most , and at exactly that rate while the buffer is nonempty.
A trajectory is clearing (Definition 1) if each machine leaves its buffer exactly at the first time the buffer is empty while another of its buffers is nonempty, and then sets up for such a buffer. It is CAF with constants , (Definition 2) if every set-up commenced at time is for a buffer with
A trajectory is stable if for every buffer.
The graph on machines has an arc when and some part type visits right after . Machines are diconnected, , when each is reachable from the other. For each buffer, is the last earlier stage at a different machine, if any, and is that stage's machine, the prior machine. The modified input rate is if , and otherwise (11)–(13).
If
then for all , all , every CAF trajectory from every initial state is stable. The bound on each buffer may depend on the trajectory.
For a machine in a minimal class, is the work at (15), and are consecutive set-up commencements:
The result. Theorem 1 is a sufficient condition for stability that holds for every system topology and every CAF policy, with no restriction to acyclic flows. It separates two kinds of upstream supply. A machine that is not in a common cycle with its supplier needs capacity only for the average rate . A machine that is in such a cycle must budget for the supplier's peak rate. The paper's examples show that some strengthening of is needed for clearing policies on cyclic systems: they are unstable under alone. Section V of the paper builds on this gap, with a supervisory mechanism that restores stability under alone.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. A formalization must turn a two-page argument with a set-up/processing run structure, a starvation case analysis and an induction over the condensation of a directed graph into rigorous statements. The result is a reusable fluid model of scheduling with set-up times. It also makes explicit the conventions of the clearing rule, which the paper leaves informal.
A natural first attempt bounds the total work at each machine separately, using only the average arrival rates. This fails on cyclic systems. A machine downstream in a cycle can receive parts in bursts at the upstream machine's full processing rate , far above ; Example 1 of the paper builds exactly such a positive feedback. The proof therefore has to (a) bound the inflow into a machine of a minimal class by the peak rates in (14); (b) handle starvation inside a run, where the machine works below its maximal rate; (c) control the set-up overhead, which the CAF rule amortizes by forcing long runs once is large; and (d) push boundedness down the partial order of classes, where the bounded upstream buffers enter as an additive constant . Step (d) needs a bound on the total content upstream, not one per buffer.
System P M holds the data. Part types, machines and stages are 0-based (paper stage is Lean stage ). Trajectory S holds levels, cumulative outputs and runs, with N m : ℕ∞ runs per machine. Time is real, with explicit . Run starts are nondecreasing and, if infinitely many, tend to infinity. Machines never idle outside runs: idling on an empty buffer is processing at the inflow rate.Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far apart the two quantities can be. Leighton and Rao (J. ACM 46 (1999), extending their FOCS 1988 paper) proved that for uniform demands the gap is at most logarithmic in the number of nodes, and turned the proof into approximation algorithms for a range of NP-hard cut problems.
Their §2.4 extends the result to directed networks, where every edge carries flow in one direction only. The directed version is the one behind their approximation algorithms for directed problems, most prominently the minimum feedback arc set problem (§3 of the paper), where the cut structure of a digraph, not of its underlying undirected graph, is what matters.
Timeline. Ford and Fulkerson (1956): max-flow = min-cut for one commodity. Hu (1963): equality for two commodities in undirected graphs. Shahrokhi and Matula (1990, circulated 1986): the uniform concurrent flow problem and its LP dual. Leighton and Rao (FOCS 1988; J. ACM 1999): for uniform and product demands, undirected and directed, tight up to the constant for undirected uniform problems. Klein, Rao, Agrawal and Ravi (1990s) and Linial, London and Rabinovich (1995) extended the undirected theorem to general demands with an gap. For directed graphs with general demands the gap is polynomial in (Chuzhoy and Khanna 2009), so the uniform-demand directed theorem is the setting where a logarithmic gap holds.
A directed network is a finite vertex set with nodes and a capacity for each ordered pair, with ; there is an edge directed from to when . For write and let be the capacity of the edges directed from to .
The directed uniform multicommodity flow problem (directed UMFP) has one commodity for every ordered pair with , each with demand . A concurrent flow of value routes units of every commodity simultaneously, each edge carrying flow only in its own direction, with total flow on the edge at most . The max-flow is the largest such .
The ratio cost of a cut is , and the min-cut is
A distance function assigns a length to each directed edge; then also denotes the length of a shortest directed path from to , its total weight is , and the distance constraint is . The sets and are the nodes from which can be reached, respectively which can be reached from , by a directed path of length at most . Logarithms are to base .
In Lean these are DiNetwork, diCutCap, diRatio, diMinCut, diDemand, IsDiConcurrentFlow, diMaxFlow, diDist, diTotalWeight, SatisfiesDiConstraint, inBall and outBall, in the namespace LeightonRao.Directed.
There is an absolute constant such that every directed UMFP on nodes satisfies
The constant is left unfixed, as in the paper's ; any improvement of the constant leaves the goal intact.
The result. Theorem 12 says that the directed sparsest cut and the directed uniform concurrent flow agree within an factor. Since the flow is an LP, this gives an -approximation for the directed uniform sparsest cut, and through divide and conquer, polylogarithmic approximations for directed problems such as minimum feedback arc set and minimum directed cut linear arrangement (§3 of the paper). It is also the case in which a logarithmic flow–cut gap survives for digraphs: with arbitrary demands, the directed gap is polynomial.
Formalizing it. The theorem has been proved since 1988, but no part of it is formalized: Mathlib has no multicommodity flows, no directed path metrics over real lengths, and no region-growing arguments. This mission produces the directed concurrent-flow model, its LP duality, and the directed region-growing decomposition of Lemma 13, each reusable beyond this paper (directed multicut, feedback arc set, low-diameter decompositions of digraphs).
The obvious route copies the undirected proof: grow a ball around a node until the capacity on its boundary is small compared with the capacity inside, cut it off, and repeat. In a digraph this fails at two places. A ball of small out-radius can have large in-radius, so a piece cut off by out-distances is not small in the sense needed later; and cutting off a piece only controls the edges leaving it in one direction, so edges pointing back into earlier pieces are not paid for. Lemma 13 has to bound the capacity of all backward edges of an ordered partition while keeping each part inside both an in-ball and an out-ball around one of its own nodes. The final averaging step also changes: the undirected argument sums over symmetric pairs, which has no directed counterpart, so the distance constraint over ordered pairs has to be split between distances into one set and out of another.
Vertices form a Fintype with decidable equality, and every goal-level statement assumes . Commodities are ordered pairs with demand ; a flow is in arc form, with conservation, and the capacity constraint is per directed edge. The max-flow is the supremum (sSup) of the achievable values ; the min-cut is an infimum over nonempty proper subsets, since the ratio is otherwise. Shortest-path distances are infima over directed walks (lists of vertices along edges of positive capacity); for nonnegative lengths these equal shortest-path lengths. An unreachable pair would get Lean's junk value , so every statement using assumes strong connectivity ( for every proper ), the directed analogue of the paper's standing assumption on p. 789; the balls are defined through the existence of a walk and need no such assumption. counts each directed edge once, and the distance constraint sums over ordered pairs. "We can find" is read as existence; running times are not formalized. The of Theorem 12 is one absolute constant chosen before the network; the explicit constants , and of the milestones are the ones computed in the paper's proofs.
Two printed slips are corrected and disclosed: Lemma 13 (1) prints where the proof uses , and the proof's last line prints where the statement has .
The statement cannot be trivialized by a degenerate cut or flow: cuts range over nonempty proper subsets, the flow's capacity constraint is directional, and the goal's constant is quantified before the network, so a constant depending on does not count.
Needed infrastructure: LP duality for the concurrent flow LP (or a direct proof of the max-flow/distance duality), shortest directed paths with real lengths, and the region-growing bookkeeping. Contributions to any milestone are welcome, as are alternative proofs of Lemma 13 by continuous region growing.
An infinite dimensional variational problem can be described by continuous linear operators and convex functionals, yet numerical work needs finite dimensional spaces. The question is whether a solution computed in a finite dimensional approximation still approaches the solution of the original problem when the approximation is refined. Gabay and Mercier's IRIA report studies this question alongside a dual algorithm. Its Section 4 gives a convergence statement for internal approximations of the primal problem. The result is relevant to finite element methods because it identifies conditions on the discrete spaces, discrete operators, and nonsmooth part of the objective that ensure convergence of the minimizers.
The report is the June 1975 preprint of a 1976 journal paper. This mission follows the pinned report version, hal-04716124v1, whose theorem and equation numbers are used throughout. Its Section 4 first states the abstract approximation theorem and then turns to a concrete finite element construction. The abstract theorem is the target here. Gabay and Mercier, pp. 20–23.
Let and be real Hilbert spaces, and let be a continuous linear operator. A continuous linear functional supplies a linear term. Let be a proper, convex, lower semicontinuous function. Its value may be , which excludes an inadmissible point. The continuous problem is to minimize
A solution has finite objective value and minimizes over all of . The report's coercivity condition (2.5) supplies such that for every . It also assumes the interior of the effective domain of is nonempty. The proof of Proposition 2.1 explicitly requires a point with ; this feasibility condition is made explicit here. Gabay and Mercier, pp. 8–9.
For each approximation index , let be a finite dimensional subspace and a continuous linear operator. The discrete problem minimizes over . The same appears in both terms involving the image of . The report also describes a subspace containing the range of ; the abstract convergence claim uses those images only as elements of . Gabay and Mercier, pp. 20, 23.
The operator assumptions (4.1) include uniform constants and with , preservation of weak and strong limits, and for uniformly bounded families. The compatibility condition (4.3) requires, for each , points with and . The latter limit is extended valued when necessary. These conditions define what counts as an internal approximation for this theorem. Gabay and Mercier, p. 20.
The main target is Theorem 4.1. The continuous problem has a unique solution ; the discrete problems have unique solutions for all sufficiently fine approximations; and
The theorem's phrase “in strongly” is read in the common ambient space , because the spaces vary. The claim covers every selection of discrete minimizers once they exist. The paper's conditions allow a few early discrete problems to be infeasible, so existence is asserted eventually. Gabay and Mercier, p. 21, Theorem 4.1.
The milestone list follows the report's own path from the application of Proposition 2.1 on p. 20 through the variational inequality (4.4), the bound after (4.5), weak convergence after (4.7), the estimate (4.8), and the limits (4.10)–(4.11). The equations (4.5) and (4.8) contain printing slips; their milestone excerpts preserve the printed text, while their formal statements use the mathematically consistent readings explained with each item. Gabay and Mercier, pp. 21–22.
The theorem gives a precise guarantee for a family of finite dimensional problems: a computed minimizer is meaningful as an approximation to the unique solution of the infinite dimensional problem when the discretization satisfies the stated conditions. The operator may differ from the restriction of to , and the nonsmooth term may assign outside its domain. The conclusion therefore covers settings in which simply restricting the continuous objective to a subspace would describe the wrong numerical problem. Gabay and Mercier, pp. 20–23.
The result is proved in the report; the remaining task is a machine checked proof of the abstract approximation theorem and its cited intermediate claims. A formal development would also leave reusable statements about extended valued convex minimization, weak convergence of Hilbert space sequences, and uniformly consistent discrete operators. This proposal supplies statements for those claims; it does not claim that they already have machine checked proofs.
Strong convergence cannot be read off from a bound on the discrete solution norms. Uniform boundedness yields only access to weak limits in the Hilbert space; the solution's images and the nonsmooth objective must still behave correctly under the varying operators. Weak convergence of alone also does not imply convergence in norm. A proof must keep the weak limit, the lower semicontinuity of , and the discrepancy between and aligned under the same approximation assumptions. The fact that may be infinite makes unguarded subtraction of its values invalid. Gabay and Mercier, pp. 21–22.
Lean uses real complete inner product spaces for and , continuous linear maps for and , and StrongDual ℝ V for . The index represents a sequence of mesh parameters ; the report's convergence claims are sequential. Each is finite dimensional. The codomain spaces are suppressed through their inclusions in . Weak convergence uses all Hilbert inner products as tests, while “strongly” means convergence in the norm topology.
The function takes values in EReal, with properness excluding . Its limit in (4.3) uses the extended real topology. The quadratic term is real valued. A solution must have a finite objective value, and the continuous problem must have a feasible point. The section's interior-domain assumption (2.4) is retained even though the abstract proof does not use it. Condition (4.1)(iv) quantifies over every uniformly bounded family. These choices rule out the vacuous interpretation in which all continuous or discrete objective values are .
The report's automatically satisfies the earlier gradient monotonicity requirement (2.3). The published InertialFB.IFB.ConvexAnalysis definition provides properness, convexity, and weak convergence with matching conventions. The new local definition supplies the two objectives, solution predicates, and approximation hypotheses. Contributions proving the goal and its milestones are welcome; separate treatments of the concrete triangulation and quadrature construction of Proposition 4.1 are outside this mission. Gabay and Mercier, pp. 20–26.
For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller than the sparsest cut. Leighton and Rao (J. ACM 1999, building on their FOCS 1988 paper) proved that the gap is at most logarithmic for broad classes of demand patterns, and turned the proof into the first -approximation algorithms for sparsest cut, balanced separators, minimum feedback arc set, crossing number and VLSI layout problems.
This mission formalizes Section 2.3 of the paper: the extension of the uniform max-flow min-cut theorem to product multicommodity flow problems (PMFPs), where the demand between two nodes is the product of their node weights.
Timeline.
A network is a finite vertex set with a symmetric capacity on each pair, zero on the diagonal; is an edge when . For , the cut capacity is . The network is assumed connected: for every nonempty proper .
A PMFP is given by a node weighting . Write for the set of nodes with , , and . As in the paper, the weights are normalized so that . Every pair is a commodity with demand ; there are commodities with nonzero demand. The uniform problem is .
The max-flow is the largest such that units of every commodity can be routed simultaneously, with the total flow on each edge (both directions) at most its capacity. The min-cut is
the quotient being the weighted ratio cost of the cut .
The dual objects are distance functions: lengths on the edges, with total weight ; is the shortest-path distance and . The weighted distance constraint is .
There is an absolute constant such that every normalized PMFP with on a connected network satisfies
The goal leaves the constant unfixed, which is the paper's .
Theorem 7 bounds the multicommodity flow–cut gap by for every product demand pattern, so an optimal dual distance function certifies a cut within of the sparsest weighted cut. The paper itself applies it to reversible Markov chains (§3.27, p. 827). There the node weights are the stationary probabilities, and Theorem 7 shows that the inverse conductance and the resistance of a chain agree up to a factor, where is the number of states with positive stationary probability.
Theorem 7 was proved in 1988–1999 and is subsumed, up to the constant, by the general bound for arbitrary demands (Linial–London–Rabinovich 1995; Aumann–Rabani 1998). It has no machine-checked proof, and neither has any of its milestones. A complete development would also be the first formal treatment on Prove2Me of concurrent multicommodity flow, its LP dual, and region-growing (low-diameter) decompositions, which recur across approximation algorithms and metric embeddings.
The upper bound is a counting argument. The lower bound is the work. Rounding an optimal dual distance function to a cut fails directly: thresholding distances from a single node gives no control on the ratio when the weight is spread out. The paper's argument needs a decomposition of the graph into components of small radius that cuts little capacity, with a loss of only , not : the regions must be grown from weighted nodes only, while the many zero-weight nodes still sit inside the graph and its capacities. It must then separately handle the case where one component carries two thirds of the weight. Formally, the LP duality step alone requires a strong-duality statement for a linear program with one constraint per path, exponentially many, which Mathlib does not provide in this form.
All objects live in the namespace LeightonRao.Product in a single definitions file.
Finpartition.Contributions are welcome at every level:
The Nelder–Mead simplex method (Nelder and Mead, 1965) is one of the most widely used methods for minimizing a function without derivatives. It is the default unconstrained derivative-free minimizer in several numerical libraries (fminsearch in MATLAB, method="Nelder-Mead" in SciPy) and is used routinely in chemistry, engineering and statistics, where the objective is a simulation or a measurement whose gradient is unavailable.
Its theory lags far behind its use. Until 1998 there was no convergence result for the method as stated, in any dimension. Lagarias, Reeds, Wright and Wright (SIAM J. Optim. 9 (1998) 112–147) gave the first: in dimension one, on strictly convex functions with bounded level sets, the method converges to the minimizer whenever the product of its reflection and expansion coefficients is at least one. McKinnon (SIAM J. Optim. 9 (1998) 148–158) showed in the same issue that in dimension two the method can converge to a non-stationary point even for strictly convex smooth functions, so results of this kind cannot be expected in general.
Timeline:
This mission formalizes the one-dimensional convergence theorem.
Let . In dimension one a Nelder–Mead simplex is a pair of distinct points , ordered so that : is the best and the worst vertex. Four coefficients are fixed in advance, reflection , expansion , contraction and shrink , satisfying the conditions (2.1) of the paper:
From the method forms the trial points
With , , and so on, one iteration does the following:
The worst vertex is discarded, and the accepted point becomes the new best vertex if and the new worst vertex otherwise (the paper's tie-breaking rule). The diameter of the simplex is . The function is strictly convex, and it has bounded level sets: is bounded for every . It then has a unique minimizer .
If, in addition to (2.1), , then for every nondegenerate initial simplex
The goal names no rate and no constant; it is the qualitative statement the paper proves.
A further item states the paper's remark that when the vertices stay within of , so convergence to fails when the minimizer is farther away.
Theorem 4.1, together with the remark on , identifies as the right condition for global convergence of the one-dimensional method, and it holds for all contraction coefficients and for infinitely many expansion steps. It is the base case of the low-dimensional theory: the linear-rate result for (Theorem 4.2) builds on the same bracketing and proximity lemmas, and McKinnon's example shows that nothing comparable holds in dimension two.
The result is proved in the paper; no machine-checked proof of any convergence property of the Nelder–Mead method is known to exist. A formalization gives a precise, executable definition of the algorithm with its tie-breaking rules, which the literature states in several inequivalent variants, and it checks a proof with a known gap: the bound on printed in Lemma 4.2 is false (see below), so the published argument cannot be followed line by line.
The obvious argument, that the best value decreases and so the best vertex converges, fails twice. The best vertex may stall while contractions continue, and the diameter can grow, by the factor at every expansion step, so there is no monotone potential. The proof must show that the minimizer is eventually trapped in an interval proportional to the current diameter (Lemmas 4.2, 4.3), and separately that the diameter tends to zero whatever the sequence of moves (Lemmas 4.4, 4.5); the latter needs a case analysis of infinite runs of contractions and of the two limit points of a strictly convex level set.
The Lean development lives in the namespace NelderMeadLD.Conv1D. The simplex is an ordered pair p : ℝ × ℝ with p.1 (best) and p.2 (worst); one iteration step is a function of the pair, and the run is its -fold iterate from the initial pair. Committed conventions:
StrictConvexOn ℝ Set.univ f, bounded level sets are Bornology.IsBounded {x | f x ≤ μ} for every μ, and the minimizer is a binder with ∀ y, f xmin ≤ f y;Tendsto; Lemma 4.4 asserts the existence of a common limit of both value sequences.The printed bound of Lemma 4.2 is false (, , , ) and is not stated; the existence and minimality of and the bracketing are. A formalization that drops nondegeneracy or the ordering of the initial pair, or quantifies over an arbitrary point, is not this theorem: with every iteration is a shrink to the same point and the goal is false.
Needed infrastructure: elementary facts on strictly convex functions of one real variable (three-point bracketing, monotonicity beyond the minimizer, continuity), and bookkeeping for iterates of a piecewise-defined map. Lemma 4.1 is reusable beyond this mission. Contributions are welcome on every milestone, independently: Lemmas 4.4 and 4.5 do not use .
The method of multipliers (augmented Lagrangian method) of Hestenes and Powell is one of the standard algorithms for constrained convex optimization. Each iteration minimizes the Lagrangian plus a quadratic penalty on the constraint residual, then updates the multiplier estimate. Rockafellar showed in 1976 that this method is the proximal point algorithm applied to the dual problem (Rockafellar, Math. Oper. Res. 1976), which explains its global convergence for convex programs without differentiability or constraint qualifications on the primal side.
The quadratic penalty is not the only one used in practice. Exponential and other nonquadratic penalties produce twice-differentiable augmented Lagrangians and were studied by Kort and Bertsekas and by Tseng and Bertsekas. Eckstein (Math. Oper. Res. 18(1), 1993, 202–226) gave a uniform convergence theory for such methods. He replaces the squared Euclidean distance in the proximal point algorithm by the D-function of a Bregman function , proves convergence of the resulting algorithm for every maximal monotone operator (Theorem 1), and then derives nonquadratic multiplier methods by applying it to the dual of a convex program. This mission covers the linear-equality-constrained case, §4.1 and Theorem 6 of that paper.
Let be convex and lower semicontinuous, let be an matrix, , and closed and convex, with . The problem is
Write for the indicator function of ( on , off ) and . The dual functional is
assumed not identically . An optimal multiplier (Lagrange multiplier) is a maximizer of over .
For an open set , a Bregman function with zone is a function that is continuously differentiable on , strictly convex and continuous on , and satisfies the level-set and limit conditions (iv)–(vi) of Definition 1 on its D-function . Here the zone is all of , and is assumed onto . Let be the convex conjugate of , and let with . The nonquadratic method of multipliers generates by
For this is the classical method of multipliers. A run of the general Bregman proximal point algorithm for an operator is a sequence with for all .
Under the assumptions above:
The statement fixes no penalty: it holds for every Bregman function with zone and surjective gradient. It makes no claim that converges, which is false in general.
An additional item states the existence clause of Theorem 6: if the row space of meets , or and are polyhedral and the row space meets , then (9) has an infinite run from every starting point .
Theorem 6 gives global convergence of a whole family of augmented Lagrangian methods at once, with the penalty chosen through . For instance, Example 5 of the paper obtains the method with penalty for any . Its multiplier sequence behaves exactly as the dual proximal point iterates do, and it detects dual unsolvability through divergence of . Primal limit points are optimal without any assumption beyond existence of a Lagrange multiplier.
The result has a published proof (Eckstein 1993) but, to our knowledge, no machine-checked proof. Formalizing it requires a formal treatment of Bregman functions and of the Bregman proximal point algorithm (Theorem 1). It also requires the subdifferential calculus of the dual functional: conjugates, the chain rule , and the inverse relation between and . The milestones isolate the reduction of (9) to Theorem 1 and the primal recovery argument, each of which can be proved independently of the others.
The reduction step is where a direct argument fails. Showing that is a proximal point of needs the inclusion , where is a composition of a conjugate with a linear map. The subdifferential chain rule holds with equality only under a qualification condition. The argument must therefore use only the inclusion that holds unconditionally, together with the optimality condition for the -subproblem, which needs differentiability of everywhere (supplied by and strict convexity of ). On the primal side, need not be bounded or convergent, so primal optimality can only be asserted for limit points, through closedness of the graph of . Theorem 1 itself rests on the Bregman conditions (iv)–(vi), which replace the Fejér monotonicity of the Euclidean proximal point argument.
EuclideanSpace ℝ (Fin k). is a continuous linear map (equivalent to an matrix), and is its adjoint. Theorem 1 is stated on any finite-dimensional real inner product space.EReal-valued with "never " as a hypothesis. uses the published IsSubgradient; convexity is convexity of the epigraph (IsConvexFn). Maximal monotonicity, dom and zer are the published ThreeOpSplitting.Convergence definitions. The conjugate is the published fenchelConjugate, an EReal supremum.intrinsicInterior, and polyhedral sets and functions are finite intersections of closed half-spaces (for functions, of the epigraph).A retailer that sells a line of substitutable products — sizes, colours or models of one item — over a short season without replenishment must decide how to price each variate as inventory runs down. Customers substitute: when one variate is expensive or sold out, part of its demand moves to the others. Dong, Kouvelis and Tian (M&SOM 2009) model this with a multinomial logit (MNL) choice model inside a finite-horizon dynamic program and characterize the optimal prices in closed form up to one scalar equation per period.
Retailers often cannot reprice everything. A common arrangement, described in §5.1.3 of the paper, is mixed pricing: products advertised in a printed catalogue keep their catalogue prices for the season, while products sold only online are repriced dynamically. Proposition 2 of the paper gives the optimal dynamic prices in this setting. It is the third of the paper's three optimal-pricing results, after the full dynamic pricing model (Theorem 1) and unified dynamic pricing with one common price (Proposition 1); each is the subject of its own mission in this series.
There are variates and remaining periods; time counts down. In each period one customer arrives with probability . Variate has a quality index ; the no-purchase option has utility ; is the MNL scale. The inventory is , and the in-stock set is . A sold-out variate leaves the choice set.
The variates are split into a dynamic-pricing set and a fixed-pricing set , where is always sold at its fixed price . Write and . Given dynamic prices (), an arriving customer buys an in-stock variate with probability
and buys nothing with probability (numerator ). The value function is the maximum expected revenue from periods with inventory : and
The marginal value of a unit of variate is . For a fixed-price variate put and ; for the outside option , and .
In Lean the model lives in SubstitutePricing.Mixed.Model: S1, S2, P, P0, objM, piM, deltaM, v, uf, lhs15, rhs15, rstarM.
For every and inventory , the margin equation
has exactly one solution ; the dynamic prices
are allowable and attain the maximum in the optimality equation; and
In the order the paper's proof uses them: the optimality equation rewritten as a price objective plus (29); the no-purchase and fixed-price probabilities as functions of the dynamic ones (30); strict joint concavity of the objective (31) in the dynamic choice probabilities; the form (32)–(34) of an optimal price vector; the equivalence of (15) with (36) and uniqueness of its root; and the one-period recursion .
The result says that, even with part of the line frozen at catalogue prices, the optimal dynamic prices keep the structure of the full model: every repriced variate earns the same margin over its own marginal value, and one scalar equation per period determines that margin. The fixed-price variates enter (15) in exactly the role of the outside option, each weighted by its own net value ; when , (15) reduces to the margin equation (10) of Theorem 1. One difference from the full model is that the identity fails here, so the margin is not tied to the no-purchase probability alone. The structure reduces each period's -dimensional price optimization to a one-dimensional root and supports the paper's comparison of mixed, unified and full dynamic pricing in §5.
The paper gives a complete proof (Appendix A, pp. 337–338). None of it is formalized: Prove2Me and Mathlib have no MNL pricing dynamic program. The mission produces a machine-checked version of the proof, including the step the paper leaves unchecked (below).
The objective is not concave in prices, so a stationary point in price space is not automatically a maximum, and the obvious first-order argument proves nothing by itself. The fixed-price variates make the coupling worse than in the full model: their purchase probabilities move with every dynamic price, and the identity that pins the margin in Theorem 1 is lost.
The second difficulty is a gap. The price set is , and the proof never checks that the prices are nonnegative. In Theorem 1 this follows from and . Here the left side of (15) is negative for , so follows once every ; the paper bounds nowhere. Random search over small instances found no negative optimal price, so the goal is posed as printed. A complete formalization of the goal must close this gap.
Fin n; the dynamic set is a Finset; inventories are Fin n → ℕ; time counts down with defined by recursion on t : ℕ. Results are stated for .sSup over ; coordinates outside are ignored. Fixed prices are assumed nonnegative. The goal asserts feasibility of the prices, attainment of the maximum, and the value identity, so it never rests on the value of sSup at an unattained or unbounded set.A trivializing formalization — relaxing the price set to , stating the value identity without attainment, or adding a hypothesis that bounds from below — would remove the gap rather than prove the theorem, and is ruled out.
The development needs the MNL choice probabilities, the dynamic program, a strict-concavity argument on an open simplex, and a monotonicity-plus-intermediate-value root lemma. The model file is kept identical, up to the mixed-pricing data, to the files of the other two missions in this series so they can be consolidated. Proofs of any milestone, and in particular an argument closing the nonnegativity gap, are welcome.
A partially observable Markov decision process (POMDP) models an agent that acts in a stochastic world whose state it cannot see directly. The agent sees only noisy observations. POMDPs are the standard model for planning under uncertainty in robotics, dialogue systems, medical decision making and machine maintenance. The exact finite-horizon theory goes back to Smallwood and Sondik (1973), who showed that the optimal value function is piecewise linear and convex in the agent's belief, so that it can be represented by a finite set of vectors.
Kaelbling, Littman and Cassandra (1998) brought this theory to artificial intelligence. Their paper introduces policy trees as the objects behind those vectors and presents the witness algorithm, an exact value-iteration method. It is one of the most cited papers on POMDPs. The correctness of the witness algorithm rests on a single statement, Theorem A.1 of the paper's appendix, the witness theorem. This mission formalizes that theorem together with the lemmas its proof uses.
Timeline:
A POMDP is a tuple with finite sets of states, of actions and of observations. Taking action in state leads to state with probability and earns expected reward . The agent then observes with probability . Rewards are discounted by a factor with ; is the plain finite-horizon problem.
A belief state is a probability vector on ; denotes the set of all of them. After action and observation , the belief is updated by Bayes' rule to . The normalizing constant of this update is .
A -step policy tree is a single action when . For it is a root action together with one -step subtree for each observation . Its value is defined by the recursion
and at a belief state it is . The optimal -step value is over all -step trees.
A tree in a finite set is useful if some belief state gives it a strictly larger value than every tree of with a different value function. The useful trees form the parsimonious representation of . Let be the useful -step trees. The candidates are the -step trees with root and all subtrees in , and is the set of trees useful in . The Q-function is
For a set of candidates, is the current approximation. For , an observation and , the tree is with its subtree for replaced by .
For a nonempty ,
Trees with the same value function are identified, as in the paper. The statement is exact, with no constants.
The witness theorem is the stopping and growth criterion of the witness algorithm. If no single-subtree modification of the current trees beats all of them at some belief state, the current set represents the Q-function exactly. Otherwise the belief found is a witness and yields a new useful tree. Because each test is one linear program, the theorem turns an infinite search over belief space into finitely many linear programs. It is also the basis of the paper's complexity claim, polynomial time in , , , and . Incremental pruning and later exact POMDP solvers rely on the same parsimonious-set machinery.
The theorem is proved in the paper; it has not been machine-checked. A formal development would also provide reusable infrastructure: policy trees, their value recursion, belief updates, and the existence and minimality of parsimonious representations of finite sets of linear functions on the simplex. That infrastructure is needed for any formal treatment of exact POMDP value iteration.
Most steps are finite algebra. The part that needs care is the "if" direction of the goal. A belief at which a new tree beats all of shows that the true Q-function exceeds the approximation. It does not directly show that a useful tree is missing, because the maximizing tree at that belief may tie with other trees there. One needs the representation property of the parsimonious set (milestone 3): at every belief, the maximum over all candidates is attained by a useful one. Proving this means moving from a belief where several value functions tie to a nearby belief, inside the simplex, where exactly one of them is strictly largest. The proof on p. 131 also needs the Q-function to be attained on the candidate set, so that the improving subtree lies in (milestones 4 and 5).
POMDP.IsValid.PolicyTree A Ω n is the type of -step trees, so statements about -step trees with subtrees use . The type is finite, and the set of all trees of a given depth is Finset.univ.stdSimplex ℝ S. Every "there is some belief state" ranges over the simplex, not over .Finset.sup' over nonempty finite sets, or IsGreatest.The following encodings would make the theorem trivial or false, and are excluded: comparing trees by equality instead of by value function, letting range over all of , taking to be an arbitrary set, allowing , and defining the true Q-function as itself.
Contributions are welcome at every level. The parsimonious-representation lemma (milestone 3) is the reusable geometric core. The subtree-swap lemma and the Q-function identity are the algebraic core.
The residual life time of a lifetime at age is the excess given survival, . How it behaves at great ages is a question in reliability (remaining life of an item that has already lasted long), in insurance and demography (remaining life at old age), and in the peaks-over-threshold method of extreme value statistics, where exceedances over a high threshold are modelled by a generalized Pareto law.
Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974) 792–804) determined every possible limit law of the suitably normed residual life as , and their domains of attraction. For continuous limits, the classical sufficient conditions are von Mises' conditions (1936) on the derivative of . Section 4 of the paper goes further: it gives inequalities that hold at every finite age , not only in the limit. This mission formalizes that finite- result, the Corollary to Theorem 7.
Timeline: von Mises (1936) gives sufficient conditions for domains of attraction of extreme value laws; Balkema and de Haan (1974) prove the limit theorems for residual life and the finite- bounds formalized here; Pickands (1975, Ann. Statist. 3, 119–131) proves the corresponding approximation by the generalized Pareto law for excesses, the result now known as the Pickands–Balkema–de Haan theorem.
Let be a real random variable with distribution function . The residual life distribution function at age is
Assume has a positive, differentiable density for , and define the norming function
the reciprocal of the hazard rate. The normed residual life is given , with distribution function .
The comparison laws are the distribution functions , , all vanishing for :
If and satisfy for , then
The goal is the Corollary because it is the paper's final statement of Section 4: a single parameter and a single error , with no limit taken. Theorem 7 is the stronger two-parameter sandwich it rests on.
The result. Theorem 7 and its Corollary are a quantitative, non-asymptotic form of the von Mises condition . If the derivative of the reciprocal hazard stays within of from age on, then at every such age the normed excess distribution is uniformly within of the generalized Pareto (or exponential) law . Letting along recovers convergence to , and the bound itself quantifies the error of the generalized Pareto approximation used in threshold-exceedance modelling.
Formalizing it. The result is proved in the paper (1974), with short proofs. To our knowledge no part of it has a machine-checked proof. The mission produces checked versions of the theorem, the corollary and the elementary lemmas about the family : its monotonicity and Lipschitz dependence on the parameter , including across the case change at . Those facts about the generalized Pareto family are reusable in any formal development of extreme value statistics.
The analytic content is elementary, but several steps hide case analysis. The Lipschitz bound in requires the derivative of in across , where the formula changes from to , and across the boundary of the support when , where the function is not differentiable. The bound is not a crude estimate: it reduces to the comparison for the function , which needs its strict monotonicity on all of , including where the closed form is undefined. In Theorem 7 the lower bound in (13) becomes negative for and large ; this is exactly where the comparison law reaches , and the argument must handle it. The orientation is easy to get wrong: the upper bound on the derivative gives the lower bound , since decreases in .
The source is the published Annals of Probability article (DOI 10.1214/aop/1176996548); page numbers are the journal's.
μ on ℝ, is Mathlib's cdf μ, and . The normed probability is .cdf μ has derivative and has derivative , both within ; nothing is assumed to the left of .HasDerivWithinAt on ; it is the derivative the density hypothesis already provides, so this adds no assumption. Bare deriv is not used.A trivializing formalization is ruled out: the conclusion is a bound at every real and every with , the conditional probability divides by (which the density hypothesis implies), and the hypotheses are satisfied by, for example, the exponential law (, ) and the Pareto law (, ).
A complete development needs the fundamental theorem of calculus with one-sided derivatives, a change of variables in interval integrals, and calculus of Real.rpow in the exponent parameter. The lemmas on and are reusable beyond this mission; proofs of any milestone are welcome independently.
Many stochastic models produce a stationary quantity that solves a random equation , with a random map independent of . The random difference equation (perpetuities in insurance and finance, the ARCH and GARCH volatility models, random walks in random environments), the Lindley equation of queueing theory, and the random recurrences behind probabilistic analyses of algorithms are all of this form. In these models the law of is rarely explicit, while the decay of its tail is what governs ruin probabilities, extreme values and buffer overflows.
Kesten (1973) showed that the stationary solution of has a power-law tail when for some , by a long argument specific to that equation. Goldie (1991) separated the renewal-theoretic core of the phenomenon from the particular equation: the implicit renewal theorem (Theorem 2.3) gives the power-law tail of any random variable whose tails are comparable to those of , with an explicit formula for the constant. Kesten's theorem and the tail results for several other random equations then follow by checking one integrability condition. The theorem is the standard entry point to the subject, reproduced in the monograph of Buraczewski, Damek and Mikosch (2016).
Timeline:
Let be a probability space and , two independent real random variables. No equation is assumed for .
A probability law on is arithmetic if it is concentrated on a lattice for some , and nonarithmetic otherwise. Fix . The Cramér-type conditions on are
Under them, is finite and positive (Lemma 2.2), with .
The tails of enter through two tail-comparison conditions
and the constants
In the Lean development these are CramerConditions κ (P.map M), cramerMean, TailCondPlus, TailCondMinus, Cplus, Cminus and Ctwo, in the namespace GoldieRenewal.Implicit.
Let satisfy the Cramér-type conditions and let be independent of .
Case 1 ( a.s.): (2.8) implies , and (2.9) implies , as .
Case 2 (): (2.8) and (2.9) together imply
The relation means , including .
Lemma 2.2 (negative drift of , ); Lemmas 9.1–9.2 (smoothed integrable functions are directly Riemann-integrable); Lemma 9.3 (a Tauberian step from averaged to pointwise tails); the renewal equation (9.8) and its key-renewal limit in Case 1; the Case 2a step law (9.11) with mean and nonarithmetic (9.12)–(9.13), and the renewal identity (9.15); the reduction (9.16) of Case 2b to Case 1.
The theorem turns a question about an unknown law into a question about integrability. For a random equation it suffices to compare with , which is often a moment computation; this yields power tails, with constants given by expectations, for perpetuities, Lindley-type equations, random polynomial and maximum equations (Goldie 1991, §§4–8). The explicit constant also decides when the tail is genuinely of order : the theorem has content only when , since otherwise .
The theorem has been proved for thirty years; it is not formalized in any proof assistant known to the mission. A formal development would provide reusable infrastructure absent from Mathlib: direct Riemann integrability, renewal measures of walks on the whole line, the two-sided key renewal theorem (Athreya, McDonald and Ney 1978), and a Tauberian lemma for monotone tails. The sibling missions on Kesten's theorem and on rates of convergence are built on the same setting.
The obvious argument writes as a telescoping sum along the multiplicative walk and applies the key renewal theorem to the result. It fails at three points. First, the function the key renewal theorem would be applied to, , is only integrable under (2.8), not directly Riemann-integrable, and the key renewal theorem is false for general integrable functions; so no conclusion about itself follows directly. Second, when takes both signs, alone is not a random walk that controls : the sign of decides which tail of is involved, so the walk is Markov-modulated. Third, the walk lives on the whole line and may jump to (when ), so renewal theory on , the version in most textbooks, does not apply.
IsProbabilityMeasure P; M, R measurable real random variables; independence is IndepFun R M P. In (9.16) the copy lives on the same space, with IdentDistrib M' M P P and iIndepFun of .P.map M; the moments are lower Lebesgue integrals in . The conditional law in (2.5) conditions on before taking , so Lean's Real.log 0 = 0 never enters; is an extended real with .P.real {ω | t < R ω} with the paper's strict inequalities. (2.8), (2.9) are IntegrableOn … (Set.Ioi 0); the constants are Bochner integrals, used only under the corresponding integrability hypothesis.Tendsto (fun t => t ^ κ * P.real {…}) atTop (𝓝 C).Three formalizations would trivialize the goal and are excluded: reading "" as a ratio (which is false when ); assuming (which forces ); and placing a key-renewal-theorem conclusion among the hypotheses.
Contributions welcome: proofs of any milestone; a general two-sided key renewal theorem for nonarithmetic laws with positive mean (reusable beyond this mission); Mathlib-quality lemmas on direct Riemann integrability and renewal measures.
Many operators of harmonic analysis are bounded on by an orthogonality argument but fail to be bounded on ; what survives at is a weak-type estimate . For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on for orthogonality reasons, and their behaviour on -bounded martingales is the delicate endpoint.
R. F. Gundy (1968) supplied the martingale analogue: an -bounded martingale can be written as the sum of three martingales, one bounded in , one whose differences are absolutely summable in , and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants , and . This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.
Timeline:
Let be a probability space and a nondecreasing sequence of sub--fields of . A martingale relative to is a sequence of integrable random variables with -measurable and . Its difference sequence is with , i.e. , (the convention is ).
The maximal function is , the square function is , and is its -th partial version. For ,
and is -bounded when . For , the exit time (with ) is the first index at which exceeds ; , , denote evaluation at the random index, with .
The Lean development names these objects dseq (), sqFnN/sqFn (, ), maxFnN/maxFn (, ), pNorm (), exitTime () and valAt/sqFnAt (evaluation at an index in ), all in the namespace BurkholderDFI.Gundy.
For every -bounded martingale and every there are martingales relative to the same -fields, with difference sequences , such that
The three bounds hold together; each alone is trivial ( satisfies the first two, the first and last).
with equality on the left for martingales.
The result. The decomposition is the standard device for passing from to weak-type estimates for martingale operators: an operator that is bounded on , controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type . Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class , martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants , , make every such weak-type constant explicit.
Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of -bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.
The obvious attempt imitates the Calderón–Zygmund cut directly: truncate at height , or stop it when it first exceeds . Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit and the stopped values on — so Doob's convergence theorem cannot be avoided.
Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from ; Lean's index is never read by any quantity in the statements, which use the paper's convention . Mathlib's martingale definition additionally constrains ; this is no restriction, since every martingale indexed from extends this way. The goal asserts that are Mathlib martingales for the same filtration as , and the identity is required for .
Further committed conventions:
A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.
Infrastructure needed: stopped values at unbounded stopping times and their bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.
Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.
Theorem 6.1 of the paper states that simulating steps requires at least the initial memory size and, asymptotically, a multiple of accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.
There are numbered balls and numbered cells. Cell initially contains ball , and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of accesses is written , and its visible sequence is .
A request sequence names a ball for each of rounds. A run satisfies if it is legal and there are indices such that ball is in the player's hand after the first accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.
A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of is identical for every pair of request sequences of length . Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.
For every correct oblivious player and every run in the support of its response, the mission targets
where and depend only on the fixed hand size . This is the paper's form, with representing the number of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.
The milestones record the first-round bound, the at-most- count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds
These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.
The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The term also accounts for the initially occupied memory, independently of the asymptotic term.
The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.
The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed -access run serves at most request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when . The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.
The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length .
The two printed estimates and are false: with and , taking both balls in two accesses satisfies all request sequences, while the printed product is . Footnote 29's also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold handles small .
Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.