Operations Research

Motivation

Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.

Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.

Setting

Fix a finite set of players $\mathcal M$ and, for each player $m$, a finite nonempty strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$, and $p^{-m}$ denotes the strategies of the players other than $m$. A game is a family of utilities $u = (u^m)_m$ with $u^m : E \to \mathbb R$, so the space of games is $\mathcal G_{\mathcal M,E} \cong C_0^{\mathcal M}$, where $C_0 = \{E \to \mathbb R\}$ with $\langle \varphi,\psi\rangle_0 = \sum_p \varphi(p)\psi(p)$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function $X : E\times E\to\mathbb R$ that is antisymmetric on edges and zero off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\text{ edge}} X(p,q)Y(p,q)$. Triangular flows $C_2$ live on ordered 3-cliques.

The operators are: the gradient $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator; the curl $(\delta_1X)(p,q,r) = X(p,q)+X(q,r)+X(r,p)$ on 3-cliques; the per-player gradient $(D_m\varphi)(p,q) = W^m(p,q)(\varphi(q)-\varphi(p))$, with $W^m$ the indicator of $m$-comparability; and $D : C_0^{\mathcal M}\to C_1$, $Du = \sum_m D_m u^m$, the flow of pairwise comparisons of $u$. Adjoints are written ${}^*$ and Moore–Penrose pseudoinverses ${}^\dagger$. The space $C_0^{\mathcal M}$ carries the unweighted inner product $\sum_m\langle u^m,v^m\rangle_0$. Further, $\Delta_1 = \delta_1^*\delta_1+\delta_0\delta_0^*$, $\Delta_{0,m} = D_m^*D_m$, $\Pi_m = D_m^\dagger D_m$, and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$.

A game is normalized if $\sum_{p^m} u^m(p^m,p^{-m}) = 0$ for all $p^{-m}$ and $m$ (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)

$$\mathcal P = \{u \mid u = \Pi u,\ Du\in\operatorname{im}\delta_0\},\qquad \mathcal H = \{u \mid u = \Pi u,\ Du\in\ker\delta_0^*\},\qquad \mathcal N = \ker D .$$

Formalization targets

Goal: Theorem 4.1

$$\mathcal G_{\mathcal M,E} = \mathcal P\oplus\mathcal H\oplus\mathcal N,$$

and every game $u$ splits as $u = u_P + u_H + u_N$ with

$$u_P = D^\dagger\delta_0\delta_0^\dagger Du\in\mathcal P,\quad u_H = D^\dagger(I-\delta_0\delta_0^\dagger)Du\in\mathcal H,\quad u_N = (I-D^\dagger D)u\in\mathcal N,$$

where $\varphi = \delta_0^\dagger Du$ is a potential function of $u_P$, i.e. $Du_P = \delta_0\varphi$.

Milestones

1. Theorem 3.1 (Helmholtz decomposition), on an arbitrary finite graph: $C_1 = \operatorname{im}\delta_0\oplus\ker\Delta_1\oplus\operatorname{im}\delta_1^*$, orthogonally, with $\ker\Delta_1 = \ker\delta_1\cap\ker\delta_0^*$.
2. Lemma 4.1: $\Delta_{0,m} = h_m\Pi_m$.
3. Lemma 4.2: $\ker D_m = \ker\Pi_m = \ker\Delta_{0,m}$, with an explicit basis indexed by $E^{-m}$.
4. Lemma 4.4 (i)–(v): $D_m^\dagger = \tfrac1{h_m}D_m^*$; $(\sum_iD_i)^\dagger D_j = (\sum_iD_i^*D_i)^\dagger D_j^*D_j$; $D^\dagger = [D_1^\dagger;\dots;D_M^\dagger]$; $\Pi = D^\dagger D$; $DD^\dagger\delta_0 = \delta_0$.
5. Lemma 4.5: $u$ normalized $\iff$ $\Pi_mu^m = u^m$ for all $m$ $\iff$ $\Pi u = u$ $\iff$ $u\in(\ker D)^\perp$.

Lemma 4.6 (the unique normalized game with the same pairwise comparisons is $\Pi u$) is included as a supporting theorem.

Significance

The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.

Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.

Difficulty

The decomposition is not orthogonal decomposition along a single map. The subspaces $\mathcal P$ and $\mathcal H$ are defined through $\Pi$, which is assembled player by player from the $D_m$, while the flow conditions involve $\delta_0$ and the combined operator $D$. Connecting the two requires the player operators to have mutually orthogonal ranges ($D_k^*D_m = 0$ for $k\ne m$) and the explicit form of $D_m^*D_m$ as a scaled projection. Without these, $\Pi = D^\dagger D$ (Lemma 4.4 (iv)) and $DD^\dagger\delta_0 = \delta_0$ (Lemma 4.4 (v)) are not available, and they are what make the formulas for $u_P$ and $u_H$ land in $\mathcal P$ and $\mathcal H$. A direct attempt to apply the Helmholtz decomposition to $Du$ produces a flow decomposition, not a game decomposition; the pullback through $D$ is not formal, because $D$ is neither injective nor surjective.

Formalization scope

Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and $h_m$ is Fintype.card (E m). Profiles are ∀ m, E m, and $(q^m,p^{-m})$ is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires $p\ne q$, so the graph has no loops, as the Laplacian (15) requires. $C_0$ is EuclideanSpace ℝ on profiles. $C_1$ and $C_2$ are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor $\tfrac12$ on $C_1$. Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of $C_0$, whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im}L$.

$\mathcal P$, $\mathcal H$ and $\mathcal N$ are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing $E^m = \{1,\dots,h_m\}$.

Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, $L^\dagger L$ is the projection onto $(\ker L)^\perp$, invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical Ranking and Combinatorial Hodge Theory, Mathematical Programming 127:203–244, 2011. https://arxiv.org/abs/0811.1067
• R. Penrose, A generalized inverse for matrices, Mathematical Proceedings of the Cambridge Philosophical Society 51(3):406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Firms that buy from unreliable suppliers have two broad ways to protect themselves against supply disruptions: dual sourcing, which splits the order between two suppliers so that a shortfall at one is cushioned by the other, and process improvement, which invests in a supplier's operations so that it fails less often. Wang, Gilland and Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement? (M&SOM 12(3):489–510, 2010), compare the two in a single-period model in which the uncertainty is in the supplier's capacity, not in a proportional yield.

