Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Two strategic levers shape the balance of power between a manufacturer and the retailer that resells its product. The first is strategic inventory: a buyer that orders more than it sells today, and carries the surplus into the next period, weakens the supplier's leverage over tomorrow's wholesale price. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period channel the buyer withholds inventory exactly when its unit holding cost is below . The second is supplier encroachment: a supplier that can sell directly to consumers competes with its own buyer. Arya, Mittendorf and Sappington (Marketing Science 2007) showed that the threat of encroachment can lower wholesale prices and benefit both parties.
Guan, Gurnani, Geng and Luo, Strategic Inventory and Supplier Encroachment (MSOM 2019), combine the two levers in one game. Their headline qualitative finding is Proposition 4.2. When the supplier's direct channel is costly, but not quite too costly to use, the buyer keeps withholding inventory at every finite holding cost. This contrasts with the cutoff of Anand et al. This mission formalizes that proposition, together with the equilibrium characterizations of Appendix A on which it rests.
There is one supplier and one buyer, two periods, deterministic demand and complete information. In each period the market price is , where is the total quantity sold in that period and is the demand intercept. The buyer pays a per-unit holding cost on inventory carried into period 2. The supplier pays a per-unit direct selling cost . All other costs and the salvage value are zero. The moves are:
The total profits are
A strategy profile assigns an action to every history at which a player moves. It is a subgame perfect equilibrium (SPE) if, at every feasible history, the mover's prescribed action is feasible and no feasible alternative, followed by the profile afterwards, raises the mover's total profit. The equilibrium path is the outcome the profile generates; the equilibrium inventory is on that path. Following the paper (§4), the goal theorem sets .
With ,
Here may depend on , and the bound applies at the same .
The thresholds , , , , are explicit algebraic functions of , given in Appendix A.
Proposition 4.2 separates the combined model from the two models it merges. Without a direct channel, inventory disappears once . With a direct channel, a threat of encroachment that is only barely credible keeps inventory alive at every holding cost. The total holding cost nevertheless stays below a constant, because the inventory shrinks as grows. Milestone 6 shows the flip side: for a fixed , a large enough removes the inventory. This is why the window must depend on .
The paper's proofs are in an online appendix that is not reproduced in the article. The article itself gives the equilibrium only as tables. A formal development would supply a checked backward-induction proof of those tables in the regions near . It would also give a machine-checked SPE framework for multi-stage pricing-and-quantity games in supply chains, which none of the following exists for: Stackelberg pricing, sequential quantity competition, or dual-channel encroachment. No part of this paper has been formalized before.
The equilibrium is found by backward induction through five stages. Each stage's value function is only piecewise smooth, because the supplier's direct-channel response switches on and off. As a result the buyer's period-2 profit has kinks, the supplier's period-2 profit as a function of has several local maxima, and the period-1 problems must compare branches whose boundaries are the irrational thresholds of Appendix A. The obvious approach, solving the first-order conditions stage by stage, fails at the kinks. At some region boundaries it also misses that the supplier is indifferent between two first-period prices, which makes the equilibrium path change discontinuously. Proposition 4.2 then needs uniform control of , and as , where the denominator of tends to .
IsSPE imposes optimality at every feasible history, including off-path ones. All actions are real numbers; wholesale prices and quantities are nonnegative, with and .Game, IsSPE and Thresholds are shared by every statement. Welcome contributions include:
Competitive-equilibrium theory for economies of divisible commodities — where consumption and production are real vectors — has rested on a rigorous mathematical foundation since around 1960, built from convexity, compactness, and fixed-point theorems (Debreu 1959; Arrow–Hahn 1971; McKenzie 2002). A large share of real markets, however, trade goods that cannot be split: houses, cars, aircraft, job assignments, radio spectrum licenses. For such economies, no comparably general existence theory existed before the framework this mission formalizes. Kelso and Crawford (1982) and Gul and Stacchetti (1999) had identified the gross substitutes property as the right condition on preferences for equilibrium to exist in labor-market and assignment models; Danilov, Koshevoy, and Murota (1998, 2001) showed that gross substitutes, and several other conditions proposed independently in the economics literature, all coincide with a single combinatorial notion from discrete convex analysis: M-natural-concavity. This mission formalizes the resulting existence theorem for economies with indivisible goods, together with the definitional results that pin down exactly what M-natural-concavity of a utility function means and how it connects to the classical demand-set language of general equilibrium theory.
Fix a finite set of indivisible commodity types and a finite set of consumers ("she"). A consumption bundle is an integer vector , one coordinate per commodity. Consumer 's preferences over bundles, net of a perfectly divisible numeraire ("money"), are summarized by a utility function , where marks bundles outside her feasible range (her effective domain, ). Given a price vector (one real price per commodity), consumer chooses a bundle from her demand set
the bundles that maximize utility net of expenditure; the shorthand is used throughout. For the notion this mission is built around, write for the -th unit vector, and for let and . A function with nonempty effective domain is M-natural-concave if it satisfies the exchange axiom: for and ,
with the convention that a maximum over the empty set is . A producer from a finite set is symmetric, described by a cost function that is M-natural-convex — the mirror-image exchange axiom with in place of and the inequality reversed — and a supply set . An equilibrium for a total initial endowment is a tuple with , , market clearing , and .
This is the weakest form of the existence claim the mission proves in full — no producers, so no interaction between two different M-natural-convexity classes is needed — and is the natural target because it isolates exactly what M-natural-concavity buys on the consumer side alone. Two companion results sharpen the picture: Theorem 11.4 pins down M-natural-concavity through an equivalent single-step ascent property, and Theorem 11.7 restates it through the combinatorial structure (M-natural-convexity) of the demand sets themselves, connecting the definition to the gross-substitutes literature. Proposition 11.12 supplies the structural fact the existence proof turns on (the aggregate excess-cost function inherits M-natural-convexity and has a nonempty subdifferential), Theorem 11.14 extends existence to the general economy with producers by transporting an equilibrium down from a continuous relaxation, and Theorem 11.16 establishes that the set of all equilibrium prices is not merely nonempty but a lattice-structured polyhedron.
The result itself. Theorem 11.13 is a genuine existence theorem for a discrete general- equilibrium model — not an approximation or a relaxation of the continuous theory, but a free-standing result about the integer lattice. Its consequence set is also constructive by consequence: Theorem 11.16's lattice structure and section 11.5's reduction to submodular-flow computation (not part of this mission) together show that finding an extreme equilibrium price is a polynomial-time problem, not merely a nonempty-existence claim. Before this line of work, economists working with indivisible goods either restricted to special two-sided matching structures or worked with sufficient conditions (such as gross substitutes) whose relationship to each other and to any unifying combinatorial property was not understood; Fujishige–Yang (2003) and Murota–Tamura independently identified the M-natural-concavity connection cited here.
Formalizing it. All of the results in this mission are proved in the source text; nothing here is open. What formalization adds is a machine-checked confirmation that the demand/supply-set and equilibrium definitions, and the exchange-axiom characterization of M-natural-concavity, compose exactly as the informal statements claim — a nontrivial check, since the definitions involve several layers of arg-max/arg-min over integer lattices and price-shifted objectives that are easy to state slightly wrong (e.g. conflating and , or omitting the extended index in the single-improvement axiom).
The obvious approach to existence — relax the discrete problem to , apply a classical fixed-point argument, and round the resulting continuous equilibrium to the nearest integer point — fails outright, and the book devotes section 11.2 to a two-agent, two-good example that demonstrates this concretely: at certain initial endowments, every candidate integer allocation leaves an unclaimed unit of surplus, so no equilibrium price exists at all, even though the continuous relaxation of the same economy has one. The gap is a failure of convexity in the Minkowski sum : ordinary discrete demand sets can be "hole-free" individually and still sum to a set with a hole. M-natural-concavity is precisely the condition under which Minkowski sums of demand sets stay hole-free (a consequence of the parallel discrete-convex-set theory this book develops earlier), which is what makes the round-down argument valid after all — but only under this specific hypothesis, not under plain concavity or submodularity.
Commodities and prices live on a general finite type (Fintype, DecidableEq), not a fixed
; consumers and producers are indexed by general finite types , , with the
pure exchange economy realized as the special case . Utility values lie in
WithBot ℝ () and cost values in WithTop ℝ (), matching the book's asymmetric conventions for the two families exactly; no
constant appears anywhere in this mission's statements (all hypotheses and conclusions are
qualitative), so there is no explicit-constant obligation to record. The one hypothesis that must
never be silently dropped is "nondecreasing" in Theorem 11.13: it is a real, separate condition
from M-natural-concavity (more of a good is always weakly preferred), stated as its own conjunct
rather than folded into the concavity predicate. A formalization that replaced M-natural-concavity
with ordinary real-valued concavity, or dropped the boundedness hypothesis on the domains, would
be a different — and for indivisible goods, false — statement; section 11.2's example is a
concrete witness that discreteness together with a weaker structural hypothesis than
M-natural-concavity is not enough. This mission's "M-natural-convex set" (used in Theorem 11.7)
and "L-natural-convex polyhedron" (used in Theorem 11.16) are each formalized via one of the
book's own stated equivalent characterizations (projection of an M-convex set on an extended
ground set, and the (SBS-natural[R]) lattice-translation property respectively) rather than
reintroduced as new primitives. Reusable beyond this mission: the general subdifferential
SubdiffR and the EReal-valued concave/convex closure constructions apply to any discrete
convex/concave function, not only to the aggregate cost function of this chapter. Contributions
welcome on the sorry'd proofs, and on formalizing section 11.5's computational reduction to the
M-convex submodular flow problem (deferred here — see HARD.md — pending chunk 12's flow
vocabulary).
Minimizing the total weighted completion time of jobs with release dates on a single machine, written in scheduling notation, is strongly NP-hard. Most constant-factor approximation algorithms for it, and for many related scheduling problems, follow one pattern: solve a linear programming relaxation, which gives a lower bound on the optimum, and round its solution into a schedule whose cost is compared with that bound. The quality of the algorithm is therefore limited by the quality of the relaxation, and the question of which relaxations are equivalent is a basic one for the method.
Two relaxations of are central. The time-indexed relaxation of Dyer and Wolsey (doi:10.1016/0166-218X(90)90104-K) has one variable per job and unit time slot, a pseudopolynomial number of variables. The mean busy time relaxation has one variable per job but one constraint per subset of jobs, the shifted parallel inequalities studied by Queyranne and others. Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X, Section 2) show that both have the same optimal value, and that both are solved by one simple preemptive schedule. This mission formalizes that result, Corollary 2.6, together with the lemmas and theorems its proof uses.
Timeline:
There are jobs . Job has an integral processing time , an integral release date and a weight . For a nonempty set of jobs, and .
A preemptive schedule gives each job a bounded measurable set of processing times of Lebesgue measure , the sets pairwise disjoint. The mean busy time of is .
The LP schedule processes, at every moment, the available (released, unfinished) job of largest ratio , ties broken by index. With the jobs indexed so that , this is the available job of smallest index. As the data are integral, it runs one job or none in each unit slot ; records whether it runs there, and is its mean busy time of .
The preemptive time-indexed relaxation (D) with horizon has real variables for and reads
The mean busy time relaxation (R) reads
The horizon is required to bound the makespan of some feasible nonpreemptive schedule, for instance .
For every instance, every weight vector and every admissible horizon ,
No ordering of the jobs and no reference to the LP schedule appear in the goal.
The equality lets one choose, for each purpose, the more convenient of the two relaxations. (D) is intuitive and a transportation problem, but has pseudopolynomially many variables; (R) has variables and a supermodular right-hand side, which the paper uses to describe its polyhedron. Theorems 2.2 and 2.5 show that the common optimum is attained by the LP schedule, which is computable greedily; the approximation guarantees of Section 3 of the paper, and of later work on -point scheduling, are all measured against this value.
A formal development adds three things. First, a machine-checked model of preemptive single-machine schedules with release dates, of mean busy times, and of the LP schedule as a concrete recursive object, reusable by any formalization of -point methods (two companion missions of this series use the same objects). Second, a formal statement of the two relaxations with honest optimal values. Third, verified proofs of results that are proved in the paper by short interchange and averaging arguments, whose measure-theoretic details (integrals over processing sets, null sets in the equality case) the paper leaves implicit. The results are proved in the literature; to our knowledge none of them has been machine-checked.
The paper's arguments are short, and each rests on a step that is informal on the page. Lemma 2.1 cites the integrality of transportation problems, a statement about the vertices of a polytope rather than a one-line fact. Theorem 2.2 ends with the claim that a 0/1 solution admitting no improving exchange "must correspond to the LP schedule", which is a property of the greedy rule that has to be derived from its definition. Theorem 2.5 depends on how the LP schedule arranges the jobs of each prefix of the sorted order in time; this is the only place sortedness enters, and it is again a property of the concrete schedule. Lemma 2.4 is an extremal statement about integrals over sets of prescribed measure, and its equality case holds only up to null sets. Finally, the goal concerns arbitrary, unsorted weights, while the two theorems it combines are about sorted indices, so the goal is not a direct conjunction of the milestones.
Jobs are Fin n, numbered from ; , and the horizon are natural numbers and weights are real. A preemptive schedule is a family of processing sets , not indicator functions. The LP schedule is defined by recursion on unit slots with the smallest-index rule; the sortedness of is a hypothesis of Theorems 2.2 and 2.5, not part of the definition. Variables of (D) are functions required to vanish outside . and are infima of the objective over the feasible sets; under the stated hypotheses the feasible sets are nonempty and the objectives bounded below, so these are the LP values. Optimality in the milestones is stated as attaining the minimum, not through these infima.
The horizon hypothesis rules out the trivializing case in which (D) is infeasible and its infimum takes the junk value ; (D) is kept a linear program over real , since restricting to would make Lemma 2.1 vacuous. The running-time claim of Corollary 2.6 () is not formalized.
A complete development needs: integrals of the identity over finite unions of intervals; a rearrangement lemma for sets of given measure; basic properties of the LP schedule (it is a preemptive schedule, it is work-conserving and finishes by any admissible , its blocks are canonical); and a relabelling argument. The schedule model and the LP-schedule lemmas are reusable for the companion missions on -point scheduling. Contributions of any of these lemmas as separate theorems are welcome.
Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.
For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its
boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm
searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its
extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a
convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is
certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige
(IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining
a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting
path and no "active triple" together certify near-optimality.
If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then
z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small
enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book
calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max
relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's
placed results, and Proposition 10.23 is a direct corollary of it.
Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds-
intersection-theorem consequence, found by direct reading — the extractor's table missed it).
Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear
orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use
as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish
that the domain reduction algorithm's central part B° is always nonempty, via an explicit
vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition
10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the
termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.
Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.
None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).
Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are
excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation
count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction
algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully
stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for
that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the
input function, threading a step/evaluation counter, instantiated over an unbounded family of
ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind
of formalization task (computational complexity theory) from every one of the roughly 280 other
numbered results in this book, none of which require modeling the cost of computing them. See
HARD.md.
Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is
redeclared from prior missions. Linear orderings of V are represented as bijections
V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for
order-indexed families over sequential data structures. Proposition 10.5's witness vector is
stated as an existence claim (the mathematical content of the proposition), rather than by
reconstructing the specific recursive modification procedure the book uses to produce it — a
choice consistent with how this series has always formalized "the algorithm produces X"
claims where X is a mathematical property, by asserting X's existence rather than executing the
algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered
results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md.
Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9
carry the most independent proof content.
Chapters 6 through 9 characterized minimality for M-convex functions structurally (the M-optimality criterion, Theorem 6.26: a point is a global minimizer iff no local swap improves it) without saying how to find one. Chapter 10 turns that structural fact into an algorithm: the local characterization is the termination test of the simplest possible minimization procedure, steepest descent by coordinate swaps. This mission formalizes that algorithm and its two complexity bounds, plus a structural min-max identity for submodular base polyhedra that the chapter's heavier submodular-minimization algorithms build on. It is the first mission in this series whose goal names a method, not just a property of a class of functions — formalizing it faithfully means giving the algorithm itself a Lean representation that the complexity theorem then quantifies over, not just describing its output.
Let be an M-convex function (MExchangeAxiom,
chunk 06), . The steepest descent algorithm repeatedly replaces the current point
by for a pair minimizing , stopping
when no such swap improves on — at which point, by the M-optimality criterion, is a
global minimizer. This mission represents a run of the algorithm as a sequence satisfying these step and termination relations directly, so that "the number
of iterations" is a genuine property of any such run, not an informal gloss. Separately, for a
submodular set function (chunk 04's SubmodularSetFunction), the
base polyhedron (chunk 04's BasePolyhedron) is the polytope .
For an M-convex function with finite -diameter (Eq. (10.1)), the number of iterations in the steepest descent algorithm using the tie-breaking rule (10.2) — a fixed lexicographic rule for choosing among tied steepest pairs, based on an arbitrary but fixed ordering of — is bounded by .
Proposition 10.1: an unconditional warm-up — if has a unique minimizer , any run of the plain (untied) algorithm from terminates within iterations, with no tie-breaking rule needed. Proposition 10.8: a structural min-max identity, , for a submodular set function — chosen deliberately as a milestone that names no algorithm at all, in contrast to this mission's other two items.
The result itself. Proposition 10.2 is the complexity backbone of §10.1: it is what turns "steepest descent terminates" (an easy monotonicity observation) into a genuine polynomial bound, and it is the base case the chapter's more elaborate scaling and domain-reduction algorithms (not drafted here) improve on. Proposition 10.8, though algorithm-free, is the structural fact ("verifying membership in seems to need a submodular minimization procedure — but demonstrating optimality of a cut only needs a base with ") that makes Schrijver's and the IFF algorithms' correctness proofs possible, and specializes chunk 04's Edmonds's intersection theorem to the two-function case .
Formalizing it. A prior-art search (q=steepest descent, q=submodular minimization,
q=base polyhedron) found no existing platform items for any of this chapter's results. This
mission gives the first formal statement of an M-convex minimization algorithm's complexity,
and directly reuses chunk 06's MExchangeAxiom/ArgMin/CharVec/DomZ and chunk 04's
SubmodularSetFunction/BasePolyhedron — genuine cross-chunk substrate reuse spanning two
different chapters' worth of prior missions.
The chapter's own framing (quoted in BRIEF.md) is that every other chapter's theorems state a
property of a class of functions or sets, while this chapter's theorems state properties of a
named algorithm run on such an object. Formalizing "the number of iterations in the steepest
descent algorithm is bounded by ..." faithfully means giving the algorithm's steps (S0-S3) and
termination test a Lean representation that the bound then quantifies over — stating the bound
about "the minimizer" alone, with the algorithm silently dropped, would misrepresent the
theorem as a fact about minimizers rather than about a procedure that finds one. This mission
represents a run of the algorithm as an abstract sequence satisfying the book's own
step-transition relations (documented in full in MODERATION_NOTES.md), letting the complexity
theorems quantify over any valid run rather than committing to one executable implementation.
A second difficulty is scope: the chapter's recommended primary goal, Proposition 10.18
(Schrijver's algorithm's complexity), needs a scaling procedure with several auxiliary data
structures — a materially larger definitional undertaking than steepest descent's simple
greedy-swap loop. Per BRIEF.md's own explicit fallback authorization, this mission takes
Proposition 10.2 as its goal instead; see HARD.md and MODERATION_NOTES.md for the full
reasoning.
Runs of the algorithm are represented as x : ℕ → V → ℤ satisfying IsSteepestDescentRun
(plain) or IsSteepestDescentRunTieBreak (with the tie-breaking rule) — a step relation plus a
termination test, with an explicit iteration count N the theorems bound. The tie-breaking key
(Eq. (10.2)) and its lexicographic order are formalized directly (a manual
three-way comparison, not Mathlib's default componentwise Prod order). Both iteration bounds
are stated as 2 * N ≤ k rather than N ≤ k / 2, avoiding natural-number division. Not
drafted: the derived "hence ... in time" corollary of Proposition 10.2
(needs a cost-model primitive for "time" and "" this mission does not otherwise use — the
iteration-count bound itself, this proposition's genuine combinatorial content, is drafted in
full); Schrijver's algorithm and everything in §10.2.2 onward; the steepest descent scaling
algorithm, the domain reduction algorithm and its scaling variant (§10.1.2-10.1.3, structurally
different algorithms); the quasi-M-convex extension mentioned immediately after Proposition
10.2. A trivializing formalization would state the iteration bound as an unconditional fact
about "a" minimizer-finding procedure, or would drop the tie-breaking rule from Proposition
10.2 and thereby understate what the bound actually requires; neither is done.
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 one complex variable the Riemann mapping theorem classifies a whole class of domains by topology alone: every nonempty simply connected proper subdomain of is biholomorphic to the unit disc. Nothing of the kind holds in several variables. The two most obvious generalizations of the disc to , the unit ball and the unit polydisc, are homeomorphic, yet no biholomorphic map carries one onto the other. This is the first result a student of several complex variables meets that has no one-variable shadow, and it is the standard illustration that the geometry of the boundary, not the topology of the domain, governs holomorphic equivalence.
As recounted in the source, Poincaré (1907) observed the inequivalence by computing the automorphism groups of and , assuming the maps extend past the boundary; H. Cartan gave the first complete proof in 1931; and Rothstein (1935) proved that there is not even a proper holomorphic map from the bidisc to the ball. This mission follows the presentation in §1.4–1.6 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026), where the inequivalence is derived from a general theorem on proper maps out of product domains, followed by Cartan's uniqueness theorem and the basic structure theory of zero sets and injective maps.
Write for -tuples of complex numbers, for the unit disc, and for the Euclidean norm. The unit ball and unit polydisc are
and the unit sphere is . A domain is a nonempty connected open set. A map between open subsets of complex spaces is holomorphic if it is complex differentiable at every point.
A continuous map is proper if is compact for every compact . A biholomorphic map is a holomorphic bijection whose inverse is holomorphic; every biholomorphism is proper. An analytic disc is a nonconstant holomorphic map , and a set contains no analytic discs if no analytic disc has . A circular domain is a domain with whenever and .
The goal is chosen as the textbook's headline result of §1.4. Theorem 1.4.8 is strictly more general; it is a milestone, so a solver may prove the goal as its special case.
Rothstein's theorem implies the biholomorphic inequivalence of and , the basic example that the Riemann mapping theorem has no analogue in several variables. Theorem 1.4.8 isolates the reason: a boundary that contains analytic discs cannot be mapped properly into a boundary that contains none. Cartan's uniqueness theorem and its corollary are the standard tools for computing automorphism groups of the ball and the polydisc. The Riemann extension theorem, the local graph structure of zero sets and the Jacobian criterion for injective maps are used throughout the theory of analytic varieties and of holomorphic mappings.
All of these results are classical and proved in the source. None of them is formalized in Mathlib or on the platform for with : Mathlib has one-variable Riemann removable singularities and the maximum modulus principle, and the platform has one-variable results on injective holomorphic maps. This mission produces machine-checked statements of the several-variable versions, and infrastructure (proper maps between subsets, analytic discs, holomorphic families) that later chapters of the series reuse.
The goal cannot be reached through topology: and are homeomorphic, so any argument must use holomorphy essentially and must see the boundary. The step that needs genuine analysis is passing from properness, a statement about compact sets, to a statement about boundary values of holomorphic functions of one variable along slices of the product domain; this requires normal families (Montel's theorem) in several variables, which Mathlib does not provide in the needed form. Cartan's theorem rests on power-series expansions in homogeneous parts and vector-valued Cauchy estimates on polydiscs. Theorem 1.6.2 needs the holomorphic implicit function theorem and Rouché's theorem, and Theorem 1.6.6 an induction on dimension that runs through Theorem 1.6.2. The Riemann extension theorem needs holomorphy of parameter-dependent Cauchy integrals.
is Fin n → ℂ. Mathlib's norm on this type is the sup norm, so Metric.ball 0 1 is the polydisc, not the ball. The ball and the sphere are therefore defined with the explicit Euclidean condition, unitBall n = {z | ∑ k, ‖z k‖ ^ 2 < 1} and unitSphere n = {z | ∑ k, ‖z k‖ ^ 2 = 1}. The polydisc is written coordinatewise as unitPolydisc n. Reading the ball as the sup-norm ball would trivialize the goal (the identity of the bidisc is a proper holomorphic self-map); the definitions exclude that reading. Boundedness is Bornology.IsBounded, and boundaries are Mathlib's frontier; neither depends on the norm. A domain is IsOpen U ∧ IsConnected U, so it is nonempty.
Holomorphic means DifferentiableOn ℂ on an open set. On open sets this is equivalent to the book's Definition 1.1.2 (Proposition 1.1.3 and Theorem 1.2.1). Maps into are Fin m → ℂ-valued. is fderiv ℂ f a, and the Jacobian determinant is LinearMap.det of it. Maps are ambient functions whose values off the relevant set are irrelevant. Consequently:
IsProperMapOn f U V: f maps U into V, is continuous on U, and U ∩ f ⁻¹' K is compact for every compact K ⊆ V. This is Definition 1.4.3 for the restricted map. It is not IsProperMap of the ambient map.g holomorphic on with Set.InvOn g f U V.Lemma 1.4.7 works in Fin n → ℝ and reads "limit point of the sequence " as a cluster point of the sequence (MapClusterPt). Theorem 1.4.8 uses the product type (Fin n → ℂ) × (Fin k → ℂ) for . In Theorem 1.6.2, "after reordering the variables" means choosing the index j of the solved-for coordinate. The remaining coordinates are indexed by {i // i ≠ j}. Only the open-disc part of Definition 1.4.5 (analytic discs) is formalized, because closed analytic discs are not used here.
A complete development needs Montel's theorem for maps into bounded subsets of , homogeneous expansions and Cauchy estimates on polydiscs, the holomorphic implicit function theorem, Rouché's theorem, and holomorphic parameter-dependent Cauchy integrals. All of it is reusable beyond this mission, and contributions of it are welcome.
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.Chapter 8 is where discrete convex analysis explains why it needed two separate notions —
M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is
conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly
dual to each other, the discrete analogue of the fact that convex analysis's transform is
self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the
integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral
version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a
real-variable M-/L-convex-function layer the series had not yet built. That layer now exists,
built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This
mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its
nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex
functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the
Edmonds intersection theorem's own combinatorics is built from.
Fix a finite ground set . For , the Legendre-Fenchel transform is . A polyhedral convex function is M-convex () if it satisfies (M-EXC[R]); is L-convex () if it satisfies (SBF[R]) and (TRF[R]). A concave function is always represented via , an ordinary convex function, so every "" hypothesis is restated as "" — an equivalent formulation avoiding any need to represent in the codomain. A polyhedral cone's polar is . A function is M2-convex if it is the sum of two M-convex functions.
The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one
correspondence under the Legendre-Fenchel transform: ,
, and the transform is an involution (,
) on each class, with the identical statement for the M/L
variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing
infrastructure this series has since built.
Twelve further results build the surrounding theory. Proposition 8.2 gives the easy
two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a
milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference
lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone
polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to
general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the
separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the
functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality
equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31
(plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of
M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex,
and their global optimality reduces to a finite local check.
The goal is the theorem that retroactively explains this entire series' two-track structure:
missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are
not two independent theories that happen to share techniques — they are conjugate images of each
other, so every theorem proved on one side has a dual counterpart automatically available on the
other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the
diagram the book draws connecting , , and submodular
set functions (already correspondences this series proved independently, in
missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of
one single conjugacy fact rather than three separate coincidences. The separation and Fenchel
duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex
optimization course opens with, and the book is explicit that they are not corollaries of the
classical versions plus convex extensibility — they carry genuinely combinatorial content,
specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as
examples the book itself gives.
None of these results are open — they are Murota's account of the duality at the heart of
discrete convex analysis, the reason the theory needed two dual notions rather than one. What
this mission contributes is a faithful, machine-checked formal statement of each, completing a
theorem mission 10-conjugacy-i explicitly left for a future session once the necessary
polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own
automated extractor missed; no comparable formalization exists on the platform (see
Formalization scope).
The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about 's own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.
Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ
valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose
defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this
chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one
documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the
integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result
in this chunk requires — see HARD.md. Concave functions are always represented via
and every inequality restated as , avoiding WithTop ℝ
negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate
(printed = PDF 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every
citation here uses the corrected offset. This mission's base vocabulary is redeclared from
missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets,
23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since
sibling drafts in this series cannot yet reference one another. Contributions completing any of
the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof
content.
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.
The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function , its conjugate is again proper closed convex, and the transform is an involution — . This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.
Let be a finite ground set. For , the Legendre-Fenchel transform is ; is submodular if and supermodular under the reverse inequality. For , the discrete Legendre-Fenchel transform restricts the same supremum formula to : for — a genuinely different object from the real-valued transform, since the supremum is now over integer only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate is the transform applied twice. is integer valued if every finite value it takes is an integer (the classes , of the goal theorem are exactly the M-/L-convex functions with this property).
(1) The classes and are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for and , , , , and . (2) The same correspondence holds between and .
Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M-convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.
The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.
Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.
The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the
real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the
real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing
arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete
arg min need not vary continuously with the perturbation the way a polyhedral one does. The
book's actual strategy instead routes through the convex extension of the discrete function
(chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued
conjugacy theorem to the extension, and then must separately argue that the resulting conjugate,
restricted back to integer points, is again integer-valued and satisfies the discrete exchange
axiom — an argument that needs different treatment depending on whether the original function's
domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer
interval, invoking chunk 06's proximity theorem to control convergence). Skipping this
discreteness argument and treating the real-valued theorem as if it settled the integer case
would silently discard exactly the chapter's own point.
The ground set is a Fintype with DecidableEq. ConvexConjugate (the discrete transform)
has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in
EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal
map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same
type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem
8.1) is a separate object with no shared code, per the explicit warning against conflating the
two transforms; the two never appear in the same item.
A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as
if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance
convention to change which values are compared; neither is done. Theorem 8.4 itself (the
polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh,
otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs
(see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type
duality theorem (8.21) are likewise left for a follow-on mission; contributions building the
polyhedral bridge or the separation theorems, which depend on machinery this mission
establishes, are welcome.
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.
List colouring asks for a proper colouring of a graph in which every vertex takes its colour from its own prescribed list. A graph is -choosable if such a colouring exists for every assignment of lists of size . Choosability is harder to guarantee than colourability: planar triangle-free graphs are 3-colourable (Grötzsch) but not all are 3-choosable (Voigt, 1995), and planar graphs are 4-colourable but not all 4-choosable (Voigt, 1993), while every planar graph is 5-choosable (Thomassen, 1994).
A long line of work asks which forbidden cycle lengths make a planar graph 3-colourable or 3-choosable, motivated by Steinberg's conjecture (every planar graph without cycles of lengths 4 and 5 is 3-colourable), which was disproved by Cohen-Addad, Hebdige, Král', Li and Salgado (arXiv:1604.05108).
Timeline.
All graphs are finite and simple. A list assignment gives each vertex a finite set of colours; an -coloring is a map with for all and on every edge . is -choosable if an -coloring exists whenever for all .
Write for a set of colours. A -correspondence assignment assigns to each edge a partial matching between and . A -coloring is a map such that and are not matched in for any edge . Ordinary colouring is the case where every matches equal colours.
For a closed walk (), is inconsistent on if there are colours with for every and ; otherwise it is consistent on . is consistent if it is consistent on every closed walk. An edge is straight if only matches equal colours, and full if is a perfect matching.
A plane graph is a graph with a fixed drawing in the plane without crossings; its faces are the connected components of the complement of the drawing, and a vertex is incident with a face if it lies in the face's closure. A graph is planar if it has such a drawing.
Theorem 8 implies Theorem 6 (), and Theorem 6 with Lemma 5 implies Theorem 1.
The result. Theorem 1 settles Borodin's question and is still the best known forbidden-interval result for 3-choosability of planar graphs with triangles allowed. Theorem 6 is a strengthening in the correspondence setting, and Theorem 8, a precolouring-extension statement, is the form used for induction. The broader contribution is correspondence colouring itself: it allows reductions that identify vertices, which list colouring does not, and it has since been developed by Bernshteyn, Kostochka, Pron and many others as DP-colouring.
Formalizing it. The results are proved in the paper; none has a machine-checked proof. Mathlib has no planarity, no list colouring and no correspondence colouring. This mission produces the first formal definitions of -choosability and correspondence colouring on the platform, the equivalence between list colouring and consistent correspondence colouring (Lemma 5), and a formal statement of the planar result, together with the paper's reduction lemmas as independent targets.
Lemma 5 and Lemma 7 are finite combinatorics. The main obstacle is Theorem 8. The natural list-colouring argument by reducible configurations fails: reductions for ordinary colouring identify two vertices, which is meaningless when their lists differ. Correspondence colouring removes that obstruction only when the identification does not create parallel edges or short cycles, and the main reduction (Lemma 12) needs consistency on triangles, which is why Theorem 6 carries that hypothesis. On the formal side, the proof uses planar topology: faces, the open disk bounded by a cycle, 2-connectedness of a minimal counterexample, and a discharging argument over faces that relies on Euler's formula. None of this exists in Mathlib.
Conventions committed to in the Lean statements:
SimpleGraph V on a Fintype vertex type; the paper's graphs are finite and simple (p. 3).α : Type and lists L : V → Finset α of cardinality exactly .M u c v d on V × Fin k × V × Fin k that lives on edges, is symmetric, and is a partial matching. The paper's is Fin k.G.Walk v v through getVert. The paper's example of Figure 1(a) (p. 5) was checked against this definition by a sorry-free local proof.ℝ × ℝ: injective vertex positions, no vertex on a non-incident edge, and disjoint segments for edges with no common end. These are the clauses of the platform's OPG401.IsPlanar. By Fáry's theorem this is equivalent to planarity for finite simple graphs, and every plane graph has a straight-line drawing with the same faces. Faces are components of the complement of the drawing, incidence is membership in the closure, and the outer face is the unbounded face. Theorem 8 is stated for every drawing and any face, not only the outer one.Type. The measure counts ordered pairs, which gives the same lexicographic order. A minimal counterexample is minimal among all targets of this kind.Formalizations that would trivialize or change the problem are ruled out:
Infrastructure needed and reusable beyond this mission: planar straight-line drawings and their faces (Euler's formula, the Jordan curve theorem for polygons), 2-connectivity and facial cycles, and a DP-colouring library (renaming, consistency, Lemma 5). Contributions to any of these are welcome. So are proofs of Lemma 5 and Lemma 7, which need no topology.
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.
Linear second-order parabolic equations such as model diffusion with advection, growth or decay, and external sources. The heat equation is the prototype. For coefficients that are only bounded and measurable, classical solutions need not exist, and the natural well-posedness theory is the energy theory of weak solutions. In that theory the solution is a curve in a Sobolev space, and the equation holds in the dual space. This framework, developed by J.-L. Lions and others in the 1950s–60s (Lions–Magenes 1972), underlies the numerical analysis of parabolic problems through finite elements and spectral Galerkin methods. It also underlies the existence theory for nonlinear evolution equations such as the Navier–Stokes equations (Temam 1977).
This mission formalizes Chapter 6 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): the existence, uniqueness and energy estimate for weak solutions of the parabolic initial–boundary value problem, proved by the Galerkin method. It also formalizes the vector-valued calculus on Hilbert triples that the proof rests on, and the Ehrling and Aubin–Lions compactness results of §6.6.
Let be a bounded open set and . is the closure of in the norm . is its dual, with pairing . Every acts on by .
The operator is . Its coefficients satisfy Assumption 6.1: , , and uniform ellipticity for some . The associated form is
A function has weak time derivative if for all , with Bochner integrals in . Given and , is a weak solution of
when three conditions hold. First, and . Second, for every and a.e. . Third, , where the value at is that of the continuous representative in .
The Galerkin approximations use an -orthonormal basis of Dirichlet eigenfunctions and the spaces . The approximation solves the projected equation for , with .
A Hilbert triple consists of two separable Hilbert spaces , and the dual , with dense continuous injective embeddings and for . The model is .
For every and there is a unique weak solution with . There is also a constant such that
Theorem 6.3 is the basic well-posedness theorem for linear parabolic equations with rough coefficients. It gives existence and uniqueness, and continuous dependence on the data through the linear estimate. The same argument gives the Galerkin convergence that justifies spectral and finite-element semi-discretizations. The Hilbert-triple calculus of Theorems 6.41–6.42 is the standard setting for linear and nonlinear evolution equations. The Aubin–Lions lemma is the compactness tool for nonlinear problems, such as the semilinear heat equation of §6.6 and the Navier–Stokes equations of §6.7.
All of these results are classical and proved in the notes, except that Theorem 6.41's proof leans on vector-valued mollification. As far as a search of the platform shows, none of them is formalized there. Mathlib has the Bochner integral, spaces of Banach-valued functions and Gronwall's inequality. It does not have weak derivatives of vector-valued functions, Hilbert triples, or evolution-equation existence theorems. The work here is therefore to formalize known proofs, and in doing so to build reusable infrastructure for time-dependent PDEs.
The main obstacle is that the natural objects are equivalence classes of vector-valued functions, not functions. The initial condition is meaningless for an element of until Theorem 6.41 provides a continuous representative. Its proof needs extension across the endpoints and mollification of -valued functions. Passing to the limit in the Galerkin scheme needs weak compactness in and , identified with a dual Bochner space. Proposition 6.5 is a linear ODE system whose coefficients are only in time, so the Picard–Lindelöf theorem for continuous right-hand sides does not apply directly. The bound on needs the projection to be bounded on as well as on , which is why the basis is taken to be eigenfunctions. Uniqueness needs the energy identity (6.46) and a Gronwall argument in weak form.
EuclideanSpace ℝ (Fin n), with 0-based coordinates. H10 n Ω is the closure of the jets , , in , so its norm is the full norm. Hm1 n Ω is StrongDual ℝ (H10 n Ω). l2Embed is the embedding .MemLp for Lebesgue measure on , and norms are eLpNorm with values in . Constants are finite nonnegative reals. Every constant is quantified before the data it must not depend on: before , in Theorem 6.3, and before the basis, , , in Propositions 6.6–6.7.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.
A differentiable convex function on is determined, up to an additive constant, by its gradient, and a vector field is a gradient of a convex function exactly when it satisfies a monotonicity condition along closed cycles. Convex analysis and optimization need the same statement for nonsmooth and extended-valued functions on infinite-dimensional spaces: the subdifferential replaces the gradient, and the question becomes which multivalued maps from a Banach space to its dual arise as subdifferentials, and how much of the function they determine. The answer underlies the treatment of optimality conditions, variational inequalities and evolution equations governed by subdifferentials, where one works with the operator and needs to recover from it.
Timeline.
Let be a real Banach space with dual , and write for the value of at . A proper convex function on is a function , not identically , with for all and . It is lower semicontinuous (lsc) in the norm topology. Its subdifferential is the multivalued map
A multivalued map is a cyclically monotone operator if
and maximal cyclically monotone if, in addition, its graph is not properly contained in the graph of any other cyclically monotone operator. The conjugate of is on , and . In the Lean development these are ProperConvex, subdiff, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone, conj and halfSqNorm, in the namespace RockafellarMaxMono.Cyclic.
For every multivalued map on a real Banach space ,
and if and are lsc proper convex with , then for a real constant . Both halves are one statement.
The result. Theorem B gives an intrinsic description of subdifferential maps: an operator is the subdifferential of a closed proper convex function if and only if it satisfies the cycle inequality and cannot be enlarged without violating it. The uniqueness clause says that a closed convex function is recovered from its subdifferential up to a constant, the nonsmooth counterpart of recovering a function from its gradient. Milestone 7 is stronger than uniqueness: a one-sided inclusion already forces , and this is what gives maximality.
Formalizing it. The theorem is proved in the paper, and nothing of it is formalized on the platform. Mathlib has convex functions, continuous duals, biduals and weak-* topologies, but not extended-valued subdifferentials on Banach spaces, conjugate duality in the nonreflexive setting, or monotone operator theory. This mission produces formal statements of the paper's steps, the standard max formula for directional derivatives on a Banach space, and the Fenchel conjugate facts the argument uses, each as a separate target.
In a reflexive space the argument is short, because is the inverse of . In a nonreflexive space it is not: maps into , and points of appear. The naive route, transferring the inclusion to the conjugates by inverting the maps, breaks down there, and the 1966 argument failed at a related step, where the dual vectors in an approximation could be unbounded. Relating to without reflexivity is where the difficulty sits; the boundedness of the approximating nets in Proposition 1 is essential and cannot be dropped. The finite continuous case and the max formula (3.7) are needed on an arbitrary Banach space, including the dual , not only on .
is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace); is StrongDual ℝ E with the operator norm, is StrongDual ℝ (StrongDual ℝ E), and is NormedSpace.inclusionInDoubleDual. No reflexivity, inner product or finite dimension is assumed. Explicit readings:
EReal with the requirement ; convexity is the paper's inequality for in EReal arithmetic. Lower semicontinuity is in the norm topology.E → Set (StrongDual ℝ E); means for every .Fin (n + 1) with wrap-around addition, so the last term is . Maximality is graph inclusion among cyclically monotone operators, not among monotone operators.atTop; weak** convergence is pointwise convergence on ; "bounded" is a uniform norm bound.IsGreatest, so it is attained; the directional derivative is the limit along .A formalization that drops lower semicontinuity, allows an extended-real constant, or replaces "maximal cyclically monotone" by "maximal monotone" states a different, and in the first two cases false or trivial, theorem; the statements here keep all three.
The proof reduces Theorem B to milestone 7 through Theorem 1 of Rockafellar (1966) and its Corollary 2, which are not stated in this paper and are not milestones; formal statements of them are welcome as supporting theorems. Contributions of reusable infrastructure are welcome: extended-valued subdifferentials and conjugates on normed spaces, the Fenchel–Moreau identity on , the sum rule with a continuous function, and the max formula for directional derivatives.