Combinatorics

Motivation

Two classical extremal results bound the number of edges of an $n$-vertex graph under a single restriction. Turán's theorem (1941) says that a graph with no clique on $k+1$ vertices has at most $t(n,k)$ edges, the edge count of the balanced complete $k$-partite graph. The Erdős–Gallai theorem (1959) gives the maximum number of edges of an $n$-vertex graph whose largest matching has at most $s$ edges. N. Alon and P. Frankl, Turán graphs with bounded matching number (arXiv:2210.15076v1; J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002), combine the two restrictions. Their Theorem 1.1 determines the maximum for the clique constraint and every $n\ge 2s+1$ (mission 1 of this series). Their Proposition 3.1, the goal here, treats a whole class of forbidden graphs, the color-critical ones, when $s$ is large in terms of the forbidden graph and $n$ is large in terms of $s$.

Color-critical graphs are the natural class for exact Turán results: by a theorem of M. Simonovits (1968), for a color-critical $H$ of chromatic number $k+1$ the Turán graph $T(N,k)$ is extremal for $H$-freeness once $N$ is large. Proposition 3.1 is the analogue of Simonovits' theorem under a matching constraint.

Setting

All graphs are finite and simple. For a graph $G$, a matching is a set of pairwise disjoint edges, and the matching number $\nu(G)$ is the largest size of a matching. For a graph $H$, $G$ is $H$-free if it contains no subgraph (not necessarily induced) isomorphic to $H$. The chromatic number $\chi(H)$ is the least number of colors in a proper vertex coloring. $H$ is color-critical if it has an edge $e$ with $\chi(H-e)<\chi(H)$; examples are complete graphs and odd cycles.

The Turán graph $T(n,k)$ is the complete $k$-partite graph on $n$ vertices with classes of sizes as equal as possible; $t(n,k)$ is its number of edges. For $k\ge 2$ and $2s\le n$, the graph $G(n,k,s)$ is the complete $k$-partite graph on $n$ vertices consisting of $k-1$ classes of sizes as equal as possible whose total size is $s$, and one further class of size $n-s$. Its number of edges is $g(n,k,s)$.

In the Lean development, vertices of $G$ are Fin n; the shared objects of this series live in TuranMatching.Clique.Setting: $\nu$ is matchingNumber, $t(n,k)$ is turanNum n k (Mathlib's turanGraph), $G(n,k,s)$ is bigGraph n k s, $g(n,k,s)$ is gNum n k s, color-criticality is IsColorCritical, and the set $X$ of vertices of degree exceeding $2s$ is highDeg G s.

Formalization targets

Goal: Proposition 3.1 (p. 5)

There is $n_0:\mathbb N\to\mathbb N$ such that for every color-critical $H$ with $\chi(H)=k+1>2$ there is $s_0(H)$ with: for all $s>s_0(H)$ and $n>n_0(s)$,

$$\max\{|E(G)| : |V(G)|=n,\ G\ H\text{-free},\ \nu(G)\le s\}=g(n,k,s).$$

The maximum is stated as an upper bound for every admissible $G$ together with an admissible graph attaining $g(n,k,s)$. The thresholds $s_0$ and $n_0$ are left existential, as on the page.

Milestones (pp. 5–6)

1. $G(n,k,s)$ is $k$-colorable, $H$-free for every $H$ with $\chi(H)=k+1$, and $\nu(G(n,k,s))=s$ (for $2s\le n$).
2. If $\nu(G)\le s$ then at most $s$ vertices have degree exceeding $2s$: $|X|\le s$.
3. If every degree is at most $2s$ and $\nu(G)\le s$, then $|E(G)|\le(2s+1)s$.
4. If $\nu(G)\le s$ and $|X|<s$, then $|E(G)|<(s-1)n+2(s+1)s$.
5. $(s-1)n+2(s+1)s<g(n,k,s)$ for $n>3s^2+2s$.
6. If $\nu(G)\le s$ and $|X|=s$, then $V-X$ is independent.
7. Simonovits' theorem: an $H$-free graph on $N\ge N_0(H)$ vertices has at most $t(N,k)$ edges.
8. If $|X|=s$, $V-X$ is independent, $Z$ is disjoint from $X$ with $|Z|=\lfloor s/(k-1)\rfloor$ and $G[X\cup Z]$ has at most $t(s+\lfloor s/(k-1)\rfloor,k)$ edges, then $|E(G)|\le g(n,k,s)$.

Significance

The proposition settles, for every color-critical $H$ and large parameters, the Turán problem with a bounded matching number, and identifies the extremal graph $G(n,k,s)$, which does not depend on $H$ beyond its chromatic number. For $H=K_{k+1}$ it agrees with the large-$n$ case of Theorem 1.1 of the same paper. The structural steps (few high-degree vertices, the independence of the low-degree side) are reusable in other degree-based arguments under matching constraints.

The result is proved in the paper; none of it is formalized. The mission produces, besides the goal, two classical theorems absent from Mathlib in the forms needed here: the matching-number consequence of Vizing's theorem (milestone 3) and Simonovits' exact Turán theorem for color-critical graphs (milestone 7). Milestone 7 is a cited classical theorem, not a result of Alon and Frankl; it is posed because the proof rests on it. Mathlib currently has Turán's theorem for cliques and the Erdős–Stone–Simonovits density theorem, but not the exact result for color-critical graphs.

Difficulty

Milestones 1, 2, 4, 5, 6 and 8 are elementary counting arguments, though each requires building matchings or explicit counts in Lean. Milestone 8 contains the paper's "easy to see" isomorphism, which in Lean is an identity between two edge counts, $t(s+m,k)+(n-s-m)s=g(n,k,s)$ with $m=\lfloor s/(k-1)\rfloor$.

Milestone 3 needs Vizing's edge-coloring theorem (a graph of maximum degree $\Delta$ is properly $(\Delta+1)$-edge-colorable). A naive greedy edge coloring gives only $2\Delta-1$ colors, which bounds the edge count by about $(4s-1)s$ and is too weak for the comparison in milestones 4 and 5.

Milestone 7 is the hardest item. The density version (Erdős–Stone–Simonovits) gives $t(N,k)+o(N^2)$ edges only; the exact bound for color-critical $H$ requires Simonovits' stability method, an argument that an almost-extremal $H$-free graph is close to $T(N,k)$ followed by a cleaning step that uses the critical edge.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency; edges are counted by #G.edgeFinset. The matching number is the supremum, in $\mathbb N$, of the edge counts of matching subgraphs; the set is nonempty and bounded, so this is the true maximum and not a junk value. $g(n,k,s)$ is defined as the edge count of the graph $G(n,k,s)$, not by a closed formula. Chromatic numbers live in $\mathbb N\cup\{\infty\}$ (Mathlib's chromaticNumber), both in the definition of color-critical and in the hypothesis $\chi(H)=k+1$. $H$-freeness is Mathlib's SimpleGraph.Free (no subgraph copy). The vertex type of $H$ is any finite type in the lowest universe.

Conventions committed to:

