The OR Formalization Drive

Motivation

In 1965 Erdős asked how large a family of $k$-element subsets of an $n$-element set can be if it contains no $s+1$ pairwise disjoint members. The question, now called the Erdős Matching Conjecture (EMC), contains the Erdős–Ko–Rado theorem (the case $s=1$) and is one of the central open problems of extremal set theory. Beyond combinatorics it is tied to tail bounds for sums of random variables (generalizations of Markov's inequality, see Alon, Frankl, Huang, Rödl, Ruciński and Sudakov, JCTA 2012, as cited on p. 2 of the paper) and to Dirac-type thresholds for perfect matchings in hypergraphs.

Timeline.

• 1965: Erdős proves the conjecture for $n\ge n_0(k,s)$.
• 1959/1968: Erdős–Gallai settle $k=2$; Kleitman settles the case $n=k(s+1)$ implicitly.
• 1976: Bollobás, Daykin and Erdős prove it for $n\ge2k^3s$.
• 2012: Huang, Loh and Sudakov prove it for $n\ge3k^2s$.
• 2013: Frankl proves it for $n\ge(2s+1)k-s$ (JCTA 120).
• 2017: Frankl settles $k=3$ completely.
• 2018–2022: Frankl and Kupavskii prove it for $n\ge\frac53sk-\frac23s$ and all $s\ge s_0$ (arXiv:1806.08855), the result of this mission.

Setting

Write $[n]=\{1,\dots,n\}$ and $\binom{[n]}{k}$ for the set of its $k$-element subsets. For a family $\mathcal F\subseteq\binom{[n]}k$, a matching is a subfamily of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The Erdős matching function is

$$m(n,k,s)=\max\Big\{|\mathcal F| : \mathcal F\subseteq\tbinom{[n]}{k},\ \nu(\mathcal F)\le s\Big\}.$$

Two families show the conjectured value. The family of all $k$-sets meeting $[s]$ has $\binom nk-\binom{n-s}k$ members; the family of all $k$-subsets of $[k(s+1)-1]$ has $\binom{k(s+1)-1}k$ members. Both have $\nu\le s$, and the EMC asserts $m(n,k,s)$ is the larger of the two numbers. For $n\ge(k+1)s$ the first is larger.

The proof uses the shifting order: for $A=\{a_1<\dots<a_k\}$ and $B=\{b_1<\dots<b_k\}$, $A\prec B$ if $a_i\le b_i$ for all $i$ and $A\ne B$. A family is initial if it is closed downward under $\prec$. For $S\subseteq[s+1]$, $\mathcal F(S)=\{F\setminus S: F\in\mathcal F,\ F\cap[s+1]=S\}$, and $\partial$ denotes the shadow. Families $\mathcal F_1,\dots,\mathcal F_{s+1}$ are cross-dependent if no choice $F_i\in\mathcal F_i$ is pairwise disjoint, and nested if $\mathcal F_1\supseteq\dots\supseteq\mathcal F_{s+1}$. A random $t$-matching is a uniformly random ordered $t$-tuple of pairwise disjoint $l$-subsets of $[m]$, and $\eta=|\mathcal G\cap\mathcal B|$ counts how many of its sets lie in a fixed family $\mathcal G$ of density $\alpha=|\mathcal G|/\binom ml$.

Formalization targets

Goal: Theorem 1

There is an absolute constant $s_0$ such that for all $k\ge1$, $s\ge s_0$ and

$$n\ge\tfrac53sk-\tfrac23s\qquad\text{we have}\qquad m(n,k,s)=\binom nk-\binom{n-s}k .$$

The constant $s_0$ is existential and uniform in $n$ and $k$; no value is fixed, so any improvement of the proof keeps the statement valid.

Stronger form: Theorem 14

For every $\varepsilon>0$ there is $s_0(\varepsilon)$ such that the same equality holds for all $s\ge s_0$, $k\ge1$ and $n\ge s+(1.666+\varepsilon)s(k-1)$. Theorem 1 follows by taking $\varepsilon<\frac53-1.666$.

Milestones

Following the paper's proof: Lemma 3 (shifting), Proposition 4, Lemma 5, Proposition 6, Corollary 7 and Lemma 8 (structure of initial families and their shadows); Proposition 11, Theorem 12 and Proposition 13 (concentration of $\eta$ for random matchings); Lemma 18 and Lemma 15 (the weighted bound for cross-dependent nested families); Lemmas 16 and 17 (the induction step at $n=s+(1.666+\varepsilon)s(k-1)$); Theorem 14.

Significance

The theorem extends the range in which the EMC is known from $n\ge(2s+1)k-s$ to $n\ge\frac53sk-\frac23s$ for large $s$, settling roughly a third of the remaining range. The paper uses it as a black box to derive a universal upper bound on $m(n,k,s)$ below that range (its Theorem 2) and consequences for Dirac thresholds. The concentration inequality of Theorem 12, a Gaussian tail for the number of members of a fixed family hit by a random matching, is a tool of independent use and has since been applied to rainbow versions of the problem (Kupavskii, arXiv:2104.08083).

The result is proved on paper; this mission formalizes it. No part of the argument has a machine-checked proof: Mathlib has shadows and the Erdős–Ko–Rado theorem, and the platform has Erdős–Ko–Rado for $s=1$, but there is no formal theory of the matching number, shifted families, Kneser graph spectra, or martingale concentration for random matchings. A complete formalization would make the EMC in this range, and the concentration theorem, available for reuse.

Difficulty

Averaging over a random full partition of $[n]$ into $k$-sets gives only $m(n,k,s)\le s\binom{n-1}{k-1}$, far from the truth: the expected number of partition classes in $\mathcal F$ says nothing about how that number is distributed. The paper's step is to show the count is concentrated (Theorem 12) and to exploit the deterministic bound of Lemma 18, which penalizes matchings with many classes in $\mathcal F_{s+1}$. Controlling the regime where the density $\alpha$ is small needs the separate comparison of Proposition 13.

The second difficulty is Lemma 17, whose proof in the appendix is a delicate estimate on sums and products of binomial coefficients over all $k\ge4$, supported by numerical computations done in Mathematica. A formal proof needs certified numerics for these finite checks and a separate stability argument for $k>2\cdot10^4$. The case $k=3$ is an external base case (Frankl 2017), so the induction on $k$ also needs that result or another route.

Formalization scope

Sets are finite sets of natural numbers; $[n]$ is Finset.Icc 1 n, so the paper's indices such as $[i(s+1)-1]$ and $s+1,2(s+1),\dots$ appear unshifted. $\nu$ is a maximum over subfamilies (members are distinct), and $m(n,k,s)$ is a finite maximum, always attained. Initial families are closed downward among $k$-subsets of $[m]$ only. Random matchings are ordered tuples, and probabilities, expectations and covariances are uniform averages over the finite sample space. The constant $1.666$ is the exact decimal, not $5/3$. The paper omits integer parts at $n=s+(c+\varepsilon)s(k-1)$; the formalization rounds $n$ up. Where the paper leaves hypotheses implicit, they are binders: $k\ge2$ in Corollary 7, Lemma 8 and Lemma 16, $k\ge4$ and the induction hypothesis in Lemma 17, $t\ge1$ in Theorem 12, and $q>0$ (the division $sx/q$) in Lemma 15.

The goal is the equality $m(n,k,s)=\binom nk-\binom{n-s}k$; exhibiting the family of $k$-sets meeting $[s]$ proves only the lower bound and does not close it.

Useful infrastructure, reusable beyond this mission: shifting and the compression argument (Lemma 3), the shadow bounds of Section 2, the expander mixing lemma and the second eigenvalue of Kneser graphs, and the Azuma–Hoeffding inequality for the exposure martingale of a random matching. Contributions of any of these, and of alternative proofs of the milestones, are welcome.

Selected references

• P. Frankl, A. Kupavskii, The Erdős Matching Conjecture and concentration inequalities, J. Combin. Theory Ser. B (2022); arXiv:1806.08855v3. https://arxiv.org/abs/1806.08855, https://doi.org/10.1016/j.jctb.2022.08.002
• P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965), 93–95.
• P. Frankl, Improved bounds for Erdős' Matching Conjecture, J. Combin. Theory Ser. A 120 (2013), 1068–1072. https://doi.org/10.1016/j.jcta.2013.01.008
• P. Frankl, On the maximum number of edges in a hypergraph with given matching number, Discrete Appl. Math. 216 (2017), 562–581.
• H. Huang, P.-S. Loh, B. Sudakov, The size of a hypergraph and its matching number, Combin. Probab. Comput. 21 (2012), 442–450.
• N. Alon, F. Chung, Explicit construction of linear sized tolerant networks, Discrete Math. 72 (1988), 15–19. https://doi.org/10.1016/0012-365X(88)90189-6
• L. Lovász, On the Shannon capacity of a graph, IEEE Trans. Inform. Theory 25 (1979), 1–7. https://doi.org/10.1109/TIT.1979.1055985

