The k-round game: what a Σₖ definition of alternating acceptance guesses

DescriptiveComplexity.ATMData.AltAcc recurses one step at a time; a Σₖ sentence has k quantifiers and must therefore commit a whole round at a time. This file defines the round game – the object the second-order blocks of the membership proof guess – together with the facts about walks it needs. No vocabulary appears, as in DescriptiveComplexity.Machines; the file sits under Problems/Machine only because it reads the rank machinery of DescriptiveComplexity.Problems.Machine.Walk.

What a round guesses

A walk is a configuration per position, positions being times as everywhere in the bridge. Round i's walk is asked for three things (DescriptiveComplexity.ATMData.LegalBelow):

• it is initial at the lowest position;
• its blocks never decrease along the order (DescriptiveComplexity.ATMData.BlkMono) – true of any real run, and needed of a guess so that the times of a block form one stretch rather than several;
• at each immediate successor it steps out of a non-accepting configuration, or stutters in an accepting or stuck one – but only where its state is in a block below i.

Acceptance is therefore absorbing: a walk that has accepted may not move again, so it still accepts at the highest position, and every later round is obliged to copy it. Without that, a round could step past an acceptance and let a later player steer the run into rejection, while DescriptiveComplexity.ATMData.AltAcc grants an accepting configuration outright.

The last restriction is what keeps the game cheap. Round i answers for the blocks up to i and no further, so its walk may be arbitrary from the moment it hands over; that is why building a witness never needs a legal continuation to the end of time. Stuttering must be allowed at a stuck configuration, not only at an accepting one as in DescriptiveComplexity.TMData.IsWalk: otherwise a machine that stops has no legal walk at all, the universal rounds become vacuous, and getting stuck would count as accepting – the opposite of the convention of DescriptiveComplexity.MachinesAlt.

What a round inherits

DescriptiveComplexity.ATMData.AgreeBelow makes round i reproduce what the earlier rounds committed: the configuration at every time whose block – in the previous round's walk – is below i, and the configuration at the immediate successor of such a time. The second clause is not redundant: the move out of the last configuration of block i - 1 belongs to the previous player, so the successor of a committed time is committed too. At i = 0 both clauses are vacuous, which is why the first round is free (DescriptiveComplexity.ATMData.altGame_eq_gameFrom).

The order lemmas

Two facts about the linear order of the positions are proved here and used throughout: induction upwards from a position (DescriptiveComplexity.ATMData.le_induction), and the successor function DescriptiveComplexity.ATMData.nextPos walking along it, whose rank increases by one until the highest position is reached.

Induction along the positions

theorem DescriptiveComplexity.ATMData.le_induction {A : Type} {M : ATMData A} [Finite A] (hlin : IsLinOrd M.Le) {P : A → Prop} {s : A} (hs : M.Posn s) (hP : P s) (hstep : ∀ (p q : A), SuccPos M.Le M.Posn p q → M.Le s p → P p → P q) (q : A) : M.Posn q → M.Le s q → P q

Induction upwards from a position: a property holding at s and inherited along immediate successors holds at every position above s. The same induction as DescriptiveComplexity.TMData.stepsIn_of_segment, isolated because the game needs it for properties that are not about runs.

noncomputable def DescriptiveComplexity.ATMData.nextPos {A : Type} (M : ATMData A) (t : A) : A

The next position after t, or t itself at the highest position.

Equations

• M.nextPos t = if h : ∃ (q : A), DescriptiveComplexity.SuccPos M.Le M.Posn t q then h.choose else t

theorem DescriptiveComplexity.ATMData.succPos_nextPos {A : Type} {M : ATMData A} {t : A} (h : ∃ (q : A), SuccPos M.Le M.Posn t q) : SuccPos M.Le M.Posn t (M.nextPos t)

noncomputable def DescriptiveComplexity.ATMData.posSeq {A : Type} (M : ATMData A) (t : A) : ℕ → A

The positions reached from t by stepping j times along the order.

Equations

• M.posSeq t 0 = t
• M.posSeq t j.succ = M.nextPos (M.posSeq t j)

@[simp]

theorem DescriptiveComplexity.ATMData.posSeq_zero {A : Type} (M : ATMData A) (t : A) : M.posSeq t 0 = t

@[simp]

theorem DescriptiveComplexity.ATMData.posSeq_succ {A : Type} (M : ATMData A) (t : A) (j : ℕ) : M.posSeq t (j + 1) = M.nextPos (M.posSeq t j)

theorem DescriptiveComplexity.ATMData.succPos_nextPos_of_not_max {A : Type} {M : ATMData A} [Finite A] (hlin : IsLinOrd M.Le) {t : A} (ht : M.Posn t) (hmax : ¬MaxPos M.Le M.Posn t) : SuccPos M.Le M.Posn t (M.nextPos t)

The rank increases by one along nextPos, as long as the highest position has not been reached.

Walks

def DescriptiveComplexity.ATMData.BlkMono {A : Type} (M : ATMData A) (w : A → Config A) : Prop

The blocks of a walk never decrease. True of any run, and asked of a guess so that the times of one block form a single stretch.

