All missions

Motivation

Scattered subspaces are a central object of finite geometry. An $\mathbb F_q$-subspace $U$ of an $r$-dimensional vector space over $\mathbb F_{q^n}$ defines an $\mathbb F_q$-linear set of the projective space $\mathrm{PG}(r-1,q^n)$, and when $U$ is scattered this linear set has the largest possible number of points for its rank. Maximum scattered subspaces give rise to maximum rank distance (MRD) codes, to translation caps, and to two-intersection sets and the associated two-weight codes and strongly regular graphs (Polverino 2010; Sheekey–Van de Voorde 2020).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) generalised the notion to $h$-scattered subspaces, which meet every $h$-dimensional $\mathbb F_{q^n}$-subspace in dimension at most $h$, and proved that such a subspace has dimension at most $rn/(h+1)$ unless it defines a subgeometry. This mission concerns the extremal case: subspaces attaining $rn/(h+1)$, and the way they meet hyperplanes.

Timeline.

• 2000: Blokhuis and Lavrauw (Geom. Dedicata 81, Theorem 4.2) prove the case $h=1$: a scattered subspace of dimension $rn/2$ meets each hyperplane in dimension $rn/2-n$ or $rn/2-n+1$, and they count the hyperplanes of each kind.
• 2020: Csajbók, Marino, Polverino and Zullo prove the general statement (Theorem 2.7) by a double count and $q$-series identities, and use it to build maximum $h$-scattered subspaces by Delsarte duality.
• Later work by Zini and Zullo (Scattered subspaces and related codes, reference [29] of the paper) determines the number of hyperplanes of each intersection dimension for every $h$; the case $h=2$ is in Napolitano–Zullo.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, $n = [\mathbb F_{q^n}:\mathbb F_q]$, and let $V = V(r,q^n)$ be an $r$-dimensional vector space over $\mathbb F_{q^n}$, viewed also as an $rn$-dimensional vector space over $\mathbb F_q$. A hyperplane of $V$ is an $(r-1)$-dimensional $\mathbb F_{q^n}$-subspace.

Fix an integer $h$ with $0<h\le r-1$. An $\mathbb F_q$-subspace $U$ of $V$ is $h$-scattered if $\langle U\rangle_{\mathbb F_{q^n}} = V$ and every $h$-dimensional $\mathbb F_{q^n}$-subspace $S$ satisfies $\dim_{\mathbb F_q}(S\cap U)\le h$. It is maximum $h$-scattered if no $h$-scattered subspace of $V$ has larger $\mathbb F_q$-dimension.

Put $s=h+1$ and suppose $s\mid rn$. For an $\mathbb F_q$-subspace $U$ of dimension $rn/s$, let $h_i$ be the number of hyperplanes $W$ with $\dim_{\mathbb F_q}(W\cap U)=i$. The proof works with the Gaussian binomial coefficients $\left[{n\atop k}\right]_q$, the $q$-Pochhammer symbols $(a;q)_k=(1-a)(1-aq)\cdots(1-aq^{k-1})$, the elementary symmetric values $\sigma_{k,l}$ of $1,q,\dots,q^k$, and the sums

$$\alpha_k=\sum_i h_i(q^n-1)q^{ki},\qquad \beta_k=\sum_i h_i(q^n-1)\prod_{j=0}^{k-1}(q^i-q^j),$$ $$A=\sum_i h_i(q^n-1)\prod_{l=0}^{s-1}\bigl(q^i-q^{\,n(r-s)/s+l}\bigr).$$

Formalization targets

Goal: Theorem 2.7

If $U$ is a maximum $h$-scattered $\mathbb F_q$-subspace of $V(r,q^n)$ of dimension $rn/(h+1)$, then for every hyperplane $W$ of $V$

$$\frac{rn}{h+1}-n\;\le\;\dim_{\mathbb F_q}(U\cap W)\;\le\;\frac{rn}{h+1}-n+h.$$

Milestones, in the order of the proof (§5, pp. 20–24)

1. $h_i=0$ for $i<rn/s-n$ (the lower bound), and (23): $\sum_i h_i(q^n-1)=q^{rn}-1$.
2. Lemma 5.7: for $0\le k\le s-1$,

$$\sum_i h_i(q^n-1)\prod_{j=0}^{k}(q^i-q^j)=\prod_{j=0}^{k}(q^{rn/s}-q^j)\,(q^{(r-k-1)n}-1).$$