• $k\ge 2$ is the page's $k+1>2$; it is needed because $G(n,k,s)$ has $k-1$ classes and the proof divides by $k-1$.
• Quantifier order is the page's: $n_0$ is a function of $s$ alone and is chosen before $H$; $s_0$ depends on $H$ only.
• Milestone 1 states $k$-colorability for the page's "$k$ chromatic", and carries $2s\le n$, which the page leaves implicit.
• Milestone 3 bounds edges where the page writes "the number of vertices"; the vertex count is not bounded.
• Milestone 5 uses the threshold $n>3s^2+2s$. The page's "$n$ exceeding, say, $3s^2$" is too small: for $k=2$, $s=2$, $n=13$ one has $(s-1)n+2(s+1)s=25>22=g(13,2,2)$. The goal is unaffected, since $n_0(s)$ is unspecified.
• Milestone 4 carries $s\ge 1$ so that $s-1$ is honest natural-number subtraction.

A formalization that states only the upper bound, without an attaining graph, or that places the existential $n_0$ after $s$ is fixed as a constant independent of $s$, or that defines $\nu$ or $g$ so that they take junk values, is a different and weaker statement and is ruled out.

Infrastructure that would be reusable beyond this mission: a matching-number API on Mathlib's Subgraph.IsMatching (in particular $\nu(G)\le\nu(G')$ for $G\le G'$ and the behaviour under induced subgraphs); Vizing's theorem; and Simonovits' theorem. Contributions of any of these, and of partial results toward milestone 7 (for example the case $H=C_{2\ell+1}$), are welcome.

Selected references

• N. Alon and P. Frankl, Turán graphs with bounded matching number, arXiv:2210.15076v1, 2022; J. Combin. Theory Ser. B, 2024. https://arxiv.org/abs/2210.15076, https://doi.org/10.1016/j.jctb.2023.12.002
• M. Simonovits, A method for solving extremal problems in graph theory, stability problems, in: Theory of Graphs (Proc. Colloq., Tihany, 1966), Academic Press, 1968, pp. 279–319.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
• P. Turán, On an extremal problem in graph theory (in Hungarian), Mat. Fiz. Lapok 48 (1941), 436–452.
• V. G. Vizing, On an estimate of the chromatic class of a p-graph, Diskret. Analiz 3 (1964), 25–30.

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint of a given instance holds. Feder and Vardi conjectured, and Bulatov and Zhuk proved in 2017, that every CSP over a finite set of relations is either polynomial-time solvable or NP-complete, and that the answer is governed by the polymorphisms of the relations: the functions that map tuples of satisfying assignments, coordinate by coordinate, to a satisfying assignment.

A promise CSP (PCSP) relaxes the question. Each constraint comes as a pair of relations $P \subseteq Q$; the input is promised to be satisfiable with every constraint read as $P$, or unsatisfiable even with every constraint read as $Q$, and the task is to tell which. Approximate graph colouring ("is this 3-colourable graph 100-colourable?") and $(2+\varepsilon)$-SAT are of this kind. Austrin, Guruswami and Håstad (2017, doi:10.1137/15M1006507) showed that $(2+\varepsilon)$-SAT is NP-hard via polymorphisms; Brakensiek and Guruswami extended the polymorphism view to general Boolean PCSPs and proved a dichotomy for symmetric Boolean families (arXiv:1704.01937v2, SODA 2018, SIAM J. Comput. 2021). Later work by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) built the general algebraic theory of PCSPs on this foundation.

This mission takes one ingredient of the dichotomy: the tractable side for two polymorphism families that have no counterpart among tractable CSPs, the Majority and the Alternating-Threshold functions. The paper solves both with the same linear programming test.

Setting

The domain is $\{0,1\}$. A finite family of promise relations is $\Gamma = \{(P_R, Q_R) : R \in \tau\}$, with $\tau$ finite and $P_R \subseteq Q_R \subseteq \{0,1\}^{k_R}$. An instance $\Psi = (\Psi_P, \Psi_Q)$ has variables $x_1, \dots, x_n$ and clauses $R_j(x_{j_1}, \dots, x_{j_k})$; a variable may occur several times in a clause. $\Psi_P$ reads each clause with $P_{R_j}$, and $\Psi_Q$ with $Q_{R_j}$. Since $P \subseteq Q$, satisfiability of $\Psi_P$ implies that of $\Psi_Q$.

A function $f : \{0,1\}^L \to \{0,1\}$ is a polymorphism of $\Gamma$ if for every $R$ and all $x^{(1)}, \dots, x^{(L)} \in P_R$ the tuple $\big(f(x^{(1)}_1, \dots, x^{(L)}_1), \dots, f(x^{(1)}_k, \dots, x^{(L)}_k)\big)$ lies in $Q_R$. For odd $L$,

$$\mathrm{Maj}_L(x) = 1 \iff \sum_{i=1}^L x_i > \frac L2, \qquad \mathrm{AT}_L(x) = 1 \iff \sum_{i=1}^L (-1)^{i-1} x_i > 0 .$$

The LP relaxation of $\Psi$ has one unknown $v_j \in [0,1]$ per variable, and for every clause $R_j(x_{j_1}, \dots, x_{j_k})$ of $\Psi_P$ it requires $(v_{j_1}, \dots, v_{j_k})$ to lie in the convex hull of $P_{R_j}$. The §3.2 algorithm loops over the variables: it fixes $v_j = 0$ and re-solves the LP, then, if that is infeasible, fixes $v_j = 1$ and re-solves, and outputs "unsatisfiable" if both are infeasible. If every variable passes, it outputs "satisfiable". In Lean the answer is the predicate LPAlgAccepts 𝔸 X: the LP is feasible and, for each $j$, it has a solution with $v_j = 0$ or one with $v_j = 1$.

Formalization targets

Goal: correctness of the §3.2 algorithm

If $\mathrm{Maj}_L \in \mathrm{Pol}(\Gamma)$ for every odd $L$, or $\mathrm{AT}_L \in \mathrm{Pol}(\Gamma)$ for every odd $L$, then for every instance $\Psi$

$$\Psi_P \text{ satisfiable} \;\Longrightarrow\; \texttt{LPAlgAccepts}(\Psi) \;\Longrightarrow\; \Psi_Q \text{ satisfiable}.$$

No symmetry of the relations is assumed.

Milestones, in the order of the proof (pp. 14–15)

1. Completeness. If $\Psi_P$ is satisfiable, the algorithm accepts; no polymorphism is needed.
2. Convexity. A convex combination of LP solutions is an LP solution.
3. Case 1 claim. If $M \in ([0,1]\cap\mathbb Q)^{n\times n}$ has $M_{ii} \in \{0,1\}$, some rational probability vector $v$ has $(Mv)_i \ne 1/2$ for all $i$.
4. Case 1 rounding. With $\mathrm{Maj}_L$ for all odd $L$, an LP solution $w$ with no coordinate $1/2$ rounds to a satisfying assignment $x^*_i = \lfloor w_i \rceil$ of $\Psi_Q$.
5. Case 2 perturbation. For such $M$ and any rational $\hat w$, some $v$ has $(Mv)_i \ne \hat w_i$ wherever $\hat w_i \notin \{0,1\}$.
6. Case 2 rounding. With $\mathrm{AT}_L$ for all odd $L$, two LP solutions $w, \hat w$ that agree only where $\hat w_i \in \{0,1\}$ give the satisfying assignment $x^*_i = [w_i > \hat w_i \text{ or } w_i = \hat w_i = 1]$ of $\Psi_Q$.

