Theoretical Computer Science

Motivation

Scheduling jobs on parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$ is a basic model of service and computing systems. Two features of practice are hard to combine with performance guarantees: jobs are not known in advance but arrive over time, and their processing times are random, with only their distributions known when they arrive. Machines are moreover often unrelated: a job's processing time distribution depends arbitrarily on the machine, and some jobs cannot run on some machines at all.

Gupta, Moseley, Uetz and Xie (arXiv:1703.01634, Math. Oper. Res. 2020) give the first performance guarantee for this combination: a simple greedy policy whose expected cost is within a factor depending only on the variability of the processing times of the best nonanticipatory policy, which knows all jobs in advance.

Timeline. For deterministic jobs arriving over time, Hall, Schulz, Shmoys and Wein (1997) gave an 8-competitive algorithm on unrelated machines. Megow, Uetz and Vredeveld (2006) introduced the stochastic online model and analysed greedy policies on identical machines with modified release dates. Skutella, Sviridenko and Uetz (2016) gave LP-based approximation algorithms for offline stochastic scheduling on unrelated machines, with guarantees linear in the squared coefficient of variation. The present paper (conference version IPCO 2017) treats the online, stochastic, unrelated case with release dates.

Setting

There is a finite set $M$ of machines and jobs $j=1,\dots,n$. Job $j$ is released at an integer time $r_j\ge0$, jobs are indexed so that $r_1\le\dots\le r_n$, and job $j$ has weight $w_j\ge0$. If job $j$ runs on machine $i$ its processing time is a random variable $P_{ij}$ with values in $\{0,1,2,\dots\}$; on forbidden pairs the page writes $\mathbb E[P_{ij}]=\infty$, and every job has an allowed machine. On allowed pairs $\mathbb E[P_{ij}]\ge1$ and the variance is finite. Different jobs are independent; one job's times on different machines need not be. The squared coefficient of variation is $\mathbb{CV}[P_{ij}]^2=\operatorname{Var}[P_{ij}]/\mathbb E[P_{ij}]^2$, and $\Delta$ bounds it on every allowed pair.

A policy decides, for each job, a machine and a start time; jobs are nonpreemptive and a machine runs one job at a time. It is nonanticipatory if its decisions up to time $t$ use only what is known at $t$: the processing time of a job is learned when the job completes. $\mathsf{OPT}$ is the least expected cost $\mathbb E[\sum_jw_jC_j]$ of a nonanticipatory policy that knows all jobs, release dates and distributions in advance.

The greedy algorithm (§6.1) is first defined for deterministic times $p_{ij}$. On machine $i$ job $j$ gets the modified release date $r_{ij}=\max\{r_j,c\,p_{ij}\}$. On arrival, job $j$ is assigned to a machine $m(j)$ minimizing an explicit upper bound $\operatorname{cost}(j\to i)$ on the increase of the objective (Definition 4), and each machine runs WSPT (largest $w_k/p_{ik}$ first) among its jobs whose modified release dates have passed. Run on $p_{ij}=\mathbb E[P_{ij}]$ with $c=\frac23$ it yields the nominal schedule $(m,s)$. The stochastic greedy policy (§6.3) keeps $m$ and the nominal order on each machine, and starts the $\ell$th job on machine $i$ at $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$, never before its nominal start. Its expected cost is $\mathsf{ALG}$, and

$$h(\Delta)=1+\tfrac{\sqrt\Delta}2\ (\Delta\le1),\qquad h(\Delta)=1+\tfrac{\Delta}{\Delta+1}\ (\Delta\ge1).$$

Formalization targets

Goal: Theorem 4

$$\mathsf{ALG}\;\le\;(7.216+3.608\,\Delta)\,h(\Delta)\,\mathsf{OPT}.$$

The goal is stated against every admissible nonanticipatory policy, for every tie-breaking of the greedy algorithm.

Milestones

1. Lemma 6: the deterministic greedy schedule has $\mathsf{ALG}\le\sum_j\operatorname{cost}(j\to m(j))$.
2. Lemma 7, feasibility: with $\alpha_j=\operatorname{cost}(j\to m(j))$, $\beta_{i,t}$ the weight of jobs on machine $i$ released by $t$ and unfinished at $t$, and the speed-scaled values (12), $(\alpha^f/a,\beta^f/b)$ is feasible for the dual $(\mathrm D_r)$ when $af\ge2(2+c)$, $1/c\le f(a-1)$, $af\ge b$.
3. (13): $z^{P_r}\le(1+\frac\Delta2)z^{S_r}\le(1+\frac\Delta2)\mathsf{OPT}$ for the time-indexed relaxations with release dates.
4. Lemma 10: $\mathbb E[(X-\mu)^+]\le\mu\sqrt\Delta/2$ for $\Delta\le1$ and $\le\mu\Delta/(\Delta+1)$ for $\Delta\ge1$.
5. Lemma 8: $\mathbb E[S_j]\le h(\Delta)\,s_j$ for every job.

Significance

The result. Theorem 4 is the first constant-factor guarantee, for fixed $\Delta$, for stochastic online scheduling on unrelated machines with release dates, and it is achieved by a combinatorial policy that needs no LP solution. For deterministic jobs ($\Delta=0$, $h=1$) it gives a deterministic 7.216-competitive algorithm (Theorem 3), improving the ratio 8 of Hall et al.; for exponential processing times ($\Delta=1$) the factor is $(7.216+3.608)\cdot\frac32$. The order $O(\Delta)$ matches earlier offline results on unrelated machines and online results on identical machines.

Formalizing it. The result is proved on paper and has no machine-checked proof. A formalization needs nonanticipatory policies with machine choice, a time-indexed LP relaxation with countably many variables and its weak duality, and a dual-fitting argument. It also exposes a gap: the second sentence of Lemma 7, the bound $z^{D_r}(\alpha^f/a,\beta^f/b)\ge\mathsf{ALG}/(7+\frac{11}{51})$, fails as printed. On one machine with jobs $r=(0,0,0,5)$, $p=(\frac54,\frac54,1,3)$, $w=(2,1,\frac1{1000},\frac1{100})$ the greedy schedule has $\mathsf{ALG}=\frac{6049}{600}$ while $z^{D_r}=\frac{8879}{6400}<\mathsf{ALG}/(7+\frac{11}{51})=\frac{4471}{3200}$. The step $\sum_{i,s}\beta^f_{is}=\mathsf{ALG}/f$ counts a job at $\lfloor C_k/f\rfloor-\lceil r_k/f\rceil+1$ integer slots, up to one more than $C_k/f$. A complete proof of the goal has to close this gap.

Difficulty

Three parts are hard. First, the comparison is with an optimal adaptive policy, so the lower bound has to come from a relaxation that every nonanticipatory policy satisfies in expectation. Writing the time-indexed LP for policies that choose machines at start time, idle deliberately and start at real times, and showing it is a relaxation, requires nonanticipation and job independence to decouple a job's machine from its own processing time. Second, the dual fitting runs through a speed-scaled instance with a non-integer speed $f=\frac{23}6$, so the dual's integer slots and the schedule's real times do not align; this is where the printed objective bound breaks. Third, the obvious stochastic policy, WSEPT list scheduling without forced idleness, fails: Remark 2 of the paper gives an instance where it has $\mathbb E[C]=\Omega(n)$ against $O(1)$. The analysis therefore has to work with deliberately delayed starts.

