The fully independent SparseStack sketch is a vertical stack of $s$ independent CountSketch matrices, scaled by $s^{-1/2}$, so that every column has exactly $s$ nonzero entries. We prove that it is an oblivious subspace embedding for $d$-dimensional subspaces with distortion $ε$ and failure probability $δ$ when $m = O((d+\log(1/δ))/ε^2)$ and $s = O(\log(d/δ)/ε)$, with explicit constants. These are the parameters conjectured by Nelson and Nguyen (FOCS 2013) for this construction; the row count is optimal by their lower bound. The proof bounds the even moments of the Gram error. A conditional-expectation coupling replaces each signed one-hot column selector by a vector with independent three-point entries, at the cost of a constant factor per moment order. The three-point law has a three-dimensional $L_2$ space, so multiplication by an entry is a $3 \times 3$ Jacobi matrix, and the $2q$-th moment becomes a vacuum matrix element of a deterministic operator on a finite tensor product, graded by total occupation. The operator has three grade bands, and we bound each band on the grade-$ν$ sector by $C(\sqrt{(d+ν+1)/m} + (d+ν+1)/m + (ν+1)/s)$ with $C = 3+\sqrt{2}$. The key step is a shared-factor inequality: each row block of the positive operator attached to one tensor slot is rank one with trace $d$, and the sum over $\ell$ slots sharing the same external factor has norm at most $d+\ell-1$. A $2q$-step expansion and Markov's inequality complete the argument, which is finite-dimensional and does not use Gaussian comparison. The theorem has been formally verified in Lean 4. The proof was developed with AI systems under the author's direction, as disclosed in the paper.