All missions

Motivation

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 $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

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).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ 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 $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ 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.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ 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 $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ 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 $T_N$, then fewest tasks between $T_N$ 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 $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). 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 $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, 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 $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, 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 $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) 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.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5

Motivation

The residual life time of a lifetime $X$ at age $t$ is the remaining life $X - t$ given survival past $t$. Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as $t \to \infty$ and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.

Limit theorems describe the behaviour only as $t \to \infty$. Section 4 of the paper gives approximation results for finite $t$. In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law $\Phi_\alpha$: $tF'(t)/(1 - F(t)) \to \alpha$. Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).

Setting

Let $X$ be a real random variable with law $\mu$ and distribution function $F(x) = P\{X \le x\}$. For an age $t$ with $P\{X > t\} > 0$, the residual life distribution function is

$$F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t + x])}{\mu((t, \infty))}, \qquad x \in \mathbb R,$$

which is $0$ for $x < 0$. For $t > 0$ the residual life scaled by the age has distribution function $P\{(X - t)/t \le x \mid X > t\} = F_t(xt)$.

For $\alpha > 0$ the Pareto-type law $\Gamma_\alpha$ is

$$\Gamma_\alpha(x) = 1 - (1 + x)^{-\alpha} \quad (x \ge 0), \qquad \Gamma_\alpha(x) = 0 \quad (x < 0).$$

It is the law of $Y - 1$ when $P\{Y > y\} = y^{-\alpha}$ for $y \ge 1$. $F$ has a positive density $F'$ for $t \ge t_0$ if $F$ is differentiable at every $t \ge t_0$ with derivative $F'(t) > 0$. The quantity $F'(t)/(1 - F(t))$ is the hazard rate of $X$ at $t$, and $tF'(t)/(1 - F(t))$ is the hazard rate scaled by the age.

Formalization targets

Goal: Theorem 6 (p. 801)

Let $F$ have a positive density $F'$ for $t \ge t_0$, and let $\alpha_1, \alpha_2 > 0$ satisfy $\alpha_1 \le tF'(t)/(1 - F(t)) \le \alpha_2$ for $t \ge t_0$. Then for all $t \ge t_0$ and all real $x$,

$$\Gamma_{\alpha_1}(x) \;\le\; P\Big\{\frac{X - t}{t} \le x \;\Big|\; X > t\Big\} \;\le\; \Gamma_{\alpha_2}(x).$$

The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail $1 - F(t) = Ct^{-\alpha}$ one may take $\alpha_1 = \alpha_2 = \alpha$, and both inequalities are equalities.

Milestone: the integrated hazard bounds (proof of Theorem 6, p. 801)

For $t \ge t_0$ and $x > 0$,

$$\alpha_1 \int_t^{(1+x)t} \frac{du}{u} \le \int_t^{(1+x)t} \frac{F'(u)}{1 - F(u)}\,du \le \alpha_2 \int_t^{(1+x)t} \frac{du}{u}.$$

Significance

The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age $t \ge t_0$ rather than only in the limit. If moreover $tF'(t)/(1 - F(t)) \to \alpha$, then $\alpha_1, \alpha_2$ can be taken arbitrarily close to $\alpha$ for large $t_0$, which recovers the convergence $P\{(X - t)/t \le x \mid X > t\} \to \Gamma_\alpha(x)$ with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.

The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and $-\log(1 - F)$ for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and $\Gamma_\alpha$) are shared.

Difficulty

The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to $-\log(1 - F)$ with a derivative that is not assumed continuous, and its integrability on $[t, (1+x)t]$ has to come from the hazard bounds themselves. That $1 - F$ stays positive, that $t_0 > 0$, and that the case $x \le 0$ is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with $1 - R((1+x)t)/R(t)$, where $R = 1 - F$, through the measure of intervals.

Formalization scope