Motivation

Least-squares fitting is a standard tool in estimation, identification and data analysis, and its data $A$, $b$ are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose $x$ to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of $[A\ b]$ and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix $\Delta$ through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).

In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings $S$ and $G$ below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).

Setting

Vectors carry the Euclidean norm $\|v\|$. For a matrix $X$, $\|X\|$ is its largest singular value (operator norm between Euclidean spaces). Let $\mathcal D$ be a linear subspace of $\mathbb R^{N\times N}$ (the perturbation structure), and fix $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^n$, $L \in \mathbb R^{n\times N}$, $R_A \in \mathbb R^{N\times m}$, $R_b \in \mathbb R^N$, $D \in \mathbb R^{N\times N}$. For $\Delta \in \mathcal D$ with $\det(I - D\Delta) \ne 0$ the perturbed data are

$$A(\Delta) = A + L\Delta(I - D\Delta)^{-1}R_A, \qquad b(\Delta) = b + L\Delta(I - D\Delta)^{-1}R_b .$$

With the normalization $\rho = 1$ (the paper's, with no loss of generality), the worst-case residual of $x \in \mathbb R^m$ is

$$r_{\mathcal D}(A,b,x) = \max_{\Delta \in \mathcal D,\ \|\Delta\| \le 1} \|A(\Delta)x - b(\Delta)\|$$

if $\det(I - D\Delta) \ne 0$ for every such $\Delta$, and $+\infty$ otherwise (35). The commutant scalings are $\mathcal S = \{S = S^T : S\Delta = \Delta S\ \forall \Delta \in \mathcal D\}$ and $\mathcal G = \{G = -G^T : G\Delta = \Delta G\ \forall \Delta \in \mathcal D\}$ (37). The SDP constraint is

$$\mathcal F(\lambda,S,G,x) = \begin{bmatrix} \Theta & \begin{matrix} Ax - b \\ R_Ax - R_b\end{matrix} \\ \begin{matrix}(Ax-b)^T & (R_Ax - R_b)^T\end{matrix} & \lambda\end{bmatrix} \succ 0, \quad \Theta = \begin{bmatrix} \lambda I - LSL^T & -LSD^T + LG \\ -DSL^T + G^TL^T & S + DG - GD^T - DSD^T\end{bmatrix}. \qquad (38),(39)$$

Formalization targets

Goal: Theorem 5.2 (corrected)

For all $x$ and $\lambda$:

$$\text{(a)}\quad S \in \mathcal S,\ G \in \mathcal G,\ S \succ 0,\ G\Delta \text{ skew } \forall \Delta \in \mathcal D,\ \mathcal F(\lambda,S,G,x) \succ 0 \ \Longrightarrow\ \lambda > r_{\mathcal D}(A,b,x);$$ $$\text{(b)}\quad \mathcal D = \mathbb R^{N\times N},\ \lambda > r_{\mathcal D}(A,b,x) \ \Longrightarrow\ \exists s > 0:\ \mathcal F(\lambda, sI, 0, x) \succ 0 .$$

Part (a) says the value of the SDP $\inf\{\lambda : (\lambda, S, G) \text{ feasible}\}$ (40) is an upper bound on $r_{\mathcal D}$. Part (b) says this upper bound is exact for full perturbations, including the case $r_{\mathcal D} = \infty$, where (40) is infeasible.

Milestones

1. Lemma 2.2, both directions: the full-block S-procedure. $\det(I - T_4\Delta) \ne 0$ and $T(\Delta) \succeq 0$ for all $\|\Delta\| \le 1$ if and only if $\|T_4\| < 1$ and a one-scalar LMI (10) holds (the "only if" under $T_2 \ne 0$ or $T_3 = 0$).
2. Lemma 2.3: sufficiency of the scaled LMI for a structured $\mathcal D$, and its strict necessity for $\mathcal D = \mathbb R^{N\times N}$.
3. §5.4, p. 1047: $\lambda > r_{\mathcal D}(A,b,x)$ if and only if a linear-fractional matrix function of $\Delta$ is positive definite on the structured unit ball.
4. §5.4, (38)–(39): the certificate (a) in the paper's own words.

Significance

The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate $(S, G)$. Since $x$ enters (38) linearly, the same constraint can also be optimized over $x$ (Theorem 5.3, not part of this mission). For $\mathcal D = \mathbb R^{N\times N}$ the bound is exact, which covers the model $[A(\Delta)\ b(\Delta)] = [A\ b] + L\Delta[R_A\ R_b]$ and, as a special case, the unstructured problem of §3.

The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.

Difficulty

Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse $(I - D\Delta)^{-1}$. The certificate is one LMI in which $\Delta$ does not appear, while the conclusion is about a rational function of $\Delta$ over a whole structured ball. The certificate also has to guarantee that $I - D\Delta$ is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating $\mathcal F$ at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only $\succeq$, and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case $T_2 = 0$ is not covered by the S-lemma's regularity condition and has to be handled separately.

Formalization scope

• Dimensions are Fin n, Fin m, Fin N; $\mathcal D$ is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with $\mathcal D = \mathbb R^{N\times N}$ as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. $\|\Delta\|$ is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.
• $\lambda > r_{\mathcal D}(A,b,x)$ is the predicate ResidualBelow: every $\Delta \in \mathcal D$ with $\|\Delta\| \le 1$ has $\det(I - D\Delta) \ne 0$ and residual $< \lambda$. It is false for every $\lambda$ when $r_{\mathcal D} = \infty$. No real-valued supremum is used, so the $\infty$ branch of (35) cannot turn into a default $0$. Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.
• $\rho = 1$ throughout, as in the paper; general $\rho$ follows by scaling $\Delta$.
• Corrections of the printed statements. (i) (40) must require $S \succ 0$. Without it, $N = n = m = 1$, $D = 2$, $L = 1$, $A = b = R_A = R_b = 0$, $x = 0$, $S = -1$, $G = 0$ satisfy (38) for every $\lambda > 1/3$, while $r_{\mathcal D} = \infty$. (ii) $G$ must make $G\Delta$ skew-symmetric for every $\Delta \in \mathcal D$, which is the identity $p^TGq = 0$ used in the proof of Lemma 2.3. For $\mathcal D = \operatorname{span}\{I, J\}$, $J = \begin{bmatrix}0&1\\-1&0\end{bmatrix}$, the printed bound certifies $\lambda = 3/2$ for an instance with worst-case residual $2$. The added condition holds automatically when every element of $\mathcal D$ is symmetric (e.g. the diagonal structures (36)) and when $G = 0$ (e.g. $\mathcal D = \mathbb R^{N\times N}$). (iii) Lemma 2.2's "only if" is stated under $T_2 \ne 0$ or $T_3 = 0$. (iv) Lemma 2.3's necessity is stated in strict form, and its sufficiency concludes $T(\Delta) \succ 0$.
• Not stated: "If $\Theta > 0$ at the optimum, the upper bound is also exact". The infimum over the strict LMI (38) is not attained, and the paper does not say which limit is meant. Theorem 5.3, Lemma 2.4 and Lemma 5.1 are also not stated.
• Trivializing encodings ruled out: the goal is not a statement about the value of an infimum (which a junk value could satisfy), and the added hypotheses are satisfiable (for instance $S = sI$, $G = 0$ for full $\mathcal D$, which part (b) produces).
• Infrastructure needed: the Schur complement for block matrices (in Mathlib), a lossless S-lemma for two homogeneous quadratic forms in strict and non-strict form (the platform has ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with $\mathcal D$, and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.

Selected references

• L. El Ghaoui and H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18(4):1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
• S. Boyd, L. El Ghaoui, E. Feron and V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777
• M. K. H. Fan, A. L. Tits and J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36(1):25–38, 1991. https://doi.org/10.1109/9.62265
• I. Pólik and T. Terlaky, A survey of the S-lemma, SIAM Review 49(3):371–418, 2007. https://doi.org/10.1137/S003614450444614X

Motivation

Integer programming asks whether a system of linear inequalities $Ax\le b$ has a solution $x\in\mathbb Z^n$. In fixed dimension $n$ it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in $n^{O(n)}$ operations, and runs integer programming in $O(n^{9n/2}s)$ arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.

Timeline.

• Korkine and Zolotareff (1873): the reduced bases used here.
• Minkowski (1896): a symmetric convex body of volume greater than $2^n$ contains a nonzero integer point.
• Khinchine (1948): lattice-free convex bodies have lattice width bounded by a function of $n$ alone (the flatness theorem).
• Lenstra (1983): integer programming in fixed dimension is polynomial, via a flat direction.
• Kannan (1987, this paper): Theorem (5.5), with subspaces $V$ of any dimension between $1$ and $n-1$ and an explicit bound $n^{2(n-\dim V)}$.
• Kannan and Lovász (1988), Banaszczyk et al. (1999), and later work: polynomial bounds on the flatness constant.

Setting

$\mathcal R^n$ is Euclidean space with dot product $(a,b)$ and length $|a|$, and $\mathbb Z^n$ is the set of integer vectors. For linearly independent $b_1,\dots,b_m\in\mathcal R^k$, the lattice $L(b_1,\dots,b_m)$ is the set of integer combinations $\sum_j\lambda_jb_j$, $\lambda_j\in\mathbb Z$, and $b_1,\dots,b_m$ is a basis. Gram–Schmidt orthogonalisation gives $b_1^*,\dots,b_m^*$ and unit vectors $u_j=b_j^*/|b_j^*|$, and $b_i(j)=(b_i,u_j)$, so $b_i=\sum_jb_i(j)u_j$ and $b_j(j)=|b_j^*|$. The determinant is $d(L)=\prod_j|b_j^*|$. $\Lambda_1(L)$ is the length of a shortest nonzero vector of $L$. The projected lattice $L_j(b_1,\dots,b_m)$ is the image of $L$ under orthogonal projection onto the complement of $\operatorname{span}(b_1,\dots,b_{j-1})$. A basis is reduced (Definition 2.6) if $b_j(j)=\Lambda_1(L_j)$ for every $j$ and $|b_i(j)|\le b_j(j)/2$ for $i>j$.

A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace $V$ has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets $z+V$ with $z\in\mathbb Z^n$.

In Lean, $\mathcal R^k$ is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), $|b_j^*|$ is gsLen b j, $b_i(j)$ is gsCoeff b i j, $d(L)$ is latticeDet b, $\Lambda_1$ is lambdaOne, $L_{j+1}$ is projLattice b j, and a reduced basis is IsReduced b.

Formalization targets

Goal: Theorem (5.5), corrected reading

For $n\ge2$ and every bounded convex set $K\subseteq\mathcal R^n$ with nonempty interior and $K\cap\mathbb Z^n=\emptyset$ there is a subspace $V$ spanned by integer vectors with $1\le\dim V\le n-1$ and

$$\#\{\,z+V : z\in\mathbb Z^n,\ (z+V)\cap K\ne\emptyset\,\}\ \le\ n^{2(n-\dim V)}.$$

The printed theorem allows "an $i$ dimensional space $V$" with $1\le i\le n$ and bound $n^{2(n-i+1)}$. Taken literally that is trivial ($V=\mathcal R^n$, one translate). The proof on the same page takes $V=\operatorname{span}(b_1,\dots,b_{i-1})$, of dimension $i-1$, and remarks that this "ensures that the subspace $V$ is always of dimension at least 1". The goal states that reading.

Milestones

1. Theorem (1.11), Minkowski's convex body theorem (referenced from the platform, in Mathlib's general form).
2. Theorem (1.12): every $m$-dimensional lattice has a nonzero vector with $|v|\le\sqrt m\,d(L)^{1/m}$.
3. Proposition 1.9: a primitive lattice vector belongs to some basis.
4. Proposition 2.16, existence form: every lattice has a reduced basis.
5. Proposition 4.2: for any $b_0$ with projection $\bar b_0$ onto the span, some $b\in L$ has $|b-\bar b_0|\le\frac12(\sum_jb_j(j)^2)^{1/2}\le\frac{\sqrt m}2\max_jb_j(j)$.
6. Proposition 4.3: for a reduced basis and $i$ maximising $b_i(i)$, the tail $(\lambda_i,\dots,\lambda_m)$ of every closest lattice point to $b_0$ lies in an explicit set of at most $m^{m-i+1}$ integer vectors.

