Algebra

Motivation

Multivariate multipoint evaluation asks for the values $f(\alpha_0), \dots, f(\alpha_{N-1})$ of one polynomial $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ at $N$ points of $\mathbb F_q^m$. Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of $f(g(X)) \bmod h(X)$ for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.

The paper gives two such algorithms. Section 4 works over any ring $\mathbb Z/r\mathbb Z$ and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the $m$-variate $f$ at a point be read off from the evaluation of a single univariate polynomial $f^*$ at a related point of an extension ring.

Setting

Let $p$ be a prime and $\mathbb F_q$ a finite field of characteristic $p$. Fix integers $m \ge 0$ and $d \ge 1$. Let $h = p^c$ be a power of $p$ with $h > m^2 d$ (the paper takes the least such power), and let $P(W) \in \mathbb F_p[W]$ be a polynomial of degree $c$ that is irreducible over $\mathbb F_p$. Then:

• $K = \mathbb F_p[W]/(P(W))$ is a field with $h$ elements. Let $\eta$ be a primitive element of $K$, a generator of its multiplicative group, so $\eta$ has multiplicative order $h-1$.
• $R = \mathbb F_q[W]/(P(W))$, with $P$ viewed over $\mathbb F_q$. $P$ need not remain irreducible over $\mathbb F_q$, so $R$ is a ring containing $\mathbb F_q$ and $K$ but in general not a field.
• $\sigma : R \to R$, $x \mapsto x^h$, is a power of the Frobenius endomorphism; $\sigma^i$ is $x \mapsto x^{h^i}$. On $\mathbb F_q$ it is an automorphism, with inverse $\sigma^{-i}$.
• $E(Z) = Z^{h-1} - \eta \in R[Z]$ and $S = R[Z]/(E(Z))$. Every element of $S$ has a canonical representative, its remainder modulo the monic $E$, of degree less than $h-1$.

Three maps connect the problem to $S$:

• the lift $\varphi : \mathbb F_q^m \to S$ sends $\alpha = (\alpha_0, \dots, \alpha_{m-1})$ to the class of the polynomial $g_\alpha(Z) \in R[Z]$ of degree at most $m-1$ with $g_\alpha(\eta^i) = \sigma^{-i}(\alpha_i)$ for $i = 0, \dots, m-1$ (Eq. (6.1));
• the projection $\pi : S \to R$ sends an element with canonical representative $g(Z)$ to $g(1)$;
• the Kronecker substitution sends $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ to the univariate

$$f^*(Y) = f\big(Y, Y^h, Y^{h^2}, \dots, Y^{h^{m-1}}\big) \in S[Y].$$

In the Lean development these are K, R, h, ι (the inclusion $K \subseteq R$), sigma i ($=\sigma^i$), E, S, sigmaInv i ($=\sigma^{-i}$ on $\mathbb F_q$), gAlpha, phi, pi, gIter ($g_\alpha^{(i)}$) and fStar, in the namespace KedlayaUmans.FrobeniusLift.

Formalization targets

Goal: Lemma 6.1 (p. 19)

For every $f \in \mathbb F_q[X_0, \dots, X_{m-1}]$ with degree at most $d-1$ in each variable and every $\alpha \in \mathbb F_q^m \subseteq R^m$,

$$\pi\big(f^*(\varphi(\alpha))\big) = f(\alpha).$$

Milestones, in the order the proof uses them

1. Properties of $\eta$ (p. 18): $\eta$ has order $h-1$ in $R$, and $\eta^i - \eta^j$ is a unit of $R$ for $i \ne j$ in $\{0, \dots, m-1\}$.
2. Eq. (6.1) (p. 19): $\sigma^i(\sigma^{-i}(a)) = a$ for $a \in \mathbb F_q$; $\deg g_\alpha \le m-1$; $g_\alpha(\eta^i) = \sigma^{-i}(\alpha_i)$.
3. The Frobenius congruence (p. 19): $\eta$ is fixed by $\sigma$, and $(g(Z))^{h^i} \equiv \sigma^i(g)(\eta^i Z) \pmod{E(Z)}$ for every $g \in R[Z]$.
4. Eq. (6.2) (p. 19): with $g_\alpha^{(i)} = g_\alpha^{h^i} \bmod E$, $\deg g_\alpha^{(i)} = \deg g_\alpha$ and $g_\alpha^{(i)}(1) = \alpha_i$ for $i < m$.
5. No reduction (pp. 19–20): the canonical representative of $f^*(\varphi(\alpha))$ is $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)}) \bmod E$, and this remainder equals $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)})$ itself.

