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

theorem DescriptiveComplexity.ATMData.le_blk_of_blockPlay {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {i : ℕ} {c : Config A} {ℓ : ℕ} {f : ℕ → Config A} (hplay : M.BlockPlay i c ℓ f) (hc : M.Blk i c.state) (j : ℕ) : j ≤ ℓ → ∀ (jj : ℕ), M.Blk jj (f j).state → i ≤ jj

The blocks along a play never decrease: a play takes genuine steps, and a step never lowers the block.

theorem DescriptiveComplexity.ATMData.PlayEnds.congr {A : Type} {M : ATMData A} {start : Bool} {i n ℓ : ℕ} {f g : ℕ → Config A} (h : f ℓ = g ℓ) (hf : M.PlayEnds start i n ℓ f) : M.PlayEnds start i n ℓ g

Both readings of the end of a play depend only on its last configuration.

theorem DescriptiveComplexity.ATMData.UnivPlayOk.congr {A : Type} {M : ATMData A} {start : Bool} {i n ℓ : ℕ} {f g : ℕ → Config A} (h : f ℓ = g ℓ) (hf : M.UnivPlayOk start i n ℓ f) : M.UnivPlayOk start i n ℓ g

The universal reading likewise.

Standing still

theorem DescriptiveComplexity.ATMData.constant_of_absorbing {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {i : ℕ} {w : A → Config A} (hw : M.LegalBelow i w) {x : A} (hx : M.Posn x) (hb : M.BlkLt i (w x).state) (habs : M.Acc (w x).state ∨ M.Stuck (w x)) (y : A) : M.Posn y → M.Le x y → w y = w x

An absorbing configuration is never left. Once a walk is accepting or stuck at a position whose block it still answers for, its legality forces it to stand still at every later position.

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

theorem DescriptiveComplexity.ATMData.posSeq_eq_of_le {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {p₁ : A} (hmax : MaxPos M.Le M.Posn p₁) {t s : A} (ht : M.Posn t) (hs : M.Posn s) (hle : M.Le t s) : s = M.posSeq t (bitRank M.Le M.Posn s - bitRank M.Le M.Posn t)

A position above t is the one the enumeration reaches at its rank.

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.

theorem DescriptiveComplexity.ATMData.altAcc_iff_guardQ {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) {c : Config A} (hc : M.Blk i c.state) {C : (A → Config A) → Prop} (hC1 : ∀ (w : A → Config A), C w → M.LegalBelow (i + 1) w) (hC2 : ∀ (w : A → Config A), C w → w t = c) (hC3 : ∀ (w : A → Config A), C w → ∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (w s).state) (hC4 : ∀ (ℓ : ℕ) (f : ℕ → Config A), ℓ ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t → M.BlockPlay i c ℓ f → (ℓ < bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t → M.BlkLt (i + 1) (f ℓ).state → M.Acc (f ℓ).state ∨ M.Stuck (f ℓ)) → ∃ (w : A → Config A), C w ∧ ∀ j ≤ ℓ, w (M.posSeq t j) = f j) : M.AltAcc start (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) c ↔ guardQ (blockPol start i) C fun (w : A → Config A) => M.gameFrom start (i + 1) m w

One round of the game.

The induction over the rounds

theorem DescriptiveComplexity.ATMData.gameFrom_iff {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) (m i : ℕ) : i + m = k → 0 < i → ∀ (prev : A → Config A) (t : A), M.LegalBelow i prev → M.Posn t → M.Blk i (prev t).state → (∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (prev s).state) → (M.AltAcc start (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) (prev t) ↔ M.gameFrom start i m prev)

The game from round i on decides acceptance at the entry into block i. The induction is on the number of rounds left; the base case is vacuous because a state of block k does not exist, and the step is DescriptiveComplexity.ATMData.altAcc_iff_guardQ with the agreement condition of the round as its admissibility.

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.