Operations Research

Motivation

A lifetime observed only after it has survived to a high age is described by its residual life: the additional time until failure, conditional on survival so far. Reliability analysis asks whether these conditional distributions settle into a stable shape after scaling and shifting. Extreme-value theory asks a related question about the largest observation in a large independent sample. Balkema and de Haan identify an exact connection between these questions for the exponential residual-life limit and the Gumbel maxima limit in Theorem 3 of their 1974 article. The connection lets one recognize the asymptotic form of old-age lifetimes from the domain of attraction of sample maxima, provided the lifetime distribution has no finite upper endpoint.

The article studies several residual-life limits. This mission isolates its exponential case, where the limiting conditional excess has distribution function $\Pi(x)=1-e^{-x}$ for $x\ge0$. The other continuous family $\Gamma_\alpha$ and the paper's discrete limits have separate hypotheses and attraction domains; they are outside this theorem.

Setting

Let $X$ have a probability distribution function $F$ on $\mathbb R$, and let its survival function be $R(x)=\Pr(X>x)=1-F(x)$. For a threshold $t$ with $R(t)>0$, the residual-life distribution function is

$$F_t(x)=\Pr(X-t\le x\mid X>t)=\frac{\Pr(t<X\le t+x)}{R(t)}.$$

It is zero for $x<0$. The class $D_0$ consists of the distributions with $R(x)>0$ for every real $x$. This says that the upper endpoint is infinite and makes $F_t$ meaningful at every threshold.

A law $F$ belongs to the domain of residual-life attraction $D_r(G)$ when $F\in D_0$ and there are a positive scale $a(t)$ and a shift $b(t)$ such that $F_t(b(t)+xa(t))$ converges weakly to $G(x)$ as $t\to\infty$. The shift here acts on $X-t$, the residual lifetime. Weak convergence means convergence at every continuity point of the limiting distribution function; it does not require convergence at a jump.

For maxima, $F$ belongs to the domain of attraction $D(G)$ if there are sequences $a_n>0$ and $b_n$ for which $F(a_nx+b_n)^n$ converges weakly to $G(x)$ as $n\to\infty$. The power is the distribution function of the maximum of $n$ independent observations after the indicated normalization. The relevant limit laws are the exponential residual-life law and the Gumbel law:

$$\Pi(x)=\begin{cases}0,&x<0,\\1-e^{-x},&x\ge0,\end{cases}\qquad \Lambda(x)=e^{-e^{-x}}\quad(x\in\mathbb R).$$

These definitions and formulas come from the introduction and §2 of the published article, printed pages 792–793 and 798.

Formalization targets

Theorem 3: the exact domain identity

The goal is the identity stated on printed page 798:

$$D_r(\Pi)=D(\Lambda)\cap D_0.$$

Both inclusions are required. In particular, membership in the maxima domain alone is insufficient: the maximum of a sample can have a Gumbel limit even when the underlying distribution has a finite upper endpoint, while residual life cannot be conditioned on survival beyond that endpoint. The $D_0$ condition is therefore part of the mathematical claim.

Supporting targets

The milestone list follows the statements used in the article's treatment of Theorem 3: the convergence-of-types remark on page 795; Lemma 3's asymptotic ratio $R(x-0)/R(x+0)\to1$; the tail criterion $nR(b_n+xa_n)\to e^{-x}$ associated with Gumbel attraction; the inclusion $D(\Lambda)\cap D_0\subseteq D_r(\Pi)$; and the passage from this tail limit on $x>0$ to all $x\in\mathbb R$. The last step retains the same normalization sequences. The article presents the criterion in one direction and relies on its converse at the end; the formal milestone records both directions with the same sequences.

Significance

The identity translates a conditional limit at a moving high threshold into a classical maxima-domain statement. A theorem about sample extremes can therefore characterize whether normalized remaining lifetime is asymptotically exponential. Conversely, observing exponential residual-life attraction determines a Gumbel maxima limit once the tail normalization is extended across the real line. The condition $D_0$ marks exactly where the conditional lifetime exists; omitting it would misstate the equivalence.

The article proves the result mathematically. The Lean targets here provide a precise representation of its distributions, normalizations, and limiting claims, with Theorem 3 still posed for formal proof. A complete development would add proofs of the supporting tail and convergence-of-types statements, then establish both inclusions. The definitions of weak convergence at continuity points, survival functions, and attraction domains can also support later formalizations of the paper's Pareto and discrete cases.

Difficulty

The simple comparison $F(a_nx+b_n)^n\approx e^{-nR(a_nx+b_n)}$ only relates the two limits after a suitable normalization is already available. The reverse direction starts with conditional residual-life convergence indexed by real thresholds, whereas maxima attraction needs a sequence indexed by integers. Sampling thresholds must preserve the tail asymptotics despite possible atoms. More seriously, the residual-life statement initially yields the required scaled-tail convergence only for positive arguments. The maxima limit must hold on the whole real line. A proof confined to that half-line cannot establish $D(\Lambda)$; the continuation across its left boundary is the central difficulty highlighted by the article on printed pages 798–799.

Formalization scope

Lean represents $F$ as the cumulative distribution function of a probability measure on $\mathbb R$ and uses real-valued probabilities of intervals for $R$ and $F_t$. The residual-life denominator is positive wherever $D_r$ is asserted. The extrema normalization is indexed by natural numbers, while the residual-life normalization is indexed by real thresholds. The scale is positive at every index; only large indices affect the limit. Weak convergence is encoded at every continuity point of the limit. As $\Pi$ and $\Lambda$ are continuous, their particular domain conditions amount to convergence at every real argument.

The paper uses two shift conventions: $F_t(b(t)+xa(t))$ shifts $X-t$, while the scaled-tail expressions $R(b_n+xa_n)$ shift $X$. Each statement uses the convention of its source passage. The convergence-of-types remark makes explicit the antitonicity and right-continuity of its limiting tails and states its identity where both arguments lie in the half-line on which convergence is known. Gnedenko's criterion is formalized as an equivalence: the printed sentence states the forward implication, and the conclusion of Theorem 3 uses the converse. The page-799 expression $R(b(t)+xa(t))/(t)$ has a missing $R$ in the denominator; the formal statement uses the intended $R(t)$, consistent with conditional probability and with equation (11). These choices prevent a zero-denominator quotient or an out-of-domain limit identity from trivializing a target. In particular, $D_0$ is part of the definition of $D_r(G)$: without it a law with a finite upper endpoint would have $R(t)=0$ for large $t$, the conditional distribution would be the junk quotient $0/0=0$, and the domain would be mis-specified. In Lemma 3 the limit $G$ is the distribution function of a probability measure, assumed continuous on all of $\mathbb R$.

The development needs measure-theoretic cumulative distributions and interval probabilities, filters for limits, and real exponential identities. The domain definitions and scaled-tail predicate are reusable beyond this theorem. Contributions that prove the stated milestones, or supply general lemmas about weak convergence and normalized tails, fit the scope.

Selected references

