Combinatorics

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

Let $V$ be an $r$-dimensional vector space over the finite field $\mathbb F_{q^n}$. Viewed over the subfield $\mathbb F_q$, $V$ has dimension $rn$, and its one-dimensional $\mathbb F_{q^n}$-subspaces form the Desarguesian spread. An $\mathbb F_q$-subspace $U$ of $V$ is scattered if it meets every element of this spread in an $\mathbb F_q$-subspace of dimension at most one. Scattered subspaces define scattered $\mathbb F_q$-linear sets in $\mathrm{PG}(r-1,q^n)$. Through these linear sets they are connected to projective two-weight codes, strongly regular graphs and maximum rank distance (MRD) codes. In 2000 Blokhuis and Lavrauw proved that a scattered subspace has dimension at most $rn/2$, and a sequence of papers showed that this bound is attained whenever $2 \mid rn$.

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2; Combinatorica 41, 2021) replace the one-dimensional spread elements by all $h$-dimensional $\mathbb F_{q^n}$-subspaces. This gives a hierarchy of conditions, the $h$-scattered subspaces, that refines the scattered case. For $h = r-1$ and dimension $n$ these subspaces had already been identified with $\mathbb F_{q^n}$-linear MRD codes by Sheekey and Van de Voorde. This mission formalizes the paper's main theorem, the dimension bound for $h$-scattered subspaces.

Timeline.

• 2000: Blokhuis and Lavrauw, Scattered spaces with respect to a spread in PG(n, q), prove $\dim_{\mathbb F_q} U \le rn/2$ for scattered $U$ (the case $h = 1$).
• 2000–2018: Ball–Blokhuis–Lavrauw (2000), Blokhuis–Lavrauw (2000), Csajbók–Marino–Polverino–Zullo (2017) and Bartoli–Giulietti–Marino–Polverino (2018) together show that scattered subspaces of dimension $rn/2$ exist whenever $rn$ is even.
• 2020: Sheekey and Van de Voorde study subspaces scattered with respect to hyperplanes ($h = r-1$) and relate them to MRD codes.
• 2019–2021: Csajbók, Marino, Polverino and Zullo introduce $h$-scattered subspaces and prove the bound $rn/(h+1)$ for every $h$ (Theorem 2.3).

Setting

Let $\mathbb F_q \subseteq \mathbb F_{q^n}$ be finite fields, so $n = \dim_{\mathbb F_q}\mathbb F_{q^n}$, and let $V$ be a vector space over $\mathbb F_{q^n}$ of dimension $r$. Every $\mathbb F_{q^n}$-subspace of $V$ is also an $\mathbb F_q$-subspace. For an $\mathbb F_q$-subspace $U$ of $V$, $\langle U\rangle_{\mathbb F_{q^n}}$ denotes its $\mathbb F_{q^n}$-span.

Definition 1.1. Let $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$ of $V$ satisfies $\dim_{\mathbb F_q}(S\cap U) \le h$. In Lean this is HScattered.Bound.IsHScattered F K h U, with F $=\mathbb F_q$, K $=\mathbb F_{q^n}$, and $r$ = Module.finrank K V.

An $\mathbb F_q$-subspace $U$ defines a subgeometry of $\mathrm{PG}(V,\mathbb F_{q^n})$ if some $\mathbb F_q$-basis of $U$ is also an $\mathbb F_{q^n}$-basis of $V$ (HScattered.Construction.DefinesSubgeometry F K U, a definition shared with the other missions of this series). In coordinates, $U$ is then $\mathbb F_q^{\,r}$ inside $\mathbb F_{q^n}^{\,r}$.

A rank distance code of $\mathbb F_q^{n\times m}$, $n \le m$, is a set $\mathcal C$ of $\mathbb F_q$-linear maps from an $m$-dimensional to an $n$-dimensional $\mathbb F_q$-space, with distance $d(f,g) = \operatorname{rk}(f-g)$.

Formalization targets

Goal: Theorem 2.3

If $U$ is an $h$-scattered $\mathbb F_q$-subspace of $V$, then either $\dim_{\mathbb F_q}U = r$, $U$ defines a subgeometry and $U$ is $(r-1)$-scattered, or

$$\dim_{\mathbb F_q} U \le \frac{rn}{h+1}.$$

The disjunction is inclusive. The statement holds for every $h$ in the range $0 < h \le r-1$, including $h = 1$.

Milestones

• Proposition 2.1. For $h > 1$, an $h$-scattered subspace is $i$-scattered for every $0 < i < h$.
• Lemma 2.2. If $r \ge 2$ and $r \le i \le n$, then $V$ contains an $(r-1)$-scattered $\mathbb F_q$-subspace of dimension $i$.
• Result 4.6 (Delsarte). A rank distance code of $\mathbb F_q^{n\times m}$, $n\le m$, with minimum distance $d$ has $|\mathcal C| \le q^{m(n-d+1)}$.

Significance

The result. Theorem 2.3 is the upper end of the theory of $h$-scattered subspaces. It shows that the bound $rn/(h+1)$ decreases with $h$: a stronger intersection condition forces a smaller subspace. Every subspace reaching the bound is a maximum $h$-scattered subspace. The rest of the paper builds on such subspaces. Its constructions show the bound is sharp when $h+1 \mid r$. Its intersection numbers with hyperplanes lie in $[rn/(h+1)-n,\ rn/(h+1)-n+h]$. Its Delsarte-type duality sends maximum $h$-scattered subspaces to maximum $(n-h-2)$-scattered ones. Each of these statements presupposes the bound. For $h = r-1$, the bound $\dim U \le n$ is the geometric counterpart of the Singleton bound for MRD codes.

Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization would provide a Lean model of $h$-scattered subspaces over a field tower and a rank-metric Singleton bound, and the bound itself as a reusable lemma for the companion missions on constructions, hyperplane intersections and duality. The case $h = 1$ is attributed in the paper to Blokhuis–Lavrauw and is not reproved there, so a complete formal proof must also supply that case.

Difficulty

