The minimum cardinality is \[ 19. \] One attaining set is \[ A=\{0,\pm2,\pm7,\pm30,\pm37,\pm38,\pm43,\pm48,\pm60,\pm63\}\subseteq\mathbb Z/127\mathbb Z. \] In least nonnegative residues this is \[ \{0,2,7,30,37,38,43,48,60,63,64,67,79,84,89,90,97,120,125\}. \] The executable certificate forms all 361 ordered sums and obtains all 127 residues.

Every admissible set has cardinality \(2k+1\). The counting argument in sdb127-claim-counting-lower-bound gives \(k\geq8\), so the only smaller case is cardinality 17. Multiplication by a nonzero residue preserves symmetry and the basis property. Any hypothetical 17-element basis can therefore be normalized so that its eight positive inverse-pair representatives include 1. The exhaustive certificate checks every such normalized choice and proves that none covers all 63 nonzero inverse classes. Thus the displayed 19-element basis is minimum.

Write an admissible set as \[ A=\{0,\pm a_1,\ldots,\pm a_k\}. \] Identify each nonzero residue with its inverse pair \(\{r,-r\}\). Every nonzero class in \(A+A\) must occur in one of four forms: \(a_i\), \(2a_i\), \(a_i+a_j\), or \(a_i-a_j\), with \(i<j\) in the last two forms. There are at most \[ k+k+2\binom{k}{2}=k^2+k \] such classes. The group \(\mathbb Z/127\mathbb Z\) has 63 nonzero inverse classes, so \(k^2+k\geq63\). Hence \(k\geq8\) and \(|A|=2k+1\geq17\). This count also supplies the collision budget used by the exact search: at \(k=8\), the 72 formal sum types may contain at most nine repetitions if all 63 classes are to appear.

Because \(A=-A\), the condition \(A+A=\mathbb Z/127\mathbb Z\) is equivalent to \(A-A=\mathbb Z/127\mathbb Z\). This places the problem inside the theory of difference bases. Banakh and Gavrylkiv define the unrestricted difference size \(\Delta[C_n]\), prove \[ \frac{1+\sqrt{4n-3}}2\leq\Delta[C_n]\leq\frac32\sqrt n, \] and calculate exact cyclic values through \(n=100\). Their definition allows arbitrary bases. It does not impose \(0\in A\) or \(A=-A\), and the tabulated exact range stops before 127. A focused search by the modulus, the inverse-closed condition, and the symmetric sum-basis formulation found no published value for this normalization. The exact value 19 in this dataset therefore rests on the reproduced finite certificate.

The search represents each inverse pair \(\{x,-x\}\) by the integer \(\min(x,127-x)\) in \(\{1,\ldots,63\}\). For a chosen representative \(v\), it inserts the classes of \(v\) and \(2v\). For each earlier representative \(u\), it also inserts the classes of \(v+u\) and \(v-u\). Thus a partial choice of \(t\) representatives has generated \(t^2+t\) formal sum types.

At size eight there are 72 formal types and all 63 classes must be distinct except for at most nine repetitions. The number of repetitions can only increase as representatives are added, so a partial branch with more than nine repetitions is impossible and may be pruned. The program enumerates every increasing eight-subset containing 1 that survives this exact prune. This normalization is complete: given any candidate and any selected nonzero representative \(s\), multiplication by \(s^{-1}\) sends its inverse pair to \(\{1,-1\}\) and preserves all hypotheses.

The run visited 42,244,920 nodes and finished all 56 second-representative branches without finding a size-17 basis. It separately checked that the displayed size-19 set has 19 distinct elements and covers all 127 residues.