Combinatorics

Motivation

In stochastic matching a platform knows, for every potential pair, the probability that the pair would succeed, but learns whether it does only by trying it, and a successful trial is binding. Kidney exchange, online dating and labour markets are the standard examples: a crossmatch test, a date or an interview is a probe whose outcome is random, and a positive outcome commits both sides. Each participant also tolerates only a limited number of attempts, its patience. The algorithmic question, studied since Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009), is how much of the optimal adaptive strategy's expected weight a simple, non-adaptive rule can secure.

The modern approach solves a linear programming relaxation and rounds its fractional solution online, through a contention resolution scheme: edges are examined one at a time, and an edge is used only when it does not conflict with earlier decisions. Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012) introduced the relaxation (LP (3) below) and showed that it bounds every adaptive probing algorithm. Baveja, Chavan, Nikiforov, Srinivasan and Xu (Algorithmica 2018) analysed processing edges in a uniformly random order. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892) add attenuation: an independent coin that sometimes skips an edge on purpose, so that edges likely to block others are probed less often. This mission formalizes their guarantee when patience is unlimited.

Setting

Let $G=(V,E)$ be a finite graph. Each edge $e$ is active independently with known probability $p_e\in[0,1]$, and each vertex $v$ has a patience $t_v\in\mathbb N\cup\{\infty\}$, the maximal number of edges at $v$ that may be probed. Write $\delta(v)$ for the edges incident to $v$. A vector $(y_e)_{e\in E}$ is feasible for LP (3) when

$$0\le y_e\le 1,\qquad \sum_{e\in\delta(v)}y_ep_e\le 1,\qquad \sum_{e\in\delta(v)}y_e\le t_v\qquad(e\in E,\ v\in V);$$

$y_e$ is read as the probability of probing $e$, and $z_e=y_ep_e$ as the probability that $e$ is matched.

An attenuation function is a map $\tilde a:[0,1]\to[0,1]$, and the attenuation of an edge is $a(e)=\tilde a(p_ey_e)$. The paper's examples (Definition 4) are $\tilde a_{\exp}(z)=e^{-\alpha z}$, $\tilde a_{\rm lin}(z)=1-\alpha z$, and $\tilde a(z)=\frac{1-z}{1-e^{-(1-z)}}(1-1/e)$. A function is effective (Definition 3) when $\tilde a(0)=1$ and $z\mapsto\ln(1-xz\tilde a(z))$ is convex on $[0,1]$ for every $x\in(0,1)$.

Algorithm 1 draws independent coins $Y_e\sim\mathrm{Bernoulli}(y_e)$ and $A_e\sim\mathrm{Bernoulli}(a(e))$ and processes the edges in a uniformly random order. When it reaches $e$, it probes $e$ if $e$ is free (both endpoints unmatched and with remaining patience), $Y_e=1$ and $A_e=1$. A probe uses one unit of patience at both endpoints and reveals the activeness $P_e\sim\mathrm{Bernoulli}(p_e)$; if $P_e=1$, both endpoints are matched. The edge $e=\{u,v\}$ is safe when, before $e$ is processed, each endpoint $r$ has received at most $t_r-1$ probes and no earlier edge $f\neq e$ at $u$ or $v$ has $A_fP_fY_f=1$.

Formalization targets

Goal: Corollary 5 (p. 16)

If every patience is $\infty$, $(y_e)$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\rm lin}$ with $\alpha=1/2$, then for every edge $e$

$$\Pr[\text{Algorithm 1 probes }e]\ \ge\ \Bigl(\int_0^1e^{-2x}\,dx\Bigr)y_e=\tfrac12\bigl(1-e^{-2}\bigr)y_e\approx0.432\,y_e .$$

Milestones