The law of $X$ is a probability measure $\mu$ on $\mathbb R$, and $F$ is Mathlib's ProbabilityTheory.cdf μ. The probability $P\{(X - t)/t \le x \mid X > t\}$ is residualLife μ t (x * t) $= \mu((t, t + xt])/\mu((t, \infty))$. $\Gamma_\alpha$ is a real function defined by cases, with Real.rpow for the power. The density is an explicit function $f$ with $F$ having derivative $f(t) > 0$ at every $t \ge t_0$, the derivative taken within $[t_0, \infty)$. This is a right derivative at $t_0$ and the ordinary derivative for $t > t_0$. It is the weakest reading of "positive density $F'$ for $t \ge t_0$", and it admits the exact Pareto law with $t_0 = 1$, whose distribution function has no two-sided derivative at $1$. The bounds are stated for $t \cdot f(t)/(1 - F(t))$ with Lean's real division.

No hypothesis is added to the printed theorem, and no printed slip was found. The conditions $t_0 > 0$ and $F(t) < 1$ follow from the hypotheses: for $t \le 0$ the ratio is not $\ge \alpha_1 > 0$, and a positive derivative on $[t_0, \infty)$ makes $F$ strictly increasing there. Lean's convention $a/0 = 0$ therefore never acts at the ages concerned. The conclusion is stated for all real $x$, as printed; for $x \le 0$ all three quantities are $0$. The milestone does not assume the hazard rate integrable: it is bounded and measurable on $[t, (1+x)t]$, and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced $F'$ by deriv without differentiability, or let the bounds hold only on a set not containing every $t \ge t_0$ would not be this theorem; all three are excluded by the statement.

A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity $\int_t^{(1+x)t} du/u = \log(1+x)$, and the chain rule for $\log(1 - F)$. Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that $\Gamma_\alpha$ is a distribution function and that the Pareto law satisfies the hypotheses with $\alpha_1 = \alpha_2$.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
• R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
• L. de Haan, A. Ferreira, Extreme Value Theory: An Introduction, Springer, 2006. https://doi.org/10.1007/0-387-34471-3

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

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.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

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 $S_n$ for the first $n$ 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.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

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 $S_n$ 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).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

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.

Difficulty

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).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. 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 $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ 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.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{1.9992})$ algorithm for 3SUM on $n$ polynomially bounded integers, on a word RAM with $O(\log n)$-bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.

The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.

References

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
2. Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_3SUM.

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$; the root that becomes a child is unmarked. The operations act as follows:

• make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
• delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
• decrease key $(\Delta, i, h)$, $\Delta \ge 0$, lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
• After every cut of a child of $p$, if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$.

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

$$\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}$$

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

1. LEMMA 1: the $i$th child of a node, in linking order, has rank at least $i - 2$.
2. $F_{k+2} \ge \varphi^k$, with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$.
3. COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
4. A node of rank $k$ in an $n$-item heap has $\varphi^k \le n$, hence $k \le \log n / \log\varphi$.
5. make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
6. delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
7. decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
8. From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$, all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$, and minimum spanning trees in $O(m\,\beta(m,n))$.

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$, fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant "$\le 1.4404 \log n$" on p. 604 is a rounding slip ($1/\log_2 \varphi = 1.44042\ldots$); milestones use the exact $\log_\varphi n$.

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
• J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
• R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

Motivation

A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.

The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).

Setting

A graph $G=(N,E)$ has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths $c_e$ are real and nonnegative, as in §2, p. 89.

The degree of $v$ is the number of named edges meeting it. Let $T$ be the set of nodes of odd degree. For every edge $e$, let $x_e\in\mathbb N$ be the number of additional traversals. The parity equations require a nonnegative integer $w_v$ at each node such that

$$\sum_{e\ni v}x_e=2w_v+b_v,\qquad b_v=\begin{cases}1&v\in T,\\0&v\notin T.\end{cases}$$

Their objective is $z(x)=\sum_{e\in E}c_ex_e$. These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding $x_e$ copies of each original edge.

For nodes $u,v$, write $d(u,v)$ for the length of a shortest path in $G$. This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from $u$ to $v$. Connectivity and nonnegative edge lengths make that specification meaningful. Let $G_p$ be the complete graph on $T$, with edge $\{u,v\}$ of weight $d(u,v)$. A 1-matching $M$ pairs every node of $T$ with exactly one distinct node. Its length is $L(M)=\sum_{\{u,v\}\in M}d(u,v)$, equivalently half the sum of $d(v,f(v))$ over $v\in T$ for the pairing involution $f$ (§3, p. 92).