The obvious approach is to count. Every $h$-dimensional $\mathbb F_{q^n}$-subspace meets $U$ in at most $q^h$ vectors. But these subspaces overlap heavily, and a double count of incidences between vectors of $U$ and $h$-dimensional subspaces does not produce a bound of the form $rn/(h+1)$. The $h$-scattered condition must be used on subspaces of every dimension $t < h$ at once, which is the content of Proposition 2.1. The argument for $h = 1$ does not carry over directly either: the paper treats $h = r-1$, $1 < h < r-1$ with $n \ge h+1$, and $n < h+1$ as separate cases. The case $h = r-1$ rests on a coding-theoretic input (Result 4.6), and the middle case needs auxiliary subspaces whose existence (Lemma 2.2) holds only when $n \ge h+1$.

Formalization scope

• Field tower. $\mathbb F_q$ and $\mathbb F_{q^n}$ are finite fields F, K with [Algebra F K]. $V$ is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]). The parameters are $q$ = Fintype.card F, $n$ = Module.finrank F K and $r$ = Module.finrank K V.
• Subspaces. $\mathbb F_q$-subspaces are Submodule F V and $\mathbb F_{q^n}$-subspaces are Submodule K V. The intersection $S\cap U$ is S.restrictScalars F ⊓ U.
• The definition. The range $0 < h < r$ and the spanning condition $\langle U\rangle_{\mathbb F_{q^n}} = V$ are clauses of IsHScattered.
• No division. $rn/(h+1)$ never appears with division: "$\dim U \le rn/(h+1)$" is $(h+1)\dim U \le rn$ in $\mathbb N$.
• Result 4.6. The code is a Finset of linear maps. The minimum distance $d$ enters as a lower bound on all pairwise rank distances, with $1 \le d \le n$.
• Lemma 2.2. It carries $r \ge 2$, which Definition 1.1 forces for $(r-1)$-scattered subspaces.

Ruling out trivial readings. Without the range $h < r$, every spanning subspace would be "$h$-scattered" for $h \ge r$, and $U = V$ of dimension $rn$ would refute the goal. Without the spanning condition, $U = 0$ would satisfy the bound vacuously. Both conditions are part of the definition, and the goal is the inclusive disjunction for every $h$-scattered $U$.

Cited inputs. Result 4.6 is Delsarte's theorem [13], numbered in this paper and posed here with sorry. The case $h = 1$ of the goal is the Blokhuis–Lavrauw bound [4], which the paper cites without proof and says can be obtained by adapting its argument (Zullo's thesis [30]). It is not an item: a complete proof of the goal must cover it.

Infrastructure. A proof needs: dimension arithmetic for restriction of scalars in a tower; the rank–nullity theorem for $\mathbb F_q$-linear maps; the count of roots of a $q$-polynomial $\sum_j a_j x^{q^j}$, for Lemma 2.2; and a rank-metric Singleton bound. The Singleton bound and Lemma 2.2 are reusable beyond this mission. Contributions are welcome on any milestone, on the $h = 1$ case, and on the reduction for $n < h+1$.

Selected references

• B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, arXiv:1906.10590v2 (2020); Combinatorica 41 (2021). https://arxiv.org/abs/1906.10590v2
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81 (2000) 231–243. https://doi.org/10.1023/A:1005283806897
• P. Delsarte, Bilinear forms over a finite field, with applications to coding theory, J. Combin. Theory Ser. A 25 (1978) 226–241. https://doi.org/10.1016/0097-3165(78)90015-8
• J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Designs, Codes and Cryptography 88 (2020) 655–675. https://doi.org/10.1007/s10623-019-00703-z

Motivation

A promise constraint satisfaction problem $\mathrm{PCSP}(\mathbf A,\mathbf B)$ is given by two finite relational structures with a homomorphism $\mathbf A\to\mathbf B$. An instance is a third structure $\mathbf I$, and the task is to answer yes if $\mathbf I\to\mathbf A$ and no if $\mathbf I\not\to\mathbf B$; the promise is that one of the two holds. Approximate graph colouring (colour a $k$-colourable graph with $c\ge k$ colours) and the search for a not-all-equal assignment of a 1-in-3-satisfiable formula are of this form, and their complexity has been open since the 1970s and 2010s respectively.

For ordinary CSPs ($\mathbf A=\mathbf B$) the algebraic approach, in which the complexity is governed by the polymorphisms of the template, led to the classification of all finite-template CSPs (Bulatov 2017, Zhuk 2017). Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970, J. ACM 2021) extend that approach to promise problems. Their central structural result is Theorem 4.12: the existence of a minion homomorphism between polymorphism minions, which by their Theorem 3.1 yields a log-space reduction between the PCSPs, is characterized in five other ways, two of them purely relational.

Timeline:

• 1998: Jeavons shows that polymorphisms determine the complexity of $\mathrm{CSP}(\mathbf A)$, through a Galois correspondence between pp-definable relations and polymorphisms.
• 2002: Pippenger develops the Galois correspondence for pairs of sets that underlies the promise setting.
• 2016–2018: Brakensiek and Guruswami (arXiv:1704.01937) prove that $\mathrm{Pol}(\mathbf A,\mathbf B)\subseteq\mathrm{Pol}(\mathbf A',\mathbf B')$ yields a reduction for templates over the same domains.
• 2018: Barto, Opršal and Pinsker (arXiv:1510.04521) characterize pp-constructibility of CSP templates by minor-preserving maps of polymorphism clones.
• 2019: the present paper defines minion homomorphisms between polymorphism minions of promise templates and proves Theorem 4.12.

Setting

A signature is a finite set $\tau$ of relation symbols $R$ with arities $\mathrm{ar}(R)\ge1$. A structure $\mathbf A$ on a finite set $A$ gives a relation $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$ for each $R$; a homomorphism $h:\mathbf A\to\mathbf B$ maps every tuple of $R^{\mathbf A}$ into $R^{\mathbf B}$. A PCSP template is a pair $(\mathbf A,\mathbf B)$ of structures with the same signature and $\mathbf A\to\mathbf B$.

