Operations Research

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$, the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$. When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$, a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ($\varphi$) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$, $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$, which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$, not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
• R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

Motivation

A two-sided market in which each participant trades with at most one partner on the other side — houses and buyers, workers and firms, producers and consumers under exclusive bilateral contracts — is the setting of L. S. Shapley and M. Shubik's assignment game (Int. J. Game Theory 1 (1971) 111–130). Money is transferable, so the natural solution concept is cooperative: a division of the total gain that no coalition of traders can improve upon. The question the paper answers first is whether such a division exists and how to find it, given that a market with $m$ sellers and $n$ buyers has $2^{m+n}$ coalitions.

The answer, Theorem 2 of the paper, connects the core of the game with the dual of the linear-programming relaxation of the optimal assignment problem. It is the starting point of the literature on two-sided matching markets with transfers: the lattice structure of the core (Theorem 3 of the same paper), the ascending auctions of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the equivalence of core outcomes with competitive equilibrium prices. The same LP pairing reappears in stable matching with transfers and in the VCG analysis of multi-item auctions with unit demand.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers; either may be empty and their sizes need not agree. A matrix $a = (a_{ij})_{i \in M, j\in N}$ of nonnegative reals records the profit $a_{ij} \ge 0$ that the partnership of seller $i$ and buyer $j$ can realise (in the real-estate reading, $a_{ij} = \max(0, h_{ij} - c_i)$ with $h_{ij}$ buyer $j$'s valuation of house $i$ and $c_i$ its owner's reservation value).

A coalition $S \subseteq M \cup N$ is described by its sellers $A = S\cap M$ and buyers $B = S \cap N$. A matching inside $(A, B)$ is a set of seller–buyer pairs from $A \times B$ in which no player appears twice. The characteristic function (2.6) assigns to $S$ its worth

$$v(S) = \max_{P} \sum_{(i,j) \in P} a_{ij},$$