Formalization targets

Odd-node matching reduction

The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:

$$\forall M\;\exists x\text{ satisfying the parity equations}:\quad x_e\in\{0,1\},\ z(x)\le L(M),$$ $$\forall x\text{ satisfying the parity equations}\;\exists M:\quad L(M)\le z(x).$$

The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).

Postman-tour reduction

The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge $e$ exactly $1+x_e$ times, and its length is

$$\sum_{e\in E}c_e(1+x_e) =\sum_{e\in E}c_e+z(x).$$

Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).

Significance

The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.

A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, $T$-joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.

Difficulty

A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting $x_e=1$ for the union then loses the additivity of path lengths, and setting $x_e=2$ loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible $x$ may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).

Formalization scope

Lean uses the published EdmondsMatching65.Polyhedron.Graph for $G$: finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.

The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of $G$.

The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.

Selected references

• Jack Edmonds and Ellis L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973), 88–124. DOI: 10.1007/BF01580113.

Motivation

The Chinese postman problem asks for a shortest closed walk in a graph that traverses every edge at least once. Edmonds and Johnson (Math. Programming 5 (1973) 88–124) reduce it to two subproblems: choosing, by matching, which edges to duplicate so that every node has even degree, and then actually finding an Euler tour of the resulting even graph, a closed walk using every edge exactly once. Euler's theorem guarantees such a tour exists in a connected even graph, but an algorithm has to produce one and represent it compactly.

Section 5 of the paper gives two such representations and two algorithms. This mission formalizes the next-node representation: for each node $n$, a list of the nodes the tour goes to when leaving $n$. Theorem 5.1, which the paper attributes to its reference [1] (van Aardenne-Ehrenfest and de Bruijn, 1951) and to Berge's textbook, characterises exactly which lists describe an Euler tour; Theorem 5.2 shows the paper's next-node algorithm produces such lists. The same correspondence between Euler tours and arborescences is the combinatorial core of the BEST theorem on counting Euler tours of directed graphs (van Aardenne-Ehrenfest and de Bruijn, 1951).

Setting

A graph $G$ is a finite set of nodes and a finite set $E$ of edges, each edge meeting two distinct nodes; several edges may meet the same pair of nodes. The degree $\deg(n)$ counts the edges meeting $n$, and $\#(n,m)$ counts the edges meeting both $n$ and $m$. A tour is an alternating sequence $(n_1, e_1, n_2, \dots, e_l, n_{l+1} = n_1)$ in which $e_i$ meets $n_i$ and $n_{i+1}$; an Euler tour contains every edge exactly once. $G$ is connected when every two nodes are joined by such a sequence, and even when every degree is even.

Next-node lists assign to each node $n$ a list $L_n(1), \dots, L_n(k_n)$ of nodes. Given a starting node $r$, the lists specify a walk: start at $r$; the first time a node $n$ is reached (for $r$, at the start), leave it to $L_n(k_n)$; the second time, to $L_n(k_n - 1)$; and so on, so the lists are read from the last entry to the first. The walk stops at the first node whose list is used up. The lists describe an Euler tour when this walk uses every entry of every list and its node sequence is the node sequence of an Euler tour of $G$. With parallel edges, the lists name nodes only, and the edge used at each step is chosen so that every edge is used once.

An arborescence with root $r$ is a tree whose edges are directed so that every node $n \ne r$ has exactly one edge directed away from it, and $r$ has none.

Formalization targets

Goal: Theorem 5.1 (p. 112)

For any node $r$ of an even, connected graph $G$, next-node lists describe an Euler tour from $r$ if and only if

$$\text{(i)}\ k_n = \tfrac12\deg(n)\ \ \forall n,\qquad \text{(ii)}\ \#(n,m) = |\{i : L_m(i) = n\}| + |\{i : L_n(i) = m\}|\ \ \forall n, m,\qquad \text{(iii)}\ \{\,n \to L_n(1) : n \ne r\,\}\ \text{is an arborescence with root } r .$$