1. The exponential and linear functions with $\alpha=1/2$ are effective (p. 9).
2. Equation (4) (p. 9): the expected matched weight is $\sum_ew_ep_e\Pr[e\text{ free}]\Pr[Y_e=1\cap A_e=1]=\sum_ew_ep_ey_ea(e)\Pr[e\text{ free}]$.
3. Equation (7) (p. 10): $a(e)\Pr[e\text{ is free}]\ge\tilde a(p_ey_e)\Pr[e\text{ is safe}]$.
4. Lemma 3 (p. 11): $\prod_{f\in E_1(r)}(1-xa(f)y_f)\ge e^{-x\sum_{f\in E_1(r)}y_f}$ for effective $\tilde a$, where $E_1(r)$ is the set of edges $f\neq e$ at $r$ with $p_f=1$.
5. §3.3 (p. 16): $z\mapsto\tilde a(z)\int_0^1e^{-2x(1-z)}dx$ is minimized on $[0,1]$ at $z=0$.

Companion: Corollary 6 (p. 16)

On a star graph with infinite patience and the third attenuation function, $\Pr[e\text{ is probed}]\ge(1-1/e)\,y_e$. It comes with the identity of p. 16 behind it: for the third function, $\tilde a(z)\int_0^1e^{-x(1-z)}dx=1-1/e$ for all $z\in[0,1]$. Both are plain items of the mission, not milestones.

Significance

By (4), Corollary 5 bounds the expected weight of Algorithm 1 by $\frac12(1-e^{-2})\sum_ew_ep_ey_e$, and with an optimal $y$ and the bound of Bansal et al. this is a $0.432$-approximation for stochastic matching without patience constraints. Because the bound holds edge by edge and for every feasible $y$, it also gives a random-order contention resolution scheme for the matching polytope, which is the form reused for other objectives and in online settings. Corollary 6 is the rank-one analogue with the constant $1-1/e$.

None of this is formalized. Stochastic probing, patience, random-order processing and attenuation have no counterpart in Mathlib or on the platform. The mission produces a finite, executable model of a probing algorithm run on random coins and a random order, in which these probabilities are exact finite sums; that model is reusable for the other results of the paper and for related rounding schemes. The paper's results are proved in §3.2 (pp. 9–15) and §3.3 (p. 16); the milestones are the steps used there.

Difficulty

The obvious argument treats the edges at the two endpoints of $e$ as independent obstacles, each blocking $e$ with probability proportional to its LP value. That fails because being free is not a product event: whether an earlier edge $f$ blocks $e$ depends on whether $f$ was itself free, which depends on the whole run before $f$. A second difficulty is uniformity. The bound must hold for every feasible $y$, and the LP mass at an endpoint can be split among arbitrarily many edges of arbitrary sizes; the quantities involved are not monotone in how that mass is split, and the bound must survive the worst split, including the limit of many tiny edges. The choice of attenuation matters here: the third function of Definition 4 violates the convexity condition of Definition 3, which is why Corollary 6 is not covered by the paper's argument. Finally, the paper reasons with continuous arrival times, while the model has only permutations and finitely many coins.

Formalization scope

• Model. The graph is the platform's EdmondsMatching65.Polyhedron.Graph (finite, loopless, parallel edges allowed). Probabilities $p$, LP values $y$, weights $w$ and attenuations are real; patience is in ℕ∞, with $\top=\infty$. Every probability is a finite average over the $|E|!$ orders of $E$ and over all outcomes of the coins $Y$, $A$, $P$, with product weights. The paper's independent uniform arrival times induce exactly this uniform order. The run of Algorithm 1 is computed step by step, with matched vertices and probe counters; free, probed and safe are events of that run.
• Standing assumptions. $0\le p_e\le1$ for every edge (the meaning of "probability of being active"); LP (3) feasibility, which contains $0\le y_e\le1$; attenuations with values in $[0,1]$ on $[0,1]$.
• Disclosed choices. Corollary 5 is stated for $\tilde a_{\exp}$ and $\tilde a_{\rm lin}$ with $\alpha=1/2$: the corollary says "the effective attenuation functions from Definition 4", its proof names these two, and the third function fails Definition 3 ($g''(0)<0$ for $x$ near 1). The effectiveness milestone is stated for these two only. The third function is given its limit $1-1/e$ at $z=1$, where the printed formula is $0/0$. Corollary 6 is a companion item, not a milestone: the paper's argument for it passes through Lemma 3, which does not apply to the third function, so it is supported by numerical checks but its printed proof has a gap.
• Not stated. The approximation-ratio and "balanced contention resolution scheme" sentences of Corollaries 5 and 6 need a model of all adaptive probing algorithms (Lemma 1 of the paper, from Bansal et al.) and are out of scope; the goals are the displayed probability bounds.
• Ruled out. Defining $\Pr[e\text{ is free}]$ or $\Pr[e\text{ is probed}]$ by the product formula of p. 11 instead of from the run, or stating the goal for "some" attenuation function, would make the goal a different and easier theorem; neither is done.
• Welcome contributions. Proofs of the milestones; a general lemma that an event depending only on the edges before $e$ is independent of $e$'s coins; a conditioning-on-arrival-time lemma for uniform permutations; a proof (or a counterexample) for Corollary 6.