Real supply bases are rarely symmetric. Suppliers differ in cost, reliability and capacity because of their history or location, and the paper (p. 501) cites evidence that global sourcing has widened those differences. This mission formalizes the paper's analytical answer to one question this raises: as two otherwise identical suppliers drift apart in unit cost, which strategy gains? The paper's answer (Theorem 7, p. 502) is that the advantage of single sourcing with improvement over dual sourcing grows with the cost gap.

Setting

A firm sells one product over one season with unit revenue $r$, salvage value $v$ and penalty $p$ per unit of unmet demand; demand $X \ge 0$ has a known law with finite mean. Supplier $i \in \{1, 2\}$ has unit cost $c_i$, committed-cost fraction $\eta_i \in [0, 1]$ and design capacity $K_i > 0$. Its realized capacity loss $\xi_i \ge 0$ has a continuous distribution $G_i(\cdot, a_i)$ indexed by a reliability index $a_i$; a larger index means a stochastically smaller loss: $a \le a'$ implies $G_i(t, a) \le G_i(t, a')$ for all $t$. Losses are independent of each other and of demand.

An order $q_i \ge 0$ delivers $y_i = \min\{q_i, (K_i - \xi_i)^+\}$ and costs $(\eta_i q_i + (1 - \eta_i) y_i) c_i$. The realized profit is

$$\pi(q) = -\sum_i (\eta_i q_i + (1-\eta_i) y_i) c_i + r\min\Big\{x, \sum_i y_i\Big\} + v\Big(\sum_i y_i - x\Big)^+ - p\Big(x - \sum_i y_i\Big)^+,$$

the second-stage expected profit is $\Pi_2(q; a) = \mathbb E[\pi(q)]$, and $\Pi_2^*(a) = \sup_{q \ge 0}\Pi_2(q; a)$.

• Dual sourcing (DS) orders from both suppliers at their initial indices: $\Pi^*_{DS} = \Pi_2^*(a_1^0, a_2^0)$.
• Single sourcing with improvement (SSI) commits to one supplier $i$, spends $m_i z_i(a)$ to try to raise its index to $a \ge a_i^0$ (success probability $\theta_i$), and orders only from it. With $\Pi_2^*(a_i)$ the single-supplier optimal value, its profit is $\Pi_1(a_i) = -m_i z_i(a_i) + \theta_i \Pi_2^*(a_i) + (1-\theta_i)\Pi_2^*(a_i^0)$ (Eq. (7)), and $\Pi^*_{SSI} = \max_i \sup_{a \ge a_i^0} \Pi_1(a)$.
• Heterogeneity. For suppliers identical except in cost, $c_1 = c - \Delta_c$ and $c_2 = c + \Delta_c$ with $0 \le \Delta_c < c$; $\Delta_c$ is the cost heterogeneity parameter. The committed-cost parameter $\Delta_\eta$ is defined in the same way.

In Lean these objects are MitigateSupplyRisk.Heterogeneity.Model (with Pi2, Pi2star, PiDS, Pi1single, PiSSI, Pi1) and SymData (with costModel Δ and etaModel Δ).

Formalization targets

Goal: Theorem 7 (p. 502)

For suppliers identical except in unit cost,

$$\Delta_c \mapsto \Pi^*_{SSI}(\Delta_c) - \Pi^*_{DS}(\Delta_c) \quad\text{is nondecreasing on } [0, c).$$

The statement fixes no parameter values and no particular distribution; it asserts only the direction of the effect.

Milestones

1. Theorem 6(a) (p. 501): $\Pi^*_{SSI}$ is nondecreasing in $\Delta_c$ on $[0, c)$ and in $\Delta_\eta$ on $[0, \min\{\eta, 1-\eta\}]$.
2. Theorem 6(b) (p. 501): $\Pi^*_{DS}$ is nondecreasing in $\Delta_c$ and in $\Delta_\eta$ on the same ranges.
3. Lemma 5 (p. 504): the combined-strategy profit $\Pi_1(a)$ of Eq. (5), which improves one or both suppliers before dual sourcing, is submodular on $[a_1^0, \infty) \times [a_2^0, \infty)$:

$$\Pi_1(a \vee b) + \Pi_1(a \wedge b) \le \Pi_1(a) + \Pi_1(b).$$

Significance

Theorem 7 turns a strategy comparison into a comparative-statics statement: once SSI is preferred at some cost gap, it stays preferred at every larger gap, so the preference switches at most once along a cost-heterogeneity path. Theorem 6 shows separately that both strategies benefit from heterogeneity, which is immediate for a single-sourcing strategy but not for dual sourcing, where one supplier improves and the other deteriorates. Lemma 5 is the structural fact the paper uses for the combined strategy: improvement efforts at the two suppliers are substitutes.

The results are proved in the paper's online appendix, which this formalization does not use. To our knowledge none of them has a machine-checked proof. A formal development would supply reusable pieces: an expected-profit model for random capacity with integrable profits, envelope and convexity arguments for suprema of affine families, and monotone comparative statics for single- and dual-supplier newsvendor problems.

Difficulty

$\Pi^*_{SSI}$ and $\Pi^*_{DS}$ are both nondecreasing in $\Delta_c$ (Theorem 6), so the goal compares the growth rates of two optimal values. Neither has a closed form. Both are suprema of families affine in $\Delta_c$, so they are convex but may have kinks, and an optimal improvement level need not exist when the index set $[a^0, \infty)$ is unbounded. The comparison concerns orders at different cost levels and under different strategies, so it needs a link between the dual-sourcing order from the cheaper supplier and the single-sourcing order and its response to improvement. Evaluating each side at a fixed optimizer does not give it, because the two optimizers move with $\Delta_c$. For Lemma 5, submodularity of $\Pi_2(q; a)$ in $a$ for each fixed $q$ does not pass to the supremum over $q$ by itself.

