Optimization

Burn-in ovens as batch processing machines

In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.

This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time $0$ and processing times and due dates are agreeable. That is the problem the paper writes $1/B/T_{\max}$. The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a $T_{\max}$ minimizer.

The batch machine

There are $n$ jobs $1,\dots,n$. Job $i$ has a processing time $p_i$ and a due date $d_i$, both natural numbers. The machine has capacity $B\ge 1$. A batch is a nonempty set of at most $B$ jobs processed together. It occupies the machine for the processing time of its longest job,

$$t(P)=\max_{i\in P}p_i .$$

A batch schedule of a job set $J$ is a sequence $S=(P_1,\dots,P_m)$ of pairwise disjoint batches covering $J$, processed in this order and back to back from time $0$. Batch $P_k$ and all of its jobs complete at $C(P_k)=t(P_1)+\dots+t(P_k)$. The makespan is $C_{\max}(S)=C(P_m)$, and the maximum tardiness is

$$T_{\max}(S)=\max_k\max_{i\in P_k}\max\{0,\,C(P_k)-d_i\}.$$

A schedule is feasible when $T_{\max}(S)=0$, that is, when every job meets its due date.

A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if $p_i<p_j$ implies $d_i\le d_j$. A schedule is consecutive when every batch is a block $\{i,i+1,\dots,k\}$ of indices and the blocks appear in increasing order.

Algorithm DP2 computes values $f(0),\dots,f(n)\in\mathbb N\cup\{\infty\}$:

$$f(0)=0,\qquad f(j)=\min_{\max\{1,\,j-B+1\}\le i\le j} f_i(j),\qquad f_i(j)=\begin{cases}f(i-1)+p_j,& f(i-1)+p_j\le d_i,\\ \infty,&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: correctness of DP2

Index the jobs so that $d_1\le\dots\le d_n$ and $p_1\le\dots\le p_n$. Then for every $0\le j\le n$,

$$f(j)=\min\{\,C_{\max}(S) : S \text{ a batch schedule of jobs } 1,\dots,j,\ T_{\max}(S)=0\,\},$$

with $\min\emptyset=\infty$. The minimum ranges over all schedules: any batching, any order. This is the paper's reading of $f(j)$ as "the minimum completion time of jobs $1,\dots,j$ if they can be scheduled feasibly, and infinity otherwise".

Milestones

1. Lemma 3. With agreeable processing times and due dates, if a feasible schedule exists, then a feasible schedule in batch-EDD order exists.
2. Consecutive partition (justification of DP2). Under the index order above, if jobs $1,\dots,j$ can be scheduled feasibly, then some feasible schedule of minimum makespan is consecutive.
3. FBEDD. With equal processing times and due dates in index order, the Full-Batch EDD schedule $\{1,\dots,B\},\{B+1,\dots,2B\},\dots$ has $T_{\max}$ no larger than that of any batch schedule.

Significance

DP2 is the paper's feasibility test for $1/B/T_{\max}$ with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing $T_{\max}$. A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.

No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.

Difficulty

The recursion charges $p_j$ for the last batch $\{i,\dots,j\}$ and checks only $d_i$. Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for $B=2$, $p=(3,1)$, $d=(5,5)$ it gives $f(2)=1$, while every schedule takes at least $3$. The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.

Formalization scope

• Jobs are Fin n (job $i$ of the paper is index $i-1$); jobs $1,\dots,j$ are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).
• A schedule is a List (Finset (Fin n)); validity requires nonempty batches of size at most $B$ inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.
• $\infty$ is ⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.
• Explicit readings of loose phrases:
  • "jobs are indexed in increasing order of due dates" (p. 767) becomes Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;
  • "agreeable" (printed "$p_i\le p_j$ implies $d_i\le d_j$", which would force equal due dates for equal processing times) becomes the strict form $p_i<p_j\Rightarrow d_i\le d_j$, a weaker hypothesis;
  • "optimally solves" for FBEDD becomes "valid, and $T_{\max}$ at most that of every valid schedule";
  • "a consecutive partition problem" becomes the existence of a consecutive minimum-makespan feasible schedule.
• Not formalized: the $O(nB)$ and $O[nB\log_2(np_{\max})]$ running times, the bisection procedure, and the remark that $np_{\max}$ bounds $T_{\max}$.
• Trivializations ruled out: the goal's minimum ranges over all valid schedules, not only batch-EDD or consecutive ones (which would assume the milestones), and DP2 is the printed recursion, not a restatement of the optimum.
• Infrastructure needed: list-indexed schedules, exchange arguments on adjacent batches, and induction on prefix length for the recursion. The single-machine batch model is shared in spirit with missions 1 and 3 of this series. No published platform definition was reused, since nothing on batch machines exists yet.

Selected references

• C.-Y. Lee, R. Uzsoy, L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 764–775, 1992. https://doi.org/10.1287/opre.40.4.764
• Y. Ikura, M. Gimple, Efficient scheduling algorithms for a single batch processing machine, Operations Research Letters 5(2), 61–65, 1986. https://doi.org/10.1016/0167-6377(86)90104-5
• C. N. Potts, M. Y. Kovalyov, Scheduling with batching: A review, European Journal of Operational Research 120(2), 228–249, 2000. https://doi.org/10.1016/S0377-2217(99)00153-8