the maximum over matchings $P$ inside $S$. One-sided coalitions and singletons are worth $0$.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb R^M$, $v \in \mathbb R^N$ (the paper uses $v$ both for the characteristic function and for buyers' payoffs; the formal development calls the former worth). The core is the set of payoff vectors with

$$\sum_{i\in M} u_i + \sum_{j \in N} v_j = v(M \cup N) \quad (3.5), \qquad \sum_{i\in S\cap M} u_i + \sum_{j \in S\cap N} v_j \ge v(S)\ \text{ for all } S \quad (3.6).$$

The assignment LP (3.1)–(3.2) maximises $z = \sum_{i,j} a_{ij} x_{ij}$ over $x_{ij} \ge 0$ with $\sum_{i} x_{ij} \le 1$ for each $j$ and $\sum_j x_{ij} \le 1$ for each $i$. Its dual (3.3)–(3.4) minimises $w = \sum_i u_i + \sum_j v_j$ over $u_i \ge 0$, $v_j \ge 0$ with $u_i + v_j \ge a_{ij}$ for all $i, j$. The optimal values are $z_{\max}$ and $w_{\min}$.

Formalization targets

Goal: Theorem 2 (p. 118)

$$\operatorname{core}(a) = \{(u,v) : (u,v) \text{ is an optimal solution of the dual LP (3.3)–(3.4)}\}.$$

The statement holds for every finite $M$, $N$ and every $a \ge 0$, with no constants to fix.

Milestones, in the order the paper's argument uses them

1. Eq. (3.6), p. 118: every dual-feasible $(u, v)$ gives every coalition at least its worth.
2. Sec. 3.1, p. 117 (quoting Dantzig, p. 318): the assignment LP attains its maximum at a $0/1$ point, and $z_{\max} = v(M \cup N)$.
3. Sec. 3.1, p. 118 (quoting Dantzig, p. 129): both LPs have optima and $w_{\min} = z_{\max}$.
4. Eq. (3.5), p. 118: every dual minimiser satisfies $\sum_i u_i + \sum_j v_j = v(M \cup N)$.

Further results on the same definitions

• Sec. 3.2, p. 118: the core is nonempty.
• Sec. 3.2, p. 119: for $(u,v)$ in the core, $v_j = \max\bigl(0, \max_{i}(a_{ij} - u_i)\bigr)$ for every buyer $j$ — at the seller prices $p_i = c_i + u_i$, buyer $j$'s best net gain is exactly $v_j$.

Significance

Theorem 2 replaces the $2^{m+n}$ coalition constraints of the core with the $mn$ constraints of a linear program. Consequences stated in the paper: the core is never empty; its points are exactly the dual optimal solutions, so the core is a polytope computable by linear programming without evaluating the worth of any coalition other than the grand one; and dual variables are prices — a seller's core payoff determines a price at which every buyer's best purchase yields that buyer's core payoff. The lattice and corner results of Sec. 3.3 build on this identification.

The paper's proof is short but leans on two results quoted from Dantzig's Linear Programming and Extensions: the integrality of the rectangular assignment polytope and the LP duality theorem. A formalization makes these dependencies explicit for the inequality-constrained rectangular case with possibly unequal sides. To our knowledge Theorem 2 has no machine-checked proof. On Prove2Me, general LP strong duality is formalized (LinearOptimization.lp_strong_duality, SmaleNinth.lp_strong_duality), and integrality of the square doubly stochastic assignment LP (UnderstandingML.assignment_lp_integral, FamousTheorems.birkhoff_von_neumann); neither is the specialised statement here, but both are natural substrate.

Difficulty

The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth $v(M \cup N)$, which is not a statement about linear programming alone: it needs both LP duality and the integrality of the assignment polytope. The integrality needed is for the polytope cut out by inequalities $\le 1$ on a possibly non-square matrix, which is not the Birkhoff polytope of doubly stochastic matrices already on the platform; the gap between the two must be bridged.

The converse, "core ⊆ dual optimal", is dismissed as "clearly" in the paper, but the core is defined through the worth of every coalition, a maximum over exponentially many matchings, while dual optimality is a comparison with every dual-feasible vector. Neither side mentions the other's objects, and the naive reading "the core is the dual feasible set" is false: large payoffs are dual feasible and violate (3.5).

Formalization scope

Lean represents sellers and buyers as types M, N with [Fintype M] [Fintype N]; no nonemptiness is assumed, so markets with an empty side are included (there the core is $\{0\}$). The matrix is a : M → N → ℝ with the standing hypothesis ∀ i j, 0 ≤ a i j on every theorem. A coalition is a pair (A, B) : Finset M × Finset N. A matching is a Finset (M × N) inside A ×ˢ B with no repeated seller and no repeated buyer. The worth is Finset.sup' over the finite, nonempty set of matchings (the empty matching is always present), so there is no junk value. The paper's (2.6) takes exactly $k = \min(|S\cap M|, |S\cap N|)$ pairs; the formal definition takes all partial matchings, which gives the same maximum because $a \ge 0$.

Payoff vectors are pairs (M → ℝ) × (N → ℝ). The core is defined by (3.5) and (3.6) for all coalitions; nonnegativity is not a separate clause since it follows from singleton coalitions. The dual LP keeps the nonnegativity of $u$ and $v$ that (3.3) imposes, and "solutions of the LP dual" is read as optimal solutions (DualOptimal: dual feasible and of minimal objective among dual-feasible vectors), as the text preceding Theorem 2 does.

The worth is the combinatorial maximum, not the LP value, and the core is defined by coalitions, not through the dual; defining either through the other would make Theorem 2 true by unfolding, and such a formalization is ruled out. Likewise the goal is not the weaker "core = dual feasible set", which is false.

Contributions welcome: integrality of the rectangular inequality-form assignment polytope, a specialisation of general LP duality to this pair, and the coalitional inequality (3.6). The first two are reusable for any bipartite matching model.

Selected references

• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9 (1962), 45–48. https://doi.org/10.1002/nav.3800090106
• G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393

Motivation

Every stability result up through mission VII proves that a particular control policy — a fixed priority list, HLSPS, a policy tailored to one network's topology — keeps a specific processing network stable throughout its subcritical region. None of them answer a more practical question a system designer actually faces: given an arbitrary Leontief network (one where every activity has a well-defined, unique buffer it draws from), is there a single control rule, computable from the network's data alone with no bespoke analysis, that is guaranteed stable whenever stability is possible at all? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this in Chapter 9 with the back-pressure (equivalently, in the single-hop case, max-weight) control policy: at every decision time, choose the allocation of service effort that maximizes a bilinear "weighted throughput" objective built directly from current buffer contents. This mission formalizes the policy, the characteristic fluid equation it induces, and the resulting maximal-stability theorem — the chapter's central result and one of the most cited scheduling policies in the queueing-networks literature.

Setting

A Leontief network (Definition 9.5) is an SPN whose input-output matrix $R$ satisfies two assumptions: Assumption 9.1, that each activity has a unique buffer it draws material from (so $i(j)$, the buffer served by activity $j$, is well-defined), and Assumption 9.2, that there is a nonnegative activity-level vector driving every buffer's net output rate strictly positive — the structural condition under which the network can be drained at all. The back-pressure (or, in the single-server, single-hop case, max-weight) control policy chooses, at each decision time, the feasible allocation $\beta$ of service rates that maximizes the bilinear objective $p(\beta, \hat z) = \hat z \cdot R\beta$, where $\hat z$ is the current vector of buffer contents. The "relaxed" version of the policy allows $\beta$ to range continuously over the allocation polytope $\mathcal A = \{\beta \in \mathbb R^J_+ : A\beta \le b\}$; the "basic" version restricts to integer service-initiation decisions in a genuine SPN with discrete jobs. A network's static planning problem's optimal value $\gamma^* < 1$ is the subcriticality condition throughout this chapter, exactly as in missions II, III, and V.

Formalization targets

Goal: Theorem 9.12 — maximal stability of relaxed back-pressure

Consider a Leontief network operating under the relaxed back-pressure control policy. If the static planning problem has optimal objective value $\gamma^* < 1$, then the corresponding fluid limit is stable, and hence, by Theorem 6.2 (mission III), the network's ambient Markov chain is positive recurrent. This is the chapter's payoff: back-pressure control needs no network-specific tuning — it stabilizes every Leontief network throughout its entire subcritical region, the same universal guarantee mission VI showed only for feedforward networks and HLSPS control specifically.

Supporting milestones

Lemma 9.3 and Proposition 9.4 develop the linear-algebraic machinery of basis matrices: any feasible material-balance vector can be re-expressed using only $I$ "basic" activities (Lemma 9.3), and Assumption 9.2 holds if and only if some basis's associated matrix has spectral radius below one (Proposition 9.4) — the practical, checkable criterion for the network being well-posed at all. Proposition 9.6 shows the back-pressure optimization problem always admits a solution among the finitely many extreme allocations, licensing Remark 9.7's standing convention of restricting attention to that finite set. Lemma 9.10 shows a $z$-maximal extreme allocation can always be chosen to idle any activity whose buffer is currently empty — a fact that looks obvious but genuinely needs proof, because at the fluid level an activity can serve an instantaneously empty buffer at a positive rate (Section 9.5's tandem-model illustration). Theorem 9.8 is the chapter's characteristic fluid equation: under relaxed back-pressure control, the realized fluid service-rate derivative always achieves the bilinear maximum over the allocation polytope, at every regular point. Lemma 9.11 derives this from the raw ("pre-limit") stochastic dynamics — a strictly dominated allocation accrues no processing time — via a genuine limit-passage argument. Theorem 9.13 and Lemma 9.14 extend the maximal-stability guarantee from the relaxed policy to the basic (discrete-decision) policy, under the extra restriction that each server pool is a single server acting alone; this needs a residual-time strong law of large numbers (Lemma 9.14) to show that a server's decision to switch away from a dominated allocation happens quickly enough, relative to elapsed time, that the fluid limit is unaffected.

Significance

The result itself. Theorem 9.12 is the book's formalization of the max-weight/back-pressure maximal-stability theorem originally due to Tassiulas and Ephremides (1992) for multi-hop packet radio networks, later popularized under the "back-pressure" name by Tassiulas (1995) and extended substantially by Dai and Lin (2005), on whose work this chapter is explicitly based. Unlike every policy considered in missions IV, VI, and VII, back-pressure requires no topology-specific insight to design or verify — it is defined uniformly from $B$, $\Gamma$, $A$, and current buffer contents, and Theorem 9.12 certifies it stable for every Leontief network in its subcritical region. This universality is precisely what distinguishes it from HLSPS (mission VI), which needs the network to be feedforward or the policy to be head-of-the-line proportional-sampling before the same guarantee holds.

Formalizing it. A live prior-art check (GET /theorems?q=max-weight%20scheduling, q=back-pressure) returns no hits, so this mission formalizes the policy, its characteristic fluid equation, and both stability theorems entirely from scratch. SPNPlanningData, the input-output matrix R, and the static planning problem are restated from mission II's own apparatus; RegularPoint is restated from mission V's Definition 8.7.

Difficulty

The chapter's central subtlety is that "operating under back-pressure control" cannot be stated directly as a hypothesis on the fluid-limit path $(\hat D,\hat F,\hat T,\hat Z)$ itself: the policy is defined in terms of the discrete, pre-limit decision process, and its fluid-level consequence — the characteristic equation (9.22) — is a genuine theorem (9.8), not a restatement of the policy's definition. Formalizing Theorem 9.8 naively by hypothesizing "$\hat T$ satisfies (9.22)" would make Lemma 9.11 (whose conclusion (9.28)-(9.31) is what Theorem 9.8's own proof literally invokes) circular relative to it. This mission instead hypothesizes Lemma 9.11's raw, pre-limit optimality condition (hYopt: a strictly dominated allocation accrues no processing time over any interval where domination persists) as the operational meaning of "following the back-pressure rule," and derives (9.28)-(9.31) from it as Lemma 9.11's genuine conclusion — Fed into Theorem 9.8 exactly as the book's own proof does ("By Lemma 9.11 and the fact that $\sum_\beta \dot{\hat Y}_\beta(t) = 1$..."). A second difficulty is Theorem 9.13's genuinely distinct proof from Theorem 9.12's: the basic (discrete) policy's fluid limit satisfying the same characteristic equation is not automatic, and needs the residual-time SLLN of Lemma 9.14 plus two extra structural hypotheses (each server pool is a single server, each activity uses exactly one server) that go beyond "basic vs. relaxed" and are stated explicitly rather than folded silently into the policy's name.

Formalization scope

SPNPlanningData, its input-output matrix R, and the static planning problem (SPPFeasible, IsOptimalSPPValue) are restated unmodified from mission II's own apparatus (drafts in this series do not import one another); RegularPoint is restated unmodified from mission V's Definition 8.7. "Basis" is named ActivityBasis, not Basis, to avoid colliding with Mathlib's vector-space Basis type — a deliberate departure from the book's own overloaded terminology, which its own text flags as "slightly narrower than [the] standard meaning in linear programming theory." ExtremeAllocations reuses Mathlib's Set.extremePoints directly rather than restating extreme-point theory from scratch, and Proposition 9.4's spectral-radius condition reuses Mathlib's own spectralRadius (Mathlib.Analysis.Normed.Algebra.Spectrum) rather than defining eigenvalues by hand. IsZMaximal (Definition 9.9) is phrased as "feasible and dominates every feasible alternative" rather than via an explicit sSup/⨆ expression, which sidesteps any Mathlib junk-value risk while remaining definitionally equivalent to "achieves the maximum" whenever a maximizer exists — the same convention this series has used since mission III. Theorem 9.8's hypothesis that the fluid limit "operates under relaxed back-pressure control" is packaged as Lemma 9.11's own conclusion (hTY/hYmono/hYsum/hYopt), matching the book's proof architecture exactly rather than re-deriving it inline. Theorem 9.13 states its two extra single-server hypotheses (hb1, hA01) explicitly as the mission's own BRIEF.md warns to. Lemma 9.14's condition (9.44) — quoted in the book's preparatory material for Theorem 9.13 rather than in the excerpt originally assembled for this lemma — was located directly in source.txt (p. 178, PDF p. 194) and confirmed verbatim, not reconstructed; its formalization (h944) matches the confirmed text exactly. The one acknowledged source inconsistency, noted by BRIEF.md itself, is that (9.56)'s printed left-hand side reads u_i(s,ω) where the surrounding proof otherwise uses t throughout — treated as a typesetting slip and formalized with t, as the lemma evidently intends. IsFluidModelSolution, IsRelaxedBPFluidSolution, RelaxedBPFluidStable, ActivityBasis, AllocationPolytope, and IsZMaximal are the primary reusable contributions; contributions completing the nine by sorry proofs, especially Lemma 9.11's limit-passage argument and Lemma 9.14's SLLN chain, are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• L. Tassiulas and A. Ephremides, "Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks," IEEE Transactions on Automatic Control 37 (1992), 1936–1948.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197–218.

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$. The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$) needs.

Timeline.

• Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
• Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$. For $X\subseteq\mathbb R^n$, $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$-subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$, the line $x_2=2x_1$ is a $\Lambda$-subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$.

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$-free convex set of $W$ if $S\subseteq W$, $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$. It is maximal if no other $\Lambda$-free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ($W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$. The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$.

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$, a set $S$ is a maximal $\Lambda$-free convex set of $W$ if and only if

$$\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};$$ $$\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};$$ $$\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}$$

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$, $S$ is a maximal $\Lambda$-free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$-subspace and $\dim S=\dim P+\dim L=\dim V$, with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$-subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ($S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$-free), Lemma 17 (projection along a $\Lambda$-subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$.

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$-subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$.

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$, the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$-subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$, and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$, and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

1. Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$. For $W=V=\{0\}$ the only maximal set is $\emptyset$, which satisfies none of the listed cases, so the printed statements are false there.
2. Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$, discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
• L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

Motivation

Monotone operators from a Banach space $E$ to its dual $E^*$ are the abstract framework for nonlinear equations, variational inequalities and evolution equations, and for the convergence theory of proximal-point and splitting algorithms in infinite dimensions. Within that framework, the class that behaves well — for surjectivity results, for resolvents, for sums — is the class of maximal monotone operators. The most important source of such operators is convex analysis: the subdifferential of a convex function. Whether every subdifferential of a closed proper convex function is maximal monotone, in an arbitrary Banach space, is therefore a basic question for convex optimization in function spaces.

Timeline:

• 1964. G. J. Minty proves maximality of the subdifferential for convex functions that are finite and continuous everywhere (Minty, Pacific J. Math. 14 (1964)).
• 1965. A. Brøndsted and R. T. Rockafellar show that subgradients exist on a dense set and approximate ε-subgradients (Brøndsted–Rockafellar, Proc. AMS 16 (1965)). J.-J. Moreau develops proximal maps and conjugate duality for convex functions in Hilbert space (Moreau, Bull. SMF 93 (1965)); his later lecture notes Fonctionnelles convexes (Collège de France, 1967) are the paper's reference for conjugates in locally convex spaces.
• 1966. R. T. Rockafellar announces the general Banach-space result, for every lower semicontinuous proper convex function (Rockafellar, Pacific J. Math. 17 (1966)). H. Brézis later points out a gap in that proof: a subgradient chosen in the argument may grow without bound.
• 1970. Rockafellar gives a complete proof by a different route, valid in nonreflexive spaces, in the paper formalized here (Rockafellar, Pacific J. Math. 33 (1970)).

Setting

Let $E$ be a real Banach space with dual $E^*$ and bidual $E^{**}$, and write $\langle x, x^*\rangle = x^*(x)$. $E$ sits in $E^{**}$ through the canonical embedding.

A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$, not identically $+\infty$, such that $f((1-\lambda)x + \lambda y) \le (1-\lambda) f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$. It is lower semicontinuous for the norm topology.

The subdifferential of $f$ is the multivalued map $\partial f : E \to E^*$,

$$\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.$$

A multivalued map $T : E \to E^*$ is monotone if $\langle x_0 - x_1, x_0^* - x_1^* \rangle \ge 0$ whenever $x_0^* \in T(x_0)$ and $x_1^* \in T(x_1)$. It is maximal monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other monotone map $T' : E \to E^*$.

The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} \{\langle x, x^*\rangle - f(x)\}$, a function on $E^*$; its subdifferential $\partial f^*$ maps $E^*$ into $E^{**}$. Finally $j(x) = \tfrac12 \|x\|^2$.