Formalization scope

• Representation. Suppliers are indexed by Fin 2. Each $G_i(\cdot, a)$ is the cdf of a measure ν i a on ℝ. Expectations are Bochner integrals against the product of the two loss laws and the demand law. The integrand is bounded by a constant times $1 + |x|$, so the integrals are genuine.
• Optimal values. Optimal values are real suprema over $q \ge 0$ and $a \ge a_i^0$. Under the standing assumptions every such set is nonempty and bounded above by $(r + |v|)(K_1 + K_2)$, so no supremum takes Lean's default value. $\Pi^*_{SSI}$ is the early-commitment value and maximizes over the choice of supplier; it does not fix supplier 1.
• Standing assumptions (fields of Model.Standing and SymData.Standing):
  • the demand is a probability law on $[0, \infty)$ with finite mean;
  • each loss law is a continuous probability law on $[0, \infty)$, stochastically decreasing in the index;
  • $\eta_i \in [0, 1]$, $K_i > 0$, $\theta_i \in [0, 1]$, $m_i \ge 0$;
  • $z_i$ is convex and nondecreasing on $[a_i^0, \infty)$ with $z_i(a_i^0) = 0$.
• Disclosed readings.
  • $r \ge 0$, $p \ge 0$ and $c_i \ge 0$ ($c > 0$ in the heterogeneity statements, so that $c_1 > 0$) are the paper's readings of revenue, penalty and cost.
  • $v < r + p$ is implicit in the paper's Eq. (2), which divides by $r + p - v$.
  • The effort function $z_i(a)$ is taken as the primitive, as on p. 493. This presumes that every index $a \ge a_i^0$ is reachable.
  • $\Delta_\eta$ ranges over $[0, \min\{\eta, 1-\eta\}]$, the reading of "analogously" (p. 501) that keeps both committed costs in $[0, 1]$.
• Weak monotonicity. "Increasing" is weak (p. 492) and is stated as MonotoneOn.
• Corrections. No printed slip is corrected in this mission.
• Not formalized. Theorem 7 is stated without $\eta = 0$ and without concavity of $G$ in $a$, as on the page. The $\Delta_K$ and $\Delta_a$ clauses of Theorem 6 are not formalized, because the paper does not pin down how the improvement function depends on an initial index that differs between suppliers. Theorem 8 is also left out.
• Non-trivialization. Both values are recomputed as optimal values of the model at every $\Delta_c$. Defining them by a formula, fixing an optimizer at $\Delta_c = 0$, or hard-coding supplier 1 as the single source would trivialize the goal, and none of these is done.

Contributions are welcome at every level: integrability and boundedness lemmas for $\Pi_2$, convexity of the optimal values in $\Delta$, the symmetry argument behind Theorem 6(b), and monotone comparative statics of single-supplier orders in the reliability index.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• J. Hazra, B. Mahadevan, Impact of supply base heterogeneity in electronic markets, European Journal of Operational Research 174(3):1580–1594, 2006 (cited on p. 501 of the paper for the growth of supply-base heterogeneity).

Motivation

A $T$-join of a graph $G$ is a set of edges $F$ such that exactly the vertices of a prescribed even set $T$ have odd degree in $F$. Minimum $T$-joins are a classical object of combinatorial optimization: they contain shortest paths ($|T|=2$), Chinese postman tours and perfect matchings as special cases, and their duality with $T$-cuts connects them to integral multiflows. Whether the minimum size $\tau(G,T)$ of a $T$-join equals the maximum number $\nu(G,T)$ of disjoint $T$-cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).

Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum $T$-join, motivated by the observation that a minimum $T$-join with few components yields a large integral packing of $T$-cuts. Deciding whether some minimum $T$-join has at most $k$ components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, $k=1$: Theorem 6 characterizes exactly when a minimum $T$-join can be chosen connected, in terms of the shortest-path metric of $G$ restricted to $T$. The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.

Setting

All graphs are finite, simple, undirected and connected. For vertices $x,y$ of $G$, $\mu_G(x,y)$ is the number of edges of a shortest $x$–$y$ path. For $T\subseteq V(G)$, $\mu_G|_T$ is the restriction of $\mu_G$ to pairs of vertices of $T$.

For an edge set $F\subseteq E(G)$, $\deg_F(v)$ is the number of edges of $F$ at $v$; $F$ is a $T$-join if $\deg_F(v)$ is odd exactly when $v\in T$. A minimum $T$-join has the fewest edges among all $T$-joins; a minimal one has no proper subset that is a $T$-join. $V(F)$ is the set of endpoints of edges of $F$; $F$ is connected (a tree) when the graph $(V(F),F)$ is connected (a tree), and $\mu_F$ is the distance in $(V(F),F)$.

An isometry from $(X,\mu)$ to $(Y,\nu)$ is a map $f$ with $\nu(f(x),f(y))=\mu(x,y)$ for all $x,y$. A metric $\mu$ on a finite set $X$ is a tree metric if there is a tree $A$ (unit edge lengths) and an isometry $g$ from $(X,\mu)$ to $A$; the pair $(A,g)$ is a realization. A realization is inclusionwise minimal if no proper subtree of $A$ contains $g(X)$. A tree $A$ is an $S$-join if its vertices of odd degree are exactly those of $S$.

Formalization targets

Goal: Theorem 6

For $G$ connected and $T$ nonempty of even cardinality,

$$\exists\,F\ \text{minimum connected }T\text{-join} \iff \begin{cases}\mu_G|_T \text{ is a tree metric, and for its minimal realization }(A,g),\ T':=g(T):\\ A \text{ is a } T'\text{-join},\\ \exists\,\varphi:V(A)\to V(G)\ \text{isometry with } \varphi(g(t))=t\ (t\in T).\end{cases}$$

The conditions are required of every minimal realization; all of them are isomorphic.

Milestones