3. The $q$-series tools: Lemma 5.5 ($\sigma_{k,l}=q^{l(l-1)/2}\left[{k+1\atop l}\right]_q$), Carlitz's inversion (Theorem 5.6), the $q$-binomial theorem (Theorem 5.2) and its specialisation (Corollary 5.3).
4. (24): $\alpha_k=\sum_{j\le k}\left[{k\atop j}\right]_q\beta_j$. Identity (25), which expresses $A$ through $\alpha_0,\dots,\alpha_s$, is included as a supporting item rather than a milestone.
5. Propositions 5.8 and 5.9: two triple sums $a_s$, $b_s$ both equal $q^{nr}(-1)^s(q^{-n};q)_s$.
6. $A=0$, which forces $h_i=0$ for $i>n(r-s)/s+s-1$.

Significance

The result. Theorem 2.7 says that a maximum $h$-scattered subspace of dimension $rn/(h+1)$ has only $h+1$ possible intersection dimensions with hyperplanes. Its linear set therefore meets hyperplanes in few sizes, which links these subspaces to sets of few intersection numbers and to codes with few weights. Inside the paper, the upper bound is the input to §3: it shows that the Delsarte dual of a maximum $h$-scattered subspace of dimension $rn/(h+1)$ is maximum $(n-h-2)$-scattered (Theorem 3.3). That theorem in turn gives maximum $h$-scattered subspaces when $h+1$ does not divide $r$.

Formalizing it. The theorem is proved in the paper, but no machine-checked version exists. Beyond the geometry, the mission produces a library of finite $q$-series facts: Gaussian binomials as rational functions of $q$, the $q$-binomial theorem in both forms, Carlitz's inversion formula, and the elementary symmetric evaluation $\sigma_{k,l}$. Some of these are proved on the platform in a different Mathlib environment, but they are not available in this one. Counting statements about subspaces over finite fields (hyperplanes through a subspace, ordered independent tuples) are also needed and are reusable.

Difficulty

The lower bound is a dimension count. The upper bound is not: the obvious approach bounds $\dim(U\cap W)$ from the scattered property alone, but the $h$-scattered condition controls intersections with $h$-dimensional subspaces, and hyperplanes have dimension $r-1$, which is far larger. No pointwise argument is known; the paper determines the distribution $(h_i)$ only through its first $s+1$ moments, given by a double count, and then shows that a specific nonnegative combination of the $h_i$ vanishes. The moment identities hold only for $k\le s-1$ (Lemma 5.7 needs each $k+1\le h+1$ independent vectors of $U$ to stay independent over $\mathbb F_{q^n}$), and closing the argument requires exact evaluation of a triple $q$-series with signed Gaussian binomials and quadratic exponents.

Formalization scope

• $\mathbb F_q$ is a finite field F, $\mathbb F_{q^n}$ a finite field K with [Algebra F K], and $V$ a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V). We take $r=$ finrank K V, $n=$ finrank F K and $q=$ Fintype.card F.
• The range $0<h<r$ and the spanning condition are part of IsHScattered.
• "Dimension $rn/(h+1)$" is the equation $(h+1)\dim_{\mathbb F_q}U = rn$. Both bounds of Theorem 2.7 are stated with $n$ moved to the other side: $\dim U\le\dim(U\cap W)+n\le\dim U+h$. A version written with natural-number subtraction would make the lower bound vacuous whenever $rn/(h+1)<n$, and dropping the dimension hypothesis would make the upper bound false. Both trivialisations are ruled out.
• Gaussian binomials are defined by the product formula (15) for real $q$ and vanish for $k>n$. The $q$-identities are stated for real $q>1$, which covers every prime power. Carlitz's formula is stated for complex sequences.
• Every fraction in an exponent is an exact quotient: $rn/s$ is passed as $m$ with $sm=nr$, and halves $l(l-1)/2$ are binomial coefficients $\binom l2$. Possibly negative exponents use integer powers.
• The milestones of §5 carry the full $h$-scattered hypothesis, spanning included. The printed setting of §5.2 omits spanning, but Lemma 5.7 uses Proposition 2.1, which needs it.
• Cited inputs stated as milestones: Lemma 5.5 ([6]), Theorem 5.2 ([15]) and Theorem 5.6 ([7]). Identity (18) is used inside proofs and is not an item.

Proofs of any milestone, of standard counting facts for subspaces of finite vector spaces, and of the $q$-series lemmas are welcome.

Selected references