In Lean these are ProperConvex f, subdiff f, IsMonotoneOp T, IsMaximalMonotone T, conj f and halfSqNorm, all stated over an arbitrary real normed space V so that they apply equally to $E$ and to $E^*$.

Formalization targets

Goal: Theorem A (p. 210)

$$f \text{ lower semicontinuous proper convex on } E \quad\Longrightarrow\quad \partial f : E \to E^* \text{ is maximal monotone.}$$

No reflexivity, inner product or finite dimension is assumed.

Milestones, in attack order

1. (2.2) Fenchel–Young: $f(x) + f^*(x^*) \ge \langle x, x^* \rangle$, with equality iff $x^* \in \partial f(x)$.
2. §2, p. 210. $f^*$ is a weak* lower semicontinuous (hence strongly lower semicontinuous) proper convex function on $E^*$.
3. §2, p. 211. The restriction of $f^{**}$ to $E$ is $f$.
4. Proposition 1. $x^{**} \in \partial f^*(x^*)$ iff there are a net $x_i^* \to x^*$ in norm and a bounded net $x_i \to x^{**}$ weak**, on one directed index set, with $x_i^* \in \partial f(x_i)$.
5. (3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for all $x \in E$.
6. §3, p. 213. $(f + j)^*$ is finite and continuous throughout $E^*$.
7. §3, p. 213 (Minty). On any real Banach space, a convex function that is finite and continuous everywhere has a maximal monotone subdifferential.

Significance

Theorem A places every closed proper convex function in the maximal monotone class, in every real Banach space. Downstream, it is what allows convex minimization problems to be treated by the general theory: surjectivity of $\partial f + \lambda J$ (with $J$ the duality map) in reflexive spaces, existence for evolution equations governed by subdifferentials, the definition of resolvents and proximal maps, and the convergence of proximal-point and splitting methods for convex problems. Proposition 1 is of independent interest: in a nonreflexive space $\partial f^*$ is not the inverse of $\partial f$, but it is still completely determined by $\partial f$ through bounded weak** nets.

The theorem is classical and fully proved in the literature. What this mission adds is a machine-checked proof of the nonreflexive Banach-space statement, together with the infrastructure it needs: extended-real-valued proper convex functions, the subdifferential and the conjugate on a normed space and its dual, monotone and maximal monotone operators, and the Fenchel–Moreau identity $f^{**}|_E = f$. None of these exists in Mathlib at the pinned revision, and Mathlib contains no statement of Theorem A, in Hilbert or in Banach spaces.

Difficulty

Monotonicity of $\partial f$ follows in two lines from the definition; the whole difficulty is maximality. In a Hilbert space the standard argument solves $x + \partial f(x) \ni y$ by minimizing $f + \tfrac12\|\cdot - y\|^2$ and uses the identification of $E$ with $E^*$; in a general Banach space there is no such identification, and minimizers need not exist without reflexivity. The 1966 argument tried to approximate subgradients of $f$ at nearby points, and it failed because those subgradients could become unbounded as the approximation was refined. Any argument that passes through the dual meets a second obstacle: $\partial f^*$ takes values in the bidual $E^{**}$, which is strictly larger than $E$ when $E$ is not reflexive, so $\partial f^*$ is not the inverse of $\partial f$. Relating the two is the content of Proposition 1, and its necessity half requires approximation results well beyond the definitions.

Formalization scope

Lean representation and committed conventions:

• $E$ is a real Banach space: NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E. $E^*$ is StrongDual ℝ E with the operator norm; the pairing $\langle x, x^*\rangle$ is x' x; $E^{**}$ is StrongDual ℝ (StrongDual ℝ E) and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual ℝ E.
• The value set $(-\infty,+\infty]$ is EReal with the clause "never $\bot$". Properness also requires some value $\ne \top$. Convexity is the paper's inequality for $0 < \lambda < 1$, computed in EReal.
• Multivalued maps are V → Set (StrongDual ℝ V). Maximality is graph inclusion, quantified over every monotone T', not only over subdifferentials.
• The conjugate is an EReal supremum over all of $V$; the biconjugate is conj (conj f) on the bidual.
• (2.2) is stated as $\langle x, x^*\rangle \le f(x) + f^*(x^*)$ with the equality case, avoiding EReal subtraction.
• Weak* lower semicontinuity of $f^*$ is lower semicontinuity on WeakDual ℝ E.
• In Proposition 1 a net is a map from a nonempty, directed, partially ordered index type (in the universe of $E$), with convergence along atTop. Weak** convergence is pointwise convergence on $E^*$ of the canonical images, which is convergence in the weak topology induced on $E^{**}$ by $E^*$. Boundedness is a uniform norm bound.
• (3.1) reads the printed $\partial(f+j)$ as $\partial(f+j)(x)$; the right side is the pointwise (Minkowski) set sum.
• "Finite and continuous" for $(f+j)^*$ is the existence of a continuous real-valued $h$ on $E^*$ equal to it everywhere.
• Minty's case is stated for an arbitrary real Banach space $V$, because the proof applies it on $E^*$.

A trivializing formalization is ruled out: properness excludes $f \equiv +\infty$ (whose empty subdifferential is monotone but not maximal) and $-\infty$ values, maximality ranges over all monotone operators, and the index set in Proposition 1 is nonempty and directed so that no convergence statement holds vacuously.

Infrastructure needed and reusable beyond this mission: extended-real convex analysis on normed spaces (conjugates, the Fenchel–Moreau theorem via Hahn–Banach separation, lower semicontinuity in the weak and weak* topologies), subdifferential calculus for a sum with a continuous function, nets and weak** approximation in the bidual (Goldstine-type arguments), and the Brøndsted–Rockafellar approximation of ε-subgradients. Contributions are welcome at every milestone; the definitions layer and milestones 1–3 are the natural starting points.

Selected references

• R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific Journal of Mathematics 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific Journal of Mathematics 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
• G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific Journal of Mathematics 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
• J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
• A. Brøndsted and R. T. Rockafellar, On the subdifferentiability of convex functions, Proceedings of the American Mathematical Society 16 (1965), 605–611. https://doi.org/10.1090/S0002-9939-1965-0178103-8

Motivation

Mission III's Theorem 6.2 reduces SPN stability to a question about deterministic fluid model solutions: does every solution of a fixed system of equations get driven to the origin, uniformly in its starting size? Mission IV showed how to derive the extra, policy-specific equations a fluid model must satisfy. What remains is a method for proving that a system of fluid equations forces extinction — and the standard tool for that, across dynamical systems generally, is a Lyapunov function: a scalar-valued potential that decreases along every trajectory. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 8 to making this method precise for fluid models, and to explaining exactly why it is easier to apply here than the analogous drift condition for the underlying Markov chain.

The chapter's calculus culminates in a genuinely delicate real-analysis fact: the ordinary "Lyapunov function decreases everywhere it should" argument needs the function to be differentiable, but fluid model solutions are typically only Lipschitz (hence differentiable only almost everywhere), and some Lyapunov functions used later in the book (Chapter 10's entropy function) are not even Lipschitz. The chapter's most general result, Lemma 8.11, resolves this by working with the upper-right Dini derivative rather than the ordinary one, following an approach whose subtlety is illustrated by a counterexample due to L. Massoulié when one of its three hypotheses is dropped.

