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.inSweepR_step / DescriptiveComplexity.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.exists_step_of_inSweepR, DescriptiveComplexity.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.CanHandOver, and it is exactly the case where the formula is false.

The block of a sweeping state

theorem DescriptiveComplexity.AltQbf.isUniv_stG {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {d : Bool} : (altMachine k A cnf).IsUniv start (stG i.castSucc d) ↔ blockPol start ↑i = false

A sweeping state is universal exactly when its block is.

The sweep is never stuck

theorem DescriptiveComplexity.AltQbf.posn_le_posCell_cases {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hp : AltPosn p) (hle : tagTupleLe p (posCell qtopA)) : p = posStart ∨ p = posCell (p.2 0)

A position at or below the last cell is the left marker or a cell.

theorem DescriptiveComplexity.AltQbf.posn_between_cases {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hp : AltPosn p) (hlo : tagTupleLe (posCell qbotA) p) (hhi : tagTupleLe p posEnd) : p = posCell (p.2 0) ∨ p = posEnd

A position between the first cell and the right marker is a cell or the right marker.

theorem DescriptiveComplexity.AltQbf.not_maxPos_of_ne_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p : AltV k A} (hhi : tagTupleLe p posEnd) (hne : p ≠ posEnd) : ¬MaxPos tagTupleLe AltPosn p

A cell has a position above it: the right marker.

theorem DescriptiveComplexity.AltQbf.not_minPos_posCell {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : ¬MinPos tagTupleLe AltPosn (posCell x)

A cell has a position below it: the left marker.

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.

noncomputable def DescriptiveComplexity.AltQbf.altNumPos (k : ℕ) (A : Type) [LinearOrder A] : ℕ

The number of positions on the tape: the yardstick a sweep is measured against.

Equations

• DescriptiveComplexity.AltQbf.altNumPos k A = Nat.card { p : DescriptiveComplexity.AltQbf.AltV k A // DescriptiveComplexity.AltQbf.AltPosn p }

theorem DescriptiveComplexity.AltQbf.altAcc_of_inSweepL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} {n' : ℕ} (huniv : blockPol start ↑i = false) (hover : ↑i + 1 = k → CanHandOver k A cnf) (hexit : ∀ (ν' : A → Prop) (c : Config (AltV k A)), (∀ (x : A), ν' x → QbfBlk i x) → AfterSweep cnf i (Function.update νs i ν') c → (altMachine k A cnf).AltAcc start n' c) (r n : ℕ) (c : Config (AltV k A)) : InSweepL i νs c → bitRank tagTupleLe AltPosn c.head ≤ r → r + 1 + n' ≤ n → (altMachine k A cnf).AltAcc start n c

The leftward pass of a universal round accepts, given that whatever it hands over accepts.

theorem DescriptiveComplexity.AltQbf.altAcc_of_inSweepR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} {n' : ℕ} (huniv : blockPol start ↑i = false) (hover : ↑i + 1 = k → CanHandOver k A cnf) (hexit : ∀ (ν' : A → Prop) (c : Config (AltV k A)), (∀ (x : A), ν' x → QbfBlk i x) → AfterSweep cnf i (Function.update νs i ν') c → (altMachine k A cnf).AltAcc start n' c) (r n : ℕ) (c : Config (AltV k A)) : InSweepR i νs c → bitRank tagTupleLe AltPosn posEnd - bitRank tagTupleLe AltPosn c.head ≤ r → r + 1 + (bitRank tagTupleLe AltPosn (posCell qtopA) + 1 + n') ≤ n → (altMachine k A cnf).AltAcc start n c

The rightward pass of a universal round accepts. The measure is what the head has left to climb; at the turn the leftward pass takes over, with what it has left to descend. The two together are the length of the sweep, so a universal round costs no more than the run it must survive.

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.

