One round of the game, and what it leaves behind

The step of the induction that turns alternating acceptance into the k-round game. Round i starts at the position t, in the configuration the previous round handed over; whatever walk it plays describes a play of block i (DescriptiveComplexity.Problems.Machine.AltRank), and DescriptiveComplexity.ATMData.game_iff_end says that the rest of the game is decided by how that play ends – which is exactly the shape DescriptiveComplexity.ATMData.PlayEnds and DescriptiveComplexity.ATMData.UnivPlayOk of the two collapse lemmas.

Two things end a play. Either it hands over to block i + 1, and then the rest of the game is the game from round i + 1, by the induction hypothesis; or it stops inside block i, and then – because acceptance is absorbing and a stuck configuration cannot move – the walk stands still from there to the highest position, every block is low, and DescriptiveComplexity.ATMData.gameFrom_of_blkLt reduces the rest of the game to whether that configuration accepts.

Blocks along a sequence

Standing still

The rest of the game, read off the end of the play

theorem DescriptiveComplexity.ATMData.game_iff_end {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {p₁ : A} (hmax : MaxPos M.Le M.Posn p₁) (start : Bool) {i m : ℕ} (hIH : ∀ (v : A → Config A) (t' : A), M.LegalBelow (i + 1) v → M.Posn t' → M.Blk (i + 1) (v t').state → (∀ (s : A), M.Posn s → M.Le s t' → s ≠ t' → M.BlkLt (i + 1) (v s).state) → (M.AltAcc start (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t') (v t') ↔ M.gameFrom start (i + 1) m v)) {t : A} (ht : M.Posn t) {w : A → Config A} (hw : M.LegalBelow (i + 1) w) (hwt : M.Blk i (w t).state) (hpastw : ∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (w s).state) {ℓ : ℕ} (hℓ : ℓ ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) (hplay : M.BlockPlay i (w t) ℓ fun (j : ℕ) => w (M.posSeq t j)) (hstop : ℓ = bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t ∨ ¬M.Blk i (w (M.posSeq t ℓ)).state ∨ M.Acc (w (M.posSeq t ℓ)).state ∨ M.Stuck (w (M.posSeq t ℓ))) : (M.gameFrom start (i + 1) m w ↔ M.PlayEnds start i (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) ℓ fun (j : ℕ) => w (M.posSeq t j)) ∧ (M.gameFrom start (i + 1) m w ↔ M.UnivPlayOk start i (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) ℓ fun (j : ℕ) => w (M.posSeq t j))

What the rest of the game decides: the game from round i + 1 holds exactly when the play of block i that round i's walk describes ends well – in either of the two readings the collapse lemmas use.

One round, against an abstract admissibility condition

Both the induction step and its base – the first round, which has nothing to inherit – are this one lemma, differing only in what makes a walk admissible. C is that condition; the four hypotheses say it forces a walk to be legal below i + 1, to start the round at c, to keep the past in low blocks, and to be met by the walk DescriptiveComplexity.ATMData.splice builds out of any play that ends the way a round may end.

The induction over the rounds

Acceptance is the game

theorem DescriptiveComplexity.ATMData.altAccepts_iff_altGame {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {p₁ : A} (hmax : MaxPos M.Le M.Posn p₁) (start : Bool) {p₀ : A} (hmin : MinPos M.Le M.Posn p₀) (hk : 0 < k) : M.AltAccepts start ↔ M.AltGame start k

Alternating acceptance is the k-round game. The first round has nothing to inherit, so it is the general round with the initial configuration as its own choice – which is why DescriptiveComplexity.ATMData.AltAccepts quantifies that configuration at the polarity of block 0.