The intended run: the check phase

Once the k sweeps have written DescriptiveComplexity.qbfVal in every cell, the machine walks the clauses one by one, sweeping the tape and accumulating a flag. The tape never changes again, so the frame condition of every step here is rfl.

The flag means two different things, and that is the whole of the disjunctive case. For a conjunctive matrix it records that some literal of the clause is satisfied; for a disjunctive one, that some literal of the term is violated. The two are the same test at the flipped truth value (DescriptiveComplexity.AltQbf.xorB), so one transition family serves both, and the accepting turn fires at the flag cnf: set for a conjunctive matrix, where it means the clause is satisfied, clear for a disjunctive one, where it means no literal of the term is violated.

A sweep alternates direction with each clause, as in DescriptiveComplexity.Problems.Machine.Hardness: the first runs rightwards from the first cell, having been entered by DescriptiveComplexity.AltQbf.step_toChk.

What the check tests

def DescriptiveComplexity.AltQbf.QGood (k : ℕ) {A : Type} [(FirstOrder.Language.qbf k).Structure A] (cnf : Bool) (c x : A) (v : Bool) : Prop

The literal test of the check phase: for a conjunctive matrix, that the cell of x holding v satisfies the clause c; for a disjunctive one, that it violates it.

Equations

• DescriptiveComplexity.AltQbf.QGood k cnf c x v = DescriptiveComplexity.AltQbf.QbfLit k c x (DescriptiveComplexity.AltQbf.xorB cnf v)

noncomputable def DescriptiveComplexity.AltQbf.chkVal {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] (νs : Fin k → A → Prop) (x : A) : Bool

The value the tape holds in the cell of x once every sweep has run.

Equations

• DescriptiveComplexity.AltQbf.chkVal νs x = DescriptiveComplexity.AltQbf.valAfter νs k x

A rightward check sweep

noncomputable def DescriptiveComplexity.AltQbf.chkFlagR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) : Bool

The flag of a rightward check sweep with the head at p: some cell already visited – that is, strictly below p – is good for the clause c.

Equations

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

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

The configuration during a rightward check sweep of the clause c.

Equations

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

A leftward check sweep

noncomputable def DescriptiveComplexity.AltQbf.chkFlagL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] (cnf : Bool) (νs : Fin k → A → Prop) (c : A) (p : AltV k A) : Bool

The flag of a leftward check sweep with the head at p: some cell already visited – that is, strictly above p – is good for the clause c.

Equations

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

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

The configuration during a leftward check sweep of the clause c.

Equations

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

The turns

One clause, checked end to end

Walking the clauses

theorem DescriptiveComplexity.AltQbf.accepts_from_chk_cnf {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} (hcnf : cnf = true) (hsat : ∀ (e : A), QbfCl k e → ∃ (y : A), QGood k cnf e y (chkVal νs y)) (c : A) : QbfCl k c → (∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkL cnf νs c (posCell qtopA)) cfin ∧ AltAccSt cfin.state) ∧ ∃ (n : ℕ) (cfin : Config (AltV k A)), n ≤ {e : A | QbfCl k e ∧ c ≤ e}.ncard * bitRank tagTupleLe AltPosn posEnd ∧ (altMachine k A cnf).StepsIn n (confChkR cnf νs c (posCell qbotA)) cfin ∧ AltAccSt cfin.state

A conjunctive matrix: the machine checks every remaining clause and accepts, in at most one sweep's worth of steps per clause.

A deterministic run accepts at either polarity

The check phase is deterministic, so its run is a legitimate move for the universal player as much as for the existential one: “every successor accepts” and “some successor accepts” say the same thing when there is exactly one.

The check phase is deterministic

The run is short enough

The budget of DescriptiveComplexity.ATMData.AltAccepts counts the positions of the tape, of which the fillers alone supply 8(k+1)n². A sweep, by contrast, costs about as many steps as the instance has elements: only the left marker and the cells lie below the right marker.