Alternating acceptance is Σₖ-definable

The membership half of the machine bridge for the polynomial hierarchy: ATMAccept (k+1) true is Σₖ₊₁-definable, hence in Σₖ₊₁ᵖ, and ATMAccept (k+1) false is Πₖ₊₁-definable, hence in Πₖ₊₁ᵖ. The two are the same sentence at the two starting polarities.

The proof is the assembly of the four layers below it:

• alternating acceptance is the k-round game (DescriptiveComplexity.ATMData.altAccepts_iff_altGame), and the game is an implication ladder (DescriptiveComplexity.ATMData.altGame_iff_altLadder), provided a start state exists – which is what DescriptiveComplexity.akStartExClause contributes to the kernel;
• the ladder over walks is the ladder over the relations a block guesses (DescriptiveComplexity.ATMData.altLadder_iff_runAltLadder);
• the ladder's own quantifiers are the alternating prefix over one guess per round (DescriptiveComplexity.ATMData.altBlockQuant_runMatrix), leaving the quantifier-free matrix behind;
• the matrix is the kernel (DescriptiveComplexity.realize_akKernel), and the prefix is k+1 copies of one block (DescriptiveComplexity.sorealize_repBlocks).

Definability