Formalization scope

Machines are a Fintype, Nonempty type; jobs are Fin n in release order. Processing times are ℕ-valued measurable functions on a probability space, with finite second moment and mean at least one on eligible pairs, and with jobs independent (iIndepFun over jobs of the machine-indexed vectors). Forbidden pairs are an eligibility relation, never a zero or junk mean. Release dates are natural numbers: the relaxation of §6.2 has integer slots $s\ge r_j$, and (13) is false for a fractional release date. Weights are nonnegative; $\Delta$ is any upper bound on the squared coefficients of variation, which is at least as strong as the page's maximum.

$\mathsf{OPT}$ is never written as an infimum. The goal and (13) quantify over every admissible policy: a map from realizations to machines and real start times that is feasible (eligible machine, start at or after release, disjoint half-open processing intervals per machine), nonanticipatory, and has integrable completion times. A non-integrable comparator would have Bochner integral $0$ and would make the bound trivial or false; the integrability requirement rules this out. The greedy algorithm is a predicate on an outcome (assignment and start times): cost-minimal assignment, no start before the modified release date, no unnecessary idleness, and the WSPT priority. Every tie-breaking is covered, and the goal fixes $c=\frac23$. The stochastic policy is the recursion $S_{i,\ell}=\max\{s_{i,\ell},S_{i,\ell-1}+P_{i,\ell-1}\}$ itself. LP feasibility includes summability of every series, and LP optima appear only through "for every feasible point there is a feasible point" statements.

A complete development needs: weak duality for $(\mathrm P_r)$/$(\mathrm D_r)$ with countably many variables; the identity $\mathbb E[C_j]=C^S_j$ for the expected occupation variables of a nonanticipatory policy (reusable for any time-indexed stochastic scheduling relaxation); Lemma 10, a self-contained probability inequality; and the dual fitting. Contributions are welcome on each milestone and on a repaired objective bound for Lemma 7.

Selected references

• V. Gupta, B. Moseley, M. Uetz, Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, Mathematics of Operations Research, 2020; arXiv:1703.01634v4. https://arxiv.org/abs/1703.01634, https://doi.org/10.1287/moor.2019.0999
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• N. Megow, M. Uetz, T. Vredeveld, Models and algorithms for stochastic online scheduling, Mathematics of Operations Research 31(3):513–525, 2006. https://doi.org/10.1287/moor.1060.0201
• M. Skutella, M. Sviridenko, M. Uetz, Unrelated machine scheduling with stochastic processing times, Mathematics of Operations Research 41(3):851–864, 2016. https://doi.org/10.1287/moor.2015.0757

Motivation

Online scheduling asks for decisions before the full job set is known. In the online-list model, jobs are revealed one at a time and each must be assigned to a machine before the next job is revealed; the scheduler may choose the processing order after the list is complete. When processing durations are random and machines are unrelated, the same job may have different duration distributions on different machines. An assignment decision therefore affects both its own completion time and the waiting time of other jobs. Gupta, Moseley, Uetz and Xie study a greedy assignment rule for this setting and prove a bound against a scheduler that knows all distributions and all jobs in advance but cannot see future processing-time realizations (arXiv:1703.01634v4, §§2–5). This comparison is relevant to systems that must commit work to heterogeneous servers as requests arrive, while service times remain uncertain.

Setting

Let $M$ be a nonempty finite set of machines and $J=\{0,\ldots,n-1\}$ a finite set of jobs indexed by their presentation order. Job $j$ has a nonnegative weight $w_j$. An eligibility relation $E\subseteq M\times J$ records which machines can process each job; every job has at least one eligible machine. For an eligible pair $(i,j)$, $P_{ij}$ is a nonnegative integer-valued random processing time with mean $\mu_{ij}=\mathbb E[P_{ij}]\ge1$ and a finite second moment. The vector $(P_{ij})_{i\in M}$ for one job may have dependence across machines, but the vectors for different jobs are independent. A parameter $\Delta\ge0$ bounds $\operatorname{Var}(P_{ij})/\mu_{ij}^{2}$ for all eligible pairs. These conventions follow the standing model and coefficient-of-variation bound in the paper (§2, pp. 4–6 and Definition 3, p. 7).

The greedy assignment sends each newly presented job to an eligible machine that minimizes the instantaneous increase in expected total weighted completion time. For a fixed machine, jobs are sequenced by decreasing ratio $w_j/\mu_{ij}$, with job index breaking equal-ratio ties. This is the weighted shortest expected processing time, or WSEPT, order. The algorithm runs each machine continuously from time zero in that order. Its expected objective, $\mathrm{ALG}$, is the expectation of $\sum_j w_j C_j$ for the resulting realized completion times, not a value assigned by a closed formula (§4, pp. 8–9).

A comparator policy can choose machines and start times as earlier jobs finish. It must schedule nonpreemptively, use only information available when a decision is made, and have integrable completion times. It may know the full job set and every processing-time distribution before time zero, but not the future realizations. Write $C_j^\Pi$ for its realized completion time and $\mathrm{OPT}$ for the least expected weighted completion cost among such policies when an optimum exists (§2.1, pp. 5–6).

Formalization targets

The goal is the paper's Theorem 1 (p. 11). It compares every eligible-minimum greedy assignment, including every tie choice, with every admissible nonanticipatory comparator $\Pi$:

$$\mathrm{ALG}\le(4+2\Delta)\,\mathbb E\!\left[\sum_{j\in J}w_j C_j^\Pi\right].$$

This universal comparison expresses $\mathrm{ALG}\le(4+2\Delta)\mathrm{OPT}$ without requiring an optimizer to exist. The milestone list contains the paper's integer tail identities (Lemma 1), the completion-time expression for one job (Lemma 9), the comparison of two time-indexed relaxations and its policy consequence (Lemma 2 and Corollary 1), and the three dual-variable claims used around the greedy algorithm (Lemmas 3–5). Their printed indices and formulas are attached to the proposal in proof order.

Significance

The result supplies a performance guarantee for a combinatorial online algorithm on heterogeneous machines with random durations. The factor varies explicitly with the processing-time variability: for deterministic eligible processing times, $\Delta=0$ and the bound is $4$; greater permitted variability increases it linearly. Forbidden machine-job pairs are included, so the claim applies when some jobs have a restricted set of possible servers. The comparator may postpone machine selection until processing begins and adapt to completed work, so the bound is not limited to fixed-assignment schedules (Theorem 1 and §2.1).

The theorem is proved in the cited paper. In this proposal, the Lean statements and definitions have compiled, while the theorem modules still contain sorry; the remaining formalization work is to supply machine-checked proofs. A completed development would contribute reusable definitions for nonanticipatory unrelated-machine policies, time-indexed stochastic scheduling relaxations, and comparisons with countably many LP variables. Those interfaces can support later scheduling results that use the same information structure.

Difficulty

The most immediate comparison treats the greedy assignment costs as dual variables. For this paper's linear program, the direct halved dual point is feasible, but the resulting dual objective is zero, so feasibility alone gives no useful upper bound on $\mathrm{ALG}$ (Lemmas 3–4 and the beginning of §5). The random processing times also require care when translating occupancy probabilities into completion costs: the time-indexed expression uses both first and second moments, and a policy's start decision must not depend on the job's unobserved duration. The proof must reconcile the greedy order, those probability identities, and a comparison with policies that may change machines and start times adaptively.

