Discrete Geometry

The problem

Place $N$ distinct points $x_1,\dots,x_N$ on the unit sphere in $\mathbb{R}^3$ to minimise the Coulomb energy

$$E(x) = \sum_{i<j} \frac{1}{\lVert x_i - x_j\rVert}.$$

Good configurations are easy to find numerically, but proving that one is the global minimum is hard. Rigorous proofs exist for only a few $N$:

• $N = 2, 3$: classical.
• $N = 4, 6, 12$: the Delsarte–Yudin linear-programming bound is exact (Yudin; Andreev; Cohn–Kumar).
• $N = 5$: Schwartz, by a large computer-assisted search.
• $N = 8$: Kryvonos–Liehr–Taylor; in Lean by Tooby-Smith–Zughaid.
• $N = 7$: a Lean-verified proof by Hung Tran (package, write-up).

This mission

• $N = 10$ (capped square antiprism) and $N = 9$ (tricapped trigonal prism) are stated as "some member of this one-parameter symmetric family is a global minimiser over all configurations", because the optimal parameter has no known closed form. No symmetry is assumed of competing configurations, and uniqueness is not required. $N = 10$ comes first: like $N = 7$ it has an antipodal pair of poles, which makes the case split easier.
• $N = 32$ (an icosahedron nested with its dual dodecahedron) is the challenge. It is the numerically best-known configuration, but the standard bounds do not close the gap there, so a new idea is needed.

The shared lemmas (the distance formula, two-point positivity behind the Delsarte–Yudin bound, and three-point positivity behind the Bachoc–Vallentin and Cohn–Woo bounds) are stated once for reuse, along with well-posedness of each configuration.

Motivation

A linear set of the projective line $\mathrm{PG}(1, q^n)$ is the set of points $\langle u\rangle_{\mathbb F_{q^n}}$ spanned by the nonzero vectors $u$ of an $\mathbb F_q$-subspace $U \subseteq \mathbb F_{q^n}^2$. The extremal ones, the maximum scattered linear sets, are given by scattered polynomials $f$ over $\mathbb F_{q^n}$, and each such $f$ also gives an $\mathbb F_{q^n}$-linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey, Adv. Math. Commun. 10, 2016). Rank-distance codes are used in network coding, and linear sets appear in the study of semifields, blocking sets and two-intersection sets.

Linear sets and codes are classified up to equivalence: two linear sets are the same object if a collineation of the line, an element of $\mathrm{P\Gamma L}(2, q^n)$, maps one onto the other. The question is therefore not only whether new scattered polynomials exist but how many inequivalent linear sets they produce.

• 2000–2001. The monomials $x^{q^s}$, $\gcd(s,n) = 1$ (Blokhuis–Lavrauw 2000), all give a single linear set of $\mathrm{PG}(1,q^n)$ (pseudoregulus type); the binomials $\delta x^{q^s} + x^{q^{n-s}}$ (Lunardon–Polverino 2001) give at most $\varphi(n)$ times a function of $q$ classes.
• 2018. Csajbók, Marino and Polverino (J. Combin. Theory Ser. A 157, 2018) develop the equivalence theory of linear sets of $\mathrm{PG}(1, q^n)$, including coefficient identities that two $q$-polynomials defining the same linear set must satisfy.
• 2021. Longobardi and Zanella (J. Algebraic Combin. 2021) give a third family, again with at most $\varphi(n)/2$ classes.
• 2021. Longobardi, Marino, Trombetti and Zhou (arXiv:2102.08287v3) construct the family $\psi_{h,t}$ (Theorem 3.1, the companion mission) and show (Theorem 5.1) that it contains a number of $\mathrm{P\Gamma L}$-classes growing exponentially in $n$. This mission formalizes that count.

Setting

Let $p$ be an odd prime, $r \ge 1$, $q = p^r$, $t \ge 1$, $n = 2t$, and let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$. Its subfield $\mathbb F_q$ is $\{c : c^q = c\}$.

A $q$-polynomial is a map $f(x) = \sum_{i=0}^{n-1} \alpha_i x^{q^i}$ with $\alpha_i \in F$ (qpoly). It is scattered (IsScatteredPoly) if for all $z, y \in F^*$, $f(z)/z = f(y)/y$ forces $z = cy$ with $c \in \mathbb F_q$.

The graph of $f$ is $U_f = \{(x, f(x)) : x \in F\} \subseteq F^2$ (graph). A point $\langle v \rangle_{\mathbb F_{q^n}}$ of $\mathrm{PG}(1, q^n)$ is the set of all $F$-multiples of a nonzero $v \in F^2$ (point), and the linear set of $f$ is the point set

$$L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\} \quad (\texttt{linSet}).$$

For a field automorphism $\sigma$ and an invertible $2 \times 2$ matrix $A$ over $F$, the map $v \mapsto A v^\sigma$ ($\sigma$ acting on coordinates, act) is an element of $\Gamma\mathrm L(2, q^n)$; with $\sigma = \mathrm{id}$ it is in $\mathrm{GL}(2, q^n)$. Two subsets $U, W \subseteq F^2$ are GL- or ΓL-equivalent (GLEquiv, GammaLEquiv) if such a map sends $U$ onto $W$. Two point sets are PGL- or PΓL-equivalent (PGLEquiv, PGammaLEquiv) if the induced map on points, $P \mapsto \{A v^\sigma : v \in P\}$, sends one onto the other.

The family. For $h \in F$,

$$\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}} \quad (\texttt{psi}),$$

$H = \{h \in F : h^{q^t+1} = -1\}$ (hSet), $U_h = U_{\psi_{h,t}}$ and $L_{h,t} = L_{\psi_{h,t}}$. For $t \ge 3$ and $h \in H \setminus \mathbb F_{q^t}$, $\psi_{h,t}$ is scattered and $L_{h,t}$ is a maximum scattered linear set (Theorem 3.1).

Formalization targets

Goal: Theorem 5.1

