Let \[ S=\{(x,y,z)\in\mathbb F_7^3:x^2+y^2+z^2=1\}. \] Direct enumeration gives \(|S|=42\). The displayed set \[ \begin{split} A=\{&(3,5,4),(2,4,4),(2,5,0),(4,3,5),(4,5,3),\\ &(2,0,5),(4,2,4),(5,0,5),(5,3,4),(0,0,1),\\ &(2,3,3),(0,2,5),(5,5,0)\} \end{split} \] lies in \(S\). The executable verifier evaluates all \(2^{13}-1=8191\) nonempty subsets and finds no zero sum. This proves that the unknown maximum \(M\) satisfies \(M\geq13\).

Olson proved the exact Davenport constant for finite abelian p-groups. Applied to \(C_7^3\), it gives \[ D(C_7^3)=1+3(7-1)=19. \] Every sequence of 19 elements of \(C_7^3\) therefore has a nonempty zero-sum subsequence. A 19-point subset of \(S\) is such a sequence, with each term appearing once, so \(M\leq18\). Hence \[ 13\leq M\leq18. \] The computation reported in the candidate record supplies the lower endpoint. This fixture independently replays it. The exact value remains open in this audit.

The 8191 nonempty subsets of \(A\) produce every member of \(\mathbb F_7^3\setminus\{0\}\) and never produce zero. For any \(v\in\mathbb F_7^3\setminus A\) with \(v\ne0\), some nonempty subset of \(A\) sums to \(-v\). Adjoining \(v\) then creates a zero-sum subset. Thus the witness cannot be enlarged, even when new points may be chosen outside the sphere. This maximality property concerns the displayed witness. It does not prove that every zero-sum-free spherical set has at most 13 points.

A focused literature audit located the general zero-sum-free-set framework and the exact p-group Davenport constant, but no result for this 42-point quadratic sphere. Ordaz, Philipp, Santos, and Schmid define the small Olson constant and survey exact cases. Their exact elementary p-group results cover rank at most two and other parameter ranges. Pohoata and Zakharov treat \(\mathbb F_p^d\) asymptotically for fixed dimension and large primes. Neither source determines this restricted instance at \(p=7,d=3\).

The timeboxed feasibility search used one Boolean selection variable \(x_i\) for each sphere point and reachability variables \(r_{i,s}\) for subset sums after the first \(i\) points. Its exact recurrence was \[ r_{i,s}\longleftrightarrow r_{i-1,s}\vee(x_i\wedge r_{i-1,s-v_i}), \] with only \(r_{0,0}\) true. The clause \(\neg x_i\vee\neg r_{i-1,-v_i}\) prevents a newly selected point from closing a zero sum, and a cardinality constraint imposes \(\sum_i x_i=14\).

Orthogonal symmetry sends a selected unit vector to \((0,0,1)\). Its stabilizer has five orbits on permissible second points, indexed by their last coordinate \(0,2,3,4,5\). Z3 returned UNSAT for representatives \((0,1,0)\) and \((0,2,2)\), in 29.684 and 33.485 seconds. The remaining three runs were interrupted to keep the research bounded. No solver proof artifact was retained, so these observations do not improve the certified upper bound of 18.

A complete continuation should run the same finite-state encoding on the last three orbits and retain independently checkable unsatisfiability proofs. If any case is satisfiable, its model supplies a 14-point construction. If all three are unsatisfiable and the two completed cases are rerun with proof logging, the result proves that 13 is exact.

The program enumerates all 343 vectors of \(\mathbb F_7^3\) and confirms that exactly 42 satisfy the unit-sphere equation. It checks that the 13 displayed vectors are distinct sphere points. It then enumerates every nonempty subset by cardinality, reduces its coordinate sum modulo 7, and asserts that zero never occurs.

The union of the subset-sum images has size 342, equal to the number of nonzero ambient vectors. Across all subset cardinalities, a nonzero vector has between 1 and 52 representations. The numbers of distinct sums at cardinalities 1 through 13 are \[ 13,63,138,199,230,251,251,230,199,138,63,13,1. \] The canonical summary has SHA-256 digest `4c8d575a1977615fcc5205ed8eb14b59f079740153789e32b799a60a4e6fb2a9`.