• B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, Combinatorica 41 (2021). arXiv:1906.10590v2. https://arxiv.org/abs/1906.10590v2
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
• O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2009.04.007
• J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://doi.org/10.1007/s10623-019-00703-z
• G. Gasper, M. Rahman, Basic Hypergeometric Series, 2nd ed., Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511526251
• L. Carlitz, Some inverse relations, Duke Math. J. 40 (1973), 893–901. https://doi.org/10.1215/S0012-7094-73-04083-0
• V. Napolitano, F. Zullo, Codes with few weights arising from linear sets, arXiv:2002.07241. https://arxiv.org/abs/2002.07241
• P. J. Cameron, Notes on Counting: An Introduction to Enumerative Combinatorics, Cambridge University Press, 2017. https://doi.org/10.1017/9781108277457

Motivation

A constraint satisfaction problem (CSP) asks whether variables ranging over a finite domain $D$ can be assigned values so that every constraint from a fixed finite list of relations is satisfied. A central organizing principle of the algebraic theory of CSPs is that the complexity of $\mathrm{CSP}(\Gamma)$ is governed by its polymorphisms, the functions $f : D^L \to D$ that preserve every relation of $\Gamma$ when applied coordinate-wise. For this principle to be usable, one needs to know which sets of functions arise as polymorphism sets. For ordinary relations this goes back to the Galois theory of clones and relations. Pippenger (Galois theory for minors of finite functions, Discrete Mathematics, 2002) characterized the families of functions that are the polymorphism sets of pairs of relations, allowing infinitely many pairs.

Promise constraint satisfaction problems (PCSPs) relax CSPs: every constraint comes as a pair $P \subseteq Q$, and the task is to distinguish instances satisfiable with the strong relations $P$ from those unsatisfiable even with the weak relations $Q$. Approximate graph colouring and $(2+\varepsilon)$-SAT are PCSPs. Brakensiek and Guruswami (arXiv:1704.01937v2, SIAM J. Comput. 2021) develop an algebraic theory of PCSPs based on polymorphisms. In §6.2 they prove a finite version of Pippenger's characterization: the families of the form $\mathrm{Pol}(\Gamma)$ for a finite family $\Gamma$ of promise relations are exactly the families satisfying three explicit conditions. This mission formalizes that theorem and its CSP analogue (§6.3).

Setting

Fix a finite set $D$. A family of functions $\mathcal F$ over $D$ consists, for every arity $L \ge 1$, of a set of functions $D^L \to D$.

A promise relation of arity $k$ is a pair $(P, Q)$ of subsets of $D^k$ with $P \subseteq Q$. A finite family $\Gamma = \{(P_i, Q_i)\}$ of promise relations is indexed by a finite set of relation symbols, each with its own arity $k_i$. A function $f : D^L \to D$ is a polymorphism of $\Gamma$ if for every $i$ and all $x^{(1)}, \dots, x^{(L)} \in P_i$, applying $f$ coordinate by coordinate gives a tuple in $Q_i$:

$$\bigl(f(x^{(1)}_1, \dots, x^{(L)}_1), \dots, f(x^{(1)}_{k_i}, \dots, x^{(L)}_{k_i})\bigr) \in Q_i.$$

$\mathrm{Pol}(\Gamma)$ is the family of all polymorphisms of $\Gamma$.

For $f : D^L \to D$ and a map $\pi : [L] \to [R]$, the projection (or minor) $f^\pi : D^R \to D$ is

$$f^\pi(y) = f(y_{\pi(1)}, \dots, y_{\pi(L)}).$$

A family $\mathcal F$ is projection-closed if $f^\pi \in \mathcal F$ whenever $f \in \mathcal F$ has arity $L$ and $\pi : [L] \to [R]$. It is finitizable if there is a finitized arity $R$ such that for every arity $L$ and every $f : D^L \to D$,

$$f \in \mathcal F \iff f^\pi \in \mathcal F \text{ for all } \pi : [L] \to [R].$$

Finally $\mathrm{id}_D : D \to D$ is the identity, a function of arity $1$.

Formalization targets

Goal: Theorem 6.5

$$\exists\, \Gamma \text{ finite with } \mathcal F = \mathrm{Pol}(\Gamma) \iff \mathcal F \text{ is projection-closed and finitizable, and } \mathrm{id}_D \in \mathcal F.$$

The finite family is existential together with its signature and arities; nothing about its shape is fixed in the statement.

Milestones