For $t > 4$, the number $M$ of $\mathrm{P\Gamma L}(2,q^n)$-classes met by the sets $L_{h,t}$, $h \in H$, satisfies

$$M \ge \begin{cases} \left\lfloor \dfrac{q^t+1}{8rt} \right\rfloor, & t \not\equiv 2 \pmod 4,\\[1.5ex] \left\lfloor \dfrac{q^t+1}{4rt(q^2+1)} \right\rfloor, & t \equiv 2 \pmod 4.\end{cases}$$

It is stated as: some $S \subseteq H$ of at least that size has pairwise $\mathrm{P\Gamma L}$-inequivalent $L_{h,t}$. The goal fixes the paper's constants; the proof on p. 26 in fact counts classes exactly in terms of class sizes, so a sharper bound is a natural follow-up.

Milestones

1. Proposition 3.2 (p. 7): $h \in H \Rightarrow h^{q^2+1} \ne 1$ and $h^{q^{t-2}} \ne -h$.
2. $|H| = q^t + 1$ (p. 26).
3. Display (29) (p. 16): for $h, k \in H$, $U_h \sim_{\mathrm{GL}} U_k$ iff $h = \pm k$ ($t \not\equiv 2$) or $h = \ell k$ with $\ell^{q^2+1} = 1$ ($t \equiv 2 \bmod 4$).
4. Theorem 4.2 (a)–(b) (p. 16), in the $U_h$ form: $U_h \sim_{\Gamma\mathrm L} U_k$ iff $h = \pm k^\rho$ (resp. $\ell k^\rho$) for some $\rho \in \mathrm{Aut}(\mathbb F_{q^n})$.
5. Proof of Corollary 4.3 (p. 18): the GL-class of $U_h$ in the family has $\xi_h = 2$ (resp. $q^2+1$) members, and its ΓL-class at most $nr\xi_h$.
6. Lemma 2.2 (p. 5, from Csajbók–Marino–Polverino): $L_f = L_g$ forces $\alpha_0 = \beta_0$ and two families of coefficient identities.
7. Display (37) (pp. 20–21): PGL-equivalence of $L_f, L_g$ as an equality of sets of quotients.
8. The case $b = 0$ of (37) (p. 21): $c = 0$.
9. Lemma 5.2 (p. 21): the case $b = 0$ for $\psi_{h,t}, \psi_{k,t}$ gives $(h/k)^{q^2+1} = 1$ and $U_h \sim_{\Gamma\mathrm L} U_k$.
10. Lemma 5.3 (p. 22): the case $b = 1$, with its three conclusions.

Significance

The result. Theorem 5.1 shows that maximum scattered linear sets of $\mathrm{PG}(1, q^n)$, and hence $\mathbb F_{q^n}$-linear MRD codes, exist in numbers exponential in $n$ up to equivalence, whereas each previously known infinite family yields at most $\varphi(n)$ times a function of $q$ classes (Table 1, p. 3). Remark 5.4 draws the consequence that the family is new. Its intermediate results, the classification of the $\mathrm{GL}$- and $\Gamma\mathrm L$-equivalences between the $U_h$ (Theorem 4.2) and the reduction of $\mathrm{PGL}$-equivalence to sets of quotients, are the standard tools for any later classification of this family.

Formalizing it. The theorem has a complete published proof; none of it is machine-checked. The platform has no action of $\mathrm{GL}(2, q^n)$ or $\Gamma\mathrm L(2, q^n)$ on the projective line, no linear sets of $\mathrm{PG}(1,q^n)$ as point sets, and no coefficient identities for $q$-polynomials defining the same linear set. The mission produces these, then the class counts. Lemma 2.2 is a result of an earlier paper (Csajbók–Marino–Polverino 2018) cited without proof, so formalizing it means formalizing part of that paper too.

Difficulty

Equality of two linear sets is equality of sets of points, which says nothing directly about the polynomials: different $q$-polynomials can define the same linear set (all $x^{q^s}$ with $\gcd(s,n)=1$ do). The obvious idea, that $\mathrm{P\Gamma L}$-equivalent linear sets come from $\Gamma\mathrm L$-equivalent subspaces $U_h$, fails in general (p. 3), so the count cannot be read off Theorem 4.2. The step that needs the restriction $t > 4$ is the comparison of coefficients in the $q$-polynomial identities, which for $t = 3, 4$ is open (Remark 5.5). A second difficulty is bookkeeping: the exponents $q^{t\pm1}$, $q^{2t-1}$, the negative powers of $h$ and the case split on $t \bmod 4$ must all be tracked through every identity.

Formalization scope

• Field. $F$ is a finite field with CharP F p, p prime, Odd p ("$q$ odd"), q = p ^ r with 0 < r, and Fintype.card F = q ^ (2 * t). $r$ is the exponent of $q = p^r$, as in Theorem 5.1, so $|\mathrm{Aut}(\mathbb F_{q^n})| = rn$. Lemma 2.2, (37) and the $b = 0$ step are stated for general $n \ge 1$ and Fintype.card F = q ^ n, without "$q$ odd", as printed.
• Exponents. $x^{q^i}$ is x ^ q ^ i; negative powers of $h$ are field quotients (h / h ^ q ^ (t+1) for $h^{1-q^{t+1}}$), exact since $h \ne 0$ on $H$. Natural-number subtractions $t-1$, $2t-1$, $3t-2$, $n-k$, $q^i - 1$ are exact in the stated ranges.
• Geometry. The plane is Fin 2 → F; points are sets of scalar multiples; linear sets are sets of points. Equivalences are stated as images of sets under $v \mapsto A v^\sigma$ with $\det A$ a unit and $\sigma : F \simeq F$ a ring automorphism.
• Pinned readings.
  1. "Scattered" is the p. 2 quotient definition with $\mathbb F_q = \{c : c^q = c\}$.
  2. Proposition 3.2's $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$ (equal for $t \ge 2$), and "$q$ odd" is added.
  3. Theorem 4.2 (a)–(b), stated for codes $\mathcal C_{h,t}$, is formalized as the $\Gamma\mathrm L$-equivalence of $U_h, U_k$, which the proof establishes and which is the code equivalence by Theorem 2.1 (from Sheekey 2016). The automorphism-group sentence is omitted.
  4. Lemma 5.3's hypothesis "(41) holds" is read in the setting of p. 21: $b = 1$, $\bar c = c - da \ne 0$, $\bar g = \sum \gamma_i y^{q^i}$ inverse to $x \mapsto ax + g(x)$ (47), and $d + \bar c\gamma_0 = 0$ (40).
  5. In (37), $ax + bg(x) \ne 0$ for $x \ne 0$ is part of the condition (stated on p. 21 for $b = 1$).
  6. "The total number $M$ of inequivalent $L_{h,t}$" is the number of classes met by $\{L_{h,t} : h \in H\}$, formalized through a pairwise-inequivalent subset of $H$. $H$ is not restricted to $h \notin \mathbb F_{q^t}$, as in the count $|H| = q^t+1$ of p. 26; "maximum scattered" is descriptive.