Formalization scope

The Lean model uses Fin n in arrival order and permits $n=0$; the empty instance gives a trivial inequality. The machine type is finite and nonempty. Processing times are natural-valued random variables, while policy start times are real. Processing intervals are half-open, so a zero-duration job occupies no machine time. An ineligible pair is represented by the eligibility relation, never by a zero mean. Each eligible processing time has finite second moment and mean at least one; $\Delta$ is any nonnegative upper bound on squared coefficients of variation. The paper leaves $w_j\ge0$ implicit; it is included because negative weights invalidate the comparison. Dependence across machines for the same job is allowed, and the entire time vector is independent across jobs.

Nonanticipation is stated by comparing two realizations that agree on the durations observed by time $t$ and on the fact that running jobs have not yet completed. Admissible comparator policies must work for every realization and have integrable completion times, preventing a default zero value for a nonintegrable integral. The goal quantifies over all such policies, so it cannot be made true by choosing a restricted benchmark. The greedy predicate reads only earlier assignments and admits every eligible minimizing machine; it does not fix a favorable tie choice.

The LP variables $y_{ijs}$ are real and nonnegative, supported on eligible pairs, and their countable sums and time-weighted sums must converge. LP comparisons use feasible witnesses instead of a real infimum, whose value would be misleading for an empty feasible set. A source-level discretization issue is isolated in Lemma 4: $\sum_s\beta_{is}$ counts whole slots up to a nominal completion time, so the printed second equality requires integer means. Its first equality and the goal do not take that condition. A complete proof needs measurable-policy reasoning, tail-sum identities, summability arguments, WSEPT order properties and dual weak duality. Definitions and lemmas that isolate those components are welcome.

Selected references

• V. Gupta, B. Moseley, M. Uetz and Q. Xie, Greed Works – Online Algorithms For Unrelated Machine Stochastic Scheduling, accepted version of Mathematics of Operations Research, 2020. arXiv:1703.01634v4; DOI:10.1287/moor.2019.0999.

Motivation

A suffix tree of a text $T[1..n]$ answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies $\Theta(n)$ machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text contains. A standard measure of that information is $r$, the number of runs (maximal blocks of one repeated symbol) of the Burrows–Wheeler transform of $T$. On repetitive collections $r$ is orders of magnitude smaller than $n$, and indexes using $O(r)$ words are of direct practical interest in bioinformatics and in versioned document stores.

Gagie, Navarro and Prezza (arXiv:1809.02792v2, 2019) build a compressed suffix tree in $O(r\log(n/r))$ words (their Theorem 9, p. 28). A compressed suffix tree in the style of Abeliuk, Cánovas and Navarro (Algorithms 2013) needs the longest common prefix array $LCP$ in compressed form, and stores it differentially, as $DLCP$. The paper's route to compressing $DLCP$ is one exact combinatorial fact: $DLCP$ has a bidirectional macro scheme of size at most $4r+1$ (p. 28). A cited conversion of macro schemes into run-length grammars (Lemma 18, from Gagie, Navarro and Prezza, LATIN 2018) then gives the $O(r\log(n/r))$ grammar. This mission formalizes that combinatorial fact and the lemmas it rests on.

Setting

A text $T[1..n]$, $n\ge 1$, is a string over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix**$T[i..]$is$T[i]T[i+1]\cdots T[n]$. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$ listing the starting positions of the suffixes in increasing lexicographic order.

The Burrows–Wheeler transform is $BWT[p]=T[SA[p]-1]$ if $SA[p]>1$ and $BWT[p]=T[n]$ if $SA[p]=1$: the symbol preceding the $p$-th smallest suffix, read cyclically. The LF mapping is

$$LF(p)=C[BWT[p]]+\operatorname{rank}[p],$$

where $C[c]$ counts the symbols of $BWT$ smaller than $c$ and $\operatorname{rank}[p]$ counts the occurrences of $BWT[p]$ in $BWT[1..p]$. A position $p$ starts a run if $p=1$ or $BWT[p]\ne BWT[p-1]$; $r$ is the number of run starts, written $p_1<\dots<p_r$.

