Walking the positions, and reading a play off a walk

The bookkeeping between the two shapes a round of the game comes in: a walk, one configuration per position, which is what a second-order block guesses, and a play (DescriptiveComplexity.ATMData.BlockPlay), an ℕ-indexed sequence of steps, which is what the collapse lemmas of DescriptiveComplexity.MachinesAltPlay speak about. Translating between them is arithmetic on DescriptiveComplexity.bitRank, exactly as DescriptiveComplexity.TMData.accepts_iff_exists_walk cashes in the unary time bound of the nondeterministic bridge.

The order facts

The rank is injective on positions (DescriptiveComplexity.ATMData.bitRank_inj), so a position is the highest one exactly when its rank is (DescriptiveComplexity.ATMData.maxPos_iff_rank), and comparing ranks compares positions (DescriptiveComplexity.ATMData.le_of_bitRank_le). Iterating DescriptiveComplexity.ATMData.nextPos from a position therefore enumerates the positions above it in order, its rank going up by one each time (DescriptiveComplexity.ATMData.posSeq_spec), until the highest is reached – which is where the budget of a configuration comes from: from the position t there are exactly rank p₁ - rank t steps left.

Reading a play

DescriptiveComplexity.ATMData.exists_play_of_legalBelow is the one theorem here: from a walk legal below i + 1 and a position t whose configuration is in block i, the configurations at t, nextPos t, … form a play of block i, stopped at the first moment the walk leaves the block, accepts, gets stuck, or runs out of budget. Those four alternatives are exactly the cases the two collapse lemmas distinguish, so this is the whole interface the round induction needs in that direction.

Ranks and positions

theorem DescriptiveComplexity.ATMData.bitRank_inj {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {x y : A} (hx : M.Posn x) (hy : M.Posn y) (h : bitRank M.Le M.Posn x = bitRank M.Le M.Posn y) : x = y

The rank is injective on positions.

theorem DescriptiveComplexity.ATMData.le_of_bitRank_le {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {x y : A} (hx : M.Posn x) (hy : M.Posn y) (h : bitRank M.Le M.Posn x ≤ bitRank M.Le M.Posn y) : M.Le x y

Comparing ranks compares positions.

theorem DescriptiveComplexity.ATMData.maxPos_iff_rank {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {x p₁ : A} (hx : M.Posn x) (hmax : MaxPos M.Le M.Posn p₁) : MaxPos M.Le M.Posn x ↔ bitRank M.Le M.Posn x = bitRank M.Le M.Posn p₁

A position is the highest one exactly when its rank is.

theorem DescriptiveComplexity.ATMData.bitRank_lt_of_not_maxPos {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {x p₁ : A} (hx : M.Posn x) (hmax : MaxPos M.Le M.Posn p₁) (h : ¬MaxPos M.Le M.Posn x) : bitRank M.Le M.Posn x < bitRank M.Le M.Posn p₁

The rank of a position other than the highest is below the highest rank.

theorem DescriptiveComplexity.ATMData.posSeq_spec {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {t p₁ : A} (ht : M.Posn t) (hmax : MaxPos M.Le M.Posn p₁) (j : ℕ) : j ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t → M.Posn (M.posSeq t j) ∧ bitRank M.Le M.Posn (M.posSeq t j) = bitRank M.Le M.Posn t + j

Iterating nextPos enumerates the positions above t in order: the j-th one is a position of rank rank t + j, as long as the budget rank p₁ - rank t has not run out.

theorem DescriptiveComplexity.ATMData.posSeq_succPos {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {t p₁ : A} (ht : M.Posn t) (hmax : MaxPos M.Le M.Posn p₁) {j : ℕ} (hj : j < bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t) : SuccPos M.Le M.Posn (M.posSeq t j) (M.posSeq t (j + 1))

Consecutive positions of the enumeration are immediate successors.

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

The enumeration reaches the highest position exactly at the end of the budget.

Reading a play off a sequence

theorem DescriptiveComplexity.ATMData.exists_play_of_seq {A : Type} {M : ATMData A} {i : ℕ} {c : Config A} {g : ℕ → Config A} (n : ℕ) (hg0 : g 0 = c) (hgstep : ∀ j < n, M.Blk i (g j).state → ¬M.Acc (g j).state → ¬M.Stuck (g j) → M.Step (g j) (g (j + 1))) : ∃ ℓ ≤ n, M.BlockPlay i c ℓ g ∧ (ℓ = n ∨ ¬M.Blk i (g ℓ).state ∨ M.Acc (g ℓ).state ∨ M.Stuck (g ℓ))

Cutting a sequence of configurations into a play of block i. The sequence is stopped at the first of four events – the bound n is reached, the sequence leaves the block, it accepts, it gets stuck – and up to there it is a DescriptiveComplexity.ATMData.BlockPlay. The only thing asked of the sequence is that it takes a genuine step whenever none of the four has happened, which is what both a legal walk and the greedy continuation of DescriptiveComplexity.ATMData.greedy provide.

theorem DescriptiveComplexity.ATMData.BlockPlay.congr {A : Type} {M : ATMData A} {i : ℕ} {c : Config A} {ℓ : ℕ} {f g : ℕ → Config A} (h : ∀ j ≤ ℓ, f j = g j) (hf : M.BlockPlay i c ℓ f) : M.BlockPlay i c ℓ g

A play depends only on its first ℓ + 1 configurations.

Reading a play off a walk

theorem DescriptiveComplexity.ATMData.exists_play_of_legalBelow {A : Type} [Finite A] {M : ATMData A} (hlin : IsLinOrd M.Le) {i : ℕ} {w : A → Config A} (hw : M.LegalBelow (i + 1) w) {t p₁ : A} (ht : M.Posn t) (hmax : MaxPos M.Le M.Posn p₁) : ∃ ℓ ≤ bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn t, (M.BlockPlay i (w t) ℓ fun (j : ℕ) => w (M.posSeq t j)) ∧ (ℓ = 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 ℓ)))

A walk legal below i + 1 carries a play of block i. From the position t, whose configuration is in block i, follow the walk along the order: the configurations form a play of block i, and it stops at the first moment one of the four things happens that end a block – the budget runs out, the walk leaves the block, it accepts, or it gets stuck.