1. (p. 389) A minimal $T$-join is the edge-disjoint union of $|T|/2$ paths pairing the vertices of $T$.
2. (p. 391) In every realization of $\mu$, the distance from $g(x)$ to the $g(y)$–$g(z)$ path equals $\tfrac12(\mu(x,y)+\mu(x,z)-\mu(y,z))$.
3. (p. 391) A tree metric has an inclusionwise minimal realization, unique up to an isomorphism respecting the realization maps.
4. (Lemma 2, p. 392) A connected $T$-join $F$ is minimum if and only if $F$ is a tree and $\mu_F=\mu_G$ on $V(F)$.
5. (p. 392) If $A$ is a $T'$-join and $\varphi$ an isometry from $A$ to $G$ extending $g^{-1}$, the image of $A$ under $\varphi$ is a $T$-join that is a tree with $\mu_F=\mu_G$ on $V(F)$.

Significance

Theorem 6 turns the existence of a connected minimum $T$-join, a question about all $T$-joins of $G$, into conditions on the finite metric $\mu_G|_T$ alone plus one isometric embedding of a tree into $G$. Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since $T'$ contains all leaves of $A$. The authors deduce that connected minimum $T$-joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for $k$ components. A consequence stated in the paper: if the minimal realization of $\mu_G|_T$ is not a $T'$-join, then no minimum $T$-join is connected.

The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither $T$-joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.

Difficulty

The central difficulty is in the necessity direction. A connected minimum $T$-join $F$ is itself a minimal realization of $\mu_G|_T$ (Lemma 2), so $F$ satisfies the conditions; but the conditions concern the minimal realization, and transferring them from $F$ to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph $G$.

Formalization scope

• Graphs are SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about $G$ (SimpleGraph.dist is $0$ on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).
• Edge sets are Finset (Sym2 V). Connectivity, the tree property and $\mu_F$ refer to the graph with edge set $F$ induced on $V(F)$, not on all of $V$.
• "Minimum" is "$|F|\le|F'|$ for every $T$-join $F'$", never an infimum over $\mathbb N$.
• A realization is a tree on Fin N together with a map $g:X\to$ Fin N; this avoids quantifying over a universe. A tree metric must satisfy $\mu(x,y)=0\Rightarrow x=y$.
• "The unique minimal realization" is encoded by quantifying over all inclusionwise minimal realizations. A goal that only asks for some minimal realization satisfying the conditions is a different, weaker statement (its necessity half needs no uniqueness) and is not this mission's target.
• $T\neq\emptyset$ is added: for $T=\emptyset$ the minimum $T$-join is empty and its connectivity is only a convention.
• "$f$ is the inverse of $g$ and $\varphi$ extends $f$" is encoded as $\varphi(g(t))=t$. Isometries preserve all distances, not only adjacency.
• Halving and subtraction (milestone 2) are multiplied out.

Reusable beyond this mission: the $T$-join vocabulary, the path decomposition of minimal $T$-joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.

Selected references

• András Sebő, Eric Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• András Sebő, Eric Tannier, Connected joins in graphs, Integer Programming and Combinatorial Optimization (IPCO 2001), Lecture Notes in Computer Science 2081, 383–395, 2001. https://doi.org/10.1007/3-540-45535-3
• Peter Buneman, A note on the metric properties of trees, Journal of Combinatorial Theory, Series B 17:48–50, 1974. https://doi.org/10.1016/0095-8956(74)90047-1
• Paul Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981. https://doi.org/10.1112/plms/s3-42.1.178

Motivation

In a linearly parameterized bandit, the expected rewards of many arms are driven by a small number of unknown parameters. Each arm is a vector $u \in \mathbb R^r$, and its expected reward is the inner product $u'Z$ with an unknown parameter vector $Z$. Problems of this kind arise in marketing and revenue management, where each product is described by $r$ features (price, popularity, …) and the expected revenues of thousands of products are, to a good approximation, linear in a few unknown feature weights. Pulling one arm then reveals information about all of them, and a good policy has to exploit this correlation.

Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, 2010) studied this model with unbounded, sub-Gaussian noise and a prior on $Z$. They proved an $\Omega(r\sqrt T)$ lower bound, a matching policy for smooth arm sets, and the Uncertainty Ellipsoid (UE) policy for arbitrary arm sets. This mission formalizes their Theorem 4.2: when the set of arms is finite, the regret of UE grows like $\log T$, within a constant factor of the Lai–Robbins lower bound for the classical multi-armed bandit (Lai and Robbins, 1985).

Timeline.

• 1985: Lai and Robbins prove that, for independent arms, the regret of any uniformly good policy grows at least like $\log T$, and give policies attaining it.
• 2002: Auer, Cesa-Bianchi and Fischer give the finite-time UCB1 analysis (doi:10.1023/A:1013689704352), whose pull-count argument the UE analysis adapts. Auer, in the same year, studies linear payoffs with confidence bounds (JMLR 3).
• 2010: Rusmevichientong and Tsitsiklis treat unbounded sub-Gaussian noise with an anytime policy (UE), and prove the $\log T$ regret and $\log^2 T$ Bayes-risk bounds for finitely many arms formalized here.

Setting

Let $r \ge 2$ and let $\mathcal U_r \subset \mathbb R^r$ be a finite, nonempty set of arms. Fix $z \in \mathbb R^r$, the value of the unknown parameter. Playing arm $u$ in period $t$ yields the reward $X_t = u'z + W_t$. The noise $W_t$ is drawn afresh in each period from a law $\nu_u$ that depends only on the arm played, independently of the past. A policy chooses the arm $U_{t+1}$ of period $t+1$ as a function of the history $H_t = (U_1, X_1, \dots, U_t, X_t)$. The regret given $Z = z$ is

$$\mathrm{Regret}(z, T, \psi) = \sum_{t=1}^T \mathbb E\Big[\max_{v \in \mathcal U_r} v'z - U_t'z \,\Big|\, Z = z\Big],$$

and for a prior $\mu$ of $Z$ the Bayes risk is $\mathrm{Risk}(T, \psi) = \mathbb E_{Z \sim \mu}[\mathrm{Regret}(Z, T, \psi)]$. The gap of arm $u$ is $\Delta^u(z) = \max_{v \in \mathcal U_r} v'z - u'z$, and $N^u(z, T)$ is the number of periods among the first $T$ in which $u$ is played.

Assumption 1.