• A. A. Balkema and L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2(5), 792–804 (1974). DOI: 10.1214/aop/1176996548.
• B. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44(3), 423–453 (1943). DOI: 10.2307/1968974.

Residual life at great age

A component that has survived to age $t$ has a residual life time $X - t$, and in reliability, actuarial work and the analysis of excesses over high thresholds the question is what its conditional law looks like when $t$ is large. Balkema and de Haan (Ann. Probab. 2 (1974), 792–804) answered this in full generality: after an affine normalization, the only possible limit laws are the exponential law $\Pi$, the Pareto-type laws $\Gamma_\alpha$, and a two-parameter family of discrete laws $\Pi_{p,c}$. The continuous half of their classification became the Pickands–Balkema–de Haan theorem behind the peaks-over-threshold method of extreme-value statistics. The discrete half is less known, and this mission treats it: Theorem 5 of the paper (§3, p. 800) describes exactly which lifetimes are attracted to $\Pi_{p,c}$.

Discrete limits appear only when the normalization is allowed both a scale and a shift. They describe lifetimes that live, asymptotically, on a lattice-like set of ages whose spacing grows geometrically, with a fixed fraction of survivors failing at each lattice point.

The source is the published article in The Annals of Probability (DOI 10.1214/aop/1176996548); page numbers below are the journal's.

Setting

Let $X$ be a real random variable with law $\mu$, distribution function $F$ and tail $R(x) = 1 - F(x) = P\{X > x\}$, and assume $F(x) < 1$ for every $x$. The residual life distribution function at age $t$ is (1), p. 792,

$$F_t(x) = P\{X - t \le x \mid X > t\} = \frac{\mu((t, t+x])}{\mu((t,\infty))}.$$

A family of distribution functions $H_t$ converges weakly to $G$ if $H_t(x) \to G(x)$ at every continuity point $x$ of $G$. The domain of residual life time attraction $D_r(G)$ (p. 798) is the set of $F$ with $F(x) < 1$ for all $x$ for which some $a(t) > 0$ and $b(t)$ give

$$F_t(b(t) + x a(t)) \to G(x) \quad \text{weakly as } t \to \infty.$$

For $p > 0$ and $c \ge 0$ the discrete limit law is (p. 793), for $x \ge 0$,

$$\Pi_{p,c}(x) = 1 - \exp\Big(-p\Big[1 + \frac{\log(1+cx)}{cp}\Big]\Big) \ (c > 0), \qquad \Pi_{p,0}(x) = 1 - \exp\Big(-p\Big[1 + \frac{x}{p}\Big]\Big),$$

and $\Pi_{p,c}(x) = 0$ for $x < 0$; $[\,\cdot\,]$ is the integer part. Its tail takes the values $e^{-p}, e^{-2p}, \dots$ and jumps at $(e^{kpc} - 1)/c$, $k = 0, 1, \dots$ (at $kp$ if $c = 0$).

A distribution function $F_0 = 1 - R_0$ is discrete with jump sequence $t_0 < t_1 < \cdots$ if the $t_n$ are unbounded, each carries positive mass and there is no other mass. Two distribution functions with $F_i(x) < 1$ for all $x$ are tail equivalent if $1 - F_1(x) \sim 1 - F_2(x)$ as $x \to \infty$. The conditions of §3 are

$$\text{(12a)}\ \ \frac{t_{n+1} - t_n}{t_n - t_{n-1}} \to e^{pc}, \qquad \text{(12b)}\ \ \frac{R_0(t_{n+1})}{R_0(t_n)} \to e^{-p}.$$

Formalization targets

Goal: Theorem 5 (p. 800)

For $p > 0$ and $c \ge 0$,

$$F \in D_r(\Pi_{p,c}) \iff F \text{ is tail equivalent to a discrete } F_0 \text{ whose jumps satisfy (12a) and whose tail satisfies (12b).}$$

Milestones

1. (§3, pp. 799–800) A discrete $F$ satisfying (12a) and (12b) lies in $D_r(\Pi_{p,c})$.
2. (§3, p. 800) If $F_1$ is tail equivalent to $F_2 \in D_r(\Pi_{p,c})$, then $F_1 \in D_r(\Pi_{p,c})$. Milestones 1 and 2 give the "if" half.
3. (Proof of Theorem 5, p. 800) If $F \in D_r(\Pi_{p,c})$, there are $b_n \uparrow \infty$ with $R(b_{n+1})/R(b_n) \to e^{-p}$ and a discrete $F_0$, tail equivalent to $F$, with $R_0(t_n) = R(b_n)$ at its jumps.
4. (Proof of Theorem 5, pp. 800–801) Such an $F_0$ satisfies (12b) and (12a). Milestones 3 and 4 give the "only if" half.

Significance

Theorem 5, together with Theorems 1, 3 and 4 of the paper, completes the description of residual-life attraction: every nondegenerate limit is of one of the listed types, and each type's domain of attraction is identified. For the discrete types the answer is a statement purely about the geometry of the atoms of an approximating law, which makes membership checkable for concrete lifetimes (geometric-type laws on $\{0, 1, 2, \dots\}$ fall under $c = 0$, laws on a geometric grid $\{\lambda^n\}$ under $c > 0$). It also explains why discrete limits are invisible when only a scale normalization is allowed.

The theorem has been proved since 1974; it has not been formalized. A machine-checked development would supply weak convergence of distribution functions at continuity points, residual-life normalizations and tail equivalence as reusable objects, and would check a proof that the paper compresses into a page, including a convergence-of-types step on a half line that the paper cites from its own §1.

Difficulty

The "if" half is close to a computation, but the computation is about weak convergence to a step function: the normed tails converge only off the jumps, and the normalization must be extended from the jump times $t_n$ to all real ages $t$.

The "only if" half is the core. From $F \in D_r(\Pi_{p,c})$ alone one has to manufacture the atoms $t_n$ of a discrete law that $F$ itself need not have. The obvious attempt, reading the atoms off the jumps of $F$, fails because $F$ may be continuous: membership in $D_r(\Pi_{p,c})$ only says that $F$ drops by a factor close to $e^{-p}$ over short stretches, relative to the normalization, and never by an intermediate factor. Making "never by an intermediate factor" precise uniformly in the age $t$, with normalizations $a(t), b(t)$ about which nothing but their existence is known, is where the work lies; the same lack of control over $a(t)$ is what makes the gap ratio (12a) hard to extract.

Formalization scope

A law is a measure μ : Measure ℝ with IsProbabilityMeasure μ; the tail $R(x)$ is (μ (Set.Ioi x)).toReal, and $F_t(x)$ is μ((t, t+x]) / μ((t,∞)). $D_r(G)$ (InDr) includes $F(x) < 1$ for all $x$, normalizations $a(t) > 0$ for all real $t$, and "weakly" means convergence at every continuity point of $G$ and nowhere else; requiring convergence at the jumps of $\Pi_{p,c}$ would make $D_r(\Pi_{p,c})$ empty. $\Pi_{p,c}$ (piPC) is defined by cases $c = 0$ / $c > 0$ with Int.floor, so that $c = 0$ is not the junk value of a division by zero; it is used only with $p > 0$, $c \ge 0$. A discrete law with jump sequence $t$ (IsDiscreteWithJumps) has $t$ strictly increasing and tending to $\infty$, positive mass at each $t_n$ and no mass elsewhere. (12a) is indexed from $n = 1$. Tail equivalence (TailEquiv) includes $F_i(x) < 1$ for both laws.