Significance

Theorem (5.5) is a structural form of the flatness theorem. For $\dim V=n-1$ it says that a lattice-free convex body meets fewer than $n^2$ consecutive integer hyperplanes of some integral direction. For smaller $\dim V$ it gives a finer decomposition of $\mathbb Z^n$ into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.

The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.

Difficulty

The naive route to (5.5) is to take a flat direction directly: bound the lattice width of $K$ and count hyperplanes. That needs a flatness theorem with an explicit bound below $n^2$, which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its $n$-fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each $L_i$ with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.

Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of $\Lambda_1$ on every projected lattice and a lifting argument (Proposition 1.9).

Formalization scope

Conventions: indices are 0-based (Fin m), so the paper's $L_j$ is projLattice b (j-1) and its bound $n^{n-i+1}$ is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and $m\le k$ is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. $K$ is assumed convex, bounded and with nonempty interior, but not closed.

Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.

• (1.12)'s constant $\frac12\sqrt n$ is false for $n\le7$ (for example $L=\mathbb Z$, or the hexagonal lattice) and is replaced by $\sqrt n$, the constant the paper's own later proofs use.
• Proposition 4.2's second sentence is stated for $\bar b_0$ instead of $b_0$.
• Proposition 4.3 fails at $n=1$ and is stated for $m\ge2$ with the proof's explicit candidate set $T$, since an existential $T$ is satisfied by the set of tails of closest points and says nothing.