An $n$-ary polymorphism $f:A^n\to B$, $n\ge1$, applied coordinatewise to any $n$ tuples of $R^{\mathbf A}$, gives a tuple of $R^{\mathbf B}$. The minor of an $m$-ary $g$ given by $\pi:[m]\to[n]$ is $f(x_1,\dots,x_n)=g(x_{\pi(1)},\dots,x_{\pi(m)})$. A minion is a nonempty set of functions of positive arity closed under minors; $\mathrm{Pol}(\mathbf A,\mathbf B)$ is one. A minion homomorphism $\xi:\mathcal M\to\mathcal N$ preserves arities and satisfies $\xi(g(x_{\pi(1)},\dots,x_{\pi(m)}))=\xi(g)(x_{\pi(1)},\dots,x_{\pi(m)})$.

A bipartite minor condition is a finite set of identities $f(x_1,\dots,x_n)\approx g(x_{\pi(1)},\dots,x_{\pi(m)})$ between symbols from two disjoint sets; a minion satisfies it if the symbols can be assigned members of matching arity that make every identity true. For a structure $\mathbf A$ with $A=\{a_1,\dots,a_n\}$ and an instance $\mathbf I$, the condition $\Sigma(\mathbf A,\mathbf I)$ has an $n$-ary symbol $f_v$ per element $v$ of $\mathbf I$, an $|R^{\mathbf A}|$-ary symbol $g_C$ per constraint $C$, and one identity per position of each constraint, read off the list of tuples of $R^{\mathbf A}$. The free structure $F_{\mathcal M}(\mathbf A)$ has universe $\mathcal M^{(n)}$, and a tuple $(f_1,\dots,f_k)$ lies in its relation $R$ when all $f_i$ are minors of one $|R^{\mathbf A}|$-ary member of $\mathcal M$ in the pattern given by $R^{\mathbf A}$.

A pp-power $(\mathbf A',\mathbf B')$ of $(\mathbf A,\mathbf B)$ lives on $A^N$, $B^N$, each relation being defined in $\mathbf A$ and in $\mathbf B$ by one and the same primitive positive formula. A homomorphic relaxation $(\mathbf A',\mathbf B')$ of $(\mathbf A,\mathbf B)$ has homomorphisms $\mathbf A'\to\mathbf A$ and $\mathbf B\to\mathbf B'$. pp-constructibility is the closure under finitely many such steps.

Formalization targets

Goal: Theorem 4.12

For PCSP templates $(\mathbf A_i,\mathbf B_i)$ of finite structures and $\mathcal M_i=\mathrm{Pol}(\mathbf A_i,\mathbf B_i)$, the following are equivalent:

$$\begin{aligned} &(1)\ \exists\,\xi:\mathcal M_1\to\mathcal M_2 &&(4)\ F_{\mathcal M_1}(\mathbf A_2)\to\mathbf B_2\\ &(2)\ \mathcal M_1\models\Sigma\Rightarrow\mathcal M_2\models\Sigma\text{ for every bipartite }\Sigma &&(5)\ (\mathbf A_2,\mathbf B_2)\text{ relaxes a pp-power of }(\mathbf A_1,\mathbf B_1)\\ &(3)\ \mathcal M_2\models\Sigma(\mathbf A_2,F_{\mathcal M_1}(\mathbf A_2)) &&(6)\ (\mathbf A_2,\mathbf B_2)\text{ is pp-constructible from }(\mathbf A_1,\mathbf B_1). \end{aligned}$$

Milestones

In the order of the proof on p. 27: Lemma 4.8 (relaxations and pp-powers give minion homomorphisms) and Corollary 4.10 for (6) ⇒ (1); Lemma 4.3 ($\mathcal M\models\Sigma(\mathbf A,F_{\mathcal M}(\mathbf A))$) for (2) ⇒ (3); Lemma 3.14 for (3) ⇒ (4); Lemma 4.11 ($(\mathbf A_2,F_{\mathcal M_1}(\mathbf A_2))$ relaxes a pp-power of $(\mathbf A_1,\mathbf B_1)$) for (4) ⇒ (5). Lemma 4.4, the bijection between homomorphisms $F_{\mathcal M}(\mathbf A)\to\mathbf B$ and minion homomorphisms $\mathcal M\to\mathrm{Pol}(\mathbf A,\mathbf B)$, is included as an extra item.

Significance

Theorem 4.12 replaces a property of infinitely many functions, the existence of a minion homomorphism, by a homomorphism between two finite structures (item 4), which is decidable, and by a relational construction (items 5–6). The free-structure criterion is what bounds the arity of polymorphisms that a hardness proof must inspect, and the paper uses it to prove NP-hardness of $\mathrm{PCSP}(\mathbf K_k,\mathbf K_{2k-1})$ and to analyse the 1-in-3 versus not-all-equal problem. Later work on approximate graph and hypergraph colouring states its reductions in these terms.

The result is proved in the paper. As far as is known it has not been machine-checked: Mathlib has no minions, minor conditions, pp-formulas or pp-constructions. The mission produces a reusable Lean vocabulary for the algebraic theory of promise CSPs, together with a formal proof of the equivalence. The complexity consequences are not formalized.

Difficulty

Four of the implications are short once the definitions are fixed. The substantial step is (4) ⇒ (5), Lemma 4.11: a statement about the polymorphism minion, an object defined by infinitely many conditions, must be turned into a finite relational construction, and the relations of the pp-power have to be defined by one formula that is correct in $\mathbf A_1$ and in $\mathbf B_1$ at the same time. The indices involved, tuples over a power of $A_1$, coordinates indexed by $A_2$, and the enumeration of each $R^{\mathbf A_2}$, are where an informal reading leaves the most to check. Lemma 4.8(2) needs that polymorphisms preserve every pp-definable relation, a statement about arbitrary formulas, not only about the relations of the template. Corollary 4.10 is an induction over a sequence of templates whose signatures and domains change from step to step, which a formal statement cannot treat as a sequence in one fixed type.

Formalization scope