• Lemma 6.7. If $\mathcal F$ is projection-closed, finitizable and contains $\mathrm{id}_D$, then $\mathcal F = \mathrm{Pol}(\Gamma)$ for some finite $\Gamma$.

Further items for the other direction

• Claim 6.6. For every finite family $\Gamma$ of promise relations, $\mathrm{Pol}(\Gamma)$ is projection-closed and finitizable.
• §6.2, p. 29. Since $P \subseteq Q$ for every $(P, Q) \in \Gamma$, $\mathrm{id}_D \in \mathrm{Pol}(\Gamma)$.

Further item: Lemma 6.8

A CSP is a finite family with $P = Q$ for every pair. With $\mathcal F$ a clone (for $f \in \mathcal F$ of arity $L_1$ and $g_1, \dots, g_{L_1} \in \mathcal F$ of arity $L_2$, the function $h(x^{(1)}, \dots, x^{(L_1)}) = f(g_1(x^{(1)}), \dots, g_{L_1}(x^{(L_1)}))$ of arity $L_1L_2$ is in $\mathcal F$):

$$\exists\, \Lambda \text{ CSP with } \mathcal F = \mathrm{Pol}(\Lambda) \iff \mathcal F \text{ is finitizable, a clone, and } \mathrm{id}_D \in \mathcal F.$$

Significance

Theorem 6.5 identifies the polymorphism families of finite promise templates intrinsically, without reference to relations. Together with the Galois correspondence of §6.1 (if $\mathrm{Pol}(\Gamma) \subseteq \mathrm{Pol}(\Gamma')$ then $\Gamma'$ is definable from $\Gamma$, so $\mathrm{PCSP}(\Gamma')$ reduces to $\mathrm{PCSP}(\Gamma)$), it justifies studying PCSPs entirely through families of functions closed under minors, the viewpoint later systematized by the theory of minions (Barto, Bulín, Krokhin, Opršal, arXiv:1811.00970). Lemma 6.8 recovers, in the same language, the description of polymorphism clones of finite CSP templates as the finitely related clones.

The results are proved in the paper; to our knowledge none of them has a machine-checked proof. The mission produces a Lean formalization of both directions, built on the published definitions of relational structures and polymorphisms already used by other PCSP missions on the platform, and reusable definitions of projections (minors), projection-closed and finitizable families, and clones.

Difficulty

The arguments are elementary, and the difficulty lies in uniformity and finiteness. For Claim 6.6, a single arity $R$ must detect every failure of the polymorphism condition for functions of every arity $L$, so $R$ has to be bounded independently of $L$; an argument that handles each arity separately does not give finitizability. For Lemma 6.7, a finite family of promise relations has to be produced from $\mathcal F$ alone. The general Galois connection between functions and relations produces infinitely many relations (one for each arity and each witness of non-membership), and the content of the lemma is that the three conditions allow a finite family instead. In both directions the encoding matters: functions of arity $R$ must be compared with tuples of a relation, and coordinates, projections and the identity must be matched exactly, with no degenerate arity left over.

Formalization scope

A family of functions is FunFamily D := (L : ℕ) → Set ((Fin L → D) → D), with $D$ a finite type with decidable equality. Coordinates are 0-based (Fin L), and $f^\pi$ is fun y => f (y ∘ π) with π : Fin L → Fin R. A finite family of promise relations is a finite type τ of symbols with arities ar : τ → ℕ and two structures 𝔸 𝔹 : RelStruct τ ar D with 𝔸.rel R ⊆ 𝔹.rel R; polymorphisms are the published IsPolymorphism (definition PCSPBLPAff_Symmetric_Setting), and a CSP uses one structure on both sides.

All function arities are positive. The paper's "$L, R \in \mathbb N$" is read as positive integers: "$\mathcal F = \mathrm{Pol}(\Gamma)$" is compared at every arity $L \ge 1$, projection-closure and finitizability quantify over $L, R \ge 1$, and the finitized arity is at least $1$. Including arity $0$ would make the necessity direction false as stated (with every $P_i$ empty the paper's finitized arity is $0$).

The clone condition of Lemma 6.8 is the paper's displayed one (p. 30): $g_1, \dots, g_{L_1}$ act on disjoint blocks of inputs, and the composed function has arity $L_1 L_2$.

A trivializing formalization is ruled out by the statement's shape: the finite family, its signature and its arities are all existentially quantified (fixing a single relation would turn the necessity direction into a special case), $P \subseteq Q$ is part of every family (without it $\mathrm{id}_D \in \mathrm{Pol}(\Gamma)$ fails), and finitizability is an equivalence for every function, members and non-members alike.

The development needs only finite types and functions; no complexity theory is involved. Proofs of the milestones, and reusable lemmas about projections (composition of projections, projections along injective maps), are welcome.

Selected references

• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy, SIAM J. Comput. 50(6), 2021; arXiv:1704.01937v2. https://arxiv.org/abs/1704.01937
• N. Pippenger, Galois theory for minors of finite functions, Discrete Mathematics 254 (1–3), 2002 (cited as [48] in the paper).
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, J. ACM 68(4), 2021; arXiv:1811.00970. https://arxiv.org/abs/1811.00970

Motivation

Discrete optimal transport between two histograms is a linear program. Its feasible set, the transportation polytope, has been studied since Hitchcock (1941) and Kantorovich, and the structure of its vertices underlies the classical algorithms for the problem: the north-west corner rule produces a vertex, and the network simplex moves from vertex to vertex. A linear program with a nonempty bounded feasible set attains its minimum at a vertex, so knowing what vertices look like tells us what optimal transport plans can be assumed to look like.

This mission is the fourth of a series formalizing G. Peyré and M. Cuturi, Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019). It covers §3.4.1 of the book, Tree Structure of the Support of All Vertices of U(a, b) (pp. 405–407), whose single numbered result, Proposition 3.4, states that the support of a vertex is a forest. The book credits the result to Brualdi, Combinatorial Matrix Classes (2006, Theorem 8.1.2).

Setting

Fix integers $n, m$ and histograms $a \in \Sigma_n$, $b \in \Sigma_m$. The transportation polytope is

$$U(a,b) = \{ P \in \mathbb R_+^{n\times m} : P\mathbb 1_m = a,\ P^\top\mathbb 1_n = b \},$$

the set of nonnegative $n\times m$ matrices whose row sums are $a_1,\dots,a_n$ and whose column sums are $b_1,\dots,b_m$. Histograms are nonnegative and sum to one; $U(a,b)$ is the set of couplings between them. The cost of a plan $P$ for a cost matrix $C$ is $\langle C, P\rangle = \sum_{i,j} C_{ij}P_{ij}$.

A point $x$ of a set $S$ is an extremal point (vertex) of $S$ if, whenever $y, z \in S$ and $x = (y+z)/2$, necessarily $x = y = z$.

Take $n$ source nodes $V = \{1,\dots,n\}$ and $m$ target nodes $V' = \{1',\dots,m'\}$. The complete bipartite graph between them has the $nm$ edges $(i, j')$. For a matrix $P$, the support $S(P)$ is the set of edges $(i,j')$ with $P_{ij} > 0$, and the support graph is $G(P) = (V\cup V', S(P))$. A transport plan is a flow on the complete bipartite graph, with $a_i$ leaving node $i$ and $b_j$ entering node $j'$; $G(P)$ records the edges the flow actually uses.

