The check phase decides the matrix

DescriptiveComplexity.accepts_from_chk_cnf and its disjunctive twin build an accepting run when the matrix holds. This is the converse: if the check phase accepts, the matrix holds. Together they say that the tape the sweeps leave behind is tested exactly.

The check phase is deterministic, so no read-off is needed: acceptance descends along its unique run whatever the polarity of the block it sits in (DescriptiveComplexity.StepForced), and each sweep can only end in one of the two turns. The turn that accepts 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 – and that is precisely the semantic conclusion. The turn that moves on fires at the flag true, and hands the argument to the next clause.

The induction is therefore over the clauses, upwards, exactly as in the two forward lemmas: DescriptiveComplexity.ChkOk is what the run from a clause proves about that clause and every clause above it.

What a check sweep proves

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

Some literal of the clause c is good: satisfied, for a conjunctive matrix; violated, for a disjunctive one.

Equations

• DescriptiveComplexity.AltQbf.QChkGood k cnf νs c = ∃ (y : A), DescriptiveComplexity.AltQbf.QGood k cnf c y (DescriptiveComplexity.AltQbf.chkVal νs y)

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

What the check phase has left to prove when it reaches the clause c: that every clause from c up is satisfied, or that some term from c up has no violated literal.

Equations

• DescriptiveComplexity.AltQbf.ChkOk k true νs c = ∀ (e : A), DescriptiveComplexity.AltQbf.QbfCl k e → c ≤ e → DescriptiveComplexity.AltQbf.QChkGood k true νs e
• DescriptiveComplexity.AltQbf.ChkOk k false νs c = ∃ (e : A), DescriptiveComplexity.AltQbf.QbfCl k e ∧ c ≤ e ∧ ¬DescriptiveComplexity.AltQbf.QChkGood k false νs e

Elementary facts about check configurations

theorem DescriptiveComplexity.AltQbf.not_acc_stChk {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf f d : Bool} {c : A} : ¬(altMachine k A cnf).Acc (stChk f d c)

A checking state is not accepting.