Significance

The theorem shows that the Majority and Alternating-Threshold cases of Theorem 3.2 are tractable. Since $\Gamma$ is fixed, the LP has size linear in the instance, so linear programming decides $\mathrm{PCSP}(\Gamma)$ in polynomial time. Unlike the Zero, One, AND, OR and Parity cases of §3.1, these families cannot be handled by sandwiching a tractable CSP between $P$ and $Q$: footnote 12 of the paper observes that the closure of $\{\mathrm{Maj}_L\}$ or $\{\mathrm{AT}_L\}$ under identification of variables is not a clone. The tractable half of the paper's symmetric Boolean dichotomy (Theorem 2.16) depends on this result. Later work replaced this LP by the Basic LP and BLP+Affine relaxations (Brakensiek–Guruswami 2019, Barto et al. 2021).

The result is proved in the paper; to our knowledge it has no machine-checked proof. The formal content is a finite-dimensional rational convexity argument plus a counting argument on columns of polymorphism inputs. Related platform work: the published PCSPBLPAff.Symmetric.theorem_2 and theorem_3 concern the BLP+Affine algorithm with symmetric or block-symmetric polymorphisms. That is a different relaxation, and $\mathrm{AT}_L$ is not symmetric.

Difficulty

Completeness is immediate. Soundness is where the difficulty lies. The obvious approach, rounding an arbitrary LP solution, fails. For Majority, a coordinate equal to $1/2$ has no nearest integer, and the LP may admit no solution without such coordinates unless one uses the per-variable solutions the algorithm found. For Alternating-Threshold, there is no fixed threshold at all, and a single LP solution gives no rule for rounding a fractional coordinate. Two further points need care. Getting from a fractional point back to a polymorphism application needs a polymorphism of an arity that depends on the denominators of the hull weights, so a single fixed arity does not suffice. In the Alternating-Threshold case, as printed, the paper pads the inputs with an arbitrary point of $P$, and that step fails at coordinates where both solutions equal $0$ or $1$; the padding point has to come from the support of the hull weights.

Formalization scope

The domain $\{0,1\}$ is Bool. $\Gamma$ is a pair 𝔸 𝔹 : RelStruct τ ar Bool with [Fintype τ] and 𝔸.rel R ⊆ 𝔹.rel R, and instances, satisfiability and polymorphisms come from the published PCSPBLPAff_Symmetric_Setting. Coordinates are 0-based (Fin L), so the sign of $\mathrm{AT}_L$ is $(-1)^i$. The LP is stated over $\mathbb Q$; an LP with rational data is feasible over $\mathbb R$ exactly when it is feasible over $\mathbb Q$. The hull condition uses $P_R$, never $Q_R$. The acceptance predicate also requires the LP itself to be feasible, which matters only for instances without variables. The hypothesis is a disjunction of two universal statements ("$\mathrm{Maj}_L$ for all odd $L$, or $\mathrm{AT}_L$ for all odd $L$"), not "for every odd $L$, one of the two". A formalization that drops the hull constraint, replaces $P$ by $Q$ in the LP, or lets the acceptance predicate be satisfied without solving the LP would make the theorem trivial or different, and is ruled out by the definitions here.

Out of scope: polynomial running time and the printed conclusion "PCSP(Γ) is polynomial-time tractable" of Theorem 3.2; the polynomial-time solvability of linear programs; the Zero/One/AND/OR/Parity cases (Lemma 3.1, which invokes Schaefer's theorem); and the non-idempotent ("anti-") cases, which go through the reduction of Lemma 2.13(2). The Remark on p. 15 says the algorithm decides but does not find a solution. Only the decision is formalized.

Infrastructure needed: finite convex combinations over $\mathbb Q$, a perturbation lemma for avoiding finitely many hyperplanes in the rational simplex, and counting identities for $\mathrm{Maj}_L$ and $\mathrm{AT}_L$ on block inputs. The perturbation lemma and the counting identities are reusable beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the affine-hull algorithm in the Remark on p. 14), are welcome.

Selected references

• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy, arXiv:1704.01937v2, 2021; SIAM J. Comput. 50(6), 2021. https://arxiv.org/abs/1704.01937v2
• P. Austrin, V. Guruswami, J. Håstad, (2+ε)-Sat Is NP-Hard, SIAM J. Comput. 46(5), 2017. https://doi.org/10.1137/15M1006507
• 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
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
• T. J. Schaefer, The Complexity of Satisfiability Problems, STOC 1978. https://doi.org/10.1145/800133.804350

Motivation

Linear sets are point sets of a finite projective space defined by a subspace over a subfield. They appear throughout finite geometry, for instance in the study of semifields and, through the correspondence studied by Sheekey and Van de Voorde (arXiv:1806.05929), maximum rank distance (MRD) codes; see Polverino's survey (doi:10.1016/j.disc.2009.04.007). In these applications one needs to decide when two linear sets are the same up to a collineation, which can be difficult (Csajbók–Zanella, arXiv:1501.03441; Csajbók–Marino–Polverino, arXiv:1607.06962). The natural candidate answer, "when their defining subspaces are in the same orbit of the semilinear group", is only a sufficient condition: on the projective line $\mathrm{PG}(1,q^n)$ there are maximum scattered subspaces in different $\Gamma\mathrm L(2,q^n)$-orbits defining equivalent linear sets (the two papers just cited).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590, Combinatorica 41 (2021)) introduced $h$-scattered subspaces, a generalisation of scattered subspaces, and showed in their §4 that for $h \ge 2$ the sufficient condition is also necessary. This mission formalizes that result, Theorem 4.5.

Setting

Let $\mathbb F_q \subseteq \mathbb F_{q^n}$ be finite fields and let $V$ be an $r$-dimensional vector space over $\mathbb F_{q^n}$; it is also a vector space over $\mathbb F_q$. The projective space $\mathrm{PG}(V,\mathbb F_{q^n}) = \mathrm{PG}(r-1,q^n)$ has as points the one-dimensional $\mathbb F_{q^n}$-subspaces $\langle u\rangle_{\mathbb F_{q^n}}$, $u \ne 0$.

For an $\mathbb F_q$-subspace $U$ of $V$, the $\mathbb F_q$-linear set of $U$ is

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

of rank $\dim_{\mathbb F_q} U$.

For $0 < h \le r-1$, the subspace $U$ is $h$-scattered (Definition 1.1) 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$. The linear set $L_U$ of an $h$-scattered $U$ is called $h$-scattered (Definition 4.1); for $h = 2$ it is scattered with respect to lines.

The group $\Gamma\mathrm L(r,q^n)$ consists of the bijective additive maps $f$ of $V$ that are semilinear: $f(av) = a^\sigma f(v)$ for some field automorphism $\sigma$ of $\mathbb F_{q^n}$. Each $f$ induces a collineation $\varphi_f$ of $\mathrm{PG}(V,\mathbb F_{q^n})$, $\langle u\rangle \mapsto \langle f(u)\rangle$, and these collineations form $\mathrm P\Gamma\mathrm L(r,q^n)$. Two linear sets are $\mathrm P\Gamma\mathrm L$-equivalent if $\varphi_f(L_U) = L_W$ for some $f$; two subspaces are $\Gamma\mathrm L$-equivalent if $f(U) = W$ for some $f$.