Equations

• M.BlkMono w = ∀ (p q : A), DescriptiveComplexity.SuccPos M.Le M.Posn p q → ∀ (j j' : ℕ), M.Blk j (w p).state → M.Blk j' (w q).state → j ≤ j'

def DescriptiveComplexity.ATMData.LegalBelow {A : Type} (M : ATMData A) (i : ℕ) (w : A → Config A) : Prop

A walk legal below block i: initial at the lowest position, with non-decreasing blocks, and stepping or stuttering at every immediate successor whose configuration is in a block below i. Round i of the game guesses a walk legal below i + 1: it answers for its own block and no later one.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.ATMData.AccAt {A : Type} (M : ATMData A) (w : A → Config A) : Prop

The walk accepts: its state at the highest position is accepting.

Equations

• M.AccAt w = ∀ (p : A), DescriptiveComplexity.MaxPos M.Le M.Posn p → M.Acc (w p).state

def DescriptiveComplexity.ATMData.AgreeBelow {A : Type} (M : ATMData A) (i : ℕ) (w prev : A → Config A) : Prop

Round i reproduces what the earlier rounds committed: the configuration at every time whose block in prev is below i, and at the immediate successor of such a time – the move out of the last committed configuration belonging to the previous player.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.ATMData.RoundCond {A : Type} (M : ATMData A) (i : ℕ) (prev w : A → Config A) : Prop

The condition round i puts on its walk: legal below i + 1, and agreeing with the previous round below i.

Equations

• M.RoundCond i prev w = (M.LegalBelow (i + 1) w ∧ M.AgreeBelow i w prev)

Reading the blocks of a walk

theorem DescriptiveComplexity.ATMData.blkLt_iff {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {i j : ℕ} {q : A} (hj : M.Blk j q) : M.BlkLt i q ↔ j < i

Membership in a block below i, once the block is known.

theorem DescriptiveComplexity.ATMData.blkLt_top {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (q : A) : M.BlkLt k q

Every state is in a block below k.

theorem DescriptiveComplexity.ATMData.legalBelow_top_step {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {w : A → Config A} (hw : M.LegalBelow k w) {p q : A} (hpq : SuccPos M.Le M.Posn p q) : M.Step (w p) (w q) ∧ ¬M.Acc (w p).state ∨ w q = w p ∧ (M.Acc (w p).state ∨ M.Stuck (w p))

Below the top block every walk is fully legal: at i = k the restriction in DescriptiveComplexity.ATMData.LegalBelow is no restriction.

theorem DescriptiveComplexity.ATMData.blk_eq_of_entry {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {w : A → Config A} {i : ℕ} (hw : M.LegalBelow i w) {p q : A} (hpq : SuccPos M.Le M.Posn p q) (hp : M.BlkLt i (w p).state) (hq : ¬M.BlkLt i (w q).state) : M.Blk i (w q).state

A walk enters the blocks in order: the first time whose block is not below i is in block i exactly, since the step into it is legal.

theorem DescriptiveComplexity.ATMData.blkLt_of_le {A : Type} {M : ATMData A} {k : ℕ} [Finite A] (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {w : A → Config A} (hmono : M.BlkMono w) {i : ℕ} {s q : A} (hs : M.Posn s) (hq : M.Posn q) (hle : M.Le s q) (h : M.BlkLt i (w q).state) : M.BlkLt i (w s).state

The times of the low blocks form a prefix.

The game

def DescriptiveComplexity.ATMData.gameFrom {A : Type} (M : ATMData A) (start : Bool) (i : ℕ) : ℕ → (A → Config A) → Prop

The game from round i on, with m rounds still to play and prev the walk the previous round produced: the owner of block i chooses a walk subject to DescriptiveComplexity.ATMData.RoundCond, and play passes to the next block. When no round is left, the walk that remains must accept.

Equations

• One or more equations did not get rendered due to their size.
• M.gameFrom start i 0 x✝ = M.AccAt x✝

def DescriptiveComplexity.ATMData.AltGame {A : Type} (M : ATMData A) (start : Bool) : ℕ → Prop

The whole k-round game. The first round is free – there is nothing committed yet – so it is peeled off; every later round inherits from the one before it.

Equations

• One or more equations did not get rendered due to their size.
• M.AltGame start 0 = False

theorem DescriptiveComplexity.ATMData.altGame_eq_gameFrom {A : Type} {M : ATMData A} (start : Bool) (m : ℕ) (prev : A → Config A) : M.AltGame start (m + 1) ↔ M.gameFrom start 0 (m + 1) prev

The first round of the game is the general round with any predecessor: agreement below block 0 is vacuous.

A finished run plays itself out

theorem DescriptiveComplexity.ATMData.gameFrom_of_blkLt {A : Type} {M : ATMData A} (start : Bool) (m i : ℕ) (prev : A → Config A) : M.LegalBelow i prev → (∀ (s : A), M.Posn s → M.BlkLt i (prev s).state) → (M.gameFrom start i m prev ↔ M.AccAt prev)

Once every time is in a low block the game is decided: each remaining round can only copy what it inherited, so the outcome is whether the walk accepts.