theorem DescriptiveComplexity.AltQbf.stChk_eq_iff {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {f d f' d' : Bool} {c c' : A} : stChk f d c = stChk f' d' c' ↔ f = f' ∧ d = d' ∧ c = c'

Checking states are told apart by their flag, their direction and their clause.

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

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

theorem DescriptiveComplexity.AltQbf.stepForced_of_inCheck {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} {c c' : Config (AltV k A)} (hP : InCheck c) (hnacc : ¬(altMachine k A cnf).Acc c.state) (hstep : (altMachine k A cnf).Step c c') : StepForced (altMachine k A cnf) start c c'

Every step of the check phase is forced: it is the only one available, so acceptance descends along it whatever the polarity of the block.

theorem DescriptiveComplexity.AltQbf.exists_step_of_altAcc {k : ℕ} {A : Type} {M : ATMData (AltV k A)} {start : Bool} {n : ℕ} {c : Config (AltV k A)} (hnacc : ¬M.Acc c.state) (hacc : M.AltAcc start n c) : ∃ (c' : Config (AltV k A)) (m : ℕ), M.Step c c' ∧ M.AltAcc start m c'

A configuration that accepts and is not accepting outright has an accepting successor, whichever player owns it.

Descending a check sweep

theorem DescriptiveComplexity.AltQbf.altAcc_chkR_posEnd {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf start : Bool} {c : A} (hc : QbfCl k c) {n : ℕ} (hacc : (altMachine k A cnf).AltAcc start n (confChkR cnf νs c (posCell qbotA))) : ∃ (m : ℕ), (altMachine k A cnf).AltAcc start m (confChkR cnf νs c posEnd)

A rightward check sweep reaches the right marker.

theorem DescriptiveComplexity.AltQbf.altAcc_chkL_posStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf start : Bool} {c : A} (hc : QbfCl k c) {n : ℕ} (hacc : (altMachine k A cnf).AltAcc start n (confChkL cnf νs c (posCell qtopA))) : ∃ (m : ℕ), (altMachine k A cnf).AltAcc start m (confChkL cnf νs c posStart)

A leftward check sweep reaches the left marker.

What the turn says

theorem DescriptiveComplexity.AltQbf.turn_of_step_chkR {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} {c' : Config (AltV k A)} (hstep : (altMachine k A cnf).Step (confChkR cnf νs c posEnd) c') : (QChkGood k cnf νs c ∧ ∃ (e : A), QbfNextCl k c e ∧ c' = confChkL cnf νs e (posCell qtopA)) ∨ chkFlagR cnf νs c posEnd = cnf ∧ (cnf = true → QbfMaxCl k c)

The turn at the right marker, read backwards. Either the clause has a good literal and the run moves on to the next one, or the flag settles the run and the semantics of the matrix is decided on the spot.

theorem DescriptiveComplexity.AltQbf.turn_of_step_chkL {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} {c' : Config (AltV k A)} (hstep : (altMachine k A cnf).Step (confChkL cnf νs c posStart) c') : (QChkGood k cnf νs c ∧ ∃ (e : A), QbfNextCl k c e ∧ c' = confChkR cnf νs e (posCell qbotA)) ∨ chkFlagL cnf νs c posStart = cnf ∧ (cnf = true → QbfMaxCl k c)

The turn at the left marker, read backwards.

Putting the clauses together

theorem DescriptiveComplexity.AltQbf.chkOk_of_flag {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {νs : Fin k → A → Prop} {cnf : Bool} {c : A} (hc : QbfCl k c) (hmax : cnf = true → QbfMaxCl k c) (hgood : QChkGood k cnf νs c ↔ cnf = true) : ChkOk k cnf νs c

What the accepting turn says: the clause settles the run, so it is the last one that matters.

theorem DescriptiveComplexity.AltQbf.chkOk_of_next {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {νs : Fin k → A → Prop} {cnf : Bool} {c e : A} (hnext : QbfNextCl k c e) (hgood : QChkGood k cnf νs c) (hok : ChkOk k cnf νs e) : ChkOk k cnf νs c

What the turn to the next clause says: this clause is good, and the run goes on to settle the ones above it.

theorem DescriptiveComplexity.AltQbf.chkOk_of_altAcc {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf start : Bool} (c : A) : QbfCl k c → (∀ (n : ℕ), (altMachine k A cnf).AltAcc start n (confChkR cnf νs c (posCell qbotA)) → ChkOk k cnf νs c) ∧ ∀ (n : ℕ), (altMachine k A cnf).AltAcc start n (confChkL cnf νs c (posCell qtopA)) → ChkOk k cnf νs c

The check phase decides the matrix. Whichever sweep it is on and whichever clause it has reached, an accepting run proves that clause and every clause above it settled.

The check's literal test is the matrix's

theorem DescriptiveComplexity.AltQbf.xorB_true (v : Bool) : xorB true v = v

theorem DescriptiveComplexity.AltQbf.xorB_false (v : Bool) : xorB false v = !v

theorem DescriptiveComplexity.AltQbf.chkVal_eq_true {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} : chkVal νs x = true ↔ qbfVal νs x

theorem DescriptiveComplexity.AltQbf.chkVal_eq_false {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {x : A} : chkVal νs x = false ↔ ¬qbfVal νs x

theorem DescriptiveComplexity.AltQbf.qChkGood_true_iff {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {c : A} : QChkGood k true νs c ↔ ∃ (x : A), QbfPos k c x ∧ qbfVal νs x ∨ QbfNeg k c x ∧ ¬qbfVal νs x

A conjunctive clause is good exactly when the assignment satisfies one of its literals.

theorem DescriptiveComplexity.AltQbf.not_qChkGood_false_iff {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {c : A} : ¬QChkGood k false νs c ↔ ∀ (x : A), (QbfPos k c x → qbfVal νs x) ∧ (QbfNeg k c x → ¬qbfVal νs x)

A disjunctive term has no violated literal exactly when the assignment satisfies all of them.

theorem DescriptiveComplexity.AltQbf.chkOk_iff_qbfMatrix {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] {νs : Fin k → A → Prop} {cnf : Bool} {c₀ : A} (hmin : QbfMinCl k c₀) : ChkOk k cnf νs c₀ ↔ QbfMatrix cnf νs

What the check phase tests is the matrix.

The check phase, both ways

What the last round hands over: from the entry of the check phase the machine accepts exactly when the matrix holds of the tape the sweeps have written.

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

A generous bound on the length of the check phase: one sweep per clause.

Equations

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

theorem DescriptiveComplexity.AltQbf.qbfMatrix_of_altAcc {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf start : Bool} {c₀ : A} (hmin : QbfMinCl k c₀) {n : ℕ} (hacc : (altMachine k A cnf).AltAcc start n (confChkR cnf νs c₀ (posCell qbotA))) : QbfMatrix cnf νs

The check phase proves the matrix.

theorem DescriptiveComplexity.AltQbf.altAcc_of_qbfMatrix {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {cnf start : Bool} {c₀ : A} (hmin : QbfMinCl k c₀) (hmat : QbfMatrix cnf νs) {n : ℕ} (hn : chkLen k A ≤ n) : (altMachine k A cnf).AltAcc start n (confChkR cnf νs c₀ (posCell qbotA))

The matrix makes the check phase accept, at either polarity of the block it sits in, since the phase is deterministic.