# Polynomial removal fails for ordered binary matrices

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Polynomial removal fails for ordered binary matrices](../../preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026/paper.pdf)

## Scope

The formalized result disproves a polynomial removal bound for one explicit $66\times66$ binary pattern. For every $c,C>0$, there is an $n\times n$ binary matrix at normalized edit distance at least $\varepsilon>0$ from being pattern-free but with fewer than $c\varepsilon^C n^{132}$ induced ordered copies. Row and column indices are independently increasing, and every zero and one entry must match. The construction gives an explicit sequence of such matrices, allowing edits in both directions.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Failure of polynomial removal for ordered binary matrices | [MatrixRemoval.lean](../ComparatorChallenges/MatrixRemoval.lean) |