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

Abstract

We exhibit a fixed $4\times 4$ binary matrix with no polynomial induced ordered removal bound. At depth $h\ge 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 $\Theta (h^{-2})$, while its induced-copy density is $\Theta (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.

Lean formalization and verification sources included as ancillary files