Optimization

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (BertsekasSSPModel). Operators

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$-stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
• D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).

This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.

Setting

Let $X$ be a real normed space and $K\subseteq X$ a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.

When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets

These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).

For two convex sets $K_1,K_2$, Eidelheit separation means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.

Formalization targets

Gauge and geometric Hahn--Banach milestones

Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that

This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).

Supporting hyperplanes and convex-set separation

For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:

These are Theorems 2 and 3 of §5.12 (pp. 133--134).

Convex minimum-distance duality

Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and

Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).

Significance

The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.

Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.

Difficulty

A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.

Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.

Formalization scope

The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.

The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. Public scan.

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.

Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is

with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$,

and the volume contracts:

. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.

Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.

How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.

Every linear programming problem has a shadow. To the primal $\min c'x$ we associate the dual $\max p'b$, whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality $p'b \le c'x$ for any primal-feasible $x$ and dual-feasible $p$ (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible $x, p$ with $p'b = c'x$ are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible $x$ and $p$ are simultaneously optimal if and only if $p_i(a_i'x - b_i) = 0$ for all $i$ and $(c_j - p'A_j)x_j = 0$ for all $j$ — the certificate structure behind the dual simplex method and every LP optimality check.

How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem $\min c'x$ subject to $Ax = b$, $x \ge 0$ has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs

measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ($\bar{c} \ge 0$ implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction $d$ satisfying $Ad = 0$, $d \ge 0$, $c'd < 0$ certifying optimal cost $-\infty$. The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.

Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.

Motivation

In industries built on a key component sold by one dominant supplier, such as smartphone chipsets, the supplier's contract terms shape how much its downstream customers innovate. Some suppliers require their customers to cross-license their own patents to each other as a condition of buying the component, so that each manufacturer's innovation also improves its rival's product. Wang, Huang and Lee (SSRN 3053682; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2019.0477) ask when a supplier facing two manufacturers of unequal innovation ability benefits from imposing cross-licensing. Their answer runs through the equilibrium of the manufacturers' innovation game, which is the subject of this mission: Proposition 2 describes how much each manufacturer innovates and shows that the supplier never ends up selling to a single manufacturer.

Setting

A supplier sells a component at wholesale price $r \ge 0$ to manufacturers $M_1$ and $M_2$. Manufacturer $M_i$ chooses a quality improvement $T_i \ge 0$ at cost $k_iT_i^2$. With cross-licensing of effectiveness $\beta \in [0, 1]$, the quality improvement of $M_i$ is $T_i + \beta T_j$ ($j \ne i$), and its inverse demand is $p_i = 1 + T_i + \beta T_j - q_i - q_j$. The standing assumptions are

so $M_2$ is the superior manufacturer. The game has three stages.

1. Quantities. Given $(T_1, T_2)$ and $r$, each $M_i$ chooses $q_i \ge 0$ to maximize $\Pi_i = (1 + T_i + \beta T_j - q_i - q_j - r)q_i$ (display (1)). The equilibrium quantities, display (2), are a duopoly when $r$ is low and a monopoly of the manufacturer with the higher quality when $r$ is higher.
2. Price. The supplier chooses $r \ge 0$ to maximize $r(q_1 + q_2)$. Its price $r^*(T_1, T_2)$ is the least maximizer. Lemma 1 computes it: the supplier induces a duopoly exactly when $\beta \ge \sqrt3 - 1$ or $T_2 \le \hat T_2(T_1\mid\beta)$, where

3. Innovation. Each $M_i$ chooses $T_i \ge 0$ to maximize $\Pi^*_i(T_1, T_2\mid\beta) - k_iT_i^2$, where $\Pi^*_i$ is its Cournot profit at the supplier's price. An innovation equilibrium is a pure Nash equilibrium of this game.

The proof of Proposition 2 defines two candidate profiles in closed form: the interior candidate $T^I = (T^I_1, T^I_2)$, which solves both manufacturers' first-order conditions, and the boundary candidate $T^B = (T^B_1, T^B_2)$, where $M_2$ invests exactly up to $\hat T_2$. A threshold $\hat k_2(k_1\mid\beta)$ separates them, and $T^*(\beta) = T^B$ if $k_2 < \hat k_2(k_1\mid\beta)$, $T^*(\beta) = T^I$ otherwise.

Formalization targets

Goal: Proposition 2 (p. 12)

Under the standing assumptions:

1. every innovation equilibrium is a duopoly, meaning both manufacturers sell a positive quantity at the supplier's price;
2. $T^*(\beta)$ is an innovation equilibrium and a duopoly;
3. if $k_2 < \hat k_2(k_1\mid\beta)$, then $\beta < \sqrt3 - 1$ and $M_2$ is on the boundary:

4. if $k_2 \ge \hat k_2(k_1\mid\beta)$, then $T^*(\beta) = T^I$ and both duopoly first-order conditions hold at $T^*(\beta)$.

Milestones

• display (2): the Cournot quantities are the unique equilibrium of the quantity game;
• Lemma 1: the supplier's price, the regime, its optimal profit, and the gross profits $\Pi^*_1, \Pi^*_2$;
• monopoly infeasibility at $T_1 = 0$, from the proof (p. A.1): $M_2$'s monopoly optimum $1/(16k_2 - 1)$ lies below $\hat T_2(0\mid\beta)$;
• $T^I$ is the unique solution of the two first-order conditions (p. A.1);
• $T^B_2 = \hat T_2(T^B_1\mid\beta)$, and $T^B_1$ is $M_1$'s best response to $T^B_2$ (p. A.1);
• $\hat k_2$ is where $T^I_2 = T^B_2$, and above it $T^I$ lies in the duopoly region (p. A.2);
• $\hat k_2(k_1\mid\beta)$ is strictly decreasing in $\beta$ with $\hat k_2(k_1\mid 1) = 0$ (p. A.2), so the boundary region shrinks to empty as $\beta$ grows.

Significance

Proposition 2 is the paper's equilibrium characterization. Proposition 3 is its instance $\beta = 0$ (no cross-licensing), and Proposition 4 compares the supplier's equilibrium profits with and without cross-licensing on the closed forms $T^B$, $T^I$ and $\hat k_2$ established here. The economic content is that, under cross-licensing, the supplier always ends up selling to both manufacturers. When the superior manufacturer's cost advantage is large it caps its own innovation exactly where the supplier stops preferring a monopoly.

The paper's proof states the closed forms and asserts the checks ("one can obtain", "we verify"). This mission produces a machine-checked version: a complete definition of the three-stage game, with the supplier's price defined as an optimization rather than by its solution, and the equilibrium claims stated against that game. To our knowledge no part of this result has been formalized before.

Difficulty

The innovation payoff of the superior manufacturer is discontinuous. When $T_2$ moves just above $\hat T_2(T_1\mid\beta)$, the supplier switches from a duopoly price to a monopoly price, and $M_2$'s gross profit jumps down. A first-order argument therefore does not show that $T^*$ is an equilibrium. One must also show that $M_2$ never gains by moving into the monopoly region, and that $M_1$ never gains by deviating above $T_2$, where $M_1$ itself becomes the potential monopolist. The boundary candidate is an equilibrium only because the supplier breaks its indifference at the boundary toward the duopoly.

Part 1 quantifies over every equilibrium, not only $T^*$. The paper checks monopoly infeasibility only at $T_1 = 0$, so the general case needs its own argument. The equilibrium is not unique: for some parameters a mirrored profile with $M_1$ at its own boundary is also an equilibrium. Uniqueness is therefore not claimed. The remaining steps are polynomial and rational inequalities in $(k_1, k_2, \beta)$ involving $\sqrt3$.

Formalization scope

• Parameters $\beta, k_1, k_2$ are real numbers. The standing assumptions $0 \le \beta \le 1$ and $49/144 < k_2 < k_1$ are bundled as Standing β k1 k2.
• Quantities and innovation levels range over $\mathbb R_{\ge 0}$ (NNReal). Equilibria use the published two-player predicate CompetingChains.Cournot.IsPureNash.
• Wholesale prices range over $[0, \infty)$. The paper leaves this implicit, so it is a disclosed addition.
• Display (2) is encoded in symmetric form, with the manufacturer of larger quality as the possible monopolist. The paper prints it for $T_2 \ge T_1$, but deviations in the innovation game reach $T_1 > T_2$.
• The supplier's price is the least maximizer of $r(q_1 + q_2)$ over $r \ge 0$. This is the tie-break Lemma 1 uses at $T_2 = \hat T_2$.
• First-order conditions are stated as derivatives (HasDerivAt … 0) of Lemma 1's duopoly polynomials, because the game payoff is not differentiable at the boundary.
• All closed forms are transcribed as printed, with $\sqrt3$ as Real.sqrt 3. Every denominator is proved nonzero in its regime, never assumed.

Two trivializing formalizations are ruled out. Equilibria are never defined by first-order conditions or by the closed forms, and the supplier's price is never defined by Lemma 1's case rule. Both are theorems here.

The source is the authors' SSRN manuscript (abstract 3053682, version of 2023-04-27); its proofs are in the appendix, pp. A.1–A.9. The paper's equivalent threshold $\hat\beta(k_1, k_2)$ is not formalized. Proofs of any milestone are welcome. Lemma 1 and display (2) are self-contained, and the closed-form milestones need only real-algebraic inequalities with $\sqrt3$.

Selected references

• J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN 3053682, version of 2023-04-27. https://ssrn.com/abstract=3053682
• J. Wang, T. Huang, H. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2019.0477

Motivation

Many consequential decisions, such as lending, hiring or admissions, are made by policies that map an individual's features to a probability of a positive decision. When the policy is published, individuals respond to it: they change their features, at a cost, to raise their chance of a positive decision. Tsirtsis, Tabibian, Khajehnejad, Singla, Schölkopf and Gomez-Rodriguez (arXiv:1905.09239, Management Science 2024) model this as a Stackelberg game and ask which policy maximizes the decision maker's utility once individuals best respond.

In the classical, non-strategic setting, where features do not react to the policy, the optimal policy is a deterministic threshold rule: decide positively exactly when the probability of a good outcome is at least a cost constant $\gamma$ (Corbett-Davies et al., KDD 2017; Valera, Singla and Gomez-Rodriguez, NeurIPS 2018). The paper shows that strategic behaviour breaks this picture. A three-value example in §3 (p. 5) exhibits an instance whose costs satisfy the natural outcome monotonicity condition and whose optimal policy is nevertheless stochastic. This mission formalizes that example.

Setting

There are $m$ feature values $x_1,\dots,x_m$, a feature distribution $P(x)$, an outcome probability $P(y=1\mid x)$, a constant $\gamma\in(0,1)$, and a cost $c(x_i,x_j)\ge0$ of changing from $x_i$ to $x_j$.

• A policy $\pi$ assigns to each feature value a probability $\pi(x)=\pi(d=1\mid x)\in[0,1]$ of a positive decision. The individual benefit is $b(x)=\pi(x)$.
• An individual starting at $x_i$ moves to a best response

with ties broken toward the feature value with the highest $P(y\mid x_j)$ (standing assumption (ii)).

• The strategic utility is

and a policy is optimal if it maximizes $u$ over all policies.

• The non-strategic utility $u_{\mathrm{NS}}(\pi,\gamma)=\sum_x P(x)(P(y=1\mid x)-\gamma)\pi(x)$ is the same quantity when nobody moves.
• A cost is outcome monotonic (p. 6) if improving one's outcome requires increasing effort and worsening it requires none.

The instance of §3 has $x\in\{1,2,3\}$, $\gamma=0.1$, $P(x)=(0.1,0.4,0.5)$, $P(y=1\mid x)=(1.0,0.7,0.4)$ and

row $i$ being the origin. In Lean the feature values $1,2,3$ are Fin 3 indices $0,1,2$; the model lives in the namespace StrategicPolicy.StochasticOpt, with Policies, br, u, uNS, OMCost, StandingI and the instance γ0, p0, q0, c0.

Formalization targets

Goal: the optimal policies of the §3 instance

every optimal policy is non-deterministic, and $u\bigl((1,0.7,0),\gamma\bigr)=0.66$. The paper prints a single optimal policy, $(1,0.7,0)$; the optimum is not unique, and the goal states the exact optimal set, which contains the printed policy and makes the "stochastic" claim a statement about every optimum.

Milestones

1. The instance's cost is outcome monotonic and satisfies standing assumption (i).
2. The non-strategic optimum is unique and equals the threshold policy $(1,1,1)$.
3. Under $\pi^*=(1,0.7,0)$ the individuals at $x=3$ move to $x=2$ and those at $x=2$ move to $x=1$.
4. $u_{\mathrm{NS}}((1,1,1))<u(\pi^*)$ and $u((1,1,1))<u(\pi^*)$: the strategic optimum beats its non-strategic counterpart under either reading of "counterpart".

Significance

The example separates two regimes. Without strategic behaviour the optimum is a deterministic threshold rule; with it, randomization is strictly necessary, even under the cost structure (outcome monotonicity) that the paper later uses to restrict the search for optimal policies to a structured family (Proposition 2, Theorem 3). It is the concrete witness for the paper's claim that "optimal decision policies are not always deterministic threshold rules", and it shows that the outcome monotonic binary policies of Theorem 3 must include fractional values such as $0.7=1-0.3$.

The paper reports the optimum from "a brute force search", that is, numerically. A formal proof replaces the search by an argument valid over the whole continuum $[0,1]^3$, determines the full optimal set rather than one optimizer, and certifies the tie-breaking at both thresholds. No part of this paper has a machine-checked proof that this mission is aware of.

Difficulty

The utility is piecewise linear in $\pi$ but discontinuous: it jumps whenever a best response switches, and the switching surfaces are exactly where the optimum sits. At $\pi(x=2)=0.7$ the individuals at $x=2$ are indifferent between staying and moving to $x=1$, and at $\pi(x=3)=0.4$ those at $x=3$ are indifferent between staying and moving to $x=2$. The optimum is attained only because tie-break (ii) resolves both indifferences upward. Checking finitely many candidate policies proves nothing about the rest of $[0,1]^3$, and a naive concavity or first-order argument does not apply to a discontinuous objective. An upper bound must hold for every policy, across all configurations of best responses.

Formalization scope

• Policies are functions Fin 3 → ℝ with values in $[0,1]$; optimality is IsMaxOn u (Policies 3) π, over the whole cube, never over a grid or over deterministic policies.
• The best response br is computed from $\pi$, $c$ and $P(y\mid x)$ as the maximizer of (5) with the highest outcome, then the least index; it is never a free function constrained by hypotheses. With the instance's distinct outcomes the least-index rule never fires.
• The model is the paper's base model: $b(x)=\pi(x)$, and $P(y\mid x)$ is unchanged by best responses (§2). Standing assumption (i) and outcome monotonicity are proved for the instance (milestone 1), not assumed.
• Outcome monotonicity is imposed for distinct feature values together with $c(x,x)=0$, since the printed zero-cost equivalence at $i=j$ would forbid free staying.
• All numbers are exact rationals ($1/10$, $7/10$, $2/5$, $6/5$, $3/10$).
• A formalization that states only "$(1,0.7,0)$ is optimal", or optimality against finitely many policies, would drop the stochasticity claim or trivialize the goal; neither is posed.
• Out of scope: Theorem 1 (NP-hardness), Proposition 2 and Theorem 3 (the structural results, mission 1 of this series), the general-cost example of §5 (mission 3), the algorithms and the experiments.

Needed infrastructure is small: finite sums over Fin 3, Finset.filter, Finset.min'. Lemmas evaluating br on regions of the policy cube are reusable across the series' examples.

Selected references

• S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, Management Science, 2024; read as arXiv:1905.09239v5, 2020. https://arxiv.org/abs/1905.09239v5
• S. Corbett-Davies, E. Pierson, A. Feller, S. Goel, A. Huq, Algorithmic Decision Making and the Cost of Fairness, KDD 2017. https://doi.org/10.1145/3097983.3098095
• I. Valera, A. Singla, M. Gomez-Rodriguez, Enhancing the Accuracy and Fairness of Human Decision Making, NeurIPS 2018. https://arxiv.org/abs/1805.10318
• M. Hardt, N. Megiddo, C. Papadimitriou, M. Wootters, Strategic Classification, ITCS 2016. https://doi.org/10.1145/2840728.2840730

Motivation

A lender or other decision maker may publish a rule that assigns a positive decision to an individual with some probability. Once the rule is visible, individuals can change the features on which it acts. The decision maker must therefore evaluate a rule under the distribution it induces after individuals respond, rather than only under the original population. Tsirtsis and coauthors study this problem with finitely many feature values and a cost for changing from one value to another. Their preprint gives a utility model, a best response rule, and structural results for costs that respect the ordering of outcomes.

This mission isolates Theorem 3 of that preprint. It asks whether, under additive and outcome monotonic costs, an optimal decision rule can be found among policies with a particular binary choice at each relevant feature value. The result concerns the structure of an optimum. It does not assert that an arbitrary starting policy is itself binary or that every optimum has this form.

Setting

There are $m\ge1$ feature values $x_1,\ldots,x_m$, indexed from highest to lowest positive-outcome probability. Write $p_i=P(x_i)$ for their original population masses and $q_i=P(y=1\mid x_i)$ for their outcomes. The masses are nonnegative and sum to one, $q_i\in[0,1]$, and the outcomes are distinct in this mission. A policy $\pi$ chooses a positive decision at $x_i$ with probability $\pi_i\in[0,1]$. Each positive decision costs the decision maker $\gamma\in(0,1)$.

An individual originally at $x_i$ can move to $x_j$ at change cost $c_{ij}$. In the paper's base model, the individual's benefit at a destination is $\pi_j$, so she maximizes $\pi_j-c_{ij}$. Ties go to a destination with higher $q_j$. If a tie remains, the formalization picks the smallest index. Write $r_\pi(i)$ for this best response. The outcome probabilities $q_j$ themselves do not change after the response; the response changes where the population mass is counted. The decision maker's utility is

A policy is outcome monotonic here when $\pi_i<\pi_j$ implies $q_i<q_j$. An outcome monotonic cost obeys the paper's two conditions for distinct feature values: improving outcome through successive values has the specified strict cost ordering, and a move to a lower outcome has zero cost. An additive cost satisfies $c_{ij}+c_{jk}=c_{ik}$ when $q_i<q_j<q_k$. Staying costs zero. The section's standing assumption also makes a distinct move toward a weakly higher outcome cost strictly positive.

Formalization targets

Main goal: Theorem 3

If $\pi^*$ maximizes utility among all policies in $[0,1]^m$, and the cost is additive and outcome monotonic, then some outcome monotonic policy $\pi$ has $u(\pi,\gamma)=u(\pi^*,\gamma)$ and satisfies

The paper calls this an outcome monotonic binary policy. Binary describes the two allowed relationships between adjacent policy values; the probabilities themselves can be fractional. The goal is conditional on a maximizer $\pi^*$, exactly as Theorem 3 is stated. The preprint does not establish that an optimum always exists, and its best response tie thresholds make that question separate.

Milestones

The first milestone records the observation following Proposition 2: under an outcome monotonic policy, an individual never selects a destination with lower outcome than the origin. Proposition 2 then states that some outcome monotonic policy attains the utility of an optimal policy under outcome monotonic costs. The final two milestones formalize the two individual policy changes stated in Appendix A.3, one when a policy value lies between its predecessor and the cost threshold, and one when it lies below that threshold.

Significance

Theorem 3 narrows a continuous search over policy probabilities to a structured family without losing the optimal value, provided an optimum exists. The restriction depends on how feature changes affect the induced population distribution. It is therefore a statement about decision making with strategic responses, not merely about sorting policy values by outcome. Proposition 2 is independently useful: under outcome monotonic costs, the optimal utility can be attained by an outcome monotonic policy even without additivity.

The result is proved in the cited preprint, while the proposed Lean declarations are open proof targets. A complete formalization would make the finite best response rule, the tie convention, and the cost assumptions explicit, then give checked proofs of the structural claims. The definitions of the policy space, response rule, and induced utility may also support later work on the same paper's stochastic examples and algorithms. No machine-checked proof of these proposed statements is claimed here.

Difficulty

The utility depends on a best response selected by an argmax, so changing one policy probability can switch the destination of several population groups at once. The utility need not vary continuously across tie thresholds. A naive coordinate adjustment that improves the outcome probability at one destination can alter who moves there and change the contribution from other origins. This is why a direct appeal to monotonicity of the displayed sum does not establish Proposition 2 or Theorem 3.

The Appendix A.3 statements identify two threshold regimes for a policy value. Their comparisons must account for the tie rule and for all origins whose selected destination changes. The mission keeps these comparisons as separate targets because the conclusion about the whole policy depends on them.

Formalization scope

Lean represents the features by Fin m, with Lean index $0$ standing for $x_1$. The model requires $m>0$ so that the best response has a value. The initial distribution and the conditional outcome probabilities are real valued, with explicit probability bounds. Policies range over the full cube $[0,1]^m$. The best response is computed from the policy and cost, with the highest-outcome tie rule; it is not supplied as independent data. Optimality means membership in that cube and maximal utility over that cube.

The formalization records several readings needed to make the preprint's displays consistent. Formula (1) prints a strict biconditional, but formula (9) allows equal adjacent policy values, so policy monotonicity is the implication from a strictly larger policy value to a strictly larger outcome. The cost equivalences apply to distinct values; staying is free. Additivity applies along strictly improving outcome chains, since an all-triples equality would conflict with positive improvement cost. Outcomes are assumed distinct, as needed for this version of Theorem 3. These choices are stated on the definition item and checked against the source in the moderation notes.

The goal retains the optimal-policy hypothesis and every clause of the binary property. It cannot be satisfied by defining the best response arbitrarily, shrinking the policy set to a selected candidate, or asserting only that a binary policy exists. The model covers the paper's base case $b(x)=\pi(x)$ with unchanged $P(y\mid x)$. The algorithms, complexity claims, experiments, and the paper's other examples are outside this mission. Contributions on the best response interface, finite optimization lemmas, Proposition 2, and either Appendix comparison are welcome.

Selected references

• S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, and M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, arXiv:1905.09239v5, 2020, §§2–4 and Appendix A.2–A.3; published in Management Science, 2024. arXiv preprint

Why the final licensing choice matters

A component supplier can influence a product market through both the wholesale price it charges and the technology its customers may share. Wang, Huang and Lee study a supply chain with one upstream supplier and two downstream manufacturers that invest in product quality and then compete in quantities. A cross-licensing policy lets each manufacturer use some of the other's innovation. The supplier may promise a policy before the investments, or leave the decision until after the investments and wholesale price are fixed. The latter choice creates a precise comparison: at that final stage, does permitting cross-licensing reduce the supplier's revenue? The authors answer it in Proposition 1 of their SSRN manuscript, version of 2023-04-27. Its proof is in the attached appendix, p. A.1.

This mission concerns that final-stage comparison. It is one part of the paper's broader study of how a supplier's licensing commitment affects manufacturers' innovation incentives and downstream market structure. The later innovation and initial-contract comparisons are separate questions. Here, investments and wholesale price are fixed, so the result isolates the direct quantity-market effect of licensing at the moment the supplier chooses its policy.

The downstream quantity game

Manufacturers $M_1$ and $M_2$ have already selected nonnegative innovation levels $T_1$ and $T_2$, with $T_1\le T_2$ in the presentation of equations (2) and (3). Each chooses a nonnegative production quantity $q_i$. The wholesale price $r$ is the amount each manufacturer pays the common supplier for one unit. The market-size intercept is normalized to one and per-unit manufacturing cost to zero. If licensing effectiveness is $\beta\in[0,1]$, manufacturer $i$ receives a quality improvement $T_i+\beta T_j$; $\beta=0$ represents no cross-licensing. Its inverse demand is $1+T_i+\beta T_j-q_1-q_2$. These are the model's conventions on pp. 9–10.

At fixed $T_1,T_2,\beta,r$, the manufacturers play a simultaneous quantity game. Their respective profits are

A Nash equilibrium is a pair $(q_1,q_2)\in[0,\infty)^2$ for which neither manufacturer increases its profit by changing its own nonnegative quantity while the other's quantity stays fixed. The supplier's profit at a quantity profile is $r(q_1+q_2)$. The supplier's comparison must therefore account for the manufacturers' responses under each licensing policy; it cannot compare profit at an arbitrary fixed quantity pair.

Formalization targets

The first milestone gives the exact equilibrium quantities of equation (2). Write $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$. For $r\le r_1$ both manufacturers can sell; for $r_1<r\le r_2$ only $M_2$ sells; above $r_2$ neither sells. The statement characterizes every equilibrium and thereby gives existence and uniqueness across the two threshold boundaries, including the cases where a manufacturer's equilibrium quantity is zero.

The second milestone identifies the supplier's revenue at an equilibrium with the piecewise expression $\pi_s^{\mathrm{cl}}(r)$ in equation (3). Setting $\beta=0$ in that expression gives the paper's no-licensing expression $\pi_s^{\mathrm n}(r)$ in equation (4). This milestone links the paper's algebraic profit comparison to the strategic quantity game, while keeping the equilibrium property as the premise.

The goal is the supplier's ex-post preference in Proposition 1. If $q^{\mathrm{cl}}$ is any equilibrium with licensing effectiveness $\beta$ and $q^{\mathrm n}$ is any equilibrium at $\beta=0$, then both equilibria exist and

This weak inequality is intentional. At $\beta=0$ the two games coincide, and there are other parameter values at which the profits tie. The comparison holds at the same innovation levels and the same wholesale price; it is not a comparison after re-optimizing the supplier's price or the manufacturers' investment decisions.

What the result establishes

For fixed investments and price, the supplier need not lose revenue by enforcing cross-licensing after observing the manufacturers' innovation. This gives mathematical content to the paper's claim that, without an initial commitment, the supplier will choose to enforce licensing at the final contract stage. The model does not specify a separate final-contract bargaining game, so the formal goal is the profit comparison that supports that interpretation. The result does not settle whether committing to licensing before innovation is preferable: changing the initial policy can change the innovation levels themselves, which the ex-post comparison holds fixed.

The authors prove Proposition 1 by comparing the supplier-profit expressions (3) and (4) in the manuscript's appendix. A machine-checked development would additionally secure the connection from the manufacturers' Nash conditions to those expressions, including the monopoly and zero-sales regimes. These statements are currently posed as open formalization targets; a Lean file with sorry only checks that the statements are well formed, not that the paper's argument has been verified by Lean. The general two-player Nash definition can be reused for other real-strategy games; the payoff and threshold definitions are specific to this supply chain.

Where the argument has to account for cases

The quantity equilibrium changes form as the wholesale price crosses $r_1$ and $r_2$. An argument confined to the two-selling-firms region misses cases in which $M_1$ sells nothing, or neither manufacturer sells. Comparing only the duopoly formulas cannot establish an inequality at every nonnegative price. The first milestone therefore covers all three regimes, and the goal compares the profits of actual equilibria. The fact that $T_2\ge T_1$ orders the possible monopoly toward $M_2$ under the paper's chosen labels; a formulation that silently assumes both equilibrium quantities are strictly positive would lose part of Proposition 1.

Formalization scope

All parameters and quantities are real. The permitted quantity strategies and wholesale prices are nonnegative. The paper treats $r$ as a wholesale price without writing a bound in Proposition 1; $r\ge0$ is made explicit because a negative price can reverse the supplier-profit inequality. The innovation ordering $0\le T_1\le T_2$ is the convention immediately preceding equation (2). Licensing effectiveness lies in $[0,1]$. Innovation costs $k_iT_i^2$ and the paper's bound $k_2>49/144$ are unnecessary once innovation levels are fixed, so they do not enter this mission's statements.

The formalization uses an explicit pair $(q_1,q_2)$, with the first coordinate for $M_1$. The quantity-game equilibrium is defined by unilateral payoff comparisons over $[0,\infty)$, and it is not defined by equation (2). Equation (2) is instead a theorem characterizing the equilibrium. The supplier's profit is defined as $r(q_1+q_2)$ for any pair, independently of equation (3). These choices prevent the goal from becoming an inequality between two expressions whose connection to the game has merely been assumed. Equation (2)'s missing closing parenthesis in the manuscript is interpreted as the displayed first quantity divided by three. No division in the model's displayed formulas has a variable denominator.

Selected references

• J. Wang, T. Huang and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, pp. 9–11 and Appendix p. A.1; published in Manufacturing & Service Operations Management, 2023. Manuscript; DOI.

Why this formulation matters

Clustering separates observations into groups whose members resemble one another. In kernel clustering, a matrix $K$ records a similarity score for each pair of observations, and an assignment seeks groups with high total within-group similarity. Real data can also contain outliers, observations that should not be assigned to any cluster. Srivastava, Sarkar, and Hanasusanto use a binary assignment program that permits those unassigned observations and then express the same exact problem through a matrix of pairwise co-memberships. The relationship is stated as Proposition 1 of their preprint. It is the algebraic starting point for the tractable relaxations introduced immediately after the proposition in §3.

The two exact programs have different variables. The assignment program describes each observation's cluster directly. The lifted program records whether each pair belongs to the same cluster. The latter representation makes positive semidefiniteness and rank explicit, and it is the one the paper relaxes to obtain its semidefinite program. A precise equivalence matters because a relaxation of the wrong feasible set would no longer be a relaxation of the stated assignment problem.

The two finite matrix programs

Let $N$ be the number of observations and $r$ the number of available clusters. A binary assignment matrix $Z\in\{0,1\}^{N\times r}$ has one row per observation and one column per cluster. In formulation (3), each row sums to at most one. A row with one nonzero entry assigns its observation to that cluster; a zero row leaves the observation unassigned. Thus the same matrix represents both inliers and outliers. Cluster sizes need not be equal, and unused cluster columns are allowed.

The clustering matrix $X=ZZ^\top$ has one row and column per observation. Its entry $X_{ij}$ is one when observations $i$ and $j$ share a cluster and zero otherwise, including when either observation has a zero assignment row. Formulation (4) asks instead for an $N\times N$ matrix $X$ whose entries lie in $\{0,1\}$, that is positive semidefinite, and whose rank is at most $r$. The rank bound limits the number of distinct nonzero cluster directions. Positive semidefiniteness is a property of the full real matrix, including its symmetry; it is not merely a condition on its diagonal.

Let $K\in\mathbb R^{N\times N}$ be the similarity matrix, $\gamma\in\mathbb R$ a penalty parameter, and $E_N$ the all-ones $N\times N$ matrix. The entrywise Frobenius inner product is $\langle A,B\rangle=\sum_{i,j}A_{ij}B_{ij}$. The programs maximize, respectively, $\langle K-\gamma E_N,ZZ^\top\rangle$ over feasible $Z$ and $\langle K-\gamma E_N,X\rangle$ over feasible $X$. Both have a feasible zero matrix, even at the boundary values $N=0$ and $r=0$.

Formalization targets

The goal is Proposition 1, stated with its factor and rotation. If $X^*$ is an optimal matrix for (4), there must exist $G\in\mathbb R^{N\times r}$ and an orthogonal $O\in\mathbb R^{r\times r}$ such that $Z^*=GO$ is feasible and optimal for (3), with

Here “feasible and optimal” includes the zero-one entry condition, the row-sum bound, and comparison with every feasible assignment matrix. The objective identity alone would say little: once the Gram factorization and orthogonality hold, it follows algebraically. The substantive result is the existence of an assignment-compatible rotation of a factor of every lifted optimum.

The milestone list follows the five claims in Appendix B of the preprint: lifting a feasible assignment to a feasible $X$ without changing its value; factoring a rank-bounded positive semidefinite $X$ through $r$ columns; classifying factor rows as zero or unit vectors; showing that distinct nonzero rows are orthogonal; and rotating those rows into assignment coordinates. These statements address both directions of the feasible-set correspondence used by Proposition 1.

What the result supplies

The proposition says that the matrix constraints in (4) describe the same exact clustering choices as the assignment constraints in (3), up to a choice of orthogonal coordinates for the factor. A lifted optimum therefore represents an assignment optimum rather than merely a matrix with the same numerical objective. Conversely, an assignment can always be lifted to a matrix accepted by (4). The paper can then drop the binary or rank constraints to obtain relaxations while keeping a clear exact program as their reference point; see §3 of the preprint.

The proposition is proved in the source paper. This mission seeks a machine-checked proof of that known claim and reusable finite-matrix results about binary positive semidefinite Gram matrices. In particular, the factorization and row-structure milestones can be used beyond spectral clustering whenever a zero-one Gram matrix appears with a rank bound. The Lean declarations here are proposed statements; their sorry proofs remain for solvers to complete.

Where the difficulty lies

The forward implication is immediate once a valid assignment matrix is given: its Gram matrix is positive semidefinite and has rank at most the number of cluster columns. The reverse implication carries the mathematical work. Positive semidefiniteness and low rank alone produce a real factor, but the factor need not have zero-one entries. A generic factor rotation also need not yield one-hot rows. The zero-one condition on every Gram entry is what constrains the relative positions of the nonzero rows strongly enough to recover assignment directions. The result must work when several observations share a direction, when some rows vanish, and when fewer than $r$ clusters are occupied.

Formalization scope

The formalization uses Mathlib matrices indexed by Fin N and Fin r over $\mathbb R$. Feasibility of (3) is entrywise membership in $\{0,1\}$ together with row sums at most one. Feasibility of (4) is entrywise membership in $\{0,1\}$, Matrix.PosSemidef, and Matrix.rank ≤ r. The objectives use the explicit sum of entrywise products, so no operator norm or alternate matrix inner product enters the statement. Global optimality is defined by comparison against the corresponding whole feasible set. The factor $G$ has exactly $r$ columns, and the rotation belongs to the real orthogonal group of dimension $r$.

The paper obtains $K$ from a Gaussian kernel and takes $\gamma\in(0,1)$ for the clustering application. Proposition 1 and Appendix B use only the displayed algebraic programs, so the formal statement permits arbitrary real $K$ and $\gamma$. No probability model, symmetry assumption on $K$, positive dimension assumption, or nonempty-cluster condition is needed. The boundary cases $N=0$ and $r=0$ retain their literal meanings. The formalization cannot assume that a feasible $X$ is already block diagonal or is already a Gram matrix of a binary assignment; that is the conclusion being established.

Useful contributions include proofs of the five Appendix B milestones, a finite-dimensional factorization theorem with the prescribed number of columns, and the rotation theorem that handles repeated or zero rows. These pieces should share the stated definitions so that the eventual proof of Proposition 1 uses precisely formulations (3) and (4).

Selected references

• P. R. Srivastava, P. Sarkar, and G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, Operations Research 71(1), 2023; arXiv:1912.07546v3, §3, Proposition 1 and Appendix B.