Conventions and disclosed readings:

• The page proves the "if" direction by showing convergence to a function of the type of $1 - \Pi_{p,c}$; since $D_r$ lets $a, b$ be chosen freely, milestone 1 is stated with $\Pi_{p,c}$ itself.
• The proof of Theorem 5 uses the normalization (2)–(3) of p. 794, where $b(t)$ shifts $X$ rather than $X - t$; milestone 3 only asserts the existence of the sequence $b_n$ with $R(b_{n+1})/R(b_n) \to e^{-p}$, so no convention enters its statement.
• "$F_0$ only takes the values $F(b_n)$" is formalized as $R_0(t_n) = R(b_n)$ for all $n$, the form the next paragraph of the page uses. This identity is a hypothesis of milestone 4, as on the page, and cannot be dropped: a law tail equivalent to $F$ may carry extra atoms of vanishing relative mass, at which (12a) and (12b) fail.
• The page identifies the limit of the gap ratios as the scale constant $A$ of a functional equation; milestone 4 states it as $e^{pc}$, the gap ratio of the jumps of $\Pi_{p,c}$.
• Theorem 5 prints "distribution fuction"; this typo is kept in the quoted text only.

No statement is trivialized: $D_r(\Pi_{p,c})$ is nonempty (the geometric law on $\{0,1,2,\dots\}$ lies in $D_r(\Pi_{p,0})$), and Theorem 5 is not a definitional unfolding, since $D_r$ is defined by weak convergence and the right-hand side by discrete approximation.

A complete development needs: weak convergence of distribution functions at continuity points, a convergence-of-types lemma on a half line (the Remark after Lemma 1 of the paper, p. 795), and elementary facts on step functions. The first two are reusable across the whole paper and across extreme-value theory. Contributions of either half of the theorem, or of the convergence-of-types lemma, are welcome.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), 119–131. https://doi.org/10.1214/aos/1176343003
• B. V. Gnedenko, Sur la distribution limite du terme maximum d'une série aléatoire, Annals of Mathematics 44 (1943), 423–453. https://doi.org/10.2307/1968974
• L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

Motivation

In the edge-disjoint paths problem (EDP) one is given an undirected graph and a list of source–sink pairs, and asks how many pairs can be connected simultaneously by paths that share no edge. Its relaxation EDP with congestion (EDPwC) allows every edge to carry up to a fixed number of paths. Both are central problems of network routing and of approximation algorithms, and the standard algorithmic tool for them is the multicommodity flow relaxation: a linear program that may split each pair's unit of demand fractionally over many paths. Rounding this LP is how most approximation algorithms for routing work, so the ratio between its optimum and the best integral routing, the integrality gap, bounds what any LP-based algorithm can achieve.

Without congestion the gap of this relaxation can be as large as $\Omega(\sqrt V)$ (Chekuri–Khanna–Shepherd 2006), and the question is how much a small congestion helps. Andrews, Chuzhoy, Guruswami, Khanna, Talwar and Zhang (Combinatorica 2010) proved hardness of approximation for EDPwC (their Theorems 1 and 2) and, independently and unconditionally, that the gap of the relaxation remains $(\log V)^{\Omega(1/c)}$ even when the integral solution may use congestion $c-1$ (their Theorem 5). In particular, for every fixed integer $i$ the gap between $(1/i)$-integral and fractional multicommodity flow in undirected graphs is superconstant. This mission formalizes Theorem 5 for EDPwC.

Setting

Fix integers $n\ge1$ and $c\ge2$. Write $\log$ for $\log_2$ and $\ln$ for the natural logarithm, and set

$$\beta_1=\frac14\Big(\frac{\log n}{150(\log\log n)^2}\Big)^{1/c},\qquad \beta_2=6(2\beta_1)^{c-1}\ln\beta_1 .$$

A random $c$-uniform hypergraph $H$ on the vertex set $\{0,\dots,n-1\}$ has $m=\lfloor\beta_2 n\rfloor$ hyperedges $h_0,\dots,h_{m-1}$, chosen independently, each uniformly among the $c$-element subsets of the vertices.

From $H$ one builds a graph $G=G(H)$. For every hyperedge $h_i$ it has two vertices $\ell_i,r_i$ joined by a special edge; for every vertex $v$ of $H$ it has a source $s(v)$ and a sink $t(v)$. If $v$ lies in the hyperedges $h_{i_1},\dots,h_{i_k}$ with $i_1<\dots<i_k$, the regular edges $(s(v),\ell_{i_1})$, $(r_{i_j},\ell_{i_{j+1}})$ for $1\le j<k$, and $(r_{i_k},t(v))$ are added. The canonical path of $v$ is $P(v)=(s(v),\ell_{i_1},r_{i_1},\dots,\ell_{i_k},r_{i_k},t(v))$; it crosses the special edge of every hyperedge containing $v$. The EDP instance has one pair $(s(v),t(v))$ for each $v$.

A feasible fractional solution puts flow $f(P)\in[0,1]$ on $s(v)$–$t(v)$ paths $P$, with routed amount $x_v=\sum_P f(P)\le1$ for each pair and at most one unit of flow through each edge; its value is $\sum_v x_v$. An integral routing with congestion at most $c-1$ connects a set of pairs, each by one path, so that every edge lies on at most $c-1$ of these paths; its value is the number of connected pairs.

The analysis uses three events of $H$: $\mathcal E_1$, that some set of $n/\beta_1$ vertices contains no hyperedge; $\mathcal E_2$, that more than $n/\beta_1$ vertices lie in more than $10\beta_2c$ hyperedges; and $\mathcal E_3(g)$, that the graph $G'$ obtained from $G$ by contracting every special edge has more than $(6\beta_2c^2)^{g+1}$ cycles of length at most $g$.

Formalization targets

Goal: Theorem 5 for EDPwC, in the explicit form of Section 2

There are absolute constants $\alpha>0$ and $N_0$ such that for all $n\ge N_0$ and all integers $c$ with $2\le c\le\alpha\log\log n/\log\log\log n$ some hypergraph $H$ as above satisfies

$$\exists\ \text{fractional solution of } G(H)\ \text{of value } \frac nc\qquad\text{and}\qquad \text{every congestion-}(c-1)\text{ routing of } G(H)\ \text{routes}\ \le\frac{4n}{\beta_1}\ \text{pairs},$$

so the integrality gap is at least $\beta_1/(4c)$. The paper's Theorem 5 states this as $\Omega\big(\frac1{c}(\log V/(\log\log V)^2)^{1/(c+1)}\big)$ for congestion $c$ and $V$ vertices; the goal keeps the paper's own Section 2 parameters, which fix the instance and leave the constants $\alpha,N_0$ open.

Milestones

