结果族 190：Polynomial removal fails for ordered binary matrices · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
玩”找茬”：一张巨大的 0-1 表格里藏着许多与你手里模板一模一样的图案，问要改多少格才能毁掉所有图案？直觉说：如果非改很多格不可（离”干净”很远），图案一定多得随手可抓。本文造出一张固定的 @@M@@66\times66@@ 模板，让这个直觉在”行列有顺序的 0-1 矩阵”世界里彻底失灵——所谓有序，就是拷贝里行与行的先后、列与列的先后都不能乱。
关键词卡片
@@M@@\ge c\,\epsilon^C n^{2k}@@ 型下界；本文否定其存在。看个具体例子
定理数字版：存在宿主矩阵 @@M@@A_h@@，改动比例至少 @@M@@\epsilon_h=(386h+2)^{-2}@@ 才能变成”不含 @@M@@H@@“，但有序拷贝数不超过 @@M@@\epsilon_h\,2^{-h}\,n^{132}@@——随 @@M@@h@@ 增大，任何 @@M@@c\,\epsilon^C n^{132}@@ 型多项式下界都被击穿。
为什么值得关心
它否定了 2007 年起被反复陈述的多项式有序矩阵删除猜想，还连带表明固定精度的采样测试器需要超多项式的采样量。值得注意的是，定性版本依然成立：每个固定距离都有正的拷贝下界，爆炸的只是数量级——”定性成立、定量爆炸”的罕见标本。玄机在于：毁掉现有拷贝只需 @@M@@2^h@@ 个格子，但这么一改会立刻造出新拷贝，任何彻底修复仍须改动至少 @@M@@4^h@@ 个格子。
已 Lean 形式化
第一级台阶
导读把问题比作”找茬”游戏：一张巨大的黑白表格里藏着多少与模板处处相同的图案？要翻转多少格才能毁掉所有图案？去掉比喻但仍不用符号：对象是一个固定的小图案与一张巨大的 0-1 表格；操作有两种——数”处处相同”的图案个数、翻转格子把图案赶尽杀绝；”有序”意味着图案里行与行、列与列的先后不容打乱，黑白两色都要逐格对上。
第二级台阶
用本科组合语言精确化：设 H 为固定的 k×k 0-1 矩阵，A 中的一个有序拷贝是严格递增的行标与列标选择，使子矩阵与 H 逐格相等——0 与 1 都须匹配。A 不含拷贝则称 H-free；归一化距离 dist_H(A) 是变成 H-free 所须改动的格子比例，双向改动均被允许。删除引理式的问题：离 H-free 很远时，拷贝数 N_H(A) 至少有多少？
第三级台阶
定理构造了固定的 66×66 矩阵 H，并对每个 h≥1 给出 n_h=(386h+2)·2^h 阶宿主 A_h：它离 H-free 至少 ε_h=(386h+2)^{-2}，拷贝密度却不超过 ε_h·2^{-h}。随 h 增大，任何形如 N_H ≥ c·ε^C·n^{2k} 的多项式下界都被击穿。注意结论只否定定量形式：定性删除引理（固定距离必有正拷贝下界）依然成立；被推翻的是 Alon–Ben-Eliezer 问题 1.4 与 Gishboliner–Shapira 综述猜想 4.5 的多项式版本。
第一级台阶
导读把问题比作”找茬”游戏：一张巨大的黑白表格里藏着多少与模板处处相同的图案？要翻转多少格才能毁掉所有图案？去掉比喻但仍不用符号：对象是一个固定的小图案与一张巨大的 0-1 表格；操作有两种——数”处处相同”的图案个数、翻转格子把图案赶尽杀绝；”有序”意味着图案里行与行、列与列的先后不容打乱，黑白两色都要逐格对上。
第二级台阶
用本科组合语言精确化：设 H 为固定的 k×k 0-1 矩阵，A 中的一个有序拷贝是严格递增的行标与列标选择，使子矩阵与 H 逐格相等——0 与 1 都须匹配。A 不含拷贝则称 H-free；归一化距离 dist_H(A) 是变成 H-free 所须改动的格子比例，双向改动均被允许。删除引理式的问题：离 H-free 很远时，拷贝数 N_H(A) 至少有多少？
第三级台阶
定理构造了固定的 66×66 矩阵 H，并对每个 h≥1 给出 n_h=(386h+2)·2^h 阶宿主 A_h：它离 H-free 至少 ε_h=(386h+2)^{-2}，拷贝密度却不超过 ε_h·2^{-h}。随 h 增大，任何形如 N_H ≥ c·ε^C·n^{2k} 的多项式下界都被击穿。注意结论只否定定量形式：定性删除引理（固定距离必有正拷贝下界）依然成立；被推翻的是 Alon–Ben-Eliezer 问题 1.4 与 Gishboliner–Shapira 综述猜想 4.5 的多项式版本。
本文构造了一个固定的 @@M@@66\times66@@ 0-1 矩阵 @@M@@H@@，并给出一列宿主矩阵：它们离不含 @@M@@H@@ 很远，但所含 @@M@@H@@ 的有序拷贝（ordered copy）密度低于任何多项式界，从而否定了有序二值矩阵的多项式删除引理猜想。
图删除引理（removal lemma）断言：若图离 @@M@@H@@-free 至少 @@M@@\epsilon@@ 远，则必含约 @@M@@\delta n^{v(H)}@@ 个 @@M@@H@@；定量版本追问 @@M@@\delta@@ 能否取成 @@M@@\epsilon@@ 的幂（如 @@M@@\delta\ge c\,\epsilon^C@@）。把问题搬到带行序与列序的 0-1 矩阵上——拷贝须保持行、列各自的顺序，且 0 与 1 都要匹配——就得到多项式有序矩阵删除猜想：Alon–Fischer–Newman（2007）率先发问，Alon–Ben-Eliezer（2020 年问题 1.4）与 Gishboliner–Shapira 综述（猜想 4.5）明确陈述。定性版本已由 Alon–Ben-Eliezer–Fischer 证得：每个固定距离都有正的拷贝下界，但定量依赖未知。此前的非多项式下界例子都依赖宿主中的第三个符号，纯二值情形悬而未决。本文用单个 66 阶模式将其否定。
论文显式给出 @@M@@66\times66@@ 模式 @@M@@H@@：左上 @@M@@64\times64@@ 块是”锚”（anchor）@@M@@S@@——除右下角嵌入全部 32 个五比特字的块外均为 @@M@@S(u,v)=\mathbf 1[u\ne v]@@；最末两行两列构成”本体”（body）@@M@@P=\begin{pmatrix}1&0\\1&1\end{pmatrix}@@。主定理：对每个 @@M@@h\ge1@@，取 @@M@@n_h=(386h+2)2^h@@、@@M@@\epsilon_h=(386h+2)^{-2}@@，存在 @@M@@n_h\times n_h@@ 二值矩阵 @@M@@A_h@@，同时满足 @@M@@\operatorname{dist}_H(A_h)\ge\epsilon_h@@（改成 @@M@@H@@-free 至少须改动 @@M@@\epsilon_h n_h^2@@ 个格子，且 0、1 两个方向都可改）与拷贝数不等式 @@M@@N_H(A_h)/n_h^{132}\le\epsilon_h2^{-h}@@。于是对任何常数 @@M@@c,C>0@@，沿此序列 @@M@@N_H(A_h)/(\epsilon_h^C n_h^{132})\to0@@，形如 @@M@@N_H\ge c\,\epsilon^C n^{2k}@@ 的多项式界无从成立。附带推论：仅当采样子矩阵含 @@M@@H@@ 才拒绝的典型行–列采样测试器（tester），要保持固定拒绝概率需 @@M@@q\ge\exp(\Omega(\epsilon_h^{-1/2}))@@ 个采样，为超多项式。
宿主 @@M@@A_h@@ 的行列由深度 @@M@@h@@ 的二叉树索引：每个内部结点在每根轴上挂一个”加”块与一个”减”块，叶层两块合一；再前置 @@M@@6h@@ 组模式锚块与一个哑块（dummy），共 @@M@@n=(386h+2)2^h@@ 个位置。证明分两半。
先证距离下界，即改动少于 @@M@@m^2=4^h@@ 格必有拷贝。在每根轴上均匀选取一条根到叶路径及各锚块、哑块的代表；凡涉及锚、哑或根层的”受保护”格子，其行、列被同时选中的概率恰为 @@M@@1/m^2@@，对改动集 @@M@@E@@ 作并界，@@M@@|E|<m^2@@ 时必存在一次完全避开 @@M@@E@@ 的选取。再假定改后的 @@M@@B@@ 是 @@M@@H@@-free，则每个模式下本体 @@M@@P@@ 被禁。而未动的根格子给出 @@M@@B(x_0^+,y_0^+)=1@@ 与 @@M@@B(x_0^-,y_0^-)=0@@；@@M@@V@@ 模式借哑列提供全 1 列，把值沿相邻行层下传，@@M@@W@@ 模式再借哑行传入相邻列层。归纳到叶层时加、减两号共享同一格子，它须同时等于 1 与 0，矛盾。归一化即得 @@M@@\operatorname{dist}_H\ge d_h^{-2}=\epsilon_h@@。
再证拷贝上界：原矩阵里拷贝极少。关键是”锚刚性”——@@M@@S@@ 右下角含全部 32 个五比特字，而变元行的 1 在每个类中呈后缀（suffix）分布，五个变元列上至多实现 27 个字，故任一拷贝在某根轴上必有超过 32 个锚位；结合 @@M@@S@@ 前 32 行的高密度与不同模式锚块间的全 0 条目，逼出整个拷贝落在单一模式的锚组内，本体行列也落入该模式指定集合。最后逐一核查四种模式：序关系（子块夹在父块两块之间）与赋值规则 @@M@@\mathbf 1[p\le q]@@、@@M@@\mathbf 1[p<q]@@ 处处与 @@M@@P@@ 冲突，唯独叶层减号模式 @@M@@p=q@@ 幸存——拷贝的 @@M@@(65,65)@@ 格必落在仅含 @@M@@m@@ 格的叶对角 @@M@@\mathcal L_h@@ 上，故 @@M@@N_H\le m\,n^{130}@@，密度 @@M@@\le 2^{-h}/d_h^2@@。两半合并即得定理。
论文评注还点出玄机：全部原拷贝只须 @@M@@2^h@@ 格即可命中，但把这些格子改成 0 会立刻造出新拷贝，任何修复仍须改动至少 @@M@@4^h@@ 格——”命中集”（hitting set）与”修复”（repair）的鸿沟，正解释了既有正结果为何帮不上忙。
本篇是结果族 190 的唯一手稿，主结果按任务元数据已配 Lean 形式化证明，正文距离与计数两半各自独立又互相咬合。它否定的是多项式版本猜想，定性删除引理不受影响，反而说明其定量依赖必不可多项式化。按 OpenAI 官方声明，未经形式化的结果可能存在问题；本文主结果既已形式化，读者仍可对照原文核查显式构造。
问 1：证明里最关键的一步是什么？
答：距离下界的逐格采样论证。对任意改动后的矩阵，沿每根轴采样一条树路径加锚位、哑位；凡需保持原值的”受保护”格子，其行、列被同时选中的概率恰为 m^{-2}（m=2^h），对实际改动集作并界，少于 m² 处改动必留下一次完全避开的选取。引言特别强调：逐格论证避免了随类数增长的损失，才拿到 ε_h=(386h+2)^{-2} 这个逆平方距离。
问 2：最脆弱的环节在哪里？
答：拷贝上界的”锚刚性”。论证依赖一个五列块实现全部 32 个五比特字，而候选变元行的 1 在每类中呈后缀分布、至多实现 27 个字，由此逼每个拷贝的锚落入指定锚块，再对四种模式逐一核对序关系与阈值赋值。这是大量显式簿记，任何一处模式核对有漏，计数上界即失效。
问 3：与已有工作相比真正的新意是什么？
答：此前的非多项式下界例子（Fischer–Rozenberg、Alon–Ben-Eliezer）都要宿主带第三个符号；本文是首个纯二值宿主的反例，且单个 66×66 图案就否定了猜想。机制上它把”命中 2^h 格即可灭掉现有拷贝、彻底修复却须 4^h 格”的鸿沟做成显式构造，说明 Alon–Ben-Eliezer 关于边不相交拷贝的正结果为何在此失效。
问 4：这个反例为什么不推翻定性删除引理？
答：Alon–Ben-Eliezer–Fischer 的定性版本只说每个固定正距离有正的拷贝密度；本文序列里 ε_h 随 h 趋于零，下界只是随 ε 爆炸得比任何幂都快。玄机在于：把 2^h 个命中格改掉会立刻造出新拷贝，故任何修复仍须至少 4^h 格——”命中集”与”修复”的鸿沟正是删除引理失效之源。
问 5：AI 生成证明最可能出错的模式？
答：显式构造类证明的最大风险是簿记错误——66 阶图案、386h+2 个位置、锚块与哑块的分工、四种模式的冲突核对，任何笔误都可能让距离或计数半边悄悄失效。本文主定理已配 Lean 形式化，风险大降；但采样测试器推论及正文评注是否同被形式化，论文未逐一说明，宜单独核对。
问 6：下游谁会用到？
答：性质测试社区最直接：推论表明行-列均匀采样测试器要保持固定拒绝概率需 q ≥ exp(Ω(ε^{-1/2})) 个采样，超多项式的坏消息首次在二值有序矩阵落地；一切依赖多项式删除引理的有序模式算法，其复杂度保证都需据此重估。
总评
用一个 66 阶显式图案干净地关闭近二十年的猜想，且主定理已形式化，可信度高；余下风险在推论衔接处，以及”构造为何奏效”的机制尚未从个案上升为一般理论。
问 1：证明里最关键的一步是什么？
答：距离下界的逐格采样论证。对任意改动后的矩阵，沿每根轴采样一条树路径加锚位、哑位；凡需保持原值的”受保护”格子，其行、列被同时选中的概率恰为 m^{-2}（m=2^h），对实际改动集作并界，少于 m² 处改动必留下一次完全避开的选取。引言特别强调：逐格论证避免了随类数增长的损失，才拿到 ε_h=(386h+2)^{-2} 这个逆平方距离。
问 2：最脆弱的环节在哪里？
答：拷贝上界的”锚刚性”。论证依赖一个五列块实现全部 32 个五比特字，而候选变元行的 1 在每类中呈后缀分布、至多实现 27 个字，由此逼每个拷贝的锚落入指定锚块，再对四种模式逐一核对序关系与阈值赋值。这是大量显式簿记，任何一处模式核对有漏，计数上界即失效。
问 3：与已有工作相比真正的新意是什么？
答：此前的非多项式下界例子（Fischer–Rozenberg、Alon–Ben-Eliezer）都要宿主带第三个符号；本文是首个纯二值宿主的反例，且单个 66×66 图案就否定了猜想。机制上它把”命中 2^h 格即可灭掉现有拷贝、彻底修复却须 4^h 格”的鸿沟做成显式构造，说明 Alon–Ben-Eliezer 关于边不相交拷贝的正结果为何在此失效。
问 4：这个反例为什么不推翻定性删除引理？
答：Alon–Ben-Eliezer–Fischer 的定性版本只说每个固定正距离有正的拷贝密度；本文序列里 ε_h 随 h 趋于零，下界只是随 ε 爆炸得比任何幂都快。玄机在于：把 2^h 个命中格改掉会立刻造出新拷贝，故任何修复仍须至少 4^h 格——”命中集”与”修复”的鸿沟正是删除引理失效之源。
问 5：AI 生成证明最可能出错的模式？
答：显式构造类证明的最大风险是簿记错误——66 阶图案、386h+2 个位置、锚块与哑块的分工、四种模式的冲突核对，任何笔误都可能让距离或计数半边悄悄失效。本文主定理已配 Lean 形式化，风险大降；但采样测试器推论及正文评注是否同被形式化，论文未逐一说明，宜单独核对。
问 6：下游谁会用到？
答：性质测试社区最直接：推论表明行-列均匀采样测试器要保持固定拒绝概率需 q ≥ exp(Ω(ε^{-1/2})) 个采样，超多项式的坏消息首次在二值有序矩阵落地；一切依赖多项式删除引理的有序模式算法，其复杂度保证都需据此重估。
总评
用一个 66 阶显式图案干净地关闭近二十年的猜想，且主定理已形式化，可信度高；余下风险在推论衔接处，以及”构造为何奏效”的机制尚未从个案上升为一般理论。