The printed condition (iii) names the edges $(n, L_n(k_n))$; the paper's own proofs of Theorems 5.1 and 5.2 use $(n, L_n(1))$, the last exit from $n$, and the printed version is false on a five-edge example. The goal states $L_n(1)$.

Milestones

The proof on pp. 112–113 splits into five claims, each a milestone:

1. an Euler tour's lists satisfy (i) and (ii);
2. every node set $S$ with $r \notin S$ has a last-exit edge $n \to L_n(1)$ leaving it;
3. a map with one outgoing edge per node $n \ne r$ and an edge leaving every set avoiding $r$ is an arborescence;
4. under (i) and (ii) the walk from $r$ returns to $r$ having traversed every edge meeting $r$;
5. at that point every node $n$ incident to an untraversed edge differs from $r$ and still has its last exit $L_n(1)$ unused.

Companion: Theorem 5.2 (p. 112)

The lists produced by any complete run of the next-node algorithm of §5.2 satisfy (i), (ii) and (iii); together with Theorem 5.1, they describe an Euler tour.

Significance

Theorem 5.1 replaces a global property, that a walk uses each edge exactly once, by three local checks: list lengths, pair counts, and a tree condition on one distinguished entry per node. That is what makes the next-node representation usable. An algorithm only has to build lists with (i)–(iii), and Theorem 5.2 shows the paper's algorithm does so for every nondeterministic choice it makes. The same arborescence condition counts Euler tours in the BEST theorem: each arborescence and each ordering of the remaining exits gives a distinct tour.

The results have been proved since 1951. What this mission proposes is a Lean formalization on multigraphs with parallel edges, which is the setting the Chinese postman reduction needs, since duplicated edges are parallel. A search of Mathlib and of the platform finds no formalization of Theorem 5.1, of next-node lists, or of arborescences in this form. Mathlib has Eulerian walks only for simple graphs, and the existing platform statements of Euler's theorem (for example SupplyChainTheory.euler_tour_iff) are about simple graphs and existence only.

Difficulty

The necessity of (i) and (ii) is counting. The substance is in two places.

First, necessity of (iii): the last exits must be shown to leave every set avoiding $r$. The tempting choice of the first exits $L_n(k_n)$, which is what the theorem's printed text says, is wrong: on an Euler tour the first exits can form a cycle, so any argument that does not distinguish first from last exits cannot work.

Second, the converse: a walk that follows lists satisfying only (i) and (ii) can return to $r$ early and leave edges untraversed, so (iii) is indispensable, and the statement depends on exactly which list entries have been used when the walk stops. Making that bookkeeping precise for a walk defined by a counter per node, and turning the used entries into an actual edge sequence in a multigraph, is the main formal work. For Theorem 5.2 the difficulty is the invariant of a nondeterministic algorithm: every trail it starts closes at its starting node because the graph is even.

Formalization scope

All declarations live in the namespace ChinesePostman.NextNode. A graph is a local ChinesePostman.NextNode.Graph V E structure on finite types: ends : E → Sym2 V and a proof that no edge is a loop, so parallel edges are distinct elements of E with the same ends. Walks are pairs of a node list and an edge list. A list $L_n$ is a Lean List V, so $L_n(i)$ is the entry at index $i-1$ and $k_n$ is the length. The walk specified by the lists is computed by follow L r, a fuel-bounded iteration whose state is the current node and the number of departures made from each node. It returns the node sequence and the final counters. DescribesEulerTour G r L requires every counter to reach the list length and some edge list to make the node sequence an Euler tour. Condition (ii) is quantified over all pairs including $n = m$, where it forbids a node in its own list. Condition (iii) requires every list of a node $n \ne r$ to be nonempty, its chosen exit to be an edge of $G$, and requires the iterates of the parent map $n \mapsto L_n(1)$ (with $r \mapsto r$) to reach $r$ from every node. The next-node algorithm is an inductive step relation on states, and "produced" means reachable termination from the Step 0 state.

Added hypotheses: Theorem 5.2 and its corollary assume an edge $e_0$ meeting $r$, which Step 0 needs; a one-node graph without edges satisfies Theorem 5.1 trivially and is not excluded. Milestones drop the hypotheses their claims do not use (connectivity, evenness), which makes them stronger.