Selected references

• B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
• N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP Is the Cure for Your Matching Woes: Improved Bounds for Stochastic Matchings, Algorithmica 63(4):733–762, 2012. https://link.springer.com/journal/453/volumes-and-issues/63-4
• A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved Bounds in Stochastic Matching and Optimization, Algorithmica 80(11):3225–3252, 2018. https://link.springer.com/journal/453/volumes-and-issues/80-11
• N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating Matches Made in Heaven, ICALP 2009, LNCS 5555. https://doi.org/10.1007/978-3-642-02927-1

Motivation

The joint replenishment problem is a basic model of coordinated inventory control. A firm stocks $n$ commodities, each of which follows its own Economic Order Quantity (EOQ) model, but every order also incurs a joint ordering cost $K_0$, regardless of which commodities it contains. Ordering commodities together therefore saves money, and the question is how to synchronize their replenishment cycles.

Since the mid-1980s the best known guarantee for the continuous-time problem came from power-of-2 policies (Roundy 1985, 1986; Jackson, Maxwell and Muckstadt 1985; Muckstadt and Roundy 1987). Their cost is within $\sqrt{9/8}\approx1.06$ of optimal for a fixed base period, and within $1/(\sqrt2\ln2)\approx1.02$ when the base is optimized. On the hardness side, Schulz and Telha (2022) and Tuisov and Yedidsion (2020) showed the problem to be intractable; the latter proved it strongly NP-hard, which rules out a fully polynomial-time approximation scheme.

Segev (arXiv:2302.09941, published in Management Science, 2025) gave the first improvement over power-of-2 policies. For every $\epsilon\in(0,\tfrac12)$ the problem can be approximated within $1+\epsilon$ of optimal in time $O(2^{\tilde O(1/\epsilon^3)}\cdot n^{O(1)})$. This mission formalizes the approximation guarantee behind that theorem. The source is the arXiv v1 preprint, and all theorem numbers refer to it.

Setting

Commodity $i\in[n]$ has ordering cost $K_i>0$ and holding cost $H_i>0$. Ordering it every $T_i>0$ time units costs per unit time

$$C_i(T_i)=\frac{K_i}{T_i}+H_iT_i .$$

A policy is a vector $T=(T_1,\dots,T_n)$ of positive intervals. For $t>0$ and $\Delta\ge0$, let $\mathcal M_{t,\Delta}=\{0,t,2t,\dots,\lfloor\Delta/t\rfloor t\}$ be the multiples of $t$ in $[0,\Delta]$. A policy places

$$N(T,\Delta)=\Big|\bigcup_{i\in[n]}\mathcal M_{T_i,\Delta}\Big|$$

joint orders in $[0,\Delta]$. Its joint ordering cost and total cost are

$$J(T)=K_0\cdot\lim_{\Delta\to\infty}\frac{N(T,\Delta)}{\Delta},\qquad F(T)=J(T)+\sum_{i\in[n]}C_i(T_i).$$

For $\mathcal N\subseteq[n]$, $M_{\mathcal N}$ is the least common multiple of $\{T_i\}_{i\in\mathcal N}$, and $M_{\mathcal N}=\infty$ when the intervals have no common multiple.

The algorithm works against a reference policy $T^*$ with $T^*_{\min}=\min_iT^*_i$ and an estimate $F(T^*)\le\widetilde{\mathrm{OPT}}\le2F(T^*)$.

