定位Gardam单位：F_2[P]中单位的支撑几何及其非唯一积相关群
Localizing the Gardam unit: the support geometry of units in F_2[P] and its non-unique-product relatives
浏览论文内容
中文总结 AI 辅助
本文通过DRAT证明和扫描，确认Gardam单位最小支撑为21，并确定Promislow群及Nielsen-Soelberg群G3的单位定位半径均为4，同时证明最小支撑可计算。
中文摘要 AI 辅助
Gardam对Kaplansky单位猜想的反例是$\mathbb{F}_2[P]$中的一个单位，其中$P$为Promislow群，其支撑有21个元素，Gardam曾询问21是否是最小可能值。在$\mathbb{F}_2$上，单位方程是对一对支撑的奇偶性条件，对于顺从群，该条件既必要又充分，因此可通过在词球上进行搜索来判定。小半径下的图像归功于Dietrich-Lee-Nies-Vinyals，而半径3的陈述是Craven-Pappas定理的一个特例。我们独立地重新推导了这些事实，并将其升级为可认证的陈述：$B(3)$的不存在性带有DRAT证明，并由独立验证器检查；阈值$m_u(P;4)=42$——即两个支撑都在$B(4)$中的任何非平凡单位的总支撑至少为42——通过90路大小分割的DRAT扫描得到认证，从而以球受限形式确认了Gardam的预期。除$P$外，我们还扫描了无挠非唯一积群$H_4$以及Nielsen-Soelberg群$G_1,G_2,G_3$：在搜索的球内均不存在单位（$H_4$、$G_1$、$G_3$到半径3；$G_2$到半径1）。对于$G_3$，这是精确的：通用Nielsen-Soelberg群恰好是Gardam第二个反例的融合$S$，我们将他的定理B中的单位定位到半径4的球内，因此$r_u(G_3)=4=r_u(P)$——这是第二个单位定位半径被确定的群。此外，$H_4$在半径5内抵抗了扭曲酉ansatz，这为Dietrich-Lee-Nies-Vinyals的提议提供了证据，即$H_4$可能满足平凡单位性质而同时不满足唯一积性质。最后，我们证明了一个有效的定位原理：在$\mathbb{F}_2[P]$中，如果存在总支撑为$n$的非平凡单位，则存在一个在明确有界球内的单位，因此最小支撑大小原则上可计算；新的成分是一个奇偶粗化引理。
英文摘要
Gardam's counterexample to the Kaplansky unit conjecture is a unit of $\mathbb{F}_2[P]$, $P$ the Promislow group, with support of size $21$; Gardam asked whether $21$ is least possible. Over $\mathbb{F}_2$ the unit equation is a parity condition on a pair of supports, searchable over word balls. We upgrade two statements to machine-checked certificates: no support pair of sizes $\ge2$ lies in the radius-$3$ ball (a DRAT proof of a ball form of the Craven--Pappas theorem), and every nontrivial unit with supports in the radius-$4$ ball has total support at least $42$, confirming Gardam's expectation in ball-limited form. The relatives $H_4=F(3,4)$ and the Nielsen--Soelberg groups are swept with certificates; $G_3$ is Gardam's amalgam $S$, whose unit we localize into its radius-$4$ ball. $H_4$ resists the twisted-unitary ansatz through radius $6$ for every non-identity dihedral twist. An effective localization principle makes the least support of a nontrivial unit of $\mathbb{F}_2[P]$ computable in principle.