def DescriptiveComplexity.AltQbf.StepForced {k : ℕ} {A : Type} (M : ATMData (AltV k A)) (start : Bool) (c c' : Config (AltV k A)) : Prop

Acceptance descends across a step when the step is not a choice: either the state is universal, and then every successor accepts, or it is the only step available, and then the successor the machine picks is that one.

Equations

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

theorem DescriptiveComplexity.AltQbf.altAcc_down_step {k : ℕ} {A : Type} {M : ATMData (AltV k A)} {start : Bool} {n : ℕ} {c c' : Config (AltV k A)} (hf : StepForced M start c c') (hstep : M.Step c c') (hacc : M.AltAcc start n c) : 1 ≤ n ∧ M.AltAcc start (n - 1) c'

One step down.

theorem DescriptiveComplexity.AltQbf.altAcc_along_segment {k : ℕ} {A : Type} [Finite A] {M : ATMData (AltV k A)} {start : Bool} (hlin : IsLinOrd M.Le) {conf : AltV k A → Config (AltV k A)} {p₀ p₁ : AltV k A} (hp₀ : M.Posn p₀) (hstep : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf p) (conf q)) (hf : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → StepForced M start (conf p) (conf q)) (n : ℕ) (p : AltV k A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.AltAcc start n (conf p₀) → bitRank M.Le M.Posn p - bitRank M.Le M.Posn p₀ ≤ n ∧ M.AltAcc start (n - (bitRank M.Le M.Posn p - bitRank M.Le M.Posn p₀)) (conf p)

Down a rising segment.

theorem DescriptiveComplexity.AltQbf.altAcc_along_segment_down {k : ℕ} {A : Type} [Finite A] {M : ATMData (AltV k A)} {start : Bool} (hlin : IsLinOrd M.Le) {conf : AltV k A → Config (AltV k A)} {p₀ p₁ : AltV k A} (hp₁ : M.Posn p₁) (hstep : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf q) (conf p)) (hf : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → StepForced M start (conf q) (conf p)) (n : ℕ) (p : AltV k A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.AltAcc start n (conf p₁) → bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn p ≤ n ∧ M.AltAcc start (n - (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn p)) (conf p)

Down a falling segment.

A universal round, followed for one assignment at a time

theorem DescriptiveComplexity.AltQbf.not_acc_stG {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin (k + 1)} {d : Bool} : ¬(altMachine k A cnf).Acc (stG i d)

A sweeping state is not accepting.

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

theorem DescriptiveComplexity.AltQbf.altAcc_passes_down {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} (huniv : blockPol start ↑i = false) {n : ℕ} (hacc : (altMachine k A cnf).AltAcc start n (confSweep νs i.castSucc (posCell qbotA))) : passLen k A ≤ n ∧ (altMachine k A cnf).AltAcc start (n - passLen k A) (confBack νs i.castSucc posStart)

A universal round, followed along the run of one assignment. Both passes are runs of universal configurations, so acceptance descends along them: whatever the round's assignment, the configuration it leaves at the left marker accepts too.

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.

theorem DescriptiveComplexity.AltQbf.altAcc_up_step {k : ℕ} {A : Type} {M : ATMData (AltV k A)} {start : Bool} {n : ℕ} {c c' : Config (AltV k A)} (hnu : ¬M.IsUniv start c.state) (hstep : M.Step c c') (hacc : M.AltAcc start n c') : M.AltAcc start (n + 1) c

One step up.

theorem DescriptiveComplexity.AltQbf.altAcc_along_segment_up {k : ℕ} {A : Type} [Finite A] {M : ATMData (AltV k A)} {start : Bool} (hlin : IsLinOrd M.Le) {conf : AltV k A → Config (AltV k A)} {p₀ p₁ : AltV k A} (hp₀ : M.Posn p₀) (hstep : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf p) (conf q)) (hnu : ∀ (p : AltV k A), ¬M.IsUniv start (conf p).state) (n : ℕ) (p : AltV k A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.AltAcc start n (conf p) → M.AltAcc start (n + (bitRank M.Le M.Posn p - bitRank M.Le M.Posn p₀)) (conf p₀)

Up a rising segment.

theorem DescriptiveComplexity.AltQbf.altAcc_along_segment_up_down {k : ℕ} {A : Type} [Finite A] {M : ATMData (AltV k A)} {start : Bool} (hlin : IsLinOrd M.Le) {conf : AltV k A → Config (AltV k A)} {p₀ p₁ : AltV k A} (hp₁ : M.Posn p₁) (hstep : ∀ (p q : AltV k A), SuccPos M.Le M.Posn p q → M.Le p₀ p → M.Le q p₁ → M.Step (conf q) (conf p)) (hnu : ∀ (p : AltV k A), ¬M.IsUniv start (conf p).state) (n : ℕ) (p : AltV k A) : M.Posn p → M.Le p₀ p → M.Le p p₁ → M.AltAcc start n (conf p) → M.AltAcc start (n + (bitRank M.Le M.Posn p₁ - bitRank M.Le M.Posn p)) (conf p₁)

Up a falling segment.

theorem DescriptiveComplexity.AltQbf.altAcc_passes_up {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} (hex : blockPol start ↑i = true) {n : ℕ} (hacc : (altMachine k A cnf).AltAcc start n (confBack νs i.castSucc posStart)) : (altMachine k A cnf).AltAcc start (n + passLen k A) (confSweep νs i.castSucc (posCell qbotA))

An existential round, played along the run of the assignment it picks. The mirror of DescriptiveComplexity.altAcc_passes_down: acceptance at the left marker, where the round hands over, climbs back to its entry.

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

def DescriptiveComplexity.AltQbf.InSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (i : Fin k) (νs : Fin k → A → Prop) (c : Config (AltV k A)) : Prop

Being somewhere in the sweep of round i, on either pass.

Equations

• DescriptiveComplexity.AltQbf.InSweep i νs c = (DescriptiveComplexity.AltQbf.InSweepR i νs c ∨ DescriptiveComplexity.AltQbf.InSweepL i νs c)

theorem DescriptiveComplexity.AltQbf.inSweep_step {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 c' : Config (AltV k A)} (hinv : InSweep i νs c) (hstep : (altMachine k A cnf).Step c c') : InSweep i νs c' ∨ ∃ (ν' : A → Prop), (∀ (x : A), ν' x → QbfBlk i x) ∧ AfterSweep cnf i (Function.update νs i ν') c'

A sweep either continues or hands over, whatever the machine does.

theorem DescriptiveComplexity.AltQbf.state_of_inSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {i : Fin k} {νs : Fin k → A → Prop} {c : Config (AltV k A)} (hinv : InSweep i νs c) : c.state = stG i.castSucc true ∨ c.state = stG i.castSucc false

The state of a sweeping configuration.

theorem DescriptiveComplexity.AltQbf.not_acc_of_inSweep {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 : InSweep i νs c) : ¬(altMachine k A cnf).Acc c.state

A sweeping configuration is not accepting.

theorem DescriptiveComplexity.AltQbf.not_isUniv_of_inSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} {c : Config (AltV k A)} (hex : blockPol start ↑i = true) (hinv : InSweep i νs c) : ¬(altMachine k A cnf).IsUniv start c.state

The moves of an existential round belong to the machine.

theorem DescriptiveComplexity.AltQbf.exit_of_altAcc {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {i : Fin k} {νs : Fin k → A → Prop} (n : ℕ) (c : Config (AltV k A)) : InSweep i νs c → (altMachine k A cnf).AltAcc start n c → ∃ (ν' : A → Prop) (d : Config (AltV k A)), ∃ m < n, (∀ (x : A), ν' x → QbfBlk i x) ∧ AfterSweep cnf i (Function.update νs i ν') d ∧ (altMachine k A cnf).AltAcc start m d

Any accepting run of a round hands over an assignment. Whichever player owns the block, an accepting configuration has an accepting successor – the one it picks, or any of the ones it must survive – and following those successors reaches the handover, since a sweeping state never accepts.