Formalization targets

Goal: Theorem 4.5 (p. 14)

For $h \ge 2$ and $h$-scattered $\mathbb F_q$-subspaces $U$, $W$ of $V(r,q^n)$,

$$L_U \sim_{\mathrm P\Gamma\mathrm L(r,q^n)} L_W \iff U \sim_{\Gamma\mathrm L(r,q^n)} W .$$

Milestones (in the order of the proof)

1. Proposition 2.1 (p. 3): an $h$-scattered subspace is $i$-scattered for every $0 < i < h$.
2. Proposition 4.2 (p. 13, quoted from Bonoli–Polverino [5]): on a projective line $\mathrm{PG}(1,q^n)$, (1) a linear set with $q+1$ points has rank $2$; (2) two subspaces defining the same linear set of size $q+1$ and sharing a nonzero vector coincide.
3. Proposition 4.3 (p. 13): if $U$ is $2$-scattered and $L_W = L_U$, then $\dim_{\mathbb F_q} W = \dim_{\mathbb F_q} U$.
4. Lemma 4.4 (p. 13): if $U$ is $2$-scattered and $L_U = L_W$, then $U = \lambda W$ for some $\lambda\in\mathbb F_{q^n}^*$.

Significance

The result. Theorem 4.5 says that, for $h\ge2$, an $h$-scattered linear set remembers its defining subspace up to a scalar and up to the semilinear group. The equivalence problem for such linear sets, a geometric question about point sets, becomes the equivalence problem for subspaces, which is algebraic and can be attacked with linearized polynomials. Through the correspondence of Sheekey and Van de Voorde between maximum $(r-1)$-scattered subspaces and MRD codes, the paper derives from it (Theorem 4.10, not part of this mission) that two $\mathbb F_q$-linear MRD codes with minimum distance $n-r+1$, $r>2$, and left idealiser isomorphic to $\mathbb F_{q^n}$ are equivalent if and only if their associated linear sets in $\mathrm{PG}(r-1,q^n)$ are $\mathrm P\Gamma\mathrm L$-equivalent. Lemma 4.4 and Proposition 4.3 are of independent use: they say that the rank and, up to scalars, the subspace of any linear set scattered with respect to lines are invariants of the point set.

The formalization. The theorem is proved in the paper; no part of it, nor any statement about linear sets over a field extension, is machine-checked in Mathlib. The mission produces a formal model of linear sets, of the semilinear group and of its induced collineations that later finite-geometry missions can reuse, together with formal proofs of the four milestones. Proposition 4.2 is quoted from [5] without proof in the paper, so formalizing it means formalizing Bonoli and Polverino's argument.

Difficulty

The "if" direction is a direct computation, $L_{U^f} = L_U^{\varphi_f}$. The obvious approach to the converse, reconstructing $U$ from $L_U$ point by point, fails because a point $\langle u\rangle$ of $L_U$ determines $U\cap\langle u\rangle$ only up to a scalar of $\mathbb F_{q^n}^*$, and these scalars can a priori differ from point to point. Without the condition $h \ge 2$ they really do differ: for $h = 1$ the theorem is false. The step that needs $h\ge2$ is the rigidity of the intersections of $U$ with two-dimensional $\mathbb F_{q^n}$-subspaces, which is where the quoted result on linear sets of size $q+1$ on a projective line enters. Proposition 4.2 itself is a counting statement about point weights on $\mathrm{PG}(1,q^n)$ and is not available in any library.

Formalization scope

• $\mathbb F_q$ and $\mathbb F_{q^n}$ are arbitrary finite fields F, K with [Algebra F K]; $q$ is Fintype.card F. $V$ is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]), and $r$ is Module.finrank K V.
• IsHScattered F K h U includes the range $0 < h < r$ and the spanning condition $\langle U\rangle_{\mathbb F_{q^n}} = V$, as in Definition 1.1. With $h\ge2$ this forces $r\ge3$.
• A point is the K-submodule K ∙ u; linearSet F K U is a Set (Submodule K V) and $|L_U|$ is its Set.ncard.
• $\Gamma\mathrm L$ is the set of f : V ≃+ V for which some σ : K ≃+* K gives f (a • v) = σ a • f v. The collineation $\varphi_f$ sends a subspace $P$ to Submodule.span K (f '' P). The image $U^f$ is the set f '' U, and $\lambda W$ is (λ • ·) '' W with $\lambda\ne0$.
• Two trivializing readings are excluded. Restricting to linear maps (GL, PGL) would prove a different, weaker statement; taking $\mathrm{P}\Gamma\mathrm{L}$-equivalence to mean "some bijection of points maps $L_U$ to $L_W$" would make the "only if" direction false. Both equivalences quantify over the full semilinear group, and the collineation is the one induced by the same $f$.
• Proposition 4.2 is a result the paper numbers but quotes from [5] (Bonoli–Polverino, $\mathbb F_q$-linear blocking sets in $\mathrm{PG}(2,q^4)$). It is a milestone with its own proof obligation and is not assumed. The two parts are separate items.
• Proposition 2.1's "for any $i < h$" is read as $0 < i < h$, the range on which Definition 1.1 defines $i$-scattered.

Welcome contributions: the general theory of linear sets (point weights, $|L_U| \le (q^k-1)/(q-1)$ with equality iff $U$ is scattered), the fact that a semilinear map of $V$ maps $\mathbb F_q$-subspaces to $\mathbb F_q$-subspaces, and the counting argument behind Proposition 4.2. These are reusable for every linear-set mission.

Selected references

• B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, Combinatorica 41 (2021); arXiv:1906.10590v2 (2020). https://arxiv.org/abs/1906.10590
• G. Bonoli, O. Polverino, $\mathbb F_q$-linear blocking sets in $\mathrm{PG}(2,q^4)$, Innov. Incidence Geom. 2 (2005), 35–56. https://doi.org/10.2140/iig.2005.2.35
• B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in $\mathrm{PG}(1,q^n)$, J. Combin. Theory Ser. A 157 (2018), 402–426. https://arxiv.org/abs/1607.06962
• B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81 (2016), 269–281. https://arxiv.org/abs/1501.03441
• O. Polverino, Linear sets in finite projective spaces, Discrete Math. 310 (2010), 3096–3107. https://doi.org/10.1016/j.disc.2009.04.007
• J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://arxiv.org/abs/1806.05929

Two classical extremal problems and their common generalization

Two of the oldest results in extremal graph theory bound the number of edges of a graph under a single structural restriction. Turán's theorem (Turán 1941) determines the maximum number of edges $t(n,k)$ of an $n$-vertex graph with no complete subgraph on $k+1$ vertices. The Erdős–Gallai theorem (Erdős and Gallai 1959) determines the maximum number of edges of an $n$-vertex graph with no $s+1$ pairwise disjoint edges; for $n\ge 2s+1$ it is $\max\{\binom{2s+1}{2},\binom{s}{2}+s(n-s)\}$, attained by a clique on $2s+1$ vertices plus isolated vertices, or by $s$ vertices joined to everything.