A trivializing formalization is ruled out explicitly: the lists are read backwards, from $L_n(k_n)$ to $L_n(1)$, and must all be used up. Reading them forwards, dropping the "uses every entry" clause, or stating (iii) with an empty-list default for the parent would each make a different, and in some cases false, statement.

The development needs walks on multigraphs, counting arguments for closed walks (in-degree equals out-degree along the walk), and a finite pigeonhole/orbit argument for the arborescence. The arborescence lemma (milestone 3) is graph-free and reusable. Proofs of any milestone, and of the multigraph walk lemmas they need, are welcome.

Selected references

• J. Edmonds and E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• T. van Aardenne-Ehrenfest and N. G. de Bruijn, Circuits and trees in oriented linear graphs, Simon Stevin 28 (1951) 203–217 (reference [1] of the paper, cited there as "Circuits and trees in oriented graphs").
• C. Berge, The Theory of Graphs and its Applications, Wiley, New York, 1962 (reference [3] of the paper).

Motivation

A matroid abstracts the dependence structure of the columns of a matrix: which sets of columns are linearly independent, forgetting the numbers themselves. Graphs are the special case of incidence matrices over the integers mod 2, where a set of edges is independent exactly when it contains no cycle. A natural combinatorial question in this setting is the minimum partition (or covering) problem: how few independent sets are needed to cover all the elements? For a graph this is the least number of forests that cover its edges, its arboricity.

J. Edmonds answered this question for every finite matroid in Minimum partition of a matroid into independent subsets (J. Res. NBS 69B, 1965, doi:10.6028/jres.069b.004). The answer is a good characterization in Edmonds's sense: there is a short certificate both that a partition into $k$ independent sets exists (the partition itself) and that it does not (a single subset that is too large for its rank). The paper is also the source of the matroid partition algorithm, which together with matroid intersection became a basic tool of combinatorial optimization.

Timeline:

• 1935 — H. Whitney introduces matroids through rank and independence postulates (doi:10.2307/2371182).
• 1961–1964 — C. St. J. A. Nash-Williams and W. T. Tutte characterize graphs whose edges split into $k$ forests, and graphs containing $k$ edge-disjoint spanning trees (doi:10.1112/jlms/s1-39.1.12).
• 1965 — Edmonds proves the partition theorem for all matroids, with Nash-Williams's forest theorem as a corollary; the companion paper "Lehman's switching game and a theorem of Tutte and Nash-Williams" treats the packing side.

Setting

Let $M$ be a finite set of elements and call some subsets of $M$ independent. Edmonds's two axioms are:

• Axiom 1. Every subset of an independent set is independent. (A system satisfying this is an independence system.)
• Axiom 2. For any subset $A$ of the elements, all maximal independent sets contained in $A$ contain the same number of elements.

A matroid is a system satisfying both. The rank $r(A)$ of $A\subseteq M$ is the largest cardinality of an independent subset of $A$; in a matroid every maximal independent subset of $A$ has exactly $r(A)$ elements.

A circuit is a minimal dependent set. A span (closed set) is a set $S$ such that no circuit has exactly one element outside $S$, and the span $S(A)$ of $A$ is the minimal span containing $A$. A partition into $k$ independent sets is a family $I_1,\dots,I_k$ of mutually disjoint independent sets whose union is $M$; any number of the $I_i$ may be empty.

Formalization targets

Goal: THEOREM 1 (p. 69)

For every finite matroid $M$ and every integer $k\ge 0$, the elements of $M$ can be partitioned into $k$ independent sets if and only if there is no $A\subseteq M$ with

$$|A|>k\cdot r(A).$$

The condition ranges over all subsets $A$ of $M$, as printed.

Milestones

The milestones follow the paper's own lemmas and the claims of its main proof, in order.