Structures, homomorphisms, templates and polymorphisms are the published PCSPBLPAff.Symmetric definitions (RelStruct, IsHom, IsPromiseTemplate, IsPolymorphism). All structures are finite with nonempty domains: domains carry Fintype, DecidableEq and Nonempty (nonemptiness is the field's standing convention, which the paper uses when it identifies a domain with $[n]$; without it items (4) and (5) of the goal are not equivalent). The goal and Lemma 4.11 also assume that every relation of $\mathbf A_2$ is nonempty; the paper does not say so, but if $R^{\mathbf A_2}=\emptyset$ then $R^{F_{\mathcal M_1}(\mathbf A_2)}=\emptyset$, and when $\mathbf B_1$ has an element on which every relation holds constantly no pp-power can have an empty relation, so (4) ⇒ (5) fails, signatures are Fintype, arities are positive, minions in Lemmas 4.3–4.4 live on finite sets. Theorem 4.12 is stated only for finite templates, as in the paper (p. 46 notes that it fails for infinite ones). Minions have no nullary members. A minion homomorphism is a family of maps on the members $\mathcal M^{(n)}\to\mathcal N^{(n)}$, so it cannot be made trivial by values outside the minion. Bipartite minor conditions have finite symbol and identity types in Type; item (2) quantifies over all of them. $\Sigma(\mathbf A,\mathbf I)$ and $F_{\mathcal M}(\mathbf A)$ take the enumeration of $A$ and of each $R^{\mathbf A}$ as explicit equivalences; the paper's identification $A=[n]$ is one such choice. A pp-power uses one formula for both structures, with free variables indexed by $[k]\times[N]$. Templates are bundled for pp-constructibility, which is an inductive predicate.

The goal is the six-way equivalence (List.TFAE) and not any of its trivial fragments; the goal cannot be closed by choosing degenerate enumerations, because every statement quantifies over all of them.

Not formalized: the log-space reductions of Theorems 3.1 and 3.12, Remark 3.11's reduction between promise minor-condition problems, and the cited Theorem 2.25 [Pip02, BG16b]. Contributions are welcome on general facts that are reusable beyond this mission: polymorphisms preserve pp-definable relations, composition of minion homomorphisms, and the natural minion homomorphism $\mathcal M\to\mathrm{Pol}(\mathbf A,F_{\mathcal M}(\mathbf A))$.

Selected references

• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, J. ACM 68(4), 2021; arXiv:1811.00970v3. https://arxiv.org/abs/1811.00970
• L. Barto, J. Opršal, M. Pinsker, The wonderland of reflections, Israel J. Math. 223, 2018. https://arxiv.org/abs/1510.04521
• J. Brakensiek, V. Guruswami, Promise constraint satisfaction: structure theory and a symmetric Boolean dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• N. Pippenger, Galois theory for minors of finite functions, Discrete Math. 254, 2002. https://doi.org/10.1016/S0012-365X(01)00297-7
• P. Jeavons, On the algebraic structure of combinatorial problems, Theoret. Comput. Sci. 200, 1998. https://doi.org/10.1016/S0304-3975(97)00230-2

Approximate graph colouring

Given a graph that is promised to be $k$-colourable, how many colours are needed to find a proper colouring in polynomial time? The decision version asks to distinguish $k$-colourable graphs from graphs that are not even $c$-colourable. It has been studied since Garey and Johnson (1976) and is conjectured to be NP-hard for all fixed $3 \le k \le c$. This is the approximate graph colouring problem, and it is one of the motivating examples of promise constraint satisfaction problems (PCSPs).

Timeline of the NP-hardness results without extra assumptions, as surveyed in Example 2.9 and §6.2 of the paper:

• 2000–2004, Khanna–Linial–Safra and Guruswami–Khanna: 3 versus 4 colours.
• 2013, Huang (cited as [Hua13] in the paper): $k$ versus $2^{\Omega(k^{1/3})}$ colours for large $k$.
• 2016, Brakensiek–Guruswami: $k$ versus $2k - 2$ colours for every $k \ge 3$, via polymorphisms.
• 2018/2019, Barto–Bulín–Krokhin–Opršal (this paper): $k$ versus $2k - 1$ colours for every $k \ge 3$, in particular 3 versus 5. The argument is an instance of a general algebraic theory of PCSPs.

The method also applies to the question of 5-cycle versus 3-colouring, which Brakensiek and Guruswami had raised as an open case.

Setting

A relational structure $\mathbf A$ consists of a finite domain $A$ and relations $R^{\mathbf A} \subseteq A^{\mathrm{ar}(R)}$, one for each symbol $R$ of a signature. A PCSP template is a pair $(\mathbf A, \mathbf B)$ of structures with the same signature and a homomorphism $\mathbf A \to \mathbf B$. Write $E_k = \{0, \dots, k-1\}$.

• $\mathbf K_k = (E_k; \neq_k)$ is the complete graph: one binary relation $\{(a, b) \mid a \ne b\}$.
• $\mathbf H_k = (E_k; \mathrm{NAE}_k)$ carries the ternary not-all-equal relation $E_k^3 \setminus \{(a, a, a)\}$; $\mathrm{PCSP}(\mathbf H_k, \mathbf H_c)$ is approximate colouring of 3-uniform hypergraphs.

An $n$-ary polymorphism from $\mathbf A$ to $\mathbf B$ is a map $f : A^n \to B$ that, applied coordinatewise to any $n$ tuples of $R^{\mathbf A}$, returns a tuple of $R^{\mathbf B}$. For $\mathbf K_k$ and $\mathbf K_c$ these are exactly the $c$-colourings of the power $\mathbf K_k^n$. The set $\mathrm{Pol}(\mathbf A, \mathbf B)$ of polymorphisms of all arities $n \ge 1$ is closed under minors: $f(x_1, \dots, x_n) = g(x_{\pi(1)}, \dots, x_{\pi(m)})$ for $\pi : [m] \to [n]$. A minion is any nonempty set of functions of arities $n \ge 1$ that is closed under minors. A minion homomorphism $\xi : \mathscr M \to \mathscr N$ preserves arities and commutes with minors. Write $\mathscr H_K = \mathrm{Pol}(\mathbf H_2, \mathbf H_K)$.

An Olšák function is a 6-ary function $o$ with

$$o(x, x, y, y, y, x) = o(x, y, x, y, x, y) = o(y, x, x, x, y, y) \quad \text{for all } x, y .$$

The free structure $\mathbf F_{\mathscr M}(\mathbf A)$ has the $|A|$-ary members of $\mathscr M$ as its domain and relations defined by minor identities that follow the tuples of $\mathbf A$.

Formalization targets

Goal: the algebraic core of Theorem 6.5

For every $k \ge 3$,

$$\exists\, K \ge 2:\quad \text{there is a minion homomorphism } \mathrm{Pol}(\mathbf K_k, \mathbf K_{2k-1}) \to \mathrm{Pol}(\mathbf H_2, \mathbf H_K).$$

$K$ is left unspecified, as in the paper. This is the statement from which the paper deduces that $k$ versus $2k - 1$ colouring is NP-hard.

Milestones

1. Example 3.5: the Olšák minor condition is not satisfied in $\mathscr H_k$ for any $k \ge 2$.
2. Lemma 4.4: homomorphisms $\mathbf F_{\mathscr M}(\mathbf A) \to \mathbf B$ correspond one-to-one to minion homomorphisms $\mathscr M \to \mathrm{Pol}(\mathbf A, \mathbf B)$.
3. Theorem 6.2: for a minion $\mathscr M$ on finite sets,

$$\bigl(\exists K \ge 2,\ \exists\ \text{minion homomorphism } \mathscr M \to \mathscr H_K\bigr) \iff \mathscr M \text{ contains no Olšák function}.$$

4. Lemma 6.4: $\mathrm{Pol}(\mathbf K_k, \mathbf K_{2k-1})$ contains no Olšák function, $k \ge 3$.

One further item, not a milestone, shows the bound is sharp. Proposition 10.1 says that $\mathrm{Pol}(\mathbf K_k, \mathbf K_{2k})$ contains an Olšák function.

Significance

Theorem 6.2 is a criterion stated entirely inside the minion. Together with the reduction theory of the paper (a minion homomorphism $\mathrm{Pol}(\mathbf A, \mathbf B) \to \mathrm{Pol}(\mathbf A', \mathbf B')$ gives a log-space reduction from $\mathrm{PCSP}(\mathbf A', \mathbf B')$ to $\mathrm{PCSP}(\mathbf A, \mathbf B)$) and the NP-hardness of approximate hypergraph colouring (Dinur, Regev and Smyth 2005), it shows that every finite template without an Olšák polymorphism has an NP-hard PCSP (Corollary 6.3). Lemma 6.4 then settles the 3 versus 5 colouring case and improves the $2k - 2$ bound to $2k - 1$ for every $k \ge 3$. Proposition 10.1 shows that this criterion cannot go beyond $2k - 1$.

The results are proved in the paper. None of them has a machine-checked proof that this mission knows of. This mission produces a Lean statement of the minion side of the argument. That includes the free-structure correspondence (Lemma 4.4), which every later application of the theory uses, and Theorem 6.2 for arbitrary finite minions. A finished formalization would include the clique argument behind Lemma 6.4 and would check the key hardness inequality $c \ge 2k - 1$ of the paper by machine.

Difficulty

Lemma 6.4 is a statement about every $(2k-1)$-colouring of $\mathbf K_k^6$ that is constant on certain triples of vertices. The power graph has $k^6$ vertices, so exhaustive search is out of reach for general $k$, and case checks for $k = 3$ do not give the general claim. Showing that $2k - 1$ colours do not suffice requires an explicit obstruction, uniform in $k$, in the graph obtained by identifying those triples; the identification creates edges that are not present in $\mathbf K_k^6$, and keeping track of them is the combinatorial core. The bound is tight (Proposition 10.1), so no argument that would also apply to $2k$ colours can work.

In Theorem 6.2 the direction from "no Olšák function" to a minion homomorphism must build a minion homomorphism into $\mathscr H_K$ out of nothing but the absence of a single identity. That direction depends on Lemma 4.4, which relates maps defined on functions of a single arity to minion homomorphisms defined on all arities; in Lean the bookkeeping of enumerations, minors and dependent arities is substantial.

Formalization scope

The development reuses the published relational-structure layer PCSPBLPAff_Symmetric_Setting (RelStruct, IsHom, IsPolymorphism, IsPromiseTemplate). Domains $E_k$ are Fin k. $\mathbf K_k$ and $\mathbf H_k$ have one-symbol signatures of arity 2 and 3. Polymorphisms apply $f$ to the columns of an $n \times \mathrm{ar}(R)$ matrix whose rows lie in $R^{\mathbf A}$, which is the paper's matrix transposed. A minion is a family mem n of $n$-ary functions (Fin n → A) → B with no nullary members, nonempty and closed under the minors fun x => g (x ∘ π). A minion homomorphism is a family of maps that preserves membership and minors on members, with unconstrained values outside the minion, so Lemma 4.4's "one-to-one" is stated up to agreement on the minion. Theorem 6.2 assumes the minion's sets are finite, which is the paper's standing convention (Definition 2.20). The free structure takes an enumeration $e : \mathrm{Fin}\ n \simeq A$ of the generating domain and quantifies the enumeration of each relation existentially. In the goal, $k \ge 3$ makes $2k - 1$ free of natural-number truncation.

The codomain of the goal is exactly $\mathrm{Pol}(\mathbf H_2, \mathbf H_K)$ with $K \ge 2$. A minion homomorphism into an arbitrary or existentially chosen minion, or into $\mathscr H_K$ with $K \le 1$, would be trivial and is ruled out by the statement.

Not formalized. The NP-hardness conclusions of Theorem 6.5 and Corollary 6.3 are left out, and so are the log-space reduction of Theorem 3.1 and the cited hardness of approximate hypergraph colouring (Theorem 5.23, [DRS05]). There is no complexity-theoretic substrate in Mathlib for them. Lemma 6.6 ($\mathrm{Pol}(\mathbf C_5, \mathbf K_3)$) is a natural follow-up item. Contributions are welcome on every milestone. Lemma 4.4 and the minion layer can be reused beyond this mission, for any minion-homomorphism argument in the PCSP literature.

Selected references

• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, arXiv:1811.00970v3, 2019; J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970v3
• J. Brakensiek, V. Guruswami, New hardness results for graph and hypergraph colorings, CCC 2016. https://doi.org/10.4230/LIPIcs.CCC.2016.14
• I. Dinur, O. Regev, C. Smyth, The hardness of 3-uniform hypergraph coloring, Combinatorica 25(5), 2005. https://doi.org/10.1007/s00493-005-0032-4
• M. Olšák, The weakest nontrivial idempotent equations, Bull. London Math. Soc. 49(6), 2017. https://doi.org/10.1112/blms.12097
• S. Khanna, N. Linial, S. Safra, On the hardness of approximating the chromatic number, Combinatorica 20(3), 2000. https://doi.org/10.1007/s004930070013

Motivation

A promise constraint satisfaction problem (PCSP) is given by a pair of relational structures $(\mathbf A,\mathbf B)$ with a homomorphism $\mathbf A\to\mathbf B$: an instance is promised to be satisfiable in $\mathbf A$, and it suffices to satisfy it in $\mathbf B$. The paper of Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970v3) develops the algebraic theory of PCSPs, in which the complexity of $\mathrm{PCSP}(\mathbf A,\mathbf B)$ is governed by its polymorphisms.

