The check phase decides the matrix

DescriptiveComplexity.AltQbf.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.AltQbf.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.AltQbf.ChkOk is what the run from a clause proves about that clause and every clause above it.

What a check sweep proves

Elementary facts about check configurations

Descending a check sweep

What the turn says

Putting the clauses together

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

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.