• Trivializing formalizations ruled out. Equivalence is stated on point sets, never on quotient sets $\{f(x)/x\}$, where Lean's $y/0 = 0$ could merge inequivalent sets; the goal requires pairwise inequivalence, not distinctness of the parameters $h$ (note $\psi_{-h,t} = \psi_{h,t}$); and the hypotheses are satisfiable, with bound $\lfloor 244/40 \rfloor = 6$ at $q = 3$, $t = 5$.
• Citation basis. All indices and pages refer to arXiv:2102.08287v3 (printed page = PDF page). The Combinatorica version is not used.
• Welcome contributions. The $\Gamma\mathrm L(2,q^n)$ action on $F^2$ and on point sets, the cardinality of $\{h : h^{q^t+1} = -1\}$, and Lemma 2.2 are reusable beyond this mission. Proofs of any milestone, and of Theorem 3.1 in the companion mission, are welcome.

Selected references

• G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
• B. Csajbók, G. Marino, O. Polverino, Classes and equivalence of linear sets in PG(1, q^n), J. Combin. Theory Ser. A 157, 402–426, 2018.
• J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 475–488, 2016.
• G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81(1), 231–243, 2000.
• G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14(1), 49–56, 2001.
• B. Csajbók, C. Zanella, On the equivalence of linear sets, Des. Codes Cryptogr. 81(2), 269–281, 2016.

Motivation

A linear set of a projective space over a finite field is the set of points spanned by the nonzero vectors of a subspace over a subfield. They have been used to construct and characterize semifields, rank-metric codes, translation spreads, translation ovoids, two-intersection sets and the blocking sets for which Lunardon introduced them (Polverino 2010; Lavrauw–Van de Voorde 2015). On the projective line $\mathrm{PG}(1, q^n)$ the extremal objects, the maximum scattered linear sets, are equivalent to scattered polynomials over $\mathbb F_{q^n}$, and each scattered polynomial $f$ gives an $\mathbb F_q$-linear maximum rank-distance (MRD) code $\mathcal C_f = \{ax + bf(x) : a, b \in \mathbb F_{q^n}\}$ of minimum distance $n-1$ (Sheekey 2016). Rank-distance codes are studied in network coding theory (p. 2).

Scattered polynomials are scarce. Before this paper, only three families were known for infinitely many $n$:

• 2000. The monomials $x^{q^s}$ with $\gcd(s, n) = 1$ (pseudoregulus type). Blokhuis and Lavrauw (2000) proved that a scattered linear set of $\mathrm{PG}(1, q^n)$ has rank at most $n$.
• 2001, 2016. The binomials $\delta x^{q^s} + x^{q^{n-s}}$ with $N_{q^n/q}(\delta) \notin \{0, 1\}$ (Lunardon–Polverino 2001, Sheekey 2016).
• 2021. For $q$ odd and $n = 2t$, the polynomial $\tfrac12(x^q + x^{q^{t-1}} - x^{q^{t+1}} + x^{q^{2t-1}})$ and its variants (Longobardi–Zanella 2021).
• 2018–2020. Further families exist only for $n \in \{6, 8\}$ (Csajbók–Marino–Polverino–Zanella 2018; Csajbók–Marino–Zullo 2018; Bartoli–Zanella–Zullo 2020). Asymptotic classification results suggest that scattered polynomials are rare (Bartoli–Zhou 2018).

Longobardi, Marino, Trombetti and Zhou construct a fourth family, defined for every even $n \ge 6$ and odd $q$. This mission formalizes that construction, Theorem 3.1 of the paper.

Setting

Let $p$ be an odd prime, $r \ge 1$, $q = p^r$, $t \ge 3$ and $n = 2t$. Let $F = \mathbb F_{q^n}$ be the finite field of order $q^{2t}$. For $m \mid n$, write $\mathbb F_{q^m}$ for its subfield of order $q^m$, the set of $x$ with $x^{q^m} = x$.

A $q$-polynomial over $F$ is a map $f(x) = \sum_{i=0}^{n-1} c_i x^{q^i}$ with $c_i \in F$. It is $\mathbb F_q$-linear. Its graph $U_f = \{(x, f(x)) : x \in F\}$ is an $n$-dimensional $\mathbb F_q$-subspace of $F^2$, and it defines the linear set $L_f = \{\langle (x, f(x))\rangle_{\mathbb F_{q^n}} : x \in F^*\}$ of $\mathrm{PG}(1, q^n)$.

The polynomial $f$ is scattered when, for all $z, y \in F^*$,

$$\frac{f(z)}{z} = \frac{f(y)}{y} \quad\Longrightarrow\quad z \text{ and } y \text{ are } \mathbb F_q\text{-linearly dependent.}$$

Equivalently, $L_f$ has the maximum size $(q^n - 1)/(q - 1)$.

Fix $h \in F$ with $h^{q^t + 1} = -1$. The paper's polynomial is