• Easy regime. When $T^*_{\min}\ge\frac n\epsilon\cdot\frac{K_0}{\widetilde{\mathrm{OPT}}}$, it uses the easy policy $\hat T_i=\sqrt{(K_0+K_i)/H_i}$.
• Difficult regime. Otherwise it guesses $\tilde T_{\min}$ with $(1-\epsilon/2)T^*_{\min}\le\tilde T_{\min}\le T^*_{\min}$ (2). It cuts $[\tilde T_{\min},\tilde T_{\min}/\epsilon]$ into segments $S_\ell=[(1+\epsilon)^{\ell-1}\tilde T_{\min},(1+\epsilon)^\ell\tilde T_{\min})$, $\ell=1,\dots,L$. It keeps the active segments $\mathcal A^*$, those containing some $T^*_i$, and picks one representative $R^*_\ell$ among the $T^*_i$ in each.

Two representatives are $\Psi$-aligned when $aR^*_{\ell_1}=bR^*_{\ell_2}$ for positive integers $a,b\le\Psi=2L^2 2^L/\epsilon$. The alignment graph $G^*_\Psi$ joins $\Psi$-aligned active segments. The linear system (LP) asks for $R_\ell\in\bar S_\ell$ satisfying the same alignment relations as $R^*$. A solution is misaligned across components when representatives in different components of $G^*_\Psi$ are not $\Psi$-aligned. The final policy gives commodity $i$ the $C_i$-cheapest of the $R_\ell$ and of the single large interval $\lceil\max\{\tilde T_{\min}/\epsilon,\sqrt{K_i/H_i}\}\rceil^{(R_1)}$, rounded up to a multiple of $R_1$.

Formalization targets

Goal: the approximation half of Theorem 1.3

Fix $n\ge1$, $K_0,K_i,H_i>0$, $\epsilon\in(0,\tfrac12)$, a policy $T^*$ with all $T^*_i>0$, and $\widetilde{\mathrm{OPT}}$ with $F(T^*)\le\widetilde{\mathrm{OPT}}\le2F(T^*)$.

• (a) In the easy regime,

$$F(\hat T)\le(1+2\epsilon)F(T^*).$$

• (b) In the difficult regime, the grid of powers of $1+\epsilon/2$ contains a guess satisfying (2). For every such guess and every choice of representatives, a feasible, cross-misaligned solution of (LP) exists, and every final policy $\hat T$ built from such a solution satisfies

$$F(\hat T)\le(1+5\epsilon)\,F(T^*).$$

Milestones

The goal's proof uses the following results, in this order:

• Claim 1.1 (EOQ facts) and Lemma 1.2 (the density exists and equals $\sum_{\mathcal N}(-1)^{|\mathcal N|+1}/M_{\mathcal N}$).
• Lemma 2.1 (the easy regime) and Observations 2.2 and 2.3.
• Lemma 2.4, Lemma 2.5 and Corollary 2.6 (the structure of (LP)).
• Lemmas 3.2 and 3.3 and Claims 3.4 and 3.5 (crossing and uncrossing terms).
• Lemma 3.1 and inequality (3) (density), and Lemma 3.6 (assignability).

Significance

The theorem gives the first approximation scheme for continuous-time joint replenishment. It settles the problem's approximability up to the form of the exponential dependence on $\epsilon$, after nearly four decades in which power-of-2 policies were the best available. Its central device, synchronizing pairs of representatives through bounded integer multiples and controlling everything else by inclusion–exclusion over the alignment graph, is proposed in the paper as a template for other multi-item lot-sizing models.

The result is proved on paper, and no machine-checked version is known. A formalization adds three things.

• Lemma 1.2. A verified proof that the joint ordering cost of every positive policy is well defined. The paper notes that this is not obvious from (1).
• Bookkeeping. A check of the paper's constants and signs across a long inclusion–exclusion argument.
• Generality. Making explicit that the guarantee holds against any positive reference policy, not only an optimal one, whose existence the paper never establishes.

Difficulty