1. PROPOSITION 1. Axioms 1 and 2 are equivalent to Axioms 1 and 2', where Axiom 2' says that the union of an independent set and one element contains at most one circuit.
2. PROPOSITION 2. Axioms 1 and 2' are equivalent to the circuit axioms 1c (no circuit contains another) and 2c (if distinct circuits $C_1,C_2$ share $e$, then $C_1\cup C_2-e$ contains a circuit).
3. PROPOSITION 3 (Lehman). If $e\in C_1\cap C_2$ and $a\in C_1-C_2$ for circuits $C_1,C_2$, some circuit $C$ satisfies $a\in C\subseteq C_1\cup C_2-e$.
4. PROPOSITION 4. $e\in S(A)$ if and only if $e\in A$ or some circuit $C$ has $C-A=\{e\}$.
5. PROPOSITION 5. $S(A)$ is the unique maximal set containing $A$ with rank $r(A)$; in particular $r(S(I))=|I|$ for independent $I$.
6. "Only if" (§1.3). For any independence system, a partition into $k$ independent sets gives $|A|\le k\cdot r(A)$ for all $A$.
7. Counting step (§1.6). If $x$ lies in none of $k$ disjoint sets $I_i$, and $x\in S$ with $|S|\le k\,r(S)$, then some $I_i$ has $|I_i\cap S|<r(S)$.
8. Rank drop (§1.6). For a span $S$ and an independent $I$ with $|I\cap S|<r(S)$: $S(I\cap S)\subseteq S$ and $r(S(I\cap S))<r(S)$.
9. One-element augmentation (§1.6). If $|S|\le k\,r(S)$ for every span $S$, any $k$ disjoint independent sets missing $x$ can be rearranged into $k$ disjoint independent sets covering exactly the old elements and $x$.
10. "If" from spans (§1.6). If $|S|\le k\cdot r(S)$ holds for every span $S$, then $M$ partitions into $k$ independent sets.

A further item states the paper's COROLLARY (Nash-Williams): the edges of a loopless finite graph $G$ can be colored with $k$ colors so that no circuit is one color if and only if no nonempty node set $U$ has $|E_U|>k(|U|-1)$, where $E_U$ is the set of edges with both ends in $U$.

Significance

THEOREM 1 is the base case of matroid union: the sets coverable by $k$ independent sets form a matroid whose rank is $\min_{A}\bigl(|M\setminus A|+k\,r(A)\bigr)$, and the paper's proof is the origin of the polynomial-time matroid partition algorithm and of Edmonds's later matroid intersection theory. Its graphic case gives the arboricity formula of Nash-Williams, used for sparse-graph decompositions and orientation problems. The criterion is a certificate: a single set $A$ with $|A|>k\,r(A)$ proves that no partition exists.

The theorem has been proved since 1965 and appears in every matroid textbook. As far as the platform and Mathlib record, it has no machine-checked proof: Mathlib has matroids, circuits, closure and strong circuit elimination for its own Matroid structure, but no matroid union or partition theorem. This mission produces a formal proof from Edmonds's own axioms (Axiom 2 as an equal-cardinality condition, not an exchange axiom), together with the equivalences between his axiom systems, which are themselves standard results.

Difficulty

The "only if" direction is a three-line count. The difficulty lies in the converse: a greedy procedure that fills the $k$ sets one after another fails even for matroids, so an element $x$ that fits in no current set must be accommodated by moving other elements between sets. Such a chain of exchanges must keep all $k$ sets independent and disjoint at every step and must terminate; stating it with sets whose contents change while their labels persist is the part that needs careful bookkeeping in a formal proof. A second, smaller difficulty is the translation between the paper's equal-cardinality Axiom 2 and the circuit and span language its proof uses (PROPOSITIONS 1–5).

Formalization scope