The most prominent example is 1-in-3 versus Not-All-Equal-SAT: given a system of ternary constraints that has an assignment making exactly one variable in each constraint true, find an assignment making the variables in each constraint not all equal. Brakensiek and Guruswami (arXiv:1704.01937) showed that this problem is solvable in polynomial time, although both 1-in-3-SAT and NAE-SAT are NP-complete on their own. Their algorithm, like every tractability result for PCSPs known when the paper was written, works by finding a tractable CSP template $\mathbf C$ with $\mathbf T\to\mathbf C\to\mathbf H_2$ (a "sandwich") and solving the CSP over $\mathbf C$. For 1-in-3 vs NAE the template used is infinite: the integers with the relation $x+y+z=1$.

Section 8 of the paper shows that this is unavoidable: no finite tractable template can be sandwiched, or more generally pp-constructed, in this way. This separates PCSPs from CSPs: infinite domains are necessary in the sandwich method.

Timeline: Feder and Vardi conjectured the CSP dichotomy (1998); Barto and Kozik characterised the borderline by cyclic polymorphisms (BK12, 2012); Bulatov and Zhuk proved the dichotomy (arXiv:1703.03021, arXiv:1704.01914, 2017); Brakensiek and Guruswami proved 1-in-3 vs NAE tractable (2018); Barto, Bulín, Krokhin and Opršal proved Theorem 8.1 (2019).