The obvious argument runs as follows: round every $T^*_i$ to a nearby point of a small grid and charge joint orders to the grid. It fails because the cost of the joint orders depends on the least common multiples of the intervals, not on their sizes. Two nearby reals can have a small lcm, or none at all, and an arbitrarily small perturbation changes $N(T,\Delta)$ by a constant factor. The proof must therefore keep the arithmetic relations among the representatives exactly where they matter: within components of $G^*_\Psi$, through (LP). It must also show that relations across components contribute only lower-order terms. This requires two nested inclusion–exclusion expansions (Lemma 3.3 and Claim 3.5) whose error terms, of order $|\mathcal A^*|^2 2^{|\mathcal A^*|}$, are absorbed by the choice of $\Psi$.

Lemma 1.2 is a squeeze argument, but it rests on showing that the common multiples of finitely many positive reals form the set $M\cdot\mathbb N$.

Formalization scope

All declarations live in the namespace ContJRP.Align.

Representation.

• The model is defined on Mathlib with no external dependency.
• Commodities are Fin n with $n\ge1$.
• $N(\cdot,\Delta)$ counts a finite union of Finset ℝ, and $0$ is a member of every $\mathcal M_{t,\Delta}$.
• The density is a limUnder.
• $1/M_{\mathcal N}$ is 0 when no common multiple exists.
• Segments are indexed from $0$ in Lean, so the paper's $S_\ell$ and $R_1$ are Lean's index $\ell-1$ and R 0.

Committed conventions.

• $K_0,K_i,H_i>0$ and $\epsilon\in(0,\tfrac12)$ everywhere.
• $L$ is the least natural number with $(1+\epsilon)^L>1/\epsilon$, which the page leaves as $O(\frac1\epsilon\log\frac1\epsilon)$.
• Every alignment multiple and the $\beta^\pm$ of Lemma 2.4 are positive integers.
• Inclusion–exclusion sums range over nonempty index sets.
• The reference policy $T^*$ is any positive policy whose cost the estimate brackets; it need not be optimal.
• Lemmas in §2–§3 do not assume the difficult-regime inequality, which their proofs do not use.

What is left out. The running-time half of Theorem 1.3, the time bounds of Lemmas 2.4 and 2.5, and the final selection of the cheapest candidate (§3.3) are not formalized. The goal carries the constants the analysis proves, $1+2\epsilon$ and $1+5\epsilon$, rather than the rescaled $1+\epsilon$.

Trivializing formalizations ruled out.

• (LP) cannot be empty, because the goal asserts that a feasible, cross-misaligned solution exists.
• limUnder cannot return a junk value, because Lemma 1.2 and (3) are stated as Tendsto limits.
• The final policy is not a free parameter: each $\hat T_i$ must be one of its options and $C_i$-minimal among them.
• Misalignment quantifies over positive multiples only, so it is satisfiable.

Infrastructure and contributions. A complete development needs three pieces:

• the lattice of common multiples of positive reals, and the floor-count $|\bigcap_{i}\mathcal M_{T_i,\Delta}|=\lfloor\Delta/M\rfloor+1$;
• inclusion–exclusion for finite unions (Finset.inclusion_exclusion_card_biUnion in Mathlib);
• elementary calculus for the EOQ cost.

The density results (Lemma 1.2) are reusable for any periodic-scheduling model. Proofs of any milestone are welcome, as are alternative statements of the selection step.

Selected references

• D. Segev, The Continuous-Time Joint Replenishment Problem: ϵ-Optimal Policies via Pairwise Alignment, arXiv:2302.09941v1, 2023; Management Science, 2025. https://arxiv.org/abs/2302.09941
• R. Roundy, 98%-effective integer-ratio lot-sizing for one-warehouse multi-retailer systems, Management Science 31(11), 1985. https://doi.org/10.1287/mnsc.31.11.1416
• P. Jackson, W. Maxwell, J. Muckstadt, The joint replenishment problem with a powers-of-two restriction, IIE Transactions 17(1), 1985. https://doi.org/10.1080/07408178508975270
• C.-P. Teo, D. Bertsimas, Multistage lot sizing problems via randomized rounding, Operations Research 49(4), 2001. https://doi.org/10.1287/opre.49.4.599.11225
• A. S. Schulz, C. Telha, Integer factorization: Why two-item joint replenishment is hard, Operations Research, 2022 (forthcoming at the time of the preprint).
• A. Tuisov, L. Yedidsion, The continuous joint replenishment problem is strongly NP-hard, arXiv:2006.05310, 2020. https://arxiv.org/abs/2006.05310

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