Trivializing formalizations are ruled out: the goal forbids $\dim V=n$, which gives one translate, and $\dim V=0$, where no translate meets $K$. It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become $0$).

Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the $L_2$ closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.

Selected references

• R. Kannan, Minkowski's Convex Body Theorem and Integer Programming, Mathematics of Operations Research 12(3):415–440, 1987. https://doi.org/10.1287/moor.12.3.415
• H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4):538–548, 1983. https://doi.org/10.1287/moor.8.4.538
• R. Kannan, L. Lovász, Covering minima and lattice-point-free convex bodies, Annals of Mathematics 128(3):577–602, 1988. https://doi.org/10.2307/1971436
• A. K. Lenstra, H. W. Lenstra Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261:515–534, 1982. https://doi.org/10.1007/BF01457454
• F. John, Extremum problems with inequalities as subsidiary conditions, Studies and Essays presented to R. Courant, 1948, 187–204.

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$, complementary distribution function $\bar F$, finite mean, $f > 0$ on $[0, \mathbb Z]$ ($\mathbb Z \le +\infty$), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$, and $k(q) = S(q)/\bar F(q)$.

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$. The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$, payment follows after a term $t_2$, and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$), the supplier's expected profit is

$$\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),$$

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$, $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$, $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$, and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$. The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$, let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$, $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$, and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ($c_i = p$). With all three schemes available,