• Elements. A finite type $\alpha$ with decidable equality; $M$ is Finset.univ, subsets are Finset α, and the independent sets are a predicate Indep : Finset α → Prop.
• Axiom 1 and the rank are the published Whitney definitions IndepI1 and rankOfIndep (WhitneyMatroid.RankIndep.Postulates). The rank is integer-valued, and every inequality $|A|$ versus $k\,r(A)$ is compared in $\mathbb Z$ with $k\in\mathbb N$.
• Axiom 2 is stated exactly as printed: maximal independent subsets of each $A$ have equal cardinality. It is not replaced by an augmentation axiom or by Mathlib's Matroid.
• Added hypothesis. Every matroid statement assumes that $\emptyset$ is independent. The paper's rank presupposes it; for the empty family Axioms 1 and 2 hold vacuously and THEOREM 1 fails (an empty ground set and $k=1$).
• Spans are formalized from the paper's words, $|C\setminus S|\ne1$ for every circuit $C$; the formula printed beside them, $|S\cap C|\ne1$, is a misprint. $S(A)$ is the intersection of all spans containing $A$.
• Partitions are indexed families Fin k → Finset α of pairwise disjoint independent sets covering $M$, with empty parts allowed and $k=0$ included.
• The COROLLARY uses a graph given by ends : E → Sym2 V (parallel edges allowed, loops excluded), with independence as linear independence of incidence columns over $\mathbb Z/2\mathbb Z$. It quantifies over nonempty $U$: as printed, $U=\emptyset$ makes the statement false.
• Not a trivialization. The goal mentions neither spans nor circuits and quantifies over all subsets $A$; the spans-only condition is a separate milestone, and the augmentation step requires the new family to cover exactly the old elements plus $x$.

Contributions welcome: proofs of the axiom equivalences (reusable for any work with Edmonds-style or circuit-axiom matroids), the span lemmas, the augmentation step, and bridges to Mathlib's Matroid that would let its circuit and closure library be reused.

Selected references

• J. Edmonds, Minimum partition of a matroid into independent subsets, J. Res. Nat. Bur. Standards 69B (1965), 67–72. doi:10.6028/jres.069b.004
• J. Edmonds, Lehman's switching game and a theorem of Tutte and Nash-Williams, J. Res. Nat. Bur. Standards 69B (1965), 73–77. doi:10.6028/jres.069b.005
• C. St. J. A. Nash-Williams, Decomposition of finite graphs into forests, J. London Math. Soc. 39 (1964), 12. doi:10.1112/jlms/s1-39.1.12
• H. Whitney, On the abstract properties of linear dependence, Amer. J. Math. 57 (1935), 509–533. doi:10.2307/2371182

Motivation

Truncated-Newton methods minimize a smooth function $f:\mathbb{R}^n\to\mathbb{R}$ by taking, at each iterate $x_k$, a search direction obtained by solving the Newton equation $H(x_k)p=-g(x_k)$ only approximately, with the linear conjugate gradient (CG) method. Here $g$ is the gradient and $H$ the Hessian of $f$. 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 $f$ 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 $H$.

Setting

Fix a symmetric linear operator $H$ on $\mathbb{R}^n$, with the Euclidean inner product $u^{\mathsf T}v$ and norm $\|\cdot\|$, and a vector $g\in\mathbb{R}^n$. In the paper these are $H(x_k)$ and $g(x_k)$ at the current iterate.

The TNCG minor iteration (p. 194) runs CG on $Hp=-g$ from $p_0=0$. Its state at iteration $i$ is $(p_i,r_i,d_i,\delta_i)$:

$$p_0=0,\quad r_0=-g,\quad d_0=r_0,\quad \delta_0=r_0^{\mathsf T}r_0,$$

and, writing $q_i=Hd_i$,

$$\alpha_i=\frac{r_i^{\mathsf T}r_i}{d_i^{\mathsf T}q_i},\ \ p_{i+1}=p_i+\alpha_id_i,\ \ r_{i+1}=r_i-\alpha_iq_i,\ \ \beta_i=\frac{r_{i+1}^{\mathsf T}r_{i+1}}{r_i^{\mathsf T}r_i},\ \ d_{i+1}=r_{i+1}+\beta_id_i,\ \ \delta_{i+1}=r_{i+1}^{\mathsf T}r_{i+1}+\beta_i^2\delta_i .$$

At iteration $i$ the method first applies the curvature test (2.1), $d_i^{\mathsf T}Hd_i\le\varepsilon\,\delta_i$, and stops if it holds; otherwise it computes $r_{i+1}$ and applies the truncation test (2.2), $\|r_{i+1}\|/\|g\|\le\eta$, and stops if it holds. With $\varepsilon=\eta=0$, (2.1) reads $d_i^{\mathsf T}Hd_i\le0$ and (2.2) reads $r_{i+1}=0$. The method exits through (2.1) at $i$ when no test fired at any iteration $j<i$ and (2.1) holds at $i$.