Setting

All structures here have one ternary relation. For a set $D$ and $R\subseteq D^3$, $(D;R)$ is the structure with domain $D$ and relation $R$. The 1-in-3 structure is $\mathbf T=(\{0,1\};\{(1,0,0),(0,1,0),(0,0,1)\})$ and the not-all-equal structure is $\mathbf H_2=(\{0,1\};\{0,1\}^3\setminus\{(0,0,0),(1,1,1)\})$.

A homomorphism $h:(A;R_A)\to(B;R_B)$ is a map with $(h(a),h(b),h(c))\in R_B$ whenever $(a,b,c)\in R_A$. A polymorphism of $(D;R)$ of arity $p$ is a map $s:D^p\to D$ such that, applied coordinatewise to any $p$ triples from $R$, it yields a triple in $R$. An operation $s:D^p\to D$ is cyclic if $s(a_1,a_2,\dots,a_p)=s(a_2,\dots,a_p,a_1)$ for all $a\in D^p$ (Definition 8.2).

The proof of Theorem 8.1 works in the following situation: $D$ is finite, $f:\mathbf T\to(D;R)$ and $g:(D;R)\to\mathbf H_2$ are homomorphisms, $p>60|D|$ is a prime and $s$ is a cyclic polymorphism of $(D;R)$ of arity $p$. From $s$ it builds the $p^2$-ary operation

$$t(X)=s\big(s(x_{11},\dots,x_{p1}),\dots,s(x_{1p},\dots,x_{pp})\big)$$

on $p\times p$ matrices $X=(x_{ij})$, and studies zero-one matrices, evaluated in $D$ through $f$: their area $\lambda(X)$ (the fraction of ones), $g$-equivalence $X\sim Y\iff g(t(X))=g(t(Y))$, tameness ($X\sim 0_{p\times p}$ with $\lambda(X)<1/3$, or $X\sim 1_{p\times p}$ with $\lambda(X)>1/3$), covers (three matrices with exactly one $1$ in each position), the line segments $\langle i\rangle$ (ones in the first $i$ positions in row-major order), and almost rectangles $[k,\dots,k,l,\dots,l]$ (columns of heights $k$ then $l$, with step $0\le k-l\le 5|D|$).

Formalization targets

Goal: the algebraic core of Theorem 8.1

$$\mathbf T\xrightarrow{f}(D;R)\xrightarrow{g}\mathbf H_2,\ \ D\text{ finite},\ \ p\text{ prime},\ p>60|D|\ \Longrightarrow\ (D;R)\text{ has no cyclic polymorphism of arity }p.$$

Milestones, in proof order

1. Lemma 8.7: the three matrices of a cover are not all $g$-equivalent.
2. Lemma 8.8: $t$ is cyclic in its $p^2$ row-major arguments.
3. Lemma 8.9: with $p^2=3q+1$, $\langle 0\rangle\sim\cdots\sim\langle q\rangle\not\sim\langle q+1\rangle\sim\cdots\sim\langle 2q+1\rangle$.
4. Lemma 8.10: every $\langle i\rangle$, $0\le i\le p^2$, is tame, and $0_{p\times p}\not\sim 1_{p\times p}$.
5. Proposition 8.12: every almost rectangle is tame.
6. §8.4: there are $l_1<l_2$ in $(p/3-2|D|,\,p/3)$ with $s(1^{l_1}0^{p-l_1})=s(1^{l_2}0^{p-l_2})$.

Significance