$$e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;$$ $$1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.$$

Milestones

1. Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$, and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$, $w = c_{\mathcal F}/\bar F(q)$.
2. Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$.
3. §5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$.
4. §4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$.
5. Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$, $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

• "Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$, which is what Propositions 2 and 3 prove.
• "Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$, the order forced by the paper's boundaries ($C_s = \mathbb C_1$, $C_s = \mathbb C_3$, $C_r = \mathbb C_2$). Profits are compared, not the $\Lambda_i$.
• "The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$, since $\Lambda_{\mathcal F}$ may be $\le 0$.
• "$C_r > \mathbb C_2$" is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$, i.e. $e^{-\eta_r\tau} < 1-\rho_r$: the stated assumptions give no single crossing in $C_r$.
• "The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$; this part is stated under feasibility.
• "Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
• Continuity of $f$ is read on $[0,\mathbb Z]$, and $\mathbb Z$ as the upper end of the support.
• Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$).
• Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$, "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ($c_i < p$, largest $\Lambda_i$) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$, $k$ and $z$ under strict IFR are welcome.

Selected references

• P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
• D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
• P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

Motivation

Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.

Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.

Setting

Demand $D\ge0$ has density $f$, distribution function $F$ and $\bar F=1-F$; $f>0$ on $[0,\mathbb Z]$ with $\mathbb Z\le+\infty$ the upper end of the support, $f$ is continuous there, the mean is finite, and the failure rate $z(\xi)=f(\xi)/\bar F(\xi)$ is strictly increasing. Write $S(q)=\int_0^q\bar F(\xi)\,d\xi$ for expected sales and $k(q)=S(q)/\bar F(q)$.

A retailer (the leader) sets a wholesale price $w$, and a capital-constrained supplier (the follower) chooses a production quantity $q\ge0$; the retail price $p$ exceeds the unit cost $c$. Each firm $j\in\{s,r\}$ has a credit rating $C_j\in(C_{\min},C_{\max})$, a default probability $\rho_j=\rho(C_j)\in[0,1]$ with $\rho$ strictly decreasing, and an interest premium $\eta_j=\eta(C_j)>0$ with $\eta$ decreasing. The lead time is $t_1$, the payment term $t_2$, and $\lambda_s,\lambda_r\ge0$ are the liquidity risks.

Under a post-shipment scheme with coefficient $\Lambda$ the supplier earns

$$\pi(q;w)=(1-\rho_s)\bigl(\Lambda e^{-\lambda_s t_1}wS(q)-c\,q\,e^{\eta_s t_1}\bigr),$$

with $\Lambda_{\mathcal F}=(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}$ (recourse factoring), $\Lambda_{\mathcal N}=e^{-\eta_r t_2}(1-\rho_r)$ (non-recourse factoring) and $\Lambda_{\mathcal R}=e^{-\eta_r(t_2+\tau)}$ (reverse factoring with payment extension $\tau\ge0$). The retailer earns $\Pi=e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and

$$\Pi_{\mathcal R}(w,\tau)=e^{-\lambda_s t_1}(1-\rho_r)(2-e^{-\lambda_r\tau})(p-w)S(q_{\mathcal R})$$

under reverse factoring, where $q_{\mathcal R}$ is the supplier's best response. Its first-order condition is $w\bar F(q_{\mathcal R})=c_{\mathcal R}(\tau)=c\,e^{(\eta_s+\lambda_s)t_1+\eta_r(t_2+\tau)}$ (Eq. (12)).

Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium $(w^*_{\mathcal N},q^*_{\mathcal N})$, when $\mathbb C_{\mathcal N}<C_s\le\mathbb C_1$, and recourse, with $(w^*_{\mathcal F},q^*_{\mathcal F})$, when $C_s>\mathbb C_{\mathcal F}\vee\mathbb C_1$. The retailer keeps the existing wholesale price $w_s$ and solves problem (13): maximize $\Pi_{\mathcal R}(w_s,\tau)$ over $\tau\ge0$, subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). $\mathbb C^{\max}_{\mathcal R}$ is the rating at which $\Lambda_{\mathcal F}=e^{-\eta_r t_2}$, and $\Xi_{[0,z]}(x)=\max\{0,\min\{z,x\}\}$.