Setting

Throughout this mission, (D,F,T,Z) (without hats) denotes an arbitrary solution of the fluid equations (6.1)-(6.6), restated from mission III (drafts in this series do not import one another). A function $g$ is Lipschitz if it satisfies a Lipschitz bound on every bounded set, with a constant that may depend on the set; it is globally Lipschitz if one constant works everywhere. A point $t > 0$ is a regular point of a fluid model solution if all four components are differentiable there; because every solution is globally Lipschitz, the non-regular points form a Lebesgue-null set. A Lyapunov function for a fluid model is a Lipschitz function $H : \mathbb{R}^I_+ \to \mathbb{R}_+$ with $H(0)=0$ and $H(z) \ne 0$ for $z \ne 0$ — a positive-definite potential.

Formalization targets

Goal: Lemma 8.11 — the general Dini-derivative extinction criterion

For $f : \mathbb{R}_+ \to \mathbb{R}_+$ continuous on $(0,\infty)$, with a locally bounded upper Dini derivative $D^+f$ and $D^+f(t) \le -\varepsilon$ for a.e. $t$ with $f(t) > 0$:

$$f(t) = 0 \quad \text{for } t \ge f(0)/\varepsilon.$$

This is the weakest natural target: it drops the Lipschitz requirement of Lemma 8.5 entirely, replacing it with only continuity plus a one-sided, locally bounded derivative condition, and Lemmas 8.5 and 8.6 are recovered as the special cases $f = H \circ Z$ for $H$ Lipschitz (respectively linear-type and square-root-type drift bounds).

Supporting milestones

Lemma 8.2 (composition of Lipschitz functions) and Lemma 8.3 (every fluid model solution is globally Lipschitz) supply the regularity Lemma 8.5 needs. Lemma 8.5 (linear drift bound) and Lemma 8.6 (square-root drift bound) are the two directly-applicable extinction criteria the book presents before generalizing to Lemma 8.11. Lemma 8.9 identifies a structural fact used in nearly every application: at a regular point, an empty buffer's fluid arrival and departure rates necessarily coincide. Lemma 8.10 gives the calculus of a pointwise maximum's derivative, needed for piecewise-linear Lyapunov functions. Theorem 8.12 is the chapter's worked illustration: the tandem queueing network's fluid model is stable under the standard load condition, proved with a linear Lyapunov function that (the chapter goes on to show) does not translate into a valid Markov-chain drift bound — the concrete illustration of why the fluid-model method earns its keep.

Significance

The result itself. Lemma 8.11 is the single tool every subsequent stability chapter of the book applies: feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation (whose entropy Lyapunov function is exactly the non-Lipschitz case this lemma was built to handle), and task allocation all conclude fluid model stability via an instance of this criterion. Theorem 8.12's side observation — the same Lyapunov function that works effortlessly for the fluid model fails to give a Markov-chain drift bound at all — is the chapter's explicit argument for why fluid-model methodology is not just a convenience but a genuine technical advance over direct Markov-chain analysis.

Formalizing it. Searches for "Lyapunov function," "Dini derivative," and "Lipschitz continuous" (q=Lyapunov%20function, q=Dini%20derivative) surface no reusable extinction-criterion result; the one Lyapunov-adjacent hit, posDef_quadratic_form_lower_bound, is an unrelated quadratic-form bound. This mission is a from-scratch formalization of the fluid model's Lyapunov calculus, reusing Mathlib's own LipschitzOnWith/LipschitzWith substrate for Definition 8.1 rather than restating ordinary Lipschitz continuity, per this mission's own BRIEF.md recommendation.

Difficulty

