A Four-by-Four Obstruction to Polynomial Removal for Ordered Binary Matrices

Zinan Wang

cs.DM Oct 11, 2026 · v1 math.CO

Read PDF arXiv abstract

TL;DR

The main obstruction, exact copy count, edit-distance lower bound, classification and transversal identity are formalized in Lean 4 with Mathlib, supplied as ancillary files.

Abstract

We exhibit a fixed $4\times 4$ binary matrix with no polynomial induced ordered removal bound. At depth $h\geq 1$, let $m=2^h$. Our explicit host has order $(14h+2)m$, exactly $2m^6+\frac{1}{2}(m-2)m^5$ induced copies, and exact editing distance $m^2$ cells. Its normalized editing distance is $Θ(h^{-2})$, while its induced-copy density is $Θ(4^{-h}h^{-8})$. The lower bound holds against arbitrary cell edits through an injective family of $m^2$ protected selections. An exhaustive arithmetic classification identifies every induced copy and proves that a matching canonical repair creates none. The original-copy transversal number is exactly $m$, yielding an unbounded gap between hitting existing copies and eliminating all copies. The identities and the obstruction at every depth are formalized in Lean, with verification sources included as ancillary files.

Problem

Whether a fixed small binary pattern matrix can fail to admit a polynomial induced ordered removal bound. The earlier known obstruction used a 66x66 pattern.

Approach

An explicit host matrix A_h of order (14h+2)2^h is built from binary trees of row and column blocks, marker modes and dummy blocks, with block-constant entries. An injective family of m^2 protected selections gives a lower bound on edit distance against arbitrary cell edits. An exhaustive arithmetic classification shows every induced copy of the 4x4 pattern H_4 falls into one of two terminal families, and a canonical repair is shown to be copy-free. All identities and the obstruction at every depth are machine-checked in Lean 4.24.0 with a pinned Mathlib revision.

Results

The exact edit distance is m^2 and the exact copy count is 2m^6+(m-2)m^5/2, so normalized distance is Θ(h^{-2}) while copy density is Θ(4^{-h}h^{-8}), ruling out a polynomial removal bound for H_4. The original-copy transversal number is exactly m, giving an unbounded gap between hitting existing copies and eliminating all copies.

h	m	n_h	family I	family II	N_{H_4}(A_h)
1	2	32	128	0	128
2	4	120	8192	1024	9216
3	8	352	524288	98304	622592
4	16	928	33554432	7340032	40894464

Small-depth consistency table of exact copy counts

Papers With

A Four-by-Four Obstruction to Polynomial Removal for Ordered Binary Matrices