Verification package for the small Davenport constant of the Heisenberg group of order 343
收藏资源简介:
This dataset contains the complete verification package accompanying the preprint “The small Davenport constant of the Heisenberg group of order 343” (DOI: 10.5281/zenodo.21615339). The main result is d(H_343) = 18 for the Heisenberg group H_343 = UT_3(F_7). The lower bound is witnessed by the product-one-free sequence W_18 = (1,0,0)^6 (0,1,0)^6 (0,0,1)^6. The computer-assisted upper bound uses theoretical reductions, exhaustive stratification, and proof-producing CEGAR-SAT. The package contains the proof archives, seed and learned-cut data, 30 independently checked UNSAT/LRAT certificates, source code for generation and verification, SHA-256 manifests, reconstruction and checking scripts, and the independent audit bundle. It documents 9,920,815 verified seed cuts and 27,207 verified learned cuts across 30 final SAT strata and is intended to permit independent reconstruction and verification of the computational part of the proof. The associated manuscript is a public preprint and has not yet undergone formal peer review.