The central difficulty is Lemma 8.11 itself: proving that a bound on the upper Dini derivative $D^+f(t)$ (not the ordinary derivative) forces $f$ to decrease is genuinely subtler than the Lipschitz case, because $D^+f$ is one-sided and may not correspond to an actual rate of change at every point. The book's own proof needs a technical intermediate inequality (8.8), $f(b)-f(a) \le \int_a^b D^+f$, and states explicitly that this can fail without the local upper-boundedness hypothesis (b) — citing a counterexample of L. Massoulié — so a formalization that dropped condition (b) as "obviously implied by continuity" would be proving a false generalization, not a faithful specialization. A second difficulty, specific to Lemma 8.5/8.6's formalization, is that the hypothesis "$\dot f(t) \le -\varepsilon$ for almost all $t$ with $Z(t)\ne 0$" implicitly presupposes $\dot f(t)$ exists almost everywhere (a fact Lemma 8.3 supplies, not something to assume outright) — stating the hypothesis as a universally quantified implication over any witnessing derivative avoids smuggling in an unearned existence claim.

Formalization scope

Mission III's fluid-equation apparatus is restated locally (per that mission's own note that later chunks cannot import its draft), unmodified. Definition 8.1's two Lipschitz notions (bounded-set-wise and global) are formalized via Mathlib's own LipschitzOnWith, generalized over arbitrary (pseudo)metric domain and codomain types so the same definition serves $g:\mathbb{R}^d\to\mathbb{R}^m$ and $g:\mathbb{R}^m\to\mathbb{R}$ uniformly — reusing Mathlib substrate rather than restating Definition 8.1's $\varepsilon$-$\delta$ inequality from scratch, per BRIEF.md's explicit recommendation. The upper-right Dini derivative is restated inline (Appendix A.4 is out of series scope) via Filter.limsup along the right-neighborhood filter, and is used throughout Lemma 8.11 in place of the ordinary derivative — using deriv instead would be a strictly stronger, unfaithful hypothesis. Lemma 8.10's pointwise maximum is a supremum over the finite index type Fin d, always a genuine maximum with no junk-value risk. Theorem 8.12 restates the tandem queueing network's already-reduced fluid equations (8.11)-(8.15) directly, since Figure 1.1 belongs to Chapter 1, outside this mission series. A formalization that replaced Lemma 8.11's Dini-derivative hypotheses with ordinary-derivative ones, or that dropped condition (b)'s local bound, would each be an unfaithful strengthening or a false generalization — both ruled out here. The Lyapunov extinction criteria (lyapunov_extinction_linear, lyapunov_extinction_sqrt, dini_extinction_criterion) are the primary reusable contributions, intended for direct reuse (matching shape, since drafts do not import one another) by every later stability mission in the series; contributions completing the eight by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• L. Massoulié, "Structural properties of proportional fairness: stability and insensitivity," Annals of Applied Probability 17 (2007), 809–839.
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.

Motivation

In a periodic-review inventory system a manager observes the stock level before ordering, decides how much to order, and then faces random demand. When ordering costs a fixed setup charge plus a constant price per unit, Scarf (1960) proved that an $(s,S)$ policy is optimal in every period of a finite-horizon problem: order up to $S$ when the stock falls below $s$, otherwise order nothing. Real ordering costs are often not of this form. Quantity discounts, a choice between production facilities with different setup and marginal costs, or a supplier whose price schedule falls with volume all give an ordering cost that is concave and increasing but not "setup plus linear". Karlin had analysed the single-period problem with such costs; Porteus (1971) gave the first multiperiod result with random demand.

Timeline:

• Scarf (1960): $(s,S)$ optimality for setup-plus-linear ordering cost, via $K$-convexity of the expected cost-to-go.
• Veinott (1966): an alternative proof of $(s,S)$ optimality under different conditions (quasi-convex one-period costs).
• Porteus (1971): for concave increasing ordering costs and demand with a one-sided Pólya density, a generalized $(s,S)$ policy is optimal in every period; when the cost is piecewise linear with $r$ pieces it is an $(s,S)_r$ policy with at most $r$ reorder levels.

Setting

The ordering cost $c : [0,\infty) \to \mathbb R$ is concave, nondecreasing, and $c(0) = 0$. For $z > 0$, $C_2(z)$ is the supporting line of $c$ at $z$ with the smallest intercept, written as a pair (slope, intercept) $(\kappa, K)$. The set of slopes that occur is $C$, and $K_\kappa$ is the intercept belonging to slope $\kappa \in C$, so $c(z) = \min_{\kappa \in C}\{K_\kappa + \kappa z\}$ for $z > 0$. The limits $(c_0, K_0) = \lim_{z \downarrow 0} C_2(z)$ and $(c_\infty, K_\infty) = \lim_{z\to\infty} C_2(z)$ are assumed to exist.

Demands in successive periods are i.i.d. with density $\varphi$. A function $\varphi$ is $PF_n$ if $0 < \int\varphi < \infty$ and $\det[\varphi(x_i - t_j)]_{i,j\le k} \ge 0$ for all $k \le n$ and increasing $x_1<\dots<x_k$, $t_1<\dots<t_k$; it is a one-sided Pólya density if it is $PF_n$ for every $n$, integrates to $1$ and vanishes on $(-\infty,0)$. Exponential and Erlang densities are examples.

With holding-and-shortage cost $m$ (PF-integrable, bounded below), terminal cost $f_0$, discount factor $0 \le \alpha \le 1$, and convolution $(f*\varphi)(y) = \int f(y-x)\varphi(x)\,dx$, the value functions are

$$h_n = m * \varphi + \alpha\, f_{n-1} * \varphi, \qquad f_n(x) = \inf_{y \ge x}\{c(y-x) + h_n(y)\},$$

where $n$ counts the periods remaining. $Y_n(x)$ is the set of minimizers $S \ge x$. A generalized $(s,S)$ policy is a function $y$ with $y(x) = x$ for $x \ge s$ and $y(z) \ge y(x) \ge S \ge s$ for $z < x < s$: no order above $s$, and below $s$ an order-up-to level that is at least $S$ and does not increase with the starting stock.

Two function classes carry the argument. $f$ is non-$K$-decreasing on $X$ if $f(x) \le f(y) + K$ for $x \le y$ in $X$. For $K \ge 0$, $C_a(K)$ consists of the piecewise continuous, PF-integrable functions with $f(x)\to\infty$ as $|x|\to\infty$ that are nonincreasing on $(-\infty,a)$ or $(-\infty,a]$ and non-$K$-decreasing on the rest of the line. $C(K)$ is its continuous part. With $G_{\kappa n} = \kappa\cdot + h_n$, the assumptions A1–A5 of §VI tie $m$ and $f_0$ to $c_0$, $c_\infty$ and the $K_\kappa$.

Formalization targets

Goal: Theorem 3

Under the standing assumptions and A1–A5, for every $n \ge 1$ the convolution $f_{n-1}*\varphi$ exists and

$$\exists\, s, S,\ \exists\, y \text{ generalized } (s,S) \text{ policy}: \quad y(x) \in Y_n(x) \ \ \forall x \in \mathbb R.$$

The statement fixes no numbers: $s$ and $S$ depend on $n$ and on the data.

Milestones

1. Lemma 9: $\bigcup_a C_a(K)$ equals the class of quasi-$K$-convex, piecewise continuous, PF-integrable functions tending to $\infty$ as $|x| \to \infty$.
2. Lemma 1: every $f \in C(K)$ has reals $s \le S$ with $S$ a global minimizer, $f > f(S) + K$ on $(-\infty,s)$, $f$ nonincreasing there, and $f$ non-$K$-decreasing on $[s,\infty)$.
3. Lemma 5: for continuous $g$, $f(x) = \int_0^\infty g(x-t)\lambda e^{-\lambda t}dt$ is $C^1$ with $f' = \lambda(g-f)$.
4. Lemma 6: $g*\varphi$ is continuous and $C^1$ off a finite set for a one-sided Pólya $\varphi$.
5. Lemma 10 and Theorem 1: $f \in C_a(K) \Rightarrow f*\varphi \in C(K)$, first for exponential $\varphi$, then for every one-sided Pólya density.
6. Theorem 2: if every $G_{\kappa n} \in C(K_\kappa)$ and every $Y_n(x) \ne \emptyset$, a generalized $(s,S)$ policy is optimal in period $n$.
7. Lemma 2: $f_n(x) \le f_n(y) + c(y-x)$ for $x \le y$.
8. Lemma 3: the inductive step producing the hypotheses of Theorem 2 from properties of $f_{n-1}$.

