Algebra

Motivation

A constraint satisfaction problem (CSP) asks for an assignment of values from a finite domain $D$ to variables so that every constraint, a tuple of variables required to lie in a fixed relation, is satisfied. The algebraic theory of CSPs rests on a Galois correspondence: the complexity of $\mathrm{CSP}(\Gamma)$ is determined by the set $\mathrm{Pol}(\Gamma)$ of its polymorphisms, because $\mathrm{Pol}(\Gamma) \subseteq \mathrm{Pol}(\Gamma')$ holds exactly when every relation of $\Gamma'$ is definable from $\Gamma$ by a primitive positive formula (Geiger 1968; Bodnarčuk, Kalužnin, Kotov and Romov 1969), and such definitions translate into reductions (Jeavons 1998). This correspondence underlies the CSP dichotomy theorem.

Promise CSPs (PCSPs) relax a CSP by a promise: every constraint comes as a pair $(P, Q)$ with $P \subseteq Q$, and the task is to tell instances satisfiable with the $P$-relations from instances not even satisfiable with the $Q$-relations. Approximate graph colouring and $(2+\varepsilon)$-SAT are examples. Brakensiek and Guruswami (arXiv:1704.01937v2, §6.1) showed that the Galois correspondence survives this generalisation, with pp-definitions replaced by positive primitive promise definitions (ppp-definitions). This is the starting point of the algebraic approach to PCSPs later systematised by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970). Pippenger (2002) had earlier proved a variant of the correspondence for pairs of relations, not in this complexity-theoretic form.

Setting

Fix a finite domain $D$. A relation of arity $k$ is a set $P \subseteq D^k$, and a promise relation is a pair $(P, Q)$ of relations of arity $k$ with $P \subseteq Q$. A family $\Gamma = \{(P_R, Q_R) : R \in \tau\}$ is indexed by a set $\tau$ of symbols with arities $k_R$. In Lean it is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar D, with $P_R$ = 𝔸.rel R, $Q_R$ = 𝔹.rel R and $P_R \subseteq Q_R$ (IsPromiseFamily).

A function $f : D^L \to D$ is a polymorphism of $\Gamma$ if for every $R$ and all $x^{(1)}, \dots, x^{(L)} \in P_R$ the tuple obtained by applying $f$ coordinate-wise, $\big(f(x^{(1)}_1, \dots, x^{(L)}_1), \dots, f(x^{(1)}_{k_R}, \dots, x^{(L)}_{k_R})\big)$, lies in $Q_R$. $\mathrm{Pol}(\Gamma)$ is the set of polymorphisms of all arities $L \ge 0$.

A $\Gamma$-PCSP $\Psi$ is a finite list of clauses, each a symbol $R$ applied to a tuple of variables, with repetition allowed. It is read twice: as $\Psi_P$, with each clause asking its tuple to lie in $P_R$, and as $\Psi_Q$, with $Q_R$ in place of $P_R$. Let $\mathrm{EQUAL} = \{(i, i) : i \in D\}$.

Definition (ppp-definability). A promise relation $(P', Q') \subseteq D^k \times D^k$ is ppp-definable from a finite family $\Gamma$ if there are $\ell \ge 0$ and a $\Gamma \cup \{\mathrm{EQUAL}\}$-PCSP $\Psi$ on $k + \ell$ variables such that

1. every $x \in P'$ extends by some $y \in D^\ell$ to an assignment $(x, y)$ satisfying $\Psi_P$;
2. every assignment $z$ satisfying $\Psi_Q$ has $(z_1, \dots, z_k) \in Q'$.

A family $\Gamma'$ is ppp-definable from $\Gamma$ if each of its promise relations is.

Formalization targets

Goal: Theorem 6.1, algebraic core

For a finite family $\Gamma$ and a family $\Gamma'$ over the same finite domain,

