A tiny grid resists every polynomial repair bound
- What it is
- A paper claims one tiny 4-by-4 binary pattern defeats every polynomial bound in a particular matrix-removal problem.
- Who did it
- Zinan Wang.
- What it could mean
- If the construction and its formalization hold, they would expose a sharp limit on how efficiently one can force certain ordered matrix patterns to disappear by editing entries.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A Four-by-Four Obstruction to Polynomial Removal for Ordered Binary Matrices ↗See the proposed checks
First map the stated 4×4 pattern, host construction, induced-copy count, and arbitrary-edit lower bound from the manuscript; then separately inspect the supplied Lean statement and its correspondence to the claimed ordered-removal conclusion in an isolated environment.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
A small ordered pattern spreads through larger grids
The highlighted four-by-four grid introduces the paper's fixed binary pattern; the branching grids conceptually represent its explicit larger hosts. This does not show a counted construction, an edit-distance calculation, or a proof.
Read the source · Abstract · fixed 4×4 pattern and depth-h host construction ↗- Source kind
- Mathematical research record
- Evidence reported
- Manuscript; independent examination not started
- Source date
- ; added 2026-10-14
- What it claims
- The paper claims a fixed 4×4 binary pattern whose induced ordered removal bound is not polynomial. Its construction has order (14h+2)2^h, exact editing distance 2^(2h), and an induced-copy density that decays exponentially in h; the author reports a Lean formalization and verification sources as ancillary files.
- Why this could matter
- A tiny grid resists every polynomial repair bound Removal questions ask whether a pattern that appears rarely can be eliminated with a proportionally small edit. This paper claims a four-by-four exception: even a very sparse appearance can still demand far more repair than any polynomial rule allows.
- If it holds up
- It would give combinatorics a smaller, explicit obstruction and a precise target for studying the limits of ordered removal theorems.
- If it does not
- A failed count, edit lower bound, or formal correspondence would locate which step cannot support the claimed obstruction.
- Impact horizon
- Foundational · Combinatorics · Extremal matrix theory · Formalized mathematics
- Version
- arXiv v1; 2026-10-11.
- Why we tracked it
- source-reviewed mathematical intake, not a validated counterexample, peer review, or homepage feature.
- Highest-risk dependency
- Analyst judgment: exact induced-versus-non-induced definitions, the quantifier in the removal bound, the host construction, and the source-to-Lean correspondence are load-bearing. The reported formalization does not by itself establish that its endpoint matches every informal claim.
- Available artifacts
- arXiv v1 lists Lean formalization and verification sources as ancillary files. No local artifact, Lean project, manuscript script, or ancillary file was executed in this intake.
- Current boundary
- Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: First map the stated 4×4 pattern, host construction, induced-copy count, and arbitrary-edit lower bound from the manuscript; then separately inspect the supplied Lean statement and its correspondence to the claimed ordered-removal conclusion in an isolated environment.