Significance

The result extends $(s,S)$-type structure from setup-plus-linear to arbitrary concave increasing ordering costs, which covers quantity discounts and multi-facility production. When $c$ is piecewise linear with $r$ pieces, the optimal policy is an $(s,S)_r$ policy described by at most $r$ reorder points and order-up-to levels. That is a finite-dimensional family, which makes computing policies tractable. The class $C(K)$ and its closure under Pólya convolution (Theorem 1) are statements about functions of one real variable, independent of the inventory model. Quasi-$K$-convexity extends both $K$-convexity and quasi-convexity (Lemma 8 of the paper).

The theorem is classical and proved on paper; no machine-checked version is known. Its appendix leaves several steps as "easily proved by contradiction", which a formal proof has to fill in. The platform has Bertsekas's $K$-convex $(s,S)$ lemma (BertsekasDP.kconvex_sS_structure, a result about $K$-convex rather than $C(K)$ functions), but no Pólya frequency functions, no quasi-$K$-convexity, and no concave-cost inventory model.

Difficulty

The obvious route copies Scarf: show that the cost-to-go is $K$-convex and that $K$-convexity survives taking expectations. With a concave ordering cost there is no single $K$, and the relevant functions $G_{\kappa n}$ are generally not $K_\kappa$-convex. The weaker property that does hold, membership in $C(K_\kappa)$, is not preserved by convolution with an arbitrary density. It is preserved by one-sided Pólya densities, and Theorem 1 is the step that shows this: exponential kernels come first (via the differential identity (23)), and the general case needs the Schoenberg representation of one-sided Pólya densities as limits of convolutions of exponentials. The second difficulty is combining the different slopes $\kappa \in C$ into one policy (Theorem 2). Separate $(s,S)$ pairs for each $\kappa$ do not by themselves give a monotone policy.

Formalization scope

All functions are ℝ → ℝ; the ordering cost is used only on $[0,\infty)$. The demand density is a function, not a measure; convolution is the Lebesgue integral over $\mathbb R$. $PF_n$ uses Matrix.det over Fin k. The value functions are defined by structural recursion on $n : \mathbb N$ with $f_0$ the terminal cost; $h_n$ is used for $n \ge 1$. $Y_n(x)$ is defined by the optimality inequality, never through the infimum. $G_{\kappa n}$ is defined by the paper's identity (7), $\kappa y + h_n(y)$. $R^- = (-\infty,0)$ is open, and "increasing" is read as nondecreasing. Slopes in $C$ are written $\kappa$ to separate them from the cost function $c$.

Added hypotheses and conventions:

• $m$ piecewise continuous. The paper uses this without stating it (proof of Lemma 3). It is a hypothesis of Lemma 3 and Theorem 3.
• Real-valued $f_n$ in Lemma 2. Following the convention of §X, Lemma 2 assumes each infimum defining $f_n$ is over a set bounded below.
• Measurability of $m$ and $f_0$ (§X) is implied by their piecewise continuity and is not stated separately.

Lean returns $0$ for an infimum over a set unbounded below and for the integral of a non-integrable function. The goal therefore concludes that $f_{n-1}*\varphi$ exists and that $Y_n(x)$ is nonempty (so the infimum is a minimum); it does not assume these. It also does not quantify over arbitrary functions satisfying a Bellman equation or over an arbitrary set-valued $Y$. Everything is built from the data $(c, m, \varphi, \alpha, f_0)$. The class $C(K)$ includes PF-integrability and coercivity, without which Lemma 1 fails.

Welcome contributions: Pólya frequency functions and the exponential special cases (the exponential density is $PF_\infty$), Leibniz-rule lemmas for exponential kernels, the theory of $C(K)$ and quasi-$K$-convex functions (reusable for other inventory models), and a formal Schoenberg representation (Theorem 6 of the paper, cited there and needed for Theorem 1). Theorems 4 and 5 (nonstationary and partial-backlogging extensions) are not part of this mission.

Selected references

• E. L. Porteus, On the Optimality of Generalized (s, S) Policies, Management Science 17(7):411–426, 1971. https://doi.org/10.1287/mnsc.17.7.411
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. F. Veinott Jr., On the Optimality of (s, S) Inventory Policies: New Conditions and a New Proof, SIAM Journal on Applied Mathematics 14(5):1067–1083, 1966. https://doi.org/10.1137/0114086
• I. J. Schoenberg, On Pólya Frequency Functions I. The Totally Positive Functions and their Laplace Transforms, Journal d'Analyse Mathématique 1:331–374, 1951. https://doi.org/10.1007/BF02790092
• S. Karlin, Total Positivity, Volume 1, Stanford University Press, 1968.

Motivation

Many problems in signal processing, statistics and operations research ask to minimize a sum $\Theta = \Phi + \Psi$ of a nonsmooth convex term $\Phi$ (a constraint indicator, an $\ell^1$ penalty) and a smooth term $\Psi$. The standard method is the forward-backward (proximal-gradient) algorithm: an explicit gradient step on $\Psi$ followed by a proximal step on $\Phi$. Its classical convergence theory requires $\Psi$ to be convex and the step size to stay below $2/L_\Psi$, where $L_\Psi$ is the Lipschitz constant of $\nabla\Psi$.