$$\mathrm{Pol}(\Gamma) \subseteq \mathrm{Pol}(\Gamma') \;\Longrightarrow\; \text{every } (P', Q') \in \Gamma' \text{ is ppp-definable from } \Gamma.$$

The printed Theorem 6.1 concludes a polynomial-time reduction from $\mathrm{PCSP}(\Gamma')$ to $\mathrm{PCSP}(\Gamma)$. Its proof opens by reducing to the displayed statement, and the reduction follows from it by substituting gadgets.

Milestones

1. Sandwich remark (p. 27). If $P' \subseteq P \subseteq Q \subseteq Q'$ (same arity), then $(P', Q')$ is ppp-definable from $\{(P, Q)\}$.
2. Transitivity (p. 27). If $\Gamma'$ is ppp-definable from $\Gamma$ and $(P'', Q'')$ from $\Gamma'$, then $(P'', Q'')$ is ppp-definable from $\Gamma$.
3. Proposition 6.3 (p. 28). For $L \ge 1$, the promise relation $(S_L, T_L)$ is ppp-definable from $\Gamma$, where $S_L = \{f : D^L \to D : f \in \mathrm{Pol}(P, P)\ \forall (P,Q) \in \Gamma\}$, $T_L = \{f : f \in \mathrm{Pol}(P, Q)\ \forall (P,Q) \in \Gamma\}$, and each $f$ is read as the vector of its $|D|^L$ values.
4. $(S'_m, T'_m)$ from $(S_m, T_m)$ (p. 28). For $y^1, \dots, y^k \in D^m$, the projections $S'_m = \{(f(y^1), \dots, f(y^k)) : f \in S_m\}$ and $T'_m$ (likewise) are ppp-definable from $\{(S_m, T_m)\}$.
5. The chain (p. 28). If $\mathrm{Pol}(\Gamma) \subseteq \mathrm{Pol}(\Gamma')$, $(P', Q') \in \Gamma'$, $m = |P'|$, $x^1, \dots, x^m$ enumerate $P'$ and $y^i_j = x^j_i$, then $P' \subseteq S'_m \subseteq T'_m \subseteq Q'$.

Significance

The result. Theorem 6.1 shows that the complexity of $\mathrm{PCSP}(\Gamma)$ depends only on $\mathrm{Pol}(\Gamma)$: two finite families with the same polymorphisms have polynomial-time equivalent PCSPs. Hardness can then be read off from the absence of structured polymorphisms, and tractability from their presence. The paper's Boolean symmetric dichotomy (its Theorem 2.16) is organised in exactly this way, and the theorem justifies studying families of polymorphisms instead of families of relations. Section 6.2 of the paper, which characterises the sets of functions of the form $\mathrm{Pol}(\Gamma)$, is its companion.

Formalizing it. The result and its proof are published, and no machine-checked version is known to exist. This mission produces a reusable definition of ppp-definability for promise families over arbitrary finite domains, built on the published relational-structure vocabulary PCSPBLPAff_Symmetric_Setting. It also produces the closure properties (weakening, transitivity) any later work on gadget reductions between PCSPs will need, and the encoding of the polymorphism relation $(S_L, T_L)$ as a gadget. The complexity-theoretic conclusion, a polynomial-time reduction, is not part of the mission.

Difficulty

The printed proofs are short, but each hides a construction. Transitivity requires substituting a gadget for every clause of an intermediate PCSP: the auxiliary variables of all gadgets are renamed apart, and EQUAL clauses are carried through unchanged. Proposition 6.3 requires one clause for every symbol $R$ and every $L$-tuple of elements of $P_R$, indexed by the finite set of such tuples and laid out on the $|D|^L$ coordinates of $f$. The goal must handle $P' = \emptyset$ (so $m = 0$, nullary functions, and $D^0$ with one point), where Proposition 6.3 as printed ($L \ge 1$) does not apply. A tempting shortcut is to read the hypothesis $\mathrm{Pol}(\Gamma) \subseteq \mathrm{Pol}(\Gamma')$ only for arities $L \ge 1$. With that reading the theorem is false: for $\Gamma = \{(D, D)\}$ and $\Gamma' = \{(\emptyset, \emptyset)\}$, both unary, every function of positive arity is a polymorphism of both families, yet constant assignments satisfy every $\Psi_Q$, so $(\emptyset, \emptyset)$ is not ppp-definable.

Formalization scope

• Domain and families. $D$ is a finite type with decidable equality, and $\Gamma$ is 𝔸 𝔹 : RelStruct τ ar D with [Fintype τ] and IsPromiseFamily 𝔸 𝔹. $\Gamma'$ is a promise family over any signature τ', possibly infinite; the conclusion is stated relation by relation.
• Polymorphisms. IsPolymorphism from the published setting file. PolSubset quantifies over every arity L : ℕ, including $L = 0$. This convention makes the goal true, and no hypothesis $P' \neq \emptyset$ is added.
• PCSPs with EQUAL. A $\Gamma \cup \{\mathrm{EQUAL}\}$-PCSP is an Instance over the signature τ ⊕ Unit, whose new symbol has arity 2 and is EQUAL in both readings. The same clause list is read in withEqual 𝔸 (as $\Psi_P$) and in withEqual 𝔹 (as $\Psi_Q$). PPPDefinable requires Ψ.n = k + ℓ. The first $k$ variables are Fin.castAdd ℓ, and $(x, y)$ is Fin.append x y. The two clauses of the definition keep the paper's quantifiers: existence of an extension on the $P$ side, and every satisfying assignment on the $Q$ side. A formalization with two independent instances, or with both readings in $P$, would trivialise the notion and is excluded.
• Functions as tuples. A set of functions $D^L \to D$ becomes a relation of arity Fintype.card (Fin L → D) through any bijection e. The statements hold for every such ordering.
• Out of scope. The polynomial-time (and log-space) reduction of the printed Theorem 6.1, its constant-factor blow-up, and all complexity classes. No PolyTime predicate or placeholder is introduced.
• Welcome contributions. Proofs of the milestones. Reflexivity of ppp-definability, which is not stated here. The $L = 0$ case of Proposition 6.3. The converse direction of the correspondence (ppp-definability implies polymorphism inclusion). Reconciliation with the pp-definability of Barto–Bulín–Krokhin–Opršal (their Definition 2.24), where the two relations are defined by one pp-formula read in two structures.

Selected references

• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy, SIAM J. Comput. 50(6), 2021; cited here from arXiv:1704.01937v2. https://arxiv.org/abs/1704.01937
• P. Jeavons, On the algebraic structure of combinatorial problems, Theoretical Computer Science 200, 1998. https://doi.org/10.1016/S0304-3975(97)00230-2
• D. Geiger, Closed systems of functions and predicates, Pacific J. Math. 27(1), 1968. https://doi.org/10.2140/pjm.1968.27.95
• N. Pippenger, Galois theory for minors of finite functions, Discrete Mathematics 254, 2002. https://doi.org/10.1016/S0012-365X(01)00297-7
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970

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

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

Motivation

Linear sets are the main tool for building point sets with few intersection sizes in finite projective spaces: sets meeting every hyperplane, two-intersection sets, translation ovoids, and the geometric side of finite semifields and rank-metric codes (Polverino, 2010). Among them, scattered linear sets are those whose points all carry the smallest possible weight, and a scattered linear set of the largest possible rank is called maximum scattered. By Blokhuis and Lavrauw (2000), a maximum scattered linear set of $\mathrm{PG}(r-1,q^t)$ of rank $rt/2$ is a two-intersection set with respect to hyperplanes, so each one yields a two-weight code and a strongly regular graph.

Timeline.

• 2000, Blokhuis–Lavrauw: the rank of a scattered $\mathbb F_q$-linear set of $\mathrm{PG}(r-1,q^t)$ is at most $rt/2$, and for $r$ even this bound is attained.
• 2000, Ball–Blokhuis–Lavrauw: examples of rank $6$ in $\mathrm{PG}(2,q^4)$.
• Classical: for $r=3$, $t=2$ the bound $3$ is attained by Baer subplanes.
• 2000, Blokhuis–Lavrauw, Thm 4.4: existence (without explicit examples) for $r>3$, $t=2$, $q=2$ and for $r\ge3$, $(t-1)\mid r$, $t$ even, $q>2$.
• 2015, Bartoli, Giulietti, Marino and Polverino (arXiv:1512.07467v1, Combinatorica 37 (2017)): three explicit families in $\mathrm{PG}(2,q^{2n})$ and, by direct sums, maximum scattered linear sets in $\mathrm{PG}(r-1,q^t)$ for $t$ even in three families of $(q,t)$. This mission formalizes that result; the companion mission formalizes the paper's application to complete caps.

Setting

Let $q$ be a prime power, $t\ge1$, and let $V$ be an $r$-dimensional vector space over $\mathbb F_{q^t}$; $\mathrm{PG}(V,\mathbb F_{q^t})=\mathrm{PG}(r-1,q^t)$ has as points the spans $\langle v\rangle_{\mathbb F_{q^t}}$ of nonzero $v\in V$. An $\mathbb F_q$-subspace $U\subseteq V$ is a subset closed under addition and under multiplication by $\mathbb F_q$. It defines the $\mathbb F_q$-linear set

$$L_U=\{\langle u\rangle_{\mathbb F_{q^t}} : u\in U\setminus\{0\}\},$$

whose rank is $\dim_{\mathbb F_q}U$. A linear set comes paired with $U$, so every statement here is about $U$. The weight of a point $\langle v\rangle$ is $\dim_{\mathbb F_q}(\langle v\rangle_{\mathbb F_{q^t}}\cap U)$, and $L_U$ is scattered when every point of $L_U$ has weight $1$; equivalently, for every nonzero $u\in U$,

$$\lambda\in\mathbb F_{q^t},\ \lambda u\in U\ \Longrightarrow\ \lambda\in\mathbb F_q .$$

The plane construction (§2). Fix $n\ge2$ and the field $E=\mathbb F_{q^{6n}}$ with its subfields $\mathbb F_q\subseteq\mathbb F_{q^n}\subseteq\mathbb F_{q^{2n}}$ and $\mathbb F_{q^{3n}}$. As an $\mathbb F_{q^{2n}}$-space $E$ has dimension $3$, so $\mathrm{PG}(E,\mathbb F_{q^{2n}})=\mathrm{PG}(2,q^{2n})$. For $\omega\in\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$ and an $\mathbb F_q$-linear $f:\mathbb F_{q^{3n}}\to\mathbb F_{q^{3n}}$ the paper studies

$$U_f=\{f(x)+x\omega : x\in\mathbb F_{q^{3n}}\},$$

with $f$ a monomial $ax^{q^i}$ or a binomial $f_{i,a,b}(x)=ax^{q^i}+bx^{q^{2n+i}}$. The relative norms $N_{q^m/q^d}(x)=\prod_{j<m/d}x^{q^{dj}}$ enter the hypotheses.

Formalization targets

Goal: Theorem 1.2 (p. 3)

For $t$ even and $r\ge2$, in each of the cases (a) $q=2$, $t\ge4$; (b) $t\not\equiv0\pmod3$; (c) $q\equiv1\pmod3$, $t\equiv0\pmod3$,

$$\exists\,U\subseteq\mathbb F_{q^t}^{\,r}\ \ \mathbb F_q\text{-subspace}:\qquad \dim_{\mathbb F_q}U=\frac{rt}{2},\quad L_U\ \text{scattered}.$$

Milestones, in proof order

• Proposition 2.1 (p. 5): $U_f$ has rank $3n$, and $L_{U_f}$ is scattered iff $Q_f\cap\mathbb F_{q^{2n}}=\mathbb F_q$, where $Q_f$ is the set of quotients $\frac{f(x)+x\omega}{f(y)+y\omega}$, $y\ne0$.
• Proposition 2.2 (p. 6): the same criterion through the polynomial system (5)–(6).
• Theorems 2.3, 2.4 (pp. 7, 9): the monomial families, for $n\not\equiv0\pmod 3$ and for $q\equiv1\pmod3$.
• Theorem 2.5 (p. 10): existence in $\mathrm{PG}(2,q^{2n})$ in those two regimes.
• Lemma 2.6 (p. 11): $\varphi(x)/x$ and $\bar\varphi(x)/x$ have the same image, where $\bar\varphi$ is the trace adjoint.
• Proposition 2.7, Lemma 2.8, Proposition 2.9, Theorem 2.10 (pp. 12–16): the binomial family for $q=2$.
• Theorem 3.1 (p. 16): direct sums of scattered linear sets are scattered, of rank $rt/2$ iff each summand has rank $s_it/2$.
• The line example (p. 2, cited from Lavrauw's thesis) and the Baer-subplane case $r=3$, $t=2$ (p. 3).

Significance

Theorem 1.2 gives maximum scattered linear sets, and hence two-intersection sets, two-weight codes and strongly regular graphs, for infinitely many $(q,t)$ with $r$ odd, a regime where earlier existence results covered only a few values of $t$. The $q=2$ case feeds the paper's second main result: scattered $\mathbb F_2$-linear sets of $\mathrm{PG}(2,2^t)$ of rank $3t/2$ are translation caps, from which complete caps of size $2\sqrt{q^{\,n-1}}$ in $\mathrm{AG}(n,q)$ are built.

All statements are proved in the preprint; none has a machine-checked proof. Formalizing them requires a usable theory of subfields of a finite field as Frobenius fixed fields, relative norms and their images, linearized polynomials and their trace adjoints, and the passage between $\mathbb F_q$-dimension, cardinality and weight. Each of these is reusable for later work on linear sets, MRD codes and semifields.

Difficulty

The criterion of Proposition 2.2 reduces scatteredness to a polynomial system, but the system has to be solved for a specific $f$. For the monomials this rests on the solvability of $z^{q^i-1}=c$ in $\mathbb F_{q^{3n}}$, a norm condition interacting with the gcd hypotheses. For the binomial with $q=2$, the existence of a suitable $b$ (Lemma 2.8) needs a value-set bound for non-permutation polynomials (Turnwald, 1995) and a point count on a plane curve. The higher-dimensional statement then needs the elementary bound $\dim U\le st/2$ for scattered $U$ to obtain the rank equivalence in Theorem 3.1. A tempting shortcut, taking $U=\mathbb F_q^{\,r}$ or any small subspace, is scattered but has the wrong rank; the content is in the rank $rt/2$.

Formalization scope

• Citation basis. arXiv:1512.07467v1; page numbers equal PDF pages.
• Fields. $\mathbb F_{q^m}\subseteq E$ is the fixed field of $x\mapsto x^{q^m}$ in a finite field $E$ of characteristic $p$ with $|E|=q^{6n}$, $q=p^h$. Norms and traces are explicit Frobenius products and sums.
• Subspaces and rank. An $\mathbb F_q$-subspace is a carrier set with closure conditions. Rank $k$ is $|U|=q^k$; in Theorem 3.1 rank $rt/2$ is $|W|^2=q^{rt}$.
• Points. Scatteredness takes the spanning field as an argument: $\mathbb F_{q^{2n}}$ in §2, the whole $\mathbb F_{q^t}$ in Theorem 1.2 and §3. $\mathrm{PG}(r-1,q^t)$ is modelled on Fin r → K; the plane of §2 on $E$ itself.
• Pinned readings.
  • Theorem 1.2 prints no range for $r$. The preceding sentence and the proof (p. 17) say $r\ge5$, and $r=1$ is false. The goal assumes $r\ge2$, covered by the line example ($r=2$), §2 with the Baer case ($r=3$) and Theorem 3.1 ($r\ge4$).
  • $\omega$ is quantified over all of $\mathbb F_{q^{2n}}\setminus\mathbb F_{q^n}$.
  • The index ranges $1\le i\le3n-1$ (monomial) and $2n+i\le3n-1$ (binomial) come from the case headings on pp. 7 and 10.
  • Proposition 2.7's printed "$wx$" is $\omega x$.
  • Theorem 2.10 keeps its printed hypothesis $N_{2^{3n}/2^n}(b)\ne1$.
  • Theorem 3.1's rank clause assumes $t\ge2$; for $t=1$ it is false.
• Ruled out. Taking the span over $E$ or over $\mathbb F_q$, or dropping the rank, would make the statements false or trivial; every existence statement fixes the rank, and the span field is explicit.
• Contributions welcome. Frobenius-fixed-field cardinalities, norm surjectivity, the criteria of Propositions 2.1–2.2, the monomial and binomial families, and the direct-sum rank computation.

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). https://arxiv.org/abs/1512.07467, https://doi.org/10.1007/s00493-016-3531-6
• 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.2010.04.007
• S. Ball, A. Blokhuis, M. Lavrauw, Linear (q + 1)-fold blocking sets in PG(2, q⁴), Finite Fields Appl. 6 (2000), 294–301.
• M. Lavrauw, Scattered Spaces with respect to Spreads and Eggs in Finite Projective Spaces, Ph.D. thesis, TU Eindhoven, 2001.
• G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82.