Lemma 6, Lemma 7 and Lemma 8 ($\Pr[\mathcal E_1],\Pr[\mathcal E_2],\Pr[\mathcal E_3(g)]\le\frac14$); the joint good event of Section 2.4; the fractional solution of value $n/c$; and the three bounds of the gap analysis, $|\mathcal P_1|\le n/\beta_1$ (canonical paths), $|\mathcal P_2|\le n/\beta_1$ (long non-canonical paths), $|\mathcal P_3|\le n/\beta_1+2gc(6\beta_2c^2)^{2g+2}$ (short non-canonical paths), combined into $|\mathcal P'|\le4n/\beta_1$.

Significance

The result shows that the multicommodity flow relaxation cannot certify a constant-factor approximation for undirected EDPwC with any constant congestion: against integral solutions of congestion $c-1$ its gap is at least $(\log V)^{\Omega(1/c)}$. Any algorithm that compares its output with this LP inherits the bound. It complements the paper's hardness results, which hold only under a complexity assumption. The instance is a short explicit construction from a random hypergraph, so the theorem is also a statement in probabilistic combinatorics: random sparse uniform hypergraphs are, with constant probability, simultaneously "covering" (no large hyperedge-free set), of bounded degree, and nearly free of short cycles.

The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces one: a formal model of the path LP and of congestion-bounded integral routings on simple graphs, reusable for other routing gaps; a formal random-hypergraph model with first-moment and Chernoff-type estimates; and the deterministic gap analysis. Variants with better constants, or the stronger statement that at least a quarter of all hypergraphs work, are welcome as additional results.

Difficulty