Formalization targets

Goal: Proposition 3.4 (p. 406)

If $P$ is an extremal point of $U(a,b)$, then

$$G(P) \text{ has no cycles}\qquad\text{and}\qquad \#\{(i,j) : P_{ij}\ne 0\} \le n + m - 1 .$$

Milestones (proof of Proposition 3.4, p. 407)

1. If $G(P)$ has a cycle, there is a nonzero matrix $E$ with $E\mathbb 1_m = 0$, $E^\top\mathbb 1_n = 0$, and $E_{ij} \ne 0 \Rightarrow P_{ij} > 0$.
2. For such an $E$ and $P \in U(a,b)$, both $P + tE$ and $P - tE$ lie in $U(a,b)$ for some $t > 0$.
3. A graph with $k$ nodes and no cycles has at most $k-1$ edges.
4. For $P \ge 0$, the edges of $G(P)$ correspond one-to-one to the nonzero entries of $P$.

Companion (§3.4, p. 405)

For $a \in \Sigma_n$, $b \in \Sigma_m$ and any cost $C$, some minimizer of $\langle C, P\rangle$ over $U(a,b)$ is an extremal point of $U(a,b)$.

Significance

Proposition 3.4 is the sparsity statement of discrete optimal transport: a vertex of $U(a,b)$ moves mass along at most $n+m-1$ source–target pairs, out of $nm$ possible. With the companion, some optimal plan is that sparse. This is what makes the network simplex method a combinatorial algorithm on spanning trees of the bipartite graph (§3.5 of the book), and it is the reason the north-west corner rule (§3.4.2) can produce a feasible vertex with a tree support. The same fact, specialized to $n = m$ and uniform histograms, is one step on the way from Kantorovich's relaxation back to Monge's assignment problem.