N. Alon and P. Frankl (arXiv:2210.15076, published in J. Combin. Theory Ser. B, 2024, DOI 10.1016/j.jctb.2023.12.002) impose both restrictions at once and determine the maximum for all values of the parameters. Their answer is again the larger of two explicit constructions, and each of the two classical theorems is recovered as a degenerate range of theirs. The question belongs to a line of work on generalized Turán problems with an additional bound on the matching number, which has continued since this paper with other forbidden subgraphs in place of the clique.

Setting

All graphs are finite and simple, on the vertex set $\{0,1,\dots,n-1\}$.

• The clique number of $G$ is the largest number of vertices of a complete subgraph. "Clique number at most $k$" means that $G$ contains no complete subgraph on $k+1$ vertices.
• A matching is a set of pairwise disjoint edges. The matching number $\nu(G)$ is the largest size of a matching of $G$.
• A graph is complete $k$-partite if its vertex set is split into $k$ classes (some possibly empty) and two vertices are adjacent exactly when they lie in different classes.
• $T(n,k)$ is the complete $k$-partite graph on $n$ vertices whose classes have sizes as equal as possible, and $t(n,k)$ is its number of edges, the Turán number.
• $G(n,k,s)$ is the complete $k$-partite graph on $n$ vertices with $k-1$ classes of sizes as equal as possible and total size $s$, and one further class of size $n-s$. Its number of edges is $g(n,k,s)$.

A graph on $n$ vertices is admissible for $(k,s)$ when its clique number is at most $k$ and its matching number is at most $s$. Both constructions are admissible when $n\ge 2s+1$: $G(n,k,s)$ is $k$-colourable, and every edge of it meets the $s$ vertices of the small classes; the Turán graph $T(2s+1,k)$ on $2s+1$ of the vertices, with the other $n-2s-1$ vertices isolated, has no $s+1$ disjoint edges.

Formalization targets

Goal: Theorem 1.1

For $k\ge2$ and $n\ge 2s+1$,

$$\max\bigl\{|E(G)| : G \text{ on } n \text{ vertices},\ \omega(G)\le k,\ \nu(G)\le s\bigr\} \;=\; \max\{\,t(2s+1,k),\ g(n,k,s)\,\},$$

stated as an upper bound for every admissible graph together with an admissible graph attaining it.

Milestones

The milestones follow the proof of §2 of the paper, in attack order:

1. the two constructions are admissible (the lower bound);
2. the barrier: every graph has a vertex set $B$ such that every component of $G-B$ is odd and $|B|+\sum_i(|A_i|-1)/2=\nu(G)$;
3. Lemma 2.1: in the §2 choice of an extremal graph and barrier maximizing $\sum_i|A_i|^2$, non-adjacent vertices of $B$ have the same neighbourhood;
4. the graph induced on $B$ is then complete $k$-partite;
5. Claim 2.3: for that choice of graph and barrier, without loss of generality every component of $G-B$ has a vertex with no neighbour in the smallest class of $B$;
6. Lemma 2.2: for an extremal graph maximizing $\sum_i |A_i|^2$, at most one component of $G-B$ has more than one vertex;
7. the case analysis on $b=|B|$ that bounds the remaining structure by $\max\{t(2s+1,k),g(n,k,s)\}$;
8. the identity $t(s+\lfloor s/(k-1)\rfloor,k)+(n-s-\lfloor s/(k-1)\rfloor)\,s=g(n,k,s)$;
9. the Turán increment $t(N+1,k)-t(N,k)=N-\lfloor N/k\rfloor$ is non-decreasing in $N$, with steps at most $1$;
10. the function $f(b)=t(2s-b+1,k)+b(n-2s+b-1)$ has strictly increasing differences on the range of Case 4.

A companion item records the paper's parenthetical remark: for $n\le 2s+1$ the maximum is $t(n,k)$.

Significance

The theorem settles the edge-extremal problem for the two most basic graph parameters, clique number and matching number, jointly and for every admissible parameter value. It contains both classical theorems: when $n\le 2s+1$ the matching condition is void and the answer is Turán's $t(n,k)$; when $k\ge 2s+1$ the clique condition is void and the answer is the Erdős–Gallai bound. The two extremal constructions show that both regimes genuinely occur, and the threshold between them depends on $n$, $k$ and $s$ together. The same paper's Proposition 3.1 extends the answer $g(n,k,s)$ to every colour-critical forbidden graph for large $s$ and $n$, and the present theorem is the base case of that programme.

The theorem is proved in the paper; it has not been formalized. Mathlib has Turán's theorem (SimpleGraph.CliqueFree.card_edgeFinset_le), Tutte's theorem on perfect matchings, and extremal-graph infrastructure (SimpleGraph.IsExtremal), but no Tutte–Berge formula, no Gallai–Edmonds decomposition, and no Erdős–Gallai theorem for matchings. A formal proof would add the Tutte–Berge formula in the barrier form used here, a reusable Zykov symmetrization argument, and the first machine-checked proof of the Erdős–Gallai matching bound as a special case.

Difficulty

The arithmetic of the proof (milestones 8–10) is short. The difficulty is concentrated elsewhere.

First, the proof starts from a barrier $B$ whose removal leaves only odd components with $|B|+\sum_i(|A_i|-1)/2$ equal to the matching number. This is the Tutte–Berge formula sharpened to a maximal barrier, all of whose components are factor-critical. Mathlib's Tutte theorem covers perfect matchings only, so the deficiency version and the structure of maximal barriers have to be built.

Second, Lemma 2.1, Claim 2.3 and Lemma 2.2 are surgery on an extremal graph. Each modifies the graph (copying a neighbourhood, swapping two classes of $B$ in the neighbourhood of a component, merging two components) and must re-verify three things: the number of edges does not decrease, no clique on $k+1$ vertices appears, and the matching number stays at most $s$. The matching bound is re-verified through the barrier, so the components of the modified graph have to be tracked, and the extremality hypothesis has to be used in the right form. In particular, the paper's printed proof of Lemma 2.1 shows only that non-adjacency is transitive on $B$ and that non-adjacent vertices of $B$ have equal degree; the full "same neighbourhood" conclusion needs a further argument from extremality.

Third, the barrier equation of p. 2 is written with $s$, which presumes that an extremal graph has matching number exactly $s$; the paper does not prove this, and a solver who wants to chain the milestones needs it.

Formalization scope

Graphs are SimpleGraph (Fin n); edge counts are #G.edgeFinset. Clique number at most $k$ is G.CliqueFree (k + 1). The matching number is the supremum, in ℕ, of the edge counts of matching subgraphs (Subgraph.IsMatching); the set is nonempty and bounded, so the supremum is a maximum, and the companion sanity file proves $\nu(G)\le s$ iff every matching has at most $s$ edges. $T(n,k)$ is Mathlib's turanGraph n k. $G(n,k,s)$ is an explicit graph on Fin n (vertex $v<s$ in class $v \bmod (k-1)$, all others in class $k-1$), and $g(n,k,s)$ is defined as its edge count, not by a closed formula, so the identity of milestone 8 is a statement about the graph. Extremality is Mathlib's IsExtremal for the admissibility property. The maximality of $\sum_i a_i^2$ in Lemmas 2.1 and 2.2 and Claim 2.3 ranges over all extremal graphs together with all their odd barriers of value $s$, because the paper chooses $B$ together with $G$.