$$\psi_{h,t}(x) = x^q + x^{q^{t-1}} - h^{1-q^{t+1}} x^{q^{t+1}} + h^{1-q^{2t-1}} x^{q^{2t-1}}.$$

The proof splits it as $\psi_{h,t} = L + M$ with

$$L(x) = x^q - h^{1-q^{t+1}} x^{q^{t+1}}, \qquad M(x) = x^{q^{t-1}} + h^{1-q^{2t-1}} x^{q^{2t-1}},$$

and it also uses the $\mathbb F_{q^t}$-linear maps $R(x) = x^{q^t} + h^{q^{t-1}-q} x$ and $T(x) = x^{q^t} + h^{q-q^{t-1}} x$. The Lean development uses the same letters: psi, Lmap, Mmap, Rmap, Tmap, IsScatteredPoly, qpoly, graph.

Formalization targets

Goal: Theorem 3.1

For $q$ odd, $n = 2t$, $t \ge 3$, and every $h \in \mathbb F_{q^n} \setminus \mathbb F_{q^t}$ with $h^{q^t+1} = -1$,

$$\forall z, y \in \mathbb F_{q^n}^* :\quad \frac{\psi_{h,t}(z)}{z} = \frac{\psi_{h,t}(y)}{y} \;\Longrightarrow\; \exists c \in \mathbb F_q,\ z = c\,y .$$

Milestones

1. The equivalence of three conditions (§1, p. 2): $L_f$ is scattered; $f$ is scattered; and $f(\gamma x) = \gamma f(x)$ with $x \neq 0$ forces $\gamma \in \mathbb F_q$.
2. Proposition 3.2: $h^{q^t+1} = -1$ implies $h^{q^2+1} \neq 1$ and $h^{q^{t-2}} \neq -h$.
3. $L$ and $M$ are $\mathbb F_{q^t}$-semilinear (p. 7).
4. The kernels of $L$ and $M$, displays (4)–(5), are 1-dimensional $\mathbb F_{q^t}$-subspaces.
5. The images of $L$ and $M$, displays (6)–(7), are 1-dimensional $\mathbb F_{q^t}$-subspaces.
6. Proposition 3.3: $\mathbb F_{q^n} = \ker L \oplus \ker M = \operatorname{im} L \oplus \operatorname{im} M$.
7. $\dim \ker R = \dim \ker T = 1$ and $\ker T = h^{q^{t-1}-q}\ker R$ (p. 8).
8. Lemma 3.4: the $\mathbb F_{q^t}$-bases $\{1, \rho\}$, $\{1, \tau\}$ and the change of components (9).
9. Proposition 3.5: $a \in \ker R \iff av \in \ker L \iff aM(u) \in \operatorname{im} L$.
10. Proposition 3.6: $b \in \ker T \iff bu \in \ker M \iff bL(v) \in \operatorname{im} M$.

Significance

The result. Theorem 3.1 produces, for every odd $q$ and even $n \ge 6$, maximum scattered linear sets of $\mathrm{PG}(1, q^n)$ and MRD codes of $\mathbb F_q^{n \times n}$ with minimum distance $n - 1$. For $t = 3$ the polynomials $\psi_{h,3}$ are those of Bartoli, Zanella and Zullo. If $h$ were allowed in $\mathbb F_{q^t}$, then $h \in \mathbb F_{q^2}$ and $\psi_{h,t}$ would reduce to the Longobardi–Zanella polynomials (p. 6). The second half of the paper (Theorem 5.1, a companion mission) shows that for $t > 4$ the family contains a number of $\mathrm{P\Gamma L}$-inequivalent members that grows exponentially in $n$. Every previously known family contributes fewer than $q^2\varphi(n)/2$ classes.

Formalizing it. The theorem has a complete published proof. No scattered polynomial, linear set of the projective line or linearized-polynomial kernel computation is formalized on the platform, and none appears in Mathlib. The work is to formalize the paper's proof: the semilinear-algebra lemmas of §3 and the case analysis that follows them. The milestones are reusable statements about $q$-polynomials of $\mathbb F_{q^{2t}}$ seen as an $\mathbb F_{q^t}$-plane.

Difficulty

Writing $\psi_{h,t}(\gamma x) = \gamma \psi_{h,t}(x)$ out coefficient by coefficient gives a system in $x$ and $\gamma$ with exponents $q, q^{t\pm1}, q^{2t-1}$ that does not separate directly. The paper's route goes through two $\mathbb F_{q^t}$-direct-sum decompositions of $\mathbb F_{q^n}$ and two changes of $\mathbb F_{q^t}$-basis. Each identity involves negative powers of $h$ and holds only through $h^{q^t+1} = -1$ and the parity of $q$. The hypothesis $h \notin \mathbb F_{q^t}$ enters only at the end, and a formalization must carry the arithmetic of the exponent towers modulo $q^{2t} - 1$ throughout. The tempting shortcut, checking the statement on a few small fields, proves nothing: the theorem is uniform in $q$ and $t$.

Formalization scope