The fractional side and the bound on canonical routings are short. The difficulty lies in two places. First, Lemma 8 bounds the expected number of short cycles of $G'$; the adjacency of $G'$ depends on all hyperedges at once (consecutiveness along each vertex's sequence), and the obvious estimate through the intersection graph of $H$ fails, because many hyperedges through a common vertex form a clique there. What keeps the count small is the order structure of each vertex's hyperedge sequence, which the intersection graph forgets. Second, the bound on short non-canonical paths requires turning two distinct routing paths of a pair into a short cycle of the contracted graph and charging it with the congestion constraint. Finally, the closing estimate $2gc(6\beta_2c^2)^{2g+2}\le n/\beta_1$ holds only for large $n$ in the stated range of $c$, and the printed chain for it is not literally correct, so the asymptotics have to be done afresh.

Formalization scope

Vertices of $H$ are Fin n, hyperedges are indexed by Fin m with $m=\lfloor\beta_2n\rfloor$, and $H$ is an element of Fin m → {s : Finset (Fin n) // s.card = c}; probabilities are normalized counts over this finite set (uniform measure, which is independence of the hyperedges). The conventions are:

• $\log=\log_2$ and $\ln$ is natural; $\beta_1$ uses a real $1/c$-th power.
• The paper's integers $\beta_2n$, $n/\beta_1$ (bad-set size) and $g=3\beta_1\beta_2c^2$ are $\lfloor\beta_2n\rfloor$, $\lceil n/\beta_1\rceil$ and $\lceil3\beta_1\beta_2c^2\rceil$; the thresholds $n/\beta_1$, $4n/\beta_1$, $10\beta_2c$, $(6\beta_2c^2)^{g+1}$ stay real.
• "For sufficiently large $n$" and $c\le O(\log\log n/\log\log\log n)$ become absolute constants $N_0$ and $\alpha$, quantified before $n$ and $c$. Lemma 8 and the deterministic bounds carry instead the explicit inequalities on $\beta_1,\beta_2$ their arguments use.
• $G(H)$ is a simple graph (coinciding regular edges are one edge). A vertex in no hyperedge gets the edge $(s(v),t(v))$, the $k=0$ case of its canonical path; the page leaves this case out.
• $K_g$ counts cycles of $G'$, each once as an edge set; the paper's definition says "in $G$", its proof and use say $G'$.
• Routing paths are paths (no repeated vertex); lengths count edges of $G(H)$; canonicity is equality of vertex sequences.

The goal cannot be met by an unrelated graph: the instance must be $G(H)$ for a hypergraph with exactly $\lfloor\beta_2n\rfloor$ hyperedges of size $c$ on $n$ vertices, the fractional solution must respect $x_v\le1$ and capacity $1$, and the integral bound is over all routings of congestion $c-1$.

Not in scope: the ANFwC half of Theorem 5, the remark on a superconstant gap at $c=\Theta(\log\log V/(\log\log\log V)^2)$, and the hardness results of Sections 3–5 (Theorems 1 and 2, Corollaries 3 and 4).

A complete development needs Chernoff and Markov bounds for counting measures, binomial-coefficient estimates, cycle extraction from two distinct paths in a simple graph, and the asymptotic estimates for $\beta_1,\beta_2$. The routing and LP definitions and the cycle-extraction lemma are reusable beyond this mission.

Selected references

• M. Andrews, J. Chuzhoy, V. Guruswami, S. Khanna, K. Talwar, L. Zhang, Inapproximability of Edge-Disjoint Paths and Low Congestion Routing on Undirected Graphs, Combinatorica 30(5), 485–520, 2010. https://doi.org/10.1007/s00493-010-2455-9
• C. Chekuri, S. Khanna, F. B. Shepherd, An $O(\sqrt n)$ approximation and integrality gap for disjoint paths and unsplittable flow, Theory of Computing 2, 137–146, 2006. https://doi.org/10.4086/toc.2006.v002a007

Why expected interval length matters

A simulation run often estimates a steady-state mean without producing independent observations. A confidence interval must account for dependence in the output, and the relevant variance constant may be unknown. Standardized time series (STS) methods use the shape of an integrated output path to cancel that constant rather than estimating it separately. The resulting interval can be computed from one run, but its length can vary substantially with the chosen standardizing functional. Glynn and Iglehart introduced a common functional framework for these methods and asked how short their expected intervals can be as the run grows. Their 1990 paper identifies a universal lower bound.

The comparison is operational. A shorter confidence interval conveys a more precise estimate at the same nominal coverage. The authors also compare STS with procedures that consistently estimate the variance constant. They state that the lower bound is attained by the latter procedures and approached, but not attained, by STS intervals. The present mission isolates the bound for STS itself, Corollary 4.16. It does not make the claim that a particular STS rule attains it. This distinction follows the paper's introduction and §4.

The stochastic setting

Let $Y(t)$ be a real simulation output process for $t\ge0$. Its integrated average path at run length $n$ is $\overline Y_n(t)=n^{-1}\int_0^{nt}Y(s)\,ds$ for $0\le t\le1$. The unknown steady-state mean is $\mu$. The paper assumes a functional central limit theorem in the space $C[0,1]$ of continuous real paths:

$$X_n(t):=\sqrt n\bigl(\overline Y_n(t)-\mu t\bigr) \ \Rightarrow\ \sigma B(t),\qquad \sigma>0,$$

where $B$ is standard Brownian motion. Convergence is weak convergence of random continuous paths in the uniform topology. This is Assumption (2.1), rather than a claim that every output process satisfies it. The paper lists several classes of processes for which such a theorem is available under further conditions (§2, pp. 2–3).

An STS scale functional $g:C[0,1]\to\mathbb R$ belongs to $\mathcal M$ when it is measurable, positively homogeneous, unchanged by subtracting any multiple of the identity path $k(t)=t$, positive at $B$ almost surely, and continuous at $B$ almost surely. The last two conditions ensure that the Brownian ratio is a meaningful distributional limit. The paper also describes these functionals through the bridge map $(\Gamma x)(t)=x(t)-t x(1)$: a member of $\mathcal M$ can be written as $b\circ\Gamma$ for a suitable $b$. Thus the scale is determined by a Brownian bridge while the endpoint $B(1)$ is independent of it (Propositions 2.7–2.8).

Define $H(x)=P\{B(1)/g(B)\le x\}$. For a confidence level $1-\delta$, choose endpoints $\alpha,\beta$ with $H(\beta)-H(\alpha)=1-\delta$. The STS confidence interval from equation (2.10) has endpoints $\overline Y_n(1)-g(\overline Y_n)\beta$ and $\overline Y_n(1)-g(\overline Y_n)\alpha$. Its length is $L_n=g(\overline Y_n)(\beta-\alpha)$. Here $\delta$ lies strictly between zero and one; the endpoint equation is part of the construction, not an arbitrary choice.

Formalization target

The goal is Corollary 4.16 for every nonnegative $g\in\mathcal M$ under Assumption (2.1). Write $\Phi$ for the standard normal distribution function and $p=\Phi^{-1}(1-\delta/2)$. Then

$$\liminf_{n\to\infty}\sqrt n\,E[L_n] \ \ge\ 2\sigma p =2\sigma\Phi^{-1}(1-\delta/2).$$

The expectation and liminf admit $+\infty$. The statement does not impose an integrability assumption that would remove that case. It quantifies over every admissible STS functional and every interval whose endpoints have the specified Brownian confidence mass (Corollary 4.16, p. 12).

Three substantial targets precede the corollary. Proposition 4.1(a) relates scaled expected length to $\sigma E[g(B)](\beta-\alpha)$. Proposition 4.3 says a symmetric choice of $\alpha,\beta$ minimizes $\beta-\alpha$. Theorem 4.8 gives $E[g(B)]\Phi^{-1}_g(1-\delta/2)\ge\Phi^{-1}(1-\delta/2)$, where $\Phi^{-1}_g$ denotes the quantile of $H$. The milestone list also includes the cited Brownian independence, mixture distribution, scale invariance, and continuous mapping statements that put these targets in context.

What the bound establishes

The corollary supplies a benchmark for the asymptotic expected length of any interval in this STS class. A proposed standardizing functional cannot beat the normal-quantile constant while retaining the stated functional limit and confidence construction. It also identifies the quantity against which the paper's other interval procedures can be compared. The bound applies uniformly to the class $\mathcal M$, not to a chosen batch size or a particular form of $g$ (Glynn–Iglehart 1990, §4).

The mathematical result has been proved in the source paper. This mission supplies formal statements and their shared definitions as proof targets; it does not claim that their Lean proofs already exist. A complete development would formalize the known arguments for the milestones and corollary, including the Brownian path representation, weak convergence, quantile properties, and expectation inequalities. Those components could be reused in other work on simulation output analysis and ratios of weakly convergent processes.

Where the formal proof is demanding

Weak convergence alone does not imply convergence of expectations. In particular, a continuous mapping limit for $g(X_n)$ cannot simply be integrated as an ordinary finite real expectation when the family is not uniformly integrable. Proposition 4.1(a) asks only for a lower bound, and its statement must still account for $E[g(B)]=+\infty$. This is why the goal is expressed with a liminf and extended nonnegative expectations rather than a real-valued limit. A separate difficulty is that the interval width depends jointly on a distributional scale and a choice of two quantiles. Bounding either one in isolation does not state the corollary.

Formalization scope and conventions

Paths are Mathlib's $C([0,1],\mathbb R)$ with its uniform metric and Borel sigma algebra. A standard Brownian motion is a measurable random continuous path agreeing with an $\mathbb R_{\ge0}$-indexed real Brownian motion on $[0,1]$. The paper's discontinuity set $D(g)$ is the set where $g$ is not continuous. Assumption (2.1) includes joint measurability of $Y$ and finite-interval pathwise integrability so that each integrated average is defined. The path $\overline Y_n$ is supplied together with its defining integral equation, which determines it pointwise. Its values are not free parameters.

Indices $n$ are natural numbers. At $n=0$, the average uses Lean's total division and is zero; this initial value does not affect an asymptotic statement. The positive Brownian scale $\sigma$ is finite. The parameters satisfy $0<\delta<1$, and $H(\beta)-H(\alpha)=1-\delta$. The normal and STS quantiles appear as real parameters pinned by their distribution-function equations, avoiding an unbounded or empty real infimum. Expected nonnegative lengths and scales are integrals valued in $\mathbb R_{\ge0}\cup\{+\infty\}$. The class $\mathcal N$ explicitly requires measurability of $b$, the standing convention needed for its equality with $\mathcal M$.

The corollary retains the entire class $\mathcal M$ and Assumption (2.1), with $g\ge0$ on all continuous paths. It cannot be replaced by a statement about a single easy functional or by assuming the bound on an auxiliary criterion. Useful contributions include the Brownian bridge independence theorem, the normal scale-mixture identity, distribution-function regularity, and the asymptotic expectation result.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. DOI: 10.1287/moor.15.1.1.

Why cores of games with side payments

A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.

The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.

Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition $A\subseteq N$ is identified with its characteristic vector $\tau^A\in\{0,1\}^n$, and $\tau^N=(1,\dots,1)$. A fuzzy coalition is a vector $\tau\in[0,1]^n$, where $\tau_i$ is the rate at which player $i$ participates.

A fuzzy game with side payments is a worth function $v$ with $v(0)=0$ that is positively homogeneous, $v(t\tau)=t\,v(\tau)$ for $t>0$. Homogeneity extends $v$ from $[0,1]^n$ to the orthant $\mathbb R^n_+$. Its core is

$$\operatorname{core}(v)=\Big\{c\in\mathbb R^n:\ \sum_{i\in N}c_i=v(\tau^N),\ \ \sum_{i\in N}\tau_ic_i\ge v(\tau)\ \text{for all }\tau\in[0,1]^n\Big\},$$

the allocations that no fuzzy coalition blocks. The superdifferential of $v$ at $\tau$ is $\partial v(\tau)=\{c:\ v(\tau)-v(\sigma)\ge\sum_i c_i(\tau_i-\sigma_i)\ \text{for all }\sigma\in\mathbb R^n_+\}$.

A usual game with side payments is given by a family $\mathscr C$ of nonempty coalitions that contains $N$ and every singleton $\{i\}$, and by a worth $v(A)\in\mathbb R$ for each $A\in\mathscr C$. Its core is the set of $c\in\mathbb R^n$ with $\sum_{i\in N}c_i=v(N)$ and $\sum_{i\in A}c_i\ge v(A)$ for every $A\in\mathscr C$. For $\tau\in\mathbb R^n_+$, $\mathscr C(\tau)$ is the set of nonnegative weights $m(A)$, $A\in\mathscr C$, with $\sum_{A\ni i}m(A)=\tau_i$ for each player $i$, and

$$\pi v(\tau)=\sup_{m\in\mathscr C(\tau)}\ \sum_{A\in\mathscr C}m(A)\,v(A).$$

The game is balanced if $\pi v(\tau^N)=v(N)$.

Formalization targets

Goal: Proposition 6.1

$$\operatorname{core}(v)\neq\emptyset\iff \pi v(\tau^N)=v(N),\qquad\text{and then}\qquad \operatorname{core}(v)=\operatorname{core}(\pi v).$$

The first half is the Bondareva–Shapley theorem for an arbitrary family $\mathscr C$. The second identifies the core of the discrete game with the core of the fuzzy game $\pi v$.

Milestones

1. §2 (4)–(5). For a positively homogeneous $v$ with $v(0)=0$, $\operatorname{core}(v)=\partial v(\tau^N)$.
2. Remark 2.1. Such a $v$ is concave on $\mathbb R^n_+$ if and only if it is superadditive, $v(\tau+\sigma)\ge v(\tau)+v(\sigma)$.
3. Proposition 2.1. If $v$ is moreover concave, its core is convex, compact and nonempty; if $v$ is differentiable at $\tau^N$, the core is $\{Dv(\tau^N)\}$.
4. §6 (5). If $m\in\mathscr C(\tau)$ and $m(A)>0$, then $A\subseteq A_\tau=\{i:\tau_i>0\}$.
5. §6 (2). $\pi v$ is the smallest concave positively homogeneous function on $\mathbb R^n_+$ with $\pi v(\tau^A)\ge v(A)$ for every $A\in\mathscr C$.
6. §6, after (6). The core of the fuzzy game $\pi v$ is nonempty, convex and compact, whether or not $v$ is balanced.

Significance

Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when $\pi v$ is smooth at $\tau^N$, reduces to a single point given by the gradient.

The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family $\mathscr C$ of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension $\pi v$. The definitions (fuzzy coalitions, balances, $\pi v$) are reusable by later missions on games without side payments and on values of fuzzy games.

Difficulty

The inclusion $\operatorname{core}(v)\subseteq\operatorname{core}(\pi v)$ and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from $\pi v(\tau^N)=v(N)$, a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because $\pi v$ is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.

Formalization scope

Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:

• A fuzzy game is a function on $\mathbb R^n$ whose values off the orthant are never used; $v(0)=0$ and homogeneity for every $t>0$ and $\tau\ge0$ are hypotheses of every §2 statement, because §2 states them once for the whole section. Concavity is concavity on $\mathbb R^n_+$.
• In the superdifferential (5), $\sigma$ ranges over $\mathbb R^n_+$, the domain of the extended $v$; the paper leaves this implicit.
• "Differentiable at $\tau^N$" is DifferentiableAt at the interior point $(1,\dots,1)$, and $Dv(\tau^N)$ is the vector of partial derivatives.
• The family $\mathscr C$ contains $N$ and all singletons and excludes $\emptyset$; the core and $\pi v$ use only coalitions in $\mathscr C$, so $v(\emptyset)=0$ plays no role. Because $N\in\mathscr C$ and $\emptyset\notin\mathscr C$, the family exists only for $n\ge1$.
• $\pi v$ is a real supremum. For $\tau\ge0$ the set of values is nonempty and bounded above, so the value is the paper's; off the orthant the set is empty and the value is never used.
• The printed $v(\mathscr C)$ and $\tau^{\mathscr C}$ in §6 (2)–(3) are read as $v(A)$ and $\tau^A$, as §6 (4) settles.

Balancedness is the equation $\pi v(\tau^N)=v(N)$ with $\pi v$ built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes $\pi v$ to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1), 1981, 1–13. https://doi.org/10.1287/moor.6.1.1
• O. N. Bondareva, Some applications of linear programming methods to the theory of cooperative games, Problemy Kibernetiki 10, 1963, 119–139 (in Russian; no stable online copy).
• L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14(4), 1967, 453–460. https://doi.org/10.1002/nav.3800140404
• H. E. Scarf, The core of an N person game, Econometrica 35(1), 1967, 50–69. https://doi.org/10.2307/1909703
• L. J. Billera, Some theorems on the core of an n-person game without side-payments, SIAM Journal on Applied Mathematics 18(3), 1970, 567–579. https://doi.org/10.1137/0118007
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

A maximum matching of a graph is a largest set of edges no two of which share a vertex. Maximum matchings are rarely unique, and a basic question is which features of them are forced by the graph. J. Edmonds' paper Paths, trees, and flowers (Canad. J. Math. 17 (1965), 449–467) gave the first polynomial-time algorithm for maximum matching in general graphs. Its Section 6, Invariance of the dual, uses the output of that algorithm to answer this question. The vertices that some maximum matching leaves uncovered, their neighbours, and the rest form a decomposition of the graph that does not depend on the matching chosen or on any choice made by the algorithm.

This decomposition is now called the Gallai–Edmonds structure theorem. T. Gallai obtained it independently (Gallai 1963, 1964; see Selected references). It is a standard tool in matching theory (Lovász–Plummer, Matching Theory, 1986): it determines the minimum odd-set cover of Section 5 of the same paper canonically (6.7), and it underlies the Tutte–Berge formula and the analysis of factor-critical graphs.

Timeline. Berge (1957) characterized maximum matchings by the absence of augmenting paths. Gallai (1963–1964) and Edmonds (1965, §6) proved the structure theorem; Edmonds' proof goes through the trees and shrunken blossoms of his algorithm. Witzgall's argument, reported in 6.6, simplifies the converse half.

Setting

A graph $G$ has a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices; parallel edges are allowed. A vertex is exposed for a set of edges $M$ if no edge of $M$ meets it.

An alternating tree $J$ is a tree (a connected graph with one more vertex than edges) whose vertices are split into inner and outer vertices, so that every edge joins an inner vertex to an outer one and every inner vertex meets exactly two edges of $J$. A planted tree for $M$ with root $r$ is an alternating tree such that $M \cap J$ is a maximum matching of $J$ and $r$, the vertex of $J$ left exposed by $M \cap J$, is exposed for $M$.

Shrinking a vertex set $U$ replaces $U$ by a single pseudovertex. Edges inside $U$ disappear; edges leaving $U$ keep their identity and now meet the pseudovertex. The set $U$ is the pseudovertex's complete expansion. A blossom for $M$ is an odd circuit $B$ for which $M \cap B$ is a maximum matching of $B$. Shrinking blossoms repeatedly, inside graphs already shrunk, gives the graph $G^* = G/\mathcal P$, where $\mathcal P$ is a partition of the vertices into blossom sets.

Construction 6.0. Let $M$ be a maximum matching. Run the matching algorithm on $(G, M)$ without augmenting. It grows planted trees $J_1, \dots, J_n$ in $G^*$, one from each exposed vertex, and shrinks blossoms as they appear. The output satisfies:

1. the trees are disjoint and planted for $M^* = M/\mathcal P$;
2. every exposed vertex of $G^*$ lies in some tree;
3. $J_i$ is Hungarian in $G^* - J_1 - \dots - J_{i-1}$: its outer vertices are joined only to its own inner vertices or to earlier trees;
4. every pseudovertex is an outer vertex of some $J_i$.

The outer vertices $O(G)$ are the vertices whose part is a one-vertex outer vertex of some $J_i$, together with all vertices of pseudovertex expansions. The inner vertices $I(G)$ are the vertices whose part is an inner vertex of some $J_i$.

Formalization targets

Goal: Theorem 6.2 (a)–(c)

For every maximum matching $M$ and every output of construction 6.0:

$$\text{(a)}\quad v \in O(G) \iff \exists\, M' \text{ maximum matching of } G \text{ with } v \text{ exposed for } M',$$ $$\text{(b)}\quad v \in I(G) \iff v \notin O(G) \text{ and } v \text{ is adjacent to a vertex of } O(G),$$ $$\text{(c)}\quad u,v \text{ in the same part of } \mathcal P \iff u = v \text{ or } u, v \text{ in the same component of } O(G)^+,$$

where $O(G)^+$ is the subgraph induced on $O(G)$.

Milestones

• 4.1–4.2: the maximum matchings of an alternating tree.
• 4.14: lifting a matching through the complete expansion of a pseudovertex, with a free choice of the exposed vertex.
• 4.15, extension, in the forest form of 4.20.
• 6.4: adjacency of outer and inner vertices.
• 6.2 (b) and 6.2 (c) separately.
• 6.5: every outer vertex is exposable.
• 6.6: for non-outer $v$ meeting $e \in M$, $M - e$ is maximum in $G - v$.
• 6.6: only outer vertices are ever exposed.

A companion item states that construction 6.0 succeeds for every maximum matching.

Significance

The result. Part (a) characterizes, without reference to any algorithm, the vertices that a maximum matching can miss. Parts (b) and (c) then make $I(G)$ and $G^*$ invariants of $G$, as 6.1 announces: "the graph $G^*$ is uniquely determined by $G$ alone". Several consequences rest on this invariance: the unique preferred minimum odd-set cover (6.7), the Tutte–Berge deficiency formula read off from $|I(G)|$ and the components of $O(G)^+$, and the classification of graphs into those with and without perfect matchings in terms of a canonical barrier.

Formalizing it. The theorem has been proved since 1964, but the proof in this paper has not been machine-checked. A formalization requires the paper's own objects: multigraphs with edge identity preserved under contraction, nested blossom shrinking, and alternating and planted trees. These are the objects of Edmonds' blossom algorithm, and they are reusable for any formal treatment of it. Mathlib contains Tutte's theorem for simple graphs but neither shrinking nor the Gallai–Edmonds decomposition.

Difficulty

The statement is about one particular output of a nondeterministic process. The partition into trees depends on the order in which they were grown, and the non-matching tree edges and the blossoms chosen are arbitrary (6.1). An outer vertex of a later tree may be joined to an inner vertex of an earlier one, so the individual trees are not Hungarian in $G^*$. The tempting argument "each tree is Hungarian, so apply the tree lemma tree by tree" therefore fails. Only the ordered condition, applied in both directions as in 6.4, shows that the outer vertices of all trees together are adjacent only to inner vertices. Moving between $G$ and $G^*$ requires lifting matchings through nested blossoms, which means an induction over the nesting rather than over a single odd circuit.

Formalization scope

Graphs are the published EdmondsMatching65.Polyhedron.Graph V E: finite vertex and edge types, an unordered pair of distinct ends for each edge, parallel edges allowed. Matchings are its IsMatching, and "maximum" means maximum cardinality. A matching of a subgraph is a matching of $G$ contained in the subgraph's edges. Paths are not needed.

Shrinking is contraction along a Finpartition of the vertex set. The vertices of $G^*$ are the parts, and the edges of $G^*$ are the edges of $G$ joining different parts. Blossom sets are an inductive predicate recording the nested odd circuits directly; there is no tower of types.

The output of 6.0 is the structure Config60. It records exactly the invariants the construction establishes and nothing more, and the goal is stated for every such configuration. The configuration must not be weakened. Dropping density, the ordered Hungarian condition, the outerness of pseudovertices or the blossom condition on the parts makes (a) or (b) false. Taking the $J_i$ to be arbitrary trees, or $\mathcal P$ an arbitrary partition, would state a different and false theorem. The goal is not vacuous: exists_config_6_0 asserts that a configuration exists for every maximum matching. Shrinking is defined in 4.9 only for connected sets, so the forest form of 4.15 assumes connected parts.

Welcome contributions: the general theory of alternating trees and Hungarian forests (4.2, 4.17 and their forest forms), the lifting lemma 4.14 for nested odd circuits, and a proof of exists_config_6_0.

Selected references

• J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
• T. Gallai, Kritische Graphen II, Publ. Math. Inst. Hungar. Acad. Sci. 8 (1963), 373–395; Maximale Systeme unabhängiger Kanten, ibid. 9 (1964), 401–413.
• L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986 (reprinted AMS Chelsea, 2009). https://doi.org/10.1090/chel/367
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 24.

Motivation

The core of an exchange economy is the set of allocations that no group of consumers can improve upon by trading only among themselves. The Walras equilibria (competitive equilibria) are the allocations supported by a price system at which every consumer maximizes preference on a budget set. Every Walras equilibrium is in the core, but for a fixed finite economy the core is usually much larger. Edgeworth (1881) conjectured that the core shrinks to the competitive allocations as the number of traders grows; Debreu and Scarf (1963) proved this for replica economies, and Aumann (1964) proved exact equality for an atomless continuum of traders.

Jean-Pierre Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6 (1981) 1–13) gives a third route to the same conclusion, with a fixed finite number of consumers. Coalitions are allowed to be fuzzy: a consumer may join with any rate of participation between 0 and 1. Once all fuzzy coalitions may block, the core of the economy, now called the fuzzy core, is exactly the set of Walras equilibria (Theorem 4.1, p. 6). The paper presents this as a slight modification of the Debreu–Scarf theorem; in Remark 4.2 it observes that Debreu–Scarf's replica coalitions correspond to the rational points of the cube $[0,1]^n$.