Attouch, Peypouquet and Redont (authors' manuscript of SIAM J. Optim. 24 (2014)) derive an inertial forward-backward algorithm (IFB) as a time discretization of a second-order dissipative dynamical system with Hessian-driven damping. The added inertial terms cost essentially nothing to compute, yet they allow step sizes beyond $2/L_\Psi$ and a smooth part $\Psi$ that is not convex, provided the sum $\Theta$ is.

Timeline of the relevant results:

• Heavy-ball-with-friction methods, the inertial discretizations of $\ddot u + \alpha\dot u + \nabla\Phi(u) = 0$, were introduced by Polyak (1964) and developed by Alvarez and Attouch (2001) for proximal schemes.
• Hessian-driven damping for one potential: Alvarez, Attouch, Bolte and Redont (2002); for a nonsmooth potential plus a smooth one, the continuous dynamics underlying (IFB): Attouch, Maingé and Redont (2012).
• The discrete algorithm (IFB) and its weak convergence in Hilbert spaces: Attouch, Peypouquet and Redont (2014), the paper of this mission.

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. Let $\Phi : H \to \mathbb R\cup\{+\infty\}$ and $\Psi : H \to \mathbb R$, and write $\Theta = \Phi + \Psi$ and $\mathcal S = \operatorname{Argmin}\Theta$. A vector $g$ is a subgradient of $\Phi$ at $u$, written $g \in \partial\Phi(u)$, if $\Phi(u) < +\infty$ and $\Phi(u) + \langle g, v - u\rangle \le \Phi(v)$ for all $v$.

Hypothesis H fixes positive constants $L_\Psi$, $a$, $b$ and a step size $\lambda$ with:

• $H_\Phi$: $\Phi$ is proper, lower semicontinuous and convex;
• $H_\Psi$: $\Psi$ is differentiable and $\nabla\Psi$ is $L_\Psi$-Lipschitz;
• $H_\lambda$: $0 < \lambda < \Lambda = \min\{1/a,\ 2(a+b)/(bL_\Psi)\}$;
• $H_\Theta$: $\Theta$ is convex and bounded from below.

Algorithm (IFB). From any $(u_0, y_0) \in H \times H$, compute for $k \ge 0$

$$0 \in \frac{u_{k+1}-u_k}{\lambda} + \partial\Phi(u_{k+1}) + a u_k - b y_k, \qquad 0 = \frac{y_{k+1}-y_k}{\lambda} + \nabla\Psi(u_{k+1}) - a u_{k+1} + b y_{k+1}.$$

A sequence $u_k$ converges weakly to $p$, written $u_k \rightharpoonup p$, if $\langle u_k, v\rangle \to \langle p, v\rangle$ for every $v \in H$. The analysis uses the velocity $\xi_k = u_k - u_{k-1}$, the energy $E_k = \Theta(u_k) + \gamma\|\xi_k\|^2$ with $\gamma = (1-a\lambda)/(2b\lambda^2)$, and two auxiliary real sequences $G_k(q)$ and $F_k(q)$, defined from $u$, $y$ and a reference point $q$ by (17) and (18) of the paper.

Formalization targets

Goal: Theorem 1

Under Hypothesis H, for every sequence generated by (IFB),

$$\lim_{k\to\infty}\Theta(u_k) = \inf\Theta;$$

if $\mathcal S \ne \emptyset$ and one of (i) $\mathcal S$ is a singleton, (ii) $\Phi$ is differentiable with weak-to-weak sequentially continuous gradient, (iii) $\nabla\Psi$ is weak-to-weak sequentially continuous, (iv) $\Psi$ is convex, holds, then

$$u_k \rightharpoonup p \quad\text{for some } p \in \mathcal S;$$

and if $\mathcal S = \emptyset$, then $\|u_k\| \to +\infty$.

Milestones

In the order of the paper's argument: Proposition 2 (energy decrease, $\sum\|\xi_k\|^2 < \infty$); Proposition 3 (the identity and inequality (19) for $F_k(q)$); Proposition 4 ($G_k(q)$ is bounded above for $q\in\operatorname{dom}\Phi$); the lower bound (28) on $F_k(q)$; Lemma 5 (a real-sequence lemma); Proposition 6 ($\Theta(u_k)\to\inf\Theta$, weak cluster points lie in $\mathcal S$); Lemma 7 (a boundedness lemma); Proposition 8 (boundedness of $(u_k)$ and convergence of $F_k(q)$ when $\mathcal S \ne\emptyset$).

Significance

The result gives convergence of a forward-backward type method under a step-size bound $\Lambda$ that can be made arbitrarily large by choosing $a$ small, and for a smooth term $\Psi$ that need not be convex. The special case $\Phi = \delta_C$ (indicator of a closed convex set) yields an inertial gradient-projection method, and the paper applies the theorem to feasibility problems, the CQ algorithm, Pareto fronts and $\ell^1$ signal recovery.

The theorem is proved in the paper; to our knowledge it is not formalized anywhere. A complete formalization would provide a machine-checked Liapunov analysis of an inertial proximal method in an infinite-dimensional Hilbert space, including the passage from a minimizing sequence to weak convergence. The milestones Proposition 2, 3 and 8 are energy estimates that also underlie other inertial and proximal schemes.

Difficulty

The energy $E_k$ controls the values $\Theta(u_k)$ and the velocities $\xi_k$, but not the iterates themselves. The first idea, proving that $\|u_k - q\|$ is nonincreasing for every $q \in \mathcal S$ (Fejér monotonicity, the standard route for the classical forward-backward method), does not come out of the energy estimates for (IFB): the inertial variable $y_k$ couples consecutive steps, and the distance to a minimizer is not a Liapunov function. The paper's replacement, the sequence $F_k(q)$, carries the auxiliary sum $G_k(q)$, whose upper bound already requires the full Hypothesis H. Because $H$ is infinite-dimensional, bounded sequences have only weakly convergent subsequences, so the minimizing property has to pass through weak lower semicontinuity of $\Theta$, and the final step, uniqueness of the weak cluster point, needs a separate argument in each of the cases (i)–(iv) together with Opial's lemma, which is not in Mathlib.

Formalization scope

• $H$ is a general real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); nothing is specialized to finite dimension.
• $\Phi$ and $\Theta$ take values in EReal. Properness excludes $-\infty$. Convexity of an extended-valued function is convexity of its epigraph in $H\times\mathbb R$, because Mathlib's ConvexOn needs a scalar action that EReal lacks. The subgradient predicate requires $\Phi(u) < +\infty$, so $\partial\Phi(u) = \emptyset$ off $\operatorname{dom}\Phi$.
• (IFB) is encoded as the subgradient inclusion, not through the proximity operator. Weak convergence is convergence of all inner products $\langle u_k, v\rangle$; weak cluster points are weak limits along strictly increasing subsequences.
• $L_\Psi > 0$ is assumed (harmless: a Lipschitz gradient is Lipschitz with every larger constant). The step size $\lambda$ is written lam.
• $\xi_k$, $z_k$, $E_k$, $G_k$, $F_k$ are defined on all natural indices, and each statement quantifies $k \ge 1$ (or $k \ge 2$ for $G_k$) as the paper does. Energies and values are never truncated to real numbers, so no statement becomes true through the convention EReal.toReal ⊤ = 0.
• Deviation from the printed text: Proposition 4 is printed under $H_\Phi$ and $H_\Psi$ only, but its proof invokes Proposition 2, which needs all of Hypothesis H, and the printed statement is false for step sizes above $\Lambda$ (e.g. $H=\mathbb R$, $\Phi = x^2/2$, $\Psi = 3x^2/2$, $a=2$, $b=0.02$, $\lambda = 10$). The milestone is stated under the full Hypothesis H.
• A formalization in which $\partial\Phi(u)$ is nonempty at points of infinite value, in which the energy is converted to a real number, or in which Hypothesis H cannot be satisfied, would make these statements trivial or vacuous, and is ruled out by the definitions above.

A complete development needs Opial's lemma, weak sequential compactness of bounded sets in Hilbert space, weak lower semicontinuity of lower semicontinuous convex functions, the descent lemma for functions with Lipschitz gradient, and monotonicity of the subdifferential. These are reusable well beyond this mission; contributions of any of them, and of the milestones in any order, are welcome.

Selected references

