Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Shor's 1997 paper (SIAM J. Comput. 26(5), arXiv:quant-ph/9508027) gives a polynomial-time quantum algorithm for factoring integers. The quantum computer does not factor directly: it finds the multiplicative order of an element modulo . The step from order finding to factoring is classical and randomized, and goes back to Miller's 1976 work on primality testing (G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13 (1976)). Every account of Shor's algorithm, and every resource estimate for breaking RSA with a quantum computer, depends on this reduction succeeding with a constant probability per trial. This mission formalizes that probability bound as Shor states it on p. 1498 of the published paper.
Let be an odd integer with prime factorization
so is the number of distinct prime factors of , all odd. The unit group consists of the residues coprime to ; it has elements, where is Euler's totient function.
For a unit the order is the least positive integer with . For each the local order is the order of , taken modulo the full prime power, not modulo . For a positive integer , denotes the exponent of the largest power of dividing .
The reduction is: choose uniformly at random from , obtain its order (from the quantum subroutine), and compute
The procedure yields a nontrivial factor at when is even and . In Lean this event is ShorAlgorithms.Reduction.successEvent n u for u : (ZMod n)ˣ, and is localOrder n u p for p ∈ n.primeFactors.
It is stated for every odd . For a prime power () the bound is , so the statement says nothing there; it is informative exactly when is not a prime power, as the paper remarks. The constant is sharp: for exactly of the units succeed, so in place of would be false.
The result. The bound turns an order-finding oracle into a factoring algorithm: when is odd and not a prime power, each trial succeeds with probability at least , so independent trials all fail with probability at most . Even numbers and prime powers are split classically, as the paper notes, so the bound completes the reduction from factoring to order finding. The same criterion — a square root of other than splits — underlies the Miller–Rabin test and several classical factoring methods.
Formalizing it. The mathematics is classical and proved; the paper gives a sketch of one paragraph. This mission writes out the sketch as machine-checked statements over Mathlib's ZMod, including the probabilistic step, which in the paper is an informal appeal to the Chinese remainder theorem and "50% probability of agreeing with the previous ones". Mathlib already has the needed ingredients (cyclicity of for odd , ZMod.chineseRemainder, ZMod.card_units_eq_totient), but not the reduction or its probability bound.
The success criterion (milestone 1) is elementary. The substance is the counting. The obvious route — treating the as independent and each "equal to the previous one with probability " — needs both a precise product decomposition of the unit group modulo into the unit groups modulo , compatible with the local orders, and the count in a cyclic group of even order of the elements whose order has a given 2-adic valuation. The informal phrase "at most a 50% probability of agreeing with the previous ones" hides a conditioning argument over coordinates that has to be done by an explicit cardinality bound. A second pitfall is milestone 3: its converse direction and its forward direction use oddness of in different places, and modulo a power of the argument breaks because .
(ZMod n)ˣ; probabilities are stated in cleared-denominator form, in , with the count as Nat.card of a subtype. Non-units have no multiplicative order and are not sampled..val, which is at least for a unit when , so the natural-number subtraction in val - 1 never truncates. is natural-number division, used only under Even r.n.primeFactors.card, at least for , so k - 1 does not truncate. Since is odd this equals the page's "number of distinct odd prime factors".ZMod (p ^ n.factorization p) under the reduction homomorphism.ZMod n instead of the units would put non-units (with junk order ) into the denominator; the goal counts over (ZMod n)ˣ and divides by . The goal's constant is the paper's , which is attained, so it cannot be weakened into a triviality without changing the theorem.ZMod.chineseRemainder to unit groups and to local orders; and proofs of the milestones in any order.Shor's factoring and discrete logarithm algorithms (Shor 1997) reduce both problems to sampling from the output of a quantum Fourier transform: a register holding a superposition with a hidden period is transformed, then measured, and the measured value carries information about the period. The whole speed-up rests on one engineering fact: for the Fourier matrix, which has entries, can be applied by a quantum circuit of only elementary gates, each acting on one or two bits.
That circuit was found independently by Coppersmith (IBM RC 19642, 1994) and Deutsch, and Shor's §4 presents it following Ekert and Jozsa (Rev. Mod. Phys. 68, 1996). It is the quantum analogue of the radix-2 fast Fourier transform, and it reappears in phase estimation, in the hidden subgroup algorithms for abelian groups, and in every textbook account of quantum computation. This mission formalizes Shor's statement that the circuit computes the Fourier matrix, up to a reversal of the output bits, together with the two displayed steps of its verification.
A register of bits has one basis state for every bit string, with the least significant bit; the string encodes the integer
A state is a vector of complex amplitudes, one per basis state. A gate is a matrix whose rows are indexed by input basis vectors and whose columns are indexed by output basis vectors (§2, p. 1489). A gate on some of the bits acts on those bits through its matrix and leaves the others alone (§2, p. 1490): the output amplitude at a string is the sum, over the possible input values of the acted-on bits, of the input amplitude at with those bits replaced by , times the matrix entry from to the corresponding bits of .
The Fourier matrix (eq. (4.1)) is the matrix with entry ; it takes to .
The circuit uses two gates (eqs. (4.2), (4.3)):
The circuit is the gate sequence (4.4), applied from left to right:
that is, for it applies and then . On three bits it is .
The bit reversal of a string is the string with .
For every and every basis state , with ,
The sum runs over all -bit strings . Reading the output register in reverse order therefore yields .
The amplitude of in is
For bit strings , with the bit reversal of and their values,
The result. The goal says that , a dense unitary on amplitudes, is realized by one-bit gates and two-bit gates, followed by a relabelling of the output. This is what makes the Fourier sampling step of the factoring algorithm (§5) and of the discrete logarithm algorithm (§6) polynomial in the number of bits. Without it, the analyses of those sections describe measurements of states that no efficient circuit is known to prepare. The bit reversal is a real part of the statement: the circuit does not compute itself for , and an implementation must either permute the output bits or read them in reverse order.
Formalizing it. The identity is classical and its proof is short on paper; its content lies in bookkeeping that is easy to get wrong: which bit a gate touches, which of the input or output value a bit holds when a phase gate acts, and the order in which the gates are applied. A machine-checked version fixes all of these conventions explicitly and yields a reusable model of gate-level circuits on bit strings. To the drafter's knowledge there is no Lean formalization of this circuit on Prove2Me; the platform's FastFourierTransform rows state the classical Cooley–Tukey recursion for the unnormalized transform with the opposite sign, which is a different object.
Multiplying out the gate matrices is not an argument beyond tiny : the difficulty is to control the whole product of gates symbolically. The paper's argument (§4, p. 1496) is informal at exactly the points a formal proof must make precise: that only one sequence of intermediate basis states from to carries nonzero amplitude, and that at the moment acts, bit already holds its output value while bit still holds its input value . Both facts depend on the order (4.4); applying the same gates in the reverse order gives a different unitary, whose phase pairs with . The phase identity then holds only modulo , not as an equality of real numbers, so it cannot be closed by rearranging sums alone.
Fin l → Fin 2, with bit j equal to and value (least significant bit first). A state is a function from bit strings to ℂ. The case (, empty circuit) is included.R j and S j k — run by a left fold, so the leftmost gate acts first. It is not defined as the matrix or by its entries; a definition of that kind would make the goal true by unfolding and is ruled out.Welcome contributions: proofs of the two milestones and the goal; general lemmas about one- and two-bit gate actions on Fin l → Fin 2 states (commutation of gates on disjoint bits, linearity, action on basis states), which are reusable for any gate-level circuit; and a proof that the circuit is unitary.
Conjugate gradient methods minimize a smooth function using only gradients and a handful of stored vectors. This makes them the standard choice when is too large for Newton or quasi-Newton methods, which store an matrix. On a strictly convex quadratic with exact line searches the classical method of Hestenes and Stiefel terminates in at most steps. On general functions, and with the inexact line searches used in practice, its behaviour is much less clear.
D. F. Shanno's 1978 paper in Mathematics of Operations Research (doi:10.1287/moor.3.3.244) links conjugate gradient methods to quasi-Newton methods. It writes the search direction as , where is a positive definite approximation of the inverse Hessian that is never stored. The resulting "memoryless" BFGS directions give descent without exact line searches. The paper's new algorithm uses two BFGS updates: one from the last restart and one from the current step. Its first update is scaled by the Oren–Spedicato factor . Shanno and Phua's CONMIN code implements the algorithm, and the memoryless BFGS direction is the one-pair case of the later limited-memory BFGS methods.
Vectors are columns in . A prime denotes transpose: is the inner product and the outer product. An iterative method produces points , steps along search directions , gradients , and gradient changes . A line search is exact when .
The BFGS update of a matrix with the pair is
A restart cycle begins at iteration . At a later iteration , Shanno's self-scaled restart matrix is
The matrix is its BFGS update with , and the self-scaled two-update direction is . The unscaled variant uses the BFGS update of in place of the first matrix.
Beale's direction is
The quadratic case has gradient with symmetric positive definite.
Let be symmetric positive definite, and . Assume that for we have , and , that for , and that . Then
This is the paper's claim that "for quadratic with exact searches each of the above methods reduces exactly to Beale's method defined by (28)", with the conclusion (44). The scale is exactly .
The result. The reduction says that the new algorithm reproduces Beale's restarted conjugate gradient directions on a quadratic with exact line searches. So it keeps the finite-termination and rate-of-convergence properties behind Beale's restart. Away from that setting it behaves as a quasi-Newton method, whose directions are descent directions under any line search with . The two regimes are what justify relaxing the line search, which the paper's computations exploit. The scale changes only the length of the step, not its direction.
Formalizing it. The claim is proved in the paper by a short computation, and no machine-checked version is known. This mission produces:
The obvious attempt is to expand both BFGS updates symbolically and compare with Beale's formula. This fails without two facts that are not algebraic identities. The first is that the restart step stays orthogonal to every later gradient, . It needs the affine gradient of a quadratic, the exact search at the restart step, and conjugacy of with all later steps. The second is , which again comes from conjugacy. Beale's formula also has to be matched in its -form: the coefficient equals only when the step length is nonzero. The descent statements need a different argument: the BFGS update of a positive definite matrix with must be shown to remain positive definite, and this has to be done twice.
Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The inner product is u ⬝ᵥ v, the outer product is vecMulVec u v, and is H *ᵥ v. The quadratic enters only through its gradient A *ᵥ x + c with A.PosDef. The paper's (4) is the case . Iterates, steps, directions and gradients are sequences indexed by ℕ. Division is Lean's total division. Every statement that divides therefore carries hypotheses making its denominators nonzero: and in the quadratic statements, and or in the generic ones.
The conjugacy for is a hypothesis, exactly as the paper's proof uses it. It is not derived from a full run of Beale's algorithm. The range of Beale's formula is not assumed.
Several formalizations would make the claim easier than the paper's, and none of them is used:
The generic milestones — (34), (40), (38), (42), (43) and the descent statements — are statements about arbitrary vectors and matrices and are reusable for any BFGS-based method. Proofs of any milestone, and alternative derivations of the goal, are welcome.
In quantum mechanics the state of a system at time is , where the Hamiltonian is a self-adjoint operator. The spectral theorem splits the Hilbert space into subspaces according to the type of the spectral measure of a vector (absolutely continuous, singularly continuous, pure point). That splitting is defined through measure theory, and it is not evident what it has to do with the motion of the system. The RAGE theorem, named after Ruelle (1969), Amrein and Georgescu (1973) and Enß (1978), answers this. Vectors in the continuous subspace are exactly the states that, on time average, leave every bounded region: the scattering states. Vectors in the pure point subspace are exactly the states that stay in a bounded region uniformly in time: the bound states. This dynamical characterization is the starting point of the geometric approach to scattering theory and of the modern theory of quantum dynamics and transport.
This mission formalizes Chapter 5 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009). The chapter covers the time evolution as a unitary group, Wiener's theorem on Fourier transforms of measures, and the abstract RAGE theorem with its Heisenberg-picture corollaries.
Let be a complex Hilbert space with inner product , conjugate linear in the first argument. An operator is a linear map defined on a subspace , its domain. is self-adjoint if is dense and . denotes the bounded, everywhere defined operators.
A projection-valued measure assigns to each Borel set an orthogonal projection , with and for disjoint . The spectral measure of is the finite Borel measure . The spectral theorem says that every self-adjoint is for a unique . Then and . For a bounded Borel function , is the bounded operator with . The time evolution is , the case .
The spectral subspaces are
and the continuous subspace is . The projectors are the orthogonal projections onto these subspaces. is the set of eigenvalues of .
A finite rank operator is a with finite dimensional range. The compact operators are the norm closure of the finite rank operators. For in the resolvent set , . An operator is relatively compact with respect to if for one ; in particular . The Fourier transform of a finite complex Borel measure on is .
Let be self-adjoint and let be relatively compact operators converging strongly to . Then
The RAGE theorem connects the spectral types of the Hamiltonian with observable long-time behaviour. For Schrödinger operators on , taking to be multiplication by the indicator of the ball of radius gives a sequence of relatively compact operators. The theorem then says that states in spend, on time average, a vanishing fraction of time in every ball, while states in stay uniformly localized. Enß's proof of asymptotic completeness for short-range potentials rests on this characterization. The same argument, through Wiener's theorem, is used to relate the fractal dimensions of spectral measures to rates of quantum transport. Theorem 5.8 and Corollary 5.9 describe the asymptotic observables of the Heisenberg picture.
These results are classical and proved in the literature. They are not formalized. Mathlib has neither a spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no decomposition of a Hilbert space by spectral type. What the platform has are Stone's theorem in the separate BookProof development (for weakly measurable groups, with its own structure of unbounded self-adjoint operators) and the discrete-time von Neumann mean ergodic theorem for contractions. The mean ergodic theorem is related to Theorem 5.8 with but is a different statement. This mission formalizes the continuous-time, spectral-type-resolved statements.
The two sides of the RAGE characterization are defined in unrelated terms. and are defined by properties of the scalar measures , while the conditions in (5.14) concern norms of vectors moving under a unitary group and seen through operators that are only relatively compact. Wiener's theorem controls scalar quantities . Passing to norms needs compactness, and relative compactness only gives compactness after composing with a resolvent, which is where the restriction to in Theorems 5.6 and 5.8 comes from. The pure point characterization needs control that is uniform in , so a limit over has to be exchanged with a supremum over all times. The limits in (5.14) and (5.19)–(5.20) are iterated, not joint, and a naive exchange of the two limits is not justified. Summing over in (5.18) needs an unconditionally convergent sum over a possibly uncountable index set. Wiener's theorem itself needs a Fubini argument for a complex measure against its conjugate.
The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space. Self-adjointness is Mathlib's IsSelfAdjoint, which includes density of the domain. The Hilbert space is not assumed separable.
The spectral theorem is not part of this mission. Every statement about takes a projection-valued measure on the Borel sets of as data, together with the hypothesis that : and there. This is the form the spectral theorem guarantees, and it makes . The time evolution is the bounded operator , determined by its quadratic form, and is its value at . Nothing else the book derives is assumed.
The spectral subspaces are sets of vectors defined only from the spectral measures, as above, and is the set of sums of a vector of and a vector of . A formalization that defined or by the dynamical conditions of (5.14) would make the goal a tautology; that is ruled out here. , , are the orthogonal projections onto the closed linear spans of these sets. Compact operators are the norm closure of the finite rank operators (the book's definition), not Mathlib's IsCompactOperator. Relative compactness asks for one , its resolvent , and a compact with and . " bounded" means an everywhere defined .
Iterated limits are stated as: for every the inner limit exists, and the sequence of inner limits converges. The supremum over is taken in . Time averages use interval integrals, with Bochner integrals for vector-valued integrands; all integrands are continuous in . Wiener's theorem uses Mathlib's ComplexMeasure ℝ and its vector-measure integral. The sum over is an unconditional sum whose summability is part of the conclusion, and the sum over is an unconditional sum in . The Fourier transform has the book's normalization.
A complete development needs a functional calculus for projection-valued measures (multiplicativity, strong continuity in the function argument), the reduction of by the spectral subspaces (Lemma 3.19), the Riemann–Lebesgue lemma for absolutely continuous measures, and the approximation of compact operators by finite rank ones. These pieces are reusable across the rest of the book, notably for scattering theory. Proofs of any milestone, and of such supporting lemmas, are welcome.
Retailers hold point-of-sale data that their suppliers cannot observe, and large retailers sell access to it through data-sharing programs (Costco's CRX, Walmart's Retail Link and similar programs). When one retailer carries the substitutable products of two competing manufacturers, sharing its demand information is a strategic decision: a manufacturer who knows the demand signal sets his wholesale price in response to it, which changes the retailer's margin and the rival manufacturer's order uncertainty. Whether the retailer should sell the information, to how many manufacturers, and by which protocol, is the question of Shang, Ha and Tong (Management Science 62(1):245–263, 2016).
The paper belongs to the information-sharing literature of Li (2002), Li and Zhang (2008) and Ha, Tong and Zhang (2011), which studies competing supply chains or a single chain. The common-retailer structure differs: the retailer can price-discriminate between the manufacturers through the order in which she offers the information.
Two manufacturers sell substitutable products through one retailer. The demand for product is
where is the retail price, measures competition, and is a random shock with mean and variance . The retailer observes a demand signal that is unbiased, , and has linear expectation: for a weight (in the paper , with the signal accuracy). The retailing cost is zero, and manufacturer produces units at cost with : a production diseconomy.
The game has four stages.
The pricing stage is a Bayesian game. Its equilibrium ex ante profits are , , for the manufacturers and for the retailer, where is the number of informed manufacturers. They define a payoff table for the contracting stage.
Two contracting protocols are compared.
For every , and every signal model, the pricing stage has an equilibrium; for every pricing equilibrium, both contracting games have equilibria; and for every concurrent outcome and every sequential subgame-perfect equilibrium (either first mover),
with both inequalities strict when . Here is the retailer's profit after side payments and the manufacturers' total profit net of them. The paper's word "higher" is read as because for small neither protocol sells information and all profits coincide.
The result. Proposition 4(d) says that the order of the offers transfers surplus: selling information one manufacturer at a time lets the retailer exploit the manufacturers' fear of being the only uninformed firm, which raises her profit and lowers theirs. Propositions 2 and 3 show that concurrent contracting shares with both manufacturers or with neither, while sequential contracting can end with only one informed manufacturer. Together they give a complete map of the equilibrium sharing decisions in (Figure 1 of the paper).
Formalizing it. The results are proved in the paper, partly by "it can be shown" and "straightforward" steps: Lemma 3's proof is omitted, and so is the convexity of the function whose root is . No part of the paper has a machine-checked proof. A complete formalization would check every such step and make the equilibrium notions precise, in particular the Pareto selection and the tie-breaking at the thresholds, where the retailer is exactly indifferent.
Most of the work is in the contracting stage, not the algebra. The pricing stage must be solved over all square-integrable strategies measurable in the signal. Uniqueness is then almost sure and rests on the linear-expectation identities and . The concurrent game has multiple equilibria for intermediate payments, and the retailer's optimum lies at a payment where two equilibria coexist. The sequential game is a three-stage game with a continuum of offers: at each threshold the retailer is indifferent, and an SPE exists only if acceptance at indifference is chosen correctly. The threshold has no closed form; it is the root of a convex rational function of .
The Lean development lives in the namespace InfoSharing.Diseconomy. Conventions:
A complete development needs:
The model layer is shared with the companion mission on production economy.
In quantum mechanics the spectrum of a Hamiltonian splits into two parts that behave very differently under perturbation. Isolated eigenvalues of finite multiplicity (bound states) move, split or disappear when the operator is changed even slightly; the rest of the spectrum, which carries scattering states and accumulation points of eigenvalues, is far more rigid. Weyl's theorem makes this rigidity precise: if two self-adjoint operators have resolvents that differ by a compact operator, their essential spectra coincide. It is the standard first step in locating the spectrum of a Schrödinger operator : one shows that is a relatively compact perturbation of , concludes , and is left with the discrete eigenvalues below zero.
The result goes back to H. Weyl's 1909 work on compact perturbations of bounded self-adjoint operators; the resolvent formulation for unbounded operators is the one used in modern texts such as Reed–Simon (Vol. IV, Sec. XIII.4) and Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Section 6.4, which this mission follows.
Let be a complex Hilbert space and a linear operator with domain . For , the resolvent exists when maps bijectively onto with a bounded inverse. The resolvent set is the set of such , and the spectrum is .
The discrete spectrum is the set of eigenvalues of that are isolated points of and whose eigenspace is finite dimensional. The essential spectrum is .
A sequence with , for every (weak convergence to zero) and is a singular Weyl sequence for at .
An operator is compact if it maps bounded sets to relatively compact sets; denotes the compact operators. An operator is relatively compact with respect to if and for one . is bounded if and on ; the infimum of admissible is the -bound. A symmetric operator has defect indices .
For self-adjoint and ,
The result. Weyl's theorem reduces the determination of the essential spectrum of a perturbed operator to that of a simpler reference operator. Combined with Lemma 6.22 and the Kato–Rellich theorem, it yields for every relatively compact symmetric ; Lemma 6.23 extends this to perturbations of the form . These are the inputs to the HVZ theorem for -body systems, to the spectral analysis of one-particle Schrödinger operators with decaying potentials, and, via Theorem 6.20, to the observation that boundary conditions at a limit-circle endpoint do not affect the essential spectrum of a Sturm–Liouville operator. The Weyl criterion is independently useful: it is how points are shown to lie in in concrete examples.
Formalizing it. The results are classical and proved in every text on the subject. None of them is formalized: Mathlib has compact operators and the adjoint of a densely defined LinearPMap, but no resolvent set or spectrum for unbounded operators, no discrete or essential spectrum and no relative compactness. This mission asks for formal proofs of Teschl's statements and, with them, a reusable layer of definitions (resolvent of a LinearPMap, , , singular Weyl sequences, relative compactness) on which later chapters (free Schrödinger operator, HVZ theorem) can build.
The obvious route to all of these statements goes through the spectral theorem: Teschl's proof of the Weyl criterion uses spectral projections and spectral measures , and his characterization (6.27)–(6.28) of by ranks of spectral projections presupposes the functional calculus. Mathlib has no spectral theorem for unbounded self-adjoint operators, so this route requires either building it or finding arguments that avoid it. The definition of used here is deliberately the PVM-free one of p. 145, which makes the statements expressible now but moves the difficulty into the proofs: showing that a point of carries a singular Weyl sequence requires controlling approximate eigenvectors near a non-isolated spectral point or an eigenvalue of infinite multiplicity without projections.
A second difficulty is domain bookkeeping. , , and all involve unbounded operators with different domains, and identities such as the second resolvent formula must be established on the correct domains. Theorem 6.20 requires relating the resolvents of two self-adjoint extensions through the finite-dimensional defect spaces.
The Hilbert space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since no statement of the section needs it. Unbounded operators are Mathlib LinearPMaps H →ₗ.[ℂ] H, self-adjointness is Mathlib's IsSelfAdjoint (which implies a dense domain), and symmetric operators are densely defined by definition, as in the book. The resolvent is the bounded two-sided inverse of of p. 73 (IsResolventAt), and , are defined from it; Mathlib's Banach-algebra spectrum is not used. "For one " is an existential over and the two resolvents. Compactness is Mathlib's IsCompactOperator, which on a Hilbert space agrees with the book's norm closure of finite rank operators. for bounded is K +ᵥ A (domain ); for unbounded is the LinearPMap sum with domain . The -bound is valued in and is for an operator that is not bounded. The defect indices are "equal and finite" when both defect spaces are finite dimensional with equal finrank.
No projection-valued measure or functional calculus is taken as data, and none is needed: every statement is phrased without . For this reason the second half of Lemma 6.21, for , and the form-compactness results Lemma 6.26 and Corollary 6.27 of Section 6.5 are not part of the mission.
A trivializing formalization is ruled out: the discrete spectrum requires all three of "eigenvalue", "isolated in " and "finite-dimensional eigenspace", so is neither empty nor all of by definition, and the resolvent hypothesis of Weyl's theorem is an existential over genuine resolvents, never a junk value outside .
A complete development needs the resolvent identities for LinearPMaps, the relation between self-adjointness and real spectrum, weak convergence of bounded sequences, and the fact that compact operators map weakly null sequences to norm-null ones. The definitions of resolvent, , relative compactness and -bound are shared with other chapters of this series and are intended for reuse. Contributions of general lemmas on LinearPMap resolvents are welcome.
A b-matching with upper bounds in a graph assigns a nonnegative integer to every edge so that the edges at each node carry at most in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching (, ) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point , find a violated blossom inequality or certify that none exists.
M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds . The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.
Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated -matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.
Let be a finite simple undirected graph, and . The system is
with the node–edge incidence matrix. For write for the edges with both ends in and for the cut-set of , the edges with exactly one end in . For with odd, the blossom inequality is
Let be a real point feasible for (3.1) and its node slacks. Let be the edges with . The labelled weighted graph has nodes , a special node , and one new node for each . For each such edge , where is the end the construction scans first, it has an edge of weight and an edge of weight . Each is joined to with weight . There are no other edges. A node is odd iff is odd; is odd iff is odd; a node is odd iff plus the of the subdivided edges scanned from is odd. A node set is odd when it contains an odd number of odd nodes, and denotes the total weight of the edges leaving (its cut capacity).
For every feasible and every scan order,
The paper's closing sentence, that and can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.
Theorem 3.1 is what makes the blossom inequalities of capacitated -matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated -matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.
The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph and of the reduction, and a checked proof of it. The definitions of the capacitated -matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.
The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets with complemented edge sets and odd node sets of . In one direction the right must pick, for every cut edge, the side of that makes the edge contribute or as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses to exclude every other position of a new node , and it uses the evenness of the total label to pass from an odd set containing to its complement. A point whose blossom violation uses an edge with has no new node for . Such a has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.
The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of is not assumed. All halves and differences are computed in ℝ. When the cut-set is empty, so the paper's convention " is empty" holds automatically.
is fixed by definitions from and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node . Weights are a symmetric function on nodes with meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by , and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.
Two trivializing formalizations are ruled out: is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is and would make the right side true when no odd cut exists.
Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.
Edmonds showed that the convex hull of the matchings of a graph is described by the degree constraints together with the blossom inequalities, one for every odd set of nodes (Edmonds 1965). There are exponentially many of them, so any cutting-plane method for matching and b-matching problems must answer a separation question: given a fractional point, find a violated blossom inequality or certify that none exists. Padberg and Rao (1982) reduced this question to a purely graph-theoretic one, the odd minimum cut-set problem, and solved that problem in polynomial time with a single Gomory–Hu computation. The same subroutine underlies separation for many other odd-set constraints (for example the 2-matching and comb-type constraints of the travelling salesman polytope), and later work refined its running time (Letchford, Reinelt and Theis 2008).
This mission covers Section 1 of the paper: the combinatorial theorem about odd cuts, independent of matchings. A companion mission covers the reduction from capacitated b-matching separation (Section 3).
Let be a finite undirected graph without loops and multiple edges, with edge weights . Write for the weight of the edge , with , and if there is no such edge. For the cut-set is the set of edges with exactly one end in , and its capacity is
A nonempty set of nodes is labelled odd, the rest even. For the label is odd if is odd, and even otherwise; is even. The paper assumes throughout that is even, i.e. is even. A cut-set is odd if is odd, and an odd minimum cut-set is a solution of
A cut-set is a minimum cut-set with respect to all pairs of odd nodes if it separates two odd nodes and no cut-set separating two odd nodes has smaller capacity.
A cut-tree for the odd nodes is the output of the Gomory–Hu algorithm applied to all pairs of odd nodes (Gomory and Hu 1961). Each tree node contains exactly one odd node and possibly some even ones, so is identified with , and each node of belongs to one tree node . Removing a tree edge splits into two subtrees; the nodes of in the tree nodes of the -side subtree form a set , and the weight of is . The defining property (Hu, Theorem 9.2) is that for every tree edge the cut-set is a minimum cut-set of separating and . The cardinality of a subtree is its number of tree nodes.
For every cut-tree of for the odd nodes:
Because is even, the two subtrees have the same parity, so the condition is checked on one side.
Theorem 1.1 turns problem (1.1), a minimization over exponentially many odd sets, into maximum-flow computations followed by a scan of the tree edges. Combined with Section 3 of the paper, this gives a polynomial separation algorithm for the blossom inequalities of b-matching polytopes, and hence, by the equivalence of separation and optimization, a polynomial-time route to weighted b-matching through linear programming. The odd-cut routine is also used for separating the odd-set constraints of other polytopes.
The theorem has been proved since 1982 and is textbook material. What this mission adds is a machine-checked proof on a precise encoding of cut-trees. As far as the platform's corpus shows, neither the Gomory–Hu cut-tree property nor any odd-cut theorem has been formalized in Lean; Mathlib has trees and reachability in simple graphs but no cut-tree theory.
The obvious argument fails at the minimum. Every tree-edge shore separates two odd nodes, so a minimum-weight odd-splitting edge certainly yields an odd cut, but showing that no odd set , however it cuts across the tree nodes, has smaller capacity requires relating an arbitrary odd to a tree edge whose shore is also odd and whose endpoints separates. The cut-tree only certifies minimality for cuts separating the two ends of a tree edge; an odd set may split many tree nodes and cross many shores at once, and nothing in the cut-tree property speaks about parity. Parity bookkeeping between odd labels in and odd cardinality of subtrees is the other place where care is needed: the two notions agree only because each tree node holds exactly one odd node.
The graph is a weight function c : V → V → ℝ on a Fintype V, with hypotheses that it is symmetric and nonnegative; a missing edge has weight 0 and the diagonal never enters a cut. Node sets are Finset V and is the complement Wᶜ. The odd nodes form a Finset odd with odd.Nonempty and Even odd.card on every statement. The cut-tree is a SimpleGraph on the subtype {v // v ∈ odd} together with a map π : V → {v // v ∈ odd}; IsOddCutTree requires that the graph is a tree, that π fixes every odd node, and the Gomory–Hu minimality for every tree edge. The tree-edge weight is computed from the shore, not supplied as data. Minimality is always stated as ≤ against every competitor; no real infimum is taken.
The existence of a cut-tree (the Gomory–Hu theorem) is a hypothesis-side object and is not part of this mission; the theorems hold for every tree satisfying the cut-tree property. A statement in which the cut-tree assumption already says that the chosen edge's shore is an odd minimum cut, or in which "odd minimum cut" is minimized only over tree-edge shores, would make Theorem 1.1 definitional; both are ruled out, since IsOddMinCut ranges over every node set with odd label.
A complete development needs: submodularity-type identities for cut capacities (reusable for any cut problem), the structure of fundamental cuts of a tree (the two sides of a removed edge are complementary and the parities of along tree edges combine), and Lemma 1.1. Proofs of the milestones, alternative arguments for the goal that avoid the recursion, and a formal Gomory–Hu existence theorem are all welcome contributions.
Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested agents: the designer can pay the agents, and must choose payments so that each agent's own interest leads it to reveal what the algorithm needs. Nisan and Ronen introduced the framework with task scheduling on unrelated machines as the running example (Nisan–Ronen 2001). In the basic model, where payments depend only on what the agents declare, they showed that no truthful mechanism approximates the optimal make-span within a factor below 2, and that the natural mechanism only reaches a factor .
Their Section 5 changes the information available: in a mechanism with verification the payments may also depend on the times in which the tasks were actually performed. With this extra information, an exact optimizer becomes a strongly truthful mechanism (Theorem 5.1, the Compensation-and-Bonus mechanism). Exact scheduling on unrelated machines is NP-hard, so the question is whether an approximation algorithm can take the optimizer's place. Theorem 5.6 of the paper shows that plugging a non-optimal algorithm into Compensation-and-Bonus destroys truthfulness in general. Theorem 5.9, the subject of this mission, shows that for the bounded problem a specific approximation scheme, the rounding algorithm of Horowitz and Sahni (1976), can be combined with a modified payment rule to give a truthful mechanism whose outcome is within a factor of optimal.
There are agents and tasks. Agent needs time for task ; the vector is the type vector, and agent alone knows its row . In the bounded scheduling problem (Definition 33) there are fixed numbers with for all , and every declaration lies in the same range. An allocation assigns each task to one agent; is the set of tasks of agent .
A strategy of agent has two parts: a declaration , and an execution, which for each decision of the mechanism specifies the actual time in which agent performs each task . The mechanism chooses from the declarations alone and afterwards observes the actual times . The objective is the make-span with actual times,
Agent receives a payment and has utility .
The corrected time vector of agent keeps agent 's actual times on its own tasks and the other agents' declarations elsewhere: for and for , . For a step , rounds up to a multiple of , and .
The rounding mechanism (Definition 34) allocates with an algorithm that exactly solves the problem with rounded declarations , and pays
The first term, the compensation, uses exact actual times; the second, the bonus, uses rounded quantities.
A strategy is dominant if it is a best response to every declarations and executions of the others. The mechanism is truthful if every agent has a dominant strategy that declares its true type.
For every , every and every allocation algorithm solving the rounded problem exactly, the rounding mechanism is truthful, and at every profile of dominant strategies from the class named in the proof (declarations with the true rounded values, executions whose rounded times equal the rounded true times),
The result shows that verification does more than make exact optimization truthful: it lets a polynomial-time approximation scheme be implemented in dominant strategies, provided the bonus is computed on the same rounded instance the algorithm optimizes. This contrasts with Theorem 5.6, where an arbitrary approximation algorithm inside Compensation-and-Bonus is not truthful, and with the factor-2 lower bound of the basic model. The principle it illustrates is that the payments must reward exactly the objective the algorithm optimizes.
The paper gives only a proof sketch. Formalizing it makes the argument's hypotheses explicit: which rounding step suffices, what the allocation algorithm must satisfy, and over which strategy profiles the approximation guarantee holds. No machine-checked version of this theorem or of the Compensation-and-Bonus argument is known to exist.
The sketch reduces the theorem to "arguments similar to those in 5.1", but the rounded setting departs from Theorem 5.1 in two ways. Rounding is many-to-one, so an agent's declaration and execution are pinned down only up to their rounded values, and the algorithm's optimality holds only for the rounded instance. Consequently the claim that the strategies with the true rounded values are the only dominant ones does not survive arbitrary tie-breaking: an agent that is always favoured on ties can overstate its rounded time by one step without ever losing, and two such lies at one profile can push the make-span above the bound. The approximation guarantee therefore has to be stated for the strategy class the proof identifies, not derived from dominance alone. The remaining steps require exact bookkeeping of rounding across sums and of the corrected time vectors, which a proof sketch leaves implicit.
Fin n with [NeZero n], tasks Fin k; allocations are functions Fin k → Fin n; the make-span is a Finset.sup' over agents. Types and declarations satisfy a ≤ t i j ≤ b with 0 < a < b; actual times are only bounded below by the true times.roundUp δ r = δ * ⌈r / δ⌉. The statement holds for every , which covers the intended choice ; the paper leaves as "a function of and ".Useful infrastructure: lemmas on Int.ceil rounding of finite sums and on Finset.sup' monotonicity, and a reusable model of mechanisms with verification. Proofs of the milestones in any order are welcome.
Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).
The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.
Timeline.
There are agents and tasks. The type of agent is a vector of positive reals, being the minimum time agent needs for task ; a type vector is . An allocation gives each task to one agent. The make-span is
and is optimal for if for every allocation .
In the model with verification, an agent's strategy has two parts: a declaration (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time in which the agent performs each task it receives. An allocation algorithm maps the declarations to an allocation ; the tasks are then executed, producing actual times .
The Compensation-and-Bonus mechanism based on pays agent
a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent 's actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector ). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.
Let be an allocation algorithm such that, for some real ,
and such that for some positive and some allocation . Then the Compensation-and-Bonus mechanism based on is not truthful.
The ratio is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.
The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.
Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.
The argument is short on paper; the difficulty lies in the model. The paper's "" is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.
Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring loses nothing.Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.
Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.
The paper gives a truthful mechanism, MinWork, whose make-span is within a factor of optimal, and a lower bound of for every truthful mechanism. It conjectures that no truthful mechanism beats (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).
Timeline of the gap between and :
There are agents and tasks . The type of agent is a vector of positive reals, being the time agent needs for task ; a type vector collects all types, and denotes the types of the agents other than . An allocation is a partition of the tasks, being the set given to agent . For a set of tasks write . The make-span is
A direct mechanism maps every declared type vector to an allocation and to payments handed to the agents. An agent with true type gets utility . The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a -approximation if for every positive type vector and every allocation .
The price offered for a set to agent (Definition 12) is the payment at any declaration for which the mechanism gives agent exactly , and if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if
for every agent , type vector and set of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.
For agents and tasks, for every truthful additive mechanism and every real ,
The goal leaves the mechanism, its tie-breaking and completely general. It says that the ratio of MinWork is optimal among additive mechanisms.
Theorem 4.10 shows that the gap between MinWork's ratio and the general lower bound cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.
All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).
The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is .
Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price . For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of carries a single-task price of at least . The final step also needs care. The paper's "w.l.o.g. " is a further reduction, and the paper's bound has to be replaced by .
Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is , and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.
The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.
Let be the complete undirected graph on . Vertex is the depot and are the customers. Vehicles have capacity and each customer has an integer demand with . An LP point is a vector ; and are the same variable, and LP solutions satisfy .
For a vertex set , is the set of edges with exactly one end-vertex in (edges to the depot included), and is its cut value. For a customer set :
The capacity inequalities and the rounded capacity inequalities (RCIs) are
The violation of such an inequality at is (resp. ); it is violated when this is positive.
Shrinking a customer set contracts it to one supervertex. The supervertices of the shrunk graph are then and the single customers outside , so a union of supervertices is a customer set with or . Shrinking is safe if for every customer set with whose inequality is violated, there is such a union with and at least the same violation.
For every and every customer set with
shrinking is safe for the capacity inequalities .
Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.
The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.
When the violated set contains or misses it, itself is a union of supervertices and there is nothing to show. The difficulty is a set that crosses : no union of supervertices is obviously as violated as , because enlarging can raise its cut value — can be smaller or larger than depending on the edges leaving — and the hypotheses on say nothing about directly. Both hypotheses on and the sign condition matter here; for signed the statement fails. A violated strictly inside is not a crossing set in the paper's sense and has to be handled as well.
On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.
Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity is real (the paper does not say it is an integer) and demands are natural numbers with for customers. The bin-packing number is the least number of bins over assignments of the customers of to bins of total demand at most ; under this minimum exists. Of the LP point only is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis " for all " ranges over nonempty proper subsets.
A formalization that lets in that hypothesis is vacuous, because ; one that drops the condition " or " from safe shrinking is trivial (take ); and one that defines as , as an arbitrary monotone function, or with a junk value , or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.
Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.
Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).
Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.
Let the rows of a set-partitioning master problem be . A column is a subset of the rows, with incidence vector ( iff ). Let be a finite collection of nonempty columns with costs . The master problem is
with integer in the integer program. Its dual has one free multiplier per row and one constraint per column.
A column is redundant, eq. (30), p. 1015, if
with and ranging over the columns of that are proper subsets of ; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair has the subcolumn property if for all with . Given dual multipliers , the ratio pricing problem (31) is
the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.
Let satisfy the subcolumn property, , and let be arbitrary. If is strictly redundant, then
that is, is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.
If only holds for in , the shifted costs satisfy the subcolumn property, and on every with ,
This is the paper's remark that the shift "adds to a constant term equal to the number of rows and does not change the problem".
Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.
The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on , no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.
The mathematical difficulty is modest; the difficulty is in the reading. With multipliers of arbitrary sign in (30), the proposition is false: on rows take , , , with costs , , , and ; then , , the subcolumn property holds, and has the unique smallest ratio. The empty column is a second trap: its denominator is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over only.
Conventions committed to in Lean:
Fin m (indexed from ); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on matter.1 ⬝ᵥ incidence a, which equals .A trivializing formalization — a redundancy witness not tied to the proper subcolumns of in , signed multipliers, or an empty column with ratio — is ruled out by the definitions above.
Needed infrastructure is only finite sums of vectors in and the identity . Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.
Many problems in statistics, signal processing and machine learning have the form
where is smooth (a least-squares loss, for instance), is a nonsmooth regularizer or constraint, and is a linear map such as a finite-difference operator. When is nonconvex — the cardinality function , the quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on and a smooth step on , but for nonconvex it was long used without a convergence theory.
Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).
Let be twice continuously differentiable with bounded Hessian , let be proper (finite somewhere, never ) and closed (lower semicontinuous), and let be linear with adjoint .
A vector is a regular subgradient of at (with finite) if . The limiting subdifferential collects all limits of regular subgradients at points with . A point is stationary if
For the augmented Lagrangian is , and for a convex function the Bregman distance is . The proximal ADMM generates, from arbitrary ,
Assumption 1 requires for some (so is surjective), Loewner bounds , with , , a strong-convexity margin , and some with . Here .
Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:
and is stationary; 2. (Strict improvement) if is not stationary, and , then every cluster point satisfies
The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.
In attack order: the robustness (3) of ; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for ; the vanishing of the primal steps (16); the convergence (10) of ; and, for part (ii), , the first-step estimate (27) and the strict decrease after (28).
Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex : any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice turns the -update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking large when , , do not depend on . The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.
The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.
The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: need not decrease, because the multiplier step increases it by . The proof has to bound this increase by primal steps, which uses surjectivity of and the squared Hessian bounds, and it produces a two-step recursion (involving ) rather than a monotone sequence. Nor is known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for requires , which lower semicontinuity alone does not give. For part (ii), the start is not an iterate at all, so the first step needs its own estimate.
Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is a continuous linear map and is ContinuousLinearMap.adjoint. and take values in EReal; inequalities involving are written additively ( with real ), never through EReal.toReal. The Hessian is the derivative of the gradient. is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; adds positive definiteness. for every , possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); are free and is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.
The limiting subdifferential keeps all three requirements of its definition — , and — and the domain condition ; dropping -attentive convergence or replacing by the convex subdifferential would make stationarity a different, and for nonconvex wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of , finiteness of the objective at and . The paper's assumption that proximal maps of exist is not a hypothesis, since no statement asserts that the iteration can be run.
Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.
Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.
For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from to . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most .
Let be a real Hilbert space with inner product . A set-valued operator assigns a subset to every point . It is monotone if whenever and , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of . The class of maximally monotone operators is , and is the set of zeros.
For a step size , the resolvent maps to the unique with . It is single-valued for monotone and defined on all of for maximally monotone .
The general proximal point method with step coefficients starts at and iterates
Kim's proposed accelerated proximal point method starts at and iterates
The coefficients (25) are for and .
The PEP of Section 3 bounds the worst case of over all and all starts with . A semidefinite relaxation leads to the dual problem (D): minimize over nonnegative such that . The matrices are explicit symmetric matrices built from and the canonical basis . Its optimal value is .
For every , every , every run of the proposed method, and every with for a constant ,
The constant is the paper's, and nothing is left unfixed.
Theorem 4.1 gives the first rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).
The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.
The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an matrix whose entries are double sums over , uniformly in . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at .
is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.
The resolvent step is relational: is encoded as . For monotone and this determines uniquely, and for maximally monotone such an exists for every (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's is y (0 - 1) = y 0 under natural-number subtraction. The general method has no , so its initial-distance condition is on , as in (17). The step size is written lam.
PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i . is the infimum of the feasible values of computed in EReal, so an infeasible gets the value as in the paper; Eq. (28) compares it with the real bounds cast to EReal.
A formalization in which the iterate predicate cannot be satisfied, the residual is , the correction term is dropped or has the wrong sign, the initial point is decoupled (), or is only monotone on finitely many points, would state a different theorem, and none is used here.
Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.
One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in . It is the model behind cutting stock (cutting rolls of paper or steel to ordered widths), memory and file allocation, and batch scheduling on identical machines, and it is NP-hard. Its algorithmic study is therefore about approximation: how close to the optimum a polynomial-time algorithm can guarantee to come.
An instance is a finite multiset of piece sizes, each in the open interval . Write for the number of pieces, for the number of distinct sizes, and for the sum of all sizes. A packing of is a finite multiset of bins, each a multiset of sizes, whose union is exactly and in which every bin has total size at most . Its cost is the number of bins, and is the minimum cost.
A configuration of is a nonempty multiset of sizes occurring in with total at most . With the number of pieces of size and the number of occurrences of in configuration , the fractional bin-packing problem is the linear program
whose optimal value is . A basic feasible solution is an extreme point of its feasible region.
For instances , write if there is a one-to-one map from the pieces of into the pieces of with . Linear grouping with parameter sorts non-increasingly, cuts it into groups of consecutive pieces (the last possibly shorter), rounds every piece of up to the largest size of to get , and outputs and .
ALGORITHM 1 takes and : (1) discard the pieces of size , leaving ; (2) apply linear grouping to with , giving and ; (3) put each piece of in its own bin; (4) obtain from a Fractional Bin-Packing subroutine a basic feasible solution of the LP of with ; (5) round to a packing of with at most bins; (6) shrink the pieces back to obtain a packing of ; (7) insert the discarded pieces, opening a new bin only when a piece fits nowhere. is the cost of the resulting packing.
The additive term depends on only, so ALGORITHM 1 is an asymptotic approximation scheme. The paper prints the factor , which fails for ALGORITHM 1 as printed (see Formalization scope); running the algorithm with gives the paper's main result (4), , stated as a separate corollary with the explicit term .
The result showed that the configuration LP, of exponential size in general, can be used for a guaranteed approximation: its value is within of the integer optimum, and grouping reduces at small cost. The same template (eliminate small items, group, solve the configuration LP, round a basic solution, reinsert) underlies later schemes for bin packing, cutting stock, bin packing with cardinality constraints and scheduling, and the LP-based analysis is the starting point of the Rothvoß and Hoberg–Rothvoß improvements.
The theorems are proved in the literature; none of them has a machine-checked proof on the platform or, to our knowledge, in Mathlib. This mission produces a checked analysis of the algorithm, including a correction: the printed approximation factor is not valid for the algorithm as printed, and the checked statement records the factor its proof yields. The definitions (instances, packings, the configuration LP, basic solutions, the order , any-fit insertion) are reusable for the second mission of the series and for other bin-packing results.
The Lean statements are short, but several proofs need linear-programming structure that is not in Mathlib in this form. Lemma 2 and Corollary 1 use that an extreme point of has at most as many nonzero coordinates as there are rows of ; the configuration LP is indexed by a finite but implicitly described set of multisets. Monotonicity of under ("clearly" in the paper) requires transporting a fractional solution across a piece-to-piece matching whose images are types, not pieces. The existence of a run requires an optimal basic feasible solution of the configuration LP. Lemma 3 concerns an insertion process with unrestricted order and bin choice, so its bound has to hold for every execution, not for one greedy rule.
Multiset ℝ; packings are Multiset (Multiset ℝ) with join equal to the instance, bin loads at most , empty bins allowed and counted. is a natural-number infimum over a set that is always nonempty.Multiset ℝ →₀ ℝ supported on configurations. is a real infimum over a set that is nonempty (singleton configurations) and bounded below by . "Basic" is the extreme-point property; the bound on the number of nonzero coordinates is a consequence, not the definition.Alg1Run ε I P: is a possible output. Every open choice is quantified: the subroutine's output, the packing of Step 5 (any packing within the stated bound), the size reduction of Step 6 (bin by bin), and the insertion of Step 7 (any order, any fitting bin). The goal holds for every run, and a separate item states that a run exists, so the goal is not vacuous.Proofs of any item are welcome; Lemma 2, Corollary 1 and the monotonicity display are the most reusable.
A process on a shared-memory multiprocessor that finds a lock held must decide what to do while it waits. It can spin, repeatedly testing the lock and occupying its processor, or it can block, giving the processor to another process and paying a fixed context-switch cost to be descheduled and later restored. Spinning is cheap when the lock is released soon; blocking is cheap when the wait is long. The waiting time is not known in advance, so the choice has to be made on-line. This is the spin-block problem, studied by Karlin, Manasse, McGeoch and Owicki in Competitive Randomized Algorithms for Nonuniform Problems (Algorithmica 11, 1994, doi:10.1007/BF01189993), §4. Mathematically it is the continuous form of the ski-rental problem, and the same rent-or-buy structure recurs in power-down policies and in TCP acknowledgement (Karlin, Kenyon, Randall, STOC 2001).
Timeline:
Fix a context-switch cost . A lock wait is described by its release time . An algorithm handling the wait chooses a blocking time : it spins until time and then blocks (: never block). The cost of the wait is
so a lock released exactly at the blocking time costs . The optimal off-line algorithm, which knows , pays .
An input is a finite sequence of lock waits. A deterministic on-line algorithm chooses the blocking time of wait as a function of , the release times it has already observed. Its cost is the sum of the wait costs, and the off-line cost is .
A randomized on-line algorithm is a probability distribution over deterministic on-line algorithms: a probability space and a deterministic algorithm for each , with measurable for every . Its expected cost is . Following §1 of the paper, is -competitive against an oblivious adversary if there is a constant with
The adversary is oblivious: it fixes before the algorithm's random choices are made.
The paper's algorithm blocks at a random time with cumulative distribution
where is the probability of blocking before time .
For every :
Theorem 10 settles the randomized competitive ratio of the continuous ski-rental problem: is achievable and cannot be improved by any on-line algorithm, randomized or not, against an oblivious adversary. The same constant is the limit of the paper's snoopy-caching ratios as the block size grows, and it recurs in randomized rent-or-buy problems and in on-line primal-dual analyses.
The result is proved in the literature, and the mission's work is to formalize it. The platform has related material but not this statement: Primal-Dual Online Algorithms I: Fractional Ski Rental proves a deterministic, fractional, discrete-day bound (PrimalDualOnline.SkiRental.fractional_competitive), which is a different model and contains no lower bound. A complete formalization produces a reusable model of randomized on-line algorithms with history-dependent decisions and an exact lower bound for them.
The upper bound per lock wait is an explicit computation. The difficulty lies elsewhere. First, the on-line algorithm is allowed to adapt to the release times of all previous waits, so a bound for a single wait does not by itself bound a sequence: the randomized algorithm must be assembled so that each wait is handled with the right blocking law, whatever happened before. Second, the lower bound is a statement about every randomized algorithm and must survive the additive constant : a single hard lock wait proves nothing, because absorbs any bounded loss. It has to be shown that on long sequences of waits every algorithm loses a factor on average. The natural first idea, to exhibit one bad release time for each algorithm, fails for randomized algorithms facing an oblivious adversary.
All objects live in the namespace NonuniformCompetitive.SpinBlock. Release times are ℝ≥0, blocking times ℝ≥0∞, wait costs ℝ≥0∞, and the off-line cost is real. Committed conventions:
Infrastructure a complete development needs: Lebesgue integrals of functions of a random variable (the layer-cake formula), interval integrals of the exponential, the construction of a probability measure on with a prescribed continuous distribution function, and a Yao-type averaging argument over finitely supported input distributions for the lower bound. The model of randomized on-line algorithms with history-dependent decisions is reusable for other rent-or-buy problems. Contributions welcome: proofs of the milestones, and intermediate lemmas such as the discretised lower bound for a fixed step .
A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression
on an interval . The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at and . Whether a boundary condition is needed at all depends on the behaviour of near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.
Let and . The coefficients satisfy: with ; real-valued; with . The Hilbert space is with .
A function is locally absolutely continuous, , if it is an indefinite integral of a locally integrable function on . The equation means that and its quasi-derivative both lie in and almost everywhere. A solution of , , is a complex-valued with in this sense. The maximal domain is
The modified Wronskian is , with no complex conjugation, and , likewise.
is limit circle (l.c.) at if there is a with and for some ; otherwise it is limit point (l.p.) at . The same holds at . A function is square integrable near if for some .
For every Sturm–Liouville expression as above,
and if is l.c. at , then for every all solutions of are square integrable near . The same two statements hold at .
The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator on a half-line needs a boundary condition at infinity, or whether with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of . Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh -functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.
The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.
The definition of limit circle refers only to and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all . The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for , and so only for nonreal in general. Extending the conclusion to real , where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.
SLData bundles EReal with (infinite endpoints allowed), , and the standing hypotheses (i)–(iii) of p. 181; pointwise on . is Lp ℂ 2 for the measure on .Classical.choose (it is unique on ). is with a local integrability clause. No smoothness of the coefficients and no solutions are assumed.Filter.limUnder along , inside . They are used only on , where milestone (9.7) states that the limits exist. In Lemma 9.7, where need not lie in , the boundary condition is stated as a convergence.LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph exists (i.e. is well defined) and is self-adjoint. and follow Teschl (2.66): a bounded two-sided inverse of . No projection-valued measure or functional calculus is used.A complete development needs a Carathéodory-type existence theorem for linear first-order systems with coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.
Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.
Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.
A finite Markov decision process has a finite nonempty set of states , a finite nonempty set of actions , transition probabilities (for each state and action , a probability distribution over next states ), a reward function with , and a discount factor . A stochastic policy gives, for each state , a probability distribution over actions.
The normalized value of from is , where , , ; it lies in . The state-action value is and the advantage is .
For a state distribution (a restart distribution), the discounted future state distribution is (eq. (2.1)), and the performance measure is .
The policy advantage of a policy with respect to and is
and . The conservative update (4.1) is with . An -greedy policy chooser (Definition 4.3) returns, for every policy , a policy with .
Conservative policy iteration (§5) starts from any policy and repeats: call to get ; form an -accurate estimate of from -restarts; if , stop and return ; otherwise apply (4.1) with and repeat.
With probability at least , conservative policy iteration (i) strictly improves with every policy update, (ii) stops after at most policy updates, and (iii) returns a policy with
The estimation step is represented by its guarantee: each reached loop's estimate fails to be -accurate with probability at most , .
Lemma 6.1 (p. 6), the performance difference identity:
Theorem 4.1 (p. 4), with and all :
Corollary 4.2 (p. 5): if , the step size gives
Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by , independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.
These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.
The obvious argument for the improvement bound expands to first order in ; that only gives with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, and are infinite discounted series, so summability, exchanges of sums and the identities and must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.
Policies are functions π : S → A → ℝ with π s a the paper's , and P s a s' is ; both are constrained by the published predicates IsPolicy and IsTransitionKernel. is times the published series PolicyValue, so values are normalized as in the paper. is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty and , a transition kernel, rewards in with , , and a state distribution . In Corollary 4.2, is any upper bound on the rewards rather than necessarily the attained maximum.
In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by . Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls once more than it updates, so "at most calls" is off by one. Second, the per-loop failure budget is , which covers the loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the -biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at , which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a -greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.
Pages are PDF pages; the paper has no printed page numbers.
A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.
A two-machine flow shop is the simplest multi-stage production system: every job visits machine 1 and then machine 2, each machine works on one job at a time, and the goal is to finish all jobs as early as possible. S. M. Johnson's 1954 paper (Naval Research Logistics Quarterly 1(1):61–68, doi:10.1002/nav.3800010110) answered this question, posed by R. Bellman, with an exact rule, now called Johnson's rule. It is one of the first exact results in machine scheduling. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) the problem is written . The rule is the standard polynomial case against which the NP-hardness of the three-machine flow shop (Garey, Johnson and Sethi 1976) is contrasted, and it is still used inside heuristics for larger shops.
Timeline:
There are items . Item needs units of time on machine 1 and then units on machine 2. Each time is setup time plus work time, and the times are otherwise arbitrary. A schedule assigns start times and . It is feasible when all start times are nonnegative, the intervals of distinct items do not overlap on machine 1, the intervals do not overlap on machine 2, and for every item. The total elapsed time is the time at which the last item leaves machine 2.
An order is a permutation , where is the item in position . The as-soon-as-possible schedule of an order processes the items in the order on both machines, with no delay on machine 1. Each item starts on machine 2 as soon as it has left machine 1 and machine 2 is free.
Relation (II). Item is definitely preferred to item when
and the two items are indifferent when equality holds. An order is consistent with all the definite preferences when no item is definitely preferred to an item placed earlier.
For an order the paper uses the quantities
For positive :
The comparison is against every feasible schedule, including those whose two machines follow different orders.
The theorem reduces an optimization over a continuum of start-time vectors, and over orders, to sorting with respect to a pairwise relation. The paper's working rule computes an optimal order in time. The two-machine rule is the building block of Johnson's three-machine result, of the Campbell–Dudek–Smith heuristic for machines, and of lower bounds in branch-and-bound methods for flow shops. The closed form reappears across flow-shop theory as a longest-path formula.
The result is classical and proved. This mission contributes a machine-checked proof in Lean 4 against Mathlib. As far as a search of the platform shows, no formal statement of the flow-shop model or of Johnson's rule exists there. The mission also fixes a reusable Lean model of a two-machine schedule: start times, feasibility, total elapsed time and the as-soon-as-possible schedule of an order.
The paper's argument leaves two steps informal, and a formal proof must supply both. First, Lemma 1 is justified by a picture and the phrase "successive interchanges". The page does not show that each interchange keeps the schedule feasible and does not delay the last completion on machine 2, and this is where most of the modelling work sits. Second, relation (II) is not a strict weak order when there are ties, so the obvious sorting argument fails. Consistency on adjacent pairs does not imply optimality: the items , in that order, satisfy (II) non-strictly on both adjacent pairs, yet take 13 units against an optimum of 10. Lemma 2's exception is exactly this case.
Items are Fin n (0-based) and times are real numbers. Positivity , is a hypothesis of the goal and of Lemma 1, the as-soon-as-possible step and the closed form, as on p. 61. Lemma 2 and the interchange statements are pure min/sum algebra and carry no positivity. An order is σ : Equiv.Perm (Fin n) with σ k the item in position k. Interchanging positions is σ * Equiv.swap j (j+1). The total elapsed time is Finset.univ.fold max 0 of the machine-2 completion times, so it is when . is indexed by 0-based positions (Lean's is the paper's ), and requires .
Conventions made explicit or corrected:
Measuring the objective by , or comparing only against schedules that follow one common order, would drop Lemma 1 and change the theorem. The goal compares against every feasible start-time schedule. The working rule of p. 64 (a procedure) is not formalized.
Proofs of any milestone are welcome, as are further lemmas about the as-soon-as-possible schedule and a formalization of the working rule. The schedule definitions are the basis for the three-machine mission of this series.
A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).
Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.
The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:
The chain is ergodic (assumption 2, p. 951): is irreducible, meaning every state can be reached from every other state with positive probability. may be periodic. A stationary probability vector is with , and ; denotes the matrix every row of which is .
The -step return of the policy is the recursion (I 16) without the maximization:
The system gain is (A 6), the bias after steps is , and the fundamental matrix is (A 7).
For every irreducible row-stochastic , stationary , rewards and terminal rewards : the matrix is invertible, and
This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.
In order: the stationary vector exists, is unique and positive, and (Appendix A); the increment identity (A 1) for constant ; the Cesàro limit of the increments (A 2); invertibility of and the relations , , ; the Cesàro summability of to ; the finite- bias formula (A 3) for constant ; the relative-value equations (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains , the policy is optimal for every with , the limiting biases are , and the relative values of (5) are and .
If is moreover primitive (aperiodic), itself converges to . This is included as a supporting statement.
The asymptotic is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.
The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of , its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.
The obvious argument writes and passes to the limit term by term. This fails for periodic chains: does not converge, does not tend to zero, and the series does not converge. The paper's own example ( swaps two states) is of this kind, and there oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of requires that be a simple eigenvalue of with left eigenvector , which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of , or a one-step Doeblin condition, is not available.
States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, ), which is unique by the first milestone. , and are definitions computed from , and , never free variables. Cesàro means are , equal to at . Mathlib's matrix inverse is on singular matrices, so the goal asserts invertibility of explicitly.
Two printed slips are corrected, and the milestone texts are kept verbatim:
The printed uses for the number of states .
A trivializing formalization is ruled out: is not a junk inverse (invertibility is part of the goal), is a genuine stationary probability vector of rather than an arbitrary vector, is computed from and , and the hypotheses are met by the paper's periodic two-state example.
Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem , and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.
In quantum mechanics an observable is a self-adjoint operator on a complex Hilbert space , and the dynamics is the Schrödinger equation . In finite dimensions the solution is the matrix exponential , computed by diagonalizing . The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to for every Borel function , in particular to and to the spectral projections .
The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.
Let be a complex Hilbert space, with inner product conjugate linear in the first argument, and let be the bounded operators on it. An (unbounded) operator is a linear map defined on a subspace ; means extends . is self-adjoint if is dense and , domains included.
The resolvent set of is the set of for which is a bijection with bounded inverse, and the spectrum is its complement, .
A projection-valued measure assigns to every Borel set an orthogonal projection such that and, for pairwise disjoint Borel sets , for every vector (strong, not norm, -additivity). Each gives the spectral measure , a finite Borel measure of total mass , and by polarization the complex measures .
For a bounded Borel function the operator is the bounded operator with for all . For an arbitrary Borel function it is the operator with domain
and for . An operator is normal if it is densely defined, and on .
For every self-adjoint operator in there is a unique projection-valued measure with
an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.
A further supporting statement (not a milestone) records that is a finite measure with .
The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution , the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about or . Theorem 3.8 identifies the spectrum with the support of , which is what makes spectral questions accessible to measure theory.
Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of -algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object that every later mission of this series currently has to take as data.
The obvious route through the bounded case fails. For bounded self-adjoint one can build from polynomials by the sup norm on and extend by monotone limits; for unbounded there are no polynomials in defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform , or the bounded resolvent ) produce bounded normal operators whose spectral measures must then be transported back, and the domain must be recovered exactly as ; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections are not given by any formula in that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator alone.
is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from . The spectral integral spectralIntegral P f is the operator with domain and quadratic form (the predicate IsSpectralIntegral), selected by choice; its existence for Borel is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in . The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly .
Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with " given as a hypothesis, and is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of as the only hypothesis.
Lemma 3.4 (spectral bases), Lemma 3.6 (the family built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, , monotonicity), and of alternative proofs of the goal are welcome.
Many controlled systems do not move in unit time steps. A machine runs for a random time before it breaks down, a repair takes a random time, a queue sits in a state until the next arrival or departure. A Markov-renewal program (in later terminology a semi-Markov decision process) models such a system: the sequence of visited states is a Markov chain controlled by the decision maker, but each transition takes a random time and earns a reward that may depend on that time. When the horizon is long and rewards are not discounted, the natural criterion is the gain rate, the long-run expected reward per unit of time, not per transition.
Howard's policy-iteration algorithm (Howard 1960) finds a policy of maximal gain per transition for finite Markov decision processes. W. S. Jewell's Markov-Renewal Programming. II (Oper. Res. 11 (1963) 949–971) extends it to the time-average criterion. The paper's Fig. 2 gives the algorithm; pp. 954–955 state its claim: the algorithm "will find an optimal stationary policy for the infinite-time, undiscounted model, in the sense that the policy will have a gain rate, , which is at least as large as that obtained for any other policy". Appendix D compares Jewell's test quantity with an alternative one proposed by P. Schweitzer, and states the identity (D 3) that measures the gain-rate improvement produced by either.
Timeline. Howard (1960) introduced policy iteration for the per-transition gain of finite Markov decision processes, and sketched a semi-Markov version. Jewell (1963, Parts I and II) developed Markov-renewal programming, with the ratio test quantity of Fig. 2 for the undiscounted time-average case. Schweitzer (unpublished MIT report, cited in Appendix D) proposed the test quantity (D 1). The ratio criterion was later treated systematically for semi-Markov decision processes (e.g. Puterman 1994, Ch. 11).
There are finitely many states and, in each state, finitely many alternatives . Under alternative in state the next state is with probability (, ). The transition takes a random time with finite mean , and the transition out of earns an expected reward . The mean sojourn time is , and it is positive.
A stationary policy picks one alternative in each state. Its chain has transition matrix , and , denote the data of . The paper's standing assumption 2 is that this chain is ergodic (irreducible) for every policy. Let be the stationary probability vector of (, , ). The gain rate of is (B 7):
The value-determination equations (13) of are, in the unknowns ,
The test quantity of Fig. 2 for alternative in state is . One cycle of the algorithm solves (13) for the current policy and then chooses, in every state, an alternative that maximizes the test quantity, retaining the current alternative when it already attains the maximum. The algorithm stops when the policy does not change.
For every run of the algorithm, from any initial policy and with any choice among tied maximizers, there is with ; and whenever , is the gain rate of and, for every stationary policy ,
The result makes the time-average criterion computable: a finite sequence of linear solves and pointwise maximizations produces a policy whose reward per unit time is optimal among all stationary policies. The identity (D 3) is the quantitative content: it expresses the gain-rate change as an average of local improvements, weighted by the fraction of time the new policy spends in each state. Both test quantities, Jewell's (D 2) and Schweitzer's (D 1), are covered by it. When every the model is a Markov decision process and the algorithm is Howard's.
The result is classical and has textbook proofs for semi-Markov decision processes. The paper states the proof as "elementary" and does not write it out. None of it is machine-checked on Prove2Me, and no semi-Markov or ratio-criterion result is on the platform. The mission produces a checked account of value determination for irreducible finite chains, the improvement identity, and termination of policy iteration under ties.
The gain rate is a ratio, so the per-transition argument for Markov decision processes does not transfer by rescaling rewards: the denominator changes with the policy. Comparing two policies requires weighting local improvements by the new policy's time-stationary probabilities, and a strict improvement needs those probabilities to be positive in every state, which uses irreducibility of the new policy, not only of the current one. Termination rests on the retain-on-tie rule: without it the algorithm can cycle among tied maximizers without improving. Finally, (13) has unknowns and equations only because of the normalization ; its unique solvability is a statement about the kernel and range of for an irreducible stochastic .
States are Fin N with NeZero N; the paper's state is index (lastState N). Alternatives form a type α; the goal assumes Fintype α and Nonempty α. The model records only , and , with as a field. The transition-time distributions and reward functions of the paper enter the undiscounted infinite-time model only through these means, and every such choice of means is realized by some distributions, so nothing is lost. Ergodicity is Matrix.IsIrreducible of the policy matrix for every policy. Stationary vectors are nonnegative, sum to one and satisfy ; every statement quantifies over all of them.
The gain rate is defined by its closed form (B 7). Its identification with ((B 6), argued in Appendix B from renewal theory) is not part of the mission. (13) is stated with the full sum , equal to the paper's because . The paper states (D 3) for a policy "which led to an improved policy "; the identity holds for any two policies and is stated that way. A run of the algorithm is a relation, not a chosen argmax: the goal quantifies over every run, so the termination claim cannot be met by a particular tie-breaking. A run begins at an arbitrary policy; the "initial set of returns" entry of Fig. 2 is a run started one cycle later.
A formalization in which the improvement step already asserts optimality, or in which termination is assumed, would be trivial; here the step only asks for pointwise maximization of the test quantity, and termination is part of the conclusion.
Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, uniqueness, strict positivity), the kernel of , and finite-policy termination arguments. These are reusable for any finite Markov decision or semi-Markov model. Proofs of any milestone, and of the specialization, are welcome.
Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written , is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.
Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):
This mission formalizes the result, the paper's main theorem.
There are jobs . Job has an integral processing time , an integral release date and a weight . The jobs are indexed so that .
The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in it runs the smallest-index job with and work left, or idles. Let be the set of times at which it processes . The mean busy time of is
The mean busy time relaxation (R) has a variable per job:
with and . is a lower bound on the optimum of .
For the -point is the first time at which has been processed for units in the LP schedule; is the start time of . For a vector , the -schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of ; is the completion time of in it.
Let be the solution in of , and set
, and if each have density and are pairwise independent, then is integrable and
The bound is against the constant defined by the formula; the decimal appears only in the separate inequality .
Theorem 3.9 gives a randomized algorithm for whose expected cost is at most times the optimum, and a variant of it runs on-line (Theorem 3.14). Since is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach , so the bound is not far from what this relaxation can give.
The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, -points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of -point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average -points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later -point analyses.
The obvious argument, bounding by Corollary 3.2 and integrating each independently against , does not work directly: the set of jobs with depends on , and the two effects of the random pull in opposite directions (a small shrinks the terms , a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job (equations (3.9)–(3.11)) to separate the jobs whose is constant in from those for which it jumps from to , and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, -points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of , conditioning under pairwise independence) is real work.
Jobs are Fin n (0-based), and are natural numbers and is real. The ordering by is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. is an infimum over times, , and the -schedule is the closed form of list scheduling in lexicographic (α-point, index) order. is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for . The random vector is any probability measure on whose coordinate laws all equal the law with density and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. is any solution in of its equation.
A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral ), is supported on so every lies in almost surely, and the bound is against defined from (R), not against an expression that already contains Theorem 2.5.
Running times (, ), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary -Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the -schedule.
Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and -points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on .
Minimizing the total weighted completion time of jobs with release dates on a single machine, written in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using -points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing at random improves the guarantee.
Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random . This mission formalizes their Theorem 3.5: when a single is drawn from a truncated exponential density, the resulting schedule costs in expectation at most times the LP lower bound.
Timeline:
There are jobs . Job has an integral processing time , an integral release date and a weight . The jobs are indexed so that .
A preemptive schedule gives each job a set of processing times of measure , the sets pairwise disjoint. The mean busy time of is .
The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio . Its mean busy times are .
The mean busy time relaxation (R) minimizes subject to for every nonempty , where and . Its optimal value is , a lower bound on the optimum of .
For , the -point is the first time at which has received units of processing in the LP schedule, and is its start time. The -schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of ; is the completion time of in it. More generally, the -schedule orders the jobs by for a vector .
Let solve (), and set
If is drawn with density , then , the expectation below is finite, and
Theorem 3.5 is a randomized -approximation for , and simultaneously a bound on the integrality gap of (R): every instance has . The paper also derandomizes it: there are at most distinct -schedules (its Proposition 3.8), and the best of them can be found in time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.
On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, -points and list scheduling, and the first machine-checked instance of the -point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.
The obvious approach, bounding each separately by a multiple of , gives only the factor for fixed (Theorem 3.3 of the paper), which is at least . The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt () and which do not (), and how the fraction of each other job depends on . Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines .
Jobs are Fin n (0-based) with and real weights. The sortedness for , positivity and are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals ; a job's processing set is a finite union of such intervals. -points are infima over reals, and every statement restricts to . The -schedule's completion times are given by the closed form of list scheduling, , with ties of -points broken by index (they do not occur for ). is the infimum of the objective of (R) over its feasible set. The random has law on , and the expectation is a Lebesgue integral.
The goal asserts integrability of together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral . The bound is against defined from (R), not against , which would build Theorem 2.5 into the goal; and the density's support is written out, so no mass is placed outside . The running-time claims are not formalized, and the uniqueness of is not asserted: the statements hold for every solution in .
Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.