Online bipartite matching with stochastic arrivals models the assignment of display-advertising impressions to advertisers: requests arrive one at a time, each must be assigned irrevocably on arrival or dropped, and the arrival sequence is random rather than adversarial. Since Feldman, Mehta, Mirrokni and Muthukrishnan beat the $1 - 1/e$ barrier in the i.i.d. arrival model (FOCS 2009), a line of work has designed algorithms with better guarantees. Jaillet and Lu (Math. Oper. Res. 2014) introduce a whole class of such algorithms, the Random Lists Algorithms, and obtain ratios $0.729$, $0.725$ and $0.706$ for integral arrival rates, vertex weights and general arrival rates.

Two notions of performance coexist in this literature. One compares expectations, $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}]$; the other asks that $\mathrm{ALG}/\mathrm{OPT}$ be large on most realizations, as in Feldman et al. Section 2 of Jaillet and Lu shows that, for every algorithm of their class, the two notions are quantitatively linked by an explicit exponential tail bound. This mission formalizes that section.

Setting

A bipartite graph $G = \{A \cup I, E\}$ has a finite set $A$ of advertisers, a set $I$ of impression types, and edges $E \subseteq A \times I$; $(a, i) \in E$ means advertiser $a$ is interested in type $i$. A fixed number $n$ of requests arrive at periods $1, \dots, n$, and their types are drawn i.i.d. from a known distribution on $I$. Every advertiser can receive at most one request.

A list for type $i$ is an ordered sequence of advertisers interested in $i$. A Random Lists Algorithm fixes, for each type $i$, a distribution $\mathcal D_i$ over lists (constructed from an LP solution; the construction is irrelevant here). When a request of type $i$ arrives it draws a list from $\mathcal D_i$ and assigns the request to the first advertiser on the list not yet matched, or drops it if every listed advertiser is matched.

Formally, each request carries an outcome $x$ in a finite set $\mathcal X$ determining its type $\mathrm{typ}(x)$ and its list $\mathrm{lst}(x)$; outcomes $\omega_1, \dots, \omega_n$ are i.i.d. with law $\nu$. Starting from $W_0 = \emptyset$, the set $W_j$ of matched advertisers after the $j$-th request is obtained from $W_{j-1}$ by adding the first advertiser of $\mathrm{lst}(\omega_j)$ outside $W_{j-1}$, if any. Then:

• $\mathrm{ALG}(\omega) = |W_n|$, the number of assigned requests;
• $\mathrm{OPT}(\omega)$ is the cardinality of a maximum matching of the realized graph, in which request $j$ may go to $a$ iff $(a, \mathrm{typ}(\omega_j)) \in E$;
• $\mathbb E[\mathrm{ALG}]$, $\mathbb E[\mathrm{OPT}]$ are expectations under $\nu^{\otimes n}$, and $c = \mathbb E[\mathrm{OPT}]/n$.

Formalization targets

Goal: the concluding display of Section 2 (p. 6)

If every list contains only interested advertisers, then for every $n \ge 1$ and every $\epsilon > 0$,

$$\mathbb P\left(\frac{\mathrm{ALG}}{\mathrm{OPT}} \ge \frac{\mathbb E[\mathrm{ALG}]}{\mathbb E[\mathrm{OPT}]} - \frac{2\epsilon}{c + \epsilon}\right) \ge 1 - 2\exp(-2n\epsilon^2).$$

It holds for every instance and every law $\nu$, with no assumption on the size of $\mathbb E[\mathrm{OPT}]$.

Milestones

1. Claim 1 (p. 5). If two list sequences differ in one position, the cardinalities of the resulting matchings differ by at most one.
2. Lemma 1 (p. 5). $\mathbb P(\mathrm{ALG} - \mathbb E[\mathrm{ALG}] < -n\epsilon) \le \exp(-2n\epsilon^2)$.
3. Lemma 2 (p. 5). $\mathbb P(\mathrm{OPT} - \mathbb E[\mathrm{OPT}] > n\epsilon) \le \exp(-2n\epsilon^2)$.

