Pure O-sequences in four variables are unimodal up to socle degree six

Boyle proved that pure O-sequences in four variables are unimodal for socle degree at most 4, and that nonunimodal ones exist in four variables for every socle degree at least 7; the survey of Migliore, Nagel and Zanello (arXiv:1204.5247) records that in codimension 4 only socle degrees 5 and 6 remained open. We settle both cases: every pure O-sequence in at most four variables of socle degree 5 or 6 is unimodal. Consequently, in four variables, all pure O-sequences of socle degree e are unimodal if and only if e ≤ 6. The proof reduces each possible failure of unimodality, h_j > h_k < h_l, to one of 30 explicit 0/1 systems, using an encoding lemma proved by hand. Each system is shown infeasible by integer programming, and each is refuted by SAT solvers whose DRUP/DRAT proofs are checked by drat-trim. The hardest system is split, by three elementary covering arguments, into 454 separately certified cases, and an audit script confirms that the case tree is complete. We also record an explicit nonunimodal pure O-sequence of socle degree 7 in four variables, (1, 4, 10, 20, 35, 42, 41, 42). The CNF formulas, logs, scripts and audit tools are provided as an ancillary package.