Significance

The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate $f$ at $N$ points one computes the $N$ lifts $\varphi(\alpha_k)$, evaluates the one univariate polynomial $f^*$ at all of them by fast univariate multipoint evaluation, and projects back with $\pi$. Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth $\deg f^* \le dm\,h^m$. Corollary 6.3 turns this into an operation count of $(dm+N)^{1+\delta}$ for every $\delta>0$, provided $m \le d^{o(1)}$ and the characteristic satisfies $p \le d^{o(1)}$.

Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for $\varphi$, the canonical-representative projection for $\pi$) and splits its proof into the five steps above. The definitions of the rings $R$ and $S$, the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).

Difficulty

The obvious attempt is to treat $\pi$ as evaluation at $Z = 1$ and push it through $f^*$. This fails: $E(1) = 1 - \eta$ is a unit, not zero, so evaluation at $1$ does not factor through $S = R[Z]/(E)$, and $\pi$ is not a ring homomorphism. The identity holds only because the polynomial $f(g_\alpha^{(0)}, \dots, g_\alpha^{(m-1)})$ is already reduced modulo $E$, which requires both the degree bound $h - 1 \ge m^2 d$ and the fact that raising to the power $h^i$ does not raise the degree of $g_\alpha$ modulo $E$. The second fact depends on $\eta$ being fixed by $\sigma$ and on $\eta^{(h^i-1)/(h-1)} = \eta^i$. The equality $\deg g_\alpha^{(i)} = \deg g_\alpha$ further needs that $\sigma^i$ does not kill the leading coefficient in $R$, a ring with possible zero divisors. Finally, interpolation must happen in $R$, not a field, which is possible only because the nodes $\eta^i$ lie in the subfield $K$.

Formalization scope

• $\mathbb F_q$ is a type F with [Field F] [Fintype F] [CharP F p], $p$ a prime ([Fact p.Prime]). $P$ is a polynomial over ZMod p with [Fact (Irreducible P)]; $c$ is P.natDegree and $h$ is p ^ P.natDegree. $R$ is AdjoinRoot of $P$ mapped to F; $R$ is never assumed to be a field and $P$ is never assumed irreducible over F.
• The paper's $h$ is the least power of $p$ above $m^2 d$; the statements assume only m ^ 2 * d < h, which contains the paper's case. $d \ge 1$ is a hypothesis.
• "Primitive element" is IsPrimitiveRoot η (h - 1), equivalent to generating $K^\times$ since $|K| = h$.
• "Individual degrees $d-1$" means at most $d-1$: ∀ i, f.degreeOf i ≤ d - 1.
• Variables and points are indexed by Fin m, starting at $0$; $f^*$ substitutes $Y^{h^i}$ for $X_i$.
• $g_\alpha$ is the explicit Lagrange interpolant: Mathlib's Lagrange.basis over the field $K$ at the nodes $\eta^0, \dots, \eta^{m-1}$, mapped into $R[Z]$, with coefficients $\sigma^{-i}(\alpha_i)$. $\pi$ is the remainder modulo $E$ (AdjoinRoot.modByMonicHom) evaluated at $1$.
• Only correctness is formalized. The operation counts of Theorem 6.2 and Corollary 6.3, and the cost of finding $P$ and $\eta$, are out of scope.

