A round of the game, played by either player

What a sweep amounts to, whichever player owns its block. Its moves are exactly the truth assignments of the block: for an existential block the machine picks one, for a universal block it must survive all of them, and DescriptiveComplexity.AltQbf.inSweepR_step / DescriptiveComplexity.AltQbf.inSweepL_step say that every play is the run of some assignment.

The universal half needs two things beyond the read-off. The sweep is never stuck (DescriptiveComplexity.AltQbf.exists_step_of_inSweepR, DescriptiveComplexity.AltQbf.exists_step_of_inSweepL) – at a cell it may keep or set the value, at the markers it turns or hands over – and it terminates, the head moving up until the turn and down afterwards. Both are needed because a universal configuration accepts only when it has a successor and all of them accept, so an induction on the budget alone would never reach its base case.

The one place the handover can genuinely be stuck is the left marker of the last sweep, where the machine passes to the check phase: a disjunctive matrix with no term at all has nothing to check and nothing to accept. That is DescriptiveComplexity.AltQbf.CanHandOver, and it is exactly the case where the formula is false.

The block of a sweeping state

The sweep is never stuck

theorem DescriptiveComplexity.AltQbf.exists_step_of_inSweepR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {νs : Fin k → A → Prop} {c : Config (AltV k A)} (hinv : InSweepR i νs c) : ∃ (c' : Config (AltV k A)), (altMachine k A cnf).Step c c'

The rightward pass always has a move: at a cell it keeps the value it reads, and at the right marker it turns.

def DescriptiveComplexity.AltQbf.CanHandOver (k : ℕ) (A : Type) [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] (cnf : Bool) : Prop

The last sweep can hand over: either there is a clause to check, or there is none and the matrix is conjunctive, so the machine accepts outright. This fails only for a disjunctive matrix with no term, which is the false formula.

Equations

• DescriptiveComplexity.AltQbf.CanHandOver k A cnf = ((∃ (c₀ : A), DescriptiveComplexity.AltQbf.QbfMinCl k c₀) ∨ cnf = true ∧ ∀ (e : A), ¬DescriptiveComplexity.AltQbf.QbfCl k e)

theorem DescriptiveComplexity.AltQbf.exists_step_of_inSweepL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {νs : Fin k → A → Prop} {c : Config (AltV k A)} (hinv : InSweepL i νs c) (hover : ↑i + 1 = k → CanHandOver k A cnf) : ∃ (c' : Config (AltV k A)), (altMachine k A cnf).Step c c'

The leftward pass always has a move, given that the handover is available: at a cell it steps back, at the left marker it passes the tape on.

A universal round survives every play

Two inductions, one per pass, on the only quantity that changes monotonically: the rank of the head, which rises during the rightward pass and falls during the leftward one. The budget is threaded through as a bound rather than as a step count, since a universal player is answered by all plays at once and there is no single run to count.

Following a run of universal configurations

A universal configuration accepts only if every successor does, so acceptance descends along any run that stays universal – in particular along the intended run of a given assignment, which is how a universal round is read for one play at a time. These mirror DescriptiveComplexity.TMData.stepsIn_of_segment and its downward twin, and could be hoisted beside them.

A universal round, followed for one assignment at a time

noncomputable def DescriptiveComplexity.AltQbf.passLen (k : ℕ) (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ℕ

The steps a sweep takes before handing over: up to the right marker, round, and back to the left one.

Equations

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

theorem DescriptiveComplexity.AltQbf.sweepLen_eq_passLen {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : sweepLen k A = passLen k A + 1

Following a run of existential configurations

The mirror of the descent: an existential configuration accepts as soon as one successor does, so acceptance climbs back up any run whose configurations all belong to the machine. This is how an existential round plays the assignment it has chosen.

An existential round, and reading any round off an accepting run