Let $\operatorname{lcp}(S,S')$ be the length of the longest common prefix of two strings. Then

$$LCP[1]=0,\quad LCP[p]=\operatorname{lcp}(T[SA[p-1]..],T[SA[p]..]),\qquad DLCP[1]=LCP[1],\quad DLCP[i]=LCP[i]-LCP[i-1].$$

The differential suffix array is $DSA[1]=SA[1]$, $DSA[p]=SA[p]-SA[p-1]$.

A bidirectional macro scheme (BMS) of size $b$ on a sequence $S[1..n]$ of any symbol type (Definition 6, p. 28, after Storer and Szymanski) is a partition $S=S_1\cdots S_b$ into consecutive blocks, each either an explicit symbol (a block of length 1) or a pointer to another occurrence $S[j..j']$ of the same content. The source map sends a position at offset $i'$ inside a pointer block to $f(i)=j+i'-1$. The scheme is correct if, from every position $i$, some iterate $f^k(i)$, $k\ge0$, is an explicit symbol.

Formalization targets

Goal: a macro scheme of size at most $4r+1$

$$\exists\ \text{a correct BMS of } DLCP[1..n] \text{ of size } b\le 4r+1.$$

This is the sentence following Lemma 16 on p. 28, proved by Lemma 17. It fixes no constant beyond the paper's own count, and it is the exact input Lemma 18 needs.

Milestones

1. LF is a single cycle (§2.3, p. 8): $LF$ permutes $[1..n]$ and the orbit of position 1 visits every position in fewer than $n$ steps.
2. $LF$ walks the text backwards (§2.4, p. 9): $SA[LF(p)]=SA[p]-1$ whenever $SA[p]>1$.
3. Lemma 12 (p. 20): if $BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
4. Lemma 16 (p. 28): if $BWT[p-2]=BWT[p-1]=BWT[p]$ then $LF(p-1)=LF(p)-1$ and $DLCP[LF(p)]=DLCP[p]$.
5. Lemma 17 (p. 28): the partition of $DLCP$ into the explicit symbols $DLCP[p_i+k]$, $k\in\{0,1,2\}$, and the regions $DLCP[p_i+3..p_{i+1}-1]$ pointing to $DLCP[LF(p_i+3)..LF(p_{i+1}-1)]$, is a BMS.

Significance

The result. The bound $4r+1$ ties the compressibility of the $LCP$ array, a structure of size $n$ that does not obviously inherit the repetitiveness of the BWT, to the number of BWT runs. Through Lemma 18 it yields a run-length grammar of size $O(r\log(n/r))$ for $DLCP$ (Lemma 19, p. 29), and the paper's compressed suffix tree supports its navigation primitives on that grammar. The same pattern, runs of the BWT inducing copies in a differential array, drives the paper's $O(r\log(n/r))$-word access to $SA$ and $ISA$ (§5), of which Lemma 12 is the first step.

Formalizing it. The result is proved in the paper; to our knowledge none of it, nor the basic theory of suffix arrays and the Burrows–Wheeler transform, has a machine-checked proof on this platform. The mission produces a self-contained Lean development of the BWT and LF mapping from their counting definitions, of the $LCP$ and $DLCP$ arrays, and of macro schemes with their correctness condition. The single-cycle property of $LF$ and the identity $SA[LF(p)]=SA[p]-1$ are folklore results that underlie every FM-index; they are formalized here from the counting formula, not assumed.

Difficulty

The obvious proof of the goal counts blocks: at most $3r$ explicit symbols and at most $r+1$ regions. The counting is easy; the content lies in the two properties the count presupposes. First, the copies must be correct: a whole region $DLCP[p_i+3..p_{i+1}-1]$ must coincide with the stretch starting at $LF(p_i+3)$, which needs $LF$ to map a run onto consecutive positions and $LCP$ differences to be preserved, and it needs three consecutive equal BWT symbols, not two, because $DLCP[p]$ involves the suffixes in cells $p-2$, $p-1$ and $p$. Second, the scheme must be correct as a whole: following pointers must never cycle. A scheme in which two regions point at each other satisfies every local condition and still fails. Ruling this out requires the global fact that $LF$ is one cycle through all of $[1..n]$, which in turn rests on the lexicographic order of suffixes and the uniqueness of the terminator \$$. Connecting the counting definition of LF$to the backward step$SA[LF(p)]=SA[p]-1$ is itself a nontrivial argument about ranks of symbols among sorted suffixes.

Formalization scope

Positions are 1-based natural numbers, as in the paper. The text and the suffix array are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$, symbols are natural numbers, and \=1$. The suffix array is a hypothesis (`IsSuffixArray`: a permutation of$[1..n]$sorting the suffixes strictly), never a construction;$BWT$and$LF$are the counting formulas of p. 8, with$T[0]$read as$T[n]$.$LCP$is computed from a recursive$\operatorname{lcp}$on suffix lists;$DLCP$and$DSA$are integer-valued. A macro scheme is defined for any symbol type as a list of blocks laid out consecutively from position 1, each with a length and an optional source start; its size is the list length. Explicit blocks have length 1; a pointer block starting at$i$has a source$j\ne i$inside$[1..n]$, possibly overlapping the block. The value of$f$on explicit symbols, arbitrary on the page, is the identity. The explicit cells$p_i+k$of Lemma 17 are taken only where they exist ($\le n$), and coinciding cells of short runs are counted once; the convention$p_0=-2$only empties the region before$p_1=1$. Lemma 17 is stated as a characterisation of the scheme: explicit blocks exactly at explicit cells, pointer blocks exactly the maximal stretches of the remaining cells, each pointing to$LF$of its first cell with$LF$mapping every cell in the block to the corresponding source cell. The identity$SA[LF(p)]=SA[p]-1$carries the guard$SA[p]>1$, since for$SA[p]=1$ it holds only cyclically.

The paper's $O(\cdot)$ space and time claims (Theorem 9, Lemma 19) and the cited grammar conversion (Lemma 18) are out of scope; the goal is their explicit combinatorial content.

Every sequence has a macro scheme of size $n$ (all symbols explicit), and a set of pointers that only point at each other satisfies every local condition, so a formalization that bounds the size of an arbitrary partition, or that drops the condition that every chain of copies reaches an explicit symbol, would be empty or false; both are excluded by the definition used. $SA$, $BWT$ and $LF$ are not defined through the properties the milestones assert.

Contributions welcome: proofs of the milestones, and reusable lemmas about the LF mapping and lexicographic order of suffixes, which the paper's other missions (locating with sampled phrases, counting distinct substrings) also use.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv preprint, 2019 (v2). https://arxiv.org/abs/1809.02792
• J. A. Storer, T. G. Szymanski, Data compression via textual substitution, Journal of the ACM 29(4):928–951, 1982. https://doi.org/10.1145/322344.322346
• A. Abeliuk, R. Cánovas, G. Navarro, Practical compressed suffix trees, Algorithms 6(2):319–351, 2013. https://doi.org/10.3390/a6020319
• T. Gagie, G. Navarro, N. Prezza, On the approximation ratio of Lempel-Ziv parsing, Proc. LATIN 2018, LNCS 10807, pp. 490–503.
• M. Burrows, D. Wheeler, A block sorting lossless data compression algorithm, Technical Report 124, Digital Equipment Corporation, 1994.
• V. Mäkinen, G. Navarro, Succinct suffix arrays based on run-length encoding, Nordic Journal of Computing 12(1):40–66, 2005.

Motivation

Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length $n$, not with the amount of distinct content. The number $r$ of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in $O(r)$ words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to $n/s$ for a sampling step $s$, which defeats the purpose on repetitive data.

Timeline.

• 1994: Burrows and Wheeler introduce the transform (DEC SRC Research Report 124).
• 2000–2005: Ferragina and Manzini build the FM-index, with backward search and the LF mapping (J. ACM 52(4), 2005).
• 2005: Mäkinen and Navarro give the run-length FM-index, which counts occurrences in $O(r)$ words (Nordic J. Computing 12(1), 2005).
• 2016–2018: Prezza (PhD thesis, Udine, 2016) and Policriti and Prezza (Algorithmica 80(7), 2018) keep one known suffix-array cell, a "toehold", during backward search.
• 2017–2020: Gagie, Navarro and Prezza show that $O(r)$ words suffice to locate every occurrence (arXiv:1705.10382; arXiv:1809.02792; J. ACM 67(1), 2020). This mission formalizes the combinatorial core of that result.

Setting

A text $T[1..n]$ is a sequence over the alphabet $[1..\sigma]$ whose last symbol T[n]=\=1$is the smallest symbol and occurs nowhere else. The **suffix array**$SA[1..n]$is the permutation of$[1..n]$that lists the suffixes$T[SA[p]..n]$in strictly increasing lexicographic order, and the **inverse suffix array** satisfies$SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that $T[0]$ is read as $T[n]$. The LF mapping is the counting formula $LF(p)=C[BWT[p]]+\operatorname{rank}[p]$, where $C[c]$ counts BWT symbols smaller than $c$ and $\operatorname{rank}[p]$ counts copies of $BWT[p]$ in $BWT[1..p]$.

A run is a maximal block of equal consecutive BWT symbols, and $r$ is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most $2r$ positions are sampled. Definition 3 cuts $T$ into phrases that begin exactly at the sampled positions. For a text position $k$, the phrase head $i$ of $T[k]$ is the greatest sampled position $\le k$. The permutation $\phi(i)=SA[ISA[i]-1]$ (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are $DSA[p]=SA[p]-SA[p-1]$ and $DISA[i]=ISA[i]-ISA[i-1]$. A text position starts a phrase of $ISA$ when $ISA[i]$ is the first position of a run.

Formalization targets

Goal: the identity in the proof of Lemma 3

Let $SA[p]=k+1$, let $i$ be the phrase head of $T[k]$, let $q=ISA[i+1]$, and let $N[i]=\langle x,y\rangle=\langle SA[q-1],SA[q+1]\rangle$ be the sample stored at $i$. Then

$$SA[p-1]=x+k-i\quad(p\ge 2),\qquad SA[p+1]=y+k-i\quad(p<n),$$

and $q\ge 2$, $q<n$ respectively, so that $N[i]$ is defined.

Milestones

1. §2.4, p. 9. $SA[LF(p)]=SA[p]-1$ for $SA[p]>1$, with $LF(p)\in[1..n]$.
2. Lemma 12, p. 20. If $BWT[p-1]=BWT[p]$, then $LF(p-1)=LF(p)-1$ and $DSA[LF(p)]=DSA[p]$.
3. Run-free claim, proof of Lemma 3, pp. 12–13. For $0\le t<k-i$, the cells $LF^t(p-1),LF^t(p),LF^t(p+1)$ are contiguous and lie in one BWT run.
4. Lemma 14, p. 23. If $i$ does not start a phrase of $ISA$, then $\phi(i-1)=\phi(i)-1$ and $DISA[i]=DISA[\phi(i)]$.

A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both $c$ and a non-$c$ symbol contains an occurrence of $c$ at the first or last position of a run.

Significance

The goal says that the $O(r)$ numbers $N[i]$, one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval $SA[sp..ep]$ of a pattern, it lets an index list all occurrences in $O(r)$ space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to $s$ neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for $SA$ and $ISA$ in §5.

The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the $r$-index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.

Difficulty

The obvious argument follows the three cells $p-1,p,p+1$ backwards under LF for $k-i$ steps. It rests on two facts that are easy to state and not routine to prove. First, $SA[LF(p)]=SA[p]-1$ must be derived from the counting formula $C[c]+\operatorname{rank}[p]$: this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]$back to$T[i+1]$. This is where the choice of$i$as the *greatest* sampled position$\le k$matters, and also where the case of no sampled position in$[1..k]$needs care. Finally, one more LF step from$T[i+1]$to$T[i]$produces the cell$q$, and the shift by$k-i$ must be tracked through natural-number arithmetic.

Formalization scope

Positions are 1-based natural numbers, as in the paper. $T$ and $SA$ are functions $\mathbb N\to\mathbb N$ read only on $[1..n]$. $SA$ is a hypothesis, IsSuffixArray: it maps $[1..n]$ injectively into $[1..n]$ and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1$is unique and smallest, this order agrees with the paper's. BWT and LF are defined by the formulas of p. 8, never by the properties the milestones assert.$ISA[i]$is$0$if no cell holds$i$. Sampled positions follow the first sentence of Definition 1 (first or last in its run); the paper's "That is" clause omits the last character of the final run.$DSA$and$DISA$ are integer-valued.

Pins and guards:

• Wrap-around phrase. If no sampled position lies in $[1..k]$, the phrase containing $T[k]$ began at T[n]=\$$, which is always sampled. Its head is encoded as 0$($T[0]\equiv T[n]$), so that$q=ISA[1]$is the cell holding$$$. The goal covers this case; it does not assume a sampled position$\le k$.
• Neighbours. Each half of the goal and of the run-free claim is guarded by the existence of the neighbour ($p\ge 2$, $p<n$).
• SA[LF(p)]. The identity is stated for $SA[p]>1$; for $SA[p]=1$ it holds only cyclically.
• Lemma 14. "$[i-1..i]$ within a phrase of $ISA$" means that $i$ does not start a phrase of $ISA$, which begin only at run-first cells. Definition 3's phrases begin at run-first and run-last cells; the two parses are kept apart.

The space and time claims of Lemmas 2–3 and Theorem 1 ($O(r)$ words, $O(\log\log_w(n/r))$ time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding $SA[p]-1$", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions $\le k$.

A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and $\phi$ for the left half of the goal.

Selected references

• T. Gagie, G. Navarro, N. Prezza, Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space, arXiv:1809.02792v2, 2019. https://arxiv.org/abs/1809.02792
• T. Gagie, G. Navarro, N. Prezza, Fully Functional Suffix Trees and Optimal Text Searching in BWT-Runs Bounded Space, J. ACM 67(1), 2020. https://doi.org/10.1145/3375890
• T. Gagie, G. Navarro, N. Prezza, Optimal-Time Text Indexing in BWT-runs Bounded Space, arXiv:1705.10382, 2017 (SODA 2018). https://arxiv.org/abs/1705.10382
• P. Ferragina, G. Manzini, Indexing Compressed Text, J. ACM 52(4):552–581, 2005. https://doi.org/10.1145/1082036.1082039
• A. Policriti, N. Prezza, LZ77 Computation Based on the Run-Length Encoded BWT, Algorithmica 80(7):1986–2011, 2018. https://doi.org/10.1007/s00453-017-0327-z
• V. Mäkinen, G. Navarro, Succinct Suffix Arrays Based on Run-Length Encoding, Nordic Journal of Computing 12(1):40–66, 2005 (no DOI).
• M. Burrows, D. J. Wheeler, A Block Sorting Lossless Data Compression Algorithm, Technical Report 124, Digital Equipment Corporation, 1994 (no DOI).

Motivation

Many matrix algorithms spend most of their time reading their input. A matrix with few nonzero entries should admit routines whose cost scales with that number, rather than with the product of its dimensions. Clarkson and Woodruff study random maps that compress a matrix before a regression or low rank approximation calculation while retaining the geometric information those calculations need. Their sparse embedding has one nonzero entry per input coordinate, so applying it to a sparse matrix can be charged to the matrix's nonzero entries. The probability guarantee for its geometry is Theorem 11 of the preprint, the target of this mission.

The paper proves further results for faster regression and low rank approximation after sketching. Those applications use the subspace guarantee as an input. This mission concentrates on that guarantee and the statements in §3 that support it. The source is the 5 April 2013 arXiv version; theorem and page labels below refer to that version.

Setting

Fix a real matrix $A\in\mathbb R^{n\times d}$ of rank $r$. Its column space is $C(A)=\{Ax:x\in\mathbb R^d\}$. A map $S:\mathbb R^n\to\mathbb R^t$ is a subspace embedding for $A$ when it approximately preserves the length of every vector in $C(A)$ simultaneously. The dimension $r$, rather than the number of rows $n$, controls the size required of the compressed space.

Here $S$ is the sparse embedding matrix $\Phi D$. Each input coordinate $i$ independently chooses one bucket $h(i)\in[t]$ uniformly. The binary matrix $\Phi$ has a $1$ at $(h(i),i)$ and zero elsewhere in column $i$. Independently, $D$ is diagonal with a fair sign $+1$ or $-1$ at each coordinate. Thus the output in bucket $j$ is the signed sum of input coordinates assigned to $j$. The probability in this mission is over the joint, uniform choice of all bucket assignments and signs, with $A$ fixed in advance. This is the construction in §2, p. 7.

For an orthonormal basis matrix $U\in\mathbb R^{n\times r}$ of $C(A)$, the leverage score of row $i$ is $u_i=\sum_{j=1}^r U_{ij}^2$. A threshold $T>0$ separates light coordinates, with $u_i\le T$, from heavy coordinates, with $u_i>T$. The paper describes this split after sorting rows by leverage; the threshold description selects the same coordinates and keeps the input's original order. The bucket event $E_h$ bounds the sum of light leverage scores assigned to each bucket. The heavy event $E_B$ says that distinct heavy coordinates receive distinct buckets. These are properties of $h$ alone; the later concentration statements take probability over the independent signs after fixing a suitable $h$.

Formalization targets

Sparse subspace embedding

There is an absolute constant $C>0$ such that for every $A$ of rank $r\ge1$, every $0<\varepsilon\le1/2$, and every integer $t\ge C(r/\varepsilon)^4\log^2(r/\varepsilon)$,

$$\Pr_{h,D}\!\left[ \forall y\in C(A),\quad \bigl|\|\Phi Dy\|_2^2-\|y\|_2^2\bigr| \le\varepsilon\|y\|_2^2 \right]\ge\frac9{10}.$$

The event contains the universal quantifier over $y$: one draw must work for the whole column space. The squared-norm estimate implies the norm formulation printed in Theorem 11, p. 11 on this range of $\varepsilon$. The paper gives its proof in §3, pp. 7–11.

Supporting targets

The milestone list follows the paper's statements: a coordinate bound from §3.1; the weighted bucket estimate of Lemma 2; light-coordinate concentration in Lemma 3; the collision and exact-preservation statement of Lemma 5; the heavy-light cross-term estimate in Lemma 6; fixed-vector preservation in Lemma 7; and the passage to the whole subspace in Lemma 8. Their distinct probability spaces matter. Lemmas 2 and 5 concern bucket assignments, Lemmas 3, 6, and 7 concern signs for a fixed suitable assignment, and Lemma 8 is a general statement about a random linear map.

Significance

Theorem 11 gives a single compact random matrix that retains the Euclidean geometry of every vector in a specified rank-$r$ column space with probability at least $9/10$. It supports sketch-and-solve algorithms: a computation performed on $\Phi DA$ can use a much smaller row dimension while reasoning about the original column space. The construction also has exactly one nonzero per column, the structural fact behind its input-sparsity running time. The running-time bound is stated in the paper, but this mission's Lean target concerns the mathematical norm guarantee.

The paper already proves the theorem; the open work here is a machine-checked development of its statement and proof. The finite probability model, explicit squared norms, leverage scores, and bucket events can support later formalizations of other sparse sketching results. No machine-checked proof of Theorem 11 is claimed by this proposal. A complete development may reuse proved concentration inequalities from Mathlib or the platform, but the cited inequalities need their hypotheses checked against the finite-sign and weighted-bucket models used here.

Difficulty

A fixed-vector estimate does not itself imply that one random sketch works for all vectors of an uncountable subspace: the quantifier cannot simply be moved through the probability. Collisions also have different effects on high- and low-leverage coordinates. Heavy coordinates need a no-collision event; light coordinates can share buckets only while their total bucket weight remains controlled. The paper's statements keep these events and probability spaces separate. The final whole-subspace claim requires a uniform estimate whose failure probability accounts for the dimension $r$.

Formalization scope

Vectors are functions Fin n → ℝ, matrices are finite real matrices, and $\|v\|_2^2$ and $\|M\|_F^2$ are explicit sums of coordinate squares. The sample space is the product of all bucket maps and all Boolean sign assignments, with counting probability. Every theorem with a freely chosen bucket count assumes $t>0$; otherwise a Fin 0 sample space could make division by its cardinality meaningless. The theorem's size threshold forces this automatically when $r\ge1$ and $0<\varepsilon\le1/2$. Matrix rank is Mathlib's matrix rank.

The formalization fixes $0<\varepsilon\le1/2$ in Theorem 11. The upper bound prevents the logarithmic size expression from degenerating near $r=\varepsilon=1$, and $r\ge1$ keeps its logarithm and division meaningful. Positive $T$ and $W$ are explicit where needed; Lemma 6 restricts $\delta_C\le e^{-1}$. The heavy/light split uses leverage thresholds rather than a row permutation, and constants described as absolute are quantified before every dimension, matrix, error, and failure parameter. In particular, Theorem 11's event quantifies over all $x$ inside the probability, while Lemma 7 fixes $y$ before sampling signs. These choices exclude degenerate distributions, vacuous error ranges, and a fixed-vector claim masquerading as the goal.

The refined $t$ clause at the end of Theorem 11 is left out: its printed $s^2/30$ conflicts with the proof's collision requirement $30s^2$, and its threshold parameter is not fixed in the claim. Lemma 1 and the cited Hanson–Wright moment result, Theorem 4, are proof tools outside this proposal's milestone set. Contributions that formalize those tools faithfully, prove the bucket and sign estimates, or connect the finite model to existing probability libraries are useful for the goal.

Selected references

• Kenneth L. Clarkson and David P. Woodruff, Low Rank Approximation and Regression in Input Sparsity Time, arXiv:1207.6365v4, 2013. Preprint.

Why excluded minors matter here

Many graph classes are defined by excluding a fixed graph as a minor. A minor can be formed by deleting vertices, deleting edges, and contracting edges. Planar graphs, for example, exclude $K_5$ as a minor. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant proved that every class excluding a fixed clique minor has bounded twin-width, a graph parameter that controls how much adjacency information is lost while vertices are successively combined. Their result connects a classical graph-minor restriction with the contraction parameter used in their first-order model-checking framework. The explicit bound is very large, but it establishes that the width depends only on the excluded clique size, rather than on the graph's number of vertices. Bonnet et al., Twin-width I, Theorem 6.3.

Graphs, contractions, and matrix orders

Let $G$ be a finite simple graph. A partition of its vertices is a collection of nonempty, disjoint parts covering all vertices. Two distinct parts are homogeneous if every vertex pair across them is adjacent, or every such pair is nonadjacent. Otherwise the pair of parts is marked red. A $d$-partition has at most $d$ red neighbours at every part. A contraction sequence begins with singleton parts, merges two parts at each step, and finishes with at most one part. The statement $\operatorname{tww}(G)\le d$ says that such a sequence exists with every intermediate partition a $d$-partition. This partition formulation is equivalent to the paper's original description in terms of trigraph contractions. Bonnet et al., pp. 3:11–3:12, 3:32.

Write $K_t$ for the complete graph on $t$ vertices. The graph $G$ is $K_t$-minor free when $K_t$ cannot be obtained from $G$ by the minor operations above. The Lean statement uses a branch-set formulation: a minor model consists of disjoint, nonempty, connected vertex sets, with a connecting edge for each edge of the minor. Bonnet et al., p. 3:9.

An ordering $\sigma$ of the vertices gives a Boolean adjacency matrix $A_\sigma(G)$, with entry $1$ at an edge and $0$ otherwise. A division cuts its rows and columns into nonempty consecutive intervals. A zone is mixed if it is neither constant down its columns nor constant across its rows. A $k$-mixed minor is a division with $k$ row intervals and $k$ column intervals in which every zone is mixed; a $k$-grid minor requires a $1$ in every zone. A matrix is $k$-mixed free or $k$-grid free if the corresponding minor does not exist. A mixed Boolean zone always contains a $1$, so grid freeness implies mixed freeness. Bonnet et al., pp. 3:18–3:19.

The order used in the proof is a depth-first search (DFS). A discovery order $v_1,\dots,v_n$ lists the vertices; at each time the active vertex is the lastly discovered vertex that still has an undiscovered neighbour, and the next vertex is a neighbour of the active vertex, which becomes its parent in the DFS tree $\mathcal T$. The Lex-DFS breaks ties: among the connected components of the undiscovered vertices that meet the active vertex's neighbourhood, it enters one whose word (the $0/1$ vector recording which discovered vertices have a neighbour in the component) is lexicographically largest. The proof also uses minimal subtrees of $\mathcal T$: the union of the tree paths between the vertices of a set. Bonnet et al., pp. 3:26–3:27.

Formalization targets

The main target is the explicit excluded-clique-minor bound. With

$$c_k=\frac83(k+1)^2 2^{4k},\qquad g(t)=2(2^{4t+1}+2)^2,\qquad f(t)=4c_{g(t)}2^{4c_{g(t)}+2},$$

the goal says

$$K_t\not\preceq G\quad\Longrightarrow\quad \operatorname{tww}(G)\le f(t).$$

The $+2$ in $g(t)$ follows the value defined and used in the proof of Theorem 6.3 on p. 3:26; the printed theorem statement has $+1$. The formal target uses the proof-supported bound and records the printed statement verbatim in its provenance. It does not assert the paper's asymptotic triple-exponential notation as a separate theorem. Bonnet et al., pp. 3:26–3:29.

The milestones follow the proof in order:

1. twin-width is the maximum over connected components;
2. a Lex-DFS exists from any vertex of a connected graph;
3. Lemma 6.4: in any DFS, the vertices $a_{i,j}$ of the proof lie on one branch of $\mathcal T$;
4. Lemma 6.5: the enhancements $B^*_j$ avoid the paths $A'_i$, except the last ones;
5. $|V(H)|\le\alpha(H)\omega(H)$ for intersection graphs of subtrees of a tree;
6. the Helly property for subtrees of a tree;
7. Lemma 6.6: each component of $\mathcal T[v]-\{v\}$ meets at most two enhancements of the clique;
8. for a connected $K_t$-minor-free graph, the adjacency matrix in any Lex-DFS order is $g(t)$-grid free;
9. grid free implies mixed free for $0/1$ matrices;
10. the graph form of Theorem 5.8 with the explicit constant applied on p. 3:29.

The Helly theorem is a reference to an existing open platform statement rather than a duplicate draft. Bonnet et al., pp. 3:22–3:29.

What the bound supplies

The theorem supplies a uniform contraction-width bound for every fixed excluded clique minor. In particular, the paper applies it to planar graphs through exclusion of $K_5$. Its numerical value is far from small; the article remarks that the planar specialization has billions of digits. Without the result, excluding a clique minor alone would not yield the particular twin-width certificate required for those applications. Bonnet et al., p. 3:29.

The mathematical result is proved in the cited paper. This mission asks for machine-checked statements and, eventually, proofs of its graph and matrix claims. The reusable output includes a precise partition model of graph twin-width, interval-division models of mixed and grid minors, and a graph statement that converts a mixed-free adjacency order into a contraction-width bound. No machine-checked proof of these new target items is claimed here.

The main obstruction

A dense pattern of nonzero matrix zones does not directly give a graph minor. A matrix zone merely contains an edge somewhere between two vertex blocks. Those blocks need not induce connected subgraphs, and contracting them as if they were connected would use operations unavailable to graph minors. The proof also needs a vertex order with strong enough structure to control how the relevant connected sets overlap. These are the points that separate the grid-free milestone from a direct application of the matrix grid theorem. Bonnet et al., pp. 3:26–3:29.

The conversion from a mixed-free adjacency matrix to graph twin-width has a second issue: matrix twin-width permits separate row and column contractions, while a graph contraction merges one vertex partition and must keep the two matrix axes synchronized. Theorem 5.8 addresses the graph case. The milestone uses the explicit constant that the paper applies at the end of Theorem 6.3, while the printed Theorem 5.8 states an asymptotic bound. Bonnet et al., pp. 3:22–3:23, 3:29.

Formalization scope

Graphs are finite simple graphs, and twin-width and the number of division parts are natural numbers. The real constants $c_k$ and $f(t)$ are compared with natural-number twin-width through $\lfloor f(t)\rfloor$; the explicit value is positive. Vertex orders are equivalences with $\operatorname{Fin}(n)$. Matrix divisions use strictly increasing cut points, so every part is a nonempty consecutive interval. The adjacency matrix has a zero diagonal because simple graphs have no loops. The graph-minor predicate and the subtree representation come from existing published definitions with the same conventions; graph twin-width and the matrix objects are local draft definitions shared across this mission. Bonnet et al., pp. 3:9, 3:12, 3:17–3:19.

The grid-free milestone holds for every Lex-DFS order, as in the paper, and the existence of such an order is a separate milestone. Lemmas 6.4–6.6 are stated in the proof's context: a DFS, and vertices $a_{i,j}$, $b_{i,j}$ and blocks $B_j$ with exactly the order and adjacency properties the page uses. Lemma 6.5 is posed for every block except the last. As printed it also covers the last block $B_{g(t)/2}$, and for that block it can fail. A five-vertex example satisfies every hypothesis of the lemma and violates the printed conclusion; it is checked in Lean in the sanity file, and the formal item records the change. The theorem's bound is uniform over all finite graphs on the excluded-minor hypothesis. A twin-width definition using an unrestricted real infimum, a sequence that skips directly to one part, red degree counted over homogeneous pairs, or a grid minor over arbitrary noninterval partitions would change the claim. Components and empty graphs use the endpoint conventions stated above. The $k\ge1$ hypothesis in the graph conversion milestone rules out the degenerate zero-division case.

Contributions toward the core grid-free order claim, the symmetric contraction bridge, the component theorem, and the reusable minor and division lemmas are within scope. The running-time claims elsewhere in the paper and the pointer construction and the two $K_{t,t}$-minor constructions inside the proof of Theorem 6.3 are not separate milestones: they are unnumbered and their statements need the pointers. They remain part of the grid-free milestone.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, and R. Watrigant, Twin-width I: Tractable FO Model Checking, Journal of the ACM 69(1), Article 3, 2021. DOI:10.1145/3486655.
• A. Marcus and G. Tardos, Excluded permutation matrices and the Stanley–Wilf conjecture, Journal of Combinatorial Theory, Series A 107(1), 153–160, 2004. DOI:10.1016/j.jcta.2004.04.002.
• F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, Journal of Combinatorial Theory, Series B 16(1), 47–56, 1974. DOI:10.1016/0095-8956(74)90094-X.

Motivation

Twin-width is a graph and matrix invariant introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021). Classes of bounded twin-width include bounded tree-width and clique-width graphs, proper minor-closed classes, posets of bounded width, and permutations avoiding a fixed pattern; on all of them, first-order model checking is fixed-parameter tractable once a contraction sequence is given. The difficulty in applying this framework is to bound twin-width for a concrete class, because a contraction sequence is an intricate object.

Section 5 of the paper supplies the tool that makes such bounds routine: the Grid Minor Theorem for twin-width (Theorem 5.4). It reduces bounding twin-width to finding an order of the rows and columns of a matrix (for a graph, an order of its vertices) in which no large mixed minor appears. The paper then uses it for pattern-avoiding permutations, posets of bounded width and $K_t$-minor free graphs (Section 6, Table 1). The argument is modelled on the proof of the Stanley–Wilf conjecture by Marcus and Tardos (JCTA 107, 2004) and on its use by Guillemot and Marx for permutation pattern matching (SODA 2014).

Timeline. Füredi and Hajnal (1992) conjectured a linear bound on the number of $1$s in a $0,1$-matrix avoiding a permutation pattern. Marcus and Tardos (2004) proved it, with constant $c_t=2t^4\binom{t^2}{t}$, via $t$-grid minors. Fox (arXiv:1310.8378) improved the constant to $3t\,2^{8t}$, and Cibulka and Kynčl (arXiv:1607.07491) to $\tfrac83(t+1)^22^{4t}$. Guillemot and Marx (2014) built from the grid structure a decomposition of permutations; Bonnet et al. (2020 preprint, 2021 journal) generalized it to arbitrary matrices over a finite alphabet, which is Theorem 5.4.

Setting

Let $M=(m_{i,j})$ be an $n\times m$ matrix with entries in a finite alphabet $A$ of size $\alpha$. For sets $R$ of rows and $C$ of columns, the zone $R\cap C$ is the submatrix on those rows and columns; it is constant if all its entries are equal.

A partition of $M$ is a pair $(\mathcal R,\mathcal C)$ of a partition of the rows and a partition of the columns. Its error value is the largest number, over all parts $R_i$ (respectively $C_j$), of parts of the other side forming a non-constant zone with it. A contraction sequence is a sequence of partitions starting from the finest one (all singletons), ending at the coarsest one (one row part, one column part), each obtained from the previous by merging two row parts or two column parts. $M$ has twin-width at most $t$, $\operatorname{tww}(M)\le t$, if some contraction sequence has error value at most $t$ throughout.

A division is a partition whose parts consist of consecutive indices. $M$ is $t$-twin-ordered if it has a contraction sequence of error value at most $t$ consisting of divisions.

A zone is vertical if its rows are all equal, horizontal if its columns are all equal, and mixed otherwise. A $t$-mixed minor is a division into $t$ row intervals and $t$ column intervals all of whose $t^2$ zones are mixed; $M$ is $t$-mixed free if it has none. For $0,1$-matrices, a $t$-grid minor is such a division in which every zone contains a $1$. Finally $c_t=\tfrac83(t+1)^22^{4t}$.

Formalization targets

Goal: Theorem 5.4

For $n,m\ge1$:

$$M\ \text{$t$-twin-ordered}\ \Longrightarrow\ M\ \text{$(2t+2)$-mixed free},

$$$$

t\ge1,\ M\ \text{$t$-mixed free}\ \Longrightarrow\ \operatorname{tww}(M)\le 4c_t,\alpha^{4c_t+2}.$$

The constant is the one the paper's proof produces; the paper's summary $2^{2^{O(t)}}$ is not formalized.

Milestones, in the order of the proof

1. Lemma 5.5: a matrix is mixed iff it contains a corner, a mixed $2\times2$ submatrix on consecutive rows and columns.
2. Lemma 5.6: fusing two consecutive row parts does not increase the mixed value of a column interval (mixed zones plus mixed cuts).
3. Lemma 5.2: a sequence of partitions, each $r$-refining the next, with error value at most $t$, certifies $\operatorname{tww}(M)\le rt$.
4. Theorem 5.3 (Marcus–Tardos, constant of Cibulka–Kynčl): $c_t\max(n,m)$ entries $1$ force a $t$-grid minor.
5. Lemma 5.7: a $t$-mixed free matrix has a division sequence of mixed value at most $2c_t$.
6. The first item of Theorem 5.4.
7. The row-type count on p. 3:22: within a row part, rows restricted to the non-mixed zones take at most $\alpha^{t'+1}$ values.

Significance

Theorem 5.4 characterizes bounded twin-width of matrices, up to the order of rows and columns, by the exclusion of a mixed minor. Its second item is used in Section 6 of the same paper to show that $K_t$-minor free graphs, posets of bounded width and pattern-avoiding permutations have bounded twin-width, and in later papers of the twin-width series as the standard route to twin-width upper bounds. Without it, each such bound needs its own explicit contraction sequence.

The result is proved in the paper; no machine-checked proof of it exists in Mathlib or on the platform. The mission produces a machine-checked statement and, once solved, a proof of the grid theorem with its explicit constant, a formal treatment of contraction sequences of matrices, and a statement of the Marcus–Tardos theorem with the Cibulka–Kynčl constant, which is itself absent from Mathlib.

Difficulty

The first item is comparatively short. The second item is where the work lies. The natural first idea — contract greedily as long as the error value stays below a bound depending on $t$ — does not work: the error value is not monotone under fusions, and nothing in the absence of a mixed minor directly prevents a greedy sequence from getting stuck with large error. Any proof has to identify a quantity that is monotone under fusion and is bounded by a density argument, and then turn a sequence controlled by that quantity into a contraction sequence of bounded error value; the paper's choices (mixed value, Lemmas 5.6 and 5.7) are the milestones. The density argument rests on the Marcus–Tardos theorem with an explicit single-exponential constant, a substantial combinatorial result in its own right and not available in Mathlib.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) A with [Fintype A], and $\alpha$ is Fintype.card A. Partitions are Mathlib Finpartitions of univ; the finest is ⊥, and "coarsest" means at most one part. Twin-width is the partition form of p. 3:18, as a predicate MatTwinWidthLE M t with exactly one merge, of rows or of columns, per step; it is never an infimum over a possibly empty set. Divisions in minors are given by strictly increasing cut points $0=r_0<\dots<r_t=n$, so all parts are non-empty. Vertical and horizontal mean "all rows (columns) of the zone agree". Grid minors use Bool entries. Since $c_t$ is not an integer, $\alpha^{4c_t+2}$ is a real power, and the bound is $\lfloor 4c_t\alpha^{4c_t+2}\rfloor$; the mixed-value bound of Lemma 5.7 is $\lfloor 2c_t\rfloor$.

Hypotheses added relative to the page: $n,m\ge1$ in Theorems 5.3, 5.4 and Lemma 5.7; $t\ge1$ in the second item of Theorem 5.4, in Theorem 5.3 and in Lemma 5.7, since for $t=0$ every non-empty matrix is vacuously $0$-mixed free and the bound would be false; $m\ge1$ in the row-type count. Theorem 5.3 is stated with the explicit constant $c_t$ that the paper quotes and uses, not as a bare existence statement.

The statements are not trivializable by the usual routes: twin-width is not a junk infimum, a contraction sequence cannot jump to one part in a single step, the error value counts non-constant zones per part on both sides, minors range over divisions with non-empty interval parts rather than arbitrary partitions, and all bounds depend only on $t$ and $\alpha$, never on $M$.

A complete development needs: finite partitions and their merges, divisions as interval partitions, the Marcus–Tardos theorem, and bookkeeping for sequences of partitions. The partition machinery and Theorem 5.3 are reusable beyond this mission (graph twin-width in the other missions of this series, pattern avoidance). Proofs of individual milestones, and of the Marcus–Tardos theorem from its original argument, are welcome.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655
• A. Marcus, G. Tardos, Excluded permutation matrices and the Stanley–Wilf conjecture, J. Combin. Theory Ser. A 107(1), 153–160, 2004. https://doi.org/10.1016/j.jcta.2004.04.002
• J. Fox, Stanley–Wilf limits are typically exponential, arXiv:1310.8378, 2013. https://arxiv.org/abs/1310.8378
• J. Cibulka, J. Kynčl, Füredi–Hajnal limits are typically subexponential, arXiv:1607.07491, 2016. https://arxiv.org/abs/1607.07491
• S. Guillemot, D. Marx, Finding small patterns in permutations in linear time, SODA 2014, 82–101. https://doi.org/10.1137/1.9781611973402.7