• Field. $F$ is a finite field with CharP F p, p prime, Odd p, $q = p^r$ with $r \ge 1$ (an explicit q with hq : q = p ^ r), and Fintype.card F = q ^ (2 * t). So $F$ is $\mathbb F_{q^{2t}}$ up to isomorphism, and no particular model is chosen.
• Subfields. $\mathbb F_q$ and $\mathbb F_{q^t}$ are the fixed fields of $x \mapsto x^q$ and $x \mapsto x^{q^t}$, taken from the published definition ScatCaps.LinearSets.subfieldOf F p r m.
• Scattered. "Scattered" is the literal definition of p. 2, with $z, y$ ranging over all of $F^*$. The scattered-linear-set side of milestone 1 uses the published weight-one predicate ScatCaps.LinearSets.IsScattered, which is equivalent to the cardinality definition of p. 1.
• Powers of $h$. A negative or difference power of $h$ is written as a field quotient, e.g. $h^{1-q^{t+1}}$ as h / h ^ q ^ (t+1). This is exact because $h^{q^t+1} = -1$ forces $h \neq 0$. Natural-number subtractions in exponents ($t-1$, $2t-1$, $3t-2$) are exact in the stated ranges.
• Linear-algebra encodings. "1-dimensional $\mathbb F_{q^t}$-subspace" means closed under addition and $\mathbb F_{q^t}$-scalars, containing $0$, and of cardinality $|\mathbb F_{q^t}|$ (published IsFqSubspace, HasRank). A direct sum is stated as unique decomposition, and an $\mathbb F_{q^t}$-basis $\{1, \rho\}$ as unique representation $\lambda + \mu\rho$ with $\lambda, \mu \in \mathbb F_{q^t}$.
• Pinned readings. (1) The standing hypotheses of §3 ($q$ odd, $n = 2t$, $t \ge 3$, $h^{q^t+1} = -1$) are carried into every §3 lemma, even where its printed statement omits them. $h \notin \mathbb F_{q^t}$ is added only to Theorem 3.1, because the lemmas do not use it. (2) Proposition 3.2 is printed with $t \ge 1$ and without "$q$ odd". "$q$ odd" is added (its proof uses it, and $q$ even gives a counterexample), and $h^{q^{t-2}}$ is read as $h^{q^{3t-2}}$, which is equal to it for $t \ge 2$ and defined at $t = 1$.
• Ruling out trivial versions. A formalization in which $\mathbb F_q$ is the whole field (every map is then "scattered"), in which $\gamma$ or $z, y$ range only over a subfield, or in which $h^{1-q^{t+1}}$ is a truncated natural-number power, would not state the theorem. The statements here quantify over all of $F^*$ and conclude membership in the fixed field of $x \mapsto x^q$.
• Infrastructure. A complete development needs: Frobenius iterates on finite fields, fixed fields and their cardinalities, kernels and images of $\mathbb F_{q^t}$-semilinear maps of $\mathbb F_{q^{2t}}$, and the solution count of $x^{q^t - 1} = c$. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• G. Longobardi, G. Marino, R. Trombetti, Y. Zhou, A large family of maximum scattered linear sets of PG(1, q^n) and their associated MRD codes, arXiv:2102.08287v3, 2021 (Combinatorica 43, 2023). https://arxiv.org/abs/2102.08287v3
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geometriae Dedicata 81, 2000.
• G. Lunardon, O. Polverino, Blocking sets and derivable partial spreads, J. Algebraic Combin. 14, 2001.
• J. Sheekey, A new family of linear maximum rank distance codes, Adv. Math. Commun. 10(3), 2016.
• G. Longobardi, C. Zanella, Linear sets and MRD-codes arising from a class of scattered linearized polynomials, J. Algebraic Combin., 2021. https://doi.org/10.1007/s10801-020-01011-9
• D. Bartoli, C. Zanella, F. Zullo, A new family of maximum scattered linear sets in PG(1, q^6), Ars Math. Contemp. 19(1), 2020.
• B. Csajbók, G. Marino, O. Polverino, C. Zanella, A new family of MRD-codes, Linear Algebra Appl. 548, 2018.
• B. Csajbók, G. Marino, F. Zullo, New maximum scattered linear sets of the projective line, Finite Fields Appl. 54, 2018.
• D. Bartoli, Y. Zhou, Exceptional scattered polynomials, J. Algebra 509, 2018.
• M. Lavrauw, G. Van de Voorde, Field reduction and linear sets in finite geometry, Contemp. Math. 632, AMS, 2015, pp. 271–293.
• O. Polverino, Linear sets in finite projective spaces, Discrete Math. (22): 3096–3107, 2010.

Motivation

Incidence bounds count how often points can lie on lines, planes or other simple objects. Over the reals the model result is the Szemerédi–Trotter theorem for points and lines in the plane (Szemerédi–Trotter 1983). Its proofs use the order or topology of $\mathbb R$ (cuttings, crossing numbers, polynomial partitioning), so they say nothing over finite fields or fields of positive characteristic. These are the settings that matter for the sum–product problem in $\mathbb F_p$ and for the finite-field versions of Erdős-type distance problems, where the absence of an incidence theorem was long the bottleneck.

M. Rudnev, On the number of incidences between points and planes in three dimensions (Combinatorica 38 (2018), doi:10.1007/s00493-016-3329-6), proves a point–plane incidence bound in $\mathbb P^3$ valid over every field of characteristic $\neq2$, with a constraint only in terms of the characteristic. It became the standard tool for sum–product estimates in positive characteristic: for example, Roche-Newton, Rudnev and Shkredov and Stevens and de Zeeuw build their bounds on it.

Timeline:

• 2010: Guth and Katz settle the Erdős distinct-distances problem in $\mathbb R^2$ via a bound on line–line incidences in $\mathbb R^3$ (arXiv:1011.4105). The part of their argument that uses no ordering of $\mathbb R$ rests on the Cayley–Salmon–Monge theorem on ruled surfaces.
• 2014: Kollár carries the Guth–Katz line–line bound over to arbitrary fields under the constraint $n=O(p^2)$ (arXiv:1405.2243).
• 2014–2015: Rudnev (arXiv:1407.0426, versions v1–v5) reduces point–plane incidences in $\mathbb P^3$ to line–line incidences on a three-dimensional quadric in $\mathbb P^5$, and proves the line–line bound there.
• 2016: de Zeeuw gives a shorter proof of the same bound, using the Guth–Katz–Kollár line theorem in $\mathbb P^3$ (arXiv:1612.02719).

Setting

Let $\mathbb F$ be a field and $\mathbb P^3$ the projective three-space over $\mathbb F$. A point $q=(q_0:q_1:q_2:q_3)$ and a plane $\pi=(\pi_0:\pi_1:\pi_2:\pi_3)$ are both nonzero vectors of $\mathbb F^4$ up to scaling. The point lies on the plane, $q\in\pi$, when $q_0\pi_0+q_1\pi_1+q_2\pi_2+q_3\pi_3=0$. A line of $\mathbb P^3$ is a 2-dimensional subspace of $\mathbb F^4$. For finite sets $P$ of $m$ points and $\Pi$ of $n$ planes, the incidence count is

