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}=\operatorname{UT}*3(\mathbb{F}*p)$. Godara and Sarkar proved $\mathsf{d}(H*{27})=6$ and conjectured $\mathsf{d}(H*{p^3})=3p-3$; in a recent preprint, White proved the next case $\mathsf{d}(H_{125})=12$ and left $18\leq\mathsf{d}(H_{343})\leq24$. 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.