Combined with the theorem of Barto and Kozik (a finite CSP template whose CSP is not NP-complete has cyclic polymorphisms of every prime arity $p>|D|$) and with the paper's Theorem 4.12, the core yields Theorem 8.1: if $(\mathbf T,\mathbf H_2)$ is pp-constructible from a finite $\mathbf D$, then $\mathrm{CSP}(\mathbf D)$ is NP-complete. Hence the polynomial-time algorithm for 1-in-3 vs NAE cannot come from any finite tractable CSP, and the infinite template of Brakensiek and Guruswami is necessary. It is a concrete separation between PCSPs and CSPs: a tractable PCSP that is not explained by any finite tractable CSP.

The theorem is proved in the paper; nothing in this section has a machine-checked proof. The mission produces a formal proof of the combinatorial core, a reusable definition of cyclic operations on top of the platform's polymorphism library, and the matrix calculus of §8 (areas, covers, $t$), which is the part of the argument where index conventions are easiest to get wrong.

Difficulty

Polymorphisms of $(D;R)$ are not determined by their values on zero-one inputs, and nothing beyond cyclicity is known about $s$. The obvious attempt, to show directly that $s$ restricted to $\{f(0),f(1)\}$ depends only on the number of ones, fails: this property does not follow from cyclicity (Remark 8.15 asks whether polymorphisms of that kind always exist, and it is open). The only information available about $s$ is the coarse two-valued invariant $g(t(\cdot))$ on zero-one matrices, and the contradiction has to be produced from that invariant alone, uniformly over all finite $D$; the margin $p>60|D|$ is what keeps the areas involved away from $1/3$.

Formalization scope

Structures are instances of the published PCSPBLPAff.Symmetric.RelStruct with the single-symbol signature Unit of arity $3$; homomorphisms and polymorphisms are the published IsHom and IsPolymorphism. The domain $\{0,1\}$ is Fin 2; $D$ is a Fintype with decidable equality. Matrices are functions Fin p → Fin p → Fin 2, row index first; the $p^2$ arguments of $t$ are read row-major via finProdFinEquiv; areas are rationals. Cyclicity is s a = s (a ∘ finRotate p), the paper's $(a_2,\dots,a_p,a_1)$. The paper renames $D$ so that $f(0)=0$, $f(1)=1$; the formalization keeps $f$ and evaluates zero-one matrices through it. Definition 8.11 prints column heights $1\le k_i\le p$, but its proofs use height $0$, so heights range over $0\le k_i\le p$.

Lemmas 8.7–8.10 are stated with only the hypotheses their proofs use (Lemma 8.8 needs only cyclicity; Lemmas 8.9–8.10 need $p>3$ prime rather than $p>60|D|$). Lemmas 8.13 and 8.14 concern a minimal counterexample inside the proof of Proposition 8.12 and are not separate items.

Left out: the NP-completeness conclusion of Theorem 8.1; the reduction from pp-constructibility to a homomorphic relaxation (Theorem 4.12, mission 1 of this series); the fact that a pp-power of a finite tractable CSP template is a finite tractable CSP template; and the cited Theorem 8.3 [BK12], which is never assumed or stated.

The goal ends in False, so it would be trivial if its hypotheses were contradictory for a reason unrelated to $s$. They are not: $D=\{0,1\}$, $R$ the 1-in-3 relation, $f=g=\mathrm{id}$ satisfies every hypothesis except the existence of $s$. No restriction is placed on $s$ beyond being a cyclic polymorphism; assuming idempotence or dependence on counts only would assume away the content (Remark 8.15).

Contributions welcome: proofs of the milestones, a general library of cyclic operations and their compositions, and a formalization of Theorem 8.3 or of the pp-power step, which would turn the core into Theorem 8.1 itself.

Selected references

• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, arXiv:1811.00970v3, 2019; J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970
• L. Barto, M. Kozik, Absorbing subalgebras, cyclic terms, and the constraint satisfaction problem, Logical Methods in Computer Science 8(1:07), 2012. https://doi.org/10.2168/LMCS-8(1:7)2012
• J. Brakensiek, V. Guruswami, Promise constraint satisfaction: structure theory and a symmetric Boolean dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• A. Bulatov, A dichotomy theorem for nonuniform CSPs, FOCS 2017. https://arxiv.org/abs/1703.03021
• D. Zhuk, A proof of the CSP dichotomy conjecture, FOCS 2017; J. ACM 67(5), 2020. https://arxiv.org/abs/1704.01914

Small complete caps in Galois spaces

A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.

Counting the lines through pairs of points gives the trivial lower bound

$$\sqrt{2} \cdot \sqrt{q^{n-1}} \qquad (1)$$

for the size of a complete cap in a Galois space of dimension $n$ and order $q$. A short timeline:

• Segre (1959) constructed complete caps of size $3q + 2$ in $PG(3, q)$, $q$ even.
• Pambianco and Storme (1996) generalized this to complete caps of size $2q^s$ in $AG(2s+1, q)$, $q$ even: bound (1) is sharp up to a constant in odd dimension, for even $q$.
• Giulietti (2007) studied translation caps in $AG(r, 2^t)$ and the doubling construction, which turns a translation cap of the largest possible size into a complete cap one dimension higher.
• Bartoli, Giulietti, Marino and Polverino (arXiv 2015, Combinatorica 2017) proved that (1) is sharp up to a constant also in even dimension $n \ge 4$, when $q$ is an even square. This mission formalizes that result.

Setting

Let $q = 2^t$ and let $\mathbb F_q$ be the field with $q$ elements. The affine space $AG(r, q)$ has as points the vectors $(a_1, \dots, a_r) \in \mathbb F_q^r$; three points are collinear when they lie on a common affine line over $\mathbb F_q$.

For an additive subgroup $G$ of $\mathbb F_q^r$, $\mathcal K_G$ is the set of points whose coordinate vectors lie in $G$. A translation cap is a cap of the form $\mathcal K_G$. By Giulietti, Proposition 2.5, for $t > 1$ a translation cap has at most $q^{r/2}$ points; one attaining this bound is a maximal translation cap.

On the projective side, let $V = \mathbb F_{2^t}^r$, so that $PG(V, \mathbb F_{2^t}) = PG(r-1, 2^t)$. An $\mathbb F_2$-subspace $U$ of $V$ (an additive subgroup) of $\mathbb F_2$-dimension $k$, the rank, defines the $\mathbb F_2$-linear set $L_U = \{\langle u \rangle_{\mathbb F_{2^t}} : u \in U \setminus \{0\}\}$. It is scattered when every point $\langle u\rangle$ meets $U$ in exactly $\{0, u\}$, i.e. has weight one. A scattered linear set has rank at most $rt/2$ (Blokhuis–Lavrauw); one of rank $3t/2$ in the plane $PG(2, 2^t)$ is called maximum.