$$|I(P,\Pi)|=\#\{(q,\pi)\in P\times\Pi:\ q\in\pi\}.$$

The collinearity parameter $k$ is the largest number of planes of $\Pi$ that contain a common line.

The proof works in the space of lines of $\mathbb P^3$. The line through $q$ and $u$ has Plücker vector $L=(P_{01}:P_{02}:P_{03}:P_{23}:P_{31}:P_{12})\in\mathbb P^5$, $P_{ij}=q_iu_j-q_ju_i$. These vectors fill the Klein quadric $\mathcal K=\{P_{01}P_{23}+P_{02}P_{31}+P_{03}P_{12}=0\}$. A point $q$ defines its α-plane (the lines through $q$) and a plane $\pi$ its β-plane (the lines in $\pi$), both projective planes inside $\mathcal K$. Cutting $\mathcal K$ with a hyperplane $S$ that is not tangent to it gives a three-quadric $\mathcal G=\mathcal K\cap S\subset S\cong\mathbb P^4$, and every α- and β-plane meets $\mathcal G$ in a line.

Formalization targets

Goal: Theorem 3

There are absolute constants $c,C>0$ such that for every field $\mathbb F$ of characteristic $\neq2$, every set $P$ of $m$ points and every set $\Pi$ of $n\le m$ planes in $\mathbb P^3$, with $n\le cp^2$ when $\mathbb F$ has positive characteristic $p$,

$$|I(P,\Pi)|\le C\big(m\sqrt n+km\big).$$

In characteristic $0$ there is no constraint on $n$.

Milestones

The proof decomposes as: point–plane incidences in $\mathbb P^3$ equal line–line incidences between two families of mutually skew lines in $\mathcal G$ (Lemma 9), and those are bounded by

$$|I(L_\alpha,L_\beta)|\le C\big(m\sqrt n+km\big)\qquad(\text{Theorem 12}),$$

where $k$ now counts lines of $L_\beta$ in a three-dimensional section of $\mathcal G$. The supporting milestones are: the incidence criterion (9) for Plücker vectors, the intersection pattern of α- and β-planes, Lemma 6 on sections of $\mathcal G$, the generic projection from $\mathbb P^4$ to $\mathbb P^3$, the existence of a low-degree vanishing polynomial, the bound of $d$ zeros on a line, and Salmon's theorem (Theorem 2) on surfaces with many lines.

Significance

Theorem 3 gives the incidence bound $O(m\sqrt n+km)$ with no assumption on the field beyond characteristic. The paper shows that its main term is sharp in positive characteristic under the constraint $\min(m,n)=O(p^2)$ alone (Remark 4), and that the bound is tight for $n=m$, $k=\sqrt m$ (§6.2). It yields the paper's applications (distinct bilinear products of a planar point set over $\mathbb F_p$, and a pinned Erdős distance bound in positive characteristic), and it is the incidence input to sum–product estimates over $\mathbb F_p$ such as $|AA|+|A+A|\gg|A|^{6/5}$.