This mission formalizes §4 of the paper. It is the fourth mission of a series on the paper; the others treat the cores of fuzzy games with and without side payments and the values of smooth fuzzy games.

Setting

There are $n$ consumers $i \in N = \{1,\dots,n\}$ and $l$ commodities. Consumer $i$ consumes bundles in $\mathbb{R}^l_+$, ranks them by a preference relation $\succcurlyeq_i$ (with strict part $\succ_i$), and owns a set $Y(i) \subset \mathbb{R}^l$ of possible initial endowments. Each $Y(i)$ is closed, convex and comprehensive: whenever $y \in Y(i)$ and $z \ge 0$, also $y - z \in Y(i)$.

A fuzzy coalition is a vector $\tau \in [0,1]^n$; $\tau_i$ is the rate at which consumer $i$ participates, and $A_\tau = \{i : \tau_i > 0\}$ is the set of participants. The coalition $\tau$ disposes of the endowments

$$Y(\tau) = \sum_{i \in N} \tau_i\, Y(i),$$

and its allocations are the families $x_\tau = (x_\tau^i)_{i \in A_\tau}$ of bundles $x_\tau^i \in \mathbb{R}^l_+$ with $\sum_i \tau_i x_\tau^i \in Y(\tau)$; this set is $X(\tau)$. The allocations of the whole economy are $X(N) = X(\tau^N)$, $\tau^N = (1,\dots,1)$.