One hypothesis is added to the paper's statement: $k\ge2$. The paper says "every $k$", but $G(n,k,s)$ has $k-1$ classes of total size $s$, which is impossible for $k=1$ and $s>0$, and no nonempty graph has clique number at most $0$. Lemmas 2.1, 2.2 and Claim 2.3 keep the paper's barrier value $s$ as a hypothesis, while the barrier milestone itself is stated with $\nu(G)$.

The goal is an upper bound together with an attaining graph; an upper bound alone would be a weaker theorem. The surgery lemmas carry extremality as a hypothesis, never a hypothesis on the edge count that would presuppose the answer.

Contributions welcome beyond this mission: the Tutte–Berge formula and Gallai–Edmonds decomposition for SimpleGraph, the matching number as a reusable definition, and the Erdős–Gallai matching theorem.

Selected references

• N. Alon and P. Frankl, Turán graphs with bounded matching number, arXiv:2210.15076v1, 2022; J. Combin. Theory Ser. B, 2024. https://arxiv.org/abs/2210.15076, https://doi.org/10.1016/j.jctb.2023.12.002
• P. Turán, On an extremal problem in graph theory (in Hungarian), Mat. Fiz. Lapok 48 (1941), 436–452.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
• L. Lovász and M. D. Plummer, Matching Theory, North-Holland Mathematics Studies 121, 1986. https://doi.org/10.1090/chel/367
• A. A. Zykov, On some properties of linear complexes, Mat. Sbornik N.S. 24(66) (1949), 163–188.

Motivation

Scattered subspaces are a central object of finite geometry. An $\mathbb F_q$-subspace $U$ of an $\mathbb F_{q^n}$-vector space is scattered when every one-dimensional $\mathbb F_{q^n}$-subspace meets it in $\mathbb F_q$-dimension at most one. They give the largest scattered linear sets of projective spaces, and through them constructions of two-intersection sets, two-weight codes, strongly regular graphs and, most prominently, maximum rank distance (MRD) codes. Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2) generalise the notion to $h$-scattered subspaces, which meet every $h$-dimensional $\mathbb F_{q^n}$-subspace in $\mathbb F_q$-dimension at most $h$, prove the dimension bound $rn/(h+1)$, and ask when it is attained.

When $h+1$ divides $r$, direct sums of known examples reach the bound (Theorem 2.6 of the paper). For other values of $r$ the paper introduces a duality, the Delsarte dual, which turns a maximum $h$-scattered subspace of one space into a maximum $(n-h-2)$-scattered subspace of a space of another dimension. The name comes from Delsarte's duality on MRD codes, which the paper shows corresponds to it (Theorem 4.12). This mission is about that duality: Theorem 3.3 of the paper.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, with $n=\dim_{\mathbb F_q}\mathbb F_{q^n}$. Write $V(r,q^n)$ for an $r$-dimensional $\mathbb F_{q^n}$-vector space; it is also an $\mathbb F_q$-space of dimension $rn$.

Definition 1.1. For $0<h\le r-1$, an $\mathbb F_q$-subspace $U$ of $V=V(r,q^n)$ 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$. It is maximum $h$-scattered if no $h$-scattered subspace of $V$ has larger $\mathbb F_q$-dimension. The paper's Theorem 2.3 shows that an $h$-scattered subspace either has dimension $r$ and defines a subgeometry, or has dimension at most $rn/(h+1)$.

The setting of §3. Let $\mathbb V$ be a $k$-dimensional $\mathbb F_{q^n}$-vector space, written as a direct sum $\mathbb V=\Lambda\oplus\Gamma$ of $\mathbb F_{q^n}$-subspaces with $\dim\Lambda=r$ and $\dim\Gamma=k-r$. Let $W$ be a $k$-dimensional $\mathbb F_q$-subspace of $\mathbb V$ with $\langle W\rangle_{\mathbb F_{q^n}}=\mathbb V$ and $W\cap\Gamma=\{0\}$, and put

$$U=\langle W,\Gamma\rangle_{\mathbb F_q}\cap\Lambda ,$$

an $\mathbb F_q$-subspace of $\Lambda$. Every $k$-dimensional $\mathbb F_q$-subspace of $\Lambda$ with $k>r$ arises in this way (Lunardon and Polverino, cited as [21, Theorems 1, 2] in the paper). Let $\beta:\mathbb V\times\mathbb V\to\mathbb F_{q^n}$ be a non-degenerate reflexive sesquilinear form with companion automorphism $\sigma$ (linear in the first argument, $\beta(v,aw)=a^\sigma\beta(v,w)$) which takes values in $\mathbb F_q$ on $W\times W$; equivalently, $\beta$ extends a non-degenerate reflexive form $\beta':W\times W\to\mathbb F_q$. Write $\Gamma^\perp=\{v:\beta(v,g)=0\ \forall g\in\Gamma\}$, an $r$-dimensional subspace. The Delsarte dual of $U$ (Definition 3.2) is the $\mathbb F_q$-subspace

$$\bar U=W+\Gamma^\perp=\{w+\Gamma^\perp:w\in W\}\subseteq\mathbb V/\Gamma^\perp ,$$

a subspace of a $(k-r)$-dimensional $\mathbb F_{q^n}$-space.

Formalization targets

Goal: Theorem 3.3

Suppose $U$ is a maximum $h$-scattered $\mathbb F_q$-subspace of $\Lambda=V(r,q^n)$ of dimension $k=rn/(h+1)$, and $n\ge h+3$. Then

$$\bar U \text{ is a maximum } (n-h-2)\text{-scattered } \mathbb F_q\text{-subspace of } \mathbb V/\Gamma^\perp=V\!\left(\tfrac{rn}{h+1}-r,\ q^n\right),\qquad \dim_{\mathbb F_q}\bar U=k .$$

The statement holds for every admissible choice of the embedding and of $\beta$.

Milestones