The theorem is proved and published; it is not open. As far as is known, neither it nor its ingredients (the Klein correspondence in Plücker coordinates, the Guth–Katz polynomial argument over an arbitrary field, Salmon's theorem) has a machine-checked proof. This mission's statements give a formal target for the whole chain. Several milestones (the Plücker incidence criterion, the vanishing polynomial, zeros on a line, the generic projection) are standard facts of projective geometry over arbitrary fields that are useful well beyond this paper.

Difficulty

The obvious route, cell decomposition by polynomial partitioning as over $\mathbb R$, fails over a general field: there is no ordering, so no cells. The Guth–Katz algebraic argument survives, but in $\mathbb P^3$ it needs the hypothesis that few lines are concurrent, which point–plane arrangements violate. Rudnev's way out is to move the problem into the three-quadric $\mathcal G$. There the two line families are skew within themselves, and the collinearity parameter $k$ becomes a count of lines in a three-dimensional section of $\mathcal G$.

The hard step is Theorem 12. It needs the polynomial method over an arbitrary field together with Salmon's theorem on flecnodal surfaces. That theorem holds in characteristic $p$ only for degree $d<p$, which is the source of the constraint $n=O(p^2)$. It also needs a structure theory of ruled surfaces to rule out many incidences inside non-quadric ruled components. Salmon's theorem alone has no formal proof anywhere.

Formalization scope

Points and planes of $\mathbb P^3$ are elements of Mathlib's ℙ F (Fin 4 → F). Finite sets of them are Finsets of projective classes, so they contain distinct points and planes. Incidence is Projectivization.orthogonal. Lines of $\mathbb P^3$, $\mathbb P^4$ and $\mathbb P^5$ are 2-dimensional subspaces. Two lines meet when their intersection is a nonzero subspace, and they are skew when it is zero. Plücker vectors are indexed in the order $(P_{01},P_{02},P_{03},P_{23},P_{31},P_{12})$. A hyperplane $S$ of $\mathbb P^5$ is given by its covector $(\boldsymbol u:\boldsymbol w)$, and "not tangent to $\mathcal K$" is $\boldsymbol u\cdot\boldsymbol w\neq0$. A three-subspace of $S$ is a 4-dimensional subspace of $S$.

Committed conventions:

• The constants $c$ and $C$ of Theorems 3 and 12 are quantified before the field and the configuration, because the paper declares $O(\cdot)$ and $c$ absolute (p. 1).
• "$n=O(p^2)$" is read as $n\le cp^2$ for an existential absolute $c>0$. It applies only in positive characteristic.
• $k$ is any upper bound on the relevant count, which is equivalent to the maximum because the bound is monotone in $k$.
• The field ranges over Type. Bounds are stated in $\mathbb R$, and Salmon's threshold $d(11d-24)$ is computed in $\mathbb Z$.
• "Ruled" means that every point of the surface lies on a line contained in it.
• Lemma 6 carries the hypothesis $S_1\neq S_2$, without which it is false.

Trivializing formalizations are excluded:

• the constants may not depend on the field, the characteristic or $k$;
• the characteristic constraint is not imposed in characteristic $0$, where it would force $n=0$;
• $k$ is not a junk supremum over the infinitely many lines;
• vector Finsets that would count one point twice are not used;
• Theorem 12 is about lines in $\mathcal G\subset\mathbb P^4$, not lines in $\mathbb P^3$ (that would be the Guth–Katz theorem, with different hypotheses).

A complete development needs Plücker coordinates and the Klein correspondence over arbitrary fields, homogeneous polynomials on $\mathbb P^3$ and their zero sets, irreducible factorization, Salmon's theorem, and the Guth–Katz induction. Lemma 8 of the paper (generators of ruled surfaces as curves in $\mathcal K$) is not posed. Proofs of any milestone are welcome, as are proofs of the projective-geometry milestones as standalone Mathlib-style lemmas.

Selected references

• M. Rudnev, On the number of incidences between points and planes in three dimensions, Combinatorica 38 (2018); arXiv:1407.0426v5 (the version formalized). https://arxiv.org/abs/1407.0426
• L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. 181 (2015) 155–190. https://arxiv.org/abs/1011.4105
• J. Kollár, Szemerédi–Trotter-type theorems in dimension 3, Adv. Math. 271 (2015) 30–61. https://arxiv.org/abs/1405.2243
• J. F. Voloch, Surfaces in $\mathbb P^3$ over finite fields, Contemp. Math. 324 (2003). https://doi.org/10.1090/conm/324
• F. de Zeeuw, A short proof of Rudnev's point-plane incidence bound, arXiv:1612.02719 (2016). https://arxiv.org/abs/1612.02719
• E. Szemerédi, W. T. Trotter, Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194

Motivation

A proper coloring of a graph assigns colors to its vertices so that adjacent vertices get different colors; the least number of colors that suffices is the chromatic number $\chi(G)$. The clique number $\omega(G)$ is the size of a largest set of pairwise adjacent vertices, and $\chi(G)\ge\omega(G)$ always. A class of graphs is $\chi$-bounded if $\chi$ is bounded by a function of $\omega$ on the class. Abstract triangle-free graphs ($\omega\le2$) of arbitrarily large chromatic number have been known since Zykov (1949) and Mycielski (1955), so the question is which geometric classes are $\chi$-bounded.

For geometric intersection graphs (one vertex per set, an edge for each intersecting pair) the history is as follows.

• 1960: Asplund and Grünbaum prove that families of axis-aligned rectangles in the plane are $\chi$-bounded.
• 1965: Burling constructs triangle-free families of axis-aligned boxes in $\mathbb R^3$ with arbitrarily large chromatic number.
• 1970s: Erdős asks whether families of line segments in the plane are $\chi$-bounded (Brass–Moser–Pach, Research Problems in Discrete Geometry, §9.6, Problem 2; Gyárfás 1987, Problem 1.9).
• 2000–2014: positive special cases. McGuinness (2000) obtains bounds for triangle-free families; Suk (2014) improves them, proving that families of segments meeting a common line, and families of unit-length segments, are $\chi$-bounded.
• 2014: Pawlik, Kozik, Krawczyk, Lasoń, Micek, Trotter and Walczak answer Erdős's question negatively (arXiv:1209.1595).

The same construction disproves Scott's conjecture (1997) that graphs excluding induced subdivisions of a fixed graph are $\chi$-bounded, as first observed by Fox and Pach.

Setting

Points of the plane are pairs $(x,y)\in\mathbb R\times\mathbb R$. A line segment is a closed set $\operatorname{seg}(u,v)=\{(1-t)u+tv: 0\le t\le1\}$ with two distinct endpoints $u\neq v$. A family of segments $\mathcal S=(\sigma_i)_{i<N}$ is a finite indexed list of pairwise distinct segments. Its intersection graph has vertex set $\{0,\dots,N-1\}$, and $i\neq j$ are adjacent exactly when $\sigma_i\cap\sigma_j\neq\emptyset$. The family is triangle-free if no three of its segments pairwise intersect, and $\chi(\mathcal S)$ is the chromatic number of its intersection graph.

The milestones use the paper's auxiliary notions. An axis-aligned rectangle is $R=[a,c]\times[b,d]$, with $x\in[a,c]$ and $y\in[b,d]$. For a family $\mathcal S$ inside the open interior of $R$, a probe for $(\mathcal S,R)$ is a rectangle $P=[a',c]\times[b',d']$ sharing the right edge line of $R$ such that (i) $a<a'<c$ and $b<b'<d'<d$; (ii) no segment meets the left edge of $P$; (iii) no segment has an endpoint in the closed rectangle $P$; (iv) the segments meeting $P$ are pairwise disjoint. The diagonal $D_P$ runs from the bottom-left corner $(a',b')$ to the top-right corner $(c,d')$ of $P$. The sequences $s_k,p_k$ are given by $s_1=p_1=1$, $s_{k+1}=(p_k+1)s_k+p_k^2$ and $p_{k+1}=2p_k^2$.

Formalization targets

Goal: Theorem 1 (p. 2)

For every integer $k\ge1$ there is a finite family $\mathcal S$ of distinct line segments in the plane with triangle-free intersection graph and

$$\chi(\mathcal S)>k .$$

The goal fixes no size for $\mathcal S$ and no particular construction.

Milestones

