The rounds, one block at a time

The induction that turns the machine into the quantifier prefix. Round m starts at DescriptiveComplexity.AtRound: the head at the first cell, the tape holding what the blocks below m have written, and the state the entry of sweep m – or, when every block has played, the entry of the check phase.

Each round is answered by whichever player owns its block, and the four corners were built in AltGuess: an existential round picks an assignment (altAcc_passes_up) and any accepting run of it hands one over (exit_of_altAcc); a universal round survives all of them (altAcc_of_inSweepR) and is followed along the run of any given one (altAcc_passes_down). The base case is the check phase, decided both ways in AltVerdict.

The read-off returns some assignment, not a chosen one, which is what an existential round wants and a universal one does not. So a universal round does not follow the read-off at all: it names the configuration it wants to hand over (DescriptiveComplexity.exists_atRound) and appeals to the fact that every successor of a universal configuration accepts.

Where the machine stands between rounds

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

The entry of round m: the head at the first cell, the tape holding what the blocks below m wrote, and the state the entry of sweep m – or, once every block has played, the entry of the check phase, or acceptance outright when there is nothing to check.

Equations

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

theorem DescriptiveComplexity.AltQbf.atRound_of_afterSweep {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {ρ : Fin k → A → Prop} {c : Config (AltV k A)} (h : AfterSweep cnf i ρ c) : AtRound cnf (↑i + 1) ρ c

A round hands over to the next one.

theorem DescriptiveComplexity.AltQbf.eq_confSweep_of_atRound {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {m : ℕ} {νs : Fin k → A → Prop} {c : Config (AltV k A)} (i : Fin k) (hi : ↑i = m) (h : AtRound cnf m νs c) : c = confSweep νs i.castSucc (posCell qbotA)

Before the last block has played, the entry of a round is the entry of its sweep.

theorem DescriptiveComplexity.AltQbf.exists_atRound {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {m : ℕ} (hm : m ≤ k) (νs : Fin k → A → Prop) (hover : m = k → CanHandOver k A cnf) : ∃ (c : Config (AltV k A)), AtRound cnf m νs c

The entry of a round exists. Before the last block has played it is the entry of the next sweep; after it, the check phase starts at the lowest clause, or the machine accepts outright when there is nothing to check.

theorem DescriptiveComplexity.AltQbf.step_handover {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} {i : Fin k} {ρ : Fin k → A → Prop} {d : Config (AltV k A)} (h : AtRound cnf (↑i + 1) ρ d) : (altMachine k A cnf).Step (confBack ρ i.castSucc posStart) d

The handover step. Whatever the entry of the next round is, the machine reaches it from the left marker in one step.

theorem DescriptiveComplexity.AltQbf.canHandOver_of_qbfMatrix {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] {cnf : Bool} {ρ : Fin k → A → Prop} (hmat : QbfMatrix cnf ρ) : CanHandOver k A cnf

A satisfied matrix leaves the last sweep somewhere to go.

theorem DescriptiveComplexity.AltQbf.confSweep_update_self {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {i : Fin k} {ν : A → Prop} (νs : Fin k → A → Prop) : confSweep (Function.update νs i ν) i.castSucc (posCell qbotA) = confSweep νs i.castSucc (posCell qbotA)

Replacing a block's assignment does not change the tape its own sweep starts from.

The budget

A round costs a sweep, and a universal round costs a walk up and back down the tape once for each of the two passes, whatever the play.

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

What one round costs: exactly the sweep it plays, whichever player owns it.

Equations

• DescriptiveComplexity.AltQbf.roundStep k A = DescriptiveComplexity.AltQbf.sweepLen k A

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

What the last r rounds cost, the check phase included.

Equations

• DescriptiveComplexity.AltQbf.roundBound k A 0 = DescriptiveComplexity.AltQbf.chkLen k A
• DescriptiveComplexity.AltQbf.roundBound k A r.succ = DescriptiveComplexity.AltQbf.roundBound k A r + DescriptiveComplexity.AltQbf.roundStep k A

The induction over rounds

theorem DescriptiveComplexity.AltQbf.rounds {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (r m : ℕ) : m + r = k → ∀ (νs : Fin k → A → Prop) (c : Config (AltV k A)), AtRound cnf m νs c → (∀ (n : ℕ), (altMachine k A cnf).AltAcc start n c → AltTail (QbfMatrix cnf) r m νs (blockPol start m)) ∧ (AltTail (QbfMatrix cnf) r m νs (blockPol start m) → ∀ (n : ℕ), roundBound k A r ≤ n → (altMachine k A cnf).AltAcc start n c)

The machine plays the quantifier prefix. At the entry of round m, the machine accepts exactly when the r blocks still to play can settle the matrix – the round's own block quantified at the polarity its index gives it.

Both directions of both polarities are one line each, on top of the four corners of AltGuess: the existential player picks and climbs, the universal player is followed down one play at a time and survives all of them.

The whole run

The first sweep starts at the left marker rather than at the first cell, so the run has one step to take before round 0 begins. It is a forced step – the machine reads ⊢, which is not a guess – so it costs one unit of budget and nothing else.

theorem DescriptiveComplexity.AltQbf.eq_init_of_isInit {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} (νs : Fin k → A → Prop) {c : Config (AltV k A)} (hinit : (altMachine k A cnf).IsInit c) : c = confSweep νs 0 posStart

The machine has one initial configuration.

theorem DescriptiveComplexity.AltQbf.step_init_det {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf : Bool} (hk : 0 < k) (νs : Fin k → A → Prop) (c'' : Config (AltV k A)) : (altMachine k A cnf).Step (confSweep νs 0 posStart) c'' → c'' = confSweep νs 0 (posCell qbotA)

The step over the left marker is forced: the machine reads ⊢, and only one transition applies.

theorem DescriptiveComplexity.AltQbf.stepForced_init {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (hk : 0 < k) (νs : Fin k → A → Prop) : StepForced (altMachine k A cnf) start (confSweep νs 0 posStart) (confSweep νs 0 (posCell qbotA))

The step over the left marker descends whatever the polarity.

theorem DescriptiveComplexity.AltQbf.altAcc_init_iff {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (hk : 0 < k) (νs : Fin k → A → Prop) (n : ℕ) : (altMachine k A cnf).AltAcc start (n + 1) (confSweep νs 0 posStart) ↔ (altMachine k A cnf).AltAcc start n (confSweep νs 0 (posCell qbotA))

The run before round 0: one forced step.

theorem DescriptiveComplexity.AltQbf.altAccepts_iff_altQuant {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (hk : 0 < k) (hbudget : roundBound k A k + 1 ≤ Nat.card { p : AltV k A // AltPosn p } - 1) : (altMachine k A cnf).AltAccepts start ↔ altQuant A k (QbfMatrix cnf) start

The machine plays the formula. Acceptance of the alternating machine is the alternating quantification of the matrix over the k blocks – provided the tape is long enough to hold the run, which DescriptiveComplexity.alt_budget guarantees.

The tape is long enough

The k rounds cost one sweep each and the check one sweep per clause, which is what DescriptiveComplexity.alt_budget was proved for: the filler positions alone outnumber them.

theorem DescriptiveComplexity.AltQbf.roundBound_eq {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (r : ℕ) : roundBound k A r = chkLen k A + r * sweepLen k A

theorem DescriptiveComplexity.AltQbf.roundBound_lt_card {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : roundBound k A k + 1 ≤ Nat.card { p : AltV k A // AltPosn p } - 1

The whole run fits in the budget.

theorem DescriptiveComplexity.AltQbf.altAccepts_iff_qbf {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {cnf start : Bool} (hk : 0 < k) : (altMachine k A cnf).AltAccepts start ↔ altQuant A k (QbfMatrix cnf) start

The machine of a quantified Boolean formula accepts exactly when the formula is true. The semantic half of QBF k ≤ᶠᵒ[≤] ATMAccept k: what is left is to write the machine down in first-order logic.