1. Theorem 2.7 (p. 8): a maximum $h$-scattered subspace of dimension $rn/(h+1)$ meets every hyperplane $H$ in dimension between $rn/(h+1)-n$ and $rn/(h+1)-n+h$.
2. The identity $(S^*)^\perp=(S^{\perp'})^*$ (p. 9) for $\mathbb F_q$-subspaces $S$ of $W$, where $S^*=\langle S\rangle_{\mathbb F_{q^n}}$ and $\perp'$ is orthogonality for $\beta'$.
3. Proposition 3.1 (p. 9): if $k>r$ and every hyperplane $M$ of $\Lambda$ satisfies $\dim_{\mathbb F_q}(M\cap U)<k-1$ (condition $(\diamond)$), then $\dim_{\mathbb F_q}\bar U=k$.
4. Theorem 2.3 (p. 4): the dimension bound $rn/(h+1)$ for $h$-scattered subspaces.

Significance

The result. Theorem 3.3 converts a maximum $h$-scattered subspace of $V(r,q^n)$ of dimension $rn/(h+1)$ into a maximum $(n-h-2)$-scattered subspace of $V(rn/(h+1)-r,q^n)$. For $h=r-1$ it was known through MRD codes; the paper proves it for every $h$. Its consequences in the paper are Corollaries 3.4 and 3.5 and Theorem 3.6: when $n\ge4$ is even and $r\ge3$ is odd, maximum $(n-3)$-scattered subspaces of $V(r(n-2)/2,q^n)$ exist which the direct sum construction of Theorem 2.6 cannot produce, because $n-2$ does not divide $r(n-2)/2$. Theorem 3.3 is also the geometric counterpart of Delsarte duality of MRD codes (Theorem 4.12 of the paper).

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formalization would provide a reusable treatment of sesquilinear forms whose restriction to an $\mathbb F_q$-form is controlled, of orthogonal complements across the field extension $\mathbb F_q\subseteq\mathbb F_{q^n}$, and of the passage between $\Lambda$, $\mathbb V/\Gamma$ and $\mathbb V/\Gamma^\perp$. Theorems 2.3 and 2.7 are also the goals of companion missions in this series; here they enter as milestones.

Difficulty

The definition of $\bar U$ is easy; the content is in two dimension statements. First, $W+\Gamma^\perp$ must not collapse: $W\cap\Gamma^\perp=\{0\}$ is not automatic and depends on the hyperplane condition $(\diamond)$ on $U$, which in turn needs the upper bound of Theorem 2.7, whose proof in the paper is a long counting argument with Gaussian binomials (Section 5). Second, the scattered property must be transported through the duality: a large intersection of $\bar U$ with an $(n-h-2)$-dimensional subspace of $\mathbb V/\Gamma^\perp$ must be converted into a large intersection of $U$ with a hyperplane of $\Lambda$. This conversion runs through three different spaces and two different orthogonalities, $\perp$ over $\mathbb F_{q^n}$ and $\perp'$ over $\mathbb F_q$, and the identification $(S^*)^\perp=(S^{\perp'})^*$ between them requires that $W$ have an $\mathbb F_q$-basis which is an $\mathbb F_{q^n}$-basis of $\mathbb V$. Maximality is a further step that uses the bound of Theorem 2.3 in $\mathbb V/\Gamma^\perp$.

Formalization scope

$\mathbb F_q$ and $\mathbb F_{q^n}$ are finite fields F, K with Algebra F K; $\mathbb V$ is a finite-dimensional K-module with a compatible F-structure (IsScalarTower F K 𝕍). The setting of §3 is a structure DelsarteSetting F K 𝕍 holding $\Lambda,\Gamma$ (complementary), $W$ (with $\dim_{\mathbb F_q}W=\dim_{\mathbb F_{q^n}}\mathbb V$, spanning, $W\cap\Gamma=0$), $\sigma:\mathbb F_{q^n}\simeq\mathbb F_{q^n}$ and $\beta:\mathbb V\to_{\mathbb F_{q^n}}\mathbb V\to_{\sigma}\mathbb F_{q^n}$ with non-degeneracy, reflexivity and $\beta(W,W)\subseteq\mathbb F_q$. The embedding of $\Lambda$ into $\mathbb V$ is data, not a theorem; its existence is cited by the paper and is not an item. The paper's $\beta'$ is the restriction of $\beta$ to $W$.

Conventions pinned:

• $U$ is an F-subspace of the type ↥Λ, and "h-scattered in $\Lambda$" is Definition 1.1 with ambient space $\Lambda$, including $0<h<r$ and $\langle U\rangle_{\mathbb F_{q^n}}=\Lambda$. The dual is (n − h − 2)-scattered in the quotient 𝕍 ⧸ Γ^⊥, whose dimension is $k-r$.
• Every $rn/(h+1)$ is multiplied out: $(h+1)\dim U=rn$. Hyperplanes are subspaces with $\dim+1=\dim$ of the ambient space; $\dim<k-1$ is written $\dim+1<k$. The only natural-number subtraction is the index $n-h-2$, exact because $n\ge h+3$.
• The paper's $k>r$ is a hypothesis of Proposition 3.1, as on the page, and is derived (not assumed) in Theorem 3.3.

The form must be non-degenerate and $\mathbb F_q$-valued on $W$: with $\beta=0$ one would get $\Gamma^\perp=\mathbb V$ and a zero quotient, and without $\beta(W,W)\subseteq\mathbb F_q$ the subspace $W+\Gamma^\perp$ is not the paper's Delsarte dual; both conditions are fields of the setting and may not be dropped.