For $\mu\in\mathbb{R}$ the eigenspace is $E(\mu,H)=\{v: Hv=\mu v\}$ (A.21). The span of vectors $v_1,\dots,v_m$ is written $[v_1,\dots,v_m]$; the Krylov space of $g$ is $[g,Hg,\dots,H^{m}g]$.

Formalization targets

Goal: Theorem 2.4 (p. 197)

Let $\eta_k=\varepsilon=0$. If $H$ is not positive definite, then either the minor iteration exits through (2.1) at some iteration $i$, so that

$$d_i^{\mathsf T}Hd_i\le 0 \quad\text{at an iteration } i \text{ the method reaches},$$

or

$$g^{\mathsf T}v=0\quad\text{for every } v \text{ with } Hv=\mu v,\ \mu\le0 .$$

Milestones

1. Theorem A.1, (A.2) and (A.5), at $\varepsilon=0$ (p. 206). If $d_i^{\mathsf T}Hd_i>0$ for $i=0,\dots,k$, then $d_i^{\mathsf T}Hd_j=0$ for $i\ne j\le k$, and $[d_0,\dots,d_k]=[g,Hg,\dots,H^kg]$.
2. Theorem A.5 (p. 210). If $g$ has a nonzero projection on each eigenspace of $H$, $k$ is the number of distinct eigenvalues, and vectors $d_0,\dots,d_{k-1}$ are $H$-conjugate with $(d_i,Hd_i)>0$ and span $[g,\dots,H^{k-1}g]$, then $H$ is positive definite.
3. The first sentence of the proof of Theorem 2.4 (p. 211). If $g$ is not orthogonal to any eigenspace of $H$, and exact CG passes the curvature test up to iteration $i$ and ends with $r_{i+1}=0$, then $H$ is positive definite.

Significance

The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature $d_i$ 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 $x_k\to x^*$ and the method terminates through (2.2), then, outside this rare case, $x^*$ 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.

Difficulty

The CG relations of Theorem A.1 are usually proved for positive definite $H$, where every denominator is positive. Here $H$ 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 $r=0$" to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of $g$, so one must relate that space to the eigenspaces that $g$ meets, using symmetry of $H$ and a count of distinct eigenvalues. A direct argument via "the directions span $\mathbb{R}^n$" fails, because when $g$ misses an eigenspace the Krylov space is a proper subspace.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n); $H$ is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's $H$ is a Hessian. Positive definiteness is $v^{\mathsf T}Hv>0$ for all $v\ne0$. The CG recursion is total and carries no stopping test; division by zero returns $0$ 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 $\|r_{i+1}\|\le\eta\|g\|$.

Theorem 2.4 is stated for an arbitrary symmetric $H$ and vector $g$ rather than at an iterate of a run of the full algorithm. It uses nothing else about $f$ or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints $H^{k-1}g$ as the last Krylov vector; the correct $H^kg$ is used.

A trivializing formalization exists and is ruled out: the first alternative is not "$d_i^{\mathsf T}Hd_i\le0$ for some $i$" over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with $d=0$); it requires that iteration $i$ 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.

Selected references

• R. S. Dembo and T. Steihaug, Truncated-Newton algorithms for large-scale unconstrained optimization, Mathematical Programming 26 (1983) 190–212. https://doi.org/10.1007/BF02592055
• R. S. Dembo, S. C. Eisenstat and T. Steihaug, Inexact Newton methods, SIAM Journal on Numerical Analysis 19 (1982) 400–408. https://doi.org/10.1137/0719025
• M. R. Hestenes and E. Stiefel, Methods of conjugate gradients for solving linear systems, Journal of Research of the National Bureau of Standards 49 (1952) 409–436. https://doi.org/10.6028/jres.049.044
• T. Steihaug, The conjugate gradient method and trust regions in large scale optimization, SIAM Journal on Numerical Analysis 20 (1983) 626–637. https://doi.org/10.1137/0720042
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006. https://doi.org/10.1007/978-0-387-40065-5