Formalization targets

Goal: Proposition 6

(i) If $C_s\ge\mathbb C^{\max}_{\mathcal R}$, reverse factoring is dominated by recourse factoring. (ii) If $\mathbb C_{\mathcal N}<C_s<\mathbb C^{\max}_{\mathcal R}$, reverse factoring should be offered with

$$\tau^*_{\mathcal R}=\Xi_{[0,\tau_s]}(\tau^*_0),\qquad \lambda_r k(q)z(q)+\eta_r=2\eta_r e^{\lambda_r\tau^*_0},\quad w_s\bar F(q)=c_{\mathcal R}(\tau^*_0),$$

where $\tau_s=-\eta_r^{-1}\ln(1-\rho_r)$ with $w_s=w^*_{\mathcal N}$ in the non-recourse case, and $\tau_s=-\eta_r^{-1}\ln[(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}]-t_2$ with $w_s=w^*_{\mathcal F}$ in the recourse case.

Milestones, in attack order

1. Eq. (12): the supplier's best response under reverse factoring.
2. Proposition 4: which factoring scheme is in force before reverse factoring.
3. §5.3, $\tau_s$: acceptance holds exactly on $[0,\tau_s]$.
4. §5.3, $\tau^*_0$: the retailer's unconstrained profit is unimodal around $\tau^*_0$.

A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when $\tau^*_0\ge\tau_s$.

Significance

Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating $\mathbb C^{\max}_{\mathcal R}$ and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).

The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.

Difficulty

The retailer's objective depends on $\tau$ through two opposing channels: the liquidity factor $2-e^{-\lambda_r\tau}$ increases, while expected sales $S(q_{\mathcal R}(\tau))$ decrease because the supplier's effective cost rises. Neither factor is concave in $\tau$, and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of $k\cdot z$ along the implicitly defined response $q_{\mathcal R}(\tau)$, which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at $\tau$ against the existing equilibrium). Reducing it to $\tau\le\tau_s$ requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.

Formalization scope

The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on $\mathbb R$ with a density $f$, and $\mathbb Z$ is an extended real. "Continuous p.d.f. with $f>0$ in $[0,\mathbb Z]$" is read as continuity on $[0,\mathbb Z]$, with $f=0$ outside the support. Credit functions $\rho,\eta$ are real functions constrained on $(C_{\min},C_{\max})$. The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.

Readings of informal words, each also recorded in the item's Formalization Note:

