Reading a block's assignment off an arbitrary run

The direction a universal round needs. DescriptiveComplexity.steps_sweep exhibits the run of a sweep against a given assignment; a universal player must be answered for every play of its block, so the converse is needed: whatever the machine does during sweep i, it is the intended run of some assignment of block i.

The invariant is DescriptiveComplexity.InSweepR: at every moment of the rightward pass the tape is tapeAfter (Function.update νs i ν') (i+1) for the ν' the sweep has written so far, which is supported strictly below the head. Cells at or above the head are therefore untouched – ν' is false there, and DescriptiveComplexity.valAfter_update_succ collapses the disjunction back to the old value – so one statement covers the whole pass rather than needing a separate “below the head” clause.

The only two transitions that can fire at a cell are tGKeep, which changes nothing, and tGSet, which adds the cell's variable to ν'. That the machine has no other choice is DescriptiveComplexity.altTr_unique.

Comparing tapes

theorem DescriptiveComplexity.AltQbf.tapeAfter_congr_at {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ρ σ : Fin k → A → Prop} {m m' : ℕ} {r : AltV k A} (h : valAfter ρ m (r.2 0) = valAfter σ m' (r.2 0)) : tapeAfter ρ m r = tapeAfter σ m' r

Two tapes agree at a tuple as soon as they give its variable the same value.

The invariant of a rightward pass

def DescriptiveComplexity.AltQbf.InSweepR {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

What is true at every moment of the rightward pass of sweep i. The witness ν' is what the sweep has written so far: a set of variables block i marks, all of them strictly below the head. The head itself lies between the first cell and the right marker, which is what says that the machine still has a move: above the right marker the tape is blank, and no transition reads a blank.

Equations

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

theorem DescriptiveComplexity.AltQbf.valAfter_update_bot {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] {νs : Fin k → A → Prop} {i : Fin k} {x : A} : valAfter (Function.update νs i fun (x : A) => False) (↑i + 1) x = valAfter νs (↑i) x

Writing nothing in block i leaves the tape where the sweeps below it left it.

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

The pass starts with nothing written.

What the tape says about the head

theorem DescriptiveComplexity.AltQbf.tapeAfter_head_cases {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m : ℕ} {ρ : Fin k → A → Prop} {r : AltV k A} (hr : AltPosn r) : r.1.1 = AltBase.pStart ∧ tapeAfter ρ m r = symStart ∨ r.1.1 = AltBase.pEnd ∧ tapeAfter ρ m r = symEnd ∨ r.1.1 = AltBase.pCell ∧ tapeAfter ρ m r = symV (valAfter ρ m (r.2 0)) (r.2 0) ∨ tapeAfter ρ m r = symBlank

The four kinds of symbol a position can hold.

theorem DescriptiveComplexity.AltQbf.head_eq_posStart {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m : ℕ} {ρ : Fin k → A → Prop} {r : AltV k A} (hr : AltPosn r) (h : tapeAfter ρ m r = symStart) : r = posStart

Reading the left marker pins the head.

theorem DescriptiveComplexity.AltQbf.head_eq_posEnd {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m : ℕ} {ρ : Fin k → A → Prop} {r : AltV k A} (hr : AltPosn r) (h : tapeAfter ρ m r = symEnd) : r = posEnd

Reading the right marker pins the head.

theorem DescriptiveComplexity.AltQbf.head_eq_posCell {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m : ℕ} {ρ : Fin k → A → Prop} {r : AltV k A} {b : Bool} {x : A} (hr : AltPosn r) (h : tapeAfter ρ m r = symV b x) : r = posCell x ∧ b = valAfter ρ m x

Reading a cell's symbol pins the head to that cell.

Writing one cell

theorem DescriptiveComplexity.AltQbf.altPosn_of_isCellTup {k : ℕ} {A : Type} [LinearOrder A] {r : AltV k A} (hb : r.1.1 = AltBase.pCell) (h : IsCellTup r) : AltPosn r

A tuple with a cell's tag and a cell's shape is a position.

theorem DescriptiveComplexity.AltQbf.tapeAfter_congr_off {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {ρ σ : Fin k → A → Prop} {m m' : ℕ} {r : AltV k A} (h : r.1.1 = AltBase.pCell → IsCellTup r → valAfter ρ m (r.2 0) = valAfter σ m' (r.2 0)) : tapeAfter ρ m r = tapeAfter σ m' r

Two tapes agree at a tuple as soon as they agree at it when it is a real cell: a junk cell reads false on either.

theorem DescriptiveComplexity.AltQbf.tapeAfter_set {k : ℕ} {A : Type} [(FirstOrder.Language.qbf k).Structure A] [LinearOrder A] [Finite A] [Nonempty A] {νs : Fin k → A → Prop} {i : Fin k} {ν' : A → Prop} {x : A} {T T' : AltV k A → AltV k A} (hblk : QbfBlk i x) (hT : T = tapeAfter (Function.update νs i ν') (↑i + 1)) (hx : T' (posCell x) = symV true x) (hframe : ∀ (r : AltV k A), r ≠ posCell x → T' r = T r) : T' = tapeAfter (Function.update νs i fun (y : A) => ν' y ∨ y = x) (↑i + 1)

Setting one cell adds one variable to the block's assignment. This is the only computation the read-off of a sweep performs: the cell of x turns from false to true, and every other tuple is left alone – a real cell because its variable is not x, a junk one because it reads false regardless.

One step of the pass

def DescriptiveComplexity.AltQbf.InSweepL {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

What is true at every moment of the leftward pass: the sweep is over, the tape holds what it wrote, and the head is on its way back down from the last cell.

Equations

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

theorem DescriptiveComplexity.AltQbf.supp_step {k : ℕ} {A : Type} [LinearOrder A] {p q r : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hle : tagTupleLe r p) : tagTupleLe r q ∧ r ≠ q

Moving the head up keeps everything already written below it.

theorem DescriptiveComplexity.AltQbf.bitRank_lt_of_succPos {k : ℕ} {A : Type} [LinearOrder A] [Finite A] {p q : AltV k A} (h : SuccPos tagTupleLe AltPosn p q) : bitRank tagTupleLe AltPosn p < bitRank tagTupleLe AltPosn q

A step up raises the rank.

theorem DescriptiveComplexity.AltQbf.posCell_ne_posEnd {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : posCell x ≠ posEnd

A cell is not the right marker.

theorem DescriptiveComplexity.AltQbf.le_posEnd_of_succPos {k : ℕ} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {p q : AltV k A} (hsucc : SuccPos tagTupleLe AltPosn p q) (hle : tagTupleLe p posEnd) (hne : p ≠ posEnd) : tagTupleLe q posEnd

The head cannot step over the right marker. Anything strictly below it has its successor at or below it, since a successor admits nothing strictly between.

theorem DescriptiveComplexity.AltQbf.inSweepR_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 : InSweepR i νs c) (hstep : (altMachine k A cnf).Step c c') : InSweepR i νs c' ∧ bitRank tagTupleLe AltPosn c.head < bitRank tagTupleLe AltPosn c'.head ∨ InSweepL i νs c'

One step of the rightward pass, whatever the machine chooses. Only three transitions can fire once the pass has left the left marker: the turn at the right one changes nothing, tGKeep leaves the cell alone, and tGSet adds its variable to what the block has assigned. The head moves up until the turn, which is what makes the pass terminate.

Where a sweep hands over

def DescriptiveComplexity.AltQbf.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)) : Prop

What the machine has reached once the sweep of index i is over: the head is back at the first cell and the tape holds what the block wrote. The state is the entry of the next sweep, or – after the last one – the entry of the check phase, or acceptance outright, an instance with no clause at all being satisfied by a conjunctive matrix.

Equations

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

theorem DescriptiveComplexity.AltQbf.inSweepL_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 : InSweepL i νs c) (hstep : (altMachine k A cnf).Step c c') : InSweepL i νs c' ∧ bitRank tagTupleLe AltPosn c'.head < bitRank tagTupleLe AltPosn c.head ∨ ∃ (ν' : A → Prop), (∀ (x : A), ν' x → QbfBlk i x) ∧ AfterSweep cnf i (Function.update νs i ν') c'

One step of the leftward pass, whatever the machine chooses. Only four transitions can fire from a leftward sweeping state, and none of them writes: tGBack walks the cells back, and the three that fire at the left marker hand the tape over – to the next sweep, to the check phase, or to acceptance.