1. Base case of Lemma 2 (p. 3): one segment and one probe in any rectangle of positive area.
2. Diagonal claim (p. 3): for a probe $Q$ of a family inside the interior of $R$, a segment meets $D_Q$ if and only if it meets $Q$.
3. Color-count dichotomy (p. 4): for a proper coloring of an intersection graph and two index sets $X$, $Y$ each seeing at least $k$ colors, if the color sets differ then $X\cup Y$ sees at least $k+1$ colors; if they agree, a member adjacent to all of $Y$ gets a new color, and $X$ together with it sees at least $k+1$ colors.
4. Induction step (pp. 3–4): Lemma 2 at $k$ for every rectangle gives Lemma 2 at $k+1$ for every rectangle.
5. Lemma 2 (p. 3): for $k\ge1$ and a rectangle $R$ of positive area there are a triangle-free family $\mathcal S_k$ of exactly $s_k$ segments in the interior of $R$ and $p_k$ pairwise disjoint probes for $(\mathcal S_k,R)$ such that every proper coloring of $\mathcal S_k$ uses at least $k$ colors on the segments meeting some probe.
6. The family $\tilde{\mathcal S}_k$ (p. 4): adding the diagonals of all probes to a family with the conclusion of Lemma 2 gives a triangle-free family with $\chi>k$.

Significance

Theorem 1 shows that segment intersection graphs are not $\chi$-bounded, and it settles negatively the question for every class containing them: intersection graphs of curves crossing at most once (Kratochvíl–Nešetřil), McGuinness's class of arcwise connected sets with connected pairwise intersections, and string graphs in general. Through the Fox–Pach observation it refutes Scott's conjecture on induced subdivisions, a purely graph-theoretic statement. The counts in Lemma 2 give $|\tilde{\mathcal S}_k|=s_k+p_k$, so the maximum chromatic number of a triangle-free family of $n$ segments is $\Omega(\log\log n)$ (§4 of the paper). The family $\tilde{\mathcal S}_k$ has the same intersection graph as Burling's boxes.

The theorem is proved on paper; to the best of current knowledge no machine-checked proof exists. The mission produces a Lean 4 statement of the result about actual segments in $\mathbb R^2$, a reusable definition of intersection graphs of plane sets, and the paper's probe machinery stated precisely enough to support a full formal proof.

Difficulty

Abstract triangle-free graphs with large chromatic number are easy to build, but almost none of them are intersection graphs of segments, and the standard constructions (Mycielski, Zykov, shift graphs) do not come with a geometric realization. The difficulty is geometric: the construction has to place every new segment so that it meets exactly a prescribed independent set of old segments and nothing else, at every level of a doubly exponential nesting, while keeping finitely many rectangles disjoint and segment endpoints out of them. In a formal development the burden falls on the planar facts the paper treats as evident in one line each: which edges of a rectangle a segment can cross, when two segments must cross, and why the probe conditions survive when families are nested inside one another.

Formalization scope

• The plane is ℝ × ℝ (first coordinate $x$, second $y$), and segments are Mathlib's closed segment ℝ u v. A family is e : Fin N → (ℝ × ℝ) × (ℝ × ℝ) (endpoint pairs) with seg (e i) the $i$-th segment. "A family of line segments" is read as non-degenerate ((e i).1 ≠ (e i).2) and pairwise distinct (Function.Injective (fun i => seg (e i))).
• interGraph F : SimpleGraph ι is the intersection graph of an indexed family of plane sets: i ≠ j ∧ (F i ∩ F j).Nonempty. Triangle-free is CliqueFree 3; $\chi$ is Mathlib's chromaticNumber : ℕ∞, and the goal states the literal $(k:\mathbb N_\infty)<\chi$.
• Rectangles keep the page's letter order, Rect = ⟨a, c, b, d⟩ for $[a,c]\times[b,d]$, with positive area as a separate hypothesis. A probe is stored as $(a',b',d')$ and is the closed rectangle $[a',c]\times[b',d']$; the interior of $R$ is open.
• sSeq k, pSeq k are $s_k,p_k$, 1-based; every statement assumes $k\ge1$ (the value at $0$ is junk).
• Proper colorings take values in an arbitrary type, and "uses at least $k$ colors on the segments meeting $P$" is $k\le$ ncard of the image of those segments.
• The diagonal claim and the $\tilde{\mathcal S}_k$ milestone are stated for any data with the relevant properties, not only for the paper's construction; the hypotheses are exactly those the page's sentences use.
• The goal is about the intersection graph of the segments the existential provides. A statement about an abstract triangle-free graph with $\chi>k$ is a different, much weaker theorem (already available via Mycielski's construction) and does not count.

Needed infrastructure: elementary planar geometry of segments and axis-aligned rectangles (membership, edges, crossing of two segments via the intermediate value theorem), affine images of segment families, and finite coloring counts. The segment and intersection-graph definitions are reusable for other questions on geometric intersection graphs. Contributions are welcome on any milestone, in particular a complete proof of the diagonal claim and of the induction step.

Selected references

• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free intersection graphs of line segments with large chromatic number, J. Combin. Theory Ser. B 105 (2014) 6–10; preprint arXiv:1209.1595v5 (2014). https://arxiv.org/abs/1209.1595
• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free geometric intersection graphs with large chromatic number, Discrete Comput. Geom. 50(3) (2013) 714–726. https://arxiv.org/abs/1212.2058
• J. P. Burling, On coloring problems of families of prototypes, PhD thesis, University of Colorado, Boulder, 1965.
• E. Asplund, B. Grünbaum, On a colouring problem, Math. Scand. 8 (1960) 181–188.
• P. Brass, W. Moser, J. Pach, Research Problems in Discrete Geometry, Springer, 2005.
• A. Gyárfás, Problems from the world surrounding perfect graphs, Zastos. Mat. 19 (1987) 413–441.
• A. Suk, Coloring intersection graphs of x-monotone curves in the plane, Combinatorica 34(4) (2014) 487–505.
• A. D. Scott, Induced trees in graphs of large chromatic number, J. Graph Theory 24(4) (1997) 297–311.
• J. Mycielski, Sur le coloriage des graphes, Colloq. Math. 3 (1955) 161–162.