An allocation $x \in X(N)$ is in the fuzzy core if there is no nonzero fuzzy coalition $\tau$ and allocation $x_\tau \in X(\tau)$ with $x_\tau^i \succ_i x^i$ for every $i \in A_\tau$.

The income of consumer $i$ at prices $p \in \mathbb{R}^l$ is $r_i(p) = \sup_{y \in Y(i)} p\cdot y$, and the budget set is $B_i(p) = \{x \in \mathbb{R}^l_+ : p \cdot x \le r_i(p)\}$. An allocation $\bar x \in X(N)$ is a Walras equilibrium if some price $\bar p \in \mathbb{R}^l$ satisfies, for every $i$,

$$\bar p \cdot \bar x^i = r_i(\bar p) \qquad\text{and}\qquad \bar x^i \succcurlyeq_i x \ \text{ for all } x \in B_i(\bar p).$$

Assumption (1) of §4 requires each preference to be continuous and convex, with $x \succ_i y \Rightarrow \alpha x + (1-\alpha) y \succ_i y$ for $\alpha \in\, ]0,1[$; no consumer to be satiated; and each $Y(i)$ to contain a vector with all coordinates strictly positive.

Formalization targets

Goal: Theorem 4.1

Under assumption (1),

$$\text{fuzzy core} \;=\; \{\text{Walras equilibria}\}.$$

Milestones, from the proof of Theorem 4.1

1. Every Walras equilibrium belongs to the fuzzy core.
2. For an allocation $\bar x \in X(N)$, each set $Q(i) = Y(i) - \{x \in \mathbb{R}^l_+ : x \succ_i \bar x^i\}$ is nonempty.
3. If $\bar x$ belongs to the fuzzy core, then

$$0 \notin \operatorname{co}\Big(\bigcup_{i=1}^n Q(i)\Big).$$

The remaining step of the paper, from milestone 3 to the existence of the equilibrium price, is stated there only as "by known arguments" and is left to the solver as part of the goal.

Significance

The result. Theorem 4.1 is a core equivalence theorem for an economy with finitely many consumers and no replication or continuum of traders. It identifies the competitive allocations as exactly the allocations that are stable against partial coalitions. It also makes visible which coalitions matter: Remark 4.1 attributes the equivalence to the fact that all fuzzy coalitions are allowed to form, so that the set of coalitions is convex. The same fuzzy-coalition device underlies the nonemptiness results for cores of fuzzy games in §5–§7 of the paper.

Formalizing it. The theorem is proved in the paper, in one paragraph that defers its final step to "known arguments". To our knowledge neither the theorem nor the Debreu–Scarf or Aumann core equivalence theorems have been formalized in Lean. A complete development provides a reusable model of an exchange economy with preference relations and comprehensive endowment sets, a checked argument from separation to equilibrium prices, and a template for the classical core equivalence theorems.

Difficulty

The inclusion of the Walras equilibria in the fuzzy core is a budget computation. The converse is the content of the theorem: from the mere absence of improving fuzzy coalitions, a single price vector must be produced that works for all consumers simultaneously. Separating consumer by consumer gives one price per consumer, not a common one, so the coalitional structure has to enter before any price exists. Once a candidate price is available, it still has to be shown nonnegative, each equilibrium bundle has to exhaust its owner's income, and no bundle in a budget set may be strictly preferred; each of these uses a different part of assumption (1), and the paper leaves all three to "known arguments". The incomes $r_i(p)$ may be $+\infty$ for prices with negative coordinates, so finiteness at the equilibrium price is part of the conclusion, not an assumption.

Formalization scope

Consumers are Fin n, commodities Fin l; an allocation is a function Fin n → Fin l → ℝ, a price a vector Fin l → ℝ, and $p \cdot y = \sum_k p_k y_k$. A single definitions file (FuzzyGames.Walras.Basic) holds the economy, its assumptions, $Y(\tau)$, $X(\tau)$, the fuzzy core, incomes, budget sets, Walras equilibria and the sets $Q(i)$.

The formalization commits to the following readings, each recorded in the items' Formalization Notes:

• Complete preferences. The paper's "preference preordering" is read, as in Debreu's usage, as a reflexive, transitive and complete relation on $\mathbb{R}^l_+$. The relation is a predicate on $\mathbb{R}^l$, but every assumption and every use is restricted to $\mathbb{R}^l_+$.
• Continuity means closed upper and lower contour sets in $\mathbb{R}^l_+$; convexity means convex upper contour sets, plus the condition of (1)(i).
• Assumption (1)(i) is printed with $x \succcurlyeq y$ in the premise, which fails at $x = y$; it is stated with $x \succ y$.
• Blocking is strict and by nonzero coalitions. The fuzzy-core definition is printed with $x_\tau^i \succcurlyeq x^i$; the proof uses $\succ$, and the weak version would let every allocation block itself. The coalition $\tau = 0$ is excluded, since its condition over $A_\tau = \emptyset$ is vacuous.
• Dummy coordinates. An allocation of $\tau$ is a full family of $n$ bundles; those with $\tau_i = 0$ are multiplied by $0$, unconstrained and never compared.
• $Y(\tau)$ is Mathlib's pointwise Minkowski sum of scaled sets.
• Incomes take values in the extended reals (EReal), so that $r_i(p) = +\infty$ is represented and never replaced by a default value.

A trivializing formalization is ruled out: the assumptions are satisfiable, and a sorry-free check (one consumer, one commodity, $x \succcurlyeq y \iff x \ge y$, $Y(1) = (-\infty, 1]$) verifies them together with a Walras equilibrium, so neither side of the goal is empty by construction.

Contributions welcome: proofs of the milestones, a separation-to-prices lemma for comprehensive endowment sets, and general facts about complete continuous convex preferences on $\mathbb{R}^l_+$, which are reusable for any general equilibrium development.

Selected references

• J.-P. Aubin, Cooperative fuzzy games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• G. Debreu, H. Scarf, A limit theorem on the core of an economy, International Economic Review 4(3) (1963) 235–246. https://doi.org/10.2307/2525290
• R. J. Aumann, Markets with a continuum of traders, Econometrica 32 (1964) 39–50. https://doi.org/10.2307/1913732
• G. Debreu, Theory of Value, Cowles Foundation Monograph 17, Yale University Press, 1959.