Motivation

Minimizing the weighted number of tardy jobs on a single machine, written $1\|\sum w_jU_j$ in later scheduling notation, is one of the basic due-date objectives: each job either meets its deadline or pays a fixed penalty, and the question is which jobs to sacrifice. Moore (Management Sci. 15, 1968) solved the unweighted case $p_j = 1$ with a greedy procedure. Lawler and Moore (Management Sci. 16, 1969) handled arbitrary weights by recasting the problem as a knapsack problem with nested prefix constraints and solving it by a recursion, their Equation (3). This is the classical pseudo-polynomial algorithm for the weighted problem; Lenstra, Rinnooy Kan and Brucker (Ann. Discrete Math. 1, 1977) showed that the weighted problem is NP-hard, so a pseudo-polynomial method is the expected kind of exact algorithm.

The paper's Sections 5 and 6 state the reduction in a few sentences: on-time jobs can be taken in deadline order, the problem is "equivalent" to the prefix-constrained knapsack, and (3) solves the latter. This mission turns those sentences into precise statements.

Setting

There are $n \ge 1$ jobs, processed by a single machine one immediately following the other from time $0$. Job $j$ has a nonnegative integer processing time $a'_j$, a nonnegative integer deadline $d_j$ and a penalty $p_j \ge 0$. A sequence $\sigma$ is an ordering of all jobs; job $j$ completes at time $C_j(\sigma)$, the total processing time of job $j$ and the jobs before it. Job $j$ is tardy in $\sigma$ if $C_j(\sigma) > d_j$, and the total loss of $\sigma$ is

$$W(\sigma) = \sum_{j \text{ tardy in } \sigma} p_j ,$$

the loss $c_j(t)$ being $0$ for $t \le d_j$ and $p_j$ for $t > d_j$.

The jobs are numbered by deadline, $d_1 \le d_2 \le \cdots \le d_n$. A 0–1 vector $x$ ($x_j = 1$: job $j$ on time; $x_j = 0$: tardy) is prefix-feasible if

$$a'_1x_1 + \cdots + a'_kx_k \le d_k \qquad (k = 1, \dots, n).$$

Equation (3) defines $f(j,t)$ for $j = 0, \dots, n$ and integer $t$:

