Fully balanced permutation sequences: the complete classification

Adams and Segal-Halevi introduced fully balanced permutation sequences as a model of perpetually fair assignment, proved existence for every order n≤ 11 and nonexistence for n=6k (k≥2), for further residue classes modulo 6, and for all n>61, leaving 25 orders undecided. We complete the classification: a fully balanced permutation sequence of order n exists if and only if n ∈{1, …, 11}∪{13, 15, 17, 19, 23, 29}. Three methods are used. First, an elementary counting certificate for nonexistence: integer weights on (day, rank block) pairs such that every admissible player type has nonpositive total weight while the forced daily totals are positive. Its validity is checked by integer addition, it refutes 16 of the open orders, and a single table of twenty-four integers certifies every order n≥ 44 simultaneously; with the finite certificates this lowers the published threshold from 61 to the sharp value 29, independently of the residue-class arguments. Second, satisfiability encodings of the problem and of its prefixes (the main one printed in full), which produce sequences of orders 13, 15, 17, 19, 23 and 29 and refute orders 14 and 21 with DRAT proofs checked by drat-trim. Third, for order 22, an implied tight-rectangle equality and a day-two counting lemma extending an observation of Adams and Segal-Halevi: of the 421 cases of an exhaustive split, 311 are refuted by the lemma and the remaining 110 by checked DRAT proofs. The six sequences, the validity of the certificate for all n ≥ 44, and the obstruction showing that 44 is the best threshold at depth four are also checked in Lean 4. Supplementary archive (balanced-permutation-sequences-supplement-v1.0.0.tar, 0.94 GB): the sequences, prefixes, all weight tables, the order-43 integer witness, Farkas certificates, exact verification programs, the SAT encoders and case-split scripts, a Lean 4 project with axiom audit, and 112 compressed DRAT proofs with their CNFs and SHA-256 manifests.