A supporting theorem, not a milestone, records the fact the display uses without stating it: with interested lists, $\mathrm{ALG} \le \mathrm{OPT}$ on every realization.

Significance

The display shows that the paper's guarantees, proved for the ratio of expectations, transfer to realizations: when $\mathbb E[\mathrm{OPT}] = \Theta(n)$, $\mathrm{ALG}/\mathrm{OPT}$ is at least $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}] - O(\epsilon)$ except with probability $2e^{-2n\epsilon^2}$. It applies uniformly to the whole class of Random Lists Algorithms, whatever the LP and the list distributions, so it covers each of the paper's later algorithms at once.

The result is proved in the paper; nothing about it is open. It has no machine-checked proof. Formalizing it produces a precise model of list-based online matching (the greedy run, the realization-graph optimum, the joint type–list law) that later formalizations of the paper's competitive ratios can build on, and a worked application of the bounded-differences method to a combinatorial online algorithm.

Difficulty

The concluding display is elementary once Lemmas 1 and 2 are available. The two lemmas need McDiarmid's bounded-differences inequality in one-sided form, which Mathlib does not provide, and the bounded-difference properties of ALG and OPT.

Claim 1 is the step where the naive argument fails. Changing one list can change the assignment of every later request, so ALG is not a sum of local contributions, and a single changed list could a priori cascade into many changed assignments; the claim asserts that the cascade never changes the total by more than one. The analogous property for OPT (changing one request's type moves the maximum matching by at most one) is used in Lemma 2's proof but is not stated in the paper.

Formalization scope

• Arrivals. Outcomes live in a finite type $\mathcal X$ with the discrete σ-algebra, and the law of the arrivals is the product measure $\nu^{\otimes n}$ (Measure.pi). Any joint law of type and list is allowed; every Random Lists Algorithm is the case $\mathcal X = \{(i, l)\}$, $\nu(i, l) = p_i\,\mathcal D_i(l)$. Types and lists are not modelled as independent sequences, which would break $\mathrm{ALG} \le \mathrm{OPT}$.
• Expectations are Bochner integrals of functions on the finite space $\mathcal X^n$, hence honest finite sums.
• Matchings. OPT is the maximum size of a partial assignment Fin n → Option A that uses only edges and gives each advertiser at most one request; the empty assignment qualifies, so the maximum is over a nonempty set. ALG is $|W_n|$ for the greedy recursion.
• Pinned hypotheses. The goal assumes $n \ge 1$ (the paper's $c = \mathbb E[\mathrm{OPT}]/n$) and that every list only contains interested advertisers (stated in §2, p. 5). Claim 1 and Lemma 1 hold for arbitrary lists and carry neither hypothesis. Lists need not be nonempty or repetition-free.
• Division by zero. No hypothesis $\mathbb E[\mathrm{OPT}] > 0$ or $\mathrm{OPT} > 0$ is made. On realizations with $\mathrm{OPT} = 0$, and when $\mathbb E[\mathrm{OPT}] = 0$, Lean's $x/0 = 0$ applies; the statement remains true under it, and adding a positivity hypothesis would weaken the result.
• Not posed. Theorems 1–3 (the competitive ratios, which hold up to $1 + O(1/n)$) and the LP constructions of the algorithms are out of scope. McDiarmid's inequality is a proof tool, not an item. A one-sided version is posed elsewhere on the platform and not yet proved.

Contributions welcome: a one-sided McDiarmid inequality for Measure.pi (reusable well beyond this mission), the bounded-difference property of maximum bipartite matchings, and Claim 1.

Selected references

• P. Jaillet and X. Lu, Online Stochastic Matching: New Algorithms with Better Bounds, Mathematics of Operations Research 39(3), 2014; accepted manuscript, rev. June 2013. https://doi.org/10.1287/moor.2013.0621
• J. Feldman, A. Mehta, V. Mirrokni and S. Muthukrishnan, Online Stochastic Matching: Beating 1 − 1/e, FOCS 2009. https://arxiv.org/abs/0905.4100
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 1989. https://doi.org/10.1017/CBO9781107359949.008

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.