Cited inputs: none of the milestones is proved elsewhere; Theorems 2.3 and 2.7 duplicate the goals of companion missions 1 and 3 and may be closed by importing their proofs once published. Contributions welcome: the sesquilinear-form infrastructure (dimension of orthogonal complements, the extension of $\beta'$ from $W$ to $\mathbb V$), Proposition 3.1, and the transport argument of Theorem 3.3.

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
• G. Lunardon, O. Polverino, Translation ovoids of orthogonal polar spaces, Forum Math. 16 (2004), 663–669 (the embedding used in §3).
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243 (the case h = 1 of the bound).
• P. Delsarte, Bilinear forms over a finite field, with applications to coding theory, J. Combin. Theory Ser. A 25 (1978), 226–241 (Delsarte duality of rank-metric codes).

Why promise constraint satisfaction

A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint, drawn from a fixed finite set of relations, holds. The algebraic approach to CSPs explains their complexity through polymorphisms, the operations that preserve all constraint relations; this programme culminated in the CSP dichotomy theorem of Bulatov and Zhuk (2017). A promise CSP (PCSP) pairs each relation $P$ with a weaker relation $Q \supseteq P$: given an instance that is promised to be satisfiable with the $P$-constraints, one must distinguish it from instances that are not even satisfiable with the $Q$-constraints. Approximate graph colouring (is a 3-colourable graph 100-colourable?) and $(2+\varepsilon)$-SAT are PCSPs, and their complexity is not captured by the classical theory.

Brakensiek and Guruswami (arXiv:1704.01937) developed the polymorphism theory of PCSPs and classified the Boolean, symmetric, folded case.

Timeline.

• 1978: Schaefer classifies Boolean CSPs into polynomial-time and NP-complete.
• 2014: Austrin, Guruswami and Håstad prove $(2+\varepsilon)$-SAT NP-hard with an argument based on polymorphisms (SIAM J. Comput. 46(5), 2017).
• 2016–2018: Brakensiek and Guruswami introduce the general PCSP framework and prove a dichotomy for folded symmetric Boolean PCSPs (SODA 2018; arXiv:1704.01937v2, 2021; SIAM J. Comput. 50(6), 2021).
• 2019–2021: Barto, Bulín, Krokhin and Opršal recast the theory in terms of minions (J. ACM 68(4), 2021). Ficak, Kozik, Olšák and Stankiewicz extend the Boolean symmetric dichotomy beyond the folded case (ICALP 2019).

Setting

Fix the Boolean domain $\{0,1\}$. A promise relation of arity $k$ is a pair $(P, Q)$ with $P \subseteq Q \subseteq \{0,1\}^k$, and a family $\Gamma$ is a finite set of promise relations, possibly of different arities. A function $f : \{0,1\}^L \to \{0,1\}$ is a polymorphism of $(P,Q)$ if, whenever $x^{(1)}, \dots, x^{(L)} \in P$, applying $f$ coordinate-wise gives a tuple in $Q$; $\mathrm{Pol}(\Gamma)$ is the set of functions that are polymorphisms of every member of $\Gamma$.

A relation is symmetric if it is closed under permuting coordinates. Every symmetric relation has the form $\mathrm{Ham}_k(S) = \{x : |x| \in S\}$, where $|x|$ is the Hamming weight. A function is folded if $f(\bar x) = \neg f(x)$, and idempotent if $f(0,\dots,0) = 0$ and $f(1,\dots,1) = 1$; a family is folded (idempotent) if all its polymorphisms are. For odd $L$ the paper singles out three function families:

$$\mathrm{Par}_L(x) = \bigoplus_{i=1}^L x_i, \qquad \mathrm{Maj}_L(x) = \Big[\sum_{i} x_i > \tfrac L2\Big], \qquad \mathrm{AT}_L(x) = \Big[\sum_{i=1}^L (-1)^{i-1} x_i > 0\Big],$$

and their negations $\overline{\mathrm{Par}}_L, \overline{\mathrm{Maj}}_L, \overline{\mathrm{AT}}_L$. Finally, $f$ is $C$-fixing if some set $S$ of at most $C$ coordinates satisfies $f(x) = f(0,\dots,0)$ whenever $x$ vanishes on $S$.

Formalization targets

Goal: Theorem 4.13

Let $\Gamma$ be a finite, folded, symmetric family. If there are odd $L_1, \dots, L_6$ with

$$\mathrm{Par}_{L_1},\ \mathrm{AT}_{L_2},\ \mathrm{Maj}_{L_3},\ \overline{\mathrm{Par}}_{L_4},\ \overline{\mathrm{AT}}_{L_5},\ \overline{\mathrm{Maj}}_{L_6} \notin \mathrm{Pol}(\Gamma),$$

then

$$\exists\, C(\Gamma)\ \ \forall L\ \ \forall f \in \mathrm{Pol}(\Gamma) \cap \{0,1\}^{\{0,1\}^L}:\ f \text{ is } C(\Gamma)\text{-fixing}.$$

No value of $C$ is fixed: the goal asserts only that one bound works for all arities.

Milestones

The milestones follow the paper's proof:

• the tools of §2: Propositions 2.10, 2.12 and 2.15 and Lemma 2.13(1), which split polymorphisms into idempotent and negated idempotent ones;
• the arity-reduction Claims 4.2, 4.3 and 4.4;
• the closure computations Claim 4.6 ($\mathrm{AT}$) and Claim 4.8 ($\mathrm{Maj}$);
• the relaxation Lemmas 4.5 and 4.7, which replace $\Gamma$ by a single canonical symmetric promise relation;
• the additive-combinatorics Lemma 4.9 and its bounded Remark;
• Lemma 4.10 and Corollary 4.11, which bound the coordinates $i$ with $f(e_i) = 1$;
• Lemma 4.12, the idempotent case of the goal.

Significance

Theorem 4.13 is the structural half of the paper's main dichotomy (Theorem 2.16): a folded symmetric Boolean PCSP is polynomial-time solvable if it has one of the six families as polymorphisms for every odd arity, and NP-hard otherwise. Hardness follows by feeding the $C$-fixing structure into a Label Cover reduction (Theorem 5.3). Bounded "fixing" or junta-like structure of all polymorphisms is the standard route from algebra to NP-hardness for PCSPs. This theorem is the cleanest Boolean instance of it, and it underlies later classifications of symmetric Boolean PCSPs.

The result has been proved and published since 2018. To our knowledge none of it has been formalized. A formalization supplies a checked Boolean polymorphism toolkit (Hamming-weight relations, folding, idempotence, relaxations), checked closure computations under alternating-threshold and majority operations, and a uniform-constant Frobenius-type lemma. All of these can be reused by other Boolean PCSP missions.

Difficulty

The obvious argument fixes a polymorphism $f$ and bounds its relevant coordinates directly from a constraint that $\mathrm{Par}$, $\mathrm{AT}$ or $\mathrm{Maj}$ violates. This gives a bound that depends on the arity $L$, and an $L$-dependent bound is trivial ($C = L$ always works). The work is in making the constant uniform. The proof has to replace $\Gamma$ by a single canonical promise relation that does not depend on $f$, classify exactly which symmetric relations exclude $\mathrm{AT}_L$ and $\mathrm{Maj}_L$, and use an additive-combinatorics lemma whose constants depend only on that relation's arity. Its bounded version must hold with the same constants. The non-idempotent polymorphisms need a separate reduction through the negated family $\neg\Gamma$.

Formalization scope

The domain $\{0,1\}$ is Bool (false $= 0$). A family $\Gamma$ is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar Bool from the published definition PCSPBLPAff_Symmetric_Setting, with [Fintype τ] (finitely many relations) and 𝔸.rel R ⊆ 𝔹.rel R (promise). IsPolymorphism 𝔸 𝔹 f from that file is Definition 2.4. Coordinates are Fin L, so the 1-based sign $(-1)^{i-1}$ of $\mathrm{AT}_L$ becomes $(-1)^{i}$. Anti-functions negate the output. Family properties (folded, idempotent, non-degenerate) quantify over polymorphisms of every arity $L \ge 0$. A folded or idempotent family has no nullary polymorphisms, so admitting $L = 0$ changes nothing. The constants $C(\Gamma)$, $c(\Gamma)$, $A(n)$ and $d(n)$ are quantified before the arity and the function (respectively before $S_0, S_1$). A statement that lets the constant depend on $f$ or $L$ is trivially true and is not the goal.

Out of scope are the complexity conclusions: "PCSP($\Gamma$) is NP-hard" (Theorems 2.16 and 5.3) and item 2 of Lemma 2.13 (transfer of tractability). The cited inputs for those conclusions are also out of scope: the PCP theorem with parallel repetition (Proposition 5.2) and Schaefer's theorem. No complexity predicate appears in any statement.

A complete development needs the following, with Mathlib's Nat.frobeniusNumber as a starting point for Lemma 4.9:

• explicit matrix constructions for Claims 4.6 and 4.8;
• closure of polymorphisms under projections (minors), used in Lemma 4.10 and Corollary 4.11;
• a Frobenius-coin argument with constants uniform in the sets $S_0, S_1$.

Contributions are welcome at any milestone, including separate proofs of the closure computations and of Lemma 4.9.

Selected references

• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Algebraic Structure and a Symmetric Boolean Dichotomy, arXiv:1704.01937v2, 2021; SIAM J. Comput. 50(6), 2021. https://arxiv.org/abs/1704.01937
• P. Austrin, V. Guruswami, J. Håstad, (2+ε)-SAT is NP-hard, SIAM J. Comput. 46(5), 2017. https://doi.org/10.1137/15M1006507
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, J. ACM 68(4), 2021. https://doi.org/10.1145/3457606
• M. Ficak, M. Kozik, M. Olšák, S. Stankiewicz, Dichotomy for symmetric Boolean PCSPs, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.57
• T. J. Schaefer, The complexity of satisfiability problems, STOC 1978. https://doi.org/10.1145/800133.804350