Exact Zarankiewicz Values On Two Finite Frontier Slices

技术摘要：两个有限前沿切片的精确 Zarankiewicz 值

问题陈述
本文研究了 Zarankiewicz 问题，该问题旨在寻找在包含 $K_{s,t}$ 完全二部子图的规模为 $m$ 和 $n$ 的二部图中，最大边数（记作 $Z(m, n, s, t)$）。作者特别关注 $s=t=3$（避免 $K_{3,3}$）的情况，针对中等规模的有限参数进行研究。虽然渐近理论已发展成熟，但由于极高的对称性和证明认证的高昂成本，特定有限维度的精确值计算仍然十分困难。本文的目标是一个此前未解决或部分解决的“有限前沿”值，包括条带 $Z(12, n, 3, 3)$（其中 $18 \le n \le 22$）、特定情形 $Z(13, 22, 3, 3)$，以及围绕 $13 \times 18$ 和 $16 \times 17$ 的一组相邻值。

方法论
其证明是计算机辅助的，但严格基于证书（certificate-based），这有别于仅依赖混合整数线性规划（MILP）求解器返回“不可行”或没有显式见证者的 SAT 求解器。验证过程依赖于精确的整数和有理数算术（使用 Python 的 Fraction 及标准库），仅在初始发现证书阶段使用浮点优化。

该方法采用了多层归约策略：

1. 全局松弛与度分布（Degree Profiles）： 对于 $13 \times 22$ 的情形，作者假设存在一个具有 138 条边的矩阵。通过分析与列度数相关的“惩罚”函数 $p(d) = \binom{d}{3} - 15d + 70$，搜索空间从所有可能的矩阵缩减至仅 83 个不同的度分布（列度数的直方图）。
2. Farkas 证书： 对于这 83 个分布中的 77 个，作者构建了精确的有理 Farkas 证书。这些证书通过证明：在给定分布下，由 $K_{3,3}$-free 条件（即每个行三元组最多出现在 2 列中）所施加的线性约束无法满足任何非负整数解，从而证明了不可行性。
3. 标记行与剩余项枚举： 剩余的 6 个分布通过更细粒度的技术进行排除。作者固定一个“标记行”，删除该行，并分析剩余 12 个点上的“剩余多重图（leave multigraph）”。这涉及：
   • 同余论证： 利用行亏损（row deficits）的模运算来排除特定配置（例如分布 6187391）。
   • Gram 矩阵约束： 检查剩余块（residual blocks）关联矩阵的秩和行列式条件。
   • 精确枚举： 对剩余块设计进行穷举，并将整数缩放的 Farkas 证书应用于剩余的分解系统。
4. 删除引理与见证者： 对于 $12 \times n$ 条带和前沿闭合，作者使用“删除引理”（将 $Z(m, n)$ 与 $Z(m, n-1)$ 联系起来）结合显式的构造性见证者（实现下界的矩阵）来建立精确等式。

主要贡献与结果
本文为以下精确值和界限提供了结合证书的证明：

• $12 \times n$ 条带： 证明了对于 $18 \le n \le 22$， $Z(12, n, 3, 3) = 6n$。这是通过 $Z(12, 18, 3, 3) = 108$ 的精确证书以及随后由显式见证者支持的删除论证来确立的。
• $13 \times 22$ 情形： 证明了 $Z(13, 22, 3, 3) = 137$。通过上述详尽的分布分析排除了 138 条边的可能性。137 的下界通过显式构造（一个具有 137 个 1 且不含 $K_{3,3}$ 的 $13 \times 22$ 二进制矩阵）得到确认。
• 前沿闭合： 确定了四个相邻单元格的精确值：
  • $Z(13, 18, 3, 3) = 116$
  • $Z(14, 17, 3, 3) = 118$
  • $Z(14, 18, 3, 3) = 124$
  • $Z(15, 17, 3, 3) = 126$
  • $Z(15, 18, 3, 3) = 132$
• $16 \times 17$ 区间： 报告了区间 $132 \le Z(16, 17, 3, 3) \le 133$。下界由一个新的 132 边见证者支持；上界 133 取自先前文献（Collins 等人）。论文明确指出，该特定单元格的精确值在本研究中并未确定。

意义与主张
作者声称这项工作为这些特定的 Zarankiewicz 值提供了完整、可复现且基于证书的证明。其意义在于实现了发现（其中可能使用浮点启发式算法）与验证（使用仅精确算术）的严格分离。

• 可复现性： 论文包含一个“一键验证门”，用于重演所有 570 万次精确的非负性检查，包括重新生成度分布、重演 Farkas 证书以及对剩余块设计的穷举。
• 谦逊态度： 作者明确指出，这些结果应被视为“待独立复现和同行评审的新型计算机辅助证明”。论文并不声称解决了通用的 Zarankiewicz 问题或提供了一种通用算法，而是展示了有限极值问题中的分工：利用粗略的全局松弛消除大部分情况，并将计算密集型的精确枚举保留给少数“困难”的残余分布。
• 现有技术： 作者指出，虽然 $13 \times 22$ 的 137 边构造此前已有报道，但精确上界是新的贡献。同样，对于 $12 \times n$ 条带（$n=18$ 至 $21$）的具体值以及前沿闭合值，均被报告为截至论文日期（2026 年 8 月）在现有索引文献中未发现的新精确结果。

论文最后强调，没有任何未经验证的 DRAT 主张、SAT 超时或浮点求解器状态被用作定理的前提，确保了数学主张完全建立在显式的有限数据和精确算术之上。