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?
Mission 32-ch09b-networkflows established the potential and negative-cycle optimality criteria
for M-convex submodular flow problems. This mission finishes chapter 9 with the two topics that
close it out: the constructive engine behind the negative-cycle criterion — cycle cancellation,
which actually improves a nonoptimal flow rather than merely detecting suboptimality, resting
on a delicate "unique-min condition" for bipartite matchings — and network duality, the chapter's
capstone structural theorem showing that M-convexity and L-convexity are preserved (and their
conjugacy is preserved) under transformation by an arbitrary network.
For a feasible integer flow ξ in the M-convex submodular flow problem MSFP2, a negative cycle
in the auxiliary network (Gξ,ℓξ) witnesses suboptimality (mission 32's Theorem 9.20); cycle
cancellation modifies ξ along a smallest such cycle to produce a strictly better flow ξ̄
(Eq. (9.75)). The unique-min condition for a pair (x,y) of integer vectors with
‖x-y‖∞=1 asks whether the bipartite graph G(x,y) — vertices the positive/negative supports of
x-y, weights the M-convex exchange values Δf(x;v,u) — has a unique minimum-weight perfect
matching; when it does, the M-convex exchange inequality of Proposition 6.25 becomes an equality.
Separately, a network G=(V,A;S,T) with entrance set S and exit set T transforms a pair
of functions f,g on Zˢ into induced functions f̃,g̃ on Zᵀ (Eqs. (9.81)-(9.82)), the minimum
cost to meet a boundary specification at the exit given a production cost at the entrance and a
transportation cost along arcs.
M-(resp. M-)convexity and integer-valuedness of f transfer to the induced f̃;
L-(resp. L-)convexity and integer-valuedness of g transfer to g̃; and if f is
M-convex, g is its L-conjugate, and each arc cost ga is the conjugate of
fa, then g̃ is the conjugate of f̃. Chosen as goal: the book calls this "the harmonious
relationship between network flow and M-/L-convexity", its own proof runs roughly six pages (the
longest argument in this chunk), and it is the general fact from which Theorems 9.27-9.28
(analogues for other type combinations) and Notes 9.29-9.30 (the aggregation and infimal-
convolution closure properties of M-convex functions, already placed in mission
22-ch06b-mconvexfunctions's own Theorem 6.13) all descend.
Theorem 9.22 shows cycle cancellation strictly improves the objective; Propositions 9.23-9.25 are
"the key ingredient" behind it: Proposition 9.23 shows the unique-min condition upgrades the
M-convex exchange inequality to an equality, Proposition 9.24 gives a checkable characterization
of when a bipartite weighted graph has a unique minimum-weight perfect matching, and Proposition
9.25 is the fact that makes the machine run — the specific pair (∂ξ,∂ξ̄) arising from cycle
cancellation always satisfies the unique-min condition. Theorems 9.27 and 9.28 are the network
duality theorem's own analogues for Z→R and R→R functions, the second restoring the
conjugacy assertion (missing for Z→R) via the ordinary real Legendre-Fenchel transform.
Cycle cancellation is this book's constructive answer to the negative-cycle criterion: not just a
certificate of suboptimality, but an actual improvement step, the combinatorial core of the
cycle-canceling algorithm explained in section 10.4.3 (mission 35-ch10c-algorithms). Its
correctness proof is one of the most intricate combinatorial arguments in the entire book — a
proof by contradiction using a multiset-union identity (Eq. (9.80)) to derive a smaller negative
cycle from an assumed non-uniqueness, itself resting on Proposition 9.24's Monge-like
characterization of unique bipartite matchings. Network duality, meanwhile, is the theorem that
explains why discrete convex analysis and network flow theory are so tightly intertwined
throughout this book: it is the general mechanism (matroid induction, min-max relations, the
M-convex aggregation and infimal-convolution closure properties) underlying nearly every
construction chapter 2 introduced informally and chapter 6 proved piecemeal.
None of these results are open — they are Murota's own account of cycle cancellation (section
9.5.2) and network duality (section 9.6). What this mission contributes is a faithful,
machine-checked formal statement of each, completing the platform's coverage of chapter 9 begun
in missions 12-network-flows and 32-ch09b-networkflows; no comparable formalization exists on
the platform (see Formalization scope).
Theorem 9.26's own proof needs the full weight of everything chapter 9 has built (Theorem 9.16's
potential criterion for integer flows, the conjugacy theorem of chapter 8), which this mission
does not re-prove (proofs are sorry throughout, per this pass's scope) but whose statement
still needs the induced-function machinery built faithfully: since the general framework's
optimal-value-type quantities can genuinely be -∞ (the book's own blanket hypothesis
f̃ > -∞ acknowledges this), InducedFTilde/InducedGTilde are EReal-valued, following the
same soundness discipline established in mission 31-ch08d-conjugacyduality for Lagrangian
duality's derived quantities.
Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity
vocabulary is redeclared from prior missions. Functions "on Zˢ" for S a proper subset of the
ground set are represented as ordinary V→Z functions required to vanish outside S
(SupportedOn), rather than as functions on a dependent subset type — a padding-with-zero
encoding consistent with this whole series' preference for a single ambient ground-set domain.
C[R→R] (univariate real polyhedral convex functions, needed only for Theorem 9.28's arc costs)
is formalized as ordinary midpoint-style convexity (IsConvexUnivariateR) rather than the
book's own polyhedral characterization, since polyhedrality plays no role in Theorem 9.28's
conclusion beyond ensuring the induced functions are well-behaved. All seven numbered results
found in this chunk's page range are placed in full, with no partial-coverage scope reduction.
Contributions completing any of the seven sorrys are welcome; the goal and Proposition 9.25
carry the most independent proof content.
Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.
A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary
∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary
δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes
Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and
boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The
M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is
its linear-arc-cost special case.
For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a
minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced
boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible
flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from
it, and every other placed result either specializes it directly or builds on that specialization.
Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).
This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.
None of these results are open — they are Murota's own account of network flow duality under
M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful,
machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in
mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow
min-cut results, deliberately leaving this block for later apparatus); no comparable formalization
exists on the platform (see Formalization scope).
The eight results span real- and integer-flow versions of two nested problem hierarchies
(MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative
cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3,
Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0
literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared
generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated
three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra
Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual
integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in
Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies
outside this chunk's page range; see Formalization scope.
Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity
vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R],
M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR);
"dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient
at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent
characterization for polyhedral convex functions, and a deliberate modeling choice recorded in
MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range)
definition of these two notation classes. All eight numbered results found in this chunk's page
range are placed in full, with no partial-coverage scope reduction. Contributions completing any
of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof
content.
In best arm identification with fixed confidence, a learner samples unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed , using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every -PAC strategy needs, in expectation, at least samples, where the characteristic time is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, , is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes at plug-in estimates and tracks it.
A strategy can only track if can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.
A canonical one-parameter exponential family is a family of laws , , on with density with respect to a reference measure . The law has mean ; the set of attainable means is the mean space . For means and the Kullback–Leibler divergence is
Bernoulli laws and Gaussian laws with known variance are the standard examples.
A bandit model is identified with its vector of means . is the set of models with a unique optimal arm , and is the set of alternatives. is the probability simplex. The transportation cost of proportions and the objects of the paper are
The arms are sorted so that . The parameterized Jensen–Shannon divergence is, for ,
For let for , let , and let . Finally
With : is continuous and strictly increasing on , , as , the equation has a unique solution , and
The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).
The result. Theorem 5 reduces a -dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires scalar inversions. It gives existence and uniqueness of , which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.
Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of near the end of its domain).
The infimum in Lemma 3 ranges over , a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which and coincide, lies outside and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation is a lemma of the proof, not Lemma 3.
For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of needs the monotonicity of each and of each ratio in the moving point , and the limit at rests on the second-best arm(s) only, which is where the ordering enters. Finally the analytic facts about (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.
Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm is index 0, arm is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with on . These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of . The reference measure and normalization are part of the structure but unused here.
The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. is never defined by choice: " is optimal" is a predicate, and Theorem 5 characterizes the set of such . The functions are the inverse of on and are evaluated only on . "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on assume only that arm is the unique best arm, which is weaker than the paper's standing ordering.
A formalization that replaces by , assumes the maximizer exists and is unique, or asserts only existence of some without the formula for , does not state these results and is ruled out.
A complete development needs: basic calculus of exponential families (the Bregman form of , its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about and , and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.
A false failure return is a product returned by a consumer as defective although it has no functional or cosmetic defect; managers attribute such returns to installation difficulties, a mismatch with the consumer's preferences, and remorse. Ferguson, Guide and Souza report (pp. 376–377) that false failures account for up to 80% of Hewlett-Packard's inkjet printer returns, roughly 5% of sales, and that the per-unit cost of a false failure return to computer manufacturers is around 25% of the product's price. The manufacturer absorbs most of that cost, while the retailer is the party able to prevent the returns in the short term, by spending time with customers before the sale and supporting them after it. The retailer bears the cost of that effort but captures only part of its benefit, so without an incentive it exerts too little.
The paper (Ferguson, Guide & Souza, MSOM 2006) models this as a single-period manufacturer–retailer problem with non-contractible retailer effort, and asks which contracts restore the supply chain's optimal effort and who gains from them. It belongs to the literature on supply chain coordination with contracts (Cachon 2003) and on channel rebates with sales effort (Taylor 2002); its object is a target rebate, a payment to the retailer for every false failure return below a target.
A manufacturer with unit cost sells to a retailer at wholesale price , who sells at retail price . Avoiding one false failure return is worth
where and are the parties' return-processing costs and , are the unit sale impacts of avoiding the return (p. 381). Both are assumed positive.
The retailer chooses an effort at cost , . At effort the number of false failures is a nonnegative random variable with mean , where is the expected number at the minimum effort . The coordinated supply chain earns
maximized at the coordinated effort . Without a contract the retailer earns and chooses the decentralized effort ; the manufacturer then earns .
Under a target rebate contract the retailer receives for every false failure below the target , so the profits become
The contract coordinates the supply chain when maximizes over . In the uniform case of §3.1, , and the contract must satisfy .
Assume and , and let be uniform. For every coordinating contract with , ,
The milestones follow the paper's §3–§3.1 and the appendix proof, in attack order: concavity of and optimality of (Eqs. (1)–(2)); in the interesting case; optimality of (Eqs. (3)–(4)); ; Proposition 1 (concavity of the retailer's rebate profit when ); its uniform instance; the uniform closed form (8); the first-order condition (9); the coordinating target (10) together with the admissibility condition ; the manufacturer's profit under a coordinating contract (25); the retailer's profit (27); and the retailer's gain in the two cases (30) and (31).
The result divides the effect of the contract between the two parties. The retailer is always at least as well off as without a contract; the manufacturer, who pays the rebate, gains exactly when the supply chain's optimal effort is at least twice what the retailer would exert alone. When this is equivalent to (p. 383), so a target rebate pays for the manufacturer only when its own stake in avoiding a false failure dwarfs the retailer's. The companion result (10) shows that for every rebate exactly one admissible coordinating target exists, and none for : a coordinating rebate is always larger than the manufacturer's own cost of a return.
The results are proved in the paper by calculus and algebra. None of them has a machine-checked proof that we know of, and nothing on Prove2Me models non-contractible effort or target rebates. The mission produces a checked version of the paper's model with the expectation taken as a genuine integral against the uniform law, a formal notion of coordination as the retailer's optimization, and statements that make explicit which hypotheses each step of the appendix uses. The definitions of effort-dependent profits and coordination are reusable for other effort-inducing contracts in the same paper and in the sales-effort literature.
The algebra of the appendix is short once the first-order condition (9) holds at . The substance is getting there. Coordination is defined by optimality of for the retailer's profit, and that profit involves the expectation , which is piecewise in : it equals only while , and beyond. Deriving (9) requires showing that is an interior maximizer, that the expectation is differentiable there with the closed-form derivative, and that the side condition keeps in the closed-form region. The converse direction of (10), that the formula for produces a coordinating contract, needs concavity of the piecewise profit on all of , which is where Proposition 1 enters.
Replacing the expectation by the global formula is the tempting shortcut and it changes the problem: for the formula exceeds the true expectation, and the retailer's maximizer, hence the meaning of "coordinates", changes with it.
All parameters are real numbers, bundled in a structure Params; and are Params.Mm and Params.Rr. Effort ranges over (Set.Ici 1); statements the paper makes for every positive effort (concavity of , the closed form (8)) are stated on . Cube roots are Real.rpow with exponent on positive bases. The uniform law is Lebesgue measure conditioned on , and the expectation is the Bochner integral against it. Coordination is IsMaxOn of the retailer's profit on Set.Ici 1 at .
Three conventions differ from the printed text, each recorded in the item's formalization note:
The side condition of §3.1 is a hypothesis of the goal and of the appendix milestones; without it a coordinating contract with exists and the "if" direction fails. The unused page assertion is not imposed.
The goal is not trivialized by its coordination hypothesis: coordination is the retailer's optimization over the true profit, and milestone (10) shows that coordinating contracts with exist for every , so the hypotheses are satisfiable (Example 1 of the paper, p. 384, is an instance). The retailer half of the goal is comparatively short under this definition of coordination; that is a property of the paper's theorem, not of the encoding. The manufacturer half needs (8), (9) and (25).
The development needs only Mathlib: real calculus (derivatives, concavity, Real.rpow) and Lebesgue integration against a conditioned Lebesgue measure. The model definitions (effort-dependent profits, coordination as the retailer's optimization) are reusable for the paper's other effort-inducing contracts. Contributions welcome: proofs of any milestone, and reusable lemmas on expectations of under uniform laws.
Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).
The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.
A graph has a finite vertex set and a set of 2-element subsets of . A weight is attached to each edge, and a set of edges has weight . A spanning forest of is an acyclic graph with . A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ( and acyclic), IsSpanningTree G T ( and a tree), and weight w T for a weight w : Sym2 V → ℕ.
A digraph has with for every directed edge . Each directed edge has a length . The length is extended by for non-edges. A directed path from to is a sequence of distinct vertices in which consecutive pairs are directed edges. Its length is . The distance is the minimum length of a directed path from to , and is when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.
Dijkstra's algorithm (Algorithm 12.14) with root and keeps a sequence of permanent vertices, a value and a sequence for each vertex. Step 1 sets , , , and , for . Step with scans from the last permanent vertex . For every temporary it sets , and on a strict decrease it replaces by followed by . Each step ends by appending to a temporary vertex of minimum , chosen arbitrarily among ties. The algorithm halts at Step . DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step .
For every halted state of every run, and every vertex ,
Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.
Theorem 12.18 certifies that one pass of steps computes all distances from and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.
All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.
The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's and never change again, and is always the length of the current . None of this is recorded in the final state itself. An argument over the steps of the run has to show that each remains a path with distinct vertices, including when edges of length allow ties. It also has to handle the value , where and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest , and this is a statement about cycles and components, not about counts.
SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's ; values off are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, is written and is assumed, which the bound presupposes.ℕ, and and distances are ℕ∞, where is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.
The difficulty is size. The choice-based program has one variable for each subset of products, in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only variables and constraints. This mission formalizes that equivalence, Theorem 7 of the paper.
There are products, . Under the Markov chain choice model a customer first visits product with probability . If the product she visits is offered, she buys it. Otherwise she moves from product to product with probability , or leaves without buying with probability . The paper assumes throughout that
For an offer set , is the expected number of visits to product while it is offered, which is its purchase probability, and is the expected number of visits to while it is not offered. The pair is the solution of the (Balance) equations
Dropping the constraints tied to gives the polyhedron
The network has resources, , with capacities ; the selling horizon has periods; product earns and consumes units of resource . With the probability of offering in a period, the (Choice Based) linear program is
and the (Reduced) linear program is
In (Reduced), is the expected number of visits to product while it is available and the expected number of visits while it is not.
Let be an optimal solution of (Reduced). Then there are subsets and positive scalars with such that
and for any such subsets and scalars the vector with and for is optimal for (Choice Based), with objective value equal to that of in (Reduced). In particular the two programs have the same optimal value.
The result. Theorem 7 replaces a program with columns by one with variables and constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).
Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of and through boundedness of .
The inequality "(Reduced) (Choice Based)" is a direct computation: averaging the (Balance) equations with weights lands in . The reverse direction is where the obvious argument fails. A point of has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that is bounded, which depends on the substochasticity , and that each extreme point is exactly some , which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.
Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding , (rho j i , the transition from to ) and the standing assumptions and ; the nonnegativity , implicit in the paper because the are probabilities, is an added field. is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. is a natural number entering as a real factor exactly where the paper writes it; , , carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.
Two conventions are disclosed. The paper defines by ; the formalization sets , which agrees when the are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.
The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.
A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.
Airlines, hotels and rental firms sell a fixed stock of capacity (seats on a flight leg, rooms on a night) over a finite selling horizon, and control revenue mainly by deciding which products (fare classes, rate plans) to make available at each moment. When customers substitute between products, the decision in each period is an assortment: a subset of products to offer. Talluri and van Ryzin (Management Science 2004) formulated this single resource revenue management problem as a dynamic program for a general choice model, and showed that structural properties of the optimal policy depend strongly on how customers choose.
The Markov chain choice model of Blanchet, Gallego and Goyal (technical report 2013; Oper. Res. 2016) describes substitution by a Markov chain on the products and approximates a broad class of random-utility models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study assortment and revenue management problems under this model. This mission formalizes their structural result for the single resource problem (Theorem 5): there is an optimal policy whose offer sets are nested in the remaining capacity and in the remaining time, so that it can be implemented by protection levels, one capacity threshold per product and period.
There are products . A customer arrives to purchase product with probability . If is offered she buys it; otherwise she moves to product with probability , and leaves with probability . The paper assumes and for all . For an offer set , the purchase probabilities and the visit counts of unavailable products solve the (Balance) equations
With product revenues , the (Assortment) problem is , and its (Dual) linear program is
In the single resource problem there are periods and units of capacity. In each period at most one customer arrives; a sale of product earns and uses one unit. The optimal expected revenue from period on with units left satisfies the (Single Resource) dynamic program
with and . An optimal subset is a maximizer of the problem on the right side. The marginal value of capacity is .
There exists an optimal policy, i.e. a choice of maximizers for all , , such that
The offer set shrinks as capacity runs down, and it is smaller when more periods remain.
Theorem 5 makes the optimal policy a protection level policy: for each product and period there is a threshold such that is offered exactly when at least units remain. The policy can then be stored as numbers instead of a table of subsets, and each product can be controlled separately, which is how airline inventory systems are organized. The paper also shows (Table 2, p. 1330) that the products need not be closed in revenue order: a higher-fare product can be closed before a lower-fare one, so the result is genuinely about nested sets, not about nested fare classes. Talluri and van Ryzin (2004) show that under the multinomial logit model an optimal assortment consists of a number of products with the largest revenues; the Markov chain choice model does not have this property (Table 1, p. 1328), so their structure of the optimal policy does not carry over directly.
The result is proved in the paper. No part of it is formalized on Prove2Me. The monotonicity of marginal values for an abstract choice model is published and proved as RevenueManagement.choice_marginal_values, stated over the definitions RevenueManagement_singleResource; milestone 5 is the same statement for this paper's dynamic program and can be bridged to it. A complete development here produces machine-checked Theorem 2 and Lemma 3 for the Markov chain choice model, which are reusable for any assortment problem under this model.
The obvious argument chooses, for each , any maximizer of the stage problem. This fails: the stage problems have ties, and an arbitrary choice of maximizers need not be nested, so the theorem is an existence statement about a coordinated choice. The dependence of on is through the solution of a linear system, so the effect of adding or removing a product on the other purchase probabilities has no simple sign, and optimal assortments need not be nested by revenue (Table 1, p. 1328). The link between two stage problems is that their revenues differ by the same constant for all products, and what has to be shown is that such a uniform shift moves an optimal assortment in a controlled direction. Revenues in the stage problems, , can be negative.
Products are Fin n, offer sets Finset (Fin n), the paper's is non-strict inclusion . The model is a structure with fields , and the standing assumptions , ; is added as a field because the are probabilities. is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it is the unique nonnegative one. The value function is defined by recursion on the number of periods to go, and is used only for . Maxima over are taken over the finite family of all subsets, so they are attained; dual optimality is "feasible and no worse than every feasible point".
One hypothesis is added to Theorem 5 and milestone 5, and disclosed: , implied by the paper's description of at most one arrival per period (it makes a probability). No sign condition is placed on the revenues, as on the page. Theorem 2 and Lemma 3 are stated for arbitrary real revenues, as the proof of Theorem 5 applies them to . The first inclusion of Theorem 5 is stated for : with units there is no decision, and the paper reads as . The existential requires every in range to be optimal for its stage problem; a statement without that clause would be satisfied by the empty sets and is ruled out.
Theorem 2 and Lemma 3 need LP duality for (Dual) and the (Balance) system; milestone 5 needs the standard induction on the dynamic program, or a bridge to the published choice_marginal_values (with arrival probabilities and choice model ). Proofs of any milestone, and bridges to published Mathlib or platform LP duality results, are welcome.
A retailer or an airline decides which products to make available, and customers choose among what is offered. When a preferred product is missing, many customers substitute to another product instead of leaving. Assortment optimization asks which subset of products to offer so that the expected revenue from a customer is as large as possible, and its answer depends entirely on the choice model used to describe substitution.
The Markov chain choice model was introduced by Blanchet, Gallego and Goyal (EC 2013; Oper. Res. 64(4), 2016), who showed that it contains the multinomial logit model as a special case and proposed it as an approximation of general random-utility choice models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study revenue management under this model. Their first result, the subject of this mission, is that the assortment problem, a search over all offer sets, is solved by one linear program with variables. The same paper uses this result for its dynamic single-resource and network results, which are the subjects of the companion missions II–IV of this series.
Timeline:
There are products . A customer arrives to purchase product with probability . If the product she visits is offered, she buys it. Otherwise she transitions to product with probability and checks whether is offered, or leaves without buying with probability . Throughout, , and for all .
For an offer set , let be the expected number of visits to product while it is offered (the probability that is purchased) and the expected number of visits to while it is not offered. The pair is the unique solution of the (Balance) equations
With revenue for product , the (Assortment) problem is . Two linear programs enter: the maximization of over the polyhedron
and its dual
For every optimal solution of (Dual), the set is an optimal assortment:
Theorem 2 reduces a combinatorial problem over offer sets to a linear program, so the assortment problem under the Markov chain choice model is solvable in polynomial time. The same structure drives the rest of the paper: the dual variables are used to show that optimal offer sets shrink when all revenues fall by a common amount, to show that the optimal offer sets of the single-resource dynamic program are nested in the remaining capacity and time, and to reduce the choice-based network linear program to a compact one.
The result is proved in the paper. This mission produces a machine-checked version of it and of its supporting lemmas; to the knowledge of the mission author no formalization of the Markov chain choice model exists. The definition layer (the model, the (Balance) solution, and (Dual)) is the first formal encoding of this choice model and is shared, with the same encoding, by missions II–IV.
The obvious route, comparing across offer sets directly, fails because is defined only implicitly through a linear system whose coefficient matrix changes with ; there is no closed-form expression that can be compared across offer sets, and enumerating the sets is exponential. The connection to linear programming needs an exact correspondence between the vertices of and the (Balance) solutions, which is a statement about polyhedra, not about Markov chains. Even well-posedness is not free: existence, uniqueness and nonnegativity of depend on the row sums being strictly below one. Mathlib has extreme points of convex sets but no ready-made theory of vertices of polyhedra or of linear programming duality in this form.
Products are Fin n (0-based), offer sets are Finset (Fin n) (the paper's is non-strict inclusion, so every subset including and is an offer set), and rho j i is , the transition from to . The model structure carries the paper's standing assumptions and (p. 1325) and the implicit nonnegativity . Revenues are arbitrary reals with no sign assumption. is (Fin n → ℝ) × (Fin n → ℝ), and extreme points are Mathlib's Set.extremePoints ℝ.
The pair is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it satisfies (Balance), is nonnegative and equals every solution, so all statements are about the paper's and not about a junk value. Every optimum (of (Assortment), of the linear program over , of (Dual)) is stated as "feasible and at least as good as every feasible point", never through sSup or sInf. The goal is stated for every optimal of (Dual), which is what the proof uses; uniqueness of is neither assumed nor claimed. Replacing the hypothesis " optimal for (Dual)" by " feasible for (Dual)" would make the statement false, and an existential over would weaken it; neither is the target.
No hypothesis beyond the paper's is added. Two printed index slips on pp. 1325–1326 (a garbled sum in the discussion after (Balance), and for in the proof of Lemma 1) are not part of any statement here.
Welcome contributions: the existence and uniqueness of (Balance) solutions via Neumann series for substochastic matrices, a characterization of vertices of polyhedra given by equality constraints and nonnegativity, and a strong duality statement usable for this primal–dual pair. These are reusable well beyond this mission.
Counting the objects that avoid every one of a list of conditions is one of the most frequent tasks in enumerative combinatorics: functions that miss no value, permutations that fix no point, integers that share no prime factor with a given number. The Principle of Inclusion-Exclusion converts such a count into an alternating sum of counts of objects that do satisfy prescribed conditions, which are usually far easier to compute. Chapter 7 of Keller and Trotter's Applied Combinatorics (2017 Edition) develops the principle in the abstract language of properties and applies it to three classical questions: the number of surjections, the number of derangements, and Euler's totient function.
This mission formalizes the first two applications, with the chapter's headline result, the closed formula for the number of surjections from an -element set onto an -element set, as its goal. The surjection count answers distribution questions of the form "in how many ways can distinct objects be handed to distinct recipients so that every recipient receives at least one", which the book illustrates with fifteen lottery tickets shared among four grandchildren ().
Let be a finite set and let be a family of properties: for each and each , either satisfies or it does not. For a subset write
so that .
Two families of properties are used.
In Lean, is a type with [Fintype X], the properties are a decidable predicate family P : Fin m → X → Prop, and is AppliedComb.InclExcl.N P S. The two families are AppliedComb.InclExcl.NotInRange n m on Fin n → Fin m and AppliedComb.InclExcl.FixesPoint n on Equiv.Perm (Fin n).
For all ,
Milestones 1 and 2 are the two ingredients the book names for the goal; milestones 3 and 4 are the parallel derangement application, which shares the definition of and milestone 1.
The result itself. The surjection formula is the standard closed form for , where is the Stirling number of the second kind; it gives for and as special cases, and it underlies counts of ordered set partitions, of onto colourings, and of occupancy problems in which every cell is filled. The derangement formula is the standard answer to the hat-check problem and leads directly to the limit (Theorem 7.12 of the book). The Principle of Inclusion-Exclusion in the book's "none of the properties" form is the common tool behind both and behind Möbius inversion in general.
Formalizing it. All results are classical and fully proved in the book. Mathlib contains inclusion-exclusion for unions and intersections of finsets (Finset.inclusion_exclusion_card_biUnion, Finset.inclusion_exclusion_card_inf_compl), the derangement count via its own recurrence (numDerangements, card_derangements_eq_numDerangements, numDerangements_sum), and Stirling numbers of the second kind (Nat.stirlingSecond) with their recurrence, but no closed formula for the number of surjections. The platform has union-form inclusion-exclusion (FamousTheorems.inclusion_exclusion_card_biUnion) and the limit, neither in the property form used here. This mission produces the property-indexed statement of the principle, the two computations, and the surjection count as a cardinality of surjective functions, in a form that downstream missions of the series (generating functions, Pólya counting) can cite.
The proofs are short on paper, and the work lies in the bookkeeping that the page leaves implicit. Two points stand out. First, the Principle of Inclusion-Exclusion is phrased with properties and rather than with a union of sets; connecting the two forms, or proving the property form directly, requires handling sums over the power set of together with the sign in . Second, the step "the result follows immediately, as there are -element subsets of " requires regrouping a sum over all subsets by cardinality, which needs Lemma 7.8's statement that depends only on and a count of the subsets of each size. The book's one-line arguments for Lemmas 7.8 and 7.10 ("a string of length from an alphabet of letters", "a permutation among the remaining positions") are counting identifications that have to be made precise for subtypes of Fin n → Fin m and of Equiv.Perm (Fin n).
Fin n ; this is an index shift only.Fintype.card {f : Fin n → Fin m // Function.Surjective f} and is Fintype.card {σ : Equiv.Perm (Fin n) // ∀ i, σ i ≠ i}. Defining by the formula, or by the sum, would make the goal hold by rfl; the counts are therefore cardinalities of the sets the book describes. is also not stated through Nat.stirlingSecond, which counts unordered partitions and differs by a factor .A complete development needs only Mathlib's finite-set, power-set and binomial-coefficient API. The property-form inclusion-exclusion (Theorem 7.7) and the two lemmas are reusable for other sieve-type counts, for example Euler's totient function (Theorem 7.14 of the book), which is not part of this mission. Proofs of any milestone independently of the others are welcome, as are alternative proofs of the goal (for instance via exponential generating functions) that do not pass through Theorem 7.7.
Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.
Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is -optimal for every : no exchange of edges shortens it. So the insertion bound is tight even for tours that local search with -changes cannot improve.
Timeline, as far as this mission is concerned:
A traveling salesman graph on nodes is the node set with a distance that is symmetric and satisfies the triangle inequality . A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL .
A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour and a node , TOUR is obtained by deleting an edge of minimizing and adding and ; COST is the resulting increase in length. An insertion method chooses nodes , starts from and sets ; INSERT is the length of . Nearest insertion chooses minimizing over ; cheapest insertion chooses minimizing COST. Ties are broken arbitrarily.
A -change of a tour deletes of its edges and adds other edges so that another tour is obtained. A tour is -optimal if no -change produces a strictly shorter tour.
The extremal instance is the circle : cities equally spaced on a circular road, with the smallest with or . The insertion run of Theorem 5 inserts the cities in the order and produces the zig-zag tour : city 1, then the even cities in increasing order, then the odd cities in decreasing order.
For and there is a traveling salesman graph with OPTIMAL on which some run of nearest insertion, and some run of cheapest insertion, return a -optimal tour with
The result. The Corollary shows that the worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive -change local search, for up to a quarter of the number of cities. Theorem 6 says more generally that -optimality with does not bound the ratio to the optimum below . Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.
Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of -optimality. This mission produces a reusable definition of -changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption ").
Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting between and minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for and , so the verification must use in an essential way. Second, -optimality is a statement about every tour at edge difference , not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference from below.
Nodes are Fin n, so the paper's node is index and is index ; subtour indices stay 1-based (, approximation ). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and ; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. -optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly of the tour's edges. Ratios are multiplied out.
COUNT needs a choice of shortest arc for antipodal pairs when is even; the formalization takes the arc through . The paper's argument does not depend on this choice.
Deviations from the printed text: the Corollary is stated for (the printed statement says only , but its proof uses the example of Theorem 5, which exists for ; for , the printed statement is false). Theorem 6 keeps its printed . In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).
The existence statements carry OPTIMAL , the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour -optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.
Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.
In a combinatorial auction a set of items is sold to bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.
The items are and the bidders .
The greedy price-update algorithm. Start with all bundles empty and all prices . For : let be bidder 's demand at the current prices; remove the items of from the bundles of the earlier bidders; let be the maximizing clause for in ; set for . Write for the prices after stage (), , and for the final bundles.
In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.
For XOS valuations , every demand oracle and every XOS oracle, and every allocation ,
The comparison with every allocation is the paper's comparison with the optimal allocation.
Three further statements are included without being milestones: the output is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with one has ; and the factor is attained on the paper's two-item, two-bidder example (p. 9).
Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio , and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no -approximation is possible with polynomial communication.
The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.
The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all stages, together with the fact that a maximizing clause for the demanded set bounds on every subset, which holds because it is a clause of itself, not merely an additive function agreeing with on . Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.
Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.
In a combinatorial auction a seller offers indivisible items to bidders, each of whom values bundles of items rather than single items. Allocating the items so as to maximize the total value (the social welfare) is the central optimization problem of the area: it models spectrum auctions, procurement and resource allocation, and it is NP-hard and hard to approximate for general valuations. A large literature therefore studies restricted classes of valuations without complementarities. Among them the class XOS (valuations that are a maximum of additive valuations, also called fractionally subadditive) sits strictly between submodular and subadditive valuations and has become a standard benchmark class in algorithmic game theory.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) gave, among other results, a randomized algorithm that approximates the optimal welfare for XOS bidders within a factor , which is at most . The algorithm rounds the standard LP relaxation and resolves conflicts between bidders using the XOS structure. This mission formalizes that guarantee (Theorem 3.2 of the paper).
A short timeline: Lehmann, Lehmann and Nisan (EC 2001) introduced the XOS terminology and a 2-approximation for submodular bidders; the conference version of the present paper (STOC 2005) gave the bound for XOS with demand and XOS oracles; Feige (STOC 2006) extended the ratio to XOS bidders with demand oracles only and gave a 2-approximation for subadditive bidders.
Items are and bidders are with . Bidder has a valuation assigning a real number to every bundle . An allocation is a tuple of pairwise disjoint bundles; its welfare is .
A clause is an additive valuation given by nonnegative item values , with . A valuation is XOS if there is a nonempty finite set of clauses with
A clause of attaining the maximum for is a maximizing clause for in ; an XOS oracle returns one (arbitrarily, if several attain it).
The LP relaxation has a variable for every bidder and bundle and asks to maximize subject to for each item , for each bidder , and .
Randomized rounding draws a preallocation : independently for each bidder , bundle is chosen with probability and the empty bundle with the remaining probability . The preallocation can give an item to several bidders.
The algorithm of §3.2: (i) draw a preallocation from an optimal LP solution ; (ii) let be the maximizing clause for in ; (iii) give each item to a bidder with for all . Write for the welfare of the resulting allocation.
For every XOS profile, every optimal LP solution , every choice of maximizing clauses, every tie-breaking in step (iii) and every allocation ,
Milestone 5 is stronger than the goal (it compares with the fractional value); the goal is stated against the integral optimum because that is what Theorem 3.2 asserts.
The bound is a constant-factor guarantee for a class that includes every submodular valuation, obtained from nothing more than the LP relaxation and the clause structure of XOS. It shows that the integrality gap of the configuration LP for XOS bidders is at most , a fact reused in later work on welfare maximization, online allocation and posted-price mechanisms. The per-item analysis (Lemma 3.3 and Eq. (1)) is the same "" correlation-gap argument that recurs in submodular maximization and prophet-inequality proofs.
The result is proved in the paper. To our knowledge it has no machine-checked proof. This mission produces a Lean statement and proof of the guarantee with the randomness made explicit, a reusable model of the configuration LP and of randomized rounding over bundles, and a formal version of the inequality in Eq. (1), which is independently useful.
Each piece of the argument is short; the work is in the bookkeeping. The preallocation is infeasible, so welfare cannot be read off from the rounding directly; the proof reduces it to per-item quantities and then lower-bounds by comparing with a different assignment of item that is not the algorithm's. The expectation of that auxiliary assignment involves a product of probabilities over bidders ordered by a conditional expectation, and the final bound needs the calculus inequality of Eq. (1) together with a summation by parts. A naive attempt to bound bidder by bidder fails, because a bidder's received bundle is not contained in its preallocated bundle, and the clause values of other bidders decide what it receives.
Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. XOS is stated through its expression: each comes with a nonempty finite clause set of nonnegative clauses, and is attained by a clause of and bounded by all of them. Normalization and monotonicity, the paper's standing assumptions (p. 1), follow from this.A complete development needs finite product distributions over bundles, the AM–GM inequality, monotonicity of , and a summation-by-parts argument. The LP and rounding model are reusable for the other randomized-rounding results of the paper; proofs of any milestone are welcome.
In a combinatorial auction a seller offers indivisible items to bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.
Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an ratio; Feige observed that the same algorithm achieves and that its ratio is at least (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio () for subadditive bidders by a different rounding.
Items are and bidders . Bidder has a valuation assigning a real value to each bundle . Every valuation is normalized, , and monotone, . A valuation is complement free if for all . An allocation is a tuple of pairwise disjoint bundles; its welfare is , and denotes the largest welfare.
The LP relaxation has a variable for each bidder and bundle, with for each item and for each bidder ; its objective is , with optimum . Randomized rounding lets each bidder independently draw bundle with probability and with the remaining probability. The result, a preallocation, has expected welfare but may give an item to several bidders.
The algorithm takes and:
For all sufficiently large , for normalized, monotone, complement-free valuations and an optimal LP solution with value :
Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor into a feasible allocation losing only a factor for subadditive objectives. The same argument applies to the -duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every load estimate.
The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant in place of , a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.
The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold grows with while the mean stays at most , and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event- bound needs the preallocation's welfare as a sum of independent variables in , which requires rescaling by and monotonicity.
Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.
Explicit constants and conventions that replace the paper's notation:
Printed slips resolved in the statements:
Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible , neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.
Submodularity — the diminishing-returns property on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.
Let be a finite ground set. A function with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): for all ( componentwise max/min), and (TRF[Z]): there is with for all , where is the all-ones vector. An L-convex function is one whose lift to the extended ground set is L-convex; equivalently (Theorem 7.1), satisfies the translation-submodularity axiom (SBF[Z]): for all and all nonnegative integers . Discrete midpoint convexity asks componentwise. For a positive integer, a point satisfies scaled local optimality if for every .
Assume is a positive integer and . (1) If is L-convex with for all , and satisfies for all , then and there is with the componentwise bound
(2) If is L-convex and satisfies the two-sided version, then there is with . The bound is a genuine vector (lattice-order) inequality, not an -norm bound — the form later chapters' applications need.
Theorem 7.1: L-convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L-APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors , mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition .
The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via . The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.
Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.
A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.
The ground set is a Fintype with DecidableEq; is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and
(SBF[Z]) are stated for all of , not restricted to , so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's
structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same
concern for dom f). L-convexity is represented via an explicit lift to Option V,
matching the book's own primary definition, with the direct axiom (SBF[Z]) kept as a
separate object related to it by Theorem 7.1.
A trivializing formalization of the goal would convert its componentwise vector bound into an
-norm bound (losing the direction-of-approach information the vector form carries)
or drop Part (1)'s periodicity hypothesis ; neither is done here.
Propositions establishing dom g as an L-convex set, the L/L relationship (Theorem
7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure
properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets
for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom
vocabulary, mirroring chunks 06→07.
The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.
Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.
Timeline of the thread this mission belongs to:
Let be -dimensional Euclidean space and let be a nonempty, closed, bounded, convex set. Its dimension is the dimension of its affine span , the smallest flat containing .
For let be the point of nearest to ; it exists and is unique. The image of with respect to is
the reflexion of through . The reflexion process starts at and sets as long as (3.2). Either the process terminates with some , or it produces an infinite sequence of points outside .
The family of supporting half-spaces of consists of the closed half-spaces whose bounding hyperplane touches . The paper observes that the half-space through normal to is the member of farthest from , so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family .
A sequence of points outside is Fejér-monotone with respect to if and for all . Two points are symmetric with respect to a flat if their midpoint lies in and is orthogonal to .
For every nonempty closed bounded convex with affine span , every and every run of the reflexion process:
No number of steps is fixed: termination is finite but not uniformly bounded.
The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of , so a solution can be read off.
Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.
The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit lies on the boundary of ; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through , which keeps the iterates on a sphere around . For a convex body there are infinitely many supporting hyperplanes near , and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of at boundary points near are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.
Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of to alone can be expected.
EuclideanSpace ℝ (Fin n). is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension ", "the point of nearest to ").IsImage A p p₁ holds when for a nearest point of ; the nearest point is not chosen by a function. For closed convex nonempty this relation is a function on . A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering are unconstrained. Every statement quantifies over every run from every ; a formalization that only asserts the existence of some terminating run is ruled out.affineSpan ℝ A; is affineSpan ℝ A = ⊤, is affineSpan ℝ A ≠ ⊤. No separate natural number is introduced.IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires and strict alternation for (strict inequality, as printed).frontier A; distances to sets are Metric.infDist.exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.
Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).
Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.
Fix a dimension and an matrix whose transpose is substochastic: all entries of are nonnegative and every column sum of is at most . Assume also as . With Markovian routing, is the routing matrix of an open network of queues.
Vectors carry the norm , and matrices carry the maximum absolute column sum (Eq. (2.5)). is the space of paths that are right-continuous with left limits on . For a path , is the vector of coordinatewise sup norms, , and .
The reflection of is the pair with and
The last condition says that increases only when . In queueing terms, is the vector of queue contents and the cumulative idleness. The operator , where coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write .
For all with reflections ,
The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on .
Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod and topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order in the netput produces an error of at most in the idleness process.
On the formal side, the results are proved in the paper, but neither the reflection map nor has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.
The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of is allowed at a time where even if was positive just before. Existence needs the iterates to converge in and the limit to satisfy (2.1)–(2.3). The explicit constants involve , and . The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from .
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to matters. Membership in is the predicate IsCadlagOn T x: right-continuous on , left limits on , and (redundantly) bounded on . The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure of is zero". For this is equivalent to . is Nat.iterate, is Mathlib's matrix inverse (invertible under the standing assumptions), and is a tsum stated together with its summability.
Corrections and conventions, each disclosed in the item concerned:
A trivializing formalization would read (2.3) through a Bochner integral, which is for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.
Welcome contributions: a general API for càdlàg paths on (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.
MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least literals, it satisfies at least a fraction of the optimum.
B2 is the ancestor of a line of work on MAX-SAT approximation:
A literal is a variable or its negation . A clause is a finite set of literals. A truth assignment is a set of literals containing no pair ; it satisfies a clause when . An input is a finite set of clauses, and is the largest over subsets satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least distinct literals.
Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight per clause, starting from , , . While some literal of LIT occurs in a clause of LEFT, it picks any such literal . Let YT be the clauses of LEFT containing and YF those containing . If , it makes true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with . Finally it removes from LIT. When no literal of LIT remains in LEFT it returns SUB.
The choice of is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio and its maximum over inputs of size at most .
For every , every in MS(k) and every SUB choosable by B2 on ,
and for every there are in MS(k) and a choosable SUB with and
The paper states equality "for all sufficiently large " for every . At this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for . A separate item states that at the ratio is never attained.
The bound is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds against rather than against , a feature the paper points out. For the constant was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.
Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at . The paper's proof is complete; to our knowledge no machine-checked version exists.
The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is times to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both and . Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.
Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. is a maximum over the finite, nonempty family of satisfiable subsets.The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the tightness family, and of the correction.
An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.
The dividend model is a stationary Markov Decision Model on the integers: the state is the current risk reserve, the action (for ; only is available once ruined) is the dividend paid, the reward is , and the reserve evolves by i.i.d. increments (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of and its largest-maximizing policy (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that 's shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability , making the effective one-period discount rather than .
The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity ; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold is finite (not merely well-defined) and that is a simple barrier above it; Proposition 9.2.8 proves the increment property below that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.
Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.
The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a
band-policy is specified by an alternating chain of thresholds with a positive-width gap condition on every wave, and the policy's four
piecewise branches case-split on which wave (if any) the current state falls into. This mission
renders it existentially over the witnessing rather than as one closed-form function, a
faithful but more verbose transcription that avoids conflating the different branch conditions.
A second difficulty is Proposition 9.2.6's own finiteness claim: is a supremum over a
subset of that could, in principle, be unbounded, and Mathlib's convention for
sSup over the naturals returns a finite junk value () even for an unbounded set — using it
directly would silently trivialize "" into a claim that is true regardless of the
proposition's actual mathematical content. This mission instead states the proposition by
exhibiting the finite value of directly, so that " is finite" survives as genuine
content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's
random-horizon consumption-investment model shares no state space, action space, or definitions
with the dividend model of the goal, despite both appearing in this chunk's assigned page range;
it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting
theory, but is excluded from the milestone list proper since it plays no role in the goal's own
proof.
The dividend model's transition law is built from Mathlib's PMF (probability mass function)
type on , which supplies the "probabilities sum to one" fact automatically rather than
as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout
this mission use this whole book series' Filter.limsup-of-truncations convention for
infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership
boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment
model of §9.1 is formalized with the number of risky assets as an explicit type parameter and
its admissible-portfolio and domain restrictions as separate, citable fields rather than folded
silently into the reward or transition definitions.
Every mission in this series so far has treated a control problem that already lives in discrete time: a decision maker observes a state, chooses an action, and the process moves to a new state at the next integer time step. Many real systems evolve in continuous time instead — a machine that runs deterministically until it randomly breaks down and is repaired into a new condition, an inventory that drains continuously until a random demand arrives, a population that grows deterministically between random catastrophic events. Chapter 8 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) shows that an entire class of such continuous-time control problems — Piecewise Deterministic Markov Decision Processes, where the state moves along a deterministic, controlled flow between randomly-timed jumps to a new state — can be solved by exactly the discrete-time machinery this book's series has already built, once the problem is re-expressed as a Markov Decision Model at the jump times themselves. This mission covers that embedding and its consequences (§8.2), and a simpler, discrete-state special case, the continuous-time Markov Decision Chain, treated with both an infinite and a finite time horizon (§8.3).
A Piecewise Deterministic Markov Decision Model (Definition 8.1.1) consists of a Borel state space , a Borel control space , a deterministic drift governing the flow between jumps, a Poisson jump clock of rate , a kernel giving the distribution of the post-jump state, a reward rate , and a discount rate . A control is a whole measurable function fixed at each jump time and applied until the next one — so the "action space" of the embedded discrete-time problem is itself a function space, a genuinely new technical wrinkle this book's earlier chapters never face. Embedding at the jump times produces a discrete-time Markov Decision Model whose reward and kernel are themselves integrals of the original data against the flow (Eqs. (8.4)-(8.5)); Chapter 7's infinite-horizon existence theory, already developed for a general Borel state space, applies directly to this embedded model once its own compactness and semicontinuity hypotheses are checked. Checking them forces a further enlargement of the control space to the relaxed controls — measurable functions into probability measures on rather than itself — which is compact in a suitable topology where the space of literal control functions is not.
The goal, Theorem 8.2.6, is the chapter's central existence result: given a continuous upper bounding function with the discrete embedded model's own contraction-type condition and a package of continuity/compactness assumptions, the value function of the model embedded with relaxed controls is bounded, upper semicontinuous, and a genuine fixed point of the maximal- reward operator, and an optimal relaxed Markov policy exists. The milestones build up to it and extend past it: Theorem 8.2.1 establishes the foundational fact that the continuous-time expected reward of the original process equals the discrete-time embedded model's own value — the correspondence every other result in the chapter relies on; Lemma 8.2.5 is the technical semicontinuity-preservation step the goal's proof needs; Theorem 8.2.7 upgrades the goal's relaxed optimal policy to a genuine, nonrelaxed one under an uncontrolled-flow or convexity condition; Theorem 8.2.8 gives the classical Hamilton-Jacobi-Bellman verification technique as an alternative, differential route to the same value function. Section 8.3's continuous-time Markov Decision Chain — the same theory specialized to a countable state space, transition rates in place of a kernel, and an uncontrolled flow — is covered for both an infinite horizon (Theorem 8.3.1) and, the more finance-relevant case, a finite horizon with a terminal reward (Theorems 8.3.2-8.3.3).
Piecewise Deterministic Markov Processes have no substrate anywhere in Mathlib or on the platform, and this mission's content is a genuine method, not just a specialization of existing results: it shows how to reduce an entire continuous-time control problem to the discrete-time theory already available, at the cost of enlarging the state of the discrete embedded problem's own data (which becomes an integral against a whole flow, not a pointwise value) and enlarging the control space when compactness is needed for existence. This mission is careful to keep two distinctions the book itself insists on separate: relaxed versus nonrelaxed controls (Theorem 8.2.6 produces only the former; recovering the latter is Theorem 8.2.7's own, harder, conditional content), and the general Piecewise Deterministic model of §8.1-8.2 versus the simpler, discrete-state Markov Decision Chain of §8.3, which is a genuinely different structure (sums over a countable state space rather than integrals against a controlled flow), not an instance of the general model specialized after the fact.
The central formalization challenge is representing the continuous-time expected reward (Eq. (8.2)) faithfully, since the book itself only asserts the existence of a probability space carrying the jump-time/post-jump-state process with a specified conditional law, citing general marked-point-process theory rather than constructing it. This mission builds that probability-space data directly — via Mathlib's conditional expectation, conditioning on the current post-jump state — rather than treating as a bare hypothesis-only quantity, so that Theorem 8.2.1's value-equality claim is a genuine, non-vacuous correspondence between two independently-defined objects (a continuous-time path functional and a discrete-time recursion) rather than true by definitional fiat. A second, compounding difficulty is that the same correspondence must be built twice — once for the general flow-driven process (§8.2) and again, independently, for the discrete-state jump process of the finite-horizon chain (§8.3) — since the two models share no state-space structure. A third difficulty specific to Theorem 8.2.8 is that its Hamilton-Jacobi-Bellman verification argument is genuinely differential (a process generator built from a gradient, a self-referential closed-loop control solving its own ODE), unlike every other result in this chapter, which works through the discrete-time embedding alone.
The book's own topology on the control-function space (the coarsest making certain
integrals measurable) and the Young topology on the relaxed-control space (which the book
cites as making separable, metric and compact, without reconstructing it) are not rebuilt
from scratch; continuity/compactness hypotheses that need a topology on these spaces are stated
directly against the pointwise/product topology on the underlying function types, a faithful but
representationally simpler stand-in documented in MODERATION_NOTES.md. The embedded kernel
(Eqs. (8.4), (8.7)) is bundled as data satisfying its own defining integral identity rather
than literally constructed as a mixture of pushforward measures — a routine but heavy argument
that would add no mathematical content beyond the formula itself. This mission's own goal
(Theorem 8.2.6) explicitly produces a relaxed-control optimal policy, not a nonrelaxed one:
stating it with a -valued policy instead would silently substitute Theorem 8.2.7's strictly
harder, conditionally-true conclusion for Theorem 8.2.6's own unconditional one, exactly the
trivializing formalization this chapter's own structure warns against.
09b's Sections 9.3-9.4).Scaling algorithms are one of the standard techniques for solving discrete optimization problems efficiently: instead of searching a huge integer domain directly, an algorithm first solves a coarsened version of the problem — checking optimality only against neighbors reached by a large step size — and then refines the resulting approximate solution down to the true optimum. This strategy is only as good as the guarantee that a coarse-scale local optimum is provably close to a true, fine-scale global optimum; without such a guarantee, refinement could require an unbounded number of steps. Results providing this guarantee are called proximity theorems, and they are a standard tool across combinatorial optimization, from network flow scaling algorithms to submodular function minimization.
M-convex functions, the subject of this chapter, are exactly the class of discrete convex functions for which the classical local-optimality test of chapter 3 (checking a full neighborhood of up to sign patterns) sharpens to a much smaller, purely pairwise test: checking for every pair of coordinates . This mission formalizes the chapter's central definitional equivalence (Theorem 6.2), this pairwise optimality criterion (Theorem 6.26), a structural minimizer-cut lemma (Theorem 6.28), and the chapter's capstone, the M-proximity theorem (Theorem 6.37) — the result that makes M-convex scaling algorithms provably correct, with an explicit, dimension-and-scale-only distance bound between a coarse-scale local optimum and a true global minimizer.
Let be a finite ground set. A function with nonempty effective domain is an M-convex function if it satisfies the exchange axiom (M-EXC[Z]): for and in the positive support of , there is in the negative support of with
An M-convex function is one whose lift to the extended ground set — defined by when , and otherwise — is M-convex; equivalently (Theorem 6.2, below) satisfies the axiom (M-EXC[Z]), a variant of (M-EXC[Z]) that additionally allows a single-coordinate move ( alone, with no compensating ). Every M-convex function is M-convex, but not conversely. For a positive integer, a point satisfies the scaled local optimality condition at scale if for all relevant — a check against neighbors steps away rather than adjacent ones.
Assume is a positive integer and .
Both bounds are exact and specific to their hypothesis class; replacing either with an unspecified function of and would discard exactly the content chapter 10's algorithms rely on.
Theorem 6.2: M-convexity (defined via the lift) is equivalent to the direct exchange axiom (M-EXC[Z]) — the chapter's central definitional theorem, needed to work with M-convex functions without repeatedly invoking the lift construction. Theorem 6.26 (the M-optimality criterion): global optimality of at is equivalent to a purely pairwise local check, for all (plus, in the M case, ). Theorem 6.28 (the M-minimizer cut): from any point and any coordinate pair minimizing a one-step exchange, one can certify a coordinate-wise bound that some global minimizer must satisfy — the structural fact underlying both the domain-reduction algorithm and, via the same proof technique, the proximity theorem itself.
The result itself. Theorem 6.26 already sharpens chapter 3's local-to-global criterion (checking a full -point neighborhood) to an -size pairwise check — the minimum spanning tree optimality criterion is a direct special case. The proximity theorem builds on this to control what happens when the local check is only performed at a coarse scale : it guarantees that scaling-based algorithms, which alternate between coarse-scale local search and scale reduction, terminate with a guaranteed-close approximation at every stage, with an explicit linear-in-, linear-in- error bound rather than a qualitative "eventually converges" guarantee.
Formalizing it. No matching item exists on the platform for M-convex functions, the exchange axiom, or a discrete proximity theorem of this kind. This mission gives the first formal statement of the M-optimality criterion and the M-proximity theorem, together with the exchange-axiom / lift-based-definition equivalence (Theorem 6.2) that the rest of the M-convex function theory (chunks 07, and indirectly 10–14) is built on.
The natural first attempt at Theorem 6.37 is to try a direct coordinatewise argument: since the scaled hypothesis holds for every pair , one might hope to bound coordinate by coordinate independently. This does not work, because a single application of the exchange axiom only ever improves by trading one coordinate down and one other coordinate up simultaneously — there is no way to move a single coordinate toward a minimizer in isolation without accounting for where the compensating mass goes. The actual proof instead fixes a target coordinate , constructs a chain of strictly decreasing function values by repeatedly applying (M-EXC[Z]) against a fixed near-optimal point (exactly the technique of Theorem 6.28's proof), and then bounds how far each other coordinate can move along this chain using the scaled hypothesis itself, before summing those bounds via the M-convex domain's hyperplane constraint constant to recover the bound on . The chain construction, not a per-coordinate estimate, is what makes the linear-in- bound provable at all.
The ground set is a Fintype with DecidableEq; is (V → ℤ) → WithTop ℝ. M-convexity is represented via an explicit
lift to Option V (none standing for the extended ground set's new element ), matching the
book's own primary definition; the direct exchange-axiom form is a separate predicate related to
it by Theorem 6.2, not conflated with it. `‖x_\alpha - x^*|_\infty \le c$ is stated pointwise.
A trivializing formalization of the goal would replace either exact bound, or
, with an unspecified asymptotic bound, or merge the two hypothesis classes into a
single weaker statement; neither is done here. Propositions establishing dom f as an M-convex
set, the M/M relationship (Theorem 6.3), and several structural closure properties
are cut from this mission's scope (not needed by the chosen items' statements — see
MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 07, which
builds directly on this chunk's exchange-axiom vocabulary. Contributions building the
arg min f M-convexity corollary (Proposition 6.29) or the scaled minimizer cut (Theorem 6.39,
the direct generalization of Theorem 6.28 drafted here) are welcome.
Training a statistical model by empirical risk minimization means minimizing an average of losses over a parameter vector , where both and can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.
Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).
Let be twice continuously differentiable losses and
For a sample of size , the minibatch gradient is . For a sample of size , the subsampled Hessian is .
Assumption 1 requires constants with for every and every Hessian sample. It also requires a bound on the second moment of the stochastic gradient. denotes the minimizer of .
Algorithm 2 turns correction pairs into a matrix . With , it starts from and applies the BFGS update
for .
Algorithm 1 (SQN) runs for . It draws a gradient sample and steps
where for and , , afterwards. Every iterations it forms the block average of the last iterates and a new pair
Samples are drawn independently and uniformly among the subsets of their size. The step length is .
There are , depending only on the problem data, such that every matrix Algorithm 1 applies satisfies . Moreover, for every ,
The constants are not fixed numerically. The goal asserts a rate of order with an explicit constant in terms of them.
The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.
The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.
The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.
On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of that is uniform over all runs and all . The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.
Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices start at as in the paper. In the corollary, is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. and are -measurable, the sample is -measurable, and unbiasedness is a conditional expectation. Integrability of is part of each conclusion, so a junk-zero integral cannot satisfy it.
Two corrections to the paper, each labelled in the item titles and notes:
Smaller conventions:
Trivializing encodings are ruled out: is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all .
Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.
The classical separating hyperplane theorem says that any two disjoint convex sets in can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.
L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in , no matter how large or complicated the sets are.
Let be a finite ground set. A nonempty set is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — , where are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — , where is the all-ones vector. A distance function satisfies for every ; it satisfies the triangle inequality if for all . The admissible-potential polyhedron of is
The convex hull of a discrete set is written .
If are disjoint L-convex sets, there exists such that
Dropping the restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.
Theorem 5.2: an L-convex set is hole free () — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: is L-convex if and only if for some integer-valued distance function satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.
The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a -separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.
Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.
The natural first attempt at Theorem 5.9 is to try to construct directly from the structure of — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents via distance functions (Theorem 5.5), combines them into , and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating pattern around the cycle is exactly the vector — with the cycle's negativity translating directly into the required gap of at least . Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.
The ground set is a Fintype with DecidableEq; is a
Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum
are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation
invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently
return a junk value on an unbounded set. The conclusion is stated as
, an addition-based
reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while
remaining equivalent whenever both sides are finite.
A trivializing formalization of the goal would drop the constraint on
(recovering the classical, L-convexity-independent separation theorem) or fix a single
coordinate pattern rather than asserting existence over the full three-valued family; neither is
done here. Theorem 5.5 is stated existentially rather than via the book's named bijection
(a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15),
and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and
(4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible-
potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex
bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.
Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.
Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.
Let be a finite ground set. A set function with and is submodular (the class ) if
Its base polyhedron and submodular polyhedron are
where ; a supermodular function is one with submodular. A nonempty set is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for and in the positive support of , there is in the negative support of with both and , where is the characteristic vector of . A polyhedron is integral if .
For submodular set functions ,
with both sides attained. If are integer valued, is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.
Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: is M-convex if and only if for some integer-valued submodular — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular dominates a supermodular pointwise, a single vector separates them ( pointwise on every subset), integrally when are integer valued — derived, in the book, as a direct corollary of the goal theorem.
The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.
Formalizing it. No matching item exists on the platform (searches for "submodular set
function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's
Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general
submodular set functions or their polyhedra). This mission gives the first formal statement of
the theorem at its natural generality, together with the M-convex-set viewpoint that motivates
the rest of the book, and Frank's separation theorem as an explicit worked corollary.
The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize over ) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each 's effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data () are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.
The ground set is a Fintype with DecidableEq; subsets are Finset V, vectors are
V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly ); supermodular functions in WithBot ℝ; comparisons across the two use an explicit
embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a
common EReal witness, so that "both sides attained, at the same value" — not merely "sup
equals inf" — is what the Lean statement asserts, which is essential since the integrality
clause's whole content is about which point attains the maximum.
A trivializing formalization of the goal would drop the integrality clause (leaving unqualified
LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the
"is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is
stated as the existential "iff" (some integer submodular realizes ) rather than
reifying the book's own named bijection explicitly — a deliberate, documented scope
reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions
building the explicit map, the Lovász extension (needed for Theorem 4.16, not drafted
here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build
on this chapter's vocabulary) are welcome.
Every model in Chapters 2-4 assumed the controller sees the whole state before acting. Real control problems rarely offer that: a machine's true wear level, a customer's private valuation, a hidden regime driving asset returns — these are exactly the situations a decision-maker must act on despite never observing them directly, learning about them only through their effect on what is observed. This is the subject of Partially Observable Markov Decision Processes (POMDPs), introduced independently in operations research (K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, 1965) and studied extensively since as the right model for sequential decisions under hidden state. The central difficulty such a process raises is structural, not just computational: the state includes a component the controller never sees, so the very theory built in Chapter 2 — which assumes the controller's policies can depend on the full current state — does not apply. Bäuerle and Rieder's Chapter 5 resolves this by an idea with a long pedigree in stochastic control (Bayesian filtering, going back to R. E. Kalman and R. S. Bucy's filtering theory, and D. Blackwell's 1965 discounted-dynamic-programming treatment of the "state of information"): replace the unobservable state by the controller's own belief about it — a probability distribution, updated at every step by Bayes' rule — and show the resulting belief-state process is once again an ordinary, fully observed Markov Decision Model.
A Partially Observable Markov Decision Model (Definition 5.1.1) has data : state with observable and unobservable; feasible actions depending only on ; a stochastic kernel giving the joint law of the next state; initial law of ; rewards ; discount . A policy (Definition 5.1.3) is a sequence of decision rules , each depending only on the observable history — never on any . The objective
(Equation (5.2)) carries an extra expectation over the unknown that Chapter 2's objective never had.
Assuming has a density against reference measures, the Bayes operator and the filter recursion , (Equations (5.3)-(5.4)) compute the posterior law of given everything observed, purely from the observable history. Theorem 5.2.1 confirms is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats as an ordinary, fully-observed state, with its own kernel (built from and the marginal ), reward , and terminal reward .
under the Structure Assumption of Theorem 2.3.8; and if maximizes for each , then defines a policy optimal for the original -stage POMDP. This is where the reduction pays off: an ordinary Bellman equation, of exactly the form Chapter 2 already solves, for a problem that had no Bellman equation at all in its original, partially-observed form.
Lemma 5.2.2 (the filter-recursion identity, the technical engine behind everything that follows), Theorem 5.2.1 (the filter is truly the conditional law — without this, would be merely a formula, not a meaningful belief), and Theorem 5.3.2 (the value of the filtered model exactly equals the value of the original POMDP, policy for policy — without this, solving the filtered model would solve a different problem).
Theorem 5.3.3 is the standard justification, made precise, for the single most common technique
in applied sequential decision-making under uncertainty: replace an unknown parameter or hidden
state by a running Bayesian estimate, and optimize as if that estimate were the true state. This
technique underlies applications from inventory control with unknown demand to adaptive clinical
trial design, and Chapter 5's own closing application (two-armed Bernoulli bandits, taken up in
chunk 05b) is a direct instance. The reduction also has real content beyond convenience: it
shows the value is unchanged (Theorem 5.3.2), not merely that a good heuristic policy exists —
the filtered model's optimum is the true POMDP optimum, not an approximation to it.
No result of this chapter has a machine-checked proof on Prove2Me at the time of writing, and no substrate exists for POMDPs, filtering, or Bayes-operator constructions on the platform. Formalizing this mission means building, from Mathlib's general kernel and probability-measure infrastructure, the first POMDP/filtering vocabulary on the platform: a policy class restricted to observable histories, a recursively-computable posterior, and the value-equality between a partially and a fully observed reformulation.
The obstacle is not any single hard inequality but a representational one: an admissible policy for the original problem is a function of a growing observable history, not of a fixed-size state, so the value function cannot be written as a simple recursion over a Markov chain the way every earlier chapter's could. The chapter's insight is that the belief — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: depends on the observable history only through , never on more of the past. Recognizing this, and giving the right measurable structure to serve as a genuine Borel state space, is what makes Definition 5.3.1's reformulation a legitimate Markov Decision Model rather than an informal analogy. A formalization that let 's type be an unstructured "distribution object" with no Borel structure, or that quietly assumed the value functions of the filtered model already satisfy the Bellman equation, would miss this content entirely.
are abstract measurable spaces; the transition kernel is a genuine
MeasureTheory.Kernel, not assumed to arise from an i.i.d.-noise-driven transition function (the
form every earlier finance chapter's market used) — the chapter's own examples (Hidden Markov
Models, Bayesian models) do not have that special form in general. Observable histories are
represented as (junk-padded) sequences , rather than
dependent finite tuples, with a decision rule's dependence on only the first /
coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping
while remaining exactly equivalent to the book's own typing. The belief state
is MeasureTheory.ProbabilityMeasure E_Y, giving a genuine measurable
structure via its standard weak-topology Borel σ-algebra — the formalization scope this chunk's
own pitfall demands, ruling out an ad hoc encoding of "the space of distributions." The Bayes
operator and the filtered kernel are carried as data (functions landing genuinely in
ProbabilityMeasure/Kernel types) characterized by their defining ratio-of-integrals or
pushforward formulas, rather than constructed by normalizing a raw measure inline — proving
that normalization is a routine Fubini calculation the book itself does not spell out, and would
be proof content misplaced in a definition. Theorem 5.2.1's conditional-probability statement is
formalized via the book's own Equation (5.5) test-function identity rather than Mathlib's
conditional-expectation-with-respect-to-a-sub-σ-algebra machinery, since the two are equivalent by
the standard characterization of conditional expectation and the test-function form is what the
book's own proofs actually use. The Structure Assumption of Theorem 2.3.8 is restated locally
(existential value-function and decision-rule classes with its three defining clauses), per this
project's rule against importing another chunk's copy of shared machinery. Reusable beyond this
mission: the kernel-based expectation recursion (Ex/Vpi) is natural substrate for any later
mission needing a Markov Decision Process driven by a genuinely abstract stochastic kernel rather
than an i.i.d.-noise transition function. Contributions completing any milestone's sorry, or the
goal's, are welcome.
Many first-order methods in optimization are fixed-point iterations of a nonexpansive map : proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.
Timeline (as recounted in the paper's related-work section):
Let satisfy for all (the Euclidean norm), and assume the solution set is nonempty. The residual is , , and the averaged operator is .
Powell's weight. For , if and otherwise, with .
Window matrices. For vectors and , let be their unnormalized Gram–Schmidt orthogonalization (3.2), , and
The matrix norm is the induced operator norm.
Algorithm 3.1 (AA-I-S-m). With parameters , and max-memory : start from , , , and . At iteration , set and , orthogonalize against the current window, and restart the window (memory back to , replaced by ) if the memory would exceed or . Then apply one Powell-regularized rank-one update to obtain and the trial point . The trial point is accepted if (and increases); otherwise .
The only hypotheses are nonexpansiveness of , and the parameter ranges. The limit is not specified: it depends on and the parameters.
The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.
The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).
The accelerated step need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding , requires a bound on that holds uniformly along the run; without the Powell regularization can be singular, and without the restart rule can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.
is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; is rankOne ℝ u ŝ; is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by , the parameters and , and a sorry-free check that runs exist (for ) was built locally. The reset of in line 8 is local to its iteration. is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.
Line 9. The paper prints , derived from (3.3) through , which fails when the window starts afresh (). The mission uses (3.3) there: when , and the printed formula when .
Milestones of §4.1 and Corollary 3.5 carry the hypothesis for all , as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on , contractivity of , or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.
Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality , quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's ) and of the convergence steps are all welcome.