$$f(j,t) = \begin{cases}\max\{f(j,t-1),\ f(j-1,t),\ p_j + f(j-1,t-a'_j)\}, & 0 \le t \le d_j,\\ f(j, d_j), & t > d_j,\end{cases}$$

with $f(0,t) = 0$ for $t \ge 0$ and $f(j,t) = -\infty$ for $t < 0$.

Formalization targets

Goal: the minimum weighted number of tardy jobs

With $d_1 \le \cdots \le d_n$ and $p_j \ge 0$, $f(n, d_n)$ is finite and

$$\min_{\sigma} W(\sigma) = \sum_{j=1}^n p_j - f(n, d_n).$$

This is the paper's claim that the problem "is solved by" its recursion, with the evaluation point made explicit.

Milestones (Section 5, Section 6, Eq. (3))

1. Section 5. For any sequence, the on-time jobs, sequenced in order of their deadlines and followed by the tardy jobs in arbitrary order, stay on time, and the total loss does not increase.
2. Section 6. Every sequence has a prefix-feasible $x$ with $\sum p_j - \sum p_jx_j \le W(\sigma)$, and every prefix-feasible $x$ has a sequence with $W(\sigma) \le \sum p_j - \sum p_jx_j$: the two problems have the same optimal value.
3. Eq. (3). For $0 \le j \le n$ and $t \ge 0$,

$$f(j,t) = \max\Bigl\{\textstyle\sum_{i \le j} p_ix_i : \sum_{i\le k} a'_ix_i \le d_k\ (k \le j),\ \sum_{i\le j} a'_ix_i \le t\Bigr\}.$$

The goal follows from milestones 2 and 3 at $j = n$, $t = d_n$.

Significance

The result is the exact algorithm for $1\|\sum w_jU_j$ with running time proportional to $n\,d_n$, and the reduction behind it (on-time jobs in earliest-deadline order, then a knapsack over the on-time set) is the template reused by later work on due-date objectives, including the two-agent and batching variants. The prefix-constrained knapsack itself reappears whenever a set of jobs must be feasible under nested capacity limits.

On formalization: the paper's argument is three sentences long and leaves several points implicit: the base cases of (3), the role of the deadline numbering, the sign of the penalties, and what "equivalent" means. A machine-checked development fixes each of them and yields a verified pseudo-polynomial algorithm for an NP-hard scheduling problem. To our knowledge none of these statements has a machine-checked proof; the platform's SchedComplexity.OneMachine.* items (Lenstra, Rinnooy Kan and Brucker) state the NP-hardness of the same problem in another model, MooreLateJobs.NumLate.* covers Moore's unweighted case, and TwoAgentSched.LateLate.lemma_7_1 is a two-agent analogue of milestone 1.

Difficulty

The obvious argument works with the set of on-time jobs and asserts that this set can be sequenced on time iff its earliest-deadline order is. That step is Jackson's rule, an exchange argument on lists that is not in Mathlib; it is where both milestone 1 and the first half of milestone 2 sit. The second half of milestone 2 needs the deadline numbering: for a job $k$ that is tardy, the prefix constraint at $k$ is not a completion-time constraint of any job, and only the monotonicity $d_i \le d_k$ for the last on-time job $i \le k$ bounds it. Milestone 3 is a dynamic-programming correctness proof in which the cap $f(j,t) = f(j,d_j)$ for $t > d_j$ and the $-\infty$ base cases must be tracked through a well-founded recursion on $(j, t)$.

Formalization scope

Jobs are Fin n, 0-based: Lean job $j$ is the paper's job $j+1$, and the paper's $f(j,\cdot)$ uses Lean job ⟨j-1, _⟩. Sequences are lists in the published model MooreLateJobs.Shared (IsSchedule Finset.univ l, completionTime, no idle time, start at $0$), which replaces the paper's permutation $\pi$; tardy jobs are the published MooreLateJobs.NumLate.lateSet (strictly $d_j < C_j$). Processing times and deadlines are natural numbers, penalties real. Vectors $x$ are Fin n → Bool. $f$ takes values in WithBot ℝ, with $\bot = -\infty$ and $p + \bot = \bot$; $+\infty$ never occurs.

Explicit readings of the paper's loose phrases:

• Integer data: (3) steps $t$ by $1$ and subtracts $a'_j$, so $a'_j$ and $d_j$ are nonnegative integers.
• Penalties $p_j \ge 0$ ("a penalty $p_j$ is exacted"); the goal, milestone 1 and milestone 2 assume it, milestone 3 does not need it.
• Deadline numbering ("ordering the jobs by deadlines") is Monotone d on the job index; assumed in the goal and milestone 2 only.
• Base cases of (3) are those of Equation (1), with $-\infty$ for a maximum: $f(0,t) = 0$ ($t \ge 0$), $f(j,t) = -\infty$ ($t < 0$). The dominated term $f(j,t-1)$ is kept as printed.
• "Equivalent" is the pair of inequalities of milestone 2, i.e. equal optimal values.
• "Solved by" means $f(n,d_n)$ is finite and $\sum p_j - f(n,d_n)$ is the least weighted number of tardy jobs (IsLeast over all schedules); $n \ge 1$ only so that $d_n$ exists.
• "Arbitrary order" of the tardy jobs in milestone 1 is a universal quantifier over the remaining lists.

Section 5 literally applies Equation (1) with $a_j = a'_j$, $\alpha_j(t) = 0$, $b_j = 0$, $\beta_j(t) = p_j$; read literally, that leaves the deadlines unenforced, so the mission formalizes the paper's own corrected form (3) instead. Trivializing formalizations are ruled out: the weighted number of tardy jobs is defined from completion times, not through $x$; the optimum is a minimum over sequences, not defined as $f$; (3) keeps its cap $f(j,t) = f(j,d_j)$; the goal assumes $p_j \ge 0$ and sorted deadlines, without which it is false.

Infrastructure: an exchange lemma for earliest-deadline order on lists (Jackson's rule, posed on the platform as MooreLateJobs.NumLate.jackson) and well-founded-recursion lemmas for WithBot ℝ maxima are reusable beyond this mission. Proofs of any milestone, and of Jackson's rule, are welcome.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1), 1969, 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Tardy Jobs, Management Science 15(1), 1968, 102–109. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 1977, 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$. Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$. A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$, one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$. Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$.

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$, job $i$ must precede job $j$; such a $j$ is a successor of $i$, and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$.

For a number $\varepsilon$ the modified deadline of job $j$ is

$$\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,$$

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$.

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

$$\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .$$

Milestones (from §2 and the proof of the Theorem, p. 78)

1. For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$.
2. The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
3. If $\bar d_j < \bar d_i$, then $j$ or some successor $k$ of $j$ has $d_k \le d_i$.
4. In an on-time sequence consistent with $\rho$, two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$.

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$, not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ($\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$.

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$: one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$. That step uses the smallness of $\varepsilon$: with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$, $d = (7,9,8)$, $\varepsilon = 3$). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$, a bubble-sort argument over lists.

Formalization scope

• Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$, and the tie-break is $((j:\mathbb N)+1)\varepsilon$. Processing times and deadlines are real.
• Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$, no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
• The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
• Explicit readings of the paper's phrases:
  • "$\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$. A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
  • "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
  • "iρj implies $\bar d_i < \bar d_j$": stated for $i \ne j$, since $\rho$ is reflexive.
  • The pair condition "a consecutive pair with $\bar d_i > \bar d_j$" of milestone 3 is dropped, since the claim does not use it.
• Added hypothesis: $a_j \ge 0$. The paper uses it tacitly ("$j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
• The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$). The goal assumes the full partial order of the paper.
• Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
• Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

Motivation

Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve $0 = \bar f^\nu(x)$, where $\bar f^\nu$ averages a random integrand over $\nu$ observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.

When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation

$$0 \in f(z, x) + N(x),$$

where $N$ is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of $N$: the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.

Setting

Let $Z$ be a separable Banach space with norm $\|\cdot\|$, and let $|\cdot|$ be the Euclidean norm on $\mathbb R^n$ and $\mathbb R^m$. A multifunction $G : Z \rightrightarrows \mathbb R^n$ assigns a set $G(z) \subseteq \mathbb R^n$ to each $z$. Its graph is $\operatorname{gph} G$ and its inverse is $G^{-1}(x) = \{z \mid x \in G(z)\}$.

For sets $A_t$ indexed by $t \downarrow 0$, the upper limit $\limsup A_t$ consists of the points $x$ with $x = \lim x_k$, $x_k \in A_{t_k}$ for some $t_k \downarrow 0$, and the lower limit of the points reachable along every such sequence. The contingent derivative of $G$ at $(z, x) \in \operatorname{gph} G$ is the multifunction $DG(z|x)$ with

$$\operatorname{gph} DG(z|x) = \limsup_{t \downarrow 0} t^{-1}\big[\operatorname{gph} G - (z,x)\big].$$

$G$ is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when $t^{-1}[G(z + t w') - x] \to DG(z|x)(w)$ as $t \downarrow 0$ and $w' \to w$. A single-valued $g$ is B-differentiable at $z$ when $t^{-1}[g(z + tw') - g(z)] \to Dg(z)(w)$ in the same sense.

The deterministic problem is $0 \in f(z, x) + N(x)$ with $f : Z \times \mathbb R^n \to \mathbb R^m$, data $z$ and solution map $J(z)$. At a reference pair $(z^*, x^*)$ set $F = f(z^*, \cdot) + N$. The analytical assumptions M.1–M.4 are as follows. $f$ is jointly continuous and B-differentiable in each variable, with the $z$-derivative $D_z f(z^*, x^*)$ strong (uniform in $x$ near $x^*$). $N$ is closed and proto-differentiable. $F$ is subinvertible: $0 \in F(x^*)$, and a closed-graph, convex-valued selection of $F^{-1}$ near $0$ passes through $x^*$. The contingent derivative $DF^{-1}(0|x^*)$ is at most single-valued.

The statistical problem has i.i.d. random elements $s_1, s_2, \dots$ of a measurable space $S$ and an integrand $f : U \times S \to \mathbb R^m$ on a compact neighborhood $U$ of $x^*$. It satisfies the probabilistic assumptions P.1–P.4: continuity in $x$, measurability in $s$, a finite second moment at one point, and a Lipschitz bound $|f(x_1,s) - f(x_2,s)| \le a(s)|x_1 - x_2|$ with $E a(s_1)^2 < \infty$. The M-estimate $x^\nu$ is a measurable solution of

$$0 \in \bar f^\nu(x) + N(x), \qquad \bar f^\nu(x) = \frac1\nu\sum_{i=1}^\nu f(x, s_i),$$

and the true equation is $0 \in Ef(x) + N(x)$ with $F = Ef + N$.

Formalization targets

Goal: Theorem 2.7 (asymptotic distribution of M-estimates)

Under P.1–P.4 on a compact neighborhood $U$ of $x^*$, B-differentiability of $Ef$ at $x^*$, and M.2–M.4 for $F = Ef + N$, every sequence of measurable solutions $x^\nu$ of (2.5) with $x^\nu \to x^*$ almost surely satisfies

$$\sqrt\nu\,[x^\nu - x^*] \xrightarrow{\ \mathcal D\ } DF^{-1}(0|x^*)(-w^*), \qquad w^* \sim \mathcal N\big(0, \operatorname{cov} f(x^*, s_1)\big).$$

The goal fixes the limit law completely: the map is the contingent derivative of $F^{-1}$, and the Gaussian has the covariance of the integrand at $x^*$.

Milestones

• Theorem 2.4 gives bounds in probability, $P\{|x^\nu - x^*| > \delta\} \le P\{\alpha\lambda\|z^\nu - z^*\| > \delta\}$. Its proof uses the upper-Lipschitz property $U \cap F^{-1}(y) \subseteq x^* + \lambda|y|B$ (a display of the proof).
• Theorem 2.6 is the abstract limit theorem: if $\tau_\nu^{-1}[z^\nu - z^*] \to_{\mathcal D} w$, then $\tau_\nu^{-1}[x^\nu - x^*] \to_{\mathcal D} DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$. Its proof uses two displays: semi-differentiability of the localized solution map, with $DJ(z^*|x^*)(w) = DF^{-1}(0|x^*)(-D_z f(z^*,x^*)(w))$, and a Lipschitz bound $|x - x^*| \le \lambda\|z - z^*\|$ on $U \cap J(z)$.
• Proposition A1, Corollary A2 and Theorem A3 concern the space $C_m(U)$ under P.1–P.4. The integrand and the empirical means are random elements of $C_m(U)$, and $\sqrt\nu(\bar f^\nu - Ef)$ converges in distribution to a Gaussian element of $C_m(U)$.

The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.

Significance

Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When $N$ is the normal cone of a polyhedron, $DF^{-1}(0|x^*)$ is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.

The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.

Difficulty

The classical argument linearizes $F$ at $x^*$, inverts the Jacobian and applies the delta method. Here $F$ is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from $x^*$. The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.

The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function $\bar f^\nu$, so convergence of $\bar f^\nu$ at finitely many points is not enough. The central limit theorem must hold in the sup norm on $C_m(U)$, which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), and $Z$ is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ($t \downarrow 0$ is 𝓝[>] 0, and $(t,w') \to (0^+,w)$ is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. $s_1$ is s 0, empirical means sum over Finset.range ν, and (2.5) is required for $\nu \ge 1$. $F = Ef + N$ is empty off $U$. Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of $w^*$ is fixed through linear functionals: $\langle\ell, w^*\rangle \sim \mathcal N(0, \operatorname{Var}\langle\ell, f(x^*,s_1)\rangle)$. In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.

Explicit choices relative to the printed text:

1. The paper states that an almost surely convergent sequence of solutions "converges to the point $x^*$" (Theorems 2.6 and 2.7). This is false when the true equation has a second solution: $f(z,x) = x^2 - x - z$, $N \equiv \{0\}$, $z^* = x^* = 0$ satisfies M.1–M.4 with $J(0) = \{0, 1\}$. The formalization assumes $x^\nu \to x^*$ almost surely instead.
2. $0 \in F(x^*)$ (presupposed by $DF^{-1}(0|x^*)$) is explicit in Theorem 2.4 and the upper-Lipschitz display.
3. The threshold for "all sufficiently small $\delta$" in Theorem 2.4 is chosen with $U$ and $\lambda$, before the random elements.
4. Proposition A1 and Corollary A2 carry P.1–P.4, as stated or inherited on the Appendix page, though their measurability conclusions use only P.1.
5. In the limit theorems, the single-valued map $DF^{-1}(0|x^*)$ is a function $L$ whose values lie in the contingent derivative at every point.

The conclusion of the goal names its limit: the image of the stated Gaussian under a map $L$ whose values lie in the contingent derivative of $F^{-1}$. A statement asserting only that $\sqrt\nu(x^\nu - x^*)$ converges in distribution to some limit, or replacing $DF^{-1}(0|x^*)$ by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with $f(x,s) = x$, $N \equiv \{0\}$).

A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in $C(K)$ for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.

Selected references

• A. J. King and R. T. Rockafellar, Asymptotic theory for solutions in statistical estimation and stochastic programming, Mathematics of Operations Research 18(1) (1993). https://doi.org/10.1287/moor.18.1.148
• A. J. King and R. T. Rockafellar, Sensitivity analysis for nonsmooth generalized equations, Mathematical Programming 55 (1992) 193–212. https://doi.org/10.1007/BF01581199
• A. J. King, Generalized delta theorems for multivalued mappings and measurable selections, Mathematics of Operations Research 14(4) (1989) 720–736. https://doi.org/10.1287/moor.14.4.720
• J. Dupačová and R. J.-B. Wets, Asymptotic behavior of statistical estimators and of optimal solutions of stochastic optimization problems, Annals of Statistics 16(4) (1988) 1517–1549. https://doi.org/10.1214/aos/1176351052
• A. Shapiro, Asymptotic properties of statistical estimators in stochastic programming, Annals of Statistics 17(2) (1989) 841–858. https://doi.org/10.1214/aos/1176347146
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 221–233. https://projecteuclid.org/euclid.bsmsp/1200512988
• A. Araujo and E. Giné, The Central Limit Theorem for Real and Banach Valued Random Variables, Wiley, 1980.

Motivation

Many single-machine scheduling problems have a structure that is easy to describe: the jobs must be processed in an order that is already known, and the only decisions are how and when to process each one. Lawler and Moore, in A Functional Equation and Its Application to Resource Allocation and Sequencing Problems (Management Science 16(1), 1969, 77–84), isolate this situation in its simplest form: each job has two processing modes, and each mode has its own processing time and loss as a function of the completion time. They solve it with a single functional equation, Eq. (1), closely related to the recursion for the knapsack problem.

The point of the paper is that Eq. (1) solves more than this fixed-order problem. Later sections apply it to resource allocation in critical-path scheduling and to several sequencing problems with deadlines, including minimization of the weighted number of tardy jobs, often written $1\|\sum w_jU_j$. Everything in those applications rests on the claim checked in this mission: that the recursion computes the minimum loss it is said to compute.

Setting

There are $n$ jobs, performed one at a time in the fixed order $1, 2, \dots, n$. Job $j$ can be performed in one of two modes. In the first mode it takes $a_j$ time units, and a loss $\alpha_j(t)$ is incurred if it is completed at time $t$. In the other mode it takes $b_j$ time units, with loss $\beta_j(t)$. Times are nonnegative integers.

A mode assignment $m$ picks a mode for each job, which fixes its processing time $p_j \in \{a_j, b_j\}$. A feasible timing of the first $j$ jobs is a vector of completion times $c_1, \dots, c_j$ with

$$c_{i-1} + p_i \le c_i \qquad (i = 1, \dots, j), \qquad c_0 = 0,$$

so each job starts at time $0$ or later and after its predecessor has finished; idle time between jobs is allowed. The total loss $L_j(m, c)$ is the sum of $\alpha_i(c_i)$ over the jobs $i \le j$ in the first mode and of $\beta_i(c_i)$ over the others. The problem asks for the mode assignment and timing of all $n$ jobs that minimize $L_n(m, c)$.

The paper's recursion is defined for $j = 0, \dots, n$ and integer $t$, with values in $\mathbb R \cup \{+\infty\}$:

$$f(0, t) = 0 \ (t \ge 0), \qquad f(j, t) = +\infty \ (t < 0),$$ $$f(j, t) = \min\{f(j, t-1),\ \alpha_j(t) + f(j-1, t-a_j),\ \beta_j(t) + f(j-1, t-b_j)\} \quad (j \ge 1,\ t \ge 0). \tag{1}$$

Formalization targets

Milestone: Eq. (1) computes the constrained minimum

For $0 \le j \le n$ and every integer $t$, let $\mathcal L(j, t)$ be the set of total losses of the first $j$ jobs over all mode assignments and feasible timings with $c_j \le t$. Then

$$f(j, t) = \min \mathcal L(j, t),$$

meaning: $f(j, t) = +\infty$ exactly when $\mathcal L(j, t)$ is empty, and otherwise $f(j,t)$ is an element of $\mathcal L(j,t)$ and a lower bound for it. No assumption is made on the losses.

Goal: $f(n, T)$ solves the problem

If every $\alpha_j$ and $\beta_j$ is monotone nondecreasing and

$$T = \sum_{j=1}^n \max\{a_j, b_j\},$$

then $f(n, T)$ is finite and equals the minimum of $L_n(m, c)$ over all mode assignments and all feasible timings of the $n$ jobs, with no deadline. This is the paper's sentence "The problem is solved by the calculation of $f(n, T)$, where $T$ is a sufficiently large number. For example, if all of the $\alpha_j$'s and $\beta_j$'s are monotone nondecreasing, we may choose $T = \sum_{j=1}^n \max\{a_j, b_j\}$."

Significance

The milestone is the correctness of a dynamic program: the value table computed by (1) coincides with the optimum of a combinatorial problem whose feasible set is infinite (timings are unbounded because of idle time). The goal turns that into a finite certificate for the unconstrained problem, with an explicit horizon. Downstream, the same equation with $b_j = 0$ and suitable losses is the paper's algorithm for the weighted number of tardy jobs (§5–6), and the other sequencing applications are specializations of (1) as well; a formal version of this mission is the base on which those reductions can be stated.

The result is classical and its proof is short on paper. It has not been formalized: no item on Prove2Me states a two-mode fixed-order recursion. The work this mission asks for is a machine-checked proof of the two statements above, from the paper's own definitions.

Difficulty

The paper gives no argument beyond "the usual dynamic programming argumentation". The recursion is in two variables: $f(j, \cdot)$ refers to itself at $t-1$ as well as to $f(j-1, \cdot)$, so the correspondence with timings is not a plain stage-by-stage principle of optimality. The edge cases are where a careless reading fails: $t = 0$, where $f(j, -1) = +\infty$; zero processing times $a_j = 0$ or $b_j = 0$, where $f(j-1, t-a_j)$ is evaluated at the same $t$; and $j = 0$, where the deadline constraint degenerates to $0 \le t$. The goal is harder than the milestone: the problem's feasible set is unbounded, and the horizon $T$ is only sufficient under monotone losses. Without monotonicity the goal is false: one job with $a = b = 1$, $\alpha(1) = 5$, $\alpha(t) = 0$ for $t \ge 2$ and $\beta \equiv 5$ has optimum $0$, attained only at completion time $2 > T = 1$, while $f(1, 1) = 5$.

Formalization scope

• Jobs are Fin n and 0-based: Lean job i is the paper's job $i+1$. The recursion f takes the number $j \in \{0,\dots,n\}$ of jobs done; for $j > n$ its value is $+\infty$ and is never used.
• Modes are Bool, with true the first mode ($a_j$, $\alpha_j$). Processing times are natural numbers and may be $0$. Losses are real-valued functions of the natural-number completion time.
• Integer time is an explicit reading: the paper's recursion steps $t$ by one, so time is discrete.
• $+\infty$ is ⊤ : WithTop ℝ, so $x + (+\infty) = +\infty$ as in the paper.
• Idle time is allowed, and the first job starts at time $0$ or later.
• "Minimum total loss" is read as an attained least element of the set of total losses, with $+\infty$ exactly when that set is empty. "The problem is solved by $f(n, T)$" is read as: $f(n, T)$ is finite, at most every feasible total loss, and attained.
• "Monotone nondecreasing" is Monotone on the completion time; it is a hypothesis of the goal only.

The optimum is defined from the scheduling problem itself (lossesBy, IsFeasible, totalLoss), never as $f$; statements in which the optimum is $f$ again, timings forced to have no idle time, an $\mathbb R$-valued $f$ with an arbitrary value for $t < 0$, or monotone losses assumed in the milestone are all ruled out by this choice of definitions.

Related platform items: GilmoreGomory61.CuttingStock.knapsack_dp_recursion (an unbounded-knapsack recursion) and the CriticalPath.CostCurve items (Kelley's continuous time–cost model) treat neighbouring recursions and models; neither states this problem. Proofs of the milestone and the goal, and reusable lemmas about the value function, are welcome.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.1515/9781400835386
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102

Motivation

Many problems in statistics, engineering and operations research ask for the input level $x$ at which an unknown response function is largest, when the response can only be measured with noise: the dose that maximizes a yield, the setting that maximizes throughput in a simulation, the parameter that maximizes an expected reward. Robbins and Monro (1951) had shown how to find, by sequential noisy measurements, the root of an unknown increasing function. Kiefer and Wolfowitz (1952) adapted the idea to maximization: at each step, measure the response at two points $z_n\pm c_n$ placed symmetrically about the current estimate, and move the estimate in the direction of the observed difference. Their scheme is the origin of finite-difference stochastic approximation, the gradient-free ancestor of simultaneous-perturbation and zeroth-order methods in simulation optimization and machine learning.

Timeline. 1951: Robbins and Monro, root finding, convergence in mean square. 1952: Wolfowitz, convergence in probability for Robbins–Monro under weaker conditions; Kiefer and Wolfowitz, the present paper, convergence in probability of the maximization scheme. 1954: Blum proved almost-sure convergence of both schemes under related conditions (doi:10.1214/aoms/1177728794). Later work (Spall 1992, among many) extended the finite-difference idea to many dimensions.

Setting

For each level $x\in\mathbb R$, an observation taken at $x$ is a random number with distribution $H(\cdot\mid x)$; the family depends measurably on $x$. The regression function is the mean observation,

$$M(x)=\int_{-\infty}^{\infty}y\,dH(y\mid x),$$

and the observations have uniformly bounded variance: $\int (y-M(x))^2\,dH(y\mid x)\le S$ for all $x$. The function $M$ is unimodal about an unknown point $\theta$: strictly increasing for $x<\theta$ and strictly decreasing for $x>\theta$.

Two sequences of positive numbers $a_n$ (step sizes) and $c_n$ (probe widths) satisfy

$$c_n\to0,\qquad \sum a_n=\infty,\qquad \sum a_nc_n<\infty,\qquad \sum a_n^2c_n^{-2}<\infty,$$

for example $a_n=n^{-1}$, $c_n=n^{-1/3}$. Starting from an arbitrary number $z_1$, the Kiefer–Wolfowitz process is

$$z_{n+1}=z_n+a_n\,\frac{y_{2n}-y_{2n-1}}{c_n},$$

where, given everything observed so far, $y_{2n-1}$ and $y_{2n}$ are independent with laws $H(\cdot\mid z_n-c_n)$ and $H(\cdot\mid z_n+c_n)$.

The paper imposes three regularity conditions on $M$:

1. Condition 1 (Lipschitz near $\theta$): for some $\beta,B>0$, $|x'-\theta|+|x''-\theta|<\beta$ and $x'\neq x''$ imply $|M(x')-M(x'')|<B|x'-x''|$.
2. Condition 2 (bounded oscillation): for some $\rho,R>0$, $|x'-x''|<\rho$ implies $|M(x')-M(x'')|<R$.
3. Condition 3 (no flat regions away from $\theta$): for every $\delta>0$ there is $\pi(\delta)>0$ such that $|z-\theta|>\delta$ implies $|M(z+\varepsilon)-M(z-\varepsilon)|/\varepsilon>\pi(\delta)$ for all $0<\varepsilon<\delta/2$.

In the Lean development these objects are regFun H ($M$), SecondMomentBound H S, Unimodal, Cond1, Cond2, Cond3, StepSizes a c and the structure IsKWProcess, all in the namespace KieferWolfowitz.Convergence.

Formalization targets

Goal: convergence in probability

$$\text{for every }\eta>0,\qquad P\{|z_n-\theta|>\eta\}\longrightarrow 0\quad(n\to\infty).$$

This is the theorem of the paper (stated on p. 462, proved in §3 in the form (3.22)). It fixes no rate and no constants, so it is the stable form of the result.

Milestones, in the order of the paper's proof

1. (3.6) The one-step identity for $b_n=E(z_n-\theta)^2$: $b_{n+1}=b_n+2\frac{a_n}{c_n}E\,U_n(z_n)+\frac{a_n^2}{c_n^2}E(y_{2n}-y_{2n-1})^2$, with $U_n(z)=(z-\theta)(M(z+c_n)-M(z-c_n))$.
2. (3.8) $0\le U_n^+(z)<2Bc_n^2$ whenever $c_n<\frac12\beta$.
3. (3.11)–(3.12) $E\{(y_{2n}-y_{2n-1})^2\mid z_n\}\le 2S+R^2$ whenever $c_n<\rho/2$.
4. (3.15) $\sum (a_n/c_n)N_n$ converges, where $N_n=E\,U_n^-(z_n)$.
5. (3.18) $\liminf_n E\{K_n|z_n-\theta|\}=0$, with $K_n=|(M(z_n+c_n)-M(z_n-c_n))/c_n|$.
6. After (3.19) Along any $n_1<n_2<\cdots$ with $E\{K_{n_j}|z_{n_j}-\theta|\}\to0$, $z_{n_j}\to\theta$ in probability.
7. (3.28) If $N_0$ satisfies (3.25)–(3.27) for $s>0$, then $E\{(z_n-\theta)^2\mid z_{N_0}\}<(z_{N_0}-\theta)^2+s$ for all $n>N_0$.

Significance

The result shows that the maximizer of a function observable only through noise can be located consistently using function evaluations alone, without gradients and without a parametric model of $M$. The conditions are qualitative: no differentiability, no specific noise distribution, and the noise may change shape with $x$. This is the template for gradient-free stochastic optimization: simulation optimization with finite-difference gradient estimates, simultaneous-perturbation methods, and zeroth-order methods in learning are all analysed by refining the same bias–variance balance between the probe width $c_n$ and the step $a_n$.

The theorem has been proved since 1952 and is not open. To our knowledge no machine-checked proof of it exists. A formalization produces a checked proof of a founding result of stochastic approximation and, along the way, the probabilistic infrastructure such proofs share: processes defined through conditional laws given a filtration, recursions for second moments, conditional Chebyshev arguments, and the passage from subsequence convergence to full convergence by a restart bound. Alternative proofs (via supermartingale convergence, which would give almost-sure convergence under stronger hypotheses) are welcome as separate developments but are not the goal.

Difficulty

The obvious approach is to show that $E(z_n-\theta)^2$ decreases. It does not: the drift term $2\frac{a_n}{c_n}E\,U_n(z_n)$ is negative only on average and only once the probes straddle $\theta$ correctly, while the noise term $\frac{a_n^2}{c_n^2}e_n$ is always positive and the finite-difference estimate of the slope has a bias of order $c_n$. A one-step contraction is therefore unavailable, and summability arguments alone give smallness only along a subsequence; turning that into convergence of the whole sequence is where the difficulty lies, and it is also where Condition 3, which forbids flat stretches of $M$ away from $\theta$, cannot be dispensed with. The argument needs integrability of quantities the paper treats as finite without comment, and the conditional statements require the conditional law of the observation pair, not just its unconditional moments.

Formalization scope

• Observations. $H$ is a Markov kernel Kernel ℝ ℝ. Every $H(\cdot\mid x)$ has $\int y^2\,dH<\infty$, so $M$ and the variance in (2.2) are genuine integrals.
• The process. On a probability space with a filtration $(\mathcal F_n)$, $z_n$ is $\mathcal F_n$-measurable, the pair $(y_{2n-1},y_{2n})$ is $\mathcal F_{n+1}$-measurable, and $P(y_{2n-1}\in A, y_{2n}\in B\mid\mathcal F_n)=H(A\mid z_n-c_n)H(B\mid z_n+c_n)$ a.s. for all Borel $A,B$. This is the reading of "independent chance variables with respective distributions $H(y\mid z_n-c_n)$ and $H(y\mid z_n+c_n)$". The starting point $z_1$ is a deterministic number.
• Indices are 0-based: Lean's z 0 is $z_1$, a n, c n are $a_{n+1}$, $c_{n+1}$.
• Condition 1 as printed has a strict inequality that fails at $x'=x''$, which makes it unsatisfiable; the formalization adds $x'\neq x''$. Condition 3's infimum over $\frac12\delta>\varepsilon>0$ is stated pointwise, which is equivalent since $\pi(\delta)$ is existential, with $\pi(\delta)$ uniform in $z$.
• Explicit readings of loose phrases. "For $n$ sufficiently large" in (3.10)–(3.12) is the hypothesis $c_n<\rho/2$; conditioning "on $z_n$" or "on $z_{N_0}=z$" is conditioning on $\mathcal F_n$ or $\mathcal F_{N_0}$; "converges stochastically" is Mathlib's TendstoInMeasure; "$\liminf=0$" for a nonnegative sequence is "below every $\varepsilon>0$ infinitely often".
• Integrability of every expectation in a milestone is either a hypothesis or part of the conclusion, so no statement holds by Lean's convention that the integral of a non-integrable function is $0$.
• Ruled out. A formalization in which the observations are arbitrary random variables not tied to $H$, in which $\sum a_n=\infty$ is dropped, or in which $\pi(\delta)$ may depend on $z$, would make the goal false or a different theorem; the hypotheses here are jointly satisfiable (checked for $H(\cdot\mid x)=\delta_{-|x|}$, $\theta=0$, $a_n=n^{-1}$, $c_n=n^{-1/3}$).
• Not formalized. The remark on p. 463 that truncating $z_n\pm c_n$ to an interval $[C_1,C_2]$ preserves the conclusion (asserted without proof), the motivational discussion (a)–(c), and §4's further problems.
• Distinct from the Kiefer–Wolfowitz equivalence theorem of optimal experimental design (1960), which is already on the platform under BanditAlgorithm.kiefer_wolfowitz_equivalence; the two results share authors and nothing else.

Useful infrastructure, reusable beyond this mission: conditional expectations of functions of a pair with a given conditional law, tail-sum bounds, and the passage from a restart bound plus subsequence convergence in probability to full convergence. Contributions of any milestone, of intermediate lemmas such as (3.7), (3.9), (3.13) and (3.29), and of the final assembly are welcome.

Selected references

• J. Kiefer and J. Wolfowitz, Stochastic estimation of the maximum of a regression function, Ann. Math. Statist. 23 (1952), 462–466. https://doi.org/10.1214/aoms/1177729392
• H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586
• J. Wolfowitz, On the stochastic approximation method of Robbins and Monro, Ann. Math. Statist. 23 (1952), 457–461. https://doi.org/10.1214/aoms/1177729391
• J. R. Blum, Approximation methods which converge with probability one, Ann. Math. Statist. 25 (1954), 382–386. https://doi.org/10.1214/aoms/1177728794
• J. C. Spall, Multivariate stochastic approximation using a simultaneous perturbation gradient approximation, IEEE Trans. Automat. Control 37 (1992), 332–341. https://doi.org/10.1109/9.119632