• H. Attouch, J. Peypouquet, P. Redont, A Dynamical Approach to an Inertial Forward-Backward Algorithm for Convex Minimization, SIAM J. Optim. 24(1), 2014 (statements cited from the authors' manuscript of Aug 2013). https://doi.org/10.1137/130910294
• H. Attouch, P.-E. Maingé, P. Redont, A second-order differential system with Hessian-driven damping; application to non-elastic shock laws, Differential Equations and Applications 4(1), 2012. https://doi.org/10.7153/dea-04-02
• F. Alvarez, H. Attouch, An inertial proximal method for maximal monotone operators via discretization of a nonlinear oscillator with damping, Set-Valued Analysis 9, 2001. https://doi.org/10.1023/A:1011253113155
• F. Alvarez, H. Attouch, J. Bolte, P. Redont, A second-order gradient-like dissipative dynamical system with Hessian-driven damping, J. Math. Pures Appl. 81(8), 2002. https://doi.org/10.1016/S0021-7824(01)01253-3
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

An expander is a sparse graph in which every set of vertices has many neighbours outside itself. Expanders are the building blocks of superconcentrators (sparse directed graphs that route any $r$ inputs to any $r$ outputs along vertex-disjoint paths), of sorting and switching networks, and of many constructions in complexity theory and coding; the survey of Hoory, Linial and Wigderson (Bull. AMS 2006) describes these uses. Random regular graphs are expanders with high probability, but applications need explicit families with fixed degree and a uniform expansion constant.

Alon and Milman (J. Combin. Theory Ser. B 38 (1985)) replace combinatorial expansion by a spectral quantity, the second-smallest eigenvalue $\lambda_1$ of the matrix $Q = D - A$ of a graph, which Fiedler called the algebraic connectivity (Czech. Math. J. 1973). Their Theorem 4.3 shows that a regular graph with $\lambda_1$ bounded away from $0$ yields an expander. This mission formalizes their Section 4 source of such graphs: Cayley graphs of the finite quotients of a group with Kazhdan's property (T).

Timeline:

• 1967: Kazhdan introduces property (T) and proves that $SL(n,\mathbb{Z})$, $n \ge 3$, has it (Funct. Anal. Appl. 1 (1967)).
• 1973: Margulis uses property (T) to give the first explicit expander family (Probl. Inf. Transm. 9 (1973)).
• 1981: Gabber and Galil give a variant of Margulis' construction with an explicit expansion constant, proved by Fourier analysis (J. Comput. Syst. Sci. 22 (1981)).
• 1985: Alon and Milman state the construction in terms of $\lambda_1$ (Lemma 4.8, Theorem 4.9) and link it to the concentration property of Section 2 of their paper.

Setting

Let $T$ be a finite group. A finite multigraph on $T$ is a symmetric matrix $M = (M_{w,u})$ of nonnegative integers, $M_{w,u}$ being the number of edges joining $w$ and $u$ (diagonal entries count loops). It is $k$-regular if every row sums to $k$. Its matrix is $Q = \operatorname{diag}(d(v)) - M$ with $d(v) = \sum_u M_{v,u}$, a real symmetric positive semidefinite matrix. Its eigenvalues, repeated according to multiplicity, are $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{|T|-1}$, and $\lambda_1(G)$ denotes the second of them.

Let $H$ be a group, $S \subseteq H$ a finite set with $S = S^{-1}$, and $\phi : H \to T$ a homomorphism onto $T$. The Cayley multigraph $G(T, \phi(S))$ joins $w$ and $u$ by as many edges as there are $s \in S$ with $w u^{-1} = \phi(s)$. It is $|S|$-regular, and its matrix is $Q = |S| \cdot I - \sum_{s\in S} \pi(\phi(s))$, where $\pi(t)$ is the permutation matrix of the left regular representation, $(\pi(t))_{w,u} = 1$ iff $w u^{-1} = t$.

An $(n,k,\varepsilon)$-enlarger (Definition 4.1) is a $k$-regular graph on $n$ vertices with $\lambda_1 \ge \varepsilon$.

A unitary representation $\pi$ of $H$ in a complex Hilbert space $V$ is essentially nontrivial (Definition 4.5) if no nonzero vector is fixed by every $\pi(h)$. A discrete group $H$ has property (T) (Definition 4.6) if there are $\varepsilon > 0$ and a finite $K \subseteq H$ such that for every essentially nontrivial unitary representation $\pi$ and every unit vector $y$ some $h \in K$ satisfies $|(\pi(h)y, y)| < 1 - \varepsilon$.

Formalization targets

Goal: Theorem 4.9

Let $H$ have property (T), let $S$ be a finite generating set of $H$ with $S = S^{-1}$, and let $\phi_i : H \to T_i$ be surjective homomorphisms onto finite groups with $|T_i| \to \infty$. Then there is one $\varepsilon > 0$ with

$$G(T_i, \phi_i(S)) \text{ is a } (|T_i|,\ |S|,\ \varepsilon)\text{-enlarger for every } i \text{ with } |T_i| \ge 2 .$$

The constant is unspecified: the theorem asserts uniformity in $i$, not a value.

Milestones, in the order the paper's argument uses them

1. Lemma 4.7. For any generating set $S$ of a property (T) group there is $\varepsilon > 0$ such that every essentially nontrivial unitary representation and every unit vector $y$ admit $s \in S$ with $|(\pi(s)y,y)| < 1-\varepsilon$.
2. Proof of Lemma 4.8, essential nontriviality. For $\phi$ onto $T$, every nonzero vector of $W = \{v : \sum_t v_t = 0\}$ is moved by some $\pi(\phi(h))$.
3. Proof of Lemma 4.8, Rayleigh's principle. For the Cayley multigraph, $\min\{(Qy,y) : y \in W,\ \|y\| = 1\} = \lambda_1(G)$.
4. Lemma 4.8. With $H$, $S$ and $\varepsilon$ as in Lemma 4.7, $S$ finite and $S = S^{-1}$, and $\phi$ onto a finite group $T$, the Cayley graph $G(T,\phi(S))$ is a $(|T|, |S|, \varepsilon)$-enlarger.

Significance

Theorem 4.9 turns an analytic property of one infinite group into a uniform spectral bound for infinitely many finite graphs of fixed degree. With Theorem 4.3 of the paper it produces explicit families of linear expanders, hence of linear superconcentrators; for $H = SL(n,\mathbb{Z})$, $n \ge 3$, and its reductions modulo $i$ the paper obtains infinitely many explicit families of $(n, 4, \varepsilon)$-enlargers. The same mechanism underlies later work on expanders from groups, surveyed in Lubotzky's monograph (Birkhäuser 1994).

The result is proved in the paper, modulo Lemma 4.7, which the paper refers to Margulis for. The formalization adds a checked account of every step, including Lemma 4.7 itself. At the pinned Mathlib revision there is no notion of property (T), of Kazhdan constants, or of the algebraic connectivity of a multigraph, and no machine-checked version of Theorem 4.9 is known on this platform.

Difficulty

The combinatorial and linear-algebra steps are routine; the substance is in two places. First, Lemma 4.7: Definition 4.6 supplies a constant for one finite set $K$, nothing in the definition relates $K$ to a given generating set $S$, the paper gives no proof, and the standard references state the textbook form $\|\pi(h)y - y\| \ge \varepsilon$ rather than the paper's absolute-value form $|(\pi(h)y,y)| < 1-\varepsilon$. Second, the uniformity: a spectral gap for each fixed quotient is easy, since a connected graph has $\lambda_1 > 0$, but a bound that does not decay as $|T_i| \to \infty$ is exactly what cannot come from any finite computation and must come from property (T) through Lemma 4.8. The Rayleigh quotient of milestone 3 is taken over real vectors, while Lemma 4.7 is stated for complex Hilbert spaces.

Formalization scope

Groups are Lean types with a Group instance; the finite groups $T$ carry Fintype and DecidableEq. Graphs are multigraphs given by symmetric matrices Matrix T T ℕ, with loops allowed. This matters: when $\phi$ identifies two generators or sends one to the identity, the degree is still $|S|$, and a loop contributes $0$ to $Q$. Mathlib's SimpleGraph Cayley graph forgets these multiplicities and is not used. $\lambda_1$ is the second-smallest eigenvalue with multiplicity of the real symmetric matrix $Q$ (via Matrix.IsHermitian.eigenvalues₀). It is defined spectrally, as in the paper, and not as a Rayleigh minimum. It is only meaningful for $|T| \ge 2$, and the goal excludes trivial quotients explicitly. Unitary representations are homomorphisms into the unitary group of bounded operators on a complex Hilbert space in universe Type. Compact subsets of a discrete group are finite sets.

A trivializing formalization is ruled out. Property (T) is not replaced by the hypothesis that the regular representations of the quotients have no almost-invariant vectors, which would make Theorem 4.9 a restatement of its hypothesis. And $\lambda_1$ is not defined as the minimum of $(Qy,y)$ over zero-sum unit vectors, which would make milestone 3 true by definition.

A complete development needs basic Kazhdan-constant manipulations, Courant–Fischer for real symmetric matrices, and the regular representation of a finite group as a unitary representation. The regularity of Cayley multigraphs and the identity $Q = |S| I - \sum_s \pi(\phi(s))$ are short. The spectral and representation-theoretic lemmas are reusable beyond this mission. Contributions of intermediate lemmas, such as the variational characterization of eigenvalues₀ or the invariance of the zero-sum subspace, are welcome.

Selected references

• N. Alon, V. D. Milman, λ1, Isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• D. A. Kazhdan, Connection of the dual space of a group with the structure of its closed subgroups, Funct. Anal. Appl. 1 (1967) 63–65. https://doi.org/10.1007/BF01075866
• G. A. Margulis, Explicit constructions of concentrators, Probl. Inf. Transm. 9 (1973) 325–332. http://mi.mathnet.ru/ppi1162
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Comput. Syst. Sci. 22 (1981) 407–420. https://doi.org/10.1016/0022-0000(81)90040-4
• M. Fiedler, Algebraic connectivity of graphs, Czech. Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• A. Lubotzky, Discrete Groups, Expanding Graphs and Invariant Measures, Birkhäuser, 1994. https://doi.org/10.1007/978-3-0346-0332-4
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Cambridge University Press, 2008. https://doi.org/10.1017/CBO9780511542749
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8