Sierksma's conjecture for nine points in R³

We prove Sierksma's conjecture for nine points in R³: every nine points of R³, not necessarily distinct, have at least eight Tverberg partitions into three parts, to our knowledge the first case in dimension three. The proof combines equivariant topology (Dold's theorem on twisted constraint complexes), a general position analysis (the Tverberg partitions of a generic configuration cover 76,545 constraints), Hell's parity theorem for Birch partitions, and a finite step: the covering number under the parity restriction is 8, established by an enumeration of matching-covering families, running in about twenty seconds and independently reimplemented; a 42,373-leaf SAT cross-check, recorded as a hash ledger with sampled certificates, confirms it. Without parity the covering number is 7, witnessed by an explicit family, the unique obstruction up to relabelling. Hand-proved lower bounds, their amplification to every dimension, and a linear-programming barrier for weighted double-counting on the pair-constraint system appear in a companion paper. MSC 2020: 52A35 (primary); 05A18, 55M20, 68R05 Reproducibility package: this record archives the manuscript (PDF, v0.3) and its sources; the code and data of the finite enumeration (seeds, lifts, completion search, canonical forms and stabilizers, twist and parity filters, the maximum-multiplicity-two branch, and an independent definition-only reimplementation, with the 17 classes of matching-covering seven-families and the Sierksma control); the SAT cross-check (constraint generator, encodings, symmetry reduction, audit scripts, the task ledger with SHA-256 hashes of every CNF and DRAT proof, samples of the certificates); the exhaustive planar check of Hell's theorem; and the verification commands needed to re-run every check from a clean unpack of the archive. From version 0.3 the manuscript is split in two: this record is paper A; the hand-proved lower bounds, the linear-programming barrier, the amplification to every dimension and the (2,4) order-type evidence are the companion paper (Zenodo, concept DOI 10.5281/zenodo.22582214), whose deposit also carries the code and data behind those results. Computations, proofs, and manuscript preparation were assisted by AI systems directed and verified by the author. The finite checks E1–E5 and the SAT cross-check were independently confirmed by exact rational arithmetic or machine-checked certificates; the planar validation of Theorem 3.10, the counts in Propositions 3.9 and 5.12 (including the general-position checks of the latter) and the pin-lemma check are exact finite computations, labelled as such where they occur; all other results are human proofs.