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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).
The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.
Let be positive integers and a probability space. A fixed real matrix has rows . Random vectors and give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule , where the real matrix is chosen before is realized. Write and . A number is the given aspiration value. For each row , its reliability level is strictly between and , and is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.
The residual has raw second moment and negative mean . The aspiration error has raw second moment . These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is ; the model records the paper's assumption that the components of and are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.
Program (38) chooses and maximizes . Its inequalities bound the mean objective below by , bound below by the root-mean-square aspiration error, and bound each nonnegative between the row's risk term and . The denominator satisfies . Program (39) introduces a nonnegative scale and barred variables. It fixes and maximizes the linear objective . The barred moments are calculated from and by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.
Let contain every point satisfying all of (39), including . The paper's convex-programming claim becomes
The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.
Let be the feasible set of (38). Provided is nonempty, the mission goal states that the normalized substitution sends each point of to a point of with the same objective, and that
The suprema may be infinite. The equality concerns the complete program (39), including . Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.
The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.
The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.
The pointwise substitution only reaches points of (39) with , while (39) explicitly permits . Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: is a raw second moment and is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.
Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure , and Bochner integrals for the moments. Square integrability is stated for every component of and and every product ; this keeps the expected squares meaningful. The paper assumes and are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile is imported from the published Cohen2019.Robust.PhiInvReal, with excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.
The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization , strict , and weak are separate conditions. The slice is included, and the main theorem assumes nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.
Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan , the time at which the last operation finishes.
The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case is binary NP-hard, so two machines is exactly where the problem is easy.
Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for , proved NP-hardness for , and gave a polynomial algorithm for the preemptive problem . Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for . Lenstra (cited as forthcoming in the survey) showed , and unary NP-hard.
There are jobs and two machines , . Job has an operation on of length and an operation on of length . There is no preemption, and every job is available at time . A schedule assigns start times and to the two operations of , which then occupy on and on .
A schedule is feasible if
Write and for the two machine loads. The survey's construction uses the sets
two distinct jobs , with and , and , .
and the optimum is attained. Formally, for every : a feasible schedule completing every operation by exists if and only if , and for all . The goal mentions neither , , , nor the case analysis; those are the milestones.
The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard marks the complexity boundary for nonpreemptive open shops.
Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.
The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on then in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed , because the open shop needs some job to visit first. The survey's construction moves exactly one job, , to the front of , and its correctness depends on the choice of and and on the case split on versus . Figures 5.3 and 5.4 are drawn for ; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.
All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ( is index ). Processing times and start times are real numbers with ; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be and the goal false.
"Length at most " is CompletesBy a b S L: every operation ends by . Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to " equals the maximum and is attained". A maximum over or appears as a bound on every member, which is also correct for empty or . The orders of and are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.
The milestone on the choice of , assumes , which the page presupposes; the goal does not, and covers as well. The lower bound assumes , which matters only for .
A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all , and no constant is fixed.
Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside ), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.
Queueing results often relate an average accumulated over customers to an average accumulated over time. In the familiar relation , the long-run average number in a system equals the arrival rate times the average time spent there. Glynn and Whitt study a broader relation, , that can represent queue lengths and waiting times but also costs, work, and other cumulative inputs. Their framework is deterministic: a stochastic model may supply a sample path, yet the central comparison is a statement about functions on that path. This lets the same theorem apply to different queueing models without choosing a probability law for each one. Glynn and Whitt (1989)
The paper asks for more than the usual forward implication from a customer average to a time average. Its main theorem identifies conditions under which either average has a finite limit exactly when the other does. It also compares lim inf and lim sup when ordinary limits fail to exist. Both questions matter when sample paths fluctuate: convergence of one average cannot simply be inferred from a visual similarity between the two ways of indexing the input. Glynn and Whitt (1989), §§1–2
A cumulative input is a real-valued function on , nondecreasing separately in the customer coordinate and the time coordinate . Its marginal limits and are finite for every fixed argument. The first counts all eventual input associated with customers through index ; the second counts all input accumulated through time . The marginal averages are
The paper permits cumulative inputs that are not distribution functions of measures on rectangles. In particular, it does not require a rectangle-increment inequality or nonnegative values of . The finite marginal limits and monotonicity are the actual assumptions of its general framework. Glynn and Whitt (1989), p. 635, (1)
A time change , for , is finite, nonnegative, nondecreasing, and right-continuous, and tends to infinity with . Its right-continuous inverse is . The two time changes may differ. Both have the same asymptotic rate for a positive finite . The paper's two approximation conditions are
as , where is the left limit. Condition (14) concerns input already present by a left-limit time; condition (15) concerns input not yet present by a right-limit time. Glynn and Whitt (1989), p. 638, (3), (14)–(15)
With only (14) and the rate for , the corrected upper bounds are
With only (15) and the rate for , the corrected lower bounds reverse both inequalities. The two bounds remain useful separately when only one approximation condition holds. Their lim inf and lim sup may be infinite. Glynn and Whitt (1989), p. 639, Theorem 1(a)–(b) and Remark 2
Under both conditions, Theorem 1(c) asserts equality of the respective lim inf and lim sup. The mission goal is Theorem 1(f): for finite real limits,
Here the equivalence means existence of finite limits, with the second clause identifying their values. The lim inf and lim sup statement is retained as a milestone because it also covers nonconvergent paths. Glynn and Whitt (1989), p. 639, Theorem 1(c), (f)
The goal gives a two-way transfer between customer-indexed and time-indexed long-run averages. If an application establishes one finite average, the theorem supplies the other and fixes its value. The one-sided milestones give meaningful bounds when only one approximation condition is available; the lim inf and lim sup milestone retains information when neither average converges. These outcomes are stated for a general cumulative input, so applications can supply their own , , and without changing the theorem. Glynn and Whitt (1989), §§2–4
The paper proves these results on paper. The formalization target is a machine-checked interface for the paper's deterministic framework, its inversion lemmas, its asymptotic inequalities, and the two-way limit theorem. At this drafting stage the Lean theorem statements compile with proof placeholders; no machine-checked proofs of these new statements are claimed. The definitions and inverse-rate lemma can be reused in other sample-path results.
The two marginal averages examine different slices of , and a time change may jump or have flat intervals. A direct substitution of does not give an equality between and under the paper's assumptions. The left limit in (14) and the value in (15) also behave differently at jumps. The inverse connects the coordinates, but its boundary behavior and rate must be handled before comparing the averages. These issues are present even without stochastic randomness. Glynn and Whitt (1989), pp. 638–639
Lean represents by nonnegative real numbers and by a real-valued function with separate monotonicity and bounded marginal ranges. Real suprema represent and ; the boundedness fields ensure those suprema are the paper's finite limits. The inverse is an infimum of a nonempty set because . The left limit is the supremum over earlier nonnegative arguments, with . Ratios at zero use Lean's total division convention, but every ratio assertion is asymptotic at infinity.
Lim inf and lim sup are taken in the extended reals so an unbounded average retains an infinite limit. Multiplication by happens in the reals before conversion. Ordinary limits in Theorem 1(f) are finite real limits. The two time changes are independent and share only the positive rate . The goal assumes only (14), (15), and the stated time-change rates; it does not assume its own inverse-rate or asymptotic conclusions. No nonnegativity or rectangle inequality is imposed on .
Theorem 1(a) and (b) have their hypothesis pairing reversed in print. The formalized one-sided bounds use the corrected pairing, and the milestone text preserves the printed source for audit. The intermediate expressions involving are excluded from the corrected statements because the framework does not assume customer-coordinate right continuity. Theorem 1(c) and (f) use both conditions and are true as printed. The scope includes the definitions, Lemmas 1–2, corrected parts (a)–(b), and parts (c) and (f). Contributions toward their proofs and reusable time-change lemmas are welcome. Glynn and Whitt (1989), p. 639, Theorem 1
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).
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 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.
In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task has a length and a preferred starting time , and the discrepancy of a task started at time is . The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy : a linear-time test for a given bound after an sort, combined with a search over .
This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).
Fix a bound . A schedule has maximum discrepancy at most exactly when every task starts no earlier than its release time and finishes no later than its deadline (p. 342). These release times and deadlines are in special form: with , for every task
From here on the data are arbitrary reals , , in special form for some .
A schedule is an execution order ( is the task in position ) with starting times , such that a task finishes no later than any later-positioned task starts: for . It is feasible if and for every . Its makespan is , and it is optimum if it is feasible and no feasible schedule has a smaller makespan.
Let be a task of largest deadline. A schedule has the release time property if every task executed after has release time strictly later than the starting time of . When the tasks are indexed with , a schedule is in standard form with split index , , if it begins with an optimum schedule of , followed by started at the maximum of and the completion time of that first part, followed by in this order without idle time.
Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with .
Corollary 2 reduces the search for an optimum schedule of to candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in time after an sort; combined with a search over it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.
The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.
The obvious argument fails in Theorem 4. Exchanging a straggler (a task after released no later than starts) with shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after starts has , hence exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after , then fewest tasks between and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.
Tasks are indexed by Fin N (0-based: the paper's are ; the paper's in Corollary 2 is the index ). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.
The standing hypotheses on every structural item are , , (from , the in , and nonnegative lengths); since , start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task () is not a task; an empty first part completes at time . Corollary 1's "the set of all tasks with deadline or less" is read as excluding , the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.
A trivializing formalization is excluded: the standard form pins 's start to and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.
Running times (, ) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.
A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition of players is assigned the set of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.
Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.
The players are . A coalition is identified with its characteristic vector , and . A fuzzy coalition is a vector of participation rates with support . Write , for the vectors vanishing off , for its nonnegative part, and for the vectors strictly positive on .
A fuzzy game without side payments assigns to each a nonempty, closed, convex set . Each is comprehensive, meaning , and bounded above, meaning for some . The map is positively homogeneous: for every . Its core is the set of such that for every fuzzy coalition . With the support function and the simplex , a weak (resp. strong) canonical cooperative equilibrium is a together with a (resp. with all coordinates positive) satisfying for every .
A usual NTU game lives on a family of coalitions that contains and every singleton. For each , the set is nonempty, closed, convex, comprehensive and bounded above. A balance of is a vector of weights on with for every , and is the set of balances of . The fuzzy extension of the game is
and the game is balanced if .
For a balanced game without side payments,
and in particular .
Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer , that sandwiches the core.
The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.
Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each , so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map at , Ky Fan's inequality on a truncated simplex where all , and a limit as . That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in and convex and lower semicontinuous in . Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.
All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.
Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. is encoded as "vanishes where ", which equals for .EReal, so an unbounded supremum is and never a junk .The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: is a superadditive fuzzy game, and is a balanced game on every admissible , with in both cores.
Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.
A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).
This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.
There are tasks, indexed . Task has a nonnegative length , a nonnegative preferred starting time , and an actual starting time . Once started, it occupies the one processor until . Each start must be nonnegative. For the fixed-order problem, task must finish before task starts, so . This permits idle time when the inequality is strict. The task's discrepancy is ; because its preferred completion is , this is also its absolute completion-time discrepancy. The total discrepancy is
A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule for the first tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).
For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.
The main target is the paper's Theorem 2. For all nonnegative task data and every , the actual schedule produced by the block-shifting algorithm is feasible and satisfies
This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).
The companion target is Theorem 3. If every task has a common length and the preferred starts are indexed so that , then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:
The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).
Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).
The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.
Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).
The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below count. Task in Lean is the paper's . Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's model.
The algorithm is defined by its stated insertion and single-block-shift operations. Defining as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.
Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time leaves it at time . The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.
Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.
Timeline:
Consider one arc. Vehicles enter it at the entry rate , a continuous function of time ; the first vehicle enters at time . For an exit-time function , the arc volume at time is the inflow mass of the vehicles that entered during and have not left by time :
The linear delay function (18) of the paper is
a fixed free-flow travel time plus a queueing time determined by the service rate . The exit time is entry time plus delay, so is pinned by the exit-time equation
The equation is implicit: appears on the right through the volume. The proof partitions time at , ; in particular is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.
For and a nonnegative continuous entry rate , every satisfying the exit-time equation is strictly increasing on :
and hence injective there, so exists.
A supporting, non-milestone item states that the exit-time equation has a solution for every admissible .
The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.
The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.
The obvious argument differentiates and bounds the outflow rate. But the volume can only be written as once is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on the volume depends only on restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions , where is generally not differentiable, and show that the junctions do not accumulate.
Time is real; the entry rate is a function with and continuous on . Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval . The paper's separate pieces are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis , without which it is false.
The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through or assumed monotone would assume the conclusion and is ruled out.
The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.
Alternating-offer bargaining asks how an agreement is selected when two people can keep making proposals until one accepts. A prediction based only on behavior at the start may rely on threats that would no longer be sensible after a rejection. Ariel Rubinstein's 1982 paper studies strategies after every possible sequence of offers and gives a characterization of the partitions compatible with perfect equilibrium. Its setting has a unit pie, complete information, no fixed last round, and preferences that may describe more than a particular discount formula.
The question matters for sequential bargaining models in which the order of moves and the cost of delay affect the agreement. The paper distinguishes the set obtained when player 1 offers first from the set obtained when player 2 offers first. It also provides applications to fixed bargaining costs and fixed discount factors. This mission targets the paper's general characterization, from which those examples can be studied without building a new equilibrium concept for each preference family.
A partition is a number : player 1 receives of the unit pie and player 2 receives . An outcome means that the offer is accepted in period ; denotes perpetual disagreement. Periods of actual play start at 1. The paper also uses when comparing acceptance of a current offer with a future outcome. Each player has a complete, reflexive, transitive preference relation on outcomes. Strict preference and indifference are derived from it.
The game alternates proposals and responses. One player offers a partition, the other accepts or rejects, and rejection makes the responder the next proposer. A strategy specifies what a player does after every possible history, including histories inconsistent with the player's earlier plans. A perfect equilibrium requires the relevant player's continuation to withstand every alternative continuation strategy at each rejected history and to make a planned acceptance or rejection consistent with the current offer. The empty history is included, so the opening proposer must also have no profitable deviation.
Write for the set of player-1 shares reached by perfect equilibria when player 1 opens, and for the corresponding set when player 2 opens. Perpetual disagreement contributes no share to either set. Define by a pair of one-period thresholds: for , is the smallest share whose immediate acceptance player 1 weakly prefers to , and is the largest share whose immediate acceptance player 2 weakly prefers to . Let and be its coordinate projections. All four sets contain numbers interpreted as player-1 shares, even when player 2 moves first. These are the objects of Sections 2–5.
Under the paper's five preference assumptions (A-1)–(A-5), the goal is its THEOREM on p. 106:
with and nonempty closed intervals and some satisfying
The translation parameter is allowed to be zero, and either interval may be a single point. The goal fixes the paper's general shape without choosing a particular utility representation or assuming immediate agreement in every equilibrium.
The attack path follows Lemmas 1–4 and Propositions 1–4 in their printed order. The lemmas constrain how a partition in one opening order relates to a feasible continuation in the other. Proposition 1 places each pair in inside ; Proposition 2 asserts existence; Proposition 3 describes as a closed segment parallel to the diagonal; Proposition 4 gives the reverse containment of and in the threshold projections. Each numbered result is a separate theorem target.
The theorem identifies the full set of equilibrium partitions from preference comparisons one period apart. Nonemptiness says the model admits at least one equilibrium partition in either opening order. The interval conclusion describes cases with multiple equilibrium shares, while the translate relation states exactly how reversing the first mover changes the two sets. In the paper's discounting example, a single share is selected under the stated parameter conditions; in a fixed-cost boundary case, multiple shares can occur. These are applications in Section 6, not assumptions of the general target.
Rubinstein proved the result in 1982. Here the definitions and theorem statements are Lean drafts; the numbered targets and the main theorem still require machine-checked proofs. A local verification module establishes that one discounting instance satisfies the first three axioms and that the paper's Section 3 strategy example accepts its first offer in period 1. Completing the mission would give a reusable formal account of an infinite-horizon alternating-offer game and its subgame equilibrium conditions, alongside the paper's characterization.
A first-round equilibrium condition does not control what a strategy promises after an offer is rejected. The paper's equilibrium definition checks the entire continuation at every history, with the player's role changing after each rejection. As a result, showing that a proposed share is an equilibrium partition requires more than checking the opening offer: the answer and the next proposal must remain consistent throughout the game tree. The model also allows arbitrary complete preferences satisfying axioms, so a calculation with one discount function cannot establish the general theorem.
The boundary at a zero share requires care. Assumption (A-2) asserts strict preference for earlier positive shares; it says nothing directly about a player receiving zero. The printed proof of Lemma 1 invokes it for a comparison that can occur at that boundary. The local lemma drafts explicitly carry the paper's (A-4) closedness axiom to support that comparison. This added assumption, and its propagation to Lemmas 2–4, is disclosed in the audit notes rather than silently attributed to the Section 4 statement.
Lean represents as the subtype of real numbers in . Outcomes are an option type: an agreement contains a partition and a natural-number period, while none is perpetual disagreement. This prevents an endless play from acquiring a default last partition. Strategies are unrestricted functions of lists of past offers. The play uses the first accepted offer, with period number one greater than its zero-based sequence index. A subgame after a rejected history restarts the period count and swaps the opening role when the history has odd length. The perfect-equilibrium predicate includes the empty history; acceptance comparisons use period 0 for the offer already on the table.
The threshold correspondence uses actual least and greatest elements among partitions in . No real infimum or supremum supplies a default for an empty candidate set. “Closed interval” in the goal means an explicit with . “” is the image of under . Proposition 3's “parallel line segment” is the full image of a nonempty interval under . These readings exclude a vacuous equilibrium set, a disagreement-to-zero coercion, and a hard-coded discounting special case.
The common outcome and preference definitions, the history-based strategy and play, and the equilibrium predicate are reusable for other alternating-offer questions. Contributions toward their structural properties, the numbered milestones, and the full theorem are in scope. The two displayed claims inside proofs and the fixed-cost and discounting conclusions are deferred to keep this proposal on the theorem's numbered path. Existing platform entries on Nash's axiomatic bargaining solution and a sealed-offer double auction concern different objects; neither supplies this game's equilibrium definition.
Large scale unconstrained optimization often makes an exact Newton step expensive. At each iterate, Newton's method asks for a solution of a linear system involving the Hessian, and the cost of solving that system can dominate the cost of evaluating the objective. Dembo and Steihaug's 1983 truncated Newton method uses conjugate gradients to stop the linear solve early, either when the residual is small enough or when the current direction has insufficient positive curvature. The resulting direction is paired with a line search. The question for this mission is whether those early exits still give a globally reliable optimization method under the paper's assumptions. The answer, in Theorem 2.1, is that every resulting run has gradient norm tending to zero, and a positive definite Hessian at one limit point makes the whole sequence converge to that point.
The objective is a twice continuously differentiable function . Write for its gradient and for its Hessian. For every initial point , the paper assumes that the sublevel set is bounded. The formalization uses the Euclidean norm and its inner product, so the operator norm of is also Euclidean.
At a major iterate , the minor conjugate-gradient iteration starts at with residual and direction . It maintains a scalar , initialized to , alongside the usual conjugate-gradient state. Before taking its next conjugate-gradient step, it checks whether . If so, it returns when and the current approximation otherwise. If this first test fails, it takes a conjugate-gradient step and checks whether . If so, it returns . A TNCG direction is the direction returned by the first exit that occurs. The forcing value sets the residual tolerance.
The major iteration chooses a positive step length . With the minor iteration's output and , , the line search requires both sufficient decrease and a curvature condition:
The update is . A run is a sequence satisfying this rule from its specified starting point. The paper also states an alternative function-value curvature condition; this mission defines it because the local unit-step theorem discusses both choices, although the main run uses the displayed gradient condition.
For every starting point there is a TNCG run, and every run satisfies
If is a limit point of that run and is positive definite, then
The existence clause is the formal meaning of the paper's assertion that the iterates are well defined. The six milestones follow the paper's appendix: the conjugate-gradient relations of Theorem A.1; the uniform descent and direction bounds of Lemma A.2; the line-search existence and directional-derivative limit used in the proof of Theorem A.3; Theorem A.3 itself; and eventual unit-step admissibility in Theorem A.4. The companion Theorem 2.2 addresses the eventual residual exit and unit-step behavior when a run converges to a point with positive definite Hessian. These results are all stated in the original paper.
The target shows that the computational shortcut in the inner linear solve preserves a global first-order guarantee: no TNCG run can maintain a gradient norm bounded away from zero. It also identifies when the sequence has one limit, rather than merely having stationary accumulation points. The local companion result describes the regime where the truncated method can take full steps and the residual stopping test governs the minor iteration.
The mathematical results are proved in the 1983 paper, while this mission's Lean statements are open proof targets. A complete formalization would connect the finite-dimensional conjugate-gradient recurrence, the line-search argument on bounded sublevel sets, and the convergence statement in one machine-checked development. The conjugate-gradient identities and line-search facts could be reused in other optimization algorithms; the exact first-exit model and the global conclusion are specific to this method.
The minor iteration is not an ordinary positive definite conjugate-gradient solve. The Hessian may be indefinite away from a solution, and the iteration must stop at insufficient curvature before using a later residual state. A convergence argument that assumes positive definiteness at every iterate would therefore miss the case the algorithm was designed to handle. The line search must work for the returned direction, including the first iteration's steepest-descent fallback. The limit-point conclusion adds a separate issue: a vanishing gradient norm alone does not force an entire sequence to converge to a chosen limit point.
Lean represents as EuclideanSpace ℝ (Fin n), uses its Euclidean norm and inner product, and defines as the derivative of the gradient. The objective is and every sublevel set is bounded, as specified at the start of the paper. The TNCG recurrence is total, but an admissible direction must come from its first actual exit, with the curvature test preceding the residual test. At , the curvature exit returns , not the zero initial approximation. This prevents a false stationary run. The residual test is written as a product inequality, equivalent to the paper's quotient when the residual test is reached.
Step lengths are positive. A run is extended through stationary points by zero directions, giving an infinite sequence on which a limit can be stated. Theorem 2.1 imposes no extra restriction on the forcing sequence and no upper bound on step lengths. Theorem A.1 corrects the printed Krylov-space index from to . Theorem A.4 adds , needed for the conclusion and true in the paper's applications. Theorem 2.2 requires nonnegative forcing values and guards its residual-exit conclusion at stationary iterates. These corrections are recorded item by item in the moderation notes. Contributions to the conjugate-gradient identities, bounded-level-set line search, and isolated-limit-point argument are all within scope.
Truncated-Newton methods minimize a smooth function by taking, at each iterate , a search direction obtained by solving the Newton equation only approximately, with the linear conjugate gradient (CG) method. Here is the gradient and the Hessian of . The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).
Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of .
Fix a symmetric linear operator on , with the Euclidean inner product and norm , and a vector . In the paper these are and at the current iterate.
The TNCG minor iteration (p. 194) runs CG on from . Its state at iteration is :
and, writing ,
At iteration the method first applies the curvature test (2.1), , and stops if it holds; otherwise it computes and applies the truncation test (2.2), , and stops if it holds. With , (2.1) reads and (2.2) reads . The method exits through (2.1) at when no test fired at any iteration and (2.1) holds at .
For the eigenspace is (A.21). The span of vectors is written ; the Krylov space of is .
Let . If is not positive definite, then either the minor iteration exits through (2.1) at some iteration , so that
or
The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if and the method terminates through (2.2), then, outside this rare case, is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.
The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.
The CG relations of Theorem A.1 are usually proved for positive definite , where every denominator is positive. Here is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with " to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of , so one must relate that space to the eigenspaces that meets, using symmetry of and a count of distinct eigenvalues. A direct argument via "the directions span " fails, because when misses an eigenspace the Krylov space is a proper subspace.
is EuclideanSpace ℝ (Fin n); is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's is a Hessian. Positive definiteness is for all . The CG recursion is total and carries no stopping test; division by zero returns in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form .
Theorem 2.4 is stated for an arbitrary symmetric and vector rather than at an iterate of a run of the full algorithm. It uses nothing else about or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints as the last Krylov vector; the correct is used.
A trivializing formalization exists and is ruled out: the first alternative is not " for some " over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with ); it requires that iteration is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.
A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.
Minimizing a smooth function subject to simple bounds on the variables, , is one of the most common problems in nonlinear optimization: it arises on its own (nonnegativity constraints, box-constrained least squares, parameter estimation with physical ranges) and as the subproblem of augmented Lagrangian and penalty methods. The classical approaches are active-set methods, which follow the boundary of the box and must guess which bounds are tight, and projected-gradient methods, which project trial points onto the box.
Coleman and Li proposed an alternative that never touches the boundary: an interior-reflective Newton method. Every iterate is strictly feasible; a new affine scaling measures how far each variable is from the bound its gradient points toward; and the line search follows a reflective path, which bounces off the faces of the box instead of stopping at them or being projected back. The method is the basis of the trust-region-reflective algorithm in MATLAB's Optimization Toolbox (fmincon, lsqnonlin), so its convergence theory underlies a widely used solver.
Timeline:
This mission is the first of two drawn from the 1994 paper; the second treats the local quadratic rate.
The problem (1.1) is
with , , . The feasible box is and its strict interior is . Write and , and , along a sequence.
The standing assumption (p. 191): for the starting point , the level set is compact, and is twice continuously differentiable on an open set .
The scaling vector (Definition 2) has components if and ; if and ; if and ; if and . The scaling matrix is , and . The system is equivalent to the first-order optimality conditions of (1.1).
The reflective transformation (Fig. 6) folds onto coordinate by coordinate: a coordinate with one finite bound is reflected about it, and a coordinate with two finite bounds is folded periodically (a triangle wave between and ). The reflective path from in the direction is : it moves along and reverses the corresponding component of the direction whenever it meets a face. A breakpoint is a stepsize at which the path lies on the boundary.
The interior-reflective algorithm (Fig. 9), with and , starts at ; at each step it chooses a descent direction and a stepsize that is not a breakpoint and satisfies
and either
or ; then .
The directions are constraint-compatible (Definition 3) if is bounded, and consistent (Definition 4) if implies .
If is generated by the algorithm of Fig. 9 and is both consistent and constraint-compatible, then
No constants are involved; the statement is the paper's.
Companion results: Theorem 2 (the acceptable stepsize interval exists, so the algorithm is well defined), and Theorems 5 (1)–(2) and 6 (1)–(2) (the scaled steepest-descent directions and are constraint-compatible and consistent).
Theorem 8 is the global first-order convergence theorem of the interior-reflective approach. With Theorems 5 and 6 it shows that the simplest instance, scaled steepest descent along the reflective path, reaches first-order points from any strictly feasible start; the paper's later second-order and quadratic results for the trust-region variant are built on it. Constraint compatibility and consistency isolate exactly what a search direction must satisfy, so the theorem applies to any direction rule that can be checked against these two conditions.
The result has been proved since 1994 but, to our knowledge, not machine-checked. A formalization requires a precise model of the reflective path, which the paper describes by an algorithm (Fig. 4) and a coordinate formula (Fig. 6), and a careful treatment of points where the scaling degenerates. The formal statements also make explicit a point the printed text leaves loose: Lemma 7 is printed as an equality but only an inequality holds, and only the inequality is used.
The argument has the shape of a standard sufficient-decrease proof, but the step that is routine for straight-line searches fails here. The path is not a line: as grows, components of the direction are reversed at breakpoints, so is not in general, since a reflected component changes the linear term by an amount of order . Lemma 7 must show that, for constraint-compatible directions, only components whose reflection decreases the linear term can be reflected at small steps, and the Taylor remainders must be controlled uniformly over a run, on a neighbourhood of the compact level set inside the open set where is . The scaling also degenerates at the boundary, where vanishes; the iterates must be kept strictly interior for to be meaningful.
Points are EuclideanSpace ℝ (Fin n); the bounds are EReal vectors with , and . The box and the level set are the published LewisTorczon.BoundPS.box and levelSet. The gradient is Mathlib's gradient, and is the inner product of the derivative of the gradient map applied to with . is never formed as a matrix: , , and are written componentwise. The reflective path is with the transformation of Fig. 6, which the paper describes as the same method as Fig. 4 in another notation (p. 199); "not a breakpoint" is the requirement that the new iterate be interior. Descent direction is footnote 3's: strict decrease along the path for all small . Sequences start at index 0, which is the paper's . The standing compactness and smoothness assumption is carried as explicit hypotheses.
The goal does not assume , , or anything about breakpoints; a version of Theorem 8 that did, or one whose algorithm projected onto the box instead of reflecting, or whose run predicate no sequence can satisfy, would not be the paper's theorem. Lemma 7 keeps the paper's assumption and records the one-sided upper bound established by its proof. Theorem 3 uses the breakpoint distance in the direction of motion and applies its bound when that distance equals .
A complete development needs Taylor's theorem with uniform remainder along piecewise linear paths in a box, and basic facts about the reflection (it maps into , is the identity on , and is continuous). These are reusable for any reflective or projected line search. Proofs of the milestones in any order are welcome, as are independent proofs of the companion results.
A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.
Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.
A partially observed stationary Markov decision process has a finite state set , a partition of , and an initial state . For a state write for the set containing it. Each set carries a nonempty finite set of decisions; decision costs and moves a current state to the next state with probability . The controller sees only the sequence of sets visited, so a policy maps each observation sequence to a decision in . For a horizon , the expected cost of is
and the optimal cost is .
A quantified Boolean formula is with each and a conjunction of clauses , each a set of literals or . It is true if there is a value of such that for all values of , and so on, comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).
From a formula with clauses the paper builds a process : an initial state, six states per clause and variable , end states , and one absorbing state, so . The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, , is paid at . The horizon is .
For every formula in the paper's QSAT class (an alternating prefix beginning with and ending with , and three literals per clause), with clauses and ,
The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).
Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.
The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.
The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets and differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.
The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories of their probability times , and the optimum is the infimum over all policies. Paper clause and variable are Lean indices and .
Choices made explicit:
QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix with even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. is also a hypothesis.Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.
Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).
The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.
A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.
This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.
Let be a finite set of states and the initial state. At each there is a finite, nonempty decision set . A decision has a real cost and moves the process with certainty to . All of these data are stationary: they do not change with time. A policy chooses a decision for each state and each time . It generates a trajectory by . The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.
The paper prints the finite average with cost terms and denominator :
A time-dependent policy's averages may fail to converge. We use the upper limit and optimize over all policies, . A state is reachable if some finite walk of decision arcs goes from to . A simple cycle is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is . A loop is a one-arc simple cycle.
For states , the min-plus adjacency entry is the least cost of a decision arc from to , or when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus represents the least cost of a -arc walk from to , when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.
The first target identifies the value of the original policy optimization problem:
It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with , so it applies even when a policy's averages oscillate.
The second target identifies the finite graph calculation used in the paper:
The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from through recover the least simple-cycle mean. The restriction to reachable is essential: a cheap cycle in a disconnected component cannot be used from .
The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.
Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.
An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.
Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once is supplied. Policy time starts at zero. The printed terms divided by are retained; Lean's quotient is zero and has no effect on the limit. The optimum is the infimum over all policies , not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.
The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.
Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.
The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).
A circuit is a finite sequence of triples with . Each is one of the operations false, true, and, or. A triple with is an input; a triple with is a gate, and a gate reads two earlier triples, . The value of an input is its constant; the value of a gate is the Boolean operation applied to the values of triples and . The value of is the value of triple .
A finite Markov decision process has a finite state set , an initial state , and at each state a nonempty finite set of decisions. Taking decision at state at time costs and moves to with probability . A policy chooses a decision for every state and time. For a horizon the expected cost of is
and the optimal expected cost is over all policies.
From a circuit the proof of Theorem 1 builds a stationary process : one state per triple plus an absorbing state . An input state has one decision, moving to , at cost if the input is false and if it is true. An or gate has two free decisions, moving to and moving to . An and gate has one decision, moving to or with probability each. All other costs are zero. The initial state is triple and the horizon is .
In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.
for every circuit with triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of was true" on p. 445.
The discounted analogue, which the paper asserts in one sentence: for , the optimal expected discounted cost of is at most iff is true (discounted_reduction).
Combined with the log-space computability of from , the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.
The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.
The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.
Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.
Conventions committed to:
Fin k (paper index is Lean index ); via [NeZero k]. The fields of an input are unused (the paper sets them to , not a triple index). Triple need not be a gate.Option (Fin k), with none the state ; decisions are Fin 2 at or gates and Fin 1 elsewhere.A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.
Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time ) that are reusable for any finite-horizon process.
Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon much larger than the state set, so a method that processes all stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)
The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447
Let be a finite nonempty set of states, with , and fix an initial state . At each state , a finite nonempty set contains the available decisions. A decision has a certain successor state and a real cost . The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445
A policy is a function of both state and time. Starting at , it produces . In the convention of the paragraph before Theorem 5, horizon means decisions and therefore a walk with arcs. Its cost is
A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.
The first milestone identifies with the minimum cost of a -arc walk from . The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447
For and , let be the cheapest -arc walk from that visits . Let be the cheapest closed -arc walk at . Only choices for which these walks exist are included. The mission's goal is
The bound is the paper's finite compression claim. The divisibility condition makes an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447
The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than arcs and closed walks of at most arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447
The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.
The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447
Lean represents and each as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an -arc walk has states at indices .
The paper's general finite-horizon definition sums costs from through , while the Theorem 5 paragraph explicitly asks for a -arc walk. This mission follows the latter convention: decisions occur at . The goal also imposes , which the printed loop leaves implicit, and uses a closed walk for because that is what the length- graph calculation computes. It does not assume distinct walk costs. The condition is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447
Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.
Minimum makespan scheduling on unrelated parallel machines, written , is one of the basic models of scheduling theory: jobs must each be run on one of machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than unless (their Corollary 2).
The two bounds have stood for more than three decades. Closing the gap between and for is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of is the subject of this mission.
Timeline:
3-dimensional matching. There are three disjoint sets , , and a family of triples, each with one element of , one of and one of . A matching is a subfamily with whose union is . In Lean an instance is a map , and HasMatching T says that a matching exists.
The scheduling model. Machines are , jobs are , and is the positive integer processing time of job on machine . A schedule assigns each job to one machine; the load of machine is and the makespan is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.
The instance of Theorem 5. The triples containing are the triples of type ; let be their number. From the paper builds a scheduling instance with machines, machine corresponding to , and with
If , machine processes the element jobs of and in time , each dummy job of type in time , and every other job in time . In Lean the processing-time matrix is P T.
A -approximate schedule of an instance is a schedule with for every schedule of the same instance.
For every instance , every , and every -approximate schedule of the instance of Theorem 5 built from ,
This is the mathematical content of "for every there is no polynomial -approximation algorithm unless ": a -approximate answer on the reduced instance decides 3-dimensional matching.
For every instance ,
The result. Theorem 5 shows that is NP-hard already when every processing time lies in and the target makespan is . Corollary 2 turns this into the best known inapproximability bound for the problem, , which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.
Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the gap in one formal library.
The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold depends on the strict inequality ; at the statement is no longer implied by Theorem 5.
Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of triple indices covering every , , (the covering form of the paper's definition, which forces disjointness).MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.In 1955 Charnes, Cooper and Ferguson proposed to estimate the weights of an executive compensation scheme by linear programming instead of least squares: the weights minimise a sum of absolute deviations subject to ranking, ceiling and floor constraints, which is a linear program. The coefficients of that program are not known exactly. They are averages of ratings collected from a sample of job holders, so the program actually solved is a random perturbation of a "true" program built from population means. The Appendix of the paper (§8, Consistency of Estimates) asks the basic statistical question about such an estimator: as the sample grows, does the optimal solution of the sample program converge to the optimal solution of the true program?
The question is not specific to compensation. Whenever the constraint matrix of a linear program is estimated from data, the computed optimum is an estimator, and its consistency is the first property one wants. The Appendix is one of the earliest statements of this kind for linear programming, written at a time when the simplex method itself was only a few years old (Dantzig 1951).
Fix integers (the number of constraints, indexed by ) and (the number of variables, indexed by ), a right-hand side and a cost vector . For a real matrix consider the linear program (8)
Its feasible set is a polyhedron in , and a minimizing solution is a feasible point at which the objective is no larger than at any other feasible point.
The true matrix collects population means. For each sample size the observed matrix is
where the sampling errors are random variables on a probability space with in probability as .
The paper makes two assumptions about the true program:
A feasible point is nondegenerate if the number of strictly positive variables plus the number of constraints with strictly positive surplus equals . At an extreme point this means that the basis of the point, after adding one surplus variable per constraint, consists of strictly positive basic variables.
Under (I), (II) and nondegeneracy of , for every ,
The event asserts that the sample minimiser exists and is unique, as the paper's phrase "the minimizing solution of (8), " presupposes, and that it is close to .
A companion item records that the claim as printed, under (I) and (II) alone, is false.
The theorem says that the linear programming estimator of the paper is consistent: with enough data, the computed weights are, with high probability, the unique optimum of the sample program and close to the true weights. More generally it is a stability statement for linear programs with a unique nondegenerate optimum under perturbation of the constraint matrix, which is the setting of sensitivity analysis and of sample-average approximation for linear programs.
The paper gives a sketch, not a complete proof. Its argument transfers extreme points of the true polyhedron to the sample polyhedron and compares objective values. That transfer is valid at nondegenerate extreme points only, and the claim as printed fails without such a condition: for and the true feasible set is the single point , so (I) holds, the two columns are independent, so (II) holds, yet replacing by any value in makes the program infeasible. The mission therefore adds one disclosed hypothesis, nondegeneracy of the true optimum , and keeps everything else as on the page. To the best of the curators' knowledge, neither the paper's statement nor the repaired one has been machine-checked; this mission formalizes the repaired theorem, the steps of the paper's argument, and the counterexample to the printed statement.
The natural first idea is that the feasible set and the optimum move continuously with the data. That is false in general: a polyhedron defined by perturbed inequalities can lose extreme points, gain new ones, or become empty, and the optimum of a linear program is not a continuous function of the constraint matrix. The paper's claim that the sample polyhedron has "precisely the same number of extreme points as the true convex set" and that the parenthetical of claim B is preserved under small modifications both fail at degenerate extreme points. The difficulty is to control, near a unique nondegenerate optimum , both the feasibility of the sample program and the identity of its optimal extreme point, and to turn this into a probability statement without any measurability assumption on the estimator.
All objects live in the namespace ExecCompLP.Consistency. Matrices are Matrix (Fin m) (Fin n) ℝ with X i j the entry ; column is fun i => X i j. Indices are 0-based. Vectors are Fin n → ℝ, and distances between them use the maximum norm (dist on Fin n → ℝ); closeness of matrices is entrywise. Every norm gives the same statements.
TendstoInMeasure), which is the conclusion of (9) on p. 149 taken as a hypothesis; sample means and variances are not modelled. The probability of the goal's event is an outer measure, so no measurability of or of the estimator is assumed.A complete development needs: openness of linear independence, the inequality-form characterization of extreme points by linearly independent positive columns, continuity of basic solutions in the data, and positivity of reduced costs at a unique nondegenerate optimum. The first three are reusable for any perturbation analysis of linear programs. Proofs of any item, and alternative arguments for the goal, are welcome.
A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.
The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.
There are rated factors and job levels ordered from highest to lowest. The rating is the amount of factor required at level , and is the nonnegative weight assigned to that factor. The estimated salary at level is
The salary formula applied to a person's factor amounts is . For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each ; the top-level salary is at most the ceiling ; successive salaries descend, ; and the bottom-level salary is at least the floor . These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.
The firm specifies target salaries at a finite set of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is
The original problem minimizes over the feasible weights. At a specified level, let . The split-variable program of (4)–(5) introduces with and minimizes . The split variables are constrained only for levels in . The salary constraints (2) continue to apply to . This is the paper's transformed linear program, with a feasible set that contains many choices of above the same weight vector Charnes, Cooper and Ferguson, §§4–5.
The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:
The goal also says that minimizes exactly when the triple formed from and the positive and negative parts of minimizes . Every LP minimizer projects to a minimizer of . These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.
Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.
Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at , 10 at , and 4 at , measured in thousands of dollars. Equation (7) assigns weights , yielding the minimum deviation §7, pp. 145–148. A further companion checks the redundant ranking row.
The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.
The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.
The split-variable program permits and to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of , but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.
The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level is the final Fin L index. The assumption is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through but add no constraints to (2), matching the paper's treatment of .
A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of . The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.
The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.
Minimum makespan scheduling on unrelated parallel machines asks for an assignment of jobs to machines, where job takes time units on machine , so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is . It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for and showed that no polynomial algorithm achieves a ratio below unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:
Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case , from 3-dimensional matching to -dimensional matching.
Machines are indexed by and jobs by . A schedule assigns every job to exactly one machine. The load of machine is , and the makespan is the largest load.
-dimensional matching. An instance is a ground set of elements and a family of -element subsets of . A matching is a subfamily with and ; its members are then pairwise disjoint.
The instance of Theorem 7. Fix natural numbers that are relatively prime. Build a scheduling instance with machines, machine corresponding to , and two kinds of jobs:
Every processing time lies in .
The instance of Theorem 4. For disjoint sets , , of the same size and triples , , there are element jobs, one per element of , and dummy jobs. Machine processes the element jobs of , , in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of triples covering .
For relatively prime and a family of -subsets of a -element set, the instance above has all processing times in , and
The result. Theorems 6 and 7 together say exactly which two-valued restrictions of are tractable. Up to scaling, the polynomial case is , and every other pair with is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial -approximation with exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.
Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a -dimensional matching definition over an arbitrary family of -sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.
The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most may a priori place an element job on a machine whose tuple does not contain it, at length , and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below . What excludes them is a property of the whole schedule together with the arithmetic of and . The hypotheses are sharp for this step: for element jobs are cheaper on foreign machines, and for a load with becomes possible.
Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to . The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The -partite structure of -dimensional matching is not imposed: the reduction does not use it, and statements over all families of -sets contain the -partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when ), which are reusable across scheduling reductions.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.
In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.
The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor . When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio .
Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on . Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio , but not by a polynomial algorithm for varying ; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.
Work in with the Euclidean length , and write for the closed ball. For points , the simplex volume is
where has column vectors .
Let be convex, and let with linearly independent. Choose linear functions with
Thus measures the height above the facet opposite . The stopping condition of the second stage is
The ratio is the factor by which the volume changes when is replaced by , so (16) says that no such swap enlarges the simplex by more than .
Let be a nonsingular linear map of such that span a regular simplex, meaning that all distances , , are equal. Let be its centroid and its convex hull. For , the paper defines
The proof of the LEMMA works in model coordinates. There is the hyperplane of , the are the standard basis vectors, , and .
Under (15) and (16), with making the simplex regular and its centroid, there are positive reals with
These are conditions (3)–(4) of §1 with .
The paper's own proof derives the goal from milestone 1 and the LEMMA at . At the constant cannot be improved by this argument.
The result. The theorem is the only place in the paper where the roundness constant is computed, and enters the bound on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of to obtain ( even) and ( odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume- neighbourhood" of a regular simplex extends.
The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor , by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.
There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map . The second is the transfer to the model. The paper's "similarity transformation" identifies with a hyperplane of and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and must all be carried across this isometry up to scaling. The LEMMA is stated in , not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.
EuclideanSpace ℝ (Fin n) and the model is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching .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.