A formalization that takes $\varphi(\alpha)$ to be any element satisfying (6.2), or defines $\pi$ as a ring homomorphism, would make the goal trivial or false; both are ruled out because $\varphi$ and $\pi$ are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.

Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic $p$ ($g^{p} = \sigma(g)(Z^{p})$, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of $R$ (from separability of $P$ over the perfect field $\mathbb F_p$). Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381, version of Aug. 31, 2008. http://drops.dagstuhl.de/opus/volltexte/2008/1777
• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, SIAM J. Comput. 40(6), 2011. https://doi.org/10.1137/08073408X
• F. Parvaresh, A. Vardy, Correcting errors beyond the Guruswami–Sudan radius in polynomial time, FOCS 2005, pp. 285–294. https://doi.org/10.1109/SFCS.2005.29
• V. Guruswami, A. Rudra, Explicit capacity-achieving list-decodable codes, STOC 2006, pp. 1–10. https://doi.org/10.1145/1132516.1132518

Motivation

Multivariate multipoint evaluation asks for the values $f(\alpha_0),\dots,f(\alpha_{N-1})$ of a polynomial $f(X_0,\dots,X_{m-1})$ over a ring $R$, with individual degrees at most $d-1$, at $N$ given points of $R^m$. Kedlaya and Umans showed that, over finite fields and rings $(\mathbb Z/r\mathbb Z)[Z]/(E(Z))$, this problem can be solved in time nearly linear in the input size $d^m + mN$, for $m \le d^{o(1)}$ (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of $f(g(X)) \bmod h(X)$, to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over $\mathbb F_q$, with $O(n^{1.5+o(1)}\log^{1+o(1)} q + n^{1+o(1)}\log^{2+o(1)} q)$ bit operations for a randomized algorithm on degree-$n$ polynomials (abstract and §8).

Timeline. Brent and Kung (1978) gave the $O(n^{(\omega+1)/2})$ baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.

Setting

Let $r \ge 1$ and write $\mathbb Z/r\mathbb Z$ for the integers modulo $r$. Every element of $\mathbb Z/r\mathbb Z$ has a lift, its representative in $\{0,\dots,r-1\}$. For $f \in (\mathbb Z/r\mathbb Z)[X_0,\dots,X_{m-1}]$, $\tilde f \in \mathbb Z[X_0,\dots,X_{m-1}]$ replaces each coefficient by its lift; $\tilde\alpha \in \mathbb Z^m$ lifts a point coordinatewise.

Algorithm MULTIMODULAR with degree parameter $d$ and $t \ge 1$ rounds takes $f$ (degree at most $d-1$ in each variable) and a point $\alpha$. It lists the primes $p_1,\dots,p_k$ at most $\ell = 16\log(d^m(r-1)^{md})$, reduces $\tilde f$ and $\tilde\alpha$ modulo each $p_h$, and evaluates the reductions $f_h(\alpha_h) \in \mathbb F_{p_h}$. It does this directly when $t = 1$, and by recursion with $t-1$ rounds otherwise. It then returns, reduced modulo $r$, the unique integer in $\{0,\dots,p_1\cdots p_k - 1\}$ congruent to $f_h(\alpha_h)$ modulo every $p_h$.

Let $E(Z) \in (\mathbb Z/r\mathbb Z)[Z]$ be monic of degree $e$ and $R = (\mathbb Z/r\mathbb Z)[Z]/(E(Z))$. The lift of $x \in R$ is its representative of degree at most $e-1$, with coefficients lifted to $\{0,\dots,r-1\}$, an element of $\mathbb Z[Z]$. Put

$$M = d^m\bigl(e(r-1)\bigr)^{(d-1)m+1} + 1,\qquad r' = M^{(e-1)dm+1}.$$

Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.

1. Lift $f \in R[X_0,\dots,X_{m-1}]$ and $\alpha \in R^m$ to $\mathbb Z[Z]$.
2. Substitute $Z = M$ and reduce modulo $r'$.
3. Run MULTIMODULAR over $\mathbb Z/r'\mathbb Z$, obtaining $\beta$.
4. Form the polynomial $Q(Z)$ whose coefficients are the base-$M$ digits of $\beta$, and return $Q$ reduced modulo $r$ and $E(Z)$.

Formalization targets

Goal: Theorem 4.4 (correctness)

For $E$ monic of degree $e \ge 1$, $m \ge 1$, $d \ge 2$, $t \ge 1$, every $f \in R[X_0,\dots,X_{m-1}]$ of degree at most $d-1$ in each variable, and every $\alpha \in R^m$:

$$\mathrm{MULTIMODULAR\text{-}FOR\text{-}EXTENSION\text{-}RING}_d(f,\alpha,t) = f(\alpha).$$

Milestones

In the order the paper's proofs use them:

1. Lemma 2.4. For every integer $N \ge 2$, $\displaystyle\prod_{p \le 16\log N} p > N$.
2. Magnitude bound (proof of Theorem 4.2). $0 \le \tilde f(\tilde\alpha) \le d^m(r-1)^{md} < p_1\cdots p_k$.
3. Theorem 4.2 (correctness). $\mathrm{MULTIMODULAR}_d(f,\alpha,r,t) = f(\alpha)$ over $\mathbb Z/r\mathbb Z$.
4. Coefficient bound (proof of Theorem 4.4). $\tilde f(\tilde\alpha) \in \mathbb Z[Z]$ has degree at most $(e-1)dm$ and coefficients in $\{0,\dots,M-1\}$.
5. Coincidence (proof of Theorem 4.4). The digit polynomial $Q$ of $\bar f(\bar\alpha)$ equals $\tilde f(\tilde\alpha)$, and the reduction of $\tilde f(\tilde\alpha)$ modulo $r$ and $E(Z)$ is $f(\alpha)$.

Significance

The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form $(\mathbb Z/r\mathbb Z)[Z]/(E(Z))$, which includes every finite field $\mathbb F_q$. Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree-$n$ polynomials over $\mathbb F_q$ in $n^{1+o(1)}\log^{1+o(1)} q$ bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).

The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold $16\log N$, and the base-$M$ digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all $N \ge 2$, and is reusable independently of this mission.

Difficulty

The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to $16\log N$, so its correctness depends on the explicit inequality of Lemma 2.4 for every $N \ge 2$, not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer $\beta$ produced over $\mathbb Z/r'\mathbb Z$ must determine the polynomial $\tilde f(\tilde\alpha) \in \mathbb Z[Z]$ exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants $M$ and $r'$. A bound on $\tilde f(\tilde\alpha)$ evaluated at a point does not by itself suffice.

Formalization scope

Lean represents $\mathbb Z/r\mathbb Z$ as ZMod r with $r \ge 1$ (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed $0,\dots,m-1$, and $R$ as AdjoinRoot E for a monic E with $1 \le$ E.natDegree. "Degree at most $d-1$ in each variable" is ∀ i, f.degreeOf i ≤ d - 1. $\log$ is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes $p \le x$ for real $x$ are the primes $p \le \lfloor x\rfloor$. Each algorithm is defined for a single evaluation point, since the paper processes the $N$ points independently. The leaf $t = 1$ evaluates $f_h$ at $\alpha_h$ directly; that value is what Theorem 4.1's FFT algorithm outputs. $r'$ is $M^{(e-1)dm+1}$ as printed on p. 15; p. 16 prints $M^{(e-1)(d-1)m+1}$.

The hypotheses $d \ge 2$ and $m \ge 1$ are not written in the paper but are needed. For $r = 2$, $d = 1$, $f = 1$ the threshold $\ell$ is $0$, no prime is used, and MULTIMODULAR returns $0$. For $m = 0$ the inequality $d^m(r-1)^{(d-1)m+1} \le d^m(r-1)^{md}$ and the degree bound $(e-1)dm$ both fail.

Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from $\beta$ alone: an algorithm that evaluates $\tilde f(\tilde\alpha)$ in $\mathbb Z$ and reduces it, or that computes $f(\alpha)$ in $R$ directly, would make the theorems trivial and is not the algorithm stated here.

Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's $\theta$), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base-$M$ representations of polynomials. Lemma 2.4 and the base-$M$ uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381 (version of Aug. 31, 2008). http://drops.dagstuhl.de/opus/volltexte/2008/1777 — published in SIAM J. Comput. 40(6), 2011, https://doi.org/10.1137/08073408X.
• R. P. Brent, H. T. Kung, Fast algorithms for manipulating formal power series, J. ACM 25(4), 1978. https://doi.org/10.1145/322092.322099
• E. Kaltofen, V. Shoup, Subquadratic-time factoring of polynomials over finite fields, Math. Comp. 67, 1998. https://doi.org/10.1090/S0025-5718-98-00944-2
• J. von zur Gathen, J. Gerhard, Modern Computer Algebra, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9781139856065

Motivation

Modular composition asks, given univariate polynomials $f, g, h$ over a ring, for $f(g(X)) \bmod h(X)$. It is the bottleneck step in the classical algorithms for factoring univariate polynomials over finite fields (Cantor–Zassenhaus, von zur Gathen–Shoup, Kaltofen–Shoup), for irreducibility testing and for computing minimal polynomials. Brent and Kung (1978) gave an algorithm using $O(n^{(\omega+1)/2})$ operations for degree $n$, and for three decades no algorithm with a near-linear operation count was known in general.

Kedlaya and Umans (Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X) obtained near-linear modular composition over finite fields, and with it asymptotically faster algorithms for factoring polynomials over finite fields. Their route has two halves: a reduction of modular composition to multivariate multipoint evaluation (Section 3), and new fast algorithms for the latter (Sections 4 and 6). This mission formalizes the correctness of the first half, Theorem 3.1. The paper notes that Shoup and Smolensky used essentially the same transformation in an unpublished 1992 manuscript.

Setting

Throughout, $R$ is an arbitrary commutative ring. Variables are indexed from $0$.

MULTIVARIATE MULTIPOINT EVALUATION (Problem 2.1): given $f \in R[X_0, \dots, X_{m-1}]$ with individual degrees at most $d-1$ and points $\alpha_0, \dots, \alpha_{N-1} \in R^m$, output $f(\alpha_0), \dots, f(\alpha_{N-1})$.

MODULAR COMPOSITION (Problem 2.2): given $f \in R[X_0, \dots, X_{m-1}]$ with individual degrees at most $d-1$, and $g_0, \dots, g_{m-1}, h \in R[X]$ of degree at most $N-1$ with the leading coefficient of $h$ a unit, output $f(g_0(X), \dots, g_{m-1}(X)) \bmod h(X)$, the unique $r$ with $\deg r < \deg h$ and $h \mid f(g_0, \dots, g_{m-1}) - r$.

The inverse Kronecker map (Definition 2.3) $\psi_{h,\ell} : R[X_0, \dots, X_{m-1}] \to R[Y_{0,0}, \dots, Y_{m-1,\ell-1}]$ is the $R$-linear map that sends the monomial $\prod_i X_i^{e_i}$ to $\prod_i \prod_{j<\ell} Y_{i,j}^{a_{i,j}}$, where $e_i = \sum_{j \ge 0} a_{i,j} h^j$ is the base-$h$ expansion. It trades individual degree for number of variables: every individual degree of $\psi_{h,\ell}(f)$ is below $h$.

The algorithm of Theorem 3.1 takes $2 \le d_0 < d$, sets $\ell = \lceil \log_{d_0} d \rceil$ and $N' = N m \ell d_0$, receives points $\beta_0, \dots, \beta_{N'-1} \in R$ whose differences are units, and

1. computes $f' = \psi_{d_0,\ell}(f)$;
2. computes $g_{i,j} = g_i^{d_0^{\,j}} \bmod h$ for all $i$ and $j < \ell$;
3. computes $\alpha_{i,j,k} = g_{i,j}(\beta_k)$;
4. computes $f'(\alpha_{0,0,k}, \dots, \alpha_{m-1,\ell-1,k})$ for $k < N'$ (one multivariate multipoint evaluation);
5. interpolates these $N'$ values at the nodes $\beta_k$;
6. outputs the result modulo $h$.

Formalization targets

Goal: Theorem 3.1, correctness

$$\mathrm{algorithm}(d_0, d, f, g, h, \beta) \;=\; f\bigl(g_0(X), \dots, g_{m-1}(X)\bigr) \bmod h(X),$$

for all $m, N \ge 1$, $2 \le d_0 < d$, $f$ with individual degrees $\le d-1$, $g_i, h$ of degree $\le N-1$ with $\mathrm{lc}(h)$ a unit, and $\beta_0, \dots, \beta_{N'-1}$ distinct with unit differences. The right-hand side is stated through the characterization of the remainder (divisibility by $h$ and degree below $\deg h$).

Milestones (in the order the proof uses them)

• Definition 2.3, remark: if every individual degree of $f$ is at most $h^\ell - 1$, then $\psi_{h,\ell}(f)\bigl(X_0^{h^0}, \dots, X_{m-1}^{h^{\ell-1}}\bigr) = f$.
• Definition 2.3, remark: $\psi_{h,\ell}$ is injective on such polynomials (not used by the goal).
• Proof of Theorem 3.1: $f'(g_{0,0}, \dots, g_{m-1,\ell-1}) \equiv f(g_0, \dots, g_{m-1}) \pmod{h}$.
• Proof of Theorem 3.1, Step 5: $\deg f'(g_{0,0}(X), \dots, g_{m-1,\ell-1}(X)) < N'$.

A supporting theorem states that the interpolation formula over a commutative ring (Figure 1) recovers every polynomial of degree $< n$ from its values at $n$ nodes with unit differences.

Significance

Theorem 3.1 says that modular composition is no harder than one multivariate multipoint evaluation with $m\ell$ variables, individual degrees below $d_0$, and $N'$ points, up to quasi-linear univariate work. Combined with the paper's fast multipoint evaluation algorithms this gives modular composition over $\mathbb F_q$ in $n^{1+o(1)}\log^{1+o(1)} q$ bit operations, and from there the paper's improved bounds for polynomial factorization, irreducibility testing, minimal polynomials and modular power projection (Sections 7–8). The converse reduction (Theorem 3.3) shows the two problems are essentially equivalent.

The paper's proof of correctness is a short paragraph; the operation counts are the paper's main concern. This mission makes the correctness exact: the algorithm is defined step for step, and its output is proved equal to the specification. As far as the platform's corpus shows, neither the inverse Kronecker map nor this reduction has a machine-checked statement; the running-time half is not part of this mission.

Difficulty

The obvious argument substitutes $g_i^{d_0^j}$ for $Y_{i,j}$ and invokes the inverse Kronecker identity. Two points keep this from being immediate. First, $\psi_{h,\ell}$ is linear but not multiplicative, and it discards base-$h$ digits beyond position $\ell-1$; the identity holds only for individual degrees at most $h^\ell - 1$, which here requires $d \le d_0^{\lceil \log_{d_0} d\rceil}$. Second, the algorithm never sees $f'(g_{0,0}, \dots)$ itself, only its values at $N'$ points: interpolation recovers it only if its degree is below $N'$, which is why Step 2 reduces modulo $h$ before substituting, and interpolation over a ring (not a field) needs the unit-difference hypothesis throughout. Mathlib's Lagrange interpolation is stated over fields, so the ring version must be handled directly.

Formalization scope

• $R$ is any commutative ring (CommRing R); there is no field or nontriviality assumption.
• Variables are Fin m; the new variables $Y_{i,j}$ are Fin m × Fin ℓ; points are Fin N'.
• Individual degrees are MvPolynomial.degreeOf; "degree at most $N-1$" is natDegree ≤ N - 1.
• $\ell$ is Nat.clog d₀ d and $N' = N m \ell d_0$; $\ell$ is not a free parameter.
• "mod $h$" for $h$ with unit leading coefficient is the remainder on division by the monic associate $h \cdot \mathrm{lc}(h)^{-1}$; interpolation is the Lagrange formula with Ring.inverse of the node differences.
• Step 4 is MvPolynomial.eval, which is exactly the output of Problem 2.1.
• Added hypotheses: $m \ge 1$ and $N \ge 1$ (the paper does not consider $m = 0$, where $N' = 0$, or $N = 0$, where "degree at most $N - 1$" would collapse in natural-number arithmetic).
• In the goal, "$\deg r < \deg h$" is weakened to "$\deg r < \deg h$ or $r = 0$" only to cover the zero ring; in any nontrivial ring the two agree.
• Only correctness is formalized. Operation counts, the $O(\cdot)$ and $\mathrm{poly}\log$ bounds, and the count of invocations are out of scope.

Step 5 is the interpolation formula applied to the $N'$ computed values and nodes alone; it is not defined as the polynomial $f'(g_{0,0}, \dots, g_{m-1,\ell-1})$, and the goal is the six-step output, not the congruence alone, so the statement cannot be closed by unfolding definitions.

Useful infrastructure, reusable beyond this mission: base-$h$ digit manipulation of exponent vectors, Lagrange interpolation over commutative rings with unit node differences, and remainders modulo polynomials with unit leading coefficient. Proofs of any milestone, and of the supporting interpolation theorem, are welcome independently.

Selected references

• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, Dagstuhl Seminar Proceedings 08381, 2008. http://drops.dagstuhl.de/opus/volltexte/2008/1777
• K. S. Kedlaya, C. Umans, Fast polynomial factorization and modular composition, SIAM J. Comput. 40(6):1767–1802, 2011. https://doi.org/10.1137/08073408X
• R. P. Brent, H. T. Kung, Fast algorithms for manipulating formal power series, J. ACM 25(4):581–595, 1978. https://doi.org/10.1145/322092.322099
• J. von zur Gathen, J. Gerhard, Modern Computer Algebra, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9781139856065

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

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).