• Best response: a maximizer of the supplier's profit over $q\ge0$; equilibrium: a best response pair from which no nonnegative wholesale price with a best response gives the retailer more. Neither is defined through first-order conditions.
• Feasible: some $w\ge0$ with a best response gives the retailer positive profit; adopted (Proposition 4): feasible, with equilibrium supplier profit at least (non-recourse) or strictly above (recourse) the other feasible scheme's.
• Thresholds "the unique value of $C_s$ that satisfies …" are hypotheses in exactly that form; $c_{\mathcal N}=p$ and $c_{\mathcal F}=p$ are cross-multiplied because $\Lambda_{\mathcal F}$ can be $\le0$.
• In (13) $w$ is fixed at $w_s$ (§5.3's first sentence, footnote 23). $\pi^*_{\mathcal R}$ is the supplier's best-response profit under reverse factoring at $(w_s,\tau)$, and $\max\{\pi^*_{\mathcal F},\pi^*_{\mathcal N}\}$ is his profit in the existing equilibrium.
• Dominated (Proposition 6(i)): at every $\tau\ge0$ and every $w$, the supplier's reverse factoring best-response profit is at most his recourse one. Should be offered (6(ii)): $\tau^*_{\mathcal R}$ solves (13) and the retailer's profit is at least her existing equilibrium profit.
• $\tau^*_0$ is a hypothesis: it and some $q\in(0,\mathbb Z)$ solve the paper's two equations (the paper does not argue existence). Its optimality "without the nonnegativity constraint" is stated as unimodality of $\Pi_{\mathcal R}$ on the set of real $\tau$ with $c_{\mathcal R}(\tau)<w$.
• Always increases (Corollary 3(ii)) is strict; may remain unchanged when $\tau^*_0\ge\tau_s$ is read as "is unchanged whenever $\tau^*_0\ge\tau_s$".

Three misprints of the paper are corrected: $\Xi_{[0,z]}(x)=0$ "if $x<z$" is read as "if $x<0$"; "the retailer's maximization problem in (16)" refers to (13); the middle line of the $\Pi_{\mathcal R}$ display on p. 6082 carries a stray factor $w$, and the last line is used.

The hypotheses on $\tau^*_0$ cannot be met when $\lambda_r=0$, and the goal then says nothing about the case, as in the paper. The existing equilibrium, $\tau_s$ and $\tau^*_0$ are never free parameters: $\tau_s$ is the paper's explicit formula, and the reduction of acceptance to $\tau\le\tau_s$ is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to $\tau\le\tau_s$ or assumed unimodality would be trivial and is excluded.

The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas ($k$, $k\cdot z$ and $k(q)-q$ increasing) and the explicit best response of a newsvendor-type follower.

Selected references

• P. Kouvelis, F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• D. A. Wuttke, E. S. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019. https://doi.org/10.1002/joom.1023

Motivation

Pattern search methods minimize a function $f:\mathbb R^n\to\mathbb R$ by comparing values of $f$ at points of a structured set of trial points, without evaluating or approximating derivatives. Coordinate search and the method of Hooke and Jeeves (Hooke–Jeeves 1961) are the classical members of the family. Such methods remain in use when derivatives are unavailable, unreliable or expensive, for instance when $f$ is the output of a simulation, and practical problems of this kind usually carry simple bounds on the variables.

Torczon (SIAM J. Optim. 1997) gave a global convergence theory for pattern search on unconstrained problems: under compactness of the level set and continuous differentiability of $f$, $\liminf_k\|\nabla f(x_k)\|=0$, and under stronger hypotheses $\lim_k\|\nabla f(x_k)\|=0$. Lewis and Torczon extended this theory to bound constrained problems (ICASE Report 96-20, 1996; SIAM J. Optim. 1999). The extension is not automatic: the paper exhibits a pattern search method for unconstrained problems (Box's evolutionary operation with factorial designs) that fails on bound constrained ones, and identifies the structural condition on the pattern that restores convergence.

Timeline.

• 1961: Hooke and Jeeves introduce "direct search" pattern methods.
• 1987–1988: Calamai and Moré (Math. Program. 1987) and Conn, Gould and Toint (SIAM J. Numer. Anal. 1988) develop the projected-gradient stationarity theory for bound and linear constraints, for methods that use derivatives.
• 1997: Torczon proves global convergence of generalized pattern search for unconstrained problems.
• 1996/1999: Lewis and Torczon prove the bound constrained theory formalized here.

Setting

The problem is

$$\min f(x)\quad\text{subject to}\quad \ell\le x\le u,$$

with $\ell,u$ vectors of extended reals and $\ell_j<u_j$ for every $j$; $\ell_j=-\infty$ or $u_j=+\infty$ is allowed. The feasible region is $\Omega=\{x:\ell\le x\le u\}$, $P$ is the coordinatewise projection onto $\Omega$, $g=\nabla f$, and $L_\Omega(y)=\{x\in\Omega:f(x)\le f(y)\}$ is the feasible level set. A stationary point is an $x\in\Omega$ with $\langle g(x),z-x\rangle\ge0$ for all $z\in\Omega$. The stationarity measure is

$$q(x)=P\bigl(x-g(x)\bigr)-x,$$

which vanishes exactly at stationary points.

A generalized pattern search method is fixed by a nonsingular basis matrix $B\in\mathbb R^{n\times n}$, a finite set $\mathcal M$ of nonsingular integer matrices, a rational $\tau>1$, an integer $w_0<0$ and nonnegative integers $w_1,\dots,w_L$. At iteration $k$ the generating matrix is $C_k=[M_k\ \ {-M_k}\ \ L_k]=[\Gamma_k\ \ L_k]$ with $M_k\in\mathcal M$, $L_k$ an integer matrix containing a zero column, and $BM_k$ diagonal. A trial step is $\Delta_kBc$ for a column $c$ of $C_k$. The step $s_k$ is a trial step with $x_k+s_k\in\Omega$, and it must decrease $f$ whenever some feasible trial step from the core $\Delta_kB\Gamma_k$ does. The iterate moves, $x_{k+1}=x_k+s_k$, exactly when $f(x_k+s_k)<f(x_k)$. The step length $\Delta_k$ is multiplied by $\theta=\tau^{w_0}<1$ after an unsuccessful iteration and by some $\tau^{w_i}\ge1$ after a successful one. The Strong Hypotheses additionally require $f(x_k+s_k)$ to be no larger than the best feasible core trial value whenever that value is below $f(x_k)$.

Formalization targets

Goal: Theorem 3.3

If $L_\Omega(x_0)$ is compact, $f$ is continuously differentiable, the columns of the $C_k$ are uniformly bounded, $\Delta_k\to0$, and the Strong Hypotheses hold, then

$$\lim_{k\to\infty}\|q(x_k)\|=0 .$$

Milestones

• Lemma 2.1, Theorem 2.2, Lemma 2.3: the unconstrained results the paper recalls from Torczon (1997): nonzero steps have length at least $\zeta_*\Delta_k$; the iterates lie on the translated lattice $x_0+\beta^{r_{LB}}\alpha^{-r_{UB}}\Delta_0B\,\mathbb Z^n$ (with $\tau=\beta/\alpha$); bounded columns give $\Delta_k\ge\psi_*\|s_k^i\|$.
• Proposition 3.1 (6), (8): $\|q(x)\|\le\|g(x)\|$, and $x$ is stationary iff $q(x)=0$.
• All iterates lie in $L_\Omega(x_0)$ (§4, p. 10).
• Propositions 4.1–4.3: a descent estimate along short steep directions; a feasible core step with $g_k^Ts\le-n^{-1/2}\|q_k\|\|s\|$ whenever $q_k\ne0$ and the step length is small; a uniform $\delta$ (and, under the Strong Hypotheses, a $\sigma$) with $f(x_{k+1})\le f(x_k)-\sigma\|q(x_k)\|\|s_k\|$ when $\Delta_k<\delta$ and $\|q(x_k)\|>\eta$.
• Corollary 4.4 and Theorem 4.5: $\liminf\|q(x_k)\|\ne0$ keeps $\Delta_k$ bounded away from zero, whereas compactness alone forces $\liminf\Delta_k=0$.
• Theorem 3.2: $\liminf_k\|q(x_k)\|=0$.

Significance

Theorem 3.2 shows that a method which never computes a gradient still has a subsequence approaching first-order stationarity for the bound constrained problem, even though it cannot enforce a sufficient decrease condition measured by the projected gradient. Theorem 3.3 upgrades this to the whole sequence, so every limit point of the iterates is a KKT point. These results justify the bound constrained variants of coordinate search and Hooke–Jeeves discussed in §5 of the paper, and they are the template for the later theory of pattern search under linear constraints and generating set search.

The results are proved in the paper, and three of the milestones are proved in Torczon (1997). None of them has a machine-checked proof. Formalizing them produces a Lean model of generalized pattern search (patterns, exploratory moves, step-length updates) that later missions on direct search, mesh adaptive direct search or linearly constrained pattern search can reuse, and checks the details the paper handles briefly: the lattice argument, the feasibility of the chosen coordinate step, and uniform constants.

Difficulty

The obvious argument copies the unconstrained proof with $\nabla f$ replaced by $q$. The step that fails is the existence of a good trial step: in the unconstrained case some pattern direction makes an acute angle with $-\nabla f(x_k)$, but near the boundary of $\Omega$ that direction may leave the feasible region, and a feasible direction may not be a descent direction. For a general pattern no uniform choice exists, and the paper's counterexample in §5.2 shows convergence can fail. The diagonality of $BM_k$ is what makes the pattern contain coordinate directions, one of which is both feasible and a descent direction of quality $n^{-1/2}\|q_k\|$ (Proposition 4.2). The second difficulty is Theorem 4.5, which uses no derivatives: it rests on the rationality of $\tau$ and the integrality of the $C_k$, which confine the iterates to a lattice that meets the compact set $L_\Omega(x_0)$ in finitely many points.

Formalization scope

Points are EuclideanSpace ℝ (Fin n) with the Euclidean norm; the bounds are Fin n → EReal with the hypothesis $\ell_j<u_j$ for all $j$, so infinite bounds are allowed as in the paper. Paper coordinates $1,\dots,n$ are Lean's Fin n. The gradient is Mathlib's gradient f. A run of the method is a structure of sequences $(x_k,\Delta_k,s_k,M_k,L_k)$ together with a predicate IsGPSRun that encodes §2.1–§2.4 clause by clause; the parameter $m\ge1$ is the number of columns of $L_k$ (the paper's $p-2n$). $\tau$ is rational and the $C_k$ are integer matrices, as the lattice argument requires. "$\min\{f(x_k+y):\dots\}<f(x_k)$" over the finite set of feasible core trial points is encoded as "some feasible core trial step strictly decreases $f$". $\liminf$ statements are encoded with ∃ᶠ, not Filter.liminf. The modulus of continuity $\omega$ is not formed as a real supremum; Proposition 4.1 takes an explicit radius $\delta>\|d\|$.

Standing assumptions and every departure from the page:

1. Smoothness. The page assumes $f$ continuously differentiable on $L_\Omega(x_0)$. The mission assumes $f$ is $C^1$ on an open set $U\supseteq\Omega$. The proofs evaluate $\nabla f$ along segments to trial points that lie in $\Omega$ but generally outside $L_\Omega(x_0)$, and $L_\Omega(x_0)$ may have empty interior, so the page's hypothesis does not define what the proofs use.
2. Strong Hypothesis 3. The page prints $f(x_k+s_k)<\min\{\cdots\}$. No core step can satisfy the strict form, which would exclude coordinate search, which the paper says satisfies it. The mission uses $\le$, the form of Torczon (1997) and the one the proof of Proposition 4.3 uses. The theorem with $\le$ implies the one with $<$.
3. The nonemptiness of $\{w_1,\dots,w_L\}$ is made explicit.
4. Proposition 3.1 (7) is omitted: its $P(g(x))$ is a projected gradient the paper does not define.
5. Proposition 4.2 quantifies over every step length below $\nu_k$, because $\nu_k$ does not depend on $\Delta_k$.

The run predicate is not vacuous: an explicit run of coordinate search on $f(x)=x$ over $[0,\infty)$ satisfies IsGPSRun, the Strong Hypotheses, bounded columns, $\Delta_k\to0$ and compactness of $L_\Omega(x_0)$. That check is proved in Lean without sorry, so the goal cannot be closed by exhibiting an unsatisfiable hypothesis.

A complete development needs the mean value theorem along segments, uniform continuity of $\nabla f$ near the compact set $L_\Omega(x_0)$, finiteness of a discrete lattice inside a compact set, and elementary facts about the coordinatewise projection. The projection and lattice lemmas are reusable beyond this mission. Proofs of any milestone, alternative proofs, and a general statement of Proposition 3.1 for closed convex $\Omega$ are welcome.

Selected references

• R. M. Lewis and V. Torczon, Pattern Search Algorithms for Bound Constrained Minimization, ICASE Report No. 96-20 (NASA CR-198306), 1996; SIAM J. Optim. 9(4):1082–1099, 1999. https://doi.org/10.1137/S1052623496300507
• V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
• P. H. Calamai and J. J. Moré, Projected Gradient Methods for Linearly Constrained Problems, Math. Program. 39:93–116, 1987. https://doi.org/10.1007/BF02592073
• A. R. Conn, N. I. M. Gould and P. L. Toint, Global Convergence of a Class of Trust Region Algorithms for Optimization with Simple Bounds, SIAM J. Numer. Anal. 25(2):433–460, 1988. https://doi.org/10.1137/0725029
• R. Hooke and T. A. Jeeves, "Direct Search" Solution of Numerical and Statistical Problems, J. ACM 8(2):212–229, 1961. https://doi.org/10.1145/321062.321069