Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an -digit integer in time polynomial in (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given coprime to , find the least with . The quantum part solves order finding.
This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads off the measured value. The paper's claim is that one run of this procedure returns with probability at least .
Timeline:
Fix an integer and an integer coprime to . Its order is the least with ; since is a unit, . Let be the power of with .
A quantum state on two registers, the first holding and the second a residue , is a complex vector indexed by the basis states . Measuring it returns with probability .
The Fourier matrix is the matrix with entries , with rows indexing inputs and columns outputs. The algorithm
The observed gives us if some fraction with lowest-terms denominator below is within of , and every such fraction has lowest-terms denominator exactly . In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.
For all sufficiently large , with , and as above,
where is the state (5.4). The threshold on is uniform in and ; it is the paper's "for sufficiently large " from the per-state bound.
The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since for a constant (Hardy and Wright, Thm. 328), repetitions find with high probability, and Miller's reduction then factors . Without the bound, the algorithm is a procedure with no guarantee.
The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of and his constants, starting from the state built by applying to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where divides and the output is uniform on peaks, but that model removes the approximation that the bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.
The obvious route is to compute the output distribution in closed form. That works only when divides ; here is a power of and is arbitrary, so the amplitudes are geometric sums of terms whose phases do not cancel exactly. The per-state bound requires a lower bound on such a sum that is uniform in , and , with error terms of order controlled against a main term of order . The constant leaves only a small margin below the limiting value , so the errors must be bounded explicitly, not merely shown to vanish.
The second difficulty is the counting: distinct coprime numerators must give distinct outcomes in , and each good must determine uniquely, which uses and .
Conventions the statements commit to:
Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying to the first register gives the amplitude at .orderOf (x : ZMod n). enters through the three hypotheses , , , not through a function of .Rat.den.Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.
Not stated: the polynomial running time of any step, the repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod are reusable in the companion discrete logarithm mission.
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.
The Smale horseshoe is the standard example of a smooth invertible map of the plane with chaotic dynamics. Smale introduced it in the 1960s as the mechanism behind the complicated orbits near a transverse homoclinic point, and it became the basic model of hyperbolic invariant sets (Smale 1967). Its importance for differential equations is the Smale–Birkhoff theorem: whenever the stable and unstable manifolds of a hyperbolic fixed point intersect transversally, some iterate of the map contains a horseshoe. Melnikov's method then turns this into a checkable criterion for chaos in periodically forced planar systems such as Duffing's equation.
This mission formalizes the horseshoe as it is treated in Chapter 13 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012). It takes along the one-dimensional results from §§11.4–11.5 that the chapter's argument reuses: the tent map's Cantor set, the one-sided shift, and the metric on two-sided sequences.
Fix parameters and and let . The two horizontal strips
are mapped by
Each strip is contracted horizontally by and stretched vertically by into a vertical strip crossing . The book specifies only on and leaves the fold between them to a picture. A horseshoe map here is any given by these formulas on . On and the inverse is given by explicit formulas.
The tent map on has the invariant set
The second coordinate of is and the first coordinate of is . The horseshoe's invariant set is
The two-sided shift space is . It carries the metric
and the shift . The itinerary of a point of records, for , which strip contains . For it records which strip contains .
A system is chaotic in the book's sense (p. 296) under four conditions: is continuous, is infinite, is topologically transitive (for nonempty open some meets ), and the periodic points are dense. A Cantor set is a compact, perfect, totally disconnected set.
For , and every horseshoe map :
The book's sentence is: "The Smale horseshoe map has an invariant Cantor set on which the dynamics is equivalent to the double sided shift on two symbols. In particular it is chaotic."
Theorem 13.1 exhibits a two-dimensional invertible system with an explicit invariant set on which the dynamics is exactly the two-sided shift. Every property of the shift is then inherited:
Theorem 13.1 is the model to which the Smale–Birkhoff theorem (13.2) reduces the dynamics near a transverse homoclinic point. It is therefore the terminal object of the book's route from Melnikov integrals to chaos in forced oscillators.
The results are classical and fully proved in the literature. Their proofs have not been formalized. Mathlib has Cantor-type sets (the middle-thirds set), totally disconnected and perfect sets, and product topologies. It has no tent-map invariant set, no two-sided symbolic dynamics with the book's metric, and no conjugacy theorem of this kind. A formal proof would supply a machine-checked conjugacy between a concrete planar map and a full shift, together with the symbolic-dynamics layer it rests on.
The book's own argument for Theorem 13.1 has two gaps that a formal proof must fill. First, it asserts that a product of two Cantor sets is again a Cantor set and leaves this as an exercise. Second, it treats continuity of the itinerary map and of its inverse as an exercise. It also leans on "all other results hold with no further modifications" to transfer the one-sided lemmas (11.7–11.9) to the two-sided shift.
The two-sided transfer is not literally a restatement. The metric (11.35) weights each off-centre index by , and so the one-sided closeness estimate does not carry over verbatim; see the correction to Lemma 11.15 below.
The inverse must also be tracked alongside . The negative half of the itinerary is defined through rather than through , so the conjugacy at index couples the two halves.
Finally, the parameter endpoints need care. The book allows and . At the defining formulas are inconsistent on , and at either endpoint one factor of is the whole interval .
IsHorseshoeMap λ μ F is a predicate fixing only on , and the goal quantifies over all such . Its conclusion therefore cannot depend on how the fold is drawn. The inverse horseshoeInv is the explicit formula (13.5)–(13.6).ℝ × ℝ; its max-distance has the Euclidean topology. Sequence spaces are ℕ → Fin N and ℤ → Fin N. The metrics (11.28) and (11.35) are functions symDist and symDistZ, not type-class instances. Density and continuity are stated in – form against them, so no unmentioned product topology enters.Preperfect and IsTotallySeparated, the last being the book's definition of total disconnectedness on p. 302. is constructed as in (13.8) and as in (13.9), not quantified over. The goal asserts the full conjunction, so it cannot be discharged by exhibiting some other invariant set or some other conjugacy. For maps satisfying IsHorseshoeMap exist, so the hypothesis is not vacuous.
A complete development needs:
The tent-map and one-sided shift lemmas duplicate those of the interval-maps mission of this series and are reusable there. Contributions proving the two-sided analogues of Lemmas 11.7–11.9 as auxiliary lemmas are welcome.
Periodic solutions are the simplest non-stationary long-time behaviour of an autonomous system : limit cycles in oscillators and population models, closed orbits of conservative systems. The first question about a periodic orbit is whether it is stable. Poincaré introduced the first-return map on a transversal section, which turns this question into a question about a fixed point of a map in one dimension less. Floquet theory attacks the same question through the linear periodic system obtained by linearizing along the orbit. This mission formalizes Chapter 12, §§12.1–12.2 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version, DOI of the published book). That chapter proves the two approaches agree and derives the standard stability and persistence criteria from this.
Let be open, with , and let be the flow of with maximal intervals : is the unique maximal solution with . A point is periodic with period if and for . Its orbit is then a closed curve.
Linearization along the orbit. Put , a -periodic matrix. The first variational equation is , and denotes its principal matrix solution: , . The monodromy matrix based at is
The Poincaré map. A transversal section is with open, , and on . If there is a return time near with and . The Poincaré map is
Its derivative is a linear map of the -dimensional tangent space into itself.
Stability. The orbit is stable if every neighborhood of contains a neighborhood of from which solutions stay in for all . It is asymptotically stable if moreover for all in some neighborhood of . A periodic orbit is hyperbolic if has no eigenvalue on the unit circle.
For every ,
where is the characteristic polynomial. So the eigenvalues of together with the single value are exactly the eigenvalues of the monodromy matrix, with multiplicities. In particular they depend neither on the section nor on the base point on the orbit.
The result. Theorem 12.4 is the bridge between the two standard tools for periodic orbits. The Floquet multipliers of can often be computed or estimated, for instance through Liouville's formula . The Poincaré map is where the dynamics is decided, for instance through the fixed-point stability theory of maps. Corollaries 12.3 and 12.5 and Lemma 12.6 are the resulting stability tests. Lemma 12.7 is the structural-stability statement for hyperbolic orbits that bifurcation theory starts from. Theorems 12.8–12.10 (stable manifolds of periodic orbits) build on the same objects.
Formalizing it. All results are classical and proved in the book. None has a machine-checked proof on the platform or, as far as is known, in Mathlib, which has neither Poincaré maps nor the linearization of flows along orbits. The work is a formalization of the known proofs. It needs differentiability of the flow with respect to initial conditions, and that part is reusable across the whole of qualitative ODE theory.
The algebra of Theorem 12.4 is short. The two linear maps act on different spaces: on , and on the hyperplane . That hyperplane is in general not orthogonal to , not a coordinate hyperplane, and not invariant under . Any comparison has to go through the derivative of , which involves the derivative of the implicitly defined return time. Behind all this sits the differentiability of in and the variational equation it satisfies, which Mathlib does not provide for local flows. For the stability milestones, the delicate step is passing from the discrete iterates of on back to the continuous flow near the whole orbit. That requires uniform control over one period.
The state space is Fin n → ℝ. Norm-dependent notions (distance to the orbit, neighborhoods) do not depend on the choice of norm. The flow is local: IsMaximalFlow f M I Φ characterizes and by maximality and uniqueness, and 's values outside its domain are never used. Derivatives are Mathlib's fderiv. The section is the book's general with , not a hyperplane chosen orthogonal to . The return time is any function on a neighborhood of with and ; such a function agrees with the book's near . is an endomorphism L of LinearMap.ker (fderiv ℝ S x₀) that agrees with the derivative of there (IsPoincareDerivative). Theorems 12.4 and 12.5 assert that it exists. Eigenvalues are complex roots of characteristic polynomials.
Conventions and readings:
Needed infrastructure: existence, uniqueness and dependence on initial conditions for local flows; the implicit function theorem (Mathlib); characteristic polynomials and determinants of endomorphisms of finite-dimensional subspaces (Mathlib); Liouville's formula; stability of fixed points of maps with contracting linearization. Contributions of any of these as standalone lemmas are welcome.
Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each – matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.
Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without or minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.
All sets are finite. A clutter is a finite collection of finite sets, no member of which is contained in another; and are the two trivial clutters. Its ground set is . The blocker is the collection of minimal subsets of that meet every member of , and is the minimum cardinality of a member of .
is Mengerian if , or if for every weight map there is an integral packing with for each and
For a set , the deletion is and the contraction is the collection of minimal members of (minimal, not minimal nonempty). A minor of is any clutter obtained by a finite sequence of deletions and contractions.
A clutter is binary if is odd for all and ; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally
the triangles of with its edges labelled .
For the structure theory, a circuit of a binary clutter is a minimal nonempty with even for every ; and are parallel when is a circuit, and the point is the parallel class of . With , is critical if . In a critical binary clutter, means that every member of containing contains while , and is initial if no has . MBC abbreviates "Mengerian binary clutter".
For every binary clutter ,
In the order the proof uses them:
The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system , has integral optimal primal and dual solutions for every integral cost vector, and it identifies as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid the port is Mengerian for every element if and only if is binary and has no minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining to or to is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).
The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.
The "only if" direction is short: minors of Mengerian clutters are Mengerian, and fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a -free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.
Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, is the union of members, and deletion and contraction take an arbitrary finite set . Weights and packings are -valued. The minimum in the Mengerian condition is expressed as "some of least weight has weight equal to the packing value", never as an infimum. is Mengerian by the paper's convention, and , which the paper leaves undefined, has the junk value in Lean; every item reading excludes or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a minor" means that some minor equals the image of (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.
Four readings would change the theorem and are ruled out: real-valued packings (the weak max-flow min-cut property, which has, so the goal would be false), a non-minimal blocker or one not restricted to , dropping the exception, and reading " minor" as literal equality instead of isomorphism.
A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation . The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts , (2.1) and (2.2), and of the equivalences in (3.2) are welcome.
The quantum harmonic oscillator is the Schrödinger operator of a particle in a quadratic potential. It describes small vibrations around an equilibrium, the modes of the electromagnetic field, and phonons in a crystal. It is also one of the very few Schrödinger operators whose spectrum and eigenfunctions are known in closed form. The eigenvalues are equally spaced, and the eigenfunctions are Hermite functions. Its algebraic treatment by creation and annihilation operators goes back to Dirac (The Principles of Quantum Mechanics, 1930). That treatment became the template for second quantization and Fock space.
The same chapter of G. Teschl's Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009, Chapter 8, AMS page) contains two further results that use commutation relations. The first is the Heisenberg uncertainty principle (Heisenberg 1927; the general form for two observables is due to Robertson, Phys. Rev. 34 (1929)). The second is an abstract statement that and have the same spectrum away from . Physicists call this supersymmetric quantum mechanics, and Teschl uses it later for the hydrogen atom. This mission follows Teschl's Sections 8.1–8.4.
Let be a complex Hilbert space. A linear operator is a linear map defined on a subspace , its domain. is symmetric if is dense and for all . For a closed operator and , the resolvent exists when maps bijectively onto with a bounded inverse. The resolvent set is the set of such , and the spectrum is . An operator is essentially self-adjoint on its domain if its closure is self-adjoint.
For with (a state), the expectation is and the mean-square deviation is . The commutator is for , where .
Fix a frequency . On with Lebesgue measure, let
where and is the Euclidean norm. With and Teschl's units (, mass , so the free Hamiltonian is ), the harmonic oscillator is the operator
In one dimension the ladder operators on are
The Hermite polynomials are . The Hermite functions are
and on , .
For every the operator above exists. It is essentially self-adjoint on , the functions , , form an orthonormal basis of consisting of eigenvectors of , and
with equality if for a real , or if is an eigenvector of or .
The last two milestones do not enter the goal. They are the chapter's other two theorems and use the same operator-theoretic layer.
Theorem 8.5 is the rigorous form of the most used exactly solvable model of quantum mechanics. Once it is available, the Hermite functions become an orthonormal basis of that diagonalizes a concrete differential operator. That basis underlies Mehler's formula and the Fourier transform's action (Eq. (8.46)). Perturbation arguments around the oscillator also start from it, and so does the construction of Fock space. The uncertainty principle is the basic quantitative constraint on simultaneous measurement. Theorem 8.6 gives an eigenvalue transfer mechanism that Teschl reuses to compute the hydrogen spectrum (Section 10.4).
Formally, the mission asks for a machine-checked proof about an unbounded differential operator on , stated on a concrete core. Mathlib has unbounded operators (LinearPMap, closure, adjoint), spaces, Gaussian integrals and the probabilists' Hermite polynomials. It has no statement identifying the spectrum of a concrete Schrödinger operator. These results are proved in every textbook, but none of them has been formalized in this form.
The algebra of Eqs. (8.36)–(8.41) is a finite computation with polynomials times a Gaussian. The work in the goal is analytic. Essential self-adjointness is a statement about the closure of an operator on a non-closed domain. Symmetry of together with a family of eigenvectors in does not give it by definition, and the relevant criterion for unbounded operators is not in Mathlib. Completeness of the eigenfunctions in is a density statement about a concrete function space (Lemma 8.3), and it has to be transferred from one dimension to three. The spectrum is asked for the closure , not for on : the eigenvalues are easy to exhibit, but showing that no other point of lies in requires control of on all of . Finally, the Rodrigues formula (8.42) and the ladder construction (8.40) define the same functions only after an identity for all derivatives of .
is a complex inner product space with CompleteSpace; separability is not assumed, and no statement needs it. Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H. is LinearPMap.adjoint, and every statement using it assumes a dense domain. Self-adjointness is Mathlib's IsSelfAdjoint, and essential self-adjointness is IsSelfAdjoint H.closure. and are defined in the mission for LinearPMaps (bounded two-sided inverse of ); Mathlib's Banach-algebra spectrum is not used. is Lp ℂ 2 volume on EuclideanSpace ℝ (Fin n). The Laplacian is the sum of second Fréchet derivatives along the unit vectors. Hermite polynomials are defined by the Rodrigues formula, not as Mathlib's probabilists' Polynomial.hermite. No projection-valued measure, functional calculus or Fourier transform is taken as data.
The oscillator is not defined as a construction. IsHarmonicOscillator ω H states that and that acts on a representative as . This determines uniquely, and the goal also asserts that such an exists. Trivializing formalization ruled out: defining as the diagonal operator would make the spectrum immediate. Here is the differential operator on , and its eigenvalues must be derived.
Two choices differ from the printed text. First, Teschl's (8.34) writes the domain with , but his (8.39)–(8.41) and the conclusion use . The mission uses , which equals (8.34) for . Lemma 8.3 is stated for (8.20)'s itself. Second, Theorem 8.6 prints "", and the mission states the intended . The uncertainty principle adds explicitly; the book assumes it through its definition of a state.
Reusable pieces are the product of LinearPMaps, spectrum and resolvent for unbounded operators, the Gauss–polynomial core and its density, and the Hermite-function API. Contributions of general lemmas are welcome, for example "an operator with an orthonormal eigenbasis in its domain is essentially self-adjoint" and the spectrum of such an operator.
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.
Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.
Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor . Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.
There are tasks and agents. The type of agent is the vector of positive numbers, being the least time in which agent can perform task . An allocation gives each task to one agent; is the set of tasks of agent . For a type vector and for a vector of actual execution times the make-spans are
A mechanism with verification is a pair . The allocation is computed from the agents' declarations only. Each agent then performs its tasks, in any times it chooses, and the mechanism pays agent the amount , which may depend on the declarations and on the observed actual times. Agent 's utility is . A strategy of agent therefore has two parts: a declaration and an execution plan that says, for every allocation, how long the agent takes on each of its tasks.
A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.
The Compensation-and-Bonus mechanism uses an optimal allocation algorithm and pays
where the corrected time vector lists agent 's own tasks at their actual times and every other task at the time declared by the agent it was given to.
For agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:
For there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.
The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).
Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).
Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent 's slower execution only hurts it when agent is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.
Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).>=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes for .Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.
Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.
The paper's test case is task scheduling on unrelated machines: tasks must be assigned to agents, agent needs time for task , and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio , and no mechanism achieves a ratio below (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio .
Timeline.
There are two agents, and , and tasks. A type vector gives, for each agent and task , the positive time agent needs for task . An allocation assigns each task to one agent; is the set of tasks of agent . The make-span of is
A direct mechanism receives declared types and returns an allocation and payments handed to the agents. Agent with true type gets utility . The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.
A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.
The biased min work mechanism with parameters and treats each task separately. With the favoured agent and the other: if , task goes to , who is paid ; otherwise it goes to , who is paid . The randomly biased min work mechanism draws uniformly from and uses . Its expected make-span is
For every : the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector and every allocation ,
The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: against the deterministic lower bound of . The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.
Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to " by , and under the mechanism's tie rule a task with ratio exactly is allocated by the coin rather than to the efficient agent.
Fin 2 (agent is 0, agent is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every , including .Finset.sup') over the two agents. The expected make-span is the average over all vectors , which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.
Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most against the optimum, and that no truthful mechanism can do better than a factor . It then conjectures (Conjecture 4.9) that the factor cannot be improved by any truthful mechanism.
That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from to (Christodoulou, Koutsoupias and Vidali), to (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).
There are tasks and agents . A type vector records, for every agent and task , the positive time agent needs for task . An allocation assigns every task to one agent; is the set of tasks of agent . For a set of tasks write . The make-span of is .
A direct mechanism asks every agent for its type, computes an allocation from the declarations, and hands agent the payment . Agent 's utility is measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a -approximation if for every type vector and every allocation .
For a truthful mechanism the payment to agent depends only on the set it receives and on the declarations of the others (Proposition 4.4). This gives the price offered to agent for a set (Definition 12):
A mechanism is local (Definition 14) if depends only on the other agents' times on the tasks of . MinWork is local: its price for is .
For every , every and every real , no truthful local mechanism is a -approximation:
The bound holds for every , so together with MinWork it shows that is the exact best ratio for local truthful mechanisms.
The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio must use prices that depend on the other agents' times on tasks outside the bundle.
Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.
An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price . Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.
Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).
Conventions and explicit thresholds:
Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every , not for some.
Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.
One-dimensional maps are the smallest systems in which deterministic dynamics becomes unpredictable. Chapter 11 of Gerald Teschl's graduate text Ordinary Differential Equations and Dynamical Systems (author's version; AMS Graduate Studies in Mathematics 140, 2012, doi:10.1090/gsm/140) uses them to make the word "chaos" precise. The chapter proves that a period-three orbit of a continuous interval map forces orbits of every period (Li and Yorke, 1975, the first case of Sarkovskii's theorem), adopts Devaney's topological definition of chaos, codes the tent map by sequences of two symbols, and ends by computing the Hausdorff dimension of the tent map's invariant Cantor set. The same pattern (a Cantor set, a conjugacy to a shift, a fractal dimension) returns in the Smale horseshoe of Chapter 13 and in hyperbolic dynamics generally, so the chapter is the standard entry point to symbolic dynamics.
For a real parameter the tent map is , a map of the real line. For the peak exceeds , points leave and then escape to . The repellor of the tent map is the set of points that never leave,
which the book builds as a nested intersection of intervals of length ; for it is all of . With and , the itinerary map sends to the sequence with when .
The sequence space , , carries the metric and the shift .
A continuous map of a metric space is topologically transitive if for all nonempty open some iterate , , meets . It is chaotic if in addition is infinite and the periodic points of are dense. This is the definition used in the book, and it has no sensitivity clause. It has sensitive dependence on initial conditions if some has the property that every has points arbitrarily close to it with for some . A compact set with is repelling if some neighborhood of is eventually left by every orbit starting in . A repelling set is a repellor if is transitive. It is a strange repellor if moreover is chaotic and is fractal, meaning its Hausdorff dimension is not an integer. A Cantor set is a compact, totally disconnected, perfect set.
The book states the strange-repellor clause for . At , however, has dimension , which is an integer, so the goal restricts that clause to .
The dimension formula is the simplest non-trivial instance of the principle that the Hausdorff dimension of an expanding repellor is determined by the number of branches and the expansion rate. For conformal repellors this principle becomes Bowen's formula. Theorem 11.23 of the same chapter extends the bound to general two-branch expanding interval maps, with . The conjugacy with the full shift is the device that reduces the dynamics on to combinatorics of sequences. It is reused verbatim for the horseshoe.
On formalization: Mathlib has Hausdorff measure and dimension (MeasureTheory.Measure.hausdorffMeasure, dimH) together with Hölder and Lipschitz image bounds. It has no dimension computation for a self-similar Cantor set and no symbolic-dynamics layer. On Prove2Me, the Devaney series proves period three implies all periods and Sarkovskii's theorem for continuous maps , the density of periodic points and a dense orbit for the two-symbol shift, and a Cantor-set statement for the quadratic family. None of these states the results for self-maps of a compact interval, for symbols, or for the tent map, and none computes a Hausdorff dimension. All results here are proved in the book, except that the proof of Theorem 11.20 is terse. None is formalized in the form stated here.
The upper bound comes from the natural covers. The lower bound is the hard direction: it has to hold for every cover, including covers by sets of very different sizes that do not line up with the construction intervals. So the natural covers alone do not decide it. Counting the construction intervals that an arbitrary set of a given diameter can meet needs the gaps between them to be controlled uniformly. The heuristic self-similarity identity fixes only once is known, and that is exactly what has to be proved. For the strange-repellor clause, every part of the definition (repelling, transitive, infinite, dense periodic points, fractal) has to be checked for with the subspace topology. Transferring transitivity and density of periodic points from requires the homeomorphism of Theorem 11.5 in both directions, not just a continuous surjection. In Lemma 11.1 the difficulty is showing that the periodic point found has prime period , not a divisor of .
Everything is stated in namespace TeschlODE.IntervalMaps against Mathlib.
ℕ → Fin N, and the metric (11.28) is a function symDist N (a tsum, summable for ). Density and continuity on are stated in explicit – form with this function. Each theorem assumes , the book's .ℝ → (ℕ → Fin 2). Its values off are meaningless and never used. "Homeomorphism" in Theorem 11.5 means: is a bijection of onto , it is continuous on , and its inverse is continuous, all in metric form.Function.periodicPts, and the prime period in Lemma 11.1 is Function.minimalPeriod on the subtype .dimH, valued in . "Not an integer" means finite and different from every natural number. The goal's right-hand side is ENNReal.ofReal (log 2 / log μ).There are no "sufficiently small" or readings in this chapter. The only quantifier choices are the explicit – forms above and the nonempty open sets in transitivity.
The goal is not a dimension-only statement. For , a statement that proved only (11.49), or that restricted to a single value such as , would be a different and weaker theorem. The full strange-repellor conclusion, with every clause of the definition, is required. Solvers can reuse the symbolic-dynamics lemmas (11.6, 11.8, 11.9) and the conjugacy (11.5). General Mathlib contributions on as a metric space are welcome.
Algorithms deployed on the Internet often take their inputs from parties who own them and who may lie when lying pays. Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) proposed studying optimization problems in this setting: the algorithm designer may hand out payments, and must guarantee that the intended output is produced when every participant acts in its own interest. The paper's central test case is scheduling on unrelated machines, a standard problem of combinatorial optimization, in which the machines are the selfish participants and only they know how long each job takes them.
For this problem the paper shows that incentives cost a factor of two at least: with two or more machines, no mechanism can guarantee a make-span below twice the optimum. This was the first lower bound separating what incentive-compatible mechanisms can achieve from what ordinary approximation algorithms can achieve, and it started a line of work on the "Nisan–Ronen conjecture" (that the right factor for machines is ), with improved lower bounds by Christodoulou, Koutsoupias and Vidali (Algorithmica, 2009) and by Koutsoupias and Vidali (Algorithmica, 2013), and a resolution announced by Christodoulou, Koutsoupias and Kovács (STOC 2023).
There are agents (machines) and tasks . Agent 's private type is the vector of positive real numbers, being the time agent needs for task ; a type vector is . An allocation assigns every task to one agent; is the set of tasks given to agent . For a set of tasks write . The objective is the make-span
and an allocation rule is a -approximation if its make-span is at most times that of every allocation, on every type vector.
A mechanism gives each agent a set of strategies. On a strategy profile it outputs an allocation and hands agent a payment . An agent of type has utility . A strategy is dominant if it maximizes the agent's utility whatever the others play. The mechanism implements a -approximation if every agent of every type has a dominant strategy and every profile of dominant strategies yields a -approximate allocation.
A direct mechanism has equal to the set of types, and is truthful if reporting the true type is dominant. For a truthful mechanism, the price is the payment agent receives when, against the others' reports , some report of its own makes it receive exactly (and if none does); the price difference is .
For every , and , no mechanism with any strategy sets implements a -approximation:
The result. Theorem 4.6 shows that the requirement of dominant-strategy incentive compatibility, by itself, rules out approximation ratios below for scheduling on unrelated machines, a problem for which polynomial-time -approximation algorithms that ignore incentives exist (Lenstra, Shmoys, Tardos 1990) and for which the exact optimum is computable in exponential time. Combined with the MinWork mechanism of the same paper (an -approximation), it determines the optimal ratio for two machines. It is the base case of the Nisan–Ronen conjecture and the prototype of the "characterize truthful mechanisms by prices" technique used throughout later work on the conjecture.
Formalizing it. The theorem has been proved since 1999, but no machine-checked version is known to exist. The mission produces a formal account of general mechanisms with arbitrary strategy sets, dominant-strategy implementation, the revelation principle in that generality, and the price characterization of truthful mechanisms (independence and maximization). These are reusable for every other lower bound in this paper and for the later literature on the conjecture.
The statement quantifies over all mechanisms, with arbitrary strategy sets and arbitrary payment functions, so no finite search settles it. The revelation principle reduces to truthful direct mechanisms, but even these are an infinite-dimensional family: the allocation rule may break ties in any way, and prices may be any functions of the other agents' reports.
The printed argument also has two places that need care. Proposition 4.5 and Lemma 4.7, as printed, range over all sets of tasks, while Definition 12 gives unattainable sets price ; the statements hold only over attainable sets, and are formalized that way. And the case where agent 2's bundle has odd size is dispatched in one sentence ("which still yields the same allocation"), which the preceding lemma does not justify when agent 2's best bundle at the perturbed prices is not unique. A complete formal proof of the goal must supply an argument for that case.
Fin n, tasks Fin k; an allocation is a function Fin k → Fin n; bundles may be empty. The make-span is a finite maximum and assumes (NeZero n).A : Fin n → Type u (any universe), output and payments on dependent strategy profiles. Implements requires both that every agent of every positive type has a dominant strategy and that every profile of dominant strategies yields a -approximate allocation. Dominance is against every profile of the others, not only dominant ones. Without the existence clause, a mechanism with no dominant strategies would implement vacuously; the definition excludes that.Contributions of any of the milestones are welcome, as are alternative proofs of the goal that avoid the terse odd case.
Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than -competitive, and the best randomized algorithms are -competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).
Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.
Timeline.
A request sequence lists elements of a set . A cache of size starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum is the least number of misses over all eviction schedules chosen with knowledge of .
With each request the algorithm receives a real prediction . The true label is the position of the next request of , or if there is none. For a loss function , the error of the predictions is , and the predictions are -accurate when .
The spread of measures how cheaply a predictor can get the order of arrivals completely wrong: is the least length such that every strictly increasing integer sequence and every non-increasing real sequence have total loss .
Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length is at most , the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is .
If is concave on and majorizes the spread, then for every , every tie-breaking rule, and every sequence with -accurate predictions,
The result. Theorem 3.3 gives both guarantees at once. For an exact predictor () the ratio is a constant, , independent of ; for an arbitrary predictor it is , within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like , so the ratio grows like . The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.
Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap printed as in Lemma 3.4, and the behaviour of the spread at .
The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors and the chain lengths are both random, while the hypothesis controls only the total error against , not the number of chains in which the error is spread.
Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with for elements never requested again. The paper prints the label with equal features; the element is meant. is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. is harmonic k as a real number, never .
Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in .
The spread takes real arguments and lengths . must be concave on , finite, and at least the spread. It must also be continuous at , which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays over several lengths. -accuracy is the pointwise condition on the given pair . The competitive ratio is written as a product, so needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has in place of the printed , with the minimum inside the expectation because is random.
The statement must not be trivialized. is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss has spread .
Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.
Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.
Long-time behaviour is the central question about an autonomous differential equation : where does a trajectory go as ? In the plane this question has an almost complete answer. The theory begun by Poincaré (Mémoire sur les courbes définies par une équation différentielle, 1881–1886) and completed by Bendixson (Sur les courbes définies par des équations différentielles, Acta Math. 24, 1901, doi:10.1007/BF02403068) shows that a bounded planar trajectory can only accumulate on equilibria, on a periodic orbit, or on a chain of equilibria joined by connecting orbits. Chaotic behaviour, which already occurs for three-dimensional flows such as the Lorenz system, is excluded. It is the standard tool for proving that a planar system has a limit cycle, and it underlies Hilbert's 16th problem.
This mission formalizes Section 7.3 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS Graduate Studies in Mathematics 140, 2012), pp. 220–224, which proves the classical theorem and the generalized version with finitely many fixed points.
Let be open and . An integral curve at is a function on an open interval with , and on . The union of all such is the maximal interval . The flow , , is the value at time of the maximal integral curve at . With :
In Lean, points are Fin 2 → ℝ (general Fin n → ℝ for the Chapter 6 notions), and is a Bool with true for . The definitions are lifetime, flow, orbit, halfOrbit, omegaLimitSet, IsPeriodicPoint and IsTransversalArc, all in the namespace TeschlODE.Planar.
Fix and , and suppose is compact, connected and contains only finitely many fixed points. Then one of three cases holds:
where are fixed points in .
The theorem turns the existence of periodic solutions into a topological statement. It is enough to find a compact positively invariant region with no equilibria, often an annulus bounded by two curves on which the vector field points inward. This is how periodic orbits are established for the van der Pol and Liénard equations (Theorem 7.8 of the same chapter) and for many models in biology and chemistry. The generalized version also describes limit sets that contain equilibria, such as homoclinic and heteroclinic cycles. Corollary 7.12 records the dimensional boundary: in the plane every minimal set is a periodic orbit, while from dimension three on minimal sets can be invariant tori with dense orbits.
The results have been proved for over a century. None of them is formalized in Mathlib or on the platform. Mathlib has omegaLimit for global flows on topological spaces and existence and uniqueness of integral curves, but no local flow of a vector field on an open set, no transversal sections and no Jordan curve theorem. This mission produces a machine-checked planar limit-set theory. The local flow and limit-set layer it needs is reusable for every later chapter on dynamical systems.
The statements are topological, and the proofs rest on the Jordan curve theorem for piecewise curves: a closed curve made of an orbit segment and a piece of transversal arc separates the plane, and trajectories cannot cross it in the forbidden direction. That theorem is not in Mathlib, and the platform's Jordan-curve and Schoenflies statements are open. Everything that looks one-dimensional in a sketch, "the orbit enters the inside and is trapped", depends on it. The ingredients a sketch treats as obvious also need care: the flow-box straightening (Lemma 6.2), the local return map to a transversal arc (Lemma 6.9), and the invariance, closedness and connectedness of limit sets (Lemmas 6.5–6.6). Generic arguments about compact invariant sets do not suffice: the conclusions are false in , so any proof must use planarity.
Fin 2 → ℝ. Its sup norm induces the Euclidean topology, and no statement depends on the norm. is a total function with ContDiffOn ℝ 1 f M on the open set .lifetime f M x is the union of domains of integral curves at , and flow f M t x is the value at of such a curve, selected by choice (unique for fields). Outside the flow has the junk value , and no statement evaluates it there. Limit points must lie in , as in the book.Bool; true means (atTop), false means (atBot).IsPreconnected; nonemptiness is a separate hypothesis. "Finitely many fixed points" is Set.Finite {y ∈ ω_σ(x) | f y = 0}. The book's "" is for a fixed point . No statement uses O(·), "sufficiently small" or an unspecified constant.Most differential equations that model physical, biological or engineered systems cannot be solved in closed form, yet the question asked about them is usually qualitative: does the system settle down to an equilibrium, and does it stay near the equilibrium when perturbed? Liapunov's direct method answers that question without solving the equation, by exhibiting a function that does not increase along solutions. It is the standard tool of nonlinear stability analysis and of control design, where a controller is typically certified by a Liapunov function for the closed-loop system (Khalil, Nonlinear Systems).
A Liapunov function whose values strictly decrease along every non-constant solution gives asymptotic stability directly. In practice the natural candidate, often the total energy of a damped mechanical system, only satisfies a non-strict inequality. The Krasovskii–LaSalle invariance principle closes that gap: if the function is not constant along any complete orbit other than the equilibrium, the equilibrium is still asymptotically stable. It was established by Barbashin and Krasovskii (1952) and by LaSalle (1960, IRE Trans. Circuit Theory 7).
This mission formalizes Chapter 6 of Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version), from the local flow of an autonomous equation, through limit sets, to the principle itself.
Fix , an open set (the phase space) and a vector field of class . The autonomous system is . An integral curve is a differentiable map from an open interval into with for all .
For each there is a maximal interval and a unique maximal integral curve on with : every integral curve through at time is a restriction of it. The map on is the flow. It is a local flow: may be bounded, because solutions can leave or blow up in finite time.
The orbit of is and the forward orbit is ( with ). The -limit set is the set of with for some times in ; uses .
A point with is a fixed point. It is stable if every neighborhood of contains a neighborhood of such that solutions starting in exist and stay in for all . It is asymptotically stable if moreover as for all in some neighborhood of .
A Liapunov function at is a continuous on an open neighborhood of with , on , and for every integral curve and all with . It is strict if the inequality is always strict. denotes the connected component of containing .
Let be a fixed point and a Liapunov function at on . Write for: is not constant on any orbit lying entirely in , i.e. every with has points with . Then
and, under , every whose forward orbit lies in a compact subset of satisfies as .
In attack order: Theorem 6.1 (the maximal flow exists, is open, is on , and ); Lemma 6.3 (a forward orbit in a compact subset of forces ); Lemma 6.6 ( is then nonempty, compact and connected); Lemma 6.7 (); Theorem 6.15 (a function non-increasing along is constant on ); Lemma 6.11 (a closed is positively invariant); Lemma 6.12 ( and ); Theorem 6.13 (Liapunov: a Liapunov function makes stable).
The result itself. The invariance principle is the form of Liapunov's method used in applications. It gives asymptotic stability of damped mechanical systems from their energy, of gradient systems from their potential, and of adaptive and passivity-based controllers, where the natural Liapunov function is only non-increasing. Its limit-set formulation (Theorem 6.15) is also the entry point to the Poincaré–Bendixson theory of the next chapter, which uses the same -limit sets.
Formalizing it. Mathlib has local existence and uniqueness for ODEs and a theory of -limit sets for global flows (omegaLimit, Flow). It has no maximal solution of an ODE, no local flow with its maximal intervals, and no Liapunov stability theory. The results are classical and proved in the book; none has a machine-checked proof on this platform. This mission builds the local-flow and limit-set layer and the Liapunov layer on top of it.
The central difficulty is that the flow is local. The book's arguments pass freely between "the solution stays in a compact set" and "the solution exists for all positive time" (Lemma 6.3). In a formal setting every statement about must first establish , and the maximal interval must be constructed from local solutions. Theorem 6.1 on its own requires gluing local solutions into a maximal one and proving that the domain is open with dependence on initial conditions.
A common first idea is to assume the vector field is complete, so that Mathlib's global Flow and omegaLimit apply directly. That assumption is not available: the goal concerns orbits that stay in the neighborhood , and completeness of such orbits is a consequence of the argument, not a hypothesis. Similarly, is only continuous, so a derivative-based criterion cannot replace condition (6.36).
The state space is EuclideanSpace ℝ (Fin n), so is the Euclidean norm, and is the open ball Metric.ball. The standing assumption , , open, is a binder of every theorem (as ContDiffOn ℝ 1 f M, the weakest case, and for general in Theorem 6.1). The flow enters as a pair (I, Φ) satisfying IsMaximalFlow f M I Φ, which characterizes the maximal integral curves uniquely. Theorem 6.1 proves that such a pair exists, so no completeness or extra regularity is assumed. The two time directions of Lemmas 6.3–6.7 are one statement with a real parameter σ = 1 ∨ σ = -1. The -limit set contains only points of , as in the book.
Stability conclusions include existence of the solution for all . The Liapunov condition quantifies over every integral curve and constrains only the two endpoint values, exactly as (6.36). is a total function whose values off are never read.
Correction to the printed statement. The book's final sentence of Theorem 6.14, "every orbit lying entirely in converges to ", is false as printed. With and a strict Liapunov function, some orbits escape to infinity (Khalil, §4.1). The goal therefore asks for convergence of every forward orbit contained in a compact subset of , which is what the book's argument uses. The other two parts are as printed.
A trivializing formalization is ruled out: stability and asymptotic stability are stated for the maximal flow, with existence for all required, and not for an arbitrary map Φ or a flow assumed global. Asymptotic stability keeps both conjuncts, stability and attraction.
Needed infrastructure: maximal solutions of autonomous ODEs and their continuation (reusable across Chapters 6–13), openness of and smooth dependence on initial data, compactness arguments for limit sets, and connected components of sublevel sets. Contributions of the local-flow layer as standalone lemmas are especially welcome, since later missions of this series rely on the same objects.
Almost every quantitative statement about an ordinary differential equation, from the stability of an equilibrium to the existence of a periodic orbit, presupposes that the equation has a solution through each initial point and, usually, that this solution is unique and depends continuously on the data. Chapter 2 of Gerald Teschl's graduate textbook Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012) establishes these facts for first-order systems in . It is the foundation for the rest of the series: the flows, limit sets, Poincaré maps and invariant manifolds of later chapters are all built on the existence, uniqueness and extension results proved here.
A short history. Local existence was first proved in the nineteenth century by polygonal approximation (Cauchy) under differentiability-type hypotheses. Lipschitz isolated the condition that bears his name. Picard and Lindelöf established existence and uniqueness by successive approximation, and Banach (1922) abstracted the argument into the contraction principle. Peano (1890) showed that continuity of the right-hand side alone suffices for existence, without uniqueness. Gronwall's inequality and its integral generalisations give the continuous dependence estimates. Teschl's chapter presents all of these in a uniform notation.
An initial value problem (IVP) is
where is a continuous map from an open set to and . Here is the Euclidean norm on . A solution on an interval is a function whose graph lies in and which is differentiable on (one-sidedly at an endpoint that belongs to ) with . Such a solution is automatically continuously differentiable.
The function is locally Lipschitz in the second argument, uniformly with respect to the first, if for every compact there is a constant with whenever (the book's (2.18)).
For let , where , let , and define the existence time
The chapter also works in a real Banach space , a complete normed real vector space, where a contraction of a closed set is a map with for some .
If is continuous on and , then there is a function with solving
and the analogous statement holds on with . No Lipschitz condition is assumed and the solution need not be unique.
Peano's theorem is the existence statement with the weakest regularity hypothesis on in the classical theory. It is what lets one speak of solutions of equations with non-Lipschitz right-hand sides, such as , and it is the starting point for the theory of non-unique solutions and differential inclusions. The explicit existence time is the quantitative form used whenever one needs a uniform lower bound on the lifetime of solutions starting in a compact set. Picard–Lindelöf, Gronwall and continuous dependence together make the IVP well posed. The global existence theorem under linear growth is used throughout the later chapters to define global flows.
Mathlib already contains a Picard–Lindelöf theorem (IsPicardLindelof), Gronwall's inequality in differential form, the Banach fixed point theorem for complete (extended) metric spaces, and an Arzelà–Ascoli theorem for bounded continuous functions. It does not contain Peano's theorem, the integral form of the generalised Gronwall inequality with variable , Weissinger's theorem, or global existence under linear growth. The statements here are phrased in the book's setting: one-sided intervals, the convention for , local Lipschitz conditions on an open set, -valued functions. Connecting them to the existing Mathlib results is part of the work.
For Peano's theorem the obvious approach, Picard iteration, does not apply. Without a Lipschitz condition the integral operator need not be a contraction on any ball, its fixed points need not be unique, and a sequence of approximate solutions need not converge. Any argument has to produce a solution without a uniqueness mechanism and still reach the full interval that the theorem specifies, not merely some shorter one. On the formal side, derivatives relative to closed intervals, the corner of , and passing between the differential and the integral form of the IVP all need care.
For Theorem 2.17 the difficulty is that "every solution is defined on all of " is a statement about maximal solutions, and the book defines these only through a gluing construction. Without a Lipschitz condition that construction is no longer unique. An a-priori bound on alone does not give extension beyond a finite endpoint.
EuclideanSpace ℝ (Fin n), so is the Euclidean norm. The right-hand side is a total function ; hypotheses restrict attention to or . Banach spaces are real normed spaces with CompleteSpace.IsSolutionOn U f I x: for every , and has derivative at relative to . Initial conditions are separate hypotheses.IsGreatest {|f(p)| : p ∈ V} M. is if M = 0 then T else min T (δ / M). "Some interval around " in Theorem 2.2 is with , and "unique" means uniqueness on every interval containing . In Theorem 2.8 the suprema , of (2.41) become arbitrary constants , bounding the same quantities, which is equivalent because the bound is monotone in both; the case uses the limit . In Theorem 2.17 the constants are existential inside , so they may depend on but not on . "All solutions are defined for all " means that every solution on an open interval extends to a solution on .A complete development needs derivatives within intervals, interval integrals, uniform convergence and compactness in . The definitions IsSolutionOn and LocallyLipschitzSecond are reused throughout the Teschl series. Contributions that connect these statements to Mathlib's IsPicardLindelof, ContractingWith and BoundedContinuousFunction.arzela_ascoli are welcome.
Fictitious play is the oldest model of learning in games: players repeatedly play a fixed normal form game, and each round every player best-responds to the empirical frequencies of the opponents' past play. Brown (1951) proposed it as an algorithm for computing the value of a zero-sum game, and Robinson (1951) proved that the empirical frequencies converge to the set of equilibria in that case. In stochastic fictitious play (Fudenberg and Kreps 1993) each player's payoffs are perturbed by fresh random shocks before every choice. The shocks make best responses single-valued and smooth in beliefs, which puts the process within reach of stochastic approximation theory: its long-run behaviour is governed by a deterministic perturbed best response dynamic.
Before Hofbauer and Sandholm (2002), convergence of stochastic fictitious play was known only for 2×2 games (Fudenberg and Kreps 1993; Kaniovski and Young 1995) and for certain games with two strategies per player (Benaïm and Hirsch 1999). The difficulty was the perturbed dynamic itself, whose vector field involves choice probabilities with no closed form for general noise distributions. Hofbauer and Sandholm showed that every such dynamic can be rewritten with a deterministic payoff perturbation (their Theorem 2.1), and used that to carry Lyapunov functions over to arbitrary noise distributions. This mission covers the first two classes of games in their main convergence theorem: symmetric games with an interior evolutionarily stable strategy, and two player zero-sum games.
A two player normal form game has strategy sets and and utilities . Player 's mixed strategies form the simplex , and . The payoff vector lists the expected payoff of each pure strategy of against the opponent's mixed strategy. The game is zero-sum if for every profile .
Each player has a shock density on . The choice function , for with density , gives the perturbed best response . The densities are required to be strictly positive with continuously differentiable choice functions ("the conditions of Theorem 2.1").
Standard stochastic fictitious play. Pure strategies are identified with basis vectors . Choices are arbitrary. At every time each player draws a shock with density and plays at time the pure strategy maximizing , where the beliefs are the time averages
The shocks are independent over time and across players. The expected motion of is the perturbed best response dynamic
Symmetric games. A two player game is symmetric if and ; it is described by the matrix , and . In symmetric stochastic fictitious play two players in roles 1 and 2 play at every time, their shocks are independent and identically distributed with one density , and the state is the average of all past plays in both roles,
Its mean dynamic is on . A mixed strategy in the interior of is an interior evolutionarily stable strategy (ESS) if for all mixed near .
Rest points and chain recurrence. For a dynamic on a compact set , the rest points are the zeros of in . A point is chain recurrent if for every one can return from to by following solution segments of length at least , with jumps of size less than between segments.
(i) If has an interior ESS, then (SP) has a unique rest point and
(ii) If the two player game is zero-sum, then (P) has a unique rest point and
Both hold for all shock densities meeting the conditions of Theorem 2.1, all probability spaces carrying the shocks, and all initial choices.
The theorem gives global, almost sure convergence of a learning process for arbitrary noise distributions, not only for the logit (Gumbel) noise under which the perturbed dynamic has a closed form. For zero-sum games it is the stochastic counterpart of Robinson's theorem. For symmetric games with an interior ESS it shows that a population learning by stochastic fictitious play settles at a single mixed state. Since the choice functions are continuous, the players' choice probabilities converge as well. The limit is the rest point of the perturbed dynamic, which approximates a Nash equilibrium (in case (i), the ESS) as the noise vanishes.
On the formal side, the paper's results are proved, but no part of them is machine-checked, and the platform has no model of learning in games, of chain recurrence, or of stochastic approximation. The mission produces a formal model of stochastic fictitious play as a random process, formal statements of the Hofbauer and Hofbauer–Hopkins Lyapunov functions, and the chain recurrence characterizations that connect them to the process.
The obvious route replaces the process by the ODE (P) and argues that (P) converges. That step is where the argument is incomplete: convergence of every solution of (P) does not give convergence of the stochastic process, because a stochastic approximation can in principle circulate near a set of orbits the ODE never follows. The right invariant is the chain recurrent set, and the limit sets of the process lie in a connected component of it (Benaïm and Hirsch 1999; Benaïm 1999). The characterization therefore has to be of chain recurrence, which is strictly weaker than asymptotic stability of individual orbits.
The second obstacle is that (P) itself is defined through the noise distribution and admits no useful Lyapunov function in general. The Lyapunov functions exist for the deterministic form (PV)/(SPV), and moving between the two forms requires the representation of Theorem 2.1, whose perturbation has no closed form either.
Players and strategies are indexed from . Mixed profiles live in and every vector field is defined on that ambient space. The processes are defined pathwise from a family of shock vectors on an arbitrary probability space. Ties in the argmax are broken by the smallest index, an event of probability zero because the shocks have densities. The shock drawn at time produces the choice at time . Shock densities are arbitrary strictly positive densities with continuously differentiable choice functions; no noise law is fixed, and the two players' densities in (ii) may differ. Independence is joint over times and players (and roles in (i)). The symmetric process has its own state in one simplex and is not the standard process applied to a symmetric game.
Deterministic perturbations are functions defined on the whole space whose values off the open simplex are ignored; derivatives are taken of their composition with the projection onto the affine plane . Perturbed best responses in (PV) and (SPV) are supplied as maps together with the hypothesis that they are the unique maximizers. A strict Lyapunov function must increase strictly along every non-constant solution on . The ESS definition includes , which the source omits.
The conclusions assert existence and uniqueness of the rest point; they are not hypotheses. A statement for the ODE (P) in place of the process , for one fixed noise law, or with the ESS as the limit point would be a different theorem.
A complete development needs Theorem 2.1 (convex duality and the Legendre transform on the simplex), existence and uniqueness of solutions of (P), basic chain recurrence theory, and the stochastic approximation results of Benaïm and Hirsch, which are not restated here and are welcome as independent contributions. The model layer (games, payoff vectors, choice functions, stochastic fictitious play) is shared with the other missions of this series.
Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.
Fix two fields : typically and a field large enough to hold every number in the problem. A family is algebraically independent over if no nonzero polynomial with coefficients in vanishes at — informally, the behave as free, unconstrained parameters relative to . Fix finite row and column index sets and . A matrix over is a mixed matrix with respect to if it decomposes as
where has every entry in , and has entries in whose nonzero values, taken together as one family, are algebraically independent over . models the exact, structural part of the system; models the independent physical parameters. For and , write for the submatrix with rows and columns . The rank of is its rank over — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write , , and for the number of rows of that contain a nonzero entry of in some column of . A mixed polynomial matrix is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate (used to model the Laplace- or -transform variable of a linear time-invariant system): has every coefficient of every entry in , and the coefficients of 's entries, taken together, are algebraically independent over .
This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of 's rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of reduces to nonsingularity of a -part and a -part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.
The result itself. Theorem 12.9 gives a certificate, not just a number: a pair that simultaneously proves the exact numeric rank contribution of and exhibits a submatrix of that vanishes identically. Because (via Gaussian elimination on ) and , (via maximum bipartite matching on 's nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.
Formalizing it. All five results in this mission are proved in the source text (this is
textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that
the genericity hypothesis — "the nonzero entries of are algebraically independent" — is
precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent
rather than an informal paraphrase such as "generic" or "random" values, which would be either
meaningless or a different (probabilistic) condition.
The naive approach to testing whether is nonsingular is to expand directly and check whether the resulting expression, as a polynomial in 's free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion has no cancellation between distinct terms, precisely because the nonzero entries of are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for , a nonzero-pattern-only matching argument for ). Missing this point — e.g. by treating 's entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.
Row and column index sets , are general finite types (Fintype, with DecidableEq where
needed for Finset operations), not fixed to . No constant appears in any
statement in this mission — every quantity (ranks, cardinalities, ) is instance-dependent,
so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly
rectangular, cross-type-indexed) submatrix is formalized as I.card = J.card together
with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant
requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are
not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the
ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13
is computed the same way, via an arbitrary reindexing bijection between the row- and column-index
subtypes — a choice that changes the determinant by at most a sign and hence never changes its
degree. A formalization that replaced the genericity hypothesis on with mere distinctness of
its nonzero entries would admit spurious cancellations in the determinant expansion and would not
prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise,
non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions
from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank,
IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to
mixed-matrix decompositions.
This mission continues chapter 10's algorithmic account across its remaining two sections:
finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's
tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the
capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate
scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in
mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity
bounds; this mission places the results that are ordinary mathematical propositions.
The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F)
and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq.
(10.26)); this mission places the case-independent inequality its own legitimacy rests on, and
restates its correctness conclusion. The steepest descent algorithm for an L-convex function
g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to
p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the
resulting monotonicity fact and a domain-size bound for the L-convex adaptation.
Conjugate scaling replaces a dual-integral M-convex function's conjugate g with
g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling
operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.
For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/
integer-dual conjugate of an L-convex g), the conjugate scaling f⟨α⟩ is again
dual-integral M-convex, witnessed by g_α itself being L-convex, provided f⟨α⟩>-∞.
Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and
most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own
text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work
where a naive approach provably does not.
Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own
legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission
34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent
algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct
reading) bounds the L-convex adaptation's domain-size parameter in terms of the
original function's.
Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather
than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own
structure — completing the book's account of the M-convex submodular flow problem with an
algorithm whose polynomial running time depends on exactly this compatibility. Propositions
10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular-
minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32
are the analogous structural facts for L-convex function minimization, chapter 10's third major
algorithmic thread.
None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).
As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as
hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see
HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum
submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR
extraction demonstrably cannot distinguish the two visually different capacity-bound symbols
(c* overlined vs. underlined) central to their shared defining formula, confirmed directly
against the raw extracted bytes, making faithful reconstruction of that formula impossible from
the available text; see HARD.md.
Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions
10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is
redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type
where the original was V-specific, since this draft cannot import that sibling. Proposition
10.26 is placed as the case-independent core inequality its own proof establishes, rather than by
replicating the three-case verification against Proposition 10.24's own internal proof objects
(Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count
corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25,
10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys
are welcome; the goal carries the most independent proof content (via the conjugacy theorem and
Theorem 7.10(2), both established elsewhere in this series).
34-ch10b-algorithms's own Proposition 10.24).In the capacitated vehicle routing problem (CVRP) a fleet of vehicles of capacity leaves a depot and serves customers; every customer is visited once, and the load of each route must not exceed . In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least , but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set built from the information that can actually be estimated: support, means and dispersion bounds.
Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set . This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.
Customers are indexed by and their random demand vector is . Fix a box with , a mean vector in the interior of , and a symmetric positive definite matrix . The covariance ambiguity set is
where is the set of all probability distributions on and means that is positive semidefinite.
For a distribution and a real random variable , the value-at-risk at level , , is . For a customer set , the worst-case value-at-risk is . A route serving satisfies the chance constraint for every exactly when this number is at most .
Two componentwise bounds appear in the answer:
A route set is an ordered partition of the customers into nonempty ordered routes. It is feasible in the distributionally robust problem RVRP() if every route satisfies the chance constraint for every , and feasible in a deterministic instance with capacity and demands if every route's total demand is at most .
For every customer set ,
The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.
For a diagonal bound , program (17) collapses to a search over one parameter with :
over the for which the first bracket is nonnegative and the point of (17) that induces respects (see Formalization scope).
For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.
Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.
The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.
The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "" requires, for every feasible of (17), a sequence of distributions in (16) whose value-at-risk approaches . The value-at-risk is a lower quantile, so a distribution placing mass exactly on a high point does not attain the value: the construction has to be a limit. The inequality "" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for alone ignores the box: it yields , which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound , is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals . The covariance bound is called Sig because Σ is Lean syntax. The side conditions , , (Sig.PosDef) and are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. is Mathlib's matrix inverse.
The paper states Theorem 7 and Corollary 4 with "-VaR" without a level; the level , used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every with a nonnegative bracket. For , every large then gives the value , which can exceed and hence every value-at-risk. The formal statement adds the condition that makes each a feasible point of (17): for , where is the first bracket. With this condition the statement is the diagonal case of Theorem 7.
A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives , and it has no multiplier for .
Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.
In the capacitated vehicle routing problem (CVRP) a depot serves customers with vehicles of capacity , and every route must respect the capacity. When customer demands are uncertain, the distributionally robust chance-constrained CVRP of Ghosal and Wiesemann (Oper. Res. 68(3), 2020) requires every route to meet its capacity with probability at least under every distribution in an ambiguity set , a family of distributions consistent with what is known about the demands. Such constraints are handled in a branch-and-cut scheme through rounded capacity inequalities, whose right-hand sides require one quantity for each customer subset : the worst-case value-at-risk of the cumulative demand of .
For ambiguity sets that describe each customer separately (marginal moment sets), this quantity is additive over customers and the problem reduces to a deterministic CVRP. Such sets cannot express that the demands of customers in the same municipality, county or state vary jointly within limits. The first-order generic moment ambiguity set does express this: it bounds the mean absolute deviation of the cumulative demand of prescribed customer groups. The mean absolute deviation is a standard robust dispersion measure, less sensitive to outliers than the standard deviation (see Casella and Berger, Statistical Inference, 2002). This mission formalizes the paper's description of the worst-case value-at-risk over such sets.
Demands form a random vector on . The data are a support box with , a mean vector in the interior of , customer subsets and bounds . For , is its indicator vector. The first-order generic moment ambiguity set, Eq. (12) of the paper, is
where is the set of probability distributions on and acts componentwise. The subsets are arbitrary: they may overlap and need not cover .
For a risk level and a random variable , the value-at-risk is . For a customer subset the quantity of interest is
Write (componentwise) and for the componentwise positive part. A route set partitions into nonempty ordered routes. It is feasible in the deterministic CVRP with demands if for all , and feasible in the distributionally robust CVRP if for all and all .
For every customer subset ,
The right-hand side is the optimal value of the paper's problem (13). The statement holds for every family of subsets and all data satisfying the standing assumptions, so it is the general form of which the milestones are special cases.
If are pairwise disjoint and cover and , then
If , for and , then
For some instance with an ambiguity set of the form (12), no deterministic CVRP instance on the same customers and vehicles (capacity , demands ) has the same set of feasible route sets.
Theorem 5 makes the worst-case value-at-risk over (12) computable in polynomial time as the value of a nonsmooth convex problem over the nonnegative orthant, which the paper notes can be written as a linear program. This gives the right-hand sides of the rounded capacity inequalities in a branch-and-cut scheme for the distributionally robust CVRP. Corollaries 2 and 3 give closed forms for two structured families of groups, evaluable in time linear in . Theorem 4 shows the gain in modelling power has a cost: unlike the marginal case, the problem cannot in general be replaced by a deterministic CVRP with altered demands. With a single customer and , Theorem 5 reduces to the closed form for marginalized first-order sets, so it extends that single-customer formula to joint dispersion constraints.
All four results are proved in the paper's online supplement. As far as a platform search shows, none has been machine-checked. The mission produces checked proofs of the equality in Theorem 5, the two closed forms, and an explicit instance for Theorem 4.
The supremum ranges over an infinite-dimensional set of joint distributions, and the value-at-risk is neither convex nor concave in the distribution. Bounding the value-at-risk of each group separately and adding the bounds does not work when groups overlap, and it ignores the total-dispersion constraint. It gives only an upper bound, and in the setting of Corollary 2 that bound is strict whenever the total bound is the binding term. Showing that the infimum in (13) is attained in the limit needs distributions that saturate several overlapping dispersion constraints at once while keeping the mean fixed and the support inside the box. For Theorem 4, the witness must separate the feasible-route-set family of the robust instance from every family defined by a single linear capacity inequality with nonnegative weights.
Customers are Fin n (0-based), subsets are Sfam : Fin p → Finset (Fin n), and a distribution is a Measure (Fin n → ℝ) that is required to be a probability measure. Support is P (Set.Icc qlo qhi) = 1, the mean condition is ∫ q, q j ∂P = μ j, and the dispersion condition is ∫ q, ∑ j ∈ Sfam l, |q j - μ j| ∂P ≤ ν l. The integrability clauses stated alongside are automatic for measures carried by the box. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is the real sSup of its image over the set; under the standing assumptions this image is nonempty (the Dirac at lies in the set) and bounded (bounded support), so the real supremum is the paper's. The optimal value of (13) is the real sInf of the objective over , a nonempty set on which the objective is bounded below by . Attainment is not claimed. All statements carry the standing assumptions , , and . Corollary 2 writes with the last subset Sfam (Fin.last r). Corollary 3 indexes the singleton of customer by Fin.castSucc i. In Theorem 4 route sets are Fin m → List (Fin n) and only feasibility is modelled; costs play no role.
The theorems are not trivialized by an empty ambiguity set or a junk supremum: membership of the Dirac distribution at is checked locally with a sorry-free proof. Theorem 4 needs a genuinely separating instance: an instance in which no route set is robustly feasible, for example, is matched by a deterministic instance in which none is feasible either.
Needed infrastructure: two-point and finitely supported distributions on and their value-at-risk; weak duality for moment problems over the box; the positive-part calculus of (13). The value-at-risk lemmas for finitely supported measures are reusable in the sibling missions on this paper. Contributions of any of the milestones, of lemmas for these building blocks, or of either inequality of Theorem 5 on its own are welcome.
The capacitated vehicle routing problem (CVRP) assigns customers to a fleet of identical vehicles of capacity and orders each vehicle's visits so as to minimize transportation cost, subject to each vehicle's total load not exceeding . In practice the customers' demands are not known when the routes are planned. Two classical responses are the robust CVRP, which requires feasibility for every demand vector in an uncertainty set, and the chance-constrained CVRP, which requires each capacity constraint to hold with probability at least under a known demand distribution. The first ignores all distributional information; the second assumes a distribution that is rarely known and usually requires independent demands.
Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP, RVRP(), in which each capacity constraint must hold with probability at least under every distribution of an ambiguity set . Whether this problem can be solved with existing CVRP technology depends on how the worst-case value-at-risk of a customer set's total demand behaves as a set function. This mission formalizes §4 of the paper, which treats ambiguity sets that only constrain each customer's demand separately.
There are customers with random demand vector and a risk level . For a probability distribution and a real random variable , the value-at-risk is
For an ambiguity set and a customer subset , the worst-case value-at-risk of is .
Fix a support box with , a mean vector in the interior of , and for each customer a componentwise convex dispersion measure with bound . The marginalized moment ambiguity set (5) is
It constrains marginal moments only, and so contains joint distributions of every dependence structure, from independent to perfectly correlated demands. Three special cases have their own closed forms: the first-order set (6), where bounds the mean absolute deviation ; the variance set (8), where bounds ; and the semivariance set (10), where bound and .
A route set partitions the customers into nonempty ordered routes. It is feasible in RVRP() if for all and all , and feasible in the deterministic CVRP with demands if for all .
For every marginalized moment ambiguity set (5) and every nonempty ,
The dispersion measures are left arbitrary (convex, componentwise, any number of components), so the goal covers every set of the form (5).
Theorem 3 says that over (5) the worst case of a sum is the sum of the worst cases. Because the value-at-risk is not additive for a fixed distribution, and the online supplement exhibits distributions in such a set for which the individual values-at-risk are not additive, the statement is about the ambiguity set, not about any of its members. Its consequence, Corollary 1, is that RVRP() over (5) is a deterministic CVRP with inflated demands, so existing branch-and-cut and branch-and-cut-and-price codes solve it unchanged. Propositions 2–4 make those inflated demands explicit for three standard dispersion measures, so that the whole reduction is in closed form. The corollary also exposes a limitation: under (5) the worst-case distribution does not depend on the route set, and the model cannot represent known dependencies between customers.
The results are proved in the paper's online supplement; none has a machine-checked proof. A formalization produces a checked worst-case value-at-risk calculus over moment sets with support constraints, including sharp one-sided Chebyshev-type bounds under mean-absolute-deviation, variance and semivariance constraints, which are reusable in distributionally robust optimization beyond vehicle routing.
The value-at-risk is neither subadditive nor superadditive in general, so neither inequality of Theorem 3 follows from properties of a single distribution. The inequality "" requires combining near-worst-case distributions of the individual customers into one joint distribution in that is simultaneously near-worst for the sum; the inequality "" requires bounding the value-at-risk of the sum for an arbitrary joint law using only marginal information. In Propositions 2–4 the supremum is typically not attained: the distribution concentrating mass at the claimed worst-case value violates the mean constraint, and the value is reached only as a limit of distributions in . An argument that exhibits a single maximizer therefore fails, and the statements must be proved as equalities of suprema.
Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. An ambiguity set is a set of measures on Fin n → ℝ, each required to be a probability measure; the support condition is P (Set.Icc qlo qhi) = 1 and expectations are Bochner integrals. The sets are sets of joint laws on , never products of marginals. In (5) each expectation is required to exist; this is automatic for convex on the bounded support. The value-at-risk is the published definition MultistageStochastic.valueAtRisk P Y (1 - ε), and the worst-case value-at-risk is the real supremum of its values over the ambiguity set; under the standing assumptions that set of values is nonempty (the Dirac law at belongs to ) and bounded (by the support), so the supremum is not a default value. The single-customer quantity is the case . The standing assumptions (, , convexity of , , , ) are explicit hypotheses. Routes are lists of customers; a route set has nonempty routes whose concatenation is a permutation of all customers. Costs are not formalized, since both routing problems minimize the same cost over their feasible route sets.
All targets are equalities or equivalences; a one-sided inequality, a statement asserting that some distribution attains the value, or a formulation over product measures is a different theorem and does not count.
Contributions welcome: the reduction of the chance constraint to a value-at-risk bound, the right-continuity lemmas for the value-at-risk of a measure on , two-point constructions in the ambiguity sets, and one-sided Chebyshev-type bounds with support constraints.
The capacitated vehicle routing problem (CVRP) asks for a set of minimum-cost routes by which a fleet of identical vehicles of capacity , based at a depot, serves every customer exactly once without any vehicle carrying more than its capacity. In practice customer demands are not known when routes are planned. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust CVRP: the demand vector is random, its distribution is known only to lie in an ambiguity set , and every route must respect its capacity with probability at least under every distribution in .
Exact CVRP solvers rely on compact two-index vehicle flow formulations strengthened by rounded capacity inequalities, which bound from below the number of vehicles entering any customer subset by a demand estimator . The paper shows (its Theorem 1) that the robust two-index formulation is exact whenever the demand estimator is subadditive and demands are nonnegative, and that this fails for some natural ambiguity sets: sets that fix the marginal distribution of each customer's demand violate it (Example 1). This mission formalizes the paper's positive result for the most widely used class of ambiguity sets, the moment ambiguity sets of distributionally robust optimization (see El Ghaoui et al. 2003, Delage and Ye 2010, Wiesemann et al. 2014).
There are customers, indexed ; the demand vector is . Fix
The moment ambiguity set is
where denotes all probability distributions on . The paper's standing assumptions are , each closed and convex, and .
For a distribution the value-at-risk of a random variable is , with risk level . The worst-case value-at-risk of a customer subset is , and the demand estimator (2) is
The Lean development names these momentAmbiguitySet qlo qhi μ φ σ, worstCaseVaR, demandEstimator and twoPointMeasure in the namespace DRCVRP.Moment.
For every moment ambiguity set satisfying the standing assumptions, every and every ,
This is condition (S) of the paper, stated for the rounded estimator (2) and for all pairs of subsets, overlapping or empty ones included.
For every customer subset there are two-point distributions with and such that
Combined with the paper's Theorem 1, Theorem 2 says that for every moment ambiguity set with nonnegative demands the robust CVRP can be solved through the compact two-index formulation with robust rounded capacity inequalities, i.e. by the branch-and-cut machinery of the deterministic CVRP. It also separates moment ambiguity sets from ambiguity sets built from marginal histograms, hypothesis tests, -divergences or Wasserstein balls, whose estimators can violate subadditivity. Proposition 1 describes the worst case: however many moment constraints the set contains, two demand scenarios suffice to approach the worst-case value-at-risk, strengthening the Richter–Rogosinski theorem for this functional.
Both results are proved in the paper's online supplement. They have not, to the best of current knowledge, been machine checked. This mission produces a checked statement and proof of both, together with a reusable encoding of moment ambiguity sets and of the worst-case value-at-risk over them. The companion missions of the series formalize the equivalence theorem (I) and the explicit worst-case VaR formulas for marginalized (III), first-order (IV) and covariance (V) ambiguity sets.
Value-at-risk is not subadditive for a single distribution, so the obvious route, subadditivity of the worst-case VaR followed by , needs an argument specific to the moment set; for the marginal-histogram set of Example 1 the worst-case VaR itself fails to be subadditive. The supremum over ranges over an infinite-dimensional set of distributions and is in general not attained, so an argument that picks a maximizer does not apply, and the classical finite-support reduction (Richter–Rogosinski) yields a number of support points that grows with the number of moment constraints, not two. The integer rounding and the must also be handled for all pairs of subsets, including overlapping ones.
Customers are Fin n (0-based) and customer subsets are Finset (Fin n). Distributions are measures on Fin n → ℝ; membership in the moment set requires a probability measure giving mass one to the closed box Set.Icc qlo qhi, integrable coordinates with ∫ q, q i ∂P = μ i (an equality), and integrable φ l with ∫ q, φ l q ∂P ≤ σ l. The integrability clauses hold automatically under the standing assumptions and do not shrink the set. The dispersion measure is an arbitrary real-valued function whose components are convex (convex real functions on are continuous, which covers "closed"); is allowed. The value-at-risk is the published platform definition MultistageStochastic.valueAtRisk at level . The worst-case VaR is a real sSup; over a moment set satisfying the standing assumptions the set of VaRs is nonempty (the Dirac measure at belongs to ) and bounded by the box, so this is the true supremum. The estimator is integer valued. Every standing assumption is a hypothesis of both theorems.
Neither statement can be satisfied trivially: the goal is about the rounded estimator of the true supremum over a nonempty set, not about subadditivity of an arbitrary set function, and the milestone requires the two-point laws to lie in and their VaRs to converge to the supremum, not to be attained. Extended-valued dispersion measures, such as the one expressing the covariance set of §5.2 as an instance of (4), are outside the scope of the real-valued encoding.
A complete development needs basic facts about quantiles of finitely supported measures, the structure of the moment set, and a duality or construction argument for the worst-case VaR. Lemmas about value-at-risk of two-point laws and about moment sets are reusable across the series. Proofs of the milestone, of the goal, and of intermediate lemmas are welcome.
In one complex variable the Riemann mapping theorem classifies a whole class of domains by topology alone: every nonempty simply connected proper subdomain of is biholomorphic to the unit disc. Nothing of the kind holds in several variables. The two most obvious generalizations of the disc to , the unit ball and the unit polydisc, are homeomorphic, yet no biholomorphic map carries one onto the other. This is the first result a student of several complex variables meets that has no one-variable shadow, and it is the standard illustration that the geometry of the boundary, not the topology of the domain, governs holomorphic equivalence.
As recounted in the source, Poincaré (1907) observed the inequivalence by computing the automorphism groups of and , assuming the maps extend past the boundary; H. Cartan gave the first complete proof in 1931; and Rothstein (1935) proved that there is not even a proper holomorphic map from the bidisc to the ball. This mission follows the presentation in §1.4–1.6 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026), where the inequivalence is derived from a general theorem on proper maps out of product domains, followed by Cartan's uniqueness theorem and the basic structure theory of zero sets and injective maps.
Write for -tuples of complex numbers, for the unit disc, and for the Euclidean norm. The unit ball and unit polydisc are
and the unit sphere is . A domain is a nonempty connected open set. A map between open subsets of complex spaces is holomorphic if it is complex differentiable at every point.
A continuous map is proper if is compact for every compact . A biholomorphic map is a holomorphic bijection whose inverse is holomorphic; every biholomorphism is proper. An analytic disc is a nonconstant holomorphic map , and a set contains no analytic discs if no analytic disc has . A circular domain is a domain with whenever and .
The goal is chosen as the textbook's headline result of §1.4. Theorem 1.4.8 is strictly more general; it is a milestone, so a solver may prove the goal as its special case.
Rothstein's theorem implies the biholomorphic inequivalence of and , the basic example that the Riemann mapping theorem has no analogue in several variables. Theorem 1.4.8 isolates the reason: a boundary that contains analytic discs cannot be mapped properly into a boundary that contains none. Cartan's uniqueness theorem and its corollary are the standard tools for computing automorphism groups of the ball and the polydisc. The Riemann extension theorem, the local graph structure of zero sets and the Jacobian criterion for injective maps are used throughout the theory of analytic varieties and of holomorphic mappings.
All of these results are classical and proved in the source. None of them is formalized in Mathlib or on the platform for with : Mathlib has one-variable Riemann removable singularities and the maximum modulus principle, and the platform has one-variable results on injective holomorphic maps. This mission produces machine-checked statements of the several-variable versions, and infrastructure (proper maps between subsets, analytic discs, holomorphic families) that later chapters of the series reuse.
The goal cannot be reached through topology: and are homeomorphic, so any argument must use holomorphy essentially and must see the boundary. The step that needs genuine analysis is passing from properness, a statement about compact sets, to a statement about boundary values of holomorphic functions of one variable along slices of the product domain; this requires normal families (Montel's theorem) in several variables, which Mathlib does not provide in the needed form. Cartan's theorem rests on power-series expansions in homogeneous parts and vector-valued Cauchy estimates on polydiscs. Theorem 1.6.2 needs the holomorphic implicit function theorem and Rouché's theorem, and Theorem 1.6.6 an induction on dimension that runs through Theorem 1.6.2. The Riemann extension theorem needs holomorphy of parameter-dependent Cauchy integrals.
is Fin n → ℂ. Mathlib's norm on this type is the sup norm, so Metric.ball 0 1 is the polydisc, not the ball. The ball and the sphere are therefore defined with the explicit Euclidean condition, unitBall n = {z | ∑ k, ‖z k‖ ^ 2 < 1} and unitSphere n = {z | ∑ k, ‖z k‖ ^ 2 = 1}. The polydisc is written coordinatewise as unitPolydisc n. Reading the ball as the sup-norm ball would trivialize the goal (the identity of the bidisc is a proper holomorphic self-map); the definitions exclude that reading. Boundedness is Bornology.IsBounded, and boundaries are Mathlib's frontier; neither depends on the norm. A domain is IsOpen U ∧ IsConnected U, so it is nonempty.
Holomorphic means DifferentiableOn ℂ on an open set. On open sets this is equivalent to the book's Definition 1.1.2 (Proposition 1.1.3 and Theorem 1.2.1). Maps into are Fin m → ℂ-valued. is fderiv ℂ f a, and the Jacobian determinant is LinearMap.det of it. Maps are ambient functions whose values off the relevant set are irrelevant. Consequently:
IsProperMapOn f U V: f maps U into V, is continuous on U, and U ∩ f ⁻¹' K is compact for every compact K ⊆ V. This is Definition 1.4.3 for the restricted map. It is not IsProperMap of the ambient map.g holomorphic on with Set.InvOn g f U V.Lemma 1.4.7 works in Fin n → ℝ and reads "limit point of the sequence " as a cluster point of the sequence (MapClusterPt). Theorem 1.4.8 uses the product type (Fin n → ℂ) × (Fin k → ℂ) for . In Theorem 1.6.2, "after reordering the variables" means choosing the index j of the solved-for coordinate. The remaining coordinates are indexed by {i // i ≠ j}. Only the open-disc part of Definition 1.4.5 (analytic discs) is formalized, because closed analytic discs are not used here.
A complete development needs Montel's theorem for maps into bounded subsets of , homogeneous expansions and Cauchy estimates on polydiscs, the holomorphic implicit function theorem, Rouché's theorem, and holomorphic parameter-dependent Cauchy integrals. All of it is reusable beyond this mission, and contributions of it are welcome.
Chapters 6 through 8 built M-convex and L-convex functions and their conjugacy theory as abstract combinatorial objects on the integer lattice. Chapter 9 grounds that theory in a setting every reader already knows: network flows. The chapter's throughline is that the classical minimum cost flow problem — flows bounded by simple arc capacities, with a single linear cost — is a shadow of a much richer submodular flow problem, in which the constraint on a flow's boundary is not "equal a fixed supply vector" but "lie in the base polyhedron of an arbitrary submodular set function." This mission formalizes the feasibility theory for both problems and its capstone: a max-flow min-cut theorem for submodular flows that specializes to the classical max-flow min-cut theorem exactly when the submodular function degenerates to a plain capacity function.
Let be a finite directed graph, with giving each arc's start and end vertex. The boundary of a flow is . For , and are the arcs leaving and entering . Given an upper capacity and lower capacity , the cut capacity function is . A submodular set function with plays the same structural role as but is arbitrary problem data rather than a derived quantity.
For a feasible maximum submodular flow problem on a specified arc : , a common value in ; if the data is integer valued and the value is finite, an integer-valued maximum flow exists.
Proposition 9.2: the cut capacity function is always submodular — the fact that lets the classical minimum cost flow problem's feasibility be phrased in exactly the same base- polyhedron language as the general submodular flow problem. Theorem 9.3: a flow meeting the capacity constraint with boundary exists if and only if for all and — the classical case, and the direct predecessor of the goal's feasibility side. Theorem 9.10: the submodular flow problem is feasible if and only if for all — obtained from Theorem 9.3 via Edmonds's intersection theorem in the book's own proof, and the feasibility half of the goal's own maximum-flow variant.
The result itself. Theorem 9.13 is a genuine generalization of the max-flow min-cut theorem — one of the most-cited results in combinatorial optimization — to a submodularly constrained setting where the classical single-source-single-sink cut structure is replaced by an arbitrary vertex subset scored by a submodular function rather than merely counted. It specializes to the classical theorem when is the indicator of a fixed boundary value and the graph carries a single source/sink; the book's own derivation (dividing the target arc and reducing to Theorem 9.10's feasibility criterion) is exactly the kind of "one shared mechanism explains two theorems" result this whole book is organized around.
Formalizing it. A prior-art search (GET /theorems?q=max-flow min-cut) found two existing
platform items for the classical theorem — LinearOptimization.max_flow_min_cut (Bertsimas &
Tsitsiklis, single source/sink, plain capacities) and menger_directed_max_flow (Ford-Fulkerson,
integer capacities) — both at a genuinely different, simpler generality (no lower capacity
bounds, no submodular vertex-cut function, a fixed source/sink rather than an arbitrary marked
arc). A further search (q=network flow) found a distinct mission formalizing Bertsimas &
Tsitsiklis's uncapacitated network flow LP theory (basic feasible solutions, tree solutions,
basis-matrix integrality) — a different technique (linear-algebraic, not cut-based) for a
different problem (no capacities at all). Neither family is reused; this mission gives the
first formal statement of submodular-flow feasibility and its max-flow min-cut theorem at the
book's own generality.
The obvious shortcut — state only the value equality of Theorem 9.13 and drop the integrality clause — would misrepresent the theorem's own content: the equality of the extremal values follows from ordinary LP duality on the polyhedron (arguably already within reach of chunk 04's Edmonds's intersection theorem machinery, as the book's own proof of the feasibility predecessor Theorem 9.10 uses exactly that), whereas the integer-flow existence half is the theorem's genuine combinatorial content, unique to the integer lattice. This chunk keeps both halves in every drafted theorem (Theorem 9.3, 9.10, and the goal) rather than only the polyhedral half.
A second, more structural difficulty governed this chunk's scope: BRIEF.md recommended
Theorem 9.4 (the potential-optimality criterion) and its M-convex-cost specialization Theorem
9.14 as milestones, but both need a polyhedral convexity hypothesis on real-valued (or
M-convex) functions over that this series has never built — the identical scope
boundary chunk 10 hit with Theorem 8.4. Rather than silently drop the polyhedral-convexity
hypothesis (which would make the drafted statement unsound, since the theorem's hard direction
genuinely needs it), this chunk selects only results — Proposition 9.2, Theorem 9.3, Theorem
9.10, Theorem 9.13 — that need no convexity apparatus of any kind, only the submodularity of
/ and elementary capacity-constraint feasibility.
and are Fintypes with DecidableEq V (and DecidableEq A where a Finset.erase is
needed); tail, head : A → V are plain functions, not a bundled graph structure. Every
capacity- and cut-related quantity is WithTop ℝ-valued (ℝ ∪ {+∞}) throughout, with no
EReal: a per-term check (documented in MODERATION_NOTES.md) confirms every subtraction this
chunk needs is really an addition of two terms each individually in , via a small new cast NegLowerToUpper : WithBot ℝ → WithTop ℝ. The base
polyhedron is stated by its defining inequalities rather than via a named polyhedral
object (chunk 04's BasePolyhedron is ℤ^V-domain and does not fit chapter 9's real-vector-
space setting). Not drafted: Theorem 9.4/9.14 (needs the real-domain polyhedral-convexity layer
above), Theorem 9.6 (needs a real-domain polyhedral L-convexity notion for its dual-integrality
half), Theorem 9.5/9.18/9.20/9.22 (negative-cycle criteria, an alternative non-potential
certificate family, checked against platform prior art and found adjacent only), Propositions
9.23–9.25 (supporting technical facts), and Theorems 9.26–9.28 (the separate network-
transformation technique of §9.6). A trivializing formalization would state Theorem 9.13's
value equality with the integrality clause dropped, or would silently allow / to range over all of EReal (permitting a nonsensical upper-
capacity-like lower bound); neither is done — both the integrality clause and the WithTop ℝ/WithBot ℝ type-level domain restriction are kept exactly as the book states them.