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.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.

Reading a play off a sequence

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.