Formalization targets

Goal: Theorem 1.3

For $q = 2^t$, $t$ even, and $n \ge 4$ even, there is a complete cap $S$ in $AG(n, q)$ with

$$|S| = 2\sqrt{q^{n-1}}.$$

The exponent $t(n-1)/2$ is an integer because $t$ is even.

Milestones

1. Theorem 4.2 ([6, Lemma 2.1]): for $q$ even, $\mathcal K_G$ is a translation cap iff any two distinct non-zero vectors of $G$ are $\mathbb F_q$-linearly independent.
2. Proposition 4.3: for $t > 1$, $L_U$ is a scattered $\mathbb F_2$-linear set of $PG(r-1, 2^t)$ iff $\mathcal K_U$ is a translation cap of $AG(r, 2^t)$.
3. The bound of [6, Prop. 2.5]: a translation cap in $AG(r, 2^t)$, $t > 1$, has at most $q^{r/2}$ points.
4. Lemma 4.5 ([6, Prop. 2.8]): the product of maximal translation caps in $AG(r, 2^t)$ and $AG(\bar r, 2^t)$ is a maximal translation cap in $AG(r + \bar r, 2^t)$.
5. The parabola $\{(x, x^2) : x \in \mathbb F_{2^t}\}$ is a translation cap in $AG(2, 2^t)$.
6. Lemma 4.6 (doubling, [6, Cor. 2.12]): if $\mathcal K_G$ is a maximal translation cap in $AG(r, 2^t)$, then $\mathcal K_{G \times \{0,1\}}$ is a complete cap in $AG(r+1, 2^t)$.
7. Proposition 4.7: a maximum scattered linear set in $PG(2, q)$ yields a complete cap in $AG(n, q)$ of size $2q^{(n-1)/2}$.
8. The existence input, restated from Section 2: Lemma 2.8 and Proposition 2.9 (a suitable coefficient $b$), Theorem 2.10 (the scattered $\mathbb F_2$-linear set $\{x^2 + bx^{2^{2n+1}} + x\omega\}$ of rank $3n$ in $PG(2, 2^{2n})$, covering $t = 2n \ge 4$), and the Baer-subplane case $r = 3$, $t = 2$ (covering $q = 4$).

Significance

Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor $\sqrt 2$ in even dimension $n \ge 4$ for every even square $q$, extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in $PG(n, q)$. The proof also establishes Proposition 4.3, a dictionary between scattered $\mathbb F_2$-linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.

The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].

Difficulty

Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of $AG(r+1, q)$ outside $\mathcal K_{G\times\{0,1\}}$ lies on a secant, which uses the maximality $|G| = q^{r/2}$ in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in $PG(2, 2^t)$ is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over $\mathbb F_{2^{3n}}$. A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.

Formalization scope

• $AG(r, q)$ is Fin r → K for a finite field $K$ with $|K| = 2^t$; collinearity is Mathlib's affine Collinear K, over $K$ itself. A complete cap is quantified against every point of $AG(r, q)$.
• Sizes are Set.ncard. The goal's size $2\sqrt{q^{n-1}}$ is written $2\cdot 2^{t(n-1)/2}$ with natural-number division, exact because $t$ is even; maximality of a translation cap is the squared form $|S|^2 = q^r$, and the [6] bound is $|S|^2 \le q^r$.
• Scattered-ness is the weight-one condition "$c\,u \in U$, $c \in \mathbb F_{2^t}$, $u \ne 0$ imply $c \in \mathbb F_2$"; rank $k$ means $|U| = 2^k$. "Maximum" in Proposition 4.7 is read as rank $3t/2$, as in the first line of its proof.
• In Section 2, $\mathbb F_{2^m}$ is the fixed field of $x \mapsto x^{2^m}$ inside $E$ with $|E| = 2^{6n}$; norms are explicit Frobenius products. $\omega$ ranges over all of $\mathbb F_{2^{2n}} \setminus \mathbb F_{2^n}$ (the paper's standing $\omega$). Proposition 2.9 carries the standing assumption $n \ge 2$ of Section 2.
• Lemmas 4.5, 4.6 and the [6] bound carry $t > 1$; for $t = 1$ every subset of $AG(r, 2)$ is a cap and Lemma 4.6 fails.
• Ruled out: stating the goal with $\le$ or $\ge$ in place of the exact size, or measuring collinearity over $\mathbb F_2$ (over which every set is a cap), would make it trivial.
• Citation basis: arXiv:1512.07467v1; all theorem numbers and pages refer to that version.

Welcome contributions: a general library of caps and translation caps in $AG(r, q)$; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the $\mathbb F_{2^{6n}}$-model of Theorem 2.10 to coordinates $\mathbb F_{2^{2n}}^3$. The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.

Selected references

• D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1, 2015; Combinatorica 37 (2017). arXiv:1512.07467v1
• [3] 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
• [6] M. Giulietti, Small complete caps in PG(N, q), q even, J. Combin. Des. 15(5) (2007), 420–436. https://doi.org/10.1002/jcd.20131
• [7] M. Giulietti, The geometry of covering codes: small complete caps and saturating sets in Galois spaces, in Surveys in Combinatorics 2013, LMS Lecture Note Series 409, Cambridge University Press, 2013, pp. 51–90. https://doi.org/10.1017/CBO9781139506748.003
• [17] F. Pambianco, L. Storme, Small complete caps in spaces of even characteristic, J. Combin. Theory Ser. A 75(1) (1996), 70–84. https://doi.org/10.1006/jcta.1996.0064
• [19] B. Segre, On complete caps and ovaloids in three-dimensional Galois spaces of characteristic two, Acta Arith. 5 (1959), 315–332. https://doi.org/10.4064/aa-5-3-315-332
• [20] G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82. https://doi.org/10.1006/ffta.1995.1005