The small Davenport constant of the Heisenberg group of order 343

Abstract

For a finite group $G$, let $\mathsf{d}(G)$ denote the maximum length of a sequence having no nonempty subsequence whose terms can be ordered to have product one. For an odd prime $p$, let $H_{p^3}=\mathrm{UT}\ast 3(\mathbb{F}\ast p)$. Godara and Sarkar proved $\mathsf{d}(H\ast 27)=6$ and conjectured $\mathsf{d}(H\ast p^3)=3p-3$; in a recent preprint, White proved the next case $\mathsf{d}(H_{125})=12$ and left $18\le \mathsf{d}(H_{343})\le 24$. We prove $\mathsf{d}(H_{343})=18$. We adopt White's product-one criterion and spread framework and develop a $p=7$-specific direction stratification. An explicit product-one-free sequence gives the lower bound. For the upper bound, we stratify a hypothetical product-one-free sequence of length $19$ by the number of central terms and by the occupied projective directions of its quotient multiset. Supports on at most two directions are excluded by a theoretical argument whose finite auxiliary statements are exhaustively checked; the three-direction case and the case of five central terms are settled by exact finite computations. The remaining thirty strata are encoded by a counterexample-guided SAT procedure. A separately implemented checker verifies all $9,920,815$ seed cuts and all $27,207$ learned cuts, and each final unsatisfiable instance is accompanied by a checked LRAT certificate. A separate implementation-level audit verifies the master encoding, the proof archives, and the lower-bound witness.

15 pages, 3 tables; computer-assisted proof. Verification package available at https://doi.org/10.5281/zenodo.21833183