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?
Factoring a polynomial with rational coefficients into irreducible factors is one of the basic tasks of computer algebra. Before 1982 the standard method (Berlekamp's algorithm modulo a small prime, Hensel lifting, then recombination of the -adic factors, as in Zassenhaus's approach) could take exponential time, because the number of ways to recombine modular factors grows exponentially with the number of factors. A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave the first deterministic polynomial-time algorithm for factoring primitive polynomials in (Math. Ann. 261, 1982). Its key idea is to replace recombination by a search for a short vector in a lattice, and the lattice basis reduction algorithm introduced for that purpose (the LLL algorithm) has since become a standard tool in number theory, cryptanalysis and integer programming.
Section 2 of the paper, Factors and Lattices, is the bridge between the two halves: it shows that an irreducible factor of can be read off from a reduced basis of a lattice built from a -adic factor of . This mission formalizes that section.
Timeline. Mignotte (1974) bounded the coefficients of a factor of an integer polynomial in terms of the polynomial itself. A. K. Lenstra (Mathematisch Centrum report IW 190/81, 1981, Theorem 2) proved the weaker statement that, under the same conditions, a short lattice vector has a nontrivial gcd with . LLL (1982) proved the sharper Propositions (2.7), (2.13) and (2.16) used here, which pin down the irreducible factor itself.
For with real coefficients, the length of is . For a positive integer , is the polynomial over obtained by reducing every coefficient modulo .
Throughout, is a prime number, a positive integer, and a polynomial of degree . A polynomial is fixed with
Write , so . Proposition (2.5) shows that has an irreducible factor with , unique up to sign; this is the factor the section recovers.
Fix an integer . The lattice is the set of polynomials of degree at most such that divides . Identifying with , is a lattice of rank with basis and determinant .
A basis of is reduced if its Gram–Schmidt data , satisfy for and for .
Assume
that is a reduced basis of , and that some satisfies
If is the largest such , then
and (2.17) holds for all .
Companion items: the basis of and (2.6), and the remark that for the vector is itself an irreducible factor of .
Proposition (2.16) is what makes the factoring algorithm of Sect. 3 correct: running the reduction for increasing , the first for which (2.15) holds produces by one gcd computation, and repeating on factors completely. Together with the polynomial running time of basis reduction (missions I and II of this series), it yields the polynomial-time factoring theorem (3.6). Proposition (2.7) on its own is a general principle, often reused: a polynomial that is divisible by modulo and has small norm relative to must share the factor with .
All results here are proved in the paper and standard in textbooks (e.g. von zur Gathen and Gerhard, Modern Computer Algebra). To our knowledge there is no machine-checked proof of (2.7), (2.13) or (2.16) in Lean or Mathlib. Mathlib has Hensel-type lemmas and the Mahler measure, including a coefficient-wise Mignotte bound and Landau's inequality, but not the form of Mignotte's bound used here, nor any of the lattice statements. A Lean development of this section would be the algebraic core of a verified LLL factoring theorem.
The obvious argument for (2.7) is to bound the resultant of and : it is divisible by when they share a factor modulo , and bounded by by Hadamard. That argument gives only , the weaker version of [8], not that divides . The paper's sharper statement needs a lattice of combinations , the projection to its top coefficients, and the congruence argument (2.11) that forces the low-degree elements of into ; formalizing it requires determinant and Hadamard bounds for a lattice of rank inside a space of polynomials.
Mignotte's bound needs the Mahler measure and the inequality , which is not the coefficient-wise form available in Mathlib. The step (2.19) needs Proposition (1.12) on reduced bases, which is the goal of mission I. The final part of (2.16) needs the primitivity of the basis vectors, which depends on being exactly the set of multiples of modulo of degree at most .
Polynomials are Polynomial ℤ; is g.map (Int.castRingHom (ZMod q)); is the square root of the sum of the squares of the coefficients over the support. Degrees are natDegree, except in (2.11), where degree with values in WithBot ℕ keeps as on the page. A polynomial of degree at most is identified with its coefficient vector in EuclideanSpace ℝ (Fin (m + 1)). Linear independence of is over on coefficient vectors; "basis for " means in , independent, and spanning over . Gram–Schmidt vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt.
Indices are 0-based: the paper's is b 0. The index of (2.16) is kept as the paper's 1-based value, , so appears unchanged. The powers , , and are real powers with real exponents.
The standing assumptions are hypotheses of every item that involves , or : prime, , , (2.1)–(2.4), . Mignotte's bound (which assumes only ) and (2.18) (pure linear algebra on polynomials of degree at most ) do not need them. The factor is any irreducible with and . A gcd is stated by its universal property (divides each, and every common divisor divides it), which determines it up to sign. Two milestones are stated slightly more generally than the page: Mignotte's bound for every divisor of degree at most , and (2.18) for every nonzero common divisor .
The goal does not assume (2.7), (2.13), Mignotte's bound, (2.18) or (2.19); these are milestones. A trivial formalization in which is an arbitrary divisor of , or in which "reduced basis" is asserted of a family that need not be a basis of , is ruled out by the definitions.
Needed infrastructure: Hensel-type arguments over , Gauss's lemma, the Mahler measure, Hadamard's inequality, and Proposition (1.12) on reduced bases. The lattice determinant results and the Mignotte bound are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the missing Mathlib infrastructure.
In a store-and-forward network, messages are cut into packets that travel from node to node along wires, one wire per time step, and wait in buffers between moves. Routing such traffic splits into two problems: choosing a path for each packet, and scheduling the packets along their paths, deciding at every step which packets move and which wait. Leighton, Maggs and Rao showed that the second problem always has an essentially optimal solution: once paths are fixed, two simple parameters of the paths determine the routing time up to a constant factor, on every network.
The result separates path selection from timing in the design of routing algorithms for parallel machines, and it reaches beyond networks: a job-shop problem in which every operation takes one unit of time and no job visits a machine twice is the same problem with jobs as packets and machines as edges.
Timeline.
A network is a directed multigraph: a type of nodes, a type of edges, and maps . A path is a list of edges with ; it is edge-simple if no edge occurs twice. A finite set of packets is given, each with its path.
The dilation is the largest number of edges on a path; the congestion is the largest number of paths through one edge. Since a packet crosses at most one edge per step and an edge carries at most one packet per step, every schedule needs at least steps.
A schedule assigns to every packet and every index of its path the step at which crosses its -th edge, strictly increasing in . Its length is the last crossing step. A packet waits in its initial queue before its first crossing, in the edge queue at the head of the edge it last crossed between two crossings, and in its final queue after its last crossing. Only edge queues count for queue size: the other two are fixed by the instance. A schedule is valid if at most one packet crosses each edge at each step.
For the proof, the paper measures schedules that are not yet valid through frames: a -frame is a run of consecutive steps, and the relative congestion of a frame is the largest number of packets crossing one edge in it, divided by .
There are absolute constants and such that every finite set of packets with edge-simple paths of congestion at most and dilation at most , on any network, has a valid schedule with
The constants are not fixed: the paper proves existence, and any constants are a valid answer.
The theorem shows that congestion and dilation, two quantities read off the paths alone, determine the optimal schedule length up to a constant factor on every network, with buffers of constant size. Path-selection algorithms that minimize therefore yield near-optimal routing, and the same bound holds for unit-time job shops without repeated machines. It is also an often-cited application of the Local Lemma beyond a single round of random choices: the proof applies it times in succession.
The result has been proved since 1994, and the algorithmic version since 1999. As far as is known, no part of it is machine-checked. The mission produces a formal model of store-and-forward schedules with edge queues and frames, a formal statement of the theorem that excludes the degenerate readings, and formal versions of the steps of its proof.
The naive approach gives each packet a random initial delay and then lets it move without waiting. That gives packets per edge per step, and steps after slowing down. Lemma 3.2 does better only in frames of size , not in single steps. Recursing on frames, as in Theorem 3.3, loses a constant factor per level and gives .
Removing that factor is the central difficulty. Each refinement must keep the relative congestion nearly unchanged, , which requires second-order terms in the tail estimates, delays spread over the block rather than inserted at its start, and careful handling of block boundaries. The constant queue bound needs an invariant: every packet waits at most once every steps. The Local Lemma gives existence only; the construction is non-constructive.
Conventions committed to in Lean:
V E : Type with src tgt : E → V, no finiteness or degree bound. Packets form a Fintype P; paths are List E with matching endpoints (List.IsChain) and List.Nodup.CongestionLE path c, DilationLE path d), equivalent to exact values because every bound is monotone.Timetable: time p k : ℕ, the step at which packet p crosses its k-th edge, at least 1 and strictly increasing in k. Length at most L means every crossing step is ≤ L. Valid means two different crossings of one edge happen at different steps.g at the end of step t counts crossings of g at a step ≤ t whose packet crosses its next edge at a step > t. Initial and final queues are not counted.frameCount τ g t T counts the packets that cross g at a step in [t, t+T). Relative congestion at most r in frames of size ≥ T₀ is frameCount ≤ r·T for all T ≥ 1 with T₀ ≤ T.log is Real.logb 2. Every O(1) and "sufficiently large" is a constant quantified before the instance, and in the goal ∃ K Q comes before the network.1 ≤ b, without which the page's statement is false.These choices rule out the trivial formalizations: constants chosen after the instance would make suffice; a schedule without edge exclusivity would make the greedy schedule of length a solution; a missing queue bound drops half of the theorem; and a statement without its length bound is solved by sending one packet at a time.
Not stated: Lemmas 3.6–3.10 and the summary of the refinement step (p. 20). They concern the block decomposition and delay-insertion rules of pp. 13–14 and 17–18, which the paper defines only in prose. Contributions are welcome on the Local Lemma (finite or general), the probabilistic estimates of Lemma 3.2, Lemma 3.5, the elementary simulation step, and formal definitions of the block operations from which Lemmas 3.6–3.10 can be stated. The schedule model is reusable for other routing results, such as the on-line algorithm of §2 or the results for leveled networks.
Sequencing jobs on one machine to minimize the total weighted completion time is one of the basic problems of scheduling theory. Without precedence constraints it is solved by Smith's ratio rule (1956): sequence the jobs in nonincreasing order of . With arbitrary precedence constraints the problem is NP-hard, as Lawler shows in the same report. Between these two extremes lies the class of series parallel precedence constraints, which covers chains, rooted trees and their nested combinations, and which is exactly the class that can be assembled from single jobs by "all of this before all of that" and "this independently of that".
Lawler's report (IRIA-LABORIA No. 205, 1976; Annals of Discrete Mathematics 2, 1978) gives an algorithm for this class, once a decomposition of the constraints is known. It is the standard reference for the polynomial case of .
Timeline.
There are jobs, forming a finite set , to be processed by a single machine. Precedence constraints are given by an acyclic digraph : job must precede job if there is a directed path from to . Job has a processing time and a real weight (of either sign). A feasible sequence lists every job once and never puts a job before one that must precede it. The machine starts at time without idle time, so the completion time of job is the sum of the processing times of and the jobs before it. The cost of a sequence is , and an optimal sequence is a feasible sequence of minimum cost.
A transitive series parallel digraph is built from single nodes by series composition and parallel composition of digraphs on disjoint node sets. is series parallel if its transitive closure is transitive series parallel. A decomposition tree records such a construction: its leaves are the jobs, and its internal nodes are marked (left son before right son) or .
Sidney's theory works with three notions. A nonempty is a module if every job outside must precede all of , must follow all of , or is unconstrained with respect to all of . A subset is an initial set of if it contains, with each of its jobs, every job of that must precede it. With
an initial set is -maximal if for every initial set of .
A composite job is a sequence of jobs treated as one job whose weight and processing time are the sums over its jobs. Lawler's algorithm works bottom-up on the decomposition tree and represents an optimal sequence for each node's module as a set of composite jobs: a leaf gives its job, a -node the union of its sons' sets, and an -node the output of the series procedure (Steps 1–3, p. 11), which absorbs elements of and into a composite job or until the ratios separate.
For a decomposition tree of and any run of the algorithm on producing the set of composite jobs, every arrangement of in nonincreasing ratio order, with each composite job expanded into its sequence, is an optimal sequence:
Ties, both in the algorithm's choice of minimal and maximal elements and in the final sort, may be broken arbitrarily.
A companion theorem states that the algorithm always has a run.
The result places with series parallel constraints in polynomial time. Sidney's module and -maximal initial set machinery, which it uses, is the decomposition later used in approximation algorithms for general precedence constraints; Theorems 1 and 2 hold for arbitrary acyclic constraints.
The algorithm and Sidney's theorems are proved in the literature; none of them has a machine-checked proof. The report proves Theorems 1 and 2 by citation to Sidney's 25 lemmas and argues the algorithm's correctness informally in a few paragraphs. A formal development supplies the missing invariants (what exactly is preserved at each node of the tree) and checks that arbitrary tie-breaking is harmless.
The algorithm's correctness rests on an invariant the page states only in passing: that composite jobs behave as single jobs. Read literally, "nonincreasing ratio order is optimal for and for " does not imply the same for their parallel composition. A composite job of two unconstrained jobs can be optimal on its own module yet blocks a better interleaving once another module is added. The invariant that makes the induction go through is that every composite job is a -maximal initial set of itself, and the series procedure must be shown to preserve it while merging. The second difficulty is Theorems 1 and 2 themselves: exchange arguments over sequences of a whole module, with real weights of either sign, under arbitrary acyclic constraints.
Jobs have a type with decidable equality; is a Finset ι; the arcs are a relation G : ι → ι → Prop with endpoints in , acyclic in the sense that no job reaches itself by a path, and "must precede" is Relation.TransGen G. Processing times are positive on , weights are arbitrary reals. The objective and optimality are the published SingleMachinePrec.Biclique.WeightedCompletion; feasibility is checked against the arcs of , which for a sequence listing each job once is the same as against its paths. "Optimal for " uses the job set .
The decomposition tree is an inductive SPTree with leaves, -nodes and -nodes. It is tied to by three hypotheses: its leaves are distinct, they are exactly , and on the transitive closure of equals the arc relation of the transitive series parallel digraph the tree builds. Composite jobs are lists of jobs, sets of composite jobs are lists of lists, and their ratio is over the list. The algorithm is an inductive relation (Run, SeriesMerge, SeriesLoop), so every tie-breaking is a run. The dummies of ratio in Step 1 become vacuous conditions on empty sets.
Committed conventions and disclosed deviations:
The goal assumes nothing about modules, Theorem 2 or subtrees, only the tree, the data and a run, and the companion theorem shows that runs exist, so the goal is neither trivial nor vacuous.
Needed infrastructure: exchange arguments for on lists, restriction of sequences to modules, induction over decomposition trees. Theorems 1 and 2 and the ratio-order lemma are reusable in any development. Proofs of any milestone, and of the goal from the milestones, are welcome.
Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.
J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.
Timeline.
Let be the group of permutations of . For , a sequence of positions is ascending if . The length of the longest ascending sequence, , is the largest such .
The uniform distribution on gives each of the permutations probability , so an event has probability . Let denote a permutation drawn from this distribution. The sequence converges in probability to a real number if, for every ,
For integers , denotes the number of ascending sequences of length in . For write
the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable ; in Lean it is , because also names the constant below.)
Let be the limit in probability of . Let be the unique positive root of , and . Then
and hence
Numerically and . The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of .
The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random -dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.
Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale ; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.
The upper bound needs care with asymptotics: (2.4.7) holds for each , but the passage to (2.4.8) uses Stirling's formula with and integers tending to infinity at rate , and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every , a suitable .
The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on ; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving directly from the counting definition of is not available. Both bounds also need the existence of , which is Theorem 7.
Equiv.Perm (Fin n); the permutation is named in Lean because is Real.pi.Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root ; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.
Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.
The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.
Work on a probability space . A continuous-parameter subadditive process is a family of real random variables indexed by . It satisfies whenever . Its stationarity says that, for every real shift , the complete shifted family has the same joint distribution as . Finally, the mean exists as a finite real number for each and obeys for one constant . These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.
For an interval , the oscillation is . A process has the local oscillation condition when for one nondegenerate interval . In §1.4 the paper states that this condition then holds on every bounded interval. The quantity is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).
The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.
For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable such that
The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.
Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.
The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.
An integer-time subadditive theorem controls only on its discrete skeleton. It cannot by itself rule out large values of for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.
The paper's displayed assertion (1.4.1), that converges as real under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).
Lean indexes the family by and uses only ; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of for every and one linear lower bound on its mean. The sample-space type is called so that denotes oscillation without ambiguity.
Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval with ; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and is integrable. No continuity of paths, ergodicity, or independence is assumed.
A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.
A flow shop is the simplest multi-stage production model: every job passes through the same machines in the same order, and the question is how to sequence the work so that everything is finished as early as possible. Gonzalez and Sahni's 1978 paper in Operations Research settled the computational complexity of the preemptive version of this problem, in which a task may be interrupted and resumed later on the same machine. For two machines the optimal finish time is computed by Johnson's rule, and preemption does not help. The paper shows that with three machines the preemptive problem is already NP-complete, and its second result, Theorem 2, strengthens this to NP-completeness in the strong sense: the problem stays hard even when the task times are written in unary.
Strong NP-completeness matters because it rules out a pseudo-polynomial algorithm, one whose running time is polynomial in the sum of the task lengths. The preemptive three-machine flow shop ( in later notation) is a standard entry in complexity classifications of scheduling problems, and Theorem 2 is the reference for its status. The paper notes that Garey and Johnson obtained a proof independently.
Timeline. Johnson (1954) solved the two-machine flow shop. Garey, Johnson and Sethi (1976) proved the non-preemptive three-machine flow shop NP-complete in the strong sense. Gonzalez and Sahni (1978) treated the preemptive case: Theorem 1 (ordinary NP-completeness via Partition) and Theorem 2 (strong NP-completeness via 3-Partition), the subject of this mission.
A flow shop has processors and a finite set of jobs. Task of job runs on and takes time ; zero times are allowed. For each job, task can begin only after task has been completed, and schedules start at time .
A preemptive schedule is given, as in the paper's footnote on p. 40, by finitely many pieces per task: the task is processed on its processor during . Pieces have , pieces on the same processor do not overlap, the pieces of a task have total length , and a piece of task starts only after every piece of every earlier task of the same job has ended. A task has no preemption when it is processed in at most one piece; a non-preemptive schedule has no preemption anywhere. The completion time of job is , the end of its last piece, and the finish time is .
3-Partition. An instance , , consists of a positive integer and nonnegative integers with and . It has a 3-partition if splits into disjoint sets , each of three elements with .
The instance FS. From the proof of Lemma 4 builds a three-processor flow shop with jobs:
Each processor carries total work exactly , and the threshold is .
For every 3-Partition instance with ,
and every task time of satisfies . The second clause records that the instance's numbers are bounded by those of , the reduction's contribution to "the problem size being measured as the sum of the length of the tasks".
The result. Theorem 2 places the preemptive three-machine flow shop among the strongly NP-hard scheduling problems, so no algorithm polynomial in the number of jobs and the total processing time exists unless P = NP. It also shows that allowing preemption, which makes several single-stage problems (such as ) easy, does not help for three-stage flow shops. Lemma 3, that preemptions on the first and last machines can be removed without changing the finish time, holds for any number of machines and is a reusable structural fact about flow-shop schedules.
Formalizing it. The result is proved on paper, and its proof of the "only if" direction is an informal busy-processor argument repeated window by window. As far as is known, no part of it has a machine-checked proof. A formal development has to make the interval accounting rigorous: why each processor is busy throughout , why exactly units of element jobs end on by , and how the argument restarts on . Lemma 3 needs an exchange argument on piece representations. Both are new for the platform.
The direction "3-partition schedule" is a direct construction. The hard direction is the converse. Preemption lets any task be split across many intervals, so the usual non-preemptive arguments, which reason about the order in which whole tasks run, do not apply directly. The paper's argument that the window must contain exactly three element jobs of total on depends on every processor being continuously busy, and turning "otherwise there is idle time" into a precise statement requires a careful account of which jobs are available to each processor at each moment. The induction on windows is then not a literal restriction of the schedule to a smaller instance, because pieces may cross the boundary at .
Fin m with 0; in , are 0, 1, 2.ResourceScheduling.Chain.ThreePartition (0-based indices, t parts, b , Valid, HasSolution), whose definition is the paper's p. 37 problem.Contributions welcome: the interval-accounting lemmas (busy processors, work available before a time), Lemma 3's exchange argument, and the schedule of Figure 2.
A finite Markov decision problem can have several policies with the same long-run average reward even though they behave differently before reaching a recurrent class. Average reward discards a finite initial advantage: dividing total reward by the horizon sends any fixed transient contribution to zero. In applications where the process runs for a long but unspecified time, this leaves a genuine choice among average-optimal policies. Bias optimality uses discounted values as the discount factor approaches one to resolve that choice. Kallenberg develops the criterion in Chapter 5 of Linear Programming and Finite Markovian Control Problems, following Blackwell's earlier notion of a nearly optimal policy.
The chapter asks for a way to recognize a bias optimal policy without comparing it directly with every possible sequence of history-dependent, randomized decisions. Its central characterization, Theorem 5.2.2, gives three tests involving only pure stationary policies. That change in the comparison class matters: there are finitely many pure stationary rules, while a general policy may depend on an unbounded history. The theorem also explains why average optimality alone leaves policies untied only at the gain level, while their bias vectors can differ. The two-state example in Figure 5.2.1 exhibits an average-optimal stationary rule that is not bias optimal (Kallenberg, pp. 163–164).
The state space is with . Each state has its own finite, nonempty set of admissible actions. Choosing earns the real reward immediately and moves to state with probability . The rows are stochastic: and . This is the chapter's standing assumption, stated at the opening of §5.2 (Kallenberg, p. 162).
A policy assigns a probability distribution on the actions available at the current state after every finite history. Thus includes randomized and history-dependent decisions. A pure stationary policy instead fixes one action for each state and uses it in every period. Time starts at . From initial state , let be expected reward in period , and let be expected discounted reward for . The optimal discounted value is the supremum of over all , taken separately for each state.
The average reward is ; its optimal value is again the statewise supremum over . The corresponding limsup is . A policy is average optimal when at every state. It is bias optimal when as at every state (Kallenberg, pp. 21–23 and 161).
For a pure stationary , write and . The stationary matrix is the Cesàro limit of the powers of . The deviation matrix and bias vector are
The gain of is . These are the book's Definitions 2.4.2 and notation (2.5.5), and their finite stochastic-matrix properties are recorded in Theorem 2.4.1 (Kallenberg, pp. 29 and 33–34).
The goal is Theorem 5.2.2, for each pure stationary . It asserts that the following are equivalent: (i) is bias optimal against the value over all ; (ii) for every , the vector limit exists and is nonnegative; (iii) is average optimal and, at every state , its bias is maximal among pure stationary policies optimal at that state; and (iv) for every , the vector limit
exists. These limits are read in the extended reals: a strictly positive gain gap makes a difference tend to , which satisfies the displayed inequality. The period rewards in the last formula are not discounted values. The printed clause (iii) has a typographical error in the set following max; its proof on p. 164 supplies the intended restriction . The formal statement uses that reading and records it explicitly.
Two earlier chapter results are milestones. Lemma 5.2.1 bounds the Abel limsup by the upper average reward for any policy. Theorem 5.2.1 says that bias optimality implies average optimality, with a two-state example showing that average optimality does not imply bias optimality. The later §5.3 linear-programming construction is a separate route to finding a bias optimal policy and is outside this mission's statement layer.
The equivalence allows bias optimality to be checked through discounted differences, bias vectors, or accumulated period rewards. Its bias-vector clause identifies the relevant comparison set: a policy can be optimal in average reward at one state without being optimal at every state, and that statewise distinction cannot be discarded. It also makes the bias criterion finer than average optimality, as the two-state counterexample shows (Kallenberg, pp. 163–165).
The source proves these results; the mission asks for machine-checked proofs of the stated equivalence and its two supporting results. The finite history and reward definitions can support later formalizations of Kallenberg's average-reward and constrained models. The matrix definitions can also be reused for results about finite Markov chains, including the Cesàro limit and deviation matrix. No machine-checked proof of this specific four-way characterization is claimed here.
Comparing average rewards alone loses the transient reward information that bias is designed to retain. The discounted comparison has an apparent divergence of order whenever two policies have different gains; the finite residual becomes meaningful only after those gain terms are separated. The accumulated-reward test also takes a second Cesàro average, so a direct identification with ordinary average reward would miss its bias contribution. The theorem has to preserve both the gain ordering and the finite bias remainder across these limiting regimes (Kallenberg, pp. 164–165).
For a general policy, the discounted value is defined by infinitely many history-dependent choices, whereas and apply to one fixed stationary matrix. This is the obstacle in passing from clause (i), which compares with all , to the tests against . Treating the optimal discounted value as a supremum over stationary policies by definition would erase that obstacle and change the theorem.
Lean uses Fin N with for states and a finite action type with nonempty state-dependent admissible subsets. Rewards are real, transition rows are stochastic, and policies are distributions on actions after complete finite histories. The finite sum of products defining each history's probability supplies ; no measure-theoretic path space is needed. Discounted rewards use a real infinite sum for near one from below. Average rewards are real liminf and limsup values of bounded sequences. Optimal values are statewise suprema over all admissible policies, not over just .
The matrix is a Cesàro limit and uses the book's inverse formula. Their convergence and nonsingularity for finite stochastic matrices are mathematical obligations, not added assumptions of the goal. The value of a totalized average and the value of a discounted sum outside its summable range do not enter the limits. Contributions to the finite-chain limit facts, boundedness of reward criteria, the Abel/Cesàro comparison, and the four equivalences are all within scope. A formalization that restricts the optimum in bias optimality to pure stationary policies would not be this theorem.
Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.
R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a -level linear program with fixed criteria can encode the truth of a quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the -hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case .
A multi-level program has real variables , a feasible set (a polyhedron in the linear case), and players who move in that order; player controls and minimises a fixed linear criterion . The solution sets are defined from the last mover upwards: is the set of at which player 1's criterion is minimal given the choices of all earlier movers, and in general keeps the points of minimising among the points of that agree with on . The value is on , when . The sets can be empty even when is a nonempty polytope: the paper's four-level Example has because is not closed.
A propositional formula over blocks of atoms (block has atoms) is encoded by the linear system : one variable per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for , , . The quantifier of block is when is even, so
is a sentence.
The game adds a bookkeeper, player , who moves last. Player controls the atoms of , and player also controls auxiliary variables ; the bookkeeper controls the , a variable fixed to , and auxiliary variables . Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions (or for universal ) and , where is the length of , , and at , otherwise.
Let be the set of optimal solutions of . Then ; at every optimum all atom variables and all are binary; and
Moreover, when (3.3) holds, is player 's block in some optimum iff is binary and the sentence (4.17) holds at the truth valuation of .
In attack order: Lemma 3.1 (correctness of on binary inputs); Lemma 4.1 (robustness of near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities and in ; (4.2) and (4.3) (player 1's and player 's responses on the gadgets); Lemma 4.4 (the induction on with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value iff ), the §2 Example, and Proposition 3.2 (the pure binary game ).
The theorem shows that deciding the value of a -level linear program with fixed criteria is at least as hard as deciding sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once , and even recognising an optimal move is -hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.
The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the , cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable has no upper bound).
The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight , and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.
k : Fin p is the paper's , owned by player in .solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires ; the value is not modelled.A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.
Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?
Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.
A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).
Let be a probability space. "Decreasing" means non-increasing throughout.
A survival function is IHRA if is decreasing on (p. 631). For an exponential life, is constant. IHRA says the average failure rate over never decreases.
Dependent damages. Let be nonnegative random variables, the damages caused by successive shocks, and let and . The paper's conditions (p. 636) are:
Wear process. is the wear accumulated in . The conditions (pp. 640–641) are:
The first passage time above a level is . Its survival function is , and is the distribution function of the wear at time .
If satisfies (4.8), (4.9) and (4.10), then for every level
that is, has an IHRA distribution.
An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate with damages satisfying (4.3)–(4.5) give an IHRA life .
The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities with decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.
Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.
The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of given . Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of . The extension from rational to arbitrary ratios uses the monotonicity of paths. The identification of as a right limit of needs the pathwise reading of (4.8). The natural first idea, approximating by a compound Poisson process, would add hypotheses the theorem does not have.
All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:
pr with IsProbabilityMeasure. Time is ; with every measurable.condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions , . "Is decreasing in " is read as "has a version decreasing in ".X i is the paper's , and the kernel κ k describes given .Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).
Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.
A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.
In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.
Timeline:
The state space is finite. Each state has a finite nonempty set of actions; action in state earns and moves to with probability , . Fix weights with .
The dual linear program has one pair of variables for each state and each admissible action . Its feasible set consists of the with
A pure stationary policy uses the action whenever the chain is in state . Its transition matrix is . For a stochastic matrix , the limit matrix exists, and the deviation matrix is . A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write for the ergodic sets of .
The representative of is
with for and, for , . The paper defines the same formulas for randomized stationary policies , with in place of .
for every finite Markov decision chain, every positive probability vector and every pure stationary policy . The statement contains feasibility of the representative.
Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.
The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of : the paper prints the denominator of as , a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, : ). The denominator is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.
Feasibility is a calculation with the identities and . Extremality is the substance. Restricted to the pairs , the constraints become the square system (7) in the state variables, and system (7) determines and the transient part of , but on each ergodic set it determines only up to adding a multiple of the stationary distribution of that class: the matrix is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of , uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.
MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets (nonempty), transition probabilities nonnegative with unit row sums. and are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.Set.extremePoints ℝ. Membership in it includes feasibility.vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent is the set of states accessible from . The maximum in is a Finset.sup' over that finite nonempty set.The ellipsoid method decides questions about a convex set by maintaining an ellipsoid that contains the relevant part of and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of : it only needs, for a query point , either a confirmation that is (nearly) in or a hyperplane (nearly) separating from . From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.
The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number of ellipsoid steps produces an -optimal point.
Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.
All norms are Euclidean: , and for a symmetric matrix is the largest absolute eigenvalue. is the closed Euclidean ball of radius about , and the set of points within distance of .
A convex body consists of a compact convex , , and with
A weak separation oracle with precision answers a query either with "", or with a vector , , such that for all .
Given an objective and an accuracy (with and ), set
Start from , . At step query the oracle at . If it answers "feasible", is a feasible index and ; otherwise . Put and
and obtain , by rounding , to binary digits, keeping symmetric. The ellipsoids are , and is the set of points of whose objective value is at least that of every feasible centre found before step .
In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is , and is the published LinearOptimization.ellipsoid (x k) (A k).
If is a feasible index whose centre is best among the feasible centres, , then
The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.
Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in , , , and . This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.
The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor , or rounding.
For the exact update with factor and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by , so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from by up to in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound is what controls it. The containment must absorb both errors, and it is the inflation factor , chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.
is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds , are stated as quadratic-form (eigenvalue) bounds. uses the natural logarithm and the integer ceiling.
The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within entrywise; and data are real rather than rational.
The page's standing assumptions , , (p. 173) are hypotheses. Two hypotheses are added, because the page's , and are absolute numbers and the claims fail at extreme scales:
Neither is needed in (13) or (34).
A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is , assuming it would hide the lemma's content.
Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.
Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.
Stochastic optimization asks for a decision in a set that minimises an expected loss when the distribution of the data is known only through a sample . The classical estimator, sample average approximation, replaces by the empirical distribution . Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to . Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an -divergence ball of radius and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.
A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).
Let be i.i.d. random elements of a separable metric space with law , and let be the empirical distribution of . Let be lower semicontinuous on , with measurable for , and let be a nonempty closed feasible set, as in the paper's opening setup (p. 1).
The divergence generator is convex with ; Assumption A asks moreover that be three times differentiable near with and . For a distribution with weights on the sample points, . The robust objective and the population objective are
with radius parameter . Their solution sets are and (display (23)). The inclusion distance from a set to a set is (display (6)).
Assumption E asks for a measurable envelope with for all and for some . A class of functions on is Glivenko–Cantelli (Definition 2) if almost surely.
Let Assumptions A and E hold, let be nonempty and compact, and let be continuous on for every . Then, in outer probability,
Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.
The result. Corollary 1 shows that robustness against a -divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over , which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.
The obvious argument writes as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term is the obstacle: the weights are not bounded uniformly in for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair and the uniform control of Lemma 13 are what make moments enough.
For the solution sets, uniform convergence of to does not by itself place the minimisers of near those of ; compactness of and continuity of are needed to separate on the complement of an -enlargement of from its minimum. Measurability is a further obstacle: suprema over uncountable and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.
ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; is the law of ξ 0, and uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each .ℝ → EReal satisfying the published IsPhiDivergenceFunction (never , finite on , , convex on ) plus the smoothness of Assumption A, stated on on an open interval around .probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. . Every supremum "over with " is read over , as in (4a).∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is for every with Mathlib's outer measure and no measurability hypothesis.A martingale is a sum of increments that are uncorrelated with the past. For sums of independent random variables, sizes are compared through the sum of squares of the summands; for martingales the corresponding object is the square function
Comparing the size of with the size of is one of the basic tools of probability and of harmonic analysis: it underlies Khintchine-type inequalities, the theory of martingale transforms, the Littlewood–Paley theory of dyadic and Fourier series, and the Burkholder–Davis–Gundy inequalities used throughout stochastic calculus.
Timeline. Paley (1932) proved bounds for the square function of Walsh–Paley series, the dyadic model case. Marcinkiewicz and Zygmund (1937–38) proved the analogous inequalities for sums of independent mean-zero random variables. Burkholder (1966, Ann. Math. Statist. 37) proved them for general martingales, , together with the weak-type bound for . Burkholder and Gundy (1970) extended the comparison to functions of moderate growth by distribution function ("good-") inequalities, and Davis (1970) settled for . The 1973 Wald lectures formalized here re-derive the inequality from one elementary stopping-time identity (Lemma 2.1), with explicit constants.
Let be a probability space and sub--fields of . A martingale relative to is a sequence of integrable random variables , with -measurable and ; a submartingale has in place of .
With the convention , the difference sequence is (so ). Write
For the exit time (with ) is a stopping time; , , denote evaluation at the random index, with and .
In Lean these are dseq, sqFnN, sqFn, maxFnN, lpNormE, pNorm, exitTime, valAt and sqFnAt in the namespace BurkholderDFI.SquareFnLp.
For each there are positive constants , depending only on , such that every martingale satisfies
The goal asserts only existence of the constants, so that it does not depend on the particular numbers the paper's proof produces.
In attack order:
Here is the conjugate exponent, .
The result. Theorem 3.2 says that a martingale is bounded in exactly when its square function lies in , with comparable norms. It reduces questions about , whose increments interact, to questions about , a sum of nonnegative terms. Immediate consequences include the boundedness of martingale transforms with (unconditionality of martingale differences in ), Marcinkiewicz–Zygmund and Khintchine inequalities, and, by passing through dyadic martingales, Littlewood–Paley inequalities. Theorem 3.1 is the endpoint estimate: at the strong inequality fails, and weak type is what survives.
The formalization. The theorem is classical and proved; the remaining work is to machine-check it. Mathlib at the pinned revision contains no square function inequality for martingales (no occurrence of Burkholder's inequality or of a martingale square function in Mathlib/Probability); it has Doob's maximal inequality for nonnegative submartingales, optional stopping, and a.e. convergence of -bounded submartingales. The mission would add the stopping-time identity of Lemma 2.1, the weak-type bound with constant 3, the explicit constants and , and the general extrapolation lemma (1.3), each reusable on its own.
The obvious route, expanding by orthogonality, works only at . For no such identity exists, and interpolation from needs an endpoint estimate that is itself the hard part: is not bounded on . The paper obtains the endpoint from Lemma 2.1, whose content is an exact computation at the random time ; turning it into rigorous Lean requires handling evaluation at (where the a.e. limit enters), passage to the limit in stopped identities with only control, and integrability of the products . The upper bound is not a formal consequence of the lower one at the same exponent: it requires passing to the conjugate exponent .
f : ℕ → Ω → ℝ; martingales and submartingales are Mathlib's Martingale f ℱ P / Submartingale f ℱ P for a filtration ℱ : Filtration ℕ _ with ℱ k . The paper's is built into every definition, which never reads Lean's f 0. Mathlib additionally relates f 0 to ; this is no restriction, since any martingale relative to extends by .Type (universe 0).Infrastructure that a complete development needs and that is reusable beyond this mission: evaluation of a process at an -valued stopping time, the layer-cake formula for -valued , and conditional-expectation martingales with their difference sequences. Proofs of any milestone, in any order, are welcome.
Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).
The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses against that bound over a horizon of length . A natural improvement is to re-solve the LP as capacity is consumed.
Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):
There are customer classes and resources . Over the horizon , class- customers arrive according to independent Poisson processes with rates . Accepting a class- customer earns and consumes units of each resource ; is the bill-of-materials matrix and its -th column. The initial capacity vector is . A customer can be accepted only if componentwise, where is the capacity remaining at its arrival.
For a capacity-per-unit-time vector , let
The DLP value is .
The Frequent Re-solving policy (FR) divides the horizon into unit periods . At the start of period , with remaining capacity , it sets , computes an optimal solution of the LP with right-hand side , and during the period accepts each class- arrival with probability , subject to the capacity check. Its expected revenue is . The LP may have several optimal solutions; the results hold for every rule choosing among them.
There is a constant , depending only on , and , such that for every integer , every capacity and every choice of optimal LP solutions,
The content is the uniformity: does not depend on , so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.
The result. Because bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order is exact for FR. The nondegeneracy assumption of the earlier analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from .
Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.
The obvious argument compares FR with the DLP period by period: the LP that FR solves at time differs from the original only in its right-hand side, so the loss should be controlled by how far drifts below . Two things break a naive version of this. First, is a ratio whose denominator shrinks to , so fluctuations late in the horizon are amplified; a crude bound on the drift at each sums to more than . Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions depend on the whole past, so the consumption in different periods is not independent.
Uniformity in is the whole point. Arguments that rely on a margin between and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.
The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.
piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for ).sel; every theorem quantifies over all selectors, with constants chosen before the selector.windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of are a forward recursion (frStateExp).A trivializing formalization is ruled out. The constant is chosen before . FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.
Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.
Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).
Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)
The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)
Let be a finite set of binary coordinates and a finite set of constraints. The data are a real matrix , a real vector , and nonnegative objective coefficients . A binary assignment is represented by the set of coordinates assigned one; all other coordinates are zero. Its slack and cost are
The assignment is feasible when for every . It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem and solutions (1)–(8). The coefficients of and may have either sign; and may be empty. Balas (1965), pp. 519, 523
The algorithm generates assignments , starting at . Among the generated feasible assignments, their least cost is the ceiling ; if there are none, . Each generated assignment has an improving set formed when it first appears. Later steps cancel candidate indices and keep records of which values attached to an earlier assignment have been cancelled by the time is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528
The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion below the current ceiling adds no index in ; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533
The mission's goal is Convergence Theorem 2:
The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for . These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a
The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533
The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)
It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533
Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem adds the paper's standing assumption . There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525
The ceiling is represented in WithTop ℝ, with for . The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set remains fixed after generation; the step-5 scan uses with the stored snapshot , as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: is abandoned when the algorithm is instructed to stop, or to check some with , including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads either as the cancellations accumulated so far during iteration or as the cancellation records at the transition that obtains . Balas (1965), pp. 525–533
The paper prints in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, ; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to , the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533
Backward stochastic differential equations (BSDEs) prescribe a process by its terminal value rather than its initial value: the unknown must be adapted to the information flow, yet must reach a given random variable at the horizon . They arise in mathematical finance (pricing and hedging, where is a contingent claim), in stochastic control (adjoint equations of the stochastic maximum principle) and in economics, where the stochastic differential utility of Duffie and Epstein (1992) defines the utility of a consumption stream as the solution of a backward equation.
Timeline:
Let be a complete filtered probability space satisfying the usual hypotheses: the filtration is right-continuous and contains every -null set. Let be an adapted process with right-continuous paths of bounded variation, , whose total variation process satisfies for a constant . Integrals are pathwise Lebesgue–Stieltjes integrals over .
The Doléans–Dade measure of is the finite measure on with
and is the space of jointly measurable processes with .
The data are a driver , jointly measurable, and a terminal value , subject to hypotheses 1–4:
The backward equation is the fixed-point problem for
When this is the Duffie–Epstein equation .
Under hypotheses 1–4 there is a progressively measurable process with càdlàg paths such that
is a semimartingale through the decomposition
and any two solutions in agree -almost everywhere.
In the order of the paper's argument:
Milestones 3–7 live inside the proof, after its reduction to nondecreasing .
The result. Theorem 2.4 gives well-posedness of a backward equation with no square-integrability and no Brownian structure: the filtration is arbitrary (subject to the usual hypotheses), the integrator may jump, and only first moments are required. In the case it settles the case of the Duffie–Epstein conjecture, so stochastic differential utility is well defined for integrable consumption data. The same fixed-point scheme, with the Doléans measure of a dominating process, is the basis of the coupled backward–forward result of §3 of the paper (a separate mission of this series).
Formalizing it. The theorem is proved in the literature but, as far as is known, has no machine-checked proof; Mathlib has conditional expectations, filtrations, martingales and Stieltjes measures, but no càdlàg process theory, no optional projection and no Doléans measure. A complete development produces these pieces. Its milestones also make precise points the paper leaves implicit: G is defined only up to versions, and the iterate bound is printed with in place of .
The obvious approach is to show that itself is a contraction on . It is not in general: the one-step bound is , and nothing makes . The argument must instead control the -th iterate. This needs exchanging a conditional expectation with a Stieltjes integral against a random measure, which is the optional projection identity (2.6). It also needs iterated integrals against an integrator with jumps, where the continuous-case identity fails and only the inequality survives. A second difficulty is measure-theoretic: is defined only almost surely for each fixed , and the norm sees the whole path. A version must be chosen with càdlàg paths before the equation even makes sense in .
BVIntegrator carrying with its Jordan decomposition as data, tied to Mathlib's eVariationOn so that . are Stieltjes measures of the paths.A component with a random lifetime that has survived to age still has a random residual life time . Reliability engineering, actuarial science and the statistics of exceedances over high thresholds all ask how the conditional law of given behaves when the age is large. If is exponential, the residual life has the same law at every age (lack of memory). In general it changes with , and the natural question, as in the limit theory of sample maxima, is which laws can arise as limits once the residual life is suitably rescaled and shifted.
A. A. Balkema and L. de Haan answered this question in Residual Life Time at Great Age (The Annals of Probability 2, 1974). The answer — a short list of limit types — later underlies the peaks-over-threshold method of extreme value statistics, where the continuous limit laws reappear as the generalized Pareto family (Pickands, 1975). This mission formalizes the classification theorem of the paper, Theorem 1, together with the steps of its proof in §1.
Let be a real random variable with distribution function and distribution tail . Throughout, for every (equivalently for all ), so that the conditioning event never has probability zero. The residual life distribution function at age is
which vanishes for .
A family of distribution functions converges weakly to as if at every continuity point of . A distribution function is nondegenerate if it is not the distribution function of a point mass. is of type if for all , with and real.
The limit laws are the following distribution functions, all equal to for ; for ,
with and the integer part of . The first two are continuous; the last two are discrete, with jumps where , respectively , crosses an integer.
The lemmas of §1 use a second normalization, which shifts instead of :
where is a nondegenerate distribution function. The two normalizations differ by .
If for all , , and
for a nondegenerate distribution function , then is of type , , or for some .
Theorem 1 is to residual lives what the extremal types theorem of Fisher–Tippett and Gnedenko is to maxima: it reduces the asymptotic analysis of the residual life to a four-type list, and with it the question of domains of attraction (§§2–3 of the paper) becomes well posed. The continuous types and are, after a change of parameters, the exponential and Pareto members of the generalized Pareto family used to model exceedances over high thresholds; the discrete types and show that once a shift is allowed, lattice-like tails produce limits with atoms, a phenomenon that the scale-only Theorem 2 excludes.
The theorem has been proved since 1974. It is not formalized in any proof assistant known to us, and Mathlib has neither weak convergence of distribution functions in the form used here, nor types, nor the residual-life limit laws. A formal development provides these objects, the functional equation (4) and its solution on a half line, and a checked proof that the four-type list is exactly right — including the discrete types, which are easy to lose in an informal treatment.
The obvious approach is to pass to the limit in the identity relating the residual lives at ages and , obtaining a Cauchy-type functional equation for , and to solve it. Two features block a direct application of the classical solution. First, the limit is a minimum with , so convergence carries no information on the half line where : equation (4) holds only where , and it does not determine by itself (the paper exhibits for , for , which satisfies (4) with , , yet is of no limit type); Lemma 2 is needed to recover where . Second, the solutions of the shifted equation for a monotone are not only linear: a periodic perturbation is possible, and its analysis produces the discrete laws through the integer part. A proof that assumes continuity of misses and .
The law of is a probability measure on ; and , with probabilities taken as real numbers. Every statement assumes for all , the paper's standing assumption; Lean's division by zero would otherwise make the conditional laws meaningless. The normalizations satisfy for all (only large matter). A limit distribution function is the distribution function of a probability measure on , so no mass escapes to ; nondegenerate means is not a point mass; the limit tail is , which is right-continuous. Weak convergence is convergence at the continuity points of the limit and nowhere else. The integer part is Int.floor. Each limit law is defined to be for .
Theorem 1 is stated in the normalization (1) of the theorem, the lemmas and cases in the normalization (2) of §1, as printed. Theorem 1 names its fourth family ; it is the introduction's . In Lemma 2 the left endpoint may be (Case 1 applies the lemma on the whole line), and the condition that lies in for is written out, since (8) presupposes it. "A pair in Lemma 1" and "", "" are stated through pairs satisfying (4); the proof of Lemma 1 shows the pair is unique. The commutation identity is posed without the Case 2 assumption, which its derivation does not use. No hypothesis of the paper is dropped and none is added beyond these readings.
The statement is not trivialized by dropping nondegeneracy (a point-mass limit is always attainable), by requiring convergence at every (which would exclude the discrete types), or by defining the limit laws without the integer part (which would turn the discrete types into continuous ones); the formalization does none of these.
A complete development needs: the residual-life distribution function and the normed tail, weak convergence of distribution functions, types, the four limit laws; then monotone solutions of Cauchy-type functional equations on half lines, with their periodic perturbations. The functional-equation results and the closing-display computations are reusable beyond this mission, for instance for the scale-only Theorem 2 and for the domain-of-attraction results of §§2–3. Proofs of any milestone, of alternative routes to Theorem 1, and of the closing display for each family separately are welcome.
A discrete-event simulation of a queue, an inventory system or a communication network produces an output process , and the quantity of interest is usually its steady-state mean , the long-run average of . The natural estimator is the time average of a run of length . A confidence interval for needs the scale of the fluctuations of , the variance constant of the central limit theorem . For correlated simulation output, is a sum of autocovariances at all lags and is hard to estimate consistently.
The method of standardized time series (STS), introduced by Schruben (Schruben 1983), avoids estimating : it divides the centred time average by a functional of the whole observed path that scales like , so that cancels. Batch means, the standardized sum, and the standardized maximum are all of this form.
Glynn and Iglehart (Glynn & Iglehart 1990) put the method on a general footing. They require only a functional central limit theorem (FCLT) for , and they identify an abstract class of standardizing functionals for which the cancellation works. This mission formalizes their basic limit theorem, Theorem 2.4, and the four claims of its proof. Two companion results of §2, display (2.2) and the weak law , are included as further targets.
is the space of continuous real functions on with the uniform norm and its Borel -algebra; is the identity path . For , is the discontinuity set of , the set of at which is not continuous. A standard Brownian motion on a probability space is a random element of with Gaussian finite-dimensional laws, and .
The output is a real-valued measurable process. Its scaled partial-integral process and its centred, rescaled version are
Assumption (2.1) asks for finite constants and such that as , weak convergence of random elements of . It holds for -mixing, strongly mixing, associated and regenerative output processes, among others.
The class of (2.3) consists of the measurable with
The proof uses the auxiliary map for and otherwise.
For every , under Assumption (2.1),
and .
Theorem 2.4 is the limit theorem behind every STS confidence interval. The limit is free of and of the output process, so with chosen so that equals a prescribed level, the interval has asymptotically exact coverage for . Each choice of gives a method: batch means with a fixed number of batches, Schruben's standardized sum, the standardized maximum. The later sections of the paper compare the lengths of these intervals with those of consistent-estimation intervals, and those comparisons start from Theorem 2.4.
The theorem is classical and its proof is short on paper. What is missing is a machine-checked version. The formal proof needs a continuous mapping theorem for maps that are continuous only almost surely at the limit, on the non-locally-compact space ; Mathlib has the version for continuous maps only. A formal Theorem 2.4 also makes the class and the C[0,1]-valued FCLT available for the other results of the paper, the expected-length lower bound and its non-attainment, which are formalized in sibling missions.
The algebra (milestones 3 and 4) is elementary. The difficulty is the continuous-mapping step. The map is in general not continuous: it can be discontinuous wherever is and wherever vanishes, and itself may be discontinuous on a large set (the standardized maximum is). The continuous mapping theorem for continuous maps does not apply. One needs its almost-sure form: if and , then . The class controls only along the law of , and the hypothesis of the almost-sure theorem is about at the scaled limit , so the conditions (2.3iii) and (2.3iv) have to be transported from to and from to .
is C(unitInterval, ℝ) with its sup-norm topology; the Borel MeasurableSpace instance is declared in the mission's definition file, since Mathlib has none at this commit. Weak convergence is Mathlib's TendstoInDistribution, for the -valued FCLT and for the real-valued conclusions. The standard Brownian motion is a measurable -valued map whose coordinates agree, for every , with a process satisfying Mathlib's IsBrownianReal. is the set of points where ContinuousAt g fails, and is an outer measure, so no measurability of is assumed.
is a -valued parameter pinned pointwise by , so it is determined by . Assumption (2.1) carries joint measurability of and local integrability of each path; the second is implicit in the paper and makes defined. The index runs over , and milestone 4 assumes because (2.3i) is applied with . Real division by zero returns in Lean, which agrees with the paper's convention for ; it matters only on events of probability zero in the limit. Condition (2.3iii) is printed "" and is read as .
Condition (2.3iv) is stated with the discontinuity set, not as continuity of : requiring continuous everywhere would exclude the standardized maximum of Example 3.10 and would make the continuous-mapping step trivial. The goal assumes nothing about , or any mapping theorem; these appear only in the milestones.
Contributions welcome: the almost-sure continuous mapping theorem for TendstoInDistribution on a metric space (reusable well beyond this mission), the cone property of under positive homogeneity, and evaluation at a point as a continuous map on . Mathlib does not yet construct a Brownian motion with continuous paths as a -valued random element, so the hypotheses cannot be instantiated inside Lean; this is a hypothesis on , not a vacuity.
Generating points uniformly distributed over a bounded region is a basic subroutine in Monte Carlo integration, in estimating the volume of a region, in randomized search for optimization, and in identifying redundant constraints of mathematical programs. When is given only implicitly, for instance by a system of inequalities, the classical methods break down in high dimension: transformation methods need a tractable description of , and rejection from an enclosing box or ball accepts a fraction of proposals that decays exponentially with .
Smith (Oper. Res. 32(6), 1984) studied a family of Markov chain methods, mixing algorithms, that avoid rejection altogether. The best known member is the Random Directions Algorithm, now called hit-and-run: from the current point, pick a direction uniformly at random and move to a uniformly random point of on the line through the current point in that direction. Boneh and Golan (1979) proposed it for constraint identification and conjectured, without proof, that it generates uniform points; Smith (1980, 1984) proved asymptotic uniformity, and Section 3 of the 1984 paper gives an explicit geometric convergence rate. This mission targets that rate, Theorem 3.
Later work, in particular Lovász (Math. Program. 86, 1999) and Lovász and Vempala (SIAM J. Comput. 35, 2006), proved polynomial mixing bounds for hit-and-run on convex bodies. Smith's bound is exponential in , but it holds for every open bounded region, convex or not, and from every starting point.
Write for -dimensional Lebesgue measure (content) on and for the Euclidean norm. Let be open, bounded and nonempty.
with the normalized surface measure of the sphere, and is its -step iterate.
the fraction of its smallest enclosing ball that fills.
For , every , every measurable and every ,
The constant is the paper's. The bound is uniform in the starting point and in , and it depends on only through and .
The result. Theorems 1 and 2 of the paper (the companion mission) establish only that the chain converges to . Theorem 3 makes this quantitative: the deviation from uniformity decays geometrically, at a rate computable from the dimension and the shape ratio alone. It shows which features of a region govern convergence, it gives a stopping rule with a guarantee, and it holds for non-convex regions, which the later polynomial-time analyses of hit-and-run do not cover. The paper notes the bound is of practical use only in low dimension; its value lies in being explicit and fully general.
Formalizing it. The theorem is proved in the paper, but parts of the proof are heuristic: the density is derived by a limit over small cubes, and the step from to uses a claim about circumscribed spheres that is false as stated (see below). A machine-checked proof would produce, as reusable components, a general-state-space Doeblin bound (no such theorem currently exists on the platform; the existing Doeblin results are finite-state), a measure-theoretic definition of hit-and-run as a Markov kernel, and the polar-coordinates computation of its density. None of these has, to our knowledge, been formalized.
The obvious argument is: the density is bounded below on , so Doeblin's condition holds, so the chain converges geometrically. Each step hides work. The density is not given by the algorithm but must be derived: the algorithm draws a direction and a scalar, and the change of variables from (direction, signed distance) to the endpoint is two-to-one and carries the Jacobian , which is where and the factor 2 come from. The Doeblin step needs a stationary law and the fact that the chain started in never leaves . For non-convex , the paper's "diameter along the ray" must be replaced by the measure of the line set, and the maximal chord does not bound the distance ; the diameter of is needed instead. Finally, the paper's assertion that the ball of radius circumscribes fails already for an equilateral triangle, so the final comparison must go through the smallest enclosing ball's radius .
EuclideanSpace ℝ (Fin n) with Lebesgue measure. The region is a set S with IsOpen S and Bornology.IsBounded S; boundedness is the paper's standing assumption ("bounded regions").ProbabilityTheory.Kernel built operationally from the algorithm: the uniform law on the line set, integrated against the normalized surface measure of the unit sphere (Mathlib's Measure.toSphere, divided by its total mass ). Off the kernel is the identity, which the chain started in never uses. The -step law is the published MarkovChainCLT.iterKernel.A seller with one indivisible object must decide whether to keep it or transfer it to one of several bidders whose values she does not observe. The allocation and the payment rule affect what bidders choose to report. Myerson's 1981 paper identifies a revenue-maximizing rule when bidders' private value estimates are independent, their densities are positive, and their valuations may be revised after learning other bidders' information. It covers value distributions for which the usual virtual-value rule is not monotone, by replacing each bidder's virtual value with an ironed priority level.
The question matters to auction design because a pointwise revenue-maximizing assignment can reward a bidder for understating a value. The seller must maximize expected utility subject to both incentive compatibility and each bidder's ability to decline participation. The paper's main theorem gives a specific allocation and payment pair that meets those constraints and attains the maximum. The result is proved in the source; this mission asks for a machine-checked formalization of it.
There is a finite nonempty set of bidders and one seller. Bidder has a value estimate in a finite interval , where ; endpoints may be negative and may differ between bidders. The continuous density is strictly positive on that interval and has total integral one. The bidders' estimates are independent, so a profile has density on . Write for the distribution function. The seller's known value for keeping the object is .
A revision effect describes the change in everyone else's valuation after bidder 's estimate becomes known. Bidder 's revised value is , while the seller's is . A direct mechanism assigns each profile an allocation probability and expected payment for each bidder. Payments may be negative and need not vanish when a bidder loses. Its feasibility conditions say that allocation probabilities are nonnegative and sum to at most one, each bidder's interim expected utility is nonnegative at every possible value, and truthful reporting yields at least as much interim utility as any other report. The seller maximizes her expected utility over all feasible mechanisms.
The virtual value is . In the general case it need not increase with . Myerson transforms through the quantile : , , and is the convex envelope of on . The slope of , extended across kinks, gives the ironed priority . At profile , the winning set contains exactly those bidders whose priority is maximal and at least .
The goal is Myerson's §6 theorem. The proposed rule shares the object equally among bidders in , or keeps it when is empty, and charges each bidder the envelope payment:
The target asserts that is feasible and that every feasible has seller utility no greater than that of . The milestone list follows the paper's reduction: Lemma 2 characterizes feasible direct mechanisms by a monotone interim allocation rule and an envelope identity; equation (4.12) rewrites seller utility using virtual values; Lemma 3 turns maximization of virtual surplus into optimality. Equations (6.9)–(6.13) compare virtual and ironed priorities and establish the optimality and monotonicity of the proposed allocation.
The theorem specifies both who receives the object and how payments are computed, including irregular distributions and bidder-specific supports. The ironed priorities preserve incentives while retaining the seller's maximal expected utility. Equation (4.12) also gives the revenue-equivalence consequence: once the allocation rule and each lowest-type interim utility are fixed, expected seller utility is fixed.
A formal proof would connect several reusable results: product distributions with bidder-specific densities, interim incentive constraints, an envelope characterization, virtual-surplus accounting, and one-dimensional convex ironing. The source theorem and milestones are currently statements to be proved in this development, not existing machine-checked results. Related Börgers auction statements on Prove2Me use a common nonnegative support, at least two bidders, zero revision effects, and zero seller value; they do not provide this general theorem.
Maximizing virtual surplus at each profile is straightforward only if each bidder's virtual value rises with her report. When it falls, the resulting win probability can also fall, violating the incentive constraint. Replacing virtual values by slopes of a convex envelope restores monotonicity, but then the proof must account exactly for the difference between the original and ironed objectives, including flat portions of the envelope. Payments must satisfy the interim envelope identity for every type, while the seller's objective includes both transfers and her value for retaining the object.
The Lean model uses a finite nonempty bidder type, real-valued reports and payments, one object, independent continuous positive densities normalized on each finite support, and continuous revision effects. The latter regularity is implicit in the paper's assertion that is continuous. No mean-zero condition on revision effects is imposed: the paper explicitly says its equation (2.9) is unnecessary. One bidder, negative support endpoints, unequal supports, and arbitrary seller value remain allowed.
The profile law is Lebesgue measure restricted to and weighted by the product density. Integrating a function after replacing coordinate represents the integral, because bidder 's marginal density has mass one. Mechanisms are total functions, but allocation and incentive conditions quantify over supported profiles and reports. Feasibility explicitly requires integrability of allocations, payments, and their report sections so no undefined Bochner expectation can acquire Lean's default value zero. The convex envelope is the two-point infimum of equation (6.3); its defining set is nonempty and bounded below on . The slope uses the right derivative below quantile one and the left derivative at one. The theorem requires feasibility of the proposed pair as well as its utility bound, ruling out an empty or unconstrained maximization claim.
The Stieltjes expressions in (6.9), (6.12), and (6.13) are combined into equivalent ordinary-integral comparisons over the profile law. A complete proof needs the one-dimensional envelope theorem, product-measure integration and Fubini results, differentiation of the convex envelope, and a careful endpoint treatment. The definitions of interim utilities and ironing can be reused for related auction models; contributions that establish these analytic components or the listed source lemmas are in scope.
A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.
The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size , and its threshold includes the case of support constraints. The paper's Section 6 gives the model and its two probability guarantees.
Let be a set of decisions. A subset is the domain; a real function is the cost. An uncertain outcome belongs to a measurable space with probability measure , and imposes a constraint set . For a sample of independent outcomes, the program minimizes over that belongs to every sampled . The sample law is . There is no algebraic or topological condition on the feasible sets or on .
A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is . Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.
The violation of a decision is . Thus is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function evaluated at the observed count, . For each , the paper also uses a generalized distribution function . It need not have total mass one.
For any and any -valued on , let be the infimum of feasible values over real polynomials of degree at most satisfying
The goal is the paper's Theorem 3:
The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous in Theorem 3's range for ; its generic setting and variational problem use .
For , the paper's Theorem 4 defines as the unique root of
With for and , its conclusion is
The terminal value is essential because the paper gives examples with and .
Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter . The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.
A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.
The observed support count is data-dependent. Conditioning on therefore cannot be treated as conditioning on a fixed subset of sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with , so the distributional characterization has one measure for every and moment equations for every sample size. The resulting infinite family must still be related to the finite degree- polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.
Lean represents the decision set by an arbitrary type , with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that is nonempty.
The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The are finite measures on , so the paper's Stieltjes integrals are represented as integrals over or against those measures. The polynomial class means degree at most , matching the coefficients in (36). The value is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.
The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of , and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.
Many discrete optimization problems can be described by linear inequalities, even when their feasible solutions are integer vectors. A linear description lets one study the geometry of the feasible set and connect combinatorial methods with linear programming. The number of inequalities may be large, so a more basic question is whether each inequality needs coefficients of manageable size. Karp and Papadimitriou separated this coefficient-size issue from the number and computational recognizability of the inequalities in their study of facial descriptions Karp and Papadimitriou, MIT/LCS/TM-154, pp. 3–7.
Their Lemma 1 identifies two common families for which small coefficients suffice: zero-one problems and problems given by an integer linear system. This result establishes a geometric premise used by the paper's later complexity discussion. It says nothing by itself about finding the inequalities efficiently or recognizing whether a proposed inequality belongs to a description. Those computational conditions belong to the paper's subsequent theorems Karp and Papadimitriou, pp. 5–8.
A combinatorial optimization problem here consists of a set of binary strings, a dimension for each , and a set of feasible nonnegative integer vectors of that dimension. The geometric object is the rational convex hull . The paper calls the rationals in its notation. The values of and outside carry no meaning. A feasible set may be empty; its convex hull is then empty as well Karp and Papadimitriou, Definition 1 and footnote, p. 3.
A facial description is a collection of triples , where , , and . For every rational vector and every , membership in must be equivalent to satisfying all inequalities indexed by triples of with first component . A facial description is small when one polynomial in bounds the binary size of every coefficient of every triple in the collection. The collection itself need not be small Karp and Papadimitriou, pp. 4–5.
A zero-one problem has only vectors with entries zero or one in each . An integer-programming-type problem gives an integral matrix and right-hand side and takes to be all nonnegative integer vectors satisfying . The dimensions of these data depend on . Their total binary coefficient size is controlled by the length of the encoded input Karp and Papadimitriou, pp. 5–6.
The mission goal is the complete statement for both classes:
The milestone list records three claims used in the paper's proof. In a zero-one hull, every vertex is a zero-one vector and there are no nonzero rays. For integer hulls, the cited vertex-size result gives a uniform polynomial bound on the coordinates of vertices. Finally, the Cramer's-rule calculation bounds an integral normal and intercept by when the geometric data have coordinates bounded by Karp and Papadimitriou, pp. 5–7.
Lemma 1 permits descriptions of the whole hull, including lower-dimensional hulls that require equations and unbounded integer hulls that have recession directions. It gives a coefficient bound for every input with one polynomial, rather than a polynomial chosen separately for each instance. This is the premise needed when the paper treats a facial description as a language of short encodable inequalities. The later assertion that an NP-recognizable small facial description places the decision problem in co-NP has a distinct hypothesis and is handled by the first mission of this series Karp and Papadimitriou, Theorem 1, pp. 7–8.
The mathematical result is known; the mission asks for a Lean proof of its precise rational, input-indexed version. The local declarations are proof obligations and do not yet carry verified proofs. Existing platform work includes a rational integer-hull definition reused here, a related open theorem of Cook–Gerards–Schrijver–Tardos that bounds normal coefficients under different hypotheses, and proved real-carrier versions of Meyer's polyhedrality and finite-generation results. The related open theorem does not supply Lemma 1: it has neither this zero-one case nor the bound on the intercept . The real-carrier theorems supply neither the input-size bound nor the paper's rational convention.
The zero-one case has bounded coordinates, but a complete description must also handle an empty hull and a hull contained in a proper affine subspace. Bounding only the facet inequalities of a full-dimensional nonempty polytope does not describe those cases. The integer-programming case adds unbounded directions, and the paper's printed identification of extreme rays with rows of is false. A faithful treatment must bound suitable recession directions and then obtain a uniform coefficient bound for the inequalities describing the hull Karp and Papadimitriou, pp. 5–7.
The Lean model uses List Bool for inputs, Fin (n z) → ℤ for feasible vectors, and Fin (n z) → ℚ for the convex hull. The published CookSensitivity.ChvatalRank.polyhedron and integerHull definitions provide the general rational integer-programming substrate. This mission adds only the paper's input-indexed problem, facial description, smallness condition, and two named problem classes. The three language-recognition requirements in the paper's Definition 1 are omitted because Lemma 1 never uses them; the resulting theorem applies to every such geometric problem, including every c.o.p. in the paper's narrower definition.
The polynomial bound is represented by with a single natural exponent chosen before every input and inequality. For an integer-programming-type input, the sum over all entries of and must be at most . This makes the paper's phrase “ specifies and ” an explicit binary-size condition. The cited vertex milestone bounds coordinates in terms of alone, as the page states: a zero column gives a line direction rather than a vertex. Its statement follows the paper's unrestricted formulation; the IP-type goal additionally imposes . The paper calls an -vector, but it has one entry per row of and is an -vector here. The Cramer's-rule milestone allows rows of size , as vertex differences can reach that size.
Empty feasible sets, dimension zero, lower-dimensional hulls, and unbounded IP hulls remain in the goal. A description restricted to full-dimensional facets, or a smallness exponent chosen separately for each input, would not meet it. A complete development needs rational convex hulls, integer-hull geometry, finite descriptions of rational polyhedra, bounds on vertices and recession generators, and finite-dimensional determinant estimates. The rational integer-hull definitions and the coefficient estimates are reusable beyond this mission; contributions that establish the three listed milestones or the remaining geometric steps are in scope.
Many network design and production–distribution problems have economies of scale: shipping twice as much along an arc costs less than twice as much, because of fixed charges, set-up costs or volume discounts. Modelled as network flows, such problems ask for a flow of least cost when each arc cost is a concave function of the flow on the arc. Classical instances include the uncapacitated lot-sizing problem, the fixed-charge transportation problem, and the Steiner tree problem in graphs. Unlike linear costs, concave costs make the problem NP-hard in general, and the usual linear-programming arguments do not apply directly.
Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987) 634–664) give the send-and-split method, a dynamic program that solves such problems in time exponential only in the number of demand nodes. Before the method can run, two questions must be settled: when does a minimum-cost flow exist at all, and can the arc costs be shifted so that they are nonnegative on flows? Theorem 1 of the paper answers both. This mission formalizes Theorem 1.
Timeline. Hirsch and Hoffman (1961) showed that a concave function bounded below on a polyhedron's extreme rays attains its minimum at a vertex; Rockafellar's Convex Analysis (1970, pp. 61, 343) gives the polyhedral form. Edmonds and Karp (1972) showed how to choose node potentials making linear arc costs nonnegative. Theorem 1 (1987) extends both to additive concave costs on uncapacitated networks.
A graph has nodes and a set of ordered pairs of distinct nodes, the arcs. A demand vector assigns a demand to each node (negative demands are supplies). A preflow is a nonnegative matrix carried by the arcs, and a flow for is a preflow with
inflow minus outflow equal to demand. A circulation is a flow for .
The flow cost is , where each is concave on and . A minimum-cost flow for is a flow whose cost is at most that of every flow for .
A preflow induces the subgraph of arcs with nonzero flow. An extreme flow is a flow whose induced subgraph is a forest (in the undirected sense; two antiparallel arcs form a cycle). A simple circuit is a directed cycle through at least two distinct nodes, with arc set ; a simple circulation is a circulation whose induced subgraph is a simple circuit. The slope at infinity is the limit of the right derivative of .
Two nodes are in the same strong component if chains (directed walks) join them both ways; a component is a sink if no chain leaves it. The augmented graph appends a node and an arc for exactly one node of each sink component. Its arc costs are on arcs inside strong components and arbitrary real numbers elsewhere; is the infimum of the costs of chains from to . For , the altered costs are .
The following are equivalent:
If moreover admits a flow and on arcs joining distinct strong components, where , they are equivalent to
and is real and satisfies .
The milestones are the statements the paper's proof rests on: the Hirsch–Hoffman extension (p. 638), , the bounds , the circuit-wise form of 4° ⇔ 5°, uniqueness of the extreme circulation, between strong components, and the two inequalities giving (all p. 639).
Theorem 1 decides existence of an optimum from the costs alone: conditions 4° and 5° do not mention the demand vector, so one test settles every demand pattern at once, and 3° guarantees the optimum may be sought among extreme (forest) flows, which is what the send-and-split recursion enumerates. Condition 6° is checkable by a shortest-chain computation, and 7° supplies node potentials that convert the instance into an equivalent one with nonnegative arc costs, the standing assumption of the paper's Theorem 2 and of its running-time analysis. For linear costs the theorem reduces to the familiar statement that a minimum-cost flow exists iff no simple circuit has negative cost.
The result is proved in the paper; it has not been machine-checked. The formalization adds a precise model of extreme flows over arcs (so that antiparallel arcs form a cycle), a treatment of slopes that may equal , and the Hirsch–Hoffman extension specialized to network polyhedra, which the paper cites rather than proves. Related platform items cover the linear, capacitated case: CycleCanceling.MinMean.minCost_iff_no_negative_cycle and CycleCanceling.MinMean.minCost_iff_exists_price (Goldberg–Tarjan), and LinearOptimization.positive_directed_cycle_of_circulation and LinearOptimization.network_basic_iff_tree on a different arc encoding.
The first idea, to argue as for linear costs by cancelling negative cycles, fails because concave costs are not additive along cycle decompositions: the cost of a flow is not the sum of the costs of its cycle and path components, and a circuit can be harmless at small flow and arbitrarily negative at large flow. Existence therefore depends on the asymptotic slopes , which may be , rather than on any finite cost evaluation. The implication from bounded rays to an attained minimum (Hirsch–Hoffman) requires identifying the vertices of the flow polyhedron with forest flows and its extreme rays with simple circulations. The potential step 6° ⇒ 7° needs a cost bound on arcs between strong components, where the concave cost is only controlled up to the total positive demand .
Nodes are Fin n; a graph is ArcGraph n, a Finset (Fin n × Fin n) of arcs without loops. Preflows are real matrices vanishing off the arcs; arc costs are functions , concave on Set.Ici 0 with value at (the paper's "without further mention" assumption, made a hypothesis). The augmented graph has nodes Option (Fin n), with none the node ; chain costs, and are EReal-valued.
The explicit readings of loose phrases are:
A formalization in which extreme flows are forests of a simple graph built from the support, in which chains are simple paths, or in which a chain of cost counts as a minimum would make 3°, 6° or the equivalence trivially or falsely true; all three are ruled out by the definitions. The running-time remarks, the computation paragraph and the linear-cost remark after the proof are not formalized. Contributions are welcome on the polyhedral side (vertices and extreme rays of ), on right derivatives of concave functions at infinity, and on walk costs with negative cycles; all are reusable beyond this mission.
A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).
The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.
There are classes, numbered in route order, and stations. Every unit of fluid enters class at rate one. On completing service in class , it becomes class ; after class , it leaves. The station serving class is . Different classes may share a station. The constituency of station is , and class has positive mean service requirement , so its service rate is . The nominal workload at station is . The paper assumes at every station. Dai and Weiss (1996), pp. 115–117.
For time , is the amount of fluid in class , and is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each remains nonnegative, each starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.
A priority ranking assigns a distinct rank to every class, with smaller rank meaning higher priority. For class , let contain the classes at the same station whose rank is at least as high as 's. In a preemptive-resume priority fluid model, capacity unused by may increase only when the fluid workload in is zero. Under LBFS, : a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.
Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and :
where . The same must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.
The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time
The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.
The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.
Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.
The load inequalities compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.
Lean represents classes and stations by finite index types. Their indices start at zero: Lean class corresponds to paper class , and LBFS is Fin.revPerm. The paths and are functions on all real times, while the fluid equations and conclusions are imposed only for . The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.
The service requirements are explicit so has its intended value. The drift and emptying-time milestones explicitly assume , since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when , its normalization is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.
Network revenue managers sell access to limited capacity over time. An airline, for example, may have several products that use the same seat inventory, with some products earning more revenue than others. The decision to accept a request must be made when it arrives, before future requests are known. A standard way to guide that decision is to solve a deterministic linear program using expected demand, then use its optimal allocation as a probability of acceptance. As inventory changes, one can solve the program again. Bumpensanti and Wang study how often to do so, and show that frequent re-solving has a real limitation when the linear program is degenerate: on a particular instance its expected loss grows at least as the square root of the selling horizon. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 3.1 and 5.1.
The same paper gives an infrequent re-solving policy with uniformly bounded regret and an upper bound of order for the frequent re-solving policy. The lower-bound result is the counterpart that identifies a case where that order cannot be removed by the frequent policy itself. It uses a two-class example small enough to expose the issue without other network complications. Bumpensanti and Wang, arXiv:1802.06192v3, Theorem 1 and Propositions 2–3.
There is one resource, initially with units of capacity, and two customer classes. Class arrives through an independent Poisson process of rate one. Accepting a customer uses one unit of capacity and earns price , where . Rejected requests earn nothing, and unused capacity has no terminal value. The higher-price class has priority in the deterministic allocation, but its realized demand is random. The horizon is a positive integer, divided into periods of length one. Bumpensanti and Wang, arXiv:1802.06192v3, Section 2, pp. 7–9, and Appendix C.1, p. 32.
At the start of a period with periods left and capacity , the deterministic linear program (DLP) chooses rates that maximize subject to and . In this instance its first coordinate is . The frequent re-solving policy (FR) accepts each class- request in that period with probability , provided capacity remains. It re-solves the DLP at the next period with the new capacity. This is Algorithm 2 specialized to the example. Bumpensanti and Wang, arXiv:1802.06192v3, Algorithm 2, p. 11, and Appendix D, p. 42.
The hindsight optimum knows the total demand from both classes at the end of the horizon and chooses the best feasible allocation using that information. Its expected value is ; the first argument is horizon length and the second is initial capacity. Let be the frequent policy's expected revenue. Since hindsight has more information, their difference is a regret benchmark. The formulation uses the paper's hindsight linear program, which is exact on this unit-consumption instance. Bumpensanti and Wang, arXiv:1802.06192v3, Eq. (3) and Definition 1, p. 9.
For every pair of prices , there are and such that, for all integer and every optimal DLP selector used by FR,
This specializes Proposition 2's existence statement to the explicit family in its Appendix C.1 proof. The constant may depend on the prices, but is chosen before the selector and the horizon. The benchmark is the hindsight value, as in the proposition. Bumpensanti and Wang, arXiv:1802.06192v3, Proposition 2, p. 18, and Appendix C.1, pp. 32–34.
The milestones record the optimal DLP allocation on the example and two clauses of Lemma 7. The latter estimate the probabilities that the high-price arrival count is moderately below its mean in the first third and moderately above its mean in the last third. With an integer phase length and , the first bound is
The third-phase bound uses the standard normal cumulative distribution function and the unrounded constant . Bumpensanti and Wang, arXiv:1802.06192v3, Lemma 7 and Eqs. (49)–(53), p. 40.
This result shows that solving the DLP every period does not, by itself, give a horizon-independent expected loss. The example has only one resource and two customer classes; the gap cannot be attributed to a large network. The paper's separate bounded-regret result uses a different re-solving schedule and acceptance rule, so formalizing this lower bound helps distinguish guarantees for the two policies. Together with the upper bound for FR, it identifies the square-root order as the relevant scale for this policy on the example. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 4–5.
The mathematical proposition is proved in the cited paper; the Lean goal here remains an open theorem statement. Formalizing it requires precise interfaces for a Poisson arrival model, a capacity-limited randomized policy, a hindsight LP benchmark, and asymptotic lower bounds. Those interfaces can be reused in later revenue-management results, while the two-class instance gives a concrete check on the conventions.
The initial DLP solution allocates the average capacity to the high-price class. A simple intuition might therefore predict that repeated re-solving preserves capacity for that class. The remaining-capacity ratio, however, responds to realized arrivals; when the ratio rises above one, the re-solved LP assigns positive acceptance probability to the lower-price class. The policy then spends capacity before later high-price arrivals are known. The lower-bound analysis needs a path event that controls arrivals through the middle phase and a joint event involving the policy's accepted requests. Marginal Poisson counts alone do not determine those admissions. Bumpensanti and Wang, arXiv:1802.06192v3, Appendix C.1, pp. 32–34.
Lean uses Fin 2 for classes and Fin 1 for the resource. The general model takes positive Poisson rates, nonnegative prices and nonnegative consumption. On the lower-bound instance the rates and consumptions equal one, capacity equals , and prices satisfy . These are the operational standing assumptions of the paper's Section 2 and the positive-price reading used by the example. Optimal DLP ties are represented by quantifying over every selector. The LP value is the published RLPBidPrice.Unbiased.piValue definition, evaluated on nonnegative capacity vectors; the rate and capacity conventions make its real supremum well posed.
The window law superposes the independent class Poisson processes into a Poisson total count, independent class labels, and independent Bernoulli acceptance marks. A fold over ordered arrivals applies Algorithm 2's capacity check after every acceptance. The expected hindsight value sums over independent total demand counts, and the FR value is a backward recursion over the remaining unit periods. The target's is strictly positive and fixed before the horizon, so neither a zero constant nor a horizon-dependent constant can satisfy it trivially.
The two Lemma 7 milestones cover only and . Its continuous-time event and the joint admission event require a path probability space and are outside this draft. Equation (52) yields ; the printed rounds that value upward. The source proof divides into three exact integer-length phases, while Proposition 2 is stated for all sufficiently large ; this gap requires attention in a complete proof. The source here is arXiv:1802.06192v3, whose printed and PDF page numbers coincide.