The result is classical and proved; it has not, to our knowledge, been formalized. Mathlib has the transportation polytope only implicitly (no dedicated definition), and it has the edge count of trees (SimpleGraph.IsTree.card_edgeFinset) but not the corresponding bound for forests. The mission produces a machine-checked link between the convex geometry of $U(a,b)$ and the combinatorics of its support graph, reusable by later missions of the series on the network simplex and on the assignment problem.

Difficulty

The convex-geometric half is elementary; the work is in the passage between a cycle of a graph and a matrix. The cycle is an object of Mathlib's graph library (a closed walk with distinct vertices in a graph on $V \sqcup V'$), while the perturbation is a matrix indexed by $V \times V'$. An informal picture of a cycle as a list of edges hides what the matrix statement needs: each source and each target must be visited at most once, and Mathlib's cycles are walks whose distinctness conditions have to be carried to the matrix level.

The edge bound for forests is not packaged in Mathlib either: it counts the edges of a tree, a connected acyclic graph, while the support graph of a vertex is in general disconnected, and the empty graph must be handled.

Formalization scope

All objects live in the namespace CompOT.Vertices. Indices are Fin n and Fin m (0-based; the book's $[\![n]\!] = \{1,\dots,n\}$). Matrices are Matrix (Fin n) (Fin m) ℝ, and $U(a,b)$ is the set of matrices with nonnegative entries, row sums $a$ and column sums $b$. Extremality is the book's midpoint definition, relative to the set: the points $y, z$ in $x = (y+z)/2$ range over $U(a,b)$ only. This rules out the trivializing reading in which $y, z$ range over all matrices (no point would then be extremal and the goal would be vacuous); conversely, the sanity file shows a non-extremal coupling, so extremality is not automatic either.

The support graph is a SimpleGraph (Fin n ⊕ Fin m) with Sum.inl i adjacent to Sum.inr j exactly when $P_{ij} > 0$ and no other adjacencies. The book calls the edges $(i,j')$ directed, but the cycles of its proof alternate between sources and targets, so "no cycles" is Mathlib's SimpleGraph.IsAcyclic of this undirected graph. The number of nonzero entries is the cardinality of $\{(i,j) : P_{ij} \ne 0\}$.

The goal, feasibility milestone and companion carry $a \in \Sigma_n$, $b \in \Sigma_m$, the book's standing notation for histograms (p. 360). These hypotheses make the index sets nonempty, so natural-number subtraction in the bound $n+m-1$ agrees with the book's integer expression.

Useful infrastructure, reusable beyond this mission: the forest edge bound for finite simple graphs, and the correspondence between cycles of a bipartite graph and signed matrices with zero line sums. Contributions of either as standalone lemmas are welcome.

Selected references

• G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
• R. A. Brualdi, Combinatorial Matrix Classes, Cambridge University Press, 2006, §8.1. https://doi.org/10.1017/CBO9780511721182
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.7.
• F. L. Hitchcock, The distribution of a product from several sources to numerous localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224

Motivation

The convex feasibility problem asks for a point in the intersection of closed convex sets. It underlies signal and image reconstruction, phase retrieval relaxations, and the constraint handling inside larger optimization methods. The workhorse algorithms are projection methods: the method of alternating projections (MAP), going back to von Neumann for subspaces, and the Douglas–Rachford and Peaceman–Rachford splitting schemes, which can be applied to the indicator, distance or squared-distance functions of the sets.

Without a regularity condition on how the sets meet, projection methods can converge arbitrarily slowly. Bounded linear regularity, an error bound saying that a point close to every set is close to their intersection, is the standard condition under which linear rates are obtained (Bauschke and Borwein, SIAM Review, 1996, doi:10.1137/S0036144593251710). Section 5 of D. Davis and W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions (arXiv:1407.5210v3, Math. Oper. Res. 42(3), 2017) applies relaxed Peaceman–Rachford splitting (PRS) to the squared distance functions of two sets and proves that, under bounded linear regularity, the distance of the iterates to the intersection contracts by an explicit factor at every step, with step sizes and relaxation parameters allowed to vary between iterations. MAP is the special case of step size $1/2$ and relaxation $1$.

Setting

Let $\mathcal H$ be a real Hilbert space and $C_f, C_g \subseteq \mathcal H$ closed convex sets with $C_f\cap C_g\neq\emptyset$. For $C\subseteq\mathcal H$ the distance function is $d_C(x)=\inf_{y\in C}\|x-y\|$, and $P_C$ is the metric projection, the nearest point of $C$. The problem is modelled with

$$f(x)=d^2_{C_f}(x),\qquad g(x)=d^2_{C_g}(x).$$

For $\gamma>0$ the proximal map $\mathbf{prox}_{\gamma h}(x)$ is the minimiser of $h(y)+\frac1{2\gamma}\|y-x\|^2$, and the reflection is $\mathbf{refl}_{\gamma h}=2\,\mathbf{prox}_{\gamma h}-I$. With two step sizes, $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}=\mathbf{refl}_{\gamma_f f}\circ\mathbf{refl}_{\gamma_g g}$, and $(T)_\lambda=(1-\lambda)I+\lambda T$.

Given $z^0$, step sizes $\gamma_{f,k},\gamma_{g,k}>0$ and relaxation parameters $\lambda_k\in(0,1]$, iteration (5.1) is

$$x_g^k=\mathbf{prox}_{\gamma_{g,k}d^2_{C_g}}(z^k),\quad x_f^k=\mathbf{prox}_{\gamma_{f,k}d^2_{C_f}}(2x_g^k-z^k),\quad z^{k+1}=z^k+2\lambda_k(x_f^k-x_g^k).$$

The pair $\{C_f,C_g\}$ is boundedly linearly regular (Definition 5.1) if for every $\rho>0$ there is $\mu_\rho>0$ such that

$$d_{C_f\cap C_g}(x)\le\mu_\rho\max\{d_{C_f}(x),d_{C_g}(x)\}\qquad\text{for all }x\in B(0,\rho),$$

where $B(0,\rho)$ is the open ball. The rate function is

$$C(\gamma_f,\gamma_g,\lambda,\mu)=\left(1-\frac{4\lambda\min\{\gamma_g/(2\gamma_g+1)^2,\ \gamma_f/(2\gamma_f+1)^2\}}{\mu^2\max\{16\gamma_g^2/(2\gamma_g+1)^2,\ 1\}}\right)^{1/2}.$$

Formalization targets

Goal: Theorem 5.1

Suppose $\{C_f,C_g\}$ is boundedly linearly regular, $(z^k)$ is generated by (5.1), every $z^j$ lies in $B(0,\rho)$, and $d_{C_f\cap C_g}\le\mu_\rho\max\{d_{C_f},d_{C_g}\}$ on $B(0,\rho)$. Then for all $k\ge0$

$$d_{C_f\cap C_g}(z^{k+1})\le C(\gamma_{f,k},\gamma_{g,k},\lambda_k,\mu_\rho)\,d_{C_f\cap C_g}(z^k), \tag{5.3}$$

and if $\overline C=\sup_j C(\gamma_{f,j},\gamma_{g,j},\lambda_j,\mu_\rho)<1$, the iterates converge to a point $x\in C_f\cap C_g$ with

$$\|z^k-x\|\le 2\,d_{C_f\cap C_g}(z^0)\prod_{i=0}^{k-1}C(\gamma_{f,i},\gamma_{g,i},\lambda_i,\mu_\rho). \tag{5.4}$$

Milestones

The milestones follow the paper's own argument: Proposition 5.1 Parts 2 and 3 (the gradient of $d_C^2$ and the closed form $\mathbf{prox}_{\gamma d_C^2}=\frac1{2\gamma+1}I+\frac{2\gamma}{2\gamma+1}P_C$); Proposition 5.2, the fundamental inequality specialised to squared distances; Propositions C.1 and C.2 (the fixed-point set of $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}$ is $C_f\cap C_g$, and the iterates are Fejér monotone for $\lambda_k\in(0,1]$); and the displays (5.5)–(5.7), (5.8), (5.10) and (5.11) of the proof of Theorem 5.1, ending with the one-step contraction at a single point.

Companion: Corollary 5.1

With $\gamma_{f,k}\equiv\gamma_{g,k}\equiv\frac12$ and $\lambda_k\equiv1$, iteration (5.1) is MAP, $z^{k+1}=P_{C_f}P_{C_g}z^k$, and under the assumptions of Theorem 5.1 it contracts the distance to $C_f\cap C_g$ by $(1-1/\mu_\rho^2)^{1/2}$ from the second iterate on, converging linearly to a point of the intersection.

Significance

Theorem 5.1 gives an explicit, iteration-wise linear rate for relaxed PRS on the two-set feasibility problem with step sizes and relaxation parameters that may change from step to step. Its specialisation, Corollary 5.1, recovers linear convergence of MAP under bounded linear regularity with rate $(1-1/\mu_\rho^2)^{1/2}$, better than the $(1-1/(8\mu^2))^{1/2}$ derived in earlier work on cyclic projections. Remark 5.1 of the paper notes that Douglas–Rachford on indicator functions is a limiting case of the scheme as the step sizes grow, though the rate degenerates in that limit.

The results are proved in the paper; the proof of the convergence statement cites Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Theorem 5.12 (Fejér monotone sequences whose distance to a closed convex set decays converge strongly). No machine-checked proof of these statements was found on Prove2Me (search of 2026-10-07). A formalization produces a checked chain from the closed form of the prox of $d_C^2$ through the fundamental inequality to the linear rate, and with it reusable facts about squared distance functions, metric projections onto closed convex sets in Hilbert space, and Fejér monotone sequences.

Difficulty

The obvious argument would contract the distance to $C_f\cap C_g$ directly, but one PRS step measures only $d_{C_g}$ at $z$ and $d_{C_f}$ at the reflected point $\mathbf{refl}_{\gamma_g g}(z)$, never $d_{C_f}(z)$. Transferring the second distance back to $z$ costs a factor $\max\{c_1^2,1\}$ with $c_1=4\gamma_g/(2\gamma_g+1)$, and only after that does the regularity inequality turn $\max\{d_{C_f}(z),d_{C_g}(z)\}$ into $d_{C_f\cap C_g}(z)$. The fundamental inequality (5.2) itself rests on the prox-gradient calculus of the earlier sections, specialised to functions whose gradients $2(I-P_C)$ are Lipschitz. Passing from a contracting distance to convergence of the iterates to one point needs Fejér monotonicity and a completeness argument; a contracting distance alone does not give a limit.

Formalization scope

Everything lives in a real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); $d_C$ is Mathlib's Metric.infDist. The squared distance is viewed as an extended-real function so that the published proximal predicate ThreeOpSplitting.ConvexRates.IsProx applies, and prox maps are arbitrary maps satisfying it (unique here). Metric projections are maps satisfying the published RandomGradFree.Nonsmooth.IsMetricProjection. Step sizes and prox maps are indexed by the iteration. The hypotheses of the goal are: $C_f,C_g$ closed and convex with nonempty intersection; bounded linear regularity of the pair; $\gamma_{f,k},\gamma_{g,k}>0$; $\lambda_k\in(0,1]$; iterates in an open ball $B(0,\rho)$ on which the regularity inequality holds with $\mu_\rho>0$. The range $\lambda_k\in(0,1]$ is Algorithm 1's standing assumption, used in the proof but not restated in (5.1). The condition $\overline C<1$ is stated as a uniform bound $c<1$ on all rate factors. The product in (5.4) runs over $i=0,\dots,k-1$; the page prints the upper index $k$, which claims an extra factor that the proof does not give. In the proof's (5.9)–(5.10) the page swaps $\gamma_f$ and $\gamma_g$ relative to (5.2); the milestone states the pairing that (5.2) produces. Corollary 5.1's improved rate is stated for $k\ge1$, since it uses $z^k\in C_f$.

A trivializing formalization is ruled out: the goal mentions none of the proof's intermediate quantities, takes the prox maps as genuine minimisers of the squared-distance objective rather than chosen points, and measures distances to a nonempty intersection, so the junk value of infDist on the empty set never arises.

A complete development needs the closed form of $\mathbf{prox}_{\gamma d^2_C}$, differentiability of $d_C^2$, the fundamental inequality of the paper's §1 specialised to these functions, and the convergence theorem for Fejér monotone sequences. The last three are reusable well beyond this mission. Proofs of any milestone, and of Mathlib-level lemmas on metric projections, are welcome.

Selected references

• D. Davis, W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions, Mathematics of Operations Research 42(3), 2017; arXiv version used here: arXiv:1407.5210v3.
• H. H. Bauschke, J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38(3), 1996. doi:10.1137/S0036144593251710
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. doi:10.1007/978-1-4419-9467-7
• P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM Journal on Numerical Analysis 16(6), 1979. doi:10.1137/0716071