AI 中文总结
本文计算Hantzsche-Wendt群P对应的F₂[P]在半径4处的单侧非平凡单位数为52，通过DRAT证明的完备性结果，首次在单位猜想失效的半径处分离积分群环与其特征2商环。
AI 中文摘要
设P为Hantzsche-Wendt（Promislow）群，B(4)为其标准字度量下的半径4球。Dietrich、Lee、Nies和Vinyals确定了双侧计数：F₂[P]中恰好有36个非平凡单位u，满足supp(u)和supp(u⁻¹)均在B(4)内。本文确定单侧计数：恰好有52个非平凡单位满足supp(u)在B(4)内，对其逆无约束。这16个新单位的逆恰好支撑在半径5处，在固定生成集的对称群下形成2个大小为8的轨道，且所有52个单位的两侧支撑大小均为21。完备性是单个命题不可满足问题，由经drat-trim验证的DRAT证明确认。作为算术推论，本文证明：Z[P]中支撑在B(4)内的单位，模2后无平凡约化，且对系数或逆的支撑无约束。由于F₂[P]在该球上有52个非平凡单位，本文在非扭转情形下，于单位猜想在域上失效的首个半径处，将积分群环与其特征2商环分离开来。
英文摘要
Let P be the Hantzsche-Wendt (Promislow) group and B(4) the radius-four ball in its standard word metric. Dietrich, Lee, Nies and Vinyals determined the two-sided count: exactly 36 nontrivial units u of F_2[P] with both supp(u) and supp(u^{-1}) in B(4). We determine the one-sided count: exactly 52 nontrivial units with supp(u) in B(4) and no constraint on the inverse. The 16 new units have inverses supported at radius exactly 5; they form two orbits of size 8 under the symmetry group fixing the generating set, and all 52 units have support size 21 on both sides. Completeness is a single propositional unsatisfiability, certified by a DRAT proof checked with drat-trim. As an arithmetic consequence we prove: no unit of Z[P] with support in B(4) has nontrivial reduction modulo 2 -- with no bound on the coefficients or on the support of the inverse. Since F_2[P] has 52 nontrivial units on that ball, this separates, in the untwisted setting, the integral group ring from its characteristic-two quotient at the first radius where the unit conjecture fails over a field.
Comments12 pages. Ancillary files: complete data (52 units, orbit representatives, box computation), all verification scripts, and the drat-trim verification transcript