• (a) Every $\nu_u$ has mean zero and $\mathbb E[e^{xW}] \le e^{x^2\sigma_0^2/2}$ for all $x$.
• (b) Every arm has norm at most $\bar u$, and $\mathcal U_r$ contains $r$ linearly independent arms $b_1, \dots, b_r$ with $\lambda_{\min}(\sum_k b_kb_k') \ge \lambda_0$.

The UE policy first plays $b_1, \dots, b_r$. It then forms the least squares estimate $\widehat Z_t = C_t\sum_{s\le t}U_sX_s$ with $C_t = (\sum_{s \le t} U_sU_s')^{-1}$, and plays an arm maximizing $v'\widehat Z_t + R^v_t$. The uncertainty radius is

$$R^v_t = \alpha\sqrt{\log t}\sqrt{\min\{r\log t, |\mathcal U_r|\}}\,\sqrt{v'C_tv},$$

with $\alpha = 4\sigma_0\kappa_0^2$ and $\kappa_0 = 2\sqrt{1 + \log(1 + 36\bar u^2/\lambda_0)}$. Ties are broken arbitrarily.

Formalization targets

Goal: Theorem 4.2

There are constants $a_6, a_7 > 0$ depending only on $\sigma_0, \bar u, \lambda_0$ such that for all $T \ge r+1$ and $z$,

$$\mathrm{Regret}(z, T, \mathrm{UE}) \le a_6|\mathcal U_r|\,\|z\| + a_7|\mathcal U_r|\sum_{u \in \mathcal U_r}\min\Big\{\frac{\log T}{\Delta^u(z)}, T\Delta^u(z)\Big\}.$$

If moreover each $\Delta^u(Z)$ has a point mass at $0$ and a density bounded by $M_0$ on $\mathbb R_+$, there are $a_8, a_9 > 0$ depending only on $\sigma_0, \bar u, \lambda_0, M_0$ with

$$\mathrm{Risk}(T, \mathrm{UE}) \le a_8|\mathcal U_r|\,\mathbb E\|Z\| + a_9|\mathcal U_r|^2\log^2 T.$$

The constants are left unspecified, as in the paper. Their existence, uniformly in $r$ and in the arm set, is the content.

Milestones

• Theorem B.1 and Theorem B.2: Chernoff-type deviation bounds for adaptive least squares, with factors $t^{5|\mathcal U_r|}$ and $t^{r\kappa_0^2}$.
• Lemma B.6: the radius $R^u_t$ is exceeded with probability at most $1/t^2$.
• The pull-count bound of App. B.3: $\mathbb E[N^u(z,T)] \le 6 + 4\alpha^2|\mathcal U_r|\log T/\Delta^u(z)^2$ for every suboptimal arm.
• The regret decomposition $\mathrm{Regret} = \sum_u\Delta^u(z)\,\mathbb E[N^u(z,T)]$.
• The risk bound $\mathbb E[\min\{\log T/\Delta^u(Z), T\Delta^u(Z)\}] \le (M_0+1)\log T + M_0\log^2 T$.

Significance

The result. For a fixed finite arm set, Theorem 4.2 shows that a single anytime policy, which does not know $T$, has regret $O(\log T)$ for every parameter and Bayes risk $O(\log^2 T)$. It does this with unbounded noise and correlated arms. The dependence on the problem enters only through the gaps $\Delta^u(z)$ and the number of arms. The companion result for general compact arm sets (Theorem 4.1) gives only $\tilde O(r\sqrt T)$. The finite case shows that the same policy adapts to the easier problem.

Formalizing it. The theorem is proved on paper. As far as is known, it has no machine-checked proof. The platform's finite-armed bandit library (Lattimore–Szepesvári) has the regret decomposition and UCB pull-count bounds for independent arms, e.g. BanditAlgorithm.bandit_regret_decomposition. Those statements live in a different model and do not apply to correlated linear rewards with a least squares estimator. This mission adds:

• self-normalized deviation bounds for adaptively collected least squares estimates, under per-arm sub-Gaussian noise;
• a pull-count analysis that runs through a matrix-valued confidence radius;
• the Bayes-risk integration under a density condition.

Difficulty

The arms are chosen adaptively, so the design matrix $\sum_s U_sU_s'$ is random and depends on the noise. Applied with the realized $C_t$, the classical Chernoff bound for a fixed weighted sum of independent noises is not valid. The obvious union bound over arms does not apply either: the event concerns the random matrix $C_t$, not one arm. In the pull-count bound, the radius of arm $u$ must be controlled through the number of times $u$ was played, although $C_t$ mixes all arms, and the Gram matrix of the other arms may be singular.

Formalization scope

• Space. $\mathbb R^r$ is EuclideanSpace ℝ (Fin r), so $\|\cdot\|$ is Euclidean. The source is arXiv:0812.3465v2; its printed page numbers equal the PDF's.
• Model.
  • The arm set is a finite nonempty Set, and $|\mathcal U_r|$ is its ncard. Theorem B.2 and Lemma B.6, which the paper states for any compact arm set, are stated for compact nonempty arm sets, as printed.
  • The noise is a Markov kernel $u \mapsto \nu_u$.
  • The law of the history given $Z = z$ is built period by period, with fresh noise from $\nu_{U_{t+1}}$. This is the paper's model: noises independent of each other and of $Z$, identically distributed in $t$, mean zero.
  • Policies are deterministic and history-dependent, with measurable selection rules. The paper uses this measurability implicitly.
  • Regret is $T\max_v v'z - \mathbb E[\sum_t U_t'z]$.
  • Assumption 1(a) is an mgf bound written with a lower integral, so the exponential moments are finite. Assumption 1(b) writes $\lambda_{\min} \ge \lambda_0$ as $\lambda_0\|x\|^2 \le \sum_k (b_k'x)^2$.
  • A UE run is any measurable policy that plays $b_1, \dots, b_r$ first and then an arg max of (7). The theorems hold for every tie-breaking rule.
• Constants. They are quantified before $r$, the arm set, the noise, the policy, $T$, $z$ and the prior, so they cannot depend on any of these.
• Corrections and added hypotheses.
  • The pull-count bound is stated for arms with $\Delta^u(z) > 0$. As printed, it divides by a zero gap for an optimal arm.
  • The risk part assumes $\mathbb E\|Z\| < \infty$ and concludes the integrability of the regret.
• Conventions.
  • An optimal arm contributes $\min\{\log T/0, 0\} = 0$, the paper's reading and Lean's value.
  • The density condition says that, on $(0,\infty)$, the law of $\Delta^u(Z)$ is at most $M_0$ times Lebesgue measure.
• No trivializing reading. The regret is never a junk-valued integral that makes the bound free: the integrand is bounded and measurable, and a junk value would only raise the regret. The width $\min\{r\log t, |\mathcal U_r|\}$ uses the true cardinality, so the radius is not zero.
• Contributions welcome. Reusable pieces are the history-measure construction, Chernoff bounds for adaptive designs, and the deviation bounds of Theorems B.1–B.2, which the companion mission on general compact arm sets also needs.

Selected references

• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, arXiv:0812.3465v2, 24 Feb 2010. https://arxiv.org/abs/0812.3465
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• P. Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. H. de la Peña, M. J. Klass, T. L. Lai, Self-normalized processes: exponential inequalities, moment bounds and iterated logarithm laws, Annals of Probability 32, 2004. https://doi.org/10.1214/009117904000000397

Motivation

Firms that buy from unreliable suppliers can protect themselves in two ways: they can spread orders across several suppliers, or they can invest in improving a supplier's reliability, for example through supplier-development programmes or joint process-improvement projects. Wang, Gilland and Tomlin (MSOM 12(3):489–510, 2010) compare the two strategies in a newsvendor model with random supplier capacity.

This mission formalizes one part of that comparison: single sourcing with improvement, in which improvement efforts may fail. The firm must then decide when to choose its supplier. Under early commitment it picks one supplier, invests in it, and buys from it whatever the outcome. Under late commitment it invests in both suppliers, observes which efforts succeeded, and only then buys from the better one. Empirical work on supplier development documents both practices and the reluctance of suppliers whose improvement efforts previously failed (Handfield et al. 2000, as cited by Wang et al. 2010, p. 496; Krause et al. 2007). The question is how much the option to postpone the choice is worth.

Setting

A firm sells a single product over one season. It earns a unit revenue $r\ge 0$, salvages leftovers at $v$, and pays a penalty $p\ge 0$ per unit of unmet demand, with $v<r+p$. Demand $X$ is nonnegative with finite mean.

Supplier $i\in\{1,2\}$ has design capacity $K_i>0$, unit cost $c_i\ge 0$ and committed-cost fraction $\eta_i\in[0,1]$. Its capacity loss $\xi_i\ge 0$ has a continuous distribution $G_i(\cdot,a_i)$ that depends on a reliability index $a_i$; a higher index means a stochastically smaller loss. An order $q_i\ge 0$ delivers $y_i=\min\{q_i,(K_i-\xi_i)^+\}$. The firm pays $(\eta_iq_i+(1-\eta_i)y_i)c_i$, and the realized profit of single sourcing from $i$ is

$$\pi(q_i)=-(\eta_iq_i+(1-\eta_i)y_i)c_i+r\min\{x,y_i\}+v(y_i-x)^+-p(x-y_i)^+ .$$

The second-stage expected profit is $\Pi_2(q_i;a_i)=\mathsf E[\pi(q_i)]$, and $P_i(a_i)=\Pi_2^*(a_i)=\sup_{q_i\ge 0}\Pi_2(q_i;a_i)$ is its optimal value.

Improvement. Supplier $i$ starts at index $a_i^0$. Effort to reach index $a_i\ge a_i^0$ costs $m_iz_i(a_i)$, where $z_i$ is convex and increasing with $z_i(a_i^0)=0$. The effort succeeds with probability $\theta_i$; on failure the index stays at $a_i^0$.

• Early commitment to supplier $i$ yields

$$\Pi_{1i}^E(a_i)=-m_iz_i(a_i)+\theta_iP_i(a_i)+(1-\theta_i)P_i(a_i^0),$$

and $\Pi_1^{*E}=\max_i\sup_{a_i\ge a_i^0}\Pi_{1i}^E(a_i)$.

• Late commitment yields $\Pi_1^L(a_1,a_2)$: the improvement costs, plus, for each of the four success/failure outcomes, its probability times $\max\{P_1(\cdot),P_2(\cdot)\}$ at the realized indices (Eq. (9)). $\Pi_1^{*L}$ is its supremum over $a_1\ge a_1^0$, $a_2\ge a_2^0$.

Formalization targets

Goal: Theorem 5

Let the suppliers be identical except for their unit costs, $c_1\le c_2$, with common $\theta\in(0,1)$, $m$, $z$ and $a^0$, and let $a_2^{*E}$ be an optimal early-commitment index of supplier 2. Then

$$\bigl[P_2(a_2^{*E})-P_1(a_1^0)\bigr]^+>\frac{m\,z(a_2^{*E})}{\theta(1-\theta)}\quad\Longrightarrow\quad\Pi_1^{*L}>\Pi_1^{*E}.$$

Milestones, in the paper's order

1. Lemma 2(b), single-supplier instance: $P_i$ is increasing in the index.
2. Theorem 4(a), cost-only instance: if the suppliers differ only in unit cost, the cheaper one is preferred with and without improvement, so $i^*=j^*$.
3. §4.2.2: late commitment weakly dominates early commitment, $\Pi_1^{*E}\le\Pi_1^{*L}$.
4. Lemma 4: $a_i^{*L}\le a_i^{*E}$, in the form valid for non-unique optimizers.
5. §4.2.2: $\Pi_1^{*L}=\Pi_1^{*E}$ if $P_i(a_i^{*E})<P_j(a_j^0)$ for some $i$.
6. Corollary 3(a): strict superiority of late commitment at $c_1=\hat c_1$ persists for every $c_1\in[\hat c_1,c_2]$.

Significance

The results identify when the flexibility of postponing supplier selection has value. Late commitment never hurts. It has no value when one supplier dominates the other, even after the other's improvement. For suppliers that differ only in cost, Theorem 5 gives a checkable sufficient condition for strict value. The condition weighs the gain from switching in the outcome "the costlier supplier improves, the cheaper one does not", which has probability $\theta(1-\theta)$, against the cost of improving the costlier supplier. Together with Lemma 4 the results say that keeping the choice open lowers the reliability target but can raise expected profit. Corollary 3(a) says this value is easiest to obtain when costs are close.

The paper's proofs are in an online appendix that is not used here, and none of these statements has a machine-checked proof. The mission produces formal versions of the statements, with the hypotheses that the printed versions leave implicit made explicit (see Formalization scope), and invites proofs of them.

Difficulty

The late-commitment profit (9) is a probability-weighted sum of maxima of two optimal-value functions. It is "neither concave nor unimodal" (p. 498), so first-order conditions do not characterize its optimum, and optimizers need not be unique.

• Order of the arguments. The comparison results rest on the monotonicity of $P_i$ (Lemma 2(b)). That is a statement about a supremum of expectations under a stochastically ordered family of capacity-loss laws, and must be established before the first-stage results can use it.
• Theorem 5 and Corollary 3(a) compare two suprema, neither of which is assumed to be attained. Strictness has to survive passing to the supremum.
• Corollary 3(a) is a comparative-statics statement in $c_1$. Both $\Pi_1^{*L}$ and $\Pi_1^{*E}$ decrease as $c_1$ grows, so nothing pointwise orders their difference.

Formalization scope

Everything is in the namespace MitigateSupplyRisk.LateCommit, with one definition module Model.

• Model. The demand law is a probability measure $\mu$ on $\mathbb R$ with $\mu(-\infty,0)=0$ and finite mean; no density is assumed. Capacity losses are a family $a\mapsto\nu_a$ of atomless probability measures on $[0,\infty)$, ordered by $\nu_a(-\infty,t]\le\nu_{a'}(-\infty,t]$ for $a\le a'$. Loss and demand are independent (a product measure).
• Optimal values. $\Pi_2$ is the Bochner integral of the realized profit (1). Every optimal value is a sSup over the feasible set. The sign conventions $r,p,c_i\ge 0$, $v<r+p$ make these sets bounded above, so no supremum is a junk value, and no optimum is assumed to be attained.
• Effort. The effort function $z$ is taken as the primitive on $[a^0,\infty)$, which presumes that every index is reachable.
• Identical suppliers. "Identical except for unit costs" means that the two suppliers share the same Supplier record (committed cost, capacity, loss family) and the same Improvement record ($a^0,\theta,m,z$).
• Notation in (9). The paper writes $\Pi_2^*$ for both suppliers in (9); the Lean writes $P_1$ and $P_2$.
• Added or reread hypotheses:
  • Theorem 5 assumes $0<\theta<1$. The printed condition divides by $\theta(1-\theta)$, and Lean's $x/0=0$ would otherwise turn it into $[\cdot]^+>0$, under which the conclusion is false at $\theta=1$.
  • Lemma 4 is stated for arbitrary maximizers: $\max\{a_i^L,a_i^E\}$ is again an early maximizer. This reduces to the printed inequality when the early optimizer is unique.
  • Lemma 2(b) and Theorem 4(a) are the single-supplier and cost-only instances of the paper's statements.
  • Optimizers $a_i^{*E}$ appear as hypotheses (IsMaxOn), never as claims.
• Not trivially true. A statement in which $\Pi_1^{*L}$ or $\Pi_1^{*E}$ is a junk supremum, or in which Theorem 5's condition degenerates at $\theta\in\{0,1\}$, would be trivially true or false; the bounded feasible sets and the hypothesis $0<\theta<1$ exclude both.
• Not formalized: Theorem 4 for other attributes and Theorem 4(b), Lemma 3, and Corollary 3(b), whose printed form needs hypotheses the page does not pin.

Proofs of the milestones are welcome. A reusable lemma, that the supremum of expectations is monotone under first-order stochastic dominance of the loss, would serve the other missions of this series too.

Selected references

• Y. Wang, W. Gilland, B. Tomlin, Mitigating Supply Risk: Dual Sourcing or Process Improvement?, Manufacturing & Service Operations Management 12(3):489–510, 2010. https://doi.org/10.1287/msom.1090.0279
• R. B. Handfield, D. R. Krause, T. V. Scannell, R. M. Monczka, Avoid the pitfalls in supplier development, Sloan Management Review, 2000, pp. 37–49 (cited from the reference list of Wang et al. 2010, https://doi.org/10.1287/msom.1090.0279).
• D. R. Krause, R. B. Handfield, B. B. Tyler, The relationships between supplier development, commitment, social capital accumulation and performance improvement, Journal of Operations Management 25(2):528–545, 2007. https://doi.org/10.1016/j.jom.2006.05.007
• B. Tomlin, On the value of mitigation and contingency strategies for managing supply chain disruption risks, Management Science 52(5):639–657, 2006. https://doi.org/10.1287/mnsc.1060.0515

Motivation

Let $G$ be a connected graph and $T$ a set of vertices of even cardinality. A $T$-join is a set of edges $F$ in which exactly the vertices of $T$ have odd degree. A $T$-cut is a cut $\delta(X)$ with $|X\cap T|$ odd. Write $\tau(G,T)$ for the minimum size of a $T$-join and $\nu(G,T)$ for the maximum number of pairwise disjoint $T$-cuts. Every $T$-cut meets every $T$-join, so $\nu(G,T)\le\tau(G,T)$. When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all $T$ in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.

Korach and Penn (1992) proved that a minimum $T$-join $F$ with $k$ connected components satisfies

$$\tau(G,T)-k+1\ \le\ \nu(G,T)\ \le\ |F|.$$

So a minimum $T$-join with few components certifies a large packing of $T$-cuts, and a connected one certifies $\nu=\tau$. Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given $G$, $T$ and an integer $k$, is there a minimum $T$-join with at most $k$ connected components? They show it can be solved in polynomial time for $k=1$ and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.

Setting

Three-dimensional matching. An instance consists of three pairwise disjoint sets $W$, $X$, $Y$, each of cardinality $q$, and a set of triples $H\subseteq W\times X\times Y$. A matching is a subset $M\subseteq H$ in which every element of $W\cup X\cup Y$ occurs in exactly one triple.

The graph $G$. Take a further set $Z$ of $q$ points and put $T:=W\cup X\cup Y\cup Z$, so $|T|=4q$. The graph $G$ has as vertices the points of $T$, the triples of $H$, and one new vertex $p_{ab}$ for every unordered pair $\{a,b\}$ of distinct points of $T$. Its edges are:

1. $a\,p_{ab}$ and $p_{ab}\,b$ for every such pair, so any two points of $T$ are joined by a path of length 2;
2. $hw$, $hx$, $hy$ and $hz$ for every $h=(w,x,y)\in H$ and every $z\in Z$.

There are no other edges. In Lean, $G$ is gadget q H and $T$ is gadgetT q H.

$T$-joins and components. For $F\subseteq E(G)$ and a vertex $v$, $\deg_F(v)$ is the number of edges of $F$ at $v$. $F$ is a $T$-join (IsTJoin) if $\deg_F(v)$ is odd exactly for $v\in T$. It is a minimum $T$-join (IsMinTJoin) if no $T$-join of $G$ is smaller. The connected components of $F$ are those of the graph $(V(F),F)$, where $V(F)$ is the set of endpoints of edges of $F$. Their number is numComponents F.

Formalization targets

Goal: the Claim in the proof of Theorem 5 (p. 391)

$$\exists\,F \text{ minimum } T\text{-join of } G \text{ with at most } q \text{ components}\quad\iff\quad \exists\,M\subseteq H \text{ a matching.}$$

This statement is quantified over every $q$ and every $H$, and it is the full mathematical content of the reduction.

Milestones (p. 391, in the order the proof uses them)

1. Every $T$-join $F$ of $G$ has $|F|\ge 4q$, with equality iff each $t\in T$ lies in exactly one edge of $F$.
2. If $M$ is a matching, $Z$ can be indexed as $\{z_m: m\in M\}$, and for every such indexing $\bigcup_{m=(w,x,y)\in M}\{mw,mx,my,mz_m\}$ is a minimum $T$-join with exactly $q$ components.
3. Every minimum $T$-join $F$ has $|F|=4q$, and each $t\in T$ lies in exactly one edge of $F$.
4. Every minimum $T$-join has at least $q$ components. It has exactly $q$ iff each component contains a vertex of $H$ and exactly one vertex of each of $W$, $X$ and $Y$.

Significance

The result. The Claim shows that minimizing the number of components of a minimum $T$-join is NP-hard. A Korach–Penn certificate for a large packing of $T$-cuts therefore cannot in general be found by optimizing the component count. This sets the $k=1$ case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.

Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no $T$-join library. The mission produces a reusable vocabulary for $T$-joins, minimum $T$-joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.

Difficulty

The direction from a matching to a $T$-join is a direct verification. The converse has to control an arbitrary minimum $T$-join: its size, the shape of each of its components, and how the components meet $W$, $X$ and $Y$. A first reading of the printed proof suggests that every vertex outside $T$ that carries edges of $F$ is adjacent to at most one vertex of each of $W$, $X$, $Y$. This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of $T$, including pairs inside $W$. Such components really occur in minimum $T$-joins, so the count of components has to cover them as well. The stated conclusion (at least $q$ components, with equality only in the matching-like configuration) remains true.

On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.

Formalization scope

• 3DM. $W$, $X$, $Y$ are three copies of $\{0,\dots,q-1\}$ (Fin q), so their disjointness holds by construction. $H$ and $M$ are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of $M$, and $M\subseteq H$ is a separate hypothesis. A covering-only or at-most-one version would be a different problem.
• The graph. Its vertex type has three kinds of vertices: $T$-vertices $(i,j)$ with class $i\in\{0,1,2,3\}$ ($W,X,Y,Z$), one midpoint per non-diagonal unordered pair of $T$-vertices, and one vertex per element of $H$. The adjacency is exactly the two bullets of p. 390. The graph is fixed by the definition, not described by properties.
• $T$-joins. Edges are unordered pairs (Sym2) and $F$ is a Finset of edges of $G$. Parity uses $\deg_F$. Minimality is "$|F|\le|F'|$ for all $T$-joins $F'$", never an infimum on $\mathbb N$.
• Components. A component of $F$ is a component of the graph with edge set $F$ that contains an endpoint of an edge of $F$. Isolated vertices are never counted, and the empty edge set has $0$ components.
• The degenerate case $q=0$ is included: the graph is empty, $F=\emptyset$ is a minimum $T$-join with $0$ components, and $M=\emptyset$ is a matching.
• Not formalized. Membership of MTSC in NP, polynomial-time computability of the construction, and NP-completeness itself. The platform has no complexity-theory substrate. The Claim is the mathematical statement those rest on.
• Ruled out. The Claim must not be weakened to "exactly $q$ components" or to minimality among $T$-joins with few components, and components must not be counted on the whole vertex type. Each of these changes the statement.

Contributions welcome: proofs of the milestones, general lemmas on $T$-joins (a $T$-join in a graph where $T$ is independent has at least $|T|$ edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.

Selected references

• A. Sebő, E. Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• E. Korach, M. Penn, Tight integral duality gap in the Chinese postman problem, Mathematical Programming 55:183–191, 1992.
• P. D. Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981.
• M. Middendorf, F. Pfeiffer, On the complexity of the edge-disjoint path problem, Combinatorica (cited by Sebő and Tannier as 1998, vol. 8, pp. 103–116) — NP-completeness of deciding $\nu=\tau$.
• M. R. Garey, D. S. Johnson, Computers and Intractability, W. H. Freeman, San Francisco, 1979 — NP-completeness of 3DM.
• A. Frank, A survey on T-joins, T-cuts, and conservative weightings, in Combinatorics, Paul Erdős is Eighty, Vol. 2, 1996, pp. 213–252.
• Related platform item, not reused: UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set $H$ with "exactly one".