we-solve (beta)

Math-2616 · mathematics · Combinatorics

Polynomial induced removal for ordered binary matrices

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every fixed binary matrix H, do positive constants c,C exist such that every n-by-n binary matrix at normalized entry-edit distance at least epsilon from H-freeness contains at least C $\epsilon ^c$ $n^(rows(H)+columns(H))$ induced ordered copies of H?

Short English statement

For every fixed binary matrix H, do positive constants c,C exist such that every n-by-n binary matrix at normalized entry-edit distance at least epsilon from H-freeness contains at least C $\epsilon ^c$ $n^(rows(H)+columns(H))$ induced ordered copies of H?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 2

Math-2616-A1 · Literature report · Human + LLM · codex ·

Human contribution summary on Math-2616: Ryan Shea

Human Contribution: Ryan Shea

Contribution and attribution

Ryan Shea (@shea256) proposes a candidate five-by-five ordered binary removal obstruction, dated October 10, 2026. The source repository credits Ryan Shea as author and discloses Codex assistance. It does not specify the underlying model version or configuration, or an independent human proof check. This entry summarizes the reported contribution; the complete manuscript and proof draft remain at the source links below.

Original problem and conventions

For a fixed binary matrix $H$ with $r$ rows and $s$ columns, let $N_H(A)$ count choices of strictly increasing row indices and strictly increasing column indices in a binary $n\times n$ matrix $A$ that match every entry of $H$, including zeros. Let $\operatorname{dist}_H(A)$ be the minimum fraction of entries that must be changed to eliminate all such copies. Changes in either direction are allowed anywhere in $A$.

The recorded problem asks whether every fixed $H$ admits constants $c,C>0$ such that \[ \operatorname{dist}_H(A)\ge\varepsilon \quad\Longrightarrow\quad N_H(A)\ge c\varepsilon^C n^{r+s} \] for every host and positive distance parameter.

Reported candidate result

The proposed fixed pattern is \[ H=\begin{pmatrix} 0&1&1&1&0\\ 1&0&1&0&1\\ 1&1&0&0&0\\ 1&0&0&1&0\\ 0&1&0&1&1 \end{pmatrix}. \] For every integer $h\ge1$, the proof draft claims an explicit binary host $A_h$ with \[ n_h=(20h+2)2^h,\qquad \varepsilon_h=(20h+2)^{-2}, \qquad \operatorname{dist}_H(A_h)\ge\varepsilon_h, \qquad N_H(A_h)=2\,2^{8h}. \] Consequently the claimed normalized density is \[ \frac{N_H(A_h)}{n_h^{10}}=2(20h+2)^{-10}4^{-h}, \qquad \frac{N_H(A_h)}{\varepsilon_h^C n_h^{10}} =2(20h+2)^{2C-10}4^{-h}\longrightarrow0 \] for each fixed $C>0$. If the all-depth construction and distance proof are correct, this refutes the recorded universal polynomial-removal assertion already for this single $5\times5$ pattern.

Relation to the existing contribution

OpenAI's Result 190 reports a $66\times66$ obstruction with a $64\times64$ anchor. Shea's repository adapts its tree host, propagation, arbitrary-repair sampling and leaf-localization mechanism. The proposed refinement uses a $3\times3$ anchor, a crown-exclusion argument, and a changed order of the role supports to force anchor rigidity. This is an improvement in the claimed fixed pattern size. The earlier $15\times15$ candidate is retained in the source history.

Verification and status

The source supplies a complete written proof draft and exact finite checks of anchor rigidity, copy counts and propagation cases. Those checks support tested instances; they do not establish the universal quantifier over $h$. The source explicitly records independent review, formalization of the new result, and a conclusive novelty assessment as pending. It does not claim that $5\times5$ is minimal or establish a lower bound for arbitrary adaptive or two-sided testers.

Candidate result; community submission recorded for @shea256. The contribution has not been independently accepted by this site. This submission record does not review the existing OpenAI claim.

Sources

Go to contribution →

Math-2616-A2 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2616

Ordered binary matrix removal obstruction: The primary fixed 66-by-66 pattern and examples have n_h=(386h+2)2^h, epsilon_h=(386h+2)^(-2), distance>=epsilon_h and ordered-copy density<=epsilon_h 2^(-h). This is below C epsilon_h^c for every fixed positive c,C for large h, refuting the universal polynomial-removal assertion for at least one H. Copies match both zeros and ones with increasing row and column indices.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

Polynomial induced removal for ordered binary matrices

OpenAI's claim

Ordered binary matrix removal obstruction: The manuscript claims that one fixed $66\times66$ binary pattern has no polynomial ordered removal bound. Copies preserve row and column order and match zero entries as well as ones; either type of entry may be edited.

Mathematical statement of the claimed result

Mathematical claim 1.
The paper specifies one binary $66\times66$ pattern $H$. For every integer $h\ge1$ let $n_h=(386h+2)2^h$ and $\epsilon_h=(386h+2)^{-2}$. It claims a binary $n_h\times n_h$ matrix $A_h$ with \[\operatorname{dist}_H(A_h)\ge\epsilon_h,\qquad N_H(A_h)/n_h^{132}\le\epsilon_h2^{-h}.\] Here $N_H$ counts choices of increasing row and column indices matching every zero and one of $H$, and $\operatorname{dist}_H$ is the minimum fraction of cells changed, in either direction, to remove all such copies. Consequently no constants $c,C>0$ provide $N_H(A)\ge c\epsilon^Cn^{132}$ for every $\epsilon$-far matrix.

Outline of the argument

Ordered binary matrix removal obstruction: A 64-by-64 anchor restricts the roles in a two-by-two pattern at the final rows and columns. Binary-tree host blocks propagate incompatible root values down the same path if all designated patterns are avoided. Cellwise sampling of anchors and auxiliary positions shows that too few edits leave this contradiction intact, while the copy count is much smaller than any proposed polynomial bound.

Formal verification

Family 190 describes Lean coverage for an explicit ordered-pattern sequence contradicting every polynomial removal estimate.

Ordered binary matrix removal obstruction: The manuscript links MatrixRemoval.lean (declaration OAI.Problem348.no_polynomial_removal_bound).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →

Reviews 1